diff options
Diffstat (limited to 'src/Inky')
| -rw-r--r-- | src/Inky/Binding.idr | 88 |
1 files changed, 87 insertions, 1 deletions
diff --git a/src/Inky/Binding.idr b/src/Inky/Binding.idr index 8bd070d..56f079e 100644 --- a/src/Inky/Binding.idr +++ b/src/Inky/Binding.idr @@ -2,9 +2,11 @@ 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 @@ -79,7 +81,6 @@ nameOf b = Element b.binder ((snocSem w.world b.binder b.binder).rightToLeft (Le export binder : Name w -> Binder binder = MkBinder . fst - -- fst export binderNameOf : (b : Binder) -> binder {w = w :< b} (nameOf {w} b) = b @@ -283,3 +284,88 @@ stripCoerceSnoc : 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 |