pow, even, odd, min, max

AGENTS.md

@@ -16,6 +16,26 @@ nix build .#
 
 > **Rule of thumb:** if it builds, links, or tests, it goes through `nix`.
 
+### Write and test, don't mentally trace
+
+`nix flake check` finishes quickly. Use it.
+
+tricu's minimalism makes it easy to build a confident-sounding but wrong
+mental model of evaluation order, branch selection (`matchBool` arg order),
+or number encoding. A quick test replaces many minutes of uncertain reasoning.
+
+Prefer:
+
+1. Write a candidate implementation.
+2. Run the tests or a probe.
+3. Fix what's wrong.
+
+Over:
+
+1. Reason about semantics across multiple files.
+2. Build up a chain of inference.
+3. Write code that assumes the chain was correct.
+
 ## Project Overview
 
 **tricu** (pronounced "tree-shoe") is a programming-language experiment written primarily in Haskell.

README.md

@@ -62,19 +62,14 @@ tricu eval --format decode program.tri
 tricu eval --output result.txt program.tri
 ```
 
-Annotated programs run normally under `eval`; annotations are metadata, not
+Unchecked eval parses annotation syntax, discards contract metadata, skips
-runtime types. If you want evaluation to ignore View Contracts completely while
+producer-side View Contract checks during workspace module auto-builds, and does
-loading workspace modules, use unchecked mode:
+not publish unchecked View refs. 
 
 ```sh
 tricu eval --unchecked program.tri
 ```
 
-Unchecked eval parses annotation syntax, discards contract metadata, skips
-producer-side View Contract checks during workspace module auto-builds, and does
-not publish unchecked View refs. Executable module exports may still be cached in
-the content store.
-
 Check View Contract annotations explicitly:
 
 ```sh

docs/view-contracts.md

@@ -94,108 +94,35 @@ view envelope is well-formed, and recursively validates the `baseView`, but it
 must treat the guard payload/reference as opaque executable data, not as another
 View.
 
-## 4. Polymorphic and Abstract Views
+## 4. Soundness Boundary
 
-View Contracts support portable polymorphism over Views. The View language is
+Views are descriptive boundary metadata, not types and not proofs about opaque
-interpreted by the same portable checker model implemented in `tricu` terms.
+Tree Calculus terms. In particular, the checker does not claim parametricity,
+representation independence, or existential abstraction.
 
-Source syntax may use underscore-prefixed names as View variables inside
+Raw Tree Calculus observation can distinguish values by their tree
-annotations:
+representation. A term advertised as `Fn [A] A` can inspect its argument and
+choose a representation-dependent result; a metadata-only checker cannot rule
+that out. The same issue applies transitively through higher-order arguments and
+dynamically constructed observers.
 
-```tri
+The checker therefore accepts only monomorphic Views. Legacy `Var`, `Forall`,
-id x@_a =@_a x
+and `Exists` tags remain reserved so old artifacts fail deterministically, but
-const x@_a y@_b =@_a x
+they are not well-formed checker inputs.
-compose f@(Fn [_b] _c) g@(Fn [_a] _b) x@_a =@_c f (g x)
-```
 
-In the portable artifact, these lower to scoped View binders rather than
+The guarantees retained here are narrower:
-unscoped source-name conventions. This fits the existing View encoding style:
-Views are tagged records with numeric tags and tagged fields. Polymorphic forms
-are View records such as:
 
-```text
+- View and typed-program envelopes are structurally well formed.
-Var localId
+- Declared monomorphic Views flow consistently across explicit typed nodes.
-Forall binders body
+- Guarded Views execute their predicates at represented boundaries.
-Exists binders body
+- Artifact references bind metadata to particular stored objects.
-```
 
-The current durable encoding uses stable local binder IDs. For example,
+These guarantees do not establish that an opaque payload has an unguarded
-`id x@_a =@_a x` exports a shape equivalent to:
+structural View such as `List` or `Fn`. Such Views are conventions/assertions
-
+used to place and compose checks. Only an executed guard observes the value.
-```text
-Forall [0] (Fn [Var 0] (Var 0))
-```
-
-Source names like `_a` are for authoring; the artifact carries binder scope and
-local IDs rather than relying on source-name identity.
-
-`Forall` supports generic contracts:
-
-```tri
-map f@(Fn [_a] _b) xs@(List _a) =@(List _b) ...
-head xs@(NonEmptyList _a) =@_a ...
-```
-
-At each checked use, the checker instantiates quantified variables into
-use-local internal variables and solves View compatibility constraints. The
-portable checker uses structural use-local IDs rather than expensive numeric
-freshening, and treats unconstrained variable-variable matches as constraints
-that do not create substitution cycles. Concrete observations still bind these
-variables when enough information is available. This is what lets explicitly
-annotated higher-order boundaries accept polymorphic values, for example
-`compose id id "x"`, and lets quantified values satisfy concrete requirements
-such as `Fn [String] String`. It gives useful polymorphic contracts for
-explicitly declared/imported View facts.
-
-`Exists` supports checked abstraction boundaries. A module can expose a value as
-"some representation `_repr` plus capabilities over `_repr`":
-
-```text
-Exists _repr.
-  Pair
-    (Fn [String] _repr)   -- constructor
-    (Fn [_repr] String)   -- renderer / eliminator
-```
-
-This does not make raw Tree Calculus inspection impossible. Unchecked code can
-always inspect trees. It means checked clients cannot justify
-representation-specific operations through the View system unless the package
-exports an appropriate capability or eliminator.
-
-This leads to an important distinction for future checked subsets:
-
-```text
-controlled observation: Bool/List/Maybe/Result/etc. eliminators with Views
-raw observation: direct tree-shape inspection through triage-like power
-```
-
-Useful application code can live mostly in the controlled fragment and receive
-explicit View validation over lambdas, application, let, and typed eliminators.
-Low-level library code may still use raw intensionality, but should expose
-disciplined Views and capabilities above it. Scott-encoded constructors and
-eliminators are a natural tricu-native representation for these APIs.
-
-Tree Calculus terms do not carry intrinsic principal Views, and raw intensional
-code can invalidate parametric claims. View Contracts are an explicit evidence
-and contract layer over tricu programs; limited polymorphic Views are supported
-when they are declared or imported as facts with provenance.
-
-The first stdlib annotation island starts with parametric functions that do not
-inspect representation:
-
-```tri
-id x@_a =@_a x
-const x@_a y@_b =@_a x
-compose f@(Fn [_b] _c) g@(Fn [_a] _b) x@_a =@_c f (g x)
-```
-
-Re-export-only modules preserve imported View metadata, so these contracts flow
-through `prelude` rather than only through direct `base` imports.
-
-Functions built on raw `t`/`triage` should enter the checked world through
-trusted, controlled eliminator contracts rather than by treating arbitrary raw
-inspection as parametric.
 
+See [the intensionality analysis](../notes/view-contract-trust-provenance.md) for
+the rationale and remaining limitations.
 
 ## 5. Guards
 
@@ -259,81 +186,22 @@ A node may contain opaque executable fields. Those fields are tree terms, but
 they are not recursively decoded as view-tree nodes or Views unless the node's
 semantics explicitly says so.
 
-View facts may also carry explicit per-fact trust provenance:
+View facts may carry per-fact provenance:
 
 ```text
-Checked    -- derived by checked lowering / checker validation
+Checked
-Trusted    -- asserted by a trusted boundary, e.g. a primitive eliminator API
+Trusted
-Unchecked  -- raw or assumed; no parametricity/abstraction guarantee
+Unchecked
 ```
 
-In the portable view-tree envelope this provenance is represented as an optional
+These labels are retained for artifact compatibility and auditing. They identify
-field on `typedValue` / `typedRequire` facts. In module manifests the same
+the source of an assertion; they do not prove semantic membership, parametricity,
-provenance is carried beside the exported View Contract object reference so that
+or abstraction. An absent label is interpreted conservatively as `Unchecked`.
-imports and re-exports preserve it without relying on module-level convention.
-Absent provenance is interpreted conservatively as `Unchecked` at use sites.
 
-For parametric checked definitions, the frontend now performs a conservative
+The former value-level polymorphic `viewFacts` catalogs and frontend
-raw-intensionality dependency pass over local definitions. If a definition with
+raw-intensionality taint pass have been removed. Monomorphic imported facts may
-scoped View variables depends directly or indirectly on raw `triage` / raw `t`
+still be attached to exports, but consumers must treat them as assertions unless
-construction, or on an imported `Unchecked` fact, lowering fails and asks the
+an executable guard enforces the relevant property.
-author to route observation through a trusted eliminator boundary. This is
-intentionally provenance/dependency based; it is not an attempt to decide
-whether arbitrary Tree Calculus reduction will ever reach rule 3.
-
-View facts can be authored as ordinary value-level Tree Calculus metadata under
-one conventional top-level name:
-
-```text
-viewFacts = [fact ...]
-fact      = pair exportName (pair provenance view)
-```
-
-where `exportName` is a string naming a value exported by the module,
-`provenance` is `0 = Checked`, `1 = Trusted`, or `2 = Unchecked`, and `view` is
-the same portable View record used by `view-tree` artifacts. The host evaluates
-this value and decodes the data schema; it does not infer trust from source
-syntax, AST shape, module name, or a Haskell-side catalog.
-
-The initial trusted eliminator facts are authored this way in clearly separated
-stdlib `viewFacts` sections:
-
-```text
-matchBool  : forall r. r -> r -> Bool -> r
-matchMaybe : forall a r. r -> (a -> r) -> Maybe a -> r
-matchList  : forall a r. r -> (a -> List a -> r) -> List a -> r
-```
-
-The `base` module provides small `facts*` authoring helpers for this advanced
-metadata, e.g. `factsFact`, `factsChecked`, `factsTrusted`, `factsUnchecked`,
-`factsForall`, `factsFn`, `factsVar`, `factsBool`, `factsString`, `factsByte`,
-`factsUnit`, `factsMaybe`, and `factsList`. These helpers construct ordinary
-Tree data; authority comes from the exported `viewFacts` value and its explicit
-provenance tags. Loader validation rejects duplicate fact names and facts for
-names the module does not export.
-
-Initial derived stdlib annotations using this trusted kernel include:
-
-```text
-maybeMap  : forall a b. (a -> b) -> Maybe a -> Maybe b
-maybeBind : forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
-maybeOr   : forall a. a -> Maybe a -> a
-```
-
-Recursive list combinators are currently published as explicit `Trusted`
-value-level facts rather than `Checked` source annotations, because their bodies
-pass through raw fixed-point machinery that the conservative parametric taint
-pass intentionally does not prove safe. This is the stabilized boundary: raw
-stdlib kernels establish conventions with explicit authority; ordinary checked
-clients consume those facts rather than re-proving the internals.
-
-```text
-headMaybe / lastMaybe / nthMaybe
-append / map / filter / foldl / foldr
-length / reverse / snoc / count / all? / any? / intersect
-take / drop / splitAt / concatMap / find / partition / zipWith
-string/list-byte helpers such as strLength, startsWith?, lines, words
-```
 
 ## 7. Checker Semantics
 

lib/base.tri

@@ -1,8 +1,8 @@
 false = t
 _     = t
 true  = t t
-id a@_a =@_a a
+id a = a
-const a@_a b@_b =@_a a
+const a b = a
 pair  = t
 if cond then else = t (t else (t t then)) t cond
 
@@ -10,7 +10,7 @@ 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@(Fn [_b] _c) g@(Fn [_a] _b) x@_a =@_c f (g x)
+compose f g x = f (g x)
 
 triage leaf stem fork = t (t leaf stem) fork
 test   = triage "Leaf" (_ : "Stem") (_ _ : "Fork")
@@ -114,11 +114,52 @@ matchMaybe nothingCase justCase maybe =
     maybe
 
 maybe default f m = matchMaybe default f m
-maybeMap f@(Fn [_a] _b) m@(Maybe _a) =@(Maybe _b) matchMaybe nothing (compose just f) m
+maybeMap f m = matchMaybe nothing (x : just (f x)) m
-maybeBind m@(Maybe _a) f@(Fn [_a] (Maybe _b)) =@(Maybe _b) matchMaybe nothing f m
+maybeBind m f = matchMaybe nothing f m
-maybeOr default@_a m@(Maybe _a) =@_a matchMaybe default id 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
 -- ---------------------------------------------------------------------------
@@ -137,18 +178,15 @@ andLazy? = (a bK :
 
 pred = y (self : triage
   0
-  (_ : 0)
+  0
   (bit rest :
-    matchBool
+    ifLazy
-      (matchBool
+      bit
+      (_ : matchBool
+        (t t rest)
         0
-        (pair 0 rest)
+        rest)
-        (equal? rest 0))
+      (_ : t (t t) (self rest))))
-      (matchBool
-        0
-        (pair 1 (self rest))
-        (equal? rest 0))
-      bit))
 
 isZero? = triage true (_ : false) (_ _ : false)
 
@@ -190,6 +228,42 @@ mul = y (self a b :
     (_ : 0)
     (_ : add a (self a (pred b))))
 
+div = y (self a b :
+  ifLazy
+    (isZero? b)
+    (_ : 0)
+    (_ : ifLazy
+      (lt? a b)
+      (_ : 0)
+      (_ : succ (self (sub a b) b))))
+
+mod = y (self a b :
+  ifLazy
+    (isZero? b)
+    (_ : 0)
+    (_ : ifLazy
+      (lt? a b)
+      (_ : a)
+      (_ : self (sub a b) b)))
+
+pow = 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 = (a b : ifLazy (lte? a b) (_ : a) (_ : b))
+
+max = (a b : ifLazy (lte? a b) (_ : b) (_ : a))
+
 -- ---------------------------------------------------------------------------
 -- Result combinators
 -- ---------------------------------------------------------------------------
@@ -217,169 +291,3 @@ resultMapErr = (f result :
     (code rest : err (f code) rest)
     (value rest : ok value rest)
     result)
