tricu

An interpreted language for exploring Tree Calculus
Log | Files | Refs | README | LICENSE

contractBasics.tri (924B)

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