Obtaining eta expansion of constructor without typeclasses #19
Description
A while back, @JasonGross pointed out that you can obtain an eta expansion of a record's constructor without relying on user-provided typeclass instances like
(* all you need to do is provide something like this, listing out the fields of your record: *)
Instance etaX : Settable _ := settable! mkX <A; B; C>.and his solution looks as follows:
Record X := mkX { A : nat ; B : nat ; C : bool ; }.
Ltac make_eta X :=
let s
:= constr:(ltac:(
let x := fresh "x" in
intro x; unshelve eexists;
[ econstructor; destruct x | destruct x; reflexivity ])
: forall x : X, { x' : X | x' = x }) in
lazymatch s with
| fun x => exist _ (@?s x) _ => s
end.
Check ltac:(let s := make_eta X in exact s).It creates an eta-expanded version of the constructor mkX:
fun x : X =>
{|
A := match x with
| {| A := A; B := B; C := C |} => (fun (A0 _ : nat) (_ : bool) => A0) A B C
end;
B := match x with
| {| A := A; B := B; C := C |} => (fun (_ B0 : nat) (_ : bool) => B0) A B C
end;
C := match x with
| {| A := A; B := B; C := C |} => (fun (_ _ : nat) (C0 : bool) => C0) A B C
end
|}
: X -> XHowever, @tchajed (and myself, too) did not like that solution because it does not reuse the existing getters, but creates new ones.
Now, for those who like Ltac2 hacks, here's a way to obtain an eta-expanded constructor that does reuse the existing getters:
Require Import Ltac2.Ltac2.
Require Ltac2.Option.
Module Import ModA.
Record foo(A: Type)(n: nat) := {
fieldA: unit;
fieldB: n = n;
fieldC: bool;
}.
End ModA.
(* to show that the code below is robust against this kind of shadowing *)
Definition fieldA := @id.
Ltac2 rec strip_foralls(t: constr) :=
match Constr.Unsafe.kind t with
| Constr.Unsafe.Prod b u => let (bs, body) := strip_foralls u in (b :: bs, body)
| _ => ([], t)
end.
Ltac2 app_arg_count(t: constr) :=
match Constr.Unsafe.kind t with
| Constr.Unsafe.App f args => Array.length args
| _ => 0
end.
Ltac2 binder_to_field(qualification: ident list)(b: binder) :=
Option.get (Env.get (List.append qualification [Option.get (Constr.Binder.name b)])).
Ltac2 field_names(ctor_ref: Std.reference) :=
let ctor_type := Constr.type (Env.instantiate ctor_ref) in
let (binders, result) := strip_foralls ctor_type in
let n_type_args := app_arg_count result in
let field_name_binders := List.skipn n_type_args binders in
List.map (binder_to_field (List.removelast (Env.path ctor_ref))) field_name_binders.
Ltac2 constructor_of_record(t: constr) :=
match Constr.Unsafe.kind t with
| Constr.Unsafe.Ind ind inst =>
Std.ConstructRef (Constr.Unsafe.constructor ind 0)
| _ => Control.throw (Invalid_argument (Some (Message.of_constr t)))
end.
Ltac2 Eval constructor_of_record constr:(foo).
Ltac2 mkApp(f: constr)(args: constr array) :=
Constr.Unsafe.make (Constr.Unsafe.App f args).
Ltac2 eta(t: constr) :=
let (h, args) := match Constr.Unsafe.kind t with
| Constr.Unsafe.App h args => (h, args)
| _ => (t, Array.empty ())
end in
let ctor := constructor_of_record h in
let getters := List.map (fun getterRef => mkApp (Env.instantiate getterRef) args)
(field_names ctor) in
constr:(fun x: $t => ltac2:(
let projections := List.map (fun getter => constr:($getter &x)) getters in
let res := mkApp (mkApp (Env.instantiate ctor) args) (Array.of_list projections) in
exact $res)).
Definition foo_eta(T: Type)(n: nat): foo T n -> foo T n :=
ltac2:(let res := eta constr:(foo T n) in exact $res).
Print foo_eta.
(*
foo_eta =
fun (T : Type) (n : nat) (x : foo T n) =>
{| ModA.fieldA := ModA.fieldA T n x; fieldB := fieldB T n x; fieldC := fieldC T n x |}
: forall (T : Type) (n : nat), foo T n -> foo T n
*)
Definition X_eta: X -> X :=
ltac2:(let res := eta constr:(X) in exact $res).
Print X_eta.
(* creates an eta-expanded version of the constructor mkX, reusing the existing getters A, B, C:
X_eta = fun x : X => {| A := A x; B := B x; C := C x |}
: X -> X
*)I haven't tried yet whether it could replace the current typeclass-based approach, nor spent any thought on whether such code is morally acceptable, but just wanted to paste it here for whoever might find it entertaining 😉