Merge PR #13920: Adding an Ltac2 API to manipulate inductive types.

Reviewed-by: JasonGross
Ack-by: jfehrle

8 files changed, 127 insertions, 0 deletions

diff --git a/doc/changelog/05-tactic-language/13920-ltac2-ind-api.rst b/doc/changelog/05-tactic-language/13920-ltac2-ind-api.rst
new file mode 100644
index 0000000000..32499957be
--- /dev/null
+++ b/doc/changelog/05-tactic-language/13920-ltac2-ind-api.rst
@@ -0,0 +1,5 @@
+- **Added:**
+  Added the Ltac2 API `Ltac2.Ind` for manipulating inductive types
+  (`#13920 <https://github.com/coq/coq/pull/13920>`_,
+  fixes `#10095 <https://github.com/coq/coq/issues/10095>`_,
+  by Pierre-Marie Pédrot).
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index b0f4e883be..d67906c4a8 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -685,6 +685,7 @@ through the <tt>Require Import</tt> command.</p>
     user-contrib/Ltac2/Fresh.v
     user-contrib/Ltac2/Ident.v
     user-contrib/Ltac2/Init.v
+    user-contrib/Ltac2/Ind.v
     user-contrib/Ltac2/Int.v
     user-contrib/Ltac2/List.v
     user-contrib/Ltac2/Ltac1.v
diff --git a/test-suite/ltac2/ind.v b/test-suite/ltac2/ind.v
new file mode 100644
index 0000000000..6f7352d224
--- /dev/null
+++ b/test-suite/ltac2/ind.v
@@ -0,0 +1,25 @@
+Require Import Ltac2.Ltac2.
+Require Import Ltac2.Option.
+
+Ltac2 Eval
+  let nat := Option.get (Env.get [@Coq; @Init; @Datatypes; @nat]) in
+  let nat := match nat with
+  | Std.IndRef nat => nat
+  | _ => Control.throw Not_found
+  end in
+  let data := Ind.data nat in
+  (* Check that there is only one inductive in the block *)
+  let ntypes := Ind.nblocks data in
+  let () := if Int.equal ntypes 1 then () else Control.throw Not_found in
+  let nat' := Ind.repr (Ind.get_block data 0) in
+  (* Check it corresponds *)
+  let () := if Ind.equal nat nat' then () else Control.throw Not_found in
+  let () := if Int.equal (Ind.index nat) 0 then () else Control.throw Not_found in
+  (* Check the number of constructors *)
+  let nconstr := Ind.nconstructors data in
+  let () := if Int.equal nconstr 2 then () else Control.throw Not_found in
+  (* Create a fresh instance *)
+  let s := Ind.get_constructor data 1 in
+  let s := Env.instantiate (Std.ConstructRef s) in
+  constr:($s 0)
+.
diff --git a/user-contrib/Ltac2/Ind.v b/user-contrib/Ltac2/Ind.v
new file mode 100644
index 0000000000..f397a0e2c8
--- /dev/null
+++ b/user-contrib/Ltac2/Ind.v
@@ -0,0 +1,45 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+From Ltac2 Require Import Init.
+
+Ltac2 Type t := inductive.
+
+Ltac2 @ external equal : t -> t -> bool := "ltac2" "ind_equal".
+(** Equality test. *)
+
+Ltac2 Type data.
+(** Type of data representing inductive blocks. *)
+
+Ltac2 @ external data : t -> data := "ltac2" "ind_data".
+(** Get the mutual blocks corresponding to an inductive type in the current
+    environment. Panics if there is no such inductive. *)
+
+Ltac2 @ external repr : data -> t := "ltac2" "ind_repr".
+(** Returns the inductive corresponding to the block. Inverse of [data]. *)
+
+Ltac2 @ external index : t -> int := "ltac2" "ind_index".
+(** Returns the index of the inductive type inside its mutual block. Guaranteed
+    to range between [0] and [nblocks data - 1] where [data] was retrieved
+    using the above function. *)
+
+Ltac2 @ external nblocks : data -> int := "ltac2" "ind_nblocks".
+(** Returns the number of inductive types appearing in a mutual block. *)
+
+Ltac2 @ external nconstructors : data -> int := "ltac2" "ind_nconstructors".
+(** Returns the number of constructors appearing in the current block. *)
+
+Ltac2 @ external get_block : data -> int -> data := "ltac2" "ind_get_block".
+(** Returns the block corresponding to the nth inductive type. Index must range
+    between [0] and [nblocks data - 1], otherwise the function panics. *)
+
+Ltac2 @ external get_constructor : data -> int -> constructor := "ltac2" "ind_get_constructor".
+(** Returns the nth constructor of the inductive type. Index must range between
+    [0] and [nconstructors data - 1], otherwise the function panics. *)
diff --git a/user-contrib/Ltac2/Ltac2.v b/user-contrib/Ltac2/Ltac2.v
index ccfc7e4a70..e55c6c13d3 100644
--- a/user-contrib/Ltac2/Ltac2.v
+++ b/user-contrib/Ltac2/Ltac2.v
@@ -22,6 +22,7 @@ Require Ltac2.Fresh.
 Require Ltac2.Pattern.
 Require Ltac2.Std.
 Require Ltac2.Env.
