tricu

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

binding_analysis.tri (4161B)

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