-
--- ---------------------------------------------------------------------------
--- View facts
--- ---------------------------------------------------------------------------
-
-factsFact name provenance view = pair name (pair provenance view)
-factsChecked = 0
-factsTrusted = 1
-factsUnchecked = 2
-factsField tag value = pair tag value
-factsRecord tag fields = pair tag fields
-factsVar id = factsRecord 8 [(factsField 10 id)]
-factsForall binders body =
-  factsRecord 9 [(factsField 11 binders) (factsField 12 body)]
-factsFn args result =
-  factsRecord 1 [(factsField 0 args) (factsField 1 result)]
-factsAny = factsRecord 0 []
-factsRef symbol = factsRecord 2 [(factsField 2 symbol)]
-factsBool = factsRef 0
-factsString = factsRef 1
-factsByte = factsRef 2
-factsUnit = factsRef 3
-factsMaybe elem = factsRecord 4 [(factsField 3 elem)]
-factsList elem = factsRecord 3 [(factsField 3 elem)]
-factsPair left right = factsRecord 5 [(factsField 4 left) (factsField 5 right)]
-factsResult err ok = factsRecord 6 [(factsField 6 err) (factsField 7 ok)]
-
-viewFacts =
-  [ (factsFact "pair" factsTrusted
-      (factsForall [0]
-        (factsFn
-          [(factsVar 0) (factsList (factsVar 0))]
-          (factsList (factsVar 0)))))
-    (factsFact "nothing" factsTrusted
-      (factsForall [0]
-        (factsMaybe (factsVar 0))))
-    (factsFact "just" factsTrusted
-      (factsForall [0]
-        (factsFn [(factsVar 0)] (factsMaybe (factsVar 0)))))
-    (factsFact "false" factsTrusted factsBool)
-    (factsFact "true" factsTrusted factsBool)
-    (factsFact "if" factsTrusted
-      (factsForall [0]
-        (factsFn [factsBool (factsVar 0) (factsVar 0)] (factsVar 0))))
-    (factsFact "triage" factsTrusted
-      (factsForall [0]
-        (factsFn [factsAny factsAny factsAny factsAny] (factsVar 0))))
-    (factsFact "test" factsTrusted factsString)
-    (factsFact "matchBool" factsTrusted
-      (factsForall [0]
-        (factsFn
-          [(factsVar 0) (factsVar 0) factsBool]
-          (factsVar 0))))
-    (factsFact "lAnd" factsTrusted
-      (factsFn [factsBool factsBool] factsBool))
-    (factsFact "lOr" factsTrusted
-      (factsFn [factsBool factsBool] factsBool))
-    (factsFact "matchPair" factsTrusted
-      (factsForall [0 1 2]
-        (factsFn
-          [(factsFn [(factsVar 0) (factsVar 1)] (factsVar 2))
-           (factsPair (factsVar 0) (factsVar 1))]
-          (factsVar 2))))
-    (factsFact "fst" factsTrusted
-      (factsForall [0 1]
-        (factsFn [(factsPair (factsVar 0) (factsVar 1))] (factsVar 0))))
-    (factsFact "snd" factsTrusted
-      (factsForall [0 1]
-        (factsFn [(factsPair (factsVar 0) (factsVar 1))] (factsVar 1))))
-    (factsFact "not?" factsTrusted
-      (factsFn [factsBool] factsBool))
-    (factsFact "and?" factsTrusted
-      (factsFn [factsBool factsBool] factsBool))
-    (factsFact "or?" factsTrusted
-      (factsFn [factsBool factsBool] factsBool))
-    (factsFact "xor?" factsTrusted
-      (factsFn [factsBool factsBool] factsBool))
-    (factsFact "equal?" factsTrusted
-      (factsForall [0]
-        (factsFn [(factsVar 0) (factsVar 0)] factsBool)))
-    (factsFact "succ" factsTrusted
-      (factsFn [factsByte] factsByte))
-    (factsFact "pred" factsTrusted
-      (factsFn [factsByte] factsByte))
-    (factsFact "isZero?" factsTrusted
-      (factsFn [factsByte] factsBool))
-    (factsFact "add" factsTrusted
-      (factsFn [factsByte factsByte] factsByte))
-    (factsFact "sub" factsTrusted
-      (factsFn [factsByte factsByte] factsByte))
-    (factsFact "lte?" factsTrusted
-      (factsFn [factsByte factsByte] factsBool))
-    (factsFact "gte?" factsTrusted
-      (factsFn [factsByte factsByte] factsBool))
-    (factsFact "lt?" factsTrusted
-      (factsFn [factsByte factsByte] factsBool))
-    (factsFact "gt?" factsTrusted
-      (factsFn [factsByte factsByte] factsBool))
-    (factsFact "mul" factsTrusted
-      (factsFn [factsByte factsByte] factsByte))
-    (factsFact "matchMaybe" factsTrusted
-      (factsForall [0 1]
-        (factsFn
-          [(factsVar 1)
-           (factsFn [(factsVar 0)] (factsVar 1))
-           (factsMaybe (factsVar 0))]
-          (factsVar 1))))
-    (factsFact "maybe" factsTrusted
-      (factsForall [0 1]
-        (factsFn
-          [(factsVar 1)
-           (factsFn [(factsVar 0)] (factsVar 1))
-           (factsMaybe (factsVar 0))]
-          (factsVar 1))))
-    (factsFact "maybe?" factsTrusted
-      (factsForall [0]
-        (factsFn [(factsMaybe (factsVar 0))] factsBool)))
-    (factsFact "ifLazy" factsTrusted
-      (factsForall [0]
-        (factsFn
-          [factsBool
-           (factsFn [factsUnit] (factsVar 0))
-           (factsFn [factsUnit] (factsVar 0))]
-          (factsVar 0))))
-    (factsFact "andLazy?" factsTrusted
-      (factsFn [factsBool (factsFn [factsUnit] factsBool)] factsBool))
-    (factsFact "ok" factsTrusted
-      (factsForall [0 1]
-        (factsFn [(factsVar 1) factsAny] (factsResult (factsVar 0) (factsVar 1)))))
-    (factsFact "err" factsTrusted
-      (factsForall [0 1]
-        (factsFn [(factsVar 0) factsAny] (factsResult (factsVar 0) (factsVar 1)))))
-    (factsFact "matchResult" factsTrusted
-      (factsForall [0 1 2]
-        (factsFn
-          [(factsFn [(factsVar 0) factsAny] (factsVar 2))
-           (factsFn [(factsVar 1) factsAny] (factsVar 2))
-           (factsResult (factsVar 0) (factsVar 1))]
-          (factsVar 2))))
-    (factsFact "resultIsOk" factsTrusted
-      (factsForall [0 1]
-        (factsFn [(factsResult (factsVar 0) (factsVar 1))] factsBool)))
-    (factsFact "resultIsErr" factsTrusted
-      (factsForall [0 1]
-        (factsFn [(factsResult (factsVar 0) (factsVar 1))] factsBool)))
-    (factsFact "mapResult" factsTrusted
-      (factsForall [0 1 2]
-        (factsFn
-          [(factsFn [(factsVar 1)] (factsVar 2))
-           (factsResult (factsVar 0) (factsVar 1))]
-          (factsResult (factsVar 0) (factsVar 2)))))
-    (factsFact "bindResult" factsTrusted
-      (factsForall [0 1 2]
-        (factsFn
-          [(factsResult (factsVar 0) (factsVar 1))
-           (factsFn [(factsVar 1)] (factsResult (factsVar 0) (factsVar 2)))]
-          (factsResult (factsVar 0) (factsVar 2)))))
-    (factsFact "resultOr" factsTrusted
-      (factsForall [0 1]
-        (factsFn [(factsVar 1) (factsResult (factsVar 0) (factsVar 1))] (factsVar 1))))
-    (factsFact "resultMapErr" factsTrusted
-      (factsForall [0 1 2]
-        (factsFn
-          [(factsFn [(factsVar 0)] (factsVar 2))
-           (factsResult (factsVar 0) (factsVar 1))]
-          (factsResult (factsVar 2) (factsVar 1)))))]

lib/lazy.tri

@@ -1,30 +0,0 @@
-!import "base" !Local
-!import "list" !Local
-
-lazyBool = (thenK elseK cond :
-  ((chosen : chosen t)
-   (matchBool
-     thenK
-     elseK
-     cond)))
-
-lazyList = (nilK consK xs :
-  ((chosen : chosen t)
-   (matchList
-     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)))

lib/list.tri

@@ -232,54 +232,100 @@ contains?_ self needle haystack =
     (startsWith? needle haystack)
 contains? = needle haystack : y contains?_ needle haystack
 
-linesFinish current accRev =
+-- ---------------------------------------------------------------------------
-  reverse (pair (reverse current) accRev)
+-- 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.
+-- ---------------------------------------------------------------------------
 
-lines_ self str accRev current =
+takeWhile_ self xs f =
-  matchList
+  lazyList
-    (linesFinish current accRev)
+    (_ : t)
     (h r :
-      matchBool
+      lazyBool
-        (self r (pair (reverse current) accRev) t)
+        (_ : pair h (self r f))
-        (self r accRev (pair h current))
+        (_ : t)
-        (equal? h 10))
+        (f h))
-    str
+    xs
-lines = str : y lines_ str t t
+takeWhile = f xs : y takeWhile_ xs f
 
-unlines_ self lines =
+dropWhile_ self xs f =
-  matchList
+  lazyList
-    ""
+    (_ : t)
-    (h r : append h (append "\n" (self r)))
-    lines
-unlines = lines : y unlines_ lines
-
-wordsAdd current accRev =
-  matchBool
-    accRev
-    (pair (reverse current) accRev)
-    (emptyList? current)
-
-words_ self str accRev current =
-  matchList
-    (reverse (wordsAdd current accRev))
     (h r :
-      matchBool
+      lazyBool
-        (self r (wordsAdd current accRev) t)
+        (_ : self r f)
-        (self r accRev (pair h current))
+        (_ : pair h r)
-        (equal? h 32))
+        (f h))
-    str
+    xs
-words = str : y words_ str t t
+dropWhile = f xs : y dropWhile_ xs f
 
-unwords_ self words =
+-- Byte-level whitespace only: space and horizontal tab (HTTP OWS).
-  matchList
+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 :
-      matchBool
+      lazyBool
-        h
+        (_ : h)
-        (append h (append " " (self r)))
+        (_ : append h (append sep (self r sep)))
         (emptyList? r))
-    words
+    xs
-unwords = words : y unwords_ words
+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
@@ -291,151 +337,3 @@ zipWith_ self f xs ys =
         ys)
     xs
 zipWith = f xs ys : y zipWith_ f xs ys
-
--- ---------------------------------------------------------------------------
--- View facts
---
--- Value-level metadata consumed by View tooling. These facts are ordinary Tree
--- Calculus data, not host-side assumptions and not part of the public stdlib
--- API exported by module manifests.
--- ---------------------------------------------------------------------------
-
-viewFacts =
-  [(factsFact "matchList" factsTrusted
-     (factsForall [0 1]
-       (factsFn
-         [(factsVar 1)
-          (factsFn
-            [(factsVar 0) (factsList (factsVar 0))]
-            (factsVar 1))
-          (factsList (factsVar 0))]
-         (factsVar 1))))
-   (factsFact "emptyList?" factsTrusted
-     (factsForall [0]
-       (factsFn [(factsList (factsVar 0))] factsBool)))
-   (factsFact "tail" factsTrusted
-     (factsForall [0]
-       (factsFn [(factsList (factsVar 0))] (factsList (factsVar 0)))))
-   (factsFact "append" factsTrusted
-     (factsForall [0]
-       (factsFn
-         [(factsList (factsVar 0))
-          (factsList (factsVar 0))]
-         (factsList (factsVar 0)))))
-   (factsFact "lExist?" factsTrusted
-     (factsForall [0]
-       (factsFn [(factsVar 0) (factsList (factsVar 0))] factsBool)))
-   (factsFact "map" factsTrusted
-     (factsForall [0 1]
-       (factsFn
-         [(factsFn [(factsVar 0)] (factsVar 1))
-          (factsList (factsVar 0))]
-         (factsList (factsVar 1)))))
-   (factsFact "filter" factsTrusted
-     (factsForall [0]
-       (factsFn
-         [(factsFn [(factsVar 0)] factsBool)
-          (factsList (factsVar 0))]
-         (factsList (factsVar 0)))))
-   (factsFact "foldl" factsTrusted
-     (factsForall [0 1]
-       (factsFn
-         [(factsFn [(factsVar 1) (factsVar 0)] (factsVar 1))
-          (factsVar 1)
-          (factsList (factsVar 0))]
-         (factsVar 1))))
-   (factsFact "foldr" factsTrusted
-     (factsForall [0 1]
-       (factsFn
-         [(factsFn [(factsVar 1) (factsVar 0)] (factsVar 1))
-          (factsVar 1)
-          (factsList (factsVar 0))]
-         (factsVar 1))))
-   (factsFact "length" factsTrusted
-     (factsForall [0]
-       (factsFn [(factsList (factsVar 0))] factsByte)))
-   (factsFact "reverse" factsTrusted
-     (factsForall [0]
-       (factsFn [(factsList (factsVar 0))] (factsList (factsVar 0)))))
-   (factsFact "snoc" factsTrusted
-     (factsForall [0]
-       (factsFn [(factsVar 0) (factsList (factsVar 0))] (factsList (factsVar 0)))))
-   (factsFact "count" factsTrusted
-     (factsForall [0]
-       (factsFn [(factsVar 0) (factsList (factsVar 0))] factsByte)))
-   (factsFact "all?" factsTrusted
-     (factsForall [0]
-       (factsFn [(factsFn [(factsVar 0)] factsBool) (factsList (factsVar 0))] factsBool)))
-   (factsFact "any?" factsTrusted
-     (factsForall [0]
-       (factsFn [(factsFn [(factsVar 0)] factsBool) (factsList (factsVar 0))] factsBool)))
-   (factsFact "intersect" factsTrusted
-     (factsForall [0]
-       (factsFn [(factsList (factsVar 0)) (factsList (factsVar 0))] (factsList (factsVar 0)))))
-   (factsFact "headMaybe" factsTrusted
-     (factsForall [0]
-       (factsFn [(factsList (factsVar 0))] (factsMaybe (factsVar 0)))))
-   (factsFact "lastMaybe" factsTrusted
-     (factsForall [0]
-       (factsFn [(factsList (factsVar 0))] (factsMaybe (factsVar 0)))))
-   (factsFact "nthMaybe" factsTrusted
-     (factsForall [0]
-       (factsFn [factsByte (factsList (factsVar 0))] (factsMaybe (factsVar 0)))))
-   (factsFact "take" factsTrusted
-     (factsForall [0]
-       (factsFn [factsByte (factsList (factsVar 0))] (factsList (factsVar 0)))))
-   (factsFact "drop" factsTrusted
-     (factsForall [0]
-       (factsFn [factsByte (factsList (factsVar 0))] (factsList (factsVar 0)))))
-   (factsFact "splitAt" factsTrusted
-     (factsForall [0]
-       (factsFn
-         [factsByte (factsList (factsVar 0))]
-         (factsPair (factsList (factsVar 0)) (factsList (factsVar 0))))))
-   (factsFact "concatMap" factsTrusted
-     (factsForall [0 1]
-       (factsFn
-         [(factsFn [(factsVar 0)] (factsList (factsVar 1)))
-          (factsList (factsVar 0))]
-         (factsList (factsVar 1)))))
-   (factsFact "find" factsTrusted
-     (factsForall [0]
-       (factsFn
-         [(factsFn [(factsVar 0)] factsBool)
-          (factsList (factsVar 0))]
-         (factsMaybe (factsVar 0)))))
-   (factsFact "partition" factsTrusted
-     (factsForall [0]
-       (factsFn
-         [(factsFn [(factsVar 0)] factsBool)
-          (factsList (factsVar 0))]
-         (factsPair (factsList (factsVar 0)) (factsList (factsVar 0))))))
-   (factsFact "strLength" factsTrusted
-     (factsFn [factsString] factsByte))
-   (factsFact "strAppend" factsTrusted
-     (factsFn [factsString factsString] factsString))
-   (factsFact "strEq?" factsTrusted
-     (factsFn [factsString factsString] factsBool))
-   (factsFact "strEmpty?" factsTrusted
-     (factsFn [factsString] factsBool))
-   (factsFact "startsWith?" factsTrusted
-     (factsFn [factsString factsString] factsBool))
-   (factsFact "endsWith?" factsTrusted
-     (factsFn [factsString factsString] factsBool))
-   (factsFact "contains?" factsTrusted
-     (factsFn [factsString factsString] factsBool))
-   (factsFact "lines" factsTrusted
-     (factsFn [factsString] (factsList factsString)))
-   (factsFact "unlines" factsTrusted
-     (factsFn [(factsList factsString)] factsString))
-   (factsFact "words" factsTrusted
-     (factsFn [factsString] (factsList factsString)))
-   (factsFact "unwords" factsTrusted
-     (factsFn [(factsList factsString)] factsString))
-   (factsFact "zipWith" factsTrusted
-     (factsForall [0 1 2]
-       (factsFn
-         [(factsFn [(factsVar 0) (factsVar 1)] (factsVar 2))
-          (factsList (factsVar 0))
-          (factsList (factsVar 1))]
-         (factsList (factsVar 2)))))]

lib/prelude.tri

@@ -3,5 +3,4 @@
 !import "base"        !Local
 !import "list"        !Local
 !import "bytes"       !Local
-!import "lazy"        !Local
 !import "conversions" !Local

lib/view.tri

