tricu

A lazy functional language based on Tree Calculus
Log | Files | Refs | README | LICENSE

binding-analysis.tri (4064B)

      1 -- Analysis-only prototype over trusted resolved-core nodes. NOT a rewrite pass.
      2 -- Input: (certified selector tree, core body under the proposed binding).
      3 -- Selector certificate means exactly three arguments, first two exclusive,
      4 -- third selector evaluated once. Caller authenticates that contract.
      5 !import native_math as N
      6 !import kernels as K
      7 !export *
      8 triage = K.triage
      9 head = K.head
     10 tail = K.tail
     11 choose = K.choose
     12 lazy = K.lazy
     13 or = K.either
     14 kind node = head node
     15 payload node = head (tail node)
     16 -- (syntactic uses, (max path uses, (under lambda, (unknown consumer,
     17 --   (partial selector, malformed))))). Booleans are canonical.
     18 summary uses paths escape unknown partial bad = t uses (t paths (t escape (t unknown (t partial bad))))
     19 empty = summary 0 0 t t t t
     20 one = summary 1 1 t t t t
     21 uses x = head x
     22 paths x = head (tail x)
     23 escape x = head (tail (tail x))
     24 unknown x = head (tail (tail (tail x)))
     25 partial x = head (tail (tail (tail (tail x))))
     26 bad x = tail (tail (tail (tail (tail x))))
     27 merge a b = summary (N.add (uses a) (uses b)) (N.add (paths a) (paths b))
     28   (or (escape a) (escape b)) (or (unknown a) (unknown b))
     29   (or (partial a) (partial b)) (or (bad a) (bad b))
     30 flagUnknown x isPartial = summary (uses x) (paths x) (escape x)
     31   (or (unknown x) (N.gt (uses x) 0))
     32   (or (partial x) (K.both isPartial (N.gt (uses x) 0))) (bad x)
     33 flagEscape x = summary (uses x) (paths x) (or (escape x) (N.gt (uses x) 0))
     34   (unknown x) (partial x) (bad x)
     35 choice a b c = let flags = merge (merge a b) c in
     36   summary (uses flags) (N.add (N.maximum (paths a) (paths b)) (paths c))
     37     (escape flags) (unknown flags) (partial flags) (bad flags)
     38 -- Pure tree equality, only on finite authenticated literal trees.
     39 equal a b = triage (triage (t t) (_ : t) (_ _ : t) b)
     40   (x : triage t (y : equal x y) (_ _ : t) b)
     41   (x y : triage t (_ : t) (u v : K.both (equal x u) (equal y v)) b) a
     42 -- Peel a left-associated application into (head, argument list).
     43 peel node args = lazy
     44   (_ : let ab = payload node in peel (head ab) (t (tail ab) args))
     45   (_ : t node args) (N.equal (kind node) 3)
     46 walkArgs visit depth xs = triage empty (_ : summary 0 0 t t t (t t))
     47   (a b : merge (visit depth a) (walkArgs visit depth b)) xs
     48 isSelector selector node = lazy (_ : equal selector (payload node)) (_ : t) (N.equal (kind node) 5)
     49 -- Only explicit Leaf or literal Leaf/Stem heads with exact constructor arity.
     50 constructorSlots node = lazy (_ : 2)
     51   (_ : lazy (_ : triage 2 (_ : 1) (_ _ : 0) (payload node)) (_ : 0) (N.equal (kind node) 5))
     52   (N.equal (kind node) 1)
     53 application visit selector depth node = let spine = peel node t in
     54   let fun = head spine in let args = tail spine in let arity = K.width args in
     55   let all = merge (visit depth fun) (walkArgs visit depth args) in
     56   lazy
     57     (_ : lazy
     58       (_ : choice (visit depth (head args)) (visit depth (head (tail args)))
     59         (visit depth (head (tail (tail args)))))
     60       (_ : flagUnknown all (N.lt arity 3)) (N.equal arity 3))
     61     (_ : lazy (_ : all) (_ : flagUnknown all t)
     62       (K.both (N.gt (constructorSlots fun) 0) (N.lte arity (constructorSlots fun))))
     63     (isSelector selector fun)
     64 analyze selector body = let rec
     65   visit depth node = case kind node of
     66     1 = empty
     67     2 = choose one empty (N.equal (payload node) depth)
     68     3 = application visit selector depth node
     69     4 = flagEscape (visit (N.successor depth) (payload node))
     70     5 = empty
     71     6 = empty
     72     7 = empty
     73     8 = walkArgs visit depth (payload node)
     74     _ = summary 0 0 t t t (t t)
     75   in visit 0 body
     76 -- Diagnostic categories, not a proof that all structural observations agree:
     77 -- 0 unused (leave alone), 1 candidate, 2 multiple uses on a path,
     78 -- 3 crosses lambda, 4 unknown consumer, 5 partial selector, 6 malformed kind.
     79 classify x = choose 6 (choose 3 (choose 5 (choose 4
     80   (choose 0 (choose 2 1 (N.gt (paths x) 1)) (N.zero (uses x)))
     81   (unknown x)) (partial x)) (escape x)) (bad x)
     82 inspect input = let result = analyze (head input) (tail input) in t (classify result) result
     83 batch selector bodies = K.map (body : inspect (t selector body)) bodies