From 773f6372ea0c692a334e2153d2d95294c6b7ddae Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Mon, 27 Mar 2023 00:01:32 +0200
Subject: [PATCH] quantities in case don't need to be *exactly* the same
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

...as long as they are all compatible with the target.
for example, given ω.n : ℕ:
```
  case double_it? return ℕ of {
    'true  ⇒ plus n n;
    'false ⇒ n
  }
```
---
 lib/Quox/Context.idr          | 40 +++++++++++++++++++----------
 lib/Quox/Syntax/Qty.idr       |  7 ++---
 lib/Quox/Syntax/Qty/Three.idr |  9 +++++++
 lib/Quox/Typechecker.idr      | 48 ++++++++++++++++++++---------------
 lib/Quox/Typing/Error.idr     |  4 +--
 5 files changed, 69 insertions(+), 39 deletions(-)

diff --git a/lib/Quox/Context.idr b/lib/Quox/Context.idr
index d5b8600..450406a 100644
--- a/lib/Quox/Context.idr
+++ b/lib/Quox/Context.idr
@@ -41,33 +41,47 @@ NContext : Nat -> Type
 NContext = Context' BaseName
 
 
+public export
+unsnoc : Context tm (S n) -> (Context tm n, tm n)
+unsnoc (tel :< x) = (tel, x)
+
 public export
 head : Context tm (S n) -> tm n
-head (_ :< t) = t
+head = snd . unsnoc
 
 public export
 tail : Context tm (S n) -> Context tm n
-tail (tel :< _) = tel
+tail = fst . unsnoc
 
-export
-toSnocList : Telescope tm _ _ -> SnocList (Exists tm)
-toSnocList [<]        = [<]
-toSnocList (tel :< t) = toSnocList tel :< Evidence _ t
+parameters {0 tm : Nat -> Type} (f : forall n. tm n -> a)
+  export
+  toSnocListWith : Telescope tm _ _ -> SnocList a
+  toSnocListWith [<]        = [<]
+  toSnocListWith (tel :< t) = toSnocListWith tel :< f t
+
+  export
+  toListWith : Telescope tm _ _ -> List a
+  toListWith tel = toListAcc tel [] where
+    toListAcc : Telescope tm _ _ -> List a -> List a
+    toListAcc [<]        acc = acc
+    toListAcc (tel :< t) acc = toListAcc tel (f t :: acc)
 
 export %inline
-toList : Telescope tm _ _ -> List (Exists tm)
-toList tel = toListAcc tel [] where
-  toListAcc : Telescope tm _ _ -> List (Exists tm) -> List (Exists tm)
-  toListAcc [<]        acc = acc
-  toListAcc (tel :< t) acc = toListAcc tel (Evidence _ t :: acc)
+toSnocList : Telescope tm _ _ -> SnocList (Exists tm)
+toSnocList = toSnocListWith (Evidence _)
 
 export %inline
 toSnocList' : Telescope' a _ _ -> SnocList a
-toSnocList' = map snd . toSnocList
+toSnocList' = toSnocListWith id
+
+export %inline
+toList : Telescope tm _ _ -> List (Exists tm)
+toList = toListWith (Evidence _)
 
 export %inline
 toList' : Telescope' a _ _ -> List a
-toList' = map snd . toList
+toList' = toListWith id
+
 
 export
 fromSnocVect : SnocVect n a -> Context' a n
diff --git a/lib/Quox/Syntax/Qty.idr b/lib/Quox/Syntax/Qty.idr
index 5c3a980..4e597c0 100644
--- a/lib/Quox/Syntax/Qty.idr
+++ b/lib/Quox/Syntax/Qty.idr
@@ -12,6 +12,7 @@ public export
 interface Eq q => IsQty q where
   zero, one : q
   (+),  (*) : q -> q -> q
+  lub       : q -> q -> Maybe q
 
   ||| true if bindings of this quantity will be erased
   ||| and must not be runtime relevant
@@ -19,9 +20,9 @@ interface Eq q => IsQty q where
   isZero : Dec1 IsZero
   zeroIsZero : IsZero zero
 