@@ -335,11 +335,12 @@ wellFormedResultView? = (view :
 wellFormedGuardedView? = (view :
   fields2? (viewPayload view) viewFieldBase viewFieldGuard)
 
-wellFormedVarView? = (view :
+-- Tags 8-10 remain reserved so old artifacts decode deterministically, but
-  fields1? (viewPayload view) viewFieldVar)
+-- quantified/variable Views are no longer accepted by the checker. They
+-- implied abstraction and parametricity that raw Tree Calculus cannot enforce.
+wellFormedVarView? = (_ : false)
 
-wellFormedQuantifiedView? = (view :
+wellFormedQuantifiedView? = (_ : false)
-  fields2? (viewPayload view) viewFieldBinders viewFieldBody)
 
 wellFormedView_ self view =
   lazyBool
@@ -513,28 +514,6 @@ hasView? = (symbol view env :
     (viewSet : viewSetHas? view viewSet)
     (lookupViews symbol env))
 
-viewSetHasCompatible_ self namespace expected viewSet =
-  lazyList
-    (_ : false)
-    (fact rest :
-      lazyMaybe
-        (_ : self namespace expected rest)
-        (_ : true)
-        (matchView expected (instantiateView namespace (viewFactView fact)) t))
-    viewSet
-
-viewSetHasCompatible? = (namespace expected viewSet :
-  lazyBool
-    (_ : true)
-    (_ : y viewSetHasCompatible_ namespace expected viewSet)
-    (anyView? expected))
-
-hasCompatibleView? = (symbol view env :
-  lazyMaybe
-    (_ : anyView? view)
-    (viewSet : viewSetHasCompatible? symbol view viewSet)
-    (lookupViews symbol env))
-
 addViewToSet = (view evidence viewSet :
   lazyBool
     (_ : viewSet)
@@ -557,44 +536,19 @@ extendEnv_ self symbol view evidence env =
 extendEnv = (symbol view evidence env :
   y extendEnv_ symbol view evidence env)
 
-instantiateVarId = (namespace localId :
+findFnView_ self viewSet =
-  pair namespace localId)
-
-instantiateBinders_ self namespace binders subst =
-  lazyList
-    (_ : subst)
-    (binder rest :
-      self namespace rest (pair (pair binder (viewVar (instantiateVarId namespace binder))) subst))
-    binders
-
-instantiateBinders = (namespace binders subst :
-  y instantiateBinders_ namespace binders subst)
-
-instantiateView = (namespace view :
-  lazyBool
-    (_ : substituteView (instantiateBinders namespace (viewBinderNames view) t) (viewQuantifiedBody view))
-    (_ : view)
-    (forallView? view))
-
-viewAsFn = (namespace view :
-  let instantiated = instantiateView namespace view in
-  lazyBool
-    (_ : just instantiated)
-    (_ : nothing)
-    (fnView? instantiated))
-
-findFnView_ self namespace viewSet =
   lazyList
     (_ : nothing)
     (fact rest :
-      lazyMaybe
+      let view = viewFactView fact in
+      lazyBool
+        (_ : just view)
         (_ : self rest)
-        (fnView : just fnView)
+        (fnView? view))
-        (viewAsFn namespace (viewFactView fact)))
     viewSet
 
-findFnView = (namespace viewSet :
+findFnView = (viewSet :
-  y findFnView_ namespace viewSet)
+  y findFnView_ viewSet)
 
 firstKnownView = (viewSet :
   lazyList
@@ -607,157 +561,6 @@ actualViewFor = (symbol env :
     (_ : viewAny)
     (viewSet : firstKnownView viewSet)
     (lookupViews symbol env))
-
-substLookup_ self name subst =
-  lazyList
-    (_ : nothing)
-    (entry rest :
-      lazyBool
-        (_ : just (snd entry))
-        (_ : self name rest)
-        (equal? name (fst entry)))
-    subst
-
-substLookup = (name subst : y substLookup_ name subst)
-
-substBind = (name actual subst :
-  lazyBool
-    (_ : just subst)
-    (_ :
-      lazyBool
-        (_ : just subst)
-        (_ :
-          lazyMaybe
-            (_ : just (pair (pair name actual) subst))
-            (existing :
-              lazyBool
-                (_ : just subst)
-                (_ : nothing)
-                (equal? existing actual))
-            (substLookup name subst))
-        (varView? actual))
-    (equal? actual (viewVar name)))
-
-substituteView_ self subst view =
-  lazyBool
-    (_ :
-      lazyMaybe
-        (_ : view)
-        (bound : self subst bound)
-        (substLookup (viewVarName view) subst))
-    (_ :
-      lazyBool
-        (_ : viewFn (y substituteViews_ self subst (fnArgs view)) (self subst (fnResult view)))
-        (_ :
-          lazyBool
-            (_ : viewList (self subst (field0 (viewPayload view))))
-            (_ :
-              lazyBool
-                (_ : viewMaybe (self subst (field0 (viewPayload view))))
-                (_ :
-                  lazyBool
-                    (_ : viewPair (self subst (field0 (viewPayload view))) (self subst (field1 (viewPayload view))))
-                    (_ :
-                      lazyBool
-                        (_ : viewResult (self subst (field0 (viewPayload view))) (self subst (field1 (viewPayload view))))
-                        (_ :
-                          lazyBool
-                            (_ : viewGuarded (self subst (guardedViewBase view)) (guardedViewGuard view))
-                            (_ : view)
-                            (guardedView? view))
-                        (resultView? view))
-                    (pairView? view))
-                (maybeView? view))
-            (listView? view))
-        (fnView? view))
-    (varView? view)
-
-substituteViews_ self viewSelf subst views =
-  lazyList
-    (_ : t)
-    (view rest : pair (viewSelf subst view) (self viewSelf subst rest))
-    views
-
-substituteView = (subst view : y substituteView_ subst view)
-
-matchViewList_ self matchSelf expected actual subst =
-  lazyList
-    (_ :
-      lazyList
-        (_ : just subst)
-        (_ _ : nothing)
-        actual)
-    (expectedHead expectedRest :
-      lazyList
-        (_ : nothing)
-        (actualHead actualRest :
-          lazyMaybe
-            (_ : nothing)
-            (nextSubst : self matchSelf expectedRest actualRest nextSubst)
-            (matchSelf expectedHead actualHead subst))
-        actual)
-    expected
-
-matchView_ self expected actual subst =
-  lazyBool
-    (_ : just subst)
-    (_ :
-      lazyBool
-        (_ : substBind (viewVarName expected) actual subst)
-        (_ :
-          lazyBool
-            (_ : substBind (viewVarName actual) expected subst)
-            (_ :
-              lazyBool
-                (_ : just subst)
-                (_ :
-                  lazyBool
-                    (_ :
-                      lazyMaybe
-                        (_ : nothing)
-                        (argSubst : self (fnResult expected) (fnResult actual) argSubst)
-                        (y matchViewList_ self (fnArgs expected) (fnArgs actual) subst))
-                    (_ :
-                      lazyBool
-                        (_ : self (field0 (viewPayload expected)) (field0 (viewPayload actual)) subst)
-                    (_ :
-                      lazyBool
-                        (_ : self (field0 (viewPayload expected)) (field0 (viewPayload actual)) subst)
-                        (_ :
-                          lazyBool
-                            (_ :
-                              lazyMaybe
-                                (_ : nothing)
-                                (leftSubst : self (field1 (viewPayload expected)) (field1 (viewPayload actual)) leftSubst)
-                                (self (field0 (viewPayload expected)) (field0 (viewPayload actual)) subst))
-                            (_ :
-                              lazyBool
-                                (_ :
-                                  lazyMaybe
-                                    (_ : nothing)
-                                    (errSubst : self (field1 (viewPayload expected)) (field1 (viewPayload actual)) errSubst)
-                                    (self (field0 (viewPayload expected)) (field0 (viewPayload actual)) subst))
-                                (_ :
-                                  lazyBool
-                                    (_ : self (guardedViewBase expected) actual subst)
-                                    (_ :
-                                      lazyBool
-                                        (_ : self expected (guardedViewBase actual) subst)
-                                        (_ : nothing)
-                                        (guardedView? actual))
-                                    (guardedView? expected))
-                                (and? (resultView? expected) (resultView? actual)))
-                            (and? (pairView? expected) (pairView? actual)))
-                        (and? (maybeView? expected) (maybeView? actual)))
-                    (and? (listView? expected) (listView? actual)))
-                (and? (fnView? expected) (fnView? actual)))
-                (equal? expected actual))
-            (varView? actual))
-        (varView? expected))
-    (anyView? expected)
-
-matchView = (expected actual subst : y matchView_ expected actual subst)
-
 checkerErr = (tag fields env : err (diagnostic tag fields) env)
 checkerOk = (env : ok env t)
 
@@ -789,28 +592,16 @@ checkApplicationSymbols = (policy argSymbol outSymbol env fnView :
   lazyList
     (_ : checkerErr errorTagZeroArityFunction t env)
     (argView restArgs :
-      let actualView = instantiateView argSymbol (actualViewFor argSymbol env) in
+      let resultView = fnResidual restArgs (fnResult fnView) in
-      lazyMaybe
+      lazyBool
+        (_ : checkerOk (extendEnv outSymbol resultView evidenceTagInferred env))
         (_ :
           lazyResult
             (diag envAtError : err diag envAtError)
-            (nextEnv _ : checkerOk (extendEnv outSymbol (fnResidual restArgs (fnResult fnView)) evidenceTagInferred nextEnv))
+            (nextEnv _ : checkerOk (extendEnv outSymbol resultView evidenceTagInferred nextEnv))
             (missingArgumentOrGuardedBase policy argSymbol argView env))
-        (subst :
+        (hasView? argSymbol argView env))
-          let nextEnv =
-            lazyBool
-              (_ : extendEnv argSymbol argView evidenceTagRequired env)
-              (_ : env)
-              (guardedView? argView) in
-          checkerOk
-            (extendEnv
-              outSymbol
-              (substituteView subst (fnResidual restArgs (fnResult fnView)))
-              evidenceTagInferred
-              nextEnv))
-        (matchView argView actualView t))
     (fnArgs fnView))
-
 -- ---------------------------------------------------------------------------
 -- View-tree checker artifact
 -- ---------------------------------------------------------------------------
@@ -964,7 +755,7 @@ checkTypedRequireNode = (policy node env :
             (hasView? symbol (guardedViewBase view) env))
         (_ : missingRequiredView policy symbol view env)
         (guardedView? view))
