Lean4
/-- For a sum type `inductive Foo (α : Type) | foo1 : List α → ℕ → Foo α | ...`
``traverseConstructor `foo1 `Foo applInst f `α `β [`(x : List α), `(y : ℕ)]``
synthesizes `foo1 <$> traverse f x <*> pure y.` -/
def traverseConstructor (c n : Name) (applInst f α β : Expr) (args₀ : List Expr) (args₁ : List (Bool × Expr))
(m : MVarId) : TermElabM Unit := do
let ad ← getAuxDefOfDeclName
let g ← m.getType >>= instantiateMVars
let args' ←
args₁.mapM
(fun (y : Bool × Expr) =>
if y.1 then return (true, mkAppN (.fvar ad) #[g.appFn!, applInst, α, β, f, y.2])
else traverseField n g.appFn! f α y.2)
let gargs := args'.filterMap (fun y => if y.1 then some y.2 else none)
let v ← mkFunCtor c (args₀.map (fun e => (false, e)) ++ args')
let pureInst ← mkAppOptM ``Applicative.toPure #[none, applInst]
let constr' ← mkAppOptM ``Pure.pure #[none, pureInst, none, v]
let r ← gargs.foldlM (fun e garg => mkFunUnit garg >>= fun e' => mkAppM ``Seq.seq #[e, e']) constr'
m.assign r
where/-- `mkFunCtor ctor [(true, (arg₁ : m type₁)), (false, (arg₂ : type₂)), (true, (arg₃ : m type₃)),
(false, (arg₄ : type₄))]` makes `fun (x₁ : type₁) (x₃ : type₃) => ctor x₁ arg₂ x₃ arg₄`. -/
mkFunCtor (c : Name) (args : List (Bool × Expr)) (fvars : Array Expr := #[]) (aargs : Array Expr := #[]) :
TermElabM Expr := do
match args with
| (true, x) :: xs =>
let n ← mkFreshUserName `x
let t ← inferType x
withLocalDeclD n t.appArg! fun y => mkFunCtor c xs (fvars.push y) (aargs.push y)
| (false, x) :: xs =>
mkFunCtor c xs fvars (aargs.push x)
| [] =>
liftM <| mkAppOptM c (aargs.map some) >>= mkLambdaFVars fvars
