/-
Copyright (c) 2022 Scott Morrison. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Scott Morrison, Newell Jensen
-/
import Lean.Elab.Command
import Lean.Meta.Tactic.Constructor

open Lean Meta Elab Tactic

/--
`fconstructor` is like `constructor`
(it calls `apply` using the first matching constructor of an inductive datatype)
except that it does not reorder goals.
-/
elab "fconstructor" : tactic: Parser.Category
tactic => withMainContext: {α : Type} → TacticM α → TacticM α
withMainContext do
  let mvarIds': ?m.367
mvarIds' ← (← getMainGoal): ?m.135
(← getMainGoal: TacticM MVarId
getMainGoal(← getMainGoal): ?m.135
).constructor: MVarId →
  optParam ApplyConfig { newGoals := ApplyNewGoals.nonDependentFirst, synthAssignedInstances := true, approx := true } →
    MetaM (List MVarId)
constructor {newGoals := .all: ApplyNewGoals
.all}
  Term.synthesizeSyntheticMVarsNoPostponing: optParam Bool false → TermElabM Unit
Term.synthesizeSyntheticMVarsNoPostponing
  replaceMainGoal: List MVarId → TacticM Unit
replaceMainGoal mvarIds': ?m.367
mvarIds'

/--
`econstructor` is like `constructor`
(it calls `apply` using the first matching constructor of an inductive datatype)
except only non-dependent premises are added as new goals.
-/
elab "econstructor" : tactic: Parser.Category
tactic => withMainContext: {α : Type} → TacticM α → TacticM α
withMainContext do
  let mvarIds': ?m.2130
mvarIds' ← (← getMainGoal): ?m.1898
(← getMainGoal: TacticM MVarId
getMainGoal(← getMainGoal): ?m.1898
).constructor: MVarId →
  optParam ApplyConfig { newGoals := ApplyNewGoals.nonDependentFirst, synthAssignedInstances := true, approx := true } →
    MetaM (List MVarId)
constructor {newGoals := .nonDependentOnly: ApplyNewGoals
.nonDependentOnly}
  Term.synthesizeSyntheticMVarsNoPostponing: optParam Bool false → TermElabM Unit
Term.synthesizeSyntheticMVarsNoPostponing
  replaceMainGoal: List MVarId → TacticM Unit
replaceMainGoal mvarIds': ?m.2130
mvarIds'