tricu/lib/base.tri

false = t
_     = t
true  = t t
id a = a
const a b = a
pair  = t
if cond then else = t (t else (t t then)) t cond

y = ((mut wait fun : wait mut (x : fun (wait mut x)))
     (x : x x)
     (a0 a1 a2 : t (t a0) (t t a2) a1))

compose f g x = f (g x)

triage leaf stem fork = t (t leaf stem) fork
test   = triage "Leaf" (_ : "Stem") (_ _ : "Fork")

matchBool = (ot of : triage
  of
  (_ : ot)
  (_ _ : ot)
)

lAnd = (triage
  (_     : false)
  (_ x   : x)
  (_ _ x : x))

lOr = (triage
  (x     : x)
  (_ _   : true)
  (_ _ _ : true))

matchPair a = triage _ _ a

fst p = matchPair takeFirst p
  where takeFirst a b = a
snd p = matchPair takeSecond p
  where takeSecond a b = b

resultIsOk result =
  matchResult (err rest : false) (val rest : true) result

resultIsErr result =
  matchResult (err rest : true) (val rest : false) result

not? = matchBool false true
and? = matchBool id (_ : false)

or? = (x z : 
  matchBool 
    (matchBool true true z)
    (matchBool true false z)
    x)

xor? = (x z : 
  matchBool 
    (matchBool false true z)
    (matchBool true false z)
    x)

equal? = y (self : triage
  (triage
    true
    (_   : false)
    (_ _ : false))
  (ax :
    triage
      false
      (self ax)
      (_ _ : false))
  (ax ay :
    triage
      false
      (_ : false)
      (bx by : lAnd (self ax bx) (self ay by))))

succ = y (self :
  triage
    1
    t
    (triage
      (t (t t))
      (_ tail : t t (self tail))
      t))

ok value rest = pair true (pair value rest)
err msg rest = pair false (pair msg rest)

matchResult errCase okCase result =
  matchPair
    (tag payload :
      matchPair
        (value rest :
          matchBool
            (okCase value rest)
            (errCase value rest)
            tag)
        payload)
    result

-- ---------------------------------------------------------------------------
-- Maybe / Option type
-- ---------------------------------------------------------------------------

nothing = t
just x = t x

matchMaybe nothingCase justCase maybe =
  triage
    nothingCase
    justCase
    (_ _ : nothingCase)
    maybe

maybe default f m = matchMaybe default f m
maybeMap f m = matchMaybe nothing (x : just (f x)) m
maybeBind m f = matchMaybe nothing f m
maybeOr default m = matchMaybe default id m
maybe? = matchMaybe false (_ : true)

-- ---------------------------------------------------------------------------
-- Lazy eliminators
--
-- A strict eliminator evaluates both branches because they are ordinary
-- arguments. Give a branch that recurses, looks something up, or builds
-- structure to one of these instead: it becomes a thunk and only the selected
-- branch is ever applied.
-- ---------------------------------------------------------------------------

lazyBool = (thenK elseK cond :
  ((chosen : chosen t)
   (matchBool
     thenK
     elseK
     cond)))

-- This module has no list matcher, so `triage` is used directly: a cons is a
-- Fork, which is why the cons case sits in the fork slot, exactly as in
-- `matchList` in lib/list.tri.
lazyList = (nilK consK xs :
  ((chosen : chosen t)
   (triage
     nilK
     _
     (h r : (_ : consK h r))
     xs)))

lazyMaybe = (noneK someK m :
  ((chosen : chosen t)
   (matchMaybe
     noneK
     (x : (_ : someK x))
     m)))

lazyResult = (errK okK result :
  ((chosen : chosen t)
   (matchResult
     (code rest : (_ : errK code rest))
     (value rest : (_ : okK value rest))
     result)))

-- ---------------------------------------------------------------------------
-- Basic arithmetic
-- ---------------------------------------------------------------------------

ifLazy = (cond thenK elseK :
  matchBool
    (thenK t)
    (elseK t)
    cond)

andLazy? = (a bK :
  ifLazy
    a
    bK
    (_ : false))

pred = y (self : triage
  0
  0
  (bit rest :
    ifLazy
      bit
      (_ : matchBool
        (t t rest)
        0
        rest)
      (_ : t (t t) (self rest))))

