From 229ba34af4eb0926bf722cccd3816095731d34ed Mon Sep 17 00:00:00 2001
From: James Eversole <james@eversole.co>
Date: Tue, 1 Sep 2026 08:50:18 -0500
Subject: [PATCH] Combine base,list,contracts

---
 README.md                                 |   3 +-
 demos/contractBasics.tri                  |   4 +-
 demos/contractEffects.tri                 |   4 +-
 demos/interactionTrees/arboricxServer.tri |   2 +-
 demos/interactionTrees/environment.tri    |   3 +-
 demos/interactionTrees/forkAwait.tri      |   3 +-
 demos/interactionTrees/greet.tri          |   3 +-
 demos/interactionTrees/safeRead.tri       |   3 +-
 demos/interactionTrees/shout.tri          |   3 +-
 demos/interactionTrees/state.tri          |   3 +-
 demos/interactionTrees/writeThenRead.tri  |   3 +-
 demos/interactionTrees/yield.tri          |   3 +-
 lib/base.tri                              | 568 ++++++++++++++++++++++
 lib/bytes.tri                             |   1 -
 lib/contracts.tri                         | 240 ---------
 lib/conversions.tri                       |   1 -
 lib/guardedBase.tri                       |   4 +-
 lib/intensionalContracts.tri              |   3 +-
 lib/list.tri                              | 342 -------------
 lib/prelude.tri                           |   3 -
 src/Eval.hs                               |   8 +-
 test/Spec.hs                              |   6 +-
 tricu.workspace                           |   2 -
 23 files changed, 591 insertions(+), 624 deletions(-)
 delete mode 100644 lib/contracts.tri
 delete mode 100644 lib/list.tri

