Lean4
/-- Format a goal into a type signature for a declaration named `name`.
Example output: `myTheorem (a b : Nat) : a + b = b + a`.
The return values are:
* A formatted piece of `MessageData`, like `m!"myTheorem (a b : Nat) : a + b = b + a"`.
* The full type of the declaration, like `∀ a b, a + b = b + a`.
* The imports needed to state this declaration, as an array of module names.
-/
def goalSignature (name : Name) (g : MVarId) : TermElabM (MessageData × Expr × Array Name) :=
withoutModifyingEnv <|
withoutModifyingState
(do
let (g, _) ← g.renameInaccessibleFVars
let (_, g) ← g.revert (clearAuxDeclsInsteadOfRevert := true) (← g.getDecl).lctx.getFVarIds
let ty ← instantiateMVars (← g.getType)
if ty.hasExprMVar then
-- TODO: turn metavariables into new hypotheses?
throwError "Extracted goal has metavariables: {ty}"
let ty ← Term.levelMVarToParam ty
let seenLevels := collectLevelParams { } ty
let levels := (← Term.getLevelNames).filter fun u => seenLevels.visitedLevel.contains (.param u)
addAndCompile <|
Declaration.axiomDecl
{ name := name
levelParams := levels
isUnsafe := false
type := ty }
let sig ← addMessageContext <| MessageData.signature name
let context ← liftM (m := CoreM) <| read
let state ← get
let env ← getEnv
let (ts, _) ←
((Mathlib.Command.MinImports.getVisited name).run { context with snap? := none }).run
{ state with env, maxRecDepth := context.maxRecDepth }
let mut hm : Std.HashMap Nat Name := { }
for imp in env.header.moduleNames do
hm := hm.insert ((env.getModuleIdx? imp).getD default) imp
let mut fins : NameSet := { }
for t in ts do
let new :=
match env.getModuleIdxFor? t with
| some t => (hm.get? t).get!
| none => .anonymous
if !fins.contains new then
fins := fins.insert new
let tot := Mathlib.Command.MinImports.getIrredundantImports (← getEnv) (fins.erase .anonymous)
let fileNames := tot.toArray.qsort Name.lt
return (sig, ty, fileNames))