isZero? = triage true (_ : false) (_ _ : false)

add @nat? @nat? =@nat? (y (self x y :
  triage
    y
    (_ : succ y)
    (_ _ : succ (self (pred x) y))
    x))

sub @nat? @nat? =@nat? y (self a b :
  ifLazy
    (isZero? b)
    (_ : a)
    (_ : self (pred a) (pred b)))

lte? = y (self a b :
  ifLazy
    (isZero? a)
    (_ : true)
    (_ :
      ifLazy
        (isZero? b)
        (_ : false)
        (_ : self (pred a) (pred b))))

gte? = a b :
  lte? b a

lt? = a b :
  and? (lte? a b) (not? (equal? a b))

gt? = a b :
  lt? b a

mul @nat? @nat? =@nat? y (self a b :
  ifLazy
    (isZero? b)
    (_ : 0)
    (_ : add a (self a (pred b))))

div @nat? @nat? =@nat? y (self a b :
  ifLazy
    (isZero? b)
    (_ : 0)
    (_ : ifLazy
      (lt? a b)
      (_ : 0)
      (_ : succ (self (sub a b) b))))

mod @nat? @nat? =@nat? y (self a b :
  ifLazy
    (isZero? b)
    (_ : 0)
    (_ : ifLazy
      (lt? a b)
      (_ : a)
      (_ : self (sub a b) b)))

pow @nat? @nat? =@nat? y (self a b :
  ifLazy
    (isZero? b)
    (_ : 1)
    (_ : mul a (self a (pred b))))

even? n = (triage
  true
  (_ : false)
  (bit _ : isZero? bit)
  n)

odd? = (n : not? (even? n))

min @nat? @nat? =@nat? (a b : ifLazy (lte? a b) (_ : a) (_ : b))

max @nat? @nat? =@nat? (a b : ifLazy (lte? a b) (_ : b) (_ : a))

-- ---------------------------------------------------------------------------
-- Result combinators
-- ---------------------------------------------------------------------------

mapResult = (f result :
  matchResult
    (code rest : err code rest)
    (value rest : ok (f value) rest)
    result)

bindResult = (result f :
  matchResult
    (code rest : err code rest)
    (value rest : f value rest)
    result)

resultOr = (default result :
  matchResult
    (_ _ : default)
    (value _ : value)
    result)

resultMapErr = (f result :
  matchResult
    (code rest : err (f code) rest)
    (value rest : ok value rest)
    result)

-- ---------------------------------------------------------------------------
-- List
-- ---------------------------------------------------------------------------

matchList = a b : triage a _ b

emptyList? = matchList true (_ _ : false)
head xs@(nonEmptyListOf anyC) =@anyC matchList t (h _ : h) xs
tail xs@(nonEmptyListOf anyC) =@(listOf anyC) matchList t (_ r : r) xs

append_ self xs ys =
  matchList
    ys
    (h r : pair h (self r ys))
    xs
append = xs ys : y append_ xs ys

lExist?_ self x xs =
  matchList
    false
    (h r : or? (equal? x h) (self x r))
    xs
lExist? = x xs : y lExist?_ x xs

map_ self l f =
  matchList
    t
    (h r : pair (f h) (self r f))
    l
map = f l : y map_ l f

filter_ self l f =
  matchList
    t
    (h r :
      matchBool
        (pair h (self r f))
        (self r f)
        (f h))
    l
filter = f l : y filter_ l f

foldl_ self l f acc =
  matchList
    acc
    (h r : self r f (f acc h))
    l
foldl = f x l : y foldl_ l f x

foldr_ self l f x =
  matchList
    x
    (h r : f (self r f x) h)
    l
foldr = f x l : y foldr_ l f x

length_ self xs =
  matchList
    0
    (_ r : succ (self r))
    xs
length @(listOf anyC) =@nat? y length_

reverse_ self xs acc =
  matchList
    acc
    (h r : self r (pair h acc))
    xs
reverse = xs : y reverse_ xs t

snoc_ self x xs =
  matchList
    (pair x t)
    (h r : pair h (self x r))
    xs
snoc = x xs : y snoc_ x xs

