From e8a6467545c2814c9418889201e8be19c0cef201 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 18 Jan 2017 15:46:23 +0100 Subject: [location] Make location optional in Loc.located This completes the Loc.ghost removal, the idea is to gear the API towards optional, but uniform, location handling. We don't print anymore in the case there is no location. This is what the test suite expects. The old printing logic for located items was a bit inconsistent as it sometimes printed and other times it printed nothing as the caller checked for `is_ghost` upstream. --- tactics/autorewrite.ml | 10 +++++----- tactics/autorewrite.mli | 6 +++--- tactics/hints.ml | 4 ++-- tactics/inv.ml | 4 ++-- tactics/tacticals.ml | 6 +++--- tactics/tactics.ml | 26 +++++++++++++------------- 6 files changed, 28 insertions(+), 28 deletions(-) (limited to 'tactics') diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index e58ec5a31f..ff8b54ebfb 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -86,7 +86,7 @@ let print_rewrite_hintdb bas = Pputils.pr_glb_generic (Global.env()) tac) (mt ()) h.rew_tac) (find_rewrites bas)) -type raw_rew_rule = Loc.t * constr Univ.in_universe_context_set * bool * Genarg.raw_generic_argument option +type raw_rew_rule = (constr Univ.in_universe_context_set * bool * Genarg.raw_generic_argument option) Loc.located (* Applies all the rules of one base *) let one_base general_rewrite_maybe_in tac_main bas = @@ -291,12 +291,12 @@ let decompose_applied_relation metas env sigma c ctype left2right = | Some c -> Some c | None -> None -let find_applied_relation metas loc env sigma c left2right = +let find_applied_relation ?loc metas env sigma c left2right = let ctype = Typing.unsafe_type_of env sigma (EConstr.of_constr c) in match decompose_applied_relation metas env sigma c ctype left2right with | Some c -> c | None -> - user_err ~loc ~hdr:"decompose_applied_relation" + user_err ?loc ~hdr:"decompose_applied_relation" (str"The type" ++ spc () ++ Printer.pr_econstr_env env sigma ctype ++ spc () ++ str"of this term does not end with an applied relation.") @@ -309,9 +309,9 @@ let add_rew_rules base lrul = let intern tac = snd (Genintern.generic_intern ist tac) in let lrul = List.fold_left - (fun dn (loc,(c,ctx),b,t) -> + (fun dn (loc,((c,ctx),b,t)) -> let sigma = Evd.merge_context_set Evd.univ_rigid sigma ctx in - let info = find_applied_relation false loc env sigma c b in + let info = find_applied_relation ?loc false env sigma c b in let pat = if b then info.hyp_left else info.hyp_right in let rul = { rew_lemma = c; rew_type = info.hyp_ty; rew_pat = pat; rew_ctx = ctx; rew_l2r = b; diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli index 49e8588da3..f765318d04 100644 --- a/tactics/autorewrite.mli +++ b/tactics/autorewrite.mli @@ -12,7 +12,7 @@ open Term open Equality (** Rewriting rules before tactic interpretation *) -type raw_rew_rule = Loc.t * constr Univ.in_universe_context_set * bool * Genarg.raw_generic_argument option +type raw_rew_rule = (constr Univ.in_universe_context_set * bool * Genarg.raw_generic_argument option) Loc.located (** To add rewriting rules to a base *) val add_rew_rules : string -> raw_rew_rule list -> unit @@ -56,7 +56,7 @@ type hypinfo = { hyp_right : constr; } -val find_applied_relation : bool -> - Loc.t -> +val find_applied_relation : + ?loc:Loc.t -> bool -> Environ.env -> Evd.evar_map -> Term.constr -> bool -> hypinfo diff --git a/tactics/hints.ml b/tactics/hints.ml index bcc068d3da..52e3dd09fe 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1282,7 +1282,7 @@ let interp_hints poly = prepare_hint true (poly,false) (Global.env()) Evd.empty (evd,c) in let fref r = let gr = global_with_alias r in - Dumpglob.add_glob (loc_of_reference r) gr; + Dumpglob.add_glob ?loc:(loc_of_reference r) gr; gr in let fr r = evaluable_of_global_reference (Global.env()) (fref r) @@ -1311,7 +1311,7 @@ let interp_hints poly = let constr_hints_of_ind qid = let ind = global_inductive_with_alias qid in let mib,_ = Global.lookup_inductive ind in - Dumpglob.dump_reference (fst (qualid_of_reference qid)) "<>" (string_of_reference qid) "ind"; + Dumpglob.dump_reference ?loc:(fst (qualid_of_reference qid)) "<>" (string_of_reference qid) "ind"; List.init (nconstructors ind) (fun i -> let c = (ind,i+1) in let gr = ConstructRef c in diff --git a/tactics/inv.ml b/tactics/inv.ml index f2147db40a..a50ac31e1d 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -283,9 +283,9 @@ let generalizeRewriteIntros as_mode tac depids id = end } let error_too_many_names pats = - let loc = Loc.merge (fst (List.hd pats)) (fst (List.last pats)) in + let loc = Loc.merge_opt (fst (List.hd pats)) (fst (List.last pats)) in Proofview.tclENV >>= fun env -> - tclZEROMSG ~loc ( + tclZEROMSG ?loc ( str "Unexpected " ++ str (String.plural (List.length pats) "introduction pattern") ++ str ": " ++ pr_enum (Miscprint.pr_intro_pattern (fun c -> Printer.pr_constr (EConstr.Unsafe.to_constr (fst (run_delayed env Evd.empty c))))) pats ++ diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 074c8b9de8..5c89331b88 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -187,7 +187,7 @@ let check_or_and_pattern_size ?loc check_and names branchsigns = | IntroAndPattern l -> if not (Int.equal n 1) then errn n; let l' = List.filter (function _,IntroForthcoming _ -> true | _,IntroNaming _ | _,IntroAction _ -> false) l in - if l' != [] then errforthcoming ~loc:(fst (List.hd l')); + if l' != [] then errforthcoming ?loc:(fst (List.hd l')); if check_and then let p1 = List.count (fun x -> x) branchsigns.(0) in let p2 = List.length branchsigns.(0) in @@ -221,7 +221,7 @@ let compute_induction_names_gen check_and branchletsigns = function Array.make (Array.length branchletsigns) [] | Some (loc,names) -> let names = fix_empty_or_and_pattern (Array.length branchletsigns) names in - get_and_check_or_and_pattern_gen check_and ~loc names branchletsigns + get_and_check_or_and_pattern_gen check_and ?loc names branchletsigns let compute_induction_names = compute_induction_names_gen true @@ -492,7 +492,7 @@ module New = struct | [] -> () | (evk,evi) :: _ -> let (loc,_) = evi.Evd.evar_source in - Pretype_errors.error_unsolvable_implicit ~loc env sigma evk None + Pretype_errors.error_unsolvable_implicit ?loc env sigma evk None let tclWITHHOLES accept_unresolved_holes tac sigma = tclEVARMAP >>= fun sigma_initial -> diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 7dad90242c..d265269b8a 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -443,7 +443,7 @@ let find_name mayrepl decl naming gl = match naming with let ids_of_hyps = Tacmach.New.pf_ids_of_hyps gl in let id' = next_ident_away id ids_of_hyps in if not mayrepl && not (Id.equal id' id) then - user_err ~loc (pr_id id ++ str" is already used."); + user_err ?loc (pr_id id ++ str" is already used."); id (**************************************************************) @@ -1734,7 +1734,7 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind : with Redelimination -> (* Last chance: if the head is a variable, apply may try second order unification *) - let info = Loc.add_loc info loc in + let info = Option.cata (fun loc -> Loc.add_loc info loc) info loc in let tac = if with_destruct then descend_in_conjunctions [] @@ -1838,8 +1838,8 @@ let progress_with_clause flags innerclause clause = try List.find_map f ordered_metas with Not_found -> raise UnableToApply -let explain_unable_to_apply_lemma loc env sigma thm innerclause = - user_err ~loc (hov 0 +let explain_unable_to_apply_lemma ?loc env sigma thm innerclause = + user_err ?loc (hov 0 (Pp.str "Unable to apply lemma of type" ++ brk(1,1) ++ Pp.quote (Printer.pr_leconstr_env env sigma thm) ++ spc() ++ str "on hypothesis of type" ++ brk(1,1) ++ @@ -1855,7 +1855,7 @@ let apply_in_once_main flags innerclause env sigma (loc,d,lbind) = try aux (clenv_push_prod clause) with NotExtensibleClause -> match e with - | UnableToApply -> explain_unable_to_apply_lemma loc env sigma thm innerclause + | UnableToApply -> explain_unable_to_apply_lemma ?loc env sigma thm innerclause | _ -> iraise e' in aux (make_clenv_binding env sigma (d,thm) lbind) @@ -2281,7 +2281,7 @@ let error_unexpected_extra_pattern loc bound pat = | IntroNaming (IntroIdentifier _) -> "name", (String.plural nb " introduction pattern"), "no" | _ -> "introduction pattern", "", "none" in - user_err ~loc (str "Unexpected " ++ str s1 ++ str " (" ++ + user_err ?loc (str "Unexpected " ++ str s1 ++ str " (" ++ (if Int.equal nb 0 then (str s3 ++ str s2) else (str "at most " ++ int nb ++ str s2)) ++ spc () ++ str (if Int.equal nb 1 then "was" else "were") ++ @@ -2461,7 +2461,7 @@ let rec intro_patterns_core with_evars b avoid ids thin destopt bound n tac = | IntroAction pat -> intro_then_gen (make_tmp_naming avoid l pat) destopt true false - (intro_pattern_action ~loc with_evars (b || not (List.is_empty l)) false + (intro_pattern_action ?loc with_evars (b || not (List.is_empty l)) false pat thin destopt (fun thin bound' -> intro_patterns_core with_evars b avoid ids thin destopt bound' 0 (fun ids thin -> @@ -2498,9 +2498,9 @@ and intro_pattern_action ?loc with_evars b style pat thin destopt tac id = rewrite_hyp_then style with_evars thin l2r id (fun thin -> tac thin None []) | IntroApplyOn ((loc',f),(loc,pat)) -> let naming,tac_ipat = - prepare_intros ~loc with_evars (IntroIdentifier id) destopt pat in + prepare_intros ?loc with_evars (IntroIdentifier id) destopt pat in let doclear = - if naming = NamingMustBe (Loc.tag ~loc id) then + if naming = NamingMustBe (Loc.tag ?loc id) then Proofview.tclUNIT () (* apply_in_once do a replacement *) else clear [id] in @@ -2549,7 +2549,7 @@ let intros_patterns with_evars = function let prepare_intros_opt with_evars dft destopt = function | None -> prepare_naming dft, (fun _id -> Proofview.tclUNIT ()) - | Some (loc,ipat) -> prepare_intros ~loc with_evars dft destopt ipat + | Some (loc,ipat) -> prepare_intros ?loc with_evars dft destopt ipat let ipat_of_name = function | Anonymous -> None @@ -2692,7 +2692,7 @@ let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty = | IntroFresh heq_base -> fresh_id_in_env [id] heq_base env | IntroIdentifier id -> if List.mem id (ids_of_named_context (named_context env)) then - user_err ~loc (pr_id id ++ str" is already used."); + user_err ?loc (pr_id id ++ str" is already used."); id in let eqdata = build_coq_eq_data () in let args = if lr then [t;mkVar id;c] else [t;c;mkVar id]in @@ -2973,7 +2973,7 @@ let specialize (c,lbind) ipat = | Some (loc,ipat) -> (* Like pose proof with extra support for "with" bindings *) (* even though the "with" bindings forces full application *) - let naming,tac = prepare_intros ~loc false IntroAnonymous MoveLast ipat in + let naming,tac = prepare_intros ?loc false IntroAnonymous MoveLast ipat in Tacticals.New.tclTHENFIRST (assert_before_then_gen false naming typ tac) (exact_no_check term) @@ -4467,7 +4467,7 @@ let induction_gen_l isrec with_evars elim names lc = let lc = List.map (function | (c,None) -> c | (c,Some(loc,eqname)) -> - user_err ~loc (str "Do not know what to do with " ++ + user_err ?loc (str "Do not know what to do with " ++ Miscprint.pr_intro_pattern_naming eqname)) lc in let rec atomize_list l = match l with -- cgit v1.2.3