From 9bebbb96e58b3c1b0f7f88ba2af45462eae69b0f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 10 Dec 2017 09:26:25 +0100 Subject: [ast] Improve precision of Ast location recognition in serialization. We follow the suggestions in #402 and turn uses of `Loc.located` in `vernac` into `CAst.t`. The impact should be low as this change mostly affects top-level vernaculars. With this change, we are even closer to automatically map a text document to its AST in a programmatic way. --- plugins/funind/glob_term_to_relation.ml | 18 ++++---- plugins/funind/indfun.ml | 52 +++++++++++------------ plugins/ltac/coretactics.ml4 | 2 +- plugins/ltac/extraargs.ml4 | 14 +++---- plugins/ltac/extraargs.mli | 8 ++-- plugins/ltac/extratactics.ml4 | 2 +- plugins/ltac/g_ltac.ml4 | 22 +++++----- plugins/ltac/g_tactic.ml4 | 61 ++++++++++++++++----------- plugins/ltac/pltac.mli | 7 ++-- plugins/ltac/pptactic.ml | 28 ++++++------- plugins/ltac/rewrite.ml | 4 +- plugins/ltac/tacentries.ml | 6 +-- plugins/ltac/tacexpr.mli | 16 ++++---- plugins/ltac/tacintern.ml | 44 ++++++++++---------- plugins/ltac/tacintern.mli | 2 +- plugins/ltac/tacinterp.ml | 73 +++++++++++++++++---------------- plugins/ltac/tacinterp.mli | 6 +-- plugins/ltac/tactic_debug.mli | 2 +- plugins/ltac/tactic_matching.ml | 4 +- plugins/ltac/tauto.ml | 6 +-- plugins/quote/g_quote.ml4 | 2 +- plugins/setoid_ring/newring.ml | 6 +-- plugins/ssr/ssrcommon.ml | 8 ++-- plugins/ssr/ssrparser.ml4 | 60 ++++++++++++++------------- plugins/ssr/ssrvernac.ml4 | 24 ++++++----- plugins/ssrmatching/ssrmatching.ml4 | 4 +- 26 files changed, 250 insertions(+), 231 deletions(-) (limited to 'plugins') diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 693ab464d..22881c32c 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1295,7 +1295,7 @@ let rec rebuild_return_type rt = CAst.make ?loc @@ Constrexpr.CProdN(n,rebuild_return_type t') | Constrexpr.CLetIn(na,v,t,t') -> CAst.make ?loc @@ Constrexpr.CLetIn(na,v,t,rebuild_return_type t') - | _ -> CAst.make ?loc @@ Constrexpr.CProdN([Constrexpr.CLocalAssum ([Loc.tag Anonymous], + | _ -> CAst.make ?loc @@ Constrexpr.CProdN([Constrexpr.CLocalAssum ([CAst.make Anonymous], Constrexpr.Default Decl_kinds.Explicit, rt)], CAst.make @@ Constrexpr.CSort(GType [])) @@ -1351,12 +1351,12 @@ let do_build_inductive (fun (n,t,typ) acc -> match typ with | Some typ -> - CAst.make @@ Constrexpr.CLetIn((Loc.tag n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t, + CAst.make @@ Constrexpr.CLetIn((CAst.make n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t, Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ), acc) | None -> CAst.make @@ Constrexpr.CProdN - ([Constrexpr.CLocalAssum([(Loc.tag n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t)], + ([Constrexpr.CLocalAssum([CAst.make n],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t)], acc ) ) @@ -1418,12 +1418,12 @@ let do_build_inductive (fun (n,t,typ) acc -> match typ with | Some typ -> - CAst.make @@ Constrexpr.CLetIn((Loc.tag n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t, + CAst.make @@ Constrexpr.CLetIn((CAst.make n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t, Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ), acc) | None -> CAst.make @@ Constrexpr.CProdN - ([Constrexpr.CLocalAssum([(Loc.tag n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t)], + ([Constrexpr.CLocalAssum([CAst.make n],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t)], acc ) ) @@ -1450,18 +1450,18 @@ let do_build_inductive (fun (n,t,typ) -> match typ with | Some typ -> - Constrexpr.CLocalDef((Loc.tag n), Constrextern.extern_glob_constr Id.Set.empty t, + Constrexpr.CLocalDef((CAst.make n), Constrextern.extern_glob_constr Id.Set.empty t, Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ)) | None -> Constrexpr.CLocalAssum - ([(Loc.tag n)], Constrexpr_ops.default_binder_kind, Constrextern.extern_glob_constr Id.Set.empty t) + ([(CAst.make n)], Constrexpr_ops.default_binder_kind, Constrextern.extern_glob_constr Id.Set.empty t) ) rels_params in let ext_rels_constructors = Array.map (List.map (fun (id,t) -> - false,((Loc.tag id), + false,((CAst.make id), with_full_print (Constrextern.extern_glob_type Id.Set.empty) ((* zeta_normalize *) (alpha_rt rel_params_ids t)) ) @@ -1469,7 +1469,7 @@ let do_build_inductive (rel_constructors) in let rel_ind i ext_rel_constructors = - (((Loc.tag @@ relnames.(i)), None), + (((CAst.make @@ relnames.(i)), None), rel_params, Some rel_arities.(i), ext_rel_constructors),[] diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 96e4a94d3..e19fc9b62 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -155,7 +155,7 @@ let build_newrecursive let sigma = Evd.from_env env0 in let (rec_sign,rec_impls) = List.fold_left - (fun (env,impls) (((_,recname),_),bl,arityc,_) -> + (fun (env,impls) (({CAst.v=recname},_),bl,arityc,_) -> let arityc = Constrexpr_ops.mkCProdN bl arityc in let arity,ctx = Constrintern.interp_type env0 sigma arityc in let evd = Evd.from_env env0 in @@ -344,7 +344,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error is_general do_built (fix_rec_l:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) recdefs interactive_proof (continue_proof : int -> Names.Constant.t array -> EConstr.constr array -> int -> Tacmach.tactic) : unit = - let names = List.map (function (((_, name),_),_,_,_,_),_ -> name) fix_rec_l in + let names = List.map (function (({CAst.v=name},_),_,_,_,_),_ -> name) fix_rec_l in let fun_bodies = List.map2 prepare_body fix_rec_l recdefs in let funs_args = List.map fst fun_bodies in let funs_types = List.map (function ((_,_,_,types,_),_) -> types) fix_rec_l in @@ -365,7 +365,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error f_R_mut) in let fname_kn (((fname,_),_,_,_,_),_) = - let f_ref = Ident fname in + let f_ref = Ident CAst.(with_loc_val (fun ?loc n -> (loc,n)) fname) in locate_with_msg (pr_reference f_ref++str ": Not an inductive type!") locate_constant @@ -404,7 +404,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = match fixpoint_exprl with - | [(((_,fname),pl),_,bl,ret_type,body),_] when not is_rec -> + | [(({CAst.v=fname},pl),_,bl,ret_type,body),_] when not is_rec -> let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in ComDefinition.do_definition ~program_mode:false @@ -413,7 +413,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp bl None body (Some ret_type) (Lemmas.mk_hook (fun _ _ -> ())); let evd,rev_pconstants = List.fold_left - (fun (evd,l) ((((_,fname),_),_,_,_,_),_) -> + (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) -> let evd,c = Evd.fresh_global (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in @@ -430,7 +430,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp ComFixpoint.do_fixpoint Global (Flags.is_universe_polymorphism ()) fixpoint_exprl; let evd,rev_pconstants = List.fold_left - (fun (evd,l) ((((_,fname),_),_,_,_,_),_) -> + (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) -> let evd,c = Evd.fresh_global (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in @@ -460,7 +460,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas let rec_arg_num = let names = List.map - snd + CAst.(with_val (fun x -> x)) (Constrexpr_ops.names_of_local_assums args) in match wf_arg with @@ -476,8 +476,8 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas (None,(Ident (Loc.tag fname)),None) , (List.map (function - | _,Anonymous -> assert false - | _,Name e -> (Constrexpr_ops.mkIdentC e) + | {CAst.v=Anonymous} -> assert false + | {CAst.v=Name e} -> (Constrexpr_ops.mkIdentC e) ) (Constrexpr_ops.names_of_local_assums args) ) @@ -515,7 +515,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas | None -> begin match args with - | [Constrexpr.CLocalAssum ([(_,Name x)],k,t)] -> t,x + | [Constrexpr.CLocalAssum ([{CAst.v=Name x}],k,t)] -> t,x | _ -> error "Recursive argument must be specified" end | Some wf_args -> @@ -525,7 +525,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas (function | Constrexpr.CLocalAssum(l,k,t) -> List.exists - (function (_,Name id) -> Id.equal id wf_args | _ -> false) + (function {CAst.v=Name id} -> Id.equal id wf_args | _ -> false) l | _ -> false ) @@ -546,7 +546,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas let fun_from_mes = let applied_mes = Constrexpr_ops.mkAppC(wf_mes_expr,[Constrexpr_ops.mkIdentC wf_arg]) in - Constrexpr_ops.mkLambdaC ([(Loc.tag @@ Name wf_arg)],Constrexpr_ops.default_binder_kind,wf_arg_type,applied_mes) + Constrexpr_ops.mkLambdaC ([CAst.make @@ Name wf_arg],Constrexpr_ops.default_binder_kind,wf_arg_type,applied_mes) in let wf_rel_from_mes = Constrexpr_ops.mkAppC(Constrexpr_ops.mkRefC ltof,[wf_arg_type;fun_from_mes]) @@ -557,7 +557,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas let a = Names.Id.of_string "___a" in let b = Names.Id.of_string "___b" in Constrexpr_ops.mkLambdaC( - [Loc.tag @@ Name a;Loc.tag @@ Name b], + [CAst.make @@ Name a; CAst.make @@ Name b], Constrexpr.Default Explicit, wf_arg_type, Constrexpr_ops.mkAppC(wf_rel_expr, @@ -592,7 +592,7 @@ and rebuild_nal aux bk bl' nal typ = | _,{ CAst.v = CProdN([],typ) } -> rebuild_nal aux bk bl' nal typ | [], _ -> rebuild_bl aux bl' typ | na::nal,{ CAst.v = CProdN(CLocalAssum(na'::nal',bk',nal't)::rest,typ') } -> - if Name.equal (snd na) (snd na') || Name.is_anonymous (snd na') + if Name.equal (na.CAst.v) (na'.CAst.v) || Name.is_anonymous (na'.CAst.v) then let assum = CLocalAssum([na],bk,nal't) in let new_rest = if nal' = [] then rest else (CLocalAssum(nal',bk',nal't)::rest) in @@ -638,7 +638,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof let _is_struct = match fixpoint_exprl with | [((_,(wf_x,Constrexpr.CWfRec wf_rel),_,_,_),_) as fixpoint_expr] -> - let (((((_,name),pl),_,args,types,body)),_) as fixpoint_expr = + let (((({CAst.v=name},pl),_,args,types,body)),_) as fixpoint_expr = match recompute_binder_list [fixpoint_expr] with | [e] -> e | _ -> assert false @@ -659,10 +659,10 @@ let do_generate_principle pconstants on_error register_built interactive_proof true in if register_built - then register_wf name rec_impls wf_rel (map_option snd wf_x) using_lemmas args types body pre_hook; + then register_wf name rec_impls wf_rel (map_option (fun x -> x.CAst.v) wf_x) using_lemmas args types body pre_hook; false |[((_,(wf_x,Constrexpr.CMeasureRec(wf_mes,wf_rel_opt)),_,_,_),_) as fixpoint_expr] -> - let (((((_,name),_),_,args,types,body)),_) as fixpoint_expr = + let (((({CAst.v=name},_),_,args,types,body)),_) as fixpoint_expr = match recompute_binder_list [fixpoint_expr] with | [e] -> e | _ -> assert false @@ -683,7 +683,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof true in if register_built - then register_mes name rec_impls wf_mes wf_rel_opt (map_option snd wf_x) using_lemmas args types body pre_hook; + then register_mes name rec_impls wf_mes wf_rel_opt (map_option (fun x -> x.CAst.v) wf_x) using_lemmas args types body pre_hook; true | _ -> List.iter (function ((_na,(_,ord),_args,_body,_type),_not) -> @@ -696,7 +696,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof fixpoint_exprl; let fixpoint_exprl = recompute_binder_list fixpoint_exprl in let fix_names = - List.map (function ((((_,name),_),_,_,_,_),_) -> name) fixpoint_exprl + List.map (function ((({CAst.v=name},_),_,_,_,_),_) -> name) fixpoint_exprl in (* ok all the expressions are structural *) let recdefs,rec_impls = build_newrecursive fixpoint_exprl in @@ -757,7 +757,7 @@ let rec add_args id new_args = CAst.map (function List.map (fun (b,na,b_option) -> add_args id new_args b, na, b_option) cel, - List.map (fun (loc,(cpl,e)) -> Loc.tag ?loc @@ (cpl,add_args id new_args e)) cal + List.map CAst.(map (fun (cpl,e) -> (cpl,add_args id new_args e))) cal ) | CLetTuple(nal,(na,b_option),b1,b2) -> CLetTuple(nal,(na,Option.map (add_args id new_args) b_option), @@ -875,7 +875,7 @@ let make_graph (f_ref:global_reference) = let l = List.map (fun (id,(n,recexp),bl,t,b) -> - let loc, rec_id = Option.get n in + let { CAst.loc; v=rec_id } = Option.get n in let new_args = List.flatten (List.map @@ -883,7 +883,7 @@ let make_graph (f_ref:global_reference) = | Constrexpr.CLocalDef (na,_,_)-> [] | Constrexpr.CLocalAssum (nal,_,_) -> List.map - (fun (loc,n) -> CAst.make ?loc @@ + (fun {CAst.loc;v=n} -> CAst.make ?loc @@ CRef(Libnames.Ident(loc, Nameops.Name.get_id n),None)) nal | Constrexpr.CLocalPattern _ -> assert false @@ -891,21 +891,21 @@ let make_graph (f_ref:global_reference) = nal_tas ) in - let b' = add_args (snd id) new_args b in - ((((id,None), ( Some (Loc.tag rec_id),CStructRec),nal_tas@bl,t,Some b'),[]):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list)) + let b' = add_args id.CAst.v new_args b in + ((((id,None), ( Some CAst.(make rec_id),CStructRec),nal_tas@bl,t,Some b'),[]):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list)) ) fixexprl in l | _ -> let id = Label.to_id (Constant.label c) in - [(((Loc.tag id),None),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]] + [((CAst.make id,None),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]] in let mp,dp,_ = Constant.repr3 c in do_generate_principle [c,Univ.Instance.empty] error_error false false expr_list; (* We register the infos *) List.iter - (fun ((((_,id),_),_,_,_,_),_) -> add_Function false (Constant.make3 mp dp (Label.of_id id))) + (fun ((({CAst.v=id},_),_,_,_,_),_) -> add_Function false (Constant.make3 mp dp (Label.of_id id))) expr_list) let do_generate_principle = do_generate_principle [] warning_error true diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4 index 7d2c4d082..794a28dd4 100644 --- a/plugins/ltac/coretactics.ml4 +++ b/plugins/ltac/coretactics.ml4 @@ -346,7 +346,7 @@ let () = register_list_tactical "solve" Tacticals.New.tclSOLVE let initial_tacticals () = let idn n = Id.of_string (Printf.sprintf "_%i" n) in - let varn n = Reference (ArgVar (None, idn n)) in + let varn n = Reference (ArgVar (CAst.make (idn n))) in let iter (s, t) = Tacenv.register_ltac false false (Id.of_string s) t in List.iter iter [ "first", TacFun ([Name (idn 0)], TacML (None, (initial_entry "first", [varn 0]))); diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4 index 4c6d3c2d3..2eb1ef315 100644 --- a/plugins/ltac/extraargs.ml4 +++ b/plugins/ltac/extraargs.ml4 @@ -81,7 +81,7 @@ let pr_int_list_full _prc _prlc _prt l = pr_int_list l let pr_occurrences _prc _prlc _prt l = match l with | ArgArg x -> pr_int_list x - | ArgVar (loc, id) -> Id.print id + | ArgVar { CAst.loc = loc; v=id } -> Id.print id let occurrences_of = function | [] -> NoOccurrences @@ -102,7 +102,7 @@ let int_list_of_VList v = match Value.to_list v with let interp_occs ist gl l = match l with | ArgArg x -> x - | ArgVar (_,id as locid) -> + | ArgVar ({ CAst.v = id } as locid) -> (try int_list_of_VList (Id.Map.find id ist.lfun) with Not_found | CannotCoerceTo _ -> [interp_int ist locid]) let interp_occs ist gl l = @@ -188,7 +188,7 @@ END type 'id gen_place= ('id * hyp_location_flag,unit) location -type loc_place = Id.t Loc.located gen_place +type loc_place = lident gen_place type place = Id.t gen_place let pr_gen_place pr_id = function @@ -199,7 +199,7 @@ let pr_gen_place pr_id = function | HypLocation (id,InHypValueOnly) -> str "in (Value of " ++ pr_id id ++ str ")" -let pr_loc_place _ _ _ = pr_gen_place (fun (_,id) -> Id.print id) +let pr_loc_place _ _ _ = pr_gen_place (fun { CAst.v = id } -> Id.print id) let pr_place _ _ _ = pr_gen_place Id.print let pr_hloc = pr_loc_place () () () @@ -228,11 +228,11 @@ ARGUMENT EXTEND hloc | [ "in" "|-" "*" ] -> [ ConclLocation () ] | [ "in" ident(id) ] -> - [ HypLocation ((Loc.tag id),InHyp) ] + [ HypLocation ((CAst.make id),InHyp) ] | [ "in" "(" "Type" "of" ident(id) ")" ] -> - [ HypLocation ((Loc.tag id),InHypTypeOnly) ] + [ HypLocation ((CAst.make id),InHypTypeOnly) ] | [ "in" "(" "Value" "of" ident(id) ")" ] -> - [ HypLocation ((Loc.tag id),InHypValueOnly) ] + [ HypLocation ((CAst.make id),InHypValueOnly) ] END diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli index 00668ddc7..000c3d2fb 100644 --- a/plugins/ltac/extraargs.mli +++ b/plugins/ltac/extraargs.mli @@ -50,7 +50,7 @@ val lglob : constr_expr Pcoq.Gram.entry type 'id gen_place= ('id * Locus.hyp_location_flag,unit) location -type loc_place = Id.t Loc.located gen_place +type loc_place = lident gen_place type place = Id.t gen_place val wit_hloc : (loc_place, loc_place, place) Genarg.genarg_type @@ -77,6 +77,6 @@ val retroknowledge_field : Retroknowledge.field Pcoq.Gram.entry val wit_retroknowledge_field : (Retroknowledge.field, unit, unit) Genarg.genarg_type val wit_in_clause : - (Id.t Loc.located Locus.clause_expr, - Id.t Loc.located Locus.clause_expr, - Id.t Locus.clause_expr) Genarg.genarg_type + (lident Locus.clause_expr, + lident Locus.clause_expr, + Id.t Locus.clause_expr) Genarg.genarg_type diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index 286f9d95d..10be8a842 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -71,7 +71,7 @@ END let induction_arg_of_quantified_hyp = function | AnonHyp n -> None,ElimOnAnonHyp n - | NamedHyp id -> None,ElimOnIdent (Loc.tag id) + | NamedHyp id -> None,ElimOnIdent (CAst.make id) (* Versions *_main must come first!! so that "1" is interpreted as a ElimOnAnonHyp and not as a "constr", and "id" is interpreted as a diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index 9ef819569..85c9fc5fd 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -37,10 +37,10 @@ let genarg_of_uconstr c = in_gen (rawwit Stdarg.wit_uconstr) c let in_tac tac = in_gen (rawwit Tacarg.wit_ltac) tac let reference_to_id = function - | Libnames.Ident (loc, id) -> (loc, id) + | Libnames.Ident (loc, id) -> CAst.make ?loc id | Libnames.Qualid (loc,_) -> - CErrors.user_err ?loc - (str "This expression should be a simple identifier.") + CErrors.user_err ?loc + (str "This expression should be a simple identifier.") let tactic_mode = Gram.entry_create "vernac:tactic_command" @@ -196,7 +196,7 @@ GEXTEND Gram verbose most of the time. *) fresh_id: [ [ s = STRING -> ArgArg s (*| id = ident -> ArgVar (!@loc,id)*) - | qid = qualid -> let (_pth,id) = Libnames.repr_qualid (snd qid) in ArgVar (Loc.tag ~loc:!@loc id) ] ] + | qid = qualid -> let (_pth,id) = Libnames.repr_qualid (snd qid) in ArgVar (CAst.make ~loc:!@loc id) ] ] ; constr_eval: [ [ IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr -> @@ -225,12 +225,12 @@ GEXTEND Gram | l = ident -> Name.Name l ] ] ; let_clause: - [ [ (l,id) = identref; ":="; te = tactic_expr -> - ((l,Name id), arg_of_expr te) - | na = ["_" -> (Some !@loc,Anonymous)]; ":="; te = tactic_expr -> + [ [ idr = identref; ":="; te = tactic_expr -> + (CAst.map (fun id -> Name id) idr, arg_of_expr te) + | na = ["_" -> CAst.make ~loc:!@loc Anonymous]; ":="; te = tactic_expr -> (na, arg_of_expr te) - | (l,id) = identref; args = LIST1 input_fun; ":="; te = tactic_expr -> - ((l,Name id), arg_of_expr (TacFun(args,te))) ] ] + | idr = identref; args = LIST1 input_fun; ":="; te = tactic_expr -> + (CAst.map (fun id -> Name id) idr, arg_of_expr (TacFun(args,te))) ] ] ; match_pattern: [ [ IDENT "context"; oid = OPT Constr.ident; @@ -483,7 +483,7 @@ let pr_ltac_ref = Libnames.pr_reference let pr_tacdef_body tacdef_body = let id, redef, body = match tacdef_body with - | TacticDefinition ((_,id), body) -> Id.print id, false, body + | TacticDefinition ({CAst.v=id}, body) -> Id.print id, false, body | TacticRedefinition (id, body) -> pr_ltac_ref id, true, body in let idl, body = @@ -504,7 +504,7 @@ END VERNAC COMMAND FUNCTIONAL EXTEND VernacDeclareTacticDefinition | [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => [ VtSideff (List.map (function - | TacticDefinition ((_,r),_) -> r + | TacticDefinition ({CAst.v=r},_) -> r | TacticRedefinition (Ident (_,r),_) -> r | TacticRedefinition (Qualid (_,q),_) -> snd(repr_qualid q)) l), VtLater ] -> [ fun ~atts ~st -> let open Vernacinterp in diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4 index e68140828..338d61e6f 100644 --- a/plugins/ltac/g_tactic.ml4 +++ b/plugins/ltac/g_tactic.ml4 @@ -115,16 +115,16 @@ let mk_fix_tac (loc,id,bl,ann,ty) = match bl,ann with [([_],_,_)], None -> 1 | _, Some x -> - let ids = List.map snd (List.flatten (List.map (fun (nal,_,_) -> nal) bl)) in - (try List.index Names.Name.equal (snd x) ids + let ids = List.map (fun x -> x.CAst.v) (List.flatten (List.map (fun (nal,_,_) -> nal) bl)) in + (try List.index Names.Name.equal x.CAst.v ids with Not_found -> user_err Pp.(str "No such fix variable.")) | _ -> user_err Pp.(str "Cannot guess decreasing argument of fix.") in let bl = List.map (fun (nal,bk,t) -> CLocalAssum (nal,bk,t)) bl in (id,n, CAst.make ~loc @@ CProdN(bl,ty)) let mk_cofix_tac (loc,id,bl,ann,ty) = - let _ = Option.map (fun (aloc,_) -> - user_err ~loc:aloc + let _ = Option.map (fun { CAst.loc = aloc } -> + user_err ?loc:aloc ~hdr:"Constr:mk_cofix_tac" (Pp.str"Annotation forbidden in cofix expression.")) ann in let bl = List.map (fun (nal,bk,t) -> CLocalAssum (nal,bk,t)) bl in @@ -134,7 +134,7 @@ let mk_cofix_tac (loc,id,bl,ann,ty) = let destruction_arg_of_constr (c,lbind as clbind) = match lbind with | NoBindings -> begin - try ElimOnIdent (Constrexpr_ops.constr_loc c,snd(Constrexpr_ops.coerce_to_id c)) + try ElimOnIdent (CAst.make ?loc:(Constrexpr_ops.constr_loc c) (Constrexpr_ops.coerce_to_id c).CAst.v) with e when CErrors.noncritical e -> ElimOnConstr clbind end | _ -> ElimOnConstr clbind @@ -152,6 +152,7 @@ let mkTacCase with_evar = function (* Reinterpret ident as notations for variables in the context *) (* because we don't know if they are quantified or not *) | [(clear,ElimOnIdent id),(None,None),None],None -> + let id = CAst.(id.loc, id.v) in TacCase (with_evar,(clear,(CAst.make @@ CRef (Ident id,None),NoBindings))) | ic -> if List.exists (function ((_, ElimOnAnonHyp _),_,_) -> true | _ -> false) (fst ic) @@ -161,7 +162,7 @@ let mkTacCase with_evar = function let rec mkCLambdaN_simple_loc ?loc bll c = match bll with - | ((loc1,_)::_ as idl,bk,t) :: bll -> + | ({CAst.loc = loc1}::_ as idl,bk,t) :: bll -> CAst.make ?loc @@ CLambdaN ([CLocalAssum (idl,bk,t)],mkCLambdaN_simple_loc ?loc:(Loc.merge_opt loc1 loc) bll c) | ([],_,_) :: bll -> mkCLambdaN_simple_loc ?loc bll c | [] -> c @@ -169,7 +170,7 @@ let rec mkCLambdaN_simple_loc ?loc bll c = let mkCLambdaN_simple bl c = match bl with | [] -> c | h :: _ -> - let loc = Loc.merge_opt (fst (List.hd (pi1 h))) (Constrexpr_ops.constr_loc c) in + let loc = Loc.merge_opt (List.hd (pi1 h)).CAst.loc (Constrexpr_ops.constr_loc c) in mkCLambdaN_simple_loc ?loc bl c let loc_of_ne_list l = Loc.merge_opt (fst (List.hd l)) (fst (List.last l)) @@ -381,15 +382,20 @@ GEXTEND Gram ; hypident: [ [ id = id_or_meta -> - id,InHyp + let id : Misctypes.lident = id in + id,InHyp | "("; IDENT "type"; IDENT "of"; id = id_or_meta; ")" -> - id,InHypTypeOnly + let id : Misctypes.lident = id in + id,InHypTypeOnly | "("; IDENT "value"; IDENT "of"; id = id_or_meta; ")" -> - id,InHypValueOnly + let id : Misctypes.lident = id in + id,InHypValueOnly ] ] ; hypident_occ: - [ [ (id,l)=hypident; occs=occs -> ((occs,id),l) ] ] + [ [ (id,l)=hypident; occs=occs -> + let id : Misctypes.lident = id in + ((occs,id),l) ] ] ; in_clause: [ [ "*"; occs=occs -> @@ -433,7 +439,8 @@ GEXTEND Gram | -> true ]] ; simple_binder: - [ [ na=name -> ([na],Default Explicit, CAst.make ~loc:!@loc @@ CHole (Some (Evar_kinds.BinderType (snd na)), IntroAnonymous, None)) + [ [ na=name -> ([na],Default Explicit, CAst.make ~loc:!@loc @@ + CHole (Some (Evar_kinds.BinderType na.CAst.v), IntroAnonymous, None)) | "("; nal=LIST1 name; ":"; c=lconstr; ")" -> (nal,Default Explicit,c) ] ] ; @@ -565,28 +572,34 @@ GEXTEND Gram TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (true,na,c,p,false,e)) (* Alternative syntax for "pose proof c as id" *) - | IDENT "assert"; test_lpar_id_coloneq; "("; (loc,id) = identref; ":="; + | IDENT "assert"; test_lpar_id_coloneq; "("; lid = identref; ":="; c = lconstr; ")" -> - TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,true,None,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c)) - | IDENT "eassert"; test_lpar_id_coloneq; "("; (loc,id) = identref; ":="; + let { CAst.loc = loc; v = id } = lid in + TacAtom (Loc.tag ?loc @@ TacAssert (false,true,None,Some (Loc.tag ?loc @@ IntroNaming (IntroIdentifier id)),c)) + | IDENT "eassert"; test_lpar_id_coloneq; "("; lid = identref; ":="; c = lconstr; ")" -> - TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,true,None,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c)) + let { CAst.loc = loc; v = id } = lid in + TacAtom (Loc.tag ?loc @@ TacAssert (true,true,None,Some (Loc.tag ?loc @@ IntroNaming (IntroIdentifier id)),c)) (* Alternative syntax for "assert c as id by tac" *) - | IDENT "assert"; test_lpar_id_colon; "("; (loc,id) = identref; ":"; + | IDENT "assert"; test_lpar_id_colon; "("; lid = identref; ":"; c = lconstr; ")"; tac=by_tactic -> - TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,true,Some tac,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c)) - | IDENT "eassert"; test_lpar_id_colon; "("; (loc,id) = identref; ":"; + let { CAst.loc = loc; v = id } = lid in + TacAtom (Loc.tag ?loc @@ TacAssert (false,true,Some tac,Some (Loc.tag ?loc @@ IntroNaming (IntroIdentifier id)),c)) + | IDENT "eassert"; test_lpar_id_colon; "("; lid = identref; ":"; c = lconstr; ")"; tac=by_tactic -> - TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,true,Some tac,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c)) + let { CAst.loc = loc; v = id } = lid in + TacAtom (Loc.tag ?loc @@ TacAssert (true,true,Some tac,Some (Loc.tag ?loc @@ IntroNaming (IntroIdentifier id)),c)) (* Alternative syntax for "enough c as id by tac" *) - | IDENT "enough"; test_lpar_id_colon; "("; (loc,id) = identref; ":"; + | IDENT "enough"; test_lpar_id_colon; "("; lid = identref; ":"; c = lconstr; ")"; tac=by_tactic -> - TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,false,Some tac,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c)) - | IDENT "eenough"; test_lpar_id_colon; "("; (loc,id) = identref; ":"; + let { CAst.loc = loc; v = id } = lid in + TacAtom (Loc.tag ?loc @@ TacAssert (false,false,Some tac,Some (Loc.tag ?loc @@ IntroNaming (IntroIdentifier id)),c)) + | IDENT "eenough"; test_lpar_id_colon; "("; lid = identref; ":"; c = lconstr; ")"; tac=by_tactic -> - TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,false,Some tac,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c)) + let { CAst.loc = loc; v = id } = lid in + TacAtom (Loc.tag ?loc @@ TacAssert (true,false,Some tac,Some (Loc.tag ?loc @@ IntroNaming (IntroIdentifier id)),c)) | IDENT "assert"; c = constr; ipat = as_ipat; tac = by_tactic -> TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,true,Some tac,ipat,c)) diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli index 048dcc8e9..ecb0b5796 100644 --- a/plugins/ltac/pltac.mli +++ b/plugins/ltac/pltac.mli @@ -9,7 +9,6 @@ (** Ltac parsing entries *) open Loc -open Names open Pcoq open Libnames open Constrexpr @@ -20,7 +19,7 @@ open Misctypes val open_constr : constr_expr Gram.entry val constr_with_bindings : constr_expr with_bindings Gram.entry val bindings : constr_expr bindings Gram.entry -val hypident : (Id.t located * Locus.hyp_location_flag) Gram.entry +val hypident : (lident * Locus.hyp_location_flag) Gram.entry val constr_may_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry val constr_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry val uconstr : constr_expr Gram.entry @@ -29,8 +28,8 @@ val destruction_arg : constr_expr with_bindings destruction_arg Gram.entry val int_or_var : int or_var Gram.entry val simple_tactic : raw_tactic_expr Gram.entry val simple_intropattern : constr_expr intro_pattern_expr located Gram.entry -val in_clause : Names.Id.t Loc.located Locus.clause_expr Gram.entry -val clause_dft_concl : Names.Id.t Loc.located Locus.clause_expr Gram.entry +val in_clause : lident Locus.clause_expr Gram.entry +val clause_dft_concl : lident Locus.clause_expr Gram.entry val tactic_arg : raw_tactic_arg Gram.entry val tactic_expr : raw_tactic_expr Gram.entry val binder_tactic : raw_tactic_expr Gram.entry diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 4f430b79e..3bc9f2aa0 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -161,7 +161,7 @@ let string_of_genarg_arg (ArgumentType arg) = (keyword "eval" ++ brk (1,1) ++ pr_red_expr (prc,prlc,pr2,pr3) r ++ spc () ++ keyword "in" ++ spc() ++ prc c) - | ConstrContext ((_,id),c) -> + | ConstrContext ({CAst.v=id},c) -> hov 0 (keyword "context" ++ spc () ++ pr_id id ++ spc () ++ str "[ " ++ prlc c ++ str " ]") @@ -364,7 +364,7 @@ let string_of_genarg_arg (ArgumentType arg) = let pr_ltac_or_var pr = function | ArgArg x -> pr x - | ArgVar (loc,id) -> pr_with_comments ?loc (pr_id id) + | ArgVar {CAst.loc;v=id} -> pr_with_comments ?loc (pr_id id) let pr_ltac_constant kn = if !Flags.in_debugger then KerName.print kn @@ -404,7 +404,7 @@ let string_of_genarg_arg (ArgumentType arg) = let pr_as_name = function | Anonymous -> mt () - | Name id -> spc () ++ keyword "as" ++ spc () ++ pr_lident (Loc.tag id) + | Name id -> spc () ++ keyword "as" ++ spc () ++ pr_lident (CAst.make id) let pr_pose_as_style prc na c = spc() ++ prc c ++ pr_as_name na @@ -496,12 +496,12 @@ let string_of_genarg_arg (ArgumentType arg) = let pr_core_destruction_arg prc prlc = function | ElimOnConstr c -> pr_with_bindings prc prlc c - | ElimOnIdent (loc,id) -> pr_with_comments ?loc (pr_id id) + | ElimOnIdent {CAst.loc;v=id} -> pr_with_comments ?loc (pr_id id) | ElimOnAnonHyp n -> int n let pr_destruction_arg prc prlc (clear_flag,h) = pr_clear_flag clear_flag (pr_core_destruction_arg prc prlc) h - + let pr_inversion_kind = function | SimpleInversion -> primitive "simple inversion" | FullInversion -> primitive "inversion" @@ -684,7 +684,7 @@ let pr_goal_selector ~toplevel s = (* match t with | CHole _ -> spc() ++ prlist_with_sep spc (pr_lname) nal | _ ->*) - let s = prlist_with_sep spc pr_lname nal ++ str ":" ++ pr.pr_lconstr t in + let s = prlist_with_sep spc Ppconstr.pr_lname nal ++ str ":" ++ pr.pr_lconstr t in spc() ++ hov 1 (str"(" ++ s ++ str")") in let pr_fix_tac (id,n,c) = @@ -692,10 +692,10 @@ let pr_goal_selector ~toplevel s = (nal,ty)::bll -> if n <= List.length nal then match List.chop (n-1) nal with - _, (_,Name id) :: _ -> id, (nal,ty)::bll - | bef, (loc,Anonymous) :: aft -> + _, {CAst.v=Name id} :: _ -> id, (nal,ty)::bll + | bef, {CAst.loc;v=Anonymous} :: aft -> let id = next_ident_away (Id.of_string"y") avoid in - id, ((bef@(loc,Name id)::aft, ty)::bll) + id, ((bef@(CAst.make ?loc @@ Name id)::aft, ty)::bll) | _ -> assert false else let (id,bll') = set_nth_name avoid (n-List.length nal) bll in @@ -705,7 +705,7 @@ let pr_goal_selector ~toplevel s = let names = List.fold_left (fun ln (nal,_) -> List.fold_left - (fun ln na -> match na with (_,Name id) -> Id.Set.add id ln | _ -> ln) + (fun ln na -> match na with { CAst.v=Name id } -> Id.Set.add id ln | _ -> ln) ln nal) Id.Set.empty bll in let idarg,bll = set_nth_name names n bll in @@ -1087,7 +1087,7 @@ let pr_goal_selector ~toplevel s = if Int.equal n 0 then (List.rev acc, (ty,None)) else match DAst.get ty with Glob_term.GProd(na,Explicit,a,b) -> - strip_ty (([Loc.tag na],(a,None))::acc) (n-1) b + strip_ty (([CAst.make na],(a,None))::acc) (n-1) b | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in strip_ty [] n ty @@ -1158,7 +1158,7 @@ let pr_goal_selector ~toplevel s = if n=0 then (List.rev acc, EConstr.of_constr ty) else match Constr.kind ty with | Constr.Prod(na,a,b) -> - strip_ty (([Loc.tag na],EConstr.of_constr a)::acc) (n-1) b + strip_ty (([CAst.make na],EConstr.of_constr a)::acc) (n-1) b | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in strip_ty [] n ty @@ -1318,7 +1318,7 @@ let () = register_basic_print0 wit_ref pr_reference (pr_or_var (pr_located pr_global)) pr_global; register_basic_print0 wit_ident pr_id pr_id pr_id; - register_basic_print0 wit_var (pr_located pr_id) (pr_located pr_id) pr_id; + register_basic_print0 wit_var pr_lident pr_lident pr_id; register_print0 wit_intro_pattern (lift (Miscprint.pr_intro_pattern pr_constr_expr)) @@ -1328,7 +1328,7 @@ let () = wit_clause_dft_concl (lift (pr_clauses (Some true) pr_lident)) (lift (pr_clauses (Some true) pr_lident)) - (fun c -> Genprint.TopPrinterBasic (fun () -> pr_clauses (Some true) (fun id -> pr_lident (Loc.tag id)) c)) + (fun c -> Genprint.TopPrinterBasic (fun () -> pr_clauses (Some true) (fun id -> pr_lident (CAst.make id)) c)) ; Genprint.register_print0 wit_constr diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index acd7a30c4..e73a18b79 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1773,7 +1773,7 @@ let rec strategy_of_ast = function let mkappc s l = CAst.make @@ CAppExpl ((None,(Libnames.Ident (Loc.tag @@ Id.of_string s)),None),l) let declare_an_instance n s args = - (((Loc.tag @@ Name n),None), Explicit, + (((CAst.make @@ Name n),None), Explicit, CAst.make @@ CAppExpl ((None, Qualid (Loc.tag @@ qualid_of_string s),None), args)) @@ -2006,7 +2006,7 @@ let add_morphism glob binders m s n = let poly = Flags.is_universe_polymorphism () in let instance_id = add_suffix n "_Proper" in let instance = - (((Loc.tag @@ Name instance_id),None), Explicit, + (((CAst.make @@ Name instance_id),None), Explicit, CAst.make @@ CAppExpl ( (None, Qualid (Loc.tag @@ Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper"),None), [cHole; s; m])) diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 8112cc400..4313456a4 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -374,7 +374,7 @@ let add_ml_tactic_notation name ~level prods = in let ids = List.map_filter get_id prods in let entry = { mltac_name = name; mltac_index = len - i - 1 } in - let map id = Reference (Misctypes.ArgVar (Loc.tag id)) in + let map id = Reference (Misctypes.ArgVar (CAst.make id)) in let tac = TacML (Loc.tag (entry, List.map map ids)) in add_glob_tactic_notation false ~level prods true ids tac in @@ -431,11 +431,11 @@ let warn_unusable_identifier = let register_ltac local tacl = let map tactic_body = match tactic_body with - | Tacexpr.TacticDefinition ((loc,id), body) -> + | Tacexpr.TacticDefinition ({CAst.loc;v=id}, body) -> let kn = Lib.make_kn id in let id_pp = Id.print id in let () = if is_defined_tac kn then - CErrors.user_err ?loc + CErrors.user_err ?loc (str "There is already an Ltac named " ++ id_pp ++ str".") in let is_shadowed = diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index ccd555b61..146d8300d 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -41,7 +41,7 @@ type goal_selector = Vernacexpr.goal_selector = type 'a core_destruction_arg = 'a Misctypes.core_destruction_arg = | ElimOnConstr of 'a - | ElimOnIdent of Id.t located + | ElimOnIdent of lident | ElimOnAnonHyp of int type 'a destruction_arg = @@ -85,8 +85,8 @@ type 'a match_pattern = (* Type of hypotheses for a Match Context rule *) type 'a match_context_hyps = - | Hyp of Name.t located * 'a match_pattern - | Def of Name.t located * 'a match_pattern * 'a match_pattern + | Hyp of lname * 'a match_pattern + | Def of lname * 'a match_pattern * 'a match_pattern (* Type of a Match rule for Match Context and Match *) type ('a,'t) match_rule = @@ -254,7 +254,7 @@ and 'a gen_tactic_expr = | TacFail of global_flag * int or_var * 'n message_token list | TacInfo of 'a gen_tactic_expr | TacLetIn of rec_flag * - (Name.t located * 'a gen_tactic_arg) list * + (lname * 'a gen_tactic_arg) list * 'a gen_tactic_expr | TacMatch of lazy_flag * 'a gen_tactic_expr * @@ -300,7 +300,7 @@ type g_trm = glob_constr_and_expr type g_pat = glob_constr_pattern_and_expr type g_cst = evaluable_global_reference and_short_name or_var type g_ref = ltac_constant located or_var -type g_nam = Id.t located +type g_nam = lident type g_dispatch = < term:g_trm; @@ -328,7 +328,7 @@ type r_trm = constr_expr type r_pat = constr_pattern_expr type r_cst = reference or_by_notation type r_ref = reference -type r_nam = Id.t located +type r_nam = lident type r_lev = rlevel type r_dispatch = < @@ -357,7 +357,7 @@ type t_trm = EConstr.constr type t_pat = constr_pattern type t_cst = evaluable_global_reference type t_ref = ltac_constant located -type t_nam = Id.t +type t_nam = Id.t type t_dispatch = < term:t_trm; @@ -391,5 +391,5 @@ type ltac_call_kind = type ltac_trace = ltac_call_kind Loc.located list type tacdef_body = - | TacticDefinition of Id.t Loc.located * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *) + | TacticDefinition of lident * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *) | TacticRedefinition of reference * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *) diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index ebffde441..22ec6c5b1 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -6,12 +6,13 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pattern open Pp +open CErrors +open CAst +open Pattern open Genredexpr open Glob_term open Tacred -open CErrors open Util open Names open Libnames @@ -73,11 +74,11 @@ let strict_check = ref false let adjust_loc loc = if !strict_check then None else loc (* Globalize a name which must be bound -- actually just check it is bound *) -let intern_hyp ist (loc,id as locid) = +let intern_hyp ist ({loc;v=id} as locid) = if not !strict_check then locid else if find_ident id ist then - Loc.tag id + make id else Pretype_errors.error_var_not_found ?loc id @@ -89,7 +90,8 @@ 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 -> ArgVar (loc,id) + | Ident (loc,id) when find_var id ist -> + ArgVar CAst.(make ?loc id) | r -> let loc,_ as lqid = qualid_of_reference r in try ArgArg (loc,locate_global_with_alias lqid) @@ -99,7 +101,7 @@ let intern_ltac_variable ist = function | Ident (loc,id) -> if find_var id ist then (* A local variable of any type *) - ArgVar (loc,id) + ArgVar CAst.(make ?loc id) else raise Not_found | _ -> raise Not_found @@ -249,7 +251,7 @@ and intern_or_and_intro_pattern lf ist = function IntroOrPattern (List.map (List.map (intern_intro_pattern lf ist)) ll) let intern_or_and_intro_pattern_loc lf ist = function - | ArgVar (_,id) as x -> + | ArgVar {v=id} as x -> if find_var id ist then x else user_err Pp.(str "Disjunctive/conjunctive introduction pattern expected.") | ArgArg (loc,l) -> ArgArg (loc,intern_or_and_intro_pattern lf ist l) @@ -261,18 +263,18 @@ let intern_intro_pattern_naming_loc lf ist (loc,pat) = let intern_destruction_arg ist = function | clear,ElimOnConstr c -> clear,ElimOnConstr (intern_constr_with_bindings ist c) | clear,ElimOnAnonHyp n as x -> x - | clear,ElimOnIdent (loc,id) -> + | clear,ElimOnIdent {loc;v=id} -> if !strict_check then (* If in a defined tactic, no intros-until *) let c, p = intern_constr ist (CAst.make @@ CRef (Ident (Loc.tag id), None)) in match DAst.get c with - | GVar id -> clear,ElimOnIdent (c.CAst.loc,id) + | GVar id -> clear,ElimOnIdent CAst.(make ?loc:c.loc id) | _ -> clear,ElimOnConstr ((c, p), NoBindings) else - clear,ElimOnIdent (loc,id) + clear,ElimOnIdent CAst.(make ?loc id) let short_name = function - | AN (Ident (loc,id)) when not !strict_check -> Some (loc,id) + | AN (Ident (loc,id)) when not !strict_check -> Some CAst.(make ?loc id) | _ -> None let intern_evaluable_global_reference ist r = @@ -292,9 +294,9 @@ let intern_evaluable_reference_or_by_notation ist = function (* Globalize a reduction expression *) let intern_evaluable ist = function - | AN (Ident (loc,id)) when find_var id ist -> ArgVar (loc,id) + | AN (Ident (loc,id)) when find_var id ist -> ArgVar CAst.(make ?loc id) | AN (Ident (loc,id)) when not !strict_check && find_hyp id ist -> - ArgArg (EvalVarRef id, Some (loc,id)) + ArgArg (EvalVarRef id, Some CAst.(make ?loc id)) | r -> let e = intern_evaluable_reference_or_by_notation ist r in let na = short_name r in @@ -370,7 +372,7 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) = Inr (bound_names,(c,None),dummy_pat) in (l, match p with | Inl r -> interp_ref r - | Inr { CAst.v = CAppExpl((None,r,None),[]) } -> + | Inr { v = CAppExpl((None,r,None),[]) } -> (* We interpret similarly @ref and ref *) interp_ref (AN r) | Inr c -> @@ -400,8 +402,8 @@ let intern_red_expr ist = function | Lazy f -> Lazy (intern_flag ist f) | Pattern l -> Pattern (List.map (intern_constr_with_occurrences ist) l) | Simpl (f,o) -> - Simpl (intern_flag ist f, - Option.map (intern_typed_pattern_or_ref_with_occurrences ist) o) + Simpl (intern_flag ist f, + Option.map (intern_typed_pattern_or_ref_with_occurrences ist) o) | CbvVm o -> CbvVm (Option.map (intern_typed_pattern_or_ref_with_occurrences ist) o) | CbvNative o -> CbvNative (Option.map (intern_typed_pattern_or_ref_with_occurrences ist) o) | (Red _ | Hnf | ExtraRedExpr _ as r ) -> r @@ -438,7 +440,7 @@ let intern_pattern ist ?(as_type=false) ltacvars = function let intern_constr_may_eval ist = function | ConstrEval (r,c) -> ConstrEval (intern_red_expr ist r,intern_constr ist c) | ConstrContext (locid,c) -> - ConstrContext (intern_hyp ist locid,intern_constr ist c) + ConstrContext (intern_hyp ist locid,intern_constr ist c) | ConstrTypeOf c -> ConstrTypeOf (intern_constr ist c) | ConstrTerm c -> ConstrTerm (intern_constr ist c) @@ -452,12 +454,12 @@ let opt_cons accu = function (* Reads the hypotheses of a "match goal" rule *) let rec intern_match_goal_hyps ist ?(as_type=false) lfun = function - | (Hyp ((_,na) as locna,mp))::tl -> + | (Hyp ({v=na} as locna,mp))::tl -> let ido, metas1, pat = intern_pattern ist ~as_type:true lfun mp in let lfun, metas2, hyps = intern_match_goal_hyps ist lfun tl in let lfun' = name_cons (opt_cons lfun ido) na in lfun', metas1@metas2, Hyp (locna,pat)::hyps - | (Def ((_,na) as locna,mv,mp))::tl -> + | (Def ({v=na} as locna,mv,mp))::tl -> let ido, metas1, patv = intern_pattern ist ~as_type:false lfun mv in let ido', metas2, patt = intern_pattern ist ~as_type:true lfun mp in let lfun, metas3, hyps = intern_match_goal_hyps ist ~as_type lfun tl in @@ -467,7 +469,7 @@ let rec intern_match_goal_hyps ist ?(as_type=false) lfun = function (* Utilities *) let extract_let_names lrc = - let fold accu ((loc, name), _) = + let fold accu ({loc;v=name}, _) = Nameops.Name.fold_right (fun id accu -> if Id.Set.mem id accu then user_err ?loc ~hdr:"glob_tactic" (str "This variable is bound several times.") @@ -813,7 +815,7 @@ let notation_subst bindings tac = let fold id c accu = let loc = Glob_ops.loc_of_glob_constr (fst c) in let c = ConstrMayEval (ConstrTerm c) in - ((loc, Name id), c) :: accu + (CAst.make ?loc @@ Name id, c) :: accu in let bindings = Id.Map.fold fold bindings [] in (** This is theoretically not correct due to potential variable capture, but diff --git a/plugins/ltac/tacintern.mli b/plugins/ltac/tacintern.mli index e3a4d5c79..8021dc715 100644 --- a/plugins/ltac/tacintern.mli +++ b/plugins/ltac/tacintern.mli @@ -47,7 +47,7 @@ val intern_constr_with_bindings : glob_sign -> constr_expr * constr_expr bindings -> glob_constr_and_expr * glob_constr_and_expr bindings -val intern_hyp : glob_sign -> Id.t Loc.located -> Id.t Loc.located +val intern_hyp : glob_sign -> lident -> lident (** Adds a globalization function for extra generic arguments *) diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index f2720954d..79b5c1622 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -9,6 +9,7 @@ open Constrintern open Patternops open Pp +open CAst open Genredexpr open Glob_term open Glob_ops @@ -363,16 +364,16 @@ let error_ltac_variable ?loc id env v s = strbrk "which cannot be coerced to " ++ str s ++ str".") (* Raise Not_found if not in interpretation sign *) -let try_interp_ltac_var coerce ist env (loc,id) = +let try_interp_ltac_var coerce ist env {loc;v=id} = let v = Id.Map.find id ist.lfun in try coerce v with CannotCoerceTo s -> error_ltac_variable ?loc id env v s let interp_ltac_var coerce ist env locid = try try_interp_ltac_var coerce ist env locid - with Not_found -> anomaly (str "Detected '" ++ Id.print (snd locid) ++ str "' as ltac var at interning time.") + with Not_found -> anomaly (str "Detected '" ++ Id.print locid.v ++ str "' as ltac var at interning time.") let interp_ident ist env sigma id = - try try_interp_ltac_var (coerce_var_to_ident false env sigma) ist (Some (env,sigma)) (Loc.tag id) + try try_interp_ltac_var (coerce_var_to_ident false env sigma) ist (Some (env,sigma)) (make id) with Not_found -> id (* Interprets an optional identifier, bound or fresh *) @@ -381,25 +382,25 @@ let interp_name ist env sigma = function | Name id -> Name (interp_ident ist env sigma id) let interp_intro_pattern_var loc ist env sigma id = - try try_interp_ltac_var (coerce_to_intro_pattern env sigma) ist (Some (env,sigma)) (loc,id) + try try_interp_ltac_var (coerce_to_intro_pattern env sigma) ist (Some (env,sigma)) (make ?loc id) with Not_found -> IntroNaming (IntroIdentifier id) let interp_intro_pattern_naming_var loc ist env sigma id = - try try_interp_ltac_var (coerce_to_intro_pattern_naming env sigma) ist (Some (env,sigma)) (loc,id) + try try_interp_ltac_var (coerce_to_intro_pattern_naming env sigma) ist (Some (env,sigma)) (make ?loc id) with Not_found -> IntroIdentifier id -let interp_int ist locid = +let interp_int ist ({loc;v=id} as locid) = try try_interp_ltac_var coerce_to_int ist None locid with Not_found -> - user_err ?loc:(fst locid) ~hdr:"interp_int" - (str "Unbound variable " ++ Id.print (snd locid) ++ str".") + user_err ?loc ~hdr:"interp_int" + (str "Unbound variable " ++ Id.print id ++ str".") let interp_int_or_var ist = function | ArgVar locid -> interp_int ist locid | ArgArg n -> n let interp_int_or_var_as_list ist = function - | ArgVar (_,id as locid) -> + | ArgVar ({v=id} as locid) -> (try coerce_to_int_or_var_list (Id.Map.find id ist.lfun) with Not_found | CannotCoerceTo _ -> [ArgArg (interp_int ist locid)]) | ArgArg n as x -> [x] @@ -408,7 +409,7 @@ let interp_int_or_var_list ist l = List.flatten (List.map (interp_int_or_var_as_list ist) l) (* Interprets a bound variable (especially an existing hypothesis) *) -let interp_hyp ist env sigma (loc,id as locid) = +let interp_hyp ist env sigma ({loc;v=id} as locid) = (* Look first in lfun for a value coercible to a variable *) try try_interp_ltac_var (coerce_to_hyp env sigma) ist (Some (env,sigma)) locid with Not_found -> @@ -416,7 +417,7 @@ let interp_hyp ist env sigma (loc,id as locid) = if is_variable env id then id else Loc.raise ?loc (Logic.RefinerError (env, sigma, Logic.NoSuchHyp id)) -let interp_hyp_list_as_list ist env sigma (loc,id as x) = +let interp_hyp_list_as_list ist env sigma ({loc;v=id} as x) = try coerce_to_hyp_list env sigma (Id.Map.find id ist.lfun) with Not_found | CannotCoerceTo _ -> [interp_hyp ist env sigma x] @@ -425,8 +426,8 @@ let interp_hyp_list ist env sigma l = let interp_reference ist env sigma = function | ArgArg (_,r) -> r - | ArgVar (loc, id) -> - try try_interp_ltac_var (coerce_to_reference env sigma) ist (Some (env,sigma)) (loc, id) + | ArgVar {loc;v=id} -> + try try_interp_ltac_var (coerce_to_reference env sigma) ist (Some (env,sigma)) (make ?loc id) with Not_found -> try VarRef (get_id (Environ.lookup_named id env)) @@ -439,7 +440,7 @@ let try_interp_evaluable env (loc, id) = | _ -> error_not_evaluable (VarRef id) let interp_evaluable ist env sigma = function - | ArgArg (r,Some (loc,id)) -> + | ArgArg (r,Some {loc;v=id}) -> (* Maybe [id] has been introduced by Intro-like tactics *) begin try try_interp_evaluable env (loc, id) @@ -449,8 +450,8 @@ let interp_evaluable ist env sigma = function | _ -> error_global_not_found ?loc (qualid_of_ident id) end | ArgArg (r,None) -> r - | ArgVar (loc, id) -> - try try_interp_ltac_var (coerce_to_evaluable_ref env sigma) ist (Some (env,sigma)) (loc, id) + | ArgVar {loc;v=id} -> + try try_interp_ltac_var (coerce_to_evaluable_ref env sigma) ist (Some (env,sigma)) (make ?loc id) with Not_found -> try try_interp_evaluable env (loc, id) with Not_found -> error_global_not_found ?loc (qualid_of_ident id) @@ -521,9 +522,9 @@ let default_fresh_id = Id.of_string "H" let interp_fresh_id ist env sigma l = let extract_ident ist env sigma id = try try_interp_ltac_var (coerce_to_ident_not_fresh env sigma) - ist (Some (env,sigma)) (Loc.tag id) + ist (Some (env,sigma)) (make id) with Not_found -> id in - let ids = List.map_filter (function ArgVar (_, id) -> Some id | _ -> None) l in + let ids = List.map_filter (function ArgVar {v=id} -> Some id | _ -> None) l in let avoid = match TacStore.get ist.extra f_avoid_ids with | None -> Id.Set.empty | Some l -> l @@ -535,7 +536,7 @@ let interp_fresh_id ist env sigma l = let s = String.concat "" (List.map (function | ArgArg s -> s - | ArgVar (_,id) -> Id.to_string (extract_ident ist env sigma id)) l) in + | ArgVar {v=id} -> Id.to_string (extract_ident ist env sigma id)) l) in let s = if CLexer.is_keyword s then s^"0" else s in Id.of_string s in Tactics.fresh_id_in_env avoid id env @@ -701,7 +702,7 @@ let interp_constr_with_occurrences ist env sigma (occs,c) = let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) = let p = match a with - | Inl (ArgVar (loc,id)) -> + | Inl (ArgVar {loc;v=id}) -> (* This is the encoding of an ltac var supposed to be bound prioritary to an evaluable reference and otherwise to a constr (it is an encoding to satisfy the "union" type given to Simpl) *) @@ -710,7 +711,7 @@ let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) = with CannotCoerceTo _ -> let c = coerce_to_closed_constr env x in Inr (pattern_of_constr env sigma (EConstr.to_constr sigma c)) in - (try try_interp_ltac_var coerce_eval_ref_or_constr ist (Some (env,sigma)) (loc,id) + (try try_interp_ltac_var coerce_eval_ref_or_constr ist (Some (env,sigma)) (make ?loc id) with Not_found -> error_global_not_found ?loc (qualid_of_ident id)) | Inl (ArgArg _ as b) -> Inl (interp_evaluable ist env sigma b) @@ -756,7 +757,7 @@ let interp_may_eval f ist env sigma = function let (sigma,c_interp) = f ist env sigma c in let (redfun, _) = Redexpr.reduction_of_red_expr env redexp in redfun env sigma c_interp - | ConstrContext ((loc,s),c) -> + | ConstrContext ({loc;v=s},c) -> (try let (sigma,ic) = f ist env sigma c in let ctxt = coerce_to_constr_context (Id.Map.find s ist.lfun) in @@ -821,7 +822,7 @@ let message_of_value v = let interp_message_token ist = function | MsgString s -> Ftactic.return (str s) | MsgInt n -> Ftactic.return (int n) - | MsgIdent (loc,id) -> + | MsgIdent {loc;v=id} -> let v = try Some (Id.Map.find id ist.lfun) with Not_found -> None in match v with | None -> Ftactic.lift (Tacticals.New.tclZEROMSG (Id.print id ++ str" not found.")) @@ -881,7 +882,7 @@ let interp_intro_pattern_naming_option ist env sigma = function let interp_or_and_intro_pattern_option ist env sigma = function | None -> sigma, None - | Some (ArgVar (loc,id)) -> + | Some (ArgVar {loc;v=id}) -> (match interp_intro_pattern_var loc ist env sigma id with | IntroAction (IntroOrAndPattern l) -> sigma, Some (loc,l) | _ -> @@ -906,14 +907,14 @@ let interp_binding_name ist env sigma = function (* If a name is bound, it has to be a quantified hypothesis *) (* user has to use other names for variables if these ones clash with *) (* a name intented to be used as a (non-variable) identifier *) - try try_interp_ltac_var (coerce_to_quantified_hypothesis sigma) ist (Some (env,sigma)) (Loc.tag id) + try try_interp_ltac_var (coerce_to_quantified_hypothesis sigma) ist (Some (env,sigma)) (make id) with Not_found -> NamedHyp id let interp_declared_or_quantified_hypothesis ist env sigma = function | AnonHyp n -> AnonHyp n | NamedHyp id -> try try_interp_ltac_var - (coerce_to_decl_or_quant_hyp env sigma) ist (Some (env,sigma)) (Loc.tag id) + (coerce_to_decl_or_quant_hyp env sigma) ist (Some (env,sigma)) (make id) with Not_found -> NamedHyp id let interp_binding ist env sigma (loc,(b,c)) = @@ -924,7 +925,7 @@ let interp_bindings ist env sigma = function | NoBindings -> sigma, NoBindings | ImplicitBindings l -> - let sigma, l = interp_open_constr_list ist env sigma l in + let sigma, l = interp_open_constr_list ist env sigma l in sigma, ImplicitBindings l | ExplicitBindings l -> let sigma, l = List.fold_left_map (interp_binding ist env) sigma l in @@ -959,14 +960,14 @@ let interp_destruction_arg ist gl arg = interp_open_constr_with_bindings ist env sigma c end | keep,ElimOnAnonHyp n as x -> x - | keep,ElimOnIdent (loc,id) -> + | keep,ElimOnIdent {loc;v=id} -> let error () = user_err ?loc (strbrk "Cannot coerce " ++ Id.print id ++ strbrk " neither to a quantified hypothesis nor to a term.") in let try_cast_id id' = if Tactics.is_quantified_hypothesis id' gl - then keep,ElimOnIdent (loc,id') + then keep,ElimOnIdent CAst.(make ?loc id') else (keep, ElimOnConstr begin fun env sigma -> try (sigma, (constr_of_id env id', NoBindings)) @@ -994,7 +995,7 @@ let interp_destruction_arg ist gl arg = with Not_found -> (* We were in non strict (interactive) mode *) if Tactics.is_quantified_hypothesis id gl then - keep,ElimOnIdent (loc,id) + keep,ElimOnIdent CAst.(make ?loc id) else let c = (DAst.make ?loc @@ GVar id,Some (CAst.make @@ CRef (Ident (loc,id),None))) in let f env sigma = @@ -1043,11 +1044,11 @@ let cons_and_check_name id l = else id::l let rec read_match_goal_hyps lfun ist env sigma lidh = function - | (Hyp ((loc,na) as locna,mp))::tl -> + | (Hyp ({loc;v=na} as locna,mp))::tl -> let lidh' = Name.fold_right cons_and_check_name na lidh in Hyp (locna,read_pattern lfun ist env sigma mp):: (read_match_goal_hyps lfun ist env sigma lidh' tl) - | (Def ((loc,na) as locna,mv,mp))::tl -> + | (Def ({loc;v=na} as locna,mv,mp))::tl -> let lidh' = Name.fold_right cons_and_check_name na lidh in Def (locna,read_pattern lfun ist env sigma mv, read_pattern lfun ist env sigma mp):: (read_match_goal_hyps lfun ist env sigma lidh' tl) @@ -1112,7 +1113,7 @@ let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftacti in Tactic_debug.debug_prompt lev tac eval | _ -> value_interp ist >>= fun v -> return (name_vfun appl v) - + and eval_tactic ist tac : unit Proofview.tactic = match tac with | TacAtom (loc,t) -> @@ -1248,7 +1249,7 @@ and force_vrec ist v : Val.t Ftactic.t = and interp_ltac_reference ?loc' mustbetac ist r : Val.t Ftactic.t = match r with - | ArgVar (loc,id) -> + | ArgVar {loc;v=id} -> let v = try Id.Map.find id ist.lfun with Not_found -> in_gen (topwit wit_var) id @@ -1416,7 +1417,7 @@ and tactic_of_value ist vle = and interp_letrec ist llc u = Proofview.tclUNIT () >>= fun () -> (* delay for the effects of [lref], just in case. *) let lref = ref ist.lfun in - let fold accu ((_, na), b) = + let fold accu ({v=na}, b) = let v = of_tacvalue (VRec (lref, TacArg (Loc.tag b))) in Name.fold_right (fun id -> Id.Map.add id v) na accu in @@ -1431,7 +1432,7 @@ and interp_letin ist llc u = | [] -> let ist = { ist with lfun } in val_interp ist u - | ((_, na), body) :: defs -> + | ({v=na}, body) :: defs -> Ftactic.bind (interp_tacarg ist body) (fun v -> fold (Name.fold_right (fun id -> Id.Map.add id v) na lfun) defs) in diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index 5f2723a1e..2d448e832 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -75,7 +75,7 @@ val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr -> Evd.evar_map (** Interprets tactic expressions *) val interp_hyp : interp_sign -> Environ.env -> Evd.evar_map -> - Id.t Loc.located -> Id.t + lident -> Id.t val interp_glob_closure : interp_sign -> Environ.env -> Evd.evar_map -> ?kind:Pretyping.typing_constraint -> ?pattern_mode:bool -> glob_constr_and_expr -> @@ -125,9 +125,9 @@ val hide_interp : bool -> raw_tactic_expr -> unit Proofview.tactic option -> uni (** Internals that can be useful for syntax extensions. *) val interp_ltac_var : (value -> 'a) -> interp_sign -> - (Environ.env * Evd.evar_map) option -> Id.t Loc.located -> 'a + (Environ.env * Evd.evar_map) option -> lident -> 'a -val interp_int : interp_sign -> Id.t Loc.located -> int +val interp_int : interp_sign -> lident -> int val interp_int_or_var : interp_sign -> int or_var -> int diff --git a/plugins/ltac/tactic_debug.mli b/plugins/ltac/tactic_debug.mli index 2475e41f9..dce6f5558 100644 --- a/plugins/ltac/tactic_debug.mli +++ b/plugins/ltac/tactic_debug.mli @@ -74,7 +74,7 @@ val db_logic_failure : debug_info -> exn -> unit Proofview.NonLogical.t (** Prints a logic failure message for a rule *) val db_breakpoint : debug_info -> - Id.t Loc.located message_token list -> unit Proofview.NonLogical.t + Misctypes.lident message_token list -> unit Proofview.NonLogical.t val extract_ltac_trace : ?loc:Loc.t -> Tacexpr.ltac_trace -> Pp.t option Loc.located diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml index e87951dd7..6bf9215e0 100644 --- a/plugins/ltac/tactic_matching.ml +++ b/plugins/ltac/tactic_matching.ml @@ -306,9 +306,9 @@ module PatternMatching (E:StaticEnvironment) = struct [pat] is [Hyp _] or [Def _]. *) let hyp_match pat hyps = match pat with - | Hyp ((_,hypname),typepat) -> + | Hyp ({CAst.v=hypname},typepat) -> hyp_match_type hypname typepat hyps - | Def ((_,hypname),bodypat,typepat) -> + | Def ({CAst.v=hypname},bodypat,typepat) -> hyp_match_body_and_type hypname bodypat typepat hyps (** [hyp_pattern_list_match pats hyps lhs], matches the list of diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml index 01d3f79c7..5ce30c3d7 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -255,10 +255,10 @@ let tauto_power_flags = { } let with_flags flags _ ist = - let f = (Loc.tag @@ Id.of_string "f") in - let x = (Loc.tag @@ Id.of_string "x") in + let f = CAst.make @@ Id.of_string "f" in + let x = CAst.make @@ Id.of_string "x" in let arg = Val.Dyn (tag_tauto_flags, flags) in - let ist = { ist with lfun = Id.Map.add (snd x) arg ist.lfun } in + let ist = { ist with lfun = Id.Map.add x.CAst.v arg ist.lfun } in eval_tactic_ist ist (TacArg (Loc.tag @@ TacCall (Loc.tag (ArgVar f, [Reference (ArgVar x)])))) let register_tauto_tactic tac name0 args = diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4 index 40897d62f..55dc7f580 100644 --- a/plugins/quote/g_quote.ml4 +++ b/plugins/quote/g_quote.ml4 @@ -22,7 +22,7 @@ let x = Id.of_string "x" let make_cont (k : Val.t) (c : EConstr.t) = let c = Tacinterp.Value.of_constr c in - let tac = TacCall (Loc.tag (ArgVar (Loc.tag cont), [Reference (ArgVar (Loc.tag x))])) in + let tac = TacCall (Loc.tag (ArgVar CAst.(make cont), [Reference (ArgVar CAst.(make x))])) in let ist = { lfun = Id.Map.add cont k (Id.Map.singleton x c); extra = TacStore.empty; } in Tacinterp.eval_tactic_ist ist (TacArg (Loc.tag tac)) diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index e3e749b75..125afb1a0 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -166,12 +166,12 @@ let ltac_call tac (args:glob_tactic_arg list) = (* Calling a locally bound tactic *) let ltac_lcall tac args = - TacArg(Loc.tag @@ TacCall (Loc.tag (ArgVar(Loc.tag @@ Id.of_string tac),args))) + TacArg(Loc.tag @@ TacCall (Loc.tag (ArgVar CAst.(make @@ Id.of_string tac),args))) let ltac_apply (f : Value.t) (args: Tacinterp.Value.t list) = let fold arg (i, vars, lfun) = let id = Id.of_string ("x" ^ string_of_int i) in - let x = Reference (ArgVar (Loc.tag id)) in + let x = Reference (ArgVar CAst.(make id)) in (succ i, x :: vars, Id.Map.add id arg lfun) in let (_, args, lfun) = List.fold_right fold args (0, [], Id.Map.empty) in @@ -206,7 +206,7 @@ let get_res = let exec_tactic env evd n f args = let fold arg (i, vars, lfun) = let id = Id.of_string ("x" ^ string_of_int i) in - let x = Reference (ArgVar (Loc.tag id)) in + let x = Reference (ArgVar CAst.(make id)) in (succ i, x :: vars, Id.Map.add id (Value.of_constr arg) lfun) in let (_, args, lfun) = List.fold_right fold args (0, [], Id.Map.empty) in diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 499154d50..4ae746288 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -268,7 +268,7 @@ let interp_wit wit ist gl x = sigma, Tacinterp.Value.cast (topwit wit) arg let interp_hyp ist gl (SsrHyp (loc, id)) = - let s, id' = interp_wit wit_var ist gl (loc, id) in + let s, id' = interp_wit wit_var ist gl CAst.(make ?loc id) in if not_section_id id' then s, SsrHyp (loc, id') else hyp_err ?loc "Can't clear section hypothesis " id' @@ -835,9 +835,9 @@ let rec mkCHoles ?loc n = if n <= 0 then [] else (CAst.make ?loc @@ CHole (None, IntroAnonymous, None)) :: mkCHoles ?loc (n - 1) let mkCHole loc = CAst.make ?loc @@ CHole (None, IntroAnonymous, None) let mkCLambda ?loc name ty t = CAst.make ?loc @@ - CLambdaN ([CLocalAssum([loc, name], Default Explicit, ty)], t) + CLambdaN ([CLocalAssum([CAst.make ?loc name], Default Explicit, ty)], t) let mkCArrow ?loc ty t = CAst.make ?loc @@ - CProdN ([CLocalAssum([Loc.tag Anonymous], Default Explicit, ty)], t) + CProdN ([CLocalAssum([CAst.make Anonymous], Default Explicit, ty)], t) let mkCCast ?loc t ty = CAst.make ?loc @@ CCast (t, CastConv ty) let rec isCHoles = function { CAst.v = CHole _ } :: cl -> isCHoles cl | cl -> cl = [] @@ -855,7 +855,7 @@ let pf_interp_ty ?(resolve_typeclasses=false) ist gl ty = | _, (_, Some ty) -> let rec force_type ty = CAst.(map (function | CProdN (abs, t) -> - n_binders := !n_binders + List.length (List.flatten (List.map (function CLocalAssum (nal,_,_) -> nal | CLocalDef (na,_,_) -> [na] | CLocalPattern (_,_) -> (* We count a 'pat for 1; TO BE CHECKED *) [Loc.tag Name.Anonymous]) abs)); + n_binders := !n_binders + List.length (List.flatten (List.map (function CLocalAssum (nal,_,_) -> nal | CLocalDef (na,_,_) -> [na] | CLocalPattern _ -> (* We count a 'pat for 1; TO BE CHECKED *) [CAst.make Name.Anonymous]) abs)); CProdN (abs, force_type t) | CLetIn (n, v, oty, t) -> incr n_binders; CLetIn (n, v, oty, force_type t) | _ -> (mkCCast ty (mkCType None)).v)) ty in diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index 211cad3f5..0d8044f19 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -130,7 +130,7 @@ let pr_ssrhyp _ _ _ = pr_hyp let wit_ssrhyprep = add_genarg "ssrhyprep" pr_hyp let intern_hyp ist (SsrHyp (loc, id) as hyp) = - let _ = Tacintern.intern_genarg ist (in_gen (rawwit wit_var) (loc, id)) in + let _ = Tacintern.intern_genarg ist (in_gen (rawwit wit_var) CAst.(make ?loc id)) in if not_section_id id then hyp else hyp_err ?loc "Can't clear section hypothesis " id @@ -316,7 +316,7 @@ END let pr_index = function - | Misctypes.ArgVar (_, id) -> pr_id id + | Misctypes.ArgVar {CAst.v=id} -> pr_id id | Misctypes.ArgArg n when n > 0 -> int n | _ -> mt () let pr_ssrindex _ _ _ = pr_index @@ -330,13 +330,13 @@ let mk_index ?loc = function | iv -> iv let interp_index ist gl idx = - Tacmach.project gl, + Tacmach.project gl, match idx with | Misctypes.ArgArg _ -> idx - | Misctypes.ArgVar (loc, id) -> + | Misctypes.ArgVar id -> let i = try - let v = Id.Map.find id ist.Tacinterp.lfun in + let v = Id.Map.find id.CAst.v ist.Tacinterp.lfun in begin match Tacinterp.Value.to_int v with | Some i -> i | None -> @@ -350,8 +350,8 @@ let interp_index ist gl idx = end | None -> raise Not_found end end - with _ -> CErrors.user_err ?loc (str"Index not a number") in - Misctypes.ArgArg (check_index ?loc i) + with _ -> CErrors.user_err ?loc:id.CAst.loc (str"Index not a number") in + Misctypes.ArgArg (check_index ?loc:id.CAst.loc i) open Pltac @@ -1014,22 +1014,22 @@ let rec mkBstruct i = function | [] -> [] let rec format_local_binders h0 bl0 = match h0, bl0 with - | BFvar :: h, CLocalAssum ([_, x], _, _) :: bl -> + | BFvar :: h, CLocalAssum ([{CAst.v=x}], _, _) :: bl -> Bvar x :: format_local_binders h bl | BFdecl _ :: h, CLocalAssum (lxs, _, t) :: bl -> - Bdecl (List.map snd lxs, t) :: format_local_binders h bl - | BFdef :: h, CLocalDef ((_, x), v, oty) :: bl -> + Bdecl (List.map (fun x -> x.CAst.v) lxs, t) :: format_local_binders h bl + | BFdef :: h, CLocalDef ({CAst.v=x}, v, oty) :: bl -> Bdef (x, oty, v) :: format_local_binders h bl | _ -> [] let rec format_constr_expr h0 c0 = let open CAst in match h0, c0 with - | BFvar :: h, { v = CLambdaN ([CLocalAssum([_, x], _, _)], c) } -> + | BFvar :: h, { v = CLambdaN ([CLocalAssum([{CAst.v=x}], _, _)], c) } -> let bs, c' = format_constr_expr h c in Bvar x :: bs, c' | BFdecl _:: h, { v = CLambdaN ([CLocalAssum(lxs, _, t)], c) } -> let bs, c' = format_constr_expr h c in - Bdecl (List.map snd lxs, t) :: bs, c' - | BFdef :: h, { v = CLetIn((_, x), v, oty, c) } -> + Bdecl (List.map (fun x -> x.CAst.v) lxs, t) :: bs, c' + | BFdef :: h, { v = CLetIn({CAst.v=x}, v, oty, c) } -> let bs, c' = format_constr_expr h c in Bdef (x, oty, v) :: bs, c' | [BFcast], { v = CCast (c, CastConv t) } -> @@ -1037,7 +1037,7 @@ let rec format_constr_expr h0 c0 = let open CAst in match h0, c0 with | BFrec (has_str, has_cast) :: h, { v = CFix ( _, [_, (Some locn, CStructRec), bl, t, c]) } -> let bs = format_local_binders h bl in - let bstr = if has_str then [Bstruct (Name (snd locn))] else [] in + let bstr = if has_str then [Bstruct (Name locn.CAst.v)] else [] in bs @ bstr @ (if has_cast then [Bcast t] else []), c | BFrec (_, has_cast) :: h, { v = CCoFix ( _, [_, bl, t, c]) } -> format_local_binders h bl @ (if has_cast then [Bcast t] else []), c @@ -1156,18 +1156,18 @@ ARGUMENT EXTEND ssrbvar TYPED AS constr PRINTED BY pr_ssrbvar END let bvar_lname = let open CAst in function - | { v = CRef (Ident (loc, id), _) } -> Loc.tag ?loc @@ Name id - | { loc = loc } -> Loc.tag ?loc Anonymous + | { v = CRef (Ident (loc, id), _) } -> CAst.make ?loc @@ Name id + | { loc = loc } -> CAst.make ?loc Anonymous let pr_ssrbinder prc _ _ (_, c) = prc c ARGUMENT EXTEND ssrbinder TYPED AS ssrfwdfmt * constr PRINTED BY pr_ssrbinder | [ ssrbvar(bv) ] -> - [ let xloc, _ as x = bvar_lname bv in + [ let { CAst.loc=xloc } as x = bvar_lname bv in (FwdPose, [BFvar]), CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Explicit,mkCHole xloc)],mkCHole (Some loc)) ] | [ "(" ssrbvar(bv) ")" ] -> - [ let xloc, _ as x = bvar_lname bv in + [ let { CAst.loc=xloc } as x = bvar_lname bv in (FwdPose, [BFvar]), CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Explicit,mkCHole xloc)],mkCHole (Some loc)) ] | [ "(" ssrbvar(bv) ":" lconstr(t) ")" ] -> @@ -1191,7 +1191,7 @@ GEXTEND Gram [ ["of" | "&"]; c = operconstr LEVEL "99" -> let loc = !@loc in (FwdPose, [BFvar]), - CAst.make ~loc @@ CLambdaN ([CLocalAssum ([Loc.tag ~loc Anonymous],Default Explicit,c)],mkCHole (Some loc)) ] + CAst.make ~loc @@ CLambdaN ([CLocalAssum ([CAst.make ~loc Anonymous],Default Explicit,c)],mkCHole (Some loc)) ] ]; END @@ -1250,13 +1250,13 @@ END let pr_ssrfixfwd _ _ _ (id, fwd) = str " fix " ++ pr_id id ++ pr_fwd fwd let bvar_locid = function - | { CAst.v = CRef (Ident (loc, id), _) } -> loc, id + | { CAst.v = CRef (Ident (loc, id), _) } -> CAst.make ?loc id | _ -> CErrors.user_err (Pp.str "Missing identifier after \"(co)fix\"") ARGUMENT EXTEND ssrfixfwd TYPED AS ident * ssrfwd PRINTED BY pr_ssrfixfwd | [ "fix" ssrbvar(bv) ssrbinder_list(bs) ssrstruct(sid) ssrfwd(fwd) ] -> - [ let (_, id) as lid = bvar_locid bv in + [ let { CAst.v=id } as lid = bvar_locid bv in let (fk, h), (ck, (rc, oc)) = fwd in let c = Option.get oc in let has_cast, t', c' = match format_constr_expr h c with @@ -1265,8 +1265,10 @@ ARGUMENT EXTEND ssrfixfwd TYPED AS ident * ssrfwd PRINTED BY pr_ssrfixfwd let lb = fix_binders bs in let has_struct, i = let rec loop = function - (l', Name id') :: _ when Option.equal Id.equal sid (Some id') -> true, (l', id') - | [l', Name id'] when sid = None -> false, (l', id') + | {CAst.loc=l'; v=Name id'} :: _ when Option.equal Id.equal sid (Some id') -> + true, CAst.make ?loc:l' id' + | [{CAst.loc=l';v=Name id'}] when sid = None -> + false, CAst.make ?loc:l' id' | _ :: bn -> loop bn | [] -> CErrors.user_err (Pp.str "Bad structural argument") in loop (names_of_local_assums lb) in @@ -1282,7 +1284,7 @@ let pr_ssrcofixfwd _ _ _ (id, fwd) = str " cofix " ++ pr_id id ++ pr_fwd fwd ARGUMENT EXTEND ssrcofixfwd TYPED AS ssrfixfwd PRINTED BY pr_ssrcofixfwd | [ "cofix" ssrbvar(bv) ssrbinder_list(bs) ssrfwd(fwd) ] -> - [ let _, id as lid = bvar_locid bv in + [ let { CAst.v=id } as lid = bvar_locid bv in let (fk, h), (ck, (rc, oc)) = fwd in let c = Option.get oc in let has_cast, t', c' = match format_constr_expr h c with @@ -1323,7 +1325,7 @@ END let intro_id_to_binder = List.map (function | IPatId id -> - let xloc, _ as x = bvar_lname (mkCVar id) in + let { CAst.loc=xloc } as x = bvar_lname (mkCVar id) in (FwdPose, [BFvar]), CAst.make @@ CLambdaN ([CLocalAssum([x], Default Explicit, mkCHole xloc)], mkCHole None) @@ -1332,9 +1334,9 @@ let intro_id_to_binder = List.map (function let binder_to_intro_id = CAst.(List.map (function | (FwdPose, [BFvar]), { v = CLambdaN ([CLocalAssum(ids,_,_)],_) } | (FwdPose, [BFdecl _]), { v = CLambdaN ([CLocalAssum(ids,_,_)],_) } -> - List.map (function (_, Name id) -> IPatId id | _ -> IPatAnon One) ids - | (FwdPose, [BFdef]), { v = CLetIn ((_,Name id),_,_,_) } -> [IPatId id] - | (FwdPose, [BFdef]), { v = CLetIn ((_,Anonymous),_,_,_) } -> [IPatAnon One] + List.map (function {v=Name id} -> IPatId id | _ -> IPatAnon One) ids + | (FwdPose, [BFdef]), { v = CLetIn ({v=Name id},_,_,_) } -> [IPatId id] + | (FwdPose, [BFdef]), { v = CLetIn ({v=Anonymous},_,_,_) } -> [IPatAnon One] | _ -> anomaly "ssrbinder is not a binder")) let pr_ssrhavefwdwbinders _ _ prt (tr,((hpats, (fwd, hint)))) = @@ -1405,7 +1407,7 @@ let ssrorelse = Gram.entry_create "ssrorelse" GEXTEND Gram GLOBAL: ssrorelse ssrseqarg; ssrseqidx: [ - [ test_ssrseqvar; id = Prim.ident -> ArgVar (Loc.tag ~loc:!@loc id) + [ test_ssrseqvar; id = Prim.ident -> ArgVar (CAst.make ~loc:!@loc id) | n = Prim.natural -> ArgArg (check_index ~loc:!@loc n) ] ]; ssrswap: [[ IDENT "first" -> !@loc, true | IDENT "last" -> !@loc, false ]]; diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index 25d1472f1..8e6e0347f 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -79,9 +79,9 @@ let aliasvar = function let mk_cnotype mp = aliasvar mp, None in let mk_ctype mp t = aliasvar mp, Some t in let mk_rtype t = Some t in -let mk_dthen ?loc (mp, ct, rt) c = (Loc.tag ?loc (mp, c)), ct, rt in +let mk_dthen ?loc (mp, ct, rt) c = (CAst.make ?loc (mp, c)), ct, rt in let mk_let ?loc rt ct mp c1 = - CAst.make ?loc @@ CCases (LetPatternStyle, rt, ct, [Loc.tag ?loc (mp, c1)]) in + CAst.make ?loc @@ CCases (LetPatternStyle, rt, ct, [CAst.make ?loc (mp, c1)]) in let mk_pat c (na, t) = (c, na, t) in GEXTEND Gram GLOBAL: binder_constr; @@ -94,14 +94,16 @@ GEXTEND Gram ] ]; ssr_dthen: [[ dp = ssr_dpat; "then"; c = lconstr -> mk_dthen ~loc:!@loc dp c ]]; ssr_elsepat: [[ "else" -> [[CAst.make ~loc:!@loc @@ CPatAtom None]] ]]; - ssr_else: [[ mp = ssr_elsepat; c = lconstr -> Loc.tag ~loc:!@loc (mp, c) ]]; + ssr_else: [[ mp = ssr_elsepat; c = lconstr -> CAst.make ~loc:!@loc (mp, c) ]]; binder_constr: [ [ "if"; c = operconstr LEVEL "200"; "is"; db1 = ssr_dthen; b2 = ssr_else -> let b1, ct, rt = db1 in CAst.make ~loc:!@loc @@ CCases (MatchStyle, rt, [mk_pat c ct], [b1; b2]) | "if"; c = operconstr LEVEL "200";"isn't";db1 = ssr_dthen; b2 = ssr_else -> let b1, ct, rt = db1 in - let b1, b2 = - let (l1, (p1, r1)), (l2, (p2, r2)) = b1, b2 in (l1, (p1, r2)), (l2, (p2, r1)) in + let b1, b2 = let open CAst in + let {loc=l1; v=(p1, r1)}, {loc=l2; v=(p2, r2)} = b1, b2 in + (make ?loc:l1 (p1, r2), make ?loc:l2 (p2, r1)) + in CAst.make ~loc:!@loc @@ CCases (MatchStyle, rt, [mk_pat c ct], [b1; b2]) | "let"; ":"; mp = ssr_mpat; ":="; c = lconstr; "in"; c1 = lconstr -> mk_let ~loc:!@loc no_rt [mk_pat c no_ct] mp c1 @@ -118,7 +120,7 @@ GEXTEND Gram GLOBAL: closed_binder; closed_binder: [ [ ["of" | "&"]; c = operconstr LEVEL "99" -> - [CLocalAssum ([Loc.tag ~loc:!@loc Anonymous], Default Explicit, c)] + [CLocalAssum ([CAst.make ~loc:!@loc Anonymous], Default Explicit, c)] ] ]; END (* }}} *) @@ -553,7 +555,7 @@ GEXTEND Gram let s = coerce_reference_to_id qid in Vernacexpr.VernacDefinition ((Decl_kinds.NoDischarge,Decl_kinds.CanonicalStructure), - ((Loc.tag (Name s)),None), d) + ((CAst.make (Name s)),None), d) ]]; END @@ -584,10 +586,10 @@ END GEXTEND Gram GLOBAL: hloc; hloc: [ - [ "in"; "("; "Type"; "of"; id = ident; ")" -> - Tacexpr.HypLocation ((Loc.tag id), Locus.InHypTypeOnly) - | "in"; "("; IDENT "Value"; "of"; id = ident; ")" -> - Tacexpr.HypLocation ((Loc.tag id), Locus.InHypValueOnly) + [ "in"; "("; "Type"; "of"; id = ident; ")" -> + Tacexpr.HypLocation (CAst.make id, Locus.InHypTypeOnly) + | "in"; "("; IDENT "Value"; "of"; id = ident; ")" -> + Tacexpr.HypLocation (CAst.make id, Locus.InHypValueOnly) ] ]; END diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 71e8b4ac4..73e212365 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -137,9 +137,9 @@ let destGLambda c = match DAst.get c with GLambda (Name id, _, _, c) -> (id, c) let isGHole c = match DAst.get c with GHole _ -> true | _ -> false let mkCHole ~loc = CAst.make ?loc @@ CHole (None, IntroAnonymous, None) let mkCLambda ?loc name ty t = CAst.make ?loc @@ - CLambdaN ([CLocalAssum([Loc.tag ?loc name], Default Explicit, ty)], t) + CLambdaN ([CLocalAssum([CAst.make ?loc name], Default Explicit, ty)], t) let mkCLetIn ?loc name bo t = CAst.make ?loc @@ - CLetIn ((Loc.tag ?loc name), bo, None, t) + CLetIn ((CAst.make ?loc name), bo, None, t) let mkCCast ?loc t ty = CAst.make ?loc @@ CCast (t, dC ty) (** Constructors for rawconstr *) let mkRHole = DAst.make @@ GHole (InternalHole, IntroAnonymous, None) -- cgit v1.2.3