-    (hasCompatibleView? symbol view env))
+    (hasView? symbol view env))
 
 missingArgumentOrGuardedBase = (policy symbol view env :
   lazyBool
@@ -983,7 +774,7 @@ checkTypedApplyNode = (policy node env :
       lazyMaybe
         (_ : checkerOk env)
         (fnView : checkApplicationSymbols policy (typedApplyArg node) (typedNodeSymbol node) env fnView)
-        (findFnView (typedApplyCallee node) calleeViews))
+        (findFnView calleeViews))
     (lookupViews (typedApplyCallee node) env))
 
 checkTypedNode = (policy node env :
@@ -1762,8 +1553,8 @@ viewContractSelfTests = [
   (viewContractProbe (wellFormedView? (viewPair viewBool viewString)))
   (viewContractProbe (wellFormedView? (viewResult viewString viewBool)))
   (viewContractProbe (wellFormedView? (viewGuarded viewString (x : x))))
-  (viewContractProbe (wellFormedView? (viewVar 0)))
+  (viewContractProbe (not? (wellFormedView? (viewVar 0))))
-  (viewContractProbe (wellFormedView? (viewForall [(0)] (viewFn [(viewVar 0)] (viewVar 0)))))
+  (viewContractProbe (not? (wellFormedView? (viewForall [(0)] (viewFn [(viewVar 0)] (viewVar 0))))))
   (viewContractProbe (equal? (renderView viewBool) "Bool"))
   (viewContractProbe (equal? (renderView (viewList viewBool)) "List Bool"))
   (viewContractProbe (equal? (renderView (viewMaybe viewString)) "Maybe String"))

notes/view-contract-trust-provenance.md

@@ -1,122 +1,95 @@
-# View Contract trust provenance and controlled intensionality
+# View Contracts at the intensionality boundary
 
-## Problem
+## Conclusion
 
-Tree Calculus / tricu code can perform raw intensional observation through `t` /
+Tree Calculus does not support the abstraction theorem that the former
-`triage`-like power. Exact detection of whether an arbitrary term ever reaches
+parametric View design assumed. Views can remain useful as boundary metadata and
-rule 3 is undecidable: the SK fragment is already Turing-complete, and a program
+as instructions for runtime guard placement, but they must not be presented as
-can construct/apply an intensional observer iff an encoded machine halts.
+types, proofs of parametricity, or representation-hiding abstraction.
 
-Therefore View Contracts must not rely on an exact semantic test for "will this
+## Fundamental conflicts
-term inspect representation?".
 
-## Key correction
+### Raw observation defeats representation independence
 
-A purely syntactic invariant such as "the initial tree contains no
+A parametric contract such as:
-`Fork(Fork(_, _), _)`" is not reduction-closed. For example:
 
 ```text
-Fork (Stem (Fork a b)) c  ==>  Fork (Fork a b) c
+forall a. a -> a
 ```
 
-So absence of a current rule-3 redex is not enough.
+normally relies on code being unable to learn anything about `a`. A Tree
+Calculus term can inspect the tree supplied at `a`, distinguish
+representations, and return a representation-dependent value. The View variable
+does not hide or seal that tree.
 
-## Direction
+The same breaks existential abstraction. Advertising a payload as
+`exists repr. ...` changes no operational capability: a client can still
+inspect the representation directly.
 
-Use explicit provenance/capability discipline, not exact intensionality
+### Opaque payloads are asserted, not checked
-decision.
 
-View Contract checking and parametric checked-subset validation are distinct:
+A typed-value node carries an executable tree beside a View. Metadata validation
+deliberately treats that executable field as opaque. Consequently, accepting a
+node proves that the envelope and View are well formed; it does not prove that
+the tree denotes the advertised `Fn`, `List`, `Maybe`, or other structural
+View.
 
-- View Contract checking: verifies executable tree artifacts against declared
+Provenance labels do not change this. `Checked` and `Trusted` record where an
-  boundary Views.
+assertion came from, but neither is a derivation that another implementation can
-- Parametric checked-subset validation: verifies that abstraction/parametricity
+replay to establish the assertion.
-  claims do not depend on raw untrusted intensional observation.
 
-Unchecked/raw Tree Calculus can always inspect trees. Existential/abstract Views
+### Syntactic taint is not a semantic parametricity proof
-are checker-level opacity: checked clients cannot justify representation-specific
-operations unless an exported trusted capability/eliminator provides them.
 
-## Provenance model
+Rejecting direct uses of `t` or `triage` is neither complete nor a stable
+soundness boundary:
 
-Contract facts/artifacts should carry explicit provenance. Do not rely on module
+- an observer can be assembled after reduction;
-or catalog convention.
+- observation can arrive through higher-order or dynamically selected code;
+- unknown external code can hide observation;
+- absence of a rule-3 redex is not reduction-closed;
+- exact detection would subsume non-trivial termination/reachability questions.
 
-Recommended durable provenance classes:
+A conservative taint pass can define a programming convention, but it cannot
+justify the parametric or abstraction guarantees previously attached to Views.
 
-```text
+### Flow checking only checks represented flow
-Checked  -- derived by checked lowering / checker validation
-Trusted  -- asserted by a trusted boundary, e.g. a primitive eliminator API
-Unchecked -- no abstraction/parametricity guarantee; raw/assumed fact if exposed
-```
 
-The correct granularity is per exported View fact, not per module. A single
+The checker sees frontend-emitted value, application, and requirement nodes. It
-module may contain checked definitions, trusted eliminators, and unchecked raw
+can check consistency among those nodes, but it cannot establish that the graph
-helpers.
+faithfully represents every use performed by the opaque executable payload.
+This is useful artifact validation, not whole-program typing.
 
-## Controlled intensionality
+## Retained contract
 
-Raw intensionality should be tracked by dependency/provenance, not syntax-only.
+The reduced checker may soundly claim only:
 
-- Direct `triage` / arbitrary `t` eliminator use is raw intensional capability.
+1. View, node, and program envelopes satisfy their declared data schemas.
-- Trusted eliminators expose controlled observation and do not taint clients.
+2. Explicit monomorphic View facts are propagated consistently through the
-- Calling unchecked/untrusted code taints the caller for parametricity purposes.
+   represented application graph.
-- Constructors/literals are not automatically tainting unless they expose raw
+3. A `Guarded` View causes its executable predicate to run at represented
-  inspection power.
+   boundaries, and guard failure prevents checked execution.
+4. Content-addressed references prevent an attached View artifact from silently
+   drifting to a different stored object.
 
-Parametric checked mode rejects annotated definitions whose derivation depends
+Items 1, 2, and 4 establish metadata integrity, not semantic membership in an
-on raw/untrusted intensionality, while trusted facts may describe raw internals
+unguarded View. Item 3 is the only retained mechanism that observes an ordinary
-behind explicit contracts.
+runtime value.
 
-## Trusted eliminator kernel
+## Code direction
 
-First trusted observation capabilities should be the smallest useful kernels:
+The initial rollback therefore:
 
-```text
+- removes View-variable instantiation, substitution, and unification from the
-matchBool  : forall r. r -> r -> Bool -> r
+  portable checker;
-matchMaybe : forall a r. r -> (a -> r) -> Maybe a -> r
+- rejects `Var`, `Forall`, and `Exists` as checker inputs while reserving
-matchList  : forall a r. r -> (a -> List a -> r) -> List a -> r
+  their legacy tags for deterministic decoding;
-```
+- removes the frontend raw-intensionality taint pass;
+- removes polymorphic stdlib annotations and value-level View facts;
+- retains monomorphic View flow, artifact plumbing, diagnostics, and executable
+  guards.
 
-Derived functions should be checked against these trusted capabilities where
+Further simplification should treat unguarded structural Views as descriptive
-possible. Raw recursive kernels and other code
+labels. If stronger guarantees are desired later, they require an operational
-that passes through fixed-point/intensional machinery should publish explicit
+mechanism such as runtime recognizers/seals or a genuinely restricted language
-`Trusted` facts rather than being treated as checked.
+whose evaluator enforces the restriction. Metadata provenance alone is
-
+insufficient.
-Current stdlib shape:
-
-```text
-Checked annotations where the body checks through trusted capabilities:
-  maybeMap  : forall a b. (a -> b) -> Maybe a -> Maybe b
-  maybeBind : forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
-  maybeOr   : forall a. a -> Maybe a -> a
-
-Trusted value-level facts for raw/recursive stdlib boundaries:
-  headMaybe / lastMaybe / nthMaybe
-  append / map / filter / foldl / foldr
-  length / reverse / snoc / count / all? / any? / intersect
-  take / drop / splitAt / concatMap / find / partition / zipWith
-  string/list-byte helpers such as strLength, startsWith?, lines, words
-```
-
-Do not assign total contracts to partial APIs such as:
-
-```text
-head : List a -> a
-```
-
-Prefer `headMaybe : List a -> Maybe a`, or later introduce `NonEmptyList a`.
-
-## Implementation order
-
-Most-correct tractable path:
-
-1. Add contract provenance to the Haskell View model and portable artifacts. ✅
-2. Preserve provenance through module exports/imports/re-exports. ✅
-3. Teach checker environments to distinguish checked vs trusted facts. ✅
-4. Add trusted stdlib eliminator facts. ◐ initial value-level `viewFacts` landed for `matchBool`, `matchMaybe`, `matchList`; Haskell trusted catalog removed
-5. Add parametric-mode dependency/effect checking. ◐ local raw-dependency and unchecked-import rejection landed
-6. Annotate/publish derived stdlib Views at the right provenance. ◐ checked `maybeMap`/`maybeBind`/`maybeOr`; trusted value-level facts for recursive list combinators
-
-Avoid introducing implicit trusted catalogs before provenance exists; that would
-create semantics that later need to be unwound.

src/Check.hs

@@ -10,7 +10,7 @@ import Check.Core
 import Check.IO
 import ContentStore (ObjectRef, StorePath, getViewType)
 import Eval (evalTricu)
-import FileEval (LoadedSource(..), defaultStorePath, evaluateFile, evaluateFileWithStore, loadFileWithStore, valueViewFactsFromEnv)
+import FileEval (LoadedSource(..), defaultStorePath, evaluateFile, evaluateFileWithStore, loadFileWithStore)
 import Research (Env, ViewType)
 
 import qualified Data.Map as Map
@@ -29,8 +29,7 @@ checkFileWithStore store path = do
   let baseEnv = Map.union viewEnv (loadedImports loaded)
       checkerEnv = evalTricu baseEnv (loadedAst loaded)
   imports <- importedViewsFromResolvedModulesEither (loadImportedView store) (loadedModules loaded)
-  valueFacts <- either (errorWithoutStackTrace . ("invalid value-level viewFacts: " ++)) pure (valueViewFactsFromEnv checkerEnv)
+  checkProgramWithEnvAndImportedViews checkerEnv imports (loadedAst loaded)
-  checkProgramWithEnvAndImportedViews checkerEnv (imports ++ valueFacts) (loadedAst loaded)
 
 viewCheckerEnv :: Env
 viewCheckerEnv = unsafePerformIO (evaluateFile "./lib/view.tri")

src/Check/Core.hs

@@ -12,7 +12,6 @@ module Check.Core
   , lowerViewExpr
   ) where
 
-import Control.Applicative ((<|>))
 import Control.Monad.State.Strict
 import Data.Char (isDigit)
 import Data.Maybe (mapMaybe)
@@ -74,6 +73,11 @@ checkSourceWithEnvAndImportedViews checkerEnv imports source =
   checkProgramWithEnvAndImportedViews checkerEnv imports (parseTricu source)
 
 checkProgramWithEnvAndImportedViews :: Env -> [ImportedView] -> [TricuAST] -> IO String
+checkProgramWithEnvAndImportedViews _ _ asts
+  | not (any isAnnotatedDefinition asts) = pure "ok"
+  where
+    isAnnotatedDefinition SDefAnn {} = True
+    isAnnotatedDefinition _ = False
 checkProgramWithEnvAndImportedViews checkerEnv imports asts = do
   case lowerProgramWithImportedViewsDebugInEnv checkerEnv imports asts of
     Left err -> pure err
@@ -100,79 +104,6 @@ annotateDiagnostic debugNames message =
           "symbol " ++ symText ++ " (" ++ label ++ ") " ++ unwords rest
     _ -> message
 
-viewExprHasParametricBinder :: ViewExpr -> Bool
-viewExprHasParametricBinder expr = case expr of
-  VEVar _ -> True
-  VEVarId _ -> True
-  VEList items -> any viewExprHasParametricBinder items
-  VEApp fn arg -> viewExprHasParametricBinder fn || viewExprHasParametricBinder arg
-  VEForall binders body -> not (null binders) || viewExprHasParametricBinder body
-  VEExists binders body -> not (null binders) || viewExprHasParametricBinder body
-  VEName _ -> False
-  VEInt _ -> False
-  VEString _ -> False
-  VERaw _ -> False
-
-rawTaintedDefinitions :: Set.Set String -> [TricuAST] -> Map.Map String String
-rawTaintedDefinitions allowedExternalFacts asts = fixedPoint initiallyRaw
-  where
-    allowedFacts = allowedExternalFacts
-    definitions = Map.fromList
-      [ (name, (args, body))
-      | ast <- asts
-      , Just (name, args, body) <- [definitionBody ast]
-      ]
-    localNames = Map.keysSet definitions
-    initiallyRaw = Map.mapMaybeWithKey
-      (\name (args, body) ->
-        if name `Set.member` allowedFacts
-          then Nothing
-          else definitionUnsafeBaseReason localNames allowedFacts (Set.fromList args) body)
-      definitions
-
-    fixedPoint tainted =
-      let tainted' = Map.mapMaybeWithKey (transitiveReason tainted) definitions
-          combined = Map.union tainted tainted'
-      in if combined == tainted then tainted else fixedPoint combined
-
-    transitiveReason tainted name (args, body)
-      | name `Map.member` tainted = Nothing
-      | name `Set.member` allowedFacts = Nothing
-      | otherwise = case filter (`Map.member` tainted) (astFreeRefs (foldr Set.delete localNames args) body) of
-          helper : _ -> Just $ "depends on raw-tainted local helper " ++ show helper ++ " (" ++ tainted Map.! helper ++ ")"
-          [] -> Nothing
-
-    definitionBody ast = case ast of
-      SDef name args body -> Just (name, args, body)
-      SDefAnn name args _ body -> Just (name, defArgNames args, body)
-      _ -> Nothing
-
-definitionUnsafeBaseReason :: Set.Set String -> Set.Set String -> Set.Set String -> TricuAST -> Maybe String
-definitionUnsafeBaseReason localNames allowedExternalFacts bound ast = case ast of
-  SVar name _
-    | name `Set.member` bound -> Nothing
-    | name `Set.member` localNames -> Nothing
-    | name `Set.member` allowedExternalFacts -> Nothing
-    | name == "triage" -> Just "uses raw triage directly"
-    | otherwise -> Just $ "depends on unchecked or unknown external name " ++ show name
-  SInt _ -> Nothing
-  SStr _ -> Nothing
-  SList items -> firstJust (map (definitionUnsafeBaseReason localNames allowedExternalFacts bound) items)
-  SDef _ args body -> definitionUnsafeBaseReason localNames allowedExternalFacts (foldr Set.insert bound args) body
-  SDefAnn _ args _ body -> definitionUnsafeBaseReason localNames allowedExternalFacts (foldr Set.insert bound (defArgNames args)) body
-  SApp fn arg -> definitionUnsafeBaseReason localNames allowedExternalFacts bound fn <|> definitionUnsafeBaseReason localNames allowedExternalFacts bound arg
-  TLeaf -> Just "uses raw t directly"
-  TStem _ -> Just "uses raw t directly"
-  TFork _ _ -> Just "uses raw t directly"
-  SLambda args body -> definitionUnsafeBaseReason localNames allowedExternalFacts (foldr Set.insert bound args) body
-  SEmpty -> Nothing
-  SImport _ _ -> Nothing
-
-firstJust :: [Maybe a] -> Maybe a
-firstJust [] = Nothing
-firstJust (Just x : _) = Just x
-firstJust (Nothing : xs) = firstJust xs
-
 astFreeRefs :: Set.Set String -> TricuAST -> [String]
 astFreeRefs candidates ast = case ast of
   SVar name _ | name `Set.member` candidates -> [name]
@@ -187,6 +118,7 @@ astFreeRefs candidates ast = case ast of
   TStem inner -> astFreeRefs candidates inner
   TFork left right -> astFreeRefs candidates left ++ astFreeRefs candidates right
   SLambda args body -> astFreeRefs (foldr Set.delete candidates args) body
+  SLet name val body -> astFreeRefs candidates val ++ astFreeRefs (Set.delete name candidates) body
   SEmpty -> []
   SImport _ _ -> []
 
@@ -227,7 +159,6 @@ data LowerState = LowerState
   , knownNodeViews :: Map.Map Integer ViewExpr
   , nodePayloads :: Map.Map Integer T
   , debugNames :: Map.Map Integer String
-  , rawTaintedDefs :: Map.Map String String
   }
 
 type LowerM a = StateT LowerState (Either String) a
@@ -285,12 +216,6 @@ lowerProgramWithImportedViewsDebugInEnv checkerEnvForLowering imports asts = do
         , Just term <- [Map.lookup name checkerEnvForLowering]
         ]
       annotated = [ def | def@SDefAnn {} <- asts ]
-      allowedExternalFacts = Set.fromList
-        [ importedViewName imported
-        | imported <- imports
-        , importedViewProvenance imported `elem` [ViewChecked, ViewTrusted]
-        ]
-      taintedDefs = rawTaintedDefinitions allowedExternalFacts asts
       initialState = LowerState
         { nextSym = fromIntegral (Map.size tops + Map.size importedSyms)
         , topSyms = tops
@@ -299,7 +224,6 @@ lowerProgramWithImportedViewsDebugInEnv checkerEnvForLowering imports asts = do
         , knownNodeViews = Map.union trustedLocalKnown importKnown
         , nodePayloads = payloads
         , debugNames = Map.union topDebug importDebug
-        , rawTaintedDefs = taintedDefs
         }
   (localNodes, finalState) <- runStateT (lowerAnnotatedProgram annotated) initialState
   trustedLocalNodes <- mapM (lowerImportedView (nodePayloads finalState)) trustedLocalFacts
@@ -328,14 +252,10 @@ lowerAnnotatedProgram defs = do
 lowerDefinitionDeclaration :: TricuAST -> LowerM [String]
 lowerDefinitionDeclaration (SDefAnn name args ret _) = do
   let (_, _, declaredView) = canonicalDefinitionViews args ret
-  tainted <- gets rawTaintedDefs
+  sym <- symbolForTop name
-  if viewExprHasParametricBinder declaredView && name `Map.member` tainted
+  recordKnown sym declaredView
-    then liftEither (Left $ "parametric View definition " ++ show name ++ " depends on raw intensional Tree Calculus machinery (" ++ tainted Map.! name ++ "); use a trusted eliminator boundary instead")
+  node <- typedValueNode sym declaredView
-    else do
+  pure [node]
-      sym <- symbolForTop name
-      recordKnown sym declaredView
-      node <- typedValueNode sym declaredView
-      pure [node]
 lowerDefinitionDeclaration _ = liftEither (Left "internal check error: expected annotated definition")
 
 lowerDefinitionFlow :: TricuAST -> LowerM [String]
@@ -352,17 +272,7 @@ viewAnyType :: ViewExpr
 viewAnyType = VEName "Any"
 
 canonicalDefinitionViews :: [DefArg] -> Maybe ViewExpr -> ([DefArg], Maybe ViewExpr, ViewExpr)
-canonicalDefinitionViews args ret =
+canonicalDefinitionViews args ret = (args, ret, declaredDefinitionView args ret)
-  let rawView = declaredDefinitionView args ret
-      vars = Set.toList (freeViewVars rawView)
-      binderIds = zip vars [0..]
-      binderMap = Map.fromList binderIds
-      mappedArgs = map (mapDefArgView (rewriteViewVars binderMap)) args
-      mappedRet = fmap (rewriteViewVars binderMap) ret
-      mappedView = declaredDefinitionView mappedArgs mappedRet
-      binders = map snd binderIds
-      declaredView = if null vars then mappedView else VEForall binders mappedView
-  in (mappedArgs, mappedRet, declaredView)
 
 declaredDefinitionView :: [DefArg] -> Maybe ViewExpr -> ViewExpr
 declaredDefinitionView args ret =
@@ -372,10 +282,6 @@ declaredDefinitionView args ret =
   where
     resultType = maybe viewAnyType id ret
 
-mapDefArgView :: (ViewExpr -> ViewExpr) -> DefArg -> DefArg
-mapDefArgView f (DefBinder name mTy) = DefBinder name (fmap f mTy)
-mapDefArgView f (DefPhantom ty) = DefPhantom (f ty)
-
 argType :: DefArg -> ViewExpr
 argType (DefBinder _ Nothing) = viewAnyType
 argType (DefBinder _ (Just ty)) = ty
@@ -584,6 +490,14 @@ lowerExprKnownAgainst expr expected = case (expr, viewExprAsType expected) of
   (SApp (SApp (SVar "err" _) value) rest, Just (VTResult errView _)) ->
     lowerUnshadowedConstructor "err" expr expected $
       lowerResultConstructor expected (viewTypeToExpr errView) value rest
+  (SLet name value body, _) -> do
+    (valueSym, valueNodes, _) <- lowerExprKnown value
+    recordDebugName valueSym name
+    bodyResult <- withLocalAlias name valueSym (lowerExprKnownAgainst body expected)
+    let (bodySym, bodyNodes, bodyKnown) = bodyResult
+    pure (bodySym, valueNodes ++ bodyNodes, bodyKnown)
+  -- Hand-written immediately-applied lambda (not compiler output; let/where
+  -- now emit SLet). Kept for source that relies on alias semantics.
   (SApp (SLambda [name] body) value, _) -> do
     (valueSym, valueNodes, _) <- lowerExprKnown value
     bodyResult <- withLocalAlias name valueSym (lowerExprKnownAgainst body expected)
