split and extend Quox.Thin
This commit is contained in:
parent
a7673f901f
commit
92870fe716
13 changed files with 893 additions and 388 deletions
|
|
@ -1,388 +1,13 @@
|
|||
||| thinnings, covers, partitions, etc,
|
||||
||| for co-de Bruijn representation [@egtbs]
|
||||
module Quox.Thin
|
||||
|
||||
import Quox.NatExtra
|
||||
import Data.Nat.Views
|
||||
import Data.Singleton
|
||||
import Data.DPair
|
||||
import Syntax.PreorderReasoning
|
||||
|
||||
%default total
|
||||
|
||||
|
||||
||| "order preserving embeddings", for recording a correspondence between a
|
||||
||| smaller scope and part of a larger one. the third argument is a bitmask
|
||||
||| representing this OPE, unique for a given `n`.
|
||||
public export
|
||||
data OPE : (m, n, mask : Nat) -> Type where
|
||||
[search m n]
|
||||
Stop : OPE 0 0 0
|
||||
Drop : OPE m n mask -> mask' = mask + mask -> OPE m (S n) mask'
|
||||
Keep : OPE m n mask -> mask' = (S (mask + mask)) -> OPE (S m) (S n) mask'
|
||||
%name OPE ope
|
||||
|
||||
|
||||
||| everything selected
|
||||
public export
|
||||
id : {m : Nat} -> Subset Nat (OPE m m)
|
||||
id {m = 0} = Element _ Stop
|
||||
id {m = S m} = Element _ $ Keep id.snd Refl
|
||||
|
||||
||| nothing selected
|
||||
public export
|
||||
zero : {m : Nat} -> OPE 0 m 0
|
||||
zero {m = 0} = Stop
|
||||
zero {m = S m} = Drop zero Refl
|
||||
|
||||
|
||||
infix 6 `Eqv`
|
||||
|
||||
public export
|
||||
data Eqv : OPE m1 n1 mask1 -> OPE m2 n2 mask2 -> Type where
|
||||
EqvStop : Eqv Stop Stop
|
||||
EqvDrop : {0 p : OPE m1 n1 mask1} ->
|
||||
{0 q : OPE m2 n2 mask2} ->
|
||||
Eqv p q -> Eqv (Drop p eq1) (Drop q eq2)
|
||||
EqvKeep : {0 p : OPE m1 n1 mask1} ->
|
||||
{0 q : OPE m2 n2 mask2} ->
|
||||
Eqv p q -> Eqv (Keep p eq1) (Keep q eq2)
|
||||
%name Eqv eqv
|
||||
|
||||
export
|
||||
Reflexive (OPE m n mask) Eqv where
|
||||
reflexive {x = Stop} = EqvStop
|
||||
reflexive {x = Drop {}} = EqvDrop reflexive
|
||||
reflexive {x = Keep {}} = EqvKeep reflexive
|
||||
|
||||
export
|
||||
symmetric : p `Eqv` q -> q `Eqv` p
|
||||
symmetric EqvStop = EqvStop
|
||||
symmetric (EqvDrop eqv) = EqvDrop $ symmetric eqv
|
||||
symmetric (EqvKeep eqv) = EqvKeep $ symmetric eqv
|
||||
|
||||
export
|
||||
transitive : p `Eqv` q -> q `Eqv` r -> p `Eqv` r
|
||||
transitive EqvStop EqvStop = EqvStop
|
||||
transitive (EqvDrop x) (EqvDrop y) = EqvDrop (transitive x y)
|
||||
transitive (EqvKeep x) (EqvKeep y) = EqvKeep (transitive x y)
|
||||
|
||||
export
|
||||
eqvIndices : {0 p : OPE m1 n1 mask1} -> {0 q : OPE m2 n2 mask2} ->
|
||||
p `Eqv` q -> (m1 = m2, n1 = n2, mask1 = mask2)
|
||||
eqvIndices EqvStop = (Refl, Refl, Refl)
|
||||
eqvIndices (EqvDrop eqv {eq1 = Refl, eq2 = Refl}) =
|
||||
let (Refl, Refl, Refl) = eqvIndices eqv in (Refl, Refl, Refl)
|
||||
eqvIndices (EqvKeep eqv {eq1 = Refl, eq2 = Refl}) =
|
||||
let (Refl, Refl, Refl) = eqvIndices eqv in (Refl, Refl, Refl)
|
||||
|
||||
export
|
||||
0 eqvMask : (p : OPE m1 n mask1) -> (q : OPE m2 n mask2) ->
|
||||
mask1 = mask2 -> p `Eqv` q
|
||||
eqvMask Stop Stop _ = EqvStop
|
||||
eqvMask (Drop ope1 Refl) (Drop {mask = mm2} ope2 eq2) Refl =
|
||||
EqvDrop $ eqvMask ope1 ope2 (doubleInj _ _ eq2)
|
||||
eqvMask (Drop ope1 Refl) (Keep ope2 eq2) Refl =
|
||||
void $ notEvenOdd _ _ eq2
|
||||
eqvMask (Keep ope1 eq1) (Keep ope2 eq2) Refl =
|
||||
EqvKeep $ eqvMask ope1 ope2 (doubleInj _ _ $ inj S $ trans (sym eq1) eq2)
|
||||
eqvMask (Keep ope1 eq1) (Drop ope2 eq2) Refl =
|
||||
void $ notEvenOdd _ _ $ trans (sym eq2) eq1
|
||||
|
||||
uip : (p, q : a = b) -> p = q
|
||||
uip Refl Refl = Refl
|
||||
|
||||
export
|
||||
0 eqvEq' : (p, q : OPE m n mask) -> p `Eqv` q -> p === q
|
||||
eqvEq' Stop Stop EqvStop = Refl
|
||||
eqvEq' (Drop p eq1) (Drop q eq2) (EqvDrop eqv)
|
||||
with (doubleInj _ _ $ trans (sym eq1) eq2)
|
||||
_ | Refl = cong2 Drop (eqvEq' p q eqv) (uip eq1 eq2)
|
||||
eqvEq' (Keep p eq1) (Keep q eq2) (EqvKeep eqv)
|
||||
with (doubleInj _ _ $ inj S $ trans (sym eq1) eq2)
|
||||
_ | Refl = cong2 Keep (eqvEq' p q eqv) (uip eq1 eq2)
|
||||
|
||||
|
||||
export
|
||||
0 eqvEq : (p : OPE m1 n1 mask1) -> (q : OPE m2 n2 mask2) ->
|
||||
p `Eqv` q -> p ~=~ q
|
||||
eqvEq p q eqv = let (Refl, Refl, Refl) = eqvIndices eqv in eqvEq' p q eqv
|
||||
|
||||
|
||||
public export
|
||||
data View : OPE m n mask -> Type where
|
||||
StopV : View Stop
|
||||
DropV : (mask : Nat) -> (0 ope : OPE m n mask) -> View (Drop ope Refl)
|
||||
KeepV : (mask : Nat) -> (0 ope : OPE m n mask) -> View (Keep ope Refl)
|
||||
%name Thin.View v
|
||||
|
||||
private
|
||||
0 stopEqs : OPE m 0 mask -> (m = 0, mask = 0)
|
||||
stopEqs Stop = (Refl, Refl)
|
||||
|
||||
private
|
||||
0 fromStop : (ope : OPE 0 0 0) -> ope = Stop
|
||||
fromStop Stop = Refl
|
||||
|
||||
private
|
||||
0 fromDrop : (ope : OPE m (S n) (k + k)) ->
|
||||
(inner : OPE m n k ** ope === Drop inner Refl)
|
||||
fromDrop (Drop ope eq) with (doubleInj _ _ eq)
|
||||
fromDrop (Drop ope Refl) | Refl = (ope ** Refl)
|
||||
fromDrop (Keep ope eq) = void $ notEvenOdd _ _ eq
|
||||
|
||||
private
|
||||
0 fromKeep : (ope : OPE (S m) (S n) (S (k + k))) ->
|
||||
(inner : OPE m n k ** ope === Keep inner Refl)
|
||||
fromKeep (Drop ope eq) = void $ notEvenOdd _ _ $ sym eq
|
||||
fromKeep (Keep ope eq) with (doubleInj _ _ $ inj S eq)
|
||||
fromKeep (Keep ope Refl) | Refl = (ope ** Refl)
|
||||
|
||||
private
|
||||
0 keepIsSucc : (ope : OPE m n (S (k + k))) -> IsSucc m
|
||||
keepIsSucc (Drop ope eq) = void $ notEvenOdd _ _ $ sym eq
|
||||
keepIsSucc (Keep ope _) = ItIsSucc
|
||||
|
||||
export
|
||||
view : {0 m : Nat} -> {n, mask : Nat} -> (0 ope : OPE m n mask) -> View ope
|
||||
view {n = 0} ope with 0 (fst $ stopEqs ope) | 0 (snd $ stopEqs ope)
|
||||
_ | Refl | Refl = rewrite fromStop ope in StopV
|
||||
view {n = S n} ope with (half mask)
|
||||
_ | HalfOdd mask' with 0 (keepIsSucc ope)
|
||||
_ | ItIsSucc with 0 (fromKeep ope)
|
||||
_ | (ope' ** eq) = rewrite eq in KeepV mask' ope'
|
||||
_ | HalfEven mask' with 0 (fromDrop ope)
|
||||
_ | (ope' ** eq) = rewrite eq in DropV mask' ope'
|
||||
|
||||
export
|
||||
appOpe : {0 m : Nat} -> (n : Nat) -> {mask : Nat} ->
|
||||
(0 ope : OPE m n mask) -> Singleton m
|
||||
appOpe n ope with (view ope)
|
||||
appOpe 0 Stop | StopV = Val 0
|
||||
appOpe (S n) (Drop ope' _) | DropV _ ope' = appOpe n ope'
|
||||
appOpe (S n) (Keep ope' _) | KeepV _ ope' = [|S $ appOpe n ope'|]
|
||||
|
||||
|
||||
||| inductive definition of OPE composition
|
||||
public export
|
||||
data Comp : (l : OPE n p mask1) -> (r : OPE m n mask2) ->
|
||||
(res : OPE m p mask3) -> Type where
|
||||
[search l r]
|
||||
StopZ : Comp Stop Stop Stop
|
||||
DropZ : Comp a b c -> Comp (Drop a Refl) b (Drop c Refl)
|
||||
KeepZ : Comp a b c -> Comp (Keep a Refl) (Keep b Refl) (Keep c Refl)
|
||||
KDZ : Comp a b c -> Comp (Keep a Refl) (Drop b Refl) (Drop c Refl)
|
||||
|
||||
public export
|
||||
record CompResult (ope1 : OPE n p mask1) (ope2 : OPE m n mask2) where
|
||||
constructor MkComp
|
||||
{resultMask : Nat}
|
||||
{0 result : OPE m p resultMask}
|
||||
0 comp : Comp ope1 ope2 result
|
||||
%name CompResult comp
|
||||
|
||||
||| compose two OPEs, if the middle scope size is already known at runtime
|
||||
export
|
||||
comp' : {n, p, mask1, mask2 : Nat} ->
|
||||
(0 ope1 : OPE n p mask1) -> (0 ope2 : OPE m n mask2) ->
|
||||
CompResult ope1 ope2
|
||||
comp' ope1 ope2 with (view ope1) | (view ope2)
|
||||
comp' Stop Stop | StopV | StopV =
|
||||
MkComp StopZ
|
||||
comp' (Drop ope1 Refl) ope2 | DropV _ ope1 | _ =
|
||||
MkComp $ DropZ (comp' ope1 ope2).comp
|
||||
comp' (Keep ope1 Refl) (Drop ope2 Refl) | KeepV _ ope1 | DropV _ ope2 =
|
||||
MkComp $ KDZ (comp' ope1 ope2).comp
|
||||
comp' (Keep ope1 Refl) (Keep ope2 Refl) | KeepV _ ope1 | KeepV _ ope2 =
|
||||
MkComp $ KeepZ (comp' ope1 ope2).comp
|
||||
|
||||
||| compose two OPEs, after recomputing the middle scope size using `appOpe`
|
||||
export
|
||||
comp : {p, mask1, mask2 : Nat} ->
|
||||
(0 ope1 : OPE n p mask1) -> (0 ope2 : OPE m n mask2) ->
|
||||
CompResult ope1 ope2
|
||||
comp ope1 ope2 = let Val n = appOpe p ope1 in comp' ope1 ope2
|
||||
|
||||
-- [todo] is there a quick way to compute the mask of comp?
|
||||
|
||||
|
||||
export
|
||||
app' : OPE m1 n1 mask1 -> OPE m2 n2 mask2 -> Exists (OPE (m1 + m2) (n1 + n2))
|
||||
app' Stop ope2 = Evidence _ ope2
|
||||
app' (Drop ope1 Refl) ope2 = Evidence _ $ Drop (app' ope1 ope2).snd Refl
|
||||
app' (Keep ope1 Refl) ope2 = Evidence _ $ Keep (app' ope1 ope2).snd Refl
|
||||
|
||||
export
|
||||
(++) : {n1, n2, mask1, mask2 : Nat} ->
|
||||
(0 ope1 : OPE m1 n1 mask1) -> (0 ope2 : OPE m2 n2 mask2) ->
|
||||
Subset Nat (OPE (m1 + m2) (n1 + n2))
|
||||
ope1 ++ ope2 with (view ope1)
|
||||
Stop ++ ope2 | StopV = Element _ ope2
|
||||
Drop ope1 Refl ++ ope2 | DropV mask ope1 =
|
||||
Element _ $ Drop (ope1 ++ ope2).snd Refl
|
||||
Keep ope1 Refl ++ ope2 | KeepV mask ope1 =
|
||||
Element _ $ Keep (ope1 ++ ope2).snd Refl
|
||||
|
||||
-- [todo] this mask is just (mask1 << n2) | mask2
|
||||
-- prove it and add %transform
|
||||
|
||||
|
||||
||| the tail of a non-empty OPE is its behaviour on all but the innermost slot
|
||||
public export
|
||||
data Tail : (full : OPE m1 (S n) mask1) -> (tail : OPE m2 n mask2) -> Type where
|
||||
[search full]
|
||||
DropT : Tail (Drop ope eq) ope
|
||||
KeepT : Tail (Keep ope eq) ope
|
||||
%name Tail tail
|
||||
|
||||
public export
|
||||
record TailRes (0 ope : OPE m (S n) mask) where
|
||||
constructor MkTail
|
||||
{0 scope : Nat}
|
||||
{tailMask : Nat}
|
||||
0 tail : OPE scope n tailMask
|
||||
0 isTail : Tail ope tail
|
||||
|
||||
export
|
||||
tail : {n, mask : Nat} -> (0 ope : OPE m (S n) mask) -> TailRes ope
|
||||
tail ope with (view ope)
|
||||
tail (Drop ope _) | DropV _ ope = MkTail ope DropT
|
||||
tail (Keep ope _) | KeepV _ ope = MkTail ope KeepT
|
||||
|
||||
|
||||
namespace OPEList
|
||||
||| a list of OPEs of a given outer scope size
|
||||
public export
|
||||
data OPEList : Nat -> Type where
|
||||
Nil : OPEList n
|
||||
(::) : OPE m n mask -> OPEList n -> OPEList n
|
||||
%name OPEList opes
|
||||
|
||||
namespace Tails -- 🦊
|
||||
||| `Tails opes tails` if each i'th element of `tails` is the tail of
|
||||
||| the i'th element of `opes`
|
||||
public export
|
||||
data Tails : (full : OPEList (S n)) -> (tails : OPEList n) -> Type where
|
||||
[search full]
|
||||
Nil : Tails [] []
|
||||
(::) : Tail ope tail -> Tails opes tails ->
|
||||
Tails (ope :: opes) (tail :: tails)
|
||||
|
||||
namespace Cover
|
||||
||| an OPE list is a cover if at least one of the OPEs has `Keep` as the head,
|
||||
||| and the tails are also a cover
|
||||
|||
|
||||
||| in @egtbs it is a binary relation which is fine for ×ᵣ but i don't want to
|
||||
||| write my AST in universe-of-syntaxes style. sorry
|
||||
public export data Cover : OPEList n -> Type
|
||||
|
||||
||| the "`Keep` in the head" condition of a cover
|
||||
public export data Cover1 : OPEList n -> Type
|
||||
|
||||
data Cover where
|
||||
Nil : Cover opes {n = 0}
|
||||
(::) : Cover1 opes -> Tails opes tails => Cover tails -> Cover opes
|
||||
%name Cover cov
|
||||
|
||||
data Cover1 where
|
||||
Here : Cover1 (Keep p eq :: opes)
|
||||
There : Cover1 opes -> Cover1 (ope :: opes)
|
||||
%name Cover1 cov1
|
||||
|
||||
|
||||
public export
|
||||
record Coprod (ope1 : OPE m1 n mask1) (ope2 : OPE m2 n mask2) where
|
||||
constructor MkCoprod
|
||||
{0 size : Nat}
|
||||
{sizeMask : Nat}
|
||||
{leftMask : Nat}
|
||||
{rightMask : Nat}
|
||||
{0 sub : OPE size n sizeMask}
|
||||
{0 left : OPE m1 size leftMask}
|
||||
{0 right : OPE m2 size rightMask}
|
||||
0 leftComp : Comp sub left ope1
|
||||
0 rightComp : Comp sub right ope2
|
||||
{auto 0 isCover : Cover [left, right]}
|
||||
%name Coprod cop
|
||||
|
||||
export
|
||||
coprod : {n, mask1, mask2 : Nat} ->
|
||||
(0 ope1 : OPE m1 n mask1) -> (0 ope2 : OPE m2 n mask2) ->
|
||||
Coprod ope1 ope2
|
||||
coprod ope1 ope2 with (view ope1) | (view ope2)
|
||||
coprod Stop Stop | StopV | StopV = MkCoprod StopZ StopZ
|
||||
coprod (Drop ope1 Refl) (Drop ope2 Refl) | DropV _ ope1 | DropV _ ope2 =
|
||||
let MkCoprod l r = coprod ope1 ope2 in MkCoprod (DropZ l) (DropZ r)
|
||||
coprod (Drop ope1 Refl) (Keep ope2 Refl) | DropV _ ope1 | KeepV _ ope2 =
|
||||
let MkCoprod l r = coprod ope1 ope2 in MkCoprod (KDZ l) (KeepZ r)
|
||||
coprod (Keep ope1 Refl) (Drop ope2 Refl) | KeepV _ ope1 | DropV _ ope2 =
|
||||
let MkCoprod l r = coprod ope1 ope2 in MkCoprod (KeepZ l) (KDZ r)
|
||||
coprod (Keep ope1 Refl) (Keep ope2 Refl) | KeepV _ ope1 | KeepV _ ope2 =
|
||||
let MkCoprod l r = coprod ope1 ope2 in MkCoprod (KeepZ l) (KeepZ r)
|
||||
|
||||
-- [todo] n-ary coprod
|
||||
|
||||
|
||||
public export
|
||||
record Chunks m n where
|
||||
constructor MkChunks
|
||||
{leftMask : Nat}
|
||||
{rightMask : Nat}
|
||||
0 left : OPE m (m + n) leftMask
|
||||
0 right : OPE n (m + n) rightMask
|
||||
{auto 0 isCover : Cover [left, right]}
|
||||
%name Chunks chunks
|
||||
|
||||
export
|
||||
chunks : (m, n : Nat) -> Chunks m n
|
||||
chunks 0 0 = MkChunks Stop Stop
|
||||
chunks 0 (S n) =
|
||||
let MkChunks l r = chunks 0 n in
|
||||
MkChunks (Drop l Refl) (Keep r Refl)
|
||||
chunks (S m) n =
|
||||
let MkChunks l r = chunks m n in
|
||||
MkChunks (Keep l Refl) (Drop r Refl)
|
||||
|
||||
-- [todo] the masks here are just ((2 << m) - 1) << n and (2 << n) - 1
|
||||
|
||||
|
||||
public export
|
||||
record SplitAt m n1 n2 (ope : OPE m (n1 + n2) mask) where
|
||||
constructor MkSplitAt
|
||||
{leftMask, rightMask : Nat}
|
||||
{0 leftScope, rightScope : Nat}
|
||||
0 left : OPE leftScope n1 leftMask
|
||||
0 right : OPE rightScope n2 rightMask
|
||||
0 scopePrf : m = leftScope + rightScope
|
||||
0 opePrf : ope `Eqv` (left `app'` right).snd
|
||||
%name SplitAt split
|
||||
|
||||
export
|
||||
splitAt : (n1 : Nat) -> {n2, mask : Nat} -> (0 ope : OPE m (n1 + n2) mask) ->
|
||||
SplitAt m n1 n2 ope
|
||||
splitAt 0 ope = MkSplitAt zero ope Refl reflexive
|
||||
splitAt (S n1) ope with (view ope)
|
||||
splitAt (S n1) (Drop ope Refl) | DropV _ ope with (splitAt n1 ope)
|
||||
_ | MkSplitAt left right scopePrf opePrf =
|
||||
MkSplitAt (Drop left Refl) right scopePrf (EqvDrop opePrf)
|
||||
splitAt (S n1) (Keep ope Refl) | KeepV _ ope with (splitAt n1 ope)
|
||||
_ | MkSplitAt left right scopePrf opePrf =
|
||||
MkSplitAt (Keep left Refl) right (cong S scopePrf) (EqvKeep opePrf)
|
||||
|
||||
|
||||
public export
|
||||
record Thinned f n where
|
||||
constructor Th
|
||||
{0 scope : Nat}
|
||||
{scopeMask : Nat}
|
||||
0 ope : OPE scope n scopeMask
|
||||
term : f scope
|
||||
%name Thinned s, t, u
|
||||
|
||||
export
|
||||
pure : {n : Nat} -> f n -> Thinned f n
|
||||
pure term = Th id.snd term
|
||||
|
||||
export
|
||||
join : {n : Nat} -> Thinned (Thinned f) n -> Thinned f n
|
||||
join (Th ope1 (Th ope2 term)) = Th (comp ope1 ope2).result term
|
||||
import public Quox.Thin.Base
|
||||
import public Quox.Thin.View
|
||||
import public Quox.Thin.Eqv
|
||||
import public Quox.Thin.Cons
|
||||
import public Quox.Thin.List
|
||||
import public Quox.Thin.Append
|
||||
import public Quox.Thin.Comp
|
||||
import public Quox.Thin.Cover
|
||||
import public Quox.Thin.Coprod
|
||||
import public Quox.Thin.Split
|
||||
import public Quox.Thin.Term
|
||||
|
|
|
|||
27
lib/Quox/Thin/Append.idr
Normal file
27
lib/Quox/Thin/Append.idr
Normal file
|
|
@ -0,0 +1,27 @@
|
|||
module Quox.Thin.Append
|
||||
|
||||
import public Quox.Thin.Base
|
||||
import public Quox.Thin.View
|
||||
import Data.DPair
|
||||
|
||||
%default total
|
||||
|
||||
public export
|
||||
app' : OPE m1 n1 mask1 -> OPE m2 n2 mask2 -> Exists (OPE (m1 + m2) (n1 + n2))
|
||||
app' Stop ope2 = Evidence _ ope2
|
||||
app' (Drop ope1 Refl) ope2 = Evidence _ $ Drop (app' ope1 ope2).snd Refl
|
||||
app' (Keep ope1 Refl) ope2 = Evidence _ $ Keep (app' ope1 ope2).snd Refl
|
||||
|
||||
public export
|
||||
(++) : {n1, n2, mask1, mask2 : Nat} ->
|
||||
(0 ope1 : OPE m1 n1 mask1) -> (0 ope2 : OPE m2 n2 mask2) ->
|
||||
Subset Nat (OPE (m1 + m2) (n1 + n2))
|
||||
ope1 ++ ope2 with %syntactic (view ope1)
|
||||
Stop ++ ope2 | StopV = Element _ ope2
|
||||
Drop ope1 Refl ++ ope2 | DropV mask ope1 =
|
||||
Element _ $ Drop (ope1 ++ ope2).snd Refl
|
||||
Keep ope1 Refl ++ ope2 | KeepV mask ope1 =
|
||||
Element _ $ Keep (ope1 ++ ope2).snd Refl
|
||||
|
||||
-- [todo] this mask is just (mask1 << n2) | mask2
|
||||
-- prove it and add %transform
|
||||
80
lib/Quox/Thin/Base.idr
Normal file
80
lib/Quox/Thin/Base.idr
Normal file
|
|
@ -0,0 +1,80 @@
|
|||
module Quox.Thin.Base
|
||||
|
||||
import Data.Fin
|
||||
import Data.DPair
|
||||
|
||||
%default total
|
||||
|
||||
||| "order preserving embeddings", for recording a correspondence between a
|
||||
||| smaller scope and part of a larger one. the third argument is a bitmask
|
||||
||| representing this OPE, unique for a given `n`.
|
||||
public export
|
||||
data OPE : (m, n, mask : Nat) -> Type where
|
||||
[search m n]
|
||||
Stop : OPE 0 0 0
|
||||
Drop : OPE m n mask -> mask' = mask + mask -> OPE m (S n) mask'
|
||||
Keep : OPE m n mask -> mask' = (S (mask + mask)) -> OPE (S m) (S n) mask'
|
||||
%name OPE ope
|
||||
|
||||
export
|
||||
Show (OPE m n mask) where
|
||||
showPrec d Stop = "Stop"
|
||||
showPrec d (Drop ope Refl) = showCon d "Drop" $ showArg ope ++ " Refl"
|
||||
showPrec d (Keep ope Refl) = showCon d "Keep" $ showArg ope ++ " Refl"
|
||||
|
||||
public export %inline
|
||||
drop : OPE m n mask -> OPE m (S n) (mask + mask)
|
||||
drop ope = Drop ope Refl
|
||||
|
||||
public export %inline
|
||||
keep : OPE m n mask -> OPE (S m) (S n) (S (mask + mask))
|
||||
keep ope = Keep ope Refl
|
||||
|
||||
|
||||
public export
|
||||
data IsStop : OPE m n mask -> Type where ItIsStop : IsStop Stop
|
||||
|
||||
public export
|
||||
data IsDrop : OPE m n mask -> Type where ItIsDrop : IsDrop (Drop ope eq)
|
||||
|
||||
public export
|
||||
data IsKeep : OPE m n mask -> Type where ItIsKeep : IsKeep (Keep ope eq)
|
||||
|
||||
|
||||
export
|
||||
0 zeroIsStop : (ope : OPE m 0 mask) -> IsStop ope
|
||||
zeroIsStop Stop = ItIsStop
|
||||
|
||||
|
||||
||| everything selected
|
||||
public export
|
||||
id : {m : Nat} -> Subset Nat (OPE m m)
|
||||
id {m = 0} = Element _ Stop
|
||||
id {m = S m} = Element _ $ Keep id.snd Refl
|
||||
|
||||
public export %inline
|
||||
0 id' : OPE m m Base.id.fst
|
||||
id' = id.snd
|
||||
|
||||
||| nothing selected
|
||||
public export
|
||||
zero : {m : Nat} -> OPE 0 m 0
|
||||
zero {m = 0} = Stop
|
||||
zero {m = S m} = Drop zero Refl
|
||||
|
||||
||| a single slot selected
|
||||
public export
|
||||
one : Fin n -> Subset Nat (OPE 1 n)
|
||||
one FZ = Element _ $ keep zero
|
||||
one (FS i) = Element _ $ drop (one i).snd
|
||||
|
||||
public export %inline
|
||||
0 one' : (i : Fin n) -> OPE 1 n (one i).fst
|
||||
one' i = (one i).snd
|
||||
|
||||
|
||||
public export
|
||||
record SomeOPE n where
|
||||
constructor MkOPE
|
||||
{mask : Nat}
|
||||
0 ope : OPE m n mask
|
||||
59
lib/Quox/Thin/Comp.idr
Normal file
59
lib/Quox/Thin/Comp.idr
Normal file
|
|
@ -0,0 +1,59 @@
|
|||
module Quox.Thin.Comp
|
||||
|
||||
import public Quox.Thin.Base
|
||||
import public Quox.Thin.View
|
||||
import Data.Singleton
|
||||
|
||||
%default total
|
||||
|
||||
||| inductive definition of OPE composition
|
||||
public export
|
||||
data Comp : (l : OPE n p mask1) -> (r : OPE m n mask2) ->
|
||||
(res : OPE m p mask3) -> Type where
|
||||
[search l r]
|
||||
StopZ : Comp Stop Stop Stop
|
||||
DropZ : Comp a b c -> Comp (Drop a Refl) b (Drop c Refl)
|
||||
KeepZ : Comp a b c -> Comp (Keep a Refl) (Keep b Refl) (Keep c Refl)
|
||||
KDZ : Comp a b c -> Comp (Keep a Refl) (Drop b Refl) (Drop c Refl)
|
||||
|
||||
public export
|
||||
record CompResult (ope1 : OPE n p mask1) (ope2 : OPE m n mask2) where
|
||||
constructor MkComp
|
||||
{mask : Nat}
|
||||
{0 ope : OPE m p mask}
|
||||
0 comp : Comp ope1 ope2 ope
|
||||
%name CompResult comp
|
||||
|
||||
||| compose two OPEs, if the middle scope size is already known at runtime
|
||||
export
|
||||
comp' : {n, p, mask1, mask2 : Nat} ->
|
||||
(0 ope1 : OPE n p mask1) -> (0 ope2 : OPE m n mask2) ->
|
||||
CompResult ope1 ope2
|
||||
comp' ope1 ope2 with %syntactic (view ope1) | (view ope2)
|
||||
comp' Stop Stop | StopV | StopV =
|
||||
MkComp StopZ
|
||||
comp' (Drop ope1 Refl) ope2 | DropV _ ope1 | _ =
|
||||
MkComp $ DropZ (comp' ope1 ope2).comp
|
||||
comp' (Keep ope1 Refl) (Drop ope2 Refl) | KeepV _ ope1 | DropV _ ope2 =
|
||||
MkComp $ KDZ (comp' ope1 ope2).comp
|
||||
comp' (Keep ope1 Refl) (Keep ope2 Refl) | KeepV _ ope1 | KeepV _ ope2 =
|
||||
MkComp $ KeepZ (comp' ope1 ope2).comp
|
||||
|
||||
||| compose two OPEs, after recomputing the middle scope size using `appOpe`
|
||||
export
|
||||
comp : {p, mask1, mask2 : Nat} ->
|
||||
(0 ope1 : OPE n p mask1) -> (0 ope2 : OPE m n mask2) ->
|
||||
CompResult ope1 ope2
|
||||
comp ope1 ope2 = let Val n = appOpe p ope1 in comp' ope1 ope2
|
||||
|
||||
-- [todo] is there a quick way to compute the mask of comp?
|
||||
|
||||
export
|
||||
0 (.) : (ope1 : OPE n p mask1) -> (ope2 : OPE m n mask2) ->
|
||||
OPE m p (comp ope1 ope2).mask
|
||||
ope1 . ope2 = (comp ope1 ope2).ope
|
||||
|
||||
-- export
|
||||
-- 0 compMask : (ope1 : OPE n p mask1) -> (ope2 : OPE m n mask2) ->
|
||||
-- (ope3 : OPE m p mask3) -> Comp ope1 ope2 ope3 ->
|
||||
-- mask3 = ?aaa
|
||||
74
lib/Quox/Thin/Cons.idr
Normal file
74
lib/Quox/Thin/Cons.idr
Normal file
|
|
@ -0,0 +1,74 @@
|
|||
module Quox.Thin.Cons
|
||||
|
||||
import public Quox.Thin.Base
|
||||
import Quox.Thin.Eqv
|
||||
import Quox.Thin.View
|
||||
import Data.DPair
|
||||
import Control.Relation
|
||||
|
||||
%default total
|
||||
|
||||
|
||||
public export
|
||||
data IsHead : (ope : OPE m (S n) mask) -> Bool -> Type where
|
||||
[search ope]
|
||||
DropH : IsHead (Drop ope eq) False
|
||||
KeepH : IsHead (Keep ope eq) True
|
||||
|
||||
public export
|
||||
data IsTail : (full : OPE m (S n) mask) -> OPE m' n mask' -> Type where
|
||||
[search full]
|
||||
DropT : IsTail (Drop ope eq) ope
|
||||
KeepT : IsTail (Keep ope eq) ope
|
||||
|
||||
public export
|
||||
record Uncons (ope : OPE m (S n) mask) where
|
||||
constructor MkUncons
|
||||
0 head : Bool
|
||||
{tailMask : Nat}
|
||||
0 tail : OPE scope n tailMask
|
||||
{auto isHead : IsHead ope head}
|
||||
{auto 0 isTail : IsTail ope tail}
|
||||
|
||||
public export
|
||||
uncons : {n, mask : Nat} -> (0 ope : OPE m (S n) mask) -> Uncons ope
|
||||
uncons ope with %syntactic (view ope)
|
||||
uncons (Drop ope Refl) | DropV _ ope = MkUncons False ope
|
||||
uncons (Keep ope Refl) | KeepV _ ope = MkUncons True ope
|
||||
|
||||
public export
|
||||
head : {n, mask : Nat} -> (0 ope : OPE m (S n) mask) -> Exists $ IsHead ope
|
||||
head ope = Evidence _ (uncons ope).isHead
|
||||
|
||||
public export
|
||||
record Tail (ope : OPE m (S n) mask) where
|
||||
constructor MkTail
|
||||
{tailMask : Nat}
|
||||
0 tail : OPE scope n tailMask
|
||||
{auto 0 isTail : IsTail ope tail}
|
||||
|
||||
public export
|
||||
tail : {n, mask : Nat} -> (0 ope : OPE m (S n) mask) -> Tail ope
|
||||
tail ope = let u = uncons ope in MkTail u.tail @{u.isTail}
|
||||
|
||||
|
||||
export
|
||||
cons : {mask : Nat} -> (head : Bool) -> (0 tail : OPE m n mask) ->
|
||||
Subset Nat (OPE (if head then S m else m) (S n))
|
||||
cons False tail = Element _ $ drop tail
|
||||
cons True tail = Element _ $ keep tail
|
||||
|
||||
export
|
||||
0 consEquiv' : (self : OPE m' (S n) mask') ->
|
||||
(head : Bool) -> (tail : OPE m n mask) ->
|
||||
IsHead self head -> IsTail self tail ->
|
||||
(cons head tail).snd `Eqv` self
|
||||
consEquiv' (Drop tail _) False tail DropH DropT = EqvDrop reflexive
|
||||
consEquiv' (Keep tail _) True tail KeepH KeepT = EqvKeep reflexive
|
||||
|
||||
export
|
||||
0 consEquiv : (full : OPE m' (S n) mask') ->
|
||||
(cons (uncons full).head (uncons full).tail).snd `Eqv` full
|
||||
consEquiv full with %syntactic (uncons full)
|
||||
_ | MkUncons head tail {isHead, isTail} =
|
||||
consEquiv' full head tail isHead isTail
|
||||
41
lib/Quox/Thin/Coprod.idr
Normal file
41
lib/Quox/Thin/Coprod.idr
Normal file
|
|
@ -0,0 +1,41 @@
|
|||
module Quox.Thin.Coprod
|
||||
|
||||
import public Quox.Thin.Base
|
||||
import public Quox.Thin.Comp
|
||||
import public Quox.Thin.View
|
||||
import public Quox.Thin.List
|
||||
import public Quox.Thin.Cover
|
||||
import Data.DPair
|
||||
|
||||
%default total
|
||||
|
||||
public export
|
||||
record Coprod2 (ope1 : OPE m1 n mask1) (ope2 : OPE m2 n mask2) where
|
||||
constructor MkCoprod2
|
||||
{sizeMask : Nat}
|
||||
{leftMask : Nat}
|
||||
{rightMask : Nat}
|
||||
{0 sub : OPE size n sizeMask}
|
||||
{0 left : OPE m1 size leftMask}
|
||||
{0 right : OPE m2 size rightMask}
|
||||
0 leftComp : Comp sub left ope1
|
||||
0 rightComp : Comp sub right ope2
|
||||
{auto 0 isCover : Cover [left, right]}
|
||||
%name Coprod2 cop
|
||||
|
||||
export
|
||||
coprod2 : {n, mask1, mask2 : Nat} ->
|
||||
(0 ope1 : OPE m1 n mask1) -> (0 ope2 : OPE m2 n mask2) ->
|
||||
Coprod2 ope1 ope2
|
||||
coprod2 ope1 ope2 with (view ope1) | (view ope2)
|
||||
coprod2 Stop Stop | StopV | StopV = MkCoprod2 StopZ StopZ
|
||||
coprod2 (Drop ope1 Refl) (Drop ope2 Refl) | DropV _ ope1 | DropV _ ope2 =
|
||||
let MkCoprod2 l r = coprod2 ope1 ope2 in MkCoprod2 (DropZ l) (DropZ r)
|
||||
coprod2 (Drop ope1 Refl) (Keep ope2 Refl) | DropV _ ope1 | KeepV _ ope2 =
|
||||
let MkCoprod2 l r = coprod2 ope1 ope2 in MkCoprod2 (KDZ l) (KeepZ r)
|
||||
coprod2 (Keep ope1 Refl) (Drop ope2 Refl) | KeepV _ ope1 | DropV _ ope2 =
|
||||
let MkCoprod2 l r = coprod2 ope1 ope2 in MkCoprod2 (KeepZ l) (KDZ r)
|
||||
coprod2 (Keep ope1 Refl) (Keep ope2 Refl) | KeepV _ ope1 | KeepV _ ope2 =
|
||||
let MkCoprod2 l r = coprod2 ope1 ope2 in MkCoprod2 (KeepZ l) (KeepZ r)
|
||||
|
||||
-- [todo] n-ary coprod
|
||||
26
lib/Quox/Thin/Cover.idr
Normal file
26
lib/Quox/Thin/Cover.idr
Normal file
|
|
@ -0,0 +1,26 @@
|
|||
module Quox.Thin.Cover
|
||||
|
||||
import public Quox.Thin.Base
|
||||
import public Quox.Thin.List
|
||||
|
||||
%default total
|
||||
|
||||
||| an OPE list is a cover if at least one of the OPEs has `Keep` as the head,
|
||||
||| and the tails are also a cover
|
||||
|||
|
||||
||| in @egtbs it is a binary relation which is fine for ×ᵣ but i don't want to
|
||||
||| write my AST in universe-of-syntaxes style. sorry
|
||||
public export data Cover : OPEList n -> Type
|
||||
|
||||
||| the "`Keep` in the head" condition of a cover
|
||||
public export data Cover1 : OPEList n -> Type
|
||||
|
||||
data Cover where
|
||||
Nil : Cover opes {n = 0}
|
||||
(::) : Cover1 opes -> All2 IsTail opes tails => Cover tails -> Cover opes
|
||||
%name Cover cov
|
||||
|
||||
data Cover1 where
|
||||
Here : Cover1 (Keep ope eq :: opes)
|
||||
There : Cover1 opes -> Cover1 (ope :: opes)
|
||||
%name Cover1 cov1
|
||||
128
lib/Quox/Thin/Eqv.idr
Normal file
128
lib/Quox/Thin/Eqv.idr
Normal file
|
|
@ -0,0 +1,128 @@
|
|||
module Quox.Thin.Eqv
|
||||
|
||||
import public Quox.Thin.Base
|
||||
import public Quox.Thin.View
|
||||
import Quox.NatExtra
|
||||
import Syntax.PreorderReasoning
|
||||
|
||||
%default total
|
||||
|
||||
infix 6 `Eqv`
|
||||
|
||||
private
|
||||
uip : (p, q : a = b) -> p = q
|
||||
uip Refl Refl = Refl
|
||||
|
||||
|
||||
public export
|
||||
data Eqv : OPE m1 n1 mask1 -> OPE m2 n2 mask2 -> Type where
|
||||
EqvStop : Eqv Stop Stop
|
||||
EqvDrop : {0 p : OPE m1 n1 mask1} ->
|
||||
{0 q : OPE m2 n2 mask2} ->
|
||||
Eqv p q -> Eqv (Drop p eq1) (Drop q eq2)
|
||||
EqvKeep : {0 p : OPE m1 n1 mask1} ->
|
||||
{0 q : OPE m2 n2 mask2} ->
|
||||
Eqv p q -> Eqv (Keep p eq1) (Keep q eq2)
|
||||
%name Eqv eqv
|
||||
|
||||
export Uninhabited (Stop `Eqv` Drop p e) where uninhabited _ impossible
|
||||
export Uninhabited (Stop `Eqv` Keep p e) where uninhabited _ impossible
|
||||
export Uninhabited (Drop p e `Eqv` Stop) where uninhabited _ impossible
|
||||
export Uninhabited (Drop p e `Eqv` Keep q f) where uninhabited _ impossible
|
||||
export Uninhabited (Keep p e `Eqv` Stop) where uninhabited _ impossible
|
||||
export Uninhabited (Keep p e `Eqv` Drop q f) where uninhabited _ impossible
|
||||
|
||||
export
|
||||
Reflexive (OPE m n mask) Eqv where
|
||||
reflexive {x = Stop} = EqvStop
|
||||
reflexive {x = Drop {}} = EqvDrop reflexive
|
||||
reflexive {x = Keep {}} = EqvKeep reflexive
|
||||
|
||||
export
|
||||
symmetric : p `Eqv` q -> q `Eqv` p
|
||||
symmetric EqvStop = EqvStop
|
||||
symmetric (EqvDrop eqv) = EqvDrop $ symmetric eqv
|
||||
symmetric (EqvKeep eqv) = EqvKeep $ symmetric eqv
|
||||
|
||||
export
|
||||
transitive : p `Eqv` q -> q `Eqv` r -> p `Eqv` r
|
||||
transitive EqvStop EqvStop = EqvStop
|
||||
transitive (EqvDrop eqv1) (EqvDrop eqv2) = EqvDrop (transitive eqv1 eqv2)
|
||||
transitive (EqvKeep eqv1) (EqvKeep eqv2) = EqvKeep (transitive eqv1 eqv2)
|
||||
|
||||
|
||||
private
|
||||
recompute' : {mask1, mask2, n1, n2 : Nat} ->
|
||||
(0 p : OPE m1 n1 mask1) -> (0 q : OPE m2 n2 mask2) ->
|
||||
(0 eqv : p `Eqv` q) -> p `Eqv` q
|
||||
recompute' p q eqv with %syntactic (view p) | (view q)
|
||||
recompute' Stop Stop _ | StopV | StopV = EqvStop
|
||||
recompute' (Drop p _) (Drop q _) eqv | DropV _ p | DropV _ q =
|
||||
EqvDrop $ recompute' {eqv = let EqvDrop e = eqv in e, _}
|
||||
recompute' (Keep p _) (Keep q _) eqv | KeepV _ p | KeepV _ q =
|
||||
EqvKeep $ recompute' {eqv = let EqvKeep e = eqv in e, _}
|
||||
recompute' (Drop p _) (Keep q _) eqv | DropV _ p | KeepV _ q =
|
||||
void $ absurd eqv
|
||||
recompute' (Keep p _) (Drop q _) eqv | KeepV _ p | DropV _ q =
|
||||
void $ absurd eqv
|
||||
|
||||
private
|
||||
recompute : {mask1, mask2, n1, n2 : Nat} ->
|
||||
{0 p : OPE m1 n1 mask1} -> {0 q : OPE m2 n2 mask2} ->
|
||||
(0 _ : p `Eqv` q) -> p `Eqv` q
|
||||
recompute eqv = recompute' {eqv, _}
|
||||
|
||||
|
||||
export
|
||||
eqvIndices : {0 p : OPE m1 n1 mask1} -> {0 q : OPE m2 n2 mask2} ->
|
||||
p `Eqv` q -> (m1 = m2, n1 = n2, mask1 = mask2)
|
||||
eqvIndices EqvStop = (Refl, Refl, Refl)
|
||||
eqvIndices (EqvDrop eqv {eq1 = Refl, eq2 = Refl}) =
|
||||
let (Refl, Refl, Refl) = eqvIndices eqv in (Refl, Refl, Refl)
|
||||
eqvIndices (EqvKeep eqv {eq1 = Refl, eq2 = Refl}) =
|
||||
let (Refl, Refl, Refl) = eqvIndices eqv in (Refl, Refl, Refl)
|
||||
|
||||
export
|
||||
0 eqvMask : (p : OPE m1 n mask1) -> (q : OPE m2 n mask2) ->
|
||||
mask1 = mask2 -> p `Eqv` q
|
||||
eqvMask Stop Stop _ = EqvStop
|
||||
eqvMask (Drop ope1 Refl) (Drop {mask = mm2} ope2 eq2) Refl =
|
||||
EqvDrop $ eqvMask ope1 ope2 (doubleInj _ _ eq2)
|
||||
eqvMask (Drop ope1 Refl) (Keep ope2 eq2) Refl =
|
||||
void $ notEvenOdd _ _ eq2
|
||||
eqvMask (Keep ope1 eq1) (Keep ope2 eq2) Refl =
|
||||
EqvKeep $ eqvMask ope1 ope2 (doubleInj _ _ $ inj S $ trans (sym eq1) eq2)
|
||||
eqvMask (Keep ope1 eq1) (Drop ope2 eq2) Refl =
|
||||
void $ notEvenOdd _ _ $ trans (sym eq2) eq1
|
||||
|
||||
export
|
||||
0 eqvEq : (p, q : OPE m n mask) -> p `Eqv` q -> p === q
|
||||
eqvEq Stop Stop EqvStop = Refl
|
||||
eqvEq (Drop p eq1) (Drop q eq2) (EqvDrop eqv)
|
||||
with %syntactic (doubleInj _ _ $ trans (sym eq1) eq2)
|
||||
_ | Refl = cong2 Drop (eqvEq p q eqv) (uip eq1 eq2)
|
||||
eqvEq (Keep p eq1) (Keep q eq2) (EqvKeep eqv)
|
||||
with %syntactic (doubleInj _ _ $ inj S $ trans (sym eq1) eq2)
|
||||
_ | Refl = cong2 Keep (eqvEq p q eqv) (uip eq1 eq2)
|
||||
|
||||
export
|
||||
0 eqvEq' : (p : OPE m1 n1 mask1) -> (q : OPE m2 n2 mask2) ->
|
||||
p `Eqv` q -> p ~=~ q
|
||||
eqvEq' p q eqv = let (Refl, Refl, Refl) = eqvIndices eqv in eqvEq p q eqv
|
||||
|
||||
export
|
||||
0 maskEqInner : (0 ope1 : OPE m1 n mask1) -> (0 ope2 : OPE m2 n mask2) ->
|
||||
mask1 = mask2 -> m1 = m2
|
||||
maskEqInner Stop Stop _ = Refl
|
||||
maskEqInner (Drop ope1 Refl) (Drop ope2 Refl) eq =
|
||||
maskEqInner ope1 ope2 (doubleInj _ _ eq)
|
||||
maskEqInner (Keep ope1 Refl) (Keep ope2 Refl) eq =
|
||||
cong S $ maskEqInner ope1 ope2 $ doubleInj _ _ $ inj S eq
|
||||
maskEqInner (Drop ope1 Refl) (Keep ope2 Refl) eq = void $ notEvenOdd _ _ eq
|
||||
maskEqInner (Keep {mask = mask1'} ope1 eq1) (Drop {mask = mask2'} ope2 eq2) eq =
|
||||
-- matching on eq1, eq2, or eq here triggers that weird coverage bug ☹
|
||||
void $ notEvenOdd _ _ $ Calc $
|
||||
|~ mask2' + mask2'
|
||||
~~ mask2 ..<(eq2)
|
||||
~~ mask1 ..<(eq)
|
||||
~~ S (mask1' + mask1') ...(eq1)
|
||||
123
lib/Quox/Thin/List.idr
Normal file
123
lib/Quox/Thin/List.idr
Normal file
|
|
@ -0,0 +1,123 @@
|
|||
module Quox.Thin.List
|
||||
|
||||
import public Quox.Thin.Base
|
||||
import public Quox.Thin.Cons
|
||||
import Data.DPair
|
||||
import Data.Nat
|
||||
import Control.Function
|
||||
|
||||
%default total
|
||||
|
||||
||| a list of OPEs of a given outer scope size
|
||||
||| (at runtime just the masks)
|
||||
public export
|
||||
data OPEList : Nat -> Type where
|
||||
Nil : OPEList n
|
||||
(::) : {mask : Nat} -> (0 ope : OPE m n mask) -> OPEList n -> OPEList n
|
||||
%name OPEList opes
|
||||
|
||||
export
|
||||
length : OPEList n -> Nat
|
||||
length [] = 0
|
||||
length (_ :: opes) = S $ length opes
|
||||
|
||||
export
|
||||
toList : OPEList n -> List (SomeOPE n)
|
||||
toList [] = []
|
||||
toList (ope :: opes) = MkOPE ope :: toList opes
|
||||
|
||||
export
|
||||
fromList : List (SomeOPE n) -> OPEList n
|
||||
fromList [] = []
|
||||
fromList (MkOPE ope :: xs) = ope :: fromList xs
|
||||
|
||||
|
||||
public export
|
||||
0 Pred : Nat -> Type
|
||||
Pred n = forall m, mask. OPE m n mask -> Type
|
||||
|
||||
public export
|
||||
0 Rel : Nat -> Nat -> Type
|
||||
Rel n1 n2 = forall m1, m2, mask1, mask2.
|
||||
OPE m1 n1 mask1 -> OPE m2 n2 mask2 -> Type
|
||||
|
||||
namespace All
|
||||
public export
|
||||
data All : Pred n -> OPEList n -> Type where
|
||||
Nil : {0 p : Pred n} -> All p []
|
||||
(::) : {0 p : Pred n} -> p ope -> All p opes -> All p (ope :: opes)
|
||||
%name All.All ps, qs
|
||||
|
||||
namespace All2
|
||||
public export
|
||||
data All2 : Rel n1 n2 -> OPEList n1 -> OPEList n2 -> Type where
|
||||
Nil : {0 p : Rel n1 n2} -> All2 p [] []
|
||||
(::) : {0 p : Rel n1 n2} -> p a b -> All2 p as bs ->
|
||||
All2 p (a :: as) (b :: bs)
|
||||
%name All2.All2 ps, qs
|
||||
|
||||
namespace Any
|
||||
public export
|
||||
data Any : Pred n -> OPEList n -> Type where
|
||||
Here : {0 p : Pred n} -> p ope -> Any p (ope :: opes)
|
||||
There : {0 p : Pred n} -> Any p opes -> Any p (ope :: opes)
|
||||
%name Any.Any p, q
|
||||
|
||||
export
|
||||
{0 p : Pred n} -> Uninhabited (Any p []) where uninhabited _ impossible
|
||||
|
||||
export
|
||||
all : {0 p : Pred n} ->
|
||||
(forall m. {mask : Nat} -> (0 ope : OPE m n mask) -> p ope) ->
|
||||
(opes : OPEList n) -> All p opes
|
||||
all f [] = []
|
||||
all f (ope :: opes) = f ope :: all f opes
|
||||
|
||||
export
|
||||
allDec : {0 p : Pred n} ->
|
||||
(forall m. {mask : Nat} -> (0 ope : OPE m n mask) -> Dec (p ope)) ->
|
||||
(opes : OPEList n) -> Dec (All p opes)
|
||||
allDec f [] = Yes []
|
||||
allDec f (ope :: opes) = case f ope of
|
||||
Yes y => case allDec f opes of
|
||||
Yes ys => Yes $ y :: ys
|
||||
No k => No $ \(_ :: ps) => k ps
|
||||
No k => No $ \(p :: _) => k p
|
||||
|
||||
export
|
||||
anyDec : {0 p : Pred n} ->
|
||||
(forall m. {mask : Nat} -> (0 ope : OPE m n mask) -> Dec (p ope)) ->
|
||||
(opes : OPEList n) -> Dec (Any p opes)
|
||||
anyDec f [] = No absurd
|
||||
anyDec f (ope :: opes) = case f ope of
|
||||
Yes y => Yes $ Here y
|
||||
No nh => case anyDec f opes of
|
||||
Yes y => Yes $ There y
|
||||
No nt => No $ \case Here h => nh h; There t => nt t
|
||||
|
||||
|
||||
export
|
||||
unconses : {n : Nat} -> (opes : OPEList (S n)) -> All Uncons opes
|
||||
unconses = all uncons
|
||||
|
||||
export
|
||||
heads : {n : Nat} -> (opes : OPEList (S n)) -> All (Exists . IsHead) opes
|
||||
heads = all head
|
||||
|
||||
export
|
||||
tails : {n : Nat} -> (opes : OPEList (S n)) -> All Tail opes
|
||||
tails = all tail
|
||||
|
||||
-- [fixme] factor this out probably
|
||||
export
|
||||
tails_ : {n : Nat} -> (opes : OPEList (S n)) ->
|
||||
Subset (OPEList n) (All2 IsTail opes)
|
||||
tails_ [] = Element [] []
|
||||
tails_ (ope :: opes) = Element _ $ (tail ope).isTail :: (tails_ opes).snd
|
||||
|
||||
export
|
||||
conses : (heads : List Bool) -> (tails : OPEList n) ->
|
||||
(0 len : length heads = length tails) =>
|
||||
OPEList (S n)
|
||||
conses [] [] = []
|
||||
conses (h :: hs) (t :: ts) = snd (cons h t) :: conses hs ts @{inj S len}
|
||||
57
lib/Quox/Thin/Split.idr
Normal file
57
lib/Quox/Thin/Split.idr
Normal file
|
|
@ -0,0 +1,57 @@
|
|||
module Quox.Thin.Split
|
||||
|
||||
import public Quox.Thin.Base
|
||||
import public Quox.Thin.View
|
||||
import public Quox.Thin.Eqv
|
||||
import public Quox.Thin.Append
|
||||
import public Quox.Thin.Cover
|
||||
import Data.DPair
|
||||
import Control.Relation
|
||||
|
||||
%default total
|
||||
|
||||
public export
|
||||
record Chunks m n where
|
||||
constructor MkChunks
|
||||
{leftMask : Nat}
|
||||
{rightMask : Nat}
|
||||
0 left : OPE m (m + n) leftMask
|
||||
0 right : OPE n (m + n) rightMask
|
||||
{auto 0 isCover : Cover [left, right]}
|
||||
%name Chunks chunks
|
||||
|
||||
export
|
||||
chunks : (m, n : Nat) -> Chunks m n
|
||||
chunks 0 0 = MkChunks Stop Stop
|
||||
chunks 0 (S n) =
|
||||
let MkChunks l r = chunks 0 n in
|
||||
MkChunks (Drop l Refl) (Keep r Refl)
|
||||
chunks (S m) n =
|
||||
let MkChunks l r = chunks m n in
|
||||
MkChunks (Keep l Refl) (Drop r Refl)
|
||||
|
||||
-- [todo] the masks here are just ((2 << m) - 1) << n and (2 << n) - 1
|
||||
|
||||
|
||||
public export
|
||||
record SplitAt m n1 n2 (ope : OPE m (n1 + n2) mask) where
|
||||
constructor MkSplitAt
|
||||
{leftMask, rightMask : Nat}
|
||||
{0 leftScope, rightScope : Nat}
|
||||
0 left : OPE leftScope n1 leftMask
|
||||
0 right : OPE rightScope n2 rightMask
|
||||
0 scopePrf : m = leftScope + rightScope
|
||||
0 opePrf : ope `Eqv` (left `app'` right).snd
|
||||
%name SplitAt split
|
||||
|
||||
export
|
||||
splitAt : (n1 : Nat) -> {n2, mask : Nat} -> (0 ope : OPE m (n1 + n2) mask) ->
|
||||
SplitAt m n1 n2 ope
|
||||
splitAt 0 ope = MkSplitAt zero ope Refl reflexive
|
||||
splitAt (S n1) ope with %syntactic (view ope)
|
||||
splitAt (S n1) (Drop ope Refl) | DropV _ ope with %syntactic (splitAt n1 ope)
|
||||
_ | MkSplitAt left right scopePrf opePrf =
|
||||
MkSplitAt (Drop left Refl) right scopePrf (EqvDrop opePrf)
|
||||
splitAt (S n1) (Keep ope Refl) | KeepV _ ope with %syntactic (splitAt n1 ope)
|
||||
_ | MkSplitAt left right scopePrf opePrf =
|
||||
MkSplitAt (Keep left Refl) right (cong S scopePrf) (EqvKeep opePrf)
|
||||
179
lib/Quox/Thin/Term.idr
Normal file
179
lib/Quox/Thin/Term.idr
Normal file
|
|
@ -0,0 +1,179 @@
|
|||
module Quox.Thin.Term
|
||||
|
||||
import public Quox.Thin.Base
|
||||
import public Quox.Thin.Comp
|
||||
import public Quox.Thin.List
|
||||
import Quox.Thin.Eqv
|
||||
import public Quox.Thin.Cover
|
||||
import Quox.Name
|
||||
import Quox.Loc
|
||||
import Data.DPair
|
||||
import public Data.List.Quantifiers
|
||||
import Data.Vect
|
||||
import Data.Singleton
|
||||
import Decidable.Equality
|
||||
|
||||
%default total
|
||||
|
||||
public export
|
||||
record Thinned f n where
|
||||
constructor Th
|
||||
{0 scope : Nat}
|
||||
{scopeMask : Nat}
|
||||
0 ope : OPE scope n scopeMask
|
||||
term : f scope
|
||||
%name Thinned s, t, u
|
||||
|
||||
export
|
||||
(forall n. Eq (f n)) => Eq (Thinned f n) where
|
||||
s == t = case decEq s.scopeMask t.scopeMask of
|
||||
Yes eq => s.term == (rewrite maskEqInner s.ope t.ope eq in t.term)
|
||||
No _ => False
|
||||
|
||||
export
|
||||
(forall n. Located (f n)) => Located (Thinned f n) where
|
||||
term.loc = term.term.loc
|
||||
|
||||
export
|
||||
(forall n. Relocatable (f n)) => Relocatable (Thinned f n) where
|
||||
setLoc loc = {term $= setLoc loc}
|
||||
|
||||
namespace Thinned
|
||||
export
|
||||
pure : {n : Nat} -> f n -> Thinned f n
|
||||
pure term = Th id.snd term
|
||||
|
||||
export
|
||||
join : {n : Nat} -> Thinned (Thinned f) n -> Thinned f n
|
||||
join (Th ope1 (Th ope2 term)) = Th (ope1 . ope2) term
|
||||
|
||||
|
||||
public export
|
||||
record ScopedN (s : Nat) (f : Nat -> Type) (n : Nat) where
|
||||
constructor S
|
||||
names : Vect s BindName
|
||||
{0 scope : Nat}
|
||||
{mask : Nat}
|
||||
0 ope : OPE scope s mask
|
||||
body : f (scope + n)
|
||||
|
||||
export
|
||||
(forall n. Eq (f n)) => Eq (ScopedN s f n) where
|
||||
s1 == s2 = case decEq s1.mask s2.mask of
|
||||
Yes eq =>
|
||||
s1.names == s2.names &&
|
||||
s1.body == (rewrite maskEqInner s1.ope s2.ope eq in s2.body)
|
||||
No _ => False
|
||||
|
||||
export
|
||||
{s : Nat} -> (forall n. Show (f n)) => Show (ScopedN s f n) where
|
||||
showPrec d (S ns ope body) = showCon d "S" $
|
||||
showArg ns ++ showArg (unVal $ maskToOpe ope) ++ showArg body
|
||||
|
||||
public export
|
||||
Scoped : (Nat -> Type) -> Nat -> Type
|
||||
Scoped d n = ScopedN 1 d n
|
||||
|
||||
(.name) : Scoped f n -> BindName
|
||||
(S {names = [x], _}).name = x
|
||||
|
||||
export
|
||||
(forall n. Located (f n)) => Located (ScopedN s f n) where
|
||||
s.loc = s.body.loc
|
||||
|
||||
export
|
||||
(forall n. Relocatable (f n)) => Relocatable (ScopedN s f n) where
|
||||
setLoc loc = {body $= setLoc loc}
|
||||
|
||||
|
||||
public export
|
||||
record Thinned2 f d n where
|
||||
constructor Th2
|
||||
{0 dscope, tscope : Nat}
|
||||
{dmask, tmask : Nat}
|
||||
0 dope : OPE dscope d dmask
|
||||
0 tope : OPE tscope n tmask
|
||||
term : f dscope tscope
|
||||
%name Thinned2 term
|
||||
|
||||
export
|
||||
(forall d, n. Eq (f d n)) => Eq (Thinned2 f d n) where
|
||||
s == t = case (decEq s.dmask t.dmask, decEq s.tmask t.tmask) of
|
||||
(Yes deq, Yes teq) =>
|
||||
s.term == (rewrite maskEqInner s.dope t.dope deq in
|
||||
rewrite maskEqInner s.tope t.tope teq in t.term)
|
||||
_ => False
|
||||
|
||||
export
|
||||
(forall d, n. Located (f d n)) => Located (Thinned2 f d n) where
|
||||
term.loc = term.term.loc
|
||||
|
||||
export
|
||||
(forall d, n. Relocatable (f d n)) => Relocatable (Thinned2 f d n) where
|
||||
setLoc loc = {term $= setLoc loc}
|
||||
|
||||
namespace Thinned2
|
||||
export
|
||||
pure : {d, n : Nat} -> f d n -> Thinned2 f d n
|
||||
pure term = Th2 id.snd id.snd term
|
||||
|
||||
export
|
||||
join : {d, n : Nat} -> Thinned2 (Thinned2 f) d n -> Thinned2 f d n
|
||||
join (Th2 dope1 tope1 (Th2 dope2 tope2 term)) =
|
||||
Th2 (dope1 . dope2) (tope1 . tope2) term
|
||||
|
||||
|
||||
namespace TermList
|
||||
public export
|
||||
data Element : (Nat -> Nat -> Type) ->
|
||||
OPE dscope d dmask -> OPE tscope n tmask -> Type where
|
||||
T : f dscope tscope ->
|
||||
{dmask : Nat} -> (0 dope : OPE dscope d dmask) ->
|
||||
{tmask : Nat} -> (0 tope : OPE tscope n tmask) ->
|
||||
Element f dope tope
|
||||
%name TermList.Element s, t, u
|
||||
|
||||
export
|
||||
elementEq : (forall d, n. Eq (f d n)) =>
|
||||
Element {d, n} f dope1 tope1 -> Element {d, n} f dope2 tope2 ->
|
||||
Bool
|
||||
elementEq (T s dope1 tope1 {dmask = dm1, tmask = tm1})
|
||||
(T t dope2 tope2 {dmask = dm2, tmask = tm2}) =
|
||||
case (decEq dm1 dm2, decEq tm1 tm2) of
|
||||
(Yes deq, Yes teq) =>
|
||||
s == (rewrite maskEqInner dope1 dope2 deq in
|
||||
rewrite maskEqInner tope1 tope2 teq in t)
|
||||
_ => False
|
||||
|
||||
public export
|
||||
data TermList : List (Nat -> Nat -> Type) ->
|
||||
OPEList d -> OPEList n -> Type where
|
||||
Nil : TermList [] [] []
|
||||
(::) : Element f dope tope ->
|
||||
TermList fs dopes topes ->
|
||||
TermList (f :: fs) (dope :: dopes) (tope :: topes)
|
||||
%name TermList ss, ts, us
|
||||
|
||||
export
|
||||
termListEq : All (\f => forall d, n. Eq (f d n)) fs =>
|
||||
TermList {d, n} fs dopes1 topes1 ->
|
||||
TermList {d, n} fs dopes2 topes2 ->
|
||||
Bool
|
||||
termListEq [] [] = True
|
||||
termListEq (s :: ss) (t :: ts) @{eq :: eqs} =
|
||||
elementEq s t && termListEq ss ts
|
||||
|
||||
|
||||
public export
|
||||
record Subterms (fs : List (Nat -> Nat -> Type)) d n where
|
||||
constructor Sub
|
||||
{0 dopes : OPEList d}
|
||||
{0 topes : OPEList n}
|
||||
terms : TermList fs dopes topes
|
||||
0 dcov : Cover dopes
|
||||
0 tcov : Cover topes
|
||||
%name Subterms ss, ts, us
|
||||
|
||||
export
|
||||
All (\f => forall d, n. Eq (f d n)) fs => Eq (Subterms fs d n) where
|
||||
ss == ts = ss.terms `termListEq` ts.terms
|
||||
76
lib/Quox/Thin/View.idr
Normal file
76
lib/Quox/Thin/View.idr
Normal file
|
|
@ -0,0 +1,76 @@
|
|||
module Quox.Thin.View
|
||||
|
||||
import public Quox.Thin.Base
|
||||
import Quox.NatExtra
|
||||
import Data.Singleton
|
||||
|
||||
%default total
|
||||
|
||||
public export
|
||||
data View : OPE m n mask -> Type where
|
||||
StopV : View Stop
|
||||
DropV : (mask : Nat) -> (0 ope : OPE m n mask) -> View (Drop ope Refl)
|
||||
KeepV : (mask : Nat) -> (0 ope : OPE m n mask) -> View (Keep ope Refl)
|
||||
%name View.View v
|
||||
|
||||
private
|
||||
0 stopEqs : OPE m 0 mask -> (m = 0, mask = 0)
|
||||
stopEqs Stop = (Refl, Refl)
|
||||
|
||||
private
|
||||
0 fromStop : (ope : OPE 0 0 0) -> ope = Stop
|
||||
fromStop Stop = Refl
|
||||
|
||||
private
|
||||
0 fromDrop : (ope : OPE m (S n) (k + k)) ->
|
||||
(inner : OPE m n k ** ope === Drop inner Refl)
|
||||
fromDrop (Drop ope eq) with %syntactic (doubleInj _ _ eq)
|
||||
fromDrop (Drop ope Refl) | Refl = (ope ** Refl)
|
||||
fromDrop (Keep ope eq) = void $ notEvenOdd _ _ eq
|
||||
|
||||
private
|
||||
0 fromKeep : (ope : OPE (S m) (S n) (S (k + k))) ->
|
||||
(inner : OPE m n k ** ope === Keep inner Refl)
|
||||
fromKeep (Drop ope eq) = void $ notEvenOdd _ _ $ sym eq
|
||||
fromKeep (Keep ope eq) with %syntactic (doubleInj _ _ $ inj S eq)
|
||||
fromKeep (Keep ope Refl) | Refl = (ope ** Refl)
|
||||
|
||||
private
|
||||
0 keepIsSucc : (ope : OPE m n (S (k + k))) -> IsSucc m
|
||||
keepIsSucc (Drop ope eq) = void $ notEvenOdd _ _ $ sym eq
|
||||
keepIsSucc (Keep ope _) = ItIsSucc
|
||||
|
||||
export
|
||||
view : {0 m : Nat} -> {n, mask : Nat} -> (0 ope : OPE m n mask) -> View ope
|
||||
view {n = 0} ope with %syntactic 0 (fst $ stopEqs ope) | 0 (snd $ stopEqs ope)
|
||||
_ | Refl | Refl = rewrite fromStop ope in StopV
|
||||
view {n = S n} ope with %syntactic (half mask)
|
||||
_ | HalfOdd mask' with %syntactic 0 (keepIsSucc ope)
|
||||
_ | ItIsSucc with %syntactic 0 (fromKeep ope)
|
||||
_ | (ope' ** eq) = rewrite eq in KeepV mask' ope'
|
||||
_ | HalfEven mask' with %syntactic 0 (fromDrop ope)
|
||||
_ | (ope' ** eq) = rewrite eq in DropV mask' ope'
|
||||
|
||||
|
||||
export
|
||||
appOpe : {0 m : Nat} -> (n : Nat) -> {mask : Nat} ->
|
||||
(0 ope : OPE m n mask) -> Singleton m
|
||||
appOpe n ope with %syntactic (view ope)
|
||||
appOpe 0 Stop | StopV = Val 0
|
||||
appOpe (S n) (Drop ope' _) | DropV _ ope' = appOpe n ope'
|
||||
appOpe (S n) (Keep ope' _) | KeepV _ ope' = [|S $ appOpe n ope'|]
|
||||
|
||||
export
|
||||
maskToOpe : {n, mask : Nat} -> (0 ope : OPE m n mask) -> Singleton ope
|
||||
maskToOpe ope with %syntactic (view ope)
|
||||
maskToOpe Stop | StopV = [|Stop|]
|
||||
maskToOpe (Drop ope Refl) | DropV k ope = [|drop $ maskToOpe ope|]
|
||||
maskToOpe (Keep ope Refl) | KeepV k ope = [|keep $ maskToOpe ope|]
|
||||
|
||||
export
|
||||
0 outerInnerZero : OPE m 0 mask -> m = 0
|
||||
outerInnerZero Stop = Refl
|
||||
|
||||
export
|
||||
0 outerMaskZero : OPE m 0 mask -> mask = 0
|
||||
outerMaskZero Stop = Refl
|
||||
|
|
@ -16,9 +16,19 @@ modules =
|
|||
Quox.Decidable,
|
||||
Quox.No,
|
||||
Quox.Loc,
|
||||
Quox.OPE,
|
||||
Quox.Thin,
|
||||
Quox.Pretty,
|
||||
Quox.Thin.Base,
|
||||
Quox.Thin.View,
|
||||
Quox.Thin.Eqv,
|
||||
Quox.Thin.Cons,
|
||||
Quox.Thin.List,
|
||||
Quox.Thin.Append,
|
||||
Quox.Thin.Comp,
|
||||
Quox.Thin.Cover,
|
||||
Quox.Thin.Coprod,
|
||||
Quox.Thin.Split,
|
||||
Quox.Thin.Term,
|
||||
Quox.Thin,
|
||||
Quox.Syntax,
|
||||
Quox.Syntax.Dim,
|
||||
Quox.Syntax.DimEq,
|
||||
|
|
|
|||
Loading…
Reference in a new issue