From 22be1892ee1b6030cfe9406bf72bb320dbe68be7 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 12 Mar 2021 13:17:59 +0100
Subject: Slightly richer API allowing to shift the inductive in a block.

---
 user-contrib/Ltac2/Ind.v       | 16 ++++++++++++----
 user-contrib/Ltac2/tac2core.ml | 14 +++++++++++---
 2 files changed, 23 insertions(+), 7 deletions(-)

(limited to 'user-contrib')

diff --git a/user-contrib/Ltac2/Ind.v b/user-contrib/Ltac2/Ind.v
index 0283cb7121..f397a0e2c8 100644
--- a/user-contrib/Ltac2/Ind.v
+++ b/user-contrib/Ltac2/Ind.v
@@ -22,15 +22,23 @@ 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".
+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_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_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
diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index b9eef5c44e..d8fe03b7c0 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -1090,7 +1090,15 @@ let () = define1 "ind_data" (repr_ext val_inductive) begin fun ind ->
     throw err_notfound
 end
 
-let () = define1 "ind_ntypes" (repr_ext val_ind_data) begin fun (ind, mib) ->
+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
 
@@ -1099,9 +1107,9 @@ let () = define1 "ind_nconstructors" (repr_ext val_ind_data) begin fun ((_, n),
   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 ->
+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_inductive (fst ind, n))
+    return (Value.of_ext val_ind_data ((fst ind, n), mib))
   else throw err_notfound
 end
 
-- 
cgit v1.2.3