fix nat elim quantities

lib/Quox/Syntax/Qty.idr

@@ -10,9 +10,10 @@ import Data.DPair
 
 public export
 interface Eq q => IsQty q where
-  zero, one : q
-  (+),  (*) : q -> q -> q
-  lub       : q -> q -> Maybe q
+  zero, one, any : q
+
+  (+), (*) : q -> q -> q
+  lub      : q -> q -> Maybe q
 
   ||| true if bindings of this quantity will be erased
   ||| and must not be runtime relevant
@@ -20,6 +21,12 @@ interface Eq q => IsQty q where
   isZero : Dec1 IsZero
   zeroIsZero : IsZero zero
 
+  ||| true if bindings of this quantity can be used any number of times.
+  ||| this is needed for natural elimination
+  IsAny : Pred q
+  isAny : Dec1 IsAny
+  anyIsAny : IsAny any
+
   ||| ``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
@@ -38,7 +45,8 @@ interface Eq q => IsQty q where
   ||| quantity. so not exact usage counts, maybe.
   IsGlobal : Pred q
   isGlobal : Dec1 IsGlobal
-  zeroIsGlobal : forall pi. IsZero pi -> IsGlobal zero
+  zeroIsGlobal : forall pi. IsZero pi -> IsGlobal pi
+  anyIsGlobal : forall pi. IsAny pi -> IsGlobal pi
 
   ||| prints in a form that can be a suffix of "case"
   prettySuffix : Pretty.HasEnv m => q -> m (Doc HL)
@@ -74,6 +82,10 @@ public export %inline
 gzero : IsQty q => GQty q
 gzero = Element zero $ zeroIsGlobal zeroIsZero
 
+public export %inline
+gany : IsQty q => GQty q
+gany = Element any $ anyIsGlobal anyIsAny
+
 export %inline
 globalToSubj : IsQty q => GQty q -> SQty q
 globalToSubj q = if isYes $ isZero q.fst then szero else sone

lib/Quox/Syntax/Qty/Three.idr

@@ -106,6 +106,7 @@ public export
 IsQty Three where
   zero = Zero
   one  = One
+  any  = Any
 
   (+) = plus
   (*) = times
@@ -116,6 +117,10 @@ IsQty Three where
   isZero     = decEq Zero
   zeroIsZero = Refl
 
+  IsAny    = Equal Three.Any
+  isAny    = decEq Any
+  anyIsAny = Refl
+
   Compat = Compat3
   compat = compat3
 
@@ -128,6 +133,7 @@ IsQty Three where
   IsGlobal     = IsGlobal3
   isGlobal     = isGlobal3
   zeroIsGlobal = \Refl => GZero
+  anyIsGlobal  = \Refl => GAny
 
   prettySuffix = pretty0M
 

lib/Quox/Typechecker.idr

@@ -386,16 +386,13 @@ parameters {auto _ : IsQty q}
         sucCtx    = extendTyN [< (pisg, p, Nat), (pi', ih, ret.term)] ctx
         sucType   = substCaseSuccRet ret
     sucout :< qp :< qih <- checkC sucCtx sg suc.term sucType
-    let Just armout = lubs ctx [zerout, sucout]
-          | _ => throw $ 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 ∧ Σs)
+    -- then Ψ | Γ ⊢ case ⋯ ⇒ A[n] ⊳ πΣn + Σz + ωΣs
     pure $ InfRes {
       type = sub1 ret n,
-      qout = pi * nres.qout + armout
+      qout = pi * nres.qout + zerout + any * sucout
     }
 
   infer' ctx sg (CaseBox pi box ret body) = do