chore: update stage0

stage0/src/Lean/Elab/Do.lean

@@ -6,13 +6,52 @@ Authors: Leonardo de Moura
 import Lean.Elab.Term
 import Lean.Elab.Binders
 import Lean.Elab.Quotation
+import Lean.Elab.Match
 
 namespace Lean
 namespace Elab
 namespace Term
-
 open Meta
 
+@[builtinTermElab liftMethod] def elabLiftMethod : TermElab :=
+fun stx _ =>
+  throwErrorAt stx "invalid use of `(<- ...)`, must be nested inside a 'do' expression"
+
+private partial def hasLiftMethod : Syntax → Bool
+| Syntax.node k args =>
+  if k == `Lean.Parser.Term.do then false
+  else if k == `Lean.Parser.Term.quot then false
+  else if k == `Lean.Parser.Term.liftMethod then true
+  else args.any hasLiftMethod
+| _ => false
+
+structure ExtractMonadResult :=
+(m           : Expr)
+(α           : Expr)
+(hasBindInst : Expr)
+
+private def mkIdBindFor (type : Expr) : TermElabM ExtractMonadResult := do
+u ← getLevel type;
+let id        := Lean.mkConst `Id [u];
+let idBindVal := Lean.mkConst `Id.hasBind [u];
+pure { m := id, hasBindInst := idBindVal, α := type }
+
+private def extractBind (expectedType? : Option Expr) : TermElabM ExtractMonadResult := do
+match expectedType? with
+| none => throwError "invalid do notation, expected type is not available"
+| some expectedType => do
+  type ← withReducible $ whnf expectedType;
+  when type.getAppFn.isMVar $ throwError "invalid do notation, expected type is not available";
+  match type with
+  | Expr.app m α _ =>
+    catch
+      (do
+        bindInstType ← mkAppM `HasBind #[m];
+        bindInstVal  ← synthesizeInst bindInstType;
+        pure { m := m, hasBindInst := bindInstVal, α := α })
+      (fun ex => mkIdBindFor type)
+  | _ => mkIdBindFor type
+
 namespace Do
 
 /- A `doMatch` alternative. `vars` is the array of variables declared by `patterns`. -/
@@ -358,6 +397,167 @@ def mkWhen (ref : Syntax) (cond : Syntax) (c : CodeBlock) : CodeBlock :=
 def mkUnless (ref : Syntax) (cond : Syntax) (c : CodeBlock) : CodeBlock :=
 { c with code := Code.ite ref none mkNullNode cond (Code.«return» ref none) c.code }
 
