aboutsummaryrefslogtreecommitdiff
path: root/user-contrib
diff options
context:
space:
mode:
Diffstat (limited to 'user-contrib')
-rw-r--r--user-contrib/Ltac2/Ind.v45
-rw-r--r--user-contrib/Ltac2/Ltac2.v1
-rw-r--r--user-contrib/Ltac2/tac2core.ml75
-rw-r--r--user-contrib/Ltac2/tac2entries.ml13
-rw-r--r--user-contrib/Ltac2/tac2ffi.ml1
-rw-r--r--user-contrib/Ltac2/tac2ffi.mli1
6 files changed, 127 insertions, 9 deletions
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..bcf9ece7c8 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
@@ -1388,24 +1436,35 @@ let () =
(** Ltac2 in terms *)
let () =
- let interp ist poly env sigma concl (ids, tac) =
+ let interp ?loc ~poly env sigma tycon (ids, tac) =
(* Syntax prevents bound notation variables in constr quotations *)
let () = assert (Id.Set.is_empty ids) in
- let ist = Tac2interp.get_env ist in
+ let ist = Tac2interp.get_env @@ GlobEnv.lfun env in
let tac = Proofview.tclIGNORE (Tac2interp.interp ist tac) in
let name, poly = Id.of_string "ltac2", poly in
- let c, sigma = Proof.refine_by_tactic ~name ~poly env sigma concl tac in
- (EConstr.of_constr c, sigma)
+ let sigma, concl = match tycon with
+ | Some ty -> sigma, ty
+ | None -> GlobEnv.new_type_evar env sigma ~src:(loc,Evar_kinds.InternalHole)
+ in
+ let c, sigma = Proof.refine_by_tactic ~name ~poly (GlobEnv.renamed_env env) sigma concl tac in
+ let j = { Environ.uj_val = EConstr.of_constr c; Environ.uj_type = concl } in
+ (j, sigma)
in
GlobEnv.register_constr_interp0 wit_ltac2_constr interp
let () =
- let interp ist poly env sigma concl id =
- let ist = Tac2interp.get_env ist in
+ let interp ?loc ~poly env sigma tycon id =
+ let ist = Tac2interp.get_env @@ GlobEnv.lfun env in
let c = Id.Map.find id ist.env_ist in
let c = Value.to_constr c in
- let sigma = Typing.check env sigma c concl in
- (c, sigma)
+ let t = Retyping.get_type_of (GlobEnv.renamed_env env) sigma c in
+ match tycon with
+ | None ->
+ { Environ.uj_val = c; Environ.uj_type = t }, sigma
+ | Some ty ->
+ let sigma = Evarconv.unify_leq_delay (GlobEnv.renamed_env env) sigma t ty in
+ let j = { Environ.uj_val = c; Environ.uj_type = ty } in
+ j, sigma
in
GlobEnv.register_constr_interp0 wit_ltac2_quotation interp
diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml
index d0655890a7..faa1e74728 100644
--- a/user-contrib/Ltac2/tac2entries.ml
+++ b/user-contrib/Ltac2/tac2entries.ml
@@ -816,7 +816,18 @@ let perform_eval ~pstate e =
| Goal_select.SelectList l -> Proofview.tclFOCUSLIST l v
| Goal_select.SelectId id -> Proofview.tclFOCUSID id v
| Goal_select.SelectAll -> v
- | Goal_select.SelectAlreadyFocused -> assert false (* TODO **)
+ | Goal_select.SelectAlreadyFocused ->
+ let open Proofview.Notations in
+ Proofview.numgoals >>= fun n ->
+ if Int.equal n 1 then v
+ else
+ let e = CErrors.UserError
+ (None,
+ Pp.(str "Expected a single focused goal but " ++
+ int n ++ str " goals are focused."))
+ in
+ let info = Exninfo.reify () in
+ Proofview.tclZERO ~info e
in
let (proof, _, ans) = Proof.run_tactic (Global.env ()) v proof in
let { Proof.sigma } = Proof.data proof in
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]
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 18:45:44 +0000