From b1d749e59444f86e40f897c41739168bb1b1b9b3 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 25 Feb 2018 22:43:42 +0100 Subject: [located] Push inner locations in `reference` to a CAst.t node. The `reference` type contains some ad-hoc locations in its constructors, but there is no reason not to handle them with the standard attribute container provided by `CAst.t`. An orthogonal topic to this commit is whether the `reference` type should contain a location or not at all. It seems that many places would become a bit clearer by splitting `reference` into non-located `reference` and `lreference`, however some other places become messier so we maintain the current status-quo for now. --- plugins/ltac/tacintern.ml | 55 +++++++++++++++++++++++------------------------ 1 file changed, 27 insertions(+), 28 deletions(-) (limited to 'plugins/ltac/tacintern.ml') diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 45f4a45fc..9ad9e1520 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -92,15 +92,15 @@ let intern_int_or_var = intern_or_var (fun (n : int) -> n) let intern_string_or_var = intern_or_var (fun (s : string) -> s) let intern_global_reference ist = function - | Ident (loc,id) when find_var id ist -> + | {CAst.loc;v=Ident id} when find_var id ist -> ArgVar (make ?loc id) | r -> - let loc,_ as lqid = qualid_of_reference r in - try ArgArg (loc,locate_global_with_alias lqid) - with Not_found -> error_global_not_found (snd lqid) + let {CAst.loc} as lqid = qualid_of_reference r in + try ArgArg (loc,locate_global_with_alias lqid) + with Not_found -> error_global_not_found lqid let intern_ltac_variable ist = function - | Ident (loc,id) -> + | {loc;v=Ident id} -> if find_var id ist then (* A local variable of any type *) ArgVar (make ?loc id) @@ -109,19 +109,19 @@ let intern_ltac_variable ist = function raise Not_found let intern_constr_reference strict ist = function - | Ident (_,id) as r when not strict && find_hyp id ist -> + | {v=Ident id} as r when not strict && find_hyp id ist -> (DAst.make @@ GVar id), Some (make @@ CRef (r,None)) - | Ident (_,id) as r when find_var id ist -> + | {v=Ident id} as r when find_var id ist -> (DAst.make @@ GVar id), if strict then None else Some (make @@ CRef (r,None)) | r -> - let loc,_ as lqid = qualid_of_reference r in + let {loc} as lqid = qualid_of_reference r in DAst.make @@ GRef (locate_global_with_alias lqid,None), if strict then None else Some (make @@ CRef (r,None)) (* Internalize an isolated reference in position of tactic *) let intern_isolated_global_tactic_reference r = - let (loc,qid) = qualid_of_reference r in + let {loc;v=qid} = qualid_of_reference r in TacCall (Loc.tag ?loc (ArgArg (loc,Tacenv.locate_tactic qid),[])) let intern_isolated_tactic_reference strict ist r = @@ -135,12 +135,12 @@ let intern_isolated_tactic_reference strict ist r = try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist r)) with Not_found -> (* Reference not found *) - error_global_not_found (snd (qualid_of_reference r)) + error_global_not_found (qualid_of_reference r) (* Internalize an applied tactic reference *) let intern_applied_global_tactic_reference r = - let (loc,qid) = qualid_of_reference r in + let {loc;v=qid} = qualid_of_reference r in ArgArg (loc,Tacenv.locate_tactic qid) let intern_applied_tactic_reference ist r = @@ -151,7 +151,7 @@ let intern_applied_tactic_reference ist r = try intern_applied_global_tactic_reference r with Not_found -> (* Reference not found *) - error_global_not_found (snd (qualid_of_reference r)) + error_global_not_found (qualid_of_reference r) (* Intern a reference parsed in a non-tactic entry *) @@ -167,12 +167,12 @@ let intern_non_tactic_reference strict ist r = with Not_found -> (* By convention, use IntroIdentifier for unbound ident, when not in a def *) match r with - | Ident (loc,id) when not strict -> + | {loc;v=Ident id} when not strict -> let ipat = in_gen (glbwit wit_intro_pattern) (make ?loc @@ IntroNaming (IntroIdentifier id)) in TacGeneric ipat | _ -> (* Reference not found *) - error_global_not_found (snd (qualid_of_reference r)) + error_global_not_found (qualid_of_reference r) let intern_message_token ist = function | (MsgString _ | MsgInt _ as x) -> x @@ -268,7 +268,7 @@ let intern_destruction_arg ist = function | clear,ElimOnIdent {loc;v=id} -> if !strict_check then (* If in a defined tactic, no intros-until *) - let c, p = intern_constr ist (make @@ CRef (Ident (Loc.tag id), None)) in + let c, p = intern_constr ist (make @@ CRef (make @@ Ident id, None)) in match DAst.get c with | GVar id -> clear,ElimOnIdent (make ?loc:c.loc id) | _ -> clear,ElimOnConstr ((c, p), NoBindings) @@ -276,7 +276,7 @@ let intern_destruction_arg ist = function clear,ElimOnIdent (make ?loc id) let short_name = function - | AN (Ident (loc,id)) when not !strict_check -> Some (make ?loc id) + | {v=AN {loc;v=Ident id}} when not !strict_check -> Some (make ?loc id) | _ -> None let intern_evaluable_global_reference ist r = @@ -284,20 +284,20 @@ let intern_evaluable_global_reference ist r = try evaluable_of_global_reference ist.genv (locate_global_with_alias ~head:true lqid) with Not_found -> match r with - | Ident (loc,id) when not !strict_check -> EvalVarRef id - | _ -> error_global_not_found (snd lqid) + | {loc;v=Ident id} when not !strict_check -> EvalVarRef id + | _ -> error_global_not_found lqid let intern_evaluable_reference_or_by_notation ist = function - | AN r -> intern_evaluable_global_reference ist r - | ByNotation {loc;v=(ntn,sc)} -> + | {v=AN r} -> intern_evaluable_global_reference ist r + | {v=ByNotation (ntn,sc);loc} -> evaluable_of_global_reference ist.genv (Notation.interp_notation_as_global_reference ?loc (function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc) (* Globalize a reduction expression *) let intern_evaluable ist = function - | AN (Ident (loc,id)) when find_var id ist -> ArgVar (make ?loc id) - | AN (Ident (loc,id)) when not !strict_check && find_hyp id ist -> + | {loc;v=AN {v=Ident id}} when find_var id ist -> ArgVar (make ?loc id) + | {loc;v=AN {v=Ident id}} when not !strict_check && find_hyp id ist -> ArgArg (EvalVarRef id, Some (make ?loc id)) | r -> let e = intern_evaluable_reference_or_by_notation ist r in @@ -353,10 +353,9 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) = ref or a pattern seems interesting, with "head" reduction in case of an evaluable ref, and "strong" reduction in the subterm matched when a pattern *) - let loc = loc_of_smart_reference r in let r = match r with - | AN r -> r - | _ -> Qualid (loc,qualid_of_path (path_of_global (smart_global r))) in + | {v=AN r} -> r + | {loc} -> make ?loc @@ Qualid (qualid_of_path (path_of_global (smart_global r))) in let sign = { Constrintern.ltac_vars = ist.ltacvars; ltac_bound = Id.Set.empty; @@ -376,7 +375,7 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) = | Inl r -> interp_ref r | Inr { v = CAppExpl((None,r,None),[]) } -> (* We interpret similarly @ref and ref *) - interp_ref (AN r) + interp_ref (make @@ AN r) | Inr c -> Inr (snd (intern_typed_pattern ist ~as_type:false ~ltacvars:ist.ltacvars c))) @@ -385,13 +384,13 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) = let dump_glob_red_expr = function | Unfold occs -> List.iter (fun (_, r) -> try - Dumpglob.add_glob ?loc:(loc_of_or_by_notation Libnames.loc_of_reference r) + Dumpglob.add_glob ?loc:r.loc (Smartlocate.smart_global r) with e when CErrors.noncritical e -> ()) occs | Cbv grf | Lazy grf -> List.iter (fun r -> try - Dumpglob.add_glob ?loc:(loc_of_or_by_notation Libnames.loc_of_reference r) + Dumpglob.add_glob ?loc:r.loc (Smartlocate.smart_global r) with e when CErrors.noncritical e -> ()) grf.rConst | _ -> () -- cgit v1.2.3