count_ self x xs =
  matchList
    0
    (h r :
      matchBool
        (succ (self x r))
        (self x r)
        (equal? x h))
    xs
count = x xs : y count_ x xs

last_ self xs =
  matchList
    t
    (h r :
      matchBool
        h
        (self r)
        (emptyList? r))
    xs
last @(nonEmptyListOf anyC) =@anyC y last_

all?_ self pred xs =
  matchList
    true
    (h r : and? (pred h) (self pred r))
    xs
all? = pred xs : y all?_ pred xs

any?_ self pred xs =
  matchList
    false
    (h r : or? (pred h) (self pred r))
    xs
any? = pred xs : y any?_ pred xs

intersect = xs ys : filter (x : lExist? x ys) xs

nth_ self xs n i =
  matchList
    t
    (h r :
      matchBool
        h
        (self r n (succ i))
        (equal? i n))
    xs
nth = n xs : y nth_ xs n 0

headMaybe = matchList nothing (h _ : just h)

lastMaybe_ self xs =
  matchList
    nothing
    (h r :
      matchBool
        (just h)
        (self r)
        (emptyList? r))
    xs
lastMaybe = xs : y lastMaybe_ xs

nthMaybe_ self xs n i =
  matchList
    nothing
    (h r :
      matchBool
        (just h)
        (self r n (succ i))
        (equal? i n))
    xs
nthMaybe = n xs : y nthMaybe_ xs n 0

take_ self xs n i =
  matchList
    t
    (h r :
      matchBool
        t
        (pair h (self r n (succ i)))
        (equal? i n))
    xs
take = n xs : y take_ xs n 0

drop_ self xs n i =
  matchBool
    xs
    (matchList
      t
      (_ r : self r n (succ i))
      xs)
    (equal? i n)
drop = n xs : y drop_ xs n 0

splitAt = n xs : pair (take n xs) (drop n xs)

concatMap_ self f xs =
  matchList
    t
    (h r : append (f h) (self f r))
    xs
concatMap = f xs : y concatMap_ f xs

find_ self pred xs =
  matchList
    nothing
    (h r :
      matchBool
        (just h)
        (self pred r)
        (pred h))
    xs
find = pred xs : y find_ pred xs

partition_ self pred xs trues falses =
  matchList
    (pair (reverse trues) (reverse falses))
    (h r :
      matchBool
        (self pred r (pair h trues) falses)
        (self pred r trues (pair h falses))
        (pred h))
    xs
partition = pred xs : y partition_ pred xs t t

strLength = length
strAppend = append
strEq? = equal?
strEmpty? = emptyList?

startsWith?_ self prefix input =
  matchList
    true
    (ph pr :
      matchList
        false
        (sh sr :
          matchBool
            (self pr sr)
            false
            (equal? ph sh))
        input)
    prefix
startsWith? = prefix input : y startsWith?_ prefix input

endsWith? = prefix str : startsWith? (reverse prefix) (reverse str)

contains?_ self needle haystack =
  matchBool
    true
    (matchList
      false
      (_ r : self needle r)
      haystack)
    (startsWith? needle haystack)
contains? = needle haystack : y contains?_ needle haystack

sum @(listOf nat?) =@nat? foldl (acc x : add x acc) 0
product @(listOf nat?) =@nat? foldl (acc x : mul x acc) 1

-- ---------------------------------------------------------------------------
-- Generic separators
--
-- `lines`, `unlines`, `words` and `unwords` at the bottom of this section are
-- the byte-valued special cases of these primitives.
--
-- Joining takes any separator; splitting takes one byte. Separators are removed
-- rather than kept, and empty fields are preserved.
-- ---------------------------------------------------------------------------

takeWhile_ self xs f =
  lazyList
    (_ : t)
    (h r :
      lazyBool
        (_ : pair h (self r f))
        (_ : t)
        (f h))
    xs
takeWhile = f xs : y takeWhile_ xs f

dropWhile_ self xs f =
  lazyList
    (_ : t)
    (h r :
      lazyBool
        (_ : self r f)
        (_ : pair h r)
        (f h))
    xs
dropWhile = f xs : y dropWhile_ xs f

