Lean4
/-- Use the `args` to refine the goals `gs` in order, but whenever there is a single
goal remaining then first try applying a single constructor if it's for a single-constructor
inductive type. In `eager` mode, instead we always first try to refine, and if that fails we
always try to apply such a constructor no matter if it's the last goal.
Returns the remaining explicit goals `gs`, any goals `acc` due to `refine`, and a sublist of these
of instance arguments that we should try synthesizing after the loop.
The new set of goals should be `gs ++ acc`. -/
partial def useLoop (eager : Bool) (gs : List MVarId) (args : List Term) (acc insts : List MVarId) :
TermElabM (List MVarId × List MVarId × List MVarId) := do
trace[tactic.use]"gs = {gs }\nargs = {args }\nacc = {acc}"
match gs, args with
| gs, [] =>
return (gs, acc, insts)
| [], arg :: _ =>
throwErrorAt arg "too many arguments supplied to `use`"
| g :: gs', arg :: args' =>
g.withContext
(do
if ← g.isAssigned then
-- Goals might become assigned in inductive types with indices.
-- Let's check that what's supplied is defeq to what's already there.
let e ← Term.elabTermEnsuringType arg (← g.getType)
unless ← isDefEq e (.mvar g) do
throwErrorAt arg "argument is not definitionally equal to inferred value{indentExpr (.mvar g)}"
return ← useLoop eager gs' args' acc insts
let refineArg ← `(tactic| refine without_cdot($arg : $(← Term.exprToSyntax (← g.getType))))
if eager then
-- In eager mode, first try refining with the argument before applying the constructor
if let some newGoals←
observing?
(run g do
withoutRecover <| evalTactic refineArg) then
return ← useLoop eager gs' args' (acc ++ newGoals) insts
if eager || gs'.isEmpty then
if let some (expl, impl, insts')←
observing?
(do
try
applyTheConstructor g
catch e =>
trace[tactic.use]"Constructor. {e.toMessageData}";
throw e) then
trace[tactic.use]"expl.length = {expl.length }, impl.length = {impl.length}"
return
←
useLoop eager (expl ++ gs') args (acc ++ impl)
(insts ++ insts')
-- In eager mode, the following will give an error, which hopefully is more informative than
-- the one provided by `applyTheConstructor`.
let newGoals ←
run g do
evalTactic refineArg
useLoop eager gs' args' (acc ++ newGoals) insts)
