From 738551a294d5d8393253568764f9bea4cf45f7c5 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 19 Apr 2015 12:39:37 +0200 Subject: Slightly more efficient implementation of the logic monad. We just inline the state in the iolist: less closures makes the GC happier. --- proofs/logic_monad.ml | 120 +++++++++++++++++++++++--------------------------- 1 file changed, 56 insertions(+), 64 deletions(-) (limited to 'proofs') diff --git a/proofs/logic_monad.ml b/proofs/logic_monad.ml index d509670ec2..cb3e5a1860 100644 --- a/proofs/logic_monad.ml +++ b/proofs/logic_monad.ml @@ -208,118 +208,110 @@ struct type rich_exn = Exninfo.iexn type 'a iolist = - { iolist : 'r. (rich_exn -> 'r NonLogical.t) -> - ('a -> (rich_exn -> 'r NonLogical.t) -> 'r NonLogical.t) -> - 'r NonLogical.t } + { iolist : 'r. state -> (rich_exn -> 'r NonLogical.t) -> + ('a -> state -> (rich_exn -> 'r NonLogical.t) -> 'r NonLogical.t) -> + 'r NonLogical.t } include Monad.Make(struct - type 'a t = state -> ('a * state) iolist - let return x : 'a t = (); fun s -> - { iolist = fun nil cons -> cons (x, s) nil } + type 'a t = 'a iolist - let (>>=) (m : 'a t) (f : 'a -> 'b t) : 'b t = (); fun s -> - let m = m s in - { iolist = fun nil cons -> - m.iolist nil (fun (x, s) next -> (f x s).iolist next cons) } + let return x = + { iolist = fun s nil cons -> cons x s nil } - let (>>) (m : unit t) (f : 'a t) : 'a t = (); fun s -> - let m = m s in - { iolist = fun nil cons -> - m.iolist nil (fun ((), s) next -> (f s).iolist next cons) } + let (>>=) m f = + { iolist = fun s nil cons -> + m.iolist s nil (fun x s next -> (f x).iolist s next cons) } - let map (f : 'a -> 'b) (m : 'a t) : 'b t = (); fun s -> - let m = m s in - { iolist = fun nil cons -> m.iolist nil (fun (x, s) next -> cons (f x, s) next) } + let (>>) m f = + { iolist = fun s nil cons -> + m.iolist s nil (fun () s next -> f.iolist s next cons) } + + let map f m = + { iolist = fun s nil cons -> m.iolist s nil (fun x s next -> cons (f x) s next) } end) - let zero e : 'a t = (); fun s -> - { iolist = fun nil cons -> nil e } + let zero e = + { iolist = fun _ nil cons -> nil e } - let plus m1 m2 : 'a t = (); fun s -> - let m1 = m1 s in - { iolist = fun nil cons -> m1.iolist (fun e -> (m2 e s).iolist nil cons) cons } + let plus m1 m2 = + { iolist = fun s nil cons -> m1.iolist s (fun e -> (m2 e).iolist s nil cons) cons } - let ignore (m : 'a t) : unit t = (); fun s -> - let m = m s in - { iolist = fun nil cons -> m.iolist nil (fun (_, s) next -> cons ((), s) next) } + let ignore m = + { iolist = fun s nil cons -> m.iolist s nil (fun _ s next -> cons () s next) } - let lift (m : 'a NonLogical.t) : 'a t = (); fun s -> - { iolist = fun nil cons -> NonLogical.(m >>= fun x -> cons (x, s) nil) } + let lift m = + { iolist = fun s nil cons -> NonLogical.(m >>= fun x -> cons x s nil) } (** State related *) - let get : P.s t = (); fun s -> - { iolist = fun nil cons -> cons (s.sstate, s) nil } + let get = + { iolist = fun s nil cons -> cons s.sstate s nil } - let set (sstate : P.s) : unit t = (); fun s -> - { iolist = fun nil cons -> cons ((), { s with sstate }) nil } + let set (sstate : P.s) = + { iolist = fun s nil cons -> cons () { s with sstate } nil } - let modify (f : P.s -> P.s) : unit t = (); fun s -> - { iolist = fun nil cons -> cons ((), { s with sstate = f s.sstate }) nil } + let modify (f : P.s -> P.s) = + { iolist = fun s nil cons -> cons () { s with sstate = f s.sstate } nil } - let current : P.e t = (); fun s -> - { iolist = fun nil cons -> cons (s.rstate, s) nil } + let current = + { iolist = fun s nil cons -> cons s.rstate s nil } - let local (type a) (e:P.e) (m:a t) : a t = (); fun s -> - let m = m { s with rstate = e } in - { iolist = fun nil cons -> - m.iolist nil (fun (x,s') next -> cons (x,{s' with rstate=s.rstate}) next) } + let local e m = + { iolist = fun s nil cons -> + m.iolist { s with rstate = e } nil + (fun x s' next -> cons x {s' with rstate = s.rstate} next) } - let put (w : P.w) : unit t = (); fun s -> - { iolist = fun nil cons -> cons ((), { s with wstate = P.wprod s.wstate w }) nil } + let put w = + { iolist = fun s nil cons -> cons () { s with wstate = P.wprod s.wstate w } nil } - let update (f : P.u -> P.u) : unit t = (); fun s -> - { iolist = fun nil cons -> cons ((), { s with ustate = f s.ustate }) nil } + let update (f : P.u -> P.u) = + { iolist = fun s nil cons -> cons () { s with ustate = f s.ustate } nil } (** List observation *) - let once (m : 'a t) : 'a t = (); fun s -> - let m = m s in - { iolist = fun nil cons -> m.iolist nil (fun x _ -> cons x nil) } + let once m = + { iolist = fun s nil cons -> m.iolist s nil (fun x s _ -> cons x s nil) } - let break (f : rich_exn -> rich_exn option) (m : 'a t) : 'a t = (); fun s -> - let m = m s in - { iolist = fun nil cons -> - m.iolist nil (fun x next -> cons x (fun e -> match f e with None -> next e | Some e -> nil e)) + let break f m = + { iolist = fun s nil cons -> + m.iolist s nil (fun x s next -> cons x s (fun e -> match f e with None -> next e | Some e -> nil e)) } (** For [reflect] and [split] see the "Backtracking, Interleaving, and Terminating Monad Transformers" paper. *) type 'a reified = ('a, rich_exn -> 'a reified) list_view NonLogical.t - let rec reflect (m : 'a reified) : 'a iolist = - { iolist = fun nil cons -> + let rec reflect (m : ('a * state) reified) : 'a iolist = + { iolist = fun s0 nil cons -> let next = function | Nil e -> nil e - | Cons (x, l) -> cons x (fun e -> (reflect (l e)).iolist nil cons) + | Cons ((x, s), l) -> cons x s (fun e -> (reflect (l e)).iolist s0 nil cons) in NonLogical.(m >>= next) } - let split (m : 'a t) : ('a, rich_exn -> 'a t) list_view t = (); fun s -> - let m = m s in + let split m : ('a, rich_exn -> 'a t) list_view t = let rnil e = NonLogical.return (Nil e) in - let rcons p l = NonLogical.return (Cons (p, l)) in - { iolist = fun nil cons -> + let rcons p s l = NonLogical.return (Cons ((p, s), l)) in + { iolist = fun s nil cons -> let open NonLogical in - m.iolist rnil rcons >>= begin function - | Nil e -> cons (Nil e, s) nil + m.iolist s rnil rcons >>= begin function + | Nil e -> cons (Nil e) s nil | Cons ((x, s), l) -> - let l e = (); fun _ -> reflect (l e) in - cons (Cons (x, l), s) nil + let l e = reflect (l e) in + cons (Cons (x, l)) s nil end } let run m r s = let s = { wstate = P.wunit; ustate = P.uunit; rstate = r; sstate = s } in - let m = m s in let rnil e = NonLogical.return (Nil e) in - let rcons (x, s) l = + let rcons x s l = let p = (x, s.sstate, s.wstate, s.ustate) in NonLogical.return (Cons (p, l)) in - m.iolist rnil rcons + m.iolist s rnil rcons let repr x = x -- cgit v1.2.3 From 501d6dd5691474c807a722d9b5b6e3fa9d83c749 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Wed, 22 Apr 2015 18:51:48 +0200 Subject: Tactical `progress` compares term up to potentially equalisable universes. Followup of: f7b29094fe7cc13ea475447bd30d9a8b942f0fef . In particular, re-closes #3593. As a side effect, fixes an undiscovered bug of the `eq_constr` tactic which didn't consider terms up to evar instantiation.--- proofs/proofview.ml | 14 +------------- 1 file changed, 1 insertion(+), 13 deletions(-) (limited to 'proofs') diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 6f62634133..6e653806b7 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -722,19 +722,7 @@ let give_up = module Progress = struct - (** equality function up to evar instantiation in heterogeneous - contexts. *) - (* spiwack (2015-02-19): In the previous version of progress an - equality which considers two universes equal when it is consistent - tu unify them ([Evd.eq_constr_univs_test]) was used. Maybe this - behaviour has to be restored as well. This has to be established by - practice. *) - - let rec eq_constr sigma1 sigma2 t1 t2 = - Constr.equal_with - (fun t -> Evarutil.kind_of_term_upto sigma1 t) - (fun t -> Evarutil.kind_of_term_upto sigma2 t) - t1 t2 + let eq_constr = Evarutil.eq_constr_univs_test (** equality function on hypothesis contexts *) let eq_named_context_val sigma1 sigma2 ctx1 ctx2 = -- cgit v1.2.3 From 16d301bab5b7dec53be4786b3b6815bca54ae539 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Thu, 23 Apr 2015 14:55:11 +0200 Subject: Remove almost all the uses of string concatenation when building error messages. Since error messages are ultimately passed to Format, which has its own buffers for concatenating strings, using concatenation for preparing error messages just doubles the workload and increases memory pressure. --- proofs/evar_refiner.ml | 5 +++-- proofs/logic.ml | 22 ++++++++++++---------- proofs/redexpr.ml | 11 +++++++---- proofs/tactic_debug.ml | 14 +++++++------- 4 files changed, 29 insertions(+), 23 deletions(-) (limited to 'proofs') diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index c8cb1d1cc2..9b358210a0 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -12,6 +12,7 @@ open Names open Evd open Evarutil open Evarsolve +open Pp (******************************************) (* Instantiation of existential variables *) @@ -54,8 +55,8 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma = with e when Errors.noncritical e -> let loc = Glob_ops.loc_of_glob_constr rawc in user_err_loc - (loc,"",Pp.str ("Instance is not well-typed in the environment of " ^ - string_of_existential evk)) + (loc,"", str "Instance is not well-typed in the environment of " ++ + str (string_of_existential evk)) in define_and_solve_constraints evk typed_c env (evars_reset_evd sigma' sigma) diff --git a/proofs/logic.ml b/proofs/logic.ml index b8206ca1b5..898588d9e4 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -179,7 +179,8 @@ let check_decl_position env sign (x,_,_ as d) = let needed = global_vars_set_of_decl env d in let deps = dependency_closure env (named_context_of_val sign) needed in if Id.List.mem x deps then - error ("Cannot create self-referring hypothesis "^Id.to_string x); + errorlabstrm "Logic.check_decl_position" + (str "Cannot create self-referring hypothesis " ++ pr_id x); x::deps (* Auxiliary functions for primitive MOVE tactic @@ -488,9 +489,11 @@ let convert_hyp check sign sigma (id,b,bt as d) = (fun _ (_,c,ct) _ -> let env = Global.env_of_context sign in if check && not (is_conv env sigma bt ct) then - error ("Incorrect change of the type of "^(Id.to_string id)^"."); + errorlabstrm "Logic.convert_hyp" + (str "Incorrect change of the type of " ++ pr_id id ++ str "."); if check && not (Option.equal (is_conv env sigma) b c) then - error ("Incorrect change of the body of "^(Id.to_string id)^"."); + errorlabstrm "Logic.convert_hyp" + (str "Incorrect change of the body of "++ pr_id id ++ str "."); if check then reorder := check_decl_position env sign d; d) in reorder_val_context env sign' !reorder @@ -522,7 +525,8 @@ let prim_refiner r sigma goal = t,cl,sigma else (if !check && mem_named_context id (named_context_of_val sign) then - error ("Variable " ^ Id.to_string id ^ " is already declared."); + errorlabstrm "Logic.prim_refiner" + (str "Variable " ++ pr_id id ++ str " is already declared."); push_named_context_val (id,None,t) sign,t,cl,sigma) in let (sg2,ev2,sigma) = Goal.V82.mk_goal sigma sign cl (Goal.V82.extra sigma goal) in @@ -550,11 +554,10 @@ let prim_refiner r sigma goal = | (f,n,ar)::oth -> let ((sp',_),u') = check_ind env n ar in if not (eq_mind sp sp') then - error ("Fixpoints should be on the same " ^ - "mutual inductive declaration."); + error "Fixpoints should be on the same mutual inductive declaration."; if !check && mem_named_context f (named_context_of_val sign) then - error - ("Name "^Id.to_string f^" already used in the environment"); + errorlabstrm "Logic.prim_refiner" + (str "Name " ++ pr_id f ++ str " already used in the environment"); mk_sign (push_named_context_val (f,None,ar) sign) oth | [] -> Evd.Monad.List.map (fun (_,_,c) sigma -> @@ -584,8 +587,7 @@ let prim_refiner r sigma goal = try let _ = find_coinductive env sigma b in () with Not_found -> - error ("All methods must construct elements " ^ - "in coinductive types.") + error "All methods must construct elements in coinductive types." in let firsts,lasts = List.chop j others in let all = firsts@(f,cl)::lasts in diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 1383d75567..d25f7e9150 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -167,18 +167,20 @@ let red_expr_tab = Summary.ref String.Map.empty ~name:"Declare Reduction" let declare_reduction s f = if String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab - then error ("There is already a reduction expression of name "^s) + then errorlabstrm "Redexpr.declare_reduction" + (str "There is already a reduction expression of name " ++ str s) else reduction_tab := String.Map.add s f !reduction_tab let check_custom = function | ExtraRedExpr s -> if not (String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab) - then error ("Reference to undefined reduction expression "^s) + then errorlabstrm "Redexpr.check_custom" (str "Reference to undefined reduction expression " ++ str s) |_ -> () let decl_red_expr s e = if String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab - then error ("There is already a reduction expression of name "^s) + then errorlabstrm "Redexpr.decl_red_expr" + (str "There is already a reduction expression of name " ++ str s) else begin check_custom e; red_expr_tab := String.Map.add s e !red_expr_tab @@ -232,7 +234,8 @@ let reduction_of_red_expr env = with Not_found -> (try reduction_of_red_expr (String.Map.find s !red_expr_tab) with Not_found -> - error("unknown user-defined reduction \""^s^"\""))) + errorlabstrm "Redexpr.reduction_of_red_expr" + (str "unknown user-defined reduction \"" ++ str s ++ str "\""))) | CbvVm o -> (contextualize cbv_vm cbv_vm o, VMcast) | CbvNative o -> (contextualize cbv_native cbv_native o, NATIVEcast) in diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml index 3cc81daf58..d7f4b5ead5 100644 --- a/proofs/tactic_debug.ml +++ b/proofs/tactic_debug.ml @@ -11,6 +11,7 @@ open Names open Pp open Tacexpr open Termops +open Nameops let (prtac, tactic_printer) = Hook.make () let (prmatchpatt, match_pattern_printer) = Hook.make () @@ -231,17 +232,16 @@ let db_pattern_rule debug num r = (* Prints the hypothesis pattern identifier if it exists *) let hyp_bound = function - | Anonymous -> " (unbound)" - | Name id -> " (bound to "^(Names.Id.to_string id)^")" + | Anonymous -> str " (unbound)" + | Name id -> str " (bound to " ++ pr_id id ++ str ")" (* Prints a matched hypothesis *) let db_matched_hyp debug env (id,_,c) ido = let open Proofview.NonLogical in is_debug debug >>= fun db -> if db then - msg_tac_debug (str "Hypothesis " ++ - str ((Names.Id.to_string id)^(hyp_bound ido)^ - " has been matched: ") ++ print_constr_env env c) + msg_tac_debug (str "Hypothesis " ++ pr_id id ++ hyp_bound ido ++ + str " has been matched: " ++ print_constr_env env c) else return () (* Prints the matched conclusion *) @@ -266,8 +266,8 @@ let db_hyp_pattern_failure debug env sigma (na,hyp) = let open Proofview.NonLogical in is_debug debug >>= fun db -> if db then - msg_tac_debug (str ("The pattern hypothesis"^(hyp_bound na)^ - " cannot match: ") ++ + msg_tac_debug (str "The pattern hypothesis" ++ hyp_bound na ++ + str " cannot match: " ++ Hook.get prmatchpatt env sigma hyp) else return () -- cgit v1.2.3