+private def getDoSeqElems (doSeq : Syntax) : List Syntax :=
+if doSeq.getKind == `Lean.Parser.Term.doSeqBracketed then
+  (doSeq.getArg 1).getArgs.getSepElems.toList
+else
+  doSeq.getArgs.getSepElems.toList
+
+private def getDoSeq (doStx : Syntax) : Syntax :=
+doStx.getArg 1
+
+def getLetIdDeclVar (letIdDecl : Syntax) : Name :=
+(letIdDecl.getArg 0).getId
+
+def getLetPatDeclVars (letPatDecl : Syntax) : TermElabM (Array Name) := do
+let pattern := letPatDecl.getArg 0;
+patternVars ← getPatternVars pattern;
+pure $ patternVars.filterMap fun patternVar => match patternVar with
+  | PatternVar.localVar x => some x
+  | _ => none
+
+def getLetEqnsDeclVar (letEqnsDecl : Syntax) : Name :=
+(letEqnsDecl.getArg 0).getId
+
+def getLetDeclVars (letDecl : Syntax) : TermElabM (Array Name) := do
+let arg := letDecl.getArg 0;
+if arg.getKind == `Lean.Parser.Term.letIdDecl then
+  pure #[getLetIdDeclVar arg]
+else if arg.getKind == `Lean.Parser.Term.letPatDecl then
+  getLetPatDeclVars arg
+else if arg.getKind == `Lean.Parser.Term.letEqnsDecl then
+  pure #[getLetEqnsDeclVar arg]
+else
+  throwError "unexpected kind of let declaration"
+
+def getDoLetVars (doLet : Syntax) : TermElabM (Array Name) :=
+getLetDeclVars (doLet.getArg 1)
+
+def getDoReassignVars (doReassign : Syntax) : TermElabM (Array Name) := do
+let arg := doReassign.getArg 0;
+if arg.getKind == `Lean.Parser.Term.letIdDecl then
+  pure #[getLetIdDeclVar arg]
+else if arg.getKind == `Lean.Parser.Term.letPatDecl then
+  getLetPatDeclVars arg
+else
+  throwError "unexpected kind of reassignment"
+
+namespace ToCodeBlock
+
+structure Context :=
+(ref       : Syntax)
+(varSet    : NameSet := {})
+(insideFor : Bool := false)
+
+abbrev M := ReaderT Context TermElabM
+
+@[inline] def withNewVars {α} (newVars : Array Name) (x : M α) : M α :=
+adaptReader (fun (ctx : Context) => { ctx with varSet := insertVars ctx.varSet newVars }) x
+
+def ensureInsideFor : M Unit := do
+ctx ← read;
+unless ctx.insideFor $
+  throwError "invalid statement, can only be used inside 'for ... in ... do ...'"
+
+def ensureEOS (doElems : List Syntax) : M Unit :=
+unless doElems.isEmpty $
+  throwError "must be last element in a 'do' sequence"
+
+def isDoVar? (stx : Syntax) : M (Option Name) := do
+if stx.isIdent then do
+  ctx ← read;
+  let x := stx.getId;
+  if ctx.varSet.contains x then pure (some x) else pure none
+else
+  pure none
+
+def checkReassignable (xs : Array Name) : M Unit := do
+ctx ← read;
+xs.forM fun x =>
+  unless (ctx.varSet.contains x) do
+    throwError ("'" ++ x.simpMacroScopes ++ "' cannot be reassigned, it must be declared in the do-block")
+
+partial def doSeqToCode : List Syntax → M CodeBlock
+| [] => do ctx ← read; pure $ mkReturn ctx.ref
+| doElem::doElems => withRef doElem do
+  let ref := doElem;
+  let concatWithRest (c : CodeBlock) : M CodeBlock :=
+    match doElems with
+    | [] => pure c
+    | _  => do {
+      k ← doSeqToCode doElems;
+      liftM $ concat c k
+    };
+  let k := doElem.getKind;
+  if k == `Lean.Parser.Term.doLet then do
+    vars ← liftM $ getDoLetVars doElem;
+    mkVarDeclCore vars doElem <$> withNewVars vars (doSeqToCode doElems)
+  else if k == `Lean.Parser.Term.doLetRec then do
+    throwError "WIP"
+  else if k == `Lean.Parser.Term.doLetArrow then
+    throwError "WIP"
+  else if k == `Lean.Parser.Term.doReassign then do
+    vars ← liftM $ getDoReassignVars doElem;
+    checkReassignable vars;
+    k ← withNewVars vars (doSeqToCode doElems);
+    liftM $ mkReassignCore vars doElem k
+  else if k == `Lean.Parser.Term.doReassignArrow then
+    throwError "WIP"
+  else if k == `Lean.Parser.Term.doHave then
+    throwError "WIP"
+  else if k == `Lean.Parser.Term.doIf then
+    throwError "WIP"
+  else if k == `Lean.Parser.Term.doUnless then do
+    let cond  := doElem.getArg 1;
+    let doSeq := doElem.getArg 3;
+    body ← doSeqToCode (getDoSeqElems doSeq);
+    concatWithRest (mkUnless ref cond body)
+  else if k == `Lean.Parser.Term.doFor then
+    throwError "WIP"
+  else if k == `Lean.Parser.Term.doMatch then
+    throwError "WIP"
+  else if k == `Lean.Parser.Term.doTry then
+    throwError "WIP"
+  else if k == `Lean.Parser.Term.doBreak then do
+    ensureInsideFor;
+    ensureEOS doElems;
+    pure $ mkBreak ref
+  else if k == `Lean.Parser.Term.doContinue then do
+    ensureInsideFor;
+    ensureEOS doElems;
+    pure $ mkContinue ref
+  else if k == `Lean.Parser.Term.doReturn then do
+    ensureEOS doElems;
+    let argOpt := doElem.getArg 1;
+    if argOpt.isNone then
+      pure $ mkReturn ref
+    else do
+      let arg := argOpt.getArg 0;
+      x? ← isDoVar? arg;
+      match x? with
+      | some x => pure $ mkReturn ref x
+      | none => withFreshMacroScope do
+        auxDo ← `(do let x := $arg; return x);
+        doSeqToCode $ getDoSeqElems (getDoSeq auxDo)
+  else if k == `Lean.Parser.Term.doDbgTracethen then
+    throwError "WIP"
+  else if k == `Lean.Parser.Term.doAssert then
+    throwError "WIP"
+  else if k == `Lean.Parser.Term.doExpr then
+    let term := doElem.getArg 0;
+    if doElems.isEmpty then withFreshMacroScope do
+      auxDo ← `(do let x := $term; return x);
+      doSeqToCode $ getDoSeqElems (getDoSeq auxDo)
+    else
+      mkAction term <$> doSeqToCode doElems
+  else
+    throwError "unexpected do-element"
+
+def run (doStx : Syntax) : TermElabM CodeBlock :=
+(doSeqToCode $ getDoSeqElems $ getDoSeq doStx).run { ref := doStx }
+
+end ToCodeBlock
+
 private def mkTuple (elems : Array Syntax) : MacroM Syntax :=
 if elems.size == 1 then pure (elems.get! 0)
 else
@@ -365,34 +565,17 @@ else
     (fun elem tuple => `(($elem, $tuple)))
     (elems.back)
 
