From d7f27a140ebc8cf7990719f2a183ffddb317e47d Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 4 Dec 2020 17:23:30 +0100 Subject: [PATCH] feat: antiquotation scopes --- src/Lean/Elab/Quotation.lean | 68 ++++++++++++++++++----- src/Lean/Parser/Basic.lean | 50 ++++++----------- src/Lean/Parser/Extra.lean | 44 ++++++++++++++- src/Lean/PrettyPrinter/Formatter.lean | 22 ++++---- src/Lean/PrettyPrinter/Parenthesizer.lean | 24 ++++---- tests/lean/StxQuot.lean | 7 +++ tests/lean/StxQuot.lean.expected.out | 3 + 7 files changed, 147 insertions(+), 71 deletions(-) diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean index 9f36accbc7..d999e399a8 100644 --- a/src/Lean/Elab/Quotation.lean +++ b/src/Lean/Elab/Quotation.lean @@ -28,10 +28,11 @@ def mkAntiquotNode (term : Syntax) (nesting := 0) (name : Option String := none) | false => mkNullNode mkNode (kind ++ `antiquot) #[mkAtom "$", nesting, term, name, splice] --- Antiquotations can be escaped as in `$$x`, which is useful for nesting macros. +-- Antiquotations can be escaped as in `$$x`, which is useful for nesting macros. Also works for antiquotation scopes. def isEscapedAntiquot (stx : Syntax) : Bool := !stx[1].getArgs.isEmpty +-- Also works for antiquotation scopes. def unescapeAntiquot (stx : Syntax) : Syntax := if isAntiquot stx then stx.setArg 1 $ mkNullNode stx[1].getArgs.pop @@ -57,11 +58,36 @@ def antiquotKind? : Syntax → Option SyntaxNodeKind def isAntiquotSplice (stx : Syntax) : Bool := isAntiquot stx && stx[4].getOptional?.isSome +-- An "antiquotation scope" is something like `$[...]?` or `$[...]*`. Note that the latter could be of kind `many` or +-- `sepBy`, which have different implementations. +def antiquotScopeKind? : Syntax → Option SyntaxNodeKind + | Syntax.node (Name.str k "antiquot_scope" _) args => some k + | _ => none + +def isAntiquotScope (stx : Syntax) : Bool := + antiquotScopeKind? stx |>.isSome + +def getAntiquotScopeContents (stx : Syntax) : Array Syntax := + stx[3].getArgs + +def getAntiquotScopeSuffix (stx : Syntax) : Syntax := + stx[5] + -- If any item of a `many` node is an antiquotation splice, its result should -- be substituted into the `many` node's children def isAntiquotSplicePat (stx : Syntax) : Bool := stx.isOfKind nullKind && stx.getArgs.any fun arg => isAntiquotSplice arg && !isEscapedAntiquot arg +partial def getAntiquotationIds : Syntax → TermElabM (List Syntax) + | stx@(Syntax.node k args) => + if isAntiquot stx && !isEscapedAntiquot stx then + let anti := getAntiquotTerm stx + if anti.isIdent then [anti] + else throwErrorAt stx "complex antiquotation not allowed here" + else + List.join <$> args.toList.mapM getAntiquotationIds + | _ => [] + -- Elaborate the content of a syntax quotation term private partial def quoteSyntax : Syntax → TermElabM Syntax | Syntax.ident info rawVal val preresolved => do @@ -78,6 +104,8 @@ private partial def quoteSyntax : Syntax → TermElabM Syntax -- splices must occur in a `many` node if isAntiquotSplice stx then throwErrorAt stx "unexpected antiquotation splice" else pure $ getAntiquotTerm stx + else if isAntiquotScope stx && !isEscapedAntiquot stx then + throwErrorAt stx "unexpected antiquotation splice" else let empty ← `(Array.empty); -- if escaped antiquotation, decrement by one escape level @@ -86,6 +114,28 @@ private partial def quoteSyntax : Syntax → TermElabM Syntax if k == nullKind && isAntiquotSplice arg then -- antiquotation splice pattern: inject args array `(Array.appendCore $args $(getAntiquotTerm arg)) + else if k == nullKind && isAntiquotScope arg then do + let k := antiquotScopeKind? arg + let inner ← (getAntiquotScopeContents arg).mapM quoteSyntax + let arr ← match (← getAntiquotationIds arg) with + | [] => throwErrorAt stx "antiquotation scope must contain at least one antiquotation" + | [id] => match k with + | `optional => `(match $id:ident with + | some $id:ident => $(quote inner) + | none => #[]) + | _ => `(Array.map (fun $id => $(inner[0])) $id) + | [id1, id2] => match k with + | `optional => `(match $id1:ident, $id2:ident with + | some $id1:ident, some $id2:ident => $(quote inner) + | _ => #[]) + | _ => `(Array.zipWith $id1 $id2 fun $id1 $id2 => $(inner[0])) + | _ => throwErrorAt stx "too many antiquotations in antiquotation scope; don't be greedy" + let arr ← + if k == `sepBy then + let Syntax.atom _ sep ← (getAntiquotScopeSuffix arg)[0] | unreachable! + `(mkSepArray $arr (mkAtom $(Syntax.mkStrLit sep))) + else arr + `(Array.appendCore $args $arr) else do let arg ← quoteSyntax arg; `(Array.push $args $arg)) empty @@ -246,21 +296,11 @@ private partial def compileStxMatch : List Syntax → List Alt → TermElabM Syn `(let discr := $discr; ite (Eq $cond true) $yes $no) | _, _ => unreachable! -private partial def getPatternVarsAux : Syntax → List Syntax - | stx@(Syntax.node k args) => - if isAntiquot stx && !isEscapedAntiquot stx then - let anti := getAntiquotTerm stx - if anti.isIdent then [anti] - else [] - else - List.join $ args.toList.map getPatternVarsAux - | _ => [] - -- Get all pattern vars (as `Syntax.ident`s) in `stx` -partial def getPatternVars (stx : Syntax) : List Syntax := +partial def getPatternVars (stx : Syntax) : TermElabM (List Syntax) := if isQuot stx then do let quoted := stx.getArg 1; - getPatternVarsAux stx + getAntiquotationIds stx else if stx.isIdent then [stx] else [] @@ -270,7 +310,7 @@ partial def getPatternVars (stx : Syntax) : List Syntax := private def letBindRhss (cont : List Alt → TermElabM Syntax) : List Alt → List Alt → TermElabM Syntax | [], altsRev' => cont altsRev'.reverse | (pats, rhs)::alts, altsRev' => do - let vars := List.join $ pats.map getPatternVars + let vars ← List.join <$> pats.mapM getPatternVars match vars with -- no antiquotations => introduce Unit parameter to preserve evaluation order | [] => diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean index 9ee3072be7..afb7a2b54b 100644 --- a/src/Lean/Parser/Basic.lean +++ b/src/Lean/Parser/Basic.lean @@ -515,7 +515,7 @@ def optionalFn (p : ParserFn) : ParserFn := fun c s => firstTokens := p.firstTokens.toOptional } -@[inline] def optional (p : Parser) : Parser := { +@[inline] def optionalNoAntiquot (p : Parser) : Parser := { info := optionaInfo p.info, fn := optionalFn p.fn } @@ -559,7 +559,7 @@ partial def manyAux (p : ParserFn) : ParserFn := fun c s => let s := manyAux p c s s.mkNode nullKind iniSz -@[inline] def many (p : Parser) : Parser := { +@[inline] def manyNoAntiquot (p : Parser) : Parser := { info := noFirstTokenInfo p.info, fn := manyFn p.fn } @@ -569,7 +569,7 @@ partial def manyAux (p : ParserFn) : ParserFn := fun c s => let s := andthenFn p (manyAux p) c s s.mkNode nullKind iniSz -@[inline] def many1 (p : Parser) : Parser := { +@[inline] def many1NoAntiquot (p : Parser) : Parser := { info := p.info, fn := many1Fn p.fn } @@ -618,12 +618,12 @@ def sepBy1Fn (allowTrailingSep : Bool) (p : ParserFn) (sep : ParserFn) : ParserF firstTokens := p.firstTokens } -@[inline] def sepBy (p sep : Parser) (allowTrailingSep : Bool := false) : Parser := { +@[inline] def sepByNoAntiquot (p sep : Parser) (allowTrailingSep : Bool := false) : Parser := { info := sepByInfo p.info sep.info, fn := sepByFn allowTrailingSep p.fn sep.fn } -@[inline] def sepBy1 (p sep : Parser) (allowTrailingSep : Bool := false) : Parser := { +@[inline] def sepBy1NoAntiquot (p sep : Parser) (allowTrailingSep : Bool := false) : Parser := { info := sepBy1Info p.info sep.info, fn := sepBy1Fn allowTrailingSep p.fn sep.fn } @@ -647,7 +647,7 @@ def withResultOfFn (p : ParserFn) (f : Syntax → Syntax) : ParserFn := fun c s } @[inline] def many1Unbox (p : Parser) : Parser := - withResultOf (many1 p) fun stx => if stx.getNumArgs == 1 then stx.getArg 0 else stx + withResultOf (many1NoAntiquot p) fun stx => if stx.getNumArgs == 1 then stx.getArg 0 else stx partial def satisfyFn (p : Char → Bool) (errorMsg : String := "unexpected character") : ParserFn := fun c s => let i := s.pos @@ -1603,10 +1603,10 @@ def mkAntiquot (name : String) (kind : Option SyntaxNodeKind) (anonymous := true -- antiquotations are not part of the "standard" syntax, so hide "expected '$'" on error leadingNode kind maxPrec $ atomic $ setExpected [] "$" >> - many (checkNoWsBefore "" >> "$") >> + manyNoAntiquot (checkNoWsBefore "" >> "$") >> checkNoWsBefore "no space before spliced term" >> antiquotExpr >> nameP >> - optional (checkNoWsBefore "" >> symbol "*") + optionalNoAntiquot (checkNoWsBefore "" >> symbol "*") def tryAnti (c : ParserContext) (s : ParserState) : Bool := let (s, stx?) := peekToken c s @@ -1623,34 +1623,20 @@ def tryAnti (c : ParserContext) (s : ParserState) : Bool := info := orelseInfo antiquotP.info p.info } -/- ===================== -/ -/- End of Antiquotations -/ -/- ===================== -/ +def mkAntiquotScope (kind : SyntaxNodeKind) (p suffix : Parser) : Parser := + let kind := kind ++ `antiquot_scope + leadingNode kind maxPrec $ atomic $ + setExpected [] "$" >> + manyNoAntiquot (checkNoWsBefore "" >> "$") >> + checkNoWsBefore "no space before spliced term" >> symbol "[" >> node nullKind p >> symbol "]" >> + suffix def nodeWithAntiquot (name : String) (kind : SyntaxNodeKind) (p : Parser) (anonymous := false) : Parser := withAntiquot (mkAntiquot name kind anonymous) $ node kind p -def ident : Parser := - withAntiquot (mkAntiquot "ident" identKind) identNoAntiquot - --- `ident` and `rawIdent` produce the same syntax tree, so we reuse the antiquotation kind name -def rawIdent : Parser := - withAntiquot (mkAntiquot "ident" identKind) rawIdentNoAntiquot - -def numLit : Parser := - withAntiquot (mkAntiquot "numLit" numLitKind) numLitNoAntiquot - -def scientificLit : Parser := - withAntiquot (mkAntiquot "scientificLit" scientificLitKind) scientificLitNoAntiquot - -def strLit : Parser := - withAntiquot (mkAntiquot "strLit" strLitKind) strLitNoAntiquot - -def charLit : Parser := - withAntiquot (mkAntiquot "charLit" charLitKind) charLitNoAntiquot - -def nameLit : Parser := - withAntiquot (mkAntiquot "nameLit" nameLitKind) nameLitNoAntiquot +/- ===================== -/ +/- End of Antiquotations -/ +/- ===================== -/ def categoryParserOfStackFn (offset : Nat) : ParserFn := fun ctx s => let stack := s.stxStack diff --git a/src/Lean/Parser/Extra.lean b/src/Lean/Parser/Extra.lean index 2d053f4e45..d68163acd7 100644 --- a/src/Lean/Parser/Extra.lean +++ b/src/Lean/Parser/Extra.lean @@ -14,8 +14,48 @@ namespace Parser -- synthesize pretty printers for parsers declared prior to `Lean.PrettyPrinter` -- (because `Parser.Extension` depends on them) attribute [runBuiltinParserAttributeHooks] - leadingNode termParser commandParser antiquotNestedExpr antiquotExpr mkAntiquot nodeWithAntiquot - ident numLit scientificLit charLit strLit nameLit + leadingNode termParser commandParser mkAntiquot nodeWithAntiquot + +@[runBuiltinParserAttributeHooks] def optional (p : Parser) : Parser := + optionalNoAntiquot (withAntiquot (mkAntiquotScope `optional p (symbol "?")) p) + +@[runBuiltinParserAttributeHooks] def many (p : Parser) : Parser := + manyNoAntiquot (withAntiquot (mkAntiquotScope `many p (symbol "*")) p) + +@[runBuiltinParserAttributeHooks] def many1 (p : Parser) : Parser := + many1NoAntiquot (withAntiquot (mkAntiquotScope `many p (symbol "*")) p) + +-- all the separators you could ever want +@[runBuiltinParserAttributeHooks] def sepByScopeSuffixes : Parser := +parser! (symbol "," <|> symbol ";" <|> symbol "|") >> symbol "*" + +@[runBuiltinParserAttributeHooks] def sepBy (p psep : Parser) (allowTrailingSep : Bool := false) : Parser := + sepByNoAntiquot (withAntiquot (mkAntiquotScope `sepBy p sepByScopeSuffixes) p) psep allowTrailingSep + +@[runBuiltinParserAttributeHooks] def sepBy1 (p psep : Parser) (allowTrailingSep : Bool := false) : Parser := + sepBy1NoAntiquot (withAntiquot (mkAntiquotScope `sepBy p sepByScopeSuffixes) p) psep allowTrailingSep + +@[runBuiltinParserAttributeHooks] def ident : Parser := + withAntiquot (mkAntiquot "ident" identKind) identNoAntiquot + +-- `ident` and `rawIdent` produce the same syntax tree, so we reuse the antiquotation kind name +@[runBuiltinParserAttributeHooks] def rawIdent : Parser := + withAntiquot (mkAntiquot "ident" identKind) rawIdentNoAntiquot + +@[runBuiltinParserAttributeHooks] def numLit : Parser := + withAntiquot (mkAntiquot "numLit" numLitKind) numLitNoAntiquot + +@[runBuiltinParserAttributeHooks] def scientificLit : Parser := + withAntiquot (mkAntiquot "scientificLit" scientificLitKind) scientificLitNoAntiquot + +@[runBuiltinParserAttributeHooks] def strLit : Parser := + withAntiquot (mkAntiquot "strLit" strLitKind) strLitNoAntiquot + +@[runBuiltinParserAttributeHooks] def charLit : Parser := + withAntiquot (mkAntiquot "charLit" charLitKind) charLitNoAntiquot + +@[runBuiltinParserAttributeHooks] def nameLit : Parser := + withAntiquot (mkAntiquot "nameLit" nameLitKind) nameLitNoAntiquot @[runBuiltinParserAttributeHooks, inline] def group (p : Parser) : Parser := node nullKind p diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean index 228e4428ad..bddd0ab738 100644 --- a/src/Lean/PrettyPrinter/Formatter.lean +++ b/src/Lean/PrettyPrinter/Formatter.lean @@ -337,14 +337,14 @@ def identNoAntiquot.formatter : Formatter := do pushToken info id.toString goLeft -@[combinatorFormatter Lean.Parser.rawIdent] def rawIdent.formatter : Formatter := do +@[combinatorFormatter Lean.Parser.rawIdentNoAntiquot] def rawIdentNoAntiquot.formatter : Formatter := do checkKind identKind let Syntax.ident info _ id _ ← getCur | throwError m!"not an ident: {← getCur}" pushToken info id.toString goLeft -@[combinatorFormatter Lean.Parser.identEq] def identEq.formatter (id : Name) := rawIdent.formatter +@[combinatorFormatter Lean.Parser.identEq] def identEq.formatter (id : Name) := rawIdentNoAntiquot.formatter def visitAtom (k : SyntaxNodeKind) : Formatter := do let stx ← getCur @@ -362,30 +362,30 @@ def visitAtom (k : SyntaxNodeKind) : Formatter := do @[combinatorFormatter Lean.Parser.scientificLitNoAntiquot] def scientificLitNoAntiquot.formatter := visitAtom scientificLitKind @[combinatorFormatter Lean.Parser.fieldIdx] def fieldIdx.formatter := visitAtom fieldIdxKind -@[combinatorFormatter Lean.Parser.many] -def many.formatter (p : Formatter) : Formatter := do +@[combinatorFormatter Lean.Parser.manyNoAntiquot] +def manyNoAntiquot.formatter (p : Formatter) : Formatter := do let stx ← getCur visitArgs $ stx.getArgs.size.forM fun _ => p -@[combinatorFormatter Lean.Parser.many1] def many1.formatter (p : Formatter) : Formatter := many.formatter p +@[combinatorFormatter Lean.Parser.many1NoAntiquot] def many1NoAntiquot.formatter (p : Formatter) : Formatter := manyNoAntiquot.formatter p -@[combinatorFormatter Lean.Parser.optional] -def optional.formatter (p : Formatter) : Formatter := visitArgs p +@[combinatorFormatter Lean.Parser.optionalNoAntiquot] +def optionalNoAntiquot.formatter (p : Formatter) : Formatter := visitArgs p @[combinatorFormatter Lean.Parser.many1Unbox] def many1Unbox.formatter (p : Formatter) : Formatter := do let stx ← getCur if stx.getKind == nullKind then do - many.formatter p + manyNoAntiquot.formatter p else p -@[combinatorFormatter Lean.Parser.sepBy] -def sepBy.formatter (p pSep : Formatter) : Formatter := do +@[combinatorFormatter Lean.Parser.sepByNoAntiquot] +def sepByNoAntiquot.formatter (p pSep : Formatter) : Formatter := do let stx ← getCur visitArgs $ (List.range stx.getArgs.size).reverse.forM $ fun i => if i % 2 == 0 then p else pSep -@[combinatorFormatter Lean.Parser.sepBy1] def sepBy1.formatter := sepBy.formatter +@[combinatorFormatter Lean.Parser.sepBy1NoAntiquot] def sepBy1NoAntiquot.formatter := sepByNoAntiquot.formatter @[combinatorFormatter Lean.Parser.withPosition] def withPosition.formatter (p : Formatter) : Formatter := p @[combinatorFormatter Lean.Parser.withoutPosition] def withoutPosition.formatter (p : Formatter) : Formatter := p diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean index 23025f8635..a87f484bee 100644 --- a/src/Lean/PrettyPrinter/Parenthesizer.lean +++ b/src/Lean/PrettyPrinter/Parenthesizer.lean @@ -405,7 +405,7 @@ def trailingNode.parenthesizer (k : SyntaxNodeKind) (prec : Nat) (p : Parenthesi @[combinatorParenthesizer Lean.Parser.unicodeSymbol] def unicodeSymbol.parenthesizer (sym asciiSym : String) := visitToken @[combinatorParenthesizer Lean.Parser.identNoAntiquot] def identNoAntiquot.parenthesizer := visitToken -@[combinatorParenthesizer Lean.Parser.rawIdent] def rawIdent.parenthesizer := visitToken +@[combinatorParenthesizer Lean.Parser.rawIdentNoAntiquot] def rawIdentNoAntiquot.parenthesizer := visitToken @[combinatorParenthesizer Lean.Parser.identEq] def identEq.parenthesizer (id : Name) := visitToken @[combinatorParenthesizer Lean.Parser.nonReservedSymbol] def nonReservedSymbol.parenthesizer (sym : String) (includeIdent : Bool) := visitToken @@ -416,33 +416,33 @@ def trailingNode.parenthesizer (k : SyntaxNodeKind) (prec : Nat) (p : Parenthesi @[combinatorParenthesizer Lean.Parser.scientificLitNoAntiquot] def scientificLitNoAntiquot.parenthesizer := visitToken @[combinatorParenthesizer Lean.Parser.fieldIdx] def fieldIdx.parenthesizer := visitToken -@[combinatorParenthesizer Lean.Parser.many] -def many.parenthesizer (p : Parenthesizer) : Parenthesizer := do +@[combinatorParenthesizer Lean.Parser.manyNoAntiquot] +def manyNoAntiquot.parenthesizer (p : Parenthesizer) : Parenthesizer := do let stx ← getCur visitArgs $ stx.getArgs.size.forM fun _ => p -@[combinatorParenthesizer Lean.Parser.many1] -def many1.parenthesizer (p : Parenthesizer) : Parenthesizer := do - many.parenthesizer p +@[combinatorParenthesizer Lean.Parser.many1NoAntiquot] +def many1NoAntiquot.parenthesizer (p : Parenthesizer) : Parenthesizer := do + manyNoAntiquot.parenthesizer p @[combinatorParenthesizer Lean.Parser.many1Unbox] def many1Unbox.parenthesizer (p : Parenthesizer) : Parenthesizer := do let stx ← getCur if stx.getKind == nullKind then - many.parenthesizer p + manyNoAntiquot.parenthesizer p else p -@[combinatorParenthesizer Lean.Parser.optional] -def optional.parenthesizer (p : Parenthesizer) : Parenthesizer := do +@[combinatorParenthesizer Lean.Parser.optionalNoAntiquot] +def optionalNoAntiquot.parenthesizer (p : Parenthesizer) : Parenthesizer := do visitArgs p -@[combinatorParenthesizer Lean.Parser.sepBy] -def sepBy.parenthesizer (p pSep : Parenthesizer) : Parenthesizer := do +@[combinatorParenthesizer Lean.Parser.sepByNoAntiquot] +def sepByNoAntiquot.parenthesizer (p pSep : Parenthesizer) : Parenthesizer := do let stx ← getCur visitArgs $ (List.range stx.getArgs.size).reverse.forM $ fun i => if i % 2 == 0 then p else pSep -@[combinatorParenthesizer Lean.Parser.sepBy1] def sepBy1.parenthesizer := sepBy.parenthesizer +@[combinatorParenthesizer Lean.Parser.sepBy1NoAntiquot] def sepBy1NoAntiquot.parenthesizer := sepByNoAntiquot.parenthesizer @[combinatorParenthesizer Lean.Parser.withPosition] def withPosition.parenthesizer (p : Parenthesizer) : Parenthesizer := do -- We assume the formatter will indent syntax sufficiently such that parenthesizing a `withPosition` node is never necessary diff --git a/tests/lean/StxQuot.lean b/tests/lean/StxQuot.lean index ad77179062..e366972315 100644 --- a/tests/lean/StxQuot.lean +++ b/tests/lean/StxQuot.lean @@ -38,4 +38,11 @@ end Syntax #eval run $ do let a ← `(a.{0}); match_syntax a with `($id:ident) => pure id | _ => pure a #eval run $ do let a ← `(match a with | a => 1 | _ => 2); match_syntax a with `(match $e with $eqns:matchAlt*) => pure eqns | _ => pure #[] +#eval run do let a ← some <$> `(a); `({ a := a $[: $a]?}) +#eval run do let a ← pure none; `({ a := a $[: $a]?}) + +#eval run do + let pats := #[← `(a), ← `(a + 1)] + let rhss := #[← `(b), ← `(b + 1)] + `(match a with $[$pats => $rhss]|*) end Lean diff --git a/tests/lean/StxQuot.lean.expected.out b/tests/lean/StxQuot.lean.expected.out index 09fce44eb9..7e2a8c4af5 100644 --- a/tests/lean/StxQuot.lean.expected.out +++ b/tests/lean/StxQuot.lean.expected.out @@ -26,3 +26,6 @@ "`a._@.UnhygienicMain._hyg.1" "(Term.explicitUniv `a._@.UnhygienicMain._hyg.1 \".{\" [(numLit \"0\")] \"}\")" "#[]" +"(Term.structInst\n \"{\"\n []\n [[(Term.structInstField `a._@.UnhygienicMain._hyg.1 [] \":=\" `a._@.UnhygienicMain._hyg.1) []]]\n []\n [\":\" `a._@.UnhygienicMain._hyg.1]\n \"}\")" +"(Term.structInst\n \"{\"\n []\n [[(Term.structInstField `a._@.UnhygienicMain._hyg.1 [] \":=\" `a._@.UnhygienicMain._hyg.1) []]]\n []\n []\n \"}\")" +"(Term.match\n \"match\"\n [(Term.matchDiscr [] `a._@.UnhygienicMain._hyg.1)]\n []\n \"with\"\n (Term.matchAlts\n []\n [(Term.matchAlt [`a._@.UnhygienicMain._hyg.1] \"=>\" `b._@.UnhygienicMain._hyg.1)\n \"|\"\n (Term.matchAlt\n [(_kind.term._@.Init.Notation._hyg.637 `a._@.UnhygienicMain._hyg.1 \"+\" (numLit \"1\"))]\n \"=>\"\n (_kind.term._@.Init.Notation._hyg.637 `b._@.UnhygienicMain._hyg.1 \"+\" (numLit \"1\")))]))"