-- Byte-level whitespace only: space and horizontal tab (HTTP OWS).
spaceByte? = b : equal? b 32
tabByte?   = b : equal? b 9
trimByte?  = b : or? (spaceByte? b) (tabByte? b)

trim = xs : dropWhile trimByte? (reverse (dropWhile trimByte? (reverse xs)))

intercalate_ self xs sep =
  lazyList
    (_ : t)
    (h r :
      lazyBool
        (_ : h)
        (_ : append h (append sep (self r sep)))
        (emptyList? r))
    xs
intercalate = sep xs : y intercalate_ xs sep

-- Separator after every field, including the last one. Line-oriented formats
-- want this: `joinSuffix "\n" xs` terminates the final line while
-- `intercalate "\n" xs` does not.
joinSuffix_ self xs sep =
  lazyList
    (_ : t)
    (h r : append (append h sep) (self r sep))
    xs
joinSuffix = sep xs : y joinSuffix_ xs sep

-- Split on a single byte. 
-- Empty fields are preserved: `splitOnByte 58 "a::b"` is ["a" "" "b"].
splitByte_ self str byte acc current =
  lazyList
    (_ : map reverse (reverse (pair current acc)))
    (h r :
      lazyBool
        (_ : self r byte (pair current acc) t)
        (_ : self r byte acc (pair h current))
        (equal? h byte))
    str
splitOnByte = byte str : y splitByte_ str byte t t

-- Every one of these keeps its arguments bound: partially applying a
-- multi-argument function at the top level leaves a fixed point exposed.
lines   = str : splitOnByte 10 str
unlines = xs : joinSuffix "\n" xs

-- Runs of separators collapse: empty fields are dropped.
words   = str : filter (w : not? (emptyList? w)) (splitOnByte 32 str)
unwords = xs : intercalate " " xs

zipWith_ self f xs ys =
  matchList
    t
    (xh xt :
      matchList
        t
        (yh yt : pair (f xh yh) (self f xt yt))
        ys)
    xs
zipWith = f xs ys : y zipWith_ f xs ys

-- ---------------------------------------------------------------------------
-- Core contract type
--
-- A contract is an ordinary tricu function: Tree -> Tree -> Result Tree Tree.
-- The second argument is the conventional "rest" slot. On success a contract
-- returns the checked value wrapped in the standard ok shape; on failure it
-- returns a diagnostic wrapped in the standard err shape.
-- ---------------------------------------------------------------------------

contractOk = (value : (rest : ok value rest))
contractErr = (msg : (rest : err msg rest))

check contract value =
  withContract contract value
    (x : x)
    (msg : msg)

-- Apply a contract with the conventional rest slot and return the raw Result.
checkContract = (contract value : contract value t)

-- Apply a contract and continue with either the onOk or onFail branch.
withContract = (contract value onOk onFail :
  matchResult
    (msg _ : onFail msg)
    (checked _ : onOk checked)
    (contract value t))

-- ---------------------------------------------------------------------------
-- Basic contracts
-- ---------------------------------------------------------------------------

-- Any value passes.
anyC = (value : contractOk value)

-- Always fails with the supplied message.
neverC = (msg : (value : contractErr msg))

-- Build a contract from a predicate that inspects only the value.
guardC = (msg predicate value rest :
  lazyBool
    (_ : contractOk value rest)
    (_ : contractErr msg rest)
    (predicate value))

-- Natural number contract.
nat? = guardC "not a natural number" (n : gte? n 0)

-- Non-zero number contract.
nonZero? = guardC "non-zero" (n : not? (isZero? n))

-- Boolean contract.
bool? = guardC "not a boolean" (b : or? (equal? b true) (equal? b false))

-- ---------------------------------------------------------------------------
-- Contract combinators
-- ---------------------------------------------------------------------------

andC = (c1 c2 value rest :
  matchResult
    (msg _ : contractErr msg rest)
    (v _ : c2 v rest)
    (c1 value rest))

orC = (c1 c2 value rest :
  matchResult
    (msg _ : c2 value rest)
    (v _ : contractOk v rest)
    (c1 value rest))

notC = (c value rest :
  matchResult
    (msg _ : contractOk value rest)
    (_ _ : contractErr "notC: predicate succeeded" rest)
    (c value rest))

