23c8142e9629f029ae22b7c0b377bbfb69e4f9ecc5ce452094c47d063a49c9d6.tri (22875B)
1 !import prelude * 2 !import parser * 3 !import source_lexer * 4 !import source_ast * 5 !import source_equations * 6 !export * 7 8 -- Small, single-expression gate grammar. Its recursive expression parser is 9 -- one direct self-recursive dispatcher; atom/application/lambda helpers receive 10 -- the recursive parser as an argument rather than forming top-level cycles. 11 sourceGateExpected kind found location = 12 parserDiagnostic 2 kind found location t 13 14 sourceGateExpect kind input = 15 lazyList 16 (_ : parserReplyFail (sourceGateExpected kind t t) input false false) 17 (token rest : 18 lazyBool 19 (_ : parserReplyOk token rest true false) 20 (_ : parserReplyFail 21 (sourceGateExpected kind (sourceTokenKind token) 22 (sourceTokenStart token)) input false false) 23 (equal? (sourceTokenKind token) kind)) 24 input 25 26 sourceGateEof input = 27 lazyList 28 (_ : parserReplyOk t input false false) 29 (token rest : parserReplyFail 30 (sourceGateExpected t (sourceTokenKind token) 31 (sourceTokenStart token)) input false false) 32 input 33 34 -- A lambda head is one or more name tokens followed by a same-line colon. 35 -- Stop scanning on the first non-name; do not mistake an ordinary `f x` 36 -- application for a multi-binder head when no colon follows. 37 sourceGateLambdaHead? input = (let rec 38 scan tokens seen = (lazyList (_ : false) 39 (token rest : lazyBool (_ : scan rest true) 40 (_ : and? seen (equal? (sourceTokenKind token) sourceTokenColon)) 41 (equal? (sourceTokenKind token) sourceTokenName)) tokens) 42 in scan input false) 43 44 sourceGateParseLambda expression input = 45 parserBind (parserSome (sourceGateExpect sourceTokenName)) (names : 46 parserThen (sourceGateExpect sourceTokenColon) 47 (parserThen sourceGateSkipNestedNewlines 48 (parserMap (body : foldr 49 (value name : sourceAstLambda name value) body names) 50 expression))) input 51 52 sourceGateParseGroup expression input = 53 parserBind (sourceGateExpect sourceTokenOpen) (open : 54 parserThen sourceGateSkipNestedNewlines 55 (parserBind expression (body : 56 parserThen sourceGateSkipNestedNewlines 57 (parserMap (close : sourceAstGroup open body close) 58 (sourceGateExpect sourceTokenClose))))) input 59 60 -- Shared binding head: retain patterns until contiguous equations have 61 -- coalesced. Only unique all-name singleton heads take the lambda fast path. 62 sourceGateParseBindingWith valueParser input = sourceEquationBinding valueParser input 63 64 sourceGateParseBinding expression = sourceGateParseBindingWith expression 65 66 -- A body belongs to its definition/statement even when its first operand 67 -- follows a newline. Never reset the continuation boundary to that operand. 68 -- Validate before consuming it so a sibling cannot become a missing body. 69 sourceGateParseLayoutFirst expression mode label input = (lazyList 70 (_ : parserReplyFail (parserDiagnostic 40 label t t t) input false false) 71 (token rest : lazyBool 72 (_ : expression input) 73 (_ : parserReplyFail (parserDiagnostic 40 label (sourceTokenKind token) 74 (sourceTokenStart token) t) input false false) 75 (or? (fst mode) 76 (not? (lte_? (sourcePositionColumn (sourceTokenStart token)) (snd mode))))) input) 77 78 sourceGateParseLayoutValue expression mode label input = (lazyList 79 (_ : expression input) 80 (token rest : lazyBool 81 (_ : parserThen sourceGateSkipNestedNewlines 82 (sourceGateParseLayoutFirst expression mode label) input) 83 (_ : expression input) 84 (equal? (sourceTokenKind token) sourceTokenNewline)) input) 85 86 -- Local groups share the program head grammar, but are deliberately not 87 -- dependency-sorted: nested nonrecursive lets expose only earlier groups. 88 sourceGateLocalValue indentedExpression column input = 89 sourceGateParseLayoutValue (indentedExpression column) (sourceGateLayoutIndented column) 90 "local binding value" input 91 sourceGateLocalNext? input column = (lazyList (_ : false) 92 (token rest : lazyBool 93 (_ : sourceGateLocalAfterNewlines? rest column) 94 (_ : false) (equal? (sourceTokenKind token) sourceTokenNewline)) input) 95 sourceGateLocalAfterNewlines? input column = (lazyList (_ : false) 96 (token rest : lazyBool (_ : sourceGateLocalAfterNewlines? rest column) 97 (_ : and? (equal? (sourcePositionColumn (sourceTokenStart token)) column) 98 (sourceEquationBindingHead? input)) 99 (equal? (sourceTokenKind token) sourceTokenNewline)) input) 100 sourceGateLocalNext indentedExpression column input = (lazyBool 101 (_ : parserThen sourceGateSkipNestedNewlines 102 (sourceEquationBinding (sourceGateLocalValue indentedExpression column)) input) 103 (_ : parserReplyFail (sourceGateExpected "local equation" t t) input false false) 104 (sourceGateLocalNext? input column)) 105 sourceGateLocalGroupsReply bindings input = (lazyResult 106 (diagnostic remainder : parserReplyFail diagnostic input false false) 107 (groups unused : lazyResult 108 (diagnostic remainder : parserReplyFail diagnostic input false false) 109 (_ unused : parserReplyOk groups input false false) 110 (sourceEquationUnique groups)) (sourceEquationGroups bindings)) 111 sourceGateLocalBindings valueParser indentedExpression input = (lazyList 112 (_ : sourceGateAtomError input) 113 (token rest : parserBind 114 (sourceEquationBinding valueParser) 115 (first : parserBind (parserMany (sourceGateLocalNext indentedExpression 116 (sourcePositionColumn (sourceTokenStart token)))) 117 (remaining : sourceGateLocalGroupsReply (pair first remaining))) input) input) 118 sourceGateLocalBuild bindings body start end = (foldr 119 (rest binding : sourceAstLocal (fst binding) (snd binding) rest start end) 120 body bindings) 121 sourceGateLocalIndented indentedExpression parentColumn input = (lazyList 122 (_ : parserReplyFail (parserDiagnostic 40 "indented local block" t t t) input false false) 123 (token rest : lazyBool 124 (_ : sourceGateLocalBindings 125 (sourceGateLocalValue indentedExpression (sourcePositionColumn (sourceTokenStart token))) 126 indentedExpression input) 127 (_ : parserReplyFail (parserDiagnostic 40 "indented local block" 128 (sourceTokenKind token) (sourceTokenStart token) t) input false false) 129 (and? (not? (lte_? (sourcePositionColumn (sourceTokenStart token)) parentColumn)) 130 (not? (lte_? (sourcePositionColumn (sourceTokenStart token)) 1)))) input) 131 -- An inline binding inherits its enclosing expression context (including 132 -- explicit grouping). A newline after let/where opens a separate local block. 133 sourceGateLocalStart expression indentedExpression mode input = (lazyList 134 (_ : sourceGateLocalBindings 135 (sourceGateParseLayoutValue expression mode "local binding value") indentedExpression input) 136 (token rest : lazyBool 137 (_ : parserThen sourceGateSkipNestedNewlines 138 (sourceGateLocalIndented indentedExpression (snd mode)) input) 139 (_ : sourceGateLocalBindings 140 (sourceGateParseLayoutValue expression mode "local binding value") indentedExpression input) 141 (equal? (sourceTokenKind token) sourceTokenNewline)) input) 142 -- rec applies to exactly one contiguous function group. It is not a mutually 143 -- recursive block and never changes the scope of plain let/where bindings. 144 sourceGateLocalFinish ^false bindings body start end input = 145 parserReplyOk (sourceGateLocalBuild bindings body start end) input false false 146 sourceGateLocalFinish ^true [binding] body start end input = 147 parserReplyOk (sourceAstRecursive (fst binding) (snd binding) body start end) input false false 148 sourceGateLocalFinish _ _ _ start _ input = 149 parserReplyFail (parserDiagnostic 48 "one recursive local function" t start t) input false false 150 151 sourceGateRecursive = (parserMap (present : lazyMaybe (_ : false) (_ : true) present) 152 (parserOptional (sourceGateExpect sourceTokenRec))) 153 154 sourceGateParseLet expression indentedExpression mode input = (parserBind 155 (sourceGateExpect sourceTokenLet) (keyword : parserBind sourceGateRecursive (recursive : 156 parserBind (sourceGateLocalStart expression indentedExpression mode) (bindings : 157 parserThen sourceGateSkipNestedNewlines 158 (parserThen (sourceGateExpect sourceTokenIn) 159 (parserBind (sourceGateParseLayoutValue expression mode "local binding body") 160 (body : sourceGateLocalFinish recursive bindings body 161 (sourceTokenStart keyword) (sourceAstEnd body))))))) input) 162 sourceGateParseWhere expression indentedExpression body mode input = (parserThen 163 (sourceGateExpect sourceTokenWhere) (parserBind sourceGateRecursive (recursive : 164 parserBind (sourceGateLocalStart expression indentedExpression mode) (bindings : 165 sourceGateLocalFinish recursive bindings body (sourceAstStart body) 166 (sourceAstEnd (snd (foldl (_ binding : binding) (fst bindings) bindings)))))) input) 167 168 -- Case arms share equation patterns/validation. The branch column delimits 169 -- bodies, including nested cases and do blocks. A pattern has no function name. 170 sourceGateCaseArm expression column input = (parserBind sourceEquationParse (pattern : 171 parserThen (sourceGateExpect sourceTokenAssign) 172 (parserMap (body : pair [pattern] body) 173 (sourceGateParseLayoutValue (tokens : expression tokens (sourceGateLayoutIndented column)) 174 (sourceGateLayoutIndented column) "case arm body"))) input) 175 sourceGateCasePatternStarts? kind = (or? (sourceGateAtomStarts? kind) 176 (equal? kind sourceTokenPin)) 177 sourceGateCaseSameColumn? input column = (lazyList (_ : false) 178 (token rest : lazyBool (_ : sourceGateCaseSameColumn? rest column) 179 (_ : and? (equal? (sourcePositionColumn (sourceTokenStart token)) column) 180 (sourceGateCasePatternStarts? (sourceTokenKind token))) 181 (equal? (sourceTokenKind token) sourceTokenNewline)) input) 182 sourceGateCaseNext expression column input = (lazyList 183 (_ : parserReplyFail (sourceGateExpected "case arm" t t) input false false) 184 (token rest : lazyBool 185 (_ : parserThen sourceGateSkipNestedNewlines (sourceGateCaseArm expression column) input) 186 (_ : parserReplyFail (sourceGateExpected "case arm" t t) input false false) 187 (and? (equal? (sourceTokenKind token) sourceTokenNewline) 188 (sourceGateCaseSameColumn? rest column))) input) 189 sourceGateCaseFirst expression keyword subject parentColumn input = (lazyList 190 (_ : parserReplyFail (parserDiagnostic 40 "indented case arms" t t t) input false false) 191 (token rest : let column = sourcePositionColumn (sourceTokenStart token) in 192 lazyBool 193 (_ : parserBind (sourceGateCaseArm expression column) (first : 194 parserMap (remaining : sourceAstCase subject (pair first remaining) 195 (sourceTokenStart keyword) (sourceAstEnd (snd (foldl (_ arm : arm) first remaining)))) 196 (parserMany (sourceGateCaseNext expression column))) input) 197 (_ : parserReplyFail (parserDiagnostic 40 "indented case arms" 198 (sourceTokenKind token) (sourceTokenStart token) t) input false false) 199 (and? (not? (lte_? column parentColumn)) (not? (lte_? column 1)))) input) 200 sourceGateParseCase expression mode input = (parserBind (sourceGateExpect sourceTokenCase) (keyword : 201 parserBind (tokens : expression tokens mode) (subject : 202 parserThen (sourceGateExpect sourceTokenOf) 203 (parserThen (sourceGateExpect sourceTokenNewline) 204 (parserThen sourceGateSkipNestedNewlines 205 (sourceGateCaseFirst expression keyword subject (snd mode)))))) input) 206 207 -- Newlines are meaningful between top-level expressions but are trivia 208 -- within a bracketed list. Each element is one atom: applications inside a 209 -- list need parentheses, as in the bootstrap grammar. 210 sourceGateSkipNestedNewlines = 211 parserMap (_ : t) (parserMany (sourceGateExpect sourceTokenNewline)) 212 213 sourceGateParseList atom input = 214 parserBind (sourceGateExpect sourceTokenLeftBracket) (open : 215 parserThen sourceGateSkipNestedNewlines 216 (parserBind 217 (parserMany 218 (parserBefore atom sourceGateSkipNestedNewlines)) 219 (elements : parserMap 220 (close : sourceAstList open elements close) 221 (sourceGateExpect sourceTokenRightBracket)))) input 222 223 sourceGateAtomError input = 224 lazyList 225 (_ : parserReplyFail (sourceGateExpected 7 t t) input false false) 226 (token rest : parserReplyFail 227 (sourceGateExpected 7 (sourceTokenKind token) 228 (sourceTokenStart token)) input false false) 229 input 230 231 -- A do block begins after an explicit operator atom and a newline. Its 232 -- statements start at one located column; deeper lines belong to the current 233 -- expression, while a new line at that column starts the next statement. 234 sourceGateDoBindHead? input = 235 lazyList 236 (_ : false) 237 (token rest : 238 lazyBool 239 (_ : lazyList 240 (_ : false) 241 (next tail : equal? (sourceTokenKind next) sourceTokenBindArrow) 242 rest) 243 (_ : false) 244 (equal? (sourceTokenKind token) sourceTokenName)) 245 input 246 247 sourceGateDoSameColumn? input column = 248 lazyList 249 (_ : false) 250 (token rest : 251 lazyBool 252 (_ : sourceGateDoSameColumn? rest column) 253 (_ : and? 254 (equal? (sourcePositionColumn (sourceTokenStart token)) column) 255 (sourceGateAtomStarts? (sourceTokenKind token))) 256 (equal? (sourceTokenKind token) sourceTokenNewline)) 257 input 258 259 260 261 sourceGateParseDoStatement expression indentedExpression column input = 262 lazyBool 263 (_ : parserBind (sourceGateExpect sourceTokenName) (name : 264 parserThen (sourceGateExpect sourceTokenBindArrow) 265 (parserMap (action : pair (just name) action) 266 (sourceGateParseLayoutValue 267 (tokens : expression tokens (sourceGateLayoutIndented column)) 268 (sourceGateLayoutIndented column) "do binding action"))) input) 269 (_ : parserMap (action : pair nothing action) 270 (tokens : expression tokens (sourceGateLayoutIndented column)) 271 input) 272 (sourceGateDoBindHead? input) 273 274 sourceGateParseDoNext expression indentedExpression column input = 275 lazyBool 276 (_ : parserThen sourceGateSkipNestedNewlines 277 (sourceGateParseDoStatement expression indentedExpression column) 278 input) 279 (_ : parserReplyFail 280 (sourceGateExpected "do statement" t t) input false false) 281 (sourceGateDoSameColumn? input column) 282 283 sourceGateParseDoFirst expression indentedExpression parentColumn keyword operator input = 284 lazyList 285 (_ : parserReplyFail 286 (parserDiagnostic 40 "indented do block" t t t) input false false) 287 (token rest : 288 lazyBool 289 (_ : parserBind 290 (sourceGateParseDoStatement expression indentedExpression 291 (sourcePositionColumn (sourceTokenStart token))) 292 (first : parserBind 293 (parserMany (sourceGateParseDoNext expression indentedExpression 294 (sourcePositionColumn (sourceTokenStart token)))) 295 (remaining : (nextInput : let last = foldl (_ statement : statement) first remaining in 296 lazyMaybe 297 (_ : parserReplyOk 298 (sourceAstDo keyword operator (pair first remaining) 299 (sourceAstDoStatementValue last)) 300 nextInput false false) 301 (name : parserReplyFail 302 (parserDiagnostic 40 "do final expression" t 303 (sourceTokenStart name) t) 304 nextInput false false) 305 (sourceAstDoStatementBinder last)))) 306 input) 307 (_ : parserReplyFail 308 (parserDiagnostic 40 "indented do block" 309 (sourceTokenKind token) (sourceTokenStart token) t) 310 input false false) 311 (and? (not? (lte_? (sourcePositionColumn (sourceTokenStart token)) parentColumn)) 312 (not? (lte_? (sourcePositionColumn (sourceTokenStart token)) 1)))) 313 input 314 315 sourceGateParseDo expression indentedExpression parentColumn atom input = 316 parserBind (sourceGateExpect sourceTokenDo) (keyword : 317 parserThen sourceGateSkipNestedNewlines 318 (parserBind atom (operator : 319 parserThen (sourceGateExpect sourceTokenNewline) 320 (parserThen sourceGateSkipNestedNewlines 321 (sourceGateParseDoFirst expression indentedExpression parentColumn 322 keyword operator))))) input 323 324 -- Dispatch only after observing the first token. A selected parser consumes 325 -- its opening token; its failure must not retry another token kind. Unknown 326 -- prefixes retain the same unconsumed atom diagnostic as ordered choice. 327 sourceGateParseAtom expression mode input = (lazyList 328 (_ : sourceGateAtomError input) 329 (token _ : (let indented column tokens = expression tokens (sourceGateLayoutIndented column) in 330 let parse = (case sourceTokenKind token of 331 ^sourceTokenCase = sourceGateParseCase expression mode 332 ^sourceTokenDo = (sourceGateParseDo expression indented (snd mode) 333 (sourceGateParseAtom expression sourceGateLayoutTop)) 334 ^sourceTokenLet = sourceGateParseLet (tokens : expression tokens mode) indented mode 335 ^sourceTokenT = parserMap sourceAstLeaf (sourceGateExpect sourceTokenT) 336 ^sourceTokenName = parserMap sourceAstName (sourceGateExpect sourceTokenName) 337 ^sourceTokenNumber = parserMap sourceAstNumber (sourceGateExpect sourceTokenNumber) 338 ^sourceTokenString = parserMap sourceAstString (sourceGateExpect sourceTokenString) 339 ^sourceTokenOpen = sourceGateParseGroup (tokens : expression tokens sourceGateLayoutNested) 340 ^sourceTokenLeftBracket = sourceGateParseList (sourceGateParseAtom expression sourceGateLayoutNested) 341 _ = sourceGateAtomError) 342 in parse input)) input) 343 344 -- Only a successful atom consumes another operand. A close paren, colon or 345 -- newline is left intact for the enclosing parser; an opened but malformed 346 -- group propagates its consumed failure instead of silently ending the app. 347 -- A newline continues inside a delimiter or deeper than its owner, when a 348 -- following token can start an atom. Looking ahead prevents a newline before 349 -- ')' or 'where' from becoming a committed atom failure. 350 sourceGateAtomStarts? kind = 351 or? (equal? kind sourceTokenT) 352 (or? (equal? kind sourceTokenName) 353 (or? (equal? kind sourceTokenNumber) 354 (or? (equal? kind sourceTokenString) 355 (or? (equal? kind sourceTokenOpen) 356 (or? (equal? kind sourceTokenLeftBracket) 357 (or? (equal? kind sourceTokenLet) 358 (or? (equal? kind sourceTokenDo) (equal? kind sourceTokenCase)))))))) 359 360 -- mode = pair insideDelimiter baseColumn. A top-level baseColumn of zero 361 -- disables continuation; a nonzero column allows strictly deeper lines. 362 sourceGateLayoutTop = pair false 0 363 sourceGateLayoutNested = pair true 0 364 sourceGateLayoutIndented column = pair false column 365 366 sourceGateNewlineStartsWith? tokens predicate mode inclusive = 367 lazyList 368 (_ : false) 369 (token rest : 370 lazyBool 371 (_ : sourceGateNewlineStartsWith? rest predicate mode inclusive) 372 (_ : and? (predicate (sourceTokenKind token)) 373 (or? (fst mode) 374 (lazyBool 375 (_ : lte_? (snd mode) (sourcePositionColumn (sourceTokenStart token))) 376 (_ : and? (not? (isZero_? (snd mode))) 377 (not? (lte_? (sourcePositionColumn (sourceTokenStart token)) (snd mode)))) 378 inclusive))) 379 (equal? (sourceTokenKind token) sourceTokenNewline)) 380 tokens 381 382 383 384 sourceGateNewlineStarts? tokens predicate mode = 385 sourceGateNewlineStartsWith? tokens predicate mode false 386 387 -- Do not consume a newline until a matching token at an allowed indentation 388 -- is visible. This retains layout boundaries in parser remainders. 389 sourceGateAfterNewlines mode inclusive starts parser input = 390 lazyList 391 (_ : parser input) 392 (token rest : 393 lazyBool 394 (_ : lazyBool 395 (_ : parserThen sourceGateSkipNestedNewlines parser input) 396 (_ : parser input) 397 (sourceGateNewlineStartsWith? rest starts mode inclusive)) 398 (_ : parser input) 399 (equal? (sourceTokenKind token) sourceTokenNewline)) 400 input 401 402 -- Operators and `where` may align with their owner, but cannot cross a 403 -- dedent out of an arm, local binding or do statement. 404 sourceGateAfterLayoutNewlines mode = sourceGateAfterNewlines mode false 405 sourceGateAfterSuffixNewlines mode = sourceGateAfterNewlines mode true 406 407 sourceGateAppNext mode expression input = 408 sourceGateAfterLayoutNewlines mode sourceGateAtomStarts? 409 (sourceGateParseAtom expression mode) input 410 411 sourceGateParseApplication mode expression input = (let rec 412 remaining input acc consumed = (parserMatchReply 413 (diagnostic rest stepConsumed committed : lazyBool 414 (_ : parserReplyFail diagnostic rest (or? consumed stepConsumed) committed) 415 (_ : parserReplyOk acc input consumed false) 416 (or? stepConsumed committed)) 417 (atom rest _ _ : remaining rest (sourceAstApply acc atom) true) 418 (sourceGateAppNext mode expression input)) 419 in parserBind (sourceGateParseAtom expression mode) 420 (first : rest : remaining rest first false) input) 421 422 sourceGatePipeStarts? kind = 423 or? (equal? kind sourceTokenPipeBackward) 424 (equal? kind sourceTokenPipeForward) 425 426 sourceGateParsePipeOperator = 427 parserOr (sourceGateExpect sourceTokenPipeBackward) 428 (sourceGateExpect sourceTokenPipeForward) 429 430 sourceGateParsePipeSegment mode expression input = 431 parserBind 432 (sourceGateAfterSuffixNewlines mode 433 sourceGatePipeStarts? sourceGateParsePipeOperator) 434 (operator : parserMap (right : pair operator right) 435 (sourceGateParseLayoutValue (sourceGateParseApplication mode expression) 436 mode "pipe operand")) input 437 438 -- Application binds tighter than a left-associative pipe chain. Retain an 439 -- explicit located AST pipe; core resolution chooses the direction later. 440 sourceGateParsePipes mode expression input = 441 parserBind (sourceGateParseApplication mode expression) (first : 442 parserMap (segments : foldl 443 (left segment : sourceAstPipe (fst segment) left (snd segment)) 444 first segments) 445 (parserMany (sourceGateParsePipeSegment mode expression))) input 446 447 sourceGateExprWithLayout input mode = 448 lazyBool 449 (_ : sourceGateParseLambda (tokens : sourceGateExprWithLayout tokens mode) input) 450 (_ : parserBind 451 (sourceGateParsePipes mode sourceGateExprWithLayout) 452 (body : 453 parserMap (suffix : lazyMaybe (_ : body) (local : local) suffix) 454 (parserOptional (sourceGateAfterSuffixNewlines mode 455 (kind : equal? kind sourceTokenWhere) 456 (sourceGateParseWhere 457 (tokens : sourceGateExprWithLayout tokens mode) 458 (column tokens : sourceGateExprWithLayout tokens (sourceGateLayoutIndented column)) 459 body mode)))) input) 460 (sourceGateLambdaHead? input) 461 462 sourceGateExpr = (input : sourceGateExprWithLayout input sourceGateLayoutTop) 463 sourceGateExprIndented = (column input : 464 sourceGateExprWithLayout input (sourceGateLayoutIndented column)) 465 466 parseGateTokens input = 467 parserBefore sourceGateExpr sourceGateEof input 468 469 parseGateSource = parserWithLexer lexGateSource parseGateTokens 470