Hide the Ltac2 binder type.

For robustness and it is better to leave it opaque. Users are not supposed to
fiddle with it.

5 files changed, 48 insertions, 34 deletions

diff --git a/user-contrib/Ltac2/Constr.v b/user-contrib/Ltac2/Constr.v
index c3343db149..e778a8d677 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, constr)
+| Lambda (binder, constr, constr)
+| LetIn (binder, constr, 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, constr array)
+| CoFix (int, binder array, constr array, constr array)
 | Proj (projection, constr)
 | Uint63 (uint63)
 | Float (float)
@@ -74,6 +70,18 @@ Ltac2 @ external constructor : inductive -> int -> constructor := "ltac2" "const
 
 End Unsafe.
 
+Module Binder.
+
+Ltac2 Type relevance := [ Relevant | Irrelevant ].
+
+Ltac2 @ external make : ident option -> relevance -> binder := "ltac2" "constr_binder_make".
+
+Ltac2 @ external name : binder -> ident option := "ltac2" "constr_binder_name".
+
+Ltac2 @ external relevance : binder -> relevance := "ltac2" "constr_binder_relevance".
+
+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..c6abbf11b1 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -82,14 +82,6 @@ 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 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
@@ -99,16 +91,13 @@ let to_relevance = function
   | 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 relevance = make_repr of_relevance to_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 of_binder b =
+  Value.of_ext Value.val_binder b
+
+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,12 +108,12 @@ 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 of_binder nas,
   Value.of_array Value.of_constr ts,
   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 to_binder nas,
   Value.to_array Value.to_constr ts,
   Value.to_array Value.to_constr cs)
 
@@ -408,19 +397,19 @@ let () = define1 "constr_kind" constr begin fun c ->
     |]
   | Prod (na, t, u) ->
     v_blk 6 [|
-      of_annot of_name na;
+      of_binder na;
       Value.of_constr t;
       Value.of_constr u;
     |]
   | Lambda (na, t, c) ->
     v_blk 7 [|
-      of_annot of_name na;
+      of_binder na;
       Value.of_constr t;
       Value.of_constr c;
     |]
   | LetIn (na, b, t, c) ->
     v_blk 8 [|
-      of_annot of_name na;
+      of_binder na;
       Value.of_constr b;
       Value.of_constr t;
       Value.of_constr c;
@@ -505,17 +494,17 @@ let () = define1 "constr_make" valexpr begin fun knd ->
     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 na = to_binder na in
     let t = Value.to_constr t 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 na = to_binder na in
     let t = Value.to_constr t 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
+    let na = 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
@@ -664,6 +653,20 @@ let () = define1 "constr_pretype" (repr_ext val_preterm) begin fun c ->
   pf_apply pretype
 end
 
+let () = define2 "constr_binder_make" (option ident) relevance begin fun na rel ->
+  let na = match na with None -> Anonymous | Some id -> Name id in
+  return (Value.of_ext val_binder (Context.make_annot na rel))
+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_relevance" (repr_ext val_binder) begin fun bnd ->
+  return (of_relevance bnd.Context.binder_relevance)
+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..5138133360 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 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