tricu

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

6ec5686b652c5d5c51f11623bd99247b2a074ade4f47f9dd58d4f68cb137e684.tri (1425B)

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