tricu

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

intensionalContracts.tri (1422B)

      1 !import "prelude" !Local
      2 
      3 -- Structural contracts that exploit Tree Calculus's intensional nature.
      4 -- These are not simple type tags; they recursively inspect the tree shape.
      5 
      6 -- Any value that is not Leaf.
      7 nonEmptyTree? = guardC "empty tree" (x : not? (isZero? x))
      8 
      9 -- Every internal node is a Fork with two children; Stems are not allowed.
     10 fullTree? = guardC "not a full binary tree"
     11   (y (self x :
     12     triage
     13       true
     14       (_ : false)
     15       (l r : and? (self l) (self r))
     16       x))
     17 
     18 -- Even and odd number contracts that inspect the LSB bit tree.
     19 evenC? = guardC "not even" even?
     20 oddC?  = guardC "not odd" odd?
     21 
     22 -- A power of two has exactly one '1' bit in its LSB encoding.
     23 powerOfTwo? = guardC "not a power of two"
     24   (y (self n :
     25     triage
     26       false
     27       true
     28       (bit rest :
     29         matchBool
     30           (self rest)
     31           false
     32           (isZero? bit))
     33       n))
     34 
     35 -- A string (list of numbers) where every code point is in the ASCII range.
     36 asciiString? = listOf
     37   (guardC "non-ascii byte" (n : and? (gte? n 0) (lte? n 127)))
     38 
     39 -- Check that a list of numbers is sorted in ascending order.
     40 -- The element contract parameter is applied separately by listOf.
     41 isSorted_ = (self xs :
     42   matchList
     43     true
     44     (h r :
     45       matchBool
     46         (self r)
     47         false
     48         (matchList true (h2 _ : lte? h h2) r))
     49     xs)
     50 
     51 isSorted = y isSorted_
     52 
     53 sortedList? = (c : andC (listOf c) (guardC "not sorted" isSorted))