diff --git a/stage0/src/Init/Lean/Elab/Quotation.lean b/stage0/src/Init/Lean/Elab/Quotation.lean index b3a4266c75..a8115b1f1e 100644 --- a/stage0/src/Init/Lean/Elab/Quotation.lean +++ b/stage0/src/Init/Lean/Elab/Quotation.lean @@ -36,30 +36,30 @@ instance Nat.HasQuote : HasQuote Nat := ⟨fun n => mkStxNumLit $ toString n⟩ private def quoteName : Name → Syntax | Name.anonymous => Unhygienic.run `(_root_.Lean.Name.anonymous) -| Name.str n s _ => Unhygienic.run `(_root_.Lean.mkNameStr %%(quoteName n) %%(Lean.HasQuote.quote s)) -| Name.num n i _ => Unhygienic.run `(_root_.Lean.mkNameNum %%(quoteName n) %%(Lean.HasQuote.quote i)) +| Name.str n s _ => Unhygienic.run `(_root_.Lean.mkNameStr $(quoteName n) $(Lean.HasQuote.quote s)) +| Name.num n i _ => Unhygienic.run `(_root_.Lean.mkNameNum $(quoteName n) $(Lean.HasQuote.quote i)) instance Name.HasQuote : HasQuote Name := ⟨quoteName⟩ private def appN (fn : Syntax) (args : Array Syntax) : Syntax := -args.foldl (fun fn arg => Unhygienic.run `(%%fn %%arg)) fn +args.foldl (fun fn arg => Unhygienic.run `($fn $arg)) fn instance Prod.HasQuote {α β : Type} [HasQuote α] [HasQuote β] : HasQuote (α × β) := -⟨fun ⟨a, b⟩ => Unhygienic.run `(_root_.Prod.mk %%(Lean.HasQuote.quote a) %%(Lean.HasQuote.quote b))⟩ +⟨fun ⟨a, b⟩ => Unhygienic.run `(_root_.Prod.mk $(Lean.HasQuote.quote a) $(Lean.HasQuote.quote b))⟩ private def quoteList {α : Type} [HasQuote α] : List α → Syntax | [] => Unhygienic.run `(_root_.List.nil) -| (x::xs) => Unhygienic.run `(_root_.List.cons %%(Lean.HasQuote.quote x) %%(quoteList xs)) +| (x::xs) => Unhygienic.run `(_root_.List.cons $(Lean.HasQuote.quote x) $(quoteList xs)) instance List.HasQuote {α : Type} [HasQuote α] : HasQuote (List α) := ⟨quoteList⟩ instance Array.HasQuote {α : Type} [HasQuote α] : HasQuote (Array α) := -⟨fun xs => let stx := quote xs.toList; Unhygienic.run `(_root_.List.toArray %%stx)⟩ +⟨fun xs => let stx := quote xs.toList; Unhygienic.run `(_root_.List.toArray $stx)⟩ namespace Elab namespace Term --- `%%e*` is an antiquotation "splice" matching an arbitrary number of syntax nodes +-- `$e*` is an antiquotation "splice" matching an arbitrary number of syntax nodes private def isAntiquotSplice (stx : Syntax) : Bool := stx.isOfKind `Lean.Parser.Term.antiquot && (stx.getArg 3).getOptional.isSome @@ -78,10 +78,10 @@ private partial def quoteSyntax (env : Environment) : Syntax → TermElabM Synta let preresolved := resolveGlobalName env currNamespace openDecls val ++ preresolved; let val := quote val; -- `scp` is bound in stxQuot.expand - val ← `(Lean.addMacroScope %%val scp); + val ← `(Lean.addMacroScope $val scp); let args := quote preresolved; -- TODO: simplify quotations when we're no longer limited by name resolution in the old frontend - `(Lean.Syntax.ident Option.none (String.toSubstring %%(Lean.mkStxStrLit (HasToString.toString rawVal))) %%val %%args) + `(Lean.Syntax.ident Option.none (String.toSubstring $(Lean.mkStxStrLit (HasToString.toString rawVal))) $val $args) -- if antiquotation, insert contents as-is, else recurse | stx@(Syntax.node k args) => if k == `Lean.Parser.Term.antiquot then @@ -91,13 +91,13 @@ private partial def quoteSyntax (env : Environment) : Syntax → TermElabM Synta else if isAntiquotSplicePat stx then -- top-level antiquotation splice pattern: inject args array let quoted := (args.get! 0).getArg 1; - `(Lean.Syntax.node Lean.nullKind %%quoted) + `(Lean.Syntax.node Lean.nullKind $quoted) else do let k := quote k; args ← quote <$> args.mapM quoteSyntax; - `(Lean.Syntax.node %%k %%args) + `(Lean.Syntax.node $k $args) | Syntax.atom info val => - `(Lean.Syntax.atom Option.none %%(Lean.mkStxStrLit val)) + `(Lean.Syntax.atom Option.none $(Lean.mkStxStrLit val)) | Syntax.missing => unreachable! def stxQuot.expand (env : Environment) (stx : Syntax) : TermElabM Syntax := do @@ -107,9 +107,9 @@ let quoted := stx.getArg 1; depending on this binding. Note that regular function calls do not introduce a new macro scope (i.e. we preserve referential transparency), so we can refer to this same `scp` inside `quoteSyntax` by including it literally in a syntax quotation. -/ --- TODO: simplify to `(do scp ← getCurrMacroScope; pure %%(quoteSyntax env quoted)) +-- TODO: simplify to `(do scp ← getCurrMacroScope; pure $(quoteSyntax env quoted)) stx ← quoteSyntax env quoted; -`(HasBind.bind Lean.MonadQuotation.getCurrMacroScope (fun scp => HasPure.pure %%stx)) +`(HasBind.bind Lean.MonadQuotation.getCurrMacroScope (fun scp => HasPure.pure $stx)) /- NOTE: It may seem like the newly introduced binding `scp` may accidentally capture identifiers in an antiquotation introduced by `quoteSyntax`. However, note that the syntax quotation above enjoys the same hygiene guarantees as @@ -141,21 +141,21 @@ private abbrev Alt := List Syntax × Syntax -- bindings on the RHS. private def isVarPat? (pat : Syntax) : Option (Syntax → TermElabM Syntax) := -- TODO: reimplement using match_syntax -if pat.isOfKind `Lean.Parser.Term.id then some $ fun rhs => `(let %%pat := discr; %%rhs) +if pat.isOfKind `Lean.Parser.Term.id then some $ fun rhs => `(let $pat := discr; $rhs) else if pat.isOfKind `Lean.Parser.Term.hole then some pure else if pat.isOfKind `Lean.Parser.Term.stxQuot then let quoted := pat.getArg 1; -- We assume that atoms are uniquely determined by the surrounding node and never have to be checked if quoted.isAtom then some pure - -- TODO: antiquotations with kinds (`%%id:id`) probably can't be handled as unconditional patterns + -- TODO: antiquotations with kinds (`$id:id`) probably can't be handled as unconditional patterns else if quoted.isOfKind `Lean.Parser.Term.antiquot then let anti := quoted.getArg 1; if isAntiquotSplice quoted then some $ fun _ => throwError quoted "unexpected antiquotation splice" - else if anti.isOfKind `Lean.Parser.Term.id then some $ fun rhs => `(let %%anti := discr; %%rhs) + else if anti.isOfKind `Lean.Parser.Term.id then some $ fun rhs => `(let $anti := discr; $rhs) else unreachable! else if isAntiquotSplicePat quoted then let anti := (quoted.getArg 0).getArg 1; - some $ fun rhs => `(let %%anti := Lean.Syntax.getArgs discr; %%rhs) + some $ fun rhs => `(let $anti := Lean.Syntax.getArgs discr; $rhs) else none else none @@ -170,7 +170,7 @@ private def altNextNode? : Alt → Option SyntaxNode -- Assuming that the first pattern of the alternative is taken, replace it with patterns (if any) for its -- child nodes. --- Ex: `(%%a + (- %%b)) => `(%%a), `(+), `(- %%b) +-- Ex: `($a + (- $b)) => `($a), `(+), `(- $b) -- Note: The atom pattern `(+) will be discarded in a later step private def explodeHeadPat (numArgs : Nat) : Alt → TermElabM Alt | (pat::pats, rhs) => match isVarPat? pat with @@ -202,7 +202,7 @@ private partial def compileStxMatch (ref : Syntax) : List Syntax → List Alt | some node => do let shape := nodeShape node; -- introduce pattern matches on the discriminant's children - newDiscrs ← (List.range node.getArgs.size).mapM $ fun i => `(Lean.Syntax.getArg discr %%(Lean.HasQuote.quote i)); + newDiscrs ← (List.range node.getArgs.size).mapM $ fun i => `(Lean.Syntax.getArg discr $(Lean.HasQuote.quote i)); -- collect matching alternatives and explode them let yesAlts := alts.filter $ fun alt => match altNextNode? alt with some n => nodeShape n == shape | none => true; yesAlts ← yesAlts.mapM $ explodeHeadPat node.getArgs.size; @@ -212,12 +212,12 @@ private partial def compileStxMatch (ref : Syntax) : List Syntax → List Alt -- NOTE: use fresh macro scopes for recursion so that different `discr`s introduced by the quotation below do not collide yes ← withFreshMacroScope $ compileStxMatch (newDiscrs ++ discrs) yesAlts; no ← withFreshMacroScope $ compileStxMatch (discr::discrs) noAlts; - `(let discr := %%discr; if Lean.Syntax.isOfKind discr %%(Lean.HasQuote.quote (Prod.fst shape)) && Array.size (Lean.Syntax.getArgs discr) == %%(Lean.HasQuote.quote (Prod.snd shape)) then %%yes else %%no) + `(let discr := $discr; if Lean.Syntax.isOfKind discr $(Lean.HasQuote.quote (Prod.fst shape)) && Array.size (Lean.Syntax.getArgs discr) == $(Lean.HasQuote.quote (Prod.snd shape)) then $yes else $no) -- only unconditional patterns: introduce binds and discard patterns | none => do alts ← alts.mapM $ explodeHeadPat 0; res ← withFreshMacroScope $ compileStxMatch discrs alts; - `(let discr := %%discr; %%res) + `(let discr := $discr; $res) | _, _ => unreachable! private partial def getAntiquotVarsAux : Syntax → TermElabM (List Syntax) @@ -249,13 +249,13 @@ private def letBindRhss (cont : List Alt → TermElabM Syntax) : List Alt → Li rhs' ← `(rhs ()); -- NOTE: new macro scope so that introduced bindings do not collide stx ← withFreshMacroScope $ letBindRhss alts ((pats, rhs')::altsRev'); - `(let rhs := fun _ => %%rhs; %%stx) + `(let rhs := fun _ => $rhs; $stx) | _ => do - -- rhs ← `(fun %%vars* => %%rhs) + -- rhs ← `(fun $vars* => $rhs) let rhs := Syntax.node `Lean.Parser.Term.fun #[mkAtom "fun", Syntax.node `null vars.toArray, mkAtom "=>", rhs]; rhs' ← `(rhs); stx ← withFreshMacroScope $ letBindRhss alts ((pats, rhs')::altsRev'); - `(let rhs := %%rhs; %%stx) + `(let rhs := $rhs; $stx) def match_syntax.expand (stx : SyntaxNode) : TermElabM Syntax := do let discr := stx.getArg 1; @@ -325,17 +325,17 @@ private unsafe partial def toPreterm (env : Environment) : Syntax → Except Str let con := args.get! 2; let yes := args.get! 4; let no := args.get! 6; - toPreterm $ Unhygienic.run `(ite %%con %%yes %%no) + toPreterm $ Unhygienic.run `(ite $con $yes $no) | `Lean.Parser.Term.paren => let inner := (args.get! 1).getArgs; if inner.size == 0 then pure $ Lean.mkConst `Unit.unit else toPreterm $ inner.get! 0 | `Lean.Parser.Term.band => let lhs := args.get! 0; let rhs := args.get! 2; - toPreterm $ Unhygienic.run `(and %%lhs %%rhs) + toPreterm $ Unhygienic.run `(and $lhs $rhs) | `Lean.Parser.Term.beq => let lhs := args.get! 0; let rhs := args.get! 2; - toPreterm $ Unhygienic.run `(HasBeq.beq %%lhs %%rhs) + toPreterm $ Unhygienic.run `(HasBeq.beq $lhs $rhs) | `strLit => pure $ mkStrLit $ stx.isStrLit?.getD "" | `numLit => pure $ mkNatLit $ stx.isNatLit?.getD 0 | `expr => pure $ unsafeCast $ stx.getArg 0 -- HACK: see below diff --git a/stage0/src/Init/Lean/Elab/Term.lean b/stage0/src/Init/Lean/Elab/Term.lean index 668cf712a8..82fd7702f7 100644 --- a/stage0/src/Init/Lean/Elab/Term.lean +++ b/stage0/src/Init/Lean/Elab/Term.lean @@ -292,7 +292,7 @@ def expandCDot? : Syntax → TermElabM (Option Syntax) if args.any hasCDot then do (args, binders) ← (expandCDotArgs args).run #[]; let newNode := Syntax.node k args; - result ← `(fun %%binders* => %%newNode); + result ← `(fun $binders* => $newNode); pure result else pure none @@ -513,7 +513,7 @@ partial def expandFunBindersAux (binders : Array Syntax) : Syntax → Nat → Ar ident ← mkFreshAnonymousIdent binder; (binders, newBody) ← expandFunBindersAux body (i+1) (newBinders.push $ mkExplicitBinder ident mkHole); let major := mkTermIdFromIdent ident; - newBody ← `(match %%major with | %%pattern => %%newBody); + newBody ← `(match $major with | $pattern => $newBody); pure (binders, newBody) }; match binder with @@ -582,7 +582,7 @@ partial def mkPairsAux (elems : Array Syntax) : Nat → Syntax → TermElabM Syn if i > 0 then do let i := i - 1; let elem := elems.get! i; - acc ← `(Prod.mk %%elem %%acc); + acc ← `(Prod.mk $elem $acc); mkPairsAux i acc else pure acc @@ -601,13 +601,13 @@ fun stx expectedType? => let ref := stx.val; match_syntax ref with | `(()) => pure $ Lean.mkConst `Unit.unit - | `((%%e : %%type)) => do + | `(($e : $type)) => do type ← elabType type; e ← elabCDot e expectedType?; eType ← inferType ref e; ensureHasType ref type eType e - | `((%%e)) => elabCDot e expectedType? - | `((%%e, %%es*)) => do + | `(($e)) => elabCDot e expectedType? + | `(($e, $es*)) => do pairs ← mkPairs (#[e] ++ es.getEvenElems); withMacroExpansion stx.val (elabTerm pairs expectedType?) | _ => throwError stx.val "unexpected parentheses notation" diff --git a/stage0/src/Init/Lean/Parser/Term.lean b/stage0/src/Init/Lean/Parser/Term.lean index 3f223d2f62..d346f2e753 100644 --- a/stage0/src/Init/Lean/Parser/Term.lean +++ b/stage0/src/Init/Lean/Parser/Term.lean @@ -40,11 +40,13 @@ pushLeading >> unicodeSymbol sym asciiSym lbp >> termParser lbp def infixL (sym : String) (lbp : Nat) : TrailingParser := pushLeading >> symbol sym lbp >> termParser lbp --- Define parser for `%%e` (if name = none) or `%%e:n` (if name = some n). Both +def dollarSymbol {k : ParserKind} : Parser k := symbol "$" 1 + +-- Define parser for `$e` (if name = none) or `$e:n` (if name = some n). Both -- forms can also be used with an appended `*` to turn them into an -- antiquotation "splice". def mkAntiquot (name : Option String) : Parser leading := -leadingNode `Lean.Parser.Term.antiquot $ symbol "$" 1 >> checkNoWsBefore "no space before" >> termParser appPrec >> ( +leadingNode `Lean.Parser.Term.antiquot $ dollarSymbol >> checkNoWsBefore "no space before" >> termParser appPrec >> ( match name with | some name => let sym := ":" ++ name; checkNoWsBefore ("no space before '" ++ sym ++ "'") >> sym -- make sure to generate as many children (1) as in the first case to keep arity constant @@ -140,7 +142,7 @@ def checkIsSort := checkLeading (fun leading => leading.isOfKind `Lean.Parser.Te @[builtinTermParser] def arrow := tparser! unicodeInfixR " → " " -> " 25 @[builtinTermParser] def arrayRef := tparser! pushLeading >> symbolNoWs "[" (appPrec+1) >> termParser >>"]" -@[builtinTermParser] def dollar := tparser! try (pushLeading >> symbol " $ " 1 >> checkWsBefore "space expected") >> termParser 0 +@[builtinTermParser] def dollar := tparser! try (pushLeading >> dollarSymbol >> checkWsBefore "space expected") >> termParser 0 @[builtinTermParser] def fcomp := tparser! infixR " ∘ " 90 @[builtinTermParser] def prod := tparser! infixR " × " 35 diff --git a/stage0/stdlib/Init/Lean/Parser/Term.c b/stage0/stdlib/Init/Lean/Parser/Term.c index 53aca2b2cd..6c537261c1 100644 --- a/stage0/stdlib/Init/Lean/Parser/Term.c +++ b/stage0/stdlib/Init/Lean/Parser/Term.c @@ -81,8 +81,10 @@ lean_object* l_Lean_Parser_Term_haveAssign___elambda__1(lean_object*); lean_object* l_Lean_Parser_Term_structInstField___elambda__1(lean_object*); lean_object* l_Lean_Parser_Term_optIdent___closed__3; lean_object* l_Lean_Parser_Term_lt___elambda__1(lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Parser_Term_dollarSymbol___elambda__1___rarg(lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_mkAntiquot___closed__7; lean_object* l_Lean_Parser_Term_andthen___elambda__1___closed__4; +lean_object* l_Lean_Parser_Term_dollarSymbol___elambda__1___rarg___closed__2; lean_object* l_Lean_Parser_Term_binderTactic___elambda__1___rarg___closed__2; lean_object* l_Lean_Parser_Term_have___elambda__1___rarg___closed__3; lean_object* l_Lean_Parser_andthenInfo(lean_object*, lean_object*); @@ -94,7 +96,6 @@ lean_object* l_Lean_Parser_ParserState_mkError(lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_optType___closed__2; lean_object* l_Lean_Parser_Term_mkAntiquot___elambda__2(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_tupleTail___elambda__1___spec__2(uint8_t, uint8_t, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__12; lean_object* l_Lean_Parser_Term_binderType___elambda__1___boxed(lean_object*); lean_object* l_Lean_Parser_Term_borrowed___closed__4; lean_object* l_Lean_Parser_Term_bracktedBinder(uint8_t); @@ -109,7 +110,6 @@ lean_object* l_Lean_Parser_Term_matchAlt___closed__3; lean_object* l_Lean_Parser_Term_inaccessible___closed__2; lean_object* l_Lean_Parser_Term_structInst___closed__1; lean_object* l_Lean_Parser_Term_andM___elambda__1(lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__15; lean_object* l_Lean_Parser_Term_proj; lean_object* l_Lean_Parser_Term_dollar___elambda__1(lean_object*, lean_object*, lean_object*); extern lean_object* l_addParenHeuristic___closed__2; @@ -123,7 +123,6 @@ lean_object* l_Lean_Parser_Term_doId___elambda__1___rarg(lean_object*, lean_obje lean_object* l_Lean_Parser_Term_band; lean_object* l_Lean_Parser_Term_sub___elambda__1___closed__2; lean_object* l_Lean_Parser_Term_bnot___elambda__1___rarg___closed__2; -lean_object* l_Lean_Parser_Term_dollar___elambda__1___closed__5; lean_object* l_Lean_Parser_Term_le; extern lean_object* l_Lean_nullKind; lean_object* l_Lean_Parser_Term_instBinder; @@ -149,7 +148,6 @@ lean_object* l___regBuiltinParser_Lean_Parser_Term_explicit(lean_object*); lean_object* l_Lean_Parser_Term_type___closed__3; lean_object* l_Lean_Parser_Term_subtype___closed__6; lean_object* l___regBuiltinParser_Lean_Parser_Term_append(lean_object*); -lean_object* l_Lean_Parser_Term_dollar___elambda__1___closed__6; lean_object* l_Lean_Parser_Term_haveAssign___closed__2; lean_object* l_Lean_Parser_Term_forall___elambda__1(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_prop___elambda__1___rarg___closed__3; @@ -252,12 +250,14 @@ lean_object* l_Lean_Parser_Term_mkAntiquot___closed__12; lean_object* l_Lean_Parser_Term_heq___elambda__1___closed__5; lean_object* l_Lean_Parser_Term_namedPattern___closed__3; lean_object* l_Lean_Parser_Term_sortApp___closed__1; +lean_object* l_Lean_Parser_Term_dollarSymbol___elambda__1___rarg___closed__5; extern lean_object* l_Sigma_HasRepr___rarg___closed__1; lean_object* l_Lean_Parser_Term_listLit___closed__1; lean_object* l___regBuiltinParser_Lean_Parser_Term_emptyC(lean_object*); lean_object* l_Lean_Parser_Term_quotedName___closed__3; lean_object* l_Lean_Parser_Term_listLit___elambda__1___closed__10; lean_object* l_Lean_Parser_Term_seq___elambda__1___closed__4; +lean_object* l_Lean_Parser_Term_dollarSymbol___elambda__1___rarg___closed__3; lean_object* l_Lean_Parser_Term_bnot___elambda__1___rarg___closed__5; lean_object* l_Lean_Parser_Term_sortApp___closed__2; lean_object* l___regBuiltinParser_Lean_Parser_Term_quotedName(lean_object*); @@ -491,6 +491,7 @@ lean_object* l_Lean_Parser_Term_bor___closed__1; lean_object* l_Lean_Parser_Term_match___elambda__1___closed__7; lean_object* l_Lean_Parser_Term_doElem___closed__5; extern lean_object* l_Lean_Parser_ident___closed__1; +lean_object* l_Lean_Parser_Term_dollarSymbol___elambda__1___boxed(lean_object*, lean_object*); lean_object* lean_nat_add(lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_suffices___elambda__1___rarg___closed__5; lean_object* l_Lean_Parser_Term_inaccessible; @@ -724,7 +725,6 @@ lean_object* l_Array_shrink___main___rarg(lean_object*, lean_object*); extern lean_object* l_Lean_getBuiltinSearchPath___closed__1; lean_object* l_Lean_Parser_Term_letPatDecl___elambda__1___boxed(lean_object*); lean_object* l___regBuiltinParser_Lean_Parser_Term_dollar(lean_object*); -lean_object* l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__14; lean_object* l_Lean_Parser_Term_explicitUniv___closed__5; lean_object* l_Lean_Parser_Term_let___closed__6; lean_object* l_Lean_Parser_Term_lt___closed__2; @@ -921,7 +921,6 @@ lean_object* l_Lean_Parser_Term_arrayRef___elambda__1(lean_object*, lean_object* lean_object* l_Lean_Parser_Term_stxQuot___elambda__1___rarg___closed__7; lean_object* l_Lean_Parser_Term_orM___elambda__1___closed__2; lean_object* l___regBuiltinParser_Lean_Parser_Term_anonymousCtor(lean_object*); -lean_object* l_Lean_Parser_Term_mkAntiquot___closed__17; lean_object* l_Lean_Parser_Term_lt___closed__1; lean_object* l_Lean_Parser_Term_bindOp___closed__1; lean_object* l_Lean_Parser_Term_seq; @@ -953,6 +952,7 @@ lean_object* l_Lean_Parser_Term_fun___elambda__1___closed__1; lean_object* l_Lean_Parser_Term_namedPattern___closed__6; lean_object* l_Lean_Parser_Term_match__syntax___elambda__1(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_modN___closed__2; +lean_object* l_Lean_Parser_Term_dollarSymbol___closed__1; lean_object* l_Lean_Parser_Term_prop___elambda__1___rarg(lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_depArrow___closed__5; lean_object* l_Lean_Parser_Term_have___elambda__1___rarg___closed__2; @@ -1074,6 +1074,7 @@ lean_object* l_Lean_Parser_ParserState_restore(lean_object*, lean_object*, lean_ lean_object* l_Lean_Parser_Term_arrayRef___elambda__1___closed__1; extern lean_object* l_Lean_formatEntry___closed__1; lean_object* l_Lean_Parser_Term_tparser_x21___elambda__1___rarg___closed__5; +lean_object* l_Lean_Parser_Term_dollarSymbol___boxed(lean_object*); lean_object* l___regBuiltinParser_Lean_Parser_Term_have(lean_object*); lean_object* l_Lean_Parser_Term_structInstSource___closed__5; lean_object* l_Lean_Parser_Term_haveAssign___elambda__1___rarg___closed__4; @@ -1150,6 +1151,7 @@ lean_object* l_Lean_Parser_Term_le___elambda__1___closed__1; lean_object* l_Lean_Parser_Term_forall___elambda__1___closed__10; lean_object* l_Lean_Parser_Term_cons___closed__1; lean_object* l_Lean_Parser_Term_bnot___elambda__1___boxed(lean_object*); +lean_object* l_Lean_Parser_Term_dollarSymbol___closed__2; lean_object* l_Lean_Parser_Term_heq___elambda__1___closed__2; lean_object* l_Lean_Parser_Term_if___elambda__1(lean_object*); lean_object* l_Lean_Parser_Term_explicitBinder___closed__6; @@ -1293,7 +1295,6 @@ lean_object* l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__4; lean_object* l_Lean_Parser_mergeOrElseErrors(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_sorry___elambda__1___rarg___closed__5; lean_object* l_Lean_Parser_Term_prod___closed__1; -lean_object* l_Lean_Parser_Term_dollar___elambda__1___closed__7; lean_object* l_Lean_Parser_Term_subst___closed__3; extern lean_object* l_Lean_Parser_Level_paren___elambda__1___rarg___closed__3; lean_object* l_Lean_Parser_Term_arrayLit___closed__5; @@ -1387,6 +1388,7 @@ lean_object* l_Lean_Parser_Term_tupleTail___closed__5; lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Term_match__syntax___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_mapRev___elambda__1___closed__2; lean_object* l_Lean_Parser_Term_suffices___elambda__1___rarg(lean_object*, lean_object*); +lean_object* l_Lean_Parser_Term_dollarSymbol(uint8_t); lean_object* l_Lean_Parser_Term_id___closed__7; lean_object* l_Lean_Parser_Term_str___closed__1; lean_object* l___regBuiltinParser_Lean_Parser_Term_and(lean_object*); @@ -1616,6 +1618,7 @@ lean_object* l_Lean_Parser_identFn___rarg(lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_structInstField___closed__3; lean_object* l_Lean_Parser_Term_mkAntiquot___closed__13; lean_object* l_Lean_Parser_Term_depArrow___elambda__1___closed__12; +lean_object* l_Lean_Parser_Term_dollarSymbol___elambda__1___rarg___closed__4; lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Term_explicitUniv___elambda__1___spec__1(uint8_t, uint8_t, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_quotedName___elambda__1___rarg___closed__4; lean_object* l_Lean_Parser_Term_seqRight___elambda__1(lean_object*, lean_object*, lean_object*); @@ -1648,9 +1651,7 @@ lean_object* l_Lean_Parser_Term_beq___closed__2; lean_object* l_Lean_Parser_Term_arrayLit___closed__2; lean_object* l_Lean_Parser_Term_ne___elambda__1___closed__4; lean_object* l_Lean_Parser_Term_paren___elambda__1(lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_Parser_Term_dollar___elambda__1___closed__8; lean_object* l_Lean_Parser_Term_arrayLit___closed__1; -lean_object* l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__11; lean_object* l_Lean_Parser_Term_stxQuot___closed__1; lean_object* l_Lean_Parser_Term_nomatch___closed__5; lean_object* l_Lean_Parser_Term_beq___closed__1; @@ -1679,13 +1680,13 @@ lean_object* l_Lean_Parser_Term_not___elambda__1___rarg___closed__7; lean_object* l_Lean_Parser_Term_borrowed___closed__2; lean_object* l_Lean_Parser_Term_mapRev___elambda__1___closed__4; lean_object* l_Lean_Parser_Term_bindOp___elambda__1___closed__1; -lean_object* l_Lean_Parser_Term_dollar___elambda__1___closed__4; lean_object* l_Lean_Parser_Term_suffices; lean_object* l_Lean_Parser_Term_mapConstRev; lean_object* l_Lean_Parser_Term_iff; lean_object* l_Lean_Parser_Term_iff___elambda__1___closed__5; lean_object* l_Lean_Parser_many1Fn___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_letIdLhs; +lean_object* l_Lean_Parser_Term_dollarSymbol___elambda__1(uint8_t, lean_object*); lean_object* l_Lean_Parser_Term_subtype___closed__8; lean_object* l_Lean_Parser_Term_num___elambda__1(lean_object*); lean_object* l_Lean_Parser_Term_fun___elambda__1___closed__18; @@ -1757,6 +1758,7 @@ lean_object* l_Lean_Parser_regBuiltinTermParserAttr___closed__2; lean_object* l_Lean_Parser_Term_if___closed__7; lean_object* l_Lean_Parser_Term_match___closed__10; lean_object* l_Lean_Parser_Term_namedPattern___elambda__1___boxed(lean_object*); +lean_object* l_Lean_Parser_Term_dollarSymbol___elambda__1___rarg___closed__1; lean_object* l_Lean_Parser_Term_suffices___elambda__1___rarg___closed__1; lean_object* l_Lean_Parser_Term_modN___elambda__1___closed__2; lean_object* l_Lean_Parser_Term_if___elambda__1___rarg(lean_object*, lean_object*); @@ -1780,7 +1782,6 @@ lean_object* l_Lean_Parser_Term_arrow___closed__3; lean_object* l_Lean_Parser_Term_arrayLit___elambda__1___closed__2; lean_object* l_Lean_Parser_Term_anonymousCtor___elambda__1___closed__6; lean_object* l_Lean_Parser_Term_type___elambda__1___rarg___closed__4; -lean_object* l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__13; lean_object* l_Lean_Parser_Term_fromTerm___elambda__1(lean_object*); lean_object* l_Lean_Parser_Term_andM___elambda__1___closed__4; lean_object* l_Lean_Parser_Term_stxQuot___closed__4; @@ -2256,6 +2257,175 @@ lean_dec(x_1); return x_3; } } +lean_object* _init_l_Lean_Parser_Term_dollarSymbol___elambda__1___rarg___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("$"); +return x_1; +} +} +lean_object* _init_l_Lean_Parser_Term_dollarSymbol___elambda__1___rarg___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_Parser_Term_dollarSymbol___elambda__1___rarg___closed__1; +x_2 = l_String_trim(x_1); +return x_2; +} +} +lean_object* _init_l_Lean_Parser_Term_dollarSymbol___elambda__1___rarg___closed__3() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Char_HasRepr___closed__1; +x_2 = l_Lean_Parser_Term_dollarSymbol___elambda__1___rarg___closed__2; +x_3 = lean_string_append(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Term_dollarSymbol___elambda__1___rarg___closed__4() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Term_dollarSymbol___elambda__1___rarg___closed__3; +x_2 = l_Char_HasRepr___closed__1; +x_3 = lean_string_append(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Term_dollarSymbol___elambda__1___rarg___closed__5() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = lean_box(0); +x_2 = l_Lean_Parser_Term_dollarSymbol___elambda__1___rarg___closed__4; +x_3 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_3, 0, x_2); +lean_ctor_set(x_3, 1, x_1); +return x_3; +} +} +lean_object* l_Lean_Parser_Term_dollarSymbol___elambda__1___rarg(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; lean_object* x_4; lean_object* x_5; +x_3 = lean_ctor_get(x_2, 1); +lean_inc(x_3); +x_4 = l_Lean_Parser_tokenFn(x_1, x_2); +x_5 = lean_ctor_get(x_4, 3); +lean_inc(x_5); +if (lean_obj_tag(x_5) == 0) +{ +lean_object* x_6; lean_object* x_7; +x_6 = lean_ctor_get(x_4, 0); +lean_inc(x_6); +x_7 = l_Array_back___at___private_Init_Lean_Parser_Parser_6__updateCache___spec__1(x_6); +lean_dec(x_6); +if (lean_obj_tag(x_7) == 2) +{ +lean_object* x_8; lean_object* x_9; uint8_t x_10; +x_8 = lean_ctor_get(x_7, 1); +lean_inc(x_8); +lean_dec(x_7); +x_9 = l_Lean_Parser_Term_dollarSymbol___elambda__1___rarg___closed__2; +x_10 = lean_string_dec_eq(x_8, x_9); +lean_dec(x_8); +if (x_10 == 0) +{ +lean_object* x_11; lean_object* x_12; +x_11 = l_Lean_Parser_Term_dollarSymbol___elambda__1___rarg___closed__5; +x_12 = l_Lean_Parser_ParserState_mkErrorsAt(x_4, x_11, x_3); +return x_12; +} +else +{ +lean_dec(x_3); +return x_4; +} +} +else +{ +lean_object* x_13; lean_object* x_14; +lean_dec(x_7); +x_13 = l_Lean_Parser_Term_dollarSymbol___elambda__1___rarg___closed__5; +x_14 = l_Lean_Parser_ParserState_mkErrorsAt(x_4, x_13, x_3); +return x_14; +} +} +else +{ +lean_object* x_15; lean_object* x_16; +lean_dec(x_5); +x_15 = l_Lean_Parser_Term_dollarSymbol___elambda__1___rarg___closed__5; +x_16 = l_Lean_Parser_ParserState_mkErrorsAt(x_4, x_15, x_3); +return x_16; +} +} +} +lean_object* l_Lean_Parser_Term_dollarSymbol___elambda__1(uint8_t x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; +x_3 = lean_alloc_closure((void*)(l_Lean_Parser_Term_dollarSymbol___elambda__1___rarg), 2, 0); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Term_dollarSymbol___closed__1() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = lean_unsigned_to_nat(1u); +x_2 = lean_alloc_ctor(1, 1, 0); +lean_ctor_set(x_2, 0, x_1); +return x_2; +} +} +lean_object* _init_l_Lean_Parser_Term_dollarSymbol___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Term_dollarSymbol___elambda__1___rarg___closed__2; +x_2 = l_Lean_Parser_Term_dollarSymbol___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); +return x_3; +} +} +lean_object* l_Lean_Parser_Term_dollarSymbol(uint8_t x_1) { +_start: +{ +lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; +x_2 = lean_box(x_1); +x_3 = lean_alloc_closure((void*)(l_Lean_Parser_Term_dollarSymbol___elambda__1___boxed), 2, 1); +lean_closure_set(x_3, 0, x_2); +x_4 = l_Lean_Parser_Term_dollarSymbol___closed__2; +x_5 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_5, 0, x_4); +lean_ctor_set(x_5, 1, x_3); +return x_5; +} +} +lean_object* l_Lean_Parser_Term_dollarSymbol___elambda__1___boxed(lean_object* x_1, lean_object* x_2) { +_start: +{ +uint8_t x_3; lean_object* x_4; +x_3 = lean_unbox(x_1); +lean_dec(x_1); +x_4 = l_Lean_Parser_Term_dollarSymbol___elambda__1(x_3, x_2); +lean_dec(x_2); +return x_4; +} +} +lean_object* l_Lean_Parser_Term_dollarSymbol___boxed(lean_object* x_1) { +_start: +{ +uint8_t x_2; lean_object* x_3; +x_2 = lean_unbox(x_1); +lean_dec(x_1); +x_3 = l_Lean_Parser_Term_dollarSymbol(x_2); +return x_3; +} +} lean_object* _init_l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__1() { _start: { @@ -2296,7 +2466,7 @@ lean_object* _init_l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__5 _start: { lean_object* x_1; -x_1 = lean_mk_string("$"); +x_1 = lean_mk_string("*"); return x_1; } } @@ -2313,60 +2483,11 @@ lean_object* _init_l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__7 _start: { lean_object* x_1; -x_1 = lean_mk_string("*"); -return x_1; -} -} -lean_object* _init_l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__8() { -_start: -{ -lean_object* x_1; lean_object* x_2; -x_1 = l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__7; -x_2 = l_String_trim(x_1); -return x_2; -} -} -lean_object* _init_l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__9() { -_start: -{ -lean_object* x_1; x_1 = lean_mk_string("no space before"); return x_1; } } -lean_object* _init_l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__10() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Char_HasRepr___closed__1; -x_2 = l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__8; -x_3 = lean_string_append(x_1, x_2); -return x_3; -} -} -lean_object* _init_l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__11() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__10; -x_2 = l_Char_HasRepr___closed__1; -x_3 = lean_string_append(x_1, x_2); -return x_3; -} -} -lean_object* _init_l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__12() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__11; -x_3 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_3, 0, x_2); -lean_ctor_set(x_3, 1, x_1); -return x_3; -} -} -lean_object* _init_l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__13() { +lean_object* _init_l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__8() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; @@ -2376,22 +2497,22 @@ x_3 = lean_string_append(x_1, x_2); return x_3; } } -lean_object* _init_l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__14() { +lean_object* _init_l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__9() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__13; +x_1 = l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__8; x_2 = l_Char_HasRepr___closed__1; x_3 = lean_string_append(x_1, x_2); return x_3; } } -lean_object* _init_l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__15() { +lean_object* _init_l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__10() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = lean_box(0); -x_2 = l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__14; +x_2 = l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__9; x_3 = lean_alloc_ctor(1, 2, 0); lean_ctor_set(x_3, 0, x_2); lean_ctor_set(x_3, 1, x_1); @@ -2401,76 +2522,19 @@ return x_3; lean_object* l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg(lean_object* x_1, lean_object* x_2) { _start: { -lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_59; lean_object* x_60; lean_object* x_61; +lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; x_3 = lean_ctor_get(x_2, 0); lean_inc(x_3); x_4 = lean_array_get_size(x_3); lean_dec(x_3); -x_59 = lean_ctor_get(x_2, 1); -lean_inc(x_59); lean_inc(x_1); -x_60 = l_Lean_Parser_tokenFn(x_1, x_2); -x_61 = lean_ctor_get(x_60, 3); -lean_inc(x_61); -if (lean_obj_tag(x_61) == 0) -{ -lean_object* x_62; lean_object* x_63; -x_62 = lean_ctor_get(x_60, 0); -lean_inc(x_62); -x_63 = l_Array_back___at___private_Init_Lean_Parser_Parser_6__updateCache___spec__1(x_62); -lean_dec(x_62); -if (lean_obj_tag(x_63) == 2) -{ -lean_object* x_64; lean_object* x_65; uint8_t x_66; -x_64 = lean_ctor_get(x_63, 1); -lean_inc(x_64); -lean_dec(x_63); -x_65 = l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__6; -x_66 = lean_string_dec_eq(x_64, x_65); -lean_dec(x_64); -if (x_66 == 0) -{ -lean_object* x_67; lean_object* x_68; -x_67 = l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__15; -x_68 = l_Lean_Parser_ParserState_mkErrorsAt(x_60, x_67, x_59); -x_5 = x_68; -goto block_58; -} -else -{ -lean_dec(x_59); -x_5 = x_60; -goto block_58; -} -} -else -{ -lean_object* x_69; lean_object* x_70; -lean_dec(x_63); -x_69 = l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__15; -x_70 = l_Lean_Parser_ParserState_mkErrorsAt(x_60, x_69, x_59); -x_5 = x_70; -goto block_58; -} -} -else -{ -lean_object* x_71; lean_object* x_72; -lean_dec(x_61); -x_71 = l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__15; -x_72 = l_Lean_Parser_ParserState_mkErrorsAt(x_60, x_71, x_59); -x_5 = x_72; -goto block_58; -} -block_58: -{ -lean_object* x_6; +x_5 = l_Lean_Parser_Term_dollarSymbol___elambda__1___rarg(x_1, x_2); x_6 = lean_ctor_get(x_5, 3); lean_inc(x_6); if (lean_obj_tag(x_6) == 0) { lean_object* x_7; lean_object* x_8; lean_object* x_9; -x_7 = l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__9; +x_7 = l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__7; x_8 = l_Lean_Parser_checkNoWsBeforeFn(x_7, x_1, x_5); x_9 = lean_ctor_get(x_8, 3); lean_inc(x_9); @@ -2519,13 +2583,13 @@ lean_object* x_41; lean_object* x_42; uint8_t x_43; x_41 = lean_ctor_get(x_40, 1); lean_inc(x_41); lean_dec(x_40); -x_42 = l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__8; +x_42 = l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__6; x_43 = lean_string_dec_eq(x_41, x_42); lean_dec(x_41); if (x_43 == 0) { lean_object* x_44; lean_object* x_45; -x_44 = l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__12; +x_44 = l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__10; lean_inc(x_21); x_45 = l_Lean_Parser_ParserState_mkErrorsAt(x_37, x_44, x_21); x_22 = x_45; @@ -2541,7 +2605,7 @@ else { lean_object* x_46; lean_object* x_47; lean_dec(x_40); -x_46 = l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__12; +x_46 = l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__10; lean_inc(x_21); x_47 = l_Lean_Parser_ParserState_mkErrorsAt(x_37, x_46, x_21); x_22 = x_47; @@ -2552,7 +2616,7 @@ else { lean_object* x_48; lean_object* x_49; lean_dec(x_38); -x_48 = l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__12; +x_48 = l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__10; lean_inc(x_21); x_49 = l_Lean_Parser_ParserState_mkErrorsAt(x_37, x_48, x_21); x_22 = x_49; @@ -2642,7 +2706,6 @@ return x_57; } } } -} lean_object* l_Lean_Parser_Term_mkAntiquot___elambda__1(lean_object* x_1) { _start: { @@ -2678,10 +2741,9 @@ return x_6; lean_object* _init_l_Lean_Parser_Term_mkAntiquot___closed__1() { _start: { -lean_object* x_1; lean_object* x_2; -x_1 = lean_unsigned_to_nat(1u); -x_2 = lean_alloc_ctor(1, 1, 0); -lean_ctor_set(x_2, 0, x_1); +uint8_t x_1; lean_object* x_2; +x_1 = 0; +x_2 = l_Lean_Parser_Term_dollarSymbol(x_1); return x_2; } } @@ -2689,9 +2751,9 @@ lean_object* _init_l_Lean_Parser_Term_mkAntiquot___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__6; -x_2 = l_Lean_Parser_Term_mkAntiquot___closed__1; -x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); +x_1 = lean_box(0); +x_2 = l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__6; +x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); return x_3; } } @@ -2708,30 +2770,30 @@ return x_2; lean_object* _init_l_Lean_Parser_Term_mkAntiquot___closed__4() { _start: { -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__8; -x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); -return x_3; +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_Parser_Term_mkAntiquot___closed__2; +x_2 = l_Lean_Parser_optionaInfo(x_1); +return x_2; } } lean_object* _init_l_Lean_Parser_Term_mkAntiquot___closed__5() { _start: { -lean_object* x_1; lean_object* x_2; -x_1 = l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__8; -x_2 = lean_alloc_closure((void*)(l_Lean_Parser_symbolFn___rarg___boxed), 4, 1); -lean_closure_set(x_2, 0, x_1); -return x_2; +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_epsilonInfo; +x_2 = l_Lean_Parser_Term_mkAntiquot___closed__4; +x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); +return x_3; } } lean_object* _init_l_Lean_Parser_Term_mkAntiquot___closed__6() { _start: { -lean_object* x_1; lean_object* x_2; -x_1 = l_Lean_Parser_Term_mkAntiquot___closed__4; -x_2 = l_Lean_Parser_optionaInfo(x_1); -return x_2; +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Parser_inhabited___closed__1; +x_2 = l_Lean_Parser_Term_mkAntiquot___closed__5; +x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); +return x_3; } } lean_object* _init_l_Lean_Parser_Term_mkAntiquot___closed__7() { @@ -2747,44 +2809,26 @@ return x_3; lean_object* _init_l_Lean_Parser_Term_mkAntiquot___closed__8() { _start: { -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Parser_inhabited___closed__1; -x_2 = l_Lean_Parser_Term_mkAntiquot___closed__7; -x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); -return x_3; +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; +x_1 = l_Lean_Parser_Term_mkAntiquot___closed__1; +x_2 = lean_ctor_get(x_1, 0); +lean_inc(x_2); +x_3 = l_Lean_Parser_Term_mkAntiquot___closed__7; +x_4 = l_Lean_Parser_andthenInfo(x_2, x_3); +return x_4; } } lean_object* _init_l_Lean_Parser_Term_mkAntiquot___closed__9() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_epsilonInfo; -x_2 = l_Lean_Parser_Term_mkAntiquot___closed__8; -x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); -return x_3; -} -} -lean_object* _init_l_Lean_Parser_Term_mkAntiquot___closed__10() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Term_mkAntiquot___closed__2; -x_2 = l_Lean_Parser_Term_mkAntiquot___closed__9; -x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); -return x_3; -} -} -lean_object* _init_l_Lean_Parser_Term_mkAntiquot___closed__11() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__4; -x_2 = l_Lean_Parser_Term_mkAntiquot___closed__10; +x_2 = l_Lean_Parser_Term_mkAntiquot___closed__8; x_3 = l_Lean_Parser_nodeInfo(x_1, x_2); return x_3; } } -lean_object* _init_l_Lean_Parser_Term_mkAntiquot___closed__12() { +lean_object* _init_l_Lean_Parser_Term_mkAntiquot___closed__10() { _start: { lean_object* x_1; @@ -2792,39 +2836,50 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Term_mkAntiquot___elambda__1___bo return x_1; } } -lean_object* _init_l_Lean_Parser_Term_mkAntiquot___closed__13() { +lean_object* _init_l_Lean_Parser_Term_mkAntiquot___closed__11() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Term_mkAntiquot___closed__11; -x_2 = l_Lean_Parser_Term_mkAntiquot___closed__12; +x_1 = l_Lean_Parser_Term_mkAntiquot___closed__9; +x_2 = l_Lean_Parser_Term_mkAntiquot___closed__10; x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); lean_ctor_set(x_3, 1, x_2); return x_3; } } -lean_object* _init_l_Lean_Parser_Term_mkAntiquot___closed__14() { +lean_object* _init_l_Lean_Parser_Term_mkAntiquot___closed__12() { _start: { lean_object* x_1; lean_object* x_2; -x_1 = l_Lean_Parser_Term_mkAntiquot___closed__5; +x_1 = l_Lean_Parser_Term_mkAntiquot___closed__3; x_2 = lean_alloc_closure((void*)(l_Lean_Parser_optionalFn___rarg), 4, 1); lean_closure_set(x_2, 0, x_1); return x_2; } } -lean_object* _init_l_Lean_Parser_Term_mkAntiquot___closed__15() { +lean_object* _init_l_Lean_Parser_Term_mkAntiquot___closed__13() { _start: { lean_object* x_1; lean_object* x_2; -x_1 = l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__9; +x_1 = l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__7; x_2 = lean_alloc_closure((void*)(l_Lean_Parser_checkNoWsBefore___elambda__1___rarg___boxed), 4, 1); lean_closure_set(x_2, 0, x_1); return x_2; } } -lean_object* _init_l_Lean_Parser_Term_mkAntiquot___closed__16() { +lean_object* _init_l_Lean_Parser_Term_mkAntiquot___closed__14() { +_start: +{ +uint8_t x_1; lean_object* x_2; lean_object* x_3; +x_1 = 0; +x_2 = lean_box(x_1); +x_3 = lean_alloc_closure((void*)(l_Lean_Parser_Term_dollarSymbol___elambda__1___boxed), 2, 1); +lean_closure_set(x_3, 0, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Term_mkAntiquot___closed__15() { _start: { lean_object* x_1; @@ -2832,7 +2887,7 @@ x_1 = lean_mk_string("no space before '"); return x_1; } } -lean_object* _init_l_Lean_Parser_Term_mkAntiquot___closed__17() { +lean_object* _init_l_Lean_Parser_Term_mkAntiquot___closed__16() { _start: { lean_object* x_1; @@ -2846,64 +2901,66 @@ _start: if (lean_obj_tag(x_1) == 0) { lean_object* x_2; -x_2 = l_Lean_Parser_Term_mkAntiquot___closed__13; +x_2 = l_Lean_Parser_Term_mkAntiquot___closed__11; return x_2; } else { -lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; +lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; x_3 = lean_ctor_get(x_1, 0); x_4 = lean_box(0); -x_5 = l___private_Init_Util_1__mkPanicMessage___closed__2; -x_6 = lean_string_append(x_5, x_3); -x_7 = l_Lean_Parser_Term_mkAntiquot___closed__16; -x_8 = lean_string_append(x_7, x_6); -x_9 = l_Char_HasRepr___closed__1; -x_10 = lean_string_append(x_8, x_9); -x_11 = l_String_trim(x_6); -lean_dec(x_6); -lean_inc(x_11); -x_12 = l_Lean_Parser_symbolInfo(x_11, x_4); -x_13 = lean_alloc_closure((void*)(l_Lean_Parser_symbolFn___rarg___boxed), 4, 1); -lean_closure_set(x_13, 0, x_11); -x_14 = l_Lean_Parser_epsilonInfo; -x_15 = l_Lean_Parser_andthenInfo(x_14, x_12); -x_16 = lean_alloc_closure((void*)(l_Lean_Parser_checkNoWsBefore___elambda__1___rarg___boxed), 4, 1); -lean_closure_set(x_16, 0, x_10); -x_17 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn___rarg), 5, 2); -lean_closure_set(x_17, 0, x_16); -lean_closure_set(x_17, 1, x_13); -x_18 = l_Lean_Parser_Term_mkAntiquot___closed__6; -x_19 = l_Lean_Parser_andthenInfo(x_15, x_18); -x_20 = l_Lean_Parser_Term_mkAntiquot___closed__14; -x_21 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn___rarg), 5, 2); -lean_closure_set(x_21, 0, x_17); -lean_closure_set(x_21, 1, x_20); -x_22 = l_Lean_Parser_Parser_inhabited___closed__1; -x_23 = l_Lean_Parser_andthenInfo(x_22, x_19); -x_24 = l_Lean_Parser_Term_mkAntiquot___closed__17; -x_25 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn___rarg), 5, 2); -lean_closure_set(x_25, 0, x_24); -lean_closure_set(x_25, 1, x_21); -x_26 = l_Lean_Parser_andthenInfo(x_14, x_23); -x_27 = l_Lean_Parser_Term_mkAntiquot___closed__15; -x_28 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn___rarg), 5, 2); -lean_closure_set(x_28, 0, x_27); -lean_closure_set(x_28, 1, x_25); -x_29 = l_Lean_Parser_Term_mkAntiquot___closed__2; -x_30 = l_Lean_Parser_andthenInfo(x_29, x_26); -x_31 = l_Lean_Parser_Term_mkAntiquot___closed__3; -x_32 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn___rarg), 5, 2); -lean_closure_set(x_32, 0, x_31); -lean_closure_set(x_32, 1, x_28); -x_33 = l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__4; -x_34 = l_Lean_Parser_nodeInfo(x_33, x_30); -x_35 = lean_alloc_closure((void*)(l_Lean_Parser_Term_mkAntiquot___elambda__2), 4, 1); -lean_closure_set(x_35, 0, x_32); -x_36 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_36, 0, x_34); -lean_ctor_set(x_36, 1, x_35); -return x_36; +x_5 = l_Lean_Parser_Term_mkAntiquot___closed__1; +x_6 = lean_ctor_get(x_5, 0); +lean_inc(x_6); +x_7 = l___private_Init_Util_1__mkPanicMessage___closed__2; +x_8 = lean_string_append(x_7, x_3); +x_9 = l_Lean_Parser_Term_mkAntiquot___closed__15; +x_10 = lean_string_append(x_9, x_8); +x_11 = l_Char_HasRepr___closed__1; +x_12 = lean_string_append(x_10, x_11); +x_13 = l_String_trim(x_8); +lean_dec(x_8); +lean_inc(x_13); +x_14 = l_Lean_Parser_symbolInfo(x_13, x_4); +x_15 = lean_alloc_closure((void*)(l_Lean_Parser_symbolFn___rarg___boxed), 4, 1); +lean_closure_set(x_15, 0, x_13); +x_16 = l_Lean_Parser_epsilonInfo; +x_17 = l_Lean_Parser_andthenInfo(x_16, x_14); +x_18 = lean_alloc_closure((void*)(l_Lean_Parser_checkNoWsBefore___elambda__1___rarg___boxed), 4, 1); +lean_closure_set(x_18, 0, x_12); +x_19 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn___rarg), 5, 2); +lean_closure_set(x_19, 0, x_18); +lean_closure_set(x_19, 1, x_15); +x_20 = l_Lean_Parser_Term_mkAntiquot___closed__4; +x_21 = l_Lean_Parser_andthenInfo(x_17, x_20); +x_22 = l_Lean_Parser_Term_mkAntiquot___closed__12; +x_23 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn___rarg), 5, 2); +lean_closure_set(x_23, 0, x_19); +lean_closure_set(x_23, 1, x_22); +x_24 = l_Lean_Parser_Parser_inhabited___closed__1; +x_25 = l_Lean_Parser_andthenInfo(x_24, x_21); +x_26 = l_Lean_Parser_Term_mkAntiquot___closed__16; +x_27 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn___rarg), 5, 2); +lean_closure_set(x_27, 0, x_26); +lean_closure_set(x_27, 1, x_23); +x_28 = l_Lean_Parser_andthenInfo(x_16, x_25); +x_29 = l_Lean_Parser_Term_mkAntiquot___closed__13; +x_30 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn___rarg), 5, 2); +lean_closure_set(x_30, 0, x_29); +lean_closure_set(x_30, 1, x_27); +x_31 = l_Lean_Parser_andthenInfo(x_6, x_28); +x_32 = l_Lean_Parser_Term_mkAntiquot___closed__14; +x_33 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn___rarg), 5, 2); +lean_closure_set(x_33, 0, x_32); +lean_closure_set(x_33, 1, x_30); +x_34 = l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__4; +x_35 = l_Lean_Parser_nodeInfo(x_34, x_31); +x_36 = lean_alloc_closure((void*)(l_Lean_Parser_Term_mkAntiquot___elambda__2), 4, 1); +lean_closure_set(x_36, 0, x_33); +x_37 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_37, 0, x_35); +lean_ctor_set(x_37, 1, x_36); +return x_37; } } } @@ -26488,55 +26545,6 @@ lean_object* _init_l_Lean_Parser_Term_dollar___elambda__1___closed__3() { _start: { lean_object* x_1; -x_1 = lean_mk_string(" $ "); -return x_1; -} -} -lean_object* _init_l_Lean_Parser_Term_dollar___elambda__1___closed__4() { -_start: -{ -lean_object* x_1; lean_object* x_2; -x_1 = l_Lean_Parser_Term_dollar___elambda__1___closed__3; -x_2 = l_String_trim(x_1); -return x_2; -} -} -lean_object* _init_l_Lean_Parser_Term_dollar___elambda__1___closed__5() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Char_HasRepr___closed__1; -x_2 = l_Lean_Parser_Term_dollar___elambda__1___closed__4; -x_3 = lean_string_append(x_1, x_2); -return x_3; -} -} -lean_object* _init_l_Lean_Parser_Term_dollar___elambda__1___closed__6() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Term_dollar___elambda__1___closed__5; -x_2 = l_Char_HasRepr___closed__1; -x_3 = lean_string_append(x_1, x_2); -return x_3; -} -} -lean_object* _init_l_Lean_Parser_Term_dollar___elambda__1___closed__7() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Term_dollar___elambda__1___closed__6; -x_3 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_3, 0, x_2); -lean_ctor_set(x_3, 1, x_1); -return x_3; -} -} -lean_object* _init_l_Lean_Parser_Term_dollar___elambda__1___closed__8() { -_start: -{ -lean_object* x_1; x_1 = lean_mk_string("space expected"); return x_1; } @@ -26544,7 +26552,7 @@ return x_1; lean_object* l_Lean_Parser_Term_dollar___elambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { -lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_29; +lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_25; x_4 = lean_ctor_get(x_3, 0); lean_inc(x_4); x_5 = lean_ctor_get(x_3, 1); @@ -26553,130 +26561,108 @@ x_6 = lean_ctor_get(x_3, 3); lean_inc(x_6); x_7 = lean_array_get_size(x_4); lean_dec(x_4); -x_29 = l_Lean_Parser_ParserState_pushSyntax(x_3, x_1); +x_25 = l_Lean_Parser_ParserState_pushSyntax(x_3, x_1); if (lean_obj_tag(x_6) == 0) { -lean_object* x_30; lean_object* x_31; +lean_object* x_26; lean_object* x_27; lean_inc(x_2); -x_30 = l_Lean_Parser_tokenFn(x_2, x_29); -x_31 = lean_ctor_get(x_30, 3); +x_26 = l_Lean_Parser_Term_dollarSymbol___elambda__1___rarg(x_2, x_25); +x_27 = lean_ctor_get(x_26, 3); +lean_inc(x_27); +if (lean_obj_tag(x_27) == 0) +{ +lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; +x_28 = l_Lean_Parser_Term_dollar___elambda__1___closed__3; +x_29 = l_Lean_Parser_checkWsBeforeFn(x_28, x_2, x_26); +x_30 = lean_ctor_get(x_29, 0); +lean_inc(x_30); +x_31 = lean_ctor_get(x_29, 2); lean_inc(x_31); -if (lean_obj_tag(x_31) == 0) -{ -lean_object* x_32; lean_object* x_33; -x_32 = lean_ctor_get(x_30, 0); +x_32 = lean_ctor_get(x_29, 3); lean_inc(x_32); -x_33 = l_Array_back___at___private_Init_Lean_Parser_Parser_6__updateCache___spec__1(x_32); -lean_dec(x_32); -if (lean_obj_tag(x_33) == 2) -{ -lean_object* x_34; lean_object* x_35; uint8_t x_36; -x_34 = lean_ctor_get(x_33, 1); -lean_inc(x_34); -lean_dec(x_33); -x_35 = l_Lean_Parser_Term_dollar___elambda__1___closed__4; -x_36 = lean_string_dec_eq(x_34, x_35); -lean_dec(x_34); -if (x_36 == 0) -{ -lean_object* x_37; lean_object* x_38; -x_37 = l_Lean_Parser_Term_dollar___elambda__1___closed__7; -lean_inc(x_5); -x_38 = l_Lean_Parser_ParserState_mkErrorsAt(x_30, x_37, x_5); -x_8 = x_38; -goto block_28; -} -else -{ -lean_object* x_39; lean_object* x_40; -x_39 = l_Lean_Parser_Term_dollar___elambda__1___closed__8; -x_40 = l_Lean_Parser_checkWsBeforeFn(x_39, x_2, x_30); -x_8 = x_40; -goto block_28; -} -} -else -{ -lean_object* x_41; lean_object* x_42; -lean_dec(x_33); -x_41 = l_Lean_Parser_Term_dollar___elambda__1___closed__7; -lean_inc(x_5); -x_42 = l_Lean_Parser_ParserState_mkErrorsAt(x_30, x_41, x_5); -x_8 = x_42; -goto block_28; -} -} -else -{ -lean_object* x_43; lean_object* x_44; -lean_dec(x_31); -x_43 = l_Lean_Parser_Term_dollar___elambda__1___closed__7; -lean_inc(x_5); -x_44 = l_Lean_Parser_ParserState_mkErrorsAt(x_30, x_43, x_5); -x_8 = x_44; -goto block_28; -} -} -else -{ -lean_dec(x_6); x_8 = x_29; -goto block_28; +x_9 = x_30; +x_10 = x_31; +x_11 = x_32; +goto block_24; } -block_28: +else { -lean_object* x_9; -x_9 = lean_ctor_get(x_8, 3); -lean_inc(x_9); -if (lean_obj_tag(x_9) == 0) +lean_object* x_33; lean_object* x_34; lean_object* x_35; +lean_dec(x_27); +x_33 = lean_ctor_get(x_26, 0); +lean_inc(x_33); +x_34 = lean_ctor_get(x_26, 2); +lean_inc(x_34); +x_35 = lean_ctor_get(x_26, 3); +lean_inc(x_35); +x_8 = x_26; +x_9 = x_33; +x_10 = x_34; +x_11 = x_35; +goto block_24; +} +} +else { -lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; +lean_object* x_36; lean_object* x_37; lean_object* x_38; +lean_dec(x_6); +x_36 = lean_ctor_get(x_25, 0); +lean_inc(x_36); +x_37 = lean_ctor_get(x_25, 2); +lean_inc(x_37); +x_38 = lean_ctor_get(x_25, 3); +lean_inc(x_38); +x_8 = x_25; +x_9 = x_36; +x_10 = x_37; +x_11 = x_38; +goto block_24; +} +block_24: +{ +if (lean_obj_tag(x_11) == 0) +{ +lean_object* x_12; +lean_dec(x_10); +lean_dec(x_9); lean_dec(x_5); -x_10 = l_Lean_Parser_termParserAttribute; -x_11 = lean_unsigned_to_nat(0u); -x_12 = l_Lean_Parser_ParserAttribute_runParser(x_10, x_11, x_2, x_8); -x_13 = l_Lean_Parser_Term_dollar___elambda__1___closed__2; -x_14 = l_Lean_Parser_ParserState_mkNode(x_12, x_13, x_7); -return x_14; +x_12 = lean_ctor_get(x_8, 3); +lean_inc(x_12); +if (lean_obj_tag(x_12) == 0) +{ +lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; +x_13 = l_Lean_Parser_termParserAttribute; +x_14 = lean_unsigned_to_nat(0u); +x_15 = l_Lean_Parser_ParserAttribute_runParser(x_13, x_14, x_2, x_8); +x_16 = l_Lean_Parser_Term_dollar___elambda__1___closed__2; +x_17 = l_Lean_Parser_ParserState_mkNode(x_15, x_16, x_7); +return x_17; } else { -uint8_t x_15; +lean_object* x_18; lean_object* x_19; +lean_dec(x_12); lean_dec(x_2); -x_15 = !lean_is_exclusive(x_8); -if (x_15 == 0) -{ -lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; -x_16 = lean_ctor_get(x_8, 0); -x_17 = lean_ctor_get(x_8, 3); -lean_dec(x_17); -x_18 = lean_ctor_get(x_8, 1); -lean_dec(x_18); -x_19 = l_Array_shrink___main___rarg(x_16, x_7); -lean_ctor_set(x_8, 1, x_5); -lean_ctor_set(x_8, 0, x_19); -x_20 = l_Lean_Parser_Term_dollar___elambda__1___closed__2; -x_21 = l_Lean_Parser_ParserState_mkNode(x_8, x_20, x_7); -return x_21; +x_18 = l_Lean_Parser_Term_dollar___elambda__1___closed__2; +x_19 = l_Lean_Parser_ParserState_mkNode(x_8, x_18, x_7); +return x_19; +} } else { -lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; -x_22 = lean_ctor_get(x_8, 0); -x_23 = lean_ctor_get(x_8, 2); -lean_inc(x_23); -lean_inc(x_22); +lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_dec(x_8); -x_24 = l_Array_shrink___main___rarg(x_22, x_7); -x_25 = lean_alloc_ctor(0, 4, 0); -lean_ctor_set(x_25, 0, x_24); -lean_ctor_set(x_25, 1, x_5); -lean_ctor_set(x_25, 2, x_23); -lean_ctor_set(x_25, 3, x_9); -x_26 = l_Lean_Parser_Term_dollar___elambda__1___closed__2; -x_27 = l_Lean_Parser_ParserState_mkNode(x_25, x_26, x_7); -return x_27; -} +lean_dec(x_2); +x_20 = l_Array_shrink___main___rarg(x_9, x_7); +x_21 = lean_alloc_ctor(0, 4, 0); +lean_ctor_set(x_21, 0, x_20); +lean_ctor_set(x_21, 1, x_5); +lean_ctor_set(x_21, 2, x_10); +lean_ctor_set(x_21, 3, x_11); +x_22 = l_Lean_Parser_Term_dollar___elambda__1___closed__2; +x_23 = l_Lean_Parser_ParserState_mkNode(x_21, x_22, x_7); +return x_23; } } } @@ -26684,21 +26670,22 @@ return x_27; lean_object* _init_l_Lean_Parser_Term_dollar___closed__1() { _start: { -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Term_dollar___elambda__1___closed__4; -x_2 = l_Lean_Parser_Term_mkAntiquot___closed__1; -x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); -return x_3; +uint8_t x_1; lean_object* x_2; +x_1 = 1; +x_2 = l_Lean_Parser_Term_dollarSymbol(x_1); +return x_2; } } lean_object* _init_l_Lean_Parser_Term_dollar___closed__2() { _start: { -lean_object* x_1; lean_object* x_2; lean_object* x_3; +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; x_1 = l_Lean_Parser_Term_dollar___closed__1; -x_2 = l_Lean_Parser_epsilonInfo; -x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); -return x_3; +x_2 = lean_ctor_get(x_1, 0); +lean_inc(x_2); +x_3 = l_Lean_Parser_epsilonInfo; +x_4 = l_Lean_Parser_andthenInfo(x_2, x_3); +return x_4; } } lean_object* _init_l_Lean_Parser_Term_dollar___closed__3() { @@ -30993,6 +30980,20 @@ if (lean_io_result_is_error(res)) return res; l_Lean_Parser_termParserAttribute = lean_io_result_get_value(res); lean_mark_persistent(l_Lean_Parser_termParserAttribute); lean_dec_ref(res); +l_Lean_Parser_Term_dollarSymbol___elambda__1___rarg___closed__1 = _init_l_Lean_Parser_Term_dollarSymbol___elambda__1___rarg___closed__1(); +lean_mark_persistent(l_Lean_Parser_Term_dollarSymbol___elambda__1___rarg___closed__1); +l_Lean_Parser_Term_dollarSymbol___elambda__1___rarg___closed__2 = _init_l_Lean_Parser_Term_dollarSymbol___elambda__1___rarg___closed__2(); +lean_mark_persistent(l_Lean_Parser_Term_dollarSymbol___elambda__1___rarg___closed__2); +l_Lean_Parser_Term_dollarSymbol___elambda__1___rarg___closed__3 = _init_l_Lean_Parser_Term_dollarSymbol___elambda__1___rarg___closed__3(); +lean_mark_persistent(l_Lean_Parser_Term_dollarSymbol___elambda__1___rarg___closed__3); +l_Lean_Parser_Term_dollarSymbol___elambda__1___rarg___closed__4 = _init_l_Lean_Parser_Term_dollarSymbol___elambda__1___rarg___closed__4(); +lean_mark_persistent(l_Lean_Parser_Term_dollarSymbol___elambda__1___rarg___closed__4); +l_Lean_Parser_Term_dollarSymbol___elambda__1___rarg___closed__5 = _init_l_Lean_Parser_Term_dollarSymbol___elambda__1___rarg___closed__5(); +lean_mark_persistent(l_Lean_Parser_Term_dollarSymbol___elambda__1___rarg___closed__5); +l_Lean_Parser_Term_dollarSymbol___closed__1 = _init_l_Lean_Parser_Term_dollarSymbol___closed__1(); +lean_mark_persistent(l_Lean_Parser_Term_dollarSymbol___closed__1); +l_Lean_Parser_Term_dollarSymbol___closed__2 = _init_l_Lean_Parser_Term_dollarSymbol___closed__2(); +lean_mark_persistent(l_Lean_Parser_Term_dollarSymbol___closed__2); l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__1 = _init_l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__1(); lean_mark_persistent(l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__1); l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__2 = _init_l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__2(); @@ -31013,16 +31014,6 @@ l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__9 = _init_l_Lean_Par lean_mark_persistent(l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__9); l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__10 = _init_l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__10(); lean_mark_persistent(l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__10); -l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__11 = _init_l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__11(); -lean_mark_persistent(l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__11); -l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__12 = _init_l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__12(); -lean_mark_persistent(l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__12); -l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__13 = _init_l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__13(); -lean_mark_persistent(l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__13); -l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__14 = _init_l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__14(); -lean_mark_persistent(l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__14); -l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__15 = _init_l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__15(); -lean_mark_persistent(l_Lean_Parser_Term_mkAntiquot___elambda__1___rarg___closed__15); l_Lean_Parser_Term_mkAntiquot___closed__1 = _init_l_Lean_Parser_Term_mkAntiquot___closed__1(); lean_mark_persistent(l_Lean_Parser_Term_mkAntiquot___closed__1); l_Lean_Parser_Term_mkAntiquot___closed__2 = _init_l_Lean_Parser_Term_mkAntiquot___closed__2(); @@ -31055,8 +31046,6 @@ l_Lean_Parser_Term_mkAntiquot___closed__15 = _init_l_Lean_Parser_Term_mkAntiquot lean_mark_persistent(l_Lean_Parser_Term_mkAntiquot___closed__15); l_Lean_Parser_Term_mkAntiquot___closed__16 = _init_l_Lean_Parser_Term_mkAntiquot___closed__16(); lean_mark_persistent(l_Lean_Parser_Term_mkAntiquot___closed__16); -l_Lean_Parser_Term_mkAntiquot___closed__17 = _init_l_Lean_Parser_Term_mkAntiquot___closed__17(); -lean_mark_persistent(l_Lean_Parser_Term_mkAntiquot___closed__17); l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_explicitUniv___elambda__1___spec__2___closed__1 = _init_l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_explicitUniv___elambda__1___spec__2___closed__1(); lean_mark_persistent(l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_explicitUniv___elambda__1___spec__2___closed__1); l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_explicitUniv___elambda__1___spec__2___closed__2 = _init_l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_explicitUniv___elambda__1___spec__2___closed__2(); @@ -33076,16 +33065,6 @@ l_Lean_Parser_Term_dollar___elambda__1___closed__2 = _init_l_Lean_Parser_Term_do lean_mark_persistent(l_Lean_Parser_Term_dollar___elambda__1___closed__2); l_Lean_Parser_Term_dollar___elambda__1___closed__3 = _init_l_Lean_Parser_Term_dollar___elambda__1___closed__3(); lean_mark_persistent(l_Lean_Parser_Term_dollar___elambda__1___closed__3); -l_Lean_Parser_Term_dollar___elambda__1___closed__4 = _init_l_Lean_Parser_Term_dollar___elambda__1___closed__4(); -lean_mark_persistent(l_Lean_Parser_Term_dollar___elambda__1___closed__4); -l_Lean_Parser_Term_dollar___elambda__1___closed__5 = _init_l_Lean_Parser_Term_dollar___elambda__1___closed__5(); -lean_mark_persistent(l_Lean_Parser_Term_dollar___elambda__1___closed__5); -l_Lean_Parser_Term_dollar___elambda__1___closed__6 = _init_l_Lean_Parser_Term_dollar___elambda__1___closed__6(); -lean_mark_persistent(l_Lean_Parser_Term_dollar___elambda__1___closed__6); -l_Lean_Parser_Term_dollar___elambda__1___closed__7 = _init_l_Lean_Parser_Term_dollar___elambda__1___closed__7(); -lean_mark_persistent(l_Lean_Parser_Term_dollar___elambda__1___closed__7); -l_Lean_Parser_Term_dollar___elambda__1___closed__8 = _init_l_Lean_Parser_Term_dollar___elambda__1___closed__8(); -lean_mark_persistent(l_Lean_Parser_Term_dollar___elambda__1___closed__8); l_Lean_Parser_Term_dollar___closed__1 = _init_l_Lean_Parser_Term_dollar___closed__1(); lean_mark_persistent(l_Lean_Parser_Term_dollar___closed__1); l_Lean_Parser_Term_dollar___closed__2 = _init_l_Lean_Parser_Term_dollar___closed__2();