tricu

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

dfe628dcc1be66b2ea645295398d0d4c0357ad3312da2578298cb3c5fc30fd7d.tri (10187B)

      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_ self args raw index =
    119   lazyList
    120     (_ : raw)
    121     (arg rest : self rest
    122       (sourceAstApply raw
    123         (sourceAstName (sourceProgramArgName arg index raw)))
    124       (succ index))
    125     args
    126 sourceProgramRawApply = (args raw : y sourceProgramRawApply_ args raw 0)
    127 
    128 sourceProgramWrapArgs_ self args body index =
    129   lazyList
    130     (_ : body)
    131     (arg rest :
    132       sourceAstLambda (sourceProgramArgName arg index body)
    133         (lazyMaybe
    134           (_ : self rest body (succ index))
    135           (c : sourceProgramApply3
    136             (sourceProgramName "matchResult" c)
    137             (lazyList
    138               (_ : sourceProgramOnFailure c)
    139               (other tail : sourceProgramAbsorbFailure c)
    140               rest)
    141             (sourceAstLambda (sourceProgramArgName arg index body)
    142               (sourceAstLambda (sourceProgramSynthetic "_" c)
    143                 (self rest body (succ index))))
    144             (sourceProgramChecked c
    145               (sourceAstName (sourceProgramArgName arg index body))))
    146           (snd arg)))
    147     args
    148 sourceProgramWrapArgs = (args body : y sourceProgramWrapArgs_ args body 0)
    149 
    150 sourceProgramAnyContract_ self args =
    151   lazyList
    152     (_ : false)
    153     (arg rest : lazyMaybe
    154       (_ : self rest)
    155       (contract : true)
    156       (snd arg))
    157     args
    158 sourceProgramAnyContract? = (args : y sourceProgramAnyContract_ args)
    159 
    160 sourceProgramAnyPhantom_ self args =
    161   lazyList
    162     (_ : false)
    163     (arg rest : lazyMaybe
    164       (_ : true)
    165       (name : self rest)
    166       (fst arg))
    167     args
    168 sourceProgramAnyPhantom? = (args : y sourceProgramAnyPhantom_ args)
    169 
    170 sourceProgramAllPhantom_ self args =
    171   lazyList
    172     (_ : true)
    173     (arg rest : lazyMaybe
    174       (_ : self rest)
    175       (name : false)
    176       (fst arg))
    177     args
    178 sourceProgramAllPhantom? = (args : y sourceProgramAllPhantom_ args)
    179 
    180 sourceProgramPlainArgs_ self args body =
    181   lazyList
    182     (_ : body)
    183     (arg rest : sourceAstLambda (sourceProgramArgName arg 0 body)
    184       (self rest body))
    185     args
    186 sourceProgramPlainArgs = (args body : y sourceProgramPlainArgs_ args body)
    187 
    188 sourceProgramLowerDefinition name args result body =
    189   lazyBool
    190     (_ : lazyBool
    191       (_ : sourceAstLocal
    192         (sourceToken sourceTokenName
    193           (append "_" (append (sourceTokenPayload name) "_raw"))
    194           (sourceTokenStart name) (sourceTokenEnd name))
    195         body
    196         (sourceProgramWrapArgs args
    197           (sourceProgramReturn result
    198             (sourceProgramRawApply args
    199               (sourceProgramName
    200                 (append "_" (append (sourceTokenPayload name) "_raw"))
    201                 body))))
    202         (sourceTokenStart name) (sourceAstEnd body))
    203       (_ : sourceProgramWrapArgs args (sourceProgramReturn result body))
    204       (sourceProgramAnyPhantom? args))
    205     (_ : sourceProgramPlainArgs args body)
    206     (or? (sourceProgramAnyContract? args)
    207       (lazyMaybe (_ : false) (contract : true) result))
    208 
    209 sourceProgramParseAnnotatedBinding input =
    210   parserBind (sourceGateExpect sourceTokenName) (name :
    211     parserBind (parserMany sourceProgramArgument) (args :
    212       (remaining : lazyBool
    213         (_ : parserThen (sourceGateExpect sourceTokenAssign)
    214           (parserBind (parserOptional
    215             (parserThen (sourceGateExpect sourceTokenAt)
    216               sourceProgramContract)) (result :
    217             parserMap (body : pair name
    218               (sourceProgramLowerDefinition name args result body))
    219               sourceProgramDefinitionValue)) remaining)
    220         (_ : parserReplyFail
    221           (parserDiagnostic 47 "supported contract head" t
    222             (sourceTokenStart name) t) remaining true false)
    223         (or? (not? (sourceProgramAnyPhantom? args))
    224           (and? (sourceProgramAllPhantom? args)
    225             (lte_? (length args) 2)))))) input
    226 
    227 -- Preserve the existing bounded annotated-head path. Plain heads now retain
    228 -- located equations; annotated definitions cannot merge with those groups.
    229 sourceProgramAnnotated_ self input = (lazyList (_ : false)
    230   (token rest : let kind = sourceTokenKind token in (lazyBool (_ : true)
    231     (_ : lazyBool (_ : lazyList (_ : false)
    232         (next unused : equal? (sourceTokenKind next) sourceTokenAt) rest)
    233       (_ : lazyBool (_ : false) (_ : self rest)
    234         (equal? kind sourceTokenNewline))
    235       (equal? kind sourceTokenAssign)) (equal? kind sourceTokenAt))) input)
    236 sourceProgramAnnotated? input = y sourceProgramAnnotated_ input
    237 sourceProgramParsePlainBinding input = (lazyList
    238   (_ : sourceGateAtomError input)
    239   (token rest : sourceEquationBinding
    240     (sourceGateParseLayoutValue
    241       (sourceGateExprIndented (sourcePositionColumn (sourceTokenStart token)))
    242       sourceGateExprIndented "definition body") input) input)
    243 sourceProgramParseDefinition input =
    244   lazyBool
    245     (_ : lazyBool (_ : sourceProgramParseAnnotatedBinding input)
    246       (_ : sourceProgramParsePlainBinding input) (sourceProgramAnnotated? input))
    247     (_ : parserReplyFail
    248       (parserDiagnostic 2 sourceTokenAssign t t t) input false false)
    249     (sourceProgramDefinitionHead? input)
    250 
    251 sourceProgramParseTokens =
    252   parserThen sourceProgramSkipNewlines
    253     (parserBind
    254       (parserMany
    255         (parserBefore sourceProgramParseDefinition sourceProgramSkipNewlines))
    256       (definitions : parserBind
    257         (input : lazyResult
    258           (diagnostic rest : parserReplyFail diagnostic input false false)
    259           (groups unused : parserReplyOk groups input false false)
    260           (sourceEquationGroups definitions))
    261         (groups : parserBind
    262           (parserOptional
    263             (parserBefore sourceGateExpr sourceProgramSkipNewlines))
    264           (final : parserMap (_ : pair groups final) sourceGateEof))))
    265 
    266 parseGateProgram = parserWithLexer lexGateSource sourceProgramParseTokens
    267