aboutsummaryrefslogtreecommitdiff
path: root/user-contrib
diff options
context:
space:
mode:
Diffstat (limited to 'user-contrib')
-rw-r--r--user-contrib/Ltac2/Array.v2
-rw-r--r--user-contrib/Ltac2/Constr.v51
-rw-r--r--user-contrib/Ltac2/Control.v6
-rw-r--r--user-contrib/Ltac2/Env.v2
-rw-r--r--user-contrib/Ltac2/Ind.v45
-rw-r--r--user-contrib/Ltac2/Init.v3
-rw-r--r--user-contrib/Ltac2/Ltac1.v3
-rw-r--r--user-contrib/Ltac2/Ltac2.v1
-rw-r--r--user-contrib/Ltac2/g_ltac2.mlg40
-rw-r--r--user-contrib/Ltac2/tac2core.ml91
-rw-r--r--user-contrib/Ltac2/tac2entries.ml101
-rw-r--r--user-contrib/Ltac2/tac2entries.mli13
-rw-r--r--user-contrib/Ltac2/tac2env.ml18
-rw-r--r--user-contrib/Ltac2/tac2env.mli11
-rw-r--r--user-contrib/Ltac2/tac2ffi.ml1
-rw-r--r--user-contrib/Ltac2/tac2ffi.mli1
-rw-r--r--user-contrib/Ltac2/tac2intern.ml52
17 files changed, 361 insertions, 80 deletions
diff --git a/user-contrib/Ltac2/Array.v b/user-contrib/Ltac2/Array.v
index 5adba829c5..b5e7f37c9f 100644
--- a/user-contrib/Ltac2/Array.v
+++ b/user-contrib/Ltac2/Array.v
@@ -70,7 +70,7 @@ Ltac2 init (l : int) (f : int->'a) :=
| true => empty ()
| false =>
let arr:=make l (f 0) in
- init_aux arr 0 (length arr) f;
+ init_aux arr 1 (Int.sub l 1) f;
arr
end.
diff --git a/user-contrib/Ltac2/Constr.v b/user-contrib/Ltac2/Constr.v
index 72cac900cd..fa056910b8 100644
--- a/user-contrib/Ltac2/Constr.v
+++ b/user-contrib/Ltac2/Constr.v
@@ -96,3 +96,54 @@ Ltac2 @ external in_context : ident -> constr -> (unit -> unit) -> constr := "lt
Ltac2 @ external pretype : preterm -> constr := "ltac2" "constr_pretype".
(** Pretype the provided preterm. Assumes the goal to be focussed. *)
+
+
+Ltac2 is_evar(c: constr) :=
+ match Unsafe.kind c with
+ | Unsafe.Evar _ _ => true
+ | _ => false
+ end.
+
+Ltac2 @ external has_evar : constr -> bool := "ltac2" "constr_has_evar".
+
+Ltac2 is_var(c: constr) :=
+ match Unsafe.kind c with
+ | Unsafe.Var _ => true
+ | _ => false
+ end.
+
+Ltac2 is_fix(c: constr) :=
+ match Unsafe.kind c with
+ | Unsafe.Fix _ _ _ _ => true
+ | _ => false
+ end.
+
+Ltac2 is_cofix(c: constr) :=
+ match Unsafe.kind c with
+ | Unsafe.CoFix _ _ _ => true
+ | _ => false
+ end.
+
+Ltac2 is_ind(c: constr) :=
+ match Unsafe.kind c with
+ | Unsafe.Ind _ _ => true
+ | _ => false
+ end.
+
+Ltac2 is_constructor(c: constr) :=
+ match Unsafe.kind c with
+ | Unsafe.Constructor _ _ => true
+ | _ => false
+ end.
+
+Ltac2 is_proj(c: constr) :=
+ match Unsafe.kind c with
+ | Unsafe.Proj _ _ => true
+ | _ => false
+ end.
+
+Ltac2 is_const(c: constr) :=
+ match Unsafe.kind c with
+ | Unsafe.Constant _ _ => true
+ | _ => false
+ end.
diff --git a/user-contrib/Ltac2/Control.v b/user-contrib/Ltac2/Control.v
index 8b9d53a433..31c8871ff8 100644
--- a/user-contrib/Ltac2/Control.v
+++ b/user-contrib/Ltac2/Control.v
@@ -98,6 +98,12 @@ Ltac2 assert_bounds (msg : string) (test : bool) :=
| false => throw_out_of_bounds msg
end.
+Ltac2 assert_true b :=
+ if b then () else throw Assertion_failure.
+
+Ltac2 assert_false b :=
+ if b then throw Assertion_failure else ().
+
(** Short form backtracks *)
Ltac2 backtrack_tactic_failure (msg : string) :=
diff --git a/user-contrib/Ltac2/Env.v b/user-contrib/Ltac2/Env.v
index d7c5e693f6..9ab95e6d03 100644
--- a/user-contrib/Ltac2/Env.v
+++ b/user-contrib/Ltac2/Env.v
@@ -16,7 +16,7 @@ Ltac2 @ external get : ident list -> Std.reference option := "ltac2" "env_get".
Ltac2 @ external expand : ident list -> Std.reference list := "ltac2" "env_expand".
(** Returns the list of all global references whose absolute name contains
- the argument list as a prefix. *)
+ the argument list as a suffix. *)
Ltac2 @ external path : Std.reference -> ident list := "ltac2" "env_path".
(** Returns the absolute name of the given reference. Panics if the reference
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/Init.v b/user-contrib/Ltac2/Init.v
index 097a0ca25f..19c89d7266 100644
--- a/user-contrib/Ltac2/Init.v
+++ b/user-contrib/Ltac2/Init.v
@@ -80,3 +80,6 @@ Ltac2 Type exn ::= [ Invalid_argument (message option) ].
Ltac2 Type exn ::= [ Tactic_failure (message option) ].
(** Generic error for tactic failure. *)
+
+Ltac2 Type exn ::= [ Assertion_failure ].
+(** Used to indicate that an Ltac2 function ran into a situation that should never occcur. *)
diff --git a/user-contrib/Ltac2/Ltac1.v b/user-contrib/Ltac2/Ltac1.v
index fd1555c2fb..0f7167939b 100644
--- a/user-contrib/Ltac2/Ltac1.v
+++ b/user-contrib/Ltac2/Ltac1.v
@@ -40,5 +40,8 @@ Ltac2 @ external apply : t -> t list -> (t -> unit) -> unit := "ltac2" "ltac1_ap
Ltac2 @ external of_constr : constr -> t := "ltac2" "ltac1_of_constr".
Ltac2 @ external to_constr : t -> constr option := "ltac2" "ltac1_to_constr".
+Ltac2 @ external of_ident : ident -> t := "ltac2" "ltac1_of_ident".
+Ltac2 @ external to_ident : t -> ident option := "ltac2" "ltac1_to_ident".
+
Ltac2 @ external of_list : t list -> t := "ltac2" "ltac1_of_list".
Ltac2 @ external to_list : t -> t list option := "ltac2" "ltac1_to_list".
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/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg
index 548e12d611..4ef5c1a918 100644
--- a/user-contrib/Ltac2/g_ltac2.mlg
+++ b/user-contrib/Ltac2/g_ltac2.mlg
@@ -99,6 +99,15 @@ let pattern_of_qualid qid =
else
CErrors.user_err ?loc:qid.CAst.loc (Pp.str "Syntax error")
+let opt_fun ?loc args ty e =
+ let e = match ty with
+ | None -> e
+ | Some ty -> CAst.make ?loc:e.CAst.loc (CTacCnv (e, ty))
+ in
+ match args with
+ | [] -> e
+ | _ :: _ -> CAst.make ?loc (CTacFun (args, e))
+
}
GRAMMAR EXTEND Gram
@@ -138,8 +147,8 @@ GRAMMAR EXTEND Gram
[ "6" RIGHTA
[ e1 = SELF; ";"; e2 = SELF -> { CAst.make ~loc @@ CTacSeq (e1, e2) } ]
| "5"
- [ "fun"; it = LIST1 input_fun ; "=>"; body = ltac2_expr LEVEL "6" ->
- { CAst.make ~loc @@ CTacFun (it, body) }
+ [ "fun"; it = LIST1 input_fun; ty = type_cast; "=>"; body = ltac2_expr LEVEL "6" ->
+ { opt_fun ~loc it ty body }
| "let"; isrec = rec_flag;
lc = LIST1 let_clause SEP "with"; "in";
e = ltac2_expr LEVEL "6" ->
@@ -236,22 +245,24 @@ GRAMMAR EXTEND Gram
| tac = ltac2_expr -> { [], tac }
] ]
;
+ type_cast:
+ [ [ -> { None }
+ | ":"; ty = ltac2_type -> { Some ty }
+ ] ]
+ ;
let_clause:
- [ [ binder = let_binder; ":="; te = ltac2_expr ->
+ [ [ binder = let_binder; ty = type_cast; ":="; te = ltac2_expr ->
{ let (pat, fn) = binder in
- let te = match fn with
- | None -> te
- | Some args -> CAst.make ~loc @@ CTacFun (args, te)
- in
+ let te = opt_fun ~loc fn ty te in
(pat, te) }
] ]
;
let_binder:
[ [ pats = LIST1 input_fun ->
{ match pats with
- | [{CAst.v=CPatVar _} as pat] -> (pat, None)
- | ({CAst.v=CPatVar (Name id)} as pat) :: args -> (pat, Some args)
- | [pat] -> (pat, None)
+ | [{CAst.v=CPatVar _} as pat] -> (pat, [])
+ | ({CAst.v=CPatVar (Name id)} as pat) :: args -> (pat, args)
+ | [pat] -> (pat, [])
| _ -> CErrors.user_err ~loc (str "Invalid pattern") }
] ]
;
@@ -287,9 +298,8 @@ GRAMMAR EXTEND Gram
[ [ b = tac2pat LEVEL "0" -> { b } ] ]
;
tac2def_body:
- [ [ name = binder; it = LIST0 input_fun; ":="; e = ltac2_expr ->
- { let e = if List.is_empty it then e else CAst.make ~loc @@ CTacFun (it, e) in
- (name, e) }
+ [ [ name = binder; it = LIST0 input_fun; ty = type_cast; ":="; e = ltac2_expr ->
+ { (name, opt_fun ~loc it ty e) }
] ]
;
tac2def_val:
@@ -905,8 +915,8 @@ let classify_ltac2 = function
}
VERNAC COMMAND EXTEND VernacDeclareTactic2Definition
-| #[ local = locality ] [ "Ltac2" ltac2_entry(e) ] => { classify_ltac2 e } -> {
- Tac2entries.register_struct ?local e
+| #[ deprecation = deprecation; local = locality ] [ "Ltac2" ltac2_entry(e) ] => { classify_ltac2 e } -> {
+ Tac2entries.register_struct ?deprecation ?local e
}
| ![proof_opt_query] [ "Ltac2" "Eval" ltac2_expr(e) ] => { Vernacextend.classify_as_sideeff } -> {
fun ~pstate -> Tac2entries.perform_eval ~pstate e
diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index c299562194..4758ecf5bd 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -755,6 +755,12 @@ let () = define1 "constr_binder_type" (repr_ext val_binder) begin fun (bnd, ty)
return (of_constr ty)
end
+let () = define1 "constr_has_evar" constr begin fun c ->
+ Proofview.tclEVARMAP >>= fun sigma ->
+ let b = Evarutil.has_undefined_evars sigma c in
+ Proofview.tclUNIT (Value.of_bool b)
+end
+
(** Patterns *)
let empty_context = EConstr.mkMeta Constr_matching.special_meta
@@ -1075,6 +1081,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
@@ -1132,6 +1186,16 @@ let () = define1 "ltac1_to_constr" ltac1 begin fun v ->
return (Value.of_option Value.of_constr (Tacinterp.Value.to_constr v))
end
+let () = define1 "ltac1_of_ident" ident begin fun c ->
+ let open Ltac_plugin in
+ return (Value.of_ext val_ltac1 (Taccoerce.Value.of_ident c))
+end
+
+let () = define1 "ltac1_to_ident" ltac1 begin fun v ->
+ let open Ltac_plugin in
+ return (Value.of_option Value.of_ident (Taccoerce.Value.to_ident v))
+end
+
let () = define1 "ltac1_of_list" (list ltac1) begin fun l ->
let open Geninterp.Val in
return (Value.of_ext val_ltac1 (inject (Base typ_list) l))
@@ -1388,24 +1452,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..7af530ab0f 100644
--- a/user-contrib/Ltac2/tac2entries.ml
+++ b/user-contrib/Ltac2/tac2entries.ml
@@ -50,6 +50,12 @@ let q_pose = Pcoq.Entry.create "q_pose"
let q_assert = Pcoq.Entry.create "q_assert"
end
+let () =
+ let entries = [
+ Pcoq.AnyEntry Pltac.ltac2_expr;
+ ] in
+ Pcoq.register_grammars_by_name "ltac2" entries
+
(** Tactic definition *)
type tacdef = {
@@ -57,6 +63,7 @@ type tacdef = {
tacdef_mutable : bool;
tacdef_expr : glb_tacexpr;
tacdef_type : type_scheme;
+ tacdef_deprecation : Deprecation.t option;
}
let perform_tacdef visibility ((sp, kn), def) =
@@ -65,6 +72,7 @@ let perform_tacdef visibility ((sp, kn), def) =
Tac2env.gdata_expr = def.tacdef_expr;
gdata_type = def.tacdef_type;
gdata_mutable = def.tacdef_mutable;
+ gdata_deprecation = def.tacdef_deprecation;
} in
Tac2env.define_global kn data
@@ -77,6 +85,7 @@ let cache_tacdef ((sp, kn), def) =
Tac2env.gdata_expr = def.tacdef_expr;
gdata_type = def.tacdef_type;
gdata_mutable = def.tacdef_mutable;
+ gdata_deprecation = def.tacdef_deprecation;
} in
Tac2env.define_global kn data
@@ -322,7 +331,7 @@ let check_lowercase {loc;v=id} =
if Tac2env.is_constructor (Libnames.qualid_of_ident id) then
user_err ?loc (str "The identifier " ++ Id.print id ++ str " must be lowercase")
-let register_ltac ?(local = false) ?(mut = false) isrec tactics =
+let register_ltac ?deprecation ?(local = false) ?(mut = false) isrec tactics =
let map ({loc;v=na}, e) =
let id = match na with
| Anonymous ->
@@ -359,6 +368,7 @@ let register_ltac ?(local = false) ?(mut = false) isrec tactics =
tacdef_mutable = mut;
tacdef_expr = e;
tacdef_type = t;
+ tacdef_deprecation = deprecation;
} in
ignore (Lib.add_leaf id (inTacDef def))
in
@@ -377,9 +387,9 @@ let register_typedef ?(local = false) isrec types =
in
let () =
let check_existing_type ({v=id},_) =
- let qid = Libnames.make_qualid (Lib.current_dirpath false) id in
- try let _ = Tac2env.locate_type qid in
- user_err (str "Multiple definition of the type name " ++ pr_qualid qid)
+ let (_, kn) = Lib.make_foname id in
+ try let _ = Tac2env.interp_type kn in
+ user_err (str "Multiple definition of the type name " ++ Id.print id)
with Not_found -> ()
in
List.iter check_existing_type types
@@ -413,9 +423,10 @@ let register_typedef ?(local = false) isrec types =
in
let () =
let check_existing_ctor (id, _) =
- let qid = Libnames.make_qualid (Lib.current_dirpath false) id in
- if Tac2env.mem_constructor qid
- then user_err (str "Constructor already defined in this module " ++ pr_qualid qid)
+ let (_, kn) = Lib.make_foname id in
+ try let _ = Tac2env.interp_constructor kn in
+ user_err (str "Constructor already defined in this module " ++ Id.print id)
+ with Not_found -> ()
in
List.iter check_existing_ctor cs
in
@@ -453,7 +464,7 @@ let register_typedef ?(local = false) isrec types =
let iter (id, def) = ignore (Lib.add_leaf id (inTypDef def)) in
List.iter iter types
-let register_primitive ?(local = false) {loc;v=id} t ml =
+let register_primitive ?deprecation ?(local = false) {loc;v=id} t ml =
let t = intern_open_type t in
let rec count_arrow = function
| GTypArrow (_, t) -> 1 + count_arrow t
@@ -477,6 +488,7 @@ let register_primitive ?(local = false) {loc;v=id} t ml =
tacdef_mutable = false;
tacdef_expr = e;
tacdef_type = t;
+ tacdef_deprecation = deprecation;
} in
ignore (Lib.add_leaf id (inTacDef def))
@@ -507,9 +519,10 @@ let register_open ?(local = false) qid (params, def) =
user_err (str "Multiple definitions of the constructor " ++ Id.print id)
in
let check_existing_ctor (id, _) =
- let qid = Libnames.make_qualid (Lib.current_dirpath false) id in
- if Tac2env.mem_constructor qid
- then user_err (str "Constructor already defined in this module " ++ pr_qualid qid)
+ let (_, kn) = Lib.make_foname id in
+ try let _ = Tac2env.interp_constructor kn in
+ user_err (str "Constructor already defined in this module " ++ Id.print id)
+ with Not_found -> ()
in
let () = List.iter check_existing_ctor def in
()
@@ -599,6 +612,18 @@ let parse_token = function
let loc = loc_of_token tok in
CErrors.user_err ?loc (str "Invalid parsing token")
+let rec print_scope = function
+| SexprStr s -> str s.CAst.v
+| SexprInt i -> int i.CAst.v
+| SexprRec (_, {v=na}, []) -> Option.cata Id.print (str "_") na
+| SexprRec (_, {v=na}, e) ->
+ Option.cata Id.print (str "_") na ++ str "(" ++ pr_sequence print_scope e ++ str ")"
+
+let print_token = function
+| SexprStr {v=s} -> quote (str s)
+| SexprRec (_, {v=na}, [tok]) -> print_scope tok
+| _ -> assert false
+
end
let parse_scope = ParseToken.parse_scope
@@ -608,6 +633,7 @@ type synext = {
synext_exp : raw_tacexpr;
synext_lev : int option;
synext_loc : bool;
+ synext_depr : Deprecation.t option;
}
type krule =
@@ -628,10 +654,20 @@ let rec get_rule (tok : scope_rule token list) : krule = match tok with
let act k _ = act k in
KRule (rule, act)
+let deprecated_ltac2_notation =
+ Deprecation.create_warning
+ ~object_name:"Ltac2 notation"
+ ~warning_name:"deprecated-ltac2-notation"
+ (fun (toks : sexpr list) -> pr_sequence ParseToken.print_token toks)
+
let perform_notation syn st =
let tok = List.rev_map ParseToken.parse_token syn.synext_tok in
let KRule (rule, act) = get_rule tok in
let mk loc args =
+ let () = match syn.synext_depr with
+ | None -> ()
+ | Some depr -> deprecated_ltac2_notation ~loc (syn.synext_tok, depr)
+ in
let map (na, e) =
((CAst.make ?loc:e.loc @@ CPatVar na), e)
in
@@ -671,23 +707,24 @@ let inTac2Notation : synext -> obj =
type abbreviation = {
abbr_body : raw_tacexpr;
+ abbr_depr : Deprecation.t option;
}
let perform_abbreviation visibility ((sp, kn), abbr) =
let () = Tac2env.push_ltac visibility sp (TacAlias kn) in
- Tac2env.define_alias kn abbr.abbr_body
+ Tac2env.define_alias ?deprecation:abbr.abbr_depr kn abbr.abbr_body
let load_abbreviation i obj = perform_abbreviation (Until i) obj
let open_abbreviation i obj = perform_abbreviation (Exactly i) obj
let cache_abbreviation ((sp, kn), abbr) =
let () = Tac2env.push_ltac (Until 1) sp (TacAlias kn) in
- Tac2env.define_alias kn abbr.abbr_body
+ Tac2env.define_alias ?deprecation:abbr.abbr_depr kn abbr.abbr_body
let subst_abbreviation (subst, abbr) =
let body' = subst_rawexpr subst abbr.abbr_body in
if body' == abbr.abbr_body then abbr
- else { abbr_body = body' }
+ else { abbr_body = body'; abbr_depr = abbr.abbr_depr }
let classify_abbreviation o = Substitute o
@@ -699,12 +736,12 @@ let inTac2Abbreviation : abbreviation -> obj =
subst_function = subst_abbreviation;
classify_function = classify_abbreviation}
-let register_notation ?(local = false) tkn lev body = match tkn, lev with
+let register_notation ?deprecation ?(local = false) tkn lev body = match tkn, lev with
| [SexprRec (_, {loc;v=Some id}, [])], None ->
(* Tactic abbreviation *)
let () = check_lowercase CAst.(make ?loc id) in
let body = Tac2intern.globalize Id.Set.empty body in
- let abbr = { abbr_body = body } in
+ let abbr = { abbr_body = body; abbr_depr = deprecation } in
ignore (Lib.add_leaf id (inTac2Abbreviation abbr))
| _ ->
(* Check that the tokens make sense *)
@@ -723,6 +760,7 @@ let register_notation ?(local = false) tkn lev body = match tkn, lev with
synext_exp = body;
synext_lev = lev;
synext_loc = local;
+ synext_depr = deprecation;
} in
Lib.add_anonymous_leaf (inTac2Notation ext)
@@ -811,13 +849,11 @@ let perform_eval ~pstate e =
Goal_select.get_default_goal_selector (),
Declare.Proof.get pstate
in
- let v = match selector with
- | Goal_select.SelectNth i -> Proofview.tclFOCUS i i v
- | 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 **)
+ let nosuchgoal =
+ let info = Exninfo.reify () in
+ Proofview.tclZERO ~info (Proof.SuggestNoSuchGoals (1,proof))
in
+ let v = Goal_select.tclSELECT ~nosuchgoal selector v in
let (proof, _, ans) = Proof.run_tactic (Global.env ()) v proof in
let { Proof.sigma } = Proof.data proof in
let name = int_name () in
@@ -827,12 +863,21 @@ let perform_eval ~pstate e =
(** Toplevel entries *)
-let register_struct ?local str = match str with
-| StrVal (mut, isrec, e) -> register_ltac ?local ~mut isrec e
-| StrTyp (isrec, t) -> register_type ?local isrec t
-| StrPrm (id, t, ml) -> register_primitive ?local id t ml
-| StrSyn (tok, lev, e) -> register_notation ?local tok lev e
-| StrMut (qid, old, e) -> register_redefinition ?local qid old e
+let unsupported_deprecation = function
+| None -> ()
+| Some _ ->
+ Attributes.unsupported_attributes ["deprecated", Attributes.VernacFlagEmpty]
+
+let register_struct ?deprecation ?local str = match str with
+| StrVal (mut, isrec, e) -> register_ltac ?deprecation ?local ~mut isrec e
+| StrTyp (isrec, t) ->
+ let () = unsupported_deprecation deprecation in (* TODO *)
+ register_type ?local isrec t
+| StrPrm (id, t, ml) -> register_primitive ?deprecation ?local id t ml
+| StrSyn (tok, lev, e) -> register_notation ?deprecation ?local tok lev e
+| StrMut (qid, old, e) ->
+ let () = unsupported_deprecation deprecation in (* TODO: what does that mean? *)
+ register_redefinition ?local qid old e
(** Toplevel exception *)
diff --git a/user-contrib/Ltac2/tac2entries.mli b/user-contrib/Ltac2/tac2entries.mli
index 782968c6e1..a1e13b60fe 100644
--- a/user-contrib/Ltac2/tac2entries.mli
+++ b/user-contrib/Ltac2/tac2entries.mli
@@ -14,22 +14,19 @@ open Tac2expr
(** {5 Toplevel definitions} *)
-val register_ltac : ?local:bool -> ?mut:bool -> rec_flag ->
+val register_ltac : ?deprecation:Deprecation.t -> ?local:bool -> ?mut:bool -> rec_flag ->
(Names.lname * raw_tacexpr) list -> unit
val register_type : ?local:bool -> rec_flag ->
(qualid * redef_flag * raw_quant_typedef) list -> unit
-val register_primitive : ?local:bool ->
+val register_primitive : ?deprecation:Deprecation.t -> ?local:bool ->
Names.lident -> raw_typexpr -> ml_tactic_name -> unit
-val register_struct
- : ?local:bool
- -> strexpr
- -> unit
+val register_struct : ?deprecation:Deprecation.t -> ?local:bool -> strexpr -> unit
-val register_notation : ?local:bool -> sexpr list -> int option ->
- raw_tacexpr -> unit
+val register_notation : ?deprecation:Deprecation.t -> ?local:bool -> sexpr list ->
+ int option -> raw_tacexpr -> unit
val perform_eval : pstate:Declare.Proof.t option -> raw_tacexpr -> unit
diff --git a/user-contrib/Ltac2/tac2env.ml b/user-contrib/Ltac2/tac2env.ml
index 5479ba0d54..969b6c8e28 100644
--- a/user-contrib/Ltac2/tac2env.ml
+++ b/user-contrib/Ltac2/tac2env.ml
@@ -18,6 +18,7 @@ type global_data = {
gdata_expr : glb_tacexpr;
gdata_type : type_scheme;
gdata_mutable : bool;
+ gdata_deprecation : Deprecation.t option;
}
type constructor_data = {
@@ -35,12 +36,17 @@ type projection_data = {
pdata_indx : int;
}
+type alias_data = {
+ alias_body : raw_tacexpr;
+ alias_depr : Deprecation.t option;
+}
+
type ltac_state = {
ltac_tactics : global_data KNmap.t;
ltac_constructors : constructor_data KNmap.t;
ltac_projections : projection_data KNmap.t;
ltac_types : glb_quant_typedef KNmap.t;
- ltac_aliases : raw_tacexpr KNmap.t;
+ ltac_aliases : alias_data KNmap.t;
}
let empty_state = {
@@ -79,9 +85,10 @@ let define_type kn e =
let interp_type kn = KNmap.find kn ltac_state.contents.ltac_types
-let define_alias kn tac =
+let define_alias ?deprecation kn tac =
let state = !ltac_state in
- ltac_state := { state with ltac_aliases = KNmap.add kn tac state.ltac_aliases }
+ let data = { alias_body = tac; alias_depr = deprecation } in
+ ltac_state := { state with ltac_aliases = KNmap.add kn data state.ltac_aliases }
let interp_alias kn = KNmap.find kn ltac_state.contents.ltac_aliases
@@ -196,11 +203,6 @@ let shortest_qualid_of_constructor kn =
let sp = KNmap.find kn tab.tab_cstr_rev in
KnTab.shortest_qualid Id.Set.empty sp tab.tab_cstr
-let mem_constructor qid =
- let tab = !nametab in
- try ignore (KnTab.locate qid tab.tab_cstr) ; true
- with Not_found -> false
-
let push_type vis sp kn =
let tab = !nametab in
let tab_type = KnTab.push vis sp kn tab.tab_type in
diff --git a/user-contrib/Ltac2/tac2env.mli b/user-contrib/Ltac2/tac2env.mli
index 95dcdd7e1b..02b34b594e 100644
--- a/user-contrib/Ltac2/tac2env.mli
+++ b/user-contrib/Ltac2/tac2env.mli
@@ -23,6 +23,7 @@ type global_data = {
gdata_expr : glb_tacexpr;
gdata_type : type_scheme;
gdata_mutable : bool;
+ gdata_deprecation : Deprecation.t option;
}
val define_global : ltac_constant -> global_data -> unit
@@ -72,8 +73,13 @@ val interp_projection : ltac_projection -> projection_data
(** {5 Toplevel definition of aliases} *)
-val define_alias : ltac_constant -> raw_tacexpr -> unit
-val interp_alias : ltac_constant -> raw_tacexpr
+type alias_data = {
+ alias_body : raw_tacexpr;
+ alias_depr : Deprecation.t option;
+}
+
+val define_alias : ?deprecation:Deprecation.t -> ltac_constant -> raw_tacexpr -> unit
+val interp_alias : ltac_constant -> alias_data
(** {5 Name management} *)
@@ -83,7 +89,6 @@ val locate_extended_all_ltac : qualid -> tacref list
val shortest_qualid_of_ltac : tacref -> qualid
val push_constructor : visibility -> full_path -> ltac_constructor -> unit
-val mem_constructor : qualid -> bool
val locate_constructor : qualid -> ltac_constructor
val locate_extended_all_constructor : qualid -> ltac_constructor list
val shortest_qualid_of_constructor : ltac_constructor -> qualid
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]
diff --git a/user-contrib/Ltac2/tac2intern.ml b/user-contrib/Ltac2/tac2intern.ml
index ddf70a5a65..206f4df19d 100644
--- a/user-contrib/Ltac2/tac2intern.ml
+++ b/user-contrib/Ltac2/tac2intern.ml
@@ -467,7 +467,9 @@ let polymorphic ((n, t) : type_scheme) : mix_type_scheme =
let warn_not_unit =
CWarnings.create ~name:"not-unit" ~category:"ltac"
- (fun () -> strbrk "The following expression should have type unit.")
+ (fun (env, t) ->
+ strbrk "The following expression should have type unit but has type " ++
+ pr_glbtype env t ++ str ".")
let warn_redundant_clause =
CWarnings.create ~name:"redundant-clause" ~category:"ltac"
@@ -480,7 +482,7 @@ let check_elt_unit loc env t =
| GTypRef (Tuple 0, []) -> true
| GTypRef _ -> false
in
- if not maybe_unit then warn_not_unit ?loc ()
+ if not maybe_unit then warn_not_unit ?loc (env, t)
let check_elt_empty loc env t = match kind env t with
| GTypVar _ ->
@@ -504,7 +506,7 @@ let check_unit ?loc t =
| GTypRef (Tuple 0, []) -> true
| GTypRef _ -> false
in
- if not maybe_unit then warn_not_unit ?loc ()
+ if not maybe_unit then warn_not_unit ?loc (env, t)
let check_redundant_clause = function
| [] -> ()
@@ -655,6 +657,35 @@ let is_alias env qid = match get_variable env qid with
| ArgArg (TacAlias _) -> true
| ArgVar _ | (ArgArg (TacConstant _)) -> false
+let is_user_name qid = match qid with
+| AbsKn _ -> false
+| RelId _ -> true
+
+let deprecated_ltac2_alias =
+ Deprecation.create_warning
+ ~object_name:"Ltac2 alias"
+ ~warning_name:"deprecated-ltac2-alias"
+ (fun kn -> pr_qualid (Tac2env.shortest_qualid_of_ltac (TacAlias kn)))
+
+let deprecated_ltac2_def =
+ Deprecation.create_warning
+ ~object_name:"Ltac2 definition"
+ ~warning_name:"deprecated-ltac2-definition"
+ (fun kn -> pr_qualid (Tac2env.shortest_qualid_of_ltac (TacConstant kn)))
+
+let check_deprecated_ltac2 ?loc qid def =
+ if is_user_name qid then match def with
+ | TacAlias kn ->
+ begin match (Tac2env.interp_alias kn).alias_depr with
+ | None -> ()
+ | Some depr -> deprecated_ltac2_alias ?loc (kn, depr)
+ end
+ | TacConstant kn ->
+ begin match (Tac2env.interp_global kn).gdata_deprecation with
+ | None -> ()
+ | Some depr -> deprecated_ltac2_def ?loc (kn, depr)
+ end
+
let rec intern_rec env {loc;v=e} = match e with
| CTacAtm atm -> intern_atm env atm
| CTacRef qid ->
@@ -663,11 +694,12 @@ let rec intern_rec env {loc;v=e} = match e with
let sch = Id.Map.find id env.env_var in
(GTacVar id, fresh_mix_type_scheme env sch)
| ArgArg (TacConstant kn) ->
- let { Tac2env.gdata_type = sch } =
+ let { Tac2env.gdata_type = sch; gdata_deprecation = depr } =
try Tac2env.interp_global kn
with Not_found ->
CErrors.anomaly (str "Missing hardwired primitive " ++ KerName.print kn)
in
+ let () = check_deprecated_ltac2 ?loc qid (TacConstant kn) in
(GTacRef kn, fresh_type_scheme env sch)
| ArgArg (TacAlias kn) ->
let e =
@@ -675,7 +707,8 @@ let rec intern_rec env {loc;v=e} = match e with
with Not_found ->
CErrors.anomaly (str "Missing hardwired alias " ++ KerName.print kn)
in
- intern_rec env e
+ let () = check_deprecated_ltac2 ?loc qid (TacAlias kn) in
+ intern_rec env e.alias_body
end
| CTacCst qid ->
let kn = get_constructor env qid in
@@ -695,12 +728,13 @@ let rec intern_rec env {loc;v=e} = match e with
| CTacApp ({loc;v=CTacCst qid}, args) ->
let kn = get_constructor env qid in
intern_constructor env loc kn args
-| CTacApp ({v=CTacRef qid}, args) when is_alias env qid ->
+| CTacApp ({v=CTacRef qid; loc=aloc}, args) when is_alias env qid ->
let kn = match get_variable env qid with
| ArgArg (TacAlias kn) -> kn
| ArgVar _ | (ArgArg (TacConstant _)) -> assert false
in
let e = Tac2env.interp_alias kn in
+ let () = check_deprecated_ltac2 ?loc:aloc qid (TacAlias kn) in
let map arg =
(* Thunk alias arguments *)
let loc = arg.loc in
@@ -709,7 +743,7 @@ let rec intern_rec env {loc;v=e} = match e with
CAst.make ?loc @@ CTacFun ([var], arg)
in
let args = List.map map args in
- intern_rec env (CAst.make ?loc @@ CTacApp (e, args))
+ intern_rec env (CAst.make ?loc @@ CTacApp (e.alias_body, args))
| CTacApp (f, args) ->
let loc = f.loc in
let (f, ft) = intern_rec env f in
@@ -1243,7 +1277,9 @@ let rec globalize ids ({loc;v=er} as e) = match er with
let mem id = Id.Set.mem id ids in
begin match get_variable0 mem ref with
| ArgVar _ -> e
- | ArgArg kn -> CAst.make ?loc @@ CTacRef (AbsKn kn)
+ | ArgArg kn ->
+ let () = check_deprecated_ltac2 ?loc ref kn in
+ CAst.make ?loc @@ CTacRef (AbsKn kn)
end
| CTacCst qid ->
let knc = get_constructor () qid in
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:03:36 +0000