From e1e9ca1b80f5c60000f400e77feb64f6dfe4b761 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Mon, 5 Jun 2023 16:19:52 +0200 Subject: [PATCH] split and extend Quox.Thin --- lib/Quox/Thin.idr | 397 ++------------------------------------- lib/Quox/Thin/Append.idr | 27 +++ lib/Quox/Thin/Base.idr | 80 ++++++++ lib/Quox/Thin/Comp.idr | 59 ++++++ lib/Quox/Thin/Cons.idr | 74 ++++++++ lib/Quox/Thin/Coprod.idr | 41 ++++ lib/Quox/Thin/Cover.idr | 26 +++ lib/Quox/Thin/Eqv.idr | 128 +++++++++++++ lib/Quox/Thin/List.idr | 123 ++++++++++++ lib/Quox/Thin/Split.idr | 57 ++++++ lib/Quox/Thin/Term.idr | 179 ++++++++++++++++++ lib/Quox/Thin/View.idr | 76 ++++++++ lib/quox-lib.ipkg | 14 +- 13 files changed, 893 insertions(+), 388 deletions(-) create mode 100644 lib/Quox/Thin/Append.idr create mode 100644 lib/Quox/Thin/Base.idr create mode 100644 lib/Quox/Thin/Comp.idr create mode 100644 lib/Quox/Thin/Cons.idr create mode 100644 lib/Quox/Thin/Coprod.idr create mode 100644 lib/Quox/Thin/Cover.idr create mode 100644 lib/Quox/Thin/Eqv.idr create mode 100644 lib/Quox/Thin/List.idr create mode 100644 lib/Quox/Thin/Split.idr create mode 100644 lib/Quox/Thin/Term.idr create mode 100644 lib/Quox/Thin/View.idr diff --git a/lib/Quox/Thin.idr b/lib/Quox/Thin.idr index a1b3a02..90eb2ae 100644 --- a/lib/Quox/Thin.idr +++ b/lib/Quox/Thin.idr @@ -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 diff --git a/lib/Quox/Thin/Append.idr b/lib/Quox/Thin/Append.idr new file mode 100644 index 0000000..37a5a4c --- /dev/null +++ b/lib/Quox/Thin/Append.idr @@ -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 diff --git a/lib/Quox/Thin/Base.idr b/lib/Quox/Thin/Base.idr new file mode 100644 index 0000000..3a6fb21 --- /dev/null +++ b/lib/Quox/Thin/Base.idr @@ -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 diff --git a/lib/Quox/Thin/Comp.idr b/lib/Quox/Thin/Comp.idr new file mode 100644 index 0000000..4561898 --- /dev/null +++ b/lib/Quox/Thin/Comp.idr @@ -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 diff --git a/lib/Quox/Thin/Cons.idr b/lib/Quox/Thin/Cons.idr new file mode 100644 index 0000000..81fe762 --- /dev/null +++ b/lib/Quox/Thin/Cons.idr @@ -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 diff --git a/lib/Quox/Thin/Coprod.idr b/lib/Quox/Thin/Coprod.idr new file mode 100644 index 0000000..c84008e --- /dev/null +++ b/lib/Quox/Thin/Coprod.idr @@ -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 diff --git a/lib/Quox/Thin/Cover.idr b/lib/Quox/Thin/Cover.idr new file mode 100644 index 0000000..886a1b3 --- /dev/null +++ b/lib/Quox/Thin/Cover.idr @@ -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 diff --git a/lib/Quox/Thin/Eqv.idr b/lib/Quox/Thin/Eqv.idr new file mode 100644 index 0000000..76b8957 --- /dev/null +++ b/lib/Quox/Thin/Eqv.idr @@ -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) diff --git a/lib/Quox/Thin/List.idr b/lib/Quox/Thin/List.idr new file mode 100644 index 0000000..5d8c7b2 --- /dev/null +++ b/lib/Quox/Thin/List.idr @@ -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} diff --git a/lib/Quox/Thin/Split.idr b/lib/Quox/Thin/Split.idr new file mode 100644 index 0000000..07bda8a --- /dev/null +++ b/lib/Quox/Thin/Split.idr @@ -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) diff --git a/lib/Quox/Thin/Term.idr b/lib/Quox/Thin/Term.idr new file mode 100644 index 0000000..25313e4 --- /dev/null +++ b/lib/Quox/Thin/Term.idr @@ -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 diff --git a/lib/Quox/Thin/View.idr b/lib/Quox/Thin/View.idr new file mode 100644 index 0000000..1d60bef --- /dev/null +++ b/lib/Quox/Thin/View.idr @@ -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 diff --git a/lib/quox-lib.ipkg b/lib/quox-lib.ipkg index 24f605f..17ec5b8 100644 --- a/lib/quox-lib.ipkg +++ b/lib/quox-lib.ipkg @@ -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,