From 17b5c56ab72d42f3cf71390e0f9beed360c9777f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 9 Mar 2021 07:45:54 +0100 Subject: Adding an Ltac2 API to manipulate inductive types. Fixes #10095: Get list of constructors of Inductive. --- user-contrib/Ltac2/Ind.v | 37 +++++++++++++++++++++++++++++++++++++ user-contrib/Ltac2/Ltac2.v | 1 + user-contrib/Ltac2/tac2core.ml | 40 ++++++++++++++++++++++++++++++++++++++++ user-contrib/Ltac2/tac2ffi.ml | 1 + user-contrib/Ltac2/tac2ffi.mli | 1 + 5 files changed, 80 insertions(+) create mode 100644 user-contrib/Ltac2/Ind.v 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 *) +(* 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] -- cgit v1.2.3 From 2915154835b8d0a90a5c3ca79c37d66142dc9a33 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 10 Mar 2021 13:57:38 +0100 Subject: Add tests for the new Ltac2 Ind API. --- test-suite/ltac2/ind.v | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) create mode 100644 test-suite/ltac2/ind.v diff --git a/test-suite/ltac2/ind.v b/test-suite/ltac2/ind.v new file mode 100644 index 0000000000..c06ffebabe --- /dev/null +++ b/test-suite/ltac2/ind.v @@ -0,0 +1,24 @@ +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.ntypes data in + let () := if Int.equal ntypes 1 then () else Control.throw Not_found in + let nat' := Ind.get_type data 0 in + (* Check it corresponds *) + let () := if Ind.equal nat nat' 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) +. -- cgit v1.2.3 From 761d3ccaf6a593a73811da38fa731c2f601902f8 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 10 Mar 2021 14:07:46 +0100 Subject: Adding a changelog and registering the new file in the documentation. --- doc/changelog/05-tactic-language/13920-ltac2-ind-api.rst | 5 +++++ doc/stdlib/index-list.html.template | 1 + 2 files changed, 6 insertions(+) create mode 100644 doc/changelog/05-tactic-language/13920-ltac2-ind-api.rst 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 `_, + fixes `#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 Require Import command.

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 -- cgit v1.2.3 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. --- test-suite/ltac2/ind.v | 5 +++-- user-contrib/Ltac2/Ind.v | 16 ++++++++++++---- user-contrib/Ltac2/tac2core.ml | 14 +++++++++++--- 3 files changed, 26 insertions(+), 9 deletions(-) diff --git a/test-suite/ltac2/ind.v b/test-suite/ltac2/ind.v index c06ffebabe..6f7352d224 100644 --- a/test-suite/ltac2/ind.v +++ b/test-suite/ltac2/ind.v @@ -9,11 +9,12 @@ Ltac2 Eval end in let data := Ind.data nat in (* Check that there is only one inductive in the block *) - let ntypes := Ind.ntypes data in + let ntypes := Ind.nblocks data in let () := if Int.equal ntypes 1 then () else Control.throw Not_found in - let nat' := Ind.get_type data 0 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 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