diff options
Diffstat (limited to 'src/Inky/Thinning.idr')
| -rw-r--r-- | src/Inky/Thinning.idr | 310 |
1 files changed, 0 insertions, 310 deletions
diff --git a/src/Inky/Thinning.idr b/src/Inky/Thinning.idr deleted file mode 100644 index 1627307..0000000 --- a/src/Inky/Thinning.idr +++ /dev/null @@ -1,310 +0,0 @@ -module Inky.Thinning - -import public Inky.Context - -import Control.Function -import Control.WellFounded -import Data.DPair -import Data.Nat - --------------------------------------------------------------------------------- --- Thinnings ------------------------------------------------------------------- --------------------------------------------------------------------------------- - -public export -data Thins : Context a -> Context a -> Type where - Id : ctx `Thins` ctx - Drop : ctx1 `Thins` ctx2 -> ctx1 `Thins` ctx2 :< x - Keep : ctx1 `Thins` ctx2 -> ctx1 :< (x :- v) `Thins` ctx2 :< (y :- v) - -%name Thins f, g, h - --- Basics - -public export -indexPos : (f : ctx1 `Thins` ctx2) -> (pos : VarPos ctx1 x v) -> Var ctx2 v -indexPos Id pos = toVar pos -indexPos (Drop f) pos = ThereVar (indexPos f pos) -indexPos (Keep f) Here = toVar Here -indexPos (Keep f) (There pos) = ThereVar (indexPos f pos) - -public export -index : ctx1 `Thins` ctx2 -> Var ctx1 v -> Var ctx2 v -index f i = indexPos f i.pos - -export -(.) : ctx2 `Thins` ctx3 -> ctx1 `Thins` ctx2 -> ctx1 `Thins` ctx3 -Id . g = g -Drop f . g = Drop (f . g) -Keep f . Id = Keep f -Keep f . Drop g = Drop (f . g) -Keep f . Keep g = Keep (f . g) - --- Basic properties - -indexPosInjective : - (f : ctx1 `Thins` ctx2) -> {i : VarPos ctx1 x v} -> {j : VarPos ctx1 y v} -> - (0 _ : toNat (indexPos f i).pos = toNat (indexPos f j).pos) -> i = j -indexPosInjective Id prf = toNatInjective prf -indexPosInjective (Drop f) prf = indexPosInjective f (injective prf) -indexPosInjective (Keep f) {i = Here} {j = Here} prf = Refl -indexPosInjective (Keep f) {i = There i} {j = There j} prf = - thereCong (indexPosInjective f $ injective prf) - -export -indexInjective : (f : ctx1 `Thins` ctx2) -> {i, j : Var ctx1 v} -> index f i = index f j -> i = j -indexInjective f {i = %% x, j = %% y} prf = toVarCong (indexPosInjective f $ toNatCong' prf) - -indexPosComp : - (f : ctx2 `Thins` ctx3) -> (g : ctx1 `Thins` ctx2) -> (pos : VarPos ctx1 x v) -> - indexPos (f . g) pos = index f (indexPos g pos) -indexPosComp Id g pos with (indexPos g pos) - _ | (%% _) = Refl -indexPosComp (Drop f) g pos = cong ThereVar (indexPosComp f g pos) -indexPosComp (Keep f) Id pos = Refl -indexPosComp (Keep f) (Drop g) pos = cong ThereVar (indexPosComp f g pos) -indexPosComp (Keep f) (Keep g) Here = Refl -indexPosComp (Keep f) (Keep g) (There pos) = cong ThereVar (indexPosComp f g pos) - -export -indexComp : - (f : ctx2 `Thins` ctx3) -> (g : ctx1 `Thins` ctx2) -> (i : Var ctx1 v) -> - index (f . g) i = index f (index g i) -indexComp f g i = indexPosComp f g i.pos - --- Congruence ------------------------------------------------------------------ - -export -infix 6 ~~~ - -public export -data (~~~) : ctx1 `Thins` ctx2 -> ctx1 `Thins` ctx2 -> Type where - IdId : Id ~~~ Id - IdKeep : Id ~~~ f -> Id ~~~ Keep f - KeepId : f ~~~ Id -> Keep f ~~~ Id - DropDrop : f ~~~ g -> Drop f ~~~ Drop g - KeepKeep : f ~~~ g -> Keep f ~~~ Keep g - -%name Thinning.(~~~) prf - -(.indexPos) : f ~~~ g -> (pos : VarPos ctx1 x v) -> indexPos f pos = indexPos g pos -(IdId).indexPos pos = Refl -(IdKeep prf).indexPos Here = Refl -(IdKeep prf).indexPos (There pos) = cong ThereVar $ prf.indexPos pos -(KeepId prf).indexPos Here = Refl -(KeepId prf).indexPos (There pos) = cong ThereVar $ prf.indexPos pos -(DropDrop prf).indexPos pos = cong ThereVar $ prf.indexPos pos -(KeepKeep prf).indexPos Here = Refl -(KeepKeep prf).indexPos (There pos) = cong ThereVar $ prf.indexPos pos - -export -(.index) : f ~~~ g -> (i : Var ctx1 v) -> index f i = index g i -prf.index i = prf.indexPos i.pos - --- Useful for Parsers ---------------------------------------------------------- - -public export -dropAll : Length ctx2 -> ctx1 `Thins` ctx1 ++ ctx2 -dropAll Z = Id -dropAll (S len) = Drop (dropAll len) - -public export -keepAll : Length ctx -> ctx1 `Thins` ctx2 -> ctx1 ++ ctx `Thins` ctx2 ++ ctx -keepAll Z f = f -keepAll (S {x = x :- _} len) f = Keep (keepAll len f) - -public export -append : - ctx1 `Thins` ctx3 -> ctx2 `Thins` ctx4 -> - {auto len : Length ctx4} -> - ctx1 ++ ctx2 `Thins` ctx3 ++ ctx4 -append f Id = keepAll len f -append f (Drop g) {len = S len} = Drop (append f g) -append f (Keep g) {len = S len} = Keep (append f g) - -public export -assoc : Length ctx3 -> ctx1 ++ (ctx2 ++ ctx3) `Thins` (ctx1 ++ ctx2) ++ ctx3 -assoc Z = Id -assoc (S {x = x :- _} len) = Keep (assoc len) - -public export -growLength : ctx1 `Thins` ctx2 -> Length ctx1 -> Length ctx2 -growLength Id len = len -growLength (Drop f) len = S (growLength f len) -growLength (Keep f) (S len) = S (growLength f len) - -public export -thinLength : ctx1 `Thins` ctx2 -> Length ctx2 -> Length ctx1 -thinLength Id len = len -thinLength (Drop f) (S len) = thinLength f len -thinLength (Keep f) (S len) = S (thinLength f len) - -public export -thinAll : ctx1 `Thins` ctx2 -> All p ctx2 -> All p ctx1 -thinAll Id env = env -thinAll (Drop f) (env :< (x :- px)) = thinAll f env -thinAll (Keep {x, y} f) (env :< (_ :- px)) = thinAll f env :< (x :- px) - -public export -splitL : - {0 ctx1, ctx2, ctx3 : Context a} -> - Length ctx3 -> - ctx1 `Thins` ctx2 ++ ctx3 -> - Exists (\ctxA => Exists (\ctxB => (ctx1 = ctxA ++ ctxB, ctxA `Thins` ctx2, ctxB `Thins` ctx3))) -splitL Z f = Evidence ctx1 (Evidence [<] (Refl, f, Id)) -splitL (S len) Id = Evidence ctx2 (Evidence ctx3 (Refl, Id, Id)) -splitL (S len) (Drop f) = - let Evidence ctxA (Evidence ctxB (Refl, g, h)) = splitL len f in - Evidence ctxA (Evidence ctxB (Refl, g, Drop h)) -splitL (S len) (Keep f) = - let Evidence ctxA (Evidence ctxB (Refl, g, h)) = splitL len f in - Evidence ctxA (Evidence (ctxB :< _) (Refl, g, Keep h)) - -public export -splitR : - {0 ctx1, ctx2, ctx3 : Context a} -> - Length ctx2 -> - ctx1 ++ ctx2 `Thins` ctx3 -> - Exists (\ctxA => Exists (\ctxB => (ctx3 = ctxA ++ ctxB, ctx1 `Thins` ctxA, ctx2 `Thins` ctxB))) -splitR Z f = Evidence ctx3 (Evidence [<] (Refl, f, Id)) -splitR (S len) Id = Evidence ctx1 (Evidence ctx2 (Refl, Id, Id)) -splitR (S len) (Drop f) = - let Evidence ctxA (Evidence ctxB (Refl, g, h)) = splitR (S len) f in - Evidence ctxA (Evidence (ctxB :< _) (Refl, g, Drop h)) -splitR (S len) (Keep f) = - let Evidence ctxA (Evidence ctxB (Refl, g, h)) = splitR len f in - Evidence ctxA (Evidence (ctxB :< _) (Refl, g, Keep h)) - --------------------------------------------------------------------------------- --- Environments ---------------------------------------------------------------- --------------------------------------------------------------------------------- - -public export -data Env : Context a -> Context a -> (a -> Type) -> Type where - Base : {0 ctx1, ctx2 : Context a} -> ctx1 `Thins` ctx2 -> Env ctx1 ctx2 p - (:<) : - {0 ctx1, ctx2 : Context a} -> - Env ctx1 ctx2 p -> (x : Assoc0 (p v)) -> - Env (ctx1 :< (x.name :- v)) ctx2 p - -%name Env env - -lookupPos : Env ctx1 ctx2 p -> VarPos ctx1 x v -> Either (Var ctx2 v) (p v) -lookupPos (Base f) pos = Left (indexPos f pos) -lookupPos (env :< (x :- pv)) Here = Right pv -lookupPos (env :< (x :- pv)) (There pos) = lookupPos env pos - -export -lookup : Env ctx1 ctx2 p -> Var ctx1 v -> Either (Var ctx2 v) (p v) -lookup env i = lookupPos env i.pos - --- Properties - -export -lookupHere : - (0 env : Env ctx1 ctx2 p) -> (0 x : String) -> (0 pv : p v) -> - lookup (env :< (x :- pv)) (toVar Here) = Right pv -lookupHere env x pv = Refl - -export -lookupFS : - (0 env : Env ctx1 ctx2 p) -> (0 x : String) -> (0 pv : p v) -> (0 i : Var ctx1 w) -> - lookup (env :< (x :- pv)) (ThereVar i) = lookup env i -lookupFS env x pv i = Refl - --------------------------------------------------------------------------------- --- Renaming Coalgebras --------------------------------------------------------- --------------------------------------------------------------------------------- - -public export -interface Rename (0 a : Type) (0 t : Context a -> a -> Type) where - var : {0 ctx : Context a} -> {0 v : a} -> Var ctx v -> t ctx v - rename : - {0 ctx1, ctx2 : Context a} -> ctx1 `Thins` ctx2 -> - {0 v : a} -> t ctx1 v -> t ctx2 v - 0 renameCong : - {0 ctx1, ctx2 : Context a} -> {0 f, g : ctx1 `Thins` ctx2} -> f ~~~ g -> - {0 v : a} -> (x : t ctx1 v) -> rename f x = rename g x - 0 renameId : {0 ctx : Context a} -> {0 v : a} -> (x : t ctx v) -> rename Id x = x - -export -lift : Rename a t => ctx2 `Thins` ctx3 -> Env ctx1 ctx2 (t ctx2) -> Env ctx1 ctx3 (t ctx3) -lift Id env = env -lift f (Base g) = Base (f . g) -lift f (env :< (x :- v)) = lift f env :< (x :- rename f v) - -lookupPosLift : - Rename a t => - (f : ctx2 `Thins` ctx3) -> (env : Env ctx1 ctx2 (t ctx2)) -> (pos : VarPos ctx1 x v) -> - lookupPos (lift f env) pos = bimap (index f) (rename f) (lookupPos env pos) -lookupPosLift Id env pos with (lookupPos env pos) - _ | Left (%% y) = Refl - _ | Right y = cong Right $ irrelevantEq $ sym $ renameId y -lookupPosLift (Drop f) (Base g) pos = cong Left $ indexPosComp (Drop f) g pos -lookupPosLift (Keep f) (Base g) pos = cong Left $ indexPosComp (Keep f) g pos -lookupPosLift (Drop f) (env :< (x :- v)) Here = Refl -lookupPosLift (Keep f) (env :< (x :- v)) Here = Refl -lookupPosLift (Drop f) (env :< (x :- v)) (There pos) = lookupPosLift (Drop f) env pos -lookupPosLift (Keep f) (env :< (x :- v)) (There pos) = lookupPosLift (Keep f) env pos - -export -lookupLift : - Rename a t => - (f : ctx2 `Thins` ctx3) -> (env : Env ctx1 ctx2 (t ctx2)) -> (i : Var ctx1 v) -> - lookup (lift f env) i = bimap (index f) (rename f) (lookup env i) -lookupLift f env i = lookupPosLift f env i.pos - --- Well Founded ---------------------------------------------------------------- - -export -Sized (Context a) where - size [<] = 0 - size (ctx :< x) = S (size ctx) - --- Environments ------------------------------------------------------ - -namespace DEnv - public export - data DEnv : (0 p : Context a -> a -> Type) -> Context a -> Type where - Lin : DEnv p [<] - (:<) : - DEnv p ctx -> (px : Assoc0 (p ctx x.value)) -> - {auto 0 prf : px.name = x.name} -> - DEnv p (ctx :< x) - - %name DEnv.DEnv env - - export - length : DEnv p ctx -> Length ctx - length [<] = Z - length (env :< px) = S (length env) - - public export - record Entry (p : Context a -> a -> Type) (ctx : Context a) (v : a) where - constructor MkEntry - {0 support : Context a} - 0 prf : support `Smaller` ctx - thins : support `Thins` ctx - value : p support v - - export - indexDEnvPos : VarPos ctx x v -> DEnv p ctx -> Entry p ctx v - indexDEnvPos Here (env :< px) = MkEntry reflexive (Drop Id) px.value - indexDEnvPos (There pos) (env :< px) = - let MkEntry prf thins value = indexDEnvPos pos env in - MkEntry (lteSuccRight prf) (Drop thins) value - - export - indexDEnv' : Var ctx v -> DEnv p ctx -> Entry p ctx v - indexDEnv' i env = indexDEnvPos i.pos env - - export - indexDEnv : Rename a p => Var ctx v -> DEnv p ctx -> p ctx v - indexDEnv i env = - let MkEntry _ f x = indexDEnv' i env in - rename f x - - export - mapProperty : ({0 ctx : Context a} -> {0 v : a} -> p ctx v -> q ctx v) -> DEnv p ctx -> DEnv q ctx - mapProperty f [<] = [<] - mapProperty f (env :< (x :- px)) = mapProperty f env :< (x :- f px) |