Nat fixes

demos/contractBasics.tri

@@ -8,8 +8,8 @@ myAndC = (c1 c2 value rest :
     (c1 value rest))
 
 -- Plain predicates lifted into contracts with a diagnostic message.
-natural? = guardC "natural" (n : gte? n 0)
+natural? = guardC "natural" isNat?
-nonZero? = guardC "non-zero" (n : not? (isZero? n))
+nonZero? = guardC "non-zero" (n : and? (isNat? n) (not? (isZero_? n)))
 
 -- Phantom annotations let point-free definitions carry their own contracts.
 -- The base library now uses the same syntax, so head/tail/div etc. are

lib/base.tri

@@ -176,7 +176,7 @@ andLazy? = (a bK :
     bK
     (_ : false))
 
-pred = y (self : triage
+pred_ = y (self : triage
   0
   0
   (bit rest :
@@ -188,81 +188,90 @@ pred = y (self : triage
         rest)
       (_ : t (t t) (self rest))))
 
-isZero? = triage true (_ : false) (_ _ : false)
+pred @nat? =@nat? pred_
+
+isZero_? = triage true (_ : false) (_ _ : false)
+
+isZero? @nat? =@bool? isZero_?
 
 add @nat? @nat? =@nat? (y (self x y :
   triage
     y
     (_ : succ y)
-    (_ _ : succ (self (pred x) y))
+    (_ _ : succ (self (pred_ x) y))
     x))
 
 sub @nat? @nat? =@nat? y (self a b :
   ifLazy
-    (isZero? b)
+    (isZero_? b)
     (_ : a)
-    (_ : self (pred a) (pred b)))
+    (_ : self (pred_ a) (pred_ b)))
 
-lte? = y (self a b :
+lte_? = y (self a b :
   ifLazy
-    (isZero? a)
+    (isZero_? a)
     (_ : true)
     (_ :
       ifLazy
-        (isZero? b)
+        (isZero_? b)
         (_ : false)
-        (_ : self (pred a) (pred b))))
+        (_ : self (pred_ a) (pred_ b))))
 
-gte? = a b :
+lte? @nat? @nat? =@bool? lte_?
-  lte? b a
 
-lt? = a b :
+gte_? = a b : lte_? b a
-  and? (lte? a b) (not? (equal? a b))
 
-gt? = a b :
+gte? @nat? @nat? =@bool? gte_?
-  lt? b a
+
+lt_? = a b : and? (lte_? a b) (not? (equal? a b))
+
+lt? @nat? @nat? =@bool? lt_?
+
+gt_? = a b : lt_? b a
+
+gt? @nat? @nat? =@bool? gt_?
 
 mul @nat? @nat? =@nat? y (self a b :
   ifLazy
-    (isZero? b)
+    (isZero_? b)
     (_ : 0)
-    (_ : add a (self a (pred b))))
+    (_ : add a (self a (pred_ b))))
 
 div @nat? @nat? =@nat? y (self a b :
   ifLazy
-    (isZero? b)
+    (isZero_? b)
     (_ : 0)
     (_ : ifLazy
-      (lt? a b)
+      (lt_? a b)
       (_ : 0)
       (_ : succ (self (sub a b) b))))
 
 mod @nat? @nat? =@nat? y (self a b :
   ifLazy
-    (isZero? b)
+    (isZero_? b)
     (_ : 0)
     (_ : ifLazy
-      (lt? a b)
+      (lt_? a b)
       (_ : a)
       (_ : self (sub a b) b)))
 
 pow @nat? @nat? =@nat? y (self a b :
   ifLazy
-    (isZero? b)
+    (isZero_? b)
     (_ : 1)
-    (_ : mul a (self a (pred b))))
+    (_ : mul a (self a (pred_ b))))
 
 even? n = (triage
   true
   (_ : false)
-  (bit _ : isZero? bit)
+  (bit _ : isZero_? bit)
   n)
 
 odd? = (n : not? (even? n))
 
-min @nat? @nat? =@nat? (a b : ifLazy (lte? a b) (_ : a) (_ : b))
+min @nat? @nat? =@nat? (a b : ifLazy (lte_? a b) (_ : a) (_ : b))
 
-max @nat? @nat? =@nat? (a b : ifLazy (lte? a b) (_ : b) (_ : a))
+max @nat? @nat? =@nat? (a b : ifLazy (lte_? a b) (_ : b) (_ : a))
 
 -- ---------------------------------------------------------------------------
 -- Result combinators
@@ -666,11 +675,26 @@ guardC = (msg predicate value rest :
     (_ : contractErr msg rest)
     (predicate value))
 
--- Natural number contract.
+-- Structural natural-number predicate.
-nat? = guardC "not a natural number" (n : gte? n 0)
+-- A natural is either Leaf (0) or Fork bit rest where bit is Leaf (even)
+-- or Stem Leaf (odd) and rest is itself a natural.
+isNat? = y (self n :
+  triage
+    true
+    (_ : false)
+    (bit r :
+      triage
+        (self r)
+        (_ : self r)
+        (_ _ : false)
+        bit)
+    n)
 
--- Non-zero number contract.
+-- Natural number contract.
-nonZero? = guardC "non-zero" (n : not? (isZero? n))
+nat? = guardC "not a natural number" isNat?
+
+-- Non-zero natural number contract.
+nonZero? = guardC "non-zero" (n : and? (isNat? n) (not? (isZero_? n)))
 
 -- Boolean contract.
 bool? = guardC "not a boolean" (b : or? (equal? b true) (equal? b false))

src/Frontend/ContractDesugar.hs

@@ -47,7 +47,16 @@ desugarDefAnn name args ret body
     body' = wrapReturn ret body
 
     okCont = SLambda ["r"] (SVar "r" Nothing)
-    errCont = SLambda ["msg"] (SVar "msg" Nothing)
+    -- | Failure continuation used for the final argument contract or the
+    -- result contract. It returns the diagnostic message directly because
+    -- no further arguments are expected.
+    errContFinal = SLambda ["msg"] (SVar "msg" Nothing)
+    -- | Failure continuation used for non-final argument contracts. It
+    -- returns a function that ignores the next argument and then returns the
+    -- diagnostic message. This prevents a failed partial application from
+    -- being treated as the final result when the remaining arguments are
+    -- eventually supplied.
+    errContAbsorb = SLambda ["msg"] (SLambda ["_"] (SVar "msg" Nothing))
 
     isPhantom (DefPhantom _) = True
     isPhantom _              = False
@@ -57,15 +66,16 @@ desugarDefAnn name args ret body
 
     wrapReturn Nothing b = b
     wrapReturn (Just c) b =
-      withContractE (viewExprToAst c) b okCont errCont
+      withContractE (viewExprToAst c) b okCont errContFinal
 
     wrapArgs [] b = b
     wrapArgs (DefBinder nm Nothing : rest) b = SLambda [nm] (wrapArgs rest b)
     wrapArgs (DefBinder nm (Just c) : rest) b =
-      SLambda [nm] $
+      let onFail = if null rest then errContFinal else errContAbsorb
+      in SLambda [nm] $
         withContractE (viewExprToAst c) (SVar nm Nothing)
           (SLambda [nm] (wrapArgs rest b))
-          errCont
+          onFail
     wrapArgs (DefPhantom _ : _) _ =
       error "phantom contract arguments are not yet supported by the frontend"