@@ -658,6 +572,14 @@ lowerExprKnown TLeaf = do
 lowerExprKnown (SList items) = do
   (sym, nodes, view, _) <- lowerListLiteral items
   pure (sym, nodes, Just view)
+lowerExprKnown (SLet name value body) = do
+  (valueSym, valueNodes, _) <- lowerExprKnown value
+  recordDebugName valueSym name
+  bodyResult <- withLocalAlias name valueSym (lowerExprKnown body)
+  let (bodySym, bodyNodes, bodyKnown) = bodyResult
+  pure (bodySym, valueNodes ++ bodyNodes, bodyKnown)
+-- Hand-written immediately-applied lambda (not compiler output; let/where
+-- now emit SLet). Kept for source that relies on alias semantics.
 lowerExprKnown (SApp (SLambda [name] body) value) = do
   (valueSym, valueNodes, known) <- lowerExprKnown value
   bodyResult <- withLocalAlias name valueSym (lowerExprKnown body)
@@ -880,8 +802,8 @@ lowerViewExpr ty = case ty of
   VEName "Byte" -> Right "viewByte"
   VEName "Unit" -> Right "viewUnit"
   VEName name -> Right name
-  VEVar name -> Right $ "viewVar " ++ show name
+  VEVar name -> Left $ "polymorphic View variables are unsupported: " ++ show name
-  VEVarId varId -> Right $ "viewVar " ++ show varId
+  VEVarId varId -> Left $ "polymorphic View variables are unsupported: " ++ show varId
   VEInt n -> Right (show n)
   VEString s -> Right (show s)
   VEList items -> do
@@ -911,45 +833,10 @@ lowerViewExpr ty = case ty of
     f <- lowerViewExpr func
     a <- lowerViewExpr arg
     Right $ parens f ++ " " ++ parens a
-  VEForall binders body -> do
+  VEForall _ _ -> Left "quantified View contracts are unsupported"
-    bodyExpr <- lowerViewExpr body
+  VEExists _ _ -> Left "existential View contracts are unsupported"
-    Right $ "viewForall " ++ lowerStringList binders ++ " " ++ parens bodyExpr
-  VEExists binders body -> do
-    bodyExpr <- lowerViewExpr body
-    Right $ "viewExists " ++ lowerStringList binders ++ " " ++ parens bodyExpr
   VERaw raw -> Right raw
 
-lowerStringList :: [Integer] -> String
-lowerStringList items = "[" ++ unwords (map (parens . show) items) ++ "]"
-
-quantifyFreeViewVars :: ViewExpr -> ViewExpr
-quantifyFreeViewVars view =
-  let vars = Set.toList (freeViewVars view)
-      binderIds = zip vars [0..]
-      binderMap = Map.fromList binderIds
-      body = rewriteViewVars binderMap view
-      binders = map snd binderIds
-  in if null vars then view else VEForall binders body
-
-rewriteViewVars :: Map.Map String Integer -> ViewExpr -> ViewExpr
-rewriteViewVars binderMap view = case view of
-  VEVar name -> maybe (VEVar name) VEVarId (Map.lookup name binderMap)
-  VEList items -> VEList (map (rewriteViewVars binderMap) items)
-  VEApp f a -> VEApp (rewriteViewVars binderMap f) (rewriteViewVars binderMap a)
-  VEForall binders body -> VEForall binders (rewriteViewVars binderMap body)
-  VEExists binders body -> VEExists binders (rewriteViewVars binderMap body)
-  _ -> view
-
-freeViewVars :: ViewExpr -> Set.Set String
-freeViewVars view = case view of
-  VEVar name -> Set.singleton name
-  VEVarId _ -> Set.empty
-  VEList items -> Set.unions (map freeViewVars items)
-  VEApp f a -> Set.union (freeViewVars f) (freeViewVars a)
-  VEForall _ body -> freeViewVars body
-  VEExists _ body -> freeViewVars body
-  _ -> Set.empty
-
 treeSource :: T -> String
 treeSource Leaf = "t"
 treeSource (Stem x) = "(t " ++ treeSource x ++ ")"

src/Check/IO.hs

@@ -105,6 +105,7 @@ instrumentIOContinuations asts = mapM transformTop asts
       SApp (SVar "io" h) action -> SApp (SVar "io" h) <$> transformIOAction action
       SApp f a -> SApp <$> transformExpr f <*> transformExpr a
       SLambda params body -> SLambda params <$> transformExpr body
+      SLet name val body -> SLet name <$> transformExpr val <*> transformExpr body
       TStem x -> TStem <$> transformExpr x
       TFork x y -> TFork <$> transformExpr x <*> transformExpr y
       _ -> pure expr
@@ -118,6 +119,7 @@ instrumentIOContinuations asts = mapM transformTop asts
         SApp <$> (SApp (SVar "bind" h) <$> transformIOAction left) <*> (SLambda params <$> transformIOAction body)
       SApp f a -> SApp <$> transformIOAction f <*> transformIOAction a
       SLambda params body -> SLambda params <$> transformIOAction body
+      SLet name val body -> SLet name <$> transformIOAction val <*> transformIOAction body
       _ -> transformExpr action
 
     checkedPureActionFor value =
@@ -183,6 +185,7 @@ mentionsContractedName contracts expr = case expr of
   SVar name _ -> Map.member name contracts
   SApp f a -> mentionsContractedName contracts f || mentionsContractedName contracts a
   SLambda _ body -> mentionsContractedName contracts body
+  SLet _ val body -> mentionsContractedName contracts val || mentionsContractedName contracts body
   SList items -> any (mentionsContractedName contracts) items
   TStem x -> mentionsContractedName contracts x
   TFork x y -> mentionsContractedName contracts x || mentionsContractedName contracts y
@@ -372,6 +375,7 @@ substAst subst expr = case expr of
   SVar name Nothing -> Map.findWithDefault expr name subst
   SApp f a -> SApp (substAst subst f) (substAst subst a)
   SLambda params body -> SLambda params (substAst (foldr Map.delete subst params) body)
+  SLet name val body -> SLet name (substAst subst val) (substAst (Map.delete name subst) body)
   SList items -> SList (map (substAst subst) items)
   TStem x -> TStem (substAst subst x)
   TFork x y -> TFork (substAst subst x) (substAst subst y)
@@ -397,6 +401,7 @@ astSource expr = case expr of
   SList items -> "[" ++ unwords (map (parens . astSource) items) ++ "]"
   SApp f a -> parens (astSource f) ++ " " ++ parens (astSource a)
   SLambda params body -> parens (unwords params ++ " : " ++ astSource body)
+  SLet name val body -> parens ("let " ++ name ++ " = " ++ astSource val ++ " in " ++ astSource body)
   TLeaf -> "t"
   TStem x -> "(t " ++ astSource x ++ ")"
   TFork x y -> "(t " ++ astSource x ++ " " ++ astSource y ++ ")"

src/Eval.hs

@@ -75,6 +75,7 @@ evalTricu env x = go env (reorderDefs env (map recoverParams x))
 evalASTSync :: Env -> TricuAST -> T
 evalASTSync env term = case term of
   SLambda _ _ -> evalASTSync env (elimLambda term)
+  SLet name val body -> evalASTSync env (SApp (SLambda [name] body) val)
   SVar name Nothing -> case Map.lookup name env of
     Just v -> v
     Nothing -> errorWithoutStackTrace $ "Variable " ++ name ++ " not defined"
@@ -108,6 +109,7 @@ annotatedBinders (DefPhantom _ : rest) = annotatedBinders rest
 elimLambda :: TricuAST -> TricuAST
 elimLambda = go
   where
+    go (SLet name val body) = go (SApp (SLambda [name] body) val)
     go term
       | etaReduction term   = go (etaReduceResult term)
       | triagePattern term  = _TRI
@@ -190,6 +192,8 @@ freeVars (SVar v Nothing) = Set.singleton v
 freeVars (SVar v (Just _)) = Set.singleton v
 freeVars (SApp t u) = Set.union (freeVars t) (freeVars u)
 freeVars (SLambda vs body) = Set.difference (freeVars body) (Set.fromList vs)
+freeVars (SLet name val body) =
+  Set.union (freeVars val) (Set.delete name (freeVars body))
 freeVars (SDef _ params body) = Set.difference (freeVars body) (Set.fromList params)
 freeVars (SDefAnn _ args _ body) = Set.difference (freeVars body) (Set.fromList (annotatedBinders args))
 freeVars (TStem t) = freeVars t
@@ -297,6 +301,7 @@ findVarNames ast = case ast of
   SVar name _ -> [name]
   SApp a b -> findVarNames a ++ findVarNames b
   SLambda args body -> findVarNames body \\ args
+  SLet name val body -> findVarNames val ++ (findVarNames body \\ [name])
   SDef name args body -> name : (findVarNames body \\ args)
   SDefAnn name args _ body -> name : (findVarNames body \\ annotatedBinders args)
   _ -> []
@@ -317,6 +322,7 @@ toDB env = \case
   SInt n       -> BInt n
   SList xs     -> BList (map (toDB env) xs)
   SEmpty       -> BEmpty
+  SLet name val body -> toDB env (SApp (SLambda [name] body) val)
   SDef{}       -> error "toDB: unexpected SDef at this stage"
   SDefAnn{}    -> error "toDB: unexpected SDefAnn at this stage"
   SImport _ _  -> BEmpty

src/FileEval.hs

@@ -14,7 +14,6 @@ module FileEval
   , compileFileWithStore
   , loadFileWithStore
   , loadFileWithStoreMode
-  , valueViewFactsFromEnv
   , defaultStorePath
   ) where
 
@@ -36,8 +35,6 @@ import Wire (buildBundle, encodeBundle, decodeBundle, verifyBundle, Bundle(..))
 
 import Data.List       (partition, isPrefixOf)
 import Data.Maybe      (mapMaybe)
-import Control.Monad   (forM)
-import qualified Data.Set as Set
 import System.Directory (getHomeDirectory, getTemporaryDirectory)
 import System.FilePath ((</>))
 import System.Exit (die)
@@ -204,12 +201,9 @@ buildWorkspaceModule ctx store moduleName sourcePath = do
   localViewsResult <- localViews
   resolvedLocalViews <- either (errorWithoutStackTrace . (("Workspace module " ++ show moduleName ++ " has invalid exported View Contract annotation: ") ++)) pure localViewsResult
   importedViews <- importedViewsFromResolvedModulesEither (getViewType store) (loadedModules loaded)
-  valueFacts <- either (errorWithoutStackTrace . (("Workspace module " ++ show moduleName ++ " has invalid value-level viewFacts: ") ++)) pure (valueViewFactsFromEnv env)
-  validateValueViewFactExports moduleName names valueFacts
   let localViewFacts = Map.map (\view -> (view, ViewChecked)) resolvedLocalViews
       importedViewFacts = Map.fromList [(importedViewName iv, (importedViewType iv, importedViewProvenance iv)) | iv <- importedViews]
-      valueViewFacts = Map.fromList [(importedViewName iv, (importedViewType iv, importedViewProvenance iv)) | iv <- valueFacts]
+      exportViewFacts = Map.union localViewFacts importedViewFacts
-      exportViewFacts = Map.unions [localViewFacts, valueViewFacts, importedViewFacts]
   exports <- mapM (buildExport env exportViewFacts) names
   manifestHash <- putManifest store (ModuleManifest [] exports)
   writeAlias store ModuleAlias (T.pack moduleName) (ObjectRef (unDomain manifestDomain) manifestHash)
@@ -237,62 +231,12 @@ enforceWorkspaceModuleContracts store moduleName importEnv modules asts
       viewEnv <- evaluateFileWithContextWithStoreAndMode IgnoreContracts (Just store) Map.empty "./lib/view.tri"
       let checkerEnv = evalTricu (Map.union viewEnv importEnv) asts
       imports <- importedViewsFromResolvedModulesEither (getViewType store) modules
-      valueFacts <- either (errorWithoutStackTrace . (("Workspace module " ++ show moduleName ++ " has invalid value-level viewFacts: ") ++)) pure (valueViewFactsFromEnv checkerEnv)
+      resultText <- checkProgramWithEnvAndImportedViews checkerEnv imports asts
-      resultText <- checkProgramWithEnvAndImportedViews checkerEnv (imports ++ valueFacts) asts
       case resultText of
         "ok" -> pure ()
         diagnostic -> errorWithoutStackTrace $
           "Workspace module " ++ show moduleName ++ " failed View Contract check: " ++ diagnostic
 
-valueViewFactsFromEnv :: Env -> Either String [ImportedView]
-valueViewFactsFromEnv env = case Map.lookup "viewFacts" env of
-  Nothing -> Right []
-  Just factsTree -> do
-    facts <- context "viewFacts is not a list" (toList factsTree)
-    decoded <- forM (zip [0 :: Int ..] facts) (uncurry decodeFactAt)
-    rejectDuplicateFacts decoded
-    pure decoded
-  where
-    decodeFactAt index factTree = do
-      (nameTree, rest) <- context prefix (pairParts factTree)
-      name <- context (prefix ++ ": export name is not a string") (toString nameTree)
-      (provenanceTree, viewTree) <- context (prefixFor name ++ ": payload is not a pair") (pairParts rest)
-      provenance <- context (prefixFor name ++ ": invalid provenance") (decodeProvenance provenanceTree)
-      view <- context (prefixFor name ++ ": malformed View") (treeToViewType viewTree)
-      pure (ImportedView name view provenance)
-      where
-        prefix = "viewFacts[" ++ show index ++ "]"
-        prefixFor name = prefix ++ " for " ++ show name
-
-    pairParts (Fork left right) = Right (left, right)
-    pairParts _ = Left "expected pair"
-
-    decodeProvenance tree = do
-      n <- toNumber tree
-      case n of
-        0 -> Right ViewChecked
-        1 -> Right ViewTrusted
-        2 -> Right ViewUnchecked
-        _ -> Left $ "unknown provenance tag " ++ show n
-
-    rejectDuplicateFacts facts = go Set.empty facts
-      where
-        go _ [] = Right ()
-        go seen (fact : rest)
-          | importedViewName fact `Set.member` seen = Left $ "duplicate viewFacts entry for " ++ show (importedViewName fact)
-          | otherwise = go (Set.insert (importedViewName fact) seen) rest
-
-    context label = either (Left . ((label ++ ": ") ++)) Right
-
-validateValueViewFactExports :: String -> [String] -> [ImportedView] -> IO ()
-validateValueViewFactExports moduleName exportedNames facts = do
-  let exported = Set.fromList exportedNames
-      missing = [importedViewName fact | fact <- facts, importedViewName fact `Set.notMember` exported]
-  case missing of
-    [] -> pure ()
-    name : _ -> errorWithoutStackTrace $
-      "Workspace module " ++ show moduleName ++ " has value-level viewFacts for non-exported name " ++ show name
-
 isAnnotatedDefinition :: TricuAST -> Bool
 isAnnotatedDefinition SDefAnn {} = True
 isAnnotatedDefinition _ = False
@@ -300,13 +244,10 @@ isAnnotatedDefinition _ = False
 topLevelDefinitions :: [TricuAST] -> [String]
 topLevelDefinitions = mapMaybe go
   where
-    go (SDef name _ _) | not (isViewFactMetadataName name) = Just name
+    go (SDef name _ _) = Just name
-    go (SDefAnn name _ _ _) | not (isViewFactMetadataName name) = Just name
+    go (SDefAnn name _ _ _) = Just name
     go _ = Nothing
 
-isViewFactMetadataName :: String -> Bool
-isViewFactMetadataName name = name == "viewFacts"
-
 topLevelDefinitionViews :: [TricuAST] -> Map.Map String ViewExpr
 topLevelDefinitionViews asts = Map.fromList (mapMaybe go asts)
   where
@@ -328,7 +269,7 @@ resolveViewExpression checkerEnv view = do
     Left err -> Left $ "could not validate view expression " ++ show expr ++ ": " ++ err
 
 definitionView :: [DefArg] -> Maybe ViewExpr -> ViewExpr
