tricu

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

program.tri (9886B)

      1 !import prelude *
      2 !import parser *
      3 !import source_parser *
      4 !import source_lexer *
      5 !import source_ast *
      6 !import source_equations *
      7 !export *
      8 
      9 -- Program = pair definitions (Maybe finalExpression).
     10 -- Definition = pair locatedNameToken body. Contiguous plain equations
     11 -- coalesce into one located equation body; unique all-name singleton heads
     12 -- take the ordinary lambda path. Program parsing is distinct from the
     13 -- single-expression gate.
     14 sourceProgramDefinitions program = fst program
     15 sourceProgramFinal program = snd program
     16 sourceDefinitionName definition = sourceTokenPayload (fst definition)
     17 sourceDefinitionPosition definition = sourceTokenStart (fst definition)
     18 sourceDefinitionBody definition = snd definition
     19 
     20 sourceProgramSkipNewlines =
     21   parserMap (_ : t) (parserMany (sourceGateExpect sourceTokenNewline))
     22 
     23 -- Both definition and local-binding bodies use the same located transition:
     24 -- unindented lines are top-level; indented values may continue on lines whose
     25 -- first token starts in a strictly deeper column.
     26 sourceProgramDefinitionValue =
     27   sourceGateParseLayoutValue sourceGateExpr sourceGateExprIndented
     28     "definition body"
     29 
     30 -- Look ahead across the head (including delimited pattern newlines). This
     31 -- distinguishes `f t` (expression) from `f x = x` (definition), without
     32 -- consuming tokens or trying a partially consumed alternative.
     33 sourceProgramAssignOnLine? tokens = sourceEquationAssignLine? tokens
     34 
     35 sourceProgramDefinitionHead? tokens =
     36   lazyList
     37     (_ : false)
     38     (token rest :
     39       lazyBool
     40         (_ : sourceProgramAssignOnLine? rest)
     41         (_ : false)
     42         (equal? (sourceTokenKind token) sourceTokenName))
     43     tokens
     44 
     45 -- Bootstrap contract profile: definition heads only. Contract expressions
     46 -- are ordinary names or parenthesized applications, never static types.
     47 -- Keep the runtime Result checks (including short-circuit and value passing)
     48 -- identical to Frontend.ContractDesugar's supported base-library forms.
     49 sourceProgramContract =
     50   parserOr (sourceGateParseGroup sourceGateExpr)
     51     (parserMap sourceAstName (sourceGateExpect sourceTokenName))
     52 
     53 -- Argument = pair (Maybe namedBinderToken) (Maybe contractExpression).
     54 sourceProgramArgNamed input =
     55   parserBind (sourceGateExpect sourceTokenName) (name :
     56     parserMap (contract : pair (just name) contract)
     57       (parserOptional (parserThen (sourceGateExpect sourceTokenAt)
     58         sourceProgramContract))) input
     59 
     60 sourceProgramArgPhantom =
     61   parserMap (contract : pair nothing (just contract))
     62     (parserThen (sourceGateExpect sourceTokenAt) sourceProgramContract)
     63 
     64 sourceProgramArgument = parserOr sourceProgramArgPhantom sourceProgramArgNamed
     65 
     66 sourceProgramSynthetic name node =
     67   sourceToken sourceTokenName name
     68     (sourceAstStart node) (sourceAstStart node)
     69 
     70 sourceProgramName name node = sourceAstName (sourceProgramSynthetic name node)
     71 sourceProgramApply2 function first second =
     72   sourceAstApply (sourceAstApply function first) second
     73 sourceProgramApply3 function first second third =
     74   sourceAstApply (sourceProgramApply2 function first second) third
     75 
     76 sourceProgramChecked contract value =
     77   sourceProgramApply2 (sourceProgramName "withContract" contract) contract value
     78 
     79 sourceProgramFailure msg =
     80   sourceProgramApply2
     81     (sourceProgramName "err" msg) msg
     82     (sourceAstLeaf (sourceProgramSynthetic "t" msg))
     83 
     84 sourceProgramOnFailure node =
     85   sourceAstLambda
     86     (sourceProgramSynthetic "msg" node)
     87     (sourceAstLambda (sourceProgramSynthetic "_" node)
     88       (sourceProgramFailure (sourceProgramName "msg" node)))
     89 
     90 -- Earlier failed arguments must still accept the remaining arguments before
     91 -- producing the error, just like the historical Haskell lowering.
     92 sourceProgramAbsorbFailure node =
     93   sourceAstLambda
     94     (sourceProgramSynthetic "msg" node)
     95     (sourceAstLambda (sourceProgramSynthetic "_" node)
     96       (sourceAstLambda (sourceProgramSynthetic "_" node)
     97         (sourceProgramFailure (sourceProgramName "msg" node))))
     98 
     99 sourceProgramReturn contract body =
    100   lazyMaybe
    101     (_ : body)
    102     (c : sourceProgramApply3
    103       (sourceProgramName "matchResult" c)
    104       (sourceProgramOnFailure c)
    105       (sourceAstLambda (sourceProgramSynthetic "r" c)
    106         (sourceAstLambda (sourceProgramSynthetic "_" c)
    107           (sourceProgramName "r" c)))
    108       (sourceProgramChecked c body))
    109     contract
    110 
    111 sourceProgramArgName arg index anchor =
    112   lazyMaybe
    113     (_ : sourceProgramSynthetic
    114       (if (isZero_? index) "x" (if (equal? index 1) "y" "z")) anchor)
    115     (token : token)
    116     (fst arg)
    117 
    118 sourceProgramRawApply args raw = (let rec
    119   walk args raw index =
    120     lazyList
    121       (_ : raw)
    122       (arg rest : walk rest
    123         (sourceAstApply raw
    124           (sourceAstName (sourceProgramArgName arg index raw)))
    125         (succ index))
    126       args
    127   in walk args raw 0)
    128 
    129 sourceProgramWrapArgs args body = (let rec
    130   walk args index =
    131     lazyList
    132       (_ : body)
    133       (arg rest :
    134         sourceAstLambda (sourceProgramArgName arg index body)
    135           (lazyMaybe
    136             (_ : walk rest (succ index))
    137             (c : sourceProgramApply3
    138               (sourceProgramName "matchResult" c)
    139               (lazyList
    140                 (_ : sourceProgramOnFailure c)
    141                 (other tail : sourceProgramAbsorbFailure c)
    142                 rest)
    143               (sourceAstLambda (sourceProgramArgName arg index body)
    144                 (sourceAstLambda (sourceProgramSynthetic "_" c)
    145                   (walk rest (succ index))))
    146               (sourceProgramChecked c
    147                 (sourceAstName (sourceProgramArgName arg index body))))
    148             (snd arg)))
    149       args
    150   in walk args 0)
    151 
    152 sourceProgramAnyContract? args =
    153   lazyList
    154     (_ : false)
    155     (arg rest : lazyMaybe
    156       (_ : sourceProgramAnyContract? rest)
    157       (contract : true)
    158       (snd arg))
    159     args
    160 
    161 sourceProgramAnyPhantom? args =
    162   lazyList
    163     (_ : false)
    164     (arg rest : lazyMaybe
    165       (_ : true)
    166       (name : sourceProgramAnyPhantom? rest)
    167       (fst arg))
    168     args
    169 
    170 sourceProgramAllPhantom? args =
    171   lazyList
    172     (_ : true)
    173     (arg rest : lazyMaybe
    174       (_ : sourceProgramAllPhantom? rest)
    175       (name : false)
    176       (fst arg))
    177     args
    178 
    179 sourceProgramPlainArgs args body =
    180   lazyList
    181     (_ : body)
    182     (arg rest : sourceAstLambda (sourceProgramArgName arg 0 body)
    183       (sourceProgramPlainArgs rest body))
    184     args
    185 
    186 sourceProgramLowerDefinition name args result body =
    187   lazyBool
    188     (_ : lazyBool
    189       (_ : sourceAstLocal
    190         (sourceToken sourceTokenName
    191           (append "_" (append (sourceTokenPayload name) "_raw"))
    192           (sourceTokenStart name) (sourceTokenEnd name))
    193         body
    194         (sourceProgramWrapArgs args
    195           (sourceProgramReturn result
    196             (sourceProgramRawApply args
    197               (sourceProgramName
    198                 (append "_" (append (sourceTokenPayload name) "_raw"))
    199                 body))))
    200         (sourceTokenStart name) (sourceAstEnd body))
    201       (_ : sourceProgramWrapArgs args (sourceProgramReturn result body))
    202       (sourceProgramAnyPhantom? args))
    203     (_ : sourceProgramPlainArgs args body)
    204     (or? (sourceProgramAnyContract? args)
    205       (lazyMaybe (_ : false) (contract : true) result))
    206 
    207 sourceProgramParseAnnotatedBinding input =
    208   parserBind (sourceGateExpect sourceTokenName) (name :
    209     parserBind (parserMany sourceProgramArgument) (args :
    210       (remaining : lazyBool
    211         (_ : parserThen (sourceGateExpect sourceTokenAssign)
    212           (parserBind (parserOptional
    213             (parserThen (sourceGateExpect sourceTokenAt)
    214               sourceProgramContract)) (result :
    215             parserMap (body : pair name
    216               (sourceProgramLowerDefinition name args result body))
    217               sourceProgramDefinitionValue)) remaining)
    218         (_ : parserReplyFail
    219           (parserDiagnostic 47 "supported contract head" t
    220             (sourceTokenStart name) t) remaining true false)
    221         (or? (not? (sourceProgramAnyPhantom? args))
    222           (and? (sourceProgramAllPhantom? args)
    223             (lte_? (length args) 2)))))) input
    224 
    225 -- Preserve the existing bounded annotated-head path. Plain heads now retain
    226 -- located equations; annotated definitions cannot merge with those groups.
    227 sourceProgramAnnotated? input = (lazyList (_ : false)
    228   (token rest : let kind = sourceTokenKind token in (lazyBool (_ : true)
    229     (_ : lazyBool (_ : lazyList (_ : false)
    230         (next unused : equal? (sourceTokenKind next) sourceTokenAt) rest)
    231       (_ : lazyBool (_ : false) (_ : sourceProgramAnnotated? rest)
    232         (equal? kind sourceTokenNewline))
    233       (equal? kind sourceTokenAssign)) (equal? kind sourceTokenAt))) input)
    234 sourceProgramParsePlainBinding input = (lazyList
    235   (_ : sourceGateAtomError input)
    236   (token rest : sourceEquationBinding
    237     (sourceGateParseLayoutValue
    238       (sourceGateExprIndented (sourcePositionColumn (sourceTokenStart token)))
    239       sourceGateExprIndented "definition body") input) input)
    240 sourceProgramParseDefinition input =
    241   lazyBool
    242     (_ : lazyBool (_ : sourceProgramParseAnnotatedBinding input)
    243       (_ : sourceProgramParsePlainBinding input) (sourceProgramAnnotated? input))
    244     (_ : parserReplyFail
    245       (parserDiagnostic 2 sourceTokenAssign t t t) input false false)
    246     (sourceProgramDefinitionHead? input)
    247 
    248 sourceProgramParseTokens =
    249   parserThen sourceProgramSkipNewlines
    250     (parserBind
    251       (parserMany
    252         (parserBefore sourceProgramParseDefinition sourceProgramSkipNewlines))
    253       (definitions : parserBind
    254         (input : lazyResult
    255           (diagnostic rest : parserReplyFail diagnostic input false false)
    256           (groups unused : parserReplyOk groups input false false)
    257           (sourceEquationGroups definitions))
    258         (groups : parserBind
    259           (parserOptional
    260             (parserBefore sourceGateExpr sourceProgramSkipNewlines))
    261           (final : parserMap (_ : pair groups final) sourceGateEof))))
    262 
    263 parseGateProgram = parserWithLexer lexGateSource sourceProgramParseTokens
    264