OPE & scope stuff
This commit is contained in:
parent
8c05957f60
commit
c8187c0801
3 changed files with 370 additions and 169 deletions
|
|
@ -55,3 +55,47 @@ parameters {base : Nat} {auto 0 _ : base `GTE` 2} (chars : Vect base Char)
|
||||||
export
|
export
|
||||||
showHex : Nat -> String
|
showHex : Nat -> String
|
||||||
showHex = showAtBase $ fromList $ unpack "0123456789ABCDEF"
|
showHex = showAtBase $ fromList $ unpack "0123456789ABCDEF"
|
||||||
|
|
||||||
|
|
||||||
|
n2i = natToInteger
|
||||||
|
i2n = fromInteger {ty = Nat}
|
||||||
|
|
||||||
|
private partial %inline
|
||||||
|
divNatViaInteger : (m, n : Nat) -> Nat
|
||||||
|
divNatViaInteger m n = i2n $ n2i m `div` n2i n
|
||||||
|
%transform "divNat" divNat = divNatViaInteger
|
||||||
|
|
||||||
|
private %inline
|
||||||
|
divNatViaIntegerNZ : (m, n : Nat) -> (0 _ : NonZero n) -> Nat
|
||||||
|
divNatViaIntegerNZ m n _ = assert_total divNatViaInteger m n
|
||||||
|
%transform "divNat" divNatNZ = divNatViaIntegerNZ
|
||||||
|
|
||||||
|
private partial %inline
|
||||||
|
modNatViaInteger : (m, n : Nat) -> Nat
|
||||||
|
modNatViaInteger m n = i2n $ n2i m `mod` n2i n
|
||||||
|
%transform "modNat" modNat = modNatViaInteger
|
||||||
|
|
||||||
|
private %inline
|
||||||
|
modNatViaIntegerNZ : (m, n : Nat) -> (0 _ : NonZero n) -> Nat
|
||||||
|
modNatViaIntegerNZ m n _ = assert_total modNatViaInteger m n
|
||||||
|
%transform "modNat" modNatNZ = modNatViaIntegerNZ
|
||||||
|
|
||||||
|
|
||||||
|
public export
|
||||||
|
data ViewLsb : Nat -> Type where
|
||||||
|
Lsb0 : (n : Nat) -> ViewLsb (2 * n)
|
||||||
|
Lsb1 : (n : Nat) -> ViewLsb (S (2 * n))
|
||||||
|
|
||||||
|
private
|
||||||
|
viewLsb' : (m, d : Nat) -> (0 _ : m `LT` 2) -> ViewLsb (m + 2 * d)
|
||||||
|
viewLsb' 0 d p = Lsb0 d
|
||||||
|
viewLsb' 1 d p = Lsb1 d
|
||||||
|
viewLsb' (S (S _)) _ (LTESucc p) = void $ absurd p
|
||||||
|
|
||||||
|
export
|
||||||
|
viewLsb : (n : Nat) -> ViewLsb n
|
||||||
|
viewLsb n =
|
||||||
|
let nz = the (NonZero 2) %search in
|
||||||
|
rewrite DivisionTheorem n 2 nz nz in
|
||||||
|
rewrite multCommutative (divNatNZ n 2 nz) 2 in
|
||||||
|
viewLsb' (modNatNZ n 2 nz) (divNatNZ n 2 nz) (boundModNatNZ n 2 nz)
|
||||||
|
|
|
||||||
401
lib/Quox/OPE.idr
401
lib/Quox/OPE.idr
|
|
@ -3,194 +3,257 @@
|
||||||
module Quox.OPE
|
module Quox.OPE
|
||||||
|
|
||||||
import Quox.NatExtra
|
import Quox.NatExtra
|
||||||
|
import public Data.DPair
|
||||||
import Data.Nat
|
import public Data.SnocList
|
||||||
|
import public Data.SnocList.Elem
|
||||||
|
|
||||||
%default total
|
%default total
|
||||||
|
|
||||||
|
LTE_n = Nat.LTE
|
||||||
public export
|
%hide Nat.LTE
|
||||||
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
|
public export
|
||||||
dropInner' : LTE' m n -> OPE m n
|
Scope : Type -> Type
|
||||||
dropInner' LTERefl = Id
|
Scope = SnocList
|
||||||
dropInner' (LTESuccR p) = Drop $ dropInner' $ force p
|
|
||||||
|
|
||||||
public export
|
public export
|
||||||
dropInner : {n : Nat} -> LTE m n -> OPE m n
|
data LTE : Scope a -> Scope a -> Type where
|
||||||
dropInner = dropInner' . fromLte
|
End : [<] `LTE` [<]
|
||||||
|
Keep : xs `LTE` ys -> xs :< z `LTE` ys :< z
|
||||||
|
Drop : xs `LTE` ys -> xs `LTE` ys :< z
|
||||||
|
%name LTE p, q
|
||||||
|
|
||||||
public export
|
-- [todo] bitmask representation???
|
||||||
dropInnerN : (m : Nat) -> OPE n (m + n)
|
|
||||||
dropInnerN 0 = Id
|
|
||||||
dropInnerN (S m) = Drop $ dropInnerN m
|
export
|
||||||
|
dropLast : (xs :< x) `LTE` ys -> xs `LTE` ys
|
||||||
|
dropLast (Keep p) = Drop p
|
||||||
|
dropLast (Drop p) = Drop $ dropLast p
|
||||||
|
|
||||||
|
export
|
||||||
|
Uninhabited (xs :< x `LTE` [<]) where uninhabited _ impossible
|
||||||
|
|
||||||
|
export
|
||||||
|
Uninhabited (xs :< x `LTE` xs) where
|
||||||
|
uninhabited (Keep p) = uninhabited p
|
||||||
|
uninhabited (Drop p) = uninhabited $ dropLast p
|
||||||
|
|
||||||
|
|
||||||
|
export
|
||||||
|
lteLen : xs `LTE` ys -> length xs `LTE_n` length ys
|
||||||
|
lteLen End = LTEZero
|
||||||
|
lteLen (Keep p) = LTESucc $ lteLen p
|
||||||
|
lteLen (Drop p) = lteSuccRight $ lteLen p
|
||||||
|
|
||||||
|
export
|
||||||
|
lteNilRight : xs `LTE` [<] -> xs = [<]
|
||||||
|
lteNilRight End = Refl
|
||||||
|
|
||||||
|
|
||||||
public export
|
public export
|
||||||
interface Tighten t where
|
data Length : Scope a -> Type where
|
||||||
tighten : Alternative f => OPE m n -> t n -> f (t m)
|
Z : Length [<]
|
||||||
|
S : (s : Length xs) -> Length (xs :< x)
|
||||||
|
%name Length s
|
||||||
|
%builtin Natural Length
|
||||||
|
|
||||||
parameters {auto _ : Tighten t} {auto _ : Alternative f}
|
export %hint
|
||||||
|
lengthLeft : xs `LTE` ys -> Length xs
|
||||||
|
lengthLeft End = Z
|
||||||
|
lengthLeft (Keep p) = S (lengthLeft p)
|
||||||
|
lengthLeft (Drop p) = lengthLeft p
|
||||||
|
|
||||||
|
export %hint
|
||||||
|
lengthRight : xs `LTE` ys -> Length ys
|
||||||
|
lengthRight End = Z
|
||||||
|
lengthRight (Keep p) = S (lengthRight p)
|
||||||
|
lengthRight (Drop p) = S (lengthRight p)
|
||||||
|
|
||||||
|
|
||||||
|
export
|
||||||
|
id : Length xs => xs `LTE` xs
|
||||||
|
id @{Z} = End
|
||||||
|
id @{S s} = Keep id
|
||||||
|
|
||||||
|
export
|
||||||
|
zero : Length xs => [<] `LTE` xs
|
||||||
|
zero @{Z} = End
|
||||||
|
zero @{S s} = Drop zero
|
||||||
|
|
||||||
|
export
|
||||||
|
single : Length xs => x `Elem` xs -> [< x] `LTE` xs
|
||||||
|
single @{S _} Here = Keep zero
|
||||||
|
single @{S _} (There p) = Drop $ single p
|
||||||
|
|
||||||
|
|
||||||
|
export
|
||||||
|
(.) : ys `LTE` zs -> xs `LTE` ys -> xs `LTE` zs
|
||||||
|
End . End = End
|
||||||
|
Keep p . Keep q = Keep (p . q)
|
||||||
|
Keep p . Drop q = Drop (p . q)
|
||||||
|
Drop p . q = Drop (p . q)
|
||||||
|
|
||||||
|
export
|
||||||
|
(++) : xs1 `LTE` ys1 -> xs2 `LTE` ys2 -> (xs1 ++ xs2) `LTE` (ys1 ++ ys2)
|
||||||
|
p ++ End = p
|
||||||
|
p ++ Keep q = Keep (p ++ q)
|
||||||
|
p ++ Drop q = Drop (p ++ q)
|
||||||
|
|
||||||
|
|
||||||
|
public export
|
||||||
|
record Split {a : Type} (xs, ys, zs : Scope a) (p : xs `LTE` ys ++ zs) where
|
||||||
|
constructor MkSplit
|
||||||
|
{0 leftSub, rightSub : Scope a}
|
||||||
|
leftThin : leftSub `LTE` ys
|
||||||
|
rightThin : rightSub `LTE` zs
|
||||||
|
0 eqScope : xs = leftSub ++ rightSub
|
||||||
|
0 eqThin : p ~=~ leftThin ++ rightThin
|
||||||
|
|
||||||
|
export
|
||||||
|
split : (zs : Scope a) -> (p : xs `LTE` ys ++ zs) -> Split xs ys zs p
|
||||||
|
split [<] p = MkSplit p zero Refl Refl
|
||||||
|
split (zs :< z) (Keep p) with (split zs p)
|
||||||
|
split (zs :< z) (Keep (l ++ r)) | MkSplit l r Refl Refl =
|
||||||
|
MkSplit l (Keep r) Refl Refl
|
||||||
|
split (zs :< z) (Drop p) {xs} with (split zs p)
|
||||||
|
split (zs :< z) (Drop (l ++ r)) {xs = _} | MkSplit l r Refl Refl =
|
||||||
|
MkSplit l (Drop r) Refl Refl
|
||||||
|
|
||||||
|
|
||||||
|
public export
|
||||||
|
data Comp : ys `LTE` zs -> xs `LTE` ys -> xs `LTE` zs -> Type where
|
||||||
|
CEE : Comp End End End
|
||||||
|
CKK : Comp p q pq -> Comp (Keep p) (Keep q) (Keep pq)
|
||||||
|
CKD : Comp p q pq -> Comp (Keep p) (Drop q) (Drop pq)
|
||||||
|
CD0 : Comp p q pq -> Comp (Drop p) q (Drop pq)
|
||||||
|
|
||||||
|
export
|
||||||
|
comp : (p : ys `LTE` zs) -> (q : xs `LTE` ys) -> Comp p q (p . q)
|
||||||
|
comp End End = CEE
|
||||||
|
comp (Keep p) (Keep q) = CKK (comp p q)
|
||||||
|
comp (Keep p) (Drop q) = CKD (comp p q)
|
||||||
|
comp (Drop p) q = CD0 (comp p q)
|
||||||
|
|
||||||
|
export
|
||||||
|
0 compOk : Comp p q r -> r = (p . q)
|
||||||
|
compOk CEE = Refl
|
||||||
|
compOk (CKK z) = cong Keep $ compOk z
|
||||||
|
compOk (CKD z) = cong Drop $ compOk z
|
||||||
|
compOk (CD0 z) = cong Drop $ compOk z
|
||||||
|
|
||||||
|
export
|
||||||
|
compZero : (sx : Length xs) => (sy : Length ys) =>
|
||||||
|
(p : xs `LTE` ys) -> Comp p (OPE.zero @{sx}) (OPE.zero @{sy})
|
||||||
|
compZero {sx = Z, sy = Z} End = CEE
|
||||||
|
compZero {sx = S _, sy = S _} (Keep p) = CKD (compZero p)
|
||||||
|
compZero {sy = S _} (Drop p) = CD0 (compZero p)
|
||||||
|
|
||||||
|
export
|
||||||
|
compIdLeft : (sy : Length ys) =>
|
||||||
|
(p : xs `LTE` ys) -> Comp (OPE.id @{sy}) p p
|
||||||
|
compIdLeft {sy = Z} End = CEE
|
||||||
|
compIdLeft {sy = S _} (Keep p) = CKK (compIdLeft p)
|
||||||
|
compIdLeft {sy = S _} (Drop p) = CKD (compIdLeft p)
|
||||||
|
|
||||||
|
export
|
||||||
|
compIdRight : (sx : Length xs) =>
|
||||||
|
(p : xs `LTE` ys) -> Comp p (OPE.id @{sx}) p
|
||||||
|
compIdRight {sx = Z} End = CEE
|
||||||
|
compIdRight {sx = S _} (Keep p) = CKK (compIdRight p)
|
||||||
|
compIdRight (Drop p) = CD0 (compIdRight p)
|
||||||
|
|
||||||
|
|
||||||
|
private
|
||||||
|
0 compExample :
|
||||||
|
Comp {zs = [< a, b, c, d, e]}
|
||||||
|
(Keep $ Drop $ Keep $ Drop $ Keep End)
|
||||||
|
(Keep $ Drop $ Keep End)
|
||||||
|
(Keep $ Drop $ Drop $ Drop $ Keep End)
|
||||||
|
compExample = %search
|
||||||
|
|
||||||
|
|
||||||
|
export
|
||||||
|
0 compAssoc : (p : ys `LTE` zs) -> (q : xs `LTE` ys) -> (r : ws `LTE` xs) ->
|
||||||
|
p . (q . r) = (p . q) . r
|
||||||
|
compAssoc End End End = Refl
|
||||||
|
compAssoc (Keep p) (Keep q) (Keep r) = cong Keep $ compAssoc p q r
|
||||||
|
compAssoc (Keep p) (Keep q) (Drop r) = cong Drop $ compAssoc p q r
|
||||||
|
compAssoc (Keep p) (Drop q) r = cong Drop $ compAssoc p q r
|
||||||
|
compAssoc (Drop p) q r = cong Drop $ compAssoc p q r
|
||||||
|
compAssoc End (Drop _) _ impossible
|
||||||
|
|
||||||
|
|
||||||
|
public export
|
||||||
|
Scoped : Type -> Type
|
||||||
|
Scoped a = Scope a -> Type
|
||||||
|
|
||||||
|
public export
|
||||||
|
Subscope : Scope a -> Type
|
||||||
|
Subscope xs = Exists (`LTE` xs)
|
||||||
|
|
||||||
|
public export
|
||||||
|
SubMap : {xs, ys : Scope a} -> xs `LTE` zs -> ys `LTE` zs -> Type
|
||||||
|
SubMap p q = DPair (xs `LTE` ys) (\r => Comp q r p)
|
||||||
|
|
||||||
|
parameters (p : xs `LTE` ys)
|
||||||
export
|
export
|
||||||
tightenInner : {n : Nat} -> m `LTE` n -> t n -> f (t m)
|
subId : SubMap p p
|
||||||
tightenInner = tighten . dropInner
|
subId = (id ** compIdRight p)
|
||||||
|
|
||||||
export
|
export
|
||||||
tightenN : (m : Nat) -> t (m + n) -> f (t n)
|
subZero : SubMap OPE.zero p
|
||||||
tightenN m = tighten $ dropInnerN m
|
subZero = (zero ** compZero p)
|
||||||
|
|
||||||
export
|
|
||||||
tighten1 : t (S n) -> f (t n)
|
public export
|
||||||
tighten1 = tightenN 1
|
data All : (a -> Type) -> Scoped a where
|
||||||
|
Lin : All p [<]
|
||||||
|
(:<) : All p xs -> p x -> All p (xs :< x)
|
||||||
|
%name OPE.All ps, qs
|
||||||
|
|
||||||
|
export
|
||||||
|
mapAll : (forall x. p x -> q x) -> All p xs -> All q xs
|
||||||
|
mapAll f [<] = [<]
|
||||||
|
mapAll f (x :< y) = mapAll f x :< f y
|
||||||
|
|
||||||
|
export
|
||||||
|
subAll : xs `LTE` ys -> All p ys -> All p xs
|
||||||
|
subAll End [<] = [<]
|
||||||
|
subAll (Keep q) (ps :< x) = subAll q ps :< x
|
||||||
|
subAll (Drop q) (ps :< x) = subAll q ps
|
||||||
|
|
||||||
|
|
||||||
|
public export
|
||||||
|
data Cover_ : (overlap : Bool) -> xs `LTE` zs -> ys `LTE` zs -> Type where
|
||||||
|
CE : Cover_ ov End End
|
||||||
|
CL : Cover_ ov p q -> Cover_ ov (Keep p) (Drop q)
|
||||||
|
CR : Cover_ ov p q -> Cover_ ov (Drop p) (Keep q)
|
||||||
|
C2 : Cover_ ov p q -> Cover_ True (Keep p) (Keep q)
|
||||||
|
|
||||||
|
public export
|
||||||
|
Cover : xs `LTE` zs -> ys `LTE` zs -> Type
|
||||||
|
Cover = Cover_ True
|
||||||
|
|
||||||
|
public export
|
||||||
|
Partition : xs `LTE` zs -> ys `LTE` zs -> Type
|
||||||
|
Partition = Cover_ False
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
-- [todo] can this be done with fancy nats too?
|
public export
|
||||||
-- with bitmasks sure but that might not be worth the effort
|
data LTEMaskView : xs `LTE` ys -> Nat -> Type where
|
||||||
-- [the next day] it probably isn't
|
END : LTEMaskView End 0
|
||||||
|
KEEP : (0 _ : LTEMaskView p n) -> LTEMaskView (Keep p) (S (2 * n))
|
||||||
|
DROP : (0 _ : LTEMaskView p n) -> LTEMaskView (Drop p) (2 * n)
|
||||||
|
|
||||||
-- public export
|
record LTEMask {a : Type} (xs, ys : Scope a) where
|
||||||
-- data OPE' : Nat -> Nat -> Type where
|
constructor LTEM
|
||||||
-- None : OPE' 0 0
|
mask : Nat
|
||||||
-- Drop : OPE' m n -> OPE' m (S n)
|
0 lte : xs `LTE` ys
|
||||||
-- Keep : OPE' m n -> OPE' (S m) (S n)
|
0 view0 : LTEMaskView lte mask
|
||||||
-- %name OPE' q
|
|
||||||
|
|
||||||
|
export
|
||||||
-- public export %inline
|
view : (sx : Length xs) => (sy : Length ys) =>
|
||||||
-- drop' : Integer -> Integer
|
(m : LTEMask xs ys) -> LTEMaskView m.lte m.mask
|
||||||
-- 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, _}
|
|
||||||
|
|
|
||||||
94
lib/Quox/Scope.idr
Normal file
94
lib/Quox/Scope.idr
Normal file
|
|
@ -0,0 +1,94 @@
|
||||||
|
module Quox.Scope
|
||||||
|
|
||||||
|
import public Quox.OPE
|
||||||
|
|
||||||
|
|
||||||
|
public export
|
||||||
|
record Sub {a : Type} (t : Scoped a) (xs : Scope a) where
|
||||||
|
constructor Su
|
||||||
|
{0 support : Scope a}
|
||||||
|
term : t support
|
||||||
|
thin : support `LTE` xs
|
||||||
|
|
||||||
|
public export
|
||||||
|
CoverS : Sub s xs -> Sub t xs -> Type
|
||||||
|
CoverS ss tt = Cover ss.thin tt.thin
|
||||||
|
|
||||||
|
export %inline
|
||||||
|
inj : Length xs => t xs -> Sub t xs
|
||||||
|
inj x = Su x id
|
||||||
|
|
||||||
|
export %inline
|
||||||
|
flat : Sub (Sub t) xs -> Sub t xs
|
||||||
|
flat (Su (Su x q) p) = Su x (p . q)
|
||||||
|
|
||||||
|
export %inline
|
||||||
|
thinSub : xs `LTE` ys -> Sub t xs -> Sub t ys
|
||||||
|
thinSub p x = flat $ Su x p
|
||||||
|
|
||||||
|
export %inline
|
||||||
|
map : (forall x. s x -> t x) -> Sub s x -> Sub t x
|
||||||
|
map f = {term $= f}
|
||||||
|
|
||||||
|
public export
|
||||||
|
data Unit : Scoped a where
|
||||||
|
Nil : Unit [<]
|
||||||
|
|
||||||
|
export %inline
|
||||||
|
unit : Length xs => Sub Unit xs
|
||||||
|
unit = Su [] zero
|
||||||
|
|
||||||
|
public export
|
||||||
|
record Coprod {a : Type} {xs, ys, zs : Scope a}
|
||||||
|
(p : xs `LTE` zs) (q : ys `LTE` zs) where
|
||||||
|
constructor Cop
|
||||||
|
{0 scope : Scope a}
|
||||||
|
{thin : scope `LTE` zs}
|
||||||
|
{thinP : xs `LTE` scope}
|
||||||
|
{thinQ : ys `LTE` scope}
|
||||||
|
compP : Comp thin thinP p
|
||||||
|
compQ : Comp thin thinQ q
|
||||||
|
0 cover : Cover thinP thinQ
|
||||||
|
|
||||||
|
export
|
||||||
|
coprod : (p : xs `LTE` zs) -> (q : ys `LTE` zs) -> Coprod p q
|
||||||
|
coprod End End = %search
|
||||||
|
coprod (Keep p) (Keep q) = let Cop {} = coprod p q in %search
|
||||||
|
coprod (Keep p) (Drop q) = let Cop {} = coprod p q in %search
|
||||||
|
coprod (Drop p) (Keep q) = let Cop {} = coprod p q in %search
|
||||||
|
coprod (Drop p) (Drop q) =
|
||||||
|
-- idk why this one is harder to solve
|
||||||
|
let Cop compP compQ cover = coprod p q in
|
||||||
|
Cop (CD0 compP) (CD0 compQ) cover
|
||||||
|
|
||||||
|
public export
|
||||||
|
record Pair {a : Type} (s, t : Scoped a) (zs : Scope a) where
|
||||||
|
constructor MkPair
|
||||||
|
fst : Sub s zs
|
||||||
|
snd : Sub t zs
|
||||||
|
0 cover : CoverS fst snd
|
||||||
|
|
||||||
|
export
|
||||||
|
pair : Sub s xs -> Sub t xs -> Sub (Pair s t) xs
|
||||||
|
pair (Su x p) (Su y q) =
|
||||||
|
let c = coprod p q in
|
||||||
|
Su (MkPair (Su x c.thinP) (Su y c.thinQ) c.cover) c.thin
|
||||||
|
|
||||||
|
|
||||||
|
public export
|
||||||
|
data Var : a -> Scope a -> Type where
|
||||||
|
Only : Var x [< x]
|
||||||
|
|
||||||
|
export %inline
|
||||||
|
var : (0 x : a) -> [< x] `LTE` xs => Sub (Var x) xs
|
||||||
|
var x @{p} = Su Only p
|
||||||
|
|
||||||
|
|
||||||
|
infix 0 \\\, \\
|
||||||
|
public export
|
||||||
|
data Bind : (t : Scoped a) -> (new, old : Scope a) -> Type where
|
||||||
|
(\\\) : new' `LTE` new -> t (old ++ new') -> Bind t new old
|
||||||
|
|
||||||
|
(\\) : (new : Scope a) -> Sub t (old ++ new) -> Sub (Bind t new) old
|
||||||
|
vs \\ Su term p with (split vs p)
|
||||||
|
vs \\ Su term (l ++ r) | MkSplit l r Refl Refl = Su (r \\\ term) l
|
||||||
Loading…
Reference in a new issue