diff --git a/README.md b/README.md
index 592305d..641c2e0 100644
--- a/README.md
+++ b/README.md
@@ -8,7 +8,7 @@ tricu is the word for "tree" in Lojban: `(x1) is a tree of species/cultivar (x2)
 
 In the `ext/` directory there are implementations of TC evaluators and tooling in other languages. Here be dragons; beware.
 
-I have fully embraced the slopmachine (LLM-assisted development) for this project. Nothing is stable or sacred. We will discover sanity at the end of the journey but we won't strive for it until then.
+While my original implementation was hand-written, I have since fully embraced the slopmachine for this project. Nothing is stable or sacred. We will discover sanity at the end of the journey but we won't strive for it until then. The `main` branch will see my latest thoughts and experiments. Emphasis on "AUTHOR DISCLAIMS ALL WARRANTIES" from the LICENSE.
 
 This README.md is 100% human written. No other .md file will be until stabilization.
 
@@ -31,6 +31,7 @@ tricu < triage = (a b c : t (t a b) c)
 tricu < test = triage "Leaf" (z : "Stem") (a b : "Fork")
 tricu < test (t t)
 tricu > "Stem"
+
 tricu < -- We can even convert a term back to source code (/demos/toSource.tri)
 tricu < toSource not?
 tricu > "(t (t (t t) (t t t)) (t t (t t t)))"
diff --git a/demos/contractBasics.tri b/demos/contractBasics.tri
index 893e9bb..479362a 100644
--- a/demos/contractBasics.tri
+++ b/demos/contractBasics.tri
@@ -1,6 +1,4 @@
-!import "base" !Local
-!import "list" !Local
-!import "contracts" !Local
+!import "prelude" !Local
 
 -- A custom 'and' combinator written directly against base.matchResult.
 -- It succeeds only when *both* contracts succeed, threading the checked value
diff --git a/demos/contractEffects.tri b/demos/contractEffects.tri
index ecd2b8a..63062a8 100644
--- a/demos/contractEffects.tri
+++ b/demos/contractEffects.tri
@@ -1,6 +1,4 @@
-!import "base" !Local
-!import "list" !Local
-!import "contracts" !Local
+!import "prelude" !Local
 
 -- ---------------------------------------------------------------------------
 -- Contracts + interaction trees with `do` notation
diff --git a/demos/interactionTrees/arboricxServer.tri b/demos/interactionTrees/arboricxServer.tri
index d424a31..2c0bf44 100644
--- a/demos/interactionTrees/arboricxServer.tri
+++ b/demos/interactionTrees/arboricxServer.tri
@@ -1,4 +1,4 @@
-!import "base"            !Local
+!import prelude !Local
 !import "io"              !Local
 !import "arboricx.server" !Local
 
diff --git a/demos/interactionTrees/environment.tri b/demos/interactionTrees/environment.tri
index d7a7813..d8462cc 100644
--- a/demos/interactionTrees/environment.tri
+++ b/demos/interactionTrees/environment.tri
@@ -1,5 +1,4 @@
-!import "base" !Local
-!import "list" !Local
+!import prelude !Local
 !import "io"   !Local
 
 -- Environment effects: ask and local.
diff --git a/demos/interactionTrees/forkAwait.tri b/demos/interactionTrees/forkAwait.tri
index d23c0ae..cd1f5da 100644
--- a/demos/interactionTrees/forkAwait.tri
+++ b/demos/interactionTrees/forkAwait.tri
@@ -1,5 +1,4 @@
-!import "base" !Local
-!import "list" !Local
+!import prelude !Local
 !import "io"   !Local
 
 -- Basic fork and await.
diff --git a/demos/interactionTrees/greet.tri b/demos/interactionTrees/greet.tri
index 5b65692..75548f2 100644
--- a/demos/interactionTrees/greet.tri
+++ b/demos/interactionTrees/greet.tri
@@ -1,5 +1,4 @@
-!import "base" !Local
-!import "list" !Local
+!import prelude !Local
 !import "io"   !Local
 
 -- Greet and return a pure value.
diff --git a/demos/interactionTrees/safeRead.tri b/demos/interactionTrees/safeRead.tri
index 2a8c58c..3ddeb49 100644
--- a/demos/interactionTrees/safeRead.tri
+++ b/demos/interactionTrees/safeRead.tri
@@ -1,5 +1,4 @@
-!import "base" !Local
-!import "list" !Local
+!import prelude !Local
 !import "io"   !Local
 
 -- readFile returns a Result.  matchResult branches on ok / err.
diff --git a/demos/interactionTrees/shout.tri b/demos/interactionTrees/shout.tri
index 9526865..061a23e 100644
--- a/demos/interactionTrees/shout.tri
+++ b/demos/interactionTrees/shout.tri
@@ -1,5 +1,4 @@
-!import "base" !Local
-!import "list" !Local
+!import prelude !Local
 !import "io"   !Local
 
 -- Transform an IO result.
diff --git a/demos/interactionTrees/state.tri b/demos/interactionTrees/state.tri
index 0976f5c..97d5d22 100644
--- a/demos/interactionTrees/state.tri
+++ b/demos/interactionTrees/state.tri
@@ -1,5 +1,4 @@
-!import "base" !Local
-!import "list" !Local
+!import prelude !Local
 !import "io"   !Local
 
 -- Mutable state via get and put.
diff --git a/demos/interactionTrees/writeThenRead.tri b/demos/interactionTrees/writeThenRead.tri
index 15aacbd..29282e7 100644
--- a/demos/interactionTrees/writeThenRead.tri
+++ b/demos/interactionTrees/writeThenRead.tri
@@ -1,5 +1,4 @@
-!import "base" !Local
-!import "list" !Local
+!import prelude !Local
 !import "io"   !Local
 
 -- Write a file, then read it back.
diff --git a/demos/interactionTrees/yield.tri b/demos/interactionTrees/yield.tri
index bf9e883..475e916 100644
--- a/demos/interactionTrees/yield.tri
+++ b/demos/interactionTrees/yield.tri
@@ -1,5 +1,4 @@
-!import "base" !Local
-!import "list" !Local
+!import prelude !Local
 !import "io"   !Local
 
 -- Cooperative scheduling with yield.
diff --git a/lib/base.tri b/lib/base.tri
index d3e7775..43be9c8 100644
--- a/lib/base.tri
+++ b/lib/base.tri
@@ -291,3 +291,571 @@ resultMapErr = (f result :
     (code rest : err (f code) rest)
     (value rest : ok value rest)
     result)
+
+-- ---------------------------------------------------------------------------
+-- List
+-- ---------------------------------------------------------------------------
+
+matchList = a b : triage a _ b
+
+emptyList? = matchList true (_ _ : false)
+head = matchList t (head _ : head)
+tail = matchList t (_ tail : tail)
+
+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 = xs : y length_ xs
+
+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 = xs : y last_ xs
+
+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 = foldl (acc x : add x acc) 0
+product = 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))
+
+-- 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))
diff --git a/lib/bytes.tri b/lib/bytes.tri
index 9f47b8c..4b6b986 100644
--- a/lib/bytes.tri
+++ b/lib/bytes.tri
@@ -1,5 +1,4 @@
 !import "base" !Local
-!import "list" !Local
 
 bytesNil? = emptyList?
 
diff --git a/lib/contracts.tri b/lib/contracts.tri
deleted file mode 100644
index fe62e78..0000000
--- a/lib/contracts.tri
+++ /dev/null
@@ -1,240 +0,0 @@
-!import "base" !Local
-!import "list" !Local
-
--- ---------------------------------------------------------------------------
--- 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))
-
--- 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))
diff --git a/lib/conversions.tri b/lib/conversions.tri
index 3e5af88..d4d4174 100644
--- a/lib/conversions.tri
+++ b/lib/conversions.tri
@@ -1,5 +1,4 @@
 !import "base" !Local
-!import "list" !Local
 
 incDecRev = y (self : matchList
   "1"
diff --git a/lib/guardedBase.tri b/lib/guardedBase.tri
index d002be3..4be71c7 100644
--- a/lib/guardedBase.tri
+++ b/lib/guardedBase.tri
@@ -1,6 +1,4 @@
-!import "base" !Local
-!import "list" !Local
-!import "contracts" !Local
+!import "prelude" !Local
 !import "intensional" !Local
 
 -- Runtime-guarded wrappers around partial or structurally-sensitive base/list
diff --git a/lib/intensionalContracts.tri b/lib/intensionalContracts.tri
index ab70021..93ad477 100644
--- a/lib/intensionalContracts.tri
+++ b/lib/intensionalContracts.tri
@@ -1,5 +1,4 @@
-!import "base" !Local
-!import "list" !Local
+!import "prelude" !Local
 !import "contracts" !Local
 
 -- Structural contracts that exploit Tree Calculus's intensional nature.
diff --git a/lib/list.tri b/lib/list.tri
deleted file mode 100644
index 94cd5b1..0000000
--- a/lib/list.tri
+++ /dev/null
@@ -1,342 +0,0 @@
-!import "base" !Local
-
-_ = t
-
-matchList = a b : triage a _ b
-
-emptyList? = matchList true (_ _ : false)
-head = matchList t (head _ : head)
-tail = matchList t (_ tail : tail)
-
-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 = xs : y length_ xs
-
-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 = xs : y last_ xs
-
-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 = foldl (acc x : add x acc) 0
-product = 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.
---
--- The workers below follow notes/tricu-normalization-rules.md: consumed data
--- first, lazy eliminators around every recursive branch, `y` only inside the
--- public wrapper, and `pair`-only state updates.
--- ---------------------------------------------------------------------------
-
-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. A separator byte is never stored, so the state
--- updates stay `pair`s and every recursive argument is a variable: the input is
--- walked exactly once and the fields are reversed back once, when it ends.
---
--- Splitting on a multi-byte separator is deliberately not here. Detecting a
--- separator longer than a byte means re-walking the remaining input at every
--- split point (or splicing the field), which is quadratic in the best case and
--- blew up when tried. `http.tri` wants CRLF and `:` splits; that wants a shape
--- where the separator drives the recursion instead of the input.
---
--- 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
diff --git a/lib/prelude.tri b/lib/prelude.tri
index 3421c1d..cde13a8 100644
--- a/lib/prelude.tri
+++ b/lib/prelude.tri
@@ -1,6 +1,3 @@
--- Standard tricu prelude.
-
 !import "base"        !Local
-!import "list"        !Local
 !import "bytes"       !Local
 !import "conversions" !Local
diff --git a/src/Eval.hs b/src/Eval.hs
index f73a18a..554a6e0 100644
--- a/src/Eval.hs
+++ b/src/Eval.hs
@@ -68,10 +68,14 @@ evalTricu env x = go env (reorderDefs env (map recoverParams (desugarContracts x
   where
     go env' []     = env'
     go env' [def]    =
-      let updatedEnv = evalSingle env' def
+      let updatedEnv = evalSingle (trace ("evaluating: " ++ defName' def) env') def
       in Map.insert "!result" (result updatedEnv) updatedEnv
     go env' (def:xs) =
-      evalTricu (evalSingle env' def) xs
+      evalTricu (evalSingle (trace ("evaluating: " ++ defName' def) env') def) xs
+
+    defName' (SDef name _ _) = name
+    defName' (SDefAnn name _ _ _) = name
+    defName' _ = "<expr>"
 
 evalASTSync :: Env -> TricuAST -> T
 evalASTSync env term = case term of
diff --git a/test/Spec.hs b/test/Spec.hs
index 21c7554..3caa9a3 100644
--- a/test/Spec.hs
+++ b/test/Spec.hs
@@ -51,17 +51,15 @@ testStore = StorePath "/tmp/tricu-test-store"
 allTestLibsEnv :: Env
 allTestLibsEnv = unsafePerformIO $ do
   base    <- evaluateFile "./lib/base.tri"
-  list    <- evaluateFile "./lib/list.tri"
   bytes   <- evaluateFile "./lib/bytes.tri"
   bin     <- evaluateFile "./lib/binary.tri"
   http    <- evaluateFile "./lib/http.tri"
   arbor   <- evaluateFile "./lib/arboricx/arboricx.tri"
   io      <- evaluateFile "./lib/io.tri"
   sock    <- evaluateFile "./lib/socket.tri"
-  contracts     <- evaluateFile "./lib/contracts.tri"
   intensional   <- evaluateFile "./lib/intensionalContracts.tri"
   guarded       <- evaluateFile "./lib/guardedBase.tri"
-  pure (Map.unions [base, list, bytes, bin, http, arbor, io, sock, contracts, intensional, guarded])
+  pure (Map.unions [base, bytes, bin, http, arbor, io, sock, intensional, guarded])
 {-# NOINLINE allTestLibsEnv #-}
 
 tests :: TestTree
@@ -1679,7 +1677,7 @@ demos = testGroup "Test provided demo functionality"
       res     <- liftIO $ evaluateFileResult "./demos/contractEffects.tri"
       decodeResult res @?= "[t t, 10]"
   , testCase "Safe base wrappers demo" $ do
-      res     <- liftIO $ evaluateFileResult "./demos/safeBaseWrappers.tri"
+      res     <- liftIO $ evaluateFileResult "./demos/contractBasics.tri"
       decodeResult res @?= "[t t, 1]"
   ]
 
diff --git a/tricu.workspace b/tricu.workspace
index e48bc96..7c6ea6e 100644
--- a/tricu.workspace
+++ b/tricu.workspace
@@ -1,6 +1,5 @@
 # tricu workspace module source map
 module base = lib/base.tri
-module list = lib/list.tri
 module bytes = lib/bytes.tri
 module conversions = lib/conversions.tri
 module prelude = lib/prelude.tri
@@ -9,7 +8,6 @@ module patterns = lib/patterns.tri
 module io = lib/io.tri
 module socket = lib/socket.tri
 module http = lib/http.tri
-module contracts = lib/contracts.tri
 module intensional = lib/intensionalContracts.tri
 module guarded = lib/guardedBase.tri
 module arboricx.common = lib/arboricx/common.tri