+Require Ltac2.Ind.
 Require Ltac2.Printf.
 Require Ltac2.Ltac1.
 Require Export Ltac2.Notations.
diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index 948a359124..d8fe03b7c0 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -1075,6 +1075,54 @@ let () = define1 "env_instantiate" reference begin fun r ->
   return (Value.of_constr c)
 end
 
+(** Ind *)
+
+let () = define2 "ind_equal" (repr_ext val_inductive) (repr_ext val_inductive) begin fun ind1 ind2 ->
+  return (Value.of_bool (Ind.UserOrd.equal ind1 ind2))
+end
+
+let () = define1 "ind_data" (repr_ext val_inductive) begin fun ind ->
+  Proofview.tclENV >>= fun env ->
+  if Environ.mem_mind (fst ind) env then
+    let mib = Environ.lookup_mind (fst ind) env in
+    return (Value.of_ext val_ind_data (ind, mib))
+  else
+    throw err_notfound
+end
+
+let () = define1 "ind_repr" (repr_ext val_ind_data) begin fun (ind, _) ->
+  return (Value.of_ext val_inductive ind)
+end
+
+let () = define1 "ind_index" (repr_ext val_inductive) begin fun (ind, n) ->
+  return (Value.of_int n)
+end
+
+let () = define1 "ind_nblocks" (repr_ext val_ind_data) begin fun (ind, mib) ->
+  return (Value.of_int (Array.length mib.Declarations.mind_packets))
+end
+
+let () = define1 "ind_nconstructors" (repr_ext val_ind_data) begin fun ((_, n), mib) ->
+  let open Declarations in
+  return (Value.of_int (Array.length mib.mind_packets.(n).mind_consnames))
+end
+
+let () = define2 "ind_get_block" (repr_ext val_ind_data) int begin fun (ind, mib) n ->
+  if 0 <= n && n < Array.length mib.Declarations.mind_packets then
+    return (Value.of_ext val_ind_data ((fst ind, n), mib))
+  else throw err_notfound
+end
+
+let () = define2 "ind_get_constructor" (repr_ext val_ind_data) int begin fun ((mind, n), mib) i ->
+  let open Declarations in
+  let ncons = Array.length mib.mind_packets.(n).mind_consnames in
+  if 0 <= i && i < ncons then
+    (* WARNING: In the ML API constructors are indexed from 1 for historical
+       reasons, but Ltac2 uses 0-indexing instead. *)
+    return (Value.of_ext val_constructor ((mind, n), i + 1))
+  else throw err_notfound
+end
+
 (** Ltac1 in Ltac2 *)
 
 let ltac1 = Tac2ffi.repr_ext Value.val_ltac1
diff --git a/user-contrib/Ltac2/tac2ffi.ml b/user-contrib/Ltac2/tac2ffi.ml
index a09438c6bf..5f9fbc4e41 100644
--- a/user-contrib/Ltac2/tac2ffi.ml
+++ b/user-contrib/Ltac2/tac2ffi.ml
@@ -104,6 +104,7 @@ 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"
+let val_ind_data : (Names.Ind.t * Declarations.mutual_inductive_body) Val.tag = Val.create "ind_data"
 
 let extract_val (type a) (type b) (tag : a Val.tag) (tag' : b Val.tag) (v : b) : a =
 match Val.eq tag tag' with
diff --git a/user-contrib/Ltac2/tac2ffi.mli b/user-contrib/Ltac2/tac2ffi.mli
index c9aa50389e..e87ad7139c 100644
--- a/user-contrib/Ltac2/tac2ffi.mli
+++ b/user-contrib/Ltac2/tac2ffi.mli
@@ -184,6 +184,7 @@ 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
+val val_ind_data : (Names.Ind.t * Declarations.mutual_inductive_body) Val.tag
 
 val val_exn : Exninfo.iexn Tac2dyn.Val.tag
 (** Toplevel representation of OCaml exceptions. Invariant: no [LtacError]