summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Data/These/Decidable.idr16
-rw-r--r--src/Inky/Binding.idr371
-rw-r--r--src/Inky/Env.idr30
-rw-r--r--src/Inky/Erased.idr6
-rw-r--r--src/Inky/Kind.idr50
-rw-r--r--src/Inky/Kit.idr78
-rw-r--r--src/Inky/OnlyWhen.idr44
-rw-r--r--src/Inky/Thinning.idr173
-rw-r--r--src/Inky/Type.idr1016
9 files changed, 1073 insertions, 711 deletions
diff --git a/src/Data/These/Decidable.idr b/src/Data/These/Decidable.idr
new file mode 100644
index 0000000..c044ca4
--- /dev/null
+++ b/src/Data/These/Decidable.idr
@@ -0,0 +1,16 @@
+module Data.These.Decidable
+
+import Data.Bool.Decidable
+import Data.These
+
+export
+viaEquivalence : a <=> b -> a `Reflects` x -> b `Reflects` x
+viaEquivalence eq (RTrue x) = RTrue (eq.leftToRight x)
+viaEquivalence eq (RFalse f) = RFalse (f . eq.rightToLeft)
+
+export
+reflectThese : a `Reflects` x -> b `Reflects` y -> These a b `Reflects` x || y
+reflectThese (RTrue x) (RTrue y) = RTrue (Both x y)
+reflectThese (RTrue x) (RFalse ny) = RTrue (This x)
+reflectThese (RFalse nx) (RTrue y) = RTrue (That y)
+reflectThese (RFalse nx) (RFalse ny) = RFalse (these nx ny $ const ny)
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
+ }
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-30 05:42:26 +0000