-  ||| ``p `Compat` q`` if it is ok for a binding of
-  ||| quantity `q` to be used exactly `p` times.
-  ||| e.g. ``1 `Compat` 1``, ``1 `Compat` ω``
+  ||| ``p `Compat` q`` if it is ok for a binding of quantity `q` to be used
+  ||| exactly `p` times. e.g. ``1 `Compat` 1``, ``1 `Compat` ω``.
+  ||| if ``π `lub` ρ`` exists, then both `π` and `ρ` must be compatible with it
   Compat : Rel q
   compat : Dec2 Compat
 
diff --git a/lib/Quox/Syntax/Qty/Three.idr b/lib/Quox/Syntax/Qty/Three.idr
index 6713036..2c05a8f 100644
--- a/lib/Quox/Syntax/Qty/Three.idr
+++ b/lib/Quox/Syntax/Qty/Three.idr
@@ -50,6 +50,13 @@ times One  rh   = rh
 times pi   One  = pi
 times Any  Any  = Any
 
+public export
+lub3 : Three -> Three -> Maybe Three
+lub3 p q =
+  if p == Any || q == Any then Just Any
+  else if p == q then Just p
+  else Nothing
+
 public export
 data Compat3 : Rel Three where
   CmpRefl : Compat3 rh rh
@@ -103,6 +110,8 @@ IsQty Three where
   (+) = plus
   (*) = times
 
+  lub = lub3
+
   IsZero     = Equal Zero
   isZero     = decEq Zero
   zeroIsZero = Refl
diff --git a/lib/Quox/Typechecker.idr b/lib/Quox/Typechecker.idr
index b71b50b..4135681 100644
--- a/lib/Quox/Typechecker.idr
+++ b/lib/Quox/Typechecker.idr
@@ -5,6 +5,7 @@ import public Quox.Equal
 
 import Data.List
 import Data.SnocVect
+import Data.List1
 
 %default total
 
@@ -18,16 +19,28 @@ public export
 CanTC q = CanTC' q IsGlobal
 
 
-private
+export
 popQs : HasErr q m => IsQty q =>
         QOutput q s -> QOutput q (s + n) -> m (QOutput q n)
 popQs [<]         qout         = pure qout
 popQs (pis :< pi) (qout :< rh) = do expectCompatQ rh pi; popQs pis qout
 
-private %inline
+export %inline
 popQ : HasErr q m => IsQty q => q -> QOutput q (S n) -> m (QOutput q n)
 popQ pi = popQs [< pi]
 
+export
+lubs1 : IsQty q => List1 (QOutput q n) -> Maybe (QOutput q n)
+lubs1 ([<] ::: _) = Just [<]
+lubs1 ((qs :< p) ::: pqs) =
+  let (qss, ps) = unzip $ map unsnoc pqs in
+  [|lubs1 (qs ::: qss) :< foldlM lub p ps|]
+
+export
+lubs : IsQty q => TyContext q d n -> List (QOutput q n) -> Maybe (QOutput q n)
+lubs ctx []        = Just $ zeroFor ctx
+lubs ctx (x :: xs) = lubs1 $ x ::: xs
+
 
 parameters {auto _ : IsQty q} {auto _ : CanTC q m}
  mutual
