diff options
Diffstat (limited to 'plugins/ssr/ssrcommon.ml')
| -rw-r--r-- | plugins/ssr/ssrcommon.ml | 81 |
1 files changed, 3 insertions, 78 deletions
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 80d421b9fc..efc4a2c743 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -1000,7 +1000,7 @@ let applyn ~with_evars ?beta ?(with_shelve=false) n t gl = | _ -> assert false in loop sigma t [] n in pp(lazy(str"Refiner.refiner " ++ Printer.pr_econstr_env (pf_env gl) (project gl) t)); - Tacmach.refine_no_check t gl + Refiner.refiner ~check:false EConstr.Unsafe.(to_constr t) gl let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc gl = let rec mkRels = function 1 -> [] | n -> mkRel n :: mkRels (n-1) in @@ -1017,81 +1017,6 @@ let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc gl = try applyn ~with_evars ~with_shelve:true ?beta n (EConstr.of_constr oc) gl with e when CErrors.noncritical e -> raise dependent_apply_error -(** Profiling *)(* {{{ *************************************************************) -type profiler = { - profile : 'a 'b. ('a -> 'b) -> 'a -> 'b; - reset : unit -> unit; - print : unit -> unit } -let profile_now = ref false -let something_profiled = ref false -let profilers = ref [] -let add_profiler f = profilers := f :: !profilers;; -let _ = - Goptions.declare_bool_option - { Goptions.optname = "ssreflect profiling"; - Goptions.optkey = ["SsrProfiling"]; - Goptions.optread = (fun _ -> !profile_now); - Goptions.optdepr = false; - Goptions.optwrite = (fun b -> - Ssrmatching.profile b; - profile_now := b; - if b then List.iter (fun f -> f.reset ()) !profilers; - if not b then List.iter (fun f -> f.print ()) !profilers) } -let () = - let prof_total = - let init = ref 0.0 in { - profile = (fun f x -> assert false); - reset = (fun () -> init := Unix.gettimeofday ()); - print = (fun () -> if !something_profiled then - prerr_endline - (Printf.sprintf "!! %-39s %10d %9.4f %9.4f %9.4f" - "total" 0 (Unix.gettimeofday() -. !init) 0.0 0.0)) } in - let prof_legenda = { - profile = (fun f x -> assert false); - reset = (fun () -> ()); - print = (fun () -> if !something_profiled then begin - prerr_endline - (Printf.sprintf "!! %39s ---------- --------- --------- ---------" - (String.make 39 '-')); - prerr_endline - (Printf.sprintf "!! %-39s %10s %9s %9s %9s" - "function" "#calls" "total" "max" "average") end) } in - add_profiler prof_legenda; - add_profiler prof_total -;; - -let mk_profiler s = - let total, calls, max = ref 0.0, ref 0, ref 0.0 in - let reset () = total := 0.0; calls := 0; max := 0.0 in - let profile f x = - if not !profile_now then f x else - let before = Unix.gettimeofday () in - try - incr calls; - let res = f x in - let after = Unix.gettimeofday () in - let delta = after -. before in - total := !total +. delta; - if delta > !max then max := delta; - res - with exc -> - let after = Unix.gettimeofday () in - let delta = after -. before in - total := !total +. delta; - if delta > !max then max := delta; - raise exc in - let print () = - if !calls <> 0 then begin - something_profiled := true; - prerr_endline - (Printf.sprintf "!! %-39s %10d %9.4f %9.4f %9.4f" - s !calls !total !max (!total /. (float_of_int !calls))) end in - let prof = { profile = profile; reset = reset; print = print } in - add_profiler prof; - prof -;; -(* }}} *) - (* We wipe out all the keywords generated by the grammar rules we defined. *) (* The user is supposed to Require Import ssreflect or Require ssreflect *) (* and Import ssreflect.SsrSyntax to obtain these keywords and as a *) @@ -1167,8 +1092,8 @@ let tclDO n tac = let _, info = CErrors.push e in let e' = CErrors.UserError (l, prefix i ++ s) in Util.iraise (e', info) - | Ploc.Exc(loc, CErrors.UserError (l, s)) -> - raise (Ploc.Exc(loc, CErrors.UserError (l, prefix i ++ s))) in + | Gramlib.Ploc.Exc(loc, CErrors.UserError (l, s)) -> + raise (Gramlib.Ploc.Exc(loc, CErrors.UserError (l, prefix i ++ s))) in let rec loop i gl = if i = n then tac_err_at i gl else (tclTHEN (tac_err_at i) (loop (i + 1))) gl in |