From 3a23bd851fc1a5d6e161dabc8a13f06bc8544a1d Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Mon, 9 Sep 2024 11:33:45 +0100 Subject: Restart. - use De Bruijn, as Namely, Painless had more pain than promised; - remove higher-kinded types; - provide ill-typing predicates; - prove substitution respects ill-typing; --- src/Inky/Binding.idr | 371 ------------------ src/Inky/Env.idr | 30 -- src/Inky/Erased.idr | 6 - src/Inky/Kind.idr | 50 --- src/Inky/Kit.idr | 78 ---- src/Inky/OnlyWhen.idr | 44 --- src/Inky/Thinning.idr | 173 +++++++++ src/Inky/Type.idr | 1016 ++++++++++++++++++++++++++++++++++++++++++------- 8 files changed, 1057 insertions(+), 711 deletions(-) delete mode 100644 src/Inky/Binding.idr delete mode 100644 src/Inky/Env.idr delete mode 100644 src/Inky/Erased.idr delete mode 100644 src/Inky/Kind.idr delete mode 100644 src/Inky/Kit.idr delete mode 100644 src/Inky/OnlyWhen.idr create mode 100644 src/Inky/Thinning.idr (limited to 'src/Inky') diff --git a/src/Inky/Binding.idr b/src/Inky/Binding.idr deleted file mode 100644 index 56f079e..0000000 --- a/src/Inky/Binding.idr +++ /dev/null @@ -1,371 +0,0 @@ -module Inky.Binding - -import Control.Relation -import Control.Order -import Data.Bool -import Data.DPair -import Data.List -import Data.Nat -import Data.Nat.Order.Properties -import Data.So -import Decidable.Equality - --- Types ----------------------------------------------------------------------- - -export -record World where - constructor MkWorld - world : List Bool - -export -record Binder where - constructor MkBinder - binder : Nat - -Member : Nat -> List Bool -> Type -k `Member` [] = Void -Z `Member` b :: bs = So b -S n `Member` b :: bs = n `Member` bs - -snoc : List Bool -> Nat -> List Bool -snoc [] Z = True :: [] -snoc [] (S n) = False :: snoc [] n -snoc (_ :: bs) Z = True :: bs -snoc (b :: bs) (S n) = b :: snoc bs n - -export -(:<) : World -> Binder -> World -w :< x = MkWorld (snoc w.world x.binder) - -snocSem : - (bs : List Bool) -> (k : Nat) -> (n : Nat) -> - n `Member` snoc bs k <=> Either (n = k) (n `Member` bs) -snocSem [] Z Z = MkEquivalence (const $ Left Refl) (const Oh) -snocSem [] Z (S n) = MkEquivalence absurd absurd -snocSem [] (S k) 0 = MkEquivalence absurd absurd -snocSem [] (S k) (S n) = - let equiv = snocSem [] k n in - MkEquivalence - (mapFst (\prf => cong S prf) . equiv.leftToRight) - (equiv.rightToLeft . mapFst injective) -snocSem (b :: bs) Z Z = - MkEquivalence (const $ Left Refl) (const Oh) -snocSem (b :: bs) Z (S n) = MkEquivalence Right (\case (Right x) => x) -snocSem (b :: bs) (S k) Z = MkEquivalence Right (\case (Right x) => x) -snocSem (b :: bs) (S k) (S n) = - let equiv = snocSem bs k n in - MkEquivalence - (mapFst (\prf => cong S prf) . equiv.leftToRight) - (equiv.rightToLeft . mapFst injective) - -export -Name : World -> Type -Name w = Subset Nat (`Member` w.world) - --- Countable binders ----------------------------------------------------------- - -export -BZ : Binder -BZ = MkBinder Z - -export -BS : Binder -> Binder -BS = MkBinder . S . binder - --- Binders to names ------------------------------------------------------------ - -export -nameOf : forall w. (b : Binder) -> Name (w :< b) -nameOf b = Element b.binder ((snocSem w.world b.binder b.binder).rightToLeft (Left Refl)) - -export -binder : Name w -> Binder -binder = MkBinder . fst - -export -binderNameOf : (b : Binder) -> binder {w = w :< b} (nameOf {w} b) = b -binderNameOf (MkBinder k) = Refl - --- [<] world ----------------------------------------------------------------- - -export -Lin : World -Lin = MkWorld [] - -export -Uninhabited (Name [<]) where - uninhabited n = void n.snd - --- Names are comparable and stripable ------------------------------------------ - -export -Eq (Name w) where - n == k = n == k - -soEq : (n : Nat) -> So (n == n) -soEq Z = Oh -soEq (S k) = soEq k - -export -strip : {b : Binder} -> Name (w :< b) -> Maybe (Name w) -strip (Element n member) = - case decSo (b.binder == n) of - Yes _ => Nothing - No neq => - Just - (Element n - (either - (\eq => void $ neq $ rewrite eq in soEq b.binder) - id $ - (snocSem w.world b.binder n).leftToRight member)) - -public export -maybe' : - (0 p : Maybe a -> Type) -> - Lazy (p Nothing) -> - Lazy ((x : a) -> p (Just x)) -> - (x : Maybe a) -> p x -maybe' p x f Nothing = x -maybe' p x f (Just y) = f y - -public export -stripWith' : - (0 a : Maybe (Name w) -> Type) -> {b : Binder} -> - Lazy (a Nothing) -> Lazy ((n : Name w) -> a (Just n)) -> - (n : Name (w :< b)) -> a (strip {w, b} n) -stripWith' a x f n = maybe' a x f (strip n) - -public export -stripWith : - {b : Binder} -> Lazy a -> Lazy (Name w -> a) -> Name (w :< b) -> a -stripWith x f = maybe x f . strip - --- Freshness ------------------------------------------------------------------- - -export -record FreshIn (b : Binder) (w : World) where - constructor MkFresh - fresh : So (b.binder `gte` length w.world) - -export -freshInEmpty : b `FreshIn` [<] -freshInEmpty = MkFresh Oh - -snocLength : - (bs : List Bool) -> (k : Nat) -> - So (k `gte` length bs) -> So (S k `gte` length (snoc bs k)) -snocLength [] 0 prf = Oh -snocLength [] (S k) prf = snocLength [] k prf -snocLength (b :: bs) (S k) prf = snocLength bs k prf - -%inline -soRecomputable : (0 s : So b) -> So b -soRecomputable Oh = Oh - -export -sucFresh : b `FreshIn` w -> BS b `FreshIn` w :< b -sucFresh prf = MkFresh (soRecomputable (snocLength w.world b.binder prf.fresh)) - --- World inclusion ------------------------------------------------------------- - -export -record (<=) (w, v : World) where - constructor MkLte - lte : (n : Nat) -> n `Member` w.world -> n `Member` v.world - -export -coerce : (0 prf : w <= v) -> Name w -> Name v -coerce lte n = Element n.fst (lte.lte _ n.snd) - -export -Reflexive World (<=) where - reflexive = MkLte (\_, prf => prf) - -export -Transitive World (<=) where - transitive f g = MkLte (\n => g.lte n . f.lte n) - -export -Preorder World (<=) where - -export -emptyMin : [<] <= w -emptyMin = MkLte (\_ => absurd) - -export -snocMono : {w, v : World} -> (b : Binder) -> w <= v -> w :< b <= v :< b -snocMono b lte = MkLte - (\n => - (snocSem v.world b.binder _).rightToLeft - . mapSnd (lte.lte n) - . (snocSem w.world b.binder _).leftToRight - ) - -export -freshLte : {b : Binder} -> {w : World} -> (0 fresh : b `FreshIn` w) -> w <= w :< b -freshLte _ = MkLte (\n => (snocSem w.world b.binder n).rightToLeft . Right) - --- DeBruijn Worlds ------------------------------------------------------------- - -export -WS : World -> World -WS = MkWorld . (False ::) . world - -public export -shift : World -> World -shift w = WS w :< BZ - -invertSuc : (n : Nat) -> n `Member` (False :: bs) -> (k ** (S k = n, k `Member` bs)) -invertSuc (S n) prf = (n ** (Refl, prf)) - -export -sucMono : w <= v -> WS w <= WS v -sucMono lte = MkLte (\case - Z => absurd - (S n) => lte.lte n) - -public export -shiftMono : {w, v : World} -> w <= v -> shift w <= shift v -shiftMono lte = snocMono BZ (sucMono lte) - -export -sucLteShift : WS w <= shift w -sucLteShift = MkLte (\case - Z => absurd - S n => id) - -export -sucInjective : WS w <= WS v -> w <= v -sucInjective lte = MkLte (\n => lte.lte (S n)) - -export -shiftInjective : shift w <= shift v -> w <= v -shiftInjective lte = MkLte (\n => lte.lte (S n)) - -export -sucLteShiftInjective : WS w <= shift v -> w <= v -sucLteShiftInjective lte = MkLte (\n => lte.lte (S n)) - -export -sucEmpty : WS [<] <= [<] -sucEmpty = - MkLte (\case - Z => absurd - (S n) => absurd) - --- Suc and snoc ---------------------------------------------------------------- - -export -sucDistributesOverSnocLte : WS (w :< b) <= WS w :< BS b -sucDistributesOverSnocLte = - MkLte (\case - Z => absurd - (S n) => id) - -export -sucDistributesOverSnocGte : WS w :< BS b <= WS (w :< b) -sucDistributesOverSnocGte = - MkLte (\case - Z => absurd - (S n) => id) - --- Strip and coerce ------------------------------------------------------------ - -memberUniq : (n : Nat) -> (bs : List Bool) -> (p, q : Member n bs) -> p = q -memberUniq n [] p q = absurd p -memberUniq Z (True :: bs) Oh Oh = Refl -memberUniq Z (False :: bs) p q = absurd p -memberUniq (S n) (_ :: bs) p q = memberUniq n bs p q - -export -stripCoerceSnoc : - (b : Binder) -> (0 lte : w <= v) -> (n : Name (w :< b)) -> - strip {w = v, b} (coerce (snocMono b lte) n) = map (coerce lte) (strip {w, b} n) -stripCoerceSnoc b lte (Element n member) with (decSo $ equalNat b.binder n) - _ | Yes _ = Refl - _ | No _ = cong (\prf => Just $ Element n prf) (memberUniq n v.world {}) - --- De Bruijn Utilities --------------------------------------------------------- - -public export -(+) : World -> Nat -> World -w + Z = w -w + S n = WS (w + n) - -public export -lift : World -> Nat -> World -w `lift` Z = w -w `lift` S n = shift (w `lift` n) - -public export -plusMono : (k : Nat) -> w <= v -> w + k <= v + k -plusMono Z lte = lte -plusMono (S k) lte = sucMono (plusMono k lte) - -public export -plusInjective : (k : Nat) -> w + k <= v + k -> w <= v -plusInjective Z lte = lte -plusInjective (S k) lte = plusInjective k (sucInjective lte) - -public export -liftMono : {w, v : World} -> (k : Nat) -> w <= v -> (w `lift` k) <= (v `lift` k) -liftMono Z lte = lte -liftMono (S k) lte = shiftMono (liftMono k lte) - -public export -liftInjective : (k : Nat) -> (w `lift` k) <= (v `lift` k) -> w <= v -liftInjective Z lte = lte -liftInjective (S k) lte = liftInjective k (shiftInjective lte) - -plusWorld : (0 w : World) -> (k : Nat) -> (w + k).world = replicate k False ++ w.world -plusWorld w Z = Refl -plusWorld w (S k) = cong (False ::) (plusWorld w k) - -liftWorld : (0 w : World) -> (k : Nat) -> (w `lift` k).world = replicate k True ++ w.world -liftWorld w Z = Refl -liftWorld w (S k) = cong (True ::) (liftWorld w k) - -plusMember : (k : Nat) -> Member n bs -> Member (k + n) (replicate k False ++ bs) -plusMember Z prf = prf -plusMember (S k) prf = plusMember k prf - -export -plus : (k : Nat) -> Name w -> Name (w + k) -plus k (Element n prf) = rewrite plusWorld w k in Element (k + n) (plusMember k prf) - -minusMember : {n : Nat} -> (k : Nat) -> Member n (replicate k False ++ bs) -> Member (n `minus` k) bs -minusMember Z prf = rewrite minusZeroRight n in prf -minusMember {n = S n} (S k) prf = minusMember k prf - -export -minus : (k : Nat) -> Name (w + k) -> Name w -minus k (Element n prf) = - Element (n `minus` k) - (minusMember {bs = w.world} k (rewrite sym $ plusWorld w k in prf)) - -cmpLt : {n : Nat} -> n `LT` k -> Member n (replicate k True ++ bs) -> Member n (replicate k True ++ []) -cmpLt {n = Z} (LTESucc prf) member = member -cmpLt {n = S n} (LTESucc prf) member = cmpLt prf member - -cmpGte : n `GTE` k -> Member n (replicate k True ++ bs) -> Member n (replicate k False ++ bs) -cmpGte LTEZero member = member -cmpGte (LTESucc prf) member = cmpGte prf member - -export -cmp : (k : Nat) -> Name (w `lift` k) -> Either (Name ([<] `lift` k)) (Name (w + k)) -cmp k (Element n member) = - case decSo $ n `lt` k of - Yes prf => - Left $ - Element n $ - rewrite liftWorld [<] k in - cmpLt {bs = w.world} (ltIsLT n k $ soToEq prf) $ - rewrite sym $ liftWorld w k in - member - No prf => - Right $ - Element n $ - rewrite plusWorld w k in - cmpGte {bs = w.world} (notltIsGTE n k $ notTrueIsFalse $ prf . eqToSo) $ - rewrite sym $ liftWorld w k in - member diff --git a/src/Inky/Env.idr b/src/Inky/Env.idr deleted file mode 100644 index 174b681..0000000 --- a/src/Inky/Env.idr +++ /dev/null @@ -1,30 +0,0 @@ -module Inky.Env - -import Control.Relation -import Inky.Binding - -infix 2 :~ - -public export -record Assoc (0 a : Type) where - constructor (:~) - binder : Binder - value : a - -public export -data PartialEnv : Type -> World -> World -> Type where - Lin : PartialEnv a w w - (:<) : PartialEnv a w v -> (x : Assoc a) -> PartialEnv a (w :< x.binder) v - -public export -Env : Type -> World -> Type -Env a w = PartialEnv a w [<] - -public export -partialLookup : PartialEnv a w v -> Name w -> Either (Name v) a -partialLookup [<] = Left -partialLookup (env :< (x :~ v)) = stripWith (Right v) (partialLookup env) - -public export -lookup : Env a w -> Name w -> a -lookup = either absurd id .: partialLookup diff --git a/src/Inky/Erased.idr b/src/Inky/Erased.idr deleted file mode 100644 index 05bb29e..0000000 --- a/src/Inky/Erased.idr +++ /dev/null @@ -1,6 +0,0 @@ -module Inky.Erased - -public export -record Erased (t : Type) where - constructor Forget - 0 val : t diff --git a/src/Inky/Kind.idr b/src/Inky/Kind.idr deleted file mode 100644 index a09c97d..0000000 --- a/src/Inky/Kind.idr +++ /dev/null @@ -1,50 +0,0 @@ -module Inky.Kind - -import Control.Function -import Data.Bool.Decidable -import Decidable.Equality.Core - -public export -data Kind : Type where - KStar : Kind - KArrow : Kind -> Kind -> Kind - -export -Eq Kind where - KStar == KStar = True - (t1 `KArrow` u1) == (t2 `KArrow` u2) = t1 == t2 && u1 == u2 - _ == _ = False - -export -Uninhabited (KStar = KArrow t u) where - uninhabited prf impossible - -export -Uninhabited (KArrow t u = KStar) where - uninhabited prf impossible - -export -Biinjective KArrow where - biinjective Refl = (Refl, Refl) - -export -DecEq Kind where - decEq KStar KStar = Yes Refl - decEq KStar (KArrow _ _) = No absurd - decEq (KArrow k1 k2) KStar = No absurd - decEq (KArrow k1 k2) (KArrow j1 j2) = - case (decEq k1 j1, decEq k2 j2) of - (Yes eq1, Yes eq2) => Yes (cong2 KArrow eq1 eq2) - (Yes eq1, No neq2) => No (neq2 . snd . biinjective) - (No neq1, _) => No (neq1 . fst . biinjective) - -export -decEqReflects : (k, j : Kind) -> (k = j) `Reflects` (k == j) -decEqReflects KStar KStar = RTrue Refl -decEqReflects KStar (KArrow _ _) = RFalse absurd -decEqReflects (KArrow k1 k2) KStar = RFalse absurd -decEqReflects (KArrow k1 k2) (KArrow j1 j2) with (decEqReflects k1 j1) | (k1 == j1) - _ | RTrue eq1 | _ with (decEqReflects k2 j2) | (k2 == j2) - _ | RTrue eq2 | _ = RTrue (cong2 KArrow eq1 eq2) - _ | RFalse neq2 | _ = RFalse (neq2 . snd . biinjective) - _ | RFalse neq1 | _ = RFalse (neq1 . fst . biinjective) diff --git a/src/Inky/Kit.idr b/src/Inky/Kit.idr deleted file mode 100644 index a601a3f..0000000 --- a/src/Inky/Kit.idr +++ /dev/null @@ -1,78 +0,0 @@ -module Inky.Kit - -import public Control.Monad.Identity -import Inky.Binding -import Inky.Erased - -public export -record TrKit (env : World -> World -> Type) (res : World -> Type) where - constructor MkTrKit - name : forall w, v. env w v -> Name w -> res v - binder : forall w, v. env w v -> Binder -> Binder - extend : forall w, v. (b : Binder) -> (e : env w v) -> env (w :< b) (v :< binder e b) - -export -map : (forall w. res1 w -> res2 w) -> TrKit env res1 -> TrKit env res2 -map f kit = MkTrKit - { name = f .: kit.name - , binder = kit.binder - , extend = kit.extend - } - -export -pure : Applicative m => TrKit env res -> TrKit env (m . res) -pure = map pure - -export -Coerce : TrKit (Erased .: (<=)) Name -Coerce = MkTrKit (\e => coerce e.val) (const id) (\b, e => Forget (snocMono b e.val)) - -public export -record Supply (w : World) where - constructor MkSupply - seed : Binder - fresh : seed `FreshIn` w - -public export -record SubstEnv (res : World -> Type) (w, v : World) where - constructor MkEnv - name : Name w -> res v - supply : Supply v - -export -substKitE : - Monad m => - (var : forall w. Name w -> m (res w)) -> - (coerce : forall w, v. (0 _ : w <= v) -> res w -> m (res v)) -> - TrKit (SubstEnv (m . res)) (m . res) -substKitE var coerce = MkTrKit - { name = \e, n => e.name n - , binder = \e, _ => e.supply.seed - , extend = \b, e => MkEnv - { name = - stripWith - (var (nameOf e.supply.seed)) - (\n => do - n <- e.name n - coerce (freshLte e.supply.fresh) n) - , supply = MkSupply - { seed = BS e.supply.seed - , fresh = sucFresh e.supply.fresh - } - } - } - -public export -interface Traverse (0 t : World -> Type) where - var : Name w -> t w - - traverseE : Applicative m => TrKit env (m . t) -> env w v -> t w -> m (t v) - - renameE : Applicative m => TrKit env (m . Name) -> env w v -> t w -> m (t v) - renameE kit = traverseE (Kit.map (Prelude.map var) kit) - - traverse : TrKit env t -> env w v -> t w -> t v - traverse kit e t = (traverseE (Kit.pure kit) e t).runIdentity - - rename : TrKit env Name -> env w v -> t w -> t v - rename kit e t = (renameE (Kit.pure kit) e t).runIdentity diff --git a/src/Inky/OnlyWhen.idr b/src/Inky/OnlyWhen.idr deleted file mode 100644 index 7bed91a..0000000 --- a/src/Inky/OnlyWhen.idr +++ /dev/null @@ -1,44 +0,0 @@ -module Inky.OnlyWhen - -import Data.DPair - -public export -data OnlyWhen : Maybe a -> (a -> Type) -> Type where - Yes : forall x. (px : p x) -> Just x `OnlyWhen` p - No : ((x : a) -> Not (p x)) -> Nothing `OnlyWhen` p - -public export -decDPair : (v ** v `OnlyWhen` p) <=> Dec (x : a ** p x) -decDPair = - MkEquivalence - { leftToRight = \case - (Just x ** Yes px) => Yes (x ** px) - (Nothing ** No prf) => No (\(x ** px) => prf x px) - , rightToLeft = \case - Yes (x ** px) => (Just x ** Yes px) - No prf => (Nothing ** No (\x, px => prf (x ** px))) - } - -public export -decExists : Exists (`OnlyWhen` p) <=> Dec (Exists p) -decExists = - MkEquivalence - { leftToRight = \case - Evidence .(Just x) (Yes px) => Yes (Evidence x px) - Evidence .(Nothing) (No prf) => No (\(Evidence x px) => void (prf x px)) - , rightToLeft = \case - Yes (Evidence x px) => Evidence (Just x) (Yes px) - No prf => Evidence Nothing (No (\x, px => prf (Evidence x px))) - } - -public export -decSubset : Subset (Maybe a) (`OnlyWhen` p) <=> Dec (Subset a p) -decSubset = - MkEquivalence - { leftToRight = \case - Element (Just x) prf => Yes (Element x (case prf of Yes px => px)) - Element Nothing prf => No (\(Element x px) => void (case prf of No prf => prf x px)) - , rightToLeft = \case - Yes (Element x px) => Element (Just x) (Yes px) - No prf => Element Nothing (No (\x, px => prf (Element x px))) - } diff --git a/src/Inky/Thinning.idr b/src/Inky/Thinning.idr new file mode 100644 index 0000000..c3235c0 --- /dev/null +++ b/src/Inky/Thinning.idr @@ -0,0 +1,173 @@ +module Inky.Thinning + +import public Data.Fin + +import Control.Function + +-------------------------------------------------------------------------------- +-- Thinnings ------------------------------------------------------------------- +-------------------------------------------------------------------------------- + +public export +data Thins : Nat -> Nat -> Type where + Id : n `Thins` n + Drop : k `Thins` n -> k `Thins` S n + Keep : k `Thins` n -> S k `Thins` S n + +%name Thins f, g, h + +-- Basics + +export +index : k `Thins` n -> Fin k -> Fin n +index Id x = x +index (Drop f) x = FS (index f x) +index (Keep f) FZ = FZ +index (Keep f) (FS x) = FS (index f x) + +export +(.) : k `Thins` n -> j `Thins` k -> j `Thins` n +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 + +export +indexInjective : (f : k `Thins` n) -> {x, y : Fin k} -> index f x = index f y -> x = y +indexInjective Id eq = eq +indexInjective (Drop f) eq = indexInjective f $ injective eq +indexInjective (Keep f) {x = FZ} {y = FZ} eq = Refl +indexInjective (Keep f) {x = FS x} {y = FS y} eq = cong FS $ indexInjective f $ injective eq + +export +(f : k `Thins` n) => Injective (index f) where + injective = indexInjective f + +export +indexId : (0 x : Fin n) -> index Id x = x +indexId x = Refl + +export +indexDrop : (0 f : k `Thins` n) -> (0 x : Fin k) -> index (Drop f) x = FS (index f x) +indexDrop f x = Refl + +export +indexKeepFZ : (0 f : k `Thins` n) -> index (Keep f) FZ = FZ +indexKeepFZ f = Refl + +export +indexKeepFS : (0 f : k `Thins` n) -> (0 x : Fin k) -> index (Keep f) (FS x) = FS (index f x) +indexKeepFS f x = Refl + +export +indexComp : + (f : k `Thins` n) -> (g : j `Thins` k) -> (x : Fin j) -> + index (f . g) x = index f (index g x) +indexComp Id g x = Refl +indexComp (Drop f) g x = cong FS (indexComp f g x) +indexComp (Keep f) Id x = Refl +indexComp (Keep f) (Drop g) x = cong FS (indexComp f g x) +indexComp (Keep f) (Keep g) FZ = Refl +indexComp (Keep f) (Keep g) (FS x) = cong FS (indexComp f g x) + +-- Congruence ------------------------------------------------------------------ + +export +infix 6 ~~~ + +public export +data (~~~) : k `Thins` n -> k `Thins` n -> 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 + +export +(.index) : f ~~~ g -> (x : Fin k) -> index f x = index g x +(IdId).index x = Refl +(IdKeep prf).index FZ = Refl +(IdKeep prf).index (FS x) = cong FS (prf.index x) +(KeepId prf).index FZ = Refl +(KeepId prf).index (FS x) = cong FS (prf.index x) +(DropDrop prf).index x = cong FS (prf.index x) +(KeepKeep prf).index FZ = Refl +(KeepKeep prf).index (FS x) = cong FS (prf.index x) + +export +pointwise : {f, g : k `Thins` n} -> (0 _ : (x : Fin k) -> index f x = index g x) -> f ~~~ g +pointwise {f = Id} {g = Id} prf = IdId +pointwise {f = Id} {g = Drop g} prf = void $ absurd $ prf FZ +pointwise {f = Id} {g = Keep g} prf = IdKeep (pointwise $ \x => injective $ prf $ FS x) +pointwise {f = Drop f} {g = Id} prf = void $ absurd $ prf FZ +pointwise {f = Drop f} {g = Drop g} prf = DropDrop (pointwise $ \x => injective $ prf x) +pointwise {f = Drop f} {g = Keep g} prf = void $ absurd $ prf FZ +pointwise {f = Keep f} {g = Id} prf = KeepId (pointwise $ \x => injective $ prf $ FS x) +pointwise {f = Keep f} {g = Drop g} prf = void $ absurd $ prf FZ +pointwise {f = Keep f} {g = Keep g} prf = KeepKeep (pointwise $ \x => injective $ prf $ FS x) + +-------------------------------------------------------------------------------- +-- Environments ---------------------------------------------------------------- +-------------------------------------------------------------------------------- + +public export +data Env : Nat -> Nat -> Type -> Type where + Base : k `Thins` n -> Env k n a + (:<) : Env k n a -> a -> Env (S k) n a + +%name Env env + +export +lookup : Env k n a -> Fin k -> Either (Fin n) a +lookup (Base f) x = Left (index f x) +lookup (env :< v) FZ = Right v +lookup (env :< v) (FS x) = lookup env x + +-- Properties + +export +lookupFZ : (0 env : Env k n a) -> (0 v : a) -> lookup (env :< v) FZ = Right v +lookupFZ env v = Refl + +export +lookupFS : + (0 env : Env k n a) -> (0 v : a) -> (0 x : Fin k) -> + lookup (env :< v) (FS x) = lookup env x +lookupFS env v x = Refl + +-------------------------------------------------------------------------------- +-- Renaming Coalgebras --------------------------------------------------------- +-------------------------------------------------------------------------------- + +public export +interface Rename (0 a : Nat -> Type) where + var : Fin n -> a n + rename : k `Thins` n -> a k -> a n + 0 renameCong : {0 f, g : k `Thins` n} -> f ~~~ g -> (x : a k) -> rename f x = rename g x + 0 renameId : (x : a n) -> rename Id x = x + +export +lift : Rename a => k `Thins` n -> Env j k (a k) -> Env j n (a n) +lift Id env = env +lift f (Base g) = Base (f . g) +lift f (env :< v) = lift f env :< rename f v + +export +lookupLift : + Rename a => + (f : k `Thins` n) -> (env : Env j k (a k)) -> (x : Fin j) -> + lookup (lift f env) x = bimap (index f) (rename f) (lookup env x) +lookupLift Id env x with (lookup env x) + _ | Left y = Refl + _ | Right y = cong Right $ irrelevantEq $ sym $ renameId y +lookupLift (Drop f) (Base g) x = cong Left $ indexComp (Drop f) g x +lookupLift (Drop f) (env :< y) FZ = Refl +lookupLift (Drop f) (env :< y) (FS x) = lookupLift (Drop f) env x +lookupLift (Keep f) (Base g) x = cong Left $ indexComp (Keep f) g x +lookupLift (Keep f) (env :< y) FZ = Refl +lookupLift (Keep f) (env :< y) (FS x) = lookupLift (Keep f) env x diff --git a/src/Inky/Type.idr b/src/Inky/Type.idr index 71f5409..cab2fd3 100644 --- a/src/Inky/Type.idr +++ b/src/Inky/Type.idr @@ -1,148 +1,900 @@ module Inky.Type +import public Data.List1 + +import Control.Function import Data.Bool.Decidable -import public Data.DPair -import public Data.List.Quantifiers -import Inky.Binding -import Inky.Env -import Inky.Kind -import Inky.OnlyWhen - -namespace Raw - public export - data RawSTy : World -> Type - - public export - data RawCTy : World -> Type - - data RawSTy where - TVar : (x : Name w) -> RawSTy w - TNat : RawSTy w - TArrow : RawCTy w -> RawCTy w -> RawSTy w - TSum : List (RawCTy w) -> RawSTy w - TProd : List (RawCTy w) -> RawSTy w - TApp : RawSTy w -> RawCTy w -> RawSTy w - TAnnot : RawCTy w -> Kind -> RawSTy w - - data RawCTy where - TFix : (x : Binder) -> RawCTy (w :< x) -> RawCTy w - TEmbed : RawSTy w -> RawCTy w +import Data.Either +import Data.These +import Data.These.Decidable +import Decidable.Equality +import Inky.Thinning + +-- Utilities ------------------------------------------------------------------- + +reflectEq : (i, j : Fin n) -> (i = j) `Reflects` (i == j) +reflectEq FZ FZ = RTrue Refl +reflectEq FZ (FS j) = RFalse absurd +reflectEq (FS i) FZ = RFalse absurd +reflectEq (FS i) (FS j) = + viaEquivalence (MkEquivalence (\prf => cong FS prf) injective) + (reflectEq i j) + +-- Definition ------------------------------------------------------------------ public export -data SynthKind : Env Kind w -> RawSTy w -> Kind -> Type where -public export -data CheckKind : Env Kind w -> Kind -> RawCTy w -> Type where +data Ty : Nat -> Type where + TVar : Fin n -> Ty n + TNat : Ty n + TArrow : List1 (Ty n) -> Ty n -> Ty n + TUnion : List1 (Ty n) -> Ty n + TProd : List (Ty n) -> Ty n + TSum : List (Ty n) -> Ty n + TFix : Ty (S n) -> Ty n -data SynthKind where - TVar : SynthKind env (TVar x) (lookup env x) - TNat : SynthKind env TNat KStar - TArrow : CheckKind env KStar t -> CheckKind env KStar u -> SynthKind env (t `TArrow` u) KStar - TSum : All (CheckKind env KStar) ts -> SynthKind env (TSum ts) KStar - TProd : All (CheckKind env KStar) ts -> SynthKind env (TProd ts) KStar - TApp : SynthKind env f (k `KArrow` j) -> CheckKind env k t -> SynthKind env (f `TApp` t) j - TAnnot : CheckKind env k t -> SynthKind env (TAnnot t k) k +%name Ty a, b, c -data CheckKind where - TFix : CheckKind (env :< (x :~ k)) k t -> CheckKind env k (TFix x t) - TEmbed : SynthKind env a j -> k = j -> CheckKind env k (TEmbed a) +-- Occurs ---------------------------------------------------------------------- -export -synthKindUniq : SynthKind env t k -> SynthKind env t j -> k = j -synthKindUniq TVar TVar = Refl -synthKindUniq TNat TNat = Refl -synthKindUniq (TArrow p1 p2) (TArrow p3 p4) = Refl -synthKindUniq (TSum ps1) (TSum ps2) = Refl -synthKindUniq (TProd ps1) (TProd ps2) = Refl -synthKindUniq (TApp p1 p2) (TApp p3 p4) = case (synthKindUniq p1 p3) of Refl => Refl -synthKindUniq (TAnnot p1) (TAnnot p2) = Refl +OccursIn : Fin n -> Ty n -> Type +OccursInAny : Fin n -> List (Ty n) -> Type +OccursInAny1 : Fin n -> List1 (Ty n) -> Type + +i `OccursIn` TVar j = i = j +i `OccursIn` TNat = Void +i `OccursIn` TArrow as b = These (i `OccursInAny1` as) (i `OccursIn` b) +i `OccursIn` TUnion as = i `OccursInAny1` as +i `OccursIn` TProd as = i `OccursInAny` as +i `OccursIn` TSum as = i `OccursInAny` as +i `OccursIn` TFix a = FS i `OccursIn` a + +i `OccursInAny` [] = Void +i `OccursInAny` a :: as = These (i `OccursIn` a) (i `OccursInAny` as) + +i `OccursInAny1` a ::: as = These (i `OccursIn` a) (i `OccursInAny` as) + +-- Decidable + +occursIn : (i : Fin n) -> (a : Ty n) -> Bool +occursInAny : (i : Fin n) -> (as : List (Ty n)) -> Bool +occursInAny1 : (i : Fin n) -> (as : List1 (Ty n)) -> Bool + +reflectOccursIn : + (i : Fin n) -> (a : Ty n) -> + (i `OccursIn` a) `Reflects` (i `occursIn` a) +reflectOccursInAny : + (i : Fin n) -> (as : List (Ty n)) -> + (i `OccursInAny` as) `Reflects` (i `occursInAny` as) +reflectOccursInAny1 : + (i : Fin n) -> (as : List1 (Ty n)) -> + (i `OccursInAny1` as) `Reflects` (i `occursInAny1` as) + +i `occursIn` (TVar j) = i == j +i `occursIn` TNat = False +i `occursIn` (TArrow as b) = (i `occursInAny1` as) || (i `occursIn` b) +i `occursIn` (TUnion as) = i `occursInAny1` as +i `occursIn` (TProd as) = i `occursInAny` as +i `occursIn` (TSum as) = i `occursInAny` as +i `occursIn` (TFix a) = FS i `occursIn` a + +i `occursInAny` [] = False +i `occursInAny` (a :: as) = (i `occursIn` a) || (i `occursInAny` as) + +i `occursInAny1` (a ::: as) = (i `occursIn` a) || (i `occursInAny` as) + +reflectOccursIn i (TVar j) = reflectEq i j +reflectOccursIn i TNat = RFalse id +reflectOccursIn i (TArrow as b) = reflectThese (reflectOccursInAny1 i as) (reflectOccursIn i b) +reflectOccursIn i (TUnion as) = reflectOccursInAny1 i as +reflectOccursIn i (TProd as) = reflectOccursInAny i as +reflectOccursIn i (TSum as) = reflectOccursInAny i as +reflectOccursIn i (TFix a) = reflectOccursIn (FS i) a + +reflectOccursInAny i [] = RFalse id +reflectOccursInAny i (a :: as) = reflectThese (reflectOccursIn i a) (reflectOccursInAny i as) + +reflectOccursInAny1 i (a ::: as) = reflectThese (reflectOccursIn i a) (reflectOccursInAny i as) + +-- Not Strictly Positive ----------------------------------------------------------- + +-- We use negation so we get a cause on failure. + +NotPositiveIn : Fin n -> Ty n -> Type +NotPositiveInAny : Fin n -> List (Ty n) -> Type +NotPositiveInAny1 : Fin n -> List1 (Ty n) -> Type + +i `NotPositiveIn` TVar j = Void +i `NotPositiveIn` TNat = Void +i `NotPositiveIn` TArrow as b = These (i `OccursInAny1` as) (i `NotPositiveIn` b) +i `NotPositiveIn` TUnion as = i `NotPositiveInAny1` as +i `NotPositiveIn` TProd as = i `NotPositiveInAny` as +i `NotPositiveIn` TSum as = i `NotPositiveInAny` as +i `NotPositiveIn` TFix a = FS i `OccursIn` a + -- Prevent mutual recursion; + -- Can add back in without breaking things + +i `NotPositiveInAny` [] = Void +i `NotPositiveInAny` a :: as = These (i `NotPositiveIn` a) (i `NotPositiveInAny` as) + +i `NotPositiveInAny1` a ::: as = These (i `NotPositiveIn` a) (i `NotPositiveInAny` as) + +-- Not Positive implies Occurs + +notPositiveToOccurs : (a : Ty k) -> i `NotPositiveIn` a -> i `OccursIn` a +notPositiveAnyToOccursAny : (as : List (Ty k)) -> i `NotPositiveInAny` as -> i `OccursInAny` as +notPositiveAny1ToOccursAny1 : (as : List1 (Ty k)) -> i `NotPositiveInAny1` as -> i `OccursInAny1` as + +notPositiveToOccurs (TVar j) = absurd +notPositiveToOccurs TNat = id +notPositiveToOccurs (TArrow as b) = mapSnd (notPositiveToOccurs b) +notPositiveToOccurs (TUnion as) = notPositiveAny1ToOccursAny1 as +notPositiveToOccurs (TProd as) = notPositiveAnyToOccursAny as +notPositiveToOccurs (TSum as) = notPositiveAnyToOccursAny as +notPositiveToOccurs (TFix a) = id + +notPositiveAnyToOccursAny [] = id +notPositiveAnyToOccursAny (a :: as) = bimap (notPositiveToOccurs a) (notPositiveAnyToOccursAny as) + +notPositiveAny1ToOccursAny1 (a ::: as) = bimap (notPositiveToOccurs a) (notPositiveAnyToOccursAny as) + +-- Decidable + +notEnvPositiveIn : (i : Fin n) -> (a : Ty n) -> Bool +notEnvPositiveInAny : (i : Fin n) -> (as : List (Ty n)) -> Bool +notEnvPositiveInAny1 : (i : Fin n) -> (as : List1 (Ty n)) -> Bool + +i `notEnvPositiveIn` (TVar j) = False +i `notEnvPositiveIn` TNat = False +i `notEnvPositiveIn` (TArrow as b) = (i `occursInAny1` as) || (i `notEnvPositiveIn` b) +i `notEnvPositiveIn` (TUnion as) = i `notEnvPositiveInAny1` as +i `notEnvPositiveIn` (TProd as) = i `notEnvPositiveInAny` as +i `notEnvPositiveIn` (TSum as) = i `notEnvPositiveInAny` as +i `notEnvPositiveIn` (TFix a) = FS i `occursIn` a + +i `notEnvPositiveInAny` [] = False +i `notEnvPositiveInAny` (a :: as) = (i `notEnvPositiveIn` a) || (i `notEnvPositiveInAny` as) + +i `notEnvPositiveInAny1` (a ::: as) = (i `notEnvPositiveIn` a) || (i `notEnvPositiveInAny` as) + +reflectNotPositiveIn : + (i : Fin n) -> (a : Ty n) -> + (i `NotPositiveIn` a) `Reflects` (i `notEnvPositiveIn` a) +reflectNotPositiveInAny : + (i : Fin n) -> (as : List (Ty n)) -> + (i `NotPositiveInAny` as) `Reflects` (i `notEnvPositiveInAny` as) +reflectNotPositiveInAny1 : + (i : Fin n) -> (as : List1 (Ty n)) -> + (i `NotPositiveInAny1` as) `Reflects` (i `notEnvPositiveInAny1` as) + +reflectNotPositiveIn i (TVar j) = RFalse id +reflectNotPositiveIn i TNat = RFalse id +reflectNotPositiveIn i (TArrow as b) = + reflectThese (reflectOccursInAny1 i as) (reflectNotPositiveIn i b) +reflectNotPositiveIn i (TUnion as) = reflectNotPositiveInAny1 i as +reflectNotPositiveIn i (TProd as) = reflectNotPositiveInAny i as +reflectNotPositiveIn i (TSum as) = reflectNotPositiveInAny i as +reflectNotPositiveIn i (TFix a) = reflectOccursIn (FS i) a + +reflectNotPositiveInAny i [] = RFalse id +reflectNotPositiveInAny i (a :: as) = + reflectThese (reflectNotPositiveIn i a) (reflectNotPositiveInAny i as) + +reflectNotPositiveInAny1 i (a ::: as) = + reflectThese (reflectNotPositiveIn i a) (reflectNotPositiveInAny i as) + +-- Well Formed ----------------------------------------------------------------- + +-- Negating reflectidable properties is fun. export -synthKind : (env : Env Kind w) -> (a : RawSTy w) -> Maybe Kind +IllFormed : Ty n -> Type +AnyIllFormed : List (Ty n) -> Type +Any1IllFormed : List1 (Ty n) -> Type + +IllFormed (TVar v) = Void +IllFormed TNat = Void +IllFormed (TArrow as b) = These (Any1IllFormed as) (IllFormed b) +IllFormed (TUnion as) = Any1IllFormed as +IllFormed (TProd as) = AnyIllFormed as +IllFormed (TSum as) = AnyIllFormed as +IllFormed (TFix a) = These (FZ `NotPositiveIn` a) (IllFormed a) + +AnyIllFormed [] = Void +AnyIllFormed (a :: as) = These (IllFormed a) (AnyIllFormed as) + +Any1IllFormed (a ::: as) = These (IllFormed a) (AnyIllFormed as) + +-- Decidable + export -checkKind : (env : Env Kind w) -> (k : Kind) -> (t : RawCTy w) -> Bool - -checkAllKinds : (env : Env Kind w) -> (k : Kind) -> (ts : List (RawCTy w)) -> Bool - -synthKind env (TVar x) = Just (lookup env x) -synthKind env TNat = Just KStar -synthKind env (TArrow t u) = do - guard (checkKind env KStar t) - guard (checkKind env KStar u) - Just KStar -synthKind env (TSum ts) = do - guard (checkAllKinds env KStar ts) - Just KStar -synthKind env (TProd ts) = do - guard (checkAllKinds env KStar ts) - Just KStar -synthKind env (TApp f t) = do - dom `KArrow` cod <- synthKind env f - | _ => Nothing - guard (checkKind env dom t) - Just cod -synthKind env (TAnnot t k) = do - guard (checkKind env k t) - Just k - -checkKind env k (TFix x t) = checkKind (env :< (x :~ k)) k t -checkKind env k (TEmbed a) = - case synthKind env a of - Nothing => False - Just k' => k == k' - -checkAllKinds env k [] = True -checkAllKinds env k (t :: ts) = checkKind env k t && checkAllKinds env k ts +illFormed : (a : Ty n) -> Bool +anyIllFormed : (as : List (Ty n)) -> Bool +any1IllFormed : (as : List1 (Ty n)) -> Bool + + +illFormed (TVar j) = False +illFormed TNat = False +illFormed (TArrow as b) = any1IllFormed as || illFormed b +illFormed (TUnion as) = any1IllFormed as +illFormed (TProd as) = anyIllFormed as +illFormed (TSum as) = anyIllFormed as +illFormed (TFix a) = (FZ `notEnvPositiveIn` a) || illFormed a + +anyIllFormed [] = False +anyIllFormed (a :: as) = illFormed a || anyIllFormed as + +any1IllFormed (a ::: as) = illFormed a || anyIllFormed as export -synthKindPrf : (env : Env Kind w) -> (a : RawSTy w) -> synthKind env a `OnlyWhen` SynthKind env a +reflectIllFormed : (a : Ty n) -> IllFormed a `Reflects` illFormed a +reflectAnyIllFormed : (as : List (Ty n)) -> AnyIllFormed as `Reflects` anyIllFormed as +reflectAny1IllFormed : (as : List1 (Ty n)) -> Any1IllFormed as `Reflects` any1IllFormed as + +reflectIllFormed (TVar j) = RFalse id +reflectIllFormed TNat = RFalse id +reflectIllFormed (TArrow as b) = + reflectThese (reflectAny1IllFormed as) (reflectIllFormed b) +reflectIllFormed (TUnion as) = reflectAny1IllFormed as +reflectIllFormed (TProd as) = reflectAnyIllFormed as +reflectIllFormed (TSum as) = reflectAnyIllFormed as +reflectIllFormed (TFix a) = reflectThese (reflectNotPositiveIn FZ a) (reflectIllFormed a) + +reflectAnyIllFormed [] = RFalse id +reflectAnyIllFormed (a :: as) = + reflectThese (reflectIllFormed a) (reflectAnyIllFormed as) + +reflectAny1IllFormed (a ::: as) = + reflectThese (reflectIllFormed a) (reflectAnyIllFormed as) + +-------------------------------------------------------------------------------- +-- Thinning -------------------------------------------------------------------- +-------------------------------------------------------------------------------- + +thin : k `Thins` n -> Ty k -> Ty n +thinAll : k `Thins` n -> List (Ty k) -> List (Ty n) +thinAll1 : k `Thins` n -> List1 (Ty k) -> List1 (Ty n) + +thin f (TVar i) = TVar (index f i) +thin f TNat = TNat +thin f (TArrow as b) = TArrow (thinAll1 f as) (thin f b) +thin f (TUnion as) = TUnion (thinAll1 f as) +thin f (TProd as) = TProd (thinAll f as) +thin f (TSum as) = TSum (thinAll f as) +thin f (TFix a) = TFix (thin (Keep f) a) + +thinAll f [] = [] +thinAll f (a :: as) = thin f a :: thinAll f as + +thinAll1 f (a ::: as) = thin f a ::: thinAll f as + +-- Renaming Coalgebra + +thinCong : f ~~~ g -> (a : Ty k) -> thin f a = thin g a +thinCongAll : f ~~~ g -> (as : List (Ty k)) -> thinAll f as = thinAll g as +thinCongAll1 : f ~~~ g -> (as : List1 (Ty k)) -> thinAll1 f as = thinAll1 g as + +thinCong prf (TVar i) = cong TVar (prf.index i) +thinCong prf TNat = Refl +thinCong prf (TArrow as b) = cong2 TArrow (thinCongAll1 prf as) (thinCong prf b) +thinCong prf (TUnion as) = cong TUnion (thinCongAll1 prf as) +thinCong prf (TProd as) = cong TProd (thinCongAll prf as) +thinCong prf (TSum as) = cong TSum (thinCongAll prf as) +thinCong prf (TFix a) = cong TFix (thinCong (KeepKeep prf) a) + +thinCongAll prf [] = Refl +thinCongAll prf (a :: as) = cong2 (::) (thinCong prf a) (thinCongAll prf as) + +thinCongAll1 prf (a ::: as) = cong2 (:::) (thinCong prf a) (thinCongAll prf as) + +thinId : (a : Ty n) -> thin Id a = a +thinIdAll : (as : List (Ty n)) -> thinAll Id as = as +thinIdAll1 : (as : List1 (Ty n)) -> thinAll1 Id as = as + +thinId (TVar i) = cong TVar (indexId i) +thinId TNat = Refl +thinId (TArrow as b) = cong2 TArrow (thinIdAll1 as) (thinId b) +thinId (TUnion as) = cong TUnion (thinIdAll1 as) +thinId (TProd as) = cong TProd (thinIdAll as) +thinId (TSum as) = cong TSum (thinIdAll as) +thinId (TFix a) = cong TFix (trans (thinCong (KeepId IdId) a) (thinId a)) + +thinIdAll [] = Refl +thinIdAll (a :: as) = cong2 (::) (thinId a) (thinIdAll as) + +thinIdAll1 (a ::: as) = cong2 (:::) (thinId a) (thinIdAll as) + export -checkKindPrf : (env : Env Kind w) -> (k : Kind) -> (t : RawCTy w) -> CheckKind env k t `Reflects` checkKind env k t -checkAllKindsPrf : - (env : Env Kind w) -> (k : Kind) -> - (ts : List (RawCTy w)) -> All (CheckKind env k) ts `Reflects` checkAllKinds env k ts - -synthKindPrf env (TVar x) = Yes TVar -synthKindPrf env TNat = Yes TNat -synthKindPrf env (TArrow t u) with (checkKindPrf env KStar t) | (checkKind env KStar t) - _ | RTrue tStar | _ with (checkKindPrf env KStar u) | (checkKind env KStar u) - _ | RTrue uStar | _ = Yes (TArrow tStar uStar) - _ | RFalse uUnstar | _ = No (\_ => \case TArrow _ uStar => uUnstar uStar) - _ | RFalse tUnstar | _ = No (\_ => \case TArrow tStar _ => tUnstar tStar) -synthKindPrf env (TSum ts) with (checkAllKindsPrf env KStar ts) | (checkAllKinds env KStar ts) - _ | RTrue tsStar | _ = Yes (TSum tsStar) - _ | RFalse tsUnstar | _ = No (\_ => \case TSum tsStar => tsUnstar tsStar) -synthKindPrf env (TProd ts) with (checkAllKindsPrf env KStar ts) | (checkAllKinds env KStar ts) - _ | RTrue tsStar | _ = Yes (TProd tsStar) - _ | RFalse tsUnstar | _ = No (\_ => \case TProd tsStar => tsUnstar tsStar) -synthKindPrf env (TApp f t) with (synthKindPrf env f) | (synthKind env f) - _ | Yes fArrow | Just (KArrow dom cod) with (checkKindPrf env dom t) | (checkKind env dom t) - _ | RTrue uDom | _ = Yes (TApp fArrow uDom) - _ | RFalse uUndom | _ = - No (\_ => \case - TApp fKind uDom => case synthKindUniq fArrow fKind of - Refl => uUndom uDom) - _ | Yes fStar | Just KStar = No (\_ => \case TApp fArrow _ => absurd (synthKindUniq fStar fArrow)) - _ | No fUnkind | Nothing = No (\_ => \case TApp fKind _ => void (fUnkind _ fKind)) -synthKindPrf env (TAnnot t k) with (checkKindPrf env k t) | (checkKind env k t) - _ | RTrue tKind | _ = Yes (TAnnot tKind) - _ | RFalse tUnkind | _ = No (\_ => \case TAnnot tKind => tUnkind tKind) - -checkKindPrf env k (TFix x t) with (checkKindPrf (env :< (x :~ k)) k t) | (checkKind (env :< (x :~ k)) k t) - _ | RTrue tKind | _ = RTrue (TFix tKind) - _ | RFalse tUnkind | _ = RFalse (\case TFix tKind => tUnkind tKind) -checkKindPrf env k (TEmbed a) with (synthKindPrf env a) | (synthKind env a) - _ | Yes aKind | Just k' with (decEqReflects k k') | (k == k') - _ | RTrue eq | _ = RTrue (TEmbed aKind eq) - _ | RFalse neq | _ = RFalse (\case TEmbed aKind' eq => neq $ trans eq $ synthKindUniq aKind' aKind) - _ | No aUnkind | _ = RFalse (\case TEmbed aKind Refl => aUnkind _ aKind) - -checkAllKindsPrf env k [] = RTrue [] -checkAllKindsPrf env k (t :: ts) with (checkKindPrf env k t) | (checkKind env k t) - _ | RFalse tUnkind | _ = RFalse (\case (tKind :: _) => tUnkind tKind) - _ | RTrue tKind | _ with (checkAllKindsPrf env k ts) | (checkAllKinds env k ts) - _ | RTrue tsKinds | _ = RTrue (tKind :: tsKinds) - _ | RFalse tsUnkinds | _ = RFalse (\case (_ :: tsKinds) => tsUnkinds tsKinds) +Rename Ty where + var = TVar + rename = thin + renameCong = thinCong + renameId = thinId + +-- Properties ------------------------------------------------------------------ + +-- Occurs -- + +thinOccursIn : + (0 f : k `Thins` n) -> (0 i : Fin k) -> (a : Ty k) -> + i `OccursIn` a -> + index f i `OccursIn` thin f a +thinOccursInAny : + (0 f : k `Thins` n) -> (0 i : Fin k) -> (as : List (Ty k)) -> + i `OccursInAny` as -> + index f i `OccursInAny` thinAll f as +thinOccursInAny1 : + (0 f : k `Thins` n) -> (0 i : Fin k) -> (as : List1 (Ty k)) -> + i `OccursInAny1` as -> + index f i `OccursInAny1` thinAll1 f as + +thinOccursIn f i (TVar x) = \Refl => Refl +thinOccursIn f i TNat = id +thinOccursIn f i (TArrow as b) = bimap (thinOccursInAny1 f i as) (thinOccursIn f i b) +thinOccursIn f i (TUnion as) = thinOccursInAny1 f i as +thinOccursIn f i (TProd as) = thinOccursInAny f i as +thinOccursIn f i (TSum as) = thinOccursInAny f i as +thinOccursIn f i (TFix a) = + rewrite sym $ indexKeepFS f i in + thinOccursIn (Keep f) (FS i) a + +thinOccursInAny f i [] = id +thinOccursInAny f i (a :: as) = bimap (thinOccursIn f i a) (thinOccursInAny f i as) + +thinOccursInAny1 f i (a ::: as) = bimap (thinOccursIn f i a) (thinOccursInAny f i as) + +-- Inverse + +thinOccursInInv' : + (0 f : k `Thins` n) -> (0 i : Fin n) -> + (a : Ty k) -> + i `OccursIn` thin f a -> + (j ** (index f j = i, j `OccursIn` a)) +thinOccursInAnyInv' : + (0 f : k `Thins` n) -> (0 i : Fin n) -> + (as : List (Ty k)) -> + i `OccursInAny` thinAll f as -> + (j ** (index f j = i, j `OccursInAny` as)) +thinOccursInAny1Inv' : + (0 f : k `Thins` n) -> (0 i : Fin n) -> + (as : List1 (Ty k)) -> + i `OccursInAny1` thinAll1 f as -> + (j ** (index f j = i, j `OccursInAny1` as)) + +thinOccursInInv' f i (TVar j) = \eq => (j ** (sym eq , Refl)) +thinOccursInInv' f i TNat = absurd +thinOccursInInv' f i (TArrow as b) = + these + (\occurs => + let (j ** (eq, prf)) = thinOccursInAny1Inv' f i as occurs in + (j ** (eq, This prf))) + (\occurs => + let (j ** (eq, prf)) = thinOccursInInv' f i b occurs in + (j ** (eq, That prf))) + (\occurs1, occurs2 => + let (j1 ** (eq1, prf1)) = thinOccursInAny1Inv' f i as occurs1 in + let (j2 ** (eq2, prf2)) = thinOccursInInv' f i b occurs2 in + (j1 ** (eq1, + Both prf1 $ + rewrite indexInjective f {x = j1, y = j2} $ trans eq1 (sym eq2) in + prf2))) +thinOccursInInv' f i (TUnion as) = thinOccursInAny1Inv' f i as +thinOccursInInv' f i (TProd as) = thinOccursInAnyInv' f i as +thinOccursInInv' f i (TSum as) = thinOccursInAnyInv' f i as +thinOccursInInv' f i (TFix a) = + \occurs => + case thinOccursInInv' (Keep f) (FS i) a occurs of + (FZ ** prf) => absurd (trans (sym $ indexKeepFZ f) (fst prf)) + (FS j ** (eq, prf)) => + (j ** (irrelevantEq (injective $ trans (sym $ indexKeepFS f j) eq), prf)) + +thinOccursInAnyInv' f i [] = absurd +thinOccursInAnyInv' f i (a :: as) = + these + (\occurs => + let (j ** (eq, prf)) = thinOccursInInv' f i a occurs in + (j ** (eq, This prf))) + (\occurs => + let (j ** (eq, prf)) = thinOccursInAnyInv' f i as occurs in + (j ** (eq, That prf))) + (\occurs1, occurs2 => + let (j1 ** (eq1, prf1)) = thinOccursInInv' f i a occurs1 in + let (j2 ** (eq2, prf2)) = thinOccursInAnyInv' f i as occurs2 in + (j1 ** (eq1, + Both prf1 $ + rewrite indexInjective f {x = j1, y = j2} $ trans eq1 (sym eq2) in + prf2))) + +thinOccursInAny1Inv' f i (a ::: as) = + these + (\occurs => + let (j ** (eq, prf)) = thinOccursInInv' f i a occurs in + (j ** (eq, This prf))) + (\occurs => + let (j ** (eq, prf)) = thinOccursInAnyInv' f i as occurs in + (j ** (eq, That prf))) + (\occurs1, occurs2 => + let (j1 ** (eq1, prf1)) = thinOccursInInv' f i a occurs1 in + let (j2 ** (eq2, prf2)) = thinOccursInAnyInv' f i as occurs2 in + (j1 ** (eq1, + Both prf1 $ + rewrite indexInjective f {x = j1, y = j2} $ trans eq1 (sym eq2) in + prf2))) + +thinOccursInInv : + (0 f : k `Thins` n) -> (0 i : Fin k) -> (a : Ty k) -> + index f i `OccursIn` thin f a -> + i `OccursIn` a +thinOccursInInv f i a occurs = + let (j ** (eq, prf)) = thinOccursInInv' f (index f i) a occurs in + rewrite indexInjective f {x = i, y = j} $ sym eq in + prf + +thinOccursInAny1Inv : + (0 f : k `Thins` n) -> (0 i : Fin k) -> (as : List1 (Ty k)) -> + index f i `OccursInAny1` thinAll1 f as -> + i `OccursInAny1` as +thinOccursInAny1Inv f i as occurs = + let (j ** (eq, prf)) = thinOccursInAny1Inv' f (index f i) as occurs in + rewrite indexInjective f {x = i, y = j} $ sym eq in + prf + +-- Not Positive -- + +thinNotPositiveInv : + (0 f : k `Thins` n) -> (0 i : Fin k) -> (a : Ty k) -> + index f i `NotPositiveIn` thin f a -> i `NotPositiveIn` a +thinNotPositiveAnyInv : + (0 f : k `Thins` n) -> (0 i : Fin k) -> (as : List (Ty k)) -> + index f i `NotPositiveInAny` thinAll f as -> i `NotPositiveInAny` as +thinNotPositiveAny1Inv : + (0 f : k `Thins` n) -> (0 i : Fin k) -> (as : List1 (Ty k)) -> + index f i `NotPositiveInAny1` thinAll1 f as -> i `NotPositiveInAny1` as + +thinNotPositiveInv f i (TVar j) = id +thinNotPositiveInv f i TNat = id +thinNotPositiveInv f i (TArrow as b) = + bimap + (thinOccursInAny1Inv f i as) + (thinNotPositiveInv f i b) +thinNotPositiveInv f i (TUnion as) = thinNotPositiveAny1Inv f i as +thinNotPositiveInv f i (TProd as) = thinNotPositiveAnyInv f i as +thinNotPositiveInv f i (TSum as) = thinNotPositiveAnyInv f i as +thinNotPositiveInv f i (TFix a) = + \occurs => + thinOccursInInv (Keep f) (FS i) a $ + rewrite indexKeepFS f i in + occurs + +thinNotPositiveAnyInv f i [] = id +thinNotPositiveAnyInv f i (a :: as) = + bimap (thinNotPositiveInv f i a) (thinNotPositiveAnyInv f i as) + +thinNotPositiveAny1Inv f i (a ::: as) = + bimap (thinNotPositiveInv f i a) (thinNotPositiveAnyInv f i as) + +-- Ill Formed -- + +thinIllFormedInv : + (0 f : k `Thins` n) -> (a : Ty k) -> + IllFormed (thin f a) -> IllFormed a +thinAnyIllFormedInv : + (0 f : k `Thins` n) -> (as : List (Ty k)) -> + AnyIllFormed (thinAll f as) -> AnyIllFormed as +thinAny1IllFormedInv : + (0 f : k `Thins` n) -> (as : List1 (Ty k)) -> + Any1IllFormed (thinAll1 f as) -> Any1IllFormed as + +thinIllFormedInv f (TVar i) = id +thinIllFormedInv f TNat = id +thinIllFormedInv f (TArrow as b) = bimap (thinAny1IllFormedInv f as) (thinIllFormedInv f b) +thinIllFormedInv f (TUnion as) = thinAny1IllFormedInv f as +thinIllFormedInv f (TProd as) = thinAnyIllFormedInv f as +thinIllFormedInv f (TSum as) = thinAnyIllFormedInv f as +thinIllFormedInv f (TFix a) = + bimap + (\npos => thinNotPositiveInv (Keep f) FZ a $ rewrite indexKeepFZ f in npos) + (thinIllFormedInv (Keep f) a) + +thinAnyIllFormedInv f [] = id +thinAnyIllFormedInv f (a :: as) = bimap (thinIllFormedInv f a) (thinAnyIllFormedInv f as) + +thinAny1IllFormedInv f (a ::: as) = bimap (thinIllFormedInv f a) (thinAnyIllFormedInv f as) + +-------------------------------------------------------------------------------- +-- Substitution ---------------------------------------------------------------- +-------------------------------------------------------------------------------- public export -ATy : {w : World} -> Env Kind w -> Type -ATy env = Subset (RawCTy w) (CheckKind env KStar) +fromVar : Either (Fin n) (Ty n) -> Ty n +fromVar = either TVar id + +export +sub : Env k n (Ty n) -> Ty k -> Ty n +subAll : Env k n (Ty n) -> List (Ty k) -> List (Ty n) +subAll1 : Env k n (Ty n) -> List1 (Ty k) -> List1 (Ty n) + +sub env (TVar i) = fromVar $ lookup env i +sub env TNat = TNat +sub env (TArrow as b) = TArrow (subAll1 env as) (sub env b) +sub env (TUnion as) = TUnion (subAll1 env as) +sub env (TProd as) = TProd (subAll env as) +sub env (TSum as) = TSum (subAll env as) +sub env (TFix a) = TFix (sub (lift (Drop Id) env :< TVar FZ) a) + +subAll env [] = [] +subAll env (a :: as) = sub env a :: subAll env as + +subAll1 env (a ::: as) = sub env a ::: subAll env as + +-- Properties ------------------------------------------------------------------ + +pushEither : + (0 f : c -> d) -> (0 g : a -> c) -> (0 h : b -> c) -> (x : Either a b) -> + f (either g h x) = either (f . g) (f . h) x +pushEither f g h (Left x) = Refl +pushEither f g h (Right x) = Refl + +-- Occurs -- + +subOccursIn : + (env : Env k n (Ty n)) -> (i : Fin k) -> (a : Ty k) -> + j `OccursIn` fromVar (lookup env i) -> + i `OccursIn` a -> + j `OccursIn` sub env a +subOccursInAny : + (env : Env k n (Ty n)) -> (i : Fin k) -> (as : List (Ty k)) -> + j `OccursIn` fromVar (lookup env i) -> + i `OccursInAny` as -> + j `OccursInAny` subAll env as +subOccursInAny1 : + (env : Env k n (Ty n)) -> (i : Fin k) -> (as : List1 (Ty k)) -> + j `OccursIn` fromVar (lookup env i) -> + i `OccursInAny1` as -> + j `OccursInAny1` subAll1 env as + +subOccursIn env i (TVar x) occurs = \Refl => occurs +subOccursIn env i TNat occurs = id +subOccursIn env i (TArrow as b) occurs = + bimap + (subOccursInAny1 env i as occurs) + (subOccursIn env i b occurs) +subOccursIn env i (TUnion as) occurs = subOccursInAny1 env i as occurs +subOccursIn env i (TProd as) occurs = subOccursInAny env i as occurs +subOccursIn env i (TSum as) occurs = subOccursInAny env i as occurs +subOccursIn env i (TFix a) occurs = + subOccursIn (lift (Drop Id) env :< TVar FZ) (FS i) a {j = FS j} $ + rewrite lookupFS (lift (Drop Id) env) (TVar FZ) i in + rewrite lookupLift (Drop Id) env i in + rewrite eitherBimapFusion TVar id (index (Drop Id)) (thin (Drop Id)) (lookup env i) in + rewrite sym $ pushEither (thin (Drop Id)) TVar id (lookup env i) in + rewrite sym $ indexId j in + rewrite sym $ indexDrop Id j in + thinOccursIn (Drop Id) j (fromVar $ lookup env i) $ + occurs + +subOccursInAny env i [] occurs = id +subOccursInAny env i (a :: as) occurs = + bimap (subOccursIn env i a occurs) (subOccursInAny env i as occurs) + +subOccursInAny1 env i (a ::: as) occurs = + bimap (subOccursIn env i a occurs) (subOccursInAny env i as occurs) + +-- Inverse + +0 EnvOccursUniq : Env k n (Ty n) -> (i : Fin n) -> (j : Fin k) -> Type +EnvOccursUniq env i j = (x : Fin k) -> i `OccursIn` fromVar (lookup env x) -> j = x + +liftEnvOccursUniq : + (0 env : Env k n (Ty n)) -> + EnvOccursUniq env i j -> + EnvOccursUniq (lift (Drop Id) env :< TVar FZ) (FS i) (FS j) +liftEnvOccursUniq env prf FZ = + rewrite lookupFZ (lift (Drop Id) env) (TVar FZ) in + absurd +liftEnvOccursUniq env prf (FS x) = + rewrite lookupFS (lift (Drop Id) env) (TVar FZ) x in + rewrite lookupLift (Drop Id) env x in + rewrite eitherBimapFusion TVar id (index (Drop Id)) (rename (Drop Id)) (lookup env x) in + \occurs => + cong FS $ + prf x $ + thinOccursInInv (Drop Id) i (fromVar $ lookup env x) $ + rewrite pushEither (rename (Drop Id)) TVar id (lookup env x) in + rewrite indexDrop Id i in + rewrite indexId i in + occurs + +liftOccursUniqFZ : + (env : Env k n (Ty n)) -> + EnvOccursUniq (lift (Drop Id) env :< TVar FZ) FZ FZ +liftOccursUniqFZ env FZ = + rewrite lookupFZ (lift (Drop Id) env) (TVar FZ) in + const Refl +liftOccursUniqFZ env (FS x) = + rewrite lookupFS (lift (Drop Id) env) (TVar FZ) x in + rewrite lookupLift (Drop Id) env x in + rewrite eitherBimapFusion TVar id (index (Drop Id)) (rename (Drop Id)) (lookup env x) in + \occurs => + let + (j ** (eq, occurs')) = + thinOccursInInv' (Drop Id) FZ (fromVar $ lookup env x) $ + rewrite pushEither (rename (Drop Id)) TVar id (lookup env x) in + occurs + in + absurd $ trans (sym eq) (indexDrop Id j) + +subOccursInInv : + (0 env : Env k n (Ty n)) -> + (0 prf : EnvOccursUniq env i j) -> + (a : Ty k) -> + i `OccursIn` sub env a -> j `OccursIn` a +subOccursInAnyInv : + (0 env : Env k n (Ty n)) -> + (0 prf : EnvOccursUniq env i j) -> + (as : List (Ty k)) -> + i `OccursInAny` subAll env as -> j `OccursInAny` as +subOccursInAny1Inv : + (0 env : Env k n (Ty n)) -> + (0 prf : EnvOccursUniq env i j) -> + (as : List1 (Ty k)) -> + i `OccursInAny1` subAll1 env as -> j `OccursInAny1` as + +subOccursInInv env prf (TVar x) = \p => irrelevantEq $ prf x p +subOccursInInv env prf TNat = id +subOccursInInv env prf (TArrow as b) = + bimap + (subOccursInAny1Inv env prf as) + (subOccursInInv env prf b) +subOccursInInv env prf (TUnion as) = subOccursInAny1Inv env prf as +subOccursInInv env prf (TProd as) = subOccursInAnyInv env prf as +subOccursInInv env prf (TSum as) = subOccursInAnyInv env prf as +subOccursInInv env prf (TFix a) = + subOccursInInv + (lift (Drop Id) env :< TVar FZ) + (liftEnvOccursUniq env prf) + a + +subOccursInAnyInv env prf [] = id +subOccursInAnyInv env prf (a :: as) = + bimap + (subOccursInInv env prf a) + (subOccursInAnyInv env prf as) + +subOccursInAny1Inv env prf (a ::: as) = + bimap + (subOccursInInv env prf a) + (subOccursInAnyInv env prf as) + + +-- Not Positive -- + +subNotPositiveIn : + (env : Env k n (Ty n)) -> (i : Fin k) -> (a : Ty k) -> + j `OccursIn` fromVar (lookup env i) -> + i `NotPositiveIn` a -> + j `NotPositiveIn` sub env a +subNotPositiveInAny : + (env : Env k n (Ty n)) -> (i : Fin k) -> (as : List (Ty k)) -> + j `OccursIn` fromVar (lookup env i) -> + i `NotPositiveInAny` as -> + j `NotPositiveInAny` subAll env as +subNotPositiveInAny1 : + (env : Env k n (Ty n)) -> (i : Fin k) -> (as : List1 (Ty k)) -> + j `OccursIn` fromVar (lookup env i) -> + i `NotPositiveInAny1` as -> + j `NotPositiveInAny1` subAll1 env as + +subNotPositiveIn env i (TVar x) occurs = absurd +subNotPositiveIn env i TNat occurs = id +subNotPositiveIn env i (TArrow as b) occurs = + bimap + (subOccursInAny1 env i as occurs) + (subNotPositiveIn env i b occurs) +subNotPositiveIn env i (TUnion as) occurs = subNotPositiveInAny1 env i as occurs +subNotPositiveIn env i (TProd as) occurs = subNotPositiveInAny env i as occurs +subNotPositiveIn env i (TSum as) occurs = subNotPositiveInAny env i as occurs +subNotPositiveIn env i (TFix a) occurs = + subOccursIn (lift (Drop Id) env :< TVar FZ) (FS i) a {j = FS j} $ + rewrite lookupFS (lift (Drop Id) env) (TVar FZ) i in + rewrite lookupLift (Drop Id) env i in + rewrite eitherBimapFusion TVar id (index (Drop Id)) (thin (Drop Id)) (lookup env i) in + rewrite sym $ pushEither (thin (Drop Id)) TVar id (lookup env i) in + rewrite sym $ indexId j in + rewrite sym $ indexDrop Id j in + thinOccursIn (Drop Id) j (fromVar $ lookup env i) $ + occurs + +subNotPositiveInAny env i [] occurs = id +subNotPositiveInAny env i (a :: as) occurs = + bimap + (subNotPositiveIn env i a occurs) + (subNotPositiveInAny env i as occurs) + +subNotPositiveInAny1 env i (a ::: as) occurs = + bimap + (subNotPositiveIn env i a occurs) + (subNotPositiveInAny env i as occurs) + +-- Inverse + +0 EnvPositiveIn : Env k n (Ty n) -> (i : Fin n) -> Type +EnvPositiveIn env i = (x : Fin k) -> Not (i `NotPositiveIn` fromVar (lookup env x)) + +liftPositiveInFZ : + (env : Env k n (Ty n)) -> + EnvPositiveIn (lift (Drop Id) env :< TVar FZ) FZ +liftPositiveInFZ env FZ = + rewrite lookupFZ (lift (Drop Id) env) (TVar FZ) in + id +liftPositiveInFZ env (FS x) = + rewrite lookupFS (lift (Drop Id) env) (TVar FZ) x in + rewrite lookupLift (Drop Id) env x in + rewrite eitherBimapFusion TVar id (index (Drop Id)) (rename (Drop Id)) (lookup env x) in + \npos => + let + (j ** (eq, occurs)) = + thinOccursInInv' (Drop Id) FZ (fromVar $ lookup env x) $ + rewrite pushEither (thin (Drop Id)) TVar id (lookup env x) in + notPositiveToOccurs _ npos + in + absurd $ trans (sym (indexDrop Id j)) eq + +subNotPositiveInInv : + (0 env : Env k n (Ty n)) -> + (0 prf1 : EnvPositiveIn env i) -> + (0 prf2 : EnvOccursUniq env i j) -> + (a : Ty k) -> + i `NotPositiveIn` sub env a -> j `NotPositiveIn` a +subNotPositiveInAnyInv : + (0 env : Env k n (Ty n)) -> + (0 prf1 : EnvPositiveIn env i) -> + (0 prf2 : EnvOccursUniq env i j) -> + (as : List (Ty k)) -> + i `NotPositiveInAny` subAll env as -> j `NotPositiveInAny` as +subNotPositiveInAny1Inv : + (0 env : Env k n (Ty n)) -> + (0 prf1 : EnvPositiveIn env i) -> + (0 prf2 : EnvOccursUniq env i j) -> + (as : List1 (Ty k)) -> + i `NotPositiveInAny1` subAll1 env as -> j `NotPositiveInAny1` as + +subNotPositiveInInv env prf1 prf2 (TVar x) = \npos => void $ prf1 x npos +subNotPositiveInInv env prf1 prf2 TNat = id +subNotPositiveInInv env prf1 prf2 (TArrow as b) = + bimap + (subOccursInAny1Inv env prf2 as) + (subNotPositiveInInv env prf1 prf2 b) +subNotPositiveInInv env prf1 prf2 (TUnion as) = subNotPositiveInAny1Inv env prf1 prf2 as +subNotPositiveInInv env prf1 prf2 (TProd as) = subNotPositiveInAnyInv env prf1 prf2 as +subNotPositiveInInv env prf1 prf2 (TSum as) = subNotPositiveInAnyInv env prf1 prf2 as +subNotPositiveInInv env prf1 prf2 (TFix a) = + subOccursInInv + (lift (Drop Id) env :< TVar FZ) + (liftEnvOccursUniq env prf2) + a + +subNotPositiveInAnyInv env prf1 prf2 [] = id +subNotPositiveInAnyInv env prf1 prf2 (a :: as) = + bimap + (subNotPositiveInInv env prf1 prf2 a) + (subNotPositiveInAnyInv env prf1 prf2 as) + +subNotPositiveInAny1Inv env prf1 prf2 (a ::: as) = + bimap + (subNotPositiveInInv env prf1 prf2 a) + (subNotPositiveInAnyInv env prf1 prf2 as) + +-- Ill Formed -- + +subIllFormed : + (env : Env k n (Ty n)) -> (a : Ty k) -> + IllFormed a -> IllFormed (sub env a) +subAnyIllFormed : + (env : Env k n (Ty n)) -> (as : List (Ty k)) -> + AnyIllFormed as -> AnyIllFormed (subAll env as) +subAny1IllFormed : + (env : Env k n (Ty n)) -> (as : List1 (Ty k)) -> + Any1IllFormed as -> Any1IllFormed (subAll1 env as) + +subIllFormed env (TVar i) = absurd +subIllFormed env TNat = id +subIllFormed env (TArrow as b) = bimap (subAny1IllFormed env as) (subIllFormed env b) +subIllFormed env (TUnion as) = subAny1IllFormed env as +subIllFormed env (TProd as) = subAnyIllFormed env as +subIllFormed env (TSum as) = subAnyIllFormed env as +subIllFormed env (TFix a) = + bimap + (subNotPositiveIn (lift (Drop Id) env :< TVar FZ) FZ a $ + rewrite lookupFZ (lift (Drop Id) env) (TVar FZ) in + Refl) + (subIllFormed (lift (Drop Id) env :< TVar FZ) a) + +subAnyIllFormed env [] = id +subAnyIllFormed env (a :: as) = bimap (subIllFormed env a) (subAnyIllFormed env as) + +subAny1IllFormed env (a ::: as) = bimap (subIllFormed env a) (subAnyIllFormed env as) + +-- Inverse + +export +0 EnvWellFormed : Env k n (Ty n) -> Type +EnvWellFormed env = (x : Fin k) -> Not (IllFormed $ fromVar $ lookup env x) + +liftEnvWellFormed : + (env : Env k n (Ty n)) -> + EnvWellFormed env -> + EnvWellFormed (lift (Drop Id) env :< TVar FZ) +liftEnvWellFormed env prf FZ = + rewrite lookupFZ (lift (Drop Id) env) (TVar FZ) in + id +liftEnvWellFormed env prf (FS x) = + rewrite lookupFS (lift (Drop Id) env) (TVar FZ) x in + rewrite lookupLift (Drop Id) env x in + rewrite eitherBimapFusion TVar id (index (Drop Id)) (rename (Drop Id)) (lookup env x) in + \ill => + prf x $ + thinIllFormedInv (Drop Id) (either TVar id $ lookup env x) $ + rewrite pushEither (thin (Drop Id)) TVar id (lookup env x) in + ill + +subIllFormedInv : + (0 env : Env k n (Ty n)) -> + (0 prf : EnvWellFormed env) -> + (a : Ty k) -> + IllFormed (sub env a) -> IllFormed a +subAnyIllFormedInv : + (0 env : Env k n (Ty n)) -> + (0 prf : EnvWellFormed env) -> + (as : List (Ty k)) -> + AnyIllFormed (subAll env as) -> AnyIllFormed as +subAny1IllFormedInv : + (0 env : Env k n (Ty n)) -> + (0 prf : EnvWellFormed env) -> + (as : List1 (Ty k)) -> + Any1IllFormed (subAll1 env as) -> Any1IllFormed as + +subIllFormedInv env prf (TVar i) = \ill => void $ prf i ill +subIllFormedInv env prf TNat = id +subIllFormedInv env prf (TArrow as b) = + bimap + (subAny1IllFormedInv env prf as) + (subIllFormedInv env prf b) +subIllFormedInv env prf (TUnion as) = subAny1IllFormedInv env prf as +subIllFormedInv env prf (TProd as) = subAnyIllFormedInv env prf as +subIllFormedInv env prf (TSum as) = subAnyIllFormedInv env prf as +subIllFormedInv env prf (TFix a) = + bimap + (subNotPositiveInInv + (lift (Drop Id) env :< TVar FZ) + (liftPositiveInFZ env) + (liftOccursUniqFZ env) + a) + (subIllFormedInv + (lift (Drop Id) env :< TVar FZ) + (liftEnvWellFormed env prf) + a) + +subAnyIllFormedInv env prf [] = id +subAnyIllFormedInv env prf (a :: as) = + bimap + (subIllFormedInv env prf a) + (subAnyIllFormedInv env prf as) + +subAny1IllFormedInv env prf (a ::: as) = + bimap + (subIllFormedInv env prf a) + (subAnyIllFormedInv env prf as) + +-- Equivalent + +export +subIllFormedEquiv : + (env : Env k n (Ty n)) -> + (0 prf : EnvWellFormed env) -> + (a : Ty k) -> + IllFormed a <=> IllFormed (sub env a) +subIllFormedEquiv env prf a = + MkEquivalence + { leftToRight = subIllFormed env a + , rightToLeft = subIllFormedInv env prf a + } -- cgit v1.2.3