Merge PR #11607: Hide binder type in Ltac2

Reviewed-by: JasonGross
Ack-by: SkySkimmer

7 files changed, 102 insertions, 65 deletions

diff --git a/test-suite/ltac2/binder.v b/test-suite/ltac2/binder.v
new file mode 100644
index 0000000000..eac74688b2
--- /dev/null
+++ b/test-suite/ltac2/binder.v
@@ -0,0 +1,37 @@
+Require Import Ltac2.Ltac2.
+
+Ltac2 check () :=
+let t := Control.goal () in
+match Constr.Unsafe.kind t with
+| Constr.Unsafe.Prod b t =>
+  let na := Constr.Binder.name b in
+  let u := Constr.Binder.type b in
+  let b := Constr.Binder.make na u in
+  let c := Constr.Unsafe.make (Constr.Unsafe.Prod b t) in
+  pose (v := $c);
+  refine '(_ : &v);
+  unfold &v
+| _ => fail
+end.
+
+Goal forall x : nat, x = x.
+Proof.
+check (); intros; reflexivity.
+Qed.
+
+Goal forall x : Type, x = x.
+Proof.
+check (); intros; reflexivity.
+Qed.
+
+Goal forall x : Set, x = x.
+Proof.
+check (); intros; reflexivity.
+Qed.
+
+Inductive True : SProp := I.
+
+Goal forall x : True, True.
+Proof.
+check (); intros; constructor.
+Qed.
diff --git a/test-suite/ltac2/constr.v b/test-suite/ltac2/constr.v
index 39601d99a8..018596ed95 100644
--- a/test-suite/ltac2/constr.v
+++ b/test-suite/ltac2/constr.v
@@ -2,11 +2,11 @@ Require Import Ltac2.Constr Ltac2.Init Ltac2.Control.
 Import Unsafe.
 
 Ltac2 Eval match (kind '(nat -> bool)) with
-           | Prod a b c => a
+           | Prod a c => a
            | _ => throw Match_failure end.
 
 Set Allow StrictProp.
 Axiom something : SProp.
 Ltac2 Eval match (kind '(forall x : something, bool)) with
-           | Prod a b c => a
+           | Prod a c => a
            | _ => throw Match_failure end.
diff --git a/user-contrib/Ltac2/Constr.v b/user-contrib/Ltac2/Constr.v
index c3343db149..94d468e640 100644
--- a/user-contrib/Ltac2/Constr.v
+++ b/user-contrib/Ltac2/Constr.v
@@ -16,10 +16,6 @@ Ltac2 @ external type : constr -> constr := "ltac2" "constr_type".
 Ltac2 @ external equal : constr -> constr -> bool := "ltac2" "constr_equal".
 (** Strict syntactic equality: only up to α-conversion and evar expansion *)
 
-Ltac2 Type relevance := [ Relevant | Irrelevant ].
-
-Ltac2 Type 'a binder_annot := { binder_name : 'a; binder_relevance : relevance }.
-
 Module Unsafe.
 
 (** Low-level access to kernel terms. Use with care! *)
@@ -33,16 +29,16 @@ Ltac2 Type kind := [
 | Evar (evar, constr array)
 | Sort (sort)
 | Cast (constr, cast, constr)
-| Prod (ident option binder_annot, constr, constr)
-| Lambda (ident option binder_annot, constr, constr)
-| LetIn (ident option binder_annot, constr, constr, constr)
+| Prod (binder, constr)
+| Lambda (binder, constr)
+| LetIn (binder, constr, constr)
 | App (constr, constr array)
 | Constant (constant, instance)
 | Ind (inductive, instance)
 | Constructor (constructor, instance)
 | Case (case, constr, constr, constr array)
-| Fix (int array, int, ident option binder_annot array, constr array, constr array)
-| CoFix (int, ident option binder_annot array, constr array, constr array)
+| Fix (int array, int, binder array, constr array)
+| CoFix (int, binder array, constr array)
 | Proj (projection, constr)
 | Uint63 (uint63)
 | Float (float)
@@ -74,6 +70,19 @@ Ltac2 @ external constructor : inductive -> int -> constructor := "ltac2" "const
 
 End Unsafe.
 
+Module Binder.
+
+Ltac2 @ external make : ident option -> constr -> binder := "ltac2" "constr_binder_make".
+(** Create a binder given the name and the type of the bound variable. *)
+
+Ltac2 @ external name : binder -> ident option := "ltac2" "constr_binder_name".
+(** Retrieve the name of a binder. *)
+
+Ltac2 @ external type : binder -> constr := "ltac2" "constr_binder_type".
+(** Retrieve the type of a binder. *)
+
+End Binder.
+
 Ltac2 @ external in_context : ident -> constr -> (unit -> unit) -> constr := "ltac2" "constr_in_context".
 (** On a focused goal [Γ ⊢ A], [in_context id c tac] evaluates [tac] in a
     focused goal [Γ, id : c ⊢ ?X] and returns [fun (id : c) => t] where [t] is
diff --git a/user-contrib/Ltac2/Init.v b/user-contrib/Ltac2/Init.v
index 271c3de556..a4f6d497df 100644
--- a/user-contrib/Ltac2/Init.v
+++ b/user-contrib/Ltac2/Init.v
@@ -32,6 +32,7 @@ Ltac2 Type projection.
 Ltac2 Type pattern.
 Ltac2 Type constr.
 Ltac2 Type preterm.
+Ltac2 Type binder.
 
 Ltac2 Type message.
 Ltac2 Type exn := [ .. ].
diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index 864e2ebb0d..38b05bed6b 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -82,33 +82,11 @@ open Core
 let v_unit = Value.of_unit ()
 let v_blk = Valexpr.make_block
 
-let of_name c = match c with
-| Anonymous -> Value.of_option Value.of_ident None
-| Name id -> Value.of_option Value.of_ident (Some id)
+let of_binder b =
+  Value.of_ext Value.val_binder b
 
-let to_name c = match Value.to_option Value.to_ident c with
-| None -> Anonymous
-| Some id -> Name id
-
-let of_relevance = function
-  | Sorts.Relevant -> ValInt 0
-  | Sorts.Irrelevant -> ValInt 1
-
-let to_relevance = function
-  | ValInt 0 -> Sorts.Relevant
-  | ValInt 1 -> Sorts.Irrelevant
-  | _ -> assert false
-
-let of_annot f Context.{binder_name;binder_relevance} =
-  of_tuple [|(f binder_name); of_relevance binder_relevance|]
-
-let to_annot f x =
-  match to_tuple x with
-  | [|x;y|] ->
-    let x = f x in
-    let y = to_relevance y in
-    Context.make_annot x y
-  | _ -> assert false
+let to_binder b =
+  Value.to_ext Value.val_binder b
 
 let of_instance u =
   let u = Univ.Instance.to_array (EConstr.Unsafe.to_instance u) in
@@ -119,13 +97,14 @@ let to_instance u =
   EConstr.EInstance.make (Univ.Instance.of_array u)
 
 let of_rec_declaration (nas, ts, cs) =
-  (Value.of_array (of_annot of_name) nas,
-  Value.of_array Value.of_constr ts,
+  let binders = Array.map2 (fun na t -> (na, t)) nas ts in
+  (Value.of_array of_binder binders,
   Value.of_array Value.of_constr cs)
 
-let to_rec_declaration (nas, ts, cs) =
-  (Value.to_array (to_annot to_name) nas,
-  Value.to_array Value.to_constr ts,
+let to_rec_declaration (nas, cs) =
+  let nas = Value.to_array to_binder nas in
+  (Array.map fst nas,
+  Array.map snd nas,
   Value.to_array Value.to_constr cs)
 
 let of_result f = function
@@ -408,21 +387,18 @@ let () = define1 "constr_kind" constr begin fun c ->
     |]
   | Prod (na, t, u) ->
     v_blk 6 [|
-      of_annot of_name na;
-      Value.of_constr t;
+      of_binder (na, t);
       Value.of_constr u;
     |]
   | Lambda (na, t, c) ->
     v_blk 7 [|
-      of_annot of_name na;
-      Value.of_constr t;
+      of_binder (na, t);
       Value.of_constr c;
     |]
   | LetIn (na, b, t, c) ->
     v_blk 8 [|
-      of_annot of_name na;
+      of_binder (na, t);
       Value.of_constr b;
-      Value.of_constr t;
       Value.of_constr c;
     |]
   | App (c, cl) ->
@@ -453,20 +429,18 @@ let () = define1 "constr_kind" constr begin fun c ->
       Value.of_array Value.of_constr bl;
     |]
   | Fix ((recs, i), def) ->
-    let (nas, ts, cs) = of_rec_declaration def in
+    let (nas, cs) = of_rec_declaration def in
     v_blk 14 [|
       Value.of_array Value.of_int recs;
       Value.of_int i;
       nas;
-      ts;
       cs;
     |]
   | CoFix (i, def) ->
-    let (nas, ts, cs) = of_rec_declaration def in
+    let (nas, cs) = of_rec_declaration def in
     v_blk 15 [|
       Value.of_int i;
       nas;
-      ts;
       cs;
     |]
   | Proj (p, c) ->
@@ -504,20 +478,17 @@ let () = define1 "constr_make" valexpr begin fun knd ->
     let k = Value.to_ext Value.val_cast k in
     let t = Value.to_constr t in
     EConstr.mkCast (c, k, t)
-  | (6, [|na; t; u|]) ->
-    let na = to_annot to_name na in
-    let t = Value.to_constr t in
+  | (6, [|na; u|]) ->
+    let (na, t) = to_binder na in
     let u = Value.to_constr u in
     EConstr.mkProd (na, t, u)
-  | (7, [|na; t; c|]) ->
-    let na = to_annot to_name na in
-    let t = Value.to_constr t in
+  | (7, [|na; c|]) ->
+    let (na, t) = to_binder na in
     let u = Value.to_constr c in
     EConstr.mkLambda (na, t, u)
-  | (8, [|na; b; t; c|]) ->
-    let na = to_annot to_name na in
+  | (8, [|na; b; c|]) ->
+    let (na, t) = to_binder na in
     let b = Value.to_constr b in
-    let t = Value.to_constr t in
     let c = Value.to_constr c in
     EConstr.mkLetIn (na, b, t, c)
   | (9, [|c; cl|]) ->
@@ -542,14 +513,14 @@ let () = define1 "constr_make" valexpr begin fun knd ->
     let t = Value.to_constr t in
     let bl = Value.to_array Value.to_constr bl in
     EConstr.mkCase (ci, c, t, bl)
-  | (14, [|recs; i; nas; ts; cs|]) ->
+  | (14, [|recs; i; nas; cs|]) ->
     let recs = Value.to_array Value.to_int recs in
     let i = Value.to_int i in
-    let def = to_rec_declaration (nas, ts, cs) in
+    let def = to_rec_declaration (nas, cs) in
     EConstr.mkFix ((recs, i), def)
-  | (15, [|i; nas; ts; cs|]) ->
+  | (15, [|i; nas; cs|]) ->
     let i = Value.to_int i in
-    let def = to_rec_declaration (nas, ts, cs) in
+    let def = to_rec_declaration (nas, cs) in
     EConstr.mkCoFix (i, def)
   | (16, [|p; c|]) ->
     let p = Value.to_ext Value.val_projection p in
@@ -664,6 +635,23 @@ let () = define1 "constr_pretype" (repr_ext val_preterm) begin fun c ->
   pf_apply pretype
 end
 
+let () = define2 "constr_binder_make" (option ident) constr begin fun na ty ->
+  pf_apply begin fun env sigma ->
+  let rel = Retyping.relevance_of_type env sigma ty in
+  let na = match na with None -> Anonymous | Some id -> Name id in
+  return (Value.of_ext val_binder (Context.make_annot na rel, ty))
+  end
+end
+
+let () = define1 "constr_binder_name" (repr_ext val_binder) begin fun (bnd, _) ->
+  let na = match bnd.Context.binder_name with Anonymous -> None | Name id -> Some id in
+  return (Value.of_option Value.of_ident na)
+end
+
+let () = define1 "constr_binder_type" (repr_ext val_binder) begin fun (bnd, ty) ->
+  return (of_constr ty)
+end
+
 (** Patterns *)
 
 let empty_context = EConstr.mkMeta Constr_matching.special_meta
diff --git a/user-contrib/Ltac2/tac2ffi.ml b/user-contrib/Ltac2/tac2ffi.ml
index 58173faea6..a09438c6bf 100644
--- a/user-contrib/Ltac2/tac2ffi.ml
+++ b/user-contrib/Ltac2/tac2ffi.ml
@@ -100,6 +100,7 @@ let val_constant = Val.create "constant"
 let val_constructor = Val.create "constructor"
 let val_projection = Val.create "projection"
 let val_case = Val.create "case"
+let val_binder = Val.create "binder"
 let val_univ = Val.create "universe"
 let val_free : Names.Id.Set.t Val.tag = Val.create "free"
 let val_ltac1 : Geninterp.Val.t Val.tag = Val.create "ltac1"
diff --git a/user-contrib/Ltac2/tac2ffi.mli b/user-contrib/Ltac2/tac2ffi.mli
index d84d2cabb7..c9aa50389e 100644
--- a/user-contrib/Ltac2/tac2ffi.mli
+++ b/user-contrib/Ltac2/tac2ffi.mli
@@ -180,6 +180,7 @@ val val_constant : Constant.t Val.tag
 val val_constructor : constructor Val.tag
 val val_projection : Projection.t Val.tag
 val val_case : Constr.case_info Val.tag
+val val_binder : (Name.t Context.binder_annot * types) Val.tag
 val val_univ : Univ.Level.t Val.tag
 val val_free : Id.Set.t Val.tag
 val val_ltac1 : Geninterp.Val.t Val.tag