Adding an Ltac2 API to manipulate inductive types.

Fixes #10095: Get list of constructors of Inductive.

5 files changed, 80 insertions, 0 deletions

diff --git a/user-contrib/Ltac2/Ind.v b/user-contrib/Ltac2/Ind.v
new file mode 100644
index 0000000000..0283cb7121
--- /dev/null
+++ b/user-contrib/Ltac2/Ind.v
@@ -0,0 +1,37 @@
+(************************************************************************)
+(*         *   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 ntypes : data -> int := "ltac2" "ind_ntypes".
+(** 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_type : data -> int -> t := "ltac2" "ind_get_type".
+(** Returns the nth inductive type in the block. Index must range between [0]
+    and [ntypes 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..b9eef5c44e 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -1075,6 +1075,46 @@ 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_ntypes" (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_type" (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_inductive (fst ind, n))
+  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]