-definitionView args resultView = quantifyFreeViewVars $
+definitionView args resultView =
   case argViews of
     [] -> finalView
     _  -> VEApp (VEApp (VEName "Fn") (VEList argViews)) finalView
@@ -336,34 +277,6 @@ definitionView args resultView = quantifyFreeViewVars $
     argViews = map defArgView args
     finalView = maybe exportedViewAny id resultView
 
-quantifyFreeViewVars :: ViewExpr -> ViewExpr
-quantifyFreeViewVars view =
-  let vars = Set.toList (freeViewVars view)
-      binderIds = zip vars [0..]
-      binderMap = Map.fromList binderIds
-      body = rewriteViewVars binderMap view
-      binders = map snd binderIds
-  in if null vars then view else VEForall binders body
-
-rewriteViewVars :: Map.Map String Integer -> ViewExpr -> ViewExpr
-rewriteViewVars binderMap view = case view of
-  VEVar name -> maybe (VEVar name) VEVarId (Map.lookup name binderMap)
-  VEList items -> VEList (map (rewriteViewVars binderMap) items)
-  VEApp f a -> VEApp (rewriteViewVars binderMap f) (rewriteViewVars binderMap a)
-  VEForall binders body -> VEForall binders (rewriteViewVars binderMap body)
-  VEExists binders body -> VEExists binders (rewriteViewVars binderMap body)
-  _ -> view
-
-freeViewVars :: ViewExpr -> Set.Set String
-freeViewVars view = case view of
-  VEVar name -> Set.singleton name
-  VEVarId _ -> Set.empty
-  VEList items -> Set.unions (map freeViewVars items)
-  VEApp f a -> Set.union (freeViewVars f) (freeViewVars a)
-  VEForall _ body -> freeViewVars body
-  VEExists _ body -> freeViewVars body
-  _ -> Set.empty
-
 defArgView :: DefArg -> ViewExpr
 defArgView (DefBinder _ Nothing) = exportedViewAny
 defArgView (DefBinder _ (Just ty)) = ty

src/Main.hs

@@ -17,11 +17,13 @@ import FileEval
   )
 import IODriver (IOPermissions(..), runIO)
 import Parser (parseTricu)
-import REPL (repl)
+import REPL (repl, replWithStore)
 import Research (T, EvaluatedForm(..), Env, formatT, exportDag)
 import Wire (encodeBundle, defaultExportNames, Bundle(..))
 
-import Control.Monad (foldM, unless, when)
+import Control.Monad (foldM, forM, unless, when)
+import Data.Char (isAlphaNum)
+import Data.List (sortOn)
 import qualified Data.Text as T
 import Data.Version (showVersion)
 import Paths_tricu (version)
@@ -31,13 +33,18 @@ import qualified Data.ByteString as BS
 import qualified Data.ByteString.Lazy as BL
 import qualified Data.Sequence as Seq
 import qualified Data.Map as Map
-import System.Directory (getHomeDirectory)
+import System.Directory (createDirectoryIfMissing, getHomeDirectory)
 import System.FilePath (takeBaseName, (</>))
 
 -- ---------------------------------------------------------------------------
 -- CLI argument types
 -- ---------------------------------------------------------------------------
 
+data AppArgs = AppArgs
+  { globalStore :: Maybe FilePath
+  , appCommand   :: TricuArgs
+  } deriving (Show)
+
 data TricuArgs
   = Repl
   | Check
@@ -74,6 +81,8 @@ data TricuArgs
       , exportOutput  :: FilePath
       , exportNames   :: [String]
       , exportStore   :: Maybe FilePath
+      , exportAll     :: Bool
+      , exportSplit   :: Bool
       , dag           :: Bool
       }
   | StoreAliasList
@@ -251,6 +260,14 @@ exportParser = ArboricxExport
      <> metavar "PATH"
      <> help "Content-addressed store path"
       ))
