1 files changed, 77 insertions, 26 deletions
diff --git a/src/Total/Syntax.idr b/src/Total/Syntax.idr
index 6c34250..fead586 100644
--- a/src/Total/Syntax.idr
+++ b/src/Total/Syntax.idr
@@ -5,9 +5,10 @@ import public Data.List.Quantifiers
 import public Data.SnocList
 import public Data.SnocList.Quantifiers
 import public Total.Term
+import public Total.Term.CoDebruijn
 
 infixr 20 ~>*
-infix 9 .*
+infixl 9 .~, .*
 
 public export
 (~>*) : SnocList Ty -> Ty -> Ty
@@ -31,47 +32,97 @@ before Z f x = x
 before (S k) f x = before k f (after k (. f) x)
 
 export
-Lit : Nat -> Term ctx N
-Lit 0 = Zero
-Lit (S n) = Suc (Lit n)
+lit : Len ctx => Nat -> FullTerm N ctx
+lit 0 = Zero `Over` empty
+lit (S n) = suc (lit n)
 
-AbsHelper :
+absHelper :
   (k : Len tys) ->
-  Fun k (flip Elem (ctx ++ tys)) (Term (ctx ++ tys) ty) ->
-  Term ctx (tys ~>* ty)
-AbsHelper Z x = x
-AbsHelper (S k) x =
-  AbsHelper k $
-  after k (\f => Term.Abs (f SnocList.Elem.Here)) $
+  Fun k (flip Elem (ctx ++ tys)) (FullTerm ty (ctx ++ tys)) ->
+  FullTerm (tys ~>* ty) ctx
+absHelper Z x = x
+absHelper (S k) x =
+  absHelper k $
+  after k (\f => CoDebruijn.abs (f SnocList.Elem.Here)) $
   before k SnocList.Elem.There x
 
 export
-Abs' :
+abs' :
+  (len : Len ctx) =>
   (k : Len tys) ->
-  Fun k (Term (ctx ++ tys)) (Term (ctx ++ tys) ty) ->
-  Term ctx (tys ~>* ty)
-Abs' k = AbsHelper k . before k Var
+  Fun k (flip FullTerm (ctx ++ tys)) (FullTerm ty (ctx ++ tys)) ->
+  FullTerm (tys ~>* ty) ctx
+abs' k = absHelper k . before k (var @{lenAppend len k})
 
 export
-App' : {tys : SnocList Ty} -> Term ctx (tys ~>* ty) -> All (Term ctx) tys -> Term ctx ty
-App' t [<] = t
-App' t (us :< u) = App (App' t us) u
+app' :
+  {tys : SnocList Ty} ->
+  FullTerm (tys ~>* ty) ctx ->
+  All (flip FullTerm ctx) tys ->
+  FullTerm ty ctx
+app' t [<] = t
+app' t (us :< u) = app (app' t us) u
+
+-- export
+-- compose :
+--   {ty, ty' : Ty} ->
+--   (t : FullTerm (ty' ~> ty'') ctx) ->
+--   (u : FullTerm (ty ~> ty') ctx) ->
+--   Len u.support =>
+--   Covering Covers t.thin u.thin ->
+--   CoTerm (ty ~> ty'') ctx
+-- compose (t `Over` thin1) (u `Over` thin2) cover =
+--   Abs
+--     (MakeBound
+--       (App
+--         (MakePair
+--           (t `Over` Drop thin1)
+--           (App
+--             (MakePair
+--               (u `Over` Drop id)
+--               (Var `Over` Keep empty)
+--               (DropKeep (coverIdLeft empty)))
+--            `Over` Keep thin2)
+--           (DropKeep cover)))
+--       (Keep Empty))
+
+-- export
+-- (.~) :
+--   Len ctx =>
+--   {ty, ty' : Ty} ->
+--   CoTerm (ty' ~> ty'') ctx ->
+--   CoTerm (ty ~> ty') ctx ->
+--   CoTerm (ty ~> ty'') ctx
+-- t .~ u = compose (t `Over` id) (u `Over` id) (coverIdLeft id)
 
 export
-(.) : Len ctx => {ty, ty' : Ty} -> Term ctx (ty' ~> ty'') -> Term ctx (ty ~> ty') -> Term ctx (ty ~> ty'')
-t . u = Abs' (S Z) (\x => App (wkn t (Drop id)) (App (wkn u (Drop id)) x))
+(.) :
+  Len ctx =>
+  {ty, ty' : Ty} ->
+  FullTerm (ty' ~> ty'') ctx ->
+  FullTerm (ty ~> ty') ctx ->
+  FullTerm (ty ~> ty'') ctx
+t . u = abs' (S Z) (\x => app (drop t) (app (drop u) x))
 
 export
 (.*) :
   Len ctx =>
   {ty : Ty} ->
   {tys : SnocList Ty} ->
-  Term ctx (ty ~> ty') ->
-  Term ctx (tys ~>* ty) ->
-  Term ctx (tys ~>* ty')
-(.*) {tys = [<]} t u = App t u
-(.*) {tys = tys :< ty''} t u = Abs' (S Z) (\f => wkn t (Drop id) . f) .*  u
+  FullTerm (ty ~> ty') ctx ->
+  FullTerm (tys ~>* ty) ctx ->
+  FullTerm (tys ~>* ty') ctx
+(.*) {tys = [<]} t u = app t u
+(.*) {tys = tys :< ty''} t u = abs' (S Z) (\f => drop t . f) .*  u
 
 export
-lift : {ctx : SnocList Ty} -> Term [<] ty -> Term ctx ty
+lift : Len ctx => FullTerm ty [<] -> FullTerm ty ctx
 lift t = wkn t empty
+
+export
+id' : CoTerm (ty ~> ty) [<]
+id' = Abs (MakeBound Var (Keep Empty))
+
+export
+id : FullTerm (ty ~> ty) [<]
+id = id' `Over` empty