Preterm vs Constr.Unsafe · Ltac2

Can someone explain the difference between Ltac2 preterms and terms constructed via Constr.Unsafe?
The documentation states that preterms are untyped syntactic Coq expressions. Is that different from constructing terms through the Constr.Unsafe API? Would it make sense to have a Constr.Unsafe.from_preterm : preterm -> kind function?

For context: I am manipulating some terms under an arbitrary number of binders. My goal is to decompose for example input := fun x y z => op (g x y) (h y z) into left := fun x y z => g x y and right := fun x y z => h y z for some operator op, along with a proof that ∀ x y z, input x y z = op (left x y z) (right x y z).
I use Constr.Unsafe.kind to look beneath an arbitrary number of Lambdas. This allows me to match! on the head of the function (i.e. check that it is op), and get the arguments (i.e. g _ _ and h _ _ in this case). The arguments to g and h will mention de Bruijn variables, however, so I need to put lambdas around these again---and the same applies for the proof term.
The proof term is somewhat annoying: I'd like to write something like '(my_proof_term $left $right) and then rebind this under the binders. But there are situations where I get an Anomaly: "in retyping: Unbound local variable".---I think when a de Bruijn variable is the head term of left or right. I can write preterm:(my_proof_term $left $right) without these complaints, but then I cannot rebind this: I can only Constr.pretype preterms. The one thing that works is to use Constr.Unsafe.App to explicitly write the term I want, but this is much more verbose than using preterms.

Gaëtan Gilbert (Mar 25 2024 at 10:53):

preterm is before elaboration
for instance preterm:(_) is not an evar, it's a preterm which generates an evar when given to pretyping. So for instance let c := preterm:(_) in let c1 := pretype c in let c2 := pretype c in Constr.equal c1 c2 returns false because c1 and c2 are 2 unrelated evars

since it's not an evar there's no appropriate kind to return from an hypothetical preterm -> kind function

(BTW printing goes through those stages in the opposite direction, detyping/extern/printing)

intern does things like expanding notations, inserting holes for implicit arguments, resolving global names (so eg fun x => id x is internalized to fun x : _ => @whatever.id _ x)
pretype does things like inserting coercions, match compilation, turning holes into evars and resolving evars through unification as required for typechecking

Gaëtan Gilbert (Mar 25 2024 at 10:58):

you can also build more preterms, eg let c := preterm:(_) in preterm:(0 : $preterm:c)($preterm:x is like $x but for preterm variables) (constr:(bla $preterm:x) will run pretyping on the preterm bound to x)
not sure how well building preterms with unbound rels and later closing them to pretype works but you can try

Ike Mulder (Mar 25 2024 at 11:19):

Cannot we go to kind by generating evars? Or is the problem that there might not be enough information to do so?

Ike Mulder (Mar 25 2024 at 11:21):

From Ltac2 Require Import Ltac2 Printf.

Section test.
Notation f := (fun (x : nat) P => x = 0 /\ P).

Lemma as_and_trivial (P Q : Prop) : (P /\ Q) = (P /\ Q).
Proof. reflexivity. Qed.

Goal True.
match Constr.Unsafe.kind 'f with
| Constr.Unsafe.Lambda b1 t1 =>
  match Constr.Unsafe.kind t1 with
  | Constr.Unsafe.Lambda b2 t2 =>
    lazy_match! t2 with
    | and ?l ?r =>
      printf "left: %t   right: %t" l r;
      let proto_preterm := preterm:(as_and_trivial $l $r) in
      (* let proto_open_constr := '(as_and_trivial $l $r) in *)
      (* above produces:   Anomaly "in retyping: Unbound local variable." *)
      let b1_type := Constr.Binder.type b1 in
      let b2_type := Constr.Binder.type b2 in
      let result := '(fun (x : $b1_type) (P : $b2_type) => $preterm:proto_preterm) in
      printf "result: %t" result
    end
  | _ => Control.throw Not_found
  end
| _ => Control.throw Not_found
end.
Abort.
End test.

but I wouldn't know how to make result when all I have is a bs : binder list.

Gaëtan Gilbert (Mar 25 2024 at 11:46):

Ltac2 wrap_binder (c:preterm) b :=
  let t := Constr.Binder.type b in
  preterm:(fun (x : $t) => $preterm:c).

(* or fold_right depending on which order the list is in *)
Ltac2 wrap_binders bs c := List.fold_left wrap_binder c bs.

Ltac2 make_result bs c := let c := wrap_binders bs c in pretype c.

?
But if you want to put a variable number of binders with different naming in the rel context I don't think we have the APIs

Ike Mulder (Mar 25 2024 at 12:16):

Ah, of course, one can just stay in preterm. Yes, so the only downside is that this loses the naming information, the rest works out.

Completed example

From Ltac2 Require Import Ltac2 Printf.
Require Import Vector.


Section test.
Notation f := (fun (x : nat) (v : Vector.t nat x) P => v = v /\ P).

Lemma as_and_trivial (P Q : Prop) : (P /\ Q) = (P /\ Q).
Proof. reflexivity. Qed.

Ltac2 wrap_binder b (c:preterm) :=
  let t := Constr.Binder.type b in
  preterm:(fun (x : $t) => $preterm:c).

Ltac2 wrap_binders bs c := List.fold_right wrap_binder bs c.

Ltac2 make_result bs c := let c := wrap_binders bs c in Constr.pretype c.

(* [get_head_term_n_args] returns the head symbol and arguments of provided [p : constr],
even if [p] is a lambda-term. Useful for matching beneath binders.
Also returns the list of binders under which was recursed *)
Ltac2 rec get_head_term_n_args (p : constr) : constr * constr list * binder list :=
  match Constr.Unsafe.kind p with
  | Constr.Unsafe.Lambda b p' =>
    let (h, args_i, bs) := (get_head_term_n_args p') in
    (h, args_i, b :: bs)
  | Constr.Unsafe.App p' args =>
    let (h, args_i, bs) := (get_head_term_n_args p') in
    (h, List.append args_i (Array.to_list args), bs)
  | Constr.Unsafe.Cast p' _ _ => get_head_term_n_args p'
  | _ => p, [], []
  end.


Goal True.
let (head, args, bs) := get_head_term_n_args 'f in
printf "head: %t" head;
lazy_match! head with
| and =>
  let l := List.nth args 0 in
  let r := List.nth args 1 in
  printf "left: %t   right: %t" l r;
  let proto_preterm := preterm:(as_and_trivial $l $r) in
  let result := make_result bs proto_preterm in
  printf "result: %t" result
end.
Abort.
End test.

Stream: Ltac2