tricu

binding-substitution.tri (4841B)

---

 -- Isolated resolved-core substitution and Boolean-binding rewrite prototype.
 -- Trusted well-formed core only. Not wired into the accepted compiler.
 !import analysis as A
 !import native_math as N
 !import kernels as K
 !export *
 head = K.head
 tail = K.tail
 kind = A.kind
 payload = A.payload
 lazy = K.lazy
 choose = K.choose
 rebuild original value = t (kind original) (t value (tail (tail original)))
 withSpan original value = t (kind value) (t (payload value) (tail (tail original)))
 -- Positive de Bruijn shift. Local variables below cutoff are unchanged.
 shift amount cutoff node = lazy (_ : node)
   (_ : case kind node of
     2 = lazy (_ : rebuild node (N.add amount (payload node))) (_ : node) (N.gte (payload node) cutoff)
     3 = let ab = payload node in rebuild node
       (t (shift amount cutoff (head ab)) (shift amount cutoff (tail ab)))
     4 = rebuild node (shift amount (N.successor cutoff) (payload node))
     8 = rebuild node (K.map (child : shift amount cutoff child) (payload node))
     _ = node) (N.zero amount)
 -- Remove one surrounding binder. RHS is in the outer scope, not that binder's.
 substitute rhs depth node = case kind node of
   2 = lazy (_ : shift depth 0 rhs)
     (_ : lazy (_ : rebuild node (N.predecessor (payload node))) (_ : node)
       (N.gt (payload node) depth)) (N.equal (payload node) depth)
   3 = let ab = payload node in rebuild node
     (t (substitute rhs depth (head ab)) (substitute rhs depth (tail ab)))
   4 = rebuild node (substitute rhs (N.successor depth) (payload node))
   8 = rebuild node (K.map (child : substitute rhs depth child) (payload node))
   _ = node
 containsLambda node = case kind node of
   4 = t t
   3 = let ab = payload node in K.either (containsLambda (head ab)) (containsLambda (tail ab))
   8 = (let rec walk xs = K.triage t (_ : t t)
         (a b : K.either (containsLambda a) (walk b)) xs in walk (payload node))
   _ = t
 boolTree value = K.triage (t t) (child : N.zero child) (_ _ : t) value
 leafLiteral node = lazy (_ : t t)
   (_ : lazy (_ : N.zero (payload node)) (_ : t) (N.equal (kind node) 5)) (N.equal (kind node) 1)
 -- Literal Boolean trees, including the core constructor spelling `t t`.
 boolLiteral node = case kind node of
   1 = t t
   5 = boolTree (payload node)
   6 = boolTree (payload node)
   3 = let ab = payload node in K.both (leafLiteral (head ab)) (leafLiteral (tail ab))
   _ = t
 -- The literal identity is matched only when saturated with one argument.
 -- The harness authenticates the certificate's Boolean-result contract.
 booleanRhs negation node = lazy (_ : t t)
   (_ : lazy
     (_ : let ab = payload node in let fun = head ab in let arg = tail ab in
       K.both (K.either (N.equal (kind arg) 2) (boolLiteral arg))
         (K.both (N.equal (kind fun) 5) (A.equal (payload fun) negation)))
     (_ : t) (N.equal (kind node) 3)) (boolLiteral node)
 -- Input node must be Apply (Lambda body) rhs. The screening certificate is
 -- still experimental, not a general proof for arbitrary reflective contexts.
 -- 0..6: analysis decisions; 7: uncertified RHS; 8: any nested body lambda;
 -- 9: not an immediate binding. Only decision 1 performs substitution.
 rewrite selector negation node = lazy
   (_ : let ab = payload node in let fun = head ab in
     lazy
       (_ : let body = payload fun in let rhs = tail ab in
         let decision = A.classify (A.analyze selector body) in
         lazy
           (_ : lazy (_ : t 7 node)
             (_ : lazy (_ : t 8 node)
               (_ : t 1 (withSpan node (substitute rhs 0 body))) (containsLambda body))
             (K.not (booleanRhs negation rhs)))
           (_ : t decision node) (N.equal decision 1))
       (_ : t 9 node) (N.equal (kind fun) 4))
   (_ : t 9 node) (N.equal (kind node) 3)
 -- Batch transport helpers for independent host oracles.
 shiftBatch inputs = K.map (x : let rest = tail x in shift (head x) (head rest) (tail rest)) inputs
 substituteBatch inputs = K.map (x : substitute (head x) 0 (tail x)) inputs
 rewriteBatch certificates nodes = K.map (node : rewrite (head certificates) (tail certificates) node) nodes
 -- Conservative whole-core traversal: an immediate binding is a decision unit.
 -- Rejected bindings are returned exactly, without rewriting their descendants.
 -- Accepted bindings are substituted once; no fixed-point rewrite loop.
 transform selector negation node = case kind node of
   3 = let ab = payload node in
     lazy (_ : tail (rewrite selector negation node))
       (_ : rebuild node (t (transform selector negation (head ab))
         (transform selector negation (tail ab)))) (N.equal (kind (head ab)) 4)
   4 = rebuild node (transform selector negation (payload node))
   8 = rebuild node (K.map (child : transform selector negation child) (payload node))
   _ = node
 transformBatch certificates nodes = K.map (node : transform (head certificates) (tail certificates) node) nodes