tricu

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

intensionalContracts.tri (1408B)

      1 !import base *
      2 !export *
      3 
      4 -- Structural checks inspect arbitrary trees, not checked numeric operations.
      5 nonEmptyTree? = guardC "empty tree" (value : not? (isZero_? value))
      6 
      7 fullTree? = (guardC "not a full binary tree" full
      8   where rec
      9     full value = (triage true (_ : false)
     10       (left right : and? (full left) (full right)) value))
     11 
     12 -- Numeric contracts validate shape before inspecting bits or comparing values.
     13 evenC? = andC nat? (guardC "not even" even?)
     14 oddC? = andC nat? (guardC "not odd" odd?)
     15 
     16 -- Exactly one set bit in a validated canonical natural.
     17 powerOfTwo? = (andC nat? (guardC "not a power of two" oneBit)
     18   where rec
     19     oneBit remaining = (triage
     20       false
     21       (_ : false)
     22       (bit rest : case bit of
     23         t = oneBit rest
     24         _ = isZero_? rest)
     25       remaining))
     26 
     27 asciiString? = listOf (andC nat?
     28   (guardC "non-ascii byte" (value : lte_? value 127)))
     29 
     30 -- Sortedness has a natural-number domain; a caller's element contract may be
     31 -- weaker than nat?, so it is not sufficient validation for this comparison.
     32 isSorted xs = (let rec
     33   ordered previous remaining = case remaining of
     34     [] = true
     35     [next | rest] = (and? (isNat? next)
     36       (and? (lte_? previous next) (ordered next rest)))
     37     _ = false
     38   in case xs of
     39     [] = true
     40     [first | rest] = and? (isNat? first) (ordered first rest)
     41     _ = false)
     42 
     43 sortedList? c = andC (listOf c) (guardC "not sorted" isSorted)