Reset using only co-de Bruijn syntax.

1 files changed, 0 insertions, 128 deletions

diff --git a/src/Total/Syntax.idr b/src/Total/Syntax.idr
deleted file mode 100644
index fead586..0000000
--- a/src/Total/Syntax.idr
+++ /dev/null
@@ -1,128 +0,0 @@
-module Total.Syntax
-
-import public Data.List
-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 ~>*
-infixl 9 .~, .*
-
-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)
-
-export
-lit : Len ctx => 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)) ->
-  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' :
-  (len : Len ctx) =>
-  (k : Len tys) ->
-  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} ->
-  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} ->
-  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} ->
-  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 : 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