aboutsummaryrefslogtreecommitdiff
path: root/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'ltac')
-rw-r--r--ltac/evar_tactics.ml2
-rw-r--r--ltac/extraargs.ml42
-rw-r--r--ltac/extratactics.ml445
-rw-r--r--ltac/g_class.ml414
-rw-r--r--ltac/g_ltac.ml42
-rw-r--r--ltac/g_rewrite.ml426
-rw-r--r--ltac/ltac.mllib1
-rw-r--r--ltac/profile_ltac.ml535
-rw-r--r--ltac/profile_ltac.mli43
-rw-r--r--ltac/profile_ltac_tactics.ml43
-rw-r--r--ltac/rewrite.ml161
-rw-r--r--ltac/rewrite.mli4
-rw-r--r--ltac/taccoerce.ml344
-rw-r--r--ltac/taccoerce.mli96
-rw-r--r--ltac/tacentries.ml8
-rw-r--r--ltac/tacenv.ml6
-rw-r--r--ltac/tacintern.ml8
-rw-r--r--ltac/tacinterp.ml19
-rw-r--r--ltac/tactic_debug.ml7
19 files changed, 911 insertions, 415 deletions
diff --git a/ltac/evar_tactics.ml b/ltac/evar_tactics.ml
index 2e0996bf5a..30aeba3bbc 100644
--- a/ltac/evar_tactics.ml
+++ b/ltac/evar_tactics.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Util
-open Errors
+open CErrors
open Evar_refiner
open Tacmach
open Tacexpr
diff --git a/ltac/extraargs.ml4 b/ltac/extraargs.ml4
index 8185a14d99..c6d72e03e2 100644
--- a/ltac/extraargs.ml4
+++ b/ltac/extraargs.ml4
@@ -90,7 +90,7 @@ let occurrences_of = function
| n::_ as nl when n < 0 -> AllOccurrencesBut (List.map abs nl)
| nl ->
if List.exists (fun n -> n < 0) nl then
- Errors.error "Illegal negative occurrence number.";
+ CErrors.error "Illegal negative occurrence number.";
OnlyOccurrences nl
let coerce_to_int v = match Value.to_int v with
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index 725f2a5342..e50b0520bc 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -19,7 +19,7 @@ open Mod_subst
open Names
open Tacexpr
open Glob_ops
-open Errors
+open CErrors
open Util
open Evd
open Termops
@@ -337,11 +337,18 @@ END
(**********************************************************************)
(* Refine *)
+let constr_flags = {
+ Pretyping.use_typeclasses = true;
+ Pretyping.use_unif_heuristics = true;
+ Pretyping.use_hook = Some Pfedit.solve_by_implicit_tactic;
+ Pretyping.fail_evar = false;
+ Pretyping.expand_evars = true }
+
let refine_tac ist simple c =
Proofview.Goal.nf_enter { enter = begin fun gl ->
let concl = Proofview.Goal.concl gl in
let env = Proofview.Goal.env gl in
- let flags = Pretyping.all_no_fail_flags in
+ let flags = constr_flags in
let expected_type = Pretyping.OfType concl in
let c = Pretyping.type_uconstr ~flags ~expected_type ist c in
let update = { run = fun sigma -> c.delayed env sigma } in
@@ -517,11 +524,29 @@ VERNAC COMMAND EXTEND AddStepr CLASSIFIED AS SIDEFF
[ add_transitivity_lemma false t ]
END
+let cache_implicit_tactic (_,tac) = match tac with
+ | Some tac -> Pfedit.declare_implicit_tactic (Tacinterp.eval_tactic tac)
+ | None -> Pfedit.clear_implicit_tactic ()
+
+let subst_implicit_tactic (subst,tac) =
+ Option.map (Tacsubst.subst_tactic subst) tac
+
+let inImplicitTactic : glob_tactic_expr option -> obj =
+ declare_object {(default_object "IMPLICIT-TACTIC") with
+ open_function = (fun i o -> if Int.equal i 1 then cache_implicit_tactic o);
+ cache_function = cache_implicit_tactic;
+ subst_function = subst_implicit_tactic;
+ classify_function = (fun o -> Dispose)}
+
+let declare_implicit_tactic tac =
+ Lib.add_anonymous_leaf (inImplicitTactic (Some (Tacintern.glob_tactic tac)))
+
+let clear_implicit_tactic () =
+ Lib.add_anonymous_leaf (inImplicitTactic None)
+
VERNAC COMMAND EXTEND ImplicitTactic CLASSIFIED AS SIDEFF
-| [ "Declare" "Implicit" "Tactic" tactic(tac) ] ->
- [ Pfedit.declare_implicit_tactic (Tacinterp.interp tac) ]
-| [ "Clear" "Implicit" "Tactic" ] ->
- [ Pfedit.clear_implicit_tactic () ]
+| [ "Declare" "Implicit" "Tactic" tactic(tac) ] -> [ declare_implicit_tactic tac ]
+| [ "Clear" "Implicit" "Tactic" ] -> [ clear_implicit_tactic () ]
END
@@ -622,7 +647,7 @@ let hResolve id c occ t =
Pretyping.understand env sigma t_hole
with
| Pretype_errors.PretypeError (_,_,Pretype_errors.UnsolvableImplicit _) as e ->
- let (e, info) = Errors.push e in
+ let (e, info) = CErrors.push e in
let loc = match Loc.get_loc info with None -> Loc.ghost | Some loc -> loc in
resolve_hole (subst_hole_with_term (fst (Loc.unloc loc)) c_raw t_hole)
in
@@ -641,7 +666,7 @@ let hResolve_auto id c t =
hResolve id c n t
with
| UserError _ as e -> raise e
- | e when Errors.noncritical e -> resolve_auto (n+1)
+ | e when CErrors.noncritical e -> resolve_auto (n+1)
in
resolve_auto 1
@@ -791,9 +816,11 @@ END
TACTIC EXTEND is_evar
| [ "is_evar" constr(x) ] ->
- [ match kind_of_term x with
+ [ Proofview.tclBIND Proofview.tclEVARMAP begin fun sigma ->
+ match Evarutil.kind_of_term_upto sigma x with
| Evar _ -> Proofview.tclUNIT ()
| _ -> Tacticals.New.tclFAIL 0 (str "Not an evar")
+ end
]
END
diff --git a/ltac/g_class.ml4 b/ltac/g_class.ml4
index eaa6aad4f6..18df596eb8 100644
--- a/ltac/g_class.ml4
+++ b/ltac/g_class.ml4
@@ -44,18 +44,10 @@ ARGUMENT EXTEND debug TYPED AS bool PRINTED BY pr_debug
| [ ] -> [ false ]
END
-let pr_depth _prc _prlc _prt = function
- Some i -> Pp.int i
- | None -> Pp.mt()
-
-ARGUMENT EXTEND depth TYPED AS int option PRINTED BY pr_depth
- | [ int_or_var_opt(v) ] -> [ match v with Some (ArgArg i) -> Some i | _ -> None ]
-END
-
(* true = All transparent, false = Opaque if possible *)
VERNAC COMMAND EXTEND Typeclasses_Settings CLASSIFIED AS SIDEFF
- | [ "Typeclasses" "eauto" ":=" debug(d) depth(depth) ] -> [
+ | [ "Typeclasses" "eauto" ":=" debug(d) int_opt(depth) ] -> [
set_typeclasses_debug d;
set_typeclasses_depth depth
]
@@ -63,9 +55,9 @@ END
(** Compatibility: typeclasses eauto has 8.5 and 8.6 modes *)
TACTIC EXTEND typeclasses_eauto
- | [ "typeclasses" "eauto" depth(d) "with" ne_preident_list(l) ] ->
+ | [ "typeclasses" "eauto" int_or_var_opt(d) "with" ne_preident_list(l) ] ->
[ typeclasses_eauto d l ]
- | [ "typeclasses" "eauto" depth(d) ] -> [
+ | [ "typeclasses" "eauto" int_or_var_opt(d) ] -> [
typeclasses_eauto ~only_classes:true ~depth:d [Hints.typeclasses_db] ]
END
diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4
index fbeb89a634..a3ca4ebc4a 100644
--- a/ltac/g_ltac.ml4
+++ b/ltac/g_ltac.ml4
@@ -36,7 +36,7 @@ let genarg_of_uconstr c = in_gen (rawwit Constrarg.wit_uconstr) c
let reference_to_id = function
| Libnames.Ident (loc, id) -> (loc, id)
| Libnames.Qualid (loc,_) ->
- Errors.user_err_loc (loc, "",
+ CErrors.user_err_loc (loc, "",
str "This expression should be a simple identifier.")
let tactic_mode = Gram.entry_create "vernac:tactic_command"
diff --git a/ltac/g_rewrite.ml4 b/ltac/g_rewrite.ml4
index 7a20975158..82b79c883d 100644
--- a/ltac/g_rewrite.ml4
+++ b/ltac/g_rewrite.ml4
@@ -106,17 +106,11 @@ END
let db_strat db = StratUnary (Topdown, StratHints (false, db))
let cl_rewrite_clause_db db = cl_rewrite_clause_strat (strategy_of_ast (db_strat db))
-let cl_rewrite_clause_db =
- if Flags.profile then
- let key = Profile.declare_profile "cl_rewrite_clause_db" in
- Profile.profile3 key cl_rewrite_clause_db
- else cl_rewrite_clause_db
-
TACTIC EXTEND rewrite_strat
-| [ "rewrite_strat" rewstrategy(s) "in" hyp(id) ] -> [ Proofview.V82.tactic (cl_rewrite_clause_strat s (Some id)) ]
-| [ "rewrite_strat" rewstrategy(s) ] -> [ Proofview.V82.tactic (cl_rewrite_clause_strat s None) ]
-| [ "rewrite_db" preident(db) "in" hyp(id) ] -> [ Proofview.V82.tactic (cl_rewrite_clause_db db (Some id)) ]
-| [ "rewrite_db" preident(db) ] -> [ Proofview.V82.tactic (cl_rewrite_clause_db db None) ]
+| [ "rewrite_strat" rewstrategy(s) "in" hyp(id) ] -> [ cl_rewrite_clause_strat s (Some id) ]
+| [ "rewrite_strat" rewstrategy(s) ] -> [ cl_rewrite_clause_strat s None ]
+| [ "rewrite_db" preident(db) "in" hyp(id) ] -> [ cl_rewrite_clause_db db (Some id) ]
+| [ "rewrite_db" preident(db) ] -> [ cl_rewrite_clause_db db None ]
END
let clsubstitute o c =
@@ -125,7 +119,7 @@ let clsubstitute o c =
(fun cl ->
match cl with
| Some id when is_tac id -> tclIDTAC
- | _ -> cl_rewrite_clause c o AllOccurrences cl)
+ | _ -> Proofview.V82.of_tactic (cl_rewrite_clause c o AllOccurrences cl))
TACTIC EXTEND substitute
| [ "substitute" orient(o) glob_constr_with_bindings(c) ] -> [ Proofview.V82.tactic (clsubstitute o c) ]
@@ -136,15 +130,15 @@ END
TACTIC EXTEND setoid_rewrite
[ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) ]
- -> [ Proofview.V82.tactic (cl_rewrite_clause c o AllOccurrences None) ]
+ -> [ cl_rewrite_clause c o AllOccurrences None ]
| [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) "in" hyp(id) ] ->
- [ Proofview.V82.tactic (cl_rewrite_clause c o AllOccurrences (Some id))]
+ [ cl_rewrite_clause c o AllOccurrences (Some id) ]
| [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) "at" occurrences(occ) ] ->
- [ Proofview.V82.tactic (cl_rewrite_clause c o (occurrences_of occ) None)]
+ [ cl_rewrite_clause c o (occurrences_of occ) None ]
| [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) "at" occurrences(occ) "in" hyp(id)] ->
- [ Proofview.V82.tactic (cl_rewrite_clause c o (occurrences_of occ) (Some id))]
+ [ cl_rewrite_clause c o (occurrences_of occ) (Some id) ]
| [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) "in" hyp(id) "at" occurrences(occ)] ->
- [ Proofview.V82.tactic (cl_rewrite_clause c o (occurrences_of occ) (Some id))]
+ [ cl_rewrite_clause c o (occurrences_of occ) (Some id) ]
END
VERNAC COMMAND EXTEND AddRelation CLASSIFIED AS SIDEFF
diff --git a/ltac/ltac.mllib b/ltac/ltac.mllib
index 65ed114cff..fc51e48ae4 100644
--- a/ltac/ltac.mllib
+++ b/ltac/ltac.mllib
@@ -1,3 +1,4 @@
+Taccoerce
Tacsubst
Tacenv
Tactic_debug
diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml
index f332e1a0d5..102918e5e5 100644
--- a/ltac/profile_ltac.ml
+++ b/ltac/profile_ltac.ml
@@ -11,6 +11,8 @@ open Pp
open Printer
open Util
+module M = CString.Map
+
(** [is_profiling] and the profiling info ([stack]) should be synchronized with
the document; the rest of the ref cells are either local to individual
tactic invocations, or global flags, and need not be synchronized, since no
@@ -21,10 +23,6 @@ let is_profiling = Flags.profile_ltac
let set_profiling b = is_profiling := b
let get_profiling () = !is_profiling
-let new_call = ref false
-let entered_call () = new_call := true
-let is_new_call () = let b = !new_call in new_call := false; b
-
(** LtacProf cannot yet handle backtracking into multi-success tactics.
To properly support this, we'd have to somehow recreate our location in the
call-stack, and stop/restart the intervening timers. This is tricky and
@@ -35,7 +33,7 @@ let encountered_multi_success_backtracking = ref false
let warn_profile_backtracking =
CWarnings.create ~name:"profile-backtracking" ~category:"ltac"
(fun () -> strbrk "Ltac Profiler cannot yet handle backtracking \
- into multi-success tactics; profiling results may be wildly inaccurate.")
+ into multi-success tactics; profiling results may be wildly inaccurate.")
let warn_encountered_multi_success_backtracking () =
if !encountered_multi_success_backtracking then
@@ -48,164 +46,92 @@ let encounter_multi_success_backtracking () =
warn_encountered_multi_success_backtracking ()
end
-type entry = {
- mutable total : float;
- mutable local : float;
- mutable ncalls : int;
- mutable max_total : float
-}
-
-let empty_entry () = { total = 0.; local = 0.; ncalls = 0; max_total = 0. }
-let add_entry e add_total { total; local; ncalls; max_total } =
- if add_total then e.total <- e.total +. total;
- e.local <- e.local +. local;
- e.ncalls <- e.ncalls + ncalls;
- if add_total then e.max_total <- max e.max_total max_total
+(* *************** tree data structure for profiling ****************** *)
type treenode = {
- entry : entry;
- children : (string, treenode) Hashtbl.t
+ name : M.key;
+ total : float;
+ local : float;
+ ncalls : int;
+ max_total : float;
+ children : treenode M.t
}
-let empty_treenode n = { entry = empty_entry (); children = Hashtbl.create n }
-
-(** Tobias Tebbi wrote some tricky code involving mutation. Rather than
- rewriting it in a functional style, we simply freeze the state when we need
- to by issuing a deep copy of the profiling data. *)
-(** TODO: rewrite me in purely functional style *)
-let deepcopy_entry { total; local; ncalls; max_total } =
- { total; local; ncalls; max_total }
-
-let rec deepcopy_treenode { entry; children } =
- let children' = Hashtbl.create (Hashtbl.length children) in
- let iter key subtree = Hashtbl.add children' key (deepcopy_treenode subtree) in
- let () = Hashtbl.iter iter children in
- { entry = deepcopy_entry entry; children = children' }
-
-let stack =
- let freeze _ = List.map deepcopy_treenode in
- Summary.ref ~freeze [empty_treenode 20] ~name:"LtacProf-stack"
-
-let on_stack = Hashtbl.create 5
+let empty_treenode name = {
+ name;
+ total = 0.0;
+ local = 0.0;
+ ncalls = 0;
+ max_total = 0.0;
+ children = M.empty;
+}
-let get_node c table =
- try Hashtbl.find table c
- with Not_found ->
- let new_node = empty_treenode 5 in
- Hashtbl.add table c new_node;
- new_node
+let root = "root"
-let rec add_node node node' =
- add_entry node.entry true node'.entry;
- Hashtbl.iter
- (fun s node' -> add_node (get_node s node.children) node')
- node'.children
+module Local = Summary.Local
-let time () =
- let times = Unix.times () in
- times.Unix.tms_utime +. times.Unix.tms_stime
+let stack = Local.ref ~name:"LtacProf-stack" [empty_treenode root]
-(*
-let msgnl_with fmt strm = msg_with fmt (strm ++ fnl ())
-let msgnl strm = msgnl_with !Pp_control.std_ft strm
-
-let rec print_treenode indent (tn : treenode) =
- msgnl (str (indent^"{ entry = {"));
- Feedback.msg_notice (str (indent^"total = "));
- msgnl (str (indent^(string_of_float (tn.entry.total))));
- Feedback.msg_notice (str (indent^"local = "));
- msgnl (str (indent^(string_of_float tn.entry.local)));
- Feedback.msg_notice (str (indent^"ncalls = "));
- msgnl (str (indent^(string_of_int tn.entry.ncalls)));
- Feedback.msg_notice (str (indent^"max_total = "));
- msgnl (str (indent^(string_of_float tn.entry.max_total)));
- msgnl (str (indent^"}"));
- msgnl (str (indent^"children = {"));
- Hashtbl.iter
- (fun s node ->
- msgnl (str (indent^" "^s^" |-> "));
- print_treenode (indent^" ") node
- )
- tn.children;
- msgnl (str (indent^"} }"))
-
-let rec print_stack (st : treenode list) = match st with
-| [] -> msgnl (str "[]")
-| x :: xs -> print_treenode "" x; msgnl (str ("::")); print_stack xs
-*)
-
-let string_of_call ck =
- let s =
- string_of_ppcmds
- (match ck with
- | Tacexpr.LtacNotationCall s -> Names.KerName.print s
- | Tacexpr.LtacNameCall cst -> Pptactic.pr_ltac_constant cst
- | Tacexpr.LtacVarCall (id, t) -> Nameops.pr_id id
- | Tacexpr.LtacAtomCall te ->
- (Pptactic.pr_glob_tactic (Global.env ())
- (Tacexpr.TacAtom (Loc.ghost, te)))
- | Tacexpr.LtacConstrInterp (c, _) ->
- pr_glob_constr_env (Global.env ()) c
- | Tacexpr.LtacMLCall te ->
- (Pptactic.pr_glob_tactic (Global.env ())
- te)
- ) in
- for i = 0 to String.length s - 1 do if s.[i] = '\n' then s.[i] <- ' ' done;
- let s = try String.sub s 0 (CString.string_index_from s 0 "(*") with Not_found -> s in
- CString.strip s
-
-let exit_tactic start_time add_total c = match !stack with
-| [] | [_] ->
- (* oops, our stack is invalid *)
- encounter_multi_success_backtracking ()
-| node :: (parent :: _ as stack') ->
- stack := stack';
- if add_total then Hashtbl.remove on_stack (string_of_call c);
- let diff = time () -. start_time in
- parent.entry.local <- parent.entry.local -. diff;
- let node' = { total = diff; local = diff; ncalls = 1; max_total = diff } in
- add_entry node.entry add_total node'
-
-let tclFINALLY tac (finally : unit Proofview.tactic) =
- let open Proofview.Notations in
- Proofview.tclIFCATCH
- tac
- (fun v -> finally <*> Proofview.tclUNIT v)
- (fun (exn, info) -> finally <*> Proofview.tclZERO ~info exn)
+let reset_profile_tmp () =
+ Local.(stack := [empty_treenode root]);
+ encountered_multi_success_backtracking := false
-let do_profile s call_trace tac =
- let open Proofview.Notations in
- Proofview.tclLIFT (Proofview.NonLogical.make (fun () ->
- if !is_profiling && is_new_call () then
- match call_trace with
- | (_, c) :: _ ->
- let s = string_of_call c in
- let parent = List.hd !stack in
- let node, add_total = try Hashtbl.find on_stack s, false
- with Not_found ->
- let node = get_node s parent.children in
- Hashtbl.add on_stack s node;
- node, true
- in
- if not add_total && node = List.hd !stack then None else (
- stack := node :: !stack;
- let start_time = time () in
- Some (start_time, add_total)
- )
- | [] -> None
- else None)) >>= function
- | Some (start_time, add_total) ->
- tclFINALLY
- tac
- (Proofview.tclLIFT (Proofview.NonLogical.make (fun () ->
- (match call_trace with
- | (_, c) :: _ ->
- exit_tactic start_time add_total c
- | [] -> ()))))
- | None -> tac
+(* ************** XML Serialization ********************* *)
+let rec of_ltacprof_tactic (name, t) =
+ assert (String.equal name t.name);
+ let open Xml_datatype in
+ let total = string_of_float t.total in
+ let local = string_of_float t.local in
+ let ncalls = string_of_int t.ncalls in
+ let max_total = string_of_float t.max_total in
+ let children = List.map of_ltacprof_tactic (M.bindings t.children) in
+ Element ("ltacprof_tactic",
+ [ ("name", name); ("total",total); ("local",local);
+ ("ncalls",ncalls); ("max_total",max_total)],
+ children)
+
+let of_ltacprof_results t =
+ let open Xml_datatype in
+ assert(String.equal t.name root);
+ let children = List.map of_ltacprof_tactic (M.bindings t.children) in
+ Element ("ltacprof", [("total_time", string_of_float t.total)], children)
+let rec to_ltacprof_tactic m xml =
+ let open Xml_datatype in
+ match xml with
+ | Element ("ltacprof_tactic",
+ [("name", name); ("total",total); ("local",local);
+ ("ncalls",ncalls); ("max_total",max_total)], xs) ->
+ let node = {
+ name;
+ total = float_of_string total;
+ local = float_of_string local;
+ ncalls = int_of_string ncalls;
+ max_total = float_of_string max_total;
+ children = List.fold_left to_ltacprof_tactic M.empty xs;
+ } in
+ M.add name node m
+ | _ -> CErrors.anomaly Pp.(str "Malformed ltacprof_tactic XML")
+
+let to_ltacprof_results xml =
+ let open Xml_datatype in
+ match xml with
+ | Element ("ltacprof", [("total_time", t)], xs) ->
+ { name = root;
+ total = float_of_string t;
+ ncalls = 0;
+ max_total = 0.0;
+ local = 0.0;
+ children = List.fold_left to_ltacprof_tactic M.empty xs }
+ | _ -> CErrors.anomaly Pp.(str "Malformed ltacprof XML")
+
+let feedback_results results =
+ Feedback.(feedback
+ (Custom (Loc.dummy_loc, "ltacprof_results", of_ltacprof_results results)))
+
+(* ************** pretty printing ************************************* *)
let format_sec x = (Printf.sprintf "%.3fs" x)
let format_ratio x = (Printf.sprintf "%.1f%%" (100. *. x))
@@ -221,13 +147,12 @@ let rec list_iter_is_last f = function
| x :: xs -> f false x :: list_iter_is_last f xs
let header =
- str " tactic self total calls max" ++
+ str " tactic local total calls max " ++
fnl () ++
str "────────────────────────────────────────┴──────┴──────┴───────┴─────────┘" ++
fnl ()
-let rec print_node all_total indent prefix (s, n) =
- let e = n.entry in
+let rec print_node ~filter all_total indent prefix (s, e) =
h 0 (
padr_with '-' 40 (prefix ^ s ^ " ")
++ padl 7 (format_ratio (e.local /. all_total))
@@ -236,125 +161,251 @@ let rec print_node all_total indent prefix (s, n) =
++ padl 10 (format_sec (e.max_total))
) ++
fnl () ++
- print_table all_total indent false n.children
+ print_table ~filter all_total indent false e.children
-and print_table all_total indent first_level table =
- let fold s n l = if n.entry.total /. all_total < 0.02 then l else (s, n) :: l in
- let ls = Hashtbl.fold fold table [] in
+and print_table ~filter all_total indent first_level table =
+ let fold _ n l =
+ let s, total = n.name, n.total in
+ if filter s total then (s, n) :: l else l in
+ let ls = M.fold fold table [] in
match ls with
| [s, n] when not first_level ->
- print_node all_total indent (indent ^ "└") (s, n)
+ v 0 (print_node ~filter all_total indent (indent ^ "└") (s, n))
| _ ->
- let ls = List.sort (fun (_, n1) (_, n2) -> compare n2.entry.total n1.entry.total) ls in
+ let ls =
+ List.sort (fun (_, { total = s1 }) (_, { total = s2}) ->
+ compare s2 s1) ls in
let iter is_last =
- let sep0 = if first_level then "" else if is_last then " " else " │" in
- let sep1 = if first_level then "─" else if is_last then " └─" else " ├─" in
- print_node all_total (indent ^ sep0) (indent ^ sep1)
+ let sep0 = if first_level then "" else if is_last then " " else " │" in
+ let sep1 = if first_level then "─" else if is_last then " └─" else " ├─" in
+ print_node ~filter all_total (indent ^ sep0) (indent ^ sep1)
in
- prlist_with_sep fnl (fun pr -> pr) (list_iter_is_last iter ls)
-
-let get_results_string () =
- let tree = (List.hd !stack).children in
- let all_total = -. (List.hd !stack).entry.local in
- let global = Hashtbl.create 20 in
- let rec cumulate table =
- let iter s node =
- let node' = get_node s global in
- add_entry node'.entry true node.entry;
- cumulate node.children
+ prlist (fun pr -> pr) (list_iter_is_last iter ls)
+
+let to_string ~filter ?(cutoff=0.0) node =
+ let tree = node.children in
+ let all_total = M.fold (fun _ { total } a -> total +. a) node.children 0.0 in
+ let flat_tree =
+ let global = ref M.empty in
+ let find_tactic tname l =
+ try M.find tname !global
+ with Not_found ->
+ let e = empty_treenode tname in
+ global := M.add tname e !global;
+ e in
+ let add_tactic tname stats = global := M.add tname stats !global in
+ let sum_stats add_total
+ { name; total = t1; local = l1; ncalls = n1; max_total = m1 }
+ { total = t2; local = l2; ncalls = n2; max_total = m2 } = {
+ name;
+ total = if add_total then t1 +. t2 else t1;
+ local = l1 +. l2;
+ ncalls = n1 + n2;
+ max_total = if add_total then max m1 m2 else m1;
+ children = M.empty;
+ } in
+ let rec cumulate table =
+ let iter _ ({ name; children } as statistics) =
+ if filter name then begin
+ let stats' = find_tactic name global in
+ add_tactic name (sum_stats true stats' statistics);
+ end;
+ cumulate children
+ in
+ M.iter iter table
in
- Hashtbl.iter iter table
+ cumulate tree;
+ !global
in
- cumulate tree;
warn_encountered_multi_success_backtracking ();
+ let filter s n = filter s && n >= cutoff in
let msg =
h 0 (str "total time: " ++ padl 11 (format_sec (all_total))) ++
fnl () ++
+ fnl () ++
header ++
- print_table all_total "" true global ++
+ print_table ~filter all_total "" true flat_tree ++
fnl () ++
header ++
- print_table all_total "" true tree
+ print_table ~filter all_total "" true tree
in
msg
+(* ******************** profiling code ************************************** *)
-type ltacprof_entry = {total : float; self : float; num_calls : int; max_total : float}
-type ltacprof_tactic = {name: string; statistics : ltacprof_entry; tactics : ltacprof_tactic list}
-type ltacprof_results = {total_time : float; tactics : ltacprof_tactic list}
+let get_child name node =
+ try M.find name node.children
+ with Not_found -> empty_treenode name
-let to_ltacprof_entry (e: entry) : ltacprof_entry =
- {total=e.total; self=e.local; num_calls=e.ncalls; max_total=e.max_total}
+let time () =
+ let times = Unix.times () in
+ times.Unix.tms_utime +. times.Unix.tms_stime
-let rec to_ltacprof_tactic (name: string) (t: treenode) : ltacprof_tactic =
- { name = name; statistics = to_ltacprof_entry t.entry; tactics = to_ltacprof_treenode t.children }
-and to_ltacprof_treenode (table: (string, treenode) Hashtbl.t) : ltacprof_tactic list =
- Hashtbl.fold (fun name' t' c -> to_ltacprof_tactic name' t'::c) table []
+let string_of_call ck =
+ let s =
+ string_of_ppcmds
+ (match ck with
+ | Tacexpr.LtacNotationCall s -> Pptactic.pr_alias_key s
+ | Tacexpr.LtacNameCall cst -> Pptactic.pr_ltac_constant cst
+ | Tacexpr.LtacVarCall (id, t) -> Nameops.pr_id id
+ | Tacexpr.LtacAtomCall te ->
+ (Pptactic.pr_glob_tactic (Global.env ())
+ (Tacexpr.TacAtom (Loc.ghost, te)))
+ | Tacexpr.LtacConstrInterp (c, _) ->
+ pr_glob_constr_env (Global.env ()) c
+ | Tacexpr.LtacMLCall te ->
+ (Pptactic.pr_glob_tactic (Global.env ())
+ te)
+ ) in
+ for i = 0 to String.length s - 1 do if s.[i] = '\n' then s.[i] <- ' ' done;
+ let s = try String.sub s 0 (CString.string_index_from s 0 "(*") with Not_found -> s in
+ CString.strip s
-let get_profiling_results() : ltacprof_results =
- let tree = List.hd !stack in
- { total_time = -. tree.entry.local; tactics = to_ltacprof_treenode tree.children }
+let rec merge_sub_tree name tree acc =
+ try
+ let t = M.find name acc in
+ let t = {
+ name;
+ total = t.total +. tree.total;
+ ncalls = t.ncalls + tree.ncalls;
+ local = t.local +. tree.local;
+ max_total = max t.max_total tree.max_total;
+ children = M.fold merge_sub_tree tree.children t.children;
+ } in
+ M.add name t acc
+ with Not_found -> M.add name tree acc
+
+let merge_roots ?(disjoint=true) t1 t2 =
+ assert(String.equal t1.name t2.name);
+ { name = t1.name;
+ ncalls = t1.ncalls + t2.ncalls;
+ local = if disjoint then t1.local +. t2.local else t1.local;
+ total = if disjoint then t1.total +. t2.total else t1.total;
+ max_total = if disjoint then max t1.max_total t2.max_total else t1.max_total;
+ children =
+ M.fold merge_sub_tree t2.children t1.children }
+
+let rec find_in_stack what acc = function
+ | [] -> None
+ | { name } as x :: rest when String.equal name what -> Some(acc, x, rest)
+ | { name } as x :: rest -> find_in_stack what (x :: acc) rest
+
+let exit_tactic start_time c =
+ let diff = time () -. start_time in
+ match Local.(!stack) with
+ | [] | [_] ->
+ (* oops, our stack is invalid *)
+ encounter_multi_success_backtracking ();
+ reset_profile_tmp ()
+ | node :: (parent :: rest as full_stack) ->
+ let name = string_of_call c in
+ if not (String.equal name node.name) then
+ (* oops, our stack is invalid *)
+ encounter_multi_success_backtracking ();
+ let node = { node with
+ total = node.total +. diff;
+ local = node.local +. diff;
+ ncalls = node.ncalls + 1;
+ max_total = max node.max_total diff;
+ } in
+ (* updating the stack *)
+ let parent =
+ match find_in_stack node.name [] full_stack with
+ | None ->
+ (* no rec-call, we graft the subtree *)
+ let parent = { parent with
+ local = parent.local -. diff;
+ children = M.add node.name node parent.children } in
+ Local.(stack := parent :: rest);
+ parent
+ | Some(to_update, self, rest) ->
+ (* we coalesce the rec-call and update the lower stack *)
+ let self = merge_roots ~disjoint:false self node in
+ let updated_stack =
+ List.fold_left (fun s x ->
+ (try M.find x.name (List.hd s).children
+ with Not_found -> x) :: s) (self :: rest) to_update in
+ Local.(stack := updated_stack);
+ List.hd Local.(!stack)
+ in
+ (* Calls are over, we reset the stack and send back data *)
+ if rest == [] && get_profiling () then begin
+ assert(String.equal root parent.name);
+ reset_profile_tmp ();
+ feedback_results parent
+ end
-let rec of_ltacprof_tactic t =
- let open Xml_datatype in
- let total = string_of_float t.statistics.total in
- let self = string_of_float t.statistics.self in
- let num_calls = string_of_int t.statistics.num_calls in
- let max_total = string_of_float t.statistics.max_total in
- let children = List.map of_ltacprof_tactic t.tactics in
- Element ("ltacprof_tactic", [("name", t.name); ("total",total); ("self",self); ("num_calls",num_calls); ("max_total",max_total)], children)
-
-let rec of_ltacprof_results t =
- let open Xml_datatype in
- let children = List.map of_ltacprof_tactic t.tactics in
- Element ("ltacprof", [("total_time", string_of_float t.total_time)], children)
+let tclFINALLY tac (finally : unit Proofview.tactic) =
+ let open Proofview.Notations in
+ Proofview.tclIFCATCH
+ tac
+ (fun v -> finally <*> Proofview.tclUNIT v)
+ (fun (exn, info) -> finally <*> Proofview.tclZERO ~info exn)
+let do_profile s call_trace tac =
+ let open Proofview.Notations in
+ Proofview.tclLIFT (Proofview.NonLogical.make (fun () ->
+ if !is_profiling then
+ match call_trace, Local.(!stack) with
+ | (_, c) :: _, parent :: rest ->
+ let name = string_of_call c in
+ let node = get_child name parent in
+ Local.(stack := node :: parent :: rest);
+ Some (time ())
+ | _ :: _, [] -> assert false
+ | _ -> None
+ else None)) >>= function
+ | Some start_time ->
+ tclFINALLY
+ tac
+ (Proofview.tclLIFT (Proofview.NonLogical.make (fun () ->
+ (match call_trace with
+ | (_, c) :: _ -> exit_tactic start_time c
+ | [] -> ()))))
+ | None -> tac
-let get_profile_xml() =
- of_ltacprof_results (get_profiling_results())
+(* ************** Accumulation of data from workers ************************* *)
-let print_results () =
- Feedback.msg_notice (get_results_string());
- Feedback.feedback (Feedback.Custom (Loc.dummy_loc, "ltacprof_results", get_profile_xml()))
+let get_local_profiling_results () = List.hd Local.(!stack)
- (* FOR DEBUGGING *)
- (* ;
- msgnl (str"");
- print_stack (!stack)
- *)
+module SM = Map.Make(Stateid.Self)
-let print_results_tactic tactic =
- let tree = (List.hd !stack).children in
- let table_tactic = Hashtbl.create 20 in
- let rec cumulate table =
- let iter s node =
- if String.sub (s ^ ".") 0 (min (1 + String.length s) (String.length tactic)) = tactic
- then add_node (get_node s table_tactic) node
- else cumulate node.children
- in
- Hashtbl.iter iter table
- in
- cumulate tree;
- let all_total = -. (List.hd !stack).entry.local in
- let tactic_total =
- Hashtbl.fold
- (fun _ node all_total -> node.entry.total +. all_total)
- table_tactic 0. in
- warn_encountered_multi_success_backtracking ();
- let msg =
- h 0 (str"total time: " ++ padl 11 (format_sec (all_total))) ++
- h 0 (str"time spent in tactic: " ++ padl 11 (format_sec (tactic_total))) ++
- fnl () ++
- header ++
- print_table tactic_total "" true table_tactic
- in
- Feedback.msg_notice msg
+let data = ref SM.empty
+
+let _ =
+ Feedback.(add_feeder (function
+ | { id = State s; contents = Custom (_, "ltacprof_results", xml) } ->
+ let results = to_ltacprof_results xml in
+ let other_results = (* Multi success can cause this *)
+ try SM.find s !data
+ with Not_found -> empty_treenode root in
+ data := SM.add s (merge_roots results other_results) !data
+ | _ -> ()))
let reset_profile () =
- stack := [empty_treenode 20];
- encountered_multi_success_backtracking := false
+ reset_profile_tmp ();
+ data := SM.empty
+
+(* ******************** *)
+
+let print_results_filter ~cutoff ~filter =
+ let valid id _ = Stm.state_of_id id <> `Expired in
+ data := SM.filter valid !data;
+ let results =
+ SM.fold (fun _ -> merge_roots ~disjoint:true) !data (empty_treenode root) in
+ let results = merge_roots results Local.(CList.last !stack) in
+ Feedback.msg_notice (to_string ~cutoff ~filter results)
+;;
+
+let print_results ~cutoff =
+ print_results_filter ~cutoff ~filter:(fun _ -> true)
+
+let print_results_tactic tactic =
+ print_results_filter ~cutoff:0.0 ~filter:(fun s ->
+ String.(equal tactic (sub (s ^ ".") 0 (min (1+length s) (length tactic)))))
-let do_print_results_at_close () = if get_profiling () then print_results ()
+let do_print_results_at_close () =
+ if get_profiling () then print_results ~cutoff:0.0
let _ = Declaremods.append_end_library_hook do_print_results_at_close
diff --git a/ltac/profile_ltac.mli b/ltac/profile_ltac.mli
index 8e029bb2e9..e5e2e41975 100644
--- a/ltac/profile_ltac.mli
+++ b/ltac/profile_ltac.mli
@@ -8,15 +8,14 @@
(** Ltac profiling primitives *)
-val do_profile : string -> ('a * Tacexpr.ltac_call_kind) list -> 'b Proofview.tactic -> 'b Proofview.tactic
+val do_profile :
+ string -> ('a * Tacexpr.ltac_call_kind) list ->
+ 'b Proofview.tactic -> 'b Proofview.tactic
val set_profiling : bool -> unit
-val get_profiling : unit -> bool
-
-val entered_call : unit -> unit
-
-val print_results : unit -> unit
+(* Cut off results < than specified cutoff *)
+val print_results : cutoff:float -> unit
val print_results_tactic : string -> unit
@@ -30,24 +29,20 @@ val do_print_results_at_close : unit -> unit
* statistics of the two invocations combined, and also combined over all
* invocations of 'aaa'.
* total: time spent running this tactic and its subtactics (seconds)
- * self: time spent running this tactic, minus its subtactics (seconds)
- * num_calls: the number of invocations of this tactic that have been made
+ * local: time spent running this tactic, minus its subtactics (seconds)
+ * ncalls: the number of invocations of this tactic that have been made
* max_total: the greatest running time of a single invocation (seconds)
*)
-type ltacprof_entry = {total : float; self : float; num_calls : int; max_total : float}
-(* A profiling entry for a tactic and the tactics that it called
- * name: name of the tactic
- * statistics: profiling data collected
- * tactics: profiling results for each tactic that this tactic invoked;
- * multiple invocations of the same sub-tactic are combined together.
- *)
-type ltacprof_tactic = {name: string; statistics : ltacprof_entry; tactics : ltacprof_tactic list}
-(* The full results of profiling
- * total_time: time spent running tactics (seconds)
- * tactics: the tactics that have been invoked since profiling was started or reset
- *)
-type ltacprof_results = {total_time : float; tactics : ltacprof_tactic list}
-
-(* Returns the profiling results for the currently-focused state. *)
-val get_profiling_results : unit -> ltacprof_results
+type treenode = {
+ name : CString.Map.key;
+ total : float;
+ local : float;
+ ncalls : int;
+ max_total : float;
+ children : treenode CString.Map.t
+}
+
+(* Returns the profiling results known by the current process *)
+val get_local_profiling_results : unit -> treenode
+val feedback_results : treenode -> unit
diff --git a/ltac/profile_ltac_tactics.ml4 b/ltac/profile_ltac_tactics.ml4
index c092a0cb61..9083bda60a 100644
--- a/ltac/profile_ltac_tactics.ml4
+++ b/ltac/profile_ltac_tactics.ml4
@@ -31,7 +31,8 @@ VERNAC COMMAND EXTEND ResetLtacProfiling CLASSIFIED AS SIDEFF
END
VERNAC COMMAND EXTEND ShowLtacProfile CLASSIFIED AS QUERY
- [ "Show" "Ltac" "Profile" ] -> [ print_results() ]
+| [ "Show" "Ltac" "Profile" ] -> [ print_results ~cutoff:0.0 ]
+| [ "Show" "Ltac" "Profile" "CutOff" int(n) ] -> [ print_results ~cutoff:(float_of_int n) ]
END
VERNAC COMMAND EXTEND ShowLtacProfileTactic CLASSIFIED AS QUERY
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index cb39df8ab5..69f45e1aeb 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -8,14 +8,14 @@
open Names
open Pp
-open Errors
+open CErrors
open Util
open Nameops
open Namegen
open Term
open Vars
open Reduction
-open Tacticals
+open Tacticals.New
open Tacmach
open Tactics
open Pretype_errors
@@ -218,7 +218,7 @@ end) = struct
| Some (x, Some rel) -> evars, rel
in
let rec aux env evars ty l =
- let t = Reductionops.whd_betadeltaiota env (goalevars evars) ty in
+ let t = Reductionops.whd_all env (goalevars evars) ty in
match kind_of_term t, l with
| Prod (na, ty, b), obj :: cstrs ->
let b = Reductionops.nf_betaiota (goalevars evars) b in
@@ -321,7 +321,7 @@ end) = struct
let rec aux evars env prod n =
if Int.equal n 0 then start evars env prod
else
- match kind_of_term (Reduction.whd_betadeltaiota env prod) with
+ match kind_of_term (Reduction.whd_all env prod) with
| Prod (na, ty, b) ->
if noccurn 1 b then
let b' = lift (-1) b in
@@ -339,7 +339,7 @@ end) = struct
try let evars, found = aux evars env ty (succ (List.length args)) in
Some (evars, found, c, ty, arg :: args)
with Not_found ->
- let ty = whd_betadeltaiota env ty in
+ let ty = whd_all env ty in
find env (mkApp (c, [| arg |])) (prod_applist ty [arg]) args
in find env c ty args
@@ -365,7 +365,7 @@ end) = struct
rewrite_relation_class [| evar; mkApp (c, params) |] in
let _ = Typeclasses.resolve_one_typeclass env' (goalevars evars) inst in
Some (it_mkProd_or_LetIn t rels)
- with e when Errors.noncritical e -> None)
+ with e when CErrors.noncritical e -> None)
| _ -> None
@@ -438,15 +438,23 @@ let split_head = function
hd :: tl -> hd, tl
| [] -> assert(false)
+let eq_pb (ty, env, x, y as pb) (ty', env', x', y' as pb') =
+ pb == pb' || (ty == ty' && Constr.equal x x' && Constr.equal y y')
+
+let problem_inclusion x y =
+ List.for_all (fun pb -> List.exists (fun pb' -> eq_pb pb pb') y) x
+
let evd_convertible env evd x y =
try
- let evd = Evarconv.the_conv_x env x y evd in
(* Unfortunately, the_conv_x might say they are unifiable even if some
- unsolvable constraints remain, so we check them here *)
- let evd = Evarconv.consider_remaining_unif_problems env evd in
- let () = Evarconv.check_problems_are_solved env evd in
- Some evd
- with e when Errors.noncritical e -> None
+ unsolvable constraints remain, so we check that this unification
+ does not introduce any new problem. *)
+ let _, pbs = Evd.extract_all_conv_pbs evd in
+ let evd' = Evarconv.the_conv_x env x y evd in
+ let _, pbs' = Evd.extract_all_conv_pbs evd' in
+ if evd' == evd || problem_inclusion pbs' pbs then Some evd'
+ else None
+ with e when CErrors.noncritical e -> None
let convertible env evd x y =
Reductionops.is_conv_leq env evd x y
@@ -581,9 +589,9 @@ let general_rewrite_unif_flags () =
let core_flags =
{ rewrite_core_unif_flags with
Unification.modulo_conv_on_closed_terms = Some ts;
- Unification.use_evars_eagerly_in_conv_on_closed_terms = false;
+ Unification.use_evars_eagerly_in_conv_on_closed_terms = true;
Unification.modulo_delta = ts;
- Unification.modulo_delta_types = ts;
+ Unification.modulo_delta_types = full_transparent_state;
Unification.modulo_betaiota = true }
in {
Unification.core_unify_flags = core_flags;
@@ -617,7 +625,7 @@ let solve_remaining_by env sigma holes by =
| Genarg.GenArg (Genarg.Glbwit tag, tac) ->
Ftactic.run (Geninterp.interp tag ist tac) (fun _ -> Proofview.tclUNIT ())
in
- let solve_tac = Tacticals.New.tclCOMPLETE solve_tac in
+ let solve_tac = tclCOMPLETE solve_tac in
let solve sigma evk =
let evi =
try Some (Evd.find_undefined sigma evk)
@@ -1407,7 +1415,7 @@ module Strategies =
let sigma, c = Pretyping.understand_tcc env (goalevars evars) c in
let unfolded =
try Tacred.try_red_product env sigma c
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
error "fold: the term is not unfoldable !"
in
try
@@ -1416,7 +1424,7 @@ module Strategies =
state, Success { rew_car = ty; rew_from = t; rew_to = c';
rew_prf = RewCast DEFAULTcast;
rew_evars = (sigma, snd evars) }
- with e when Errors.noncritical e -> state, Fail
+ with e when CErrors.noncritical e -> state, Fail
}
@@ -1432,17 +1440,8 @@ let rewrite_with l2r flags c occs : strategy = { strategy =
fun ({ state = () } as input) ->
let unify env evars t =
let (sigma, cstrs) = evars in
- let ans =
- try Some (refresh_hypinfo env sigma c)
- with e when Class_tactics.catchable e -> None
- in
- match ans with
- | None -> None
- | Some (sigma, rew) ->
- let rew = unify_eqn rew l2r flags env (sigma, cstrs) None t in
- match rew with
- | None -> None
- | Some rew -> Some rew
+ let (sigma, rew) = refresh_hypinfo env sigma c in
+ unify_eqn rew l2r flags env (sigma, cstrs) None t
in
let app = apply_rule unify occs in
let strat =
@@ -1466,7 +1465,7 @@ let solve_constraints env (evars,cstrs) =
(Typeclasses.mark_resolvables ~filter evars)
let nf_zeta =
- Reductionops.clos_norm_flags (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
+ Reductionops.clos_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
exception RewriteFailure of Pp.std_ppcmds
@@ -1562,6 +1561,10 @@ let newfail n s =
let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
let open Proofview.Notations in
+ (** For compatibility *)
+ let beta_red _ sigma c = Reductionops.nf_betaiota sigma c in
+ let beta = Tactics.reduct_in_concl (beta_red, DEFAULTcast) in
+ let beta_hyp id = Tactics.reduct_in_hyp beta_red (id, InHyp) in
let treat sigma res =
match res with
| None -> newfail 0 (str "Nothing to rewrite")
@@ -1573,12 +1576,16 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
let gls = List.rev (Evd.fold_undefined fold undef []) in
match clause, prf with
| Some id, Some p ->
- let tac = Refine.refine ~unsafe:false { run = fun h -> Sigma (p, h, Sigma.refl) } <*> Proofview.Unsafe.tclNEWGOALS gls in
+ let tac = tclTHENLIST [
+ Refine.refine ~unsafe:false { run = fun h -> Sigma.here p h };
+ Proofview.Unsafe.tclNEWGOALS gls;
+ ] in
Proofview.Unsafe.tclEVARS undef <*>
- assert_replacing id newt tac
+ tclTHENFIRST (assert_replacing id newt tac) (beta_hyp id)
| Some id, None ->
Proofview.Unsafe.tclEVARS undef <*>
- convert_hyp_no_check (LocalAssum (id, newt))
+ convert_hyp_no_check (LocalAssum (id, newt)) <*>
+ beta_hyp id
| None, Some p ->
Proofview.Unsafe.tclEVARS undef <*>
Proofview.Goal.enter { enter = begin fun gl ->
@@ -1593,12 +1600,6 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
Proofview.Unsafe.tclEVARS undef <*>
convert_concl_no_check newt DEFAULTcast
in
- let beta_red _ sigma c = Reductionops.nf_betaiota sigma c in
- let beta = Tactics.reduct_in_concl (beta_red, DEFAULTcast) in
- let opt_beta = match clause with
- | None -> Proofview.tclUNIT ()
- | Some id -> Tactics.reduct_in_hyp beta_red (id, InHyp)
- in
Proofview.Goal.nf_enter { enter = begin fun gl ->
let concl = Proofview.Goal.concl gl in
let env = Proofview.Goal.env gl in
@@ -1623,30 +1624,32 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
let sigma = match origsigma with None -> sigma | Some sigma -> sigma in
treat sigma res <*>
(** For compatibility *)
- beta <*> opt_beta <*> Proofview.shelve_unifiable
+ beta <*> Proofview.shelve_unifiable
with
| PretypeError (env, evd, (UnsatisfiableConstraints _ as e)) ->
raise (RewriteFailure (Himsg.explain_pretype_error env evd e))
end }
let tactic_init_setoid () =
- try init_setoid (); tclIDTAC
- with e when Errors.noncritical e -> tclFAIL 0 (str"Setoid library not loaded")
+ try init_setoid (); Proofview.tclUNIT ()
+ with e when CErrors.noncritical e -> Tacticals.New.tclFAIL 0 (str"Setoid library not loaded")
let cl_rewrite_clause_strat progress strat clause =
- tclTHEN (tactic_init_setoid ())
- ((if progress then tclWEAK_PROGRESS else fun x -> x)
- (fun gl ->
- try Proofview.V82.of_tactic (cl_rewrite_clause_newtac ~progress strat clause) gl
- with RewriteFailure e ->
- errorlabstrm "" (str"setoid rewrite failed: " ++ e)
+ tactic_init_setoid () <*>
+ (if progress then Proofview.tclPROGRESS else fun x -> x)
+ (Proofview.tclOR
+ (cl_rewrite_clause_newtac ~progress strat clause)
+ (fun (e, info) -> match e with
+ | RewriteFailure e ->
+ tclZEROMSG (str"setoid rewrite failed: " ++ e)
| Refiner.FailError (n, pp) ->
- tclFAIL n (str"setoid rewrite failed: " ++ Lazy.force pp) gl))
+ tclFAIL n (str"setoid rewrite failed: " ++ Lazy.force pp)
+ | e -> Proofview.tclZERO ~info e))
(** Setoid rewriting when called with "setoid_rewrite" *)
-let cl_rewrite_clause l left2right occs clause gl =
+let cl_rewrite_clause l left2right occs clause =
let strat = rewrite_with left2right (general_rewrite_unif_flags ()) l occs in
- cl_rewrite_clause_strat true strat clause gl
+ cl_rewrite_clause_strat true strat clause
(** Setoid rewriting when called with "rewrite_strat" *)
let cl_rewrite_clause_strat strat clause =
@@ -2026,12 +2029,12 @@ let unification_rewrite l2r c1 c2 sigma prf car rel but env =
abs, sigma, res, Sorts.is_prop sort
let get_hyp gl (c,l) clause l2r =
- let evars = project gl in
- let env = pf_env gl in
+ let evars = Tacmach.New.project gl in
+ let env = Tacmach.New.pf_env gl in
let sigma, hi = decompose_applied_relation env evars (c,l) in
let but = match clause with
- | Some id -> pf_get_hyp_typ gl id
- | None -> Evarutil.nf_evar evars (pf_concl gl)
+ | Some id -> Tacmach.New.pf_get_hyp_typ id gl
+ | None -> Evarutil.nf_evar evars (Tacmach.New.pf_concl gl)
in
unification_rewrite l2r hi.c1 hi.c2 sigma hi.prf hi.car hi.rel but env
@@ -2041,7 +2044,8 @@ let general_rewrite_flags = { under_lambdas = false; on_morphisms = true }
(* let cl_rewrite_clause_tac = Profile.profile5 rewriteclaustac_key cl_rewrite_clause_tac *)
(** Setoid rewriting when called with "rewrite" *)
-let general_s_rewrite cl l2r occs (c,l) ~new_goals gl =
+let general_s_rewrite cl l2r occs (c,l) ~new_goals =
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let abs, evd, res, sort = get_hyp gl (c,l) cl l2r in
let unify env evars t = unify_abs res l2r sort env evars t in
let app = apply_rule unify occs in
@@ -2052,31 +2056,25 @@ let general_s_rewrite cl l2r occs (c,l) ~new_goals gl =
(), res
}
in
- let origsigma = project gl in
- init_setoid ();
- try
- tclWEAK_PROGRESS
+ let origsigma = Tacmach.New.project gl in
+ tactic_init_setoid () <*>
+ Proofview.tclOR
+ (tclPROGRESS
(tclTHEN
- (Refiner.tclEVARS evd)
- (Proofview.V82.of_tactic
- (cl_rewrite_clause_newtac ~progress:true ~abs:(Some abs) ~origsigma strat cl))) gl
- with RewriteFailure e ->
- tclFAIL 0 (str"setoid rewrite failed: " ++ e) gl
-
-let general_s_rewrite_clause x =
- match x with
- | None -> general_s_rewrite None
- | Some id -> general_s_rewrite (Some id)
-
-let general_s_rewrite_clause x y z w ~new_goals =
- Proofview.V82.tactic (general_s_rewrite_clause x y z w ~new_goals)
+ (Proofview.Unsafe.tclEVARS evd)
+ (cl_rewrite_clause_newtac ~progress:true ~abs:(Some abs) ~origsigma strat cl)))
+ (fun (e, info) -> match e with
+ | RewriteFailure e ->
+ tclFAIL 0 (str"setoid rewrite failed: " ++ e)
+ | e -> Proofview.tclZERO ~info e)
+ end }
-let _ = Hook.set Equality.general_setoid_rewrite_clause general_s_rewrite_clause
+let _ = Hook.set Equality.general_setoid_rewrite_clause general_s_rewrite
(** [setoid_]{reflexivity,symmetry,transitivity} tactics *)
let not_declared env ty rel =
- Tacticals.New.tclFAIL 0
+ tclFAIL 0
(str" The relation " ++ Printer.pr_constr_env env Evd.empty rel ++ str" is not a declared " ++
str ty ++ str" relation. Maybe you need to require the Coq.Classes.RelationClasses library")
@@ -2114,8 +2112,7 @@ let setoid_proof ty fn fallback =
end }
let tac_open ((evm,_), c) tac =
- Proofview.V82.tactic
- (tclTHEN (Refiner.tclEVARS evm) (tac c))
+ (tclTHEN (Proofview.Unsafe.tclEVARS evm) (tac c))
let poly_proof getp gett env evm car rel =
if Sorts.is_prop (sort_of_rel env evm rel) then
@@ -2128,7 +2125,7 @@ let setoid_reflexivity =
tac_open (poly_proof PropGlobal.get_reflexive_proof
TypeGlobal.get_reflexive_proof
env evm car rel)
- (fun c -> tclCOMPLETE (Proofview.V82.of_tactic (apply c))))
+ (fun c -> tclCOMPLETE (apply c)))
(reflexivity_red true)
let setoid_symmetry =
@@ -2137,7 +2134,7 @@ let setoid_symmetry =
tac_open
(poly_proof PropGlobal.get_symmetric_proof TypeGlobal.get_symmetric_proof
env evm car rel)
- (fun c -> Proofview.V82.of_tactic (apply c)))
+ (fun c -> apply c))
(symmetry_red true)
let setoid_transitivity c =
@@ -2146,8 +2143,8 @@ let setoid_transitivity c =
tac_open (poly_proof PropGlobal.get_transitive_proof TypeGlobal.get_transitive_proof
env evm car rel)
(fun proof -> match c with
- | None -> Proofview.V82.of_tactic (eapply proof)
- | Some c -> Proofview.V82.of_tactic (apply_with_bindings (proof,ImplicitBindings [ c ]))))
+ | None -> eapply proof
+ | Some c -> apply_with_bindings (proof,ImplicitBindings [ c ])))
(transitivity_red true c)
let setoid_symmetry_in id =
@@ -2165,9 +2162,9 @@ let setoid_symmetry_in id =
let new_hyp' = mkApp (he, [| c2 ; c1 |]) in
let new_hyp = it_mkProd_or_LetIn new_hyp' binders in
Proofview.V82.of_tactic
- (Tacticals.New.tclTHENLAST
+ (tclTHENLAST
(Tactics.assert_after_replacing id new_hyp)
- (Tacticals.New.tclTHENLIST [ intros; setoid_symmetry; apply (mkVar id); Tactics.assumption ]))
+ (tclTHENLIST [ intros; setoid_symmetry; apply (mkVar id); Tactics.assumption ]))
gl)
let _ = Hook.set Tactics.setoid_reflexivity setoid_reflexivity
diff --git a/ltac/rewrite.mli b/ltac/rewrite.mli
index 01709f29fb..f448c85430 100644
--- a/ltac/rewrite.mli
+++ b/ltac/rewrite.mli
@@ -63,12 +63,12 @@ val map_strategy : ('a -> 'b) -> ('c -> 'd) ->
('a, 'c) strategy_ast -> ('b, 'd) strategy_ast
(** Entry point for user-level "rewrite_strat" *)
-val cl_rewrite_clause_strat : strategy -> Id.t option -> tactic
+val cl_rewrite_clause_strat : strategy -> Id.t option -> unit Proofview.tactic
(** Entry point for user-level "setoid_rewrite" *)
val cl_rewrite_clause :
interp_sign * (glob_constr_and_expr * glob_constr_and_expr bindings) ->
- bool -> Locus.occurrences -> Id.t option -> tactic
+ bool -> Locus.occurrences -> Id.t option -> unit Proofview.tactic
val is_applied_rewrite_relation :
env -> evar_map -> Context.Rel.t -> constr -> types option
diff --git a/ltac/taccoerce.ml b/ltac/taccoerce.ml
new file mode 100644
index 0000000000..b0a80ef738
--- /dev/null
+++ b/ltac/taccoerce.ml
@@ -0,0 +1,344 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Util
+open Names
+open Term
+open Pattern
+open Misctypes
+open Genarg
+open Stdarg
+open Constrarg
+open Geninterp
+
+exception CannotCoerceTo of string
+
+let (wit_constr_context : (Empty.t, Empty.t, constr) Genarg.genarg_type) =
+ let wit = Genarg.create_arg "constr_context" in
+ let () = register_val0 wit None in
+ wit
+
+(* includes idents known to be bound and references *)
+let (wit_constr_under_binders : (Empty.t, Empty.t, constr_under_binders) Genarg.genarg_type) =
+ let wit = Genarg.create_arg "constr_under_binders" in
+ let () = register_val0 wit None in
+ wit
+
+(** All the types considered here are base types *)
+let val_tag wit = match val_tag wit with
+| Val.Base t -> t
+| _ -> assert false
+
+let has_type : type a. Val.t -> a typed_abstract_argument_type -> bool = fun v wit ->
+ let Val.Dyn (t, _) = v in
+ match Val.eq t (val_tag wit) with
+ | None -> false
+ | Some Refl -> true
+
+let prj : type a. a Val.typ -> Val.t -> a option = fun t v ->
+ let Val.Dyn (t', x) = v in
+ match Val.eq t t' with
+ | None -> None
+ | Some Refl -> Some x
+
+let in_gen wit v = Val.Dyn (val_tag wit, v)
+let out_gen wit v = match prj (val_tag wit) v with None -> assert false | Some x -> x
+
+module Value =
+struct
+
+type t = Val.t
+
+let normalize v = v
+
+let of_constr c = in_gen (topwit wit_constr) c
+
+let to_constr v =
+ let v = normalize v in
+ if has_type v (topwit wit_constr) then
+ let c = out_gen (topwit wit_constr) v in
+ Some c
+ else if has_type v (topwit wit_constr_under_binders) then
+ let vars, c = out_gen (topwit wit_constr_under_binders) v in
+ match vars with [] -> Some c | _ -> None
+ else None
+
+let of_uconstr c = in_gen (topwit wit_uconstr) c
+
+let to_uconstr v =
+ let v = normalize v in
+ if has_type v (topwit wit_uconstr) then
+ Some (out_gen (topwit wit_uconstr) v)
+ else None
+
+let of_int i = in_gen (topwit wit_int) i
+
+let to_int v =
+ let v = normalize v in
+ if has_type v (topwit wit_int) then
+ Some (out_gen (topwit wit_int) v)
+ else None
+
+let to_list v = prj Val.typ_list v
+
+let to_option v = prj Val.typ_opt v
+
+let to_pair v = prj Val.typ_pair v
+
+end
+
+let is_variable env id =
+ Id.List.mem id (Termops.ids_of_named_context (Environ.named_context env))
+
+(* Transforms an id into a constr if possible, or fails with Not_found *)
+let constr_of_id env id =
+ Term.mkVar (let _ = Environ.lookup_named id env in id)
+
+(* Gives the constr corresponding to a Constr_context tactic_arg *)
+let coerce_to_constr_context v =
+ let v = Value.normalize v in
+ if has_type v (topwit wit_constr_context) then
+ out_gen (topwit wit_constr_context) v
+ else raise (CannotCoerceTo "a term context")
+
+(* Interprets an identifier which must be fresh *)
+let coerce_var_to_ident fresh env v =
+ let v = Value.normalize v in
+ let fail () = raise (CannotCoerceTo "a fresh identifier") in
+ if has_type v (topwit wit_intro_pattern) then
+ match out_gen (topwit wit_intro_pattern) v with
+ | _, IntroNaming (IntroIdentifier id) -> id
+ | _ -> fail ()
+ else if has_type v (topwit wit_var) then
+ out_gen (topwit wit_var) v
+ else match Value.to_constr v with
+ | None -> fail ()
+ | Some c ->
+ (* We need it fresh for intro e.g. in "Tac H = clear H; intro H" *)
+ if isVar c && not (fresh && is_variable env (destVar c)) then
+ destVar c
+ else fail ()
+
+
+(* Interprets, if possible, a constr to an identifier which may not
+ be fresh but suitable to be given to the fresh tactic. Works for
+ vars, constants, inductive, constructors and sorts. *)
+let coerce_to_ident_not_fresh g env v =
+let id_of_name = function
+ | Names.Anonymous -> Id.of_string "x"
+ | Names.Name x -> x in
+ let v = Value.normalize v in
+ let fail () = raise (CannotCoerceTo "an identifier") in
+ if has_type v (topwit wit_intro_pattern) then
+ match out_gen (topwit wit_intro_pattern) v with
+ | _, IntroNaming (IntroIdentifier id) -> id
+ | _ -> fail ()
+ else if has_type v (topwit wit_var) then
+ out_gen (topwit wit_var) v
+ else
+ match Value.to_constr v with
+ | None -> fail ()
+ | Some c ->
+ match Constr.kind c with
+ | Var id -> id
+ | Meta m -> id_of_name (Evd.meta_name g m)
+ | Evar (kn,_) ->
+ begin match Evd.evar_ident kn g with
+ | None -> fail ()
+ | Some id -> id
+ end
+ | Const (cst,_) -> Label.to_id (Constant.label cst)
+ | Construct (cstr,_) ->
+ let ref = Globnames.ConstructRef cstr in
+ let basename = Nametab.basename_of_global ref in
+ basename
+ | Ind (ind,_) ->
+ let ref = Globnames.IndRef ind in
+ let basename = Nametab.basename_of_global ref in
+ basename
+ | Sort s ->
+ begin
+ match s with
+ | Prop _ -> Label.to_id (Label.make "Prop")
+ | Type _ -> Label.to_id (Label.make "Type")
+ end
+ | _ -> fail()
+
+
+let coerce_to_intro_pattern env v =
+ let v = Value.normalize v in
+ if has_type v (topwit wit_intro_pattern) then
+ snd (out_gen (topwit wit_intro_pattern) v)
+ else if has_type v (topwit wit_var) then
+ let id = out_gen (topwit wit_var) v in
+ IntroNaming (IntroIdentifier id)
+ else match Value.to_constr v with
+ | Some c when isVar c ->
+ (* This happens e.g. in definitions like "Tac H = clear H; intro H" *)
+ (* but also in "destruct H as (H,H')" *)
+ IntroNaming (IntroIdentifier (destVar c))
+ | _ -> raise (CannotCoerceTo "an introduction pattern")
+
+let coerce_to_intro_pattern_naming env v =
+ match coerce_to_intro_pattern env v with
+ | IntroNaming pat -> pat
+ | _ -> raise (CannotCoerceTo "a naming introduction pattern")
+
+let coerce_to_hint_base v =
+ let v = Value.normalize v in
+ if has_type v (topwit wit_intro_pattern) then
+ match out_gen (topwit wit_intro_pattern) v with
+ | _, IntroNaming (IntroIdentifier id) -> Id.to_string id
+ | _ -> raise (CannotCoerceTo "a hint base name")
+ else raise (CannotCoerceTo "a hint base name")
+
+let coerce_to_int v =
+ let v = Value.normalize v in
+ if has_type v (topwit wit_int) then
+ out_gen (topwit wit_int) v
+ else raise (CannotCoerceTo "an integer")
+
+let coerce_to_constr env v =
+ let v = Value.normalize v in
+ let fail () = raise (CannotCoerceTo "a term") in
+ if has_type v (topwit wit_intro_pattern) then
+ match out_gen (topwit wit_intro_pattern) v with
+ | _, IntroNaming (IntroIdentifier id) ->
+ (try ([], constr_of_id env id) with Not_found -> fail ())
+ | _ -> fail ()
+ else if has_type v (topwit wit_constr) then
+ let c = out_gen (topwit wit_constr) v in
+ ([], c)
+ else if has_type v (topwit wit_constr_under_binders) then
+ out_gen (topwit wit_constr_under_binders) v
+ else if has_type v (topwit wit_var) then
+ let id = out_gen (topwit wit_var) v in
+ (try [], constr_of_id env id with Not_found -> fail ())
+ else fail ()
+
+let coerce_to_uconstr env v =
+ let v = Value.normalize v in
+ if has_type v (topwit wit_uconstr) then
+ out_gen (topwit wit_uconstr) v
+ else
+ raise (CannotCoerceTo "an untyped term")
+
+let coerce_to_closed_constr env v =
+ let ids,c = coerce_to_constr env v in
+ let () = if not (List.is_empty ids) then raise (CannotCoerceTo "a term") in
+ c
+
+let coerce_to_evaluable_ref env v =
+ let fail () = raise (CannotCoerceTo "an evaluable reference") in
+ let v = Value.normalize v in
+ let ev =
+ if has_type v (topwit wit_intro_pattern) then
+ match out_gen (topwit wit_intro_pattern) v with
+ | _, IntroNaming (IntroIdentifier id) when is_variable env id -> EvalVarRef id
+ | _ -> fail ()
+ else if has_type v (topwit wit_var) then
+ let id = out_gen (topwit wit_var) v in
+ if Id.List.mem id (Termops.ids_of_context env) then EvalVarRef id
+ else fail ()
+ else if has_type v (topwit wit_ref) then
+ let open Globnames in
+ let r = out_gen (topwit wit_ref) v in
+ match r with
+ | VarRef var -> EvalVarRef var
+ | ConstRef c -> EvalConstRef c
+ | IndRef _ | ConstructRef _ -> fail ()
+ else
+ match Value.to_constr v with
+ | Some c when isConst c -> EvalConstRef (Univ.out_punivs (destConst c))
+ | Some c when isVar c -> EvalVarRef (destVar c)
+ | _ -> fail ()
+ in if Tacred.is_evaluable env ev then ev else fail ()
+
+let coerce_to_constr_list env v =
+ let v = Value.to_list v in
+ match v with
+ | Some l ->
+ let map v = coerce_to_closed_constr env v in
+ List.map map l
+ | None -> raise (CannotCoerceTo "a term list")
+
+let coerce_to_intro_pattern_list loc env v =
+ match Value.to_list v with
+ | None -> raise (CannotCoerceTo "an intro pattern list")
+ | Some l ->
+ let map v = (loc, coerce_to_intro_pattern env v) in
+ List.map map l
+
+let coerce_to_hyp env v =
+ let fail () = raise (CannotCoerceTo "a variable") in
+ let v = Value.normalize v in
+ if has_type v (topwit wit_intro_pattern) then
+ match out_gen (topwit wit_intro_pattern) v with
+ | _, IntroNaming (IntroIdentifier id) when is_variable env id -> id
+ | _ -> fail ()
+ else if has_type v (topwit wit_var) then
+ let id = out_gen (topwit wit_var) v in
+ if is_variable env id then id else fail ()
+ else match Value.to_constr v with
+ | Some c when isVar c -> destVar c
+ | _ -> fail ()
+
+let coerce_to_hyp_list env v =
+ let v = Value.to_list v in
+ match v with
+ | Some l ->
+ let map n = coerce_to_hyp env n in
+ List.map map l
+ | None -> raise (CannotCoerceTo "a variable list")
+
+(* Interprets a qualified name *)
+let coerce_to_reference env v =
+ let v = Value.normalize v in
+ match Value.to_constr v with
+ | Some c ->
+ begin
+ try Globnames.global_of_constr c
+ with Not_found -> raise (CannotCoerceTo "a reference")
+ end
+ | None -> raise (CannotCoerceTo "a reference")
+
+(* Quantified named or numbered hypothesis or hypothesis in context *)
+(* (as in Inversion) *)
+let coerce_to_quantified_hypothesis v =
+ let v = Value.normalize v in
+ if has_type v (topwit wit_intro_pattern) then
+ let v = out_gen (topwit wit_intro_pattern) v in
+ match v with
+ | _, IntroNaming (IntroIdentifier id) -> NamedHyp id
+ | _ -> raise (CannotCoerceTo "a quantified hypothesis")
+ else if has_type v (topwit wit_var) then
+ let id = out_gen (topwit wit_var) v in
+ NamedHyp id
+ else if has_type v (topwit wit_int) then
+ AnonHyp (out_gen (topwit wit_int) v)
+ else match Value.to_constr v with
+ | Some c when isVar c -> NamedHyp (destVar c)
+ | _ -> raise (CannotCoerceTo "a quantified hypothesis")
+
+(* Quantified named or numbered hypothesis or hypothesis in context *)
+(* (as in Inversion) *)
+let coerce_to_decl_or_quant_hyp env v =
+ let v = Value.normalize v in
+ if has_type v (topwit wit_int) then
+ AnonHyp (out_gen (topwit wit_int) v)
+ else
+ try coerce_to_quantified_hypothesis v
+ with CannotCoerceTo _ ->
+ raise (CannotCoerceTo "a declared or quantified hypothesis")
+
+let coerce_to_int_or_var_list v =
+ match Value.to_list v with
+ | None -> raise (CannotCoerceTo "an int list")
+ | Some l ->
+ let map n = ArgArg (coerce_to_int n) in
+ List.map map l
diff --git a/ltac/taccoerce.mli b/ltac/taccoerce.mli
new file mode 100644
index 0000000000..0b67f8726e
--- /dev/null
+++ b/ltac/taccoerce.mli
@@ -0,0 +1,96 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Util
+open Names
+open Term
+open Misctypes
+open Pattern
+open Genarg
+open Geninterp
+
+(** Coercions from highest level generic arguments to actual data used by Ltac
+ interpretation. Those functions examinate dynamic types and try to return
+ something sensible according to the object content. *)
+
+exception CannotCoerceTo of string
+(** Exception raised whenever a coercion failed. *)
+
+(** {5 High-level access to values}
+
+ The [of_*] functions cast a given argument into a value. The [to_*] do the
+ converse, and return [None] if there is a type mismatch.
+
+*)
+
+module Value :
+sig
+ type t = Val.t
+
+ val normalize : t -> t
+ (** Eliminated the leading dynamic type casts. *)
+
+ val of_constr : constr -> t
+ val to_constr : t -> constr option
+ val of_uconstr : Glob_term.closed_glob_constr -> t
+ val to_uconstr : t -> Glob_term.closed_glob_constr option
+ val of_int : int -> t
+ val to_int : t -> int option
+ val to_list : t -> t list option
+ val to_option : t -> t option option
+ val to_pair : t -> (t * t) option
+end
+
+(** {5 Coercion functions} *)
+
+val coerce_to_constr_context : Value.t -> constr
+
+val coerce_var_to_ident : bool -> Environ.env -> Value.t -> Id.t
+
+val coerce_to_ident_not_fresh : Evd.evar_map -> Environ.env -> Value.t -> Id.t
+
+val coerce_to_intro_pattern : Environ.env -> Value.t -> Tacexpr.delayed_open_constr intro_pattern_expr
+
+val coerce_to_intro_pattern_naming :
+ Environ.env -> Value.t -> intro_pattern_naming_expr
+
+val coerce_to_hint_base : Value.t -> string
+
+val coerce_to_int : Value.t -> int
+
+val coerce_to_constr : Environ.env -> Value.t -> constr_under_binders
+
+val coerce_to_uconstr : Environ.env -> Value.t -> Glob_term.closed_glob_constr
+
+val coerce_to_closed_constr : Environ.env -> Value.t -> constr
+
+val coerce_to_evaluable_ref :
+ Environ.env -> Value.t -> evaluable_global_reference
+
+val coerce_to_constr_list : Environ.env -> Value.t -> constr list
+
+val coerce_to_intro_pattern_list :
+ Loc.t -> Environ.env -> Value.t -> Tacexpr.intro_patterns
+
+val coerce_to_hyp : Environ.env -> Value.t -> Id.t
+
+val coerce_to_hyp_list : Environ.env -> Value.t -> Id.t list
+
+val coerce_to_reference : Environ.env -> Value.t -> Globnames.global_reference
+
+val coerce_to_quantified_hypothesis : Value.t -> quantified_hypothesis
+
+val coerce_to_decl_or_quant_hyp : Environ.env -> Value.t -> quantified_hypothesis
+
+val coerce_to_int_or_var_list : Value.t -> int or_var list
+
+(** {5 Missing generic arguments} *)
+
+val wit_constr_context : (Empty.t, Empty.t, constr) genarg_type
+
+val wit_constr_under_binders : (Empty.t, Empty.t, constr_under_binders) genarg_type
diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml
index 6b7ae21f3c..673ac832a3 100644
--- a/ltac/tacentries.ml
+++ b/ltac/tacentries.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
open Util
open Names
open Libobject
@@ -429,7 +429,7 @@ let register_ltac local tacl =
let kn = Lib.make_kn id in
let id_pp = pr_id id in
let () = if is_defined_tac kn then
- Errors.user_err_loc (loc, "",
+ CErrors.user_err_loc (loc, "",
str "There is already an Ltac named " ++ id_pp ++ str".")
in
let is_shadowed =
@@ -437,7 +437,7 @@ let register_ltac local tacl =
match Pcoq.parse_string Pcoq.Tactic.tactic (Id.to_string id) with
| Tacexpr.TacArg _ -> false
| _ -> true (* most probably TacAtom, i.e. a primitive tactic ident *)
- with e when Errors.noncritical e -> true (* prim tactics with args, e.g. "apply" *)
+ with e when CErrors.noncritical e -> true (* prim tactics with args, e.g. "apply" *)
in
let () = if is_shadowed then warn_unusable_identifier id in
NewTac id, body
@@ -446,7 +446,7 @@ let register_ltac local tacl =
let kn =
try Nametab.locate_tactic (snd (qualid_of_reference ident))
with Not_found ->
- Errors.user_err_loc (loc, "",
+ CErrors.user_err_loc (loc, "",
str "There is no Ltac named " ++ pr_reference ident ++ str ".")
in
UpdateTac kn, body
diff --git a/ltac/tacenv.ml b/ltac/tacenv.ml
index e3d5e18c9d..c709ab114e 100644
--- a/ltac/tacenv.ml
+++ b/ltac/tacenv.ml
@@ -24,7 +24,7 @@ let register_alias key tac =
let interp_alias key =
try KNmap.find key !alias_map
- with Not_found -> Errors.anomaly (str "Unknown tactic alias: " ++ KerName.print key)
+ with Not_found -> CErrors.anomaly (str "Unknown tactic alias: " ++ KerName.print key)
let check_alias key = KNmap.mem key !alias_map
@@ -55,7 +55,7 @@ let register_ml_tactic ?(overwrite = false) s (t : ml_tactic array) =
if overwrite then
tac_tab := MLTacMap.remove s !tac_tab
else
- Errors.anomaly (str "Cannot redeclare tactic " ++ pr_tacname s ++ str ".")
+ CErrors.anomaly (str "Cannot redeclare tactic " ++ pr_tacname s ++ str ".")
in
tac_tab := MLTacMap.add s t !tac_tab
@@ -65,7 +65,7 @@ let interp_ml_tactic { mltac_name = s; mltac_index = i } =
let () = if Array.length tacs <= i then raise Not_found in
tacs.(i)
with Not_found ->
- Errors.errorlabstrm ""
+ CErrors.errorlabstrm ""
(str "The tactic " ++ pr_tacname s ++ str " is not installed.")
(***************************************************************************)
diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml
index 2bbb3b309b..c5bb0ed076 100644
--- a/ltac/tacintern.ml
+++ b/ltac/tacintern.ml
@@ -11,7 +11,7 @@ open Pp
open Genredexpr
open Glob_term
open Tacred
-open Errors
+open CErrors
open Util
open Names
open Nameops
@@ -378,13 +378,13 @@ let dump_glob_red_expr = function
try
Dumpglob.add_glob (loc_of_or_by_notation Libnames.loc_of_reference r)
(Smartlocate.smart_global r)
- with e when Errors.noncritical e -> ()) occs
+ with e when CErrors.noncritical e -> ()) occs
| Cbv grf | Lazy grf ->
List.iter (fun r ->
try
Dumpglob.add_glob (loc_of_or_by_notation Libnames.loc_of_reference r)
(Smartlocate.smart_global r)
- with e when Errors.noncritical e -> ()) grf.rConst
+ with e when CErrors.noncritical e -> ()) grf.rConst
| _ -> ()
let intern_red_expr ist = function
@@ -564,7 +564,7 @@ and intern_tactic_seq onlytac ist = function
ist.ltacvars, TacLetIn (isrec,l,intern_tactic onlytac ist' u)
| TacMatchGoal (lz,lr,lmr) ->
- ist.ltacvars, (TacMatchGoal(lz,lr, intern_match_rule onlytac ist ~as_type:true lmr))
+ ist.ltacvars, TacMatchGoal(lz,lr, intern_match_rule onlytac ist ~as_type:true lmr)
| TacMatch (lz,c,lmr) ->
ist.ltacvars,
TacMatch (lz,intern_tactic_or_tacarg ist c,intern_match_rule onlytac ist lmr)
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index 9a4beed871..08e67a0c2f 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -13,7 +13,7 @@ open Genredexpr
open Glob_term
open Glob_ops
open Tacred
-open Errors
+open CErrors
open Util
open Names
open Nameops
@@ -209,7 +209,7 @@ let catching_error call_trace fail (e, info) =
in
if List.is_empty call_trace && List.is_empty inner_trace then fail (e, info)
else begin
- assert (Errors.noncritical e); (* preserved invariant *)
+ assert (CErrors.noncritical e); (* preserved invariant *)
let new_trace = inner_trace @ call_trace in
let located_exc = (e, Exninfo.add info ltac_trace_info new_trace) in
fail located_exc
@@ -217,8 +217,8 @@ let catching_error call_trace fail (e, info) =
let catch_error call_trace f x =
try f x
- with e when Errors.noncritical e ->
- let e = Errors.push e in
+ with e when CErrors.noncritical e ->
+ let e = CErrors.push e in
catching_error call_trace iraise e
let catch_error_tac call_trace tac =
@@ -289,7 +289,7 @@ let constr_of_id env id =
(* Some of the code further down depends on the fact that push_trace does not modify sigma (the evar map) *)
let push_trace call ist = match TacStore.get ist.extra f_trace with
| None -> Proofview.tclUNIT [call]
-| Some trace -> Proofview.tclLIFT (Proofview.NonLogical.make Profile_ltac.entered_call) <*> Proofview.tclUNIT (call :: trace)
+| Some trace -> Proofview.tclUNIT (call :: trace)
let propagate_trace ist loc id v =
let v = Value.normalize v in
@@ -813,7 +813,7 @@ let interp_may_eval f ist env sigma = function
try
f ist env sigma c
with reraise ->
- let reraise = Errors.push reraise in
+ let reraise = CErrors.push reraise in
(* spiwack: to avoid unnecessary modifications of tacinterp, as this
function already use effect, I call [run] hoping it doesn't mess
up with any assumption. *)
@@ -827,7 +827,7 @@ let interp_constr_may_eval ist env sigma c =
try
interp_may_eval interp_constr ist env sigma c
with reraise ->
- let reraise = Errors.push reraise in
+ let reraise = CErrors.push reraise in
(* spiwack: to avoid unnecessary modifications of tacinterp, as this
function already use effect, I call [run] hoping it doesn't mess
up with any assumption. *)
@@ -1822,13 +1822,10 @@ and interp_atomic ist tac : unit Proofview.tactic =
(* Conversion *)
| TacReduce (r,cl) ->
- (* spiwack: until the tactic is in the monad *)
- Proofview.Trace.name_tactic (fun () -> Pp.str"<reduce>") begin
Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
let (sigma,r_interp) = interp_red_expr ist (pf_env gl) (project gl) r in
Sigma.Unsafe.of_pair (Tactics.reduce r_interp (interp_clause ist (pf_env gl) (project gl) cl), sigma)
end }
- end
| TacChange (None,c,cl) ->
(* spiwack: until the tactic is in the monad *)
Proofview.Trace.name_tactic (fun () -> Pp.str"<change>") begin
@@ -1867,7 +1864,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
let env = Proofview.Goal.env gl in
let sigma = project gl in
let op = interp_typed_pattern ist env sigma op in
- let to_catch = function Not_found -> true | e -> Errors.is_anomaly e in
+ let to_catch = function Not_found -> true | e -> CErrors.is_anomaly e in
let c_interp patvars = { Sigma.run = begin fun sigma ->
let lfun' = Id.Map.fold (fun id c lfun ->
Id.Map.add id (Value.of_constr c) lfun)
diff --git a/ltac/tactic_debug.ml b/ltac/tactic_debug.ml
index 73d04b810d..e1c9fed637 100644
--- a/ltac/tactic_debug.ml
+++ b/ltac/tactic_debug.ml
@@ -36,10 +36,11 @@ type debug_info =
(* An exception handler *)
let explain_logic_error e =
- Errors.print (fst (Cerrors.process_vernac_interp_error (e, Exninfo.null)))
+ CErrors.print (fst (ExplainErr.process_vernac_interp_error (e, Exninfo.null)))
let explain_logic_error_no_anomaly e =
- Errors.print_no_report (fst (Cerrors.process_vernac_interp_error (e, Exninfo.null)))
+ CErrors.print_no_report
+ (fst (ExplainErr.process_vernac_interp_error (e, Exninfo.null)))
let msg_tac_debug s = Proofview.NonLogical.print_debug (s++fnl())
let msg_tac_notice s = Proofview.NonLogical.print_notice (s++fnl())
@@ -417,4 +418,4 @@ let get_ltac_trace (_, info) =
| None -> None
| Some trace -> Some (extract_ltac_trace trace loc)
-let () = Cerrors.register_additional_error_info get_ltac_trace
+let () = ExplainErr.register_additional_error_info get_ltac_trace
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 05:10:47 +0000