contractBasics.tri (917B)
1 !import "prelude" !Local 2 3 -- Custom contract combinators built directly on matchResult. 4 myAndC = (c1 c2 value rest : 5 matchResult 6 (msg _ : contractErr msg rest) 7 (v _ : c2 v rest) 8 (c1 value rest)) 9 10 -- Plain predicates lifted into contracts with a diagnostic message. 11 natural? = guardC "natural" isNat? 12 nonZero? = guardC "non-zero" (n : and? (isNat? n) (not? (isZero_? n))) 13 14 -- Phantom annotations let point-free definitions carry their own contracts. 15 -- The base library now uses the same syntax, so head/tail/div etc. are 16 -- guarded by default. 17 myHead @(nonEmptyListOf anyC) =@anyC head 18 myTail @(listOf anyC) =@(listOf anyC) tail 19 myDiv @natural? @(myAndC natural? nonZero?) =@natural? div 20 21 -- The `check` helper applies a contract to any value and returns the 22 -- checked value (or the diagnostic message on failure). 23 checkedSuccessor = check natural? (add 1 2) 24 25 main = pair checkedSuccessor (myDiv 10 2)