diff options
| -rw-r--r-- | inky.ipkg | 1 | ||||
| -rw-r--r-- | src/Inky/Binding.idr | 173 | ||||
| -rw-r--r-- | src/Inky/Env.idr | 30 | ||||
| -rw-r--r-- | src/Inky/Kit.idr | 2 |
4 files changed, 149 insertions, 57 deletions
@@ -6,5 +6,6 @@ options = "--total" modules = Inky.Binding + , Inky.Env , Inky.Erased , Inky.Kit diff --git a/src/Inky/Binding.idr b/src/Inky/Binding.idr index 4d8260a..8bd070d 100644 --- a/src/Inky/Binding.idr +++ b/src/Inky/Binding.idr @@ -10,32 +10,34 @@ 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 +record World where + constructor MkWorld + world : List Bool export -Binder : Type -Binder = Nat +record Binder where + constructor MkBinder + binder : Nat -Member : Binder -> World -> Type -n `Member` [] = Void +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 -[] :< Z = True :: [] -[] :< (S n) = False :: [] :< n -(_ :: bs) :< Z = True :: bs -(b :: bs) :< (S n) = b :: bs :< n +w :< x = MkWorld (snoc w.world x.binder) -snocSem : (bs : World) -> (k, n : Binder) -> n `Member` bs :< k <=> Either (n = k) (n `Member` bs) +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 @@ -56,40 +58,41 @@ snocSem (b :: bs) (S k) (S n) = export Name : World -> Type -Name w = Subset Binder (`Member` w) +Name w = Subset Nat (`Member` w.world) -- Countable binders ----------------------------------------------------------- export BZ : Binder -BZ = Z +BZ = MkBinder Z export BS : Binder -> Binder -BS = S +BS = MkBinder . S . binder -- Binders to names ------------------------------------------------------------ export nameOf : forall w. (b : Binder) -> Name (w :< b) -nameOf b = Element b ((snocSem w b b).rightToLeft (Left Refl)) +nameOf b = Element b.binder ((snocSem w.world b.binder b.binder).rightToLeft (Left Refl)) export binder : Name w -> Binder -binder = fst +binder = MkBinder . fst + -- fst export -binderNameOf : binder {w = w :< b} (nameOf {w} b) = b -binderNameOf = Refl +binderNameOf : (b : Binder) -> binder {w = w :< b} (nameOf {w} b) = b +binderNameOf (MkBinder k) = Refl --- Empty world ----------------------------------------------------------------- +-- [<] world ----------------------------------------------------------------- export -Empty : World -Empty = [] +Lin : World +Lin = MkWorld [] export -Uninhabited (Name Empty) where +Uninhabited (Name [<]) where uninhabited n = void n.snd -- Names are comparable and stripable ------------------------------------------ @@ -105,31 +108,51 @@ soEq (S k) = soEq k export strip : {b : Binder} -> Name (w :< b) -> Maybe (Name w) strip (Element n member) = - case decSo (b == n) of + case decSo (b.binder == n) of Yes _ => Nothing No neq => Just (Element n (either - (\eq => void $ neq $ rewrite eq in soEq b) + (\eq => void $ neq $ rewrite eq in soEq b.binder) id $ - (snocSem w b n).leftToRight member)) + (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 : {b : Binder} -> Lazy a -> Lazy (Name w -> a) -> Name (w :< b) -> a +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 -FreshIn : Binder -> World -> Type -FreshIn k bs = So (k `gte` length bs) +record FreshIn (b : Binder) (w : World) where + constructor MkFresh + fresh : So (b.binder `gte` length w.world) export -freshInEmpty : b `FreshIn` Empty -freshInEmpty = Oh +freshInEmpty : b `FreshIn` [<] +freshInEmpty = MkFresh Oh -snocLength : (w : World) -> (k : Binder) -> So (k `gte` length w) -> So (S k `gte` length (w :< k)) +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 @@ -140,54 +163,65 @@ soRecomputable Oh = Oh export sucFresh : b `FreshIn` w -> BS b `FreshIn` w :< b -sucFresh prf = soRecomputable (snocLength w b prf) +sucFresh prf = MkFresh (soRecomputable (snocLength w.world b.binder prf.fresh)) -- World inclusion ------------------------------------------------------------- export -(<=) : World -> World -> Type -w <= v = {n : Binder} -> n `Member` w -> n `Member` v +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 n.snd) +coerce lte n = Element n.fst (lte.lte _ n.snd) export Reflexive World (<=) where - reflexive = id + reflexive = MkLte (\_, prf => prf) export Transitive World (<=) where - transitive f g = g . f + transitive f g = MkLte (\n => g.lte n . f.lte n) export Preorder World (<=) where export -emptyMin : Empty <= w -emptyMin n impossible +emptyMin : [<] <= w +emptyMin = MkLte (\_ => absurd) 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 +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 _ {n} = (snocSem w b n).rightToLeft . Right +freshLte _ = MkLte (\n => (snocSem w.world b.binder n).rightToLeft . Right) -- DeBruijn Worlds ------------------------------------------------------------- export WS : World -> World -WS = (False ::) +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 {n = (S n)} member = lte member +sucMono lte = MkLte (\case + Z => absurd + (S n) => lte.lte n) public export shiftMono : {w, v : World} -> w <= v -> shift w <= shift v @@ -195,30 +229,57 @@ shiftMono lte = snocMono BZ (sucMono lte) export sucLteShift : WS w <= shift w -sucLteShift {n = (S n)} member = member +sucLteShift = MkLte (\case + Z => absurd + S n => id) export sucInjective : WS w <= WS v -> w <= v -sucInjective lte {n} member = lte {n = (S n)} member +sucInjective lte = MkLte (\n => lte.lte (S n)) export shiftInjective : shift w <= shift v -> w <= v -shiftInjective lte {n} member = lte {n = (S n)} member +shiftInjective lte = MkLte (\n => lte.lte (S n)) export sucLteShiftInjective : WS w <= shift v -> w <= v -sucLteShiftInjective lte {n} member = lte {n = (S n)} member +sucLteShiftInjective lte = MkLte (\n => lte.lte (S n)) export -sucEmpty : WS Empty <= Empty -sucEmpty {n = (S n)} member impossible +sucEmpty : WS [<] <= [<] +sucEmpty = + MkLte (\case + Z => absurd + (S n) => absurd) -- Suc and snoc ---------------------------------------------------------------- export sucDistributesOverSnocLte : WS (w :< b) <= WS w :< BS b -sucDistributesOverSnocLte {n = (S n)} member = member +sucDistributesOverSnocLte = + MkLte (\case + Z => absurd + (S n) => id) export sucDistributesOverSnocGte : WS w :< BS b <= WS (w :< b) -sucDistributesOverSnocGte {n = (S n)} member = member +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 {}) diff --git a/src/Inky/Env.idr b/src/Inky/Env.idr new file mode 100644 index 0000000..174b681 --- /dev/null +++ b/src/Inky/Env.idr @@ -0,0 +1,30 @@ +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/Kit.idr b/src/Inky/Kit.idr index d7dc286..a601a3f 100644 --- a/src/Inky/Kit.idr +++ b/src/Inky/Kit.idr @@ -1,6 +1,6 @@ module Inky.Kit -import Control.Monad.Identity +import public Control.Monad.Identity import Inky.Binding import Inky.Erased |