tricu

An interpreted language for exploring Tree Calculus
Log | Files | Refs | README | LICENSE

validate.tri (6249B)

      1 !import prelude *
      2 !export *
      3 -- Authored SCP boundary. The independent reference interpreter intentionally
      4 -- does not call this validator. Literal payloads (including initial state) are
      5 -- opaque: preparation/linking, not IR traversal, checks executable values.
      6 
      7 -- Diagnostic = (category, (zero-based rule index, (reversed path, detail))).
      8 -- Category is "malformed"; backend capability is checked separately.
      9 vDiagnostic category rule path detail = pair category (pair rule (pair path detail))
     10 vFail rule path detail = err (vDiagnostic "malformed" rule path detail) t
     11 vAt part path = pair part path
     12 vPair? value = triage false (_ : false) (_ _ : true) value
     13 vSlot_ self slots slot =
     14   (lazyList
     15     (_ : false)
     16     (head rest : lazyBool (_ : true) (_ : self rest slot)
     17       (equal? head slot)) slots)
     18 vSlot? slots slot = y vSlot_ slots slot
     19 vBind slot slots rule path =
     20   (lazyBool
     21   (_ : vFail rule path "duplicate binding")
     22   (_ : ok (pair slot slots) t) (vSlot? slots slot))
     23 
     24 -- Return the bound slots, in the reference matcher's introduction order.
     25 vPattern_ self pattern slots rule path =
     26   (lazyBool
     27   (_ : matchPair (tag payload : lazyBool (_ : ok slots t)
     28     (_ : lazyBool (_ : ok slots t)
     29     (_ : lazyBool (_ : self payload slots rule (vAt "stem" path))
     30     (_ : lazyBool
     31     (_ : lazyBool (_ : matchPair (left right : bindResult (self left slots rule (vAt "left" path)) (bound _ : self right bound rule (vAt "right" path))) payload) (_ : vFail rule path "fork payload") (vPair? payload))
     32     (_ : lazyBool (_ : vBind payload slots rule path)
     33     (_ : lazyBool (_ : ok slots t)
     34     (_ : lazyBool
     35     (_ : lazyBool (_ : matchPair (slot child : bindResult (vBind slot slots rule path) (bound _ : self child bound rule (vAt "as" path))) payload) (_ : vFail rule path "as payload") (vPair? payload))
     36     (_ : vFail rule path "unknown pattern tag")
     37     (equal? tag 6))
     38     (equal? tag 5))
     39     (equal? tag 4))
     40     (equal? tag 3))
     41     (equal? tag 2))
     42     (equal? tag 1))
     43     (equal? tag 0)) pattern)
     44   (_ : vFail rule path "pattern node") (vPair? pattern))
     45 vPattern pattern slots rule path = y vPattern_ pattern slots rule path
     46 
     47 vTwo self payload slots rule path =
     48   (lazyBool
     49   (_ : matchPair (left right : bindResult
     50     (self left slots rule (vAt "left" path))
     51     (_ _ : self right slots rule (vAt "right" path))) payload)
     52   (_ : vFail rule path "pair payload") (vPair? payload))
     53 vThree self payload slots rule path =
     54   (lazyBool
     55   (_ : matchPair (first rest : lazyBool
     56     (_ : matchPair (second third : bindResult
     57       (self first slots rule (vAt "target" path))
     58       (_ _ : bindResult (self second slots rule (vAt "input" path))
     59         (_ _ : self third slots rule (vAt "state" path)))) rest)
     60     (_ : vFail rule path "three-part payload") (vPair? rest)) payload)
     61   (_ : vFail rule path "three-part payload") (vPair? payload))
     62 vCall self payload slots rule path =
     63   (lazyBool
     64   (_ : matchPair (worker more : lazyBool
     65     (_ : matchPair (argument continuation : lazyBool
     66       (_ : matchPair (slot receiver : bindResult
     67         (self worker slots rule (vAt "target" path))
     68         (_ _ : bindResult
     69           (self argument slots rule (vAt "input" path))
     70           (_ _ : bindResult (vBind slot slots rule (vAt "receiver" path))
     71             (receiverSlots _ : self receiver receiverSlots rule
     72               (vAt "receiver" path))))) continuation)
     73       (_ : vFail rule path "call receiver payload") (vPair? continuation)) more)
     74     (_ : vFail rule path "call argument payload") (vPair? more)) payload)
     75   (_ : vFail rule path "call payload") (vPair? payload))
     76 vMatchArms_ self arms slots rule path output = (triage
     77   (ok t t)
     78   (_ : vFail rule path "match arm list")
     79   (arm rest : lazyBool
     80     (_ : matchPair (pattern body : bindResult
     81       (vPattern pattern slots rule (vAt "pattern" path)) (bound _ :
     82         bindResult (output body bound rule (vAt "arm" path)) (_ _ :
     83           self rest slots rule path output))) arm)
     84     (_ : vFail rule path "match arm") (vPair? arm)) arms)
     85 vMatchArms arms slots rule path output = y vMatchArms_ arms slots rule path output
     86 vMatch self payload slots rule path = (lazyBool
     87   (_ : matchPair (source arms : bindResult
     88     (self source slots rule (vAt "scrutinee" path)) (_ _ :
     89       triage (vFail rule path "empty match")
     90         (_ : vFail rule path "match arm list")
     91         (_ _ : vMatchArms arms slots rule path self) arms)) payload)
     92   (_ : vFail rule path "match payload") (vPair? payload))
     93 vOutput_ self output slots rule path =
     94   (lazyBool
     95   (_ : matchPair (tag payload : lazyBool (_ : ok t t)
     96     (_ : lazyBool
     97     (_ : lazyBool (_ : ok t t)
     98     (_ : vFail rule path "unknown capture") (vSlot? slots payload))
     99     (_ : lazyBool (_ : vTwo self payload slots rule path)
    100     (_ : lazyBool (_ : vTwo self payload slots rule path)
    101     (_ : lazyBool (_ : vCall self payload slots rule path)
    102     (_ : lazyBool (_ : self payload slots rule (vAt "stem" path))
    103     (_ : lazyBool (_ : vThree self payload slots rule path)
    104     (_ : lazyBool (_ : vTwo self payload slots rule path)
    105     (_ : lazyBool (_ : vMatch self payload slots rule path)
    106     (_ : vFail rule path "unknown output tag")
    107     (equal? tag 9))
    108     (equal? tag 8))
    109     (equal? tag 6))
    110     (equal? tag 5))
    111     (equal? tag 4))
    112     (equal? tag 3))
    113     (equal? tag 2))
    114     (equal? tag 1))
    115     (equal? tag 0)) output)
    116   (_ : vFail rule path "output node") (vPair? output))
    117 vOutput output slots rule path = y vOutput_ output slots rule path
    118 
    119 vRule rule index =
    120   (lazyBool
    121   (_ : matchPair (input more : lazyBool
    122     (_ : matchPair (state output : bindResult
    123       (vPattern input t index ["input pattern"])
    124       (inputSlots _ : bindResult
    125         (vPattern state inputSlots index ["state pattern"])
    126         (allSlots _ : vOutput output allSlots index ["output"]))) more)
    127     (_ : vFail index t "rule payload") (vPair? more)) rule)
    128   (_ : vFail index t "rule node") (vPair? rule))
    129 vRules_ self rules index =
    130   (triage
    131     (ok t t)
    132     (_ : vFail index t "rule list")
    133     (rule rest : bindResult (vRule rule index)
    134       (_ _ : self rest (succ index))) rules)
    135 vRules rules = y vRules_ rules 0
    136 vValidate consumer =
    137   (lazyBool
    138   (_ : bindResult (vRules (snd consumer)) (_ _ : ok consumer t))
    139   (_ : vFail 0 t "consumer node") (vPair? consumer))