WIP : use smarter weakenings.better-thinning

1 files changed, 33 insertions, 32 deletions

diff --git a/src/Total/Syntax.idr b/src/Total/Syntax.idr
index fead586..2710ad3 100644
--- a/src/Total/Syntax.idr
+++ b/src/Total/Syntax.idr
@@ -11,34 +11,42 @@ infixr 20 ~>*
 infixl 9 .~, .*
 
 public export
+data Len : SnocList a -> Type where
+  Z : Len [<]
+  S : Len sx -> Len (sx :< x)
+
+%name Len k
+
+export
+lenToNat : Len sx -> Nat
+lenToNat Z = 0
+lenToNat (S k) = S (lenToNat k)
+
+public export
 (~>*) : SnocList Ty -> Ty -> Ty
 tys ~>* ty = foldr (~>) ty tys
 
 public export
-0 Fun : {sx : SnocList a} -> Len sx -> (a -> Type) -> Type -> Type
-Fun Z arg ret = ret
-Fun (S {x = ty} k) arg ret = Fun k arg (arg ty -> ret)
-
-after : (k : Len sx) -> (a -> b) -> Fun k p a -> Fun k p b
-after Z f x = f x
-after (S k) f x = after k (f .) x
-
-before :
-  (k : Len sx) ->
-  (forall x. p x -> q x) ->
-  Fun k q ret ->
-  Fun k p ret
-before Z f x = x
-before (S k) f x = before k f (after k (. f) x)
+0 Fun : (sx : SnocList a) -> (a -> Type) -> Type -> Type
+Fun [<] p ret = ret
+Fun (sx :< x) p ret = Fun sx p (p x -> ret)
+
+after : Len sx -> (r -> s) -> Fun sx p r -> Fun sx p s
+after Z f = f
+after (S k) f = after k (f .)
+
+before : Len sx -> (forall x. p x -> q x) -> Fun sx q ret -> Fun sx p ret
+before Z f = id
+before (S k) f = before k f . after k (. f)
 
 export
-lit : Len ctx => Nat -> FullTerm N ctx
-lit 0 = Zero `Over` empty
+lit : Nat -> FullTerm N ctx
+lit 0 = Zero `Over` Empty
 lit (S n) = suc (lit n)
 
 absHelper :
-  (k : Len tys) ->
-  Fun k (flip Elem (ctx ++ tys)) (FullTerm ty (ctx ++ tys)) ->
+  Len tys ->
+  Fun tys (flip Elem (ctx ++ tys)) (FullTerm ty (ctx ++ tys)) ->
   FullTerm (tys ~>* ty) ctx
 absHelper Z x = x
 absHelper (S k) x =
@@ -48,11 +56,10 @@ absHelper (S k) x =
 
 export
 abs' :
-  (len : Len ctx) =>
-  (k : Len tys) ->
-  Fun k (flip FullTerm (ctx ++ tys)) (FullTerm ty (ctx ++ tys)) ->
+  Len tys ->
+  Fun tys (flip FullTerm (ctx ++ tys)) (FullTerm ty (ctx ++ tys)) ->
   FullTerm (tys ~>* ty) ctx
-abs' k = absHelper k . before k (var @{lenAppend len k})
+abs' k = absHelper k . before k var
 
 export
 app' :
@@ -97,7 +104,6 @@ app' t (us :< u) = app (app' t us) u
 
 export
 (.) :
-  Len ctx =>
   {ty, ty' : Ty} ->
   FullTerm (ty' ~> ty'') ctx ->
   FullTerm (ty ~> ty') ctx ->
@@ -106,7 +112,6 @@ t . u = abs' (S Z) (\x => app (drop t) (app (drop u) x))
 
 export
 (.*) :
-  Len ctx =>
   {ty : Ty} ->
   {tys : SnocList Ty} ->
   FullTerm (ty ~> ty') ctx ->
@@ -116,13 +121,9 @@ export
 (.*) {tys = tys :< ty''} t u = abs' (S Z) (\f => drop t . f) .*  u
 
 export
-lift : Len ctx => FullTerm ty [<] -> FullTerm ty ctx
-lift t = wkn t empty
-
-export
-id' : CoTerm (ty ~> ty) [<]
-id' = Abs (MakeBound Var (Keep Empty))
+lift : FullTerm ty [<] -> FullTerm ty ctx
+lift t = wkn t Empty
 
 export
 id : FullTerm (ty ~> ty) [<]
-id = id' `Over` empty
+id = Abs Var `Over` Empty