From 0afd970e15282b2ad70957c210c0a8be25cf9f63 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 6 Jan 2020 15:09:59 -0800 Subject: [PATCH] feat: add `declName?` to `TermElabM` context --- src/Init/Lean/Elab/Command.lean | 13 +++++++------ src/Init/Lean/Elab/Declaration.lean | 2 +- src/Init/Lean/Elab/Definition.lean | 2 +- src/Init/Lean/Elab/Term.lean | 2 ++ 4 files changed, 11 insertions(+), 8 deletions(-) diff --git a/src/Init/Lean/Elab/Command.lean b/src/Init/Lean/Elab/Command.lean index e95618d2ba..2d05d78fee 100644 --- a/src/Init/Lean/Elab/Command.lean +++ b/src/Init/Lean/Elab/Command.lean @@ -196,12 +196,13 @@ fun stx => withMacroExpansion stx.val $ do stx ← exp stx.val; elabCommand stx -private def mkTermContext (ctx : Context) (s : State) : Term.Context := +private def mkTermContext (ctx : Context) (s : State) (declName? : Option Name) : Term.Context := let scope := s.scopes.head!; { config := { opts := scope.opts, foApprox := true, ctxApprox := true, quasiPatternApprox := true, isDefEqStuckEx := true }, fileName := ctx.fileName, fileMap := ctx.fileMap, cmdPos := ctx.cmdPos, + declName? := declName?, macroStack := ctx.macroStack, currMacroScope := ctx.currMacroScope, currNamespace := scope.currNamespace, @@ -225,10 +226,10 @@ match result with instance CommandElabM.inhabited {α} : Inhabited (CommandElabM α) := ⟨throw $ arbitrary _⟩ -@[inline] def runTermElabM {α} (elab : Array Expr → TermElabM α) : CommandElabM α := do +@[inline] def runTermElabM {α} (declName? : Option Name) (elab : Array Expr → TermElabM α) : CommandElabM α := do ctx ← read; s ← get; -match (Term.elabBinders (getVarDecls s) elab (mkTermContext ctx s)).run (mkTermState s) with +match (Term.elabBinders (getVarDecls s) elab (mkTermContext ctx s declName?)).run (mkTermState s) with | EStateM.Result.ok a newS => do modify $ fun s => { env := newS.env, messages := newS.messages, .. s }; pure a | EStateM.Result.error (Term.Exception.error ex) newS => do modify $ fun s => { env := newS.env, messages := newS.messages, .. s }; throw ex | EStateM.Result.error Term.Exception.postpone newS => unreachable! @@ -475,7 +476,7 @@ fun n => do -- `variable` bracktedBinder let binder := n.getArg 1; -- Try to elaborate `binder` for sanity checking - runTermElabM $ fun _ => Term.elabBinder binder $ fun _ => pure (); + runTermElabM none $ fun _ => Term.elabBinder binder $ fun _ => pure (); modifyScope $ fun scope => { varDecls := scope.varDecls.push binder, .. scope } @[builtinCommandElab «variables»] def elabVariables : CommandElab := @@ -483,13 +484,13 @@ fun n => do -- `variables` bracktedBinder+ let binders := (n.getArg 1).getArgs; -- Try to elaborate `binders` for sanity checking - runTermElabM $ fun _ => Term.elabBinders binders $ fun _ => pure (); + runTermElabM none $ fun _ => Term.elabBinders binders $ fun _ => pure (); modifyScope $ fun scope => { varDecls := scope.varDecls ++ binders, .. scope } @[builtinCommandElab «check»] def elabCheck : CommandElab := fun stx => do let term := stx.getArg 1; - runTermElabM $ fun _ => do + runTermElabM none $ fun _ => do e ← Term.elabTerm term none; Term.synthesizeSyntheticMVars false; type ← Term.inferType stx.val e; diff --git a/src/Init/Lean/Elab/Declaration.lean b/src/Init/Lean/Elab/Declaration.lean index 47189daebf..f1431fa00f 100644 --- a/src/Init/Lean/Elab/Declaration.lean +++ b/src/Init/Lean/Elab/Declaration.lean @@ -94,7 +94,7 @@ withDeclId declId $ fun name => do declName ← mkDeclName modifiers name; applyAttributes stx declName modifiers.attrs AttributeApplicationTime.beforeElaboration; explictLevelNames ← getLevelNames; - decl ← runTermElabM $ fun vars => Term.elabBinders binders.getArgs $ fun xs => do { + decl ← runTermElabM declName $ fun vars => Term.elabBinders binders.getArgs $ fun xs => do { type ← Term.elabType typeStx; Term.synthesizeSyntheticMVars false; type ← Term.instantiateMVars typeStx type; diff --git a/src/Init/Lean/Elab/Definition.lean b/src/Init/Lean/Elab/Definition.lean index 9355aab29c..0a378b061a 100644 --- a/src/Init/Lean/Elab/Definition.lean +++ b/src/Init/Lean/Elab/Definition.lean @@ -127,7 +127,7 @@ withDeclId view.declId $ fun name => do declName ← mkDeclName view.modifiers name; applyAttributes ref declName view.modifiers.attrs AttributeApplicationTime.beforeElaboration; explictLevelNames ← getLevelNames; - decl? ← runTermElabM $ fun vars => Term.elabBinders view.binders.getArgs $ fun xs => + decl? ← runTermElabM declName $ fun vars => Term.elabBinders view.binders.getArgs $ fun xs => match view.type? with | some typeStx => do type ← Term.elabType typeStx; diff --git a/src/Init/Lean/Elab/Term.lean b/src/Init/Lean/Elab/Term.lean index 9671b43f48..0da0bb1c8f 100644 --- a/src/Init/Lean/Elab/Term.lean +++ b/src/Init/Lean/Elab/Term.lean @@ -22,6 +22,7 @@ structure Context extends Meta.Context := (fileMap : FileMap) (cmdPos : String.Pos) (currNamespace : Name) +(declName? : Option Name := none) (levelNames : List Name := []) (openDecls : List OpenDecl := []) (macroStack : List Syntax := []) @@ -217,6 +218,7 @@ instance LVal.hasToString : HasToString LVal := def getEnv : TermElabM Environment := do s ← get; pure s.env def getMCtx : TermElabM MetavarContext := do s ← get; pure s.mctx +def getDeclName? : TermElabM (Option Name) := do ctx ← read; pure ctx.declName? def getCurrNamespace : TermElabM Name := do ctx ← read; pure ctx.currNamespace def getOpenDecls : TermElabM (List OpenDecl) := do ctx ← read; pure ctx.openDecls def getLCtx : TermElabM LocalContext := do ctx ← read; pure ctx.lctx