From 6cb862033acc5dd63abf38dd58f9dce49cb4506f Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sun, 27 Feb 2022 02:17:09 +0100
Subject: [PATCH] add Quox.OPE

---
 src/Quox/OPE.idr | 195 +++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 195 insertions(+)
 create mode 100644 src/Quox/OPE.idr

diff --git a/src/Quox/OPE.idr b/src/Quox/OPE.idr
new file mode 100644
index 0000000..51cf042
--- /dev/null
+++ b/src/Quox/OPE.idr
@@ -0,0 +1,195 @@
+||| "order preserving embeddings", for recording a correspondence between
+||| a smaller scope and part of a larger one.
+module Quox.OPE
+
+import Data.Nat
+
+
+public export
+data OPE : Nat -> Nat -> Type where
+  Id   : OPE n n
+  Drop : OPE m n -> OPE m     (S n)
+  Keep : OPE m n -> OPE (S m) (S n)
+%name OPE p, q
+
+public export %inline Injective Drop where injective Refl = Refl
+public export %inline Injective Keep where injective Refl = Refl
+
+public export
+opeZero : {n : Nat} -> OPE 0 n
+opeZero {n = 0}   = Id
+opeZero {n = S n} = Drop opeZero
+
+public export
+(.) : OPE m n -> OPE n p -> OPE m p
+p      . Id     = p
+Id     . q      = q
+p      . Drop q = Drop $ p . q
+Drop p . Keep q = Drop $ p . q
+Keep p . Keep q = Keep $ p . q
+
+public export
+toLTE : {m : Nat} -> OPE m n -> m `LTE` n
+toLTE Id       = reflexive
+toLTE (Drop p) = lteSuccRight $ toLTE p
+toLTE (Keep p) = LTESucc      $ toLTE p
+
+
+public export
+data LTE' : Nat -> Nat -> Type where
+  LTERefl  : (n : Nat) -> LTE' n n
+  LTESuccR : Lazy (LTE' m n) -> LTE' m (S n)
+
+public export
+lteZero' : {n : Nat} -> LTE' 0 n
+lteZero' {n = 0}   = LTERefl 0
+lteZero' {n = S n} = LTESuccR $ delay lteZero'
+
+public export
+lteSucc' : LTE' m n -> LTE' (S m) (S n)
+lteSucc' (LTERefl n)  = LTERefl (S n)
+lteSucc' (LTESuccR p) = LTESuccR $ delay $ lteSucc' p
+
+public export
+fromLTE : {n : Nat} -> LTE m n -> LTE' m n
+fromLTE LTEZero     = lteZero'
+fromLTE (LTESucc p) = lteSucc' $ fromLTE p
+
+
+public export
+dropInner' : LTE' m n -> OPE m n
+dropInner' (LTERefl  n) = Id
+dropInner' (LTESuccR p) = Drop $ dropInner' $ force p
+
+public export
+dropInner : {n : Nat} -> LTE m n -> OPE m n
+dropInner = dropInner' . fromLTE
+
+public export
+dropInnerN : (m : Nat) -> OPE n (m + n)
+dropInnerN 0     = Id
+dropInnerN (S m) = Drop $ dropInnerN m
+
+
+
+-- [todo] can this be done with fancy nats too?
+-- with bitmasks sure but that might not be worth the effort
+-- [the next day] it probably isn't
+
+-- public export
+-- data OPE' : Nat -> Nat -> Type where
+--   None : OPE' 0 0
+--   Drop : OPE' m n -> OPE' m (S n)
+--   Keep : OPE' m n -> OPE' (S m) (S n)
+-- %name OPE' q
+
+
+-- public export %inline
+-- drop' : Integer -> Integer
+-- drop' n = n * 2
+
+-- public export %inline
+-- keep' : Integer -> Integer
+-- keep' n = 1 + 2 * n
+
+-- public export
+-- data IsOPE : Integer -> (OPE' m n) -> Type where
+--   IsNone : 0 `IsOPE` None
+--   IsDrop : (0 _ : m `IsOPE` q) -> drop' m `IsOPE` Drop q
+--   IsKeep : (0 _ : m `IsOPE` q) -> keep' m `IsOPE` Keep q
+-- %name IsOPE p
+
+
+-- public export
+-- record OPE m n where
+--   constructor MkOPE
+--   value  : Integer
+--   0 spec : OPE' m n
+--   0 prf  : value `IsOPE` spec
+--   0 pos  : So (value >= 0)
+
+
+-- private
+-- 0 idrisPleaseLearnAboutIntegers : {x, y : Integer} -> x = y
+-- idrisPleaseLearnAboutIntegers {x, y} = believe_me $ Refl {x}
+
+-- private
+-- 0 natIntPlus : (m, n : Nat) ->
+--                natToInteger (m + n) = natToInteger m + natToInteger n
+-- natIntPlus m n = idrisPleaseLearnAboutIntegers
+
+-- private
+-- 0 shiftTwice : (x : Integer) -> (m, n : Nat) ->
+--                x `shiftL` (m + n) = (x `shiftL` m) `shiftL` n
+-- shiftTwice x m n = idrisPleaseLearnAboutIntegers
+
+-- private
+-- 0 shift1 : (x : Integer) -> (x `shiftL` 1) = 2 * x
+-- shift1 x = idrisPleaseLearnAboutIntegers
+
+-- private
+-- 0 intPlusComm : (x, y : Integer) -> (x + y) = (y + x)
+-- intPlusComm x y = idrisPleaseLearnAboutIntegers
+
+-- private
+-- 0 intTimes2Minus1 : (x : Integer) -> 2 * x - 1 = 2 * (x - 1) + 1
+-- intTimes2Minus1 x = idrisPleaseLearnAboutIntegers
+
+-- private
+-- 0 intPosShift : So (x > 0) -> So (x `shiftL` i > 0)
+-- intPosShift p = believe_me Oh
+
+-- private
+-- 0 intNonnegDec : {x : Integer} -> So (x > 0) -> So (x - 1 >= 0)
+-- intNonnegDec p = believe_me Oh
+
+
+-- private
+-- 0 shiftSucc : (x : Integer) -> (n : Nat) ->
+--               x `shiftL` S n = 2 * (x `shiftL` n)
+-- shiftSucc x n = Calc $
+--   |~  x `shiftL` S n
+--   ~~  x `shiftL` (n + 1)
+--         ...(cong (x `shiftL`) $ sym $ plusCommutative {})
+--   ~~  (x `shiftL` n) `shiftL` 1
+--         ...(shiftTwice {})
+--   ~~  2 * (x `shiftL` n)
+--         ...(shift1 {})
+
+
+-- private
+-- opeIdVal : (n : Nat) -> Integer
+-- opeIdVal n = (1 `shiftL` n) - 1
+
+-- private
+-- 0 opeIdValSpec : (n : Nat) -> Integer
+-- opeIdValSpec 0     = 0
+-- opeIdValSpec (S n) = keep' $ opeIdValSpec n
+
+-- private
+-- 0 opeIdValOk :  (n : Nat) -> opeIdVal n = opeIdValSpec n
+-- opeIdValOk 0     = Refl
+-- opeIdValOk (S n) = Calc $
+--   |~  (1 `shiftL` S n) - 1
+--   ~~  2 * (1 `shiftL` n) - 1      ...(cong (\x => x - 1) $ shiftSucc {})
+--   ~~  2 * (1 `shiftL` n - 1) + 1  ...(intTimes2Minus1 {})
+--   ~~  1 + 2 * (1 `shiftL` n - 1)  ...(intPlusComm {})
+--   ~~  1 + 2 * opeIdValSpec n      ...(cong (\x => 1 + 2 * x) $ opeIdValOk {})
+
+-- private
+-- 0 opeIdSpec : (n : Nat) -> OPE' n n
+-- opeIdSpec 0     = None
+-- opeIdSpec (S n) = Keep $ opeIdSpec n
+
+-- private
+-- 0 opeIdProof' : (n : Nat) -> opeIdValSpec n `IsOPE` opeIdSpec n
+-- opeIdProof' 0     = IsNone
+-- opeIdProof' (S n) = IsKeep (opeIdProof' n)
+
+-- private
+-- 0 opeIdProof : (n : Nat) -> opeIdVal n `IsOPE` opeIdSpec n
+-- opeIdProof n = rewrite opeIdValOk n in opeIdProof' n
+
+-- export
+-- opeId : {n : Nat} -> OPE n n
+-- opeId {n} = MkOPE {prf = opeIdProof n, pos = intNonnegDec $ intPosShift Oh, _}