From b822e7e71334fd92d77c4f8a0a83dded920cc51e Mon Sep 17 00:00:00 2001 From: James Eversole Date: Tue, 1 Sep 2026 12:54:26 -0500 Subject: [PATCH] Nat fixes --- demos/contractBasics.tri | 4 +- lib/base.tri | 84 +++++++++++++++++++++------------ src/Frontend/ContractDesugar.hs | 18 +++++-- 3 files changed, 70 insertions(+), 36 deletions(-) diff --git a/demos/contractBasics.tri b/demos/contractBasics.tri index de284fa..92f4574 100644 --- a/demos/contractBasics.tri +++ b/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) -nonZero? = guardC "non-zero" (n : not? (isZero? n)) +natural? = guardC "natural" isNat? +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 diff --git a/lib/base.tri b/lib/base.tri index 11f4b3c..c0b5992 100644 --- a/lib/base.tri +++ b/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? b a +lte? @nat? @nat? =@bool? lte_? -lt? = a b : - and? (lte? a b) (not? (equal? a b)) +gte_? = a b : lte_? b a -gt? = a b : - lt? b a +gte? @nat? @nat? =@bool? gte_? + +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. -nat? = guardC "not a natural number" (n : gte? n 0) +-- Structural natural-number predicate. +-- 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. -nonZero? = guardC "non-zero" (n : not? (isZero? n)) +-- Natural number contract. +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)) diff --git a/src/Frontend/ContractDesugar.hs b/src/Frontend/ContractDesugar.hs index 52df607..d38b57e 100644 --- a/src/Frontend/ContractDesugar.hs +++ b/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"