quox/lib/Quox/Syntax/Term/Subst.idr

module Quox.Syntax.Term.Subst

import Quox.No
import Quox.Syntax.Term.Base
import Quox.Syntax.Subst

import Data.SnocVect
import Data.Singleton

%default total


infixl 8 ///

parameters {0 f : Nat -> Nat -> Type}
  private
  th0 : f 0 0 -> Thinned2 f d n
  th0 = Th2 zero zero

  private
  th1 : {d, n : Nat} -> f d n -> Thinned2 f d n
  th1 = Th2 id' id'

private dsubTerm : {d1, d2, n : Nat} -> Term d1 n -> DSubst d1 d2 -> TermT d2 n
private dsubElim : {d1, d2, n : Nat} -> Elim d1 n -> DSubst d1 d2 -> ElimT d2 n

dsubTerm (TYPE l loc) th = th0 $ TYPE l loc
dsubTerm (Enum strs loc) th = th0 $ Enum strs loc
dsubTerm (Tag str loc) th = th0 $ Tag str loc
dsubTerm (Nat loc) th = th0 $ Nat loc
dsubTerm (Zero loc) th = th0 $ Zero loc
dsubTerm (E e) th =
  let Th2 dope tope e' = dsubElim e th in
  Th2 dope tope $ E e'
dsubTerm (DCloT (Sub t ph)) th = th1 $ DCloT $ Sub t $ ph . th
dsubTerm t th = th1 $ DCloT $ Sub t th

dsubElim (F x l loc) th = th0 $ F x l loc
dsubElim (B loc) th = Th2 zero id' $ B loc
dsubElim (DCloE (Sub e ph)) th = th1 $ DCloE $ Sub e $ ph . th
dsubElim e th = th1 $ DCloE $ Sub e th

mutual
  namespace Term
    export
    (///) : {d1, d2, n : Nat} -> TermT d1 n -> DSubst d1 d2 -> TermT d2 n
    Th2 dope tope term /// th =
      let Val tscope = appOpe n tope; Val dscope = appOpe d1 dope
          Th2 dope' tope' term' = dsubTerm term (select dope th)
      in
      Th2 dope' (tope . tope') term'

  namespace Elim
    export
    (///) : {d1, d2, n : Nat} -> ElimT d1 n -> DSubst d1 d2 -> ElimT d2 n
    Th2 dope tope elim /// th =
      let Val tscope = appOpe n tope; Val dscope = appOpe d1 dope
          Th2 dope' tope' elim' = dsubElim elim (select dope th)
      in
      Th2 dope' (tope . tope') elim'


public export
TSubst : Nat -> Nat -> Nat -> Type
TSubst = Subst2 Elim


public export %inline FromVar (Elim 0) where var = B

export CanSubstSelf2 Elim

private subTerm : {d, n1, n2 : Nat} -> Term d n1 -> TSubst d n1 n2 -> TermT d n2
private subElim : {d, n1, n2 : Nat} -> Elim d n1 -> TSubst d n1 n2 -> ElimT d n2

subTerm (TYPE l loc) th = th0 $ TYPE l loc
subTerm (Nat loc) th = th0 $ Nat loc
subTerm (Zero loc) th = th0 $ Zero loc
subTerm (E e) th = let Th2 dope tope e' = subElim e th in Th2 dope tope $ E e'
subTerm (CloT (Sub2 s ph)) th = th1 $ CloT $ Sub2 s $ ph .% th
subTerm s th = th1 $ CloT $ Sub2 s th

subElim (F x k loc) th = th0 $ F x k loc
subElim (B loc) [< e] = e
subElim (CloE (Sub2 e ph)) th = th1 $ CloE $ Sub2 e $ ph .% th
subElim e th = th1 $ CloE $ Sub2 e th



export
CanSubstSelf2 Elim where
  Th2 dope tope elim // th =
    let
        th' = select tope th
    in
    ?sube2

