add ScopeTerm

src/Quox/Syntax/Term.idr

@@ -36,9 +36,9 @@ mutual
 
     ||| function type
     Pi  : (qtm, qty : Qty) -> (x : Name) ->
-          (arg : Term d n) -> (res : Term d (S n)) -> Term d n
+          (arg : Term d n) -> (res : ScopeTerm d n) -> Term d n
     ||| function term
-    Lam : (x : Name) -> (body : Term d (S n)) -> Term d n
+    Lam : (x : Name) -> (body : ScopeTerm d n) -> Term d n
 
     ||| elimination
     E : (e : Elim d n) -> Term d n
@@ -67,8 +67,36 @@ mutual
     ||| dimension closure/suspended substitution
     DCloE : (el : Elim dfrom n) -> (th : Lazy (DSubst dfrom dto)) -> Elim dto n
 
+  ||| a scope with one more bound variable
+  public export
+  data ScopeTerm : (d, n : Nat) -> Type where
+    ||| variable is used
+    TUsed : (body : Term d (S n)) -> ScopeTerm d n
+    ||| variable is unused
+    TUnused : (body : Term d n) -> ScopeTerm d n
+
+  ||| a scope with one more bound dimension variable
+  public export
+  data DScopeTerm : (d, n : Nat) -> Type where
+    ||| variable is used
+    DUsed : (body : Term (S d) n) -> DScopeTerm d n
+    ||| variable is unused
+    DUnused : (body : Term d n) -> DScopeTerm d n
+
 %name Term s, t, r
 %name Elim e, f
+%name ScopeTerm body
+%name DScopeTerm body
+
+export
+fromDScopeTerm : DScopeTerm d n -> Term (S d) n
+fromDScopeTerm (DUsed   body) = body
+fromDScopeTerm (DUnused body) = body `DCloT` shift 1
+
+export
+fromScopeTerm : ScopeTerm d n -> Term d (S n)
+fromScopeTerm (TUsed   body) = body
+fromScopeTerm (TUnused body) = body `CloT` shift 1
 
 
 ||| same as `F` but as a term
@@ -139,7 +167,7 @@ public export
 (:\\) : Vect m Name -> Term d (m + n) -> Term d n
 []      :\\ t = t
 x :: xs :\\ t = let t' = replace {p = Term _} (plusSuccRightSucc {}) t in
-                Lam x $ xs :\\ t'
+                Lam x $ TUsed $ xs :\\ t'
 
 public export
 record GetLams (d, n : Nat) where
@@ -152,8 +180,8 @@ record GetLams (d, n : Nat) where
 public export
 getLams : Term d n -> GetLams d n
 getLams s with (choose $ isLam s)
-  getLams (Lam x s) | Left yes =
-    let inner = getLams s in
+  getLams s@(Lam x body) | Left yes =
+    let inner = getLams $ assert_smaller s $ fromScopeTerm body in
     GotLams {names  = x :: inner.names,
              body   = inner.body,
              eq     = plusSuccRightSucc {} `trans` inner.eq,
@@ -220,6 +248,10 @@ mutual
       parensIfM SApp . hang 2 =<<
         [|withPrec SApp (prettyM e) </> prettyDSubst th|]
 
+  export covering
+  PrettyHL (ScopeTerm d n) where
+    prettyM body = prettyM $ fromScopeTerm body
+
   export covering
   prettyTSubst : Pretty.HasEnv m => TSubst d from to -> m (Doc HL)
   prettyTSubst s = prettySubstM prettyM (!ask).tnames TVar "[" "]" s
@@ -266,11 +298,18 @@ CanSubst (Elim d) (Term d) where
                          Shift SZ => s
                          th       => CloT s th
 
+export
+CanSubst (Elim d) (ScopeTerm d) where
+  TUsed   body // th = TUsed   $ body // push th
+  TUnused body // th = TUnused $ body // th
+
 export CanSubst Var (Term      d) where s // th = s // map (B {d}) th
 export CanSubst Var (Elim      d) where e // th = e // map (B {d}) th
+export CanSubst Var (ScopeTerm d) where s // th = s // map (B {d}) th
 
-export CanShift (Term d) where i // by = i // Shift by {env = Elim d}
-export CanShift (Elim d) where i // by = i // Shift by {env = Elim d}
+export CanShift (Term      d) where s // by = s // Shift by {env = Elim d}
+export CanShift (Elim      d) where e // by = e // Shift by {env = Elim d}
+export CanShift (ScopeTerm d) where s // by = s // Shift by {env = Elim d}
 
 
 infixl 8 ///
@@ -309,6 +348,20 @@ mutual
            Elim dto to
     subs e th ph = e /// th // ph
 
+  namespace ScopeTerm
+    ||| applies a dimension substitution with the same behaviour as `(//)`
+    ||| above
+    export
+    (///) : ScopeTerm dfrom n -> DSubst dfrom dto -> ScopeTerm dto n
+    TUsed   body /// th = TUsed   $ body /// th
+    TUnused body /// th = TUnused $ body /// th
+
+    ||| applies a term and dimension substitution
+    public export %inline
+    subs : ScopeTerm dfrom from -> DSubst dfrom dto -> TSubst dto from to ->
+           ScopeTerm dto to
+    subs body th ph = body /// th // ph
+
 
 private %inline
 comp' : DSubst dfrom dto -> TSubst dfrom from mid -> TSubst dto mid to ->
@@ -376,10 +429,10 @@ mutual
                     Term dfrom from -> NotCloTerm dto to
   pushSubstsTWith th ph (TYPE l) =
     ncloT $ TYPE l
-  pushSubstsTWith th ph (Pi qtm qty x a b) =
-    ncloT $ Pi qtm qty x (subs a th ph) (subs b th (push ph))
-  pushSubstsTWith th ph (Lam x t) =
-    ncloT $ Lam x $ subs t th $ push ph
+  pushSubstsTWith th ph (Pi qtm qty x a body) =
+    ncloT $ Pi qtm qty x (subs a th ph) (subs body th ph)
+  pushSubstsTWith th ph (Lam x body) =
+    ncloT $ Lam x $ subs body th ph
   pushSubstsTWith th ph (E e) =
     let Element e _ = pushSubstsEWith th ph e in ncloT $ E e
   pushSubstsTWith th ph (CloT  s ps) =
@@ -501,6 +554,12 @@ NonRedexElim : Nat -> Nat -> Type
 NonRedexElim d n = Subset (Elim d n) NotRedexE
 
 
+||| substitute a term with annotation for the bound variable of a `ScopeTerm`
+public export %inline
+substScope : (arg, argTy : Term d n) -> (body : ScopeTerm d n) -> Term d n
+substScope arg argTy (TUsed   body) = body // one (arg :# argTy)
+substScope arg argTy (TUnused body) = body
+
 public export %inline
 stepT' : (s : Term d n) -> IsRedexT s -> Term d n
 stepT' (E (s :# _)) IsUpsilon = s
@@ -514,7 +573,7 @@ stepT s = case isRedexT s of Yes y => Right $ stepT' s y; No n => Left n
 public export %inline
 stepE' : (e : Elim d n) -> IsRedexE e -> Elim d n
 stepE' ((Lam {body, _} :# Pi {arg, res, _}) :@ s) IsBetaLam =
-  (body :# res) // one (s :# arg)
+  substScope s arg body :# substScope s arg res
 stepE' (CloE  e th) IsCloE  = pushSubstsEWith' id th e
 stepE' (DCloE e th) IsDCloE = pushSubstsEWith' th id e