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;

1 files changed, 0 insertions, 371 deletions

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