diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Inky.idr | 1 | ||||
| -rw-r--r-- | src/Inky/Binding.idr | 220 |
2 files changed, 220 insertions, 1 deletions
diff --git a/src/Inky.idr b/src/Inky.idr deleted file mode 100644 index c501caf..0000000 --- a/src/Inky.idr +++ /dev/null @@ -1 +0,0 @@ -module Inky diff --git a/src/Inky/Binding.idr b/src/Inky/Binding.idr new file mode 100644 index 0000000..7562f27 --- /dev/null +++ b/src/Inky/Binding.idr @@ -0,0 +1,220 @@ +module Inky.Binding + +import Control.Relation +import Control.Order +import Data.DPair +import Data.List +import Data.Nat +import Data.So +import Decidable.Equality + +-- Types ----------------------------------------------------------------------- + +data WorldRepr : Nat -> List Bool -> Type where + Done : 0 `WorldRepr` [] + True : w `WorldRepr` bs -> 1 + 2 * w `WorldRepr` True :: bs + False : w `WorldRepr` bs -> 2 * w `WorldRepr` False :: bs + +export +World : Type +World = List Bool + +export +Binder : Type +Binder = Nat + +Member : Binder -> World -> Type +n `Member` [] = Void +Z `Member` b :: bs = So b +S n `Member` b :: bs = n `Member` bs + +export +(:<) : World -> Binder -> World +[] :< Z = True :: [] +[] :< (S n) = False :: [] :< n +(_ :: bs) :< Z = True :: bs +(b :: bs) :< (S n) = b :: bs :< n + +snocSem : (bs : World) -> (k, n : Binder) -> n `Member` 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 Binder (`Member` w) + +-- Countable binders ----------------------------------------------------------- + +export +BZ : Binder +BZ = Z + +export +BS : Binder -> Binder +BS = S + +-- Binders to names ------------------------------------------------------------ + +export +name : forall w. (b : Binder) -> Name (w :< b) +name b = Element b ((snocSem w b b).rightToLeft (Left Refl)) + +export +binder : Name w -> Binder +binder = fst + +export +binderName : binder {w = w :< b} (name {w} b) = b +binderName = Refl + +-- Empty world ----------------------------------------------------------------- + +export +Empty : World +Empty = [] + +export +Uninhabited (Name Empty) 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 == n) of + Yes _ => Nothing + No neq => + Just + (Element n + (either + (\eq => void $ neq $ rewrite eq in soEq b) + id $ + (snocSem w b n).leftToRight member)) + +-- Freshness ------------------------------------------------------------------- + +export +FreshIn : Binder -> World -> Type +FreshIn k bs = So (k `gte` length bs) + +export +freshInEmpty : b `FreshIn` Empty +freshInEmpty = Oh + +snocLength : (w : World) -> (k : Binder) -> So (k `gte` length w) -> So (S k `gte` length (w :< 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 -> S b `FreshIn` w :< b +sucFresh prf = soRecomputable (snocLength w b prf) + +-- World inclusion ------------------------------------------------------------- + +export +(<=) : World -> World -> Type +w <= v = {n : Binder} -> n `Member` w -> n `Member` v + +export +coerce : (0 prf : w <= v) -> Name w -> Name v +coerce lte n = Element n.fst (lte n.snd) + +export +Reflexive World (<=) where + reflexive = id + +export +Transitive World (<=) where + transitive f g = g . f + +export +Preorder World (<=) where + +export +emptyMin : Empty <= w +emptyMin n impossible + +export +snocMono : {w, v : World} -> (b : Binder) -> w <= v -> w :< b <= v :< b +snocMono b lte {n} = (snocSem v b n).rightToLeft . mapSnd lte . (snocSem w b n).leftToRight + +export +freshLte : {b : Binder} -> {w : World} -> (0 fresh : b `FreshIn` w) -> w <= w :< b +freshLte _ {n} = (snocSem w b n).rightToLeft . Right + +-- DeBruijn Worlds ------------------------------------------------------------- + +export +WS : World -> World +WS = (False ::) + +public export +shift : World -> World +shift w = WS w :< BZ + +export +sucMono : w <= v -> WS w <= WS v +sucMono lte {n = (S n)} member = lte member + +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 {n = (S n)} member = member + +export +sucInjective : WS w <= WS v -> w <= v +sucInjective lte {n} member = lte {n = (S n)} member + +export +shiftInjective : shift w <= shift v -> w <= v +shiftInjective lte {n} member = lte {n = (S n)} member + +export +sucLteShiftInjective : WS w <= shift v -> w <= v +sucLteShiftInjective lte {n} member = lte {n = (S n)} member + +export +sucEmpty : WS Empty <= Empty +sucEmpty {n = (S n)} member impossible + +-- Suc and snoc ---------------------------------------------------------------- + +export +sucDistributesOverSnocLte : WS (w :< b) <= WS w :< BS b +sucDistributesOverSnocLte {n = (S n)} member = member + +export +sucDistributesOverSnocGte : WS w :< BS b <= WS (w :< b) +sucDistributesOverSnocGte {n = (S n)} member = member |