diff options
Diffstat (limited to 'plugins')
47 files changed, 929 insertions, 956 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 1cb417bf4..201726d1e 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -442,11 +442,11 @@ let cc_tactic depth additionnal_terms = let open Glob_term in let env = Proofview.Goal.env gl in let terms_to_complete = List.map (build_term_to_complete uf) (epsilons uf) in - let hole = GHole (Loc.ghost, Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None) in + let hole = CAst.make @@ GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None) in let pr_missing (c, missing) = let c = Detyping.detype ~lax:true false [] env sigma c in let holes = List.init missing (fun _ -> hole) in - Printer.pr_glob_constr_env env (GApp (Loc.ghost, c, holes)) + Printer.pr_glob_constr_env env (CAst.make @@ GApp (c, holes)) in Feedback.msg_info (Pp.str "Goal is solvable by congruence but some arguments are missing."); diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 5837a7196..fc1ed335a 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -887,7 +887,7 @@ let extract_constant_inline inline r ids s = let extract_inductive r s l optstr = check_inside_section (); let g = Smartlocate.global_with_alias r in - Dumpglob.add_glob (loc_of_reference r) g; + Dumpglob.add_glob ?loc:(loc_of_reference r) g; match g with | IndRef ((kn,i) as ip) -> let mib = Global.lookup_mind kn in diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index bbe1476bc..bbb9feae2 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -61,7 +61,7 @@ let default_intuition_tac = let name = { Tacexpr.mltac_plugin = "ground_plugin"; mltac_tactic = "auto_with"; } in let entry = { Tacexpr.mltac_name = name; mltac_index = 0 } in Tacenv.register_ml_tactic name [| tac |]; - Tacexpr.TacML (Loc.ghost, entry, []) + Tacexpr.TacML (Loc.tag (entry, [])) let (set_default_solver, default_solver, print_default_solver) = Tactic_option.declare_tactic_option ~default:default_intuition_tac "Firstorder default solver" diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index b5eacee81..5e6128b1b 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -23,8 +23,8 @@ open Pltac DECLARE PLUGIN "recdef_plugin" let pr_binding prc = function - | loc, NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ cut () ++ prc c) - | loc, AnonHyp n, c -> hov 1 (int n ++ str " := " ++ cut () ++ prc c) + | loc, (NamedHyp id, c) -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ cut () ++ prc c) + | loc, (AnonHyp n, c) -> hov 1 (int n ++ str " := " ++ cut () ++ prc c) let pr_bindings prc prlc = function | ImplicitBindings l -> @@ -158,7 +158,7 @@ GEXTEND Gram GLOBAL: function_rec_definition_loc ; function_rec_definition_loc: - [ [ g = Vernac.rec_definition -> !@loc, g ]] + [ [ g = Vernac.rec_definition -> Loc.tag ~loc:!@loc g ]] ; END diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 7dc869131..7f2b21e79 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -274,10 +274,10 @@ let make_discr_match_el = *) let make_discr_match_brl i = List.map_i - (fun j (_,idl,patl,_) -> + (fun j (_,(idl,patl,_)) -> Loc.tag @@ if Int.equal j i - then (Loc.ghost,idl,patl, mkGRef (Lazy.force coq_True_ref)) - else (Loc.ghost,idl,patl, mkGRef (Lazy.force coq_False_ref)) + then (idl,patl, mkGRef (Lazy.force coq_True_ref)) + else (idl,patl, mkGRef (Lazy.force coq_False_ref)) ) 0 (* @@ -348,9 +348,9 @@ let add_pat_variables pat typ env : Environ.env = let rec add_pat_variables env pat typ : Environ.env = observe (str "new rel env := " ++ Printer.pr_rel_context_of env (Evd.from_env env)); - match pat with - | PatVar(_,na) -> Environ.push_rel (RelDecl.LocalAssum (na,typ)) env - | PatCstr(_,c,patl,na) -> + match pat.CAst.v with + | PatVar na -> Environ.push_rel (RelDecl.LocalAssum (na,typ)) env + | PatCstr(c,patl,na) -> let Inductiveops.IndType(indf,indargs) = try Inductiveops.find_rectype env (Evd.from_env env) (EConstr.of_constr typ) with Not_found -> assert false @@ -398,11 +398,11 @@ let add_pat_variables pat typ env : Environ.env = -let rec pattern_to_term_and_type env typ = function - | PatVar(loc,Anonymous) -> assert false - | PatVar(loc,Name id) -> +let rec pattern_to_term_and_type env typ = CAst.with_val (function + | PatVar Anonymous -> assert false + | PatVar (Name id) -> mkGVar id - | PatCstr(loc,constr,patternl,_) -> + | PatCstr(constr,patternl,_) -> let cst_narg = Inductiveops.constructor_nallargs_env (Global.env ()) @@ -430,6 +430,7 @@ let rec pattern_to_term_and_type env typ = function mkGApp(mkGRef(ConstructRef constr), implicit_args@patl_as_term ) + ) (* [build_entry_lc funnames avoid rt] construct the list (in fact a build_entry_return) of constructors corresponding to [rt] when replacing calls to [funnames] by calls to the @@ -463,13 +464,14 @@ let rec pattern_to_term_and_type env typ = function *) -let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = +let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = observe (str " Entering : " ++ Printer.pr_glob_constr rt); - match rt with - | GRef _ | GVar _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> + let open CAst in + match rt.v with + | GRef _ | GVar _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> (* do nothing (except changing type of course) *) mk_result [] rt avoid - | GApp(_,_,_) -> + | GApp(_,_) -> let f,args = glob_decompose_app rt in let args_res : (glob_constr list) build_entry_return = List.fold_right (* create the arguments lists of constructors and combine them *) @@ -481,20 +483,20 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = (mk_result [] [] avoid) in begin - match f with + match f.v with | GLambda _ -> let rec aux t l = match l with | [] -> t - | u::l -> - match t with - | GLambda(loc,na,_,nat,b) -> - GLetIn(Loc.ghost,na,u,None,aux b l) + | u::l -> CAst.make @@ + match t.v with + | GLambda(na,_,nat,b) -> + GLetIn(na,u,None,aux b l) | _ -> - GApp(Loc.ghost,t,l) + GApp(t,l) in build_entry_lc env funnames avoid (aux f args) - | GVar(_,id) when Id.Set.mem id funnames -> + | GVar id when Id.Set.mem id funnames -> (* if we have [f t1 ... tn] with [f]$\in$[fnames] then we create a fresh variable [res], add [res] and its "value" (i.e. [res v1 ... vn]) to each @@ -535,7 +537,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = args_res.result } | GApp _ -> assert false (* we have collected all the app in [glob_decompose_app] *) - | GLetIn(_,n,v,t,b) -> + | GLetIn(n,v,t,b) -> (* if we have [(let x := v in b) t1 ... tn] , we discard our work and compute the list of constructor for [let x = v in (b t1 ... tn)] up to alpha conversion @@ -549,7 +551,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = let new_b = replace_var_by_term id - (GVar(Loc.ghost,id)) + (CAst.make @@ GVar id) b in (Name new_id,new_b,new_avoid) @@ -567,7 +569,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = *) let f_res = build_entry_lc env funnames args_res.to_avoid f in combine_results combine_app f_res args_res - | GCast(_,b,_) -> + | GCast(b,_) -> (* for an applied cast we just trash the cast part and restart the work. @@ -578,7 +580,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = | GProd _ -> error "Cannot apply a type" end (* end of the application treatement *) - | GLambda(_,n,_,t,b) -> + | GLambda(n,_,t,b) -> (* we first compute the list of constructor corresponding to the body of the function, then the one corresponding to the type @@ -593,7 +595,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = let new_env = raw_push_named (new_n,None,t) env in let b_res = build_entry_lc new_env funnames avoid b in combine_results (combine_lam new_n) t_res b_res - | GProd(_,n,_,t,b) -> + | GProd(n,_,t,b) -> (* we first compute the list of constructor corresponding to the body of the function, then the one corresponding to the type @@ -603,13 +605,13 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = let new_env = raw_push_named (n,None,t) env in let b_res = build_entry_lc new_env funnames avoid b in combine_results (combine_prod n) t_res b_res - | GLetIn(loc,n,v,typ,b) -> + | GLetIn(n,v,typ,b) -> (* we first compute the list of constructor corresponding to the body of the function, then the one corresponding to the value [t] and combine the two result *) - let v = match typ with None -> v | Some t -> GCast (loc,v,CastConv t) in + let v = match typ with None -> v | Some t -> CAst.make ?loc:rt.loc @@ GCast (v,CastConv t) in let v_res = build_entry_lc env funnames avoid v in let v_as_constr,ctx = Pretyping.understand env (Evd.from_env env) v in let v_type = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr v_as_constr) in @@ -621,13 +623,13 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = in let b_res = build_entry_lc new_env funnames avoid b in combine_results (combine_letin n) v_res b_res - | GCases(_,_,_,el,brl) -> + | GCases(_,_,el,brl) -> (* we create the discrimination function and treat the case itself *) let make_discr = make_discr_match brl in build_entry_lc_from_case env funnames make_discr el brl avoid - | GIf(_,b,(na,e_option),lhs,rhs) -> + | GIf(b,(na,e_option),lhs,rhs) -> let b_as_constr,ctx = Pretyping.understand env (Evd.from_env env) b in let b_typ = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr b_as_constr) in let (ind,_) = @@ -641,7 +643,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = assert (Int.equal (Array.length case_pats) 2); let brl = List.map_i - (fun i x -> (Loc.ghost,[],[case_pats.(i)],x)) + (fun i x -> Loc.tag ([],[case_pats.(i)],x)) 0 [lhs;rhs] in @@ -650,7 +652,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = in (* Pp.msgnl (str "new case := " ++ Printer.pr_glob_constr match_expr); *) build_entry_lc env funnames avoid match_expr - | GLetTuple(_,nal,_,b,e) -> + | GLetTuple(nal,_,b,e) -> begin let nal_as_glob_constr = List.map @@ -671,15 +673,13 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = in let case_pats = build_constructors_of_type (fst ind) nal_as_glob_constr in assert (Int.equal (Array.length case_pats) 1); - let br = - (Loc.ghost,[],[case_pats.(0)],e) - in + let br = Loc.tag ([],[case_pats.(0)],e) in let match_expr = mkGCases(None,[b,(Anonymous,None)],[br]) in build_entry_lc env funnames avoid match_expr end | GRec _ -> error "Not handled GRec" - | GCast(_,b,_) -> + | GCast(b,_) -> build_entry_lc env funnames avoid b and build_entry_lc_from_case env funname make_discr (el:tomatch_tuples) @@ -739,7 +739,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve | [] -> (* computed_branches *) {result = [];to_avoid = avoid} | br::brl' -> (* alpha conversion to prevent name clashes *) - let _,idl,patl,return = alpha_br avoid br in + let _,(idl,patl,return) = alpha_br avoid br in let new_avoid = idl@avoid in (* for now we can no more use idl as an identifier *) (* building a list of precondition stating that we are not in this branch (will be used in the following recursive calls) @@ -862,8 +862,8 @@ let is_res id = let same_raw_term rt1 rt2 = - match rt1,rt2 with - | GRef(_,r1,_), GRef (_,r2,_) -> Globnames.eq_gr r1 r2 + match CAst.(rt1.v, rt2.v) with + | GRef(r1,_), GRef (r2,_) -> Globnames.eq_gr r1 r2 | GHole _, GHole _ -> true | _ -> false let decompose_raw_eq lhs rhs = @@ -895,16 +895,17 @@ exception Continue let rec rebuild_cons env nb_args relname args crossed_types depth rt = observe (str "rebuilding : " ++ pr_glob_constr rt); let open Context.Rel.Declaration in - match rt with - | GProd(_,n,k,t,b) -> + let open CAst in + match rt.v with + | GProd(n,k,t,b) -> let not_free_in_t id = not (is_free_in id t) in let new_crossed_types = t::crossed_types in begin match t with - | GApp(_,(GVar(_,res_id) as res_rt),args') when is_res res_id -> + | { v = GApp(({ v = GVar res_id } as res_rt),args') } when is_res res_id -> begin match args' with - | (GVar(_,this_relname))::args' -> + | { v = GVar this_relname }::args' -> (*i The next call to mk_rel_id is valid since we are constructing the graph Ensures by: obvious @@ -926,7 +927,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = | _ -> (* the first args is the name of the function! *) assert false end - | GApp(loc1,GRef(loc2,eq_as_ref,_),[ty;GVar(loc3,id);rt]) + | { loc = loc1; v = GApp({ loc = loc2; v = GRef(eq_as_ref,_) },[ty; { loc = loc3; v = GVar id};rt]) } when Globnames.eq_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous -> begin @@ -963,9 +964,8 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let params,arg' = ((Util.List.chop nparam args')) in - let rt_typ = - GApp(Loc.ghost, - GRef (Loc.ghost,Globnames.IndRef (fst ind),None), + let rt_typ = CAst.make @@ + GApp(CAst.make @@ GRef (Globnames.IndRef (fst ind),None), (List.map (fun p -> Detyping.detype false [] env (Evd.from_env env) @@ -975,7 +975,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = (mkGHole ())))) in let eq' = - GApp(loc1,GRef(loc2,jmeq,None),[ty;GVar(loc3,id);rt_typ;rt]) + CAst.make ?loc:loc1 @@ GApp(CAst.make ?loc:loc2 @@GRef(jmeq,None),[ty;CAst.make ?loc:loc3 @@ GVar id;rt_typ;rt]) in observe (str "computing new type for jmeq : " ++ pr_glob_constr eq'); let eq'_as_constr,ctx = Pretyping.understand env (Evd.from_env env) eq' in @@ -1044,7 +1044,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = mkGProd(n,t,new_b),id_to_exclude else new_b, Id.Set.add id id_to_exclude *) - | GApp(loc1,GRef(loc2,eq_as_ref,_),[ty;rt1;rt2]) + | { loc = loc1; v = GApp({ loc = loc2; v = GRef(eq_as_ref,_) },[ty;rt1;rt2]) } when Globnames.eq_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous -> begin @@ -1095,7 +1095,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = (Id.Set.filter not_free_in_t id_to_exclude) | _ -> mkGProd(n,t,new_b),Id.Set.filter not_free_in_t id_to_exclude end - | GLambda(_,n,k,t,b) -> + | GLambda(n,k,t,b) -> begin let not_free_in_t id = not (is_free_in id t) in let new_crossed_types = t :: crossed_types in @@ -1114,14 +1114,14 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = then new_b, Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude) else - GProd(Loc.ghost,n,k,t,new_b),Id.Set.filter not_free_in_t id_to_exclude + CAst.make @@ GProd(n,k,t,new_b),Id.Set.filter not_free_in_t id_to_exclude | _ -> anomaly (Pp.str "Should not have an anonymous function here") (* We have renamed all the anonymous functions during alpha_renaming phase *) end - | GLetIn(loc,n,v,t,b) -> + | GLetIn(n,v,t,b) -> begin - let t = match t with None -> v | Some t -> GCast (loc,v,CastConv t) in + let t = match t with None -> v | Some t -> CAst.make ?loc:rt.loc @@ GCast (v,CastConv t) in let not_free_in_t id = not (is_free_in id t) in let evd = (Evd.from_env env) in let t',ctx = Pretyping.understand env evd t in @@ -1137,10 +1137,10 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = match n with | Name id when Id.Set.mem id id_to_exclude && depth >= nb_args -> new_b,Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude) - | _ -> GLetIn(Loc.ghost,n,t,None,new_b), (* HOPING IT WOULD WORK *) + | _ -> CAst.make @@ GLetIn(n,t,None,new_b), (* HOPING IT WOULD WORK *) Id.Set.filter not_free_in_t id_to_exclude end - | GLetTuple(_,nal,(na,rto),t,b) -> + | GLetTuple(nal,(na,rto),t,b) -> assert (Option.is_empty rto); begin let not_free_in_t id = not (is_free_in id t) in @@ -1163,7 +1163,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = (* | Name id when Id.Set.mem id id_to_exclude -> *) (* new_b,Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude) *) (* | _ -> *) - GLetTuple(Loc.ghost,nal,(na,None),t,new_b), + CAst.make @@ GLetTuple(nal,(na,None),t,new_b), Id.Set.filter not_free_in_t (Id.Set.union id_to_exclude id_to_exclude') end @@ -1189,16 +1189,16 @@ let rebuild_cons env nb_args relname args crossed_types rt = TODO: Find a valid way to deal with implicit arguments here! *) -let rec compute_cst_params relnames params = function +let rec compute_cst_params relnames params gt = CAst.with_val (function | GRef _ | GVar _ | GEvar _ | GPatVar _ -> params - | GApp(_,GVar(_,relname'),rtl) when Id.Set.mem relname' relnames -> + | GApp({ CAst.v = GVar relname' },rtl) when Id.Set.mem relname' relnames -> compute_cst_params_from_app [] (params,rtl) - | GApp(_,f,args) -> + | GApp(f,args) -> List.fold_left (compute_cst_params relnames) params (f::args) - | GLambda(_,_,_,t,b) | GProd(_,_,_,t,b) | GLetTuple(_,_,_,t,b) -> + | GLambda(_,_,t,b) | GProd(_,_,t,b) | GLetTuple(_,_,t,b) -> let t_params = compute_cst_params relnames params t in compute_cst_params relnames t_params b - | GLetIn(_,_,v,t,b) -> + | GLetIn(_,v,t,b) -> let v_params = compute_cst_params relnames params v in let t_params = Option.fold_left (compute_cst_params relnames) v_params t in compute_cst_params relnames t_params b @@ -1209,10 +1209,11 @@ let rec compute_cst_params relnames params = function | GHole _ -> params | GIf _ | GRec _ | GCast _ -> raise (UserError(Some "compute_cst_params", str "Not handled case")) + ) gt and compute_cst_params_from_app acc (params,rtl) = match params,rtl with | _::_,[] -> assert false (* the rel has at least nargs + 1 arguments ! *) - | ((Name id,_,None) as param)::params',(GVar(_,id'))::rtl' + | ((Name id,_,None) as param)::params', { CAst.v = GVar id' }::rtl' when Id.compare id id' == 0 -> compute_cst_params_from_app (param::acc) (params',rtl') | _ -> List.rev acc @@ -1248,15 +1249,15 @@ let compute_params_name relnames (args : (Name.t * Glob_term.glob_constr * glob_ List.rev !l let rec rebuild_return_type rt = - match rt with - | Constrexpr.CProdN(loc,n,t') -> - Constrexpr.CProdN(loc,n,rebuild_return_type t') - | Constrexpr.CLetIn(loc,na,v,t,t') -> - Constrexpr.CLetIn(loc,na,v,t,rebuild_return_type t') - | _ -> Constrexpr.CProdN(Loc.ghost,[[Loc.ghost,Anonymous], - Constrexpr.Default Decl_kinds.Explicit,rt], - Constrexpr.CSort(Loc.ghost,GType [])) - + let loc = rt.CAst.loc in + match rt.CAst.v with + | Constrexpr.CProdN(n,t') -> + 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([[Loc.tag Anonymous], + Constrexpr.Default Decl_kinds.Explicit, rt], + CAst.make @@ Constrexpr.CSort(GType [])) let do_build_inductive evd (funconstants: Term.pconstant list) (funsargs: (Name.t * glob_constr * glob_constr option) list list) @@ -1307,13 +1308,12 @@ let do_build_inductive (fun (n,t,typ) acc -> match typ with | Some typ -> - Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t, + CAst.make @@ Constrexpr.CLetIn((Loc.tag 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 -> - Constrexpr.CProdN - (Loc.ghost, - [[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t], + CAst.make @@ Constrexpr.CProdN + ([[(Loc.tag n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t], acc ) ) @@ -1375,13 +1375,12 @@ let do_build_inductive (fun (n,t,typ) acc -> match typ with | Some typ -> - Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t, + CAst.make @@ Constrexpr.CLetIn((Loc.tag 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 -> - Constrexpr.CProdN - (Loc.ghost, - [[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t], + CAst.make @@ Constrexpr.CProdN + ([[(Loc.tag n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t], acc ) ) @@ -1408,18 +1407,18 @@ let do_build_inductive (fun (n,t,typ) -> match typ with | Some typ -> - Constrexpr.CLocalDef((Loc.ghost,n), Constrextern.extern_glob_constr Id.Set.empty t, + Constrexpr.CLocalDef((Loc.tag 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.ghost,n)], Constrexpr_ops.default_binder_kind, Constrextern.extern_glob_constr Id.Set.empty t) + ([(Loc.tag 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.ghost,id), + false,((Loc.tag id), with_full_print (Constrextern.extern_glob_type Id.Set.empty) ((* zeta_normalize *) (alpha_rt rel_params_ids t)) ) @@ -1427,7 +1426,7 @@ let do_build_inductive (rel_constructors) in let rel_ind i ext_rel_constructors = - (((Loc.ghost,relnames.(i)), None), + (((Loc.tag @@ relnames.(i)), None), rel_params, Some rel_arities.(i), ext_rel_constructors),[] diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 99f50437b..5abcb100f 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -10,16 +10,16 @@ open Misctypes Some basic functions to rebuild glob_constr In each of them the location is Loc.ghost *) -let mkGRef ref = GRef(Loc.ghost,ref,None) -let mkGVar id = GVar(Loc.ghost,id) -let mkGApp(rt,rtl) = GApp(Loc.ghost,rt,rtl) -let mkGLambda(n,t,b) = GLambda(Loc.ghost,n,Explicit,t,b) -let mkGProd(n,t,b) = GProd(Loc.ghost,n,Explicit,t,b) -let mkGLetIn(n,b,t,c) = GLetIn(Loc.ghost,n,b,t,c) -let mkGCases(rto,l,brl) = GCases(Loc.ghost,Term.RegularStyle,rto,l,brl) -let mkGSort s = GSort(Loc.ghost,s) -let mkGHole () = GHole(Loc.ghost,Evar_kinds.BinderType Anonymous,Misctypes.IntroAnonymous,None) -let mkGCast(b,t) = GCast(Loc.ghost,b,CastConv t) +let mkGRef ref = CAst.make @@ GRef(ref,None) +let mkGVar id = CAst.make @@ GVar(id) +let mkGApp(rt,rtl) = CAst.make @@ GApp(rt,rtl) +let mkGLambda(n,t,b) = CAst.make @@ GLambda(n,Explicit,t,b) +let mkGProd(n,t,b) = CAst.make @@ GProd(n,Explicit,t,b) +let mkGLetIn(n,b,t,c) = CAst.make @@ GLetIn(n,b,t,c) +let mkGCases(rto,l,brl) = CAst.make @@ GCases(Term.RegularStyle,rto,l,brl) +let mkGSort s = CAst.make @@ GSort(s) +let mkGHole () = CAst.make @@ GHole(Evar_kinds.BinderType Anonymous,Misctypes.IntroAnonymous,None) +let mkGCast(b,t) = CAst.make @@ GCast(b,CastConv t) (* Some basic functions to decompose glob_constrs @@ -27,7 +27,7 @@ let mkGCast(b,t) = GCast(Loc.ghost,b,CastConv t) *) let glob_decompose_prod = let rec glob_decompose_prod args = function - | GProd(_,n,k,t,b) -> + | { CAst.v = GProd(n,k,t,b) } -> glob_decompose_prod ((n,t)::args) b | rt -> args,rt in @@ -35,9 +35,9 @@ let glob_decompose_prod = let glob_decompose_prod_or_letin = let rec glob_decompose_prod args = function - | GProd(_,n,k,t,b) -> + | { CAst.v = GProd(n,k,t,b) } -> glob_decompose_prod ((n,None,Some t)::args) b - | GLetIn(_,n,b,t,c) -> + | { CAst.v = GLetIn(n,b,t,c) } -> glob_decompose_prod ((n,Some b,t)::args) c | rt -> args,rt in @@ -59,7 +59,7 @@ let glob_decompose_prod_n n = if i<=0 then args,c else match c with - | GProd(_,n,_,t,b) -> + | { CAst.v = GProd(n,_,t,b) } -> glob_decompose_prod (i-1) ((n,t)::args) b | rt -> args,rt in @@ -71,9 +71,9 @@ let glob_decompose_prod_or_letin_n n = if i<=0 then args,c else match c with - | GProd(_,n,_,t,b) -> + | { CAst.v = GProd(n,_,t,b) } -> glob_decompose_prod (i-1) ((n,None,Some t)::args) b - | GLetIn(_,n,b,t,c) -> + | { CAst.v = GLetIn(n,b,t,c) } -> glob_decompose_prod (i-1) ((n,Some b,t)::args) c | rt -> args,rt in @@ -84,7 +84,7 @@ let glob_decompose_app = let rec decompose_rapp acc rt = (* msgnl (str "glob_decompose_app on : "++ Printer.pr_glob_constr rt); *) match rt with - | GApp(_,rt,rtl) -> + | { CAst.v = GApp(rt,rtl) } -> decompose_rapp (List.fold_left (fun y x -> x::y) acc rtl) rt | rt -> rt,List.rev acc in @@ -120,93 +120,89 @@ let remove_name_from_mapping mapping na = let change_vars = let rec change_vars mapping rt = - match rt with - | GRef _ -> rt - | GVar(loc,id) -> + CAst.map (function + | GRef _ as x -> x + | GVar id -> let new_id = try Id.Map.find id mapping with Not_found -> id in - GVar(loc,new_id) - | GEvar _ -> rt - | GPatVar _ -> rt - | GApp(loc,rt',rtl) -> - GApp(loc, - change_vars mapping rt', + GVar(new_id) + | GEvar _ as x -> x + | GPatVar _ as x -> x + | GApp(rt',rtl) -> + GApp(change_vars mapping rt', List.map (change_vars mapping) rtl ) - | GLambda(loc,name,k,t,b) -> - GLambda(loc, - name, + | GLambda(name,k,t,b) -> + GLambda(name, k, change_vars mapping t, change_vars (remove_name_from_mapping mapping name) b ) - | GProd(loc,name,k,t,b) -> - GProd(loc, - name, + | GProd(name,k,t,b) -> + GProd( name, k, change_vars mapping t, change_vars (remove_name_from_mapping mapping name) b ) - | GLetIn(loc,name,def,typ,b) -> - GLetIn(loc, - name, + | GLetIn(name,def,typ,b) -> + GLetIn(name, change_vars mapping def, Option.map (change_vars mapping) typ, change_vars (remove_name_from_mapping mapping name) b ) - | GLetTuple(loc,nal,(na,rto),b,e) -> + | GLetTuple(nal,(na,rto),b,e) -> let new_mapping = List.fold_left remove_name_from_mapping mapping nal in - GLetTuple(loc, - nal, + GLetTuple(nal, (na, Option.map (change_vars mapping) rto), change_vars mapping b, change_vars new_mapping e ) - | GCases(loc,sty,infos,el,brl) -> - GCases(loc,sty, + | GCases(sty,infos,el,brl) -> + GCases(sty, infos, List.map (fun (e,x) -> (change_vars mapping e,x)) el, List.map (change_vars_br mapping) brl ) - | GIf(loc,b,(na,e_option),lhs,rhs) -> - GIf(loc, - change_vars mapping b, + | GIf(b,(na,e_option),lhs,rhs) -> + GIf(change_vars mapping b, (na,Option.map (change_vars mapping) e_option), change_vars mapping lhs, change_vars mapping rhs ) | GRec _ -> error "Local (co)fixes are not supported" - | GSort _ -> rt - | GHole _ -> rt - | GCast(loc,b,c) -> - GCast(loc,change_vars mapping b, + | GSort _ as x -> x + | GHole _ as x -> x + | GCast(b,c) -> + GCast(change_vars mapping b, Miscops.map_cast_type (change_vars mapping) c) - and change_vars_br mapping ((loc,idl,patl,res) as br) = + ) rt + and change_vars_br mapping ((loc,(idl,patl,res)) as br) = let new_mapping = List.fold_right Id.Map.remove idl mapping in if Id.Map.is_empty new_mapping then br - else (loc,idl,patl,change_vars new_mapping res) + else (loc,(idl,patl,change_vars new_mapping res)) in change_vars let rec alpha_pat excluded pat = - match pat with - | PatVar(loc,Anonymous) -> + let loc = pat.CAst.loc in + match pat.CAst.v with + | PatVar Anonymous -> let new_id = Indfun_common.fresh_id excluded "_x" in - PatVar(loc,Name new_id),(new_id::excluded),Id.Map.empty - | PatVar(loc,Name id) -> + (CAst.make ?loc @@ PatVar(Name new_id)),(new_id::excluded),Id.Map.empty + | PatVar(Name id) -> if Id.List.mem id excluded then let new_id = Namegen.next_ident_away id excluded in - PatVar(loc,Name new_id),(new_id::excluded), + (CAst.make ?loc @@ PatVar(Name new_id)),(new_id::excluded), (Id.Map.add id new_id Id.Map.empty) - else pat,excluded,Id.Map.empty - | PatCstr(loc,constr,patl,na) -> + else pat, excluded,Id.Map.empty + | PatCstr(constr,patl,na) -> let new_na,new_excluded,map = match na with | Name id when Id.List.mem id excluded -> @@ -223,7 +219,7 @@ let rec alpha_pat excluded pat = ([],new_excluded,map) patl in - PatCstr(loc,constr,List.rev new_patl,new_na),new_excluded,new_map + (CAst.make ?loc @@ PatCstr(constr,List.rev new_patl,new_na)),new_excluded,new_map let alpha_patl excluded patl = let patl,new_excluded,map = @@ -242,11 +238,11 @@ let alpha_patl excluded patl = let raw_get_pattern_id pat acc = let rec get_pattern_id pat = - match pat with - | PatVar(loc,Anonymous) -> assert false - | PatVar(loc,Name id) -> + match pat.CAst.v with + | PatVar(Anonymous) -> assert false + | PatVar(Name id) -> [id] - | PatCstr(loc,constr,patternl,_) -> + | PatCstr(constr,patternl,_) -> List.fold_right (fun pat idl -> let idl' = get_pattern_id pat in @@ -260,29 +256,30 @@ let raw_get_pattern_id pat acc = let get_pattern_id pat = raw_get_pattern_id pat [] let rec alpha_rt excluded rt = - let new_rt = - match rt with - | GRef _ | GVar _ | GEvar _ | GPatVar _ -> rt - | GLambda(loc,Anonymous,k,t,b) -> + let loc = rt.CAst.loc in + let new_rt = CAst.make ?loc @@ + match rt.CAst.v with + | GRef _ | GVar _ | GEvar _ | GPatVar _ as rt -> rt + | GLambda(Anonymous,k,t,b) -> let new_id = Namegen.next_ident_away (Id.of_string "_x") excluded in let new_excluded = new_id :: excluded in let new_t = alpha_rt new_excluded t in let new_b = alpha_rt new_excluded b in - GLambda(loc,Name new_id,k,new_t,new_b) - | GProd(loc,Anonymous,k,t,b) -> + GLambda(Name new_id,k,new_t,new_b) + | GProd(Anonymous,k,t,b) -> let new_t = alpha_rt excluded t in let new_b = alpha_rt excluded b in - GProd(loc,Anonymous,k,new_t,new_b) - | GLetIn(loc,Anonymous,b,t,c) -> + GProd(Anonymous,k,new_t,new_b) + | GLetIn(Anonymous,b,t,c) -> let new_b = alpha_rt excluded b in let new_t = Option.map (alpha_rt excluded) t in let new_c = alpha_rt excluded c in - GLetIn(loc,Anonymous,new_b,new_t,new_c) - | GLambda(loc,Name id,k,t,b) -> + GLetIn(Anonymous,new_b,new_t,new_c) + | GLambda(Name id,k,t,b) -> let new_id = Namegen.next_ident_away id excluded in let t,b = if Id.equal new_id id - then t,b + then t, b else let replace = change_vars (Id.Map.add id new_id Id.Map.empty) in (t,replace b) @@ -290,8 +287,8 @@ let rec alpha_rt excluded rt = let new_excluded = new_id::excluded in let new_t = alpha_rt new_excluded t in let new_b = alpha_rt new_excluded b in - GLambda(loc,Name new_id,k,new_t,new_b) - | GProd(loc,Name id,k,t,b) -> + GLambda(Name new_id,k,new_t,new_b) + | GProd(Name id,k,t,b) -> let new_id = Namegen.next_ident_away id excluded in let new_excluded = new_id::excluded in let t,b = @@ -303,8 +300,8 @@ let rec alpha_rt excluded rt = in let new_t = alpha_rt new_excluded t in let new_b = alpha_rt new_excluded b in - GProd(loc,Name new_id,k,new_t,new_b) - | GLetIn(loc,Name id,b,t,c) -> + GProd(Name new_id,k,new_t,new_b) + | GLetIn(Name id,b,t,c) -> let new_id = Namegen.next_ident_away id excluded in let c = if Id.equal new_id id then c @@ -314,10 +311,9 @@ let rec alpha_rt excluded rt = let new_b = alpha_rt new_excluded b in let new_t = Option.map (alpha_rt new_excluded) t in let new_c = alpha_rt new_excluded c in - GLetIn(loc,Name new_id,new_b,new_t,new_c) - + GLetIn(Name new_id,new_b,new_t,new_c) - | GLetTuple(loc,nal,(na,rto),t,b) -> + | GLetTuple(nal,(na,rto),t,b) -> let rev_new_nal,new_excluded,mapping = List.fold_left (fun (nal,excluded,mapping) na -> @@ -344,92 +340,92 @@ let rec alpha_rt excluded rt = let new_t = alpha_rt new_excluded new_t in let new_b = alpha_rt new_excluded new_b in let new_rto = Option.map (alpha_rt new_excluded) new_rto in - GLetTuple(loc,new_nal,(na,new_rto),new_t,new_b) - | GCases(loc,sty,infos,el,brl) -> + GLetTuple(new_nal,(na,new_rto),new_t,new_b) + | GCases(sty,infos,el,brl) -> let new_el = List.map (function (rt,i) -> alpha_rt excluded rt, i) el in - GCases(loc,sty,infos,new_el,List.map (alpha_br excluded) brl) - | GIf(loc,b,(na,e_o),lhs,rhs) -> - GIf(loc,alpha_rt excluded b, + GCases(sty,infos,new_el,List.map (alpha_br excluded) brl) + | GIf(b,(na,e_o),lhs,rhs) -> + GIf(alpha_rt excluded b, (na,Option.map (alpha_rt excluded) e_o), alpha_rt excluded lhs, alpha_rt excluded rhs ) | GRec _ -> error "Not handled GRec" - | GSort _ -> rt - | GHole _ -> rt - | GCast (loc,b,c) -> - GCast(loc,alpha_rt excluded b, + | GSort _ + | GHole _ as rt -> rt + | GCast (b,c) -> + GCast(alpha_rt excluded b, Miscops.map_cast_type (alpha_rt excluded) c) - | GApp(loc,f,args) -> - GApp(loc, - alpha_rt excluded f, + | GApp(f,args) -> + GApp(alpha_rt excluded f, List.map (alpha_rt excluded) args ) in new_rt -and alpha_br excluded (loc,ids,patl,res) = +and alpha_br excluded (loc,(ids,patl,res)) = let new_patl,new_excluded,mapping = alpha_patl excluded patl in let new_ids = List.fold_right raw_get_pattern_id new_patl [] in let new_excluded = new_ids@excluded in let renamed_res = change_vars mapping res in let new_res = alpha_rt new_excluded renamed_res in - (loc,new_ids,new_patl,new_res) + (loc,(new_ids,new_patl,new_res)) (* [is_free_in id rt] checks if [id] is a free variable in [rt] *) let is_free_in id = - let rec is_free_in = function + let rec is_free_in x = CAst.with_loc_val (fun ?loc -> function | GRef _ -> false - | GVar(_,id') -> Id.compare id' id == 0 + | GVar id' -> Id.compare id' id == 0 | GEvar _ -> false | GPatVar _ -> false - | GApp(_,rt,rtl) -> List.exists is_free_in (rt::rtl) - | GLambda(_,n,_,t,b) | GProd(_,n,_,t,b) -> + | GApp(rt,rtl) -> List.exists is_free_in (rt::rtl) + | GLambda(n,_,t,b) | GProd(n,_,t,b) -> let check_in_b = match n with | Name id' -> not (Id.equal id' id) | _ -> true in is_free_in t || (check_in_b && is_free_in b) - | GLetIn(_,n,b,t,c) -> + | GLetIn(n,b,t,c) -> let check_in_c = match n with | Name id' -> not (Id.equal id' id) | _ -> true in is_free_in b || Option.cata is_free_in true t || (check_in_c && is_free_in c) - | GCases(_,_,_,el,brl) -> + | GCases(_,_,el,brl) -> (List.exists (fun (e,_) -> is_free_in e) el) || List.exists is_free_in_br brl - | GLetTuple(_,nal,_,b,t) -> + | GLetTuple(nal,_,b,t) -> let check_in_nal = not (List.exists (function Name id' -> Id.equal id' id | _ -> false) nal) in is_free_in t || (check_in_nal && is_free_in b) - | GIf(_,cond,_,br1,br2) -> + | GIf(cond,_,br1,br2) -> is_free_in cond || is_free_in br1 || is_free_in br2 | GRec _ -> raise (UserError(None,str "Not handled GRec")) | GSort _ -> false | GHole _ -> false - | GCast (_,b,(CastConv t|CastVM t|CastNative t)) -> is_free_in b || is_free_in t - | GCast (_,b,CastCoerce) -> is_free_in b - and is_free_in_br (_,ids,_,rt) = + | GCast (b,(CastConv t|CastVM t|CastNative t)) -> is_free_in b || is_free_in t + | GCast (b,CastCoerce) -> is_free_in b + ) x + and is_free_in_br (_,(ids,_,rt)) = (not (Id.List.mem id ids)) && is_free_in rt in is_free_in -let rec pattern_to_term = function - | PatVar(loc,Anonymous) -> assert false - | PatVar(loc,Name id) -> +let rec pattern_to_term pt = CAst.with_val (function + | PatVar Anonymous -> assert false + | PatVar(Name id) -> mkGVar id - | PatCstr(loc,constr,patternl,_) -> + | PatCstr(constr,patternl,_) -> let cst_narg = Inductiveops.constructor_nallargs_env (Global.env ()) @@ -448,78 +444,73 @@ let rec pattern_to_term = function mkGApp(mkGRef(Globnames.ConstructRef constr), implicit_args@patl_as_term ) - + ) pt let replace_var_by_term x_id term = - let rec replace_var_by_pattern rt = - match rt with - | GRef _ -> rt - | GVar(_,id) when Id.compare id x_id == 0 -> term - | GVar _ -> rt - | GEvar _ -> rt - | GPatVar _ -> rt - | GApp(loc,rt',rtl) -> - GApp(loc, - replace_var_by_pattern rt', + let rec replace_var_by_pattern x = CAst.map (function + | GVar id when Id.compare id x_id == 0 -> term.CAst.v + | GRef _ + | GVar _ + | GEvar _ + | GPatVar _ as rt -> rt + | GApp(rt',rtl) -> + GApp(replace_var_by_pattern rt', List.map replace_var_by_pattern rtl ) - | GLambda(_,Name id,_,_,_) when Id.compare id x_id == 0 -> rt - | GLambda(loc,name,k,t,b) -> - GLambda(loc, - name, + | GLambda(Name id,_,_,_) as rt when Id.compare id x_id == 0 -> rt + | GLambda(name,k,t,b) -> + GLambda(name, k, replace_var_by_pattern t, replace_var_by_pattern b ) - | GProd(_,Name id,_,_,_) when Id.compare id x_id == 0 -> rt - | GProd(loc,name,k,t,b) -> - GProd(loc, - name, + | GProd(Name id,_,_,_) as rt when Id.compare id x_id == 0 -> rt + | GProd(name,k,t,b) -> + GProd( name, k, replace_var_by_pattern t, replace_var_by_pattern b ) - | GLetIn(_,Name id,_,_,_) when Id.compare id x_id == 0 -> rt - | GLetIn(loc,name,def,typ,b) -> - GLetIn(loc, - name, + | GLetIn(Name id,_,_,_) as rt when Id.compare id x_id == 0 -> rt + | GLetIn(name,def,typ,b) -> + GLetIn(name, replace_var_by_pattern def, Option.map (replace_var_by_pattern) typ, replace_var_by_pattern b ) - | GLetTuple(_,nal,_,_,_) + | GLetTuple(nal,_,_,_) as rt when List.exists (function Name id -> Id.equal id x_id | _ -> false) nal -> rt - | GLetTuple(loc,nal,(na,rto),def,b) -> - GLetTuple(loc, - nal, + | GLetTuple(nal,(na,rto),def,b) -> + GLetTuple(nal, (na,Option.map replace_var_by_pattern rto), replace_var_by_pattern def, replace_var_by_pattern b ) - | GCases(loc,sty,infos,el,brl) -> - GCases(loc,sty, + | GCases(sty,infos,el,brl) -> + GCases(sty, infos, List.map (fun (e,x) -> (replace_var_by_pattern e,x)) el, List.map replace_var_by_pattern_br brl ) - | GIf(loc,b,(na,e_option),lhs,rhs) -> - GIf(loc, replace_var_by_pattern b, + | GIf(b,(na,e_option),lhs,rhs) -> + GIf(replace_var_by_pattern b, (na,Option.map replace_var_by_pattern e_option), replace_var_by_pattern lhs, replace_var_by_pattern rhs ) | GRec _ -> raise (UserError(None,str "Not handled GRec")) - | GSort _ -> rt - | GHole _ -> rt - | GCast(loc,b,c) -> - GCast(loc,replace_var_by_pattern b, + | GSort _ + | GHole _ as rt -> rt + | GCast(b,c) -> + GCast(replace_var_by_pattern b, Miscops.map_cast_type replace_var_by_pattern c) - and replace_var_by_pattern_br ((loc,idl,patl,res) as br) = + ) x + and replace_var_by_pattern_br ((loc,(idl,patl,res)) as br) = if List.exists (fun id -> Id.compare id x_id == 0) idl then br - else (loc,idl,patl,replace_var_by_pattern res) + else (loc,(idl,patl,replace_var_by_pattern res)) in replace_var_by_pattern @@ -532,9 +523,10 @@ exception NotUnifiable let rec are_unifiable_aux = function | [] -> () | eq::eqs -> + let open CAst in match eq with - | PatVar _,_ | _,PatVar _ -> are_unifiable_aux eqs - | PatCstr(_,constructor1,cpl1,_),PatCstr(_,constructor2,cpl2,_) -> + | { v = PatVar _ },_ | _, { v = PatVar _ } -> are_unifiable_aux eqs + | { v = PatCstr(constructor1,cpl1,_) }, { v = PatCstr(constructor2,cpl2,_) } -> if not (eq_constructor constructor2 constructor1) then raise NotUnifiable else @@ -554,9 +546,10 @@ let are_unifiable pat1 pat2 = let rec eq_cases_pattern_aux = function | [] -> () | eq::eqs -> + let open CAst in match eq with - | PatVar _,PatVar _ -> eq_cases_pattern_aux eqs - | PatCstr(_,constructor1,cpl1,_),PatCstr(_,constructor2,cpl2,_) -> + | { v = PatVar _ }, { v = PatVar _ } -> eq_cases_pattern_aux eqs + | { v = PatCstr(constructor1,cpl1,_) }, { v = PatCstr(constructor2,cpl2,_) } -> if not (eq_constructor constructor2 constructor1) then raise NotUnifiable else @@ -576,10 +569,11 @@ let eq_cases_pattern pat1 pat2 = let ids_of_pat = - let rec ids_of_pat ids = function - | PatVar(_,Anonymous) -> ids - | PatVar(_,Name id) -> Id.Set.add id ids - | PatCstr(_,_,patl,_) -> List.fold_left ids_of_pat ids patl + let rec ids_of_pat ids = CAst.with_val (function + | PatVar Anonymous -> ids + | PatVar(Name id) -> Id.Set.add id ids + | PatCstr(_,patl,_) -> List.fold_left ids_of_pat ids patl + ) in ids_of_pat Id.Set.empty @@ -589,22 +583,22 @@ let id_of_name = function (* TODO: finish Rec caes *) let ids_of_glob_constr c = - let rec ids_of_glob_constr acc c = + let rec ids_of_glob_constr acc {loc; CAst.v = c} = let idof = id_of_name in match c with - | GVar (_,id) -> id::acc - | GApp (loc,g,args) -> + | GVar id -> id::acc + | GApp (g,args) -> ids_of_glob_constr [] g @ List.flatten (List.map (ids_of_glob_constr []) args) @ acc - | GLambda (loc,na,k,ty,c) -> idof na :: ids_of_glob_constr [] ty @ ids_of_glob_constr [] c @ acc - | GProd (loc,na,k,ty,c) -> idof na :: ids_of_glob_constr [] ty @ ids_of_glob_constr [] c @ acc - | GLetIn (loc,na,b,t,c) -> idof na :: ids_of_glob_constr [] b @ Option.cata (ids_of_glob_constr []) [] t @ ids_of_glob_constr [] c @ acc - | GCast (loc,c,(CastConv t|CastVM t|CastNative t)) -> ids_of_glob_constr [] c @ ids_of_glob_constr [] t @ acc - | GCast (loc,c,CastCoerce) -> ids_of_glob_constr [] c @ acc - | GIf (loc,c,(na,po),b1,b2) -> ids_of_glob_constr [] c @ ids_of_glob_constr [] b1 @ ids_of_glob_constr [] b2 @ acc - | GLetTuple (_,nal,(na,po),b,c) -> + | GLambda (na,k,ty,c) -> idof na :: ids_of_glob_constr [] ty @ ids_of_glob_constr [] c @ acc + | GProd (na,k,ty,c) -> idof na :: ids_of_glob_constr [] ty @ ids_of_glob_constr [] c @ acc + | GLetIn (na,b,t,c) -> idof na :: ids_of_glob_constr [] b @ Option.cata (ids_of_glob_constr []) [] t @ ids_of_glob_constr [] c @ acc + | GCast (c,(CastConv t|CastVM t|CastNative t)) -> ids_of_glob_constr [] c @ ids_of_glob_constr [] t @ acc + | GCast (c,CastCoerce) -> ids_of_glob_constr [] c @ acc + | GIf (c,(na,po),b1,b2) -> ids_of_glob_constr [] c @ ids_of_glob_constr [] b1 @ ids_of_glob_constr [] b2 @ acc + | GLetTuple (nal,(na,po),b,c) -> List.map idof nal @ ids_of_glob_constr [] b @ ids_of_glob_constr [] c @ acc - | GCases (loc,sty,rtntypopt,tml,brchl) -> - List.flatten (List.map (fun (_,idl,patl,c) -> idl @ ids_of_glob_constr [] c) brchl) + | GCases (sty,rtntypopt,tml,brchl) -> + List.flatten (List.map (fun (_,(idl,patl,c)) -> idl @ ids_of_glob_constr [] c) brchl) | GRec _ -> failwith "Fix inside a constructor branch" | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> [] in @@ -616,61 +610,58 @@ let ids_of_glob_constr c = let zeta_normalize = - let rec zeta_normalize_term rt = - match rt with - | GRef _ -> rt - | GVar _ -> rt - | GEvar _ -> rt - | GPatVar _ -> rt - | GApp(loc,rt',rtl) -> - GApp(loc, - zeta_normalize_term rt', + let rec zeta_normalize_term x = CAst.map (function + | GRef _ + | GVar _ + | GEvar _ + | GPatVar _ as rt -> rt + | GApp(rt',rtl) -> + GApp(zeta_normalize_term rt', List.map zeta_normalize_term rtl ) - | GLambda(loc,name,k,t,b) -> - GLambda(loc, - name, + | GLambda(name,k,t,b) -> + GLambda(name, k, zeta_normalize_term t, zeta_normalize_term b ) - | GProd(loc,name,k,t,b) -> - GProd(loc, - name, + | GProd(name,k,t,b) -> + GProd(name, k, zeta_normalize_term t, zeta_normalize_term b ) - | GLetIn(_,Name id,def,typ,b) -> - zeta_normalize_term (replace_var_by_term id def b) - | GLetIn(loc,Anonymous,def,typ,b) -> zeta_normalize_term b - | GLetTuple(loc,nal,(na,rto),def,b) -> - GLetTuple(loc, - nal, + | GLetIn(Name id,def,typ,b) -> + (zeta_normalize_term (replace_var_by_term id def b)).CAst.v + | GLetIn(Anonymous,def,typ,b) -> + (zeta_normalize_term b).CAst.v + | GLetTuple(nal,(na,rto),def,b) -> + GLetTuple(nal, (na,Option.map zeta_normalize_term rto), zeta_normalize_term def, zeta_normalize_term b ) - | GCases(loc,sty,infos,el,brl) -> - GCases(loc,sty, + | GCases(sty,infos,el,brl) -> + GCases(sty, infos, List.map (fun (e,x) -> (zeta_normalize_term e,x)) el, List.map zeta_normalize_br brl ) - | GIf(loc,b,(na,e_option),lhs,rhs) -> - GIf(loc, zeta_normalize_term b, + | GIf(b,(na,e_option),lhs,rhs) -> + GIf(zeta_normalize_term b, (na,Option.map zeta_normalize_term e_option), zeta_normalize_term lhs, zeta_normalize_term rhs ) | GRec _ -> raise (UserError(None,str "Not handled GRec")) - | GSort _ -> rt - | GHole _ -> rt - | GCast(loc,b,c) -> - GCast(loc,zeta_normalize_term b, + | GSort _ + | GHole _ as rt -> rt + | GCast(b,c) -> + GCast(zeta_normalize_term b, Miscops.map_cast_type zeta_normalize_term c) - and zeta_normalize_br (loc,idl,patl,res) = - (loc,idl,patl,zeta_normalize_term res) + ) x + and zeta_normalize_br (loc,(idl,patl,res)) = + (loc,(idl,patl,zeta_normalize_term res)) in zeta_normalize_term @@ -679,40 +670,40 @@ let zeta_normalize = let expand_as = - let rec add_as map pat = + let rec add_as map ({loc; CAst.v = pat } as rt) = match pat with | PatVar _ -> map - | PatCstr(_,_,patl,Name id) -> - Id.Map.add id (pattern_to_term pat) (List.fold_left add_as map patl) - | PatCstr(_,_,patl,_) -> List.fold_left add_as map patl + | PatCstr(_,patl,Name id) -> + Id.Map.add id (pattern_to_term rt) (List.fold_left add_as map patl) + | PatCstr(_,patl,_) -> List.fold_left add_as map patl in - let rec expand_as map rt = - match rt with - | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> rt - | GVar(_,id) -> + let rec expand_as map = CAst.map (function + | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ as rt -> rt + | GVar id as rt -> begin try - Id.Map.find id map + (Id.Map.find id map).CAst.v with Not_found -> rt end - | GApp(loc,f,args) -> GApp(loc,expand_as map f,List.map (expand_as map) args) - | GLambda(loc,na,k,t,b) -> GLambda(loc,na,k,expand_as map t, expand_as map b) - | GProd(loc,na,k,t,b) -> GProd(loc,na,k,expand_as map t, expand_as map b) - | GLetIn(loc,na,v,typ,b) -> GLetIn(loc,na, expand_as map v,Option.map (expand_as map) typ,expand_as map b) - | GLetTuple(loc,nal,(na,po),v,b) -> - GLetTuple(loc,nal,(na,Option.map (expand_as map) po), + | GApp(f,args) -> GApp(expand_as map f,List.map (expand_as map) args) + | GLambda(na,k,t,b) -> GLambda(na,k,expand_as map t, expand_as map b) + | GProd(na,k,t,b) -> GProd(na,k,expand_as map t, expand_as map b) + | GLetIn(na,v,typ,b) -> GLetIn(na, expand_as map v,Option.map (expand_as map) typ,expand_as map b) + | GLetTuple(nal,(na,po),v,b) -> + GLetTuple(nal,(na,Option.map (expand_as map) po), expand_as map v, expand_as map b) - | GIf(loc,e,(na,po),br1,br2) -> - GIf(loc,expand_as map e,(na,Option.map (expand_as map) po), + | GIf(e,(na,po),br1,br2) -> + GIf(expand_as map e,(na,Option.map (expand_as map) po), expand_as map br1, expand_as map br2) | GRec _ -> error "Not handled GRec" - | GCast(loc,b,c) -> - GCast(loc,expand_as map b, + | GCast(b,c) -> + GCast(expand_as map b, Miscops.map_cast_type (expand_as map) c) - | GCases(loc,sty,po,el,brl) -> - GCases(loc, sty, Option.map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el, + | GCases(sty,po,el,brl) -> + GCases(sty, Option.map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el, List.map (expand_as_br map) brl) - and expand_as_br map (loc,idl,cpl,rt) = - (loc,idl,cpl, expand_as (List.fold_left add_as map cpl) rt) + ) + and expand_as_br map (loc,(idl,cpl,rt)) = + (loc,(idl,cpl, expand_as (List.fold_left add_as map cpl) rt)) in expand_as Id.Map.empty diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli index 84359a36b..25d79582f 100644 --- a/plugins/funind/glob_termops.mli +++ b/plugins/funind/glob_termops.mli @@ -82,11 +82,8 @@ val alpha_rt : Id.t list -> glob_constr -> glob_constr (* same as alpha_rt but for case branches *) val alpha_br : Id.t list -> - Loc.t * Id.t list * Glob_term.cases_pattern list * - Glob_term.glob_constr -> - Loc.t * Id.t list * Glob_term.cases_pattern list * - Glob_term.glob_constr - + Glob_term.cases_clause -> + Glob_term.cases_clause (* Reduction function *) val replace_var_by_term : diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index d335836df..ab83cb15a 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -156,7 +156,7 @@ let build_newrecursive let (rec_sign,rec_impls) = List.fold_left (fun (env,impls) (((_,recname),_),bl,arityc,_) -> - let arityc = Constrexpr_ops.mkCProdN Loc.ghost bl arityc in + let arityc = Constrexpr_ops.mkCProdN bl arityc in let arity,ctx = Constrintern.interp_type env0 sigma arityc in let evdref = ref (Evd.from_env env0) in let _, (_, impls') = Constrintern.interp_context_evars env evdref bl in @@ -190,18 +190,18 @@ let build_newrecursive l = let is_rec names = let names = List.fold_right Id.Set.add names Id.Set.empty in let check_id id names = Id.Set.mem id names in - let rec lookup names = function - | GVar(_,id) -> check_id id names + let rec lookup names gt = match gt.CAst.v with + | GVar(id) -> check_id id names | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> false - | GCast(_,b,_) -> lookup names b + | GCast(b,_) -> lookup names b | GRec _ -> error "GRec not handled" - | GIf(_,b,_,lhs,rhs) -> + | GIf(b,_,lhs,rhs) -> (lookup names b) || (lookup names lhs) || (lookup names rhs) - | GProd(_,na,_,t,b) | GLambda(_,na,_,t,b) -> + | GProd(na,_,t,b) | GLambda(na,_,t,b) -> lookup names t || lookup (Nameops.name_fold Id.Set.remove na names) b - | GLetIn(_,na,b,t,c) -> + | GLetIn(na,b,t,c) -> lookup names b || Option.cata (lookup names) true t || lookup (Nameops.name_fold Id.Set.remove na names) c - | GLetTuple(_,nal,_,t,b) -> lookup names t || + | GLetTuple(nal,_,t,b) -> lookup names t || lookup (List.fold_left (fun acc na -> Nameops.name_fold Id.Set.remove na acc) @@ -209,11 +209,11 @@ let is_rec names = nal ) b - | GApp(_,f,args) -> List.exists (lookup names) (f::args) - | GCases(_,_,_,el,brl) -> + | GApp(f,args) -> List.exists (lookup names) (f::args) + | GCases(_,_,el,brl) -> List.exists (fun (e,_) -> lookup names e) el || List.exists (lookup_br names) brl - and lookup_br names (_,idl,_,rt) = + and lookup_br names (_,(idl,_,rt)) = let new_names = List.fold_right Id.Set.remove idl names in lookup new_names rt in @@ -355,7 +355,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.ghost,mk_rel_id (List.nth names 0)) in + let f_R_mut = Ident (Loc.tag @@ 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!") @@ -453,7 +453,7 @@ let generate_correction_proof_wf f_ref tcc_lemma_ref let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas args ret_type body pre_hook = - let type_of_f = Constrexpr_ops.mkCProdN Loc.ghost args ret_type in + let type_of_f = Constrexpr_ops.mkCProdN args ret_type in let rec_arg_num = let names = List.map @@ -469,9 +469,8 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas in let unbounded_eq = let f_app_args = - Constrexpr.CAppExpl - (Loc.ghost, - (None,(Ident (Loc.ghost,fname)),None) , + CAst.make @@ Constrexpr.CAppExpl( + (None,(Ident (Loc.tag fname)),None) , (List.map (function | _,Anonymous -> assert false @@ -481,10 +480,10 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas ) ) in - Constrexpr.CApp (Loc.ghost,(None,Constrexpr_ops.mkRefC (Qualid (Loc.ghost,(qualid_of_string "Logic.eq")))), + CAst.make @@ Constrexpr.CApp ((None,Constrexpr_ops.mkRefC (Qualid (Loc.tag (qualid_of_string "Logic.eq")))), [(f_app_args,None);(body,None)]) in - let eq = Constrexpr_ops.mkCProdN Loc.ghost args unbounded_eq in + let eq = Constrexpr_ops.mkCProdN args unbounded_eq in let hook ((f_ref,_) as fconst) tcc_lemma_ref (functional_ref,_) (eq_ref,_) rec_arg_num rec_arg_type nb_args relation = try @@ -538,13 +537,13 @@ 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.ghost,Libnames.qualid_of_path + Libnames.Qualid (Loc.tag @@ Libnames.qualid_of_path (Libnames.make_path (make_dir ["Arith";"Wf_nat"]) (Id.of_string "ltof"))) in let fun_from_mes = let applied_mes = Constrexpr_ops.mkAppC(wf_mes_expr,[Constrexpr_ops.mkIdentC wf_arg]) in - Constrexpr_ops.mkLambdaC ([(Loc.ghost,Name wf_arg)],Constrexpr_ops.default_binder_kind,wf_arg_type,applied_mes) + Constrexpr_ops.mkLambdaC ([(Loc.tag @@ 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]) @@ -555,7 +554,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.ghost,Name a;Loc.ghost,Name b], + [Loc.tag @@ Name a;Loc.tag @@ Name b], Constrexpr.Default Explicit, wf_arg_type, Constrexpr_ops.mkAppC(wf_rel_expr, @@ -589,15 +588,15 @@ let rec rebuild_bl (aux,assoc) bl typ = | [], _ -> (List.rev aux,replace_vars_constr_expr assoc typ,assoc) | (Constrexpr.CLocalAssum(nal,bk,_))::bl',typ -> rebuild_nal (aux,assoc) bk bl' nal (List.length nal) typ - | (Constrexpr.CLocalDef(na,_,_))::bl',Constrexpr.CLetIn(_,_,nat,ty,typ') -> + | (Constrexpr.CLocalDef(na,_,_))::bl',{ CAst.v = Constrexpr.CLetIn(_,nat,ty,typ') } -> rebuild_bl ((Constrexpr.CLocalDef(na,replace_vars_constr_expr assoc nat,Option.map (replace_vars_constr_expr assoc) ty (* ??? *))::aux),assoc) bl' typ' | _ -> assert false and rebuild_nal (aux,assoc) bk bl' nal lnal typ = - match nal,typ with + match nal, typ.CAst.v with | [], _ -> rebuild_bl (aux,assoc) bl' typ - | _,CProdN(_,[],typ) -> rebuild_nal (aux,assoc) bk bl' nal lnal typ - | _,CProdN(_,(nal',bk',nal't)::rest,typ') -> + | _,CProdN([],typ) -> rebuild_nal (aux,assoc) bk bl' nal lnal typ + | _,CProdN((nal',bk',nal't)::rest,typ') -> let lnal' = List.length nal' in if lnal' >= lnal then @@ -607,15 +606,15 @@ let rec rebuild_bl (aux,assoc) bl typ = rebuild_bl ((assum :: aux), nassoc) bl' (if List.is_empty new_nal' && List.is_empty rest then typ' - else if List.is_empty new_nal' - then CProdN(Loc.ghost,rest,typ') - else CProdN(Loc.ghost,((new_nal',bk',nal't)::rest),typ')) + else CAst.make @@ if List.is_empty new_nal' + then CProdN(rest,typ') + else CProdN(((new_nal',bk',nal't)::rest),typ')) else let captured_nal,non_captured_nal = List.chop lnal' nal in let nassoc = make_assoc assoc nal' captured_nal in let assum = CLocalAssum(captured_nal,bk,replace_vars_constr_expr assoc nal't) in rebuild_nal ((assum :: aux), nassoc) - bk bl' non_captured_nal (lnal - lnal') (CProdN(Loc.ghost,rest,typ')) + bk bl' non_captured_nal (lnal - lnal') (CAst.make @@ CProdN(rest,typ')) | _ -> assert false let rebuild_bl (aux,assoc) bl typ = rebuild_bl (aux,assoc) bl typ @@ -726,67 +725,65 @@ let do_generate_principle pconstants on_error register_built interactive_proof in () -let rec add_args id new_args b = - match b with - | CRef (r,_) -> - begin match r with +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 -> - CAppExpl(Loc.ghost,(None,r,None),new_args) + CAppExpl((None,r,None),new_args) | _ -> b end | CFix _ | CCoFix _ -> anomaly ~label:"add_args " (Pp.str "todo") - | CProdN(loc,nal,b1) -> - CProdN(loc, - List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal, + | CProdN(nal,b1) -> + CProdN(List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal, add_args id new_args b1) - | CLambdaN(loc,nal,b1) -> - CLambdaN(loc, - List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal, + | CLambdaN(nal,b1) -> + CLambdaN(List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal, add_args id new_args b1) - | CLetIn(loc,na,b1,t,b2) -> - CLetIn(loc,na,add_args id new_args b1,Option.map (add_args id new_args) t,add_args id new_args b2) - | CAppExpl(loc,(pf,r,us),exprl) -> + | CLetIn(na,b1,t,b2) -> + CLetIn(na,add_args id new_args b1,Option.map (add_args id new_args) t,add_args id new_args b2) + | CAppExpl((pf,r,us),exprl) -> begin match r with | Libnames.Ident(loc,fname) when Id.equal fname id -> - CAppExpl(loc,(pf,r,us),new_args@(List.map (add_args id new_args) exprl)) - | _ -> CAppExpl(loc,(pf,r,us),List.map (add_args id new_args) exprl) + 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 - | CApp(loc,(pf,b),bl) -> - CApp(loc,(pf,add_args id new_args b), + | CApp((pf,b),bl) -> + CApp((pf,add_args id new_args b), List.map (fun (e,o) -> add_args id new_args e,o) bl) - | CCases(loc,sty,b_option,cel,cal) -> - CCases(loc,sty,Option.map (add_args id new_args) b_option, + | CCases(sty,b_option,cel,cal) -> + CCases(sty,Option.map (add_args id new_args) b_option, List.map (fun (b,na,b_option) -> add_args id new_args b, na, b_option) cel, - List.map (fun (loc,cpl,e) -> (loc,cpl,add_args id new_args e)) cal + List.map (fun (loc,(cpl,e)) -> Loc.tag ?loc @@ (cpl,add_args id new_args e)) cal ) - | CLetTuple(loc,nal,(na,b_option),b1,b2) -> - CLetTuple(loc,nal,(na,Option.map (add_args id new_args) b_option), + | CLetTuple(nal,(na,b_option),b1,b2) -> + CLetTuple(nal,(na,Option.map (add_args id new_args) b_option), add_args id new_args b1, add_args id new_args b2 ) - | CIf(loc,b1,(na,b_option),b2,b3) -> - CIf(loc,add_args id new_args b1, + | CIf(b1,(na,b_option),b2,b3) -> + CIf(add_args id new_args b1, (na,Option.map (add_args id new_args) b_option), add_args id new_args b2, add_args id new_args b3 ) - | CHole _ -> b - | CPatVar _ -> b - | CEvar _ -> b - | CSort _ -> b - | CCast(loc,b1,b2) -> - CCast(loc,add_args id new_args b1, + | CHole _ + | CPatVar _ + | CEvar _ + | CPrim _ + | CSort _ as b -> b + | CCast(b1,b2) -> + CCast(add_args id new_args b1, Miscops.map_cast_type (add_args id new_args) b2) - | CRecord (loc, pars) -> - CRecord (loc, List.map (fun (e,o) -> e, add_args id new_args o) pars) + | CRecord pars -> + CRecord (List.map (fun (e,o) -> e, add_args id new_args o) pars) | CNotation _ -> anomaly ~label:"add_args " (Pp.str "CNotation") | CGeneralization _ -> anomaly ~label:"add_args " (Pp.str "CGeneralization") - | CPrim _ -> b | CDelimiters _ -> anomaly ~label:"add_args " (Pp.str "CDelimiters") + ) exception Stop of Constrexpr.constr_expr @@ -797,8 +794,8 @@ let rec chop_n_arrow n t = if n <= 0 then t (* If we have already removed all the arrows then return the type *) else (* If not we check the form of [t] *) - match t with - | Constrexpr.CProdN(_,nal_ta',t') -> (* If we have a forall, to result are possible : + match t.CAst.v with + | Constrexpr.CProdN(nal_ta',t') -> (* If we have a forall, to result are possible : either we need to discard more than the number of arrows contained in this product declaration then we just recall [chop_n_arrow] on the remaining number of arrow to chop and [t'] we discard it and @@ -816,8 +813,8 @@ let rec chop_n_arrow n t = then aux (n - nal_l) nal_ta' else - let new_t' = - Constrexpr.CProdN(Loc.ghost, + let new_t' = CAst.make @@ + Constrexpr.CProdN( ((snd (List.chop n nal)),k,t'')::nal_ta',t') in raise (Stop new_t') @@ -832,8 +829,8 @@ let rec chop_n_arrow n t = let rec get_args b t : Constrexpr.local_binder_expr list * Constrexpr.constr_expr * Constrexpr.constr_expr = - match b with - | Constrexpr.CLambdaN (loc, (nal_ta), b') -> + match b.CAst.v with + | Constrexpr.CLambdaN ((nal_ta), b') -> begin let n = (List.fold_left (fun n (nal,_,_) -> @@ -872,8 +869,8 @@ let make_graph (f_ref:global_reference) = in let (nal_tas,b,t) = get_args extern_body extern_type in let expr_list = - match b with - | Constrexpr.CFix(loc,l_id,fixexprl) -> + match b.CAst.v with + | Constrexpr.CFix(l_id,fixexprl) -> let l = List.map (fun (id,(n,recexp),bl,t,b) -> @@ -885,7 +882,7 @@ let make_graph (f_ref:global_reference) = | Constrexpr.CLocalDef (na,_,_)-> [] | Constrexpr.CLocalAssum (nal,_,_) -> List.map - (fun (loc,n) -> + (fun (loc,n) -> CAst.make ?loc @@ CRef(Libnames.Ident(loc, Nameops.out_name n),None)) nal | Constrexpr.CLocalPattern _ -> assert false @@ -894,14 +891,14 @@ let make_graph (f_ref:global_reference) = ) in let b' = add_args (snd id) new_args b in - ((((id,None), ( Some (Loc.ghost,rec_id),CStructRec),nal_tas@bl,t,Some b'),[]):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list)) + ((((id,None), ( Some (Loc.tag rec_id),CStructRec),nal_tas@bl,t,Some b'),[]):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list)) ) fixexprl in l | _ -> let id = Label.to_id (con_label c) in - [(((Loc.ghost,id),None),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]] + [(((Loc.tag id),None),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]] in let mp,dp,_ = repr_con c in do_generate_principle [c,Univ.Instance.empty] error_error false false expr_list; diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 1c1e6843a..ea985ddec 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -66,9 +66,9 @@ let chop_rlambda_n = if n == 0 then List.rev acc,rt else - match rt with - | Glob_term.GLambda(_,name,k,t,b) -> chop_lambda_n ((name,t,None)::acc) (n-1) b - | Glob_term.GLetIn(_,name,v,t,b) -> chop_lambda_n ((name,v,t)::acc) (n-1) b + match rt.CAst.v with + | Glob_term.GLambda(name,k,t,b) -> chop_lambda_n ((name,t,None)::acc) (n-1) b + | Glob_term.GLetIn(name,v,t,b) -> chop_lambda_n ((name,v,t)::acc) (n-1) b | _ -> raise (CErrors.UserError(Some "chop_rlambda_n", str "chop_rlambda_n: Not enough Lambdas")) @@ -80,8 +80,8 @@ let chop_rprod_n = if n == 0 then List.rev acc,rt else - match rt with - | Glob_term.GProd(_,name,k,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b + match rt.CAst.v with + | Glob_term.GProd(name,k,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b | _ -> raise (CErrors.UserError(Some "chop_rprod_n",str "chop_rprod_n: Not enough products")) in chop_prod_n [] @@ -103,7 +103,7 @@ let list_add_set_eq eq_fun x l = let const_of_id id = let _,princ_ref = - qualid_of_reference (Libnames.Ident (Loc.ghost,id)) + qualid_of_reference (Libnames.Ident (Loc.tag id)) in try Constrintern.locate_reference princ_ref with Not_found -> diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 6c0c28905..8c972cd7c 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -30,8 +30,8 @@ module RelDecl = Context.Rel.Declaration let pr_binding prc = function - | loc, NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ Pp.cut () ++ prc c) - | loc, AnonHyp n, c -> hov 1 (int n ++ str " := " ++ Pp.cut () ++ prc c) + | loc, (NamedHyp id, c) -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ Pp.cut () ++ prc c) + | loc, (AnonHyp n, c) -> hov 1 (int n ++ str " := " ++ Pp.cut () ++ prc c) let pr_bindings prc prlc = function | ImplicitBindings l -> @@ -273,7 +273,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes List.map (fun decl -> List.map - (fun id -> Loc.ghost, IntroNaming (IntroIdentifier id)) + (fun id -> Loc.tag @@ IntroNaming (IntroIdentifier id)) (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum evd (RelDecl.get_type decl))))) ) branches diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 0af0898a0..b99a05dfb 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -65,14 +65,14 @@ let string_of_name = id_of_name %> Id.to_string (** [isVarf f x] returns [true] if term [x] is of the form [(Var f)]. *) let isVarf f x = match x with - | GVar (_,x) -> Id.equal x f + | { CAst.v = GVar x } -> Id.equal x f | _ -> false (** [ident_global_exist id] returns true if identifier [id] is linked in global environment. *) let ident_global_exist id = try - let ans = CRef (Libnames.Ident (Loc.ghost,id), None) in + let ans = CAst.make @@ CRef (Libnames.Ident (Loc.tag id), None) in let _ = ignore (Constrintern.intern_constr (Global.env()) ans) in true with e when CErrors.noncritical e -> false @@ -505,38 +505,38 @@ exception NoMerge let rec merge_app c1 c2 id1 id2 shift filter_shift_stable = let lnk = Array.append shift.lnk1 shift.lnk2 in - match c1 , c2 with - | GApp(_,f1, arr1), GApp(_,f2,arr2) when isVarf id1 f1 && isVarf id2 f2 -> + match CAst.(c1.v, c2.v) with + | GApp(f1, arr1), GApp(f2,arr2) when isVarf id1 f1 && isVarf id2 f2 -> let _ = prstr "\nICI1!\n" in let args = filter_shift_stable lnk (arr1 @ arr2) in - GApp (Loc.ghost,GVar (Loc.ghost,shift.ident) , args) - | GApp(_,f1, arr1), GApp(_,f2,arr2) -> raise NoMerge - | GLetIn(_,nme,bdy,typ,trm) , _ -> + CAst.make @@ GApp ((CAst.make @@ GVar shift.ident) , args) + | GApp(f1, arr1), GApp(f2,arr2) -> raise NoMerge + | GLetIn(nme,bdy,typ,trm) , _ -> let _ = prstr "\nICI2!\n" in let newtrm = merge_app trm c2 id1 id2 shift filter_shift_stable in - GLetIn(Loc.ghost,nme,bdy,typ,newtrm) - | _, GLetIn(_,nme,bdy,typ,trm) -> + CAst.make @@ GLetIn(nme,bdy,typ,newtrm) + | _, GLetIn(nme,bdy,typ,trm) -> let _ = prstr "\nICI3!\n" in let newtrm = merge_app c1 trm id1 id2 shift filter_shift_stable in - GLetIn(Loc.ghost,nme,bdy,typ,newtrm) + CAst.make @@ GLetIn(nme,bdy,typ,newtrm) | _ -> let _ = prstr "\nICI4!\n" in raise NoMerge let rec merge_app_unsafe c1 c2 shift filter_shift_stable = let lnk = Array.append shift.lnk1 shift.lnk2 in - match c1 , c2 with - | GApp(_,f1, arr1), GApp(_,f2,arr2) -> + match CAst.(c1.v, c2.v) with + | GApp(f1, arr1), GApp(f2,arr2) -> let args = filter_shift_stable lnk (arr1 @ arr2) in - GApp (Loc.ghost,GVar(Loc.ghost,shift.ident) , args) + CAst.make @@ GApp (CAst.make @@ GVar shift.ident, args) (* FIXME: what if the function appears in the body of the let? *) - | GLetIn(_,nme,bdy,typ,trm) , _ -> + | GLetIn(nme,bdy,typ,trm) , _ -> let _ = prstr "\nICI2 '!\n" in let newtrm = merge_app_unsafe trm c2 shift filter_shift_stable in - GLetIn(Loc.ghost,nme,bdy,typ,newtrm) - | _, GLetIn(_,nme,bdy,typ,trm) -> + CAst.make @@ GLetIn(nme,bdy,typ,newtrm) + | _, GLetIn(nme,bdy,typ,trm) -> let _ = prstr "\nICI3 '!\n" in let newtrm = merge_app_unsafe c1 trm shift filter_shift_stable in - GLetIn(Loc.ghost,nme,bdy,typ,newtrm) + CAst.make @@ GLetIn(nme,bdy,typ,newtrm) | _ -> let _ = prstr "\nICI4 '!\n" in raise NoMerge @@ -549,14 +549,14 @@ let rec merge_rec_hyps shift accrec filter_shift_stable : (Name.t * glob_constr option * glob_constr option) list = let mergeonehyp t reldecl = match reldecl with - | (nme,x,Some (GApp(_,i,args) as ind)) + | (nme,x,Some ({ CAst.v = GApp(i,args)} as ind)) -> nme,x, Some (merge_app_unsafe ind t shift filter_shift_stable) | (nme,Some _,None) -> error "letins with recursive calls not treated yet" | (nme,None,Some _) -> assert false | (nme,None,None) | (nme,Some _,Some _) -> assert false in match ltyp with | [] -> [] - | (nme,None,Some (GApp(_,f, largs) as t)) :: lt when isVarf ind2name f -> + | (nme,None,Some ({ CAst. v = GApp(f, largs) } as t)) :: lt when isVarf ind2name f -> let rechyps = List.map (mergeonehyp t) accrec in rechyps @ merge_rec_hyps shift accrec lt filter_shift_stable | e::lt -> e :: merge_rec_hyps shift accrec lt filter_shift_stable @@ -572,7 +572,7 @@ let find_app (nme:Id.t) ltyp = (List.map (fun x -> match x with - | _,None,Some (GApp(_,f,_)) when isVarf nme f -> raise (Found 0) + | _,None,Some { CAst.v = GApp(f,_)} when isVarf nme f -> raise (Found 0) | _ -> ()) ltyp); false @@ -631,8 +631,8 @@ let rec merge_types shift accrec1 rechyps , concl | (nme,None, Some t1)as e ::lt1 -> - (match t1 with - | GApp(_,f,carr) when isVarf ind1name f -> + (match t1.CAst.v with + | GApp(f,carr) when isVarf ind1name f -> merge_types shift (e::accrec1) lt1 concl1 ltyp2 concl2 | _ -> let recres, recconcl2 = @@ -824,7 +824,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) = let _ = prNamedRConstr (string_of_name nme) tp in let _ = prstr " ; " in let typ = glob_constr_to_constr_expr tp in - CLocalAssum ([(Loc.ghost,nme)], Constrexpr_ops.default_binder_kind, typ) :: acc) + CLocalAssum ([(Loc.tag nme)], Constrexpr_ops.default_binder_kind, typ) :: acc) [] params in let concl = Constrextern.extern_constr false (Global.env()) Evd.empty concl in let arity,_ = @@ -834,7 +834,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) = let c = RelDecl.get_type decl in let typ = Constrextern.extern_constr false env Evd.empty c in let newenv = Environ.push_rel (LocalAssum (nm,c)) env in - CProdN (Loc.ghost, [[(Loc.ghost,nm)],Constrexpr_ops.default_binder_kind,typ] , acc) , newenv) + CAst.make @@ CProdN ([[(Loc.tag nm)],Constrexpr_ops.default_binder_kind,typ] , acc) , newenv) (concl,Global.env()) (shift.funresprms2 @ shift.funresprms1 @ shift.args2 @ shift.args1 @ shift.otherprms2 @ shift.otherprms1) in @@ -848,12 +848,12 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) = FIXME: params et cstr_expr (arity) *) let glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift (rawlist:(Id.t * glob_constr) list) = - let lident = (Loc.ghost, shift.ident), None in + let lident = (Loc.tag shift.ident), None in let bindlist , cstr_expr = (* params , arities *) merge_rec_params_and_arity prms1 prms2 shift mkSet in let lcstor_expr : (bool * (lident * constr_expr)) list = List.map (* zeta_normalize t ? *) - (fun (id,t) -> false, ((Loc.ghost,id),glob_constr_to_constr_expr t)) + (fun (id,t) -> false, ((Loc.tag id),glob_constr_to_constr_expr t)) rawlist in lident , bindlist , Some cstr_expr , lcstor_expr @@ -863,7 +863,7 @@ let mkProd_reldecl (rdecl:Context.Rel.Declaration.t) (t2:glob_constr) = | LocalAssum (nme,t) -> let t = EConstr.of_constr t in let traw = Detyping.detype false [] (Global.env()) Evd.empty t in - GProd (Loc.ghost,nme,Explicit,traw,t2) + CAst.make @@ GProd (nme,Explicit,traw,t2) | LocalDef _ -> assert false @@ -901,7 +901,7 @@ let merge_inductive (ind1: inductive) (ind2: inductive) (* Find infos on identifier id. *) let find_Function_infos_safe (id:Id.t): Indfun_common.function_info = let kn_of_id x = - let f_ref = Libnames.Ident (Loc.ghost,x) in + let f_ref = Libnames.Ident (Loc.tag x) in locate_with_msg (str "Don't know what to do with " ++ Libnames.pr_reference f_ref) locate_constant f_ref in try find_Function_infos (kn_of_id id) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index bd30f1159..c46309355 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -172,7 +172,6 @@ let simpl_iter clause = let (value_f:Constr.constr list -> global_reference -> Constr.constr) = let open Term in fun al fterm -> - let d0 = Loc.ghost in let rev_x_id_l = ( List.fold_left @@ -189,16 +188,15 @@ let (value_f:Constr.constr list -> global_reference -> Constr.constr) = in let env = Environ.push_rel_context context (Global.env ()) in let glob_body = - GCases - (d0,RegularStyle,None, - [GApp(d0, GRef(d0,fterm,None), List.rev_map (fun x_id -> GVar(d0, x_id)) rev_x_id_l), + CAst.make @@ + GCases + (RegularStyle,None, + [CAst.make @@ GApp(CAst.make @@ GRef(fterm,None), List.rev_map (fun x_id -> CAst.make @@ GVar x_id) rev_x_id_l), (Anonymous,None)], - [d0, [v_id], [PatCstr(d0,(destIndRef - (delayed_force coq_sig_ref),1), - [PatVar(d0, Name v_id); - PatVar(d0, Anonymous)], - Anonymous)], - GVar(d0,v_id)]) + [Loc.tag ([v_id], [CAst.make @@ PatCstr ((destIndRef (delayed_force coq_sig_ref),1), + [CAst.make @@ PatVar(Name v_id); CAst.make @@ PatVar Anonymous], + Anonymous)], + CAst.make @@ GVar v_id)]) in let body = fst (understand env (Evd.from_env env) glob_body)(*FIXME*) in it_mkLambda_or_LetIn body context @@ -884,9 +882,8 @@ let rec make_rewrite_list expr_info max = function Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences true (* dep proofs also: *) true (mkVar hp, - ExplicitBindings[Loc.ghost,NamedHyp def, - expr_info.f_constr;Loc.ghost,NamedHyp k, - f_S max]) false) g) ) + ExplicitBindings[Loc.tag @@ (NamedHyp def, expr_info.f_constr); + Loc.tag @@ (NamedHyp k, f_S max)]) false) g) ) ) [make_rewrite_list expr_info max l; observe_tclTHENLIST (str "make_rewrite_list")[ (* x < S max proof *) @@ -912,9 +909,8 @@ let make_rewrite expr_info l hp max = (Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences true (* dep proofs also: *) true (mkVar hp, - ExplicitBindings[Loc.ghost,NamedHyp def, - expr_info.f_constr;Loc.ghost,NamedHyp k, - f_S (f_S max)]) false)) g) + ExplicitBindings[Loc.tag @@ (NamedHyp def, expr_info.f_constr); + Loc.tag @@ (NamedHyp k, f_S (f_S max))]) false)) g) [observe_tac(str "make_rewrite finalize") ( (* tclORELSE( h_reflexivity) *) (observe_tclTHENLIST (str "make_rewrite")[ @@ -1311,7 +1307,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp CErrors.error "\"abstract\" cannot handle existentials"; let hook _ _ = let opacity = - let na_ref = Libnames.Ident (Loc.ghost,na) in + let na_ref = Libnames.Ident (Loc.tag na) in let na_global = Smartlocate.global_with_alias na_ref in match na_global with ConstRef c -> is_opaque_constant c @@ -1561,7 +1557,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.ghost,term_id)] in + let _ = Extraction_plugin.Table.extraction_inline true [Ident (Loc.tag 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); diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4 index 28ff6df83..6890b3198 100644 --- a/plugins/ltac/coretactics.ml4 +++ b/plugins/ltac/coretactics.ml4 @@ -305,10 +305,9 @@ END open Tacexpr let initial_atomic () = - let dloc = Loc.ghost in let nocl = {onhyps=Some[];concl_occs=AllOccurrences} in let iter (s, t) = - let body = TacAtom (dloc, t) in + let body = TacAtom (Loc.tag t) in Tacenv.register_ltac false false (Id.of_string s) body in let () = List.iter iter @@ -323,7 +322,7 @@ let initial_atomic () = List.iter iter [ "idtac",TacId []; "fail", TacFail(TacLocal,ArgArg 0,[]); - "fresh", TacArg(dloc,TacFreshId []) + "fresh", TacArg(Loc.tag @@ TacFreshId []) ] let () = Mltop.declare_cache_obj initial_atomic "coretactics" diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml index bc9c300e2..470a93f2b 100644 --- a/plugins/ltac/evar_tactics.ml +++ b/plugins/ltac/evar_tactics.ml @@ -81,7 +81,7 @@ let instantiate_tac_by_name id c = end let let_evar name typ = - let src = (Loc.ghost,Evar_kinds.GoalEvar) in + let src = (Loc.tag Evar_kinds.GoalEvar) in Proofview.Goal.s_enter { s_enter = begin fun gl -> let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4 index ec3a49df4..a3310c2d8 100644 --- a/plugins/ltac/extraargs.ml4 +++ b/plugins/ltac/extraargs.ml4 @@ -228,11 +228,11 @@ ARGUMENT EXTEND hloc | [ "in" "|-" "*" ] -> [ ConclLocation () ] | [ "in" ident(id) ] -> - [ HypLocation ((Loc.ghost,id),InHyp) ] + [ HypLocation ((Loc.tag id),InHyp) ] | [ "in" "(" "Type" "of" ident(id) ")" ] -> - [ HypLocation ((Loc.ghost,id),InHypTypeOnly) ] + [ HypLocation ((Loc.tag id),InHypTypeOnly) ] | [ "in" "(" "Value" "of" ident(id) ")" ] -> - [ HypLocation ((Loc.ghost,id),InHypValueOnly) ] + [ HypLocation ((Loc.tag id),InHypValueOnly) ] END diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index bd48614db..cbd8a7f0f 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -73,7 +73,7 @@ END let induction_arg_of_quantified_hyp = function | AnonHyp n -> None,ElimOnAnonHyp n - | NamedHyp id -> None,ElimOnIdent (Loc.ghost,id) + | NamedHyp id -> None,ElimOnIdent (Loc.tag 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 @@ -264,7 +264,7 @@ let add_rewrite_hint bases ort t lcsr = (Declare.declare_universe_context false ctx; Univ.ContextSet.empty) in - Constrexpr_ops.constr_loc ce, (c, ctx), ort, Option.map (in_gen (rawwit wit_ltac)) t in + Loc.tag ?loc:(Constrexpr_ops.constr_loc ce) ((c, ctx), ort, Option.map (in_gen (rawwit wit_ltac)) t) in let eqs = List.map f lcsr in let add_hints base = add_rew_rules base eqs in List.iter add_hints bases @@ -628,15 +628,15 @@ let subst_var_with_hole occ tid t = let occref = if occ > 0 then ref occ else Find_subterm.error_invalid_occurrence [occ] in let locref = ref 0 in let rec substrec = function - | GVar (_,id) as x -> + | { CAst.v = GVar id } as x -> if Id.equal id tid then (decr occref; if Int.equal !occref 0 then x else (incr locref; - GHole (Loc.make_loc (!locref,0), - Evar_kinds.QuestionMark(Evar_kinds.Define true), + CAst.make ~loc:(Loc.make_loc (!locref,0)) @@ + GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true), Misctypes.IntroAnonymous, None))) else x | c -> map_glob_constr_left_to_right substrec c in @@ -648,13 +648,13 @@ let subst_hole_with_term occ tc t = let locref = ref 0 in let occref = ref occ in let rec substrec = function - | GHole (_,Evar_kinds.QuestionMark(Evar_kinds.Define true),Misctypes.IntroAnonymous,s) -> + | { CAst.v = GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true),Misctypes.IntroAnonymous,s) } -> decr occref; if Int.equal !occref 0 then tc else (incr locref; - GHole (Loc.make_loc (!locref,0), - Evar_kinds.QuestionMark(Evar_kinds.Define true),Misctypes.IntroAnonymous,s)) + CAst.make ~loc:(Loc.make_loc (!locref,0)) @@ + GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true),Misctypes.IntroAnonymous,s)) | c -> map_glob_constr_left_to_right substrec c in substrec t @@ -676,8 +676,8 @@ let hResolve id c occ t = with | Pretype_errors.PretypeError (_,_,Pretype_errors.UnsolvableImplicit _) as e -> let (e, info) = CErrors.push e in - let loc = match Loc.get_loc info with None -> Loc.ghost | Some loc -> loc in - resolve_hole (subst_hole_with_term (fst (Loc.unloc loc)) c_raw t_hole) + let loc_begin = Option.cata (fun l -> fst (Loc.unloc l)) 0 (Loc.get_loc info) in + resolve_hole (subst_hole_with_term loc_begin c_raw t_hole) in let t_constr,ctx = resolve_hole (subst_var_with_hole occ id t_raw) in let t_constr = EConstr.of_constr t_constr in @@ -781,7 +781,7 @@ let case_eq_intros_rewrite x = let rec find_a_destructable_match sigma t = let cl = induction_arg_of_quantified_hyp (NamedHyp (Id.of_string "x")) in let cl = [cl, (None, None), None], None in - let dest = TacAtom (Loc.ghost, TacInductionDestruct(false, false, cl)) in + let dest = TacAtom (Loc.tag @@ TacInductionDestruct(false, false, cl)) in match EConstr.kind sigma t with | Case (_,_,x,_) when closed0 sigma x -> if isVar sigma x then diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index 31fcf6c96..36ac10bfe 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -41,7 +41,7 @@ let in_tac tac = in_gen (rawwit Tacarg.wit_ltac) tac let reference_to_id = function | Libnames.Ident (loc, id) -> (loc, id) | Libnames.Qualid (loc,_) -> - CErrors.user_err ~loc + CErrors.user_err ?loc (str "This expression should be a simple identifier.") let tactic_mode = Gram.entry_create "vernac:tactic_command" @@ -159,9 +159,9 @@ GEXTEND Gram | g=failkw; n = [ n = int_or_var -> n | -> fail_default_value ]; l = LIST0 message_token -> TacFail (g,n,l) | st = simple_tactic -> st - | a = tactic_arg -> TacArg(!@loc,a) + | a = tactic_arg -> TacArg(Loc.tag ~loc:!@loc a) | r = reference; la = LIST0 tactic_arg_compat -> - TacArg(!@loc,TacCall (!@loc,r,la)) ] + TacArg(Loc.tag ~loc:!@loc @@ TacCall (Loc.tag ~loc:!@loc (r,la))) ] | "0" [ "("; a = tactic_expr; ")" -> a | "["; ">"; (tf,tail) = tactic_then_gen; "]" -> @@ -169,7 +169,7 @@ GEXTEND Gram | Some (t,tl) -> TacExtendTac(Array.of_list tf,t,tl) | None -> TacDispatch tf end - | a = tactic_atom -> TacArg (!@loc,a) ] ] + | a = tactic_atom -> TacArg (Loc.tag ~loc:!@loc a) ] ] ; failkw: [ [ IDENT "fail" -> TacLocal | IDENT "gfail" -> TacGlobal ] ] @@ -187,7 +187,7 @@ GEXTEND Gram (* Tactic arguments to the right of an application *) tactic_arg_compat: [ [ a = tactic_arg -> a - | c = Constr.constr -> (match c with CRef (r,None) -> Reference r | c -> ConstrMayEval (ConstrTerm c)) + | c = Constr.constr -> (match c with { CAst.v = CRef (r,None) } -> Reference r | c -> ConstrMayEval (ConstrTerm c)) (* Unambiguous entries: tolerated w/o "ltac:" modifier *) | "()" -> TacGeneric (genarg_of_unit ()) ] ] ; @@ -203,7 +203,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,id) ] ] + | qid = qualid -> let (_pth,id) = Libnames.repr_qualid (snd qid) in ArgVar (Loc.tag ~loc:!@loc id) ] ] ; constr_eval: [ [ IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr -> @@ -219,7 +219,7 @@ GEXTEND Gram ; tactic_atom: [ [ n = integer -> TacGeneric (genarg_of_int n) - | r = reference -> TacCall (!@loc,r,[]) + | r = reference -> TacCall (Loc.tag ~loc:!@loc (r,[])) | "()" -> TacGeneric (genarg_of_unit ()) ] ] ; match_key: @@ -255,10 +255,10 @@ GEXTEND Gram let t, ty = match mpv with | Term t -> (match t with - | CCast (loc, t, (CastConv ty | CastVM ty | CastNative ty)) -> Term t, Some (Term ty) + | { CAst.v = CCast (t, (CastConv ty | CastVM ty | CastNative ty)) } -> Term t, Some (Term ty) | _ -> mpv, None) | _ -> mpv, None - in Def (na, t, Option.default (Term (CHole (Loc.ghost, None, IntroAnonymous, None))) ty) + in Def (na, t, Option.default (Term (CAst.make @@ CHole (None, IntroAnonymous, None))) ty) ] ] ; match_context_rule: @@ -353,7 +353,7 @@ GEXTEND Gram operconstr: LEVEL "0" [ [ IDENT "ltac"; ":"; "("; tac = Pltac.tactic_expr; ")" -> let arg = Genarg.in_gen (Genarg.rawwit Tacarg.wit_tactic) tac in - CHole (!@loc, None, IntroAnonymous, Some arg) ] ] + CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, Some arg) ] ] ; END @@ -459,9 +459,9 @@ END let pr_ltac_production_item = function | Tacentries.TacTerm s -> quote (str s) -| Tacentries.TacNonTerm (_, (arg, None), None) -> str arg -| Tacentries.TacNonTerm (_, (arg, Some _), None) -> assert false -| Tacentries.TacNonTerm (_, (arg, sep), Some id) -> +| Tacentries.TacNonTerm (_, ((arg, None), None)) -> str arg +| Tacentries.TacNonTerm (_, ((arg, Some _), None)) -> assert false +| Tacentries.TacNonTerm (_, ((arg, sep), Some id)) -> let sep = match sep with | None -> mt () | Some sep -> str "," ++ spc () ++ quote (str sep) @@ -471,9 +471,9 @@ let pr_ltac_production_item = function VERNAC ARGUMENT EXTEND ltac_production_item PRINTED BY pr_ltac_production_item | [ string(s) ] -> [ Tacentries.TacTerm s ] | [ ident(nt) "(" ident(p) ltac_production_sep_opt(sep) ")" ] -> - [ Tacentries.TacNonTerm (loc, (Names.Id.to_string nt, sep), Some p) ] + [ Tacentries.TacNonTerm (Loc.tag ~loc ((Names.Id.to_string nt, sep), Some p)) ] | [ ident(nt) ] -> - [ Tacentries.TacNonTerm (loc, (Names.Id.to_string nt, None), None) ] + [ Tacentries.TacNonTerm (Loc.tag ~loc ((Names.Id.to_string nt, None), None)) ] END VERNAC COMMAND EXTEND VernacTacticNotation diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4 index 3e6e2db60..7d4075836 100644 --- a/plugins/ltac/g_obligations.ml4 +++ b/plugins/ltac/g_obligations.ml4 @@ -50,7 +50,7 @@ module Tactic = Pltac open Pcoq -let sigref = mkRefC (Qualid (Loc.ghost, Libnames.qualid_of_string "Coq.Init.Specif.sig")) +let sigref = mkRefC (Qualid (Loc.tag @@ Libnames.qualid_of_string "Coq.Init.Specif.sig")) type 'a withtac_argtype = (Tacexpr.raw_tactic_expr option, 'a) Genarg.abstract_argument_type diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4 index ac979bcf8..5adf8475a 100644 --- a/plugins/ltac/g_rewrite.ml4 +++ b/plugins/ltac/g_rewrite.ml4 @@ -124,7 +124,7 @@ END let clsubstitute o c = Proofview.Goal.enter { enter = begin fun gl -> - let is_tac id = match fst (fst (snd c)) with GVar (_, id') when Id.equal id' id -> true | _ -> false in + let is_tac id = match fst (fst (snd c)) with { CAst.v = GVar id' } when Id.equal id' id -> true | _ -> false in let hyps = Tacmach.New.pf_ids_of_hyps gl in Tacticals.New.tclMAP (fun cl -> diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4 index e33c25cf8..257100b01 100644 --- a/plugins/ltac/g_tactic.ml4 +++ b/plugins/ltac/g_tactic.ml4 @@ -119,14 +119,14 @@ let mk_fix_tac (loc,id,bl,ann,ty) = (try List.index Names.Name.equal (snd x) ids with Not_found -> error "No such fix variable.") | _ -> error "Cannot guess decreasing argument of fix." in - (id,n,CProdN(loc,bl,ty)) + (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 ~hdr:"Constr:mk_cofix_tac" (Pp.str"Annotation forbidden in cofix expression.")) ann in - (id,CProdN(loc,bl,ty)) + (id,CAst.make ~loc @@ CProdN(bl,ty)) (* Functions overloaded by quotifier *) let destruction_arg_of_constr (c,lbind as clbind) = match lbind with @@ -143,32 +143,32 @@ let mkTacCase with_evar = function (* Reinterpret numbers as a notation for terms *) | [(clear,ElimOnAnonHyp n),(None,None),None],None -> TacCase (with_evar, - (clear,(CPrim (Loc.ghost, Numeral (Bigint.of_int n)), + (clear,(CAst.make @@ CPrim (Numeral (Bigint.of_int n)), NoBindings))) (* 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 -> - TacCase (with_evar,(clear,(CRef (Ident id,None),NoBindings))) + TacCase (with_evar,(clear,(CAst.make @@ CRef (Ident id,None),NoBindings))) | ic -> if List.exists (function ((_, ElimOnAnonHyp _),_,_) -> true | _ -> false) (fst ic) then error "Use of numbers as direct arguments of 'case' is not supported."; TacInductionDestruct (false,with_evar,ic) -let rec mkCLambdaN_simple_loc loc bll c = +let rec mkCLambdaN_simple_loc ?loc bll c = match bll with | ((loc1,_)::_ as idl,bk,t) :: bll -> - CLambdaN (loc,[idl,bk,t],mkCLambdaN_simple_loc (Loc.merge loc1 loc) bll c) - | ([],_,_) :: bll -> mkCLambdaN_simple_loc loc bll c + CAst.make ?loc @@ CLambdaN ([idl,bk,t],mkCLambdaN_simple_loc ?loc:(Loc.merge_opt loc1 loc) bll c) + | ([],_,_) :: bll -> mkCLambdaN_simple_loc ?loc bll c | [] -> c let mkCLambdaN_simple bl c = match bl with | [] -> c | h :: _ -> - let loc = Loc.merge (fst (List.hd (pi1 h))) (Constrexpr_ops.constr_loc c) in - mkCLambdaN_simple_loc loc bl c + let loc = Loc.merge_opt (fst (List.hd (pi1 h))) (Constrexpr_ops.constr_loc c) in + mkCLambdaN_simple_loc ?loc bl c -let loc_of_ne_list l = Loc.merge (fst (List.hd l)) (fst (List.last l)) +let loc_of_ne_list l = Loc.merge_opt (fst (List.hd l)) (fst (List.last l)) let map_int_or_var f = function | ArgArg x -> ArgArg (f x) @@ -290,7 +290,7 @@ GEXTEND Gram (* (A & B & C) is translated into (A,(B,C)) *) let rec pairify = function | ([]|[_]|[_;_]) as l -> l - | t::q -> [t;(loc_of_ne_list q,IntroAction (IntroOrAndPattern (IntroAndPattern (pairify q))))] + | t::q -> [t; Loc.tag ?loc:(loc_of_ne_list q) (IntroAction (IntroOrAndPattern (IntroAndPattern (pairify q))))] in IntroAndPattern (pairify (si::tc)) ] ] ; equality_intropattern: @@ -305,8 +305,8 @@ GEXTEND Gram ; nonsimple_intropattern: [ [ l = simple_intropattern -> l - | "*" -> !@loc, IntroForthcoming true - | "**" -> !@loc, IntroForthcoming false ]] + | "*" -> Loc.tag ~loc:!@loc @@ IntroForthcoming true + | "**" -> Loc.tag ~loc:!@loc @@ IntroForthcoming false ]] ; simple_intropattern: [ [ pat = simple_intropattern_closed; @@ -314,19 +314,19 @@ GEXTEND Gram let loc0,pat = pat in let f c pat = let loc1 = Constrexpr_ops.constr_loc c in - let loc = Loc.merge loc0 loc1 in + let loc = Loc.merge_opt loc0 loc1 in IntroAction (IntroApplyOn ((loc1,c),(loc,pat))) in - !@loc, List.fold_right f l pat ] ] + Loc.tag ~loc:!@loc @@ List.fold_right f l pat ] ] ; simple_intropattern_closed: - [ [ pat = or_and_intropattern -> !@loc, IntroAction (IntroOrAndPattern pat) - | pat = equality_intropattern -> !@loc, IntroAction pat - | "_" -> !@loc, IntroAction IntroWildcard - | pat = naming_intropattern -> !@loc, IntroNaming pat ] ] + [ [ pat = or_and_intropattern -> Loc.tag ~loc:!@loc @@ IntroAction (IntroOrAndPattern pat) + | pat = equality_intropattern -> Loc.tag ~loc:!@loc @@ IntroAction pat + | "_" -> Loc.tag ~loc:!@loc @@ IntroAction IntroWildcard + | pat = naming_intropattern -> Loc.tag ~loc:!@loc @@ IntroNaming pat ] ] ; simple_binding: - [ [ "("; id = ident; ":="; c = lconstr; ")" -> (!@loc, NamedHyp id, c) - | "("; n = natural; ":="; c = lconstr; ")" -> (!@loc, AnonHyp n, c) ] ] + [ [ "("; id = ident; ":="; c = lconstr; ")" -> Loc.tag ~loc:!@loc (NamedHyp id, c) + | "("; n = natural; ":="; c = lconstr; ")" -> Loc.tag ~loc:!@loc (AnonHyp n, c) ] ] ; bindings: [ [ test_lpar_idnum_coloneq; bl = LIST1 simple_binding -> @@ -429,7 +429,7 @@ GEXTEND Gram | -> true ]] ; simple_binder: - [ [ na=name -> ([na],Default Explicit,CHole (!@loc, Some (Evar_kinds.BinderType (snd na)), IntroAnonymous, None)) + [ [ na=name -> ([na],Default Explicit, CAst.make ~loc:!@loc @@ CHole (Some (Evar_kinds.BinderType (snd na)), IntroAnonymous, None)) | "("; nal=LIST1 name; ":"; c=lconstr; ")" -> (nal,Default Explicit,c) ] ] ; @@ -457,7 +457,7 @@ GEXTEND Gram | -> None ] ] ; or_and_intropattern_loc: - [ [ ipat = or_and_intropattern -> ArgArg (!@loc,ipat) + [ [ ipat = or_and_intropattern -> ArgArg (Loc.tag ~loc:!@loc ipat) | locid = identref -> ArgVar locid ] ] ; as_or_and_ipat: @@ -465,13 +465,13 @@ GEXTEND Gram | -> None ] ] ; eqn_ipat: - [ [ IDENT "eqn"; ":"; pat = naming_intropattern -> Some (!@loc, pat) + [ [ IDENT "eqn"; ":"; pat = naming_intropattern -> Some (Loc.tag ~loc:!@loc pat) | IDENT "_eqn"; ":"; pat = naming_intropattern -> let loc = !@loc in - warn_deprecated_eqn_syntax ~loc "H"; Some (loc, pat) + warn_deprecated_eqn_syntax ~loc "H"; Some (Loc.tag ~loc pat) | IDENT "_eqn" -> let loc = !@loc in - warn_deprecated_eqn_syntax ~loc "?"; Some (loc, IntroAnonymous) + warn_deprecated_eqn_syntax ~loc "?"; Some (Loc.tag ~loc IntroAnonymous) | -> None ] ] ; as_name: @@ -510,145 +510,145 @@ GEXTEND Gram [ [ (* Basic tactics *) IDENT "intros"; pl = ne_intropatterns -> - TacAtom (!@loc, TacIntroPattern (false,pl)) + TacAtom (Loc.tag ~loc:!@loc @@ TacIntroPattern (false,pl)) | IDENT "intros" -> - TacAtom (!@loc, TacIntroPattern (false,[!@loc,IntroForthcoming false])) + TacAtom (Loc.tag ~loc:!@loc @@ TacIntroPattern (false,[Loc.tag ~loc:!@loc @@IntroForthcoming false])) | IDENT "eintros"; pl = ne_intropatterns -> - TacAtom (!@loc, TacIntroPattern (true,pl)) + TacAtom (Loc.tag ~loc:!@loc @@ TacIntroPattern (true,pl)) | IDENT "apply"; cl = LIST1 constr_with_bindings_arg SEP ","; - inhyp = in_hyp_as -> TacAtom (!@loc, TacApply (true,false,cl,inhyp)) + inhyp = in_hyp_as -> TacAtom (Loc.tag ~loc:!@loc @@ TacApply (true,false,cl,inhyp)) | IDENT "eapply"; cl = LIST1 constr_with_bindings_arg SEP ","; - inhyp = in_hyp_as -> TacAtom (!@loc, TacApply (true,true,cl,inhyp)) + inhyp = in_hyp_as -> TacAtom (Loc.tag ~loc:!@loc @@ TacApply (true,true,cl,inhyp)) | IDENT "simple"; IDENT "apply"; cl = LIST1 constr_with_bindings_arg SEP ","; - inhyp = in_hyp_as -> TacAtom (!@loc, TacApply (false,false,cl,inhyp)) + inhyp = in_hyp_as -> TacAtom (Loc.tag ~loc:!@loc @@ TacApply (false,false,cl,inhyp)) | IDENT "simple"; IDENT "eapply"; cl = LIST1 constr_with_bindings_arg SEP","; - inhyp = in_hyp_as -> TacAtom (!@loc, TacApply (false,true,cl,inhyp)) + inhyp = in_hyp_as -> TacAtom (Loc.tag ~loc:!@loc @@ TacApply (false,true,cl,inhyp)) | IDENT "elim"; cl = constr_with_bindings_arg; el = OPT eliminator -> - TacAtom (!@loc, TacElim (false,cl,el)) + TacAtom (Loc.tag ~loc:!@loc @@ TacElim (false,cl,el)) | IDENT "eelim"; cl = constr_with_bindings_arg; el = OPT eliminator -> - TacAtom (!@loc, TacElim (true,cl,el)) - | IDENT "case"; icl = induction_clause_list -> TacAtom (!@loc, mkTacCase false icl) - | IDENT "ecase"; icl = induction_clause_list -> TacAtom (!@loc, mkTacCase true icl) + TacAtom (Loc.tag ~loc:!@loc @@ TacElim (true,cl,el)) + | IDENT "case"; icl = induction_clause_list -> TacAtom (Loc.tag ~loc:!@loc @@ mkTacCase false icl) + | IDENT "ecase"; icl = induction_clause_list -> TacAtom (Loc.tag ~loc:!@loc @@ mkTacCase true icl) | "fix"; id = ident; n = natural; "with"; fd = LIST1 fixdecl -> - TacAtom (!@loc, TacMutualFix (id,n,List.map mk_fix_tac fd)) + TacAtom (Loc.tag ~loc:!@loc @@ TacMutualFix (id,n,List.map mk_fix_tac fd)) | "cofix"; id = ident; "with"; fd = LIST1 cofixdecl -> - TacAtom (!@loc, TacMutualCofix (id,List.map mk_cofix_tac fd)) + TacAtom (Loc.tag ~loc:!@loc @@ TacMutualCofix (id,List.map mk_cofix_tac fd)) | IDENT "pose"; (id,b) = bindings_with_parameters -> - TacAtom (!@loc, TacLetTac (Names.Name id,b,Locusops.nowhere,true,None)) + TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (Names.Name id,b,Locusops.nowhere,true,None)) | IDENT "pose"; b = constr; na = as_name -> - TacAtom (!@loc, TacLetTac (na,b,Locusops.nowhere,true,None)) + TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (na,b,Locusops.nowhere,true,None)) | IDENT "set"; (id,c) = bindings_with_parameters; p = clause_dft_concl -> - TacAtom (!@loc, TacLetTac (Names.Name id,c,p,true,None)) + TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (Names.Name id,c,p,true,None)) | IDENT "set"; c = constr; na = as_name; p = clause_dft_concl -> - TacAtom (!@loc, TacLetTac (na,c,p,true,None)) + TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (na,c,p,true,None)) | IDENT "remember"; c = constr; na = as_name; e = eqn_ipat; p = clause_dft_all -> - TacAtom (!@loc, TacLetTac (na,c,p,false,e)) + TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (na,c,p,false,e)) (* Alternative syntax for "pose proof c as id" *) | IDENT "assert"; test_lpar_id_coloneq; "("; (loc,id) = identref; ":="; c = lconstr; ")" -> - TacAtom (!@loc, TacAssert (true,None,Some (!@loc,IntroNaming (IntroIdentifier id)),c)) + TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,None,Some (Loc.tag ~loc:!@loc @@IntroNaming (IntroIdentifier id)),c)) (* Alternative syntax for "assert c as id by tac" *) | IDENT "assert"; test_lpar_id_colon; "("; (loc,id) = identref; ":"; c = lconstr; ")"; tac=by_tactic -> - TacAtom (!@loc, TacAssert (true,Some tac,Some (!@loc,IntroNaming (IntroIdentifier id)),c)) + TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,Some tac,Some (Loc.tag ~loc:!@loc @@IntroNaming (IntroIdentifier id)),c)) (* Alternative syntax for "enough c as id by tac" *) | IDENT "enough"; test_lpar_id_colon; "("; (loc,id) = identref; ":"; c = lconstr; ")"; tac=by_tactic -> - TacAtom (!@loc, TacAssert (false,Some tac,Some (!@loc,IntroNaming (IntroIdentifier id)),c)) + TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,Some tac,Some (Loc.tag ~loc:!@loc @@IntroNaming (IntroIdentifier id)),c)) | IDENT "assert"; c = constr; ipat = as_ipat; tac = by_tactic -> - TacAtom (!@loc, TacAssert (true,Some tac,ipat,c)) + TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,Some tac,ipat,c)) | IDENT "pose"; IDENT "proof"; c = lconstr; ipat = as_ipat -> - TacAtom (!@loc, TacAssert (true,None,ipat,c)) + TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,None,ipat,c)) | IDENT "enough"; c = constr; ipat = as_ipat; tac = by_tactic -> - TacAtom (!@loc, TacAssert (false,Some tac,ipat,c)) + TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,Some tac,ipat,c)) | IDENT "generalize"; c = constr -> - TacAtom (!@loc, TacGeneralize [((AllOccurrences,c),Names.Anonymous)]) + TacAtom (Loc.tag ~loc:!@loc @@ TacGeneralize [((AllOccurrences,c),Names.Anonymous)]) | IDENT "generalize"; c = constr; l = LIST1 constr -> let gen_everywhere c = ((AllOccurrences,c),Names.Anonymous) in - TacAtom (!@loc, TacGeneralize (List.map gen_everywhere (c::l))) + TacAtom (Loc.tag ~loc:!@loc @@ TacGeneralize (List.map gen_everywhere (c::l))) | IDENT "generalize"; c = constr; lookup_at_as_comma; nl = occs; na = as_name; l = LIST0 [","; c = pattern_occ; na = as_name -> (c,na)] -> - TacAtom (!@loc, TacGeneralize (((nl,c),na)::l)) + TacAtom (Loc.tag ~loc:!@loc @@ TacGeneralize (((nl,c),na)::l)) (* Derived basic tactics *) | IDENT "induction"; ic = induction_clause_list -> - TacAtom (!@loc, TacInductionDestruct (true,false,ic)) + TacAtom (Loc.tag ~loc:!@loc @@ TacInductionDestruct (true,false,ic)) | IDENT "einduction"; ic = induction_clause_list -> - TacAtom (!@loc, TacInductionDestruct(true,true,ic)) + TacAtom (Loc.tag ~loc:!@loc @@ TacInductionDestruct(true,true,ic)) | IDENT "destruct"; icl = induction_clause_list -> - TacAtom (!@loc, TacInductionDestruct(false,false,icl)) + TacAtom (Loc.tag ~loc:!@loc @@ TacInductionDestruct(false,false,icl)) | IDENT "edestruct"; icl = induction_clause_list -> - TacAtom (!@loc, TacInductionDestruct(false,true,icl)) + TacAtom (Loc.tag ~loc:!@loc @@ TacInductionDestruct(false,true,icl)) (* Equality and inversion *) | IDENT "rewrite"; l = LIST1 oriented_rewriter SEP ","; - cl = clause_dft_concl; t=by_tactic -> TacAtom (!@loc, TacRewrite (false,l,cl,t)) + cl = clause_dft_concl; t=by_tactic -> TacAtom (Loc.tag ~loc:!@loc @@ TacRewrite (false,l,cl,t)) | IDENT "erewrite"; l = LIST1 oriented_rewriter SEP ","; - cl = clause_dft_concl; t=by_tactic -> TacAtom (!@loc, TacRewrite (true,l,cl,t)) + cl = clause_dft_concl; t=by_tactic -> TacAtom (Loc.tag ~loc:!@loc @@ TacRewrite (true,l,cl,t)) | IDENT "dependent"; k = [ IDENT "simple"; IDENT "inversion" -> SimpleInversion | IDENT "inversion" -> FullInversion | IDENT "inversion_clear" -> FullInversionClear ]; hyp = quantified_hypothesis; ids = as_or_and_ipat; co = OPT ["with"; c = constr -> c] -> - TacAtom (!@loc, TacInversion (DepInversion (k,co,ids),hyp)) + TacAtom (Loc.tag ~loc:!@loc @@ TacInversion (DepInversion (k,co,ids),hyp)) | IDENT "simple"; IDENT "inversion"; hyp = quantified_hypothesis; ids = as_or_and_ipat; cl = in_hyp_list -> - TacAtom (!@loc, TacInversion (NonDepInversion (SimpleInversion, cl, ids), hyp)) + TacAtom (Loc.tag ~loc:!@loc @@ TacInversion (NonDepInversion (SimpleInversion, cl, ids), hyp)) | IDENT "inversion"; hyp = quantified_hypothesis; ids = as_or_and_ipat; cl = in_hyp_list -> - TacAtom (!@loc, TacInversion (NonDepInversion (FullInversion, cl, ids), hyp)) + TacAtom (Loc.tag ~loc:!@loc @@ TacInversion (NonDepInversion (FullInversion, cl, ids), hyp)) | IDENT "inversion_clear"; hyp = quantified_hypothesis; ids = as_or_and_ipat; cl = in_hyp_list -> - TacAtom (!@loc, TacInversion (NonDepInversion (FullInversionClear, cl, ids), hyp)) + TacAtom (Loc.tag ~loc:!@loc @@ TacInversion (NonDepInversion (FullInversionClear, cl, ids), hyp)) | IDENT "inversion"; hyp = quantified_hypothesis; "using"; c = constr; cl = in_hyp_list -> - TacAtom (!@loc, TacInversion (InversionUsing (c,cl), hyp)) + TacAtom (Loc.tag ~loc:!@loc @@ TacInversion (InversionUsing (c,cl), hyp)) (* Conversion *) | IDENT "red"; cl = clause_dft_concl -> - TacAtom (!@loc, TacReduce (Red false, cl)) + TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Red false, cl)) | IDENT "hnf"; cl = clause_dft_concl -> - TacAtom (!@loc, TacReduce (Hnf, cl)) + TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Hnf, cl)) | IDENT "simpl"; d = delta_flag; po = OPT ref_or_pattern_occ; cl = clause_dft_concl -> - TacAtom (!@loc, TacReduce (Simpl (all_with d, po), cl)) + TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Simpl (all_with d, po), cl)) | IDENT "cbv"; s = strategy_flag; cl = clause_dft_concl -> - TacAtom (!@loc, TacReduce (Cbv s, cl)) + TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Cbv s, cl)) | IDENT "cbn"; s = strategy_flag; cl = clause_dft_concl -> - TacAtom (!@loc, TacReduce (Cbn s, cl)) + TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Cbn s, cl)) | IDENT "lazy"; s = strategy_flag; cl = clause_dft_concl -> - TacAtom (!@loc, TacReduce (Lazy s, cl)) + TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Lazy s, cl)) | IDENT "compute"; delta = delta_flag; cl = clause_dft_concl -> - TacAtom (!@loc, TacReduce (Cbv (all_with delta), cl)) + TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Cbv (all_with delta), cl)) | IDENT "vm_compute"; po = OPT ref_or_pattern_occ; cl = clause_dft_concl -> - TacAtom (!@loc, TacReduce (CbvVm po, cl)) + TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (CbvVm po, cl)) | IDENT "native_compute"; po = OPT ref_or_pattern_occ; cl = clause_dft_concl -> - TacAtom (!@loc, TacReduce (CbvNative po, cl)) + TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (CbvNative po, cl)) | IDENT "unfold"; ul = LIST1 unfold_occ SEP ","; cl = clause_dft_concl -> - TacAtom (!@loc, TacReduce (Unfold ul, cl)) + TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Unfold ul, cl)) | IDENT "fold"; l = LIST1 constr; cl = clause_dft_concl -> - TacAtom (!@loc, TacReduce (Fold l, cl)) + TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Fold l, cl)) | IDENT "pattern"; pl = LIST1 pattern_occ SEP","; cl = clause_dft_concl -> - TacAtom (!@loc, TacReduce (Pattern pl, cl)) + TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Pattern pl, cl)) (* Change ne doit pas s'appliquer dans un Definition t := Eval ... *) | IDENT "change"; (oc,c) = conversion; cl = clause_dft_concl -> let p,cl = merge_occurrences (!@loc) cl oc in - TacAtom (!@loc, TacChange (p,c,cl)) + TacAtom (Loc.tag ~loc:!@loc @@ TacChange (p,c,cl)) ] ] ; END;; diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index a61957559..75ab1c5ee 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -51,7 +51,7 @@ let pr_global x = Nametab.pr_global_env Id.Set.empty x type 'a grammar_tactic_prod_item_expr = | TacTerm of string -| TacNonTerm of Loc.t * 'a * Names.Id.t option +| TacNonTerm of ('a * Names.Id.t option) Loc.located type grammar_terminals = Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list @@ -149,7 +149,7 @@ type 'a extra_genarg_printer = let pr_or_by_notation f = function | AN v -> f v - | ByNotation (_,s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc + | ByNotation (_,(s,sc)) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc let pr_located pr (loc,x) = pr x @@ -162,8 +162,8 @@ type 'a extra_genarg_printer = | NamedHyp id -> pr_id id let pr_binding prc = function - | loc, NamedHyp id, c -> hov 1 (pr_id id ++ str " := " ++ cut () ++ prc c) - | loc, AnonHyp n, c -> hov 1 (int n ++ str " := " ++ cut () ++ prc c) + | loc, (NamedHyp id, c) -> hov 1 (pr_id id ++ str " := " ++ cut () ++ prc c) + | loc, (AnonHyp n, c) -> hov 1 (int n ++ str " := " ++ cut () ++ prc c) let pr_bindings prc prlc = function | ImplicitBindings l -> @@ -212,7 +212,7 @@ type 'a extra_genarg_printer = let rec tacarg_using_rule_token pr_gen = function | [] -> [] | TacTerm s :: l -> keyword s :: tacarg_using_rule_token pr_gen l - | TacNonTerm (_, (symb, arg), _) :: l -> + | TacNonTerm (_, ((symb, arg), _)) :: l -> pr_gen symb arg :: tacarg_using_rule_token pr_gen l let pr_tacarg_using_rule pr_gen l = @@ -252,7 +252,7 @@ type 'a extra_genarg_printer = let prods = (KNmap.find key !prnotation_tab).pptac_prods in let pr = function | TacTerm s -> primitive s - | TacNonTerm (_, symb, _) -> str (Printf.sprintf "(%s)" (pr_user_symbol symb)) + | TacNonTerm (_, (symb, _)) -> str (Printf.sprintf "(%s)" (pr_user_symbol symb)) in pr_sequence pr prods with Not_found -> @@ -264,9 +264,9 @@ type 'a extra_genarg_printer = let rec pack prods args = match prods, args with | [], [] -> [] | TacTerm s :: prods, args -> TacTerm s :: pack prods args - | TacNonTerm (_, _, None) :: prods, args -> pack prods args - | TacNonTerm (loc, symb, (Some _ as ido)) :: prods, arg :: args -> - TacNonTerm (loc, (symb, arg), ido) :: pack prods args + | TacNonTerm (_, (_, None)) :: prods, args -> pack prods args + | TacNonTerm (loc, (symb, (Some _ as ido))) :: prods, arg :: args -> + TacNonTerm (loc, ((symb, arg), ido)) :: pack prods args | _ -> raise Not_found in let prods = pack pp.pptac_prods l in @@ -276,7 +276,7 @@ type 'a extra_genarg_printer = let pr arg = str "_" in KerName.print key ++ spc() ++ pr_sequence pr l ++ str" (* Generic printer *)" - let pr_farg prtac arg = prtac (1, Any) (TacArg (Loc.ghost, arg)) + let pr_farg prtac arg = prtac (1, Any) (TacArg (Loc.tag arg)) let is_genarg tag wit = let ArgT.Any tag = tag in @@ -332,17 +332,17 @@ type 'a extra_genarg_printer = pr_extend_gen (pr_farg prtac) let pr_raw_alias prc prlc prtac prpat lev key args = - pr_alias_gen (pr_targ (fun l a -> prtac l (TacArg (Loc.ghost, a)))) lev key args + pr_alias_gen (pr_targ (fun l a -> prtac l (TacArg (Loc.tag a)))) lev key args let pr_glob_alias prc prlc prtac prpat lev key args = - pr_alias_gen (pr_targ (fun l a -> prtac l (TacArg (Loc.ghost, a)))) lev key args + pr_alias_gen (pr_targ (fun l a -> prtac l (TacArg (Loc.tag a)))) lev key args (**********************************************************************) (* The tactic printer *) let strip_prod_binders_expr n ty = let rec strip_ty acc n ty = - match ty with - Constrexpr.CProdN(_,bll,a) -> + match ty.CAst.v with + Constrexpr.CProdN(bll,a) -> let nb = List.fold_left (fun i (nal,_,_) -> i + List.length nal) 0 bll in let bll = List.map (fun (x, _, y) -> x, y) bll in @@ -353,7 +353,7 @@ type 'a extra_genarg_printer = let pr_ltac_or_var pr = function | ArgArg x -> pr x - | ArgVar (loc,id) -> pr_with_comments loc (pr_id id) + | ArgVar (loc,id) -> pr_with_comments ?loc (pr_id id) let pr_ltac_constant kn = if !Flags.in_debugger then pr_kn kn @@ -369,8 +369,8 @@ type 'a extra_genarg_printer = let pr_esubst prc l = let pr_qhyp = function - (_,AnonHyp n,c) -> str "(" ++ int n ++ str" := " ++ prc c ++ str ")" - | (_,NamedHyp id,c) -> + (_,(AnonHyp n,c)) -> str "(" ++ int n ++ str" := " ++ prc c ++ str ")" + | (_,(NamedHyp id,c)) -> str "(" ++ pr_id id ++ str" := " ++ prc c ++ str ")" in prlist_with_sep spc pr_qhyp l @@ -417,7 +417,7 @@ type 'a extra_genarg_printer = let pr_as_name = function | Anonymous -> mt () - | Name id -> spc () ++ keyword "as" ++ spc () ++ pr_lident (Loc.ghost,id) + | Name id -> spc () ++ keyword "as" ++ spc () ++ pr_lident (Loc.tag id) let pr_pose_as_style prc na c = spc() ++ prc c ++ pr_as_name na @@ -508,7 +508,7 @@ type 'a extra_genarg_printer = 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 (loc,id) -> pr_with_comments ?loc (pr_id id) | ElimOnAnonHyp n -> int n let pr_destruction_arg prc prlc (clear_flag,h) = @@ -575,7 +575,7 @@ type 'a extra_genarg_printer = let pr_let_clause k pr (id,(bl,t)) = hov 0 (keyword k ++ spc () ++ pr_lident id ++ prlist pr_funvar bl ++ - str " :=" ++ brk (1,1) ++ pr (TacArg (Loc.ghost,t))) + str " :=" ++ brk (1,1) ++ pr (TacArg (Loc.tag t))) let pr_let_clauses recflag pr = function | hd::tl -> @@ -1038,7 +1038,7 @@ type 'a extra_genarg_printer = | TacId l -> keyword "idtac" ++ prlist (pr_arg (pr_message_token pr.pr_name)) l, latom | TacAtom (loc,t) -> - pr_with_comments loc (hov 1 (pr_atom pr strip_prod_binders tag_atom t)), ltatom + pr_with_comments ?loc (hov 1 (pr_atom pr strip_prod_binders tag_atom t)), ltatom | TacArg(_,Tacexp e) -> pr.pr_tactic (latom,E) e, latom | TacArg(_,ConstrMayEval (ConstrTerm c)) -> @@ -1049,19 +1049,19 @@ type 'a extra_genarg_printer = primitive "fresh" ++ pr_fresh_ids l, latom | TacArg(_,TacGeneric arg) -> pr.pr_generic arg, latom - | TacArg(_,TacCall(loc,f,[])) -> + | TacArg(_,TacCall(loc,(f,[]))) -> pr.pr_reference f, latom - | TacArg(_,TacCall(loc,f,l)) -> - pr_with_comments loc (hov 1 ( + | TacArg(_,TacCall(loc,(f,l))) -> + pr_with_comments ?loc (hov 1 ( pr.pr_reference f ++ spc () ++ prlist_with_sep spc pr_tacarg l)), lcall | TacArg (_,a) -> pr_tacarg a, latom - | TacML (loc,s,l) -> - pr_with_comments loc (pr.pr_extend 1 s l), lcall - | TacAlias (loc,kn,l) -> - pr_with_comments loc (pr.pr_alias (level_of inherited) kn l), latom + | TacML (loc,(s,l)) -> + pr_with_comments ?loc (pr.pr_extend 1 s l), lcall + | TacAlias (loc,(kn,l)) -> + pr_with_comments ?loc (pr.pr_alias (level_of inherited) kn l), latom ) in if prec_less prec inherited then strm @@ -1079,16 +1079,16 @@ type 'a extra_genarg_printer = | TacNumgoals -> keyword "numgoals" | (TacCall _|Tacexp _ | TacGeneric _) as a -> - hov 0 (keyword "ltac:" ++ surround (pr_tac ltop (TacArg (Loc.ghost,a)))) + hov 0 (keyword "ltac:" ++ surround (pr_tac ltop (TacArg (Loc.tag a)))) in pr_tac let strip_prod_binders_glob_constr n (ty,_) = let rec strip_ty acc n ty = if Int.equal n 0 then (List.rev acc, (ty,None)) else - match ty with - Glob_term.GProd(loc,na,Explicit,a,b) -> - strip_ty (([Loc.ghost,na],(a,None))::acc) (n-1) b + match ty.CAst.v with + Glob_term.GProd(na,Explicit,a,b) -> + strip_ty (([Loc.tag na],(a,None))::acc) (n-1) b | _ -> error "Cannot translate fix tactic: not enough products" in strip_ty [] n ty @@ -1159,7 +1159,7 @@ type 'a extra_genarg_printer = if n=0 then (List.rev acc, EConstr.of_constr ty) else match Term.kind_of_term ty with Term.Prod(na,a,b) -> - strip_ty (([Loc.ghost,na],EConstr.of_constr a)::acc) (n-1) b + strip_ty (([Loc.tag na],EConstr.of_constr a)::acc) (n-1) b | _ -> error "Cannot translate fix tactic: not enough products" in strip_ty [] n ty @@ -1254,7 +1254,7 @@ let () = wit_clause_dft_concl (pr_clauses (Some true) pr_lident) (pr_clauses (Some true) pr_lident) - (pr_clauses (Some true) (fun id -> pr_lident (Loc.ghost,id))) + (pr_clauses (Some true) (fun id -> pr_lident (Loc.tag id))) ; Genprint.register_print0 wit_constr diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 433f342c4..19bdf2d49 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -21,7 +21,7 @@ open Ppextend type 'a grammar_tactic_prod_item_expr = | TacTerm of string -| TacNonTerm of Loc.t * 'a * Names.Id.t option +| TacNonTerm of ('a * Names.Id.t option) Loc.located type 'a raw_extra_genarg_printer = (constr_expr -> std_ppcmds) -> diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index 747669852..3ff7b53c7 100644 --- a/plugins/ltac/profile_ltac.ml +++ b/plugins/ltac/profile_ltac.ml @@ -129,7 +129,7 @@ let to_ltacprof_results xml = let feedback_results results = Feedback.(feedback - (Custom (Loc.dummy_loc, "ltacprof_results", of_ltacprof_results results))) + (Custom (None, "ltacprof_results", of_ltacprof_results results))) (* ************** pretty printing ************************************* *) @@ -249,7 +249,7 @@ let string_of_call ck = | Tacexpr.LtacVarCall (id, t) -> Nameops.pr_id id | Tacexpr.LtacAtomCall te -> (Pptactic.pr_glob_tactic (Global.env ()) - (Tacexpr.TacAtom (Loc.ghost, te))) + (Tacexpr.TacAtom (Loc.tag te))) | Tacexpr.LtacConstrInterp (c, _) -> pr_glob_constr_env (Global.env ()) c | Tacexpr.LtacMLCall te -> diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 5630a2d7b..e8c9f4eba 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1786,34 +1786,34 @@ let rec strategy_of_ast = function (* By default the strategy for "rewrite_db" is top-down *) -let mkappc s l = CAppExpl (Loc.ghost,(None,(Libnames.Ident (Loc.ghost,Id.of_string s)),None),l) +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.ghost,Name n),None), Explicit, - CAppExpl (Loc.ghost, (None, Qualid (Loc.ghost, qualid_of_string s),None), + (((Loc.tag @@ Name n),None), Explicit, + CAst.make @@ CAppExpl ((None, Qualid (Loc.tag @@ qualid_of_string s),None), args)) let declare_instance a aeq n s = declare_an_instance n s [a;aeq] let anew_instance global binders instance fields = new_instance (Flags.is_universe_polymorphism ()) - binders instance (Some (true, CRecord (Loc.ghost,fields))) + binders instance (Some (true, CAst.make @@ CRecord (fields))) ~global ~generalize:false ~refine:false Hints.empty_hint_info let declare_instance_refl global binders a aeq n lemma = let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive" in anew_instance global binders instance - [(Ident (Loc.ghost,Id.of_string "reflexivity"),lemma)] + [(Ident (Loc.tag @@ Id.of_string "reflexivity"),lemma)] let declare_instance_sym global binders a aeq n lemma = let instance = declare_instance a aeq (add_suffix n "_Symmetric") "Coq.Classes.RelationClasses.Symmetric" in anew_instance global binders instance - [(Ident (Loc.ghost,Id.of_string "symmetry"),lemma)] + [(Ident (Loc.tag @@ Id.of_string "symmetry"),lemma)] let declare_instance_trans global binders a aeq n lemma = let instance = declare_instance a aeq (add_suffix n "_Transitive") "Coq.Classes.RelationClasses.Transitive" in anew_instance global binders instance - [(Ident (Loc.ghost,Id.of_string "transitivity"),lemma)] + [(Ident (Loc.tag @@ Id.of_string "transitivity"),lemma)] let declare_relation ?(binders=[]) a aeq n refl symm trans = init_setoid (); @@ -1837,16 +1837,16 @@ let declare_relation ?(binders=[]) a aeq n refl symm trans = let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder" in ignore( anew_instance global binders instance - [(Ident (Loc.ghost,Id.of_string "PreOrder_Reflexive"), lemma1); - (Ident (Loc.ghost,Id.of_string "PreOrder_Transitive"),lemma3)]) + [(Ident (Loc.tag @@ Id.of_string "PreOrder_Reflexive"), lemma1); + (Ident (Loc.tag @@ Id.of_string "PreOrder_Transitive"),lemma3)]) | (None, Some lemma2, Some lemma3) -> let _lemma_sym = declare_instance_sym global binders a aeq n lemma2 in let _lemma_trans = declare_instance_trans global binders a aeq n lemma3 in let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER" in ignore( anew_instance global binders instance - [(Ident (Loc.ghost,Id.of_string "PER_Symmetric"), lemma2); - (Ident (Loc.ghost,Id.of_string "PER_Transitive"),lemma3)]) + [(Ident (Loc.tag @@ Id.of_string "PER_Symmetric"), lemma2); + (Ident (Loc.tag @@ Id.of_string "PER_Transitive"),lemma3)]) | (Some lemma1, Some lemma2, Some lemma3) -> let _lemma_refl = declare_instance_refl global binders a aeq n lemma1 in let _lemma_sym = declare_instance_sym global binders a aeq n lemma2 in @@ -1854,11 +1854,11 @@ let declare_relation ?(binders=[]) a aeq n refl symm trans = let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" in ignore( anew_instance global binders instance - [(Ident (Loc.ghost,Id.of_string "Equivalence_Reflexive"), lemma1); - (Ident (Loc.ghost,Id.of_string "Equivalence_Symmetric"), lemma2); - (Ident (Loc.ghost,Id.of_string "Equivalence_Transitive"), lemma3)]) + [(Ident (Loc.tag @@ Id.of_string "Equivalence_Reflexive"), lemma1); + (Ident (Loc.tag @@ Id.of_string "Equivalence_Symmetric"), lemma2); + (Ident (Loc.tag @@ Id.of_string "Equivalence_Transitive"), lemma3)]) -let cHole = CHole (Loc.ghost, None, Misctypes.IntroAnonymous, None) +let cHole = CAst.make @@ CHole (None, Misctypes.IntroAnonymous, None) let proper_projection sigma r ty = let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i)) in @@ -1958,17 +1958,16 @@ let add_setoid global binders a aeq t n = let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" in ignore( anew_instance global binders instance - [(Ident (Loc.ghost,Id.of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]); - (Ident (Loc.ghost,Id.of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]); - (Ident (Loc.ghost,Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])]) + [(Ident (Loc.tag @@ Id.of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]); + (Ident (Loc.tag @@ Id.of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]); + (Ident (Loc.tag @@ Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])]) let make_tactic name = let open Tacexpr in - let loc = Loc.ghost in let tacpath = Libnames.qualid_of_string name in - let tacname = Qualid (loc, tacpath) in - TacArg (loc, TacCall (loc, tacname, [])) + let tacname = Qualid (Loc.tag tacpath) in + TacArg (Loc.tag @@ TacCall (Loc.tag (tacname, []))) let add_morphism_infer glob m n = init_setoid (); @@ -2011,14 +2010,14 @@ 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.ghost,Name instance_id),None), Explicit, - CAppExpl (Loc.ghost, - (None, Qualid (Loc.ghost, Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper"),None), + (((Loc.tag @@ Name instance_id),None), Explicit, + CAst.make @@ CAppExpl ( + (None, Qualid (Loc.tag @@ Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper"),None), [cHole; s; m])) in let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in ignore(new_instance ~global:glob poly binders instance - (Some (true, CRecord (Loc.ghost,[]))) + (Some (true, CAst.make @@ CRecord [])) ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info) (** Bind to "rewrite" too *) diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index b76009c99..e037bb4b2 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -268,11 +268,11 @@ let coerce_to_constr_list env v = List.map map l | None -> raise (CannotCoerceTo "a term list") -let coerce_to_intro_pattern_list loc env sigma v = +let coerce_to_intro_pattern_list ?loc env sigma v = match Value.to_list v with | None -> raise (CannotCoerceTo "an intro pattern list") | Some l -> - let map v = (loc, coerce_to_intro_pattern env sigma v) in + let map v = Loc.tag ?loc @@ coerce_to_intro_pattern env sigma v in List.map map l let coerce_to_hyp env sigma v = diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli index 4a44f86d9..9883c03c4 100644 --- a/plugins/ltac/taccoerce.mli +++ b/plugins/ltac/taccoerce.mli @@ -75,7 +75,7 @@ val coerce_to_evaluable_ref : val coerce_to_constr_list : Environ.env -> Value.t -> constr list val coerce_to_intro_pattern_list : - Loc.t -> Environ.env -> Evd.evar_map -> Value.t -> Tacexpr.intro_patterns + ?loc:Loc.t -> Environ.env -> Evd.evar_map -> Value.t -> Tacexpr.intro_patterns val coerce_to_hyp : Environ.env -> Evd.evar_map -> Value.t -> Id.t diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 91262f6fd..4d7b0f929 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -21,7 +21,7 @@ open Nameops type 'a grammar_tactic_prod_item_expr = 'a Pptactic.grammar_tactic_prod_item_expr = | TacTerm of string -| TacNonTerm of Loc.t * 'a * Names.Id.t option +| TacNonTerm of ('a * Names.Id.t option) Loc.located type raw_argument = string * string option type argument = Genarg.ArgT.any Extend.user_symbol @@ -166,7 +166,7 @@ let add_tactic_entry (kn, ml, tg) state = TacGeneric arg in let l = List.map map l in - (TacAlias (loc,kn,l):raw_tactic_expr) + (TacAlias (Loc.tag ~loc (kn,l)):raw_tactic_expr) in let () = if Int.equal tg.tacgram_level 0 && not (head_is_ident tg) then @@ -174,9 +174,9 @@ let add_tactic_entry (kn, ml, tg) state = in let map = function | TacTerm s -> GramTerminal s - | TacNonTerm (loc, s, ido) -> + | TacNonTerm (loc, (s, ido)) -> let EntryName (typ, e) = prod_item_of_symbol tg.tacgram_level s in - GramNonTerminal (loc, Option.map (fun _ -> typ) ido, e) + GramNonTerminal (Loc.tag ?loc @@ (Option.map (fun _ -> typ) ido, e)) in let prods = List.map map tg.tacgram_prods in let rules = make_rule mkact prods in @@ -202,7 +202,7 @@ let register_tactic_notation_entry name entry = let interp_prod_item = function | TacTerm s -> TacTerm s - | TacNonTerm (loc, (nt, sep), ido) -> + | TacNonTerm (loc, ((nt, sep), ido)) -> let symbol = parse_user_entry nt sep in let interp s = function | None -> @@ -220,7 +220,7 @@ let interp_prod_item = function end in let symbol = interp_entry_name interp symbol in - TacNonTerm (loc, symbol, ido) + TacNonTerm (loc, (symbol, ido)) let make_fresh_key = let id = Summary.ref ~name:"TACTIC-NOTATION-COUNTER" 0 in @@ -296,7 +296,7 @@ let inTacticGrammar : tactic_grammar_obj -> obj = let cons_production_parameter = function | TacTerm _ -> None -| TacNonTerm (_, _, ido) -> ido +| TacNonTerm (_, (_, ido)) -> ido let add_glob_tactic_notation local ~level prods forml ids tac = let parule = { @@ -334,10 +334,10 @@ let extend_atomic_tactic name entries = in let empty_value = function | TacTerm s -> raise NonEmptyArgument - | TacNonTerm (_, symb, _) -> + | TacNonTerm (_, (symb, _)) -> let EntryName (typ, e) = prod_item_of_symbol 0 symb in let Genarg.Rawwit wit = typ in - let inj x = TacArg (Loc.ghost, TacGeneric (Genarg.in_gen typ x)) in + let inj x = TacArg (Loc.tag @@ TacGeneric (Genarg.in_gen typ x)) in let default = epsilon_value inj e in match default with | None -> raise NonEmptyArgument @@ -351,7 +351,7 @@ let extend_atomic_tactic name entries = | Some (id, args) -> let args = List.map (fun a -> Tacexp a) args in let entry = { mltac_name = name; mltac_index = i } in - let body = TacML (Loc.ghost, entry, args) in + let body = TacML (Loc.tag (entry, args)) in Tacenv.register_ltac false false (Names.Id.of_string id) body in List.iteri add_atomic entries @@ -362,12 +362,12 @@ let add_ml_tactic_notation name ~level prods = let open Tacexpr in let get_id = function | TacTerm s -> None - | TacNonTerm (_, _, ido) -> ido + | TacNonTerm (_, (_, ido)) -> ido 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.ghost, id)) in - let tac = TacML (Loc.ghost, entry, List.map map ids) in + let map id = Reference (Misctypes.ArgVar (Loc.tag id)) in + let tac = TacML (Loc.tag (entry, List.map map ids)) in add_glob_tactic_notation false ~level prods true ids tac in List.iteri iter (List.rev prods); @@ -401,7 +401,7 @@ let create_ltac_quotation name cast (e, l) = entry), Atoken (CLexer.terminal ")")) in - let action _ v _ _ _ loc = cast (loc, v) in + let action _ v _ _ _ loc = cast (Some loc, v) in let gram = (level, assoc, [Rule (rule, action)]) in Pcoq.grammar_extend Pltac.tactic_arg None (None, [gram]) @@ -427,7 +427,7 @@ let register_ltac local tacl = let kn = Lib.make_kn id in let id_pp = pr_id 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 = @@ -444,7 +444,7 @@ let register_ltac local tacl = let kn = try Nametab.locate_tactic (snd (qualid_of_reference ident)) with Not_found -> - CErrors.user_err ~loc + CErrors.user_err ?loc (str "There is no Ltac named " ++ pr_reference ident ++ str ".") in UpdateTac kn, body diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index dac62dad3..07aa7ad82 100644 --- a/plugins/ltac/tacentries.mli +++ b/plugins/ltac/tacentries.mli @@ -20,7 +20,7 @@ val register_ltac : locality_flag -> Tacexpr.tacdef_body list -> unit type 'a grammar_tactic_prod_item_expr = 'a Pptactic.grammar_tactic_prod_item_expr = | TacTerm of string -| TacNonTerm of Loc.t * 'a * Names.Id.t option +| TacNonTerm of ('a * Names.Id.t option) Loc.located type raw_argument = string * string option (** An argument type as provided in Tactic notations, i.e. a string like diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 8aefe7605..bf760e7bb 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -184,8 +184,7 @@ type 'a gen_tactic_arg = | TacGeneric of 'lev generic_argument | ConstrMayEval of ('trm,'cst,'pat) may_eval | Reference of 'ref - | TacCall of Loc.t * 'ref * - 'a gen_tactic_arg list + | TacCall of ('ref * 'a gen_tactic_arg list) Loc.located | TacFreshId of string or_var list | Tacexp of 'tacexpr | TacPretype of 'trm @@ -207,7 +206,7 @@ constraint 'a = < 'r : ltac refs, 'n : idents, 'l : levels *) and 'a gen_tactic_expr = - | TacAtom of Loc.t * 'a gen_atomic_tactic_expr + | TacAtom of ('a gen_atomic_tactic_expr) Loc.located | TacThen of 'a gen_tactic_expr * 'a gen_tactic_expr @@ -266,9 +265,9 @@ and 'a gen_tactic_expr = | TacArg of 'a gen_tactic_arg located | TacSelect of goal_selector * 'a gen_tactic_expr (* For ML extensions *) - | TacML of Loc.t * ml_tactic_entry * 'a gen_tactic_arg list + | TacML of (ml_tactic_entry * 'a gen_tactic_arg list) Loc.located (* For syntax extensions *) - | TacAlias of Loc.t * KerName.t * 'a gen_tactic_arg list + | TacAlias of (KerName.t * 'a gen_tactic_arg list) Loc.located constraint 'a = < term:'t; @@ -389,7 +388,7 @@ type ltac_call_kind = | LtacVarCall of Id.t * glob_tactic_expr | LtacConstrInterp of Glob_term.glob_constr * Pretyping.ltac_var_map -type ltac_trace = (Loc.t * ltac_call_kind) list +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 *) diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 75227def0..da7f11472 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -31,8 +31,6 @@ open Locus (** Globalization of tactic expressions : Conversion from [raw_tactic_expr] to [glob_tactic_expr] *) -let dloc = Loc.ghost - let error_tactic_expected ?loc = user_err ?loc (str "Tactic expected.") @@ -74,16 +72,16 @@ let intern_name l ist = function let strict_check = ref false -let adjust_loc loc = if !strict_check then dloc else loc +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) = if not !strict_check then locid else if find_ident id ist then - (dloc,id) + Loc.tag id else - Pretype_errors.error_var_not_found ~loc id + Pretype_errors.error_var_not_found ?loc id let intern_or_var f ist = function | ArgVar locid -> ArgVar (intern_hyp ist locid) @@ -110,19 +108,19 @@ let intern_ltac_variable ist = function let intern_constr_reference strict ist = function | Ident (_,id) as r when not strict && find_hyp id ist -> - GVar (dloc,id), Some (CRef (r,None)) + (CAst.make @@ GVar id), Some (CAst.make @@ CRef (r,None)) | Ident (_,id) as r when find_var id ist -> - GVar (dloc,id), if strict then None else Some (CRef (r,None)) + (CAst.make @@ GVar id), if strict then None else Some (CAst.make @@ CRef (r,None)) | r -> let loc,_ as lqid = qualid_of_reference r in - GRef (loc,locate_global_with_alias lqid,None), - if strict then None else Some (CRef (r,None)) + CAst.make @@ GRef (locate_global_with_alias lqid,None), + if strict then None else Some (CAst.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 - TacCall (loc,ArgArg (loc,locate_tactic qid),[]) + TacCall (Loc.tag ?loc (ArgArg (loc,locate_tactic qid),[])) let intern_isolated_tactic_reference strict ist r = (* An ltac reference *) @@ -208,8 +206,8 @@ let intern_constr = intern_constr_gen false false let intern_type = intern_constr_gen false true (* Globalize bindings *) -let intern_binding ist (loc,b,c) = - (loc,intern_binding_name ist b,intern_constr ist c) +let intern_binding ist (loc,(b,c)) = + (loc,(intern_binding_name ist b,intern_constr ist c)) let intern_bindings ist = function | NoBindings -> NoBindings @@ -267,8 +265,8 @@ let intern_destruction_arg ist = function | clear,ElimOnIdent (loc,id) -> if !strict_check then (* If in a defined tactic, no intros-until *) - match intern_constr ist (CRef (Ident (dloc,id), None)) with - | GVar (loc,id),_ -> clear,ElimOnIdent (loc,id) + match intern_constr ist (CAst.make @@ CRef (Ident (Loc.tag id), None)) with + | {loc; CAst.v = GVar id}, _ -> clear,ElimOnIdent (loc,id) | c -> clear,ElimOnConstr (c,NoBindings) else clear,ElimOnIdent (loc,id) @@ -287,9 +285,9 @@ let intern_evaluable_global_reference ist r = let intern_evaluable_reference_or_by_notation ist = function | AN r -> intern_evaluable_global_reference ist r - | ByNotation (loc,ntn,sc) -> + | ByNotation (loc,(ntn,sc)) -> evaluable_of_global_reference ist.genv - (Notation.interp_notation_as_global_reference loc + (Notation.interp_notation_as_global_reference ?loc (function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc) (* Globalize a reduction expression *) @@ -346,10 +344,10 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) = | _ -> Qualid (loc,qualid_of_path (path_of_global (smart_global r))) in let sign = { Constrintern.ltac_vars = ist.ltacvars; Constrintern.ltac_bound = Id.Set.empty } in let c = Constrintern.interp_reference sign r in - match c with - | GRef (_,r,None) -> + match c.CAst.v with + | GRef (r,None) -> Inl (ArgArg (evaluable_of_global_reference ist.genv r,None)) - | GVar (_,id) -> + | GVar id -> let r = evaluable_of_global_reference ist.genv (VarRef id) in Inl (ArgArg (r,None)) | _ -> @@ -357,7 +355,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 (CAppExpl(_,(None,r,None),[])) -> + | Inr { CAst.v = CAppExpl((None,r,None),[]) } -> (* We interpret similarly @ref and ref *) interp_ref (AN r) | Inr c -> @@ -368,13 +366,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_of_or_by_notation Libnames.loc_of_reference r) + Dumpglob.add_glob ?loc:(loc_of_or_by_notation Libnames.loc_of_reference r) (Smartlocate.smart_global r) with e when CErrors.noncritical e -> ()) occs | Cbv grf | Lazy grf -> List.iter (fun r -> try - Dumpglob.add_glob (loc_of_or_by_notation Libnames.loc_of_reference r) + Dumpglob.add_glob ?loc:(loc_of_or_by_notation Libnames.loc_of_reference r) (Smartlocate.smart_global r) with e when CErrors.noncritical e -> ()) grf.rConst | _ -> () @@ -455,7 +453,7 @@ let rec intern_match_goal_hyps ist ?(as_type=false) lfun = function (* Utilities *) let extract_let_names lrc = let fold accu ((loc, name), _) = - if Id.Set.mem name accu then user_err ~loc + if Id.Set.mem name accu then user_err ?loc ~hdr:"glob_tactic" (str "This variable is bound several times.") else Id.Set.add name accu in @@ -546,7 +544,7 @@ and intern_tactic_seq onlytac ist = function | TacAtom (loc,t) -> let lf = ref ist.ltacvars in let t = intern_atomic lf ist t in - !lf, TacAtom (adjust_loc loc, t) + !lf, TacAtom (Loc.tag ?loc:(adjust_loc loc) t) | TacFun tacfun -> ist.ltacvars, TacFun (intern_tactic_fun ist tacfun) | TacLetIn (isrec,l,u) -> let ltacvars = Id.Set.union (extract_let_names l) ist.ltacvars in @@ -620,12 +618,12 @@ and intern_tactic_seq onlytac ist = function ist.ltacvars, TacSelect (sel, intern_pure_tactic ist tac) (* For extensions *) - | TacAlias (loc,s,l) -> + | TacAlias (loc,(s,l)) -> let l = List.map (intern_tacarg !strict_check false ist) l in - ist.ltacvars, TacAlias (loc,s,l) - | TacML (loc,opn,l) -> + ist.ltacvars, TacAlias (Loc.tag ?loc (s,l)) + | TacML (loc,(opn,l)) -> let _ignore = Tacenv.interp_ml_tactic opn in - ist.ltacvars, TacML (adjust_loc loc,opn,List.map (intern_tacarg !strict_check false ist) l) + ist.ltacvars, TacML (loc, (opn,List.map (intern_tacarg !strict_check false ist) l)) and intern_tactic_as_arg loc onlytac ist a = match intern_tacarg !strict_check onlytac ist a with @@ -633,7 +631,7 @@ and intern_tactic_as_arg loc onlytac ist a = | TacGeneric _ as a -> TacArg (loc,a) | Tacexp a -> a | ConstrMayEval _ | TacFreshId _ | TacPretype _ | TacNumgoals as a -> - if onlytac then error_tactic_expected ~loc else TacArg (loc,a) + if onlytac then error_tactic_expected ?loc else TacArg (loc,a) and intern_tactic_or_tacarg ist = intern_tactic false ist @@ -646,11 +644,11 @@ and intern_tactic_fun ist (var,body) = and intern_tacarg strict onlytac ist = function | Reference r -> intern_non_tactic_reference strict ist r | ConstrMayEval c -> ConstrMayEval (intern_constr_may_eval ist c) - | TacCall (loc,f,[]) -> intern_isolated_tactic_reference strict ist f - | TacCall (loc,f,l) -> - TacCall (loc, + | TacCall (loc,(f,[])) -> intern_isolated_tactic_reference strict ist f + | TacCall (loc,(f,l)) -> + TacCall (Loc.tag ?loc ( intern_applied_tactic_reference ist f, - List.map (intern_tacarg !strict_check false ist) l) + List.map (intern_tacarg !strict_check false ist) l)) | TacFreshId x -> TacFreshId (List.map (intern_string_or_var ist) x) | TacPretype c -> TacPretype (intern_constr ist c) | TacNumgoals -> TacNumgoals diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index ef230348f..8a10a4d76 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -200,8 +200,6 @@ end let print_top_val env v = Pptactic.pr_value Pptactic.ltop v -let dloc = Loc.ghost - let catching_error call_trace fail (e, info) = let inner_trace = Option.default [] (Exninfo.get info ltac_trace_info) @@ -314,7 +312,7 @@ let append_trace trace v = (* Dynamically check that an argument is a tactic *) let coerce_to_tactic loc id v = let v = Value.normalize v in - let fail () = user_err ~loc + let fail () = user_err ?loc (str "Variable " ++ pr_id id ++ str " should be bound to a tactic.") in let v = Value.normalize v in @@ -325,7 +323,7 @@ let coerce_to_tactic loc id v = | _ -> fail () else fail () -let intro_pattern_of_ident id = (Loc.ghost, IntroNaming (IntroIdentifier id)) +let intro_pattern_of_ident id = (Loc.tag @@ IntroNaming (IntroIdentifier id)) let value_of_ident id = in_gen (topwit wit_intro_pattern) (intro_pattern_of_ident id) @@ -369,22 +367,22 @@ let debugging_exception_step ist signal_anomaly e pp = debugging_step ist (fun () -> pp() ++ spc() ++ str "raised the exception" ++ fnl() ++ explain_exc e) -let error_ltac_variable loc id env v s = - user_err ~loc (str "Ltac variable " ++ pr_id id ++ +let error_ltac_variable ?loc id env v s = + user_err ?loc (str "Ltac variable " ++ pr_id id ++ strbrk " is bound to" ++ spc () ++ pr_value env v ++ spc () ++ 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 v = Id.Map.find id ist.lfun in - try coerce v with CannotCoerceTo s -> error_ltac_variable loc id env v s + 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") let interp_ident ist env sigma id = - try try_interp_ltac_var (coerce_var_to_ident false env sigma) ist (Some (env,sigma)) (dloc,id) + try try_interp_ltac_var (coerce_var_to_ident false env sigma) ist (Some (env,sigma)) (Loc.tag id) with Not_found -> id (* Interprets an optional identifier, bound or fresh *) @@ -403,7 +401,7 @@ let interp_intro_pattern_naming_var loc ist env sigma id = let interp_int ist locid = try try_interp_ltac_var coerce_to_int ist None locid with Not_found -> - user_err ~loc:(fst locid) ~hdr:"interp_int" + user_err ?loc:(fst locid) ~hdr:"interp_int" (str "Unbound variable " ++ pr_id (snd locid) ++ str".") let interp_int_or_var ist = function @@ -426,7 +424,7 @@ let interp_hyp ist env sigma (loc,id as locid) = with Not_found -> (* Then look if bound in the proof context at calling time *) if is_variable env id then id - else Loc.raise ~loc (Logic.RefinerError (Logic.NoSuchHyp id)) + else Loc.raise ?loc (Logic.RefinerError (Logic.NoSuchHyp id)) let interp_hyp_list_as_list ist env sigma (loc,id as x) = try coerce_to_hyp_list env sigma (Id.Map.find id ist.lfun) @@ -442,7 +440,7 @@ let interp_reference ist env sigma = function with Not_found -> try VarRef (get_id (Environ.lookup_named id env)) - with Not_found -> error_global_not_found ~loc (qualid_of_ident id) + with Not_found -> error_global_not_found ?loc (qualid_of_ident id) let try_interp_evaluable env (loc, id) = let v = Environ.lookup_named id env in @@ -458,14 +456,14 @@ let interp_evaluable ist env sigma = function with Not_found -> match r with | EvalConstRef _ -> r - | _ -> error_global_not_found ~loc (qualid_of_ident id) + | _ -> 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) with Not_found -> try try_interp_evaluable env (loc, id) - with Not_found -> error_global_not_found ~loc (qualid_of_ident id) + with Not_found -> error_global_not_found ?loc (qualid_of_ident id) (* Interprets an hypothesis name *) let interp_occurrences ist occs = @@ -524,7 +522,7 @@ let extract_ids ids lfun = if has_type v (topwit wit_intro_pattern) then let (_, ipat) = out_gen (topwit wit_intro_pattern) v in if Id.List.mem id ids then accu - else accu @ intropattern_ids (dloc, ipat) + else accu @ intropattern_ids (Loc.tag ipat) else accu in Id.Map.fold fold lfun [] @@ -534,7 +532,7 @@ 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)) (dloc,id) + ist (Some (env,sigma)) (Loc.tag id) with Not_found -> id in let ids = List.map_filter (function ArgVar (_, id) -> Some id | _ -> None) l in let avoid = match TacStore.get ist.extra f_avoid_ids with @@ -692,7 +690,7 @@ let interp_typed_pattern ist env sigma (_,c,_) = let interp_constr_in_compound_list inj_fun dest_fun interp_fun ist env sigma l = let try_expand_ltac_var sigma x = try match dest_fun x with - | GVar (_,id), _ -> + | { CAst.v = GVar id }, _ -> let v = Id.Map.find id ist.lfun in sigma, List.map inj_fun (coerce_to_constr_list env v) | _ -> @@ -734,7 +732,7 @@ let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) = 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) with Not_found -> - error_global_not_found ~loc (qualid_of_ident id)) + error_global_not_found ?loc (qualid_of_ident id)) | Inl (ArgArg _ as b) -> Inl (interp_evaluable ist env sigma b) | Inr c -> Inr (interp_typed_pattern ist env sigma c) in interp_occurrences ist occs, p @@ -792,7 +790,7 @@ let interp_may_eval f ist env sigma = function !evdref , c with | Not_found -> - user_err ~loc ~hdr:"interp_may_eval" + user_err ?loc ~hdr:"interp_may_eval" (str "Unbound context identifier" ++ pr_id s ++ str".")) | ConstrTypeOf c -> let (sigma,c_interp) = f ist env sigma c in @@ -934,7 +932,7 @@ and interp_or_and_intro_pattern ist env sigma = function and interp_intro_pattern_list_as_list ist env sigma = function | [loc,IntroNaming (IntroIdentifier id)] as l -> - (try sigma, coerce_to_intro_pattern_list loc env sigma (Id.Map.find id ist.lfun) + (try sigma, coerce_to_intro_pattern_list ?loc env sigma (Id.Map.find id ist.lfun) with Not_found | CannotCoerceTo _ -> List.fold_map (interp_intro_pattern ist env) sigma l) | l -> List.fold_map (interp_intro_pattern ist env) sigma l @@ -949,7 +947,7 @@ let interp_or_and_intro_pattern_option ist env sigma = function (match coerce_to_intro_pattern env sigma (Id.Map.find id ist.lfun) with | IntroAction (IntroOrAndPattern l) -> sigma, Some (loc,l) | _ -> - user_err ~loc (str "Cannot coerce to a disjunctive/conjunctive pattern.")) + user_err ?loc (str "Cannot coerce to a disjunctive/conjunctive pattern.")) | Some (ArgArg (loc,l)) -> let sigma,l = interp_or_and_intro_pattern ist env sigma l in sigma, Some (loc,l) @@ -970,19 +968,19 @@ let interp_binding_name ist 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 None(dloc,id) + try try_interp_ltac_var (coerce_to_quantified_hypothesis sigma) ist None(Loc.tag 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)) (dloc,id) + (coerce_to_decl_or_quant_hyp env sigma) ist (Some (env,sigma)) (Loc.tag id) with Not_found -> NamedHyp id -let interp_binding ist env sigma (loc,b,c) = +let interp_binding ist env sigma (loc,(b,c)) = let sigma, c = interp_open_constr ist env sigma c in - sigma, (loc,interp_binding_name ist sigma b,c) + sigma, (loc,(interp_binding_name ist sigma b,c)) let interp_bindings ist env sigma = function | NoBindings -> @@ -1005,14 +1003,14 @@ let interp_open_constr_with_bindings ist env sigma (c,bl) = sigma, (c, bl) let loc_of_bindings = function -| NoBindings -> Loc.ghost +| NoBindings -> None | ImplicitBindings l -> loc_of_glob_constr (fst (List.last l)) -| ExplicitBindings l -> pi1 (List.last l) +| ExplicitBindings l -> fst (List.last l) let interp_open_constr_with_bindings_loc ist ((c,_),bl as cb) = let loc1 = loc_of_glob_constr c in let loc2 = loc_of_bindings bl in - let loc = if Loc.is_ghost loc2 then loc1 else Loc.merge loc1 loc2 in + let loc = Loc.merge_opt loc1 loc2 in let f = { delayed = fun env sigma -> let sigma = Sigma.to_evar_map sigma in let (sigma, c) = interp_open_constr_with_bindings ist env sigma cb in @@ -1030,7 +1028,7 @@ let interp_destruction_arg ist gl arg = } | keep,ElimOnAnonHyp n as x -> x | keep,ElimOnIdent (loc,id) -> - let error () = user_err ~loc + let error () = user_err ?loc (strbrk "Cannot coerce " ++ pr_id id ++ strbrk " neither to a quantified hypothesis nor to a term.") in @@ -1041,7 +1039,7 @@ let interp_destruction_arg ist gl arg = (keep, ElimOnConstr { delayed = begin fun env sigma -> try Sigma.here (constr_of_id env id', NoBindings) sigma with Not_found -> - user_err ~loc ~hdr:"interp_destruction_arg" ( + user_err ?loc ~hdr:"interp_destruction_arg" ( pr_id id ++ strbrk " binds to " ++ pr_id id' ++ strbrk " which is neither a declared nor a quantified hypothesis.") end }) in @@ -1067,7 +1065,7 @@ let interp_destruction_arg ist gl arg = if Tactics.is_quantified_hypothesis id gl then keep,ElimOnIdent (loc,id) else - let c = (GVar (loc,id),Some (CRef (Ident (loc,id),None))) in + let c = (CAst.make ?loc @@ GVar id,Some (CAst.make @@ CRef (Ident (loc,id),None))) in let f = { delayed = fun env sigma -> let sigma = Sigma.to_evar_map sigma in let (sigma,c) = interp_open_constr ist env sigma c in @@ -1250,7 +1248,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with eval_tactic ist tac | TacSelect (sel, tac) -> Tacticals.New.tclSELECT sel (interp_tactic ist tac) (* For extensions *) - | TacAlias (loc,s,l) -> + | TacAlias (loc,(s,l)) -> let (ids, body) = Tacenv.interp_alias s in let (>>=) = Ftactic.bind in let interp_vars = Ftactic.List.map (fun v -> interp_tacarg ist v) l in @@ -1281,8 +1279,8 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with in Ftactic.run tac (fun () -> Proofview.tclUNIT ()) - | TacML (loc,opn,l) -> - push_trace (loc,LtacMLCall tac) ist >>= fun trace -> + | TacML (loc,(opn,l)) -> + push_trace (Loc.tag ?loc @@ LtacMLCall tac) ist >>= fun trace -> let ist = { ist with extra = TacStore.set ist.extra f_trace trace; } in let tac = Tacenv.interp_ml_tactic opn in let args = Ftactic.List.map_right (fun a -> interp_tacarg ist a) l in @@ -1301,7 +1299,7 @@ and force_vrec ist v : Val.t Ftactic.t = | v -> Ftactic.return (of_tacvalue v) else Ftactic.return v -and interp_ltac_reference loc' mustbetac ist r : Val.t Ftactic.t = +and interp_ltac_reference ?loc' mustbetac ist r : Val.t Ftactic.t = match r with | ArgVar (loc,id) -> let v = @@ -1315,7 +1313,7 @@ and interp_ltac_reference loc' mustbetac ist r : Val.t Ftactic.t = end | ArgArg (loc,r) -> let ids = extract_ids [] ist.lfun in - let loc_info = ((if Loc.is_ghost loc' then loc else loc'),LtacNameCall r) in + let loc_info = (Option.default loc loc',LtacNameCall r) in let extra = TacStore.set ist.extra f_avoid_ids ids in push_trace loc_info ist >>= fun trace -> let extra = TacStore.set extra f_trace trace in @@ -1326,7 +1324,7 @@ and interp_ltac_reference loc' mustbetac ist r : Val.t Ftactic.t = and interp_tacarg ist arg : Val.t Ftactic.t = match arg with | TacGeneric arg -> interp_genarg ist arg - | Reference r -> interp_ltac_reference dloc false ist r + | Reference r -> interp_ltac_reference false ist r | ConstrMayEval c -> Ftactic.s_enter { s_enter = begin fun gl -> let sigma = project gl in @@ -1334,17 +1332,17 @@ and interp_tacarg ist arg : Val.t Ftactic.t = let (sigma,c_interp) = interp_constr_may_eval ist env sigma c in Sigma.Unsafe.of_pair (Ftactic.return (Value.of_constr c_interp), sigma) end } - | TacCall (loc,r,[]) -> - interp_ltac_reference loc true ist r - | TacCall (loc,f,l) -> + | TacCall (loc,(r,[])) -> + interp_ltac_reference true ist r + | TacCall (loc,(f,l)) -> let (>>=) = Ftactic.bind in - interp_ltac_reference loc true ist f >>= fun fv -> + interp_ltac_reference true ist f >>= fun fv -> Ftactic.List.map (fun a -> interp_tacarg ist a) l >>= fun largs -> interp_app loc ist fv largs | TacFreshId l -> Ftactic.enter { enter = begin fun gl -> let id = interp_fresh_id ist (pf_env gl) (project gl) l in - Ftactic.return (in_gen (topwit wit_intro_pattern) (dloc, IntroNaming (IntroIdentifier id))) + Ftactic.return (in_gen (topwit wit_intro_pattern) (Loc.tag @@ IntroNaming (IntroIdentifier id))) end } | TacPretype c -> Ftactic.s_enter { s_enter = begin fun gl -> @@ -1435,7 +1433,7 @@ 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 ((_, id), b) = - let v = of_tacvalue (VRec (lref, TacArg (dloc, b))) in + let v = of_tacvalue (VRec (lref, TacArg (Loc.tag b))) in Id.Map.add id v accu in let lfun = List.fold_left fold ist.lfun llc in @@ -1761,7 +1759,7 @@ and interp_atomic ist tac : unit Proofview.tactic = (* We try to fully-typecheck the term *) let (sigma,c_interp) = interp_constr ist env sigma c in let let_tac b na c cl eqpat = - let id = Option.default (Loc.ghost,IntroAnonymous) eqpat in + let id = Option.default (Loc.tag IntroAnonymous) eqpat in let with_eq = if b then None else Some (true,id) in Tactics.letin_tac with_eq na c None cl in @@ -1773,7 +1771,7 @@ and interp_atomic ist tac : unit Proofview.tactic = else (* We try to keep the pattern structure as much as possible *) let let_pat_tac b na c cl eqpat = - let id = Option.default (Loc.ghost,IntroAnonymous) eqpat in + let id = Option.default (Loc.tag IntroAnonymous) eqpat in let with_eq = if b then None else Some (true,id) in Tactics.letin_pat_tac with_eq na c cl in @@ -2125,7 +2123,7 @@ let lift_constr_tac_to_ml_tac vars tac = let c = Id.Map.find id ist.lfun in try Some (coerce_to_closed_constr env c) with CannotCoerceTo ty -> - error_ltac_variable Loc.ghost dummy_id (Some (env,sigma)) c ty + error_ltac_variable dummy_id (Some (env,sigma)) c ty in let args = List.map_filter map vars in tac args ist diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index 494f36a95..2ec45312e 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -110,7 +110,7 @@ val interp_int : interp_sign -> Id.t Loc.located -> int val interp_int_or_var : interp_sign -> int or_var -> int -val error_ltac_variable : Loc.t -> Id.t -> +val error_ltac_variable : ?loc:Loc.t -> Id.t -> (Environ.env * Evd.evar_map) option -> value -> string -> 'a (** Transforms a constr-expecting tactic into a tactic finding its arguments in diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index fe3a9f3b2..4390ff08b 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -32,8 +32,8 @@ let subst_glob_constr_and_expr subst (c, e) = let subst_glob_constr = subst_glob_constr_and_expr (* shortening *) -let subst_binding subst (loc,b,c) = - (loc,subst_quantified_hypothesis subst b,subst_glob_constr subst c) +let subst_binding subst (loc,(b,c)) = + (loc,(subst_quantified_hypothesis subst b,subst_glob_constr subst c)) let subst_bindings subst = function | NoBindings -> NoBindings @@ -77,9 +77,7 @@ let subst_or_var f = function | ArgVar _ as x -> x | ArgArg x -> ArgArg (f x) -let dloc = Loc.ghost - -let subst_located f (_loc,id) = (dloc,f id) +let subst_located f = Loc.map f let subst_reference subst = subst_or_var (subst_located (subst_kn subst)) @@ -182,7 +180,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with TacInversion (InversionUsing (subst_glob_constr subst c,cl),hyp) and subst_tactic subst (t:glob_tactic_expr) = match t with - | TacAtom (_loc,t) -> TacAtom (dloc, subst_atomic subst t) + | TacAtom (_loc,t) -> TacAtom (Loc.tag @@ subst_atomic subst t) | TacFun tacfun -> TacFun (subst_tactic_fun subst tacfun) | TacLetIn (r,l,u) -> let l = List.map (fun (n,b) -> (n,subst_tacarg subst b)) l in @@ -229,22 +227,22 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with | TacFirst l -> TacFirst (List.map (subst_tactic subst) l) | TacSolve l -> TacSolve (List.map (subst_tactic subst) l) | TacComplete tac -> TacComplete (subst_tactic subst tac) - | TacArg (_,a) -> TacArg (dloc,subst_tacarg subst a) + | TacArg (_,a) -> TacArg (Loc.tag @@ subst_tacarg subst a) | TacSelect (s, tac) -> TacSelect (s, subst_tactic subst tac) (* For extensions *) - | TacAlias (_,s,l) -> + | TacAlias (_,(s,l)) -> let s = subst_kn subst s in - TacAlias (dloc,s,List.map (subst_tacarg subst) l) - | TacML (_loc,opn,l) -> TacML (dloc,opn,List.map (subst_tacarg subst) l) + TacAlias (Loc.tag (s,List.map (subst_tacarg subst) l)) + | TacML (loc,(opn,l)) -> TacML (loc, (opn,List.map (subst_tacarg subst) l)) and subst_tactic_fun subst (var,body) = (var,subst_tactic subst body) and subst_tacarg subst = function | Reference r -> Reference (subst_reference subst r) | ConstrMayEval c -> ConstrMayEval (subst_raw_may_eval subst c) - | TacCall (_loc,f,l) -> - TacCall (_loc, subst_reference subst f, List.map (subst_tacarg subst) l) + | TacCall (loc,(f,l)) -> + TacCall (Loc.tag ?loc (subst_reference subst f, List.map (subst_tacarg subst) l)) | TacFreshId _ as x -> x | TacPretype c -> TacPretype (subst_glob_constr subst c) | TacNumgoals -> TacNumgoals diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index 84d771bff..294cba4d7 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -365,7 +365,7 @@ let explain_ltac_call_trace last trace loc = Pptactic.pr_glob_tactic (Global.env()) t ++ str ")" | Tacexpr.LtacAtomCall te -> quote (Pptactic.pr_glob_tactic (Global.env()) - (Tacexpr.TacAtom (Loc.ghost,te))) + (Tacexpr.TacAtom (Loc.tag te))) | Tacexpr.LtacConstrInterp (c, { Pretyping.ltac_constrs = vars }) -> quote (Printer.pr_glob_constr_env (Global.env()) c) ++ (if not (Id.Map.is_empty vars) then @@ -400,16 +400,16 @@ let skip_extensions trace = | [] -> [] in List.rev (aux (List.rev trace)) -let finer_loc loc1 loc2 = Loc.merge loc1 loc2 = loc2 +let finer_loc loc1 loc2 = Loc.merge_opt loc1 loc2 = loc2 -let extract_ltac_trace trace eloc = +let extract_ltac_trace ?loc trace = let trace = skip_extensions trace in - let (loc,c),tail = List.sep_last trace in + let (tloc,c),tail = List.sep_last trace in if is_defined_ltac trace then (* We entered a user-defined tactic, we display the trace with location of the call *) - let msg = hov 0 (explain_ltac_call_trace c tail eloc ++ fnl()) in - Some msg, if finer_loc eloc loc then eloc else loc + let msg = hov 0 (explain_ltac_call_trace c tail loc ++ fnl()) in + (if finer_loc loc tloc then loc else tloc), Some msg else (* We entered a primitive tactic, we don't display trace but report on the finest location *) @@ -417,21 +417,21 @@ let extract_ltac_trace trace eloc = (* trace is with innermost call coming first *) let rec aux best_loc = function | (loc,_)::tail -> - if Loc.is_ghost best_loc || - not (Loc.is_ghost loc) && finer_loc loc best_loc + if Option.is_empty best_loc || + not (Option.is_empty loc) && finer_loc loc best_loc then aux loc tail else aux best_loc tail | [] -> best_loc in - aux eloc trace in - None, best_loc + aux loc trace in + best_loc, None let get_ltac_trace (_, info) = let ltac_trace = Exninfo.get info ltac_trace_info in - let loc = Option.default Loc.ghost (Loc.get_loc info) in + let loc = Loc.get_loc info in match ltac_trace with | None -> None - | Some trace -> Some (extract_ltac_trace trace loc) + | Some trace -> Some (extract_ltac_trace ?loc trace) let () = ExplainErr.register_additional_error_info get_ltac_trace diff --git a/plugins/ltac/tactic_debug.mli b/plugins/ltac/tactic_debug.mli index 0b4d35a22..ac35464c4 100644 --- a/plugins/ltac/tactic_debug.mli +++ b/plugins/ltac/tactic_debug.mli @@ -77,4 +77,4 @@ val db_breakpoint : debug_info -> Id.t Loc.located message_token list -> unit Proofview.NonLogical.t val extract_ltac_trace : - Tacexpr.ltac_trace -> Loc.t -> Pp.std_ppcmds option * Loc.t + ?loc:Loc.t -> Tacexpr.ltac_trace -> Pp.std_ppcmds option Loc.located diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml index c7be99616..4ec111e01 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -86,7 +86,6 @@ let _ = (** Base tactics *) -let loc = Loc.ghost let idtac = Proofview.tclUNIT () let fail = Proofview.tclINDEPENDENT (tclFAIL 0 (Pp.mt ())) @@ -204,7 +203,7 @@ let u_iff = make_unfold "iff" let u_not = make_unfold "not" let reduction_not_iff _ ist = - let make_reduce c = TacAtom (loc, TacReduce (Genredexpr.Unfold c, Locusops.allHypsAndConcl)) in + let make_reduce c = TacAtom (Loc.tag @@ TacReduce (Genredexpr.Unfold c, Locusops.allHypsAndConcl)) in let tac = match !negation_unfolding, unfold_iff () with | true, true -> make_reduce [u_not; u_iff] | true, false -> make_reduce [u_not] @@ -257,11 +256,11 @@ let tauto_power_flags = { } let with_flags flags _ ist = - let f = (loc, Id.of_string "f") in - let x = (loc, Id.of_string "x") in + let f = (Loc.tag @@ Id.of_string "f") in + let x = (Loc.tag @@ 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 - eval_tactic_ist ist (TacArg (loc, TacCall (loc, ArgVar f, [Reference (ArgVar x)]))) + eval_tactic_ist ist (TacArg (Loc.tag @@ TacCall (Loc.tag (ArgVar f, [Reference (ArgVar x)])))) let register_tauto_tactic tac name0 args = let ids = List.map (fun id -> Id.of_string id) args in @@ -269,7 +268,7 @@ let register_tauto_tactic tac name0 args = let name = { mltac_plugin = tauto_plugin; mltac_tactic = name0; } in let entry = { mltac_name = name; mltac_index = 0 } in let () = Tacenv.register_ml_tactic name [| tac |] in - let tac = TacFun (ids, TacML (loc, entry, [])) in + let tac = TacFun (ids, TacML (Loc.tag (entry, []))) in let obj () = Tacenv.register_ltac true true (Id.of_string name0) tac in Mltop.declare_cache_obj obj tauto_plugin diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 012db04a6..053bb6fa1 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -1992,7 +1992,7 @@ let micromega_gen let intro_vars = Tacticals.New.tclTHENLIST (List.map intro vars) in let intro_props = Tacticals.New.tclTHENLIST (List.map intro props) in - let ipat_of_name id = Some (Loc.ghost, Misctypes.IntroNaming (Misctypes.IntroIdentifier id)) in + let ipat_of_name id = Some (Loc.tag @@ Misctypes.IntroNaming (Misctypes.IntroIdentifier id)) in let goal_name = fresh_id [] (Names.Id.of_string "__arith") gl in let env' = List.map (fun (id,i) -> Term.mkVar id,i) vars in @@ -2107,7 +2107,7 @@ let micromega_genr prover tac = let intro_vars = Tacticals.New.tclTHENLIST (List.map intro vars) in let intro_props = Tacticals.New.tclTHENLIST (List.map intro props) in - let ipat_of_name id = Some (Loc.ghost, Misctypes.IntroNaming (Misctypes.IntroIdentifier id)) in + let ipat_of_name id = Some (Loc.tag @@ Misctypes.IntroNaming (Misctypes.IntroIdentifier id)) in let goal_name = fresh_id [] (Names.Id.of_string "__arith") gl in let env' = List.map (fun (id,i) -> Term.mkVar id,i) vars in diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4 index 6c3e66112..980f03db3 100644 --- a/plugins/quote/g_quote.ml4 +++ b/plugins/quote/g_quote.ml4 @@ -19,15 +19,14 @@ open Tacarg DECLARE PLUGIN "quote_plugin" -let loc = Loc.ghost let cont = Id.of_string "cont" 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, ArgVar (loc, cont), [Reference (ArgVar (loc, x))]) in + let tac = TacCall (Loc.tag (ArgVar (Loc.tag cont), [Reference (ArgVar (Loc.tag 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, tac)) + Tacinterp.eval_tactic_ist ist (TacArg (Loc.tag tac)) TACTIC EXTEND quote [ "quote" ident(f) ] -> [ quote f [] ] diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 6b8ef630a..e20e78b1a 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -127,11 +127,11 @@ let closed_term_ast l = mltac_name = tacname; mltac_index = 0; } in - let l = List.map (fun gr -> ArgArg(Loc.ghost,gr)) l in + let l = List.map (fun gr -> ArgArg(Loc.tag gr)) l in TacFun([Name(Id.of_string"t")], - TacML(Loc.ghost,tacname, - [TacGeneric (Genarg.in_gen (Genarg.glbwit Stdarg.wit_constr) (GVar(Loc.ghost,Id.of_string"t"),None)); - TacGeneric (Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Stdarg.wit_ref)) l)])) + TacML(Loc.tag (tacname, + [TacGeneric (Genarg.in_gen (Genarg.glbwit Stdarg.wit_constr) (CAst.make @@ GVar(Id.of_string"t"),None)); + TacGeneric (Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Stdarg.wit_ref)) l)]))) (* let _ = add_tacdef false ((Loc.ghost,Id.of_string"ring_closed_term" *) @@ -160,16 +160,16 @@ let decl_constant na ctx c = (* Calling a global tactic *) let ltac_call tac (args:glob_tactic_arg list) = - TacArg(Loc.ghost,TacCall(Loc.ghost, ArgArg(Loc.ghost, Lazy.force tac),args)) + TacArg(Loc.tag @@ TacCall (Loc.tag (ArgArg(Loc.tag @@ Lazy.force tac),args))) (* Calling a locally bound tactic *) let ltac_lcall tac args = - TacArg(Loc.ghost,TacCall(Loc.ghost, ArgVar(Loc.ghost, Id.of_string tac),args)) + TacArg(Loc.tag @@ TacCall (Loc.tag (ArgVar(Loc.tag @@ 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.ghost, id)) in + let x = Reference (ArgVar (Loc.tag 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 @@ -204,7 +204,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.ghost, id)) in + let x = Reference (ArgVar (Loc.tag 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 @@ -212,7 +212,7 @@ let exec_tactic env evd n f args = (** Build the getter *) let lid = List.init n (fun i -> Id.of_string("x"^string_of_int i)) in let n = Genarg.in_gen (Genarg.glbwit Stdarg.wit_int) n in - let get_res = TacML (Loc.ghost, get_res, [TacGeneric n]) in + let get_res = TacML (Loc.tag (get_res, [TacGeneric n])) in let getter = Tacexp (TacFun (List.map (fun n -> Name n) lid, get_res)) in (** Evaluate the whole result *) let gl = dummy_goal env evd in @@ -577,8 +577,8 @@ let interp_cst_tac env sigma rk kind (zero,one,add,mul,opp) cst_tac = | Some (Closed lc) -> closed_term_ast (List.map Smartlocate.global_with_alias lc) | None -> - let t = ArgArg(Loc.ghost,Lazy.force ltac_inv_morph_nothing) in - TacArg(Loc.ghost,TacCall(Loc.ghost,t,[])) + let t = ArgArg(Loc.tag @@ Lazy.force ltac_inv_morph_nothing) in + TacArg(Loc.tag (TacCall(Loc.tag (t,[])))) let make_hyp env evd c = let t = Retyping.get_type_of env !evd c in @@ -599,8 +599,8 @@ let interp_power env evd pow = let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in match pow with | None -> - let t = ArgArg(Loc.ghost, Lazy.force ltac_inv_morph_nothing) in - (TacArg(Loc.ghost,TacCall(Loc.ghost,t,[])), plapp evd coq_None [|carrier|]) + let t = ArgArg(Loc.tag (Lazy.force ltac_inv_morph_nothing)) in + (TacArg(Loc.tag (TacCall(Loc.tag (t,[])))), plapp evd coq_None [|carrier|]) | Some (tac, spec) -> let tac = match tac with diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index edf934c7d..862e44cca 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -48,9 +48,8 @@ open Constrexpr_ops DECLARE PLUGIN "ssrmatching_plugin" -let dummy_loc = Loc.ghost let errorstrm = CErrors.user_err ~hdr:"ssrmatching" -let loc_error loc msg = CErrors.user_err ~loc ~hdr:msg (str msg) +let loc_error loc msg = CErrors.user_err ?loc ~hdr:msg (str msg) let ppnl = Feedback.msg_info (* 0 cost pp function. Active only if env variable SSRDEBUG is set *) @@ -132,20 +131,20 @@ let add_genarg tag pr = (** Constructors for cast type *) let dC t = CastConv t (** Constructors for constr_expr *) -let isCVar = function CRef (Ident _, _) -> true | _ -> false -let destCVar = function CRef (Ident (_, id), _) -> id | _ -> +let isCVar = function { CAst.v = CRef (Ident _, _) } -> true | _ -> false +let destCVar = function { CAst.v = CRef (Ident (_, id), _) } -> id | _ -> CErrors.anomaly (str"not a CRef") -let mkCHole loc = CHole (loc, None, IntroAnonymous, None) -let mkCLambda loc name ty t = - CLambdaN (loc, [[loc, name], Default Explicit, ty], t) -let mkCLetIn loc name bo t = - CLetIn (loc, (loc, name), bo, None, t) -let mkCCast loc t ty = CCast (loc,t, dC ty) +let mkCHole ~loc = CAst.make ?loc @@ CHole (None, IntroAnonymous, None) +let mkCLambda ?loc name ty t = CAst.make ?loc @@ + CLambdaN ([[Loc.tag ?loc name], Default Explicit, ty], t) +let mkCLetIn ?loc name bo t = CAst.make ?loc @@ + CLetIn ((Loc.tag ?loc name), bo, None, t) +let mkCCast ?loc t ty = CAst.make ?loc @@ CCast (t, dC ty) (** Constructors for rawconstr *) -let mkRHole = GHole (dummy_loc, InternalHole, IntroAnonymous, None) -let mkRApp f args = if args = [] then f else GApp (dummy_loc, f, args) -let mkRCast rc rt = GCast (dummy_loc, rc, dC rt) -let mkRLambda n s t = GLambda (dummy_loc, n, Explicit, s, t) +let mkRHole = CAst.make @@ GHole (InternalHole, IntroAnonymous, None) +let mkRApp f args = if args = [] then f else CAst.make @@ GApp (f, args) +let mkRCast rc rt = CAst.make @@ GCast (rc, dC rt) +let mkRLambda n s t = CAst.make @@ GLambda (n, Explicit, s, t) (* ssrterm conbinators *) let combineCG t1 t2 f g = match t1, t2 with @@ -906,16 +905,16 @@ let glob_cpattern gs p = let name = Name (id_of_string ("_ssrpat_" ^ s)) in k, (mkRCast mkRHole (mkRLambda name mkRHole (mkRApp mkRHole l)), None) in let bind_in t1 t2 = - let d = dummy_loc in let n = Name (destCVar t1) in - fst (glob (mkCCast d (mkCHole d) (mkCLambda d n (mkCHole d) t2))) in + let mkCHole = mkCHole ~loc:None in let n = Name (destCVar t1) in + fst (glob (mkCCast mkCHole (mkCLambda n mkCHole t2))) in let check_var t2 = if not (isCVar t2) then loc_error (constr_loc t2) "Only identifiers are allowed here" in match p with | _, (_, None) as x -> x | k, (v, Some t) as orig -> if k = 'x' then glob_ssrterm gs ('(', (v, Some t)) else - match t with - | CNotation(_, "( _ in _ )", ([t1; t2], [], [])) -> + match t.CAst.v with + | CNotation("( _ in _ )", ([t1; t2], [], [])) -> (try match glob t1, glob t2 with | (r1, None), (r2, None) -> encode k "In" [r1;r2] | (r1, Some _), (r2, Some _) when isCVar t1 -> @@ -923,11 +922,11 @@ let glob_cpattern gs p = | (r1, Some _), (r2, Some _) -> encode k "In" [r1; r2] | _ -> CErrors.anomaly (str"where are we?") with _ when isCVar t1 -> encode k "In" [bind_in t1 t2]) - | CNotation(_, "( _ in _ in _ )", ([t1; t2; t3], [], [])) -> + | CNotation("( _ in _ in _ )", ([t1; t2; t3], [], [])) -> check_var t2; encode k "In" [fst (glob t1); bind_in t2 t3] - | CNotation(_, "( _ as _ )", ([t1; t2], [], [])) -> + | CNotation("( _ as _ )", ([t1; t2], [], [])) -> encode k "As" [fst (glob t1); fst (glob t2)] - | CNotation(_, "( _ as _ in _ )", ([t1; t2; t3], [], [])) -> + | CNotation("( _ as _ in _ )", ([t1; t2; t3], [], [])) -> check_var t2; encode k "As" [fst (glob t1); bind_in t2 t3] | _ -> glob_ssrterm gs orig ;; @@ -982,10 +981,10 @@ let pr_rpattern = pr_pattern type pattern = Evd.evar_map * (constr, constr) ssrpattern -let id_of_cpattern = function - | _,(_,Some (CRef (Ident (_, x), _))) -> Some x - | _,(_,Some (CAppExpl (_, (_, Ident (_, x), _), []))) -> Some x - | _,(GRef (_, VarRef x, _) ,None) -> Some x +let id_of_cpattern = let open CAst in function + | _,(_,Some { v = CRef (Ident (_, x), _) } ) -> Some x + | _,(_,Some { v = CAppExpl ((_, Ident (_, x), _), []) } ) -> Some x + | _,({ v = GRef (VarRef x, _)} ,None) -> Some x | _ -> None let id_of_Cterm t = match id_of_cpattern t with | Some x -> x @@ -1033,7 +1032,7 @@ GEXTEND Gram GLOBAL: cpattern; cpattern: [[ k = ssrtermkind; c = constr -> let pattern = mk_term k c in - if loc_ofCG pattern <> !@loc && k = '(' then mk_term 'x' c else pattern ]]; + if loc_ofCG pattern <> Some !@loc && k = '(' then mk_term 'x' c else pattern ]]; END ARGUMENT EXTEND lcpattern @@ -1050,7 +1049,7 @@ GEXTEND Gram GLOBAL: lcpattern; lcpattern: [[ k = ssrtermkind; c = lconstr -> let pattern = mk_term k c in - if loc_ofCG pattern <> !@loc && k = '(' then mk_term 'x' c else pattern ]]; + if loc_ofCG pattern <> Some !@loc && k = '(' then mk_term 'x' c else pattern ]]; END let thin id sigma goal = @@ -1083,9 +1082,10 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty = let eAsXInT e x t = E_As_X_In_T(e,x,t) in let mkG ?(k=' ') x = k,(x,None) in let decode ist t ?reccall f g = + let open CAst in try match (pf_intern_term ist gl t) with - | GCast(_,GHole _,CastConv(GLambda(_,Name x,_,_,c))) -> f x (' ',(c,None)) - | GVar(_,id) + | { v = GCast({ v = GHole _},CastConv({ v = GLambda(Name x,_,_,c)})) } -> f x (' ',(c,None)) + | { v = GVar id } when Id.Map.mem id ist.lfun && not(Option.is_empty reccall) && not(Option.is_empty wit_ssrpatternarg) -> @@ -1126,18 +1126,18 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty = thin name sigma e) sigma new_evars in sigma in - let red = let rec decode_red (ist,red) = match red with - | T(k,(GCast (_,GHole _,(CastConv(GLambda (_,Name id,_,_,t)))),None)) + let red = let rec decode_red (ist,red) = let open CAst in match red with + | T(k,({ v = GCast ({ v = GHole _ },CastConv({ v = GLambda (Name id,_,_,t)}))},None)) when let id = string_of_id id in let len = String.length id in (len > 8 && String.sub id 0 8 = "_ssrpat_") -> let id = string_of_id id in let len = String.length id in (match String.sub id 8 (len - 8), t with - | "In", GApp(_, _, [t]) -> decodeG t xInT (fun x -> T x) - | "In", GApp(_, _, [e; t]) -> decodeG t (eInXInT (mkG e)) (bad_enc id) - | "In", GApp(_, _, [e; t; e_in_t]) -> + | "In", { v = GApp( _, [t]) } -> decodeG t xInT (fun x -> T x) + | "In", { v = GApp( _, [e; t]) } -> decodeG t (eInXInT (mkG e)) (bad_enc id) + | "In", { v = GApp( _, [e; t; e_in_t]) } -> decodeG t (eInXInT (mkG e)) (fun _ -> decodeG e_in_t xInT (fun _ -> assert false)) - | "As", GApp(_, _, [e; t]) -> decodeG t (eAsXInT (mkG e)) (bad_enc id) + | "As", { v = GApp(_, [e; t]) } -> decodeG t (eAsXInT (mkG e)) (bad_enc id) | _ -> bad_enc id ()) | T t -> decode ist ~reccall:decode_red t xInT (fun x -> T x) | In_T t -> decode ist t inXInT inT @@ -1149,27 +1149,27 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty = pp(lazy(str"decoded as: " ++ pr_pattern_w_ids red)); let red = match redty with None -> red | Some ty -> let ty = ' ', ty in match red with - | T t -> T (combineCG t ty (mkCCast (loc_ofCG t)) mkRCast) + | T t -> T (combineCG t ty (mkCCast ?loc:(loc_ofCG t)) mkRCast) | X_In_T (x,t) -> let ty = pf_intern_term ist gl ty in E_As_X_In_T (mkG (mkRCast mkRHole ty), x, t) | E_In_X_In_T (e,x,t) -> let ty = mkG (pf_intern_term ist gl ty) in - E_In_X_In_T (combineCG e ty (mkCCast (loc_ofCG t)) mkRCast, x, t) + E_In_X_In_T (combineCG e ty (mkCCast ?loc:(loc_ofCG t)) mkRCast, x, t) | E_As_X_In_T (e,x,t) -> let ty = mkG (pf_intern_term ist gl ty) in - E_As_X_In_T (combineCG e ty (mkCCast (loc_ofCG t)) mkRCast, x, t) + E_As_X_In_T (combineCG e ty (mkCCast ?loc:(loc_ofCG t)) mkRCast, x, t) | red -> red in pp(lazy(str"typed as: " ++ pr_pattern_w_ids red)); - let mkXLetIn loc x (a,(g,c)) = match c with - | Some b -> a,(g,Some (mkCLetIn loc x (mkCHole loc) b)) - | None -> a,(GLetIn (loc,x,(GHole (loc, BinderType x, IntroAnonymous, None)), None, g), None) in + let mkXLetIn ?loc x (a,(g,c)) = match c with + | Some b -> a,(g,Some (mkCLetIn ?loc x (mkCHole ~loc) b)) + | None -> a,(CAst.make ?loc @@ GLetIn (x, CAst.make ?loc @@ GHole (BinderType x, IntroAnonymous, None), None, g), None) in match red with | T t -> let sigma, t = interp_term ist gl t in sigma, T t | In_T t -> let sigma, t = interp_term ist gl t in sigma, In_T t | X_In_T (x, rp) | In_X_In_T (x, rp) -> let mk x p = match red with X_In_T _ -> X_In_T(x,p) | _ -> In_X_In_T(x,p) in - let rp = mkXLetIn dummy_loc (Name x) rp in + let rp = mkXLetIn (Name x) rp in let sigma, rp = interp_term ist gl rp in let _, h, _, rp = destLetIn rp in let sigma = cleanup_XinE h x rp sigma in @@ -1178,7 +1178,7 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty = | E_In_X_In_T(e, x, rp) | E_As_X_In_T (e, x, rp) -> let mk e x p = match red with E_In_X_In_T _ ->E_In_X_In_T(e,x,p)|_->E_As_X_In_T(e,x,p) in - let rp = mkXLetIn dummy_loc (Name x) rp in + let rp = mkXLetIn (Name x) rp in let sigma, rp = interp_term ist gl rp in let _, h, _, rp = destLetIn rp in let sigma = cleanup_XinE h x rp sigma in @@ -1336,10 +1336,10 @@ let pf_fill_occ_term gl occ t = let cl,(_,t) = fill_occ_term env concl occ sigma0 t in cl, t -let cpattern_of_id id = ' ', (GRef (dummy_loc, VarRef id, None), None) +let cpattern_of_id id = ' ', (CAst.make @@ GRef (VarRef id, None), None) -let is_wildcard = function - | _,(_,Some (CHole _)|GHole _,None) -> true +let is_wildcard : cpattern -> bool = function + | _,(_,Some { CAst.v = CHole _ } | { CAst.v = GHole _ } ,None) -> true | _ -> false (* "ssrpattern" *) @@ -1388,7 +1388,7 @@ let () = let () = Tacenv.register_ml_tactic name [|mltac|] in let tac = TacFun ([Name (Id.of_string "pattern")], - TacML (Loc.ghost, { mltac_name = name; mltac_index = 0 }, [])) in + TacML (Loc.tag ({ mltac_name = name; mltac_index = 0 }, []))) in let obj () = Tacenv.register_ltac true false (Id.of_string "ssrpattern") tac in Mltop.declare_cache_obj obj "ssrmatching_plugin" diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index 638b4e254..8be989de5 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -221,7 +221,7 @@ val pf_unify_HO : goal sigma -> EConstr.constr -> EConstr.constr -> goal sigma (** Some more low level functions needed to implement the full SSR language on top of the former APIs *) val tag_of_cpattern : cpattern -> char -val loc_of_cpattern : cpattern -> Loc.t +val loc_of_cpattern : cpattern -> Loc.t option val id_of_pattern : pattern -> Names.variable option val is_wildcard : cpattern -> bool val cpattern_of_id : Names.variable -> cpattern diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml index ed8cc6ab0..e7eea0284 100644 --- a/plugins/syntax/ascii_syntax.ml +++ b/plugins/syntax/ascii_syntax.ml @@ -37,34 +37,34 @@ let glob_Ascii = lazy (make_reference "Ascii") open Lazy -let interp_ascii dloc p = +let interp_ascii ?loc p = let rec aux n p = if Int.equal n 0 then [] else let mp = p mod 2 in - GRef (dloc,(if Int.equal mp 0 then glob_false else glob_true),None) + (CAst.make ?loc @@ GRef ((if Int.equal mp 0 then glob_false else glob_true),None)) :: (aux (n-1) (p/2)) in - GApp (dloc,GRef(dloc,force glob_Ascii,None), aux 8 p) + CAst.make ?loc @@ GApp (CAst.make ?loc @@ GRef(force glob_Ascii,None), aux 8 p) -let interp_ascii_string dloc s = +let interp_ascii_string ?loc s = let p = if Int.equal (String.length s) 1 then int_of_char s.[0] else if Int.equal (String.length s) 3 && is_digit s.[0] && is_digit s.[1] && is_digit s.[2] then int_of_string s else - user_err ~loc:dloc ~hdr:"interp_ascii_string" + user_err ?loc ~hdr:"interp_ascii_string" (str "Expects a single character or a three-digits ascii code.") in - interp_ascii dloc p + interp_ascii ?loc p let uninterp_ascii r = let rec uninterp_bool_list n = function | [] when Int.equal n 0 -> 0 - | GRef (_,k,_)::l when Globnames.eq_gr k glob_true -> 1+2*(uninterp_bool_list (n-1) l) - | GRef (_,k,_)::l when Globnames.eq_gr k glob_false -> 2*(uninterp_bool_list (n-1) l) + | { CAst.v = GRef (k,_)}::l when Globnames.eq_gr k glob_true -> 1+2*(uninterp_bool_list (n-1) l) + | { CAst.v = GRef (k,_)}::l when Globnames.eq_gr k glob_false -> 2*(uninterp_bool_list (n-1) l) | _ -> raise Non_closed_ascii in try let aux = function - | GApp (_,GRef (_,k,_),l) when Globnames.eq_gr k (force glob_Ascii) -> uninterp_bool_list 8 l + | { CAst.v = GApp ({ CAst.v = GRef (k,_)},l) } when Globnames.eq_gr k (force glob_Ascii) -> uninterp_bool_list 8 l | _ -> raise Non_closed_ascii in Some (aux r) with @@ -80,4 +80,4 @@ let _ = Notation.declare_string_interpreter "char_scope" (ascii_path,ascii_module) interp_ascii_string - ([GRef (Loc.ghost,static_glob_Ascii,None)], uninterp_ascii_string, true) + ([CAst.make @@ GRef (static_glob_Ascii,None)], uninterp_ascii_string, true) diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml index ab262fea7..9a4cd6c25 100644 --- a/plugins/syntax/nat_syntax.ml +++ b/plugins/syntax/nat_syntax.ml @@ -33,21 +33,21 @@ let warn_large_nat = strbrk "may vary from 5000 to 70000 depending on your system " ++ strbrk "limits and on the command executed).") -let nat_of_int dloc n = +let nat_of_int ?loc n = if is_pos_or_zero n then begin if less_than threshold n then warn_large_nat (); - let ref_O = GRef (dloc, glob_O, None) in - let ref_S = GRef (dloc, glob_S, None) in + let ref_O = CAst.make ?loc @@ GRef (glob_O, None) in + let ref_S = CAst.make ?loc @@ GRef (glob_S, None) in let rec mk_nat acc n = if n <> zero then - mk_nat (GApp (dloc,ref_S, [acc])) (sub_1 n) + mk_nat (CAst.make ?loc @@ GApp (ref_S, [acc])) (sub_1 n) else acc in mk_nat ref_O n end else - user_err ~hdr:"nat_of_int" + user_err ?loc ~hdr:"nat_of_int" (str "Cannot interpret a negative number as a number of type nat") (************************************************************************) @@ -55,10 +55,11 @@ let nat_of_int dloc n = exception Non_closed_number -let rec int_of_nat = function - | GApp (_,GRef (_,s,_),[a]) when Globnames.eq_gr s glob_S -> add_1 (int_of_nat a) - | GRef (_,z,_) when Globnames.eq_gr z glob_O -> zero +let rec int_of_nat x = CAst.with_val (function + | GApp ({ CAst.v = GRef (s,_) } ,[a]) when Globnames.eq_gr s glob_S -> add_1 (int_of_nat a) + | GRef (z,_) when Globnames.eq_gr z glob_O -> zero | _ -> raise Non_closed_number + ) x let uninterp_nat p = try @@ -73,4 +74,4 @@ let _ = Notation.declare_numeral_interpreter "nat_scope" (nat_path,datatypes_module_name) nat_of_int - ([GRef (Loc.ghost,glob_S,None); GRef (Loc.ghost,glob_O,None)], uninterp_nat, true) + ([CAst.make @@ GRef (glob_S,None); CAst.make @@ GRef (glob_O,None)], uninterp_nat, true) diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml index a25ddb062..e23852bf8 100644 --- a/plugins/syntax/numbers_syntax.ml +++ b/plugins/syntax/numbers_syntax.ml @@ -86,10 +86,10 @@ exception Non_closed (* parses a *non-negative* integer (from bigint.ml) into an int31 wraps modulo 2^31 *) -let int31_of_pos_bigint dloc n = - let ref_construct = GRef (dloc, int31_construct, None) in - let ref_0 = GRef (dloc, int31_0, None) in - let ref_1 = GRef (dloc, int31_1, None) in +let int31_of_pos_bigint ?loc n = + let ref_construct = CAst.make ?loc @@ GRef (int31_construct, None) in + let ref_0 = CAst.make ?loc @@ GRef (int31_0, None) in + let ref_1 = CAst.make ?loc @@ GRef (int31_1, None) in let rec args counter n = if counter <= 0 then [] @@ -97,16 +97,16 @@ let int31_of_pos_bigint dloc n = let (q,r) = div2_with_rest n in (if r then ref_1 else ref_0)::(args (counter-1) q) in - GApp (dloc, ref_construct, List.rev (args 31 n)) + CAst.make ?loc @@ GApp (ref_construct, List.rev (args 31 n)) -let error_negative dloc = - CErrors.user_err ~loc:dloc ~hdr:"interp_int31" (Pp.str "int31 are only non-negative numbers.") +let error_negative ?loc = + CErrors.user_err ?loc ~hdr:"interp_int31" (Pp.str "int31 are only non-negative numbers.") -let interp_int31 dloc n = +let interp_int31 ?loc n = if is_pos_or_zero n then - int31_of_pos_bigint dloc n + int31_of_pos_bigint ?loc n else - error_negative dloc + error_negative ?loc (* Pretty prints an int31 *) @@ -114,12 +114,12 @@ let bigint_of_int31 = let rec args_parsing args cur = match args with | [] -> cur - | (GRef (_,b,_))::l when eq_gr b int31_0 -> args_parsing l (mult_2 cur) - | (GRef (_,b,_))::l when eq_gr b int31_1 -> args_parsing l (add_1 (mult_2 cur)) + | { CAst.v = GRef (b,_) }::l when eq_gr b int31_0 -> args_parsing l (mult_2 cur) + | { CAst.v = GRef (b,_) }::l when eq_gr b int31_1 -> args_parsing l (add_1 (mult_2 cur)) | _ -> raise Non_closed in function - | GApp (_, GRef (_, c, _), args) when eq_gr c int31_construct -> args_parsing args zero + | { CAst.v = GApp ({ CAst.v = GRef (c, _)}, args) } when eq_gr c int31_construct -> args_parsing args zero | _ -> raise Non_closed let uninterp_int31 i = @@ -132,7 +132,7 @@ let uninterp_int31 i = let _ = Notation.declare_numeral_interpreter int31_scope (int31_path, int31_module) interp_int31 - ([GRef (Loc.ghost, int31_construct, None)], + ([CAst.make @@ GRef (int31_construct, None)], uninterp_int31, true) @@ -162,40 +162,40 @@ let height bi = in hght 0 base (* n must be a non-negative integer (from bigint.ml) *) -let word_of_pos_bigint dloc hght n = - let ref_W0 = GRef (dloc, zn2z_W0, None) in - let ref_WW = GRef (dloc, zn2z_WW, None) in +let word_of_pos_bigint ?loc hght n = + let ref_W0 = CAst.make ?loc @@ GRef (zn2z_W0, None) in + let ref_WW = CAst.make ?loc @@ GRef (zn2z_WW, None) in let rec decomp hgt n = if hgt <= 0 then - int31_of_pos_bigint dloc n + int31_of_pos_bigint ?loc n else if equal n zero then - GApp (dloc, ref_W0, [GHole (dloc, Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None)]) + CAst.make ?loc @@ GApp (ref_W0, [CAst.make ?loc @@ GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None)]) else let (h,l) = split_at hgt n in - GApp (dloc, ref_WW, [GHole (dloc, Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None); + CAst.make ?loc @@ GApp (ref_WW, [CAst.make ?loc @@ GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None); decomp (hgt-1) h; decomp (hgt-1) l]) in decomp hght n -let bigN_of_pos_bigint dloc n = +let bigN_of_pos_bigint ?loc n = let h = height n in - let ref_constructor = GRef (dloc, bigN_constructor h, None) in - let word = word_of_pos_bigint dloc h n in + let ref_constructor = CAst.make ?loc @@ GRef (bigN_constructor h, None) in + let word = word_of_pos_bigint ?loc h n in let args = if h < n_inlined then [word] - else [Nat_syntax_plugin.Nat_syntax.nat_of_int dloc (of_int (h-n_inlined));word] + else [Nat_syntax_plugin.Nat_syntax.nat_of_int ?loc (of_int (h-n_inlined));word] in - GApp (dloc, ref_constructor, args) + CAst.make ?loc @@ GApp (ref_constructor, args) -let bigN_error_negative dloc = - CErrors.user_err ~loc:dloc ~hdr:"interp_bigN" (Pp.str "bigN are only non-negative numbers.") +let bigN_error_negative ?loc = + CErrors.user_err ?loc ~hdr:"interp_bigN" (Pp.str "bigN are only non-negative numbers.") -let interp_bigN dloc n = +let interp_bigN ?loc n = if is_pos_or_zero n then - bigN_of_pos_bigint dloc n + bigN_of_pos_bigint ?loc n else - bigN_error_negative dloc + bigN_error_negative ?loc (* Pretty prints a bigN *) @@ -203,14 +203,14 @@ let interp_bigN dloc n = let bigint_of_word = let rec get_height rc = match rc with - | GApp (_,GRef(_,c,_), [_;lft;rght]) when eq_gr c zn2z_WW -> + | { CAst.v = GApp ({ CAst.v = GRef(c,_)}, [_;lft;rght]) } when eq_gr c zn2z_WW -> 1+max (get_height lft) (get_height rght) | _ -> 0 in let rec transform hght rc = match rc with - | GApp (_,GRef(_,c,_),_) when eq_gr c zn2z_W0-> zero - | GApp (_,GRef(_,c,_), [_;lft;rght]) when eq_gr c zn2z_WW-> + | { CAst.v = GApp ({ CAst.v = GRef(c,_)},_)} when eq_gr c zn2z_W0-> zero + | { CAst.v = GApp ({ CAst.v = GRef(c,_)}, [_;lft;rght]) } when eq_gr c zn2z_WW-> let new_hght = hght-1 in add (mult (rank new_hght) (transform new_hght lft)) @@ -223,8 +223,8 @@ let bigint_of_word = let bigint_of_bigN rc = match rc with - | GApp (_,_,[one_arg]) -> bigint_of_word one_arg - | GApp (_,_,[_;second_arg]) -> bigint_of_word second_arg + | { CAst.v = GApp (_,[one_arg]) } -> bigint_of_word one_arg + | { CAst.v = GApp (_,[_;second_arg]) } -> bigint_of_word second_arg | _ -> raise Non_closed let uninterp_bigN rc = @@ -240,7 +240,7 @@ let uninterp_bigN rc = let bigN_list_of_constructors = let rec build i = if i < n_inlined+1 then - GRef (Loc.ghost, bigN_constructor i,None)::(build (i+1)) + (CAst.make @@ GRef (bigN_constructor i,None))::(build (i+1)) else [] in @@ -256,18 +256,18 @@ let _ = Notation.declare_numeral_interpreter bigN_scope (*** Parsing for bigZ in digital notation ***) -let interp_bigZ dloc n = - let ref_pos = GRef (dloc, bigZ_pos, None) in - let ref_neg = GRef (dloc, bigZ_neg, None) in +let interp_bigZ ?loc n = + let ref_pos = CAst.make ?loc @@ GRef (bigZ_pos, None) in + let ref_neg = CAst.make ?loc @@ GRef (bigZ_neg, None) in if is_pos_or_zero n then - GApp (dloc, ref_pos, [bigN_of_pos_bigint dloc n]) + CAst.make ?loc @@ GApp (ref_pos, [bigN_of_pos_bigint ?loc n]) else - GApp (dloc, ref_neg, [bigN_of_pos_bigint dloc (neg n)]) + CAst.make ?loc @@ GApp (ref_neg, [bigN_of_pos_bigint ?loc (neg n)]) (* pretty printing functions for bigZ *) let bigint_of_bigZ = function - | GApp (_, GRef(_,c,_), [one_arg]) when eq_gr c bigZ_pos -> bigint_of_bigN one_arg - | GApp (_, GRef(_,c,_), [one_arg]) when eq_gr c bigZ_neg -> + | { CAst.v = GApp ({ CAst.v = GRef(c,_) }, [one_arg])} when eq_gr c bigZ_pos -> bigint_of_bigN one_arg + | { CAst.v = GApp ({ CAst.v = GRef(c,_) }, [one_arg])} when eq_gr c bigZ_neg -> let opp_val = bigint_of_bigN one_arg in if equal opp_val zero then raise Non_closed @@ -286,19 +286,19 @@ let uninterp_bigZ rc = let _ = Notation.declare_numeral_interpreter bigZ_scope (bigZ_path, bigZ_module) interp_bigZ - ([GRef (Loc.ghost, bigZ_pos, None); - GRef (Loc.ghost, bigZ_neg, None)], + ([CAst.make @@ GRef (bigZ_pos, None); + CAst.make @@ GRef (bigZ_neg, None)], uninterp_bigZ, true) (*** Parsing for bigQ in digital notation ***) -let interp_bigQ dloc n = - let ref_z = GRef (dloc, bigQ_z, None) in - GApp (dloc, ref_z, [interp_bigZ dloc n]) +let interp_bigQ ?loc n = + let ref_z = CAst.make ?loc @@ GRef (bigQ_z, None) in + CAst.make ?loc @@ GApp (ref_z, [interp_bigZ ?loc n]) let uninterp_bigQ rc = try match rc with - | GApp (_, GRef(_,c,_), [one_arg]) when eq_gr c bigQ_z -> + | { CAst.v = GApp ({ CAst.v = GRef(c,_)}, [one_arg]) } when eq_gr c bigQ_z -> Some (bigint_of_bigZ one_arg) | _ -> None (* we don't pretty-print yet fractions *) with Non_closed -> None @@ -307,5 +307,5 @@ let uninterp_bigQ rc = let _ = Notation.declare_numeral_interpreter bigQ_scope (bigQ_path, bigQ_module) interp_bigQ - ([GRef (Loc.ghost, bigQ_z, None)], uninterp_bigQ, + ([CAst.make @@ GRef (bigQ_z, None)], uninterp_bigQ, true) diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index 8f065f528..7ce066c59 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -41,14 +41,14 @@ let glob_xI = ConstructRef path_of_xI let glob_xO = ConstructRef path_of_xO let glob_xH = ConstructRef path_of_xH -let pos_of_bignat dloc x = - let ref_xI = GRef (dloc, glob_xI, None) in - let ref_xH = GRef (dloc, glob_xH, None) in - let ref_xO = GRef (dloc, glob_xO, None) in +let pos_of_bignat ?loc x = + let ref_xI = CAst.make @@ GRef (glob_xI, None) in + let ref_xH = CAst.make @@ GRef (glob_xH, None) in + let ref_xO = CAst.make @@ GRef (glob_xO, None) in let rec pos_of x = match div2_with_rest x with - | (q,false) -> GApp (dloc, ref_xO,[pos_of q]) - | (q,true) when not (Bigint.equal q zero) -> GApp (dloc,ref_xI,[pos_of q]) + | (q,false) -> CAst.make @@ GApp (ref_xO,[pos_of q]) + | (q,true) when not (Bigint.equal q zero) -> CAst.make @@ GApp (ref_xI,[pos_of q]) | (q,true) -> ref_xH in pos_of x @@ -58,9 +58,9 @@ let pos_of_bignat dloc x = (**********************************************************************) let rec bignat_of_pos = function - | GApp (_, GRef (_,b,_),[a]) when Globnames.eq_gr b glob_xO -> mult_2(bignat_of_pos a) - | GApp (_, GRef (_,b,_),[a]) when Globnames.eq_gr b glob_xI -> add_1(mult_2(bignat_of_pos a)) - | GRef (_, a, _) when Globnames.eq_gr a glob_xH -> Bigint.one + | { CAst.v = GApp ({ CAst.v = GRef (b,_)},[a]) } when Globnames.eq_gr b glob_xO -> mult_2(bignat_of_pos a) + | { CAst.v = GApp ({ CAst.v = GRef (b,_)},[a]) } when Globnames.eq_gr b glob_xI -> add_1(mult_2(bignat_of_pos a)) + | { CAst.v = GRef (a, _) } when Globnames.eq_gr a glob_xH -> Bigint.one | _ -> raise Non_closed_number (**********************************************************************) @@ -77,22 +77,22 @@ let glob_ZERO = ConstructRef path_of_ZERO let glob_POS = ConstructRef path_of_POS let glob_NEG = ConstructRef path_of_NEG -let z_of_int dloc n = +let z_of_int ?loc n = if not (Bigint.equal n zero) then let sgn, n = if is_pos_or_zero n then glob_POS, n else glob_NEG, Bigint.neg n in - GApp(dloc, GRef (dloc,sgn,None), [pos_of_bignat dloc n]) + CAst.make @@ GApp(CAst.make @@ GRef (sgn,None), [pos_of_bignat ?loc n]) else - GRef (dloc, glob_ZERO, None) + CAst.make @@ GRef (glob_ZERO, None) (**********************************************************************) (* Printing Z via scopes *) (**********************************************************************) let bigint_of_z = function - | GApp (_, GRef (_,b,_),[a]) when Globnames.eq_gr b glob_POS -> bignat_of_pos a - | GApp (_, GRef (_,b,_),[a]) when Globnames.eq_gr b glob_NEG -> Bigint.neg (bignat_of_pos a) - | GRef (_, a, _) when Globnames.eq_gr a glob_ZERO -> Bigint.zero + | { CAst.v = GApp ({ CAst.v = GRef (b,_)},[a]) } when Globnames.eq_gr b glob_POS -> bignat_of_pos a + | { CAst.v = GApp ({ CAst.v = GRef (b,_)},[a]) } when Globnames.eq_gr b glob_NEG -> Bigint.neg (bignat_of_pos a) + | { CAst.v = GRef (a, _) } when Globnames.eq_gr a glob_ZERO -> Bigint.zero | _ -> raise Non_closed_number (**********************************************************************) @@ -107,15 +107,15 @@ let make_path dir id = Globnames.encode_con dir (Id.of_string id) let glob_IZR = ConstRef (make_path (make_dir rdefinitions) "IZR") -let r_of_int dloc z = - GApp (dloc, GRef(dloc,glob_IZR,None), [z_of_int dloc z]) +let r_of_int ?loc z = + CAst.make @@ GApp (CAst.make @@ GRef(glob_IZR,None), [z_of_int ?loc z]) (**********************************************************************) (* Printing R via scopes *) (**********************************************************************) let bigint_of_r = function - | GApp (_,GRef (_,o,_), [a]) when Globnames.eq_gr o glob_IZR -> + | { CAst.v = GApp ({ CAst.v = GRef (o,_) }, [a]) } when Globnames.eq_gr o glob_IZR -> bigint_of_z a | _ -> raise Non_closed_number @@ -128,6 +128,6 @@ let uninterp_r p = let _ = Notation.declare_numeral_interpreter "R_scope" (r_path,["Coq";"Reals";"Rdefinitions"]) r_of_int - ([GRef (Loc.ghost,glob_IZR,None)], + ([CAst.make @@ GRef (glob_IZR, None)], uninterp_r, false) diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml index de0fa77ef..b7f13b040 100644 --- a/plugins/syntax/string_syntax.ml +++ b/plugins/syntax/string_syntax.ml @@ -33,23 +33,23 @@ let glob_EmptyString = lazy (make_reference "EmptyString") open Lazy -let interp_string dloc s = +let interp_string ?loc s = let le = String.length s in let rec aux n = - if n = le then GRef (dloc, force glob_EmptyString, None) else - GApp (dloc,GRef (dloc, force glob_String, None), - [interp_ascii dloc (int_of_char s.[n]); aux (n+1)]) + if n = le then CAst.make ?loc @@ GRef (force glob_EmptyString, None) else + CAst.make ?loc @@ GApp (CAst.make ?loc @@ GRef (force glob_String, None), + [interp_ascii ?loc (int_of_char s.[n]); aux (n+1)]) in aux 0 let uninterp_string r = try let b = Buffer.create 16 in let rec aux = function - | GApp (_,GRef (_,k,_),[a;s]) when eq_gr k (force glob_String) -> + | { CAst.v = GApp ({ CAst.v = GRef (k,_) },[a;s]) } when eq_gr k (force glob_String) -> (match uninterp_ascii a with | Some c -> Buffer.add_char b (Char.chr c); aux s | _ -> raise Non_closed_string) - | GRef (_,z,_) when eq_gr z (force glob_EmptyString) -> + | { CAst.v = GRef (z,_) } when eq_gr z (force glob_EmptyString) -> Some (Buffer.contents b) | _ -> raise Non_closed_string @@ -61,6 +61,6 @@ let _ = Notation.declare_string_interpreter "string_scope" (string_path,["Coq";"Strings";"String"]) interp_string - ([GRef (Loc.ghost,static_glob_String,None); - GRef (Loc.ghost,static_glob_EmptyString,None)], + ([CAst.make @@ GRef (static_glob_String,None); + CAst.make @@ GRef (static_glob_EmptyString,None)], uninterp_string, true) diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml index b7b5fb8a5..479448e06 100644 --- a/plugins/syntax/z_syntax.ml +++ b/plugins/syntax/z_syntax.ml @@ -44,35 +44,36 @@ let glob_xI = ConstructRef path_of_xI let glob_xO = ConstructRef path_of_xO let glob_xH = ConstructRef path_of_xH -let pos_of_bignat dloc x = - let ref_xI = GRef (dloc, glob_xI, None) in - let ref_xH = GRef (dloc, glob_xH, None) in - let ref_xO = GRef (dloc, glob_xO, None) in +let pos_of_bignat ?loc x = + let ref_xI = CAst.make ?loc @@ GRef (glob_xI, None) in + let ref_xH = CAst.make ?loc @@ GRef (glob_xH, None) in + let ref_xO = CAst.make ?loc @@ GRef (glob_xO, None) in let rec pos_of x = match div2_with_rest x with - | (q,false) -> GApp (dloc, ref_xO,[pos_of q]) - | (q,true) when not (Bigint.equal q zero) -> GApp (dloc,ref_xI,[pos_of q]) + | (q,false) -> CAst.make ?loc @@ GApp (ref_xO,[pos_of q]) + | (q,true) when not (Bigint.equal q zero) -> CAst.make ?loc @@ GApp (ref_xI,[pos_of q]) | (q,true) -> ref_xH in pos_of x -let error_non_positive dloc = - user_err ~loc:dloc ~hdr:"interp_positive" +let error_non_positive ?loc = + user_err ?loc ~hdr:"interp_positive" (str "Only strictly positive numbers in type \"positive\".") -let interp_positive dloc n = - if is_strictly_pos n then pos_of_bignat dloc n - else error_non_positive dloc +let interp_positive ?loc n = + if is_strictly_pos n then pos_of_bignat ?loc n + else error_non_positive ?loc (**********************************************************************) (* Printing positive via scopes *) (**********************************************************************) -let rec bignat_of_pos = function - | GApp (_, GRef (_,b,_),[a]) when Globnames.eq_gr b glob_xO -> mult_2(bignat_of_pos a) - | GApp (_, GRef (_,b,_),[a]) when Globnames.eq_gr b glob_xI -> add_1(mult_2(bignat_of_pos a)) - | GRef (_, a, _) when Globnames.eq_gr a glob_xH -> Bigint.one +let rec bignat_of_pos x = CAst.with_val (function + | GApp ({ CAst.v = GRef (b,_) },[a]) when Globnames.eq_gr b glob_xO -> mult_2(bignat_of_pos a) + | GApp ({ CAst.v = GRef (b,_) },[a]) when Globnames.eq_gr b glob_xI -> add_1(mult_2(bignat_of_pos a)) + | GRef (a, _) when Globnames.eq_gr a glob_xH -> Bigint.one | _ -> raise Non_closed_number + ) x let uninterp_positive p = try @@ -87,9 +88,9 @@ let uninterp_positive p = let _ = Notation.declare_numeral_interpreter "positive_scope" (positive_path,binnums) interp_positive - ([GRef (Loc.ghost, glob_xI, None); - GRef (Loc.ghost, glob_xO, None); - GRef (Loc.ghost, glob_xH, None)], + ([CAst.make @@ GRef (glob_xI, None); + CAst.make @@ GRef (glob_xO, None); + CAst.make @@ GRef (glob_xH, None)], uninterp_positive, true) @@ -106,27 +107,28 @@ let glob_Npos = ConstructRef path_of_Npos let n_path = make_path binnums "N" -let n_of_binnat dloc pos_or_neg n = +let n_of_binnat ?loc pos_or_neg n = CAst.make ?loc @@ if not (Bigint.equal n zero) then - GApp(dloc, GRef (dloc,glob_Npos,None), [pos_of_bignat dloc n]) + GApp(CAst.make @@ GRef (glob_Npos,None), [pos_of_bignat ?loc n]) else - GRef (dloc, glob_N0, None) + GRef(glob_N0, None) -let error_negative dloc = - user_err ~loc:dloc ~hdr:"interp_N" (str "No negative numbers in type \"N\".") +let error_negative ?loc = + user_err ?loc ~hdr:"interp_N" (str "No negative numbers in type \"N\".") -let n_of_int dloc n = - if is_pos_or_zero n then n_of_binnat dloc true n - else error_negative dloc +let n_of_int ?loc n = + if is_pos_or_zero n then n_of_binnat ?loc true n + else error_negative ?loc (**********************************************************************) (* Printing N via scopes *) (**********************************************************************) -let bignat_of_n = function - | GApp (_, GRef (_,b,_),[a]) when Globnames.eq_gr b glob_Npos -> bignat_of_pos a - | GRef (_, a,_) when Globnames.eq_gr a glob_N0 -> Bigint.zero +let bignat_of_n = CAst.with_val (function + | GApp ({ CAst.v = GRef (b,_)},[a]) when Globnames.eq_gr b glob_Npos -> bignat_of_pos a + | GRef (a,_) when Globnames.eq_gr a glob_N0 -> Bigint.zero | _ -> raise Non_closed_number + ) let uninterp_n p = try Some (bignat_of_n p) @@ -138,8 +140,8 @@ let uninterp_n p = let _ = Notation.declare_numeral_interpreter "N_scope" (n_path,binnums) n_of_int - ([GRef (Loc.ghost, glob_N0, None); - GRef (Loc.ghost, glob_Npos, None)], + ([CAst.make @@ GRef (glob_N0, None); + CAst.make @@ GRef (glob_Npos, None)], uninterp_n, true) @@ -157,23 +159,24 @@ let glob_ZERO = ConstructRef path_of_ZERO let glob_POS = ConstructRef path_of_POS let glob_NEG = ConstructRef path_of_NEG -let z_of_int dloc n = +let z_of_int ?loc n = if not (Bigint.equal n zero) then let sgn, n = if is_pos_or_zero n then glob_POS, n else glob_NEG, Bigint.neg n in - GApp(dloc, GRef (dloc,sgn,None), [pos_of_bignat dloc n]) + CAst.make ?loc @@ GApp(CAst.make ?loc @@ GRef(sgn,None), [pos_of_bignat ?loc n]) else - GRef (dloc, glob_ZERO, None) + CAst.make ?loc @@ GRef(glob_ZERO, None) (**********************************************************************) (* Printing Z via scopes *) (**********************************************************************) -let bigint_of_z = function - | GApp (_, GRef (_,b,_),[a]) when Globnames.eq_gr b glob_POS -> bignat_of_pos a - | GApp (_, GRef (_,b,_),[a]) when Globnames.eq_gr b glob_NEG -> Bigint.neg (bignat_of_pos a) - | GRef (_, a, _) when Globnames.eq_gr a glob_ZERO -> Bigint.zero +let bigint_of_z = CAst.with_val (function + | GApp ({ CAst.v = GRef (b,_)},[a]) when Globnames.eq_gr b glob_POS -> bignat_of_pos a + | GApp ({ CAst.v = GRef (b,_)},[a]) when Globnames.eq_gr b glob_NEG -> Bigint.neg (bignat_of_pos a) + | GRef (a, _) when Globnames.eq_gr a glob_ZERO -> Bigint.zero | _ -> raise Non_closed_number + ) let uninterp_z p = try @@ -186,8 +189,8 @@ let uninterp_z p = let _ = Notation.declare_numeral_interpreter "Z_scope" (z_path,binnums) z_of_int - ([GRef (Loc.ghost, glob_ZERO, None); - GRef (Loc.ghost, glob_POS, None); - GRef (Loc.ghost, glob_NEG, None)], + ([CAst.make @@ GRef (glob_ZERO, None); + CAst.make @@ GRef (glob_POS, None); + CAst.make @@ GRef (glob_NEG, None)], uninterp_z, true) |