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