+  <*> switch
+      ( long "all"
+     <> help "Export all name aliases that point at tree-term objects"
+      )
+  <*> switch
+      ( long "split"
+     <> help "Write one single-export bundle per export; --output is treated as a directory"
+      )
   <*> switch
       ( long "dag"
      <> help "Export as a topologically-sorted DAG node table instead of a bundle"
@@ -297,9 +314,15 @@ storeAliasGetParser = StoreAliasGet
 versionStr :: String
 versionStr = "tricu " ++ showVersion version
 
-tricuParser :: Parser TricuArgs
+tricuParser :: Parser AppArgs
-tricuParser = (subparser topCommands <|> pure Repl)
+tricuParser = AppArgs
-  <**> infoOption versionStr (long "version" <> help "Show version")
+  <$> optional (option str
+      ( long "store"
+     <> metavar "PATH"
+     <> help "Global content-addressed store path used by commands and the REPL unless a subcommand overrides it"
+      ))
+  <*> ((subparser topCommands <|> pure Repl)
+      <**> infoOption versionStr (long "version" <> help "Show version"))
   where
     topCommands = mconcat
       [ command "check" (info (checkParser <**> helper)
@@ -342,13 +365,15 @@ storeAliasParser = subparser $ mconcat
 
 main :: IO ()
 main = do
-  args <- execParser $ info (tricuParser <**> helper)
+  appArgs <- execParser $ info (tricuParser <**> helper)
     ( fullDesc
    <> progDesc "Exploring Tree Calculus"
    <> header versionStr
     )
+  let mGlobalStore = globalStore appArgs
+      args = applyGlobalStore mGlobalStore (appCommand appArgs)
   case args of
-    Repl               -> runRepl
+    Repl               -> runReplWithStore mGlobalStore
     Check {}           -> runCheck args
     Eval {}            -> runEval args
     ArboricxCompile {} -> runCompile args
@@ -362,11 +387,31 @@ main = do
 -- Command runners
 -- ---------------------------------------------------------------------------
 
+applyGlobalStore :: Maybe FilePath -> TricuArgs -> TricuArgs
+applyGlobalStore mGlobal args = case args of
+  Repl -> Repl
+  Check {} -> args { checkStore = preferLocal (checkStore args) }
+  Eval {} -> args { evalStore = preferLocal (evalStore args) }
+  ArboricxCompile {} -> args { compileStore = preferLocal (compileStore args) }
+  ArboricxImport {} -> args { importStore = preferLocal (importStore args) }
+  ArboricxExport {} -> args { exportStore = preferLocal (exportStore args) }
+  StoreAliasList {} -> args { storePathOpt = preferLocal (storePathOpt args) }
+  StoreAliasGet {} -> args { storePathOpt = preferLocal (storePathOpt args) }
+  where
+    preferLocal local = case local of
+      Just _  -> local
+      Nothing -> mGlobal
+
 runRepl :: IO ()
-runRepl = do
+runRepl = runReplWithStore Nothing
+
+runReplWithStore :: Maybe FilePath -> IO ()
+runReplWithStore mStore = do
   putStrLn "Welcome to the tricu REPL"
   putStrLn "You may exit with `CTRL+D` or the `!exit` command."
-  repl
+  case mStore of
+    Nothing -> repl
+    Just store -> replWithStore (StorePath store)
 
 runCheck :: TricuArgs -> IO ()
 runCheck opts = do
@@ -466,23 +511,46 @@ runExportBundle opts = do
       modules = exportModules opts
       out     = exportOutput opts
       names   = exportNames opts
+      allFlag = exportAll opts
+      splitFlag = exportSplit opts
   when (null out) $ die "tricu arboricx export: --output is required"
-  when (null targets && null modules) $
+  when (null targets && null modules && not allFlag) $
-    die "tricu arboricx export: at least one --target or --module is required"
+    die "tricu arboricx export: at least one --target, --module, or --all is required"
+  when (splitFlag && not (null names)) $
+    die "tricu arboricx export --split: --name is not supported; split bundles use their export names"
   store <- resolveStorePath (exportStore opts)
+  allEntries <- if allFlag then resolveAllNameExports store else pure []
   targetRoots <- mapM (resolveStoreTarget store) targets
   moduleRoots <- concat <$> mapM (resolveModuleExports store) modules
   let targetEntries = zip (defaultExportNames (length targetRoots)) targetRoots
-      entries = targetEntries ++ moduleRoots
+      entries = allEntries ++ targetEntries ++ moduleRoots
       expNames = if null names then map fst entries else map T.pack names
+  when (null entries) $
+    die "tricu arboricx export: no tree-term exports found"
   when (length expNames /= length entries) $
     die "tricu arboricx export: number of --name values must match number of exported roots"
-  bundle <- packBundleFromStore store (zip expNames (map snd entries))
+  if splitFlag
-  let bundleData = encodeBundle bundle
+    then runExportBundleSplit store out (zip expNames (map snd entries))
-  BL.writeFile out (BL.fromStrict bundleData)
+    else do
-  putStrLn $ "Exported bundle with " ++ show (length entries) ++ " export(s) to " ++ out
+      bundle <- packBundleFromStore store (zip expNames (map snd entries))
-  putStrLn $ "  nodes: " ++ show (Seq.length (bundleNodes bundle))
+      let bundleData = encodeBundle bundle
-  putStrLn $ "  size: " ++ show (BS.length bundleData) ++ " bytes"
+      BL.writeFile out (BL.fromStrict bundleData)
+      putStrLn $ "Exported bundle with " ++ show (length entries) ++ " export(s) to " ++ out
+      putStrLn $ "  nodes: " ++ show (Seq.length (bundleNodes bundle))
+      putStrLn $ "  size: " ++ show (BS.length bundleData) ++ " bytes"
+
+runExportBundleSplit :: StorePath -> FilePath -> [(T.Text, ObjectHash)] -> IO ()
+runExportBundleSplit store outDir entries = do
+  createDirectoryIfMissing True outDir
+  written <- forM (zip [0 :: Int ..] entries) $ \(i, (name, root)) -> do
+    bundle <- packBundleFromStore store [(name, root)]
+    let bundleData = encodeBundle bundle
+        path = outDir </> splitBundleFileName i name
+    BL.writeFile path (BL.fromStrict bundleData)
+    pure (path, Seq.length (bundleNodes bundle), BS.length bundleData)
+  putStrLn $ "Exported " ++ show (length written) ++ " split bundle(s) to " ++ outDir
+  mapM_ (\(path, nodeCount, byteCount) ->
+    putStrLn $ "  " ++ path ++ " (nodes: " ++ show nodeCount ++ ", size: " ++ show byteCount ++ " bytes)") written
 
 runStoreAliasList :: TricuArgs -> IO ()
 runStoreAliasList opts = do
@@ -543,6 +611,19 @@ resolveStoreTarget store target = do
     Just _ -> return root
     Nothing -> die $ "Term not found in store: " ++ target
 
+resolveAllNameExports :: StorePath -> IO [(T.Text, ObjectHash)]
+resolveAllNameExports store = do
+  aliases <- sortOn fst <$> listAliases store NameAlias
+  fmap concat $ mapM exportAlias aliases
+  where
+    exportAlias (name, ref)
+      | objectRefKind ref /= unDomain treeTermDomain = pure []
+      | otherwise = do
+          mTree <- getTreeTerm store (objectRefHash ref)
+          case mTree of
+            Nothing -> die $ "Name alias tree term not found: " ++ T.unpack name
+            Just _  -> pure [(name, objectRefHash ref)]
+
 resolveModuleExports :: StorePath -> String -> IO [(T.Text, ObjectHash)]
 resolveModuleExports store moduleTarget = do
   manifestHash <- resolveModuleManifestHash store moduleTarget
@@ -574,6 +655,17 @@ resolveModuleManifestHash store moduleTarget = do
 formatObjectRef :: ObjectRef -> String
 formatObjectRef ref = T.unpack (objectRefKind ref) ++ " " ++ T.unpack (objectRefHash ref)
 
+splitBundleFileName :: Int -> T.Text -> FilePath
+splitBundleFileName i name = show i ++ "-" ++ sanitize (T.unpack name) ++ ".arboricx"
+  where
+    sanitize [] = "export"
+    sanitize xs = case map safeChar xs of
+      [] -> "export"
+      ys -> ys
+    safeChar c
+      | isAlphaNum c || c == '-' || c == '_' || c == '.' = c
+      | otherwise = '_'
+
 writeOutput :: FilePath -> String -> IO ()
 writeOutput path content
   | null path = putStr content

src/Parser.hs

@@ -496,7 +496,7 @@ whereChainP parseBody = do
     Nothing -> pure body
     Just (name, args, value) ->
       let boundValue = foldr (\p acc -> SLambda [p] acc) value args
-      in pure (SApp (SLambda [name] body) boundValue)
+      in pure (SLet name boundValue body)
 
 whereBindingP :: TokParser (String, [String], TricuAST)
 whereBindingP = do
@@ -524,7 +524,7 @@ letP = do
   bodyIndent <- skipNestedNewlinesGetIndent
   body <- exprAtIndentP bodyIndent
   let boundValue = foldr (\p acc -> SLambda [p] acc) value args
-  pure (SApp (SLambda [name] body) boundValue)
+  pure (SLet name boundValue body)
 
 data DoStmt
   = DoBind String TricuAST

src/REPL.hs

@@ -10,7 +10,17 @@ import FileEval
   )
 import Parser (parseTricu)
 import Research (EvaluatedForm(..), Env, formatT)
-import ContentStore (StorePath(..))
+import ContentStore
+  ( AliasKind(..)
+  , ObjectRef(..)
+  , StorePath(..)
+  , cachedFilesystemResolver
+  , getTreeTerm
+  , readAlias
+  , treeTermDomain
+  , unDomain
+  )
+import Module.Resolver (resolveModuleImport, resolvedModulesEnv)
 
 import Control.Exception (SomeException, catch, displayException)
 import Control.Monad.IO.Class (liftIO)
@@ -22,6 +32,7 @@ import System.Console.Haskeline
 import System.Directory (doesFileExist)
 
 import qualified Data.Map as Map
+import qualified Data.Text as T
 
 -- | Source-local REPL with the same filesystem CAS/module loader used by the
 -- CLI. View Contract checking is explicit (`!check`); evaluation can run in
@@ -35,8 +46,10 @@ data REPLState = REPLState
   }
 
 repl :: IO ()
-repl = do
+repl = defaultStorePath >>= replWithStore
-  store <- defaultStorePath
+
+replWithStore :: StorePath -> IO ()
+replWithStore store = do
   envRef <- newIORef Map.empty
   let settings = Settings
         { complete = completeRepl envRef
@@ -66,6 +79,8 @@ repl = do
             "!env" -> handleEnv state >> loop state
             _ | "!load" `isPrefixOf` s -> handleLoad state (strip $ drop 5 s)
               | "!check" `isPrefixOf` s -> handleCheck state (strip $ drop 6 s)
+              | "!use" `isPrefixOf` s -> handleUse state (strip $ drop 4 s)
+              | "!name" `isPrefixOf` s -> handleName state (strip $ drop 5 s)
               | "!store" `isPrefixOf` s -> handleStore state (strip $ drop 6 s)
               | "!format" `isPrefixOf` s -> handleFormat state (strip $ drop 7 s)
               | "!unchecked" `isPrefixOf` s -> handleUnchecked state (strip $ drop 10 s)
@@ -85,6 +100,8 @@ repl = do
       outputStrLn "  !output                - Change output format interactively"
       outputStrLn "  !format FORM           - Set output format: tree, fsl, ast, ternary, ascii, decode, number, string"
       outputStrLn "  !load FILE             - Load and evaluate a .tri file into the environment"
+      outputStrLn "  !use MODULE [NS]       - Load a module alias/manifest from the store (NS defaults to !Local)"
+      outputStrLn "  !name NAME [LOCAL]     - Load a name alias/tree-term hash from the store"
       outputStrLn "  !check FILE            - Check View Contract annotations in a .tri file"
       outputStrLn "  !store [PATH]          - Show or set the content-addressed store path"
       outputStrLn "  !unchecked [on|off]    - Show or set unchecked eval mode"
@@ -136,6 +153,49 @@ repl = do
               outputStrLn output
               loop state
 
+    handleUse :: REPLState -> String -> InputT IO ()
+    handleUse state arg = case words arg of
+      [] -> outputStrLn "Usage: !use MODULE [NAMESPACE]" >> loop state
+      [moduleTarget] -> loadModule moduleTarget "!Local"
+      [moduleTarget, namespace] -> loadModule moduleTarget namespace
+      _ -> outputStrLn "Usage: !use MODULE [NAMESPACE]" >> loop state
+      where
+        loadModule moduleTarget namespace = do
+          resolver <- liftIO $ cachedFilesystemResolver (replStore state)
+          resolved <- liftIO $ resolveModuleImport resolver moduleTarget namespace
+          let importedEnv = resolvedModulesEnv [resolved]
+              env' = Map.union importedEnv (replEnv state)
+          liftIO $ writeIORef (replEnvRef state) env'
+          outputStrLn $ "Loaded " ++ show (Map.size importedEnv) ++ " export(s) from store module " ++ moduleTarget
+          loop state { replEnv = env' }
+
+    handleName :: REPLState -> String -> InputT IO ()
+    handleName state arg = case words arg of
+      [] -> outputStrLn "Usage: !name NAME [LOCAL]" >> loop state
+      [name] -> loadName name name
+      [name, localName] -> loadName name localName
+      _ -> outputStrLn "Usage: !name NAME [LOCAL]" >> loop state
+      where
+        loadName name localName = do
+          let store = replStore state
+              nameText = T.pack name
+          mAlias <- liftIO $ readAlias store NameAlias nameText
+          let root = maybe nameText objectRefHash mAlias
+              badKind = case mAlias of
+                Just ref -> objectRefKind ref /= unDomain treeTermDomain
+                Nothing -> False
+          if badKind
+            then outputStrLn ("Name alias does not point at a tree term: " ++ name) >> loop state
+            else do
+              mTerm <- liftIO $ getTreeTerm store root
+              case mTerm of
+                Nothing -> outputStrLn ("Tree term not found in store: " ++ name) >> loop state
+                Just term -> do
+                  let env' = Map.insert localName term (replEnv state)
+                  liftIO $ writeIORef (replEnvRef state) env'
+                  outputStrLn $ "Loaded " ++ name ++ " as " ++ localName
+                  loop state { replEnv = env' }
+
     handleStore :: REPLState -> String -> InputT IO ()
     handleStore state path
       | null path = do
@@ -201,6 +261,8 @@ completeRepl envRef input@(left, _right)
       , "!reset"
       , "!help"
       , "!load"
+      , "!use"
+      , "!name"
       , "!check"
       , "!store"
       , "!unchecked"

src/Research.hs

@@ -84,6 +84,11 @@ data TricuAST
   | TStem TricuAST
   | TFork TricuAST TricuAST
   | SLambda [String] TricuAST
+  -- Non-recursive local binding: `name = boundValue` scoped over `body`.
+  -- Produced by let/where desugaring. `boundValue` already folds any binding
+  -- arguments into nested SLambda. Semantically equal to
+  --   SApp (SLambda [name] body) boundValue
+  | SLet String TricuAST TricuAST
   | SEmpty
   | SImport String String
   deriving (Show, Eq, Ord)

test/Spec.hs

@@ -80,7 +80,8 @@ tests = testGroup "Tricu Tests"
   --, parser
   --, simpleEvaluation
   --, lambdas
-  --, providedLibraries
+  , arithmetic
+  , providedLibraries
   --, maybeTests
   --, fileEval
   --, demos
@@ -94,7 +95,7 @@ tests = testGroup "Tricu Tests"
   --, binaryParserTests
   --, httpParsingTests
   --, contentStoreTests
-  , viewContractTests
+  --, viewContractTests
   --, ioDriverTests
   ]
 
@@ -336,7 +337,7 @@ parser = testGroup "Parser Tests"
 
   , testCase "Parse let expression" $ do
       let input  = "let x = t t in x"
-          expect = SApp (SLambda ["x"] (SVar "x" Nothing)) (SApp TLeaf TLeaf)
+          expect = SLet "x" (SApp TLeaf TLeaf) (SVar "x" Nothing)
       parseSingle input @?= expect
 
   , testCase "Evaluate let expression" $ do
@@ -344,18 +345,36 @@ parser = testGroup "Parser Tests"
 
   , testCase "Parse let function binding" $ do
       let input  = "let f x = x in f t"
-          expect = SApp (SLambda ["f"] (SApp (SVar "f" Nothing) TLeaf))
+          expect = SLet "f" (SLambda ["x"] (SVar "x" Nothing))
-                        (SLambda ["x"] (SVar "x" Nothing))
+                        (SApp (SVar "f" Nothing) TLeaf)
       parseSingle input @?= expect
 
   , testCase "Parse where expression" $ do
       let input  = "x where x = t t"
-          expect = SApp (SLambda ["x"] (SVar "x" Nothing)) (SApp TLeaf TLeaf)
+          expect = SLet "x" (SApp TLeaf TLeaf) (SVar "x" Nothing)
       parseSingle input @?= expect
 
   , testCase "Evaluate where expression" $ do
       tricuTestString "x where x = 1" @?= "Fork (Stem Leaf) Leaf"
 
+  , testCase "Parse where binding with arguments (SLet)" $ do
+      let input  = "f 3 where f x = x"
+          expect = SLet "f" (SLambda ["x"] (SVar "x" Nothing))
+                        (SApp (SVar "f" Nothing) (SInt 3))
+      parseSingle input @?= expect
+
+  , testCase "Evaluate where binding with arguments matches applied lambda" $ do
+      tricuTestString "f (t t) where f x = t x x"
+        @?= tricuTestString "(f : f (t t)) (x : t x x)"
+
+  , testCase "Evaluate nested let bindings" $ do
+      tricuTestString "let a = t t in let b = t in t a b"
+        @?= tricuTestString "t (t t) t"
+
+  , testCase "Inner let binding shadows outer binding" $ do
+      tricuTestString "let x = t in let x = t t in x"
+        @?= tricuTestString "t t"
+
   , testCase "Parse indented multiline definition body" $ do
       let input  = "x =\n  t\n    t"
           expect = SDef "x" [] (SApp TLeaf TLeaf)
@@ -1088,10 +1107,95 @@ providedLibraries = testGroup "Library Tests"
       let input = "unwords []"
           env = evalTricu allTestLibsEnv (parseTricu input)
       result env @?= ofString ""
+
+  , testCase "intercalate joins fields" $ do
+      let input = "intercalate \", \" [(\"a\") (\"b\") (\"c\")]"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofString "a, b, c"
+
+  , testCase "intercalate leaves a lone field alone" $ do
+      let input = "intercalate \", \" [(\"a\")]"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofString "a"
+
+  , testCase "intercalate empty list" $ do
+      let input = "intercalate \", \" []"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofString ""
+
+  , testCase "joinSuffix terminates every field" $ do
+      let input = "joinSuffix \"-\" [(\"a\") (\"b\")]"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofString "a-b-"
+
+  , testCase "splitOnByte splits on a byte" $ do
+      let input = "splitOnByte 58 \"a:b:c\""
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofList [ofString "a", ofString "b", ofString "c"]
+
+  , testCase "splitOnByte keeps empty fields" $ do
+      let input = "splitOnByte 58 \"a::b\""
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofList [ofString "a", ofString "", ofString "b"]
+
+  , testCase "splitOnByte trailing separator leaves an empty field" $ do
+      let input = "splitOnByte 58 \"a:\""
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofList [ofString "a", ofString ""]
+
+  , testCase "splitOnByte without a match" $ do
+      let input = "splitOnByte 58 \"abc\""
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofList [ofString "abc"]
+
+  , testCase "splitOnByte empty input" $ do
+      let input = "splitOnByte 58 \"\""
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofList [ofString ""]
+
+  , testCase "intercalate round trips splitOnByte" $ do
+      let input = "equal? (intercalate \":\" (splitOnByte 58 \"a:b:c\")) \"a:b:c\""
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= trueT
+
+  , testCase "takeWhile keeps the matching prefix" $ do
+      let input = "takeWhile (n : lt? n 3) [(1) (2) (3) (1)]"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofList [ofNumber 1, ofNumber 2]
+
+  , testCase "takeWhile stops at the first mismatch" $ do
+      let input = "takeWhile (n : lt? n 3) [(3) (1)]"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofList []
+
+  , testCase "dropWhile drops the matching prefix" $ do
+      let input = "dropWhile (n : lt? n 3) [(1) (2) (3) (1)]"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofList [ofNumber 3, ofNumber 1]
+
+  , testCase "dropWhile on an all matching list" $ do
+      let input = "dropWhile (n : lt? n 3) [(1) (2)]"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofList []
+
+  , testCase "trim strips surrounding spaces and tabs" $ do
+      let input = "trim \"  \\ttrimmed  \\t\""
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofString "trimmed"
+
+  , testCase "trim leaves interior bytes alone" $ do
+      let input = "trim \" a b \""
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofString "a b"
+
+  , testCase "trim all whitespace is empty" $ do
+      let input = "trim \" \\t \""
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofString ""
   ]
 
-arithmeticTests :: TestTree
+arithmetic :: TestTree
-arithmeticTests = testGroup "Arithmetic Tests"
+arithmetic = testGroup "Arithmetic Tests"
   [ testCase "isZero? on 0" $ do
       let input = "isZero? 0"
           env = evalTricu allTestLibsEnv (parseTricu input)
@@ -1271,6 +1375,181 @@ arithmeticTests = testGroup "Arithmetic Tests"
       let input = "isZero? (add 0 0)"
           env = evalTricu allTestLibsEnv (parseTricu input)
       result env @?= trueT
+
+  , testCase "div 10 3 = 3" $ do
+      let input = "div 10 3"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofNumber 3
+
+  , testCase "div 12 4 = 3 (exact)" $ do
+      let input = "div 12 4"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofNumber 3
+
+  , testCase "div 3 5 = 0 (divisor larger)" $ do
+      let input = "div 3 5"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofNumber 0
+
+  , testCase "div 7 1 = 7 (identity)" $ do
+      let input = "div 7 1"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofNumber 7
+
+  , testCase "div 0 5 = 0" $ do
+      let input = "div 0 5"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofNumber 0
+
+  , testCase "div 5 0 = 0 (div by zero)" $ do
+      let input = "div 5 0"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofNumber 0
+
+  , testCase "mod 10 3 = 1" $ do
+      let input = "mod 10 3"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofNumber 1
+
+  , testCase "mod 12 4 = 0 (exact)" $ do
+      let input = "mod 12 4"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofNumber 0
+
+  , testCase "mod 3 5 = 3 (divisor larger)" $ do
+      let input = "mod 3 5"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofNumber 3
+
+  , testCase "mod 7 1 = 0" $ do
+      let input = "mod 7 1"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofNumber 0
+
+  , testCase "mod 5 0 = 0 (mod by zero)" $ do
+      let input = "mod 5 0"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofNumber 0
+
+  , testCase "div mod consistency" $ do
+      let input = "equal? (add (mul 3 7) 4) 25"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= trueT
+
+  , testCase "pow 2 0 = 1" $ do
+      let input = "pow 2 0"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofNumber 1
+
+  , testCase "pow 2 3 = 8" $ do
+      let input = "pow 2 3"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofNumber 8
+
+  , testCase "pow 3 2 = 9" $ do
+      let input = "pow 3 2"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofNumber 9
+
+  , testCase "pow 0 0 = 1" $ do
+      let input = "pow 0 0"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofNumber 1
+
+  , testCase "pow 0 5 = 0" $ do
+      let input = "pow 0 5"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofNumber 0
+
+  , testCase "pow 1 10 = 1" $ do
+      let input = "pow 1 10"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofNumber 1
+
+  , testCase "pow 5 1 = 5" $ do
+      let input = "pow 5 1"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofNumber 5
+
+  , testCase "min 3 7 = 3" $ do
+      let input = "min 3 7"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofNumber 3
+
+  , testCase "min 7 3 = 3" $ do
+      let input = "min 7 3"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofNumber 3
+
+  , testCase "min 5 5 = 5" $ do
+      let input = "min 5 5"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofNumber 5
+
+  , testCase "min 0 5 = 0" $ do
+      let input = "min 0 5"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofNumber 0
+
+  , testCase "max 3 7 = 7" $ do
+      let input = "max 3 7"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofNumber 7
+
+  , testCase "max 7 3 = 7" $ do
+      let input = "max 7 3"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofNumber 7
+
+  , testCase "max 5 5 = 5" $ do
+      let input = "max 5 5"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofNumber 5
+
+  , testCase "max 0 5 = 5" $ do
+      let input = "max 0 5"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= ofNumber 5
+
+  , testCase "even? 0 = true" $ do
+      let input = "even? 0"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= trueT
+
+  , testCase "even? 1 = false" $ do
+      let input = "even? 1"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= falseT
+
+  , testCase "even? 2 = true" $ do
+      let input = "even? 2"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= trueT
+
+  , testCase "even? 7 = false" $ do
+      let input = "even? 7"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= falseT
+
+  , testCase "odd? 0 = false" $ do
+      let input = "odd? 0"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= falseT
+
+  , testCase "odd? 1 = true" $ do
+      let input = "odd? 1"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= trueT
+
+  , testCase "odd? 2 = false" $ do
+      let input = "odd? 2"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= falseT
+
+  , testCase "odd? 7 = true" $ do
+      let input = "odd? 7"
+          env = evalTricu allTestLibsEnv (parseTricu input)
+      result env @?= trueT
   ]
 
 fileEval :: TestTree
@@ -3216,30 +3495,6 @@ viewContractTests = testGroup "View Contract Tests"
                     view <- getViewType store viewRef
                     view @?= Right (VTFn [VTRef 10] (VTRef 10))
 
-  , testCase "Workspace modules publish explicitly quantified polymorphic views" $
-      withSystemTempDirectory "tricu-workspace-polymorphic-view" $ \dir -> do
-        let store = StorePath (dir </> "store")
-            utilPath = dir </> "util.tri"
-            mainPath = dir </> "main.tri"
-        writeFile (dir </> "tricu.workspace") "module util = util.tri\n"
-        writeFile utilPath "idP x@_a =@_a x\n"
-        writeFile mainPath "!import \"util\" Util\n\nmain =@String Util.idP \"hi\"\n"
-        _ <- evaluateFileWithStore (Just store) mainPath
-        mAlias <- readAlias store ModuleAlias "util"
-        case mAlias of
-          Nothing -> assertFailure "expected util module alias"
-          Just ref -> do
-            mManifest <- getManifest store (objectRefHash ref)
-            case mManifest of
-              Nothing -> assertFailure "expected util module manifest"
-              Just manifest -> case find ((== "idP") . unpack . moduleExportName) (moduleManifestExports manifest) of
-                Nothing -> assertFailure "expected idP export"
-                Just ex -> case moduleExportView ex of
-                  Nothing -> assertFailure "expected idP view ref"
-                  Just viewRef -> do
-                    view <- getViewType store viewRef
-                    view @?= Right (VTForall [0] (VTFn [VTVar 0] (VTVar 0)))
-
   , testCase "Workspace modules publish string custom view aliases" $
       withSystemTempDirectory "tricu-workspace-string-view-alias" $ \dir -> do
         let store = StorePath (dir </> "store")
@@ -3321,232 +3576,10 @@ viewContractTests = testGroup "View Contract Tests"
             ]
         readAlias store ModuleAlias "util" >>= (@?= Nothing)
 
-  , testCase "tricu check lowers free View variables under explicit Forall" $ do
+  , testCase "tricu check rejects polymorphic View variables" $ do
       case lowerSource "idP x@_a =@_a x\n" of
-        Left err -> assertFailure err
+        Left err -> assertBool "expected unsupported polymorphism diagnostic" $ "polymorphic View variables are unsupported" `isInfixOf` err
-        Right lowered -> do
+        Right _ -> assertFailure "expected polymorphic View rejection"
-          assertBool "expected polymorphic declaration to be explicitly quantified" $ "viewForall [(0)]" `isInfixOf` lowered
-          assertBool "expected quantified identity function body" $ "viewFn [(viewVar 0)] (viewVar 0)" `isInfixOf` lowered
-
-  , testCase "tricu check supports first-order polymorphic identity View variables" $ do
-      output <- checkSourceWithEnv allTestLibsEnv "idP x@_a =@_a x\nmain =@String idP \"hi\"\n"
-      output @?= "ok"
-
-  , testCase "tricu check propagates first-order polymorphic result relationships" $ do
-      output <- checkSourceWithEnv allTestLibsEnv "constP x@_a y@_b =@_a x\nmain =@String constP \"hi\" 1\n"
-      output @?= "ok"
-
-  , testCase "tricu check instantiates quantified Views at higher-order boundaries" $ do
-      output <- checkSourceWithEnv allTestLibsEnv "idP x@_a =@_a x\ncomposeP f@(Fn [_b] _c) g@(Fn [_a] _b) x@_a =@_c f (g x)\nmain =@String composeP idP idP \"hi\"\n"
-      output @?= "ok"
-
-  , testCase "tricu check matches quantified values against concrete Fn requirements" $ do
-      output <- checkSourceWithEnv allTestLibsEnv "idP x@_a =@_a x\nacceptSS f@(Fn [String] String) =@String f \"hi\"\nmain =@String acceptSS idP\n"
-      output @?= "ok"
-
-  , testCase "tricu check propagates nested polymorphic List relationships" $ do
-      output <- checkSourceWithEnv allTestLibsEnv "idList xs@(List _a) =@(List _a) xs\nmain =@(List String) idList [(\"hi\")]\n"
-      output @?= "ok"
-
-  , testCase "tricu check keeps polymorphic instantiation acyclic for reciprocal higher-order constraints" $ do
-      output <- checkSourceWithEnv allTestLibsEnv "idP x@_a =@_a x\nrel f@(Fn [_a] _b) g@(Fn [_b] _a) =@String \"ok\"\nmain =@String rel idP idP\n"
-      output @?= "ok"
-
-  , testCase "tricu check supports first-principles parametric stdlib island shapes" $ do
-      output <- checkSourceWithEnv allTestLibsEnv "idV x@_a =@_a x\nconstV x@_a y@_b =@_a x\ncomposeV f@(Fn [_b] _c) g@(Fn [_a] _b) x@_a =@_c f (g x)\nmain =@String composeV idV (constV \"hi\") 1\n"
-      output @?= "ok"
-
-  , testCase "tricu check rejects raw triage in parametric annotated definitions" $ do
-      output <- checkSourceWithEnv allTestLibsEnv "bad x@_a =@String triage \"leaf\" (_ : \"stem\") (_ _ : \"fork\") x\n"
-      output `containsAll` ["parametric View definition \"bad\"", "uses raw triage directly", "trusted eliminator boundary"]
-
-  , testCase "tricu check rejects raw t in parametric annotated definitions" $ do
-      output <- checkSourceWithEnv allTestLibsEnv "bad x@_a =@_a t\n"
-      output `containsAll` ["parametric View definition \"bad\"", "uses raw t directly", "trusted eliminator boundary"]
-
-  , testCase "tricu check rejects parametric definitions depending on local raw helpers" $ do
-      output <- checkSourceWithEnv allTestLibsEnv "raw x = triage \"leaf\" (_ : \"stem\") (_ _ : \"fork\") x\nbad x@_a =@String raw x\n"
-      output `containsAll` ["parametric View definition \"bad\"", "raw-tainted local helper \"raw\"", "uses raw triage directly"]
-
-  , testCase "tricu check rejects parametric definitions depending on unchecked imported facts" $ do
-      let imported = [ImportedView "Ext.raw" (VTFn [VTVar 0] (VTName "String")) ViewUnchecked]
-      output <- checkSourceWithEnvAndImportedViews allTestLibsEnv imported "bad x@_a =@String Ext.raw x\n"
-      output `containsAll` ["parametric View definition \"bad\"", "unchecked or unknown external name \"Ext.raw\""]
-
-  , testCase "tricu check accepts parametric code through value-level trusted stdlib facts" $ do
-      facts <- either assertFailure pure (valueViewFactsFromEnv allTestLibsEnv)
-      let source = "idP x@_a =@_a x\nmaybeOrV default@_a m@(Maybe _a) =@_a matchMaybe default idP m\n"
-      output <- checkSourceWithEnvAndImportedViews allTestLibsEnv facts source
-      output @?= "ok"
-
-  , testCase "unused value-level trusted facts do not perturb root selection" $ do
-      facts <- either assertFailure pure (valueViewFactsFromEnv allTestLibsEnv)
-      output <- checkSourceWithEnvAndImportedViews allTestLibsEnv facts "idP x@_a =@_a x\n"
-      output @?= "ok"
-
-  , testCase "value-level trusted stdlib facts lower with Trusted provenance" $ do
-      facts <- either assertFailure pure (valueViewFactsFromEnv allTestLibsEnv)
-      case lowerSourceWithImportedViews facts "notV x@Bool =@Bool matchBool false true x\n" of
-        Left err -> assertFailure err
-        Right lowered -> assertBool "expected trusted provenance in lowered view tree" $ "typedValueWithProvenance" `isInfixOf` lowered && "viewProvenanceTrusted" `isInfixOf` lowered
-
-  , testCase "tricu check uses annotated id const compose through re-export modules" $
-      withSystemTempDirectory "tricu-stdlib-prelude-views" $ \dir -> do
-        let store = StorePath (dir </> "store")
-            basePath = dir </> "mybase.tri"
-            preludePath = dir </> "myprelude.tri"
-            mainPath = dir </> "main.tri"
-        writeFile (dir </> "tricu.workspace") "module mybase = mybase.tri\nmodule myprelude = myprelude.tri\n"
-        writeFile basePath "id a@_a =@_a a\nconst a@_a b@_b =@_a a\ncompose f@(Fn [_b] _c) g@(Fn [_a] _b) x@_a =@_c f (g x)\n"
-        writeFile preludePath "!import \"mybase\" !Local\n"
-        writeFile mainPath "!import \"myprelude\" !Local\nmain =@String compose id (const \"hi\") 1\n"
-        output <- checkFileWithStore store mainPath
-        output @?= "ok"
-
-  , testCase "Workspace value-level viewFacts export and re-export Trusted provenance" $
-      withSystemTempDirectory "tricu-workspace-value-view-facts" $ \dir -> do
-        let store = StorePath (dir </> "store")
-            depPath = dir </> "dep.tri"
-            shimPath = dir </> "shim.tri"
-            mainPath = dir </> "main.tri"
-            factBlock = unlines
-              [ "factsPair = t"
-              , "factsFact name provenance view = factsPair name (factsPair provenance view)"
-              , "factsTrusted = 1"
-              , "factsField tag value = factsPair tag value"
-              , "factsRecord tag fields = factsPair tag fields"
-              , "factsVar id = factsRecord 8 [(factsField 10 id)]"
-              , "factsForall binders body = factsRecord 9 [(factsField 11 binders) (factsField 12 body)]"
-              , "factsFn args result = factsRecord 1 [(factsField 0 args) (factsField 1 result)]"
-              , "viewFacts = [(factsFact \"rawId\" factsTrusted (factsForall [0] (factsFn [(factsVar 0)] (factsVar 0))))]"
-              ]
-            expected = VTForall [0] (VTFn [VTVar 0] (VTVar 0))
-        writeFile (dir </> "tricu.workspace") "module dep = dep.tri\nmodule shim = shim.tri\n"
-        writeFile depPath ("rawId x = x\n" ++ factBlock)
-        writeFile shimPath "!import \"dep\" !Local\n"
-        writeFile mainPath "!import \"shim\" Shim\nmain x@_a =@_a Shim.rawId x\n"
-        output <- checkFileWithStore store mainPath
-        output @?= "ok"
-        forM_ [("dep", "rawId"), ("shim", "rawId")] $ \(moduleName, exportName) -> do
-          mAlias <- readAlias store ModuleAlias (pack moduleName)
-          case mAlias of
-            Nothing -> assertFailure ("expected " ++ moduleName ++ " module alias")
-            Just ref -> do
-              mManifest <- getManifest store (objectRefHash ref)
-              case mManifest of
-                Nothing -> assertFailure ("expected " ++ moduleName ++ " module manifest")
-                Just manifest -> do
-                  assertBool ("viewFacts should not be exported from " ++ moduleName) $
-                    all ((/= "viewFacts") . unpack . moduleExportName) (moduleManifestExports manifest)
-                  case find ((== exportName) . unpack . moduleExportName) (moduleManifestExports manifest) of
-                    Nothing -> assertFailure ("expected " ++ exportName ++ " export from " ++ moduleName)
-                    Just ex -> do
-                      moduleExportViewProvenance ex @?= Just ViewTrusted
-                      case moduleExportView ex of
-                        Nothing -> assertFailure "expected trusted value-level view ref"
-                        Just viewRef -> do
-                          view <- getViewType store viewRef
-                          view @?= Right expected
-
-  , testCase "value-level viewFacts decoder reports malformed fact context" $ do
-      let env = evalTricu Map.empty (parseTricu "viewFacts = [(t \"bad\" (t 9 t))]\n")
-      case valueViewFactsFromEnv env of
-        Right _ -> assertFailure "expected malformed provenance error"
-        Left err -> err `containsAll` ["viewFacts[0]", "bad", "invalid provenance", "unknown provenance tag 9"]
-
-  , testCase "value-level viewFacts decoder reports malformed View context" $ do
-      let env = evalTricu Map.empty (parseTricu "viewFacts = [(t \"bad\" (t 1 (t 9 [])))]\n")
-      case valueViewFactsFromEnv env of
-        Right _ -> assertFailure "expected malformed View error"
-        Left err -> err `containsAll` ["viewFacts[0]", "bad", "malformed View"]
-
-  , testCase "value-level viewFacts decoder rejects duplicate fact names" $ do
-      let env = evalTricu Map.empty (parseTricu "v = t 9 [(t 11 []) (t 12 (t 0 []))]\nviewFacts = [(t \"dup\" (t 1 v)) (t \"dup\" (t 1 v))]\n")
-      case valueViewFactsFromEnv env of
-        Right _ -> assertFailure "expected duplicate viewFacts error"
-        Left err -> err `containsAll` ["duplicate viewFacts entry", "dup"]
-
-  , testCase "Workspace modules reject viewFacts for non-exported names" $
-      withSystemTempDirectory "tricu-workspace-view-facts-nonexport" $ \dir -> do
-        let store = StorePath (dir </> "store")
-            depPath = dir </> "dep.tri"
-            mainPath = dir </> "main.tri"
-        writeFile (dir </> "tricu.workspace") "module dep = dep.tri\n"
-        writeFile depPath "rawId x = x\nv = t 9 [(t 11 []) (t 12 (t 0 []))]\nviewFacts = [(t \"missing\" (t 1 v))]\n"
-        writeFile mainPath "!import \"dep\" Dep\nmain = Dep.rawId t\n"
-        outcome <- try (evaluateFileWithStore (Just store) mainPath) :: IO (Either SomeException Env)
-        case outcome of
-          Right _ -> assertFailure "expected non-exported viewFacts rejection"
-          Left err -> show err `containsAll` ["viewFacts for non-exported name", "missing"]
-
-  , testCase "stdlib list value-level facts publish Trusted contracts" $
-      withSystemTempDirectory "tricu-stdlib-list-view-facts" $ \dir -> do
-        let store = StorePath (dir </> "store")
-            basePath = dir </> "base.tri"
-            listPath = dir </> "list.tri"
-            mainPath = dir </> "main.tri"
-        baseSource <- readFile "./lib/base.tri"
-        listSource <- readFile "./lib/list.tri"
-        writeFile (dir </> "tricu.workspace") "module base = base.tri\nmodule list = list.tri\n"
-        writeFile basePath baseSource
-        writeFile listPath listSource
-        writeFile mainPath "!import \"list\" L\ninc x@Byte =@Byte x\nmain xs@(List Byte) =@(List Byte) L.map inc xs\n"
-        output <- checkFileWithStore store mainPath
-        output @?= "ok"
-        mAlias <- readAlias store ModuleAlias (pack "list")
-        case mAlias of
-          Nothing -> assertFailure "expected list module alias"
-          Just ref -> do
-            mManifest <- getManifest store (objectRefHash ref)
-            case mManifest of
-              Nothing -> assertFailure "expected list module manifest"
-              Just manifest -> do
-                let trustedNames =
-                      [ "emptyList?", "tail", "append", "lExist?", "map", "filter"
-                      , "foldl", "foldr", "length", "reverse", "snoc", "count"
-                      , "all?", "any?", "intersect", "headMaybe", "lastMaybe"
-                      , "nthMaybe", "take", "drop", "splitAt", "concatMap", "find"
-                      , "partition", "strLength", "strAppend", "strEq?", "strEmpty?"
-                      , "startsWith?", "endsWith?", "contains?", "lines", "unlines"
-                      , "words", "unwords", "zipWith"
-                      ]
-                forM_ trustedNames $ \exportName ->
-                  case find ((== exportName) . unpack . moduleExportName) (moduleManifestExports manifest) of
-                    Nothing -> assertFailure ("expected " ++ exportName ++ " export")
-                    Just ex -> moduleExportViewProvenance ex @?= Just ViewTrusted
-
-  , testCase "Workspace re-export-only modules preserve imported View Contracts" $
-      withSystemTempDirectory "tricu-workspace-reexport-views" $ \dir -> do
-        let store = StorePath (dir </> "store")
-            depPath = dir </> "dep.tri"
-            shimPath = dir </> "shim.tri"
-            mainPath = dir </> "main.tri"
-        writeFile (dir </> "tricu.workspace") "module dep = dep.tri\nmodule shim = shim.tri\n"
-        writeFile depPath "idP x@_a =@_a x\n"
-        writeFile shimPath "!import \"dep\" !Local\n"
-        writeFile mainPath "!import \"shim\" Shim\nmain =@String Shim.idP \"hi\"\n"
-        output <- checkFileWithStore store mainPath
-        output @?= "ok"
-        mAlias <- readAlias store ModuleAlias "shim"
-        case mAlias of
-          Nothing -> assertFailure "expected shim module alias"
-          Just ref -> do
-            mManifest <- getManifest store (objectRefHash ref)
-            case mManifest of
-              Nothing -> assertFailure "expected shim module manifest"
-              Just manifest -> case find ((== "idP") . unpack . moduleExportName) (moduleManifestExports manifest) of
-                Nothing -> assertFailure "expected idP re-export"
-                Just ex -> do
-                  moduleExportViewProvenance ex @?= Just ViewChecked
-                  case moduleExportView ex of
-                    Nothing -> assertFailure "expected idP re-export view ref"
-                    Just viewRef -> do
-                      view <- getViewType store viewRef
-                      view @?= Right (VTForall [0] (VTFn [VTVar 0] (VTVar 0)))
-
-  , testCase "tricu check rejects inconsistent first-order polymorphic View bindings" $ do
-      output <- checkSourceWithEnv allTestLibsEnv "same x@_a y@_a =@_a x\nmain =@String same \"hi\" 1\n"
-      output @?= "symbol 6 (byte literal) expected String but got Byte"
 
   , testCase "tricu check catches undersaturated annotated function calls via residual Fn view" $ do
       output <- checkSourceWithEnv allTestLibsEnv "f x@String y@String =@String x\nmain =@String f \"a\"\n"

tricu.workspace

@@ -3,7 +3,6 @@ module base = lib/base.tri
 module list = lib/list.tri
 module bytes = lib/bytes.tri
 module conversions = lib/conversions.tri
-module lazy = lib/lazy.tri
 module prelude = lib/prelude.tri
 module binary = lib/binary.tri
 module patterns = lib/patterns.tri