From ddfbca7fccde41c01cebb1d58e5aaad936bacc0c Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Mon, 5 Jun 2023 17:25:02 +0200 Subject: [PATCH] (n-ary) coprod --- lib/Quox/Thin/Base.idr | 3 +- lib/Quox/Thin/Coprod.idr | 184 +++++++++++++++++++++++++++++++++------ lib/Quox/Thin/Cover.idr | 1 + lib/Quox/Thin/List.idr | 12 ++- lib/Quox/Thin/View.idr | 16 ++++ 5 files changed, 184 insertions(+), 32 deletions(-) diff --git a/lib/Quox/Thin/Base.idr b/lib/Quox/Thin/Base.idr index 3a6fb21..a60c185 100644 --- a/lib/Quox/Thin/Base.idr +++ b/lib/Quox/Thin/Base.idr @@ -76,5 +76,6 @@ one' i = (one i).snd public export record SomeOPE n where constructor MkOPE + {0 scope : Nat} {mask : Nat} - 0 ope : OPE m n mask + 0 ope : OPE scope n mask diff --git a/lib/Quox/Thin/Coprod.idr b/lib/Quox/Thin/Coprod.idr index c84008e..ca56c08 100644 --- a/lib/Quox/Thin/Coprod.idr +++ b/lib/Quox/Thin/Coprod.idr @@ -6,36 +6,166 @@ import public Quox.Thin.View import public Quox.Thin.List import public Quox.Thin.Cover import Data.DPair +import Data.Nat +import Control.Function %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 + +namespace Coprod + public export + data Comps : OPE scope n scopeMask -> + OPEList scope -> OPEList n -> Type where + Nil : Comps sub [] [] + (::) : Comp sub inner full -> + Comps sub inners fulls -> + Comps sub (inner :: inners) (full :: fulls) + %name Comps comps + + public export + record Coprod (fulls : OPEList n) where + constructor MkCoprod + {scopeMask : Nat} + {0 sub : OPE scope n scopeMask} + inners : OPEList scope + 0 comps : Comps sub inners fulls + 0 cov : Cover inners + %name Coprod 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) +0 compsLength : Comps s ts us -> length ts = length us +compsLength [] = Refl +compsLength (_ :: comps) = cong S $ compsLength comps --- [todo] n-ary coprod + +export +coprodNil : Coprod [] +coprodNil = MkCoprod [] [] [] {sub = zero} + +private +coprodHead : {n : Nat} -> (opes : OPEList (S n)) -> + Either (Cover1 opes) (All IsDrop opes) +coprodHead [] = Right [] +coprodHead (ope :: opes) = case view ope of + DropV {} => case coprodHead opes of + Left cov1 => Left $ There cov1 + Right drops => Right $ ItIsDrop :: drops + KeepV {} => Left Here + + +private +0 compsConsDrop : (opes : OPEList (S n)) -> + All IsDrop opes -> + All2 IsTail opes tails -> + Comps sub inners tails -> Comps (drop sub) inners opes +compsConsDrop [] [] [] [] = [] +compsConsDrop (Drop ope Refl :: opes) (ItIsDrop :: ds) (DropT :: ts) (c :: cs) = + DropZ c :: compsConsDrop opes ds ts cs +compsConsDrop (_ :: _) [] _ _ impossible + +private +coprodConsDrop : (0 opes : OPEList (S n)) -> + (0 ds : All IsDrop opes) -> + (0 ts : All2 IsTail opes tails) -> + Coprod tails -> Coprod opes +coprodConsDrop opes ds ts (MkCoprod inners comps cov) = + MkCoprod inners (compsConsDrop opes ds ts comps) cov + + +private +copyHeads : {m : Nat} -> + (src : OPEList (S m)) -> (tgt : OPEList n) -> + (0 eq : length src = length tgt) => OPEList (S n) +copyHeads [] [] = [] +copyHeads (s :: ss) (t :: ts) = + case view s of + DropV mask ope => drop t :: copyHeads ss ts @{inj S eq} + KeepV mask ope => keep t :: copyHeads ss ts @{inj S eq} + +private +0 copyHeadsComps : (eq : length outers = length inners) -> + All2 IsTail outers tails -> + Comps sub inners tails -> + Comps (keep sub) (copyHeads outers inners) outers +copyHeadsComps _ [] [] = [] +copyHeadsComps eq (DropT {eq = eq2} :: ps) ((c :: cs) {full}) = + let (Refl) = eq2 in -- coverage checker weirdness + rewrite viewDrop full Refl in + KDZ c :: copyHeadsComps (inj S eq) ps cs +copyHeadsComps eq (KeepT {eq = eq2} :: ps) ((c :: cs) {full}) = + let (Refl) = eq2 in + rewrite viewKeep full Refl in + KeepZ c :: copyHeadsComps (inj S eq) ps cs + +-- should be erased (coverage checker weirdness) +-- it is possibly https://github.com/idris-lang/Idris2/issues/1417 that keeps +-- happening. not 100% sure +private +cover1CopyHeads : {m : Nat} -> + (ss : OPEList (S m)) -> (ts : OPEList n) -> + (eq : length ss = length ts) -> + (cov1 : Cover1 ss) -> Cover1 (copyHeads ss ts) +cover1CopyHeads (Keep s Refl :: ss) (t :: ts) eq Here = + rewrite viewKeep s Refl in Here +cover1CopyHeads (s :: ss) (t :: ts) eq (There c) with (view s) + cover1CopyHeads (Drop {} :: ss) (t :: ts) eq (There c) | DropV {} = + There $ cover1CopyHeads ss ts (inj S eq) c + cover1CopyHeads (Keep {} :: ss) (t :: ts) eq (There c) | KeepV {} = + Here + +private +copyHeadsTails : {m : Nat} -> + (ss : OPEList (S m)) -> (ts : OPEList n) -> + (eq : length ss = length ts) -> + All2 IsTail (copyHeads ss ts) ts +copyHeadsTails [] [] eq = [] +copyHeadsTails (s :: ss) (t :: ts) eq with (view s) + copyHeadsTails (Drop ope Refl :: ss) (t :: ts) eq | DropV mask ope = + DropT :: copyHeadsTails ss ts (inj S eq) + copyHeadsTails (Keep ope Refl :: ss) (t :: ts) eq | KeepV mask ope = + KeepT :: copyHeadsTails ss ts (inj S eq) + +private +coprodConsKeep : {n : Nat} -> + (opes : OPEList (S n)) -> + {0 tails : OPEList n} -> + (cov1 : Cover1 opes) -> + (0 ts : All2 IsTail opes tails) -> + Coprod tails -> Coprod opes +coprodConsKeep opes cov1 ts (MkCoprod inners comps cov) = + MkCoprod + (copyHeads opes inners @{all2Length ts `trans` sym (compsLength comps)}) + (copyHeadsComps _ ts comps) + ((cover1CopyHeads {cov1, _} :: cov) @{copyHeadsTails {}}) + + +export +coprod : {n : Nat} -> (opes : OPEList n) -> Coprod opes + +private +coprod0 : (opes : OPEList 0) -> Coprod opes + +private +coprodS : {n : Nat} -> (opes : OPEList (S n)) -> Coprod opes + +coprod {n = 0} opes = coprod0 opes +coprod {n = S n} opes = coprodS opes + +coprod0 [] = coprodNil +coprod0 (ope :: opes) with %syntactic 0 (zeroIsStop ope) | (coprod opes) + coprod0 (Stop :: opes) + | ItIsStop | MkCoprod {sub} inners comps cov + with %syntactic 0 (zeroIsStop sub) + coprod0 (Stop :: opes) + | ItIsStop | MkCoprod {sub = Stop} inners comps cov | ItIsStop + = MkCoprod (Stop :: inners) (StopZ :: comps) [] + +coprodS [] = coprodNil +coprodS opes = + let hs = heads opes + Element ts tprf = tails_ opes + tcop = coprod $ assert_smaller opes ts + in + case coprodHead opes of + Left cov1 => coprodConsKeep opes cov1 tprf tcop + Right drops => coprodConsDrop opes drops tprf tcop diff --git a/lib/Quox/Thin/Cover.idr b/lib/Quox/Thin/Cover.idr index 886a1b3..7ef48c4 100644 --- a/lib/Quox/Thin/Cover.idr +++ b/lib/Quox/Thin/Cover.idr @@ -24,3 +24,4 @@ data Cover1 where Here : Cover1 (Keep ope eq :: opes) There : Cover1 opes -> Cover1 (ope :: opes) %name Cover1 cov1 +%builtin Natural Cover1 diff --git a/lib/Quox/Thin/List.idr b/lib/Quox/Thin/List.idr index 5d8c7b2..f0532dd 100644 --- a/lib/Quox/Thin/List.idr +++ b/lib/Quox/Thin/List.idr @@ -16,17 +16,17 @@ data OPEList : Nat -> Type where (::) : {mask : Nat} -> (0 ope : OPE m n mask) -> OPEList n -> OPEList n %name OPEList opes -export +public export length : OPEList n -> Nat length [] = 0 length (_ :: opes) = S $ length opes -export +public export toList : OPEList n -> List (SomeOPE n) toList [] = [] toList (ope :: opes) = MkOPE ope :: toList opes -export +public export fromList : List (SomeOPE n) -> OPEList n fromList [] = [] fromList (MkOPE ope :: xs) = ope :: fromList xs @@ -56,6 +56,11 @@ namespace All2 All2 p (a :: as) (b :: bs) %name All2.All2 ps, qs +export +0 all2Length : {p : Rel m n} -> All2 p ss ts -> length ss = length ts +all2Length [] = Refl +all2Length (p :: ps) = cong S $ all2Length ps + namespace Any public export data Any : Pred n -> OPEList n -> Type where @@ -108,7 +113,6 @@ 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) diff --git a/lib/Quox/Thin/View.idr b/lib/Quox/Thin/View.idr index 1d60bef..912001d 100644 --- a/lib/Quox/Thin/View.idr +++ b/lib/Quox/Thin/View.idr @@ -74,3 +74,19 @@ outerInnerZero Stop = Refl export 0 outerMaskZero : OPE m 0 mask -> mask = 0 outerMaskZero Stop = Refl + +export +0 viewStop : view Stop = StopV +viewStop = Refl + +export +0 viewDrop : (ope : OPE m n mask) -> (eq : mask2 = mask + mask) -> + view (Drop {mask} ope eq) = DropV mask ope +viewDrop ope eq with (view (Drop ope eq)) + viewDrop ope Refl | DropV _ ope = Refl + +export +0 viewKeep : (ope : OPE m n mask) -> (eq : mask2 = S (mask + mask)) -> + view (Keep {mask} ope eq) = KeepV mask ope +viewKeep ope eq with (view (Keep ope eq)) + viewKeep ope Refl | KeepV _ ope = Refl