From bf07a9fe3ee4ff06fe186e33221f7f91871b9217 Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Tue, 6 Jun 2023 12:25:26 +0100 Subject: Write an encoding for data types. --- src/Total/Encoded/Util.idr | 437 +++++++++++++++++++++++++++++++++++++++++++++ src/Total/LogRel.idr | 50 ++++-- src/Total/NormalForm.idr | 111 ++++++++++++ src/Total/Reduction.idr | 5 + src/Total/Syntax.idr | 83 +++++++++ src/Total/Term.idr | 9 + 6 files changed, 683 insertions(+), 12 deletions(-) create mode 100644 src/Total/Encoded/Util.idr create mode 100644 src/Total/Syntax.idr (limited to 'src/Total') diff --git a/src/Total/Encoded/Util.idr b/src/Total/Encoded/Util.idr new file mode 100644 index 0000000..705d74b --- /dev/null +++ b/src/Total/Encoded/Util.idr @@ -0,0 +1,437 @@ +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 : Term ctx B + True = Zero + + export + False : Term ctx B + False = Suc Zero + + export + If : Term ctx B -> Term ctx ty -> Term ctx ty -> Term ctx ty + If t u v = Rec t u (Abs $ wkn v (Drop Id)) + +namespace Arb + export + arb : {ty : Ty} -> Term [<] 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 + injL : {t, u : Ty} -> Term [<] (t ~> (t <+> u)) + export + injR : {t, u : Ty} -> Term [<] (u ~> (t <+> u)) + export + prjL : {t, u : Ty} -> Term [<] ((t <+> u) ~> t) + export + prjR : {t, u : Ty} -> Term [<] ((t <+> u) ~> u) + + injL {t = N, u = N} = Abs' (S Z) id + injL {t = N, u = u ~> u'} = Abs' (S $ S Z) (\n, _ => App (lift (prjR . injL)) n) + injL {t = t ~> t', u = N} = Abs' (S Z) id + injL {t = t ~> t', u = u ~> u'} = Abs' (S Z) (\f => lift injL . f . lift prjL) + + injR {t = N, u = N} = Abs' (S Z) id + injR {t = N, u = u ~> u'} = Abs' (S Z) id + injR {t = t ~> t', u = N} = Abs' (S $ S Z) (\n, _ => App (lift (prjL . injR)) n) + injR {t = t ~> t', u = u ~> u'} = Abs' (S Z) (\f => lift injR . f . lift prjR) + + prjL {t = N, u = N} = Abs' (S Z) id + prjL {t = N, u = u ~> u'} = Abs' (S Z) (\f => App (lift (prjL . injR) . f) (lift $ arb)) + prjL {t = t ~> t', u = N} = Abs' (S Z) id + prjL {t = t ~> t', u = u ~> u'} = Abs' (S Z) (\f => lift prjL . f . lift injL) + + prjR {t = N, u = N} = Abs' (S Z) id + prjR {t = N, u = u ~> u'} = Abs' (S Z) id + prjR {t = t ~> t', u = N} = Abs' (S Z) (\f => App (lift (prjR . injL) . f) (lift $ arb)) + prjR {t = t ~> t', u = u ~> u'} = Abs' (S Z) (\f => lift prjR . f . lift injR) + +namespace Unit + export + Unit : Ty + Unit = N + +namespace Pair + export + (*) : Ty -> Ty -> Ty + t * u = B ~> (t <+> u) + + export + pair : {t, u : Ty} -> Term [<] (t ~> u ~> (t * u)) + pair = Abs' (S $ S $ S Z) + (\fst, snd, b => If b (App (lift injL) fst) (App (lift injR) snd)) + + export + fst : {t, u : Ty} -> Term [<] ((t * u) ~> t) + fst = Abs' (S Z) (\p => App (lift prjL . p) True) + + export + snd : {t, u : Ty} -> Term [<] ((t * u) ~> u) + snd = Abs' (S Z) (\p => App (lift prjR . p) False) + + export + mapSnd : {t, u, v : Ty} -> Term [<] ((u ~> v) ~> (t * u) ~> (t * v)) + mapSnd = Abs' (S $ S Z) (\f, p => App' (lift pair) [ Ty + Product = foldl (*) Unit + + export + pair' : {tys : SnocList Ty} -> Term [<] (tys ~>* Product tys) + pair' {tys = [<]} = arb + pair' {tys = tys :< ty} = Abs' (S $ S Z) (\p, t => App' (lift pair) [ Elem ty tys -> Term [<] (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 : length tys = length tys'} -> + All (Term ctx) (zipWith (~>) tys tys') -> + Term ctx (Product tys ~> Product tys') + mapProd {tys = [<], tys' = [<]} [<] = Abs (Var Here) + mapProd {tys = tys :< ty, tys' = tys' :< ty', prf} (fs :< f) = + Abs' (S Z) + (\p => + App' (lift pair) + [ 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} -> + Term [<] ((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} -> Term [<] (Vect 0 ty) + Nil = arb + + export + Cons : {n : Nat} -> {ty : Ty} -> Term [<] (ty ~> Vect n ty ~> Vect (S n) ty) + Cons = Abs' (S $ S Z) (\t, ts => App' (lift pair) [ {ty : Ty} -> Term [<] (Vect (S n) ty ~> ty) + head = snd + + export + tail : {n : Nat} -> {ty : Ty} -> Term [<] (Vect (S n) ty ~> Vect n ty) + tail = fst + + export + index : {n : Nat} -> {ty : Ty} -> (i : Fin n) -> Term [<] (Vect n ty ~> ty) + index FZ = head + index (FS i) = index i . tail + + export + enumerate : (n : Nat) -> Term [<] (Vect n N) + enumerate 0 = arb + enumerate (S k) = App' pair [ Ty -> Ty + t + u = B * (t <+> u) + + export + left : {t, u : Ty} -> Term [<] (t ~> (t + u)) + left = Abs' (S Z) (\e => App' (lift pair) [ Term [<] (u ~> (t + u)) + right = Abs' (S Z) (\e => App' (lift pair) [ Term [<] ((t ~> ty) ~> (u ~> ty) ~> (t + u) ~> ty) + case' = Abs' (S $ S $ S Z) + (\f, g, s => + If (App (lift fst) s) + (App (f . lift (prjL . snd)) s) + (App (g . lift (prjR . snd)) s)) + + 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)) -> + Term [<] (ty ~> Sum' ty' tys) + put' {tys = []} Here = Abs' (S Z) id + put' {tys = _ :: _} Here = left + put' {tys = _ :: _} (There i) = right . put' i + + export + put : {tys : List1 Ty} -> {ty : Ty} -> (i : Elem ty (forget tys)) -> Term [<] (ty ~> Sum tys) + put {tys = _ ::: _} i = put' i + + caseAll' : + {ctx : SnocList Ty} -> + {ty, ty' : Ty} -> + {tys : List Ty} -> + All (Term ctx . (~> ty)) (ty' :: tys) -> + Term ctx (Sum' ty' tys ~> ty) + caseAll' (t :: []) = t + caseAll' (t :: u :: ts) = App' (lift case') [ + {tys : List1 Ty} -> + {ty : Ty} -> + All (Term ctx . (~> ty)) (forget tys) -> + Term ctx (Sum tys ~> ty) + caseAll {tys = _ ::: _} = caseAll' + +namespace Nat + export + IsZero : Term [<] (N ~> B) + IsZero = Abs' (S Z) (\m => Rec m (lift True) (Abs (lift False))) + + export + Add : Term [<] (N ~> N ~> N) + Add = Abs' (S $ S Z) (\m, n => Rec m n (Abs' (S Z) Suc)) + + export + sum : {n : Nat} -> Term [<] (Vect n N ~> N) + sum {n = 0} = Abs Zero + sum {n = S k} = Abs' (S Z) + (\ns => App' (lift Add) [ N) + Pred = Abs' (S Z) + (\m => + App' (lift case') + [ App (lift right) (Suc n)) + ]) + ]) + + export + Sub : Term [<] (N ~> N ~> N) + Sub = Abs' (S $ S Z) (\m, n => Rec n m (lift Pred)) + + export + LE : Term [<] (N ~> N ~> B) + LE = Abs' (S Z) (\m => lift IsZero . App (lift Sub) m) + + export + LT : Term [<] (N ~> N ~> B) + LT = Abs' (S Z) (\m => App (lift LE) (Suc m)) + + export + Cond : + {ctx : SnocList Ty} -> + {ty : Ty} -> + List (Term ctx N, Term ctx (N ~> ty)) -> + Term ctx (N ~> ty) + Cond [] = lift arb + Cond ((n, v) :: xs) = + Abs' (S Z) + (\t => + If (App' (lift LE) [ 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 ~> fill c N] + -- ^ ^ ^- tags and next positions + -- | |- offset + -- |- pred (number of tags in structure) + + mapShape : + {shape : Shape} -> + {ty, ty' : Ty} -> + Term [<] ((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 : Term ctx (Vect n (fix c))) -> + (acc : Term ctx N) -> + List (Term ctx N, Term ctx (N ~> N)) + 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) [ + {c : Container} -> + {n : Nat} -> + (ts : Term ctx (Vect n (fix c))) -> + (acc : Term ctx N) -> + List (Term ctx N, Term ctx (N ~> fill c N)) + 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) [ + {shape : Shape} -> + Elem shape (forget c) -> + Term [<] (fillShape shape (fix c) ~> fix c) + intro {shape = (shape, n)} i = Abs' (S Z) + (\t => + App' (lift $ pair' {tys = [ N, N ~> fill c N]}) + [ + {ctx : SnocList Ty} -> + {ty : Ty} -> + All (Term ctx . (~> ty) . flip Data.fillShape ty) (forget c) -> + Term ctx (fix c ~> ty) + elim cases = Abs' (S Z) + (\t => + let tags = Suc (App (lift $ project $ There $ There Here) t) in + let offset = App (lift $ project $ There Here) (wkn t (Drop $ Drop Id)) in + let vals = App (lift $ project $ Here) (wkn t (Drop $ Drop Id)) in + App' + (Rec tags + (lift arb) + (Abs' (S $ S Z) (\rec, n => + App + (caseAll {tys = map (flip fillShape N) c} + (rewrite forgetMap (flip fillShape N) c in + gmap + (\f => + wkn f (Drop $ Drop $ Drop Id) . + App (lift mapShape) (rec . App (lift Add) (App offset n))) + cases) . + vals) + 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 index b0d60ea..1ed7276 100644 --- a/src/Total/LogRel.idr +++ b/src/Total/LogRel.idr @@ -6,6 +6,7 @@ import Total.Term %prefix_record_projections off +public export LogRel : {ctx : SnocList Ty} -> (P : {ctx, ty : _} -> Term ctx ty -> Type) -> @@ -21,6 +22,7 @@ LogRel p {ty = ty ~> ty'} t = LogRel p u -> LogRel p (App (wkn t thin) u)) +export escape : {P : {ctx, ty : _} -> Term ctx ty -> Type} -> {ty : Ty} -> @@ -30,6 +32,7 @@ escape : escape {ty = N} pt = pt escape {ty = ty ~> ty'} (pt, app) = pt +public export record PreserveHelper (P : {ctx, ty : _} -> Term ctx ty -> Type) (R : {ctx, ty : _} -> Term ctx ty -> Term ctx ty -> Type) where @@ -48,11 +51,22 @@ record PreserveHelper {ty : Ty} -> {0 t, u : Term ctx ty} -> P t -> - R t u -> + (0 _ : R t u) -> P u %name PreserveHelper help +export +backStepHelper : + {0 P : {ctx, ty : _} -> Term ctx ty -> Type} -> + (forall ctx, ty. {0 t, u : Term ctx ty} -> P t -> (0 _ : u > t) -> P u) -> + PreserveHelper P (flip (>)) +backStepHelper pres = + MkPresHelper + (\thin, v, step => AppCong1 (wknStep step)) + pres + +export preserve : {P : {ctx, ty : _} -> Term ctx ty -> Type} -> {R : {ctx, ty : _} -> Term ctx ty -> Term ctx ty -> Type} -> @@ -60,7 +74,7 @@ preserve : {0 t, u : Term ctx ty} -> PreserveHelper P R -> LogRel P t -> - R t u -> + (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 = @@ -81,7 +95,7 @@ data AllLogRel : (P : {ctx, ty : _} -> Term ctx ty -> Type) -> Terms ctx' ctx -> index : {P : {ctx, ty : _} -> Term ctx ty -> Type} -> - (forall ty. (i : Elem ty ctx') -> LogRel P (Var i)) -> + ((i : Elem ty ctx') -> LogRel P (Var i)) -> {sub : Terms ctx' ctx} -> AllLogRel P sub -> (i : Elem ty ctx) -> @@ -102,21 +116,24 @@ Valid p t = (allRel : AllLogRel p sub) -> LogRel p (subst t sub) +public export record ValidHelper (P : {ctx, ty : _} -> Term ctx ty -> Type) where constructor MkValidHelper - var : forall ctx, ty. (i : Elem ty ctx) -> LogRel P (Var i) - abs : forall ctx, ty, ty'. {0 t : Term (ctx :< ty) ty'} -> LogRel P t -> P (Abs t) + var : forall ctx. {ty : Ty} -> (i : Elem ty ctx) -> LogRel P (Var i) + abs : forall ctx, ty. {ty' : Ty} -> {0 t : Term (ctx :< ty) ty'} -> LogRel P t -> P (Abs t) zero : forall ctx. P {ctx} Zero suc : forall ctx. {0 t : Term ctx N} -> P t -> P (Suc t) - rec : forall ctx, ty. + rec : + {ctx : SnocList Ty} -> + {ty : Ty} -> {0 t : Term ctx N} -> - {0 u : Term ctx ty} -> - {0 v : Term ctx (ty ~> ty)} -> + {u : Term ctx ty} -> + {v : Term ctx (ty ~> ty)} -> LogRel P t -> LogRel P u -> LogRel P v -> LogRel P (Rec t u v) - step : forall ctx, ty. {0 t, u : Term ctx ty} -> P t -> u > t -> P u + step : forall ctx, ty. {0 t, u : Term ctx ty} -> P t -> (0 _ : u > t) -> P u wkn : forall ctx, ctx', ty. {0 t : Term ctx ty} -> P t -> @@ -150,6 +167,7 @@ wknAllRel : wknAllRel help Base thin = Base wknAllRel help (allRels :< rel) thin = wknAllRel help allRels thin :< wknRel help rel thin +export allValid : {P : {ctx, ty : _} -> Term ctx ty -> Type} -> {ctx : SnocList Ty} -> @@ -169,8 +187,6 @@ allValid help (Abs t) sub allRels = help.abs rec , \thin, u, rel => let - helper : PreserveHelper P (flip (>)) - helper = MkPresHelper (\thin, v, step => AppCong1 (wknStep step)) help.step eq : (subst (wkn (subst t (wknAll sub (Drop Id) :< Var Here)) (keep thin)) (Base Id :< u) = subst t (wknAll sub thin :< u)) @@ -190,7 +206,7 @@ allValid help (Abs t) sub allRels = ...(cong (subst t . (:< u)) $ baseComp thin sub) in preserve - helper + (backStepHelper help.step) (valid (wknAll sub thin :< u) (wknAllRel help allRels thin :< rel)) (replace {p = (App (wkn (subst (Abs t) sub) thin) u >)} eq @@ -209,3 +225,13 @@ allValid help (Rec t u v) sub allRels = let relu = allValid help u sub allRels in let relv = allValid help v sub allRels in help.rec relt relu relv + +export +allRel : + {P : {ctx, ty : _} -> Term ctx ty -> Type} -> + {ctx : SnocList Ty} -> + {ty : Ty} -> + ValidHelper P -> + (t : Term ctx ty) -> + P t +allRel help t = rewrite sym $ substId t in escape (allValid help t (Base Id) Base) diff --git a/src/Total/NormalForm.idr b/src/Total/NormalForm.idr index 93a1da7..b5580b5 100644 --- a/src/Total/NormalForm.idr +++ b/src/Total/NormalForm.idr @@ -1,5 +1,6 @@ module Total.NormalForm +import Total.LogRel import Total.Reduction import Total.Term @@ -32,3 +33,113 @@ record NormalForm (0 t : Term ctx ty) where 0 normal : Normal term %name NormalForm nf + +-- Strong Normalization Proof -------------------------------------------------- + +invApp : Normal (App t u) -> Neutral (App t u) +invApp (Ntrl n) = n + +invRec : Normal (Rec t u v) -> Neutral (Rec t u v) +invRec (Ntrl n) = n + +invSuc : Normal (Suc t) -> Normal t +invSuc (Suc n) = n + +wknNe : Neutral t -> Neutral (wkn t thin) +wknNf : Normal t -> Normal (wkn t thin) + +wknNe Var = Var +wknNe (App n m) = App (wknNe n) (wknNf m) +wknNe (Rec n m k) = Rec (wknNe n) (wknNf m) (wknNf k) + +wknNf (Ntrl n) = Ntrl (wknNe n) +wknNf (Abs n) = Abs (wknNf n) +wknNf Zero = Zero +wknNf (Suc n) = Suc (wknNf n) + +backStepsNf : NormalForm t -> (0 _ : u >= t) -> NormalForm u +backStepsNf nf steps = MkNf nf.term (steps ++ nf.steps) nf.normal + +backStepsRel : + {ty : Ty} -> + {0 t, u : Term ctx ty} -> + LogRel (\t => NormalForm t) t -> + (0 _ : u >= t) -> + LogRel (\t => NormalForm t) u +backStepsRel = + preserve {R = flip (>=)} + (MkPresHelper (\thin, v, steps => AppCong1' (wknSteps steps)) backStepsNf) + +ntrlRel : {ty : Ty} -> {t : Term ctx ty} -> (0 _ : Neutral t) -> LogRel (\t => NormalForm t) t +ntrlRel {ty = N} n = MkNf t [<] (Ntrl n) +ntrlRel {ty = ty ~> ty'} n = + ( MkNf t [<] (Ntrl n) + , \thin, u, rel => + backStepsRel + (ntrlRel (App (wknNe n) (escape rel).normal)) + (AppCong2' (escape rel).steps) + ) + +recNf' : + {ctx : SnocList Ty} -> + {ty : Ty} -> + {u : Term ctx ty} -> + {v : Term ctx (ty ~> ty)} -> + (t' : Term ctx N) -> + (0 n : Normal t') -> + LogRel (\t => NormalForm t) u -> + LogRel (\t => NormalForm t) v -> + LogRel (\t => NormalForm t) (Rec t' u v) +recNf' Zero n relU relV = backStepsRel relU [ App (wkn v Id) (Rec t' u v) = rewrite wknId v in RecSuc in + backStepsRel (snd relV Id _ rec) [ ty} relV in + backStepsRel + (ntrlRel (Rec Var nfU.normal nfV.normal)) + (RecCong2' nfU.steps ++ RecCong3' nfV.steps) +recNf' t'@(App _ _) n relU relV = + let nfU = escape relU in + let nfV = escape {ty = ty ~> ty} relV in + backStepsRel + (ntrlRel (Rec (invApp n) nfU.normal nfV.normal)) + (RecCong2' nfU.steps ++ RecCong3' nfV.steps) +recNf' t'@(Rec _ _ _) n relU relV = + let nfU = escape relU in + let nfV = escape {ty = ty ~> ty} relV in + backStepsRel + (ntrlRel (Rec (invRec n) nfU.normal nfV.normal)) + (RecCong2' nfU.steps ++ RecCong3' nfV.steps) + +recNf : + {ctx : SnocList Ty} -> + {ty : Ty} -> + {0 t : Term ctx N} -> + {u : Term ctx ty} -> + {v : Term ctx (ty ~> ty)} -> + 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) + (RecCong1' nf.steps) + +helper : ValidHelper (\t => NormalForm t) +helper = MkValidHelper + { var = \i => ntrlRel Var + , abs = \rel => let nf = escape rel in MkNf (Abs nf.term) (AbsCong' nf.steps) (Abs nf.normal) + , zero = MkNf Zero [<] Zero + , suc = \nf => MkNf (Suc nf.term) (SucCong' nf.steps) (Suc nf.normal) + , rec = recNf + , step = \nf, step => backStepsNf nf [ MkNf (wkn nf.term thin) (wknSteps nf.steps) (wknNf nf.normal) + } + +export +normalize : {ctx : SnocList Ty} -> {ty : Ty} -> (t : Term ctx ty) -> NormalForm t +normalize = allRel helper diff --git a/src/Total/Reduction.idr b/src/Total/Reduction.idr index 4870f30..cb13706 100644 --- a/src/Total/Reduction.idr +++ b/src/Total/Reduction.idr @@ -95,3 +95,8 @@ 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 new file mode 100644 index 0000000..6a61cf5 --- /dev/null +++ b/src/Total/Syntax.idr @@ -0,0 +1,83 @@ +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 + +infixr 20 ~>* +infix 9 .* + +public export +(~>*) : SnocList Ty -> Ty -> Ty +tys ~>* ty = foldr (~>) ty tys + +public export +data Len : SnocList Ty -> Type where + Z : Len [<] + S : Len tys -> Len (tys :< ty) + +%name Len k, m, n + +public export +0 Fun : Len tys -> (Ty -> Type) -> Type -> Type +Fun Z arg ret = ret +Fun (S {ty} k) arg ret = Fun k arg (arg ty -> ret) + +after : (k : Len tys) -> (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 tys) -> + (forall ty. p ty -> q ty) -> + 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 : Nat -> Term ctx N +Lit 0 = Zero +Lit (S n) = Suc (Lit n) + +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)) $ + before k SnocList.Elem.There x + +export +Abs' : + (k : Len tys) -> + Fun k (Term (ctx ++ tys)) (Term (ctx ++ tys) ty) -> + Term ctx (tys ~>* ty) +Abs' k = AbsHelper k . before k Var + +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 + +export +(.) : {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)) + +export +(.*) : + {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 + +export +lift : {ctx : SnocList Ty} -> Term [<] ty -> Term ctx ty +lift t = wkn t (empty ctx) diff --git a/src/Total/Term.idr b/src/Total/Term.idr index 1530981..d4da92a 100644 --- a/src/Total/Term.idr +++ b/src/Total/Term.idr @@ -321,6 +321,15 @@ baseComp thin (sub :< t) = cong2 (:<) (baseComp thin sub) (substBase t thin) -- Substitution +export +substId : (t : Term ctx ty) -> subst t (Base Id) = t +substId (Var i) = Refl +substId (Abs t) = 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) -> -- cgit v1.2.3