-- namespace CanDSubst
--   public export
--   interface CanDSubst (0 tm : TermLike) where
--     (//) : {d1 : Nat} -> Thinned2 tm d1 n -> Lazy (DSubst d1 d2) ->
--            Thinned2 tm d2 n

-- ||| does the minimal reasonable work:
-- ||| - deletes the closure around an atomic constant like `TYPE`
-- ||| - deletes an identity substitution
-- ||| - composes (lazily) with an existing top-level dim-closure
-- ||| - otherwise, wraps in a new closure
-- export
-- CanDSubst Term where
--   Th2 _ _ (TYPE l loc)       // _        = Th2 zero zero $ TYPE l loc
--   Th2 i j (DCloT (Sub s ph)) // th       =
--     Th2 ?i' j $ DCloT $ Sub s $ ph . ?th'
--   Th2 i j s                  // th       = ?sdf -- DCloT $ Sub s th

-- -- private
-- -- subDArgs : Elim d1 n -> DSubst d1 d2 -> Elim d2 n
-- -- subDArgs (DApp f d loc) th = DApp (subDArgs f th) (d // th) loc
-- -- subDArgs e              th = DCloE $ Sub e th

-- -- ||| does the minimal reasonable work:
-- -- ||| - deletes the closure around a term variable
-- -- ||| - deletes an identity substitution
-- -- ||| - composes (lazily) with an existing top-level dim-closure
-- -- ||| - immediately looks up bound variables in a
-- -- |||   top-level sequence of dimension applications
-- -- ||| - otherwise, wraps in a new closure
-- -- export
-- -- CanDSubst Elim where
-- --   e                // Shift SZ = e
-- --   F x u loc        // _        = F x u loc
-- --   B i loc          // _        = B i loc
-- --   e@(DApp {})      // th       = subDArgs e th
-- --   DCloE (Sub e ph) // th       = DCloE $ Sub e $ ph . th
-- --   e                // th       = DCloE $ Sub e th

-- -- namespace DSubst.ScopeTermN
-- --   export %inline
-- --   (//) : ScopeTermN s d1 n -> Lazy (DSubst d1 d2) ->
-- --          ScopeTermN s d2 n
-- --   S ns (Y body) // th = S ns $ Y $ body // th
-- --   S ns (N body) // th = S ns $ N $ body // th

-- -- namespace DSubst.DScopeTermN
-- --   export %inline
-- --   (//) : {s : Nat} ->
-- --          DScopeTermN s d1 n -> Lazy (DSubst d1 d2) ->
-- --          DScopeTermN s d2 n
-- --   S ns (Y body) // th = S ns $ Y $ body // pushN s th
-- --   S ns (N body) // th = S ns $ N $ body // th


-- -- export %inline FromVar (Elim d) where fromVarLoc = B
-- -- export %inline FromVar (Term d) where fromVarLoc = E .: fromVar


-- -- ||| does the minimal reasonable work:
-- -- ||| - deletes the closure around a *free* name
-- -- ||| - deletes an identity substitution
-- -- ||| - composes (lazily) with an existing top-level closure
-- -- ||| - immediately looks up a bound variable
-- -- ||| - otherwise, wraps in a new closure
-- -- export
-- -- CanSubstSelf (Elim d) where
-- --   F x u loc       // _  = F x u loc
-- --   B i loc         // th = getLoc th i loc
-- --   CloE (Sub e ph) // th = assert_total CloE $ Sub e $ ph . th
-- --   e               // th = case force th of
-- --                                Shift SZ => e
-- --                                th       => CloE $ Sub e th

-- -- namespace CanTSubst
-- --   public export
-- --   interface CanTSubst (0 tm : TermLike) where
-- --     (//) : tm d n1 -> Lazy (TSubst d n1 n2) -> tm d n2

-- -- ||| does the minimal reasonable work:
-- -- ||| - deletes the closure around an atomic constant like `TYPE`
-- -- ||| - deletes an identity substitution
-- -- ||| - composes (lazily) with an existing top-level closure
-- -- ||| - goes inside `E` in case it is a simple variable or something
-- -- ||| - otherwise, wraps in a new closure
-- -- export
-- -- CanTSubst Term where
-- --   TYPE l loc      // _  = TYPE l loc
-- --   E e             // th = E $ e // th
-- --   CloT (Sub s ph) // th = CloT $ Sub s $ ph . th
-- --   s               // th = case force th of
-- --                                Shift SZ => s
-- --                                th       => CloT $ Sub s th

-- -- namespace ScopeTermN
-- --   export %inline
-- --   (//) : {s : Nat} ->
-- --          ScopeTermN s d n1 -> Lazy (TSubst d n1 n2) ->
-- --          ScopeTermN s d n2
-- --   S ns (Y body) // th = S ns $ Y $ body // pushN s th
-- --   S ns (N body) // th = S ns $ N $ body // th

-- -- namespace DScopeTermN
-- --   export %inline
-- --   (//) : {s : Nat} ->
-- --          DScopeTermN s d n1 -> Lazy (TSubst d n1 n2) -> DScopeTermN s d n2
-- --   S ns (Y body) // th = S ns $ Y $ body // map (// shift s) th
-- --   S ns (N body) // th = S ns $ N $ body // th

-- -- export %inline CanShift (Term d) where s // by = s // Shift by
-- -- export %inline CanShift (Elim d) where e // by = e // Shift by

-- -- export %inline
-- -- {s : Nat} -> CanShift (ScopeTermN s d) where
-- --   b // by = b // Shift by


-- -- export %inline
-- -- comp : DSubst d1 d2 -> TSubst d1 n1 mid -> TSubst d2 mid n2 -> TSubst d2 n1 n2
-- -- comp th ps ph = map (// th) ps . ph


-- -- public export %inline
-- -- dweakT : (by : Nat) -> Term d n -> Term (by + d) n
-- -- dweakT by t = t // shift by

-- -- public export %inline
-- -- dweakE : (by : Nat) -> Elim d n -> Elim (by + d) n
-- -- dweakE by t = t // shift by


-- -- public export %inline
-- -- weakT : (by : Nat) -> Term d n -> Term d (by + n)
-- -- weakT by t = t // shift by

-- -- public export %inline
-- -- weakE : (by : Nat) -> Elim d n -> Elim d (by + n)
-- -- weakE by t = t // shift by


-- -- parameters {s : Nat}
-- --   namespace ScopeTermBody
-- --     export %inline
-- --     (.term) : ScopedBody s (Term d) n -> Term d (s + n)
-- --     (Y b).term = b
-- --     (N b).term = weakT s b

-- --   namespace ScopeTermN
-- --     export %inline
-- --     (.term) : ScopeTermN s d n -> Term d (s + n)
-- --     t.term = t.body.term

-- --   namespace DScopeTermBody
-- --     export %inline
-- --     (.term) : ScopedBody s (\d => Term d n) d -> Term (s + d) n
-- --     (Y b).term = b
-- --     (N b).term = dweakT s b

-- --   namespace DScopeTermN
-- --     export %inline
-- --     (.term) : DScopeTermN s d n -> Term (s + d) n
-- --     t.term = t.body.term


-- -- export %inline
-- -- subN : ScopeTermN s d n -> SnocVect s (Elim d n) -> Term d n
-- -- subN (S _ (Y body)) es = body // fromSnocVect es
-- -- subN (S _ (N body)) _  = body

-- -- export %inline
-- -- sub1 : ScopeTerm d n -> Elim d n -> Term d n
-- -- sub1 t e = subN t [< e]

-- -- export %inline
-- -- dsubN : DScopeTermN s d n -> SnocVect s (Dim d) -> Term d n
-- -- dsubN (S _ (Y body)) ps = body // fromSnocVect ps
-- -- dsubN (S _ (N body)) _  = body

-- -- export %inline
-- -- dsub1 : DScopeTerm d n -> Dim d -> Term d n
-- -- dsub1 t p = dsubN t [< p]


-- -- public export %inline
-- -- (.zero) : DScopeTerm d n -> {default noLoc loc : Loc} -> Term d n
-- -- body.zero = dsub1 body $ K Zero loc

-- -- public export %inline
-- -- (.one) : DScopeTerm d n -> {default noLoc loc : Loc} -> Term d n
-- -- body.one = dsub1 body $ K One loc


-- -- public export
-- -- 0 CloTest : TermLike -> Type
-- -- CloTest tm = forall d, n. tm d n -> Bool

-- -- interface PushSubsts (0 tm : TermLike) (0 isClo : CloTest tm) | tm where
-- --   pushSubstsWith : DSubst d1 d2 -> TSubst d2 n1 n2 ->
-- --                    tm d1 n1 -> Subset (tm d2 n2) (No . isClo)

-- -- public export
-- -- 0 NotClo : {isClo : CloTest tm} -> PushSubsts tm isClo => Pred (tm d n)
-- -- NotClo = No . isClo

-- -- public export
-- -- 0 NonClo : (tm : TermLike) -> {isClo : CloTest tm} ->
-- --            PushSubsts tm isClo => TermLike
-- -- NonClo tm d n = Subset (tm d n) NotClo

-- -- public export %inline
-- -- nclo : {isClo : CloTest tm} -> (0 _ : PushSubsts tm isClo) =>
-- --        (t : tm d n) -> (0 nc : NotClo t) => NonClo tm d n
-- -- nclo t = Element t nc

-- -- parameters {0 isClo : CloTest tm} {auto _ : PushSubsts tm isClo}
-- --   ||| if the input term has any top-level closures, push them under one layer of
-- --   ||| syntax
-- --   export %inline
-- --   pushSubsts : tm d n -> NonClo tm d n
-- --   pushSubsts s = pushSubstsWith id id s

-- --   export %inline
-- --   pushSubstsWith' : DSubst d1 d2 -> TSubst d2 n1 n2 -> tm d1 n1 -> tm d2 n2
-- --   pushSubstsWith' th ph x = fst $ pushSubstsWith th ph x

-- --   export %inline
-- --   pushSubsts' : tm d n -> tm d n
-- --   pushSubsts' s = fst $ pushSubsts s

-- -- mutual
-- --   public export
-- --   isCloT : CloTest Term
-- --   isCloT (CloT  {}) = True
-- --   isCloT (DCloT {}) = True
-- --   isCloT (E e)      = isCloE e
-- --   isCloT _          = False

-- --   public export
-- --   isCloE : CloTest Elim
-- --   isCloE (CloE  {}) = True
-- --   isCloE (DCloE {}) = True
-- --   isCloE _          = False

-- -- mutual
-- --   export
-- --   PushSubsts Term Subst.isCloT where
-- --     pushSubstsWith th ph (TYPE l loc) =
-- --       nclo $ TYPE l loc
-- --     pushSubstsWith th ph (Pi qty a body loc) =
-- --       nclo $ Pi qty (a // th // ph) (body // th // ph) loc
-- --     pushSubstsWith th ph (Lam body loc) =
-- --       nclo $ Lam (body // th // ph) loc
-- --     pushSubstsWith th ph (Sig a b loc) =
-- --       nclo $ Sig (a // th // ph) (b // th // ph) loc
-- --     pushSubstsWith th ph (Pair s t loc) =
-- --       nclo $ Pair (s // th // ph) (t // th // ph) loc
-- --     pushSubstsWith th ph (Enum tags loc) =
-- --       nclo $ Enum tags loc
-- --     pushSubstsWith th ph (Tag tag loc) =
-- --       nclo $ Tag tag loc
-- --     pushSubstsWith th ph (Eq ty l r loc) =
-- --       nclo $ Eq (ty // th // ph) (l // th // ph) (r // th // ph) loc
-- --     pushSubstsWith th ph (DLam body loc) =
-- --       nclo $ DLam (body // th // ph) loc
-- --     pushSubstsWith _ _ (Nat loc) =
-- --       nclo $ Nat loc
-- --     pushSubstsWith _ _ (Zero loc) =
-- --       nclo $ Zero loc
-- --     pushSubstsWith th ph (Succ n loc) =
-- --       nclo $ Succ (n // th // ph) loc
-- --     pushSubstsWith th ph (BOX pi ty loc) =
-- --       nclo $ BOX pi (ty // th // ph) loc
-- --     pushSubstsWith th ph (Box val loc) =
-- --       nclo $ Box (val // th // ph) loc
-- --     pushSubstsWith th ph (E e) =
-- --       let Element e nc = pushSubstsWith th ph e in nclo $ E e
-- --     pushSubstsWith th ph (CloT (Sub s ps)) =
-- --       pushSubstsWith th (comp th ps ph) s
-- --     pushSubstsWith th ph (DCloT (Sub s ps)) =
-- --       pushSubstsWith (ps . th) ph s

-- --   export
-- --   PushSubsts Elim Subst.isCloE where
-- --     pushSubstsWith th ph (F x u loc) =
-- --       nclo $ F x u loc
-- --     pushSubstsWith th ph (B i loc) =
-- --       let res = getLoc ph i loc in
-- --       case nchoose $ isCloE res of
-- --         Left  yes => assert_total pushSubsts res
-- --         Right no  => Element res no
-- --     pushSubstsWith th ph (App f s loc) =
-- --       nclo $ App (f // th // ph) (s // th // ph) loc
-- --     pushSubstsWith th ph (CasePair pi p r b loc) =
-- --       nclo $ CasePair pi (p // th // ph) (r // th // ph) (b // th // ph) loc
-- --     pushSubstsWith th ph (CaseEnum pi t r arms loc) =
-- --       nclo $ CaseEnum pi (t // th // ph) (r // th // ph)
-- --                (map (\b => b // th // ph) arms) loc
-- --     pushSubstsWith th ph (CaseNat pi pi' n r z s loc) =
-- --       nclo $ CaseNat pi pi' (n // th // ph) (r // th // ph)
-- --                (z // th // ph) (s // th // ph) loc
-- --     pushSubstsWith th ph (CaseBox pi x r b loc) =
-- --       nclo $ CaseBox pi (x // th // ph) (r // th // ph) (b // th // ph) loc
-- --     pushSubstsWith th ph (DApp f d loc) =
-- --       nclo $ DApp (f // th // ph) (d // th) loc
-- --     pushSubstsWith th ph (Ann s a loc) =
-- --       nclo $ Ann (s // th // ph) (a // th // ph) loc
-- --     pushSubstsWith th ph (Coe ty p q val loc) =
-- --       nclo $ Coe (ty // th // ph) (p // th) (q // th) (val // th // ph) loc
-- --     pushSubstsWith th ph (Comp ty p q val r zero one loc) =
-- --       nclo $ Comp (ty // th // ph) (p // th) (q // th)
-- --                   (val // th // ph) (r // th)
-- --                   (zero // th // ph) (one // th // ph) loc
-- --     pushSubstsWith th ph (TypeCase ty ret arms def loc) =
-- --       nclo $ TypeCase (ty // th // ph) (ret  // th // ph)
-- --         (map (\t => t // th // ph) arms) (def // th // ph) loc
-- --     pushSubstsWith th ph (CloE (Sub e ps)) =
-- --       pushSubstsWith th (comp th ps ph) e
-- --     pushSubstsWith th ph (DCloE (Sub e ps)) =
-- --       pushSubstsWith (ps . th) ph e


-- -- private %inline
-- -- CompHY : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
-- --          (r : Dim d) -> (zero, one : DScopeTerm d n) -> (loc : Loc) -> Elim d n
-- -- CompHY {ty, p, q, val, r, zero, one, loc} =
-- --   let ty' = SY ty.names $ ty.term // (B VZ ty.loc ::: shift 2) in
-- --   Comp {
-- --     ty = dsub1 ty q, p, q,
-- --     val = E $ Coe ty p q val val.loc, r,
-- --     -- [fixme] better locations for these vars?
-- --     zero = SY zero.names $ E $
-- --       Coe ty' (B VZ zero.loc) (weakD 1 q) zero.term zero.loc,
-- --     one = SY one.names $ E $
-- --       Coe ty' (B VZ one.loc) (weakD 1 q) one.term one.loc,
-- --     loc
-- --   }

-- -- public export %inline
-- -- CompH' : (ty : DScopeTerm d n) ->
-- --          (p, q : Dim d) -> (val : Term d n) -> (r : Dim d) ->
-- --          (zero : DScopeTerm d n) ->
-- --          (one : DScopeTerm d n) ->
-- --          (loc : Loc) ->
-- --          Elim d n
-- -- CompH' {ty, p, q, val, r, zero, one, loc} =
-- --   case dsqueeze ty of
-- --     S _ (N ty) => Comp   {ty, p, q, val, r, zero, one, loc}
-- --     S _ (Y _)  => CompHY {ty, p, q, val, r, zero, one, loc}

-- -- ||| heterogeneous composition, using Comp and Coe (and subst)
-- -- |||
-- -- ||| comp [i ⇒ A] @p @q s @r { 0 j ⇒ t₀; 1 j ⇒ t₁ }
-- -- ||| ≔
-- -- ||| comp [A‹q/i›] @p @q (coe [i ⇒ A] @p @q s) @r {
-- -- |||   0 j ⇒ coe [i ⇒ A] @j @q t₀;
-- -- |||   1 j ⇒ coe [i ⇒ A] @j @q t₁
-- -- ||| }
-- -- public export %inline
-- -- CompH : (i : BindName) -> (ty : Term (S d) n) ->
-- --         (p, q : Dim d) -> (val : Term d n) -> (r : Dim d) ->
-- --         (j0 : BindName) -> (zero : Term (S d) n) ->
-- --         (j1 : BindName) -> (one : Term (S d) n) ->
-- --         (loc : Loc) ->
-- --         Elim d n
-- -- CompH {i, ty, p, q, val, r, j0, zero, j1, one, loc} =
-- --   CompH' {ty = SY [< i] ty, p, q, val, r,
-- --           zero = SY [< j0] zero, one = SY [< j0] one, loc}