mapC = (f c value rest :
  matchResult
    (msg _ : contractErr msg rest)
    (v _ : contractOk (f v) rest)
    (c value rest))

bindC = (c f value rest :
  matchResult
    (msg _ : contractErr msg rest)
    (v _ : f v value rest)
    (c value rest))

-- ---------------------------------------------------------------------------
-- Collection contracts
-- ---------------------------------------------------------------------------

listOf = (c value rest :
  y (self orig xs :
    matchList
      (contractOk orig rest)
      (h r :
        matchResult
          (msg _ : contractErr msg rest)
          (_ _ : self orig r)
          (c h rest))
      xs) value value)

nonEmptyListOf = (c :
  andC (guardC "empty list" (xs : not? (emptyList? xs))) (listOf c))

pairOf = (c1 c2 p rest :
  matchPair
    (a b :
      matchResult
        (msg _ : contractErr msg rest)
        (a' _ :
          matchResult
            (msg _ : contractErr msg rest)
            (b' _ : contractOk (pair a' b') rest)
            (c2 b rest))
        (c1 a rest))
    p)

-- ---------------------------------------------------------------------------
-- Higher-order function contracts
--
-- These return a Result-wrapped proxy. The proxy itself is a contract: it
-- checks arguments on the way in and results on the way out.
-- ---------------------------------------------------------------------------

fnContract = (argC resC f rest :
  contractOk
    (x : (rest1 :
      withContract argC x
        (x' :
          withContract resC (f x')
            (y : contractOk y rest1)
            (msg : contractErr msg rest1))
        (msg : contractErr msg rest1)))
    rest)

fn2 = (arg1C arg2C resC f rest :
  contractOk
    (x : (rest1 :
      withContract arg1C x
        (x' :
          contractOk
            (y : (rest2 :
              withContract arg2C y
                (y' :
                  withContract resC (f x' y')
                    (z : contractOk z rest2)
                    (msg : contractErr msg rest2))
                (msg : contractErr msg rest2)))
            rest1)
        (msg : contractErr msg rest1)))
    rest)

-- ---------------------------------------------------------------------------
-- Interaction-tree effect layer
--
-- These constructors and combinators layer catchable, composable failures on
-- top of the core Result contracts. They reuse the same tags as tricu IO:
--   0 = pureE
--   1 = bindE
--   2 = exceptE
-- ---------------------------------------------------------------------------

pureE = (value : pair 0 value)
bindE = (action k : pair 1 (pair action k))
exceptE = (tag value k : pair 2 (pair tag (pair value k)))

pureM = pureE
bindM = bindE

-- Lift a contract failure into an interaction tree.
checkM = (contract value :
  matchResult
    (msg _ : exceptE "contract" msg (_ : pureE t))
    (checked _ : pureE checked)
    (contract value t))

-- Lift a pure function into the interaction tree.
liftM = (f : (x : pureE (f x)))

-- Interpret a pure interaction tree into a Result.
runM = (tree :
  run tree
  where run =
          y (self tree :
            matchPair
              (op payload :
                matchBool
                  -- pureE
                  (contractOk (snd tree) t)
                  (matchBool
                    -- bindE
                    (matchPair
                      (action k :
                        matchResult
                          (msg _ : contractErr msg t)
                          (v _ : self (k v))
                          (self action))
                      payload)
                    -- exceptE
                    (matchPair
                      (tag pair :
                        matchPair
                          (value k :
                            contractErr value t)
                          pair)
                      payload)
                    (equal? op 1))
                  (equal? op 0))
              tree))

-- Handle matching exceptE nodes by applying the handler to the value and the
-- resumption continuation. Non-matching exceptions are left in place.
handleM = (tag handler tree :
  handle tree
  where handle =
          y (self tree :
            matchPair
              (op payload :
                matchBool
                  -- pureE
                  tree
                  (matchBool
                    -- bindE
                    (matchPair
                      (action k :
                        bindE (self action) (v : self (k v)))
                      payload)
                    -- exceptE
                    (matchPair
                      (et pair :
                        matchPair
                          (value k :
                            matchBool
                              (self (handler value k))
                              tree
                              (equal? et tag))
                          pair)
                      payload)
                    (equal? op 1))
                  (equal? op 0))
              tree))