@@ -329,19 +342,13 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     unless (ttags == armTags) $ throwError $ BadCaseEnum ttags armTags
     armres <- for arms $ \(a, s) =>
       checkC ctx sg s (sub1 ret (Tag a :# tres.type))
-    armout <- allEqual (zip armres arms)
-    -- then Ψ | Γ ⊢ σ · case ⋯ ⇒ ret[t/x] ⊳ πΣ₁ + Σ₂
+    let Just armout = lubs ctx armres
+          | _ => throwError $ BadCaseQtys ctx $
+              zipWith (\qs, (t, rhs) => (qs, Tag t)) armres arms
     pure $ InfRes {
       type = sub1 ret t,
       qout = pi * tres.qout + armout
     }
-   where
-    allEqual : List (QOutput q n, TagVal, Term q d n) -> m (QOutput q n)
-    allEqual [] = pure $ zeroFor ctx
-    allEqual lst@((x, _) :: xs) =
-      if all (\y => x == fst y) xs then pure x
-      else throwError $ BadCaseQtys ctx $
-             map (\(qs, t, s) => (qs, Tag t, s)) lst
 
   infer' ctx sg (CaseNat pi pi' n ret zer suc) = do
     -- if 1 ≤ π
@@ -354,30 +361,29 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     -- if Ψ | Γ ⊢ σ · zer ⇐ A[0 ∷ ℕ/n] ⊳ Σz
     zerout <- checkC ctx sg zer (sub1 ret (Zero :# Nat))
     -- if Ψ | Γ, n : ℕ, ih : A ⊢ σ · suc ⇐ A[succ p ∷ ℕ/n] ⊳ Σs, ρ₁.p, ρ₂.ih
-    -- with Σz = Σs, (ρ₁ + ρ₂) ≤ πσ
+    -- with ρ₂ ≤ π'σ, (ρ₁ + ρ₂) ≤ πσ
     let [< p, ih] = suc.names
         pisg      = pi * sg.fst
         sucCtx    = extendTyN [< (pisg, p, Nat), (pi', ih, ret.term)] ctx
         sucType   = substCaseNatRet ret
     sucout :< qp :< qih <- checkC sucCtx sg suc.term sucType
-    unless (zerout == sucout) $ do
-      let sucp = Succ $ FT $ unq p
-          suc  = subN suc [< F $ unq p, F $ unq ih]
-      throwError $ BadCaseQtys ctx [(zerout, Zero, zer), (sucout, sucp, suc)]
-    expectCompatQ qih pi'
+    let Just armout = lubs ctx [zerout, sucout]
+          | _ => throwError $ BadCaseQtys ctx $
+              [(zerout, Zero), (sucout, Succ $ FT $ unq p)]
+    expectCompatQ qih (pi' * sg.fst)
     -- [fixme] better error here
     expectCompatQ (qp + qih) pisg
-    -- then Ψ | Γ ⊢ case ⋯ ⇒ A[n] ⊳ πΣn + Σz
+    -- then Ψ | Γ ⊢ case ⋯ ⇒ A[n] ⊳ πΣn + (Σz ∧ Σs)
     pure $ InfRes {
       type = sub1 ret n,
-      qout = pi * nres.qout + zerout
+      qout = pi * nres.qout + armout
     }
 
   infer' ctx sg (fun :% dim) = do
-    -- if Ψ | Γ ⊢ σ · f ⇒ Eq [i ⇒ A] l r ⊳ Σ
+    -- if Ψ | Γ ⊢ σ · f ⇒ Eq [𝑖 ⇒ A] l r ⊳ Σ
     InfRes {type, qout} <- inferC ctx sg fun
     ty <- fst <$> expectEq !ask ctx type
-    -- then Ψ | Γ ⊢ σ · f p ⇒ A‹p› ⊳ Σ
+    -- then Ψ | Γ ⊢ σ · f p ⇒ A‹p/𝑖› ⊳ Σ
     pure $ InfRes {type = dsub1 ty dim, qout}
 
   infer' ctx sg (term :# type) = do
diff --git a/lib/Quox/Typing/Error.idr b/lib/Quox/Typing/Error.idr
index aa73237..92778b1 100644
--- a/lib/Quox/Typing/Error.idr
+++ b/lib/Quox/Typing/Error.idr
@@ -21,7 +21,7 @@ data Error q
 | BadUniverse  Universe Universe
 | TagNotIn     TagVal (SortedSet TagVal)
 | BadCaseEnum  (SortedSet TagVal) (SortedSet TagVal)
-| BadCaseQtys  (TyContext q d n) (List (QOutput q n, Term q d n, Term q d n))
+| BadCaseQtys  (TyContext q d n) (List (QOutput q n, Term q d n))
 
 -- first term arg of ClashT is the type
 | ClashT  (EqContext q n) EqMode (Term q 0 n) (Term q 0 n) (Term q 0 n)
@@ -167,7 +167,7 @@ parameters {auto _ : (Eq q, IsQty q, PrettyHL q)} (unicode : Bool)
 
   private
   dissectCaseQtys : TyContext q d n ->
-                    NContext n' -> List (QOutput q n', y, z) ->
+                    NContext n' -> List (QOutput q n', z) ->
                     List (Doc HL)
   dissectCaseQtys ctx [<]        arms = []
   dissectCaseQtys ctx (tel :< x) arms =