diff options
Diffstat (limited to 'src/Total')
-rw-r--r-- | src/Total/Encoded/Util.idr | 444 | ||||
-rw-r--r-- | src/Total/LogRel.idr | 355 | ||||
-rw-r--r-- | src/Total/NormalForm.idr | 187 | ||||
-rw-r--r-- | src/Total/Pretty.idr | 163 | ||||
-rw-r--r-- | src/Total/Reduction.idr | 114 | ||||
-rw-r--r-- | src/Total/Syntax.idr | 128 | ||||
-rw-r--r-- | src/Total/Term.idr | 357 | ||||
-rw-r--r-- | src/Total/Term/CoDebruijn.idr | 317 |
8 files changed, 0 insertions, 2065 deletions
diff --git a/src/Total/Encoded/Util.idr b/src/Total/Encoded/Util.idr deleted file mode 100644 index f56d1bc..0000000 --- a/src/Total/Encoded/Util.idr +++ /dev/null @@ -1,444 +0,0 @@ -module Total.Encoded.Util - -import public Data.Fin -import public Data.List1 -import public Data.List.Elem -import public Data.List.Quantifiers -import public Total.Syntax - -%prefix_record_projections off - -namespace Bool - export - B : Ty - B = N - - export - true : FullTerm B [<] - true = zero - - export - false : FullTerm B [<] - false = suc zero - - export - if' : FullTerm (B ~> ty ~> ty ~> ty) [<] - if' = abs' (S $ S $ S Z) (\b, t, f => rec b t (abs $ drop f)) - -namespace Arb - export - arb : {ty : Ty} -> FullTerm ty [<] - arb {ty = N} = zero - arb {ty = ty ~> ty'} = abs (lift arb) - -namespace Union - export - (<+>) : Ty -> Ty -> Ty - N <+> N = N - N <+> (u ~> u') = u ~> u' - (t ~> t') <+> N = t ~> t' - (t ~> t') <+> (u ~> u') = (t <+> u) ~> (t' <+> u') - - export - swap : {t, u : Ty} -> FullTerm ((t <+> u) ~> (u <+> t)) [<] - swap {t = N, u = N} = id - swap {t = N, u = u ~> u'} = id - swap {t = t ~> t', u = N} = id - swap {t = t ~> t', u = u ~> u'} = abs' (S Z) (\f => drop swap . f . drop swap) - - export - injL : {t, u : Ty} -> FullTerm (t ~> (t <+> u)) [<] - export - injR : {t, u : Ty} -> FullTerm (u ~> (t <+> u)) [<] - export - prjL : {t, u : Ty} -> FullTerm ((t <+> u) ~> t) [<] - export - prjR : {t, u : Ty} -> FullTerm ((t <+> u) ~> u) [<] - - injL {t = N, u = N} = id - injL {t = N, u = u ~> u'} = abs' (S $ S Z) (\n, _ => app (lift (prjR . injL)) n) - injL {t = t ~> t', u = N} = id - injL {t = t ~> t', u = u ~> u'} = abs' (S Z) (\f => drop injL . f . drop prjL) - - injR = swap . injL - - prjL {t = N, u = N} = id - prjL {t = N, u = u ~> u'} = abs' (S Z) (\f => app (drop (prjL . injR) . f) (drop arb)) - prjL {t = t ~> t', u = N} = id - prjL {t = t ~> t', u = u ~> u'} = abs' (S Z) (\f => drop prjL . f . drop injL) - - prjR = prjL . swap - -namespace Unit - export - Unit : Ty - Unit = N - -namespace Pair - export - (*) : Ty -> Ty -> Ty - t * u = B ~> (t <+> u) - - export - pair : {t, u : Ty} -> FullTerm (t ~> u ~> (t * u)) [<] - pair = abs' (S $ S $ S Z) - (\fst, snd, b => app' (lift if') [<b, app (lift injL) fst, app (lift injR) snd]) - - export - fst : {t, u : Ty} -> FullTerm ((t * u) ~> t) [<] - fst = abs' (S Z) (\p => app (drop prjL . p) (drop true)) - - export - snd : {t, u : Ty} -> FullTerm ((t * u) ~> u) [<] - snd = abs' (S Z) (\p => app (drop prjR . p) (drop false)) - - export - mapSnd : {t, u, v : Ty} -> FullTerm ((u ~> v) ~> (t * u) ~> (t * v)) [<] - mapSnd = abs' (S $ S Z) (\f, p => app' (lift pair) [<app (lift fst) p , app (f . lift snd) p]) - - export - Product : SnocList Ty -> Ty - Product = foldl (*) Unit - - export - pair' : {tys : SnocList Ty} -> FullTerm (tys ~>* Product tys) [<] - pair' {tys = [<]} = arb - pair' {tys = tys :< ty} = abs' (S $ S Z) (\p, t => app' (lift pair) [<p, t]) .* pair' - - export - project : {tys : SnocList Ty} -> Elem ty tys -> FullTerm (Product tys ~> ty) [<] - project {tys = tys :< ty} Here = snd - project {tys = tys :< ty} (There i) = project i . fst - - export - mapProd : - {ctx, tys, tys' : SnocList Ty} -> - {auto 0 prf : SnocList.length tys = SnocList.length tys'} -> - All (flip FullTerm ctx) (zipWith (~>) tys tys') -> - FullTerm (Product tys ~> Product tys') ctx - mapProd {tys = [<], tys' = [<]} [<] = lift id - mapProd {tys = tys :< ty, tys' = tys' :< ty', prf} (fs :< f) = - abs' (S Z) - (\p => - app' (lift pair) - [<app (drop (mapProd fs {prf = injective prf}) . lift fst) p - , app (drop f . lift snd) p - ]) - - replicate : Nat -> a -> SnocList a - replicate 0 x = [<] - replicate (S n) x = replicate n x :< x - - replicateLen : (n : Nat) -> SnocList.length (replicate n x) = n - replicateLen 0 = Refl - replicateLen (S k) = cong S (replicateLen k) - - export - Vect : Nat -> Ty -> Ty - Vect n ty = Product (replicate n ty) - - zipReplicate : - {0 f : a -> b -> c} -> - {0 p : c -> Type} -> - {n : Nat} -> - p (f x y) -> - SnocList.Quantifiers.All.All p (zipWith f (replicate n x) (replicate n y)) - zipReplicate {n = 0} z = [<] - zipReplicate {n = S k} z = zipReplicate z :< z - - export - mapVect : - {n : Nat} -> - {ty, ty' : Ty} -> - FullTerm ((ty ~> ty') ~> Vect n ty ~> Vect n ty') [<] - mapVect = - abs' (S Z) - (\f => mapProd {prf = trans (replicateLen n) (sym $ replicateLen n)} $ zipReplicate f) - - export - nil : {ty : Ty} -> FullTerm (Vect 0 ty) [<] - nil = arb - - export - cons : {n : Nat} -> {ty : Ty} -> FullTerm (ty ~> Vect n ty ~> Vect (S n) ty) [<] - cons = abs' (S $ S Z) (\t, ts => app' (lift pair) [<ts, t]) - - export - head : {n : Nat} -> {ty : Ty} -> FullTerm (Vect (S n) ty ~> ty) [<] - head = snd - - export - tail : {n : Nat} -> {ty : Ty} -> FullTerm (Vect (S n) ty ~> Vect n ty) [<] - tail = fst - - export - index : {n : Nat} -> {ty : Ty} -> (i : Fin n) -> FullTerm (Vect n ty ~> ty) [<] - index FZ = head - index (FS i) = index i . tail - - export - enumerate : (n : Nat) -> FullTerm (Vect n N) [<] - enumerate 0 = arb - enumerate (S k) = app' pair [<app' mapVect [<abs' (S Z) suc, enumerate k], zero] - -namespace Sum - export - (+) : Ty -> Ty -> Ty - t + u = B * (t <+> u) - - export - left : {t, u : Ty} -> FullTerm (t ~> (t + u)) [<] - left = abs' (S Z) (\e => app' (drop pair) [<drop true, app (drop injL) e]) - - export - right : {t, u : Ty} -> FullTerm (u ~> (t + u)) [<] - right = abs' (S Z) (\e => app' (drop pair) [<drop false, app (drop injR) e]) - - export - case' : {t, u, ty : Ty} -> FullTerm ((t + u) ~> (t ~> ty) ~> (u ~> ty) ~> ty) [<] - case' = abs' (S $ S $ S Z) - (\s, f, g => - app' (lift if') - [<app (lift fst) s - , app (f . lift (prjL . snd)) s - , app (g . lift (prjR . snd)) s]) - - export - either : {t, u, ty : Ty} -> FullTerm ((t ~> ty) ~> (u ~> ty) ~> (t + u) ~> ty) [<] - either = abs' (S $ S $ S Z) (\f, g, s => app' (lift case') [<s, f, g]) - - Sum' : Ty -> List Ty -> Ty - Sum' ty [] = ty - Sum' ty (ty' :: tys) = ty + Sum' ty' tys - - export - Sum : List1 Ty -> Ty - Sum (ty ::: tys) = Sum' ty tys - - put' : - {ty, ty' : Ty} -> - {tys : List Ty} -> - (i : Elem ty (ty' :: tys)) -> - FullTerm (ty ~> Sum' ty' tys) [<] - put' {tys = []} Here = id - put' {tys = _ :: _} Here = left - put' {tys = _ :: _} (There i) = right . put' i - - export - put : {tys : List1 Ty} -> {ty : Ty} -> (i : Elem ty (forget tys)) -> FullTerm (ty ~> Sum tys) [<] - put {tys = _ ::: _} i = put' i - - any' : - {ctx : SnocList Ty} -> - {ty, ty' : Ty} -> - {tys : List Ty} -> - All (flip FullTerm ctx . (~> ty)) (ty' :: tys) -> - FullTerm (Sum' ty' tys ~> ty) ctx - any' (t :: []) = t - any' (t :: u :: ts) = app' (lift either) [<t, any' (u :: ts)] - - export - any : - {ctx : SnocList Ty} -> - {tys : List1 Ty} -> - {ty : Ty} -> - All (flip FullTerm ctx . (~> ty)) (forget tys) -> - FullTerm (Sum tys ~> ty) ctx - any {tys = _ ::: _} = any' - -namespace Nat - export - isZero : FullTerm (N ~> B) [<] - isZero = abs' (S Z) (\m => rec m (drop true) (abs (lift false))) - - export - add : FullTerm (N ~> N ~> N) [<] - add = abs' (S $ S Z) (\m, n => rec m n (abs' (S Z) suc)) - - export - sum : {n : Nat} -> FullTerm (Vect n N ~> N) [<] - sum {n = 0} = abs zero - sum {n = S k} = abs' (S Z) - (\ns => app' (lift add) [<app (lift head) ns, app (lift (sum . tail)) ns]) - - export - pred : FullTerm (N ~> N) [<] - pred = abs' (S Z) - (\m => - app' (lift case') - [<rec m - (lift $ app left (arb {ty = Unit})) - (app' (lift either) - [<abs (lift $ app right zero) - , abs' (S Z) (\n => app (lift right) (suc n)) - ]) - , abs zero - , drop id - ]) - - export - sub : FullTerm (N ~> N ~> N) [<] - sub = abs' (S $ S Z) (\m, n => rec n m (lift pred)) - - export - le : FullTerm (N ~> N ~> B) [<] - le = abs' (S Z) (\m => lift isZero . app (lift sub) m) - - export - lt : FullTerm (N ~> N ~> B) [<] - lt = abs' (S Z) (\m => app (lift le) (suc m)) - - export - cond : - {ctx : SnocList Ty} -> - {ty : Ty} -> - List (FullTerm N ctx, FullTerm (N ~> ty) ctx) -> - FullTerm (N ~> ty) ctx - cond [] = lift arb - cond ((n, v) :: xs) = - abs' (S Z) - (\t => - app' (lift if') - [<app' (lift le) [<t, drop n] - , app (drop v) t - , app (drop $ cond xs) (app' (lift sub) [<t, drop n])]) - -namespace Data - public export - Shape : Type - Shape = (Ty, Nat) - - public export - Container : Type - Container = List1 Shape - - public export - fillShape : Shape -> Ty -> Ty - fillShape (shape, n) ty = shape * Vect n ty - - public export - fill : Container -> Ty -> Ty - fill c ty = Sum (map (flip fillShape ty) c) - - export - fix : Container -> Ty - fix c = Product [<N, N ~> N, N ~> fill c N] - -- ^ ^ ^- tags and next positions - -- | |- offset - -- |- pred (number of tags in structure) - - mapShape : - {shape : Shape} -> - {ty, ty' : Ty} -> - FullTerm ((ty ~> ty') ~> fillShape shape ty ~> fillShape shape ty') [<] - mapShape {shape = (shape, n)} = mapSnd . mapVect - - gmap : - {0 f : a -> b} -> - {0 P : a -> Type} -> - {0 Q : b -> Type} -> - ({x : a} -> P x -> Q (f x)) -> - {xs : List a} -> - All P xs -> - All Q (map f xs) - gmap f [] = [] - gmap f (px :: pxs) = f px :: gmap f pxs - - forgetMap : - (0 f : a -> b) -> - (0 xs : List1 a) -> - forget (map f xs) = map f (forget xs) - forgetMap f (head ::: tail) = Refl - - calcOffsets : - {ctx : SnocList Ty} -> - {c : Container} -> - {n : Nat} -> - (ts : FullTerm (Vect n (fix c)) ctx) -> - (acc : FullTerm N ctx) -> - List (FullTerm N ctx, FullTerm (N ~> N) ctx) - calcOffsets {n = 0} ts acc = [] - calcOffsets {n = S k} ts acc = - let hd = app (lift head) ts in - let n = app (lift $ project $ There $ There Here) hd in - let offset = app (lift $ project $ There Here) hd in - (n, app (lift add) acc . offset) :: - calcOffsets - (app (lift tail) ts) - (app' (lift add) [<suc n, acc]) - - calcData : - {ctx : SnocList Ty} -> - {c : Container} -> - {n : Nat} -> - (ts : FullTerm (Vect n (fix c)) ctx) -> - (acc : FullTerm N ctx) -> - List (FullTerm N ctx, FullTerm (N ~> fill c N) ctx) - calcData {n = 0} ts acc = [] - calcData {n = S k} ts acc = - let hd = app (lift head) ts in - let n = app (lift $ project $ There $ There Here) hd in - (n, app (lift $ project Here) hd) :: - calcData - (app (lift tail) ts) - (app' (lift add) [<suc n, acc]) - - export - intro : - {c : Container} -> - {shape : Shape} -> - Elem shape (forget c) -> - FullTerm (fillShape shape (fix c) ~> fix c) [<] - intro {shape = (shape, n)} i = abs' (S Z) - (\t => - app' (lift $ pair' {tys = [<N, N ~> N, N ~> fill c N]}) - [<app (lift (sum . app mapVect (abs' (S Z) suc . project (There $ There Here)) . snd)) t - , cond ((zero, abs' (S Z) suc) :: calcOffsets (app (lift snd) t) (suc zero)) - , cond - ( (zero, - abs - (app - (lift $ put {tys = map (flip fillShape N) c} $ - rewrite forgetMap (flip fillShape N) c in - elemMap (flip fillShape N) i) - (app' (lift mapSnd) [<abs (lift $ enumerate n), drop t]))) - :: calcData (app (lift snd) t) (suc zero) - ) - ]) - - export - elim : - {c : Container} -> - {ctx : SnocList Ty} -> - {ty : Ty} -> - All (flip FullTerm ctx . (~> ty) . flip Data.fillShape ty) (forget c) -> - FullTerm (fix c ~> ty) ctx - elim cases = abs' (S Z) - (\t => - let tags = suc (app (lift $ project $ There $ There Here) t) in - let offset = app (lift $ project $ There Here) (drop $ drop t) in - let vals = app (lift $ project $ Here) (drop $ drop t) in - app' - (rec tags - (lift arb) - (abs' (S $ S Z) (\rec, n => - app - (any {tys = map (flip fillShape N) c} - (rewrite forgetMap (flip fillShape N) c in - gmap - (\f => - drop (drop $ drop f) . - app (lift mapShape) (rec . app (lift add) (app offset n))) - cases) . - vals) - n))) - [<zero]) - - -- elim cases (#tags-1,offset,data) = - -- let - -- step : (N -> ty) -> (N -> ty) - -- step rec n = - -- case rec n of - -- i => cases(i) . mapShape (rec . (+ offset n)) - -- in - -- rec #tags arb step 0 diff --git a/src/Total/LogRel.idr b/src/Total/LogRel.idr deleted file mode 100644 index b088e6f..0000000 --- a/src/Total/LogRel.idr +++ /dev/null @@ -1,355 +0,0 @@ -module Total.LogRel - -import Data.Singleton -import Syntax.PreorderReasoning -import Total.Reduction -import Total.Term -import Total.Term.CoDebruijn - -%prefix_record_projections off - -public export -LogRel : - {ctx : SnocList Ty} -> - (P : {ctx, ty : _} -> FullTerm ty ctx -> Type) -> - {ty : Ty} -> - (t : FullTerm ty ctx) -> - Type -LogRel p {ty = N} t = p t -LogRel p {ty = ty ~> ty'} t = - (p t, - {ctx' : SnocList Ty} -> - (thin : ctx `Thins` ctx') -> - (u : FullTerm ty ctx') -> - LogRel p u -> - LogRel p (app (wkn t thin) u)) - -export -escape : - {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} -> - {ty : Ty} -> - {0 t : FullTerm ty ctx} -> - LogRel P t -> - P t -escape {ty = N} pt = pt -escape {ty = ty ~> ty'} (pt, app) = pt - -public export -record PreserveHelper - (P : {ctx, ty : _} -> FullTerm ty ctx -> Type) - (R : {ctx, ty : _} -> FullTerm ty ctx -> FullTerm ty ctx -> Type) where - constructor MkPresHelper - 0 app : - {ctx : SnocList Ty} -> - {ty, ty' : Ty} -> - (t, u : FullTerm (ty ~> ty') ctx) -> - {ctx' : SnocList Ty} -> - (thin : ctx `Thins` ctx') -> - (v : FullTerm ty ctx') -> - R t u -> - R (app (wkn t thin) v) (app (wkn u thin) v) - pres : - {0 ctx : SnocList Ty} -> - {ty : Ty} -> - {0 t, u : FullTerm ty ctx} -> - P t -> - (0 _ : R t u) -> - P u - -%name PreserveHelper help - -export -backStepHelper : - {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} -> - (forall ctx, ty. {0 t, u : FullTerm ty ctx} -> P t -> (0 _ : toTerm u > toTerm t) -> P u) -> - PreserveHelper P (flip (>) `on` CoDebruijn.toTerm) -backStepHelper pres = - MkPresHelper - (\t, u, thin, v, step => - rewrite toTermApp (wkn u thin) v in - rewrite toTermApp (wkn t thin) v in - rewrite sym $ wknToTerm t thin in - rewrite sym $ wknToTerm u thin in - AppCong1 (wknStep step)) - pres - -export -preserve : - {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} -> - {0 R : {ctx, ty : _} -> FullTerm ty ctx -> FullTerm ty ctx -> Type} -> - {ty : Ty} -> - {0 t, u : FullTerm ty ctx} -> - PreserveHelper P R -> - LogRel P t -> - (0 _ : R t u) -> - LogRel P u -preserve help {ty = N} pt prf = help.pres pt prf -preserve help {ty = ty ~> ty'} (pt, app) prf = - (help.pres pt prf, \thin, v, rel => preserve help (app thin v rel) (help.app _ _ thin v prf)) - -data AllLogRel : (P : {ctx, ty : _} -> FullTerm ty ctx -> Type) -> CoTerms ctx ctx' -> Type where - Lin : - {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} -> - AllLogRel P [<] - (:<) : - {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} -> - AllLogRel P sub -> - LogRel P t -> - AllLogRel P (sub :< t) - -%name AllLogRel allRels - -index : - {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} -> - ((i : Elem ty ctx') -> LogRel P (var i)) -> - {sub : CoTerms ctx ctx'} -> - AllLogRel P sub -> - (i : Elem ty ctx) -> - LogRel P (index sub i) -index f (allRels :< rel) Here = rel -index f (allRels :< rel) (There i) = index f allRels i - -restrict : - {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} -> - {0 sub : CoTerms ctx' ctx''} -> - AllLogRel P sub -> - (thin : ctx `Thins` ctx') -> - AllLogRel P (restrict sub thin) -restrict [<] Empty = [<] -restrict (allRels :< rel) (Drop thin) = restrict allRels thin -restrict (allRels :< rel) (Keep thin) = restrict allRels thin :< rel - -Valid : - (P : {ctx, ty : _} -> FullTerm ty ctx -> Type) -> - {ctx : SnocList Ty} -> - {ty : Ty} -> - (t : FullTerm ty ctx) -> - Type -Valid p t = - {ctx' : SnocList Ty} -> - (sub : CoTerms ctx ctx') -> - (allRel : AllLogRel p sub) -> - LogRel p (subst t sub) - -public export -record ValidHelper (P : {ctx, ty : _} -> FullTerm ty ctx -> Type) where - constructor MkValidHelper - var : forall ctx. Len ctx => {ty : Ty} -> (i : Elem ty ctx) -> LogRel P (var i) - abs : forall ctx, ty. {ty' : Ty} -> {0 t : FullTerm ty' (ctx :< ty)} -> LogRel P t -> P (abs t) - zero : forall ctx. Len ctx => P {ctx} zero - suc : forall ctx. {0 t : FullTerm N ctx} -> P t -> P (suc t) - rec : - {ctx : SnocList Ty} -> - {ty : Ty} -> - {0 t : FullTerm N ctx} -> - {u : FullTerm ty ctx} -> - {v : FullTerm (ty ~> ty) ctx} -> - LogRel P t -> - LogRel P u -> - LogRel P v -> - LogRel P (rec t u v) - step : forall ctx, ty. {0 t, u : FullTerm ty ctx} -> P t -> (0 _ : toTerm u > toTerm t) -> P u - wkn : forall ctx, ctx', ty. - {0 t : FullTerm ty ctx} -> - P t -> - (thin : ctx `Thins` ctx') -> - P (wkn t thin) - -%name ValidHelper help - -wknRel : - {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} -> - ValidHelper P -> - {ty : Ty} -> - {0 t : FullTerm ty ctx} -> - LogRel P t -> - (thin : ctx `Thins` ctx') -> - LogRel P (wkn t thin) -wknRel help {ty = N} pt thin = help.wkn pt thin -wknRel help {ty = ty ~> ty'} (pt, app) thin = - ( help.wkn pt thin - , \thin', u, rel => - rewrite wknHomo t thin' thin in - app (thin' . thin) u rel - ) - -wknAllRel : - {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} -> - ValidHelper P -> - {ctx : SnocList Ty} -> - {sub : CoTerms ctx ctx'} -> - AllLogRel P sub -> - (thin : ctx' `Thins` ctx'') -> - AllLogRel P (wknAll sub thin) -wknAllRel help [<] thin = [<] -wknAllRel help (allRels :< rel) thin = wknAllRel help allRels thin :< wknRel help rel thin - -shiftRel : - {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} -> - ValidHelper P -> - {ctx, ctx' : SnocList Ty} -> - {sub : CoTerms ctx ctx'} -> - AllLogRel P sub -> - AllLogRel P (shift {ty} sub) -shiftRel help [<] = [<] -shiftRel help (allRels :< rel) = - shiftRel help allRels :< - replace {p = LogRel P} (sym $ dropIsWkn _) (wknRel help rel (Drop id)) - -liftRel : - {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} -> - ValidHelper P -> - {ctx, ctx' : SnocList Ty} -> - {ty : Ty} -> - {sub : CoTerms ctx ctx'} -> - AllLogRel P sub -> - AllLogRel P (lift {ty} sub) -liftRel help allRels = shiftRel help allRels :< help.var Here - -absValid : - {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} -> - ValidHelper P -> - {ctx : SnocList Ty} -> - {ty, ty' : Ty} -> - (t : CoTerm ty' (ctx ++ used)) -> - (thin : used `Thins` [<ty]) -> - (valid : {ctx' : SnocList Ty} -> - (sub : CoTerms (ctx ++ used) ctx') -> - AllLogRel P sub -> - LogRel P (subst' t sub)) -> - {ctx' : SnocList Ty} -> - (sub : CoTerms ctx ctx') -> - AllLogRel P sub -> - LogRel P (subst' (Abs (MakeBound t thin)) sub) -absValid help t (Drop Empty) valid sub allRels = - ( help.abs (valid (shift sub) (shiftRel help allRels)) - , \thin, u, rel => - preserve - (backStepHelper help.step) - (valid (wknAll sub thin) (wknAllRel help allRels thin)) - ?betaStep - ) -absValid help t (Keep Empty) valid sub allRels = - ( help.abs (valid (lift sub) (liftRel help allRels)) - , \thin, u, rel => - preserve (backStepHelper help.step) - (valid (wknAll sub thin :< u) (wknAllRel help allRels thin :< rel)) - ?betaStep' - ) - -export -allValid : - {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} -> - ValidHelper P -> - (s : Singleton ctx) => - {ty : Ty} -> - (t : FullTerm ty ctx) -> - Valid P t -allValid' : - {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} -> - ValidHelper P -> - (s : Singleton ctx) => - {ty : Ty} -> - (t : CoTerm ty ctx) -> - {ctx' : SnocList Ty} -> - (sub : CoTerms ctx ctx') -> - AllLogRel P sub -> - LogRel P (subst' t sub) - -allValid help (t `Over` thin) sub allRels = - allValid' help t (restrict sub thin) (restrict allRels thin) - -allValid' help Var sub allRels = index help.var allRels Here -allValid' help {s = Val ctx} (Abs {ty, ty'} (MakeBound t thin)) sub allRels = - let s' = [| Val ctx ++ retractSingleton (Val [<ty]) thin |] in - absValid help t thin (allValid' help t) sub allRels -allValid' help (App (MakePair t u _)) sub allRels = - let (pt, app) = allValid help t sub allRels in - let rel = allValid help u sub allRels in - rewrite sym $ wknId (subst t sub) in - app id (subst u sub) rel -allValid' help Zero sub allRels = help.zero -allValid' help (Suc t) sub allRels = - let pt = allValid' help t sub allRels in - help.suc pt -allValid' help (Rec (MakePair t (MakePair u v _ `Over` thin) _)) sub allRels = - let relT = allValid help t sub allRels in - let relU = allValid help u (restrict sub thin) (restrict allRels thin) in - let relV = allValid help v (restrict sub thin) (restrict allRels thin) in - help.rec relT relU relV - --- -- allValid help (Var i) sub allRels = index help.var allRels i --- -- allValid help (Abs t) sub allRels = --- -- let valid = allValid help t in --- -- (let --- -- rec = --- -- valid --- -- (wknAll sub (Drop id) :< Var Here) --- -- (wknAllRel help allRels (Drop id) :< help.var Here) --- -- in --- -- help.abs rec --- -- , \thin, u, rel => --- -- let --- -- eq : --- -- (subst --- -- (wkn (subst t (wknAll sub (Drop Thinning.id) :< Var Here)) (Keep thin)) --- -- (Base Thinning.id :< u) = --- -- subst t (wknAll sub thin :< u)) --- -- eq = --- -- Calc $ --- -- |~ subst (wkn (subst t (wknAll sub (Drop id) :< Var Here)) (Keep thin)) (Base id :< u) --- -- ~~ subst (subst t (wknAll sub (Drop id) :< Var Here)) (restrict (Base id :< u) (Keep thin)) --- -- ...(substWkn (subst t (wknAll sub (Drop id) :< Var Here)) (Keep thin) (Base id :< u)) --- -- ~~ subst (subst t (wknAll sub (Drop id) :< Var Here)) (Base thin :< u) --- -- ...(cong (subst (subst t (wknAll sub (Drop id) :< Var Here)) . (:< u) . Base) $ identityLeft thin) --- -- ~~ subst t ((Base thin :< u) . wknAll sub (Drop id) :< u) --- -- ...(substHomo t (wknAll sub (Drop id) :< Var Here) (Base thin :< u)) --- -- ~~ subst t (Base (thin . id) . sub :< u) --- -- ...(cong (subst t . (:< u)) $ compWknAll sub (Base thin :< u) (Drop id)) --- -- ~~ subst t (Base thin . sub :< u) --- -- ...(cong (subst t . (:< u) . (. sub) . Base) $ identityRight thin) --- -- ~~ subst t (wknAll sub thin :< u) --- -- ...(cong (subst t . (:< u)) $ baseComp thin sub) --- -- in --- -- preserve --- -- (backStepHelper help.step) --- -- (valid (wknAll sub thin :< u) (wknAllRel help allRels thin :< rel)) --- -- (replace {p = (App (wkn (subst (Abs t) sub) thin) u >)} --- -- eq --- -- (AppBeta (length _))) --- -- ) --- -- allValid help (App t u) sub allRels = --- -- let (pt, app) = allValid help t sub allRels in --- -- let rel = allValid help u sub allRels in --- -- rewrite sym $ wknId (subst t sub) in --- -- app id (subst u sub) rel --- -- allValid help Zero sub allRels = help.zero --- -- allValid help (Suc t) sub allRels = --- -- let pt = allValid help t sub allRels in --- -- help.suc pt --- -- allValid help (Rec t u v) sub allRels = --- -- let relt = allValid help t sub allRels in --- -- let relu = allValid help u sub allRels in --- -- let relv = allValid help v sub allRels in --- -- help.rec relt relu relv - -idRel : - {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} -> - {ctx : SnocList Ty} -> - ValidHelper P -> - AllLogRel P {ctx} (Base Thinning.id) -idRel help {ctx = [<]} = [<] -idRel help {ctx = ctx :< ty} = liftRel help (idRel help) - -export -allRel : - {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} -> - {ctx : SnocList Ty} -> - {ty : Ty} -> - ValidHelper P -> - (t : FullTerm ty ctx) -> - P t -allRel help t = - rewrite sym $ substId t in - escape {P} $ - allValid help @{Val ctx} t (Base id) (idRel help) diff --git a/src/Total/NormalForm.idr b/src/Total/NormalForm.idr deleted file mode 100644 index a7aba57..0000000 --- a/src/Total/NormalForm.idr +++ /dev/null @@ -1,187 +0,0 @@ -module Total.NormalForm - -import Total.LogRel -import Total.Reduction -import Total.Term -import Total.Term.CoDebruijn - -%prefix_record_projections off - -public export -data Neutral' : CoTerm ty ctx -> Type -public export -data Normal' : CoTerm ty ctx -> Type - -public export -data Neutral : FullTerm ty ctx -> Type - -public export -data Normal : FullTerm ty ctx -> Type - -data Neutral' where - Var : Neutral' Var - App : Neutral t -> Normal u -> Neutral' (App (MakePair t u cover)) - Rec : - Neutral t -> - Normal u -> - Normal v -> - Neutral' (Rec (MakePair t (MakePair u v cover1 `Over` thin) cover2)) - -data Normal' where - Ntrl : Neutral' t -> Normal' t - Abs : Normal' t -> Normal' (Abs (MakeBound t thin)) - Zero : Normal' Zero - Suc : Normal' t -> Normal' (Suc t) - -data Neutral where - WrapNe : Neutral' t -> Neutral (t `Over` thin) - -data Normal where - WrapNf : Normal' t -> Normal (t `Over` thin) - -%name Neutral n, m, k -%name Normal n, m, k -%name Neutral' n, m, k -%name Normal' n, m, k - -public export -record NormalForm (0 t : FullTerm ty ctx) where - constructor MkNf - term : FullTerm ty ctx - 0 steps : toTerm t >= toTerm term - 0 normal : Normal term - -%name NormalForm nf - --- Strong Normalization Proof -------------------------------------------------- - -abs : Normal t -> Normal (abs t) - -app : Neutral t -> Normal u -> Neutral (app t u) - -suc : Normal t -> Normal (suc t) - -rec : Neutral t -> Normal u -> Normal v -> Neutral (rec t u v) - -invApp : Normal' (App x) -> Neutral' (App x) -invApp (Ntrl n) = n - -invRec : Normal' (Rec x) -> Neutral' (Rec x) -invRec (Ntrl n) = n - -invSuc : Normal' (Suc t) -> Normal' t -invSuc (Suc n) = n - -wknNe : Neutral t -> Neutral (wkn t thin) -wknNe (WrapNe n) = WrapNe n - -wknNf : Normal t -> Normal (wkn t thin) -wknNf (WrapNf n) = WrapNf n - -backStepsNf : NormalForm t -> (0 _ : toTerm u >= toTerm t) -> NormalForm u -backStepsNf nf steps = MkNf nf.term (steps ++ nf.steps) nf.normal - -backStepsRel : - {ty : Ty} -> - {0 t, u : FullTerm ty ctx} -> - LogRel (\t => NormalForm t) t -> - (0 _ : toTerm u >= toTerm t) -> - LogRel (\t => NormalForm t) u -backStepsRel = - preserve {R = flip (>=) `on` toTerm} - (MkPresHelper - (\t, u, thin, v, steps => - ?appCong1Steps) - backStepsNf) - -ntrlRel : {ty : Ty} -> {t : FullTerm ty ctx} -> (0 _ : Neutral t) -> LogRel (\t => NormalForm t) t -ntrlRel {ty = N} (WrapNe n) = MkNf t [<] (WrapNf (Ntrl n)) -ntrlRel {ty = ty ~> ty'} (WrapNe {thin = thin'} n) = - ( MkNf t [<] (WrapNf (Ntrl n)) - , \thin, u, rel => - backStepsRel - (ntrlRel (app (wknNe {thin} (WrapNe {thin = thin'} n)) (escape rel).normal)) - ?appCong2Steps - ) - -recNf'' : - {ctx : SnocList Ty} -> - {ty : Ty} -> - {u : FullTerm ty ctx} -> - {v : FullTerm (ty ~> ty) ctx} -> - (t : CoTerm N ctx') -> - (thin : ctx' `Thins` ctx) -> - (0 n : Normal' t) -> - LogRel (\t => NormalForm t) u -> - LogRel (\t => NormalForm t) v -> - LogRel (\t => NormalForm t) (rec (t `Over` thin) u v) -recNf'' Zero thin n relU relV = - backStepsRel relU [<?recZero] -recNf'' (Suc t) thin n relU relV = - let rec = recNf'' t thin (invSuc n) relU relV in - backStepsRel (snd relV id _ rec) [<?recSuc] -recNf'' t@Var thin n relU relV = - let 0 neT = WrapNe {thin} Var in - let nfU = escape relU in - let nfV = escape {ty = ty ~> ty} relV in - backStepsRel - (ntrlRel (rec neT nfU.normal nfV.normal)) - ?stepsUandV -recNf'' t@(App _) thin n relU relV = - let 0 neT = WrapNe {thin} (invApp n) in - let nfU = escape relU in - let nfV = escape {ty = ty ~> ty} relV in - backStepsRel - (ntrlRel (rec neT nfU.normal nfV.normal)) - ?stepsUandV' -recNf'' t@(Rec _) thin n relU relV = - let 0 neT = WrapNe {thin} (invRec n) in - let nfU = escape relU in - let nfV = escape {ty = ty ~> ty} relV in - backStepsRel - (ntrlRel (rec neT nfU.normal nfV.normal)) - ?stepsUandV'' - -recNf' : - {ctx : SnocList Ty} -> - {ty : Ty} -> - {u : FullTerm ty ctx} -> - {v : FullTerm (ty ~> ty) ctx} -> - (t : FullTerm N ctx) -> - (0 n : Normal t) -> - LogRel (\t => NormalForm t) u -> - LogRel (\t => NormalForm t) v -> - LogRel (\t => NormalForm t) (rec t u v) -recNf' (t `Over` thin) (WrapNf n) = recNf'' t thin n - -recNf : - {ctx : SnocList Ty} -> - {ty : Ty} -> - {0 t : FullTerm N ctx} -> - {u : FullTerm ty ctx} -> - {v : FullTerm (ty ~> ty) ctx} -> - NormalForm t -> - LogRel (\t => NormalForm t) u -> - LogRel (\t => NormalForm t) v -> - LogRel (\t => NormalForm t) (rec t u v) -recNf nf relU relV = - backStepsRel - (recNf' nf.term nf.normal relU relV) - ?recCong1Steps - -helper : ValidHelper (\t => NormalForm t) -helper = MkValidHelper - { var = \i => ntrlRel (WrapNe Var) - , abs = \rel => - let nf = escape rel in - MkNf (abs nf.term) ?absCongSteps (abs nf.normal) - , zero = MkNf zero [<] (WrapNf Zero) - , suc = \nf => MkNf (suc nf.term) ?sucCongSteps (suc nf.normal) - , rec = recNf - , step = \nf, step => backStepsNf nf [<step] - , wkn = \nf, thin => MkNf (wkn nf.term thin) ?wknSteps (wknNf nf.normal) - } - -export -normalize : {ctx : SnocList Ty} -> {ty : Ty} -> (t : FullTerm ty ctx) -> NormalForm t -normalize = allRel helper diff --git a/src/Total/Pretty.idr b/src/Total/Pretty.idr deleted file mode 100644 index eade721..0000000 --- a/src/Total/Pretty.idr +++ /dev/null @@ -1,163 +0,0 @@ -module Total.Pretty - -import public Text.PrettyPrint.Prettyprinter -import public Text.PrettyPrint.Prettyprinter.Render.Terminal - -import Data.DPair -import Data.Fin -import Data.Fin.Extra -import Data.Nat -import Data.Stream -import Data.String - -import Total.Syntax -import Total.Term - -data Syntax = Bound | Keyword - -keyword : Doc Syntax -> Doc Syntax -keyword = annotate Keyword - -bound : Doc Syntax -> Doc Syntax -bound = annotate Bound - -rec_ : Doc Syntax -rec_ = keyword "rec" - -plus : Doc Syntax -plus = keyword "+" - -arrow : Doc Syntax -arrow = keyword "=>" - -public export -interface Renderable (0 a : Type) where - fromSyntax : Syntax -> a - -export -Renderable AnsiStyle where - fromSyntax Bound = italic - fromSyntax Keyword = color BrightWhite - -startPrec, leftAppPrec, appPrec : Prec -startPrec = Open -leftAppPrec = Equal -appPrec = App - -parameters (names : Stream String) - export - prettyTerm : Len ctx -> Prec -> Term ctx ty -> Doc Syntax - prettyTerm len d (Var i) = bound (pretty $ index (minus (cast len) (S $ elemToNat i)) names) - prettyTerm len d (Abs t) = - let Evidence _ (len, t') = getLamNames (S len) t in - parenthesise (d > startPrec) $ group $ align $ hang 2 $ - backslash <+> prettyBindings len <++> arrow <+> line <+> - (prettyTerm len Open (assert_smaller t t')) - where - getLamNames : - forall ctx, ty. - Len ctx -> - Term ctx ty -> - Exists {type = Pair _ _} (\ctxTy => (Len (fst ctxTy), Term (fst ctxTy) (snd ctxTy))) - getLamNames k (Abs t) = getLamNames (S k) t - getLamNames k t@(Var _) = Evidence (_, _) (k, t) - getLamNames k t@(App _ _) = Evidence (_, _) (k, t) - getLamNames k t@Zero = Evidence (_, _) (k, t) - getLamNames k t@(Suc _) = Evidence (_, _) (k, t) - getLamNames k t@(Rec _ _ _) = Evidence (_, _) (k, t) - - prettyBindings' : Nat -> Nat -> Doc Syntax - prettyBindings' offset 0 = neutral - prettyBindings' offset 1 = bound (pretty $ index offset names) - prettyBindings' offset (S (S k)) = - bound (pretty $ index offset names) <+> comma <++> prettyBindings' (S offset) (S k) - - prettyBindings : Len ctx' -> Doc Syntax - prettyBindings k = prettyBindings' (cast len) (minus (cast k) (cast len)) - prettyTerm len d app@(App t u) = - let (f, ts) = getSpline t [prettyArg u] in - parenthesise (d >= appPrec) $ group $ align $ hang 2 $ - f <+> line <+> vsep ts - where - prettyArg : forall ty. Term ctx ty -> Doc Syntax - prettyArg v = prettyTerm len appPrec (assert_smaller app v) - - getSpline : - forall ty, ty'. - Term ctx (ty ~> ty') -> - List (Doc Syntax) -> - (Doc Syntax, List (Doc Syntax)) - getSpline (App t u) xs = getSpline t (prettyArg u :: xs) - getSpline (Rec t u v) xs = (rec_ <++> prettyArg t, prettyArg u :: prettyArg v :: xs) - getSpline t'@(Var _) xs = (prettyTerm len leftAppPrec (assert_smaller t t'), xs) - getSpline t'@(Abs _) xs = (prettyTerm len leftAppPrec (assert_smaller t t'), xs) - prettyTerm len d Zero = pretty 0 - prettyTerm len d (Suc t) = - let (lit, t') = getSucs t in - case t' of - Just t' => - parenthesise (d >= appPrec) $ group $ - pretty (S lit) <++> plus <++> prettyTerm len leftAppPrec (assert_smaller t t') - Nothing => pretty (S lit) - where - getSucs : Term ctx N -> (Nat, Maybe (Term ctx N)) - getSucs Zero = (0, Nothing) - getSucs (Suc t) = mapFst S (getSucs t) - getSucs t@(Var _) = (0, Just t) - getSucs t@(App _ _) = (0, Just t) - getSucs t@(Rec _ _ _) = (0, Just t) - prettyTerm len d (Rec t u v) = - parenthesise (d >= appPrec) $ group $ align $ hang 2 $ - rec_ <++> - prettyTerm len appPrec t <+> line <+> - prettyTerm len appPrec u <+> line <+> - prettyTerm len appPrec v - -finToChar : Fin 26 -> Char -finToChar 0 = 'x' -finToChar 1 = 'y' -finToChar 2 = 'z' -finToChar 3 = 'a' -finToChar 4 = 'b' -finToChar 5 = 'c' -finToChar 6 = 'd' -finToChar 7 = 'e' -finToChar 8 = 'f' -finToChar 9 = 'g' -finToChar 10 = 'h' -finToChar 11 = 'i' -finToChar 12 = 'j' -finToChar 13 = 'k' -finToChar 14 = 'l' -finToChar 15 = 'm' -finToChar 16 = 'n' -finToChar 17 = 'o' -finToChar 18 = 'p' -finToChar 19 = 'q' -finToChar 20 = 'r' -finToChar 21 = 's' -finToChar 22 = 't' -finToChar 23 = 'u' -finToChar 24 = 'v' -finToChar 25 = 'w' - -name : Nat -> List Char -name k = - case divMod k 26 of - Fraction k 26 0 r prf => [finToChar r] - Fraction k 26 (S q) r prf => finToChar r :: name (assert_smaller k q) - -export -canonicalNames : Stream String -canonicalNames = map (fastPack . name) nats - -export -pretty : Renderable ann => (len : Len ctx) => Term ctx ty -> Doc ann -pretty t = map fromSyntax (prettyTerm canonicalNames len Open t) - --- \x, y, z => --- rec z --- (\a, b => \c => \d => d (\d => d c) a x) --- (\a => \b => b y) --- 0 --- (\x => x) diff --git a/src/Total/Reduction.idr b/src/Total/Reduction.idr deleted file mode 100644 index a424515..0000000 --- a/src/Total/Reduction.idr +++ /dev/null @@ -1,114 +0,0 @@ -module Total.Reduction - -import Syntax.PreorderReasoning -import Total.Term - -public export -data (>) : Term ctx ty -> Term ctx ty -> Type where - AbsCong : t > u -> Abs t > Abs u - AppCong1 : t > u -> App t v > App u v - AppCong2 : u > v -> App t u > App t v - AppBeta : - (0 len : Len ctx) -> - App (Abs t) u > subst t (Base (id @{len}) :< u) - SucCong : t > u -> Suc t > Suc u - RecCong1 : t1 > t2 -> Rec t1 u v > Rec t2 u v - RecCong2 : u1 > u2 -> Rec t u1 v > Rec t u2 v - RecCong3 : v1 > v2 -> Rec t u v1 > Rec t u v2 - RecZero : Rec Zero u v > u - RecSuc : Rec (Suc t) u v > App v (Rec t u v) - -%name Reduction.(>) step - -public export -data (>=) : Term ctx ty -> Term ctx ty -> Type where - Lin : t >= t - (:<) : t >= u -> u > v -> t >= v - -%name Reduction.(>=) steps - -export -(++) : t >= u -> u >= v -> t >= v -steps ++ [<] = steps -steps ++ steps' :< step = (steps ++ steps') :< step - -export -AbsCong' : t >= u -> Abs t >= Abs u -AbsCong' [<] = [<] -AbsCong' (steps :< step) = AbsCong' steps :< AbsCong step - -export -AppCong1' : t >= u -> App t v >= App u v -AppCong1' [<] = [<] -AppCong1' (steps :< step) = AppCong1' steps :< AppCong1 step - -export -AppCong2' : u >= v -> App t u >= App t v -AppCong2' [<] = [<] -AppCong2' (steps :< step) = AppCong2' steps :< AppCong2 step - -export -SucCong' : t >= u -> Suc t >= Suc u -SucCong' [<] = [<] -SucCong' (steps :< step) = SucCong' steps :< SucCong step - -export -RecCong1' : t1 >= t2 -> Rec t1 u v >= Rec t2 u v -RecCong1' [<] = [<] -RecCong1' (steps :< step) = RecCong1' steps :< RecCong1 step - -export -RecCong2' : u1 >= u2 -> Rec t u1 v >= Rec t u2 v -RecCong2' [<] = [<] -RecCong2' (steps :< step) = RecCong2' steps :< RecCong2 step - -export -RecCong3' : v1 >= v2 -> Rec t u v1 >= Rec t u v2 -RecCong3' [<] = [<] -RecCong3' (steps :< step) = RecCong3' steps :< RecCong3 step - --- Properties ------------------------------------------------------------------ - -lemma : - (t : Term (ctx :< ty) ty') -> - (thin : ctx `Thins` ctx') -> - (u : Term ctx ty) -> - subst (wkn t (Keep thin)) (Base Thinning.id :< wkn u thin) = - wkn (subst t (Base Thinning.id :< u)) thin -lemma t thin u = - Calc $ - |~ subst (wkn t (Keep thin)) (Base id :< wkn u thin) - ~~ subst t (restrict (Base id :< wkn u thin) (Keep thin)) - ...(substWkn t (Keep thin) (Base id :< wkn u thin)) - ~~ subst t (Base (id . thin) :< wkn u thin) - ...(Refl) - ~~ subst t (Base (thin . id) :< wkn u thin) - ...(cong (subst t . (:< wkn u thin) . Base) $ trans (identityLeft thin) (sym $ identityRight thin)) - ~~ wkn (subst t (Base (id) :< u)) thin - ...(sym $ wknSubst t (Base (id @{length ctx}) :< u) thin) - -export -wknStep : t > u -> wkn t thin > wkn u thin -wknStep (AbsCong step) = AbsCong (wknStep step) -wknStep (AppCong1 step) = AppCong1 (wknStep step) -wknStep (AppCong2 step) = AppCong2 (wknStep step) -wknStep (AppBeta len {ctx, t, u}) {thin} = - let - 0 eq : - (subst (wkn t (Keep thin)) (Base Thinning.id :< wkn u thin) = - wkn (subst t (Base (id @{len}) :< u)) thin) - eq = rewrite lenUnique len (length ctx) in lemma t thin u - in - rewrite sym eq in - AppBeta _ -wknStep (SucCong step) = SucCong (wknStep step) -wknStep (RecCong1 step) = RecCong1 (wknStep step) -wknStep (RecCong2 step) = RecCong2 (wknStep step) -wknStep (RecCong3 step) = RecCong3 (wknStep step) -wknStep RecZero = RecZero -wknStep RecSuc = RecSuc - -export -wknSteps : t >= u -> wkn t thin >= wkn u thin -wknSteps [<] = [<] -wknSteps (steps :< step) = wknSteps steps :< wknStep step 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 diff --git a/src/Total/Term.idr b/src/Total/Term.idr deleted file mode 100644 index 129662a..0000000 --- a/src/Total/Term.idr +++ /dev/null @@ -1,357 +0,0 @@ -module Total.Term - -import public Data.SnocList.Elem -import public Thinning -import Syntax.PreorderReasoning - -%prefix_record_projections off - -infixr 10 ~> - -public export -data Ty : Type where - N : Ty - (~>) : Ty -> Ty -> Ty - -%name Ty ty - -public export -data Term : SnocList Ty -> Ty -> Type where - Var : (i : Elem ty ctx) -> Term ctx ty - Abs : Term (ctx :< ty) ty' -> Term ctx (ty ~> ty') - App : {ty : Ty} -> Term ctx (ty ~> ty') -> Term ctx ty -> Term ctx ty' - Zero : Term ctx N - Suc : Term ctx N -> Term ctx N - Rec : Term ctx N -> Term ctx ty -> Term ctx (ty ~> ty) -> Term ctx ty - -%name Term t, u, v - -public export -wkn : Term ctx ty -> ctx `Thins` ctx' -> Term ctx' ty -wkn (Var i) thin = Var (index thin i) -wkn (Abs t) thin = Abs (wkn t $ Keep thin) -wkn (App t u) thin = App (wkn t thin) (wkn u thin) -wkn Zero thin = Zero -wkn (Suc t) thin = Suc (wkn t thin) -wkn (Rec t u v) thin = Rec (wkn t thin) (wkn u thin) (wkn v thin) - -public export -data Terms : SnocList Ty -> SnocList Ty -> Type where - Base : ctx `Thins` ctx' -> Terms ctx' ctx - (:<) : Terms ctx' ctx -> Term ctx' ty -> Terms ctx' (ctx :< ty) - -%name Terms sub - -public export -index : Terms ctx' ctx -> Elem ty ctx -> Term ctx' ty -index (Base thin) i = Var (index thin i) -index (sub :< t) Here = t -index (sub :< t) (There i) = index sub i - -public export -wknAll : Terms ctx' ctx -> ctx' `Thins` ctx'' -> Terms ctx'' ctx -wknAll (Base thin') thin = Base (thin . thin') -wknAll (sub :< t) thin = wknAll sub thin :< wkn t thin - -public export -subst : Len ctx' => Term ctx ty -> Terms ctx' ctx -> Term ctx' ty -subst (Var i) sub = index sub i -subst (Abs t) sub = Abs (subst t $ wknAll sub (Drop id) :< Var Here) -subst (App t u) sub = App (subst t sub) (subst u sub) -subst Zero sub = Zero -subst (Suc t) sub = Suc (subst t sub) -subst (Rec t u v) sub = Rec (subst t sub) (subst u sub) (subst v sub) - -public export -restrict : Terms ctx'' ctx' -> ctx `Thins` ctx' -> Terms ctx'' ctx -restrict (Base thin') thin = Base (thin' . thin) -restrict (sub :< t) (Drop thin) = restrict sub thin -restrict (sub :< t) (Keep thin) = restrict sub thin :< t - -public export -(.) : Len ctx'' => Terms ctx'' ctx' -> Terms ctx' ctx -> Terms ctx'' ctx -sub2 . (Base thin) = restrict sub2 thin -sub2 . (sub1 :< t) = sub2 . sub1 :< subst t sub2 - --- Properties ------------------------------------------------------------------ - --- Utilities - -export -cong3 : (0 f : a -> b -> c -> d) -> x1 = x2 -> y1 = y2 -> z1 = z2 -> f x1 y1 z1 = f x2 y2 z2 -cong3 f Refl Refl Refl = Refl - --- Weakening - -export -wknHomo : - (t : Term ctx ty) -> - (thin1 : ctx `Thins` ctx') -> - (thin2 : ctx' `Thins` ctx'') -> - wkn (wkn t thin1) thin2 = wkn t (thin2 . thin1) -wknHomo (Var i) thin1 thin2 = - cong Var (indexHomo thin2 thin1 i) -wknHomo (Abs t) thin1 thin2 = - cong Abs (wknHomo t (Keep thin1) (Keep thin2)) -wknHomo (App t u) thin1 thin2 = - cong2 App (wknHomo t thin1 thin2) (wknHomo u thin1 thin2) -wknHomo Zero thin1 thin2 = - Refl -wknHomo (Suc t) thin1 thin2 = - cong Suc (wknHomo t thin1 thin2) -wknHomo (Rec t u v) thin1 thin2 = - cong3 Rec (wknHomo t thin1 thin2) (wknHomo u thin1 thin2) (wknHomo v thin1 thin2) - -export -wknId : Len ctx => (t : Term ctx ty) -> wkn t Thinning.id = t -wknId (Var i) = cong Var (indexId i) -wknId (Abs t) = cong Abs (wknId t) -wknId (App t u) = cong2 App (wknId t) (wknId u) -wknId Zero = Refl -wknId (Suc t) = cong Suc (wknId t) -wknId (Rec t u v) = cong3 Rec (wknId t) (wknId u) (wknId v) - -indexWknAll : - (sub : Terms ctx' ctx) -> - (thin : ctx' `Thins` ctx'') -> - (i : Elem ty ctx) -> - index (wknAll sub thin) i = wkn (index sub i) thin -indexWknAll (Base thin') thin i = sym $ cong Var $ indexHomo thin thin' i -indexWknAll (sub :< t) thin Here = Refl -indexWknAll (sub :< t) thin (There i) = indexWknAll sub thin i - -wknAllHomo : - (sub : Terms ctx ctx''') -> - (thin1 : ctx `Thins` ctx') -> - (thin2 : ctx' `Thins` ctx'') -> - wknAll (wknAll sub thin1) thin2 = wknAll sub (thin2 . thin1) -wknAllHomo (Base thin) thin1 thin2 = cong Base (assoc thin2 thin1 thin) -wknAllHomo (sub :< t) thin1 thin2 = cong2 (:<) (wknAllHomo sub thin1 thin2) (wknHomo t thin1 thin2) - --- Restrict - -indexRestrict : - (thin : ctx `Thins` ctx') -> - (sub : Terms ctx'' ctx') -> - (i : Elem ty ctx) -> - index (restrict sub thin) i = index sub (index thin i) -indexRestrict thin (Base thin') i = sym $ cong Var $ indexHomo thin' thin i -indexRestrict (Drop thin) (sub :< t) i = indexRestrict thin sub i -indexRestrict (Keep thin) (sub :< t) Here = Refl -indexRestrict (Keep thin) (sub :< t) (There i) = indexRestrict thin sub i - -restrictId : (len : Len ctx) => (sub : Terms ctx' ctx) -> restrict sub (id @{len}) = sub -restrictId (Base thin) = cong Base (identityRight thin) -restrictId {len = S k} (sub :< t) = cong (:< t) (restrictId sub) - -restrictHomo : - (sub : Terms ctx ctx''') -> - (thin1 : ctx'' `Thins` ctx''') -> - (thin2 : ctx' `Thins` ctx'') -> - restrict sub (thin1 . thin2) = restrict (restrict sub thin1) thin2 -restrictHomo (Base thin) thin1 thin2 = cong Base (assoc thin thin1 thin2) -restrictHomo (sub :< t) (Drop thin1) thin2 = restrictHomo sub thin1 thin2 -restrictHomo (sub :< t) (Keep thin1) (Drop thin2) = restrictHomo sub thin1 thin2 -restrictHomo (sub :< t) (Keep thin1) (Keep thin2) = cong (:< t) $ restrictHomo sub thin1 thin2 - -wknAllRestrict : - (thin1 : ctx `Thins` ctx') -> - (sub : Terms ctx'' ctx') -> - (thin2 : ctx'' `Thins` ctx''') -> - restrict (wknAll sub thin2) thin1 = wknAll (restrict sub thin1) thin2 -wknAllRestrict thin1 (Base thin) thin2 = sym $ cong Base $ assoc thin2 thin thin1 -wknAllRestrict (Drop thin) (sub :< t) thin2 = wknAllRestrict thin sub thin2 -wknAllRestrict (Keep thin) (sub :< t) thin2 = cong (:< wkn t thin2) (wknAllRestrict thin sub thin2) - --- Substitution & Weakening - -export -wknSubst : - (t : Term ctx ty) -> - (sub : Terms ctx' ctx) -> - (thin : ctx' `Thins` ctx'') -> - wkn (subst t sub) thin = subst t (wknAll sub thin) -wknSubst (Var i) sub thin = - sym (indexWknAll sub thin i) -wknSubst (Abs t) sub thin = - cong Abs $ Calc $ - |~ wkn (subst t (wknAll sub (Drop id) :< Var Here)) (Keep thin) - ~~ subst t (wknAll (wknAll sub (Drop id)) (Keep thin) :< Var (index (Keep thin) Here)) - ...(wknSubst t (wknAll sub (Drop id) :< Var Here) (Keep thin)) - ~~ subst t (wknAll sub (Keep thin . Drop id) :< Var Here) - ...(cong (subst t . (:< Var Here)) (wknAllHomo sub (Drop id) (Keep thin))) - ~~ subst t (wknAll sub (Drop id . thin) :< Var Here) - ...(cong (subst t . (:< Var Here) . wknAll sub . Drop) $ trans (identityRight thin) (sym $ identityLeft thin)) - ~~ subst t (wknAll (wknAll sub thin) (Drop id) :< Var Here) - ...(sym $ cong (subst t . (:< Var Here)) $ wknAllHomo sub thin (Drop id)) -wknSubst (App t u) sub thin = - cong2 App (wknSubst t sub thin) (wknSubst u sub thin) -wknSubst Zero sub thin = - Refl -wknSubst (Suc t) sub thin = - cong Suc (wknSubst t sub thin) -wknSubst (Rec t u v) sub thin = - cong3 Rec (wknSubst t sub thin) (wknSubst u sub thin) (wknSubst v sub thin) - -export -substWkn : - (t : Term ctx ty) -> - (thin : ctx `Thins` ctx') -> - (sub : Terms ctx'' ctx') -> - subst (wkn t thin) sub = subst t (restrict sub thin) -substWkn (Var i) thin sub = - sym (indexRestrict thin sub i) -substWkn (Abs t) thin sub = - cong Abs $ Calc $ - |~ subst (wkn t $ Keep thin) (wknAll sub (Drop id) :< Var Here) - ~~ subst t (restrict (wknAll sub (Drop id)) thin :< Var Here) - ...(substWkn t (Keep thin) (wknAll sub (Drop id) :< Var Here)) - ~~ subst t (wknAll (restrict sub thin) (Drop id) :< Var Here) - ...(cong (subst t . (:< Var Here)) $ wknAllRestrict thin sub (Drop id)) -substWkn (App t u) thin sub = - cong2 App (substWkn t thin sub) (substWkn u thin sub) -substWkn Zero thin sub = - Refl -substWkn (Suc t) thin sub = - cong Suc (substWkn t thin sub) -substWkn (Rec t u v) thin sub = - cong3 Rec (substWkn t thin sub) (substWkn u thin sub) (substWkn v thin sub) - -namespace Equiv - public export - data Equiv : Terms ctx' ctx -> Terms ctx' ctx -> Type where - Base : Equiv (Base (Keep thin)) (Base (Drop thin) :< Var Here) - WknAll : - (len : Len ctx) => - Equiv sub sub' -> - Equiv - (wknAll sub (Drop $ id @{len}) :< Var Here) - (wknAll sub' (Drop $ id @{len}) :< Var Here) - - %name Equiv prf - -indexCong : Equiv sub sub' -> (i : Elem ty ctx) -> index sub i = index sub' i -indexCong Base Here = Refl -indexCong Base (There i) = Refl -indexCong (WknAll prf) Here = Refl -indexCong (WknAll {sub, sub'} prf) (There i) = Calc $ - |~ index (wknAll sub (Drop id)) i - ~~ wkn (index sub i) (Drop id) ...(indexWknAll sub (Drop id) i) - ~~ wkn (index sub' i) (Drop id) ...(cong (flip wkn (Drop id)) $ indexCong prf i) - ~~ index (wknAll sub' (Drop id)) i ...(sym $ indexWknAll sub' (Drop id) i) - -substCong : - (len : Len ctx') => - (t : Term ctx ty) -> - {0 sub, sub' : Terms ctx' ctx} -> - Equiv sub sub' -> - subst t sub = subst t sub' -substCong (Var i) prf = indexCong prf i -substCong (Abs t) prf = cong Abs (substCong t (WknAll prf)) -substCong (App t u) prf = cong2 App (substCong t prf) (substCong u prf) -substCong Zero prf = Refl -substCong (Suc t) prf = cong Suc (substCong t prf) -substCong (Rec t u v) prf = cong3 Rec (substCong t prf) (substCong u prf) (substCong v prf) - -substBase : (t : Term ctx ty) -> (thin : ctx `Thins` ctx') -> subst t (Base thin) = wkn t thin -substBase (Var i) thin = Refl -substBase (Abs t) thin = - rewrite identityLeft thin in - cong Abs $ Calc $ - |~ subst t (Base (Drop thin) :< Var Here) - ~~ subst t (Base $ Keep thin) ...(sym $ substCong t Base) - ~~ wkn t (Keep thin) ...(substBase t (Keep thin)) -substBase (App t u) thin = cong2 App (substBase t thin) (substBase u thin) -substBase Zero thin = Refl -substBase (Suc t) thin = cong Suc (substBase t thin) -substBase (Rec t u v) thin = cong3 Rec (substBase t thin) (substBase u thin) (substBase v thin) - --- Substitution Composition - -indexComp : - (sub1 : Terms ctx' ctx) -> - (sub2 : Terms ctx'' ctx') -> - (i : Elem ty ctx) -> - index (sub2 . sub1) i = subst (index sub1 i) sub2 -indexComp (Base thin) sub2 i = indexRestrict thin sub2 i -indexComp (sub1 :< t) sub2 Here = Refl -indexComp (sub1 :< t) sub2 (There i) = indexComp sub1 sub2 i - -wknAllComp : - (sub1 : Terms ctx' ctx) -> - (sub2 : Terms ctx'' ctx') -> - (thin : ctx'' `Thins` ctx''') -> - wknAll sub2 thin . sub1 = wknAll (sub2 . sub1) thin -wknAllComp (Base thin') sub2 thin = wknAllRestrict thin' sub2 thin -wknAllComp (sub1 :< t) sub2 thin = - cong2 (:<) - (wknAllComp sub1 sub2 thin) - (sym $ wknSubst t sub2 thin) - -compDrop : - (sub1 : Terms ctx' ctx) -> - (thin : ctx' `Thins` ctx'') -> - (sub2 : Terms ctx''' ctx'') -> - sub2 . wknAll sub1 thin = restrict sub2 thin . sub1 -compDrop (Base thin') thin sub2 = restrictHomo sub2 thin thin' -compDrop (sub1 :< t) thin sub2 = cong2 (:<) (compDrop sub1 thin sub2) (substWkn t thin sub2) - -export -compWknAll : - (sub1 : Terms ctx' ctx) -> - (sub2 : Terms ctx''' ctx'') -> - (thin : ctx' `Thins` ctx'') -> - sub2 . wknAll sub1 thin = restrict sub2 thin . sub1 -compWknAll (Base thin') sub2 thin = restrictHomo sub2 thin thin' -compWknAll (sub1 :< t) sub2 thin = cong2 (:<) (compWknAll sub1 sub2 thin) (substWkn t thin sub2) - -export -baseComp : - (thin : ctx' `Thins` ctx'') -> - (sub : Terms ctx' ctx) -> - Base thin . sub = wknAll sub thin -baseComp thin (Base thin') = Refl -baseComp thin (sub :< t) = cong2 (:<) (baseComp thin sub) (substBase t thin) - --- Substitution - -export -substId : (len : Len ctx) => (t : Term ctx ty) -> subst t (Base $ id @{len}) = t -substId (Var i) = cong Var (indexId i) -substId (Abs t) = - rewrite identitySquared len in - cong Abs $ trans (sym $ substCong t Base) (substId t) -substId (App t u) = cong2 App (substId t) (substId u) -substId Zero = Refl -substId (Suc t) = cong Suc (substId t) -substId (Rec t u v) = cong3 Rec (substId t) (substId u) (substId v) - -export -substHomo : - (t : Term ctx ty) -> - (sub1 : Terms ctx' ctx) -> - (sub2 : Terms ctx'' ctx') -> - subst (subst t sub1) sub2 = subst t (sub2 . sub1) -substHomo (Var i) sub1 sub2 = - sym $ indexComp sub1 sub2 i -substHomo (Abs t) sub1 sub2 = - cong Abs $ Calc $ - |~ subst (subst t (wknAll sub1 (Drop id) :< Var Here)) (wknAll sub2 (Drop id) :< Var Here) - ~~ subst t ((wknAll sub2 (Drop id) :< Var Here) . (wknAll sub1 (Drop id) :< Var Here)) - ...(substHomo t (wknAll sub1 (Drop id) :< Var Here) (wknAll sub2 (Drop id) :< Var Here)) - ~~ subst t ((wknAll sub2 (Drop id) :< Var Here) . wknAll sub1 (Drop id) :< Var Here) - ...(Refl) - ~~ subst t (restrict (wknAll sub2 (Drop id)) id . sub1 :< Var Here) - ...(cong (subst t . (:< Var Here)) $ compDrop sub1 (Drop id) (wknAll sub2 (Drop id) :< Var Here)) - ~~ subst t (wknAll sub2 (Drop id) . sub1 :< Var Here) - ...(cong (subst t . (:< Var Here) . (. sub1)) $ restrictId (wknAll sub2 (Drop id))) - ~~ subst t (wknAll (sub2 . sub1) (Drop id) :< Var Here) - ...(cong (subst t . (:< Var Here)) $ wknAllComp sub1 sub2 (Drop id)) -substHomo (App t u) sub1 sub2 = - cong2 App (substHomo t sub1 sub2) (substHomo u sub1 sub2) -substHomo Zero sub1 sub2 = - Refl -substHomo (Suc t) sub1 sub2 = - cong Suc (substHomo t sub1 sub2) -substHomo (Rec t u v) sub1 sub2 = - cong3 Rec (substHomo t sub1 sub2) (substHomo u sub1 sub2) (substHomo v sub1 sub2) diff --git a/src/Total/Term/CoDebruijn.idr b/src/Total/Term/CoDebruijn.idr deleted file mode 100644 index 0efcdbb..0000000 --- a/src/Total/Term/CoDebruijn.idr +++ /dev/null @@ -1,317 +0,0 @@ -module Total.Term.CoDebruijn - -import public Data.SnocList.Elem -import public Thinning -import Syntax.PreorderReasoning -import Total.Term - -%prefix_record_projections off - --- Definition ------------------------------------------------------------------ - -public export -data CoTerm : Ty -> SnocList Ty -> Type where - Var : CoTerm ty [<ty] - Abs : Binds [<ty] (CoTerm ty') ctx -> CoTerm (ty ~> ty') ctx - App : {ty : Ty} -> Pair (CoTerm (ty ~> ty')) (CoTerm ty) ctx -> CoTerm ty' ctx - Zero : CoTerm N [<] - Suc : CoTerm N ctx -> CoTerm N ctx - Rec : Pair (CoTerm N) (Pair (CoTerm ty) (CoTerm (ty ~> ty))) ctx -> CoTerm ty ctx - -%name CoTerm t, u, v - -public export -FullTerm : Ty -> SnocList Ty -> Type -FullTerm ty ctx = Thinned (CoTerm ty) ctx - --- Smart Constructors ---------------------------------------------------------- - -public export -var : Len ctx => Elem ty ctx -> FullTerm ty ctx -var i = Var `Over` point i - -public export -abs : FullTerm ty' (ctx :< ty) -> FullTerm (ty ~> ty') ctx -abs = map Abs . MkBound (S Z) - -public export -app : {ty : Ty} -> FullTerm (ty ~> ty') ctx -> FullTerm ty ctx -> FullTerm ty' ctx -app t u = map App (MkPair t u) - -public export -zero : Len ctx => FullTerm N ctx -zero = Zero `Over` empty - -public export -suc : FullTerm N ctx -> FullTerm N ctx -suc = map Suc - -public export -rec : FullTerm N ctx -> FullTerm ty ctx -> FullTerm (ty ~> ty) ctx -> FullTerm ty ctx -rec t u v = map Rec $ MkPair t (MkPair u v) - --- Substitutions --------------------------------------------------------------- - -public export -data CoTerms : SnocList Ty -> SnocList Ty -> Type where - Lin : CoTerms [<] ctx' - (:<) : CoTerms ctx ctx' -> FullTerm ty ctx' -> CoTerms (ctx :< ty) ctx' - -%name CoTerms sub - -public export -index : CoTerms ctx ctx' -> Elem ty ctx -> FullTerm ty ctx' -index (sub :< t) Here = t -index (sub :< t) (There i) = index sub i - -public export -wknAll : CoTerms ctx ctx' -> ctx' `Thins` ctx'' -> CoTerms ctx ctx'' -wknAll [<] thin = [<] -wknAll (sub :< t) thin = wknAll sub thin :< wkn t thin - -public export -shift : CoTerms ctx ctx' -> CoTerms ctx (ctx' :< ty) -shift [<] = [<] -shift (sub :< t) = shift sub :< drop t - -public export -lift : Len ctx' => CoTerms ctx ctx' -> CoTerms (ctx :< ty) (ctx' :< ty) -lift sub = shift sub :< var Here - -public export -restrict : CoTerms ctx' ctx'' -> ctx `Thins` ctx' -> CoTerms ctx ctx'' -restrict [<] Empty = [<] -restrict (sub :< t) (Drop thin) = restrict sub thin -restrict (sub :< t) (Keep thin) = restrict sub thin :< t - -public export -Base : (len : Len ctx') => ctx `Thins` ctx' -> CoTerms ctx ctx' -Base Empty = [<] -Base {len = S k} (Drop thin) = shift (Base thin) -Base {len = S k} (Keep thin) = lift (Base thin) - --- Substitution Operation ------------------------------------------------------ - -public export -subst : Len ctx' => FullTerm ty ctx -> CoTerms ctx ctx' -> FullTerm ty ctx' -public export -subst' : Len ctx' => CoTerm ty ctx -> CoTerms ctx ctx' -> FullTerm ty ctx' - -subst (t `Over` thin) sub = subst' t (restrict sub thin) - -subst' Var sub = index sub Here -subst' (Abs (MakeBound t (Drop Empty))) sub = abs (subst' t $ shift sub) -subst' (Abs (MakeBound t (Keep Empty))) sub = abs (subst' t $ lift sub) -subst' (App (MakePair t u _)) sub = app (subst t sub) (subst u sub) -subst' Zero sub = zero -subst' (Suc t) sub = suc (subst' t sub) -subst' (Rec (MakePair t (MakePair u v _ `Over` thin) _)) sub = - rec (subst t sub) (subst u (restrict sub thin)) (subst v (restrict sub thin)) - --- Initiality ------------------------------------------------------------------ - -toTerm' : CoTerm ty ctx -> ctx `Thins` ctx' -> Term ctx' ty -toTerm' Var thin = Var (index thin Here) -toTerm' (Abs (MakeBound t (Drop Empty))) thin = Abs (toTerm' t (Drop thin)) -toTerm' (Abs (MakeBound t (Keep Empty))) thin = Abs (toTerm' t (Keep thin)) -toTerm' (App (MakePair (t `Over` thin1) (u `Over` thin2) _)) thin = - App (toTerm' t (thin . thin1)) (toTerm' u (thin . thin2)) -toTerm' Zero thin = Zero -toTerm' (Suc t) thin = Suc (toTerm' t thin) -toTerm' - (Rec - (MakePair - (t `Over` thin1) - (MakePair (u `Over` thin2) (v `Over` thin3) _ `Over` thin') _)) - thin = - Rec - (toTerm' t (thin . thin1)) - (toTerm' u ((thin . thin') . thin2)) - (toTerm' v ((thin . thin') . thin3)) - -export -toTerm : FullTerm ty ctx -> Term ctx ty -toTerm (t `Over` thin) = toTerm' t thin - -public export -toTerms : Len ctx' => CoTerms ctx ctx' -> Terms ctx' ctx -toTerms [<] = Base empty -toTerms (sub :< t) = toTerms sub :< toTerm t - -export -Cast (FullTerm ty ctx) (Term ctx ty) where - cast = toTerm - -export -Len ctx' => Cast (CoTerms ctx ctx') (Terms ctx' ctx) where - cast = toTerms - -export -Len ctx => Cast (Term ctx ty) (FullTerm ty ctx) where - cast (Var i) = Var `Over` point i - cast (Abs t) = abs (cast t) - cast (App {ty} t u) = app {ty} (cast t) (cast u) - cast Zero = zero - cast (Suc t) = suc (cast t) - cast (Rec t u v) = rec (cast t) (cast u) (cast v) - --- Properties ------------------------------------------------------------------ - -wknToTerm' : - (t : CoTerm ty ctx) -> - (thin : ctx `Thins` ctx') -> - (thin' : ctx' `Thins` ctx''') -> - wkn (toTerm' t thin) thin' = toTerm' t (thin' . thin) -wknToTerm' Var thin thin' = cong Var (indexHomo thin' thin Here) -wknToTerm' (Abs (MakeBound t (Drop Empty))) thin thin' = - cong Abs (wknToTerm' t (Drop thin) (Keep thin')) -wknToTerm' (Abs (MakeBound t (Keep Empty))) thin thin' = - cong Abs (wknToTerm' t (Keep thin) (Keep thin')) -wknToTerm' (App (MakePair (t `Over` thin1) (u `Over` thin2) _)) thin thin' = - rewrite sym $ assoc thin' thin thin1 in - rewrite sym $ assoc thin' thin thin2 in - cong2 App (wknToTerm' t (thin . thin1) thin') (wknToTerm' u (thin . thin2) thin') -wknToTerm' Zero thin thin' = Refl -wknToTerm' (Suc t) thin thin' = cong Suc (wknToTerm' t thin thin') -wknToTerm' - (Rec - (MakePair - (t `Over` thin1) - (MakePair (u `Over` thin2) (v `Over` thin3) _ `Over` thin'') _)) - thin - thin' = - rewrite sym $ assoc thin' thin thin1 in - rewrite sym $ assoc (thin' . thin) thin'' thin2 in - rewrite sym $ assoc thin' thin (thin'' . thin2) in - rewrite sym $ assoc thin thin'' thin2 in - rewrite sym $ assoc (thin' . thin) thin'' thin3 in - rewrite sym $ assoc thin' thin (thin'' . thin3) in - rewrite sym $ assoc thin thin'' thin3 in - cong3 Rec - (wknToTerm' t (thin . thin1) thin') - (wknToTerm' u (thin . (thin'' . thin2)) thin') - (wknToTerm' v (thin . (thin'' . thin3)) thin') - -export -wknToTerm : - (t : FullTerm ty ctx) -> - (thin : ctx `Thins` ctx') -> - wkn (toTerm t) thin = toTerm (wkn t thin) -wknToTerm (t `Over` thin') thin = wknToTerm' t thin' thin - -export -toTermVar : Len ctx => (i : Elem ty ctx) -> toTerm (var i) = Var i -toTermVar i = cong Var $ indexPoint i - -export -toTermApp : - (t : FullTerm (ty ~> ty') ctx) -> - (u : FullTerm ty ctx) -> - toTerm (app t u) = App (toTerm t) (toTerm u) -toTermApp (t `Over` thin1) (u `Over` thin2) = - cong2 App - (cong (toTerm' t) $ irrelevantEq $ triangleCorrect (coprod thin1 thin2).left) - (cong (toTerm' u) $ irrelevantEq $ triangleCorrect (coprod thin1 thin2).right) - -indexShift : - (sub : CoTerms ctx ctx') -> - (i : Elem ty ctx) -> - index (shift sub) i = drop (index sub i) -indexShift (sub :< t) Here = Refl -indexShift (sub :< t) (There i) = indexShift sub i - -indexBase : (thin : [<ty] `Thins` ctx') -> index (Base thin) Here = Var `Over` thin -indexBase (Drop thin) = trans (indexShift (Base thin) Here) (cong drop (indexBase thin)) -indexBase (Keep thin) = irrelevantEq $ cong ((Var `Over`) . Keep) $ emptyUnique empty thin - -restrictShift : - (sub : CoTerms ctx' ctx'') -> - (thin : ctx `Thins` ctx') -> - restrict (shift sub) thin = shift (restrict sub thin) -restrictShift [<] Empty = Refl -restrictShift (sub :< t) (Drop thin) = restrictShift sub thin -restrictShift (sub :< t) (Keep thin) = cong (:< drop t) (restrictShift sub thin) - -restrictBase : - (thin2 : ctx' `Thins` ctx'') -> - (thin1 : ctx `Thins` ctx') -> - CoDebruijn.restrict (Base thin2) thin1 = Base (thin2 . thin1) -restrictBase Empty Empty = Refl -restrictBase (Drop thin2) thin1 = - trans - (restrictShift (Base thin2) thin1) - (cong shift $ restrictBase thin2 thin1) -restrictBase (Keep thin2) (Drop thin1) = - trans - (restrictShift (Base thin2) thin1) - (cong shift $ restrictBase thin2 thin1) -restrictBase (Keep thin2) (Keep thin1) = - cong (:< (Var `Over` point Here)) $ - trans - (restrictShift (Base thin2) thin1) - (cong shift $ restrictBase thin2 thin1) - -substBase : - (t : CoTerm ty ctx) -> - (thin : ctx `Thins` ctx') -> - subst' t (Base thin) = t `Over` thin -substBase Var thin = indexBase thin -substBase (Abs (MakeBound t (Drop Empty))) thin = - Calc $ - |~ map Abs (MkBound (S Z) (subst' t (shift $ Base thin))) - ~~ map Abs (MkBound (S Z) (t `Over` Drop thin)) - ...(cong (map Abs . MkBound (S Z)) $ substBase t (Drop thin)) - ~~ map Abs (MakeBound t (Drop Empty) `Over` thin) - ...(Refl) - ~~ (Abs (MakeBound t (Drop Empty)) `Over` thin) - ...(Refl) -substBase (Abs (MakeBound t (Keep Empty))) thin = - Calc $ - |~ map Abs (MkBound (S Z) (subst' t (lift $ Base thin))) - ~~ map Abs (MkBound (S Z) (t `Over` Keep thin)) - ...(cong (map Abs . MkBound (S Z)) $ substBase t (Keep thin)) - ~~ map Abs (MakeBound t (Keep Empty) `Over` thin) - ...(Refl) - ~~ (Abs (MakeBound t (Keep Empty)) `Over` thin) - ...(Refl) -substBase (App (MakePair (t `Over` thin1) (u `Over` thin2) cover)) thin = - rewrite restrictBase thin thin1 in - rewrite restrictBase thin thin2 in - rewrite substBase t (thin . thin1) in - rewrite substBase u (thin . thin2) in - rewrite coprodEta thin cover in - Refl -substBase Zero thin = cong (Zero `Over`) $ irrelevantEq $ emptyUnique empty thin -substBase (Suc t) thin = cong (map Suc) $ substBase t thin -substBase - (Rec (MakePair - (t `Over` thin1) - (MakePair - (u `Over` thin2) - (v `Over` thin3) - cover' - `Over` thin') - cover)) - thin = - rewrite restrictBase thin thin1 in - rewrite restrictBase thin thin' in - rewrite restrictBase (thin . thin') thin2 in - rewrite restrictBase (thin . thin') thin3 in - rewrite substBase t (thin . thin1) in - rewrite substBase u ((thin . thin') . thin2) in - rewrite substBase v ((thin . thin') . thin3) in - rewrite coprodEta (thin . thin') cover' in - rewrite coprodEta thin cover in - Refl - -export -substId : (t : FullTerm ty ctx) -> subst t (Base Thinning.id) = t -substId (t `Over` thin) = - Calc $ - |~ subst' t (restrict (Base id) thin) - ~~ subst' t (Base $ id . thin) - ...(cong (subst' t) $ restrictBase id thin) - ~~ subst' t (Base thin) - ...(cong (subst' t . Base) $ identityLeft thin) - ~~ (t `Over` thin) - ...(substBase t thin) |