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/funind/indfun.ml | 16 ++++++++-------- plugins/funind/indfun_common.ml | 9 ++------- plugins/funind/recdef.ml | 4 ++-- 3 files changed, 12 insertions(+), 17 deletions(-) (limited to 'plugins/funind') diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 1c27b27e2..b65d9867d 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -356,7 +356,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error (*i The next call to mk_rel_id is valid since we have just construct the graph Ensures by : do_built i*) - let f_R_mut = Ident (Loc.tag @@ mk_rel_id (List.nth names 0)) in + let f_R_mut = CAst.make @@ Ident (mk_rel_id (List.nth names 0)) in let ind_kn = fst (locate_with_msg (pr_reference f_R_mut++str ": Not an inductive type!") @@ -364,7 +364,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error f_R_mut) in let fname_kn (((fname,_),_,_,_,_),_) = - let f_ref = Ident CAst.(with_loc_val (fun ?loc n -> (loc,n)) fname) in + let f_ref = CAst.map (fun n -> Ident n) fname in locate_with_msg (pr_reference f_ref++str ": Not an inductive type!") locate_constant @@ -472,7 +472,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas let unbounded_eq = let f_app_args = CAst.make @@ Constrexpr.CAppExpl( - (None,(Ident (Loc.tag fname)),None) , + (None,CAst.make @@ Ident fname,None) , (List.map (function | {CAst.v=Anonymous} -> assert false @@ -482,7 +482,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas ) ) in - CAst.make @@ Constrexpr.CApp ((None,Constrexpr_ops.mkRefC (Qualid (Loc.tag (qualid_of_string "Logic.eq")))), + CAst.make @@ Constrexpr.CApp ((None,Constrexpr_ops.mkRefC (CAst.make @@ Qualid (qualid_of_string "Logic.eq"))), [(f_app_args,None);(body,None)]) in let eq = Constrexpr_ops.mkCProdN args unbounded_eq in @@ -539,7 +539,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas | None -> let ltof = let make_dir l = DirPath.make (List.rev_map Id.of_string l) in - Libnames.Qualid (Loc.tag @@ Libnames.qualid_of_path + CAst.make @@ Libnames.Qualid (Libnames.qualid_of_path (Libnames.make_path (make_dir ["Arith";"Wf_nat"]) (Id.of_string "ltof"))) in let fun_from_mes = @@ -724,7 +724,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof let rec add_args id new_args = CAst.map (function | CRef (r,_) as b -> begin match r with - | Libnames.Ident(loc,fname) when Id.equal fname id -> + | {CAst.v=Libnames.Ident fname} when Id.equal fname id -> CAppExpl((None,r,None),new_args) | _ -> b end @@ -744,7 +744,7 @@ let rec add_args id new_args = CAst.map (function | CAppExpl((pf,r,us),exprl) -> begin match r with - | Libnames.Ident(loc,fname) when Id.equal fname id -> + | {CAst.v=Libnames.Ident fname} when Id.equal fname id -> CAppExpl((pf,r,us),new_args@(List.map (add_args id new_args) exprl)) | _ -> CAppExpl((pf,r,us),List.map (add_args id new_args) exprl) end @@ -883,7 +883,7 @@ let make_graph (f_ref:global_reference) = | Constrexpr.CLocalAssum (nal,_,_) -> List.map (fun {CAst.loc;v=n} -> CAst.make ?loc @@ - CRef(Libnames.Ident(loc, Nameops.Name.get_id n),None)) + CRef(CAst.make ?loc @@ Libnames.Ident(Nameops.Name.get_id n),None)) nal | Constrexpr.CLocalPattern _ -> assert false ) diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index d6fd2f2a0..a0b9217c7 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -32,7 +32,7 @@ let id_of_name = function | _ -> raise Not_found let locate ref = - let (loc,qid) = qualid_of_reference ref in + let {CAst.v=qid} = qualid_of_reference ref in Nametab.locate qid let locate_ind ref = @@ -100,13 +100,8 @@ let list_union_eq eq_fun l1 l2 = let list_add_set_eq eq_fun x l = if List.exists (eq_fun x) l then l else x::l - - - let const_of_id id = - let _,princ_ref = - qualid_of_reference (Libnames.Ident (Loc.tag id)) - in + let princ_ref = qualid_of_ident id in try Constrintern.locate_reference princ_ref with Not_found -> CErrors.user_err ~hdr:"IndFun.const_of_id" diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 4cbcde8e5..fb9ae64bf 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1325,7 +1325,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp CErrors.user_err Pp.(str "\"abstract\" cannot handle existentials"); let hook _ _ = let opacity = - let na_ref = Libnames.Ident (Loc.tag na) in + let na_ref = CAst.make @@ Libnames.Ident na in let na_global = Smartlocate.global_with_alias na_ref in match na_global with ConstRef c -> is_opaque_constant c @@ -1579,7 +1579,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let hook _ _ = let term_ref = Nametab.locate (qualid_of_ident term_id) in let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in - let _ = Extraction_plugin.Table.extraction_inline true [Ident (Loc.tag term_id)] in + let _ = Extraction_plugin.Table.extraction_inline true [CAst.make @@ Ident term_id] in (* message "start second proof"; *) let stop = try com_eqn (List.length res_vars) equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type); -- cgit v1.2.3