+-- @[builtinTermElab «do»]
+def elabDo : TermElab :=
+fun stx expectedType? => do
+  tryPostponeIfNoneOrMVar expectedType?;
+  bindInfo ← extractBind expectedType?;
+  codeBlock ← ToCodeBlock.run stx;
+  throwError ("WIP" ++ Format.line ++ codeBlock.toMessageData)
+
 end Do
 
-structure ExtractMonadResult :=
-(m           : Expr)
-(α           : Expr)
-(hasBindInst : Expr)
-
-private def mkIdBindFor (type : Expr) : TermElabM ExtractMonadResult := do
-u ← getLevel type;
-let id        := Lean.mkConst `Id [u];
-let idBindVal := Lean.mkConst `Id.hasBind [u];
-pure { m := id, hasBindInst := idBindVal, α := type }
-
-private def extractBind (expectedType? : Option Expr) : TermElabM ExtractMonadResult := do
-match expectedType? with
-| none => throwError "invalid do notation, expected type is not available"
-| some expectedType => do
-  type ← withReducible $ whnf expectedType;
-  when type.getAppFn.isMVar $ throwError "invalid do notation, expected type is not available";
-  match type with
-  | Expr.app m α _ =>
-    catch
-      (do
-        bindInstType ← mkAppM `HasBind #[m];
-        bindInstVal  ← synthesizeInst bindInstType;
-        pure { m := m, hasBindInst := bindInstVal, α := α })
-      (fun ex => mkIdBindFor type)
-  | _ => mkIdBindFor type
+----- OLD IMPLEMENTATION -----
 
 private def getDoElems (stx : Syntax) : Array Syntax :=
 let arg := stx.getArg 1;
@@ -405,14 +588,6 @@ if args.back.isToken ";" || args.back.isNone || (args.back.getArg 0).isToken ";"
 else
   args
 
-private partial def hasLiftMethod : Syntax → Bool
-| Syntax.node k args =>
-  if k == `Lean.Parser.Term.do then false
-  else if k == `Lean.Parser.Term.quot then false
-  else if k == `Lean.Parser.Term.liftMethod then true
-  else args.any hasLiftMethod
-| _ => false
-
 private partial def expandLiftMethodAux : Syntax → StateT (Array Syntax) MacroM Syntax
 | stx@(Syntax.node k args) =>
   if k == `Lean.Parser.Term.do then pure stx
@@ -575,7 +750,8 @@ catch
   (do stx ← expandDoElems false doElems 0; pure $ some stx)
   (fun _ => pure none)
 
-@[builtinTermElab «do»] def elabDo : TermElab :=
+@[builtinTermElab «do»]
+def elabDo : TermElab :=
 fun stx expectedType? => do
   stxNew? ← liftMacroM $ expandDo? stx;
   match stxNew? with
@@ -589,10 +765,6 @@ fun stx expectedType? => do
     { m := m, hasBindInst := bindInstVal, .. } ← extractBind expectedType?;
     processDoElems doElems m bindInstVal expectedType?.get!
 
-@[builtinTermElab liftMethod] def elabLiftMethod : TermElab :=
-fun stx _ =>
-  throwErrorAt stx "invalid use of `(<- ...)`, must be nested inside a 'do' expression"
-
 @[init] private def regTraceClasses : IO Unit := do
 registerTraceClass `Elab.do;
 pure ()

stage0/src/Lean/Parser/Do.lean

@@ -25,13 +25,15 @@ def doSeqIndent    := many1Indent $ doElemParser >> optional "; "
 def doSeqBracketed := parser! "{" >> withoutPosition (many1 (doElemParser >> optional "; ")) >> "}"
 def doSeq          := doSeqBracketed <|> doSeqIndent
 
+def notFollowedByRedefinedTermToken := notFollowedBy ("if" <|> "match" <|> "let" <|> "have" <|> "do" <|> "dbgTrace!" <|> "assert!")
+
 @[builtinDoElemParser] def doLet      := parser! "let " >> letDecl
 @[builtinDoElemParser] def doLetRec   := parser! group ("let " >> nonReservedSymbol "rec ") >> letRecDecls
-def doId   := parser! «try» (ident >> optType >> leftArrow) >> termParser
-def doPat  := parser! «try» (termParser >> leftArrow) >> termParser >> optional (" | " >> termParser)
-@[builtinDoElemParser] def doLetArrow      := parser! "let " >> (doId <|> doPat)
-@[builtinDoElemParser] def doReassign      := parser! letIdDecl <|> letPatDecl
-@[builtinDoElemParser] def doReassignArrow := doId <|> doPat
+def doIdDecl   := parser! «try» (ident >> optType >> leftArrow) >> termParser
+def doPatDecl  := parser! «try» (termParser >> leftArrow) >> termParser >> optional (" | " >> termParser)
+@[builtinDoElemParser] def doLetArrow      := parser! "let " >> (doIdDecl <|> doPatDecl)
+@[builtinDoElemParser] def doReassign      := parser! notFollowedByRedefinedTermToken >> (letIdDecl <|> letPatDecl)
+@[builtinDoElemParser] def doReassignArrow := parser! notFollowedByRedefinedTermToken >> (doIdDecl <|> doPatDecl)
 @[builtinDoElemParser] def doHave     := parser! "have " >> Term.haveDecl
 /-
 In `do` blocks, we support `if` without an `else`. Thus, we use indentation to prevent examples such as
@@ -64,10 +66,10 @@ else if c_2 then
 -/
 @[builtinDoElemParser] def doIf := parser! withPosition $
   "if " >> optIdent >> termParser >> " then " >> doSeq
-  >> many (checkColGe "'else if' in 'do' must be indented" >> «try» (" else " >> " if ") >> optIdent >> termParser >> " then " >> doSeq)
+  >> many (checkColGe "'else if' in 'do' must be indented" >> group («try» (group (" else " >> " if ")) >> optIdent >> termParser >> " then " >> doSeq))
   >> optional (checkColGe "'else' in 'do' must be indented" >> " else " >> doSeq)
-@[builtinDoElemParser] def doUnless := parser! "unless " >> termParser >> "do " >> doSeq
-@[builtinDoElemParser] def doFor    := parser! "for " >> termParser >> " in " >> termParser >> "do " >> doSeq
+@[builtinDoElemParser] def doUnless := parser! "unless " >> withPosition (termParser >> optional ",") >> doSeq
+@[builtinDoElemParser] def doFor    := parser! "for " >> termParser >> " in " >> withPosition (termParser >> optional ", ") >> doSeq
 
 /- `match`-expression where the right-hand-side of alternatives is a `doSeq` instead of a `term` -/
 def doMatchAlt : Parser  := sepBy1 termParser ", " >> darrow >> doSeq
@@ -91,7 +93,7 @@ doesn't enforce indentation restrictions, but we don't want it to be used when `
 Note that parser priorities would not solve this problem since the `doIf` parser is failing while the `if`
 parser is succeeding.
 -/
-@[builtinDoElemParser] def doExpr   := parser! notFollowedBy ("if" <|> "match" <|> "let" <|> "have" <|> "do") >> termParser
+@[builtinDoElemParser] def doExpr   := parser! notFollowedByRedefinedTermToken >> termParser
 
 @[builtinTermParser] def «do»  := parser!:maxPrec "do " >> doSeq
 

stage0/stdlib/Lean/Parser/Command.c

@@ -367,7 +367,6 @@ lean_object* l_Lean_Parser_Command_def;
 lean_object* l_Lean_Parser_Command_openRenamingItem___elambda__1___closed__13;
 lean_object* l_Lean_Parser_Command_declSig___closed__2;
 lean_object* l_Lean_Parser_Term_quot_formatter___closed__7;
-extern lean_object* l_Lean_Parser_Term_doPat___closed__2;
 lean_object* l_Lean_Parser_Command_structure___closed__2;
 lean_object* l_Lean_Parser_Command_declaration___elambda__1___closed__2;
 lean_object* l_Lean_Parser_Command_structFields___closed__4;
@@ -523,6 +522,7 @@ lean_object* l_Lean_Parser_Command_synth___elambda__1___closed__5;
 lean_object* l_Lean_Parser_Command_def_parenthesizer___closed__2;
 lean_object* l_Lean_Parser_Command_check__failure___closed__3;
 lean_object* l_Lean_Parser_Command_eval___closed__6;
+extern lean_object* l_Lean_Parser_Term_doPatDecl___elambda__1___closed__9;
 extern lean_object* l_Lean_Parser_antiquotNestedExpr_parenthesizer___closed__3;
 lean_object* l_Lean_Parser_Command_unsafe_parenthesizer___closed__2;
 lean_object* l_Lean_Parser_Command_instance___elambda__1(lean_object*, lean_object*);
@@ -1068,6 +1068,7 @@ lean_object* l_Lean_Parser_Command_init__quot_formatter(lean_object*, lean_objec
 lean_object* l_Lean_Parser_Command_example___elambda__1___closed__3;
 lean_object* l_Lean_Parser_Command_variable___elambda__1___closed__8;
 lean_object* l_Lean_Parser_Command_partial___closed__3;
+extern lean_object* l_Lean_Parser_Term_doPatDecl_formatter___closed__4;
 lean_object* l_Lean_Parser_Command_declaration_parenthesizer___closed__18;
 lean_object* l_Lean_Parser_Command_structExplicitBinder___closed__2;
 lean_object* l_Lean_Parser_Command_set__option_parenthesizer___closed__6;
@@ -1510,7 +1511,6 @@ lean_object* l_Lean_Parser_Command_extends_formatter___closed__3;
 lean_object* l_Lean_Parser_Command_declModifiers_parenthesizer___closed__11;
 lean_object* l_Lean_Parser_Command_structImplicitBinder;
 lean_object* l_Lean_Parser_Command_openRenaming_formatter___closed__5;
-extern lean_object* l_Lean_Parser_Term_doPat_formatter___closed__4;
 lean_object* l_Lean_Parser_Command_partial___elambda__1___closed__5;
 lean_object* l_Lean_Parser_Command_set__option___closed__8;
 lean_object* l_Lean_Parser_Term_quot_parenthesizer___closed__5;
@@ -1755,7 +1755,6 @@ lean_object* l_Lean_Parser_Command_resolve__name___elambda__1___closed__7;
 lean_object* l_Lean_Parser_Command_openRenamingItem___elambda__1___closed__11;
 lean_object* l_Lean_Parser_Command_openHiding___closed__2;
 lean_object* l_Lean_Parser_Command_constant___closed__4;
-extern lean_object* l_Lean_Parser_Term_doPat___elambda__1___closed__6;
 lean_object* l_Lean_Parser_Command_optDeclSig_parenthesizer___closed__4;
 lean_object* l_Lean_Parser_Command_universe_formatter___closed__3;
 lean_object* l_Lean_Parser_Command_partial___closed__2;
@@ -1842,7 +1841,6 @@ lean_object* l_Lean_Parser_Command_def_formatter___closed__2;
 lean_object* l_Lean_Parser_Command_structCtor___elambda__1___closed__4;
 lean_object* l_Lean_Parser_Command_structureTk___closed__5;
 lean_object* l_Lean_Parser_Command_universes___elambda__1___closed__9;
-extern lean_object* l_Lean_Parser_Term_doPat___elambda__1___closed__9;
 lean_object* l_Lean_Parser_Command_initialize___closed__10;
 lean_object* l_Lean_Parser_Command_print___closed__1;
 lean_object* l_Lean_Parser_Command_universes_parenthesizer___closed__2;
@@ -2148,6 +2146,7 @@ lean_object* l_Lean_Parser_Command_in_formatter(lean_object*, lean_object*, lean
 lean_object* l_Lean_Parser_Command_instance_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Command_structExplicitBinder___closed__7;
 extern lean_object* l_Lean_Parser_Term_liftMethod_formatter___closed__2;
+extern lean_object* l_Lean_Parser_Term_doPatDecl___closed__2;
 lean_object* l_Lean_Parser_Command_declSig___closed__6;
 lean_object* l_Lean_Parser_Command_print;
 lean_object* l_Lean_Parser_Command_abbrev_formatter___closed__1;
@@ -2166,6 +2165,7 @@ lean_object* l___regBuiltin_Lean_Parser_Command_universe_formatter(lean_object*)
 lean_object* l_Lean_Parser_Command_openRenamingItem_formatter___closed__2;
 lean_object* l_Lean_Parser_Command_structInstBinder_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Command_declId___closed__10;
+extern lean_object* l_Lean_Parser_Term_doPatDecl___elambda__1___closed__6;
 lean_object* l_Lean_Parser_Command_abbrev_formatter___closed__4;
 lean_object* l_Lean_Parser_Command_universe___closed__5;
 lean_object* l_Lean_Parser_Command_openHiding___elambda__1___closed__2;
@@ -13712,13 +13712,13 @@ lean_object* x_61; lean_object* x_62; uint8_t x_63;
 x_61 = lean_ctor_get(x_60, 1);
 lean_inc(x_61);
 lean_dec(x_60);
-x_62 = l_Lean_Parser_Term_doPat___elambda__1___closed__6;
+x_62 = l_Lean_Parser_Term_doPatDecl___elambda__1___closed__6;
 x_63 = lean_string_dec_eq(x_61, x_62);
 lean_dec(x_61);
 if (x_63 == 0)
 {
 lean_object* x_64; lean_object* x_65; 
-x_64 = l_Lean_Parser_Term_doPat___elambda__1___closed__9;
+x_64 = l_Lean_Parser_Term_doPatDecl___elambda__1___closed__9;
 x_65 = l_Lean_Parser_ParserState_mkErrorsAt(x_57, x_64, x_56);
 x_11 = x_65;
 goto block_55;
@@ -13734,7 +13734,7 @@ else
 {
 lean_object* x_66; lean_object* x_67; 
 lean_dec(x_60);
-x_66 = l_Lean_Parser_Term_doPat___elambda__1___closed__9;
+x_66 = l_Lean_Parser_Term_doPatDecl___elambda__1___closed__9;
 x_67 = l_Lean_Parser_ParserState_mkErrorsAt(x_57, x_66, x_56);
 x_11 = x_67;
 goto block_55;
@@ -13744,7 +13744,7 @@ else
 {
 lean_object* x_68; lean_object* x_69; 
 lean_dec(x_58);
-x_68 = l_Lean_Parser_Term_doPat___elambda__1___closed__9;
+x_68 = l_Lean_Parser_Term_doPatDecl___elambda__1___closed__9;
 x_69 = l_Lean_Parser_ParserState_mkErrorsAt(x_57, x_68, x_56);
 x_11 = x_69;
 goto block_55;
@@ -13981,13 +13981,13 @@ lean_object* x_152; lean_object* x_153; uint8_t x_154;
 x_152 = lean_ctor_get(x_151, 1);
 lean_inc(x_152);
 lean_dec(x_151);
-x_153 = l_Lean_Parser_Term_doPat___elambda__1___closed__6;
+x_153 = l_Lean_Parser_Term_doPatDecl___elambda__1___closed__6;
 x_154 = lean_string_dec_eq(x_152, x_153);
 lean_dec(x_152);
 if (x_154 == 0)
 {
 lean_object* x_155; lean_object* x_156; 
-x_155 = l_Lean_Parser_Term_doPat___elambda__1___closed__9;
+x_155 = l_Lean_Parser_Term_doPatDecl___elambda__1___closed__9;
 x_156 = l_Lean_Parser_ParserState_mkErrorsAt(x_148, x_155, x_147);
 x_84 = x_156;
 goto block_146;
@@ -14003,7 +14003,7 @@ else
 {
 lean_object* x_157; lean_object* x_158; 
 lean_dec(x_151);
-x_157 = l_Lean_Parser_Term_doPat___elambda__1___closed__9;
+x_157 = l_Lean_Parser_Term_doPatDecl___elambda__1___closed__9;
 x_158 = l_Lean_Parser_ParserState_mkErrorsAt(x_148, x_157, x_147);
 x_84 = x_158;
 goto block_146;
@@ -14013,7 +14013,7 @@ else
 {
 lean_object* x_159; lean_object* x_160; 
 lean_dec(x_149);
-x_159 = l_Lean_Parser_Term_doPat___elambda__1___closed__9;
+x_159 = l_Lean_Parser_Term_doPatDecl___elambda__1___closed__9;
 x_160 = l_Lean_Parser_ParserState_mkErrorsAt(x_148, x_159, x_147);
 x_84 = x_160;
 goto block_146;
@@ -14262,7 +14262,7 @@ lean_object* _init_l_Lean_Parser_Command_ctor___closed__5() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Term_doPat___closed__2;
+x_1 = l_Lean_Parser_Term_doPatDecl___closed__2;
 x_2 = l_Lean_Parser_Command_ctor___closed__4;
 x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
 return x_3;
@@ -25655,7 +25655,7 @@ lean_object* _init_l_Lean_Parser_Command_ctor_formatter___closed__8() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Term_doPat_formatter___closed__4;
+x_1 = l_Lean_Parser_Term_doPatDecl_formatter___closed__4;
 x_2 = l_Lean_Parser_Command_ctor_formatter___closed__7;
 x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_andthen_formatter), 7, 2);
 lean_closure_set(x_3, 0, x_1);