(n-ary) coprod

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

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
+namespace Coprod
-  constructor MkCoprod2
+  public export
-  {sizeMask  : Nat}
+  data Comps : OPE scope n scopeMask ->
-  {leftMask  : Nat}
+               OPEList scope -> OPEList n -> Type where
-  {rightMask : Nat}
+    Nil  : Comps sub [] []
-  {0 sub     : OPE size n sizeMask}
+    (::) : Comp  sub inner  full ->
-  {0 left    : OPE m1 size leftMask}
+           Comps sub inners fulls ->
-  {0 right   : OPE m2 size rightMask}
+           Comps sub (inner :: inners) (full :: fulls)
-  0 leftComp  : Comp sub left  ope1
+  %name Comps comps
-  0 rightComp : Comp sub right ope2
+
-  {auto 0 isCover : Cover [left, right]}
+  public export
-%name Coprod2 cop
+  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 compsLength : Comps s ts us -> length ts = length us
-          (0 ope1 : OPE m1 n mask1) -> (0 ope2 : OPE m2 n mask2) ->
+compsLength []           = Refl
-          Coprod2 ope1 ope2
+compsLength (_ :: comps) = cong S $ compsLength comps
-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
+
+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

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

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)

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