From 93aae7e34e7130d9541d3441079448f156d93477 Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Thu, 6 Apr 2023 16:57:25 +0100 Subject: Migrate Env to use Thinned. --- src/Core/Declarative.idr | 17 ++++++------ src/Core/Environment.idr | 68 +++++++++++++++++------------------------------- src/Core/Term.idr | 8 ++++++ 3 files changed, 40 insertions(+), 53 deletions(-) (limited to 'src') diff --git a/src/Core/Declarative.idr b/src/Core/Declarative.idr index ae7e3aa..2fff434 100644 --- a/src/Core/Declarative.idr +++ b/src/Core/Declarative.idr @@ -27,9 +27,9 @@ data EnvWf where EnvWf [<] (:<) : EnvWf env -> - TypeWf env (wkn a thin) -> + TypeWf env (expand t) -> --- - EnvWf (Add env thin a) + EnvWf (Add env t) data TypeWf where SetType : @@ -150,11 +150,10 @@ data TermConv where public export data ThinWf : sx `Thins` sy -> Env sy -> Env sx -> Type where IdWf : ThinWf (id sx) env env - DropWf : ThinWf thin env2 env1 -> ThinWf (drop thin n) (Add env2 thin' a) env1 + DropWf : ThinWf thin env2 env1 -> ThinWf (drop thin n) (Add env2 t) env1 KeepWf : ThinWf thin env2 env1 -> - {auto 0 prf : IsNotId thin} -> - ThinWf (keep thin n) (Add env2 (thin . thin') a) (Add env1 thin' a) + ThinWf (keep thin n) (Add env2 (shift t thin)) (Add env1 t) %name ThinWf thinWf @@ -166,7 +165,7 @@ typeConvRespEnvEq : TypeConv env1 a b -> EnvEq env1 env2 -> TypeConv env2 a b termWfRespEnvEq : TermWf env1 t a -> EnvEq env1 env2 -> TermWf env2 t a termConvRespEnvEq : TermConv env1 t u b -> EnvEq env1 env2 -> TermConv env2 t u b -envWfRespEnvEq [<] [<] = [<] +envWfRespEnvEq envWf Base = envWf envWfRespEnvEq (envWf :< wf) (prf :< eq) = envWfRespEnvEq envWf prf :< rewrite sym eq in typeWfRespEnvEq wf prf @@ -282,10 +281,10 @@ CompWf (KeepWf {thin = thin2, n} thinWf2) IdWf = CompWf (KeepWf {thin = thin2, n} thinWf2) (DropWf {thin = thin1} thinWf1) = rewrite compRightDrop thin2 thin1 n in DropWf (CompWf thinWf2 thinWf1) -CompWf (KeepWf {thin = thin2, n, prf = prf2} thinWf2) (KeepWf {thin = thin1, thin', prf = prf1} thinWf1) = +CompWf (KeepWf {thin = thin2, n} thinWf2) (KeepWf {thin = thin1, t} thinWf1) = rewrite compKeep thin2 thin1 n in - rewrite compAssoc thin2 thin1 thin' in - KeepWf {prf = compPresNotId prf2 prf1} (CompWf thinWf2 thinWf1) + rewrite shiftHomo t thin1 thin2 in + KeepWf (CompWf thinWf2 thinWf1) -- Weakening Preservation ------------------------------------------------------ diff --git a/src/Core/Environment.idr b/src/Core/Environment.idr index ff484f4..a0a10f4 100644 --- a/src/Core/Environment.idr +++ b/src/Core/Environment.idr @@ -14,7 +14,7 @@ import Syntax.PreorderReasoning public export data Env : Context -> Type where Lin : Env [<] - Add : Env sx -> sy `Thins` sx -> Term sy -> Env (sx :< n) + Add : Env sx -> Thinned sx -> Env (sx :< n) %name Env env @@ -22,66 +22,46 @@ data Env : Context -> Type where public export (:<) : Env sx -> Term sx -> Env (sx :< n) -env :< t = Add env (id _) t +env :< t = Add env (t `Over` id sx) --- Operations ------------------------------------------------------------------ +-- Equality -------------------------------------------------------------------- -record IndexResult (sx : Context) where - constructor MkRes - {0 sy : Context} - val : Term sy - thin : sy `Thins` sx +namespace Eq + public export + data EnvEq : Env sx -> Env sx -> Type where + Base : EnvEq env env + (:<) : EnvEq env1 env2 -> expand t = expand u -> EnvEq (Add env1 t) (Add env2 u) -shift : IndexResult sx -> IndexResult (sx :< n) -shift (MkRes val thin) = MkRes val (drop thin n) + %name EnvEq prf -expand : IndexResult sx -> Term sx -expand (MkRes val thin) = wkn val thin +-- Indexing -------------------------------------------------------------------- -doIndex : Env sx -> {0 i : Var sx} -> View i -> IndexResult sx -doIndex (Add env thin t) Here = shift $ MkRes t thin -doIndex (Add env thin t) (There i) = shift $ doIndex env $ view i +doIndex : Env sx -> {0 i : Var sx} -> View i -> Thinned sx +doIndex (Add env t) Here = shift t (wkn1 _ _) +doIndex (Add env t) (There i) = shift (doIndex env $ view i) (wkn1 _ _) export index : Env sx -> Var sx -> Term sx index env i = expand $ doIndex env $ view i --- Equality -------------------------------------------------------------------- - -namespace Eq - public export - data EnvEq : Env sx -> Env sx -> Type where - Lin : EnvEq [<] [<] - (:<) : - EnvEq env1 env2 -> - Term.wkn t thin1 = wkn u thin2 -> - EnvEq (Add env1 thin1 t) (Add env2 thin2 u) - - %name EnvEq prf - -expandShift : (val : IndexResult sx) -> expand (shift val) = wkn (expand val) (drop (id sx) n) -expandShift (MkRes val thin) = sym $ Calc $ - |~ wkn (wkn val thin) (drop (id sx) n) - ~~ wkn val (drop (id sx) n . thin) ...(wknHomo val thin $ drop (id sx) n) - ~~ wkn val (drop (id sx . thin) n) ...(cong (wkn val) $ compLeftDrop (id sx) thin n) - ~~ wkn val (drop thin n) ...(cong (\thin => wkn val (drop thin n)) $ compLeftIdentity thin) +-- Respects Equality doIndexEqIsEq : - -- {env1, env2 : _} -> EnvEq env1 env2 -> {0 i : Var sx} -> (view : View i) -> expand (doIndex env1 view) = expand (doIndex env2 view) -doIndexEqIsEq {sx = sx :< n} ((:<) {t, u, thin1, thin2} prf eq) Here = Calc $ - |~ wkn t (drop thin1 n) - ~~ wkn (wkn t thin1) (drop (id sx) n) ...(expandShift (MkRes t thin1)) - ~~ wkn (wkn u thin2) (drop (id sx) n) ...(cong (\t => wkn t (drop (id sx) n)) $ eq) - ~~ wkn u (drop thin2 n) ...(sym $ expandShift (MkRes u thin2)) +doIndexEqIsEq Base view = Refl +doIndexEqIsEq {sx = sx :< n} ((:<) {t, u} prf eq) Here = Calc $ + |~ expand (shift t $ wkn1 sx n) + ~~ wkn (expand t) (wkn1 sx n) ...(expandShift t (wkn1 sx n)) + ~~ wkn (expand u) (wkn1 sx n) ...(cong (\t => wkn t (wkn1 sx n)) $ eq) + ~~ expand (shift u $ wkn1 sx n) ...(sym $ expandShift u (wkn1 sx n)) doIndexEqIsEq {sx = sx :< n} ((:<) {env1, env2} prf eq) (There i) = Calc $ - |~ expand (shift $ doIndex env1 $ view i) - ~~ wkn (expand $ doIndex env1 $ view i) (drop (id sx) n) ...(expandShift $ doIndex env1 $ view i) - ~~ wkn (expand $ doIndex env2 $ view i) (drop (id sx) n) ...(cong (\t => wkn t (drop (id sx) n)) $ doIndexEqIsEq prf (view i)) - ~~ expand (shift $ doIndex env2 $ view i) ...(sym $ expandShift $ doIndex env2 $ view i) + |~ expand (shift (doIndex env1 $ view i) (wkn1 sx n)) + ~~ wkn (expand (doIndex env1 $ view i)) (wkn1 sx n) ...(expandShift (doIndex env1 $ view i) (wkn1 sx n)) + ~~ wkn (expand (doIndex env2 $ view i)) (wkn1 sx n) ...(cong (\t => wkn t (wkn1 sx n)) $ doIndexEqIsEq prf (view i)) + ~~ expand (shift (doIndex env2 $ view i) (wkn1 sx n)) ...(sym $ expandShift (doIndex env2 $ view i) (wkn1 sx n)) export indexEqIsEq : EnvEq env1 env2 -> (i : Var sx) -> index env1 i = index env2 i diff --git a/src/Core/Term.idr b/src/Core/Term.idr index e52545d..182e1ea 100644 --- a/src/Core/Term.idr +++ b/src/Core/Term.idr @@ -81,3 +81,11 @@ expandShift : (thin : sx `Thins` sy) -> expand (shift t thin) = wkn (expand t) thin expandShift (term `Over` thin') thin = sym $ wknHomo term thin' thin + +export +shiftHomo : + (t : Thinned sx) -> + (thin1 : sx `Thins` sy) -> + (thin2 : sy `Thins` sz) -> + shift (shift t thin1) thin2 = shift t (thin2 . thin1) +shiftHomo (term `Over` thin) thin1 thin2 = cong (term `Over`) $ compAssoc thin2 thin1 thin -- cgit v1.2.3