diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-02-14 06:57:40 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-03-09 23:23:40 +0100 |
| commit | 4af41a12a0e7e6b17d25a71568641bd03d5e1f94 (patch) | |
| tree | 9ffa30a21f0d5b80aaeae66955e652f185929498 | |
| parent | 5f989f48eaaf5e13568fce9849f40bc554ca0166 (diff) | |
[located] More work towards using CAst.t
We continue with the work of #402 and #6745 and update most of the
remaining parts of the AST:
- module declarations
- intro patterns
- top-level sentences
Now, parsed documents should be full annotated by `CAst` nodes.
64 files changed, 436 insertions, 417 deletions
diff --git a/dev/ci/user-overlays/06831-ejgallego-located+vernac_2.sh b/dev/ci/user-overlays/06831-ejgallego-located+vernac_2.sh new file mode 100644 index 000000000..df3e9cef2 --- /dev/null +++ b/dev/ci/user-overlays/06831-ejgallego-located+vernac_2.sh @@ -0,0 +1,14 @@ +if [ "$CI_PULL_REQUEST" = "6831" ] || [ "$CI_BRANCH" = "located+vernac_2" ]; then + + ltac2_CI_BRANCH=located+vernac_2 + ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 + + Equations_CI_BRANCH=located+vernac_2 + Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + + # fiat_parsers_CI_BRANCH=located+vernac + # fiat_parsers_CI_GITURL=https://github.com/ejgallego/fiat + + Elpi_CI_BRANCH=located+vernac_2 + Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi.git +fi diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 55b4fa87e..541da3b6d 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -63,7 +63,7 @@ let is_known_option cmd = match Vernacprop.under_control cmd with (** Check whether a command is forbidden in the IDE *) -let ide_cmd_checks ~id (loc,ast) = +let ide_cmd_checks ~id {CAst.loc;v=ast} = let user_error s = CErrors.user_err ?loc ~hdr:"IDE" (str s) in let warn msg = Feedback.(feedback ~id (Message (Warning, loc, strbrk msg))) in if is_debug ast then @@ -120,7 +120,7 @@ let query (route, (s,id)) = let annotate phrase = let doc = get_doc () in - let (loc, ast) = + let {CAst.loc;v=ast} = let pa = Pcoq.Gram.parsable (Stream.of_string phrase) in Stm.parse_sentence ~doc (Stm.get_current_state ~doc) pa in diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 9efaff3b9..f5a6a082e 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -850,7 +850,7 @@ let rec extern inctx scopes vars r = | Name _, _ -> Some (CAst.make na) in (sub_extern false scopes vars tm, na', - Option.map (fun (loc,(ind,nal)) -> + Option.map (fun {CAst.loc;v=(ind,nal)} -> let args = List.map (fun x -> DAst.make @@ PatVar x) nal in let fullargs = add_cpatt_for_params ind args in extern_ind_pattern_in_scope scopes vars ind fullargs @@ -929,7 +929,7 @@ and factorize_prod scopes vars na bk aty c = | Name id, GCases (LetPatternStyle, None, [(e,(Anonymous,None))],(_::_ as eqns)) when is_gvar id e && List.length (store (factorize_eqns eqns)) = 1 -> (match get () with - | [(_,(ids,disj_of_patl,b))] -> + | [{CAst.v=(ids,disj_of_patl,b)}] -> let disjpat = List.map (function [pat] -> pat | _ -> assert false) disj_of_patl in let disjpat = if occur_glob_constr id b then List.map (set_pat_alias id) disjpat else disjpat in let b = extern_typ scopes vars b in @@ -957,7 +957,7 @@ and factorize_lambda inctx scopes vars na bk aty c = | Name id, GCases (LetPatternStyle, None, [(e,(Anonymous,None))],(_::_ as eqns)) when is_gvar id e && List.length (store (factorize_eqns eqns)) = 1 -> (match get () with - | [(_,(ids,disj_of_patl,b))] -> + | [{CAst.v=(ids,disj_of_patl,b)}] -> let disjpat = List.map (function [pat] -> pat | _ -> assert false) disj_of_patl in let disjpat = if occur_glob_constr id b then List.map (set_pat_alias id) disjpat else disjpat in let b = sub_extern inctx scopes vars b in @@ -1010,7 +1010,7 @@ and extern_local_binder scopes vars = function let (assums,ids,l) = extern_local_binder scopes vars l in (assums,ids, CLocalPattern(CAst.make @@ (p,ty)) :: l) -and extern_eqn inctx scopes vars (loc,(ids,pll,c)) = +and extern_eqn inctx scopes vars {CAst.loc;v=(ids,pll,c)} = let pll = List.map (List.map (extern_cases_pattern_in_scope scopes vars)) pll in make ?loc (pll,extern inctx scopes vars c) @@ -1155,7 +1155,7 @@ let extern_closed_glob ?lax goal_concl_style env sigma t = let any_any_branch = (* | _ => _ *) - Loc.tag ([],[DAst.make @@ PatVar Anonymous], DAst.make @@ GHole (Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None)) + CAst.make ([],[DAst.make @@ PatVar Anonymous], DAst.make @@ GHole (Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None)) let compute_displayed_name_in_pattern sigma avoid na c = let open Namegen in diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 918e12e5c..55b943eac 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -524,7 +524,7 @@ let rec expand_binders ?loc mk bl c = | GLocalPattern ((disjpat,ids), id, bk, ty) -> let tm = DAst.make ?loc (GVar id) in (* Distribute the disjunctive patterns over the shared right-hand side *) - let eqnl = List.map (fun pat -> (loc,(ids,[pat],c))) disjpat in + let eqnl = List.map (fun pat -> CAst.make ?loc (ids,[pat],c)) disjpat in let c = DAst.make ?loc @@ GCases (Misctypes.LetPatternStyle, None, [tm,(Anonymous,None)], eqnl) in expand_binders ?loc mk bl (mk ?loc (Name id,Explicit,ty) c) @@ -1954,14 +1954,14 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let thevars, thepats = List.split l in let sub_rtn = (* Some (GSort (Loc.ghost,GType None)) *) None in let sub_tms = List.map (fun id -> (DAst.make @@ GVar id),(Name id,None)) thevars (* "match v1,..,vn" *) in - let main_sub_eqn = Loc.tag @@ + let main_sub_eqn = CAst.make @@ ([],thepats, (* "|p1,..,pn" *) Option.cata (intern_type env') (DAst.make ?loc @@ GHole(Evar_kinds.CasesType false,Misctypes.IntroAnonymous,None)) rtnpo) (* "=> P" if there were a return predicate P, and "=> _" otherwise *) in let catch_all_sub_eqn = if List.for_all (irrefutable globalenv) thepats then [] else - [Loc.tag @@ ([],List.make (List.length thepats) (DAst.make @@ PatVar Anonymous), (* "|_,..,_" *) + [CAst.make @@ ([],List.make (List.length thepats) (DAst.make @@ PatVar Anonymous), (* "|_,..,_" *) DAst.make @@ GHole(Evar_kinds.ImpossibleCase,Misctypes.IntroAnonymous,None))] (* "=> _" *) in Some (DAst.make @@ GCases(Term.RegularStyle,sub_rtn,sub_tms,main_sub_eqn::catch_all_sub_eqn)) in @@ -2077,7 +2077,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = List.map (fun (asubst,pl) -> let rhs = replace_vars_constr_expr asubst rhs in let rhs' = intern {env with ids = env_ids} rhs in - (loc,(eqn_ids,pl,rhs'))) pll + CAst.make ?loc (eqn_ids,pl,rhs')) pll and intern_case_item env forbidden_names_for_gen (tm,na,t) = (* the "match" part *) @@ -2110,7 +2110,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = match case_rel_ctxt,arg_pats with (* LetIn in the rel_context *) | LocalDef _ :: t, l when not with_letin -> - canonize_args t l forbidden_names match_acc ((Loc.tag Anonymous)::var_acc) + canonize_args t l forbidden_names match_acc ((CAst.make Anonymous)::var_acc) | [],[] -> (add_name match_acc na, var_acc) | (LocalAssum (cano_name,ty) | LocalDef (cano_name,_,ty)) :: t, c::tt -> @@ -2118,21 +2118,21 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = | PatVar x -> let loc = c.CAst.loc in canonize_args t tt forbidden_names - (add_name match_acc CAst.(make ?loc x)) ((loc,x)::var_acc) + (add_name match_acc CAst.(make ?loc x)) (CAst.make ?loc x::var_acc) | _ -> let fresh = Namegen.next_name_away_with_default_using_types "iV" cano_name forbidden_names (EConstr.of_constr ty) in canonize_args t tt (Id.Set.add fresh forbidden_names) - ((fresh,c)::match_acc) ((cases_pattern_loc c,Name fresh)::var_acc) + ((fresh,c)::match_acc) ((CAst.make ?loc:(cases_pattern_loc c) @@ Name fresh)::var_acc) end | _ -> assert false in let _,args_rel = List.chop nparams (List.rev mip.Declarations.mind_arity_ctxt) in canonize_args args_rel l forbidden_names_for_gen [] [] in - match_to_do, Some (cases_pattern_expr_loc t,(ind,List.rev_map snd nal)) + match_to_do, Some (CAst.make ?loc:(cases_pattern_expr_loc t) (ind,List.rev_map (fun x -> x.v) nal)) | None -> [], None in - (tm',(na.CAst.v,typ)), extra_id, match_td + (tm',(na.CAst.v, typ)), extra_id, match_td and intern_impargs c env l subscopes args = let eargs, rargs = extract_explicit_arg l args in @@ -2164,7 +2164,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = | (imp::impl', []) -> if not (Id.Map.is_empty eargs) then (let (id,(loc,_)) = Id.Map.choose eargs in - user_err ?loc (str "Not enough non implicit \ + user_err ?loc (str "Not enough non implicit \ arguments to accept the argument bound to " ++ Id.print id ++ str".")); [] diff --git a/interp/modintern.ml b/interp/modintern.ml index 887685585..dc93d8dc4 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -45,7 +45,7 @@ let error_application_to_module_type loc = or both are searched. The returned kind is never ModAny, and it is equal to the input kind when this one isn't ModAny. *) -let lookup_module_or_modtype kind (loc,qid) = +let lookup_module_or_modtype kind {CAst.loc;v=qid} = try if kind == ModType then raise Not_found; let mp = Nametab.locate_module qid in @@ -60,9 +60,9 @@ let lookup_module_or_modtype kind (loc,qid) = let lookup_module lqid = fst (lookup_module_or_modtype Module lqid) let transl_with_decl env = function - | CWith_Module ((_,fqid),qid) -> + | CWith_Module ({CAst.v=fqid},qid) -> WithMod (fqid,lookup_module qid), Univ.ContextSet.empty - | CWith_Definition ((_,fqid),udecl,c) -> + | CWith_Definition ({CAst.v=fqid},udecl,c) -> let sigma, udecl = Univdecls.interp_univ_decl_opt env udecl in let c, ectx = interp_constr env sigma c in begin match UState.check_univ_decl ~poly:(Flags.is_universe_polymorphism()) ectx udecl with @@ -81,11 +81,11 @@ let loc_of_module l = l.CAst.loc (* Invariant : the returned kind is never ModAny, and it is equal to the input kind when this one isn't ModAny. *) -let rec interp_module_ast env kind m cst = match m.CAst.v with - | CMident qid -> - let (mp,kind) = lookup_module_or_modtype kind (m.CAst.loc,qid) in +let rec interp_module_ast env kind m cst = match m with + | {CAst.loc;v=CMident qid} -> + let (mp,kind) = lookup_module_or_modtype kind CAst.(make ?loc qid) in (MEident mp, kind, cst) - | CMapply (me1,me2) -> + | {CAst.loc;v=CMapply (me1,me2)} -> let me1',kind1, cst = interp_module_ast env kind me1 cst in let me2',kind2, cst = interp_module_ast env ModAny me2 cst in let mp2 = match me2' with @@ -95,7 +95,7 @@ let rec interp_module_ast env kind m cst = match m.CAst.v with if kind2 == ModType then error_application_to_module_type (loc_of_module me2); (MEapply (me1',mp2), kind1, cst) - | CMwith (me,decl) -> + | {CAst.loc;v=CMwith (me,decl)} -> let me,kind,cst = interp_module_ast env kind me cst in if kind == Module then error_incorrect_with_in_module m.CAst.loc; let decl, cst' = transl_with_decl env decl in diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 77ef601b7..a0d69ce79 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -156,7 +156,7 @@ let protect g e na = let apply_cases_pattern ?loc ((ids,disjpat),id) c = let tm = DAst.make ?loc (GVar id) in - let eqns = List.map (fun pat -> (loc,(ids,[pat],c))) disjpat in + let eqns = List.map (fun pat -> (CAst.make ?loc (ids,[pat],c))) disjpat in DAst.make ?loc @@ GCases (LetPatternStyle, None, [tm,(Anonymous,None)], eqns) let glob_constr_of_notation_constr_with_binders ?loc g f e nc = @@ -192,7 +192,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc = let e',nal' = List.fold_right (fun na (e',nal) -> let e',na' = protect g e' na in e',na'::nal) nal (e',[]) in - e',Some (Loc.tag ?loc (ind,nal')) in + e',Some (CAst.make ?loc (ind,nal')) in let e',na' = protect g e' na in (e',(f e tm,(na',t'))::tml')) tml (e,[]) in let fold (idl,e) na = let (e,disjpat,na) = g e na in ((Name.cons na idl,e),disjpat,na) in @@ -200,7 +200,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc = let ((idl,e),patl) = List.fold_left_map (cases_pattern_fold_map ?loc fold) ([],e) patl in let disjpatl = product_of_cases_patterns patl in - List.map (fun patl -> Loc.tag (idl,patl,f e rhs)) disjpatl) eqnl in + List.map (fun patl -> CAst.make (idl,patl,f e rhs)) disjpatl) eqnl in GCases (sty,Option.map (f e') rtntypopt,tml',List.flatten eqnl') | NLetTuple (nal,(na,po),b,c) -> let e',nal = List.fold_left_map (protect g) e nal in @@ -411,13 +411,13 @@ let notation_constr_and_vars_of_glob_constr recvars a = | GProd (na,bk,ty,c) -> add_name found na; NProd (na,aux ty,aux c) | GLetIn (na,b,t,c) -> add_name found na; NLetIn (na,aux b,Option.map aux t, aux c) | GCases (sty,rtntypopt,tml,eqnl) -> - let f (_,(idl,pat,rhs)) = List.iter (add_id found) idl; (pat,aux rhs) in + let f {CAst.v=(idl,pat,rhs)} = List.iter (add_id found) idl; (pat,aux rhs) in NCases (sty,Option.map aux rtntypopt, List.map (fun (tm,(na,x)) -> add_name found na; Option.iter - (fun (_,(_,nl)) -> List.iter (add_name found) nl) x; - (aux tm,(na,Option.map (fun (_,(ind,nal)) -> (ind,nal)) x))) tml, + (fun {CAst.v=(_,nl)} -> List.iter (add_name found) nl) x; + (aux tm,(na,Option.map (fun {CAst.v=(ind,nal)} -> (ind,nal)) x))) tml, List.map f eqnl) | GLetTuple (nal,(na,po),b,c) -> add_name found na; @@ -661,7 +661,7 @@ let abstract_return_type_context pi mklam tml rtno = rtno let abstract_return_type_context_glob_constr tml rtn = - abstract_return_type_context (fun (_,(_,nal)) -> nal) + abstract_return_type_context (fun {CAst.v=(_,nal)} -> nal) (fun na c -> DAst.make @@ GLambda(na,Explicit,DAst.make @@ GHole(Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None),c)) tml rtn @@ -1241,7 +1241,7 @@ and match_extended_binders ?loc isprod u alp metas na1 na2 bk t sigma b1 b2 = | Name p, GCases (LetPatternStyle,None,[(e,_)],(_::_ as eqns)), Name id when is_gvar p e && is_bindinglist_meta id metas && List.length (store (Detyping.factorize_eqns eqns)) = 1 -> (match get () with - | [(_,(ids,disj_of_patl,b1))] -> + | [{CAst.v=(ids,disj_of_patl,b1)}] -> let disjpat = List.map (function [pat] -> pat | _ -> assert false) disj_of_patl in let disjpat = if occur_glob_constr p b1 then List.map (set_pat_alias p) disjpat else disjpat in let alp,sigma = bind_bindinglist_env alp sigma id [DAst.make ?loc @@ GLocalPattern ((disjpat,ids),p,bk,t)] in @@ -1250,7 +1250,7 @@ and match_extended_binders ?loc isprod u alp metas na1 na2 bk t sigma b1 b2 = | Name p, GCases (LetPatternStyle,None,[(e,_)],(_::_ as eqns)), Name id when is_gvar p e && is_onlybinding_pattern_like_meta false id metas && List.length (store (Detyping.factorize_eqns eqns)) = 1 -> (match get () with - | [(_,(ids,disj_of_patl,b1))] -> + | [{CAst.v=(ids,disj_of_patl,b1)}] -> let disjpat = List.map (function [pat] -> pat | _ -> assert false) disj_of_patl in let disjpat = if occur_glob_constr p b1 then List.map (set_pat_alias p) disjpat else disjpat in let alp,sigma = bind_binding_env alp sigma id disjpat in @@ -1263,7 +1263,7 @@ and match_extended_binders ?loc isprod u alp metas na1 na2 bk t sigma b1 b2 = let (alp,sigma) = match_names metas (alp,sigma) na1 na2 in match_in u alp metas sigma b1 b2 -and match_equations u alp metas sigma (_,(ids,patl1,rhs1)) (patl2,rhs2) rest1 rest2 = +and match_equations u alp metas sigma {CAst.v=(ids,patl1,rhs1)} (patl2,rhs2) rest1 rest2 = (* patl1 and patl2 have the same length because they respectively correspond to some tml1 and tml2 that have the same length *) let allow_catchall = (rest2 = [] && ids = []) in @@ -1272,7 +1272,7 @@ and match_equations u alp metas sigma (_,(ids,patl1,rhs1)) (patl2,rhs2) rest1 re (alp,sigma) patl1 patl2 in match_in u alp metas sigma rhs1 rhs2 -and match_disjunctive_equations u alp metas sigma (_,(ids,disjpatl1,rhs1)) (disjpatl2,rhs2) _ _ = +and match_disjunctive_equations u alp metas sigma {CAst.v=(ids,disjpatl1,rhs1)} (disjpatl2,rhs2) _ _ = (* patl1 and patl2 have the same length because they respectively correspond to some tml1 and tml2 that have the same length *) let (alp,sigma) = diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml index bc24a19de..6033d509b 100644 --- a/interp/smartlocate.ml +++ b/interp/smartlocate.ml @@ -68,16 +68,16 @@ let global_with_alias ?head r = let smart_global ?head = function | AN r -> global_with_alias ?head r - | ByNotation (loc,(ntn,sc)) -> + | ByNotation {CAst.loc;v=(ntn,sc)} -> Notation.interp_notation_as_global_reference ?loc (fun _ -> true) ntn sc let smart_global_inductive = function | AN r -> global_inductive_with_alias r - | ByNotation (loc,(ntn,sc)) -> + | ByNotation {CAst.loc;v=(ntn,sc)} -> destIndRef (Notation.interp_notation_as_global_reference ?loc isIndRef ntn sc) let loc_of_smart_reference = function | AN r -> loc_of_reference r - | ByNotation (loc,(_,_)) -> loc + | ByNotation {CAst.loc;v=(_,_)} -> loc diff --git a/interp/stdarg.ml b/interp/stdarg.ml index 5f1aad0c2..0958cc7ee 100644 --- a/interp/stdarg.ml +++ b/interp/stdarg.ml @@ -34,7 +34,7 @@ let wit_pre_ident : string uniform_genarg_type = let loc_of_or_by_notation f = function | AN c -> f c - | ByNotation (loc,(s,_)) -> loc + | ByNotation {CAst.loc;v=(s,_)} -> loc let wit_int_or_var = make0 ~dyn:(val_tag (topwit wit_int)) "int_or_var" diff --git a/interp/stdarg.mli b/interp/stdarg.mli index 948ec1381..b69129956 100644 --- a/interp/stdarg.mli +++ b/interp/stdarg.mli @@ -39,7 +39,7 @@ val wit_pre_ident : string uniform_genarg_type val wit_int_or_var : (int or_var, int or_var, int) genarg_type -val wit_intro_pattern : (constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type +val wit_intro_pattern : (constr_expr intro_pattern_expr CAst.t, glob_constr_and_expr intro_pattern_expr CAst.t, intro_pattern) genarg_type val wit_ident : Id.t uniform_genarg_type @@ -88,7 +88,7 @@ val wit_reference : (reference, global_reference located or_var, global_referenc val wit_global : (reference, global_reference located or_var, global_reference) genarg_type val wit_clause : (lident Locus.clause_expr, lident Locus.clause_expr, Names.Id.t Locus.clause_expr) genarg_type val wit_quantified_hypothesis : quantified_hypothesis uniform_genarg_type -val wit_intropattern : (constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type +val wit_intropattern : (constr_expr intro_pattern_expr CAst.t, glob_constr_and_expr intro_pattern_expr CAst.t, intro_pattern) genarg_type val wit_redexpr : ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen, (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen, diff --git a/interp/tactypes.ml b/interp/tactypes.ml index fc0f8de5f..83e42be89 100644 --- a/interp/tactypes.ml +++ b/interp/tactypes.ml @@ -12,7 +12,6 @@ lower API. It's not clear whether this is a temporary API or if this is meant to stay. *) -open Loc open Names open Constrexpr open Pattern @@ -29,7 +28,7 @@ type 'a delayed_open = Environ.env -> Evd.evar_map -> Evd.evar_map * 'a type delayed_open_constr = EConstr.constr delayed_open type delayed_open_constr_with_bindings = EConstr.constr with_bindings delayed_open -type intro_pattern = delayed_open_constr intro_pattern_expr located -type intro_patterns = delayed_open_constr intro_pattern_expr located list -type or_and_intro_pattern = delayed_open_constr or_and_intro_pattern_expr located -type intro_pattern_naming = intro_pattern_naming_expr located +type intro_pattern = delayed_open_constr intro_pattern_expr CAst.t +type intro_patterns = delayed_open_constr intro_pattern_expr CAst.t list +type or_and_intro_pattern = delayed_open_constr or_and_intro_pattern_expr CAst.t +type intro_pattern_naming = intro_pattern_naming_expr CAst.t diff --git a/intf/constrexpr.ml b/intf/constrexpr.ml index 31f811bc8..fda31756a 100644 --- a/intf/constrexpr.ml +++ b/intf/constrexpr.ml @@ -143,8 +143,8 @@ type constr_pattern_expr = constr_expr (** Concrete syntax for modules and module types *) type with_declaration_ast = - | CWith_Module of Id.t list Loc.located * qualid Loc.located - | CWith_Definition of Id.t list Loc.located * universe_decl_expr option * constr_expr + | CWith_Module of Id.t list CAst.t * qualid CAst.t + | CWith_Definition of Id.t list CAst.t * universe_decl_expr option * constr_expr type module_ast_r = | CMident of qualid diff --git a/intf/glob_term.ml b/intf/glob_term.ml index 39a7b956a..84be15552 100644 --- a/intf/glob_term.ml +++ b/intf/glob_term.ml @@ -72,14 +72,14 @@ and 'a fix_kind_g = | GCoFix of int and 'a predicate_pattern_g = - Name.t * (inductive * Name.t list) Loc.located option + Name.t * (inductive * Name.t list) CAst.t option (** [(na,id)] = "as 'na' in 'id'" where if [id] is [Some(l,I,k,args)]. *) and 'a tomatch_tuple_g = ('a glob_constr_g * 'a predicate_pattern_g) and 'a tomatch_tuples_g = 'a tomatch_tuple_g list -and 'a cases_clause_g = (Id.t list * 'a cases_pattern_g list * 'a glob_constr_g) Loc.located +and 'a cases_clause_g = (Id.t list * 'a cases_pattern_g list * 'a glob_constr_g) CAst.t (** [(p,il,cl,t)] = "|'cl' => 't'". Precondition: the free variables of [t] are members of [il]. *) and 'a cases_clauses_g = 'a cases_clause_g list @@ -96,7 +96,7 @@ type fix_recursion_order = [ `any ] fix_recursion_order_g type any_glob_constr = AnyGlobConstr : 'r glob_constr_g -> any_glob_constr -type 'a disjunctive_cases_clause_g = (Id.t list * 'a cases_pattern_g list list * 'a glob_constr_g) Loc.located +type 'a disjunctive_cases_clause_g = (Id.t list * 'a cases_pattern_g list list * 'a glob_constr_g) CAst.t type 'a disjunctive_cases_clauses_g = 'a disjunctive_cases_clause_g list type 'a cases_pattern_disjunction_g = 'a cases_pattern_g list diff --git a/intf/misctypes.ml b/intf/misctypes.ml index 54a4861d0..1eee3dfc7 100644 --- a/intf/misctypes.ml +++ b/intf/misctypes.ml @@ -35,12 +35,12 @@ and intro_pattern_naming_expr = and 'constr intro_pattern_action_expr = | IntroWildcard | IntroOrAndPattern of 'constr or_and_intro_pattern_expr - | IntroInjection of ('constr intro_pattern_expr) Loc.located list - | IntroApplyOn of 'constr Loc.located * 'constr intro_pattern_expr Loc.located + | IntroInjection of ('constr intro_pattern_expr) CAst.t list + | IntroApplyOn of 'constr CAst.t * 'constr intro_pattern_expr CAst.t | IntroRewrite of bool and 'constr or_and_intro_pattern_expr = - | IntroOrPattern of ('constr intro_pattern_expr) Loc.located list list - | IntroAndPattern of ('constr intro_pattern_expr) Loc.located list + | IntroOrPattern of ('constr intro_pattern_expr) CAst.t list list + | IntroAndPattern of ('constr intro_pattern_expr) CAst.t list (** Move destination for hypothesis *) @@ -95,7 +95,7 @@ type 'a cast_type = type quantified_hypothesis = AnonHyp of int | NamedHyp of Id.t -type 'a explicit_bindings = (quantified_hypothesis * 'a) Loc.located list +type 'a explicit_bindings = (quantified_hypothesis * 'a) CAst.t list type 'a bindings = | ImplicitBindings of 'a list @@ -115,7 +115,7 @@ type 'a and_short_name = 'a * lident option type 'a or_by_notation = | AN of 'a - | ByNotation of (string * string option) Loc.located + | ByNotation of (string * string option) CAst.t (* NB: the last string in [ByNotation] is actually a [Notation.delimiters], but this formulation avoids a useless dependency. *) diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4 index a1d36b822..69dc391c4 100644 --- a/parsing/g_prim.ml4 +++ b/parsing/g_prim.ml4 @@ -62,8 +62,8 @@ GEXTEND Gram ] ] ; fullyqualid: - [ [ id = ident; (l,id')=fields -> Loc.tag ~loc:!@loc @@ id::List.rev (id'::l) - | id = ident -> Loc.tag ~loc:!@loc [id] + [ [ id = ident; (l,id')=fields -> CAst.make ~loc:!@loc @@ id::List.rev (id'::l) + | id = ident -> CAst.make ~loc:!@loc [id] ] ] ; basequalid: @@ -82,14 +82,14 @@ GEXTEND Gram ] ] ; by_notation: - [ [ s = ne_string; sc = OPT ["%"; key = IDENT -> key ] -> Loc.tag ~loc:!@loc (s, sc) ] ] + [ [ s = ne_string; sc = OPT ["%"; key = IDENT -> key ] -> CAst.make ~loc:!@loc (s, sc) ] ] ; smart_global: [ [ c = reference -> Misctypes.AN c | ntn = by_notation -> Misctypes.ByNotation ntn ] ] ; qualid: - [ [ qid = basequalid -> Loc.tag ~loc:!@loc qid ] ] + [ [ qid = basequalid -> CAst.make ~loc:!@loc qid ] ] ; ne_string: [ [ s = STRING -> diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index f1ec49623..99eec9742 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -554,7 +554,7 @@ GEXTEND Gram ] ] ; module_expr_atom: - [ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident (snd qid) | "("; me = module_expr; ")" -> me ] ] + [ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident (qid.CAst.v) | "("; me = module_expr; ")" -> me ] ] ; with_declaration: [ [ "Definition"; fqid = fullyqualid; udecl = OPT univ_decl; ":="; c = Constr.lconstr -> @@ -564,7 +564,7 @@ GEXTEND Gram ] ] ; module_type: - [ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident (snd qid) + [ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident (qid.CAst.v) | "("; mt = module_type; ")" -> mt | mty = module_type; me = module_expr_atom -> CAst.make ~loc:!@loc @@ CMapply (mty,me) diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index e66aa4ade..0f8aad110 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -8,7 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Loc open Names open Extend open Vernacexpr @@ -208,10 +207,10 @@ module Prim : val integer : int Gram.entry val string : string Gram.entry val lstring : lstring Gram.entry - val qualid : qualid located Gram.entry - val fullyqualid : Id.t list located Gram.entry + val qualid : qualid CAst.t Gram.entry + val fullyqualid : Id.t list CAst.t Gram.entry val reference : reference Gram.entry - val by_notation : (string * string option) Loc.located Gram.entry + val by_notation : (string * string option) CAst.t Gram.entry val smart_global : reference or_by_notation Gram.entry val dirpath : DirPath.t Gram.entry val ne_string : string Gram.entry diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 21d1339c5..90af20b4c 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -68,9 +68,9 @@ let pr_intro_as_pat _prc _ _ pat = str"<simple_intropattern>" | None -> mt () -let out_disjunctive = function - | loc, IntroAction (IntroOrAndPattern l) -> (loc,l) - | _ -> CErrors.user_err Pp.(str "Disjunctive or conjunctive intro pattern expected.") +let out_disjunctive = CAst.map (function + | IntroAction (IntroOrAndPattern l) -> l + | _ -> CErrors.user_err Pp.(str "Disjunctive or conjunctive intro pattern expected.")) ARGUMENT EXTEND with_names TYPED AS intropattern_opt PRINTED BY pr_intro_as_pat | [ "as" simple_intropattern(ipat) ] -> [ Some ipat ] diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 7159614d9..49f7aae43 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -287,7 +287,7 @@ let make_discr_match_el = *) let make_discr_match_brl i = List.map_i - (fun j (_,(idl,patl,_)) -> Loc.tag @@ + (fun j {CAst.v=(idl,patl,_)} -> CAst.make @@ if Int.equal j i then (idl,patl, mkGRef (Lazy.force coq_True_ref)) else (idl,patl, mkGRef (Lazy.force coq_False_ref)) @@ -659,7 +659,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.tag ([],[case_pats.(i)],x)) + (fun i x -> CAst.make ([],[case_pats.(i)],x)) 0 [lhs;rhs] in @@ -689,7 +689,7 @@ 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.tag ([],[case_pats.(0)],e) in + let br = CAst.make ([],[case_pats.(0)],e) in let match_expr = mkGCases(None,[b,(Anonymous,None)],[br]) in build_entry_lc env funnames avoid match_expr @@ -756,7 +756,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 {CAst.v=(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) diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 41eb48657..40ea40b6b 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -111,11 +111,11 @@ let change_vars = Miscops.map_cast_type (change_vars mapping) c) | GProj(p,c) -> GProj(p, change_vars mapping c) ) rt - and change_vars_br mapping ((loc,(idl,patl,res)) as br) = + and change_vars_br mapping ({CAst.loc;v=(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 CAst.make ?loc (idl,patl,change_vars new_mapping res) in change_vars @@ -298,13 +298,13 @@ let rec alpha_rt excluded rt = in new_rt -and alpha_br excluded (loc,(ids,patl,res)) = +and alpha_br excluded {CAst.loc;v=(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)) + CAst.make ?loc (new_ids,new_patl,new_res) (* [is_free_in id rt] checks if [id] is a free variable in [rt] @@ -348,7 +348,7 @@ let is_free_in id = | GCast (b,CastCoerce) -> is_free_in b | GProj (_,c) -> is_free_in c ) x - and is_free_in_br (_,(ids,_,rt)) = + and is_free_in_br {CAst.v=(ids,_,rt)} = (not (Id.List.mem id ids)) && is_free_in rt in is_free_in @@ -443,10 +443,10 @@ let replace_var_by_term x_id term = | GProj(p,c) -> GProj(p,replace_var_by_pattern c) ) x - and replace_var_by_pattern_br ((loc,(idl,patl,res)) as br) = + and replace_var_by_pattern_br ({CAst.loc;v=(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 CAst.make ?loc (idl,patl,replace_var_by_pattern res) in replace_var_by_pattern @@ -547,8 +547,8 @@ let expand_as = List.map (expand_as_br map) brl) | GProj(p,c) -> GProj(p, expand_as map c) ) - 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 {CAst.loc; v=(idl,cpl,rt)} = + CAst.make ?loc (idl,cpl, expand_as (List.fold_left add_as map cpl) rt) in expand_as Id.Map.empty diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 13eda3952..1c27b27e2 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -215,7 +215,7 @@ let is_rec names = List.exists (fun (e,_) -> lookup names e) el || List.exists (lookup_br names) brl | GProj(_,c) -> lookup names c - and lookup_br names (_,(idl,_,rt)) = + and lookup_br names {CAst.v=(idl,_,rt)} = let new_names = List.fold_right Id.Set.remove idl names in lookup new_names rt in diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index b858e78d0..2743a8a2f 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -240,7 +240,7 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i List.map (fun decl -> List.map - (fun id -> Loc.tag @@ IntroNaming (IntroIdentifier id)) + (fun id -> CAst.make @@ IntroNaming (IntroIdentifier id)) (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum evd (RelDecl.get_type decl))))) ) branches @@ -256,7 +256,7 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i (* We get the identifiers of this branch *) let pre_args = List.fold_right - (fun (_,pat) acc -> + (fun {CAst.v=pat} acc -> match pat with | IntroNaming (IntroIdentifier id) -> id::acc | _ -> anomaly (Pp.str "Not an identifier.") diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 759c88633..4cbcde8e5 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -206,7 +206,7 @@ let (value_f: Constr.t list -> global_reference -> Constr.t) = (RegularStyle,None, [DAst.make @@ GApp(DAst.make @@ GRef(fterm,None), List.rev_map (fun x_id -> DAst.make @@ GVar x_id) rev_x_id_l), (Anonymous,None)], - [Loc.tag ([v_id], [DAst.make @@ PatCstr ((destIndRef (delayed_force coq_sig_ref),1), + [CAst.make ([v_id], [DAst.make @@ PatCstr ((destIndRef (delayed_force coq_sig_ref),1), [DAst.make @@ PatVar(Name v_id); DAst.make @@ PatVar Anonymous], Anonymous)], DAst.make @@ GVar v_id)]) @@ -899,8 +899,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.tag @@ (NamedHyp def, expr_info.f_constr); - Loc.tag @@ (NamedHyp k, f_S max)]) false) g) ) + ExplicitBindings[CAst.make @@ (NamedHyp def, expr_info.f_constr); + CAst.make @@ (NamedHyp k, f_S max)]) false) g) ) ) [make_rewrite_list expr_info max l; observe_tclTHENLIST (str "make_rewrite_list")[ (* x < S max proof *) @@ -926,8 +926,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.tag @@ (NamedHyp def, expr_info.f_constr); - Loc.tag @@ (NamedHyp k, f_S (f_S max))]) false)) g) + ExplicitBindings[CAst.make @@ (NamedHyp def, expr_info.f_constr); + CAst.make @@ (NamedHyp k, f_S (f_S max))]) false)) g) [observe_tac(str "make_rewrite finalize") ( (* tclORELSE( h_reflexivity) *) (observe_tclTHENLIST (str "make_rewrite")[ diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index 61632e388..2e90ce90c 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -264,7 +264,7 @@ let add_rewrite_hint ~poly bases ort t lcsr = (Declare.declare_universe_context false ctx; Univ.ContextSet.empty) in - Loc.tag ?loc:(Constrexpr_ops.constr_loc ce) ((c, ctx), ort, Option.map (in_gen (rawwit wit_ltac)) t) in + CAst.make ?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 diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index 66268f9f9..1909cd96f 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -198,7 +198,8 @@ 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 (CAst.make ~loc:!@loc id) ] ] + | qid = qualid -> let (_pth,id) = Libnames.repr_qualid qid.CAst.v in + ArgVar (CAst.make ~loc:!@loc id) ] ] ; constr_eval: [ [ IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr -> diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4 index 1b8a852d9..7643cc97d 100644 --- a/plugins/ltac/g_tactic.ml4 +++ b/plugins/ltac/g_tactic.ml4 @@ -175,7 +175,7 @@ let mkCLambdaN_simple bl c = match bl with let loc = Loc.merge_opt (List.hd (pi1 h)).CAst.loc (Constrexpr_ops.constr_loc c) in mkCLambdaN_simple_loc ?loc bl c -let loc_of_ne_list l = Loc.merge_opt (fst (List.hd l)) (fst (List.last l)) +let loc_of_ne_list l = Loc.merge_opt (List.hd l).CAst.loc (List.last l).CAst.loc let map_int_or_var f = function | ArgArg x -> ArgArg (f x) @@ -297,7 +297,7 @@ GEXTEND Gram (* (A & B & C) is translated into (A,(B,C)) *) let rec pairify = function | ([]|[_]|[_;_]) as l -> l - | t::q -> [t; Loc.tag ?loc:(loc_of_ne_list q) (IntroAction (IntroOrAndPattern (IntroAndPattern (pairify q))))] + | t::q -> [t; CAst.make ?loc:(loc_of_ne_list q) (IntroAction (IntroOrAndPattern (IntroAndPattern (pairify q))))] in IntroAndPattern (pairify (si::tc)) ] ] ; equality_intropattern: @@ -312,28 +312,28 @@ GEXTEND Gram ; nonsimple_intropattern: [ [ l = simple_intropattern -> l - | "*" -> Loc.tag ~loc:!@loc @@ IntroForthcoming true - | "**" -> Loc.tag ~loc:!@loc @@ IntroForthcoming false ]] + | "*" -> CAst.make ~loc:!@loc @@ IntroForthcoming true + | "**" -> CAst.make ~loc:!@loc @@ IntroForthcoming false ]] ; simple_intropattern: [ [ pat = simple_intropattern_closed; l = LIST0 ["%"; c = operconstr LEVEL "0" -> c] -> - let loc0,pat = pat in + let {CAst.loc=loc0;v=pat} = pat in let f c pat = let loc1 = Constrexpr_ops.constr_loc c in let loc = Loc.merge_opt loc0 loc1 in - IntroAction (IntroApplyOn ((loc1,c),(loc,pat))) in - Loc.tag ~loc:!@loc @@ List.fold_right f l pat ] ] + IntroAction (IntroApplyOn (CAst.(make ?loc:loc1 c),CAst.(make ?loc pat))) in + CAst.make ~loc:!@loc @@ List.fold_right f l pat ] ] ; simple_intropattern_closed: - [ [ 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 ] ] + [ [ pat = or_and_intropattern -> CAst.make ~loc:!@loc @@ IntroAction (IntroOrAndPattern pat) + | pat = equality_intropattern -> CAst.make ~loc:!@loc @@ IntroAction pat + | "_" -> CAst.make ~loc:!@loc @@ IntroAction IntroWildcard + | pat = naming_intropattern -> CAst.make ~loc:!@loc @@ IntroNaming pat ] ] ; simple_binding: - [ [ "("; id = ident; ":="; c = lconstr; ")" -> Loc.tag ~loc:!@loc (NamedHyp id, c) - | "("; n = natural; ":="; c = lconstr; ")" -> Loc.tag ~loc:!@loc (AnonHyp n, c) ] ] + [ [ "("; id = ident; ":="; c = lconstr; ")" -> CAst.make ~loc:!@loc (NamedHyp id, c) + | "("; n = natural; ":="; c = lconstr; ")" -> CAst.make ~loc:!@loc (AnonHyp n, c) ] ] ; bindings: [ [ test_lpar_idnum_coloneq; bl = LIST1 simple_binding -> @@ -470,7 +470,7 @@ GEXTEND Gram | -> None ] ] ; or_and_intropattern_loc: - [ [ ipat = or_and_intropattern -> ArgArg (Loc.tag ~loc:!@loc ipat) + [ [ ipat = or_and_intropattern -> ArgArg (CAst.make ~loc:!@loc ipat) | locid = identref -> ArgVar locid ] ] ; as_or_and_ipat: @@ -478,13 +478,13 @@ GEXTEND Gram | -> None ] ] ; eqn_ipat: - [ [ IDENT "eqn"; ":"; pat = naming_intropattern -> Some (Loc.tag ~loc:!@loc pat) + [ [ IDENT "eqn"; ":"; pat = naming_intropattern -> Some (CAst.make ~loc:!@loc pat) | IDENT "_eqn"; ":"; pat = naming_intropattern -> let loc = !@loc in - warn_deprecated_eqn_syntax ~loc "H"; Some (Loc.tag ~loc pat) + warn_deprecated_eqn_syntax ~loc "H"; Some (CAst.make ~loc pat) | IDENT "_eqn" -> let loc = !@loc in - warn_deprecated_eqn_syntax ~loc "?"; Some (Loc.tag ~loc IntroAnonymous) + warn_deprecated_eqn_syntax ~loc "?"; Some (CAst.make ~loc IntroAnonymous) | -> None ] ] ; as_name: @@ -525,7 +525,7 @@ GEXTEND Gram IDENT "intros"; pl = ne_intropatterns -> TacAtom (Loc.tag ~loc:!@loc @@ TacIntroPattern (false,pl)) | IDENT "intros" -> - TacAtom (Loc.tag ~loc:!@loc @@ TacIntroPattern (false,[Loc.tag ~loc:!@loc @@IntroForthcoming false])) + TacAtom (Loc.tag ~loc:!@loc @@ TacIntroPattern (false,[CAst.make ~loc:!@loc @@IntroForthcoming false])) | IDENT "eintros"; pl = ne_intropatterns -> TacAtom (Loc.tag ~loc:!@loc @@ TacIntroPattern (true,pl)) @@ -577,31 +577,31 @@ GEXTEND Gram | IDENT "assert"; test_lpar_id_coloneq; "("; lid = identref; ":="; c = lconstr; ")" -> let { CAst.loc = loc; v = id } = lid in - TacAtom (Loc.tag ?loc @@ TacAssert (false,true,None,Some (Loc.tag ?loc @@ IntroNaming (IntroIdentifier id)),c)) + TacAtom (Loc.tag ?loc @@ TacAssert (false,true,None,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) | IDENT "eassert"; test_lpar_id_coloneq; "("; lid = identref; ":="; c = lconstr; ")" -> let { CAst.loc = loc; v = id } = lid in - TacAtom (Loc.tag ?loc @@ TacAssert (true,true,None,Some (Loc.tag ?loc @@ IntroNaming (IntroIdentifier id)),c)) + TacAtom (Loc.tag ?loc @@ TacAssert (true,true,None,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) (* Alternative syntax for "assert c as id by tac" *) | IDENT "assert"; test_lpar_id_colon; "("; lid = identref; ":"; c = lconstr; ")"; tac=by_tactic -> let { CAst.loc = loc; v = id } = lid in - TacAtom (Loc.tag ?loc @@ TacAssert (false,true,Some tac,Some (Loc.tag ?loc @@ IntroNaming (IntroIdentifier id)),c)) + TacAtom (Loc.tag ?loc @@ TacAssert (false,true,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) | IDENT "eassert"; test_lpar_id_colon; "("; lid = identref; ":"; c = lconstr; ")"; tac=by_tactic -> let { CAst.loc = loc; v = id } = lid in - TacAtom (Loc.tag ?loc @@ TacAssert (true,true,Some tac,Some (Loc.tag ?loc @@ IntroNaming (IntroIdentifier id)),c)) + TacAtom (Loc.tag ?loc @@ TacAssert (true,true,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) (* Alternative syntax for "enough c as id by tac" *) | IDENT "enough"; test_lpar_id_colon; "("; lid = identref; ":"; c = lconstr; ")"; tac=by_tactic -> let { CAst.loc = loc; v = id } = lid in - TacAtom (Loc.tag ?loc @@ TacAssert (false,false,Some tac,Some (Loc.tag ?loc @@ IntroNaming (IntroIdentifier id)),c)) + TacAtom (Loc.tag ?loc @@ TacAssert (false,false,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) | IDENT "eenough"; test_lpar_id_colon; "("; lid = identref; ":"; c = lconstr; ")"; tac=by_tactic -> let { CAst.loc = loc; v = id } = lid in - TacAtom (Loc.tag ?loc @@ TacAssert (true,false,Some tac,Some (Loc.tag ?loc @@ IntroNaming (IntroIdentifier id)),c)) + TacAtom (Loc.tag ?loc @@ TacAssert (true,false,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) | IDENT "assert"; c = constr; ipat = as_ipat; tac = by_tactic -> TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,true,Some tac,ipat,c)) diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli index 699e23110..6637de745 100644 --- a/plugins/ltac/pltac.mli +++ b/plugins/ltac/pltac.mli @@ -10,7 +10,6 @@ (** Ltac parsing entries *) -open Loc open Pcoq open Libnames open Constrexpr @@ -29,7 +28,7 @@ val quantified_hypothesis : quantified_hypothesis Gram.entry val destruction_arg : constr_expr with_bindings destruction_arg Gram.entry val int_or_var : int or_var Gram.entry val simple_tactic : raw_tactic_expr Gram.entry -val simple_intropattern : constr_expr intro_pattern_expr located Gram.entry +val simple_intropattern : constr_expr intro_pattern_expr CAst.t Gram.entry val in_clause : lident Locus.clause_expr Gram.entry val clause_dft_concl : lident Locus.clause_expr Gram.entry val tactic_arg : raw_tactic_arg Gram.entry diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index fbb70cca6..a42994652 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -183,7 +183,7 @@ let string_of_genarg_arg (ArgumentType arg) = 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 {CAst.v=(s,sc)} -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc let pr_located pr (loc,x) = pr x @@ -382,9 +382,9 @@ let string_of_genarg_arg (ArgumentType arg) = let pr_as_disjunctive_ipat prc ipatl = keyword "as" ++ spc () ++ - pr_or_var (fun (loc,p) -> Miscprint.pr_or_and_intro_pattern prc p) ipatl + pr_or_var (fun {CAst.loc;v=p} -> Miscprint.pr_or_and_intro_pattern prc p) ipatl - let pr_eqn_ipat (_,ipat) = keyword "eqn:" ++ Miscprint.pr_intro_pattern_naming ipat + let pr_eqn_ipat {CAst.v=ipat} = keyword "eqn:" ++ Miscprint.pr_intro_pattern_naming ipat let pr_with_induction_names prc = function | None, None -> mt () @@ -426,7 +426,7 @@ let string_of_genarg_arg (ArgumentType arg) = let pr_assumption prc prdc prlc ipat c = match ipat with (* Use this "optimisation" or use only the general case ?*) (* it seems that this "optimisation" is somehow more natural *) - | Some (_,IntroNaming (IntroIdentifier id)) -> + | Some {CAst.v=IntroNaming (IntroIdentifier id)} -> spc() ++ surround (pr_id id ++ str " :" ++ spc() ++ prlc c) | ipat -> spc() ++ prc c ++ pr_as_ipat prdc ipat @@ -744,7 +744,7 @@ let pr_goal_selector ~toplevel s = | TacIntroPattern (ev,(_::_ as p)) -> hov 1 (primitive (if ev then "eintros" else "intros") ++ (match p with - | [_,Misctypes.IntroForthcoming false] -> mt () + | [{CAst.v=Misctypes.IntroForthcoming false}] -> mt () | _ -> spc () ++ prlist_with_sep spc (Miscprint.pr_intro_pattern pr.pr_dconstr) p)) | TacApply (a,ev,cb,inhyp) -> hov 1 ( diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index 2c7ebb745..3812a2ba2 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -147,7 +147,7 @@ let coerce_var_to_ident fresh env sigma v = let fail () = raise (CannotCoerceTo "a fresh identifier") in if has_type v (topwit wit_intro_pattern) then match out_gen (topwit wit_intro_pattern) v with - | _, IntroNaming (IntroIdentifier id) -> id + | { CAst.v=IntroNaming (IntroIdentifier id)} -> id | _ -> fail () else if has_type v (topwit wit_var) then out_gen (topwit wit_var) v @@ -171,7 +171,7 @@ let id_of_name = function let fail () = raise (CannotCoerceTo "an identifier") in if has_type v (topwit wit_intro_pattern) then match out_gen (topwit wit_intro_pattern) v with - | _, IntroNaming (IntroIdentifier id) -> id + | {CAst.v=IntroNaming (IntroIdentifier id)} -> id | _ -> fail () else if has_type v (topwit wit_var) then out_gen (topwit wit_var) v @@ -207,7 +207,7 @@ let id_of_name = function let coerce_to_intro_pattern env sigma v = if has_type v (topwit wit_intro_pattern) then - snd (out_gen (topwit wit_intro_pattern) v) + (out_gen (topwit wit_intro_pattern) v).CAst.v else if has_type v (topwit wit_var) then let id = out_gen (topwit wit_var) v in IntroNaming (IntroIdentifier id) @@ -226,7 +226,7 @@ let coerce_to_intro_pattern_naming env sigma v = let coerce_to_hint_base v = if has_type v (topwit wit_intro_pattern) then match out_gen (topwit wit_intro_pattern) v with - | _, IntroNaming (IntroIdentifier id) -> Id.to_string id + | {CAst.v=IntroNaming (IntroIdentifier id)} -> Id.to_string id | _ -> raise (CannotCoerceTo "a hint base name") else raise (CannotCoerceTo "a hint base name") @@ -239,7 +239,7 @@ let coerce_to_constr env v = let fail () = raise (CannotCoerceTo "a term") in if has_type v (topwit wit_intro_pattern) then match out_gen (topwit wit_intro_pattern) v with - | _, IntroNaming (IntroIdentifier id) -> + | {CAst.v=IntroNaming (IntroIdentifier id)} -> (try ([], constr_of_id env id) with Not_found -> fail ()) | _ -> fail () else if has_type v (topwit wit_constr) then @@ -268,7 +268,7 @@ let coerce_to_evaluable_ref env sigma v = let ev = if has_type v (topwit wit_intro_pattern) then match out_gen (topwit wit_intro_pattern) v with - | _, IntroNaming (IntroIdentifier id) when is_variable env id -> EvalVarRef id + | {CAst.v=IntroNaming (IntroIdentifier id)} when is_variable env id -> EvalVarRef id | _ -> fail () else if has_type v (topwit wit_var) then let id = out_gen (topwit wit_var) v in @@ -300,14 +300,14 @@ 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.tag ?loc @@ coerce_to_intro_pattern env sigma v in + let map v = CAst.make ?loc @@ coerce_to_intro_pattern env sigma v in List.map map l let coerce_to_hyp env sigma v = let fail () = raise (CannotCoerceTo "a variable") in if has_type v (topwit wit_intro_pattern) then match out_gen (topwit wit_intro_pattern) v with - | _, IntroNaming (IntroIdentifier id) when is_variable env id -> id + | {CAst.v=IntroNaming (IntroIdentifier id)} when is_variable env id -> id | _ -> fail () else if has_type v (topwit wit_var) then let id = out_gen (topwit wit_var) v in @@ -340,7 +340,7 @@ let coerce_to_quantified_hypothesis sigma v = if has_type v (topwit wit_intro_pattern) then let v = out_gen (topwit wit_intro_pattern) v in match v with - | _, IntroNaming (IntroIdentifier id) -> NamedHyp id + | {CAst.v=IntroNaming (IntroIdentifier id)} -> NamedHyp id | _ -> raise (CannotCoerceTo "a quantified hypothesis") else if has_type v (topwit wit_var) then let id = out_gen (topwit wit_var) v in diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 6db808dd6..8b0c44041 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -56,9 +56,9 @@ type inversion_kind = Misctypes.inversion_kind = type ('c,'d,'id) inversion_strength = | NonDepInversion of - inversion_kind * 'id list * 'd or_and_intro_pattern_expr located or_var option + inversion_kind * 'id list * 'd or_and_intro_pattern_expr CAst.t or_var option | DepInversion of - inversion_kind * 'c option * 'd or_and_intro_pattern_expr located or_var option + inversion_kind * 'c option * 'd or_and_intro_pattern_expr CAst.t or_var option | InversionUsing of 'c * 'id list type ('a,'b) location = HypLocation of 'a | ConclLocation of 'b @@ -70,8 +70,8 @@ type 'id message_token = type ('dconstr,'id) induction_clause = 'dconstr with_bindings destruction_arg * - (intro_pattern_naming_expr located option (* eqn:... *) - * 'dconstr or_and_intro_pattern_expr located or_var option) (* as ... *) + (intro_pattern_naming_expr CAst.t option (* eqn:... *) + * 'dconstr or_and_intro_pattern_expr CAst.t or_var option) (* as ... *) * 'id clause_expr option (* in ... *) type ('constr,'dconstr,'id) induction_clause_list = @@ -126,28 +126,28 @@ type delayed_open_constr_with_bindings = EConstr.constr with_bindings delayed_op type delayed_open_constr = EConstr.constr delayed_open -type intro_pattern = delayed_open_constr intro_pattern_expr located -type intro_patterns = delayed_open_constr intro_pattern_expr located list -type or_and_intro_pattern = delayed_open_constr or_and_intro_pattern_expr located -type intro_pattern_naming = intro_pattern_naming_expr located +type intro_pattern = delayed_open_constr intro_pattern_expr CAst.t +type intro_patterns = delayed_open_constr intro_pattern_expr CAst.t list +type or_and_intro_pattern = delayed_open_constr or_and_intro_pattern_expr CAst.t +type intro_pattern_naming = intro_pattern_naming_expr CAst.t (** Generic expressions for atomic tactics *) type 'a gen_atomic_tactic_expr = (* Basic tactics *) - | TacIntroPattern of evars_flag * 'dtrm intro_pattern_expr located list + | TacIntroPattern of evars_flag * 'dtrm intro_pattern_expr CAst.t list | TacApply of advanced_flag * evars_flag * 'trm with_bindings_arg list * - ('nam * 'dtrm intro_pattern_expr located option) option + ('nam * 'dtrm intro_pattern_expr CAst.t option) option | TacElim of evars_flag * 'trm with_bindings_arg * 'trm with_bindings option | TacCase of evars_flag * 'trm with_bindings_arg | TacMutualFix of Id.t * int * (Id.t * int * 'trm) list | TacMutualCofix of Id.t * (Id.t * 'trm) list | TacAssert of evars_flag * bool * 'tacexpr option option * - 'dtrm intro_pattern_expr located option * 'trm + 'dtrm intro_pattern_expr CAst.t option * 'trm | TacGeneralize of ('trm with_occurrences * Name.t) list | TacLetTac of evars_flag * Name.t * 'trm * 'nam clause_expr * letin_flag * - intro_pattern_naming_expr located option + intro_pattern_naming_expr CAst.t option (* Derived basic tactics *) | TacInductionDestruct of diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 121075f72..45f4a45fc 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -93,7 +93,7 @@ let intern_string_or_var = intern_or_var (fun (s : string) -> s) let intern_global_reference ist = function | Ident (loc,id) when find_var id ist -> - ArgVar CAst.(make ?loc id) + ArgVar (make ?loc id) | r -> let loc,_ as lqid = qualid_of_reference r in try ArgArg (loc,locate_global_with_alias lqid) @@ -103,20 +103,20 @@ let intern_ltac_variable ist = function | Ident (loc,id) -> if find_var id ist then (* A local variable of any type *) - ArgVar CAst.(make ?loc id) + ArgVar (make ?loc id) else raise Not_found | _ -> raise Not_found let intern_constr_reference strict ist = function | Ident (_,id) as r when not strict && find_hyp id ist -> - (DAst.make @@ GVar id), Some (CAst.make @@ CRef (r,None)) + (DAst.make @@ GVar id), Some (make @@ CRef (r,None)) | Ident (_,id) as r when find_var id ist -> - (DAst.make @@ GVar id), if strict then None else Some (CAst.make @@ CRef (r,None)) + (DAst.make @@ GVar id), if strict then None else Some (make @@ CRef (r,None)) | r -> let loc,_ as lqid = qualid_of_reference r in DAst.make @@ GRef (locate_global_with_alias lqid,None), - if strict then None else Some (CAst.make @@ CRef (r,None)) + if strict then None else Some (make @@ CRef (r,None)) (* Internalize an isolated reference in position of tactic *) @@ -168,7 +168,7 @@ let intern_non_tactic_reference strict ist r = (* By convention, use IntroIdentifier for unbound ident, when not in a def *) match r with | Ident (loc,id) when not strict -> - let ipat = in_gen (glbwit wit_intro_pattern) (loc, IntroNaming (IntroIdentifier id)) in + let ipat = in_gen (glbwit wit_intro_pattern) (make ?loc @@ IntroNaming (IntroIdentifier id)) in TacGeneric ipat | _ -> (* Reference not found *) @@ -209,8 +209,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 = map (fun (b,c) -> + intern_binding_name ist b,intern_constr ist c) let intern_bindings ist = function | NoBindings -> NoBindings @@ -223,12 +223,12 @@ let intern_constr_with_bindings ist (c,bl) = let intern_constr_with_bindings_arg ist (clear,c) = (clear,intern_constr_with_bindings ist c) -let rec intern_intro_pattern lf ist = function - | loc, IntroNaming pat -> - loc, IntroNaming (intern_intro_pattern_naming lf ist pat) - | loc, IntroAction pat -> - loc, IntroAction (intern_intro_pattern_action lf ist pat) - | loc, IntroForthcoming _ as x -> x +let rec intern_intro_pattern lf ist = map (function + | IntroNaming pat -> + IntroNaming (intern_intro_pattern_naming lf ist pat) + | IntroAction pat -> + IntroAction (intern_intro_pattern_action lf ist pat) + | IntroForthcoming _ as x -> x) and intern_intro_pattern_naming lf ist = function | IntroIdentifier id -> @@ -239,12 +239,12 @@ and intern_intro_pattern_naming lf ist = function and intern_intro_pattern_action lf ist = function | IntroOrAndPattern l -> - IntroOrAndPattern (intern_or_and_intro_pattern lf ist l) + IntroOrAndPattern (intern_or_and_intro_pattern lf ist l) | IntroInjection l -> - IntroInjection (List.map (intern_intro_pattern lf ist) l) + IntroInjection (List.map (intern_intro_pattern lf ist) l) | IntroWildcard | IntroRewrite _ as x -> x - | IntroApplyOn ((loc,c),pat) -> - IntroApplyOn ((loc,intern_constr ist c), intern_intro_pattern lf ist pat) + | IntroApplyOn ({loc;v=c},pat) -> + IntroApplyOn (make ?loc @@ intern_constr ist c, intern_intro_pattern lf ist pat) and intern_or_and_intro_pattern lf ist = function | IntroAndPattern l -> @@ -256,10 +256,10 @@ let intern_or_and_intro_pattern_loc lf ist = function | ArgVar {v=id} as x -> if find_var id ist then x else user_err Pp.(str "Disjunctive/conjunctive introduction pattern expected.") - | ArgArg (loc,l) -> ArgArg (loc,intern_or_and_intro_pattern lf ist l) + | ArgArg ll -> ArgArg (map (fun l -> intern_or_and_intro_pattern lf ist l) ll) -let intern_intro_pattern_naming_loc lf ist (loc,pat) = - (loc,intern_intro_pattern_naming lf ist pat) +let intern_intro_pattern_naming_loc lf ist = map (fun pat -> + intern_intro_pattern_naming lf ist pat) (* TODO: catch ltac vars *) let intern_destruction_arg ist = function @@ -268,15 +268,15 @@ let intern_destruction_arg ist = function | clear,ElimOnIdent {loc;v=id} -> if !strict_check then (* If in a defined tactic, no intros-until *) - let c, p = intern_constr ist (CAst.make @@ CRef (Ident (Loc.tag id), None)) in + let c, p = intern_constr ist (make @@ CRef (Ident (Loc.tag id), None)) in match DAst.get c with - | GVar id -> clear,ElimOnIdent CAst.(make ?loc:c.loc id) + | GVar id -> clear,ElimOnIdent (make ?loc:c.loc id) | _ -> clear,ElimOnConstr ((c, p), NoBindings) else - clear,ElimOnIdent CAst.(make ?loc id) + clear,ElimOnIdent (make ?loc id) let short_name = function - | AN (Ident (loc,id)) when not !strict_check -> Some CAst.(make ?loc id) + | AN (Ident (loc,id)) when not !strict_check -> Some (make ?loc id) | _ -> None let intern_evaluable_global_reference ist r = @@ -289,16 +289,16 @@ 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;v=(ntn,sc)} -> evaluable_of_global_reference ist.genv (Notation.interp_notation_as_global_reference ?loc (function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc) (* Globalize a reduction expression *) let intern_evaluable ist = function - | AN (Ident (loc,id)) when find_var id ist -> ArgVar CAst.(make ?loc id) + | AN (Ident (loc,id)) when find_var id ist -> ArgVar (make ?loc id) | AN (Ident (loc,id)) when not !strict_check && find_hyp id ist -> - ArgArg (EvalVarRef id, Some CAst.(make ?loc id)) + ArgArg (EvalVarRef id, Some (make ?loc id)) | r -> let e = intern_evaluable_reference_or_by_notation ist r in let na = short_name r in @@ -817,7 +817,7 @@ let notation_subst bindings tac = let fold id c accu = let loc = Glob_ops.loc_of_glob_constr (fst c) in let c = ConstrMayEval (ConstrTerm c) in - (CAst.make ?loc @@ Name id, c) :: accu + (make ?loc @@ Name id, c) :: accu in let bindings = Id.Map.fold fold bindings [] in (** This is theoretically not correct due to potential variable capture, but diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 991afe9c6..a287b13b9 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -247,7 +247,7 @@ let coerce_to_tactic loc id v = | _ -> fail () else fail () -let intro_pattern_of_ident id = (Loc.tag @@ IntroNaming (IntroIdentifier id)) +let intro_pattern_of_ident id = make @@ IntroNaming (IntroIdentifier id) let value_of_ident id = in_gen (topwit wit_intro_pattern) (intro_pattern_of_ident id) @@ -423,7 +423,7 @@ let extract_ltac_constr_values ist env = could barely be defined as a feature... *) (* Extract the identifier list from lfun: join all branches (what to do else?)*) -let rec intropattern_ids accu (loc,pat) = match pat with +let rec intropattern_ids accu {loc;v=pat} = match pat with | IntroNaming (IntroIdentifier id) -> Id.Set.add id accu | IntroAction (IntroOrAndPattern (IntroAndPattern l)) -> List.fold_left intropattern_ids accu l @@ -431,7 +431,7 @@ let rec intropattern_ids accu (loc,pat) = match pat with List.fold_left intropattern_ids accu (List.flatten ll) | IntroAction (IntroInjection l) -> List.fold_left intropattern_ids accu l - | IntroAction (IntroApplyOn ((_,c),pat)) -> intropattern_ids accu pat + | IntroAction (IntroApplyOn ({v=c},pat)) -> intropattern_ids accu pat | IntroNaming (IntroAnonymous | IntroFresh _) | IntroAction (IntroWildcard | IntroRewrite _) | IntroForthcoming _ -> accu @@ -439,9 +439,9 @@ let rec intropattern_ids accu (loc,pat) = match pat with let extract_ids ids lfun accu = let fold id v accu = if has_type v (topwit wit_intro_pattern) then - let (_, ipat) = out_gen (topwit wit_intro_pattern) v in + let {v=ipat} = out_gen (topwit wit_intro_pattern) v in if Id.List.mem id ids then accu - else intropattern_ids accu (Loc.tag ipat) + else intropattern_ids accu (make ipat) else accu in Id.Map.fold fold lfun accu @@ -762,15 +762,15 @@ let interp_message ist l = Ftactic.List.map (interp_message_token ist) l >>= fun l -> Ftactic.return (prlist_with_sep spc (fun x -> x) l) -let rec interp_intro_pattern ist env sigma = function - | loc, IntroAction pat -> - let (sigma,pat) = interp_intro_pattern_action ist env sigma pat in - sigma, (loc, IntroAction pat) - | loc, IntroNaming (IntroIdentifier id) -> - sigma, (loc, interp_intro_pattern_var loc ist env sigma id) - | loc, IntroNaming pat -> - sigma, (loc, IntroNaming (interp_intro_pattern_naming loc ist env sigma pat)) - | loc, IntroForthcoming _ as x -> sigma, x +let rec interp_intro_pattern ist env sigma = with_loc_val (fun ?loc -> function + | IntroAction pat -> + let (sigma,pat) = interp_intro_pattern_action ist env sigma pat in + sigma, make ?loc @@ IntroAction pat + | IntroNaming (IntroIdentifier id) -> + sigma, make ?loc @@ interp_intro_pattern_var loc ist env sigma id + | IntroNaming pat -> + sigma, make ?loc @@ IntroNaming (interp_intro_pattern_naming loc ist env sigma pat) + | IntroForthcoming _ as x -> sigma, make ?loc x) and interp_intro_pattern_naming loc ist env sigma = function | IntroFresh id -> IntroFresh (interp_ident ist env sigma id) @@ -784,10 +784,10 @@ and interp_intro_pattern_action ist env sigma = function | IntroInjection l -> let sigma,l = interp_intro_pattern_list_as_list ist env sigma l in sigma, IntroInjection l - | IntroApplyOn ((loc,c),ipat) -> + | IntroApplyOn ({loc;v=c},ipat) -> let c env sigma = interp_open_constr ist env sigma c in let sigma,ipat = interp_intro_pattern ist env sigma ipat in - sigma, IntroApplyOn ((loc,c),ipat) + sigma, IntroApplyOn (make ?loc c,ipat) | IntroWildcard | IntroRewrite _ as x -> sigma, x and interp_or_and_intro_pattern ist env sigma = function @@ -799,7 +799,7 @@ and interp_or_and_intro_pattern ist env sigma = function sigma, IntroOrPattern ll and interp_intro_pattern_list_as_list ist env sigma = function - | [loc,IntroNaming (IntroIdentifier id)] as l -> + | [{loc;v=IntroNaming (IntroIdentifier id)}] as l -> (try sigma, coerce_to_intro_pattern_list ?loc env sigma (Id.Map.find id ist.lfun) with Not_found | CannotCoerceTo _ -> List.fold_left_map (interp_intro_pattern ist env) sigma l) @@ -807,18 +807,18 @@ and interp_intro_pattern_list_as_list ist env sigma = function let interp_intro_pattern_naming_option ist env sigma = function | None -> None - | Some (loc,pat) -> Some (loc, interp_intro_pattern_naming loc ist env sigma pat) + | Some lpat -> Some (map_with_loc (fun ?loc pat -> interp_intro_pattern_naming loc ist env sigma pat) lpat) let interp_or_and_intro_pattern_option ist env sigma = function | None -> sigma, None | Some (ArgVar {loc;v=id}) -> (match interp_intro_pattern_var loc ist env sigma id with - | IntroAction (IntroOrAndPattern l) -> sigma, Some (loc,l) + | IntroAction (IntroOrAndPattern l) -> sigma, Some (make ?loc l) | _ -> user_err ?loc (str "Cannot coerce to a disjunctive/conjunctive pattern.")) - | Some (ArgArg (loc,l)) -> + | Some (ArgArg {loc;v=l}) -> let sigma,l = interp_or_and_intro_pattern ist env sigma l in - sigma, Some (loc,l) + sigma, Some (make ?loc l) let interp_intro_pattern_option ist env sigma = function | None -> sigma, None @@ -846,9 +846,9 @@ let interp_declared_or_quantified_hypothesis ist env sigma = function (coerce_to_decl_or_quant_hyp env sigma) ist (Some (env,sigma)) (make id) with Not_found -> NamedHyp id -let interp_binding ist env sigma (loc,(b,c)) = +let interp_binding ist env sigma {loc;v=(b,c)} = let sigma, c = interp_open_constr ist env sigma c in - sigma, (loc,(interp_binding_name ist env sigma b,c)) + sigma, (make ?loc (interp_binding_name ist env sigma b,c)) let interp_bindings ist env sigma = function | NoBindings -> @@ -873,7 +873,7 @@ let interp_open_constr_with_bindings ist env sigma (c,bl) = let loc_of_bindings = function | NoBindings -> None | ImplicitBindings l -> loc_of_glob_constr (fst (List.last l)) -| ExplicitBindings l -> fst (List.last l) +| ExplicitBindings l -> (List.last l).loc let interp_open_constr_with_bindings_loc ist ((c,_),bl as cb) = let loc1 = loc_of_glob_constr c in @@ -896,7 +896,7 @@ let interp_destruction_arg ist gl arg = in let try_cast_id id' = if Tactics.is_quantified_hypothesis id' gl - then keep,ElimOnIdent CAst.(make ?loc id') + then keep,ElimOnIdent (make ?loc id') else (keep, ElimOnConstr begin fun env sigma -> try (sigma, (constr_of_id env id', NoBindings)) @@ -911,7 +911,7 @@ let interp_destruction_arg ist gl arg = if has_type v (topwit wit_intro_pattern) then let v = out_gen (topwit wit_intro_pattern) v in match v with - | _, IntroNaming (IntroIdentifier id) -> try_cast_id id + | {v=IntroNaming (IntroIdentifier id)} -> try_cast_id id | _ -> error () else if has_type v (topwit wit_var) then let id = out_gen (topwit wit_var) v in @@ -924,9 +924,9 @@ let interp_destruction_arg ist gl arg = with Not_found -> (* We were in non strict (interactive) mode *) if Tactics.is_quantified_hypothesis id gl then - keep,ElimOnIdent CAst.(make ?loc id) + keep,ElimOnIdent (make ?loc id) else - let c = (DAst.make ?loc @@ GVar id,Some (CAst.make @@ CRef (Ident (loc,id),None))) in + let c = (DAst.make ?loc @@ GVar id,Some (make @@ CRef (Ident (loc,id),None))) in let f env sigma = let (sigma,c) = interp_open_constr ist env sigma c in (sigma, (c,NoBindings)) @@ -1221,7 +1221,7 @@ and interp_tacarg ist arg : Val.t Ftactic.t = | TacFreshId l -> Ftactic.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) (Loc.tag @@ IntroNaming (IntroIdentifier id))) + Ftactic.return (in_gen (topwit wit_intro_pattern) (make @@ IntroNaming (IntroIdentifier id))) end | TacPretype c -> Ftactic.enter begin fun gl -> @@ -1576,7 +1576,7 @@ and interp_atomic ist tac : unit Proofview.tactic = let sigma = project gl in let l = List.map (fun (k,c) -> let loc, f = interp_open_constr_with_bindings_loc ist c in - (k,(loc,f))) cb + (k,(make ?loc f))) cb in let sigma,tac = match cl with | None -> sigma, Tactics.apply_with_delayed_bindings_gen a ev l @@ -1677,7 +1677,7 @@ and interp_atomic ist tac : unit Proofview.tactic = let flags = open_constr_use_classes_flags () in let (sigma,c_interp) = interp_open_constr ~flags ist env sigma c in let let_tac b na c cl eqpat = - let id = Option.default (Loc.tag IntroAnonymous) eqpat in + let id = Option.default (make 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 @@ -1689,7 +1689,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.tag IntroAnonymous) eqpat in + let id = Option.default (make IntroAnonymous) eqpat in let with_eq = if b then None else Some (true,id) in Tactics.letin_pat_tac ev with_eq na c cl in diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index 927139c1a..a1d8b087e 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -33,8 +33,9 @@ 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 = + CAst.map (fun (b,c) -> + subst_quantified_hypothesis subst b,subst_glob_constr subst c) let subst_bindings subst = function | NoBindings -> NoBindings @@ -47,13 +48,13 @@ let subst_glob_with_bindings subst (c,bl) = let subst_glob_with_bindings_arg subst (clear,c) = (clear,subst_glob_with_bindings subst c) -let rec subst_intro_pattern subst = function - | loc,IntroAction p -> loc, IntroAction (subst_intro_pattern_action subst p) - | loc, IntroNaming _ | loc, IntroForthcoming _ as x -> x +let rec subst_intro_pattern subst = CAst.map (function + | IntroAction p -> IntroAction (subst_intro_pattern_action subst p) + | IntroNaming _ | IntroForthcoming _ as x -> x) -and subst_intro_pattern_action subst = function - | IntroApplyOn ((loc,t),pat) -> - IntroApplyOn ((loc,subst_glob_constr subst t),subst_intro_pattern subst pat) +and subst_intro_pattern_action subst = let open CAst in function + | IntroApplyOn ({loc;v=t},pat) -> + IntroApplyOn (make ?loc @@ subst_glob_constr subst t,subst_intro_pattern subst pat) | IntroOrAndPattern l -> IntroOrAndPattern (subst_intro_or_and_pattern subst l) | IntroInjection l -> IntroInjection (List.map (subst_intro_pattern subst) l) diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 52822e444..168105e8f 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -1991,7 +1991,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.tag @@ Misctypes.IntroNaming (Misctypes.IntroIdentifier id)) in + let ipat_of_name id = Some (CAst.make @@ Misctypes.IntroNaming (Misctypes.IntroIdentifier id)) in let goal_name = fresh_id Id.Set.empty (Names.Id.of_string "__arith") gl in let env' = List.map (fun (id,i) -> EConstr.mkVar id,i) vars in @@ -2106,7 +2106,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.tag @@ Misctypes.IntroNaming (Misctypes.IntroIdentifier id)) in + let ipat_of_name id = Some (CAst.make @@ Misctypes.IntroNaming (Misctypes.IntroIdentifier id)) in let goal_name = fresh_id Id.Set.empty (Names.Id.of_string "__arith") gl in let env' = List.map (fun (id,i) -> EConstr.mkVar id,i) vars in diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index 2bed8b624..2f8b8cb02 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -541,7 +541,7 @@ END (* ipats *) -let remove_loc = snd +let remove_loc x = x.CAst.v let ipat_of_intro_pattern p = Misctypes.( let rec ipat_of_intro_pattern = function @@ -608,14 +608,15 @@ let interp_intro_pattern = interp_wit wit_intro_pattern let interp_introid ist gl id = Misctypes.( try IntroNaming (IntroIdentifier (hyp_id (snd (interp_hyp ist gl (SsrHyp (Loc.tag id)))))) - with _ -> snd(snd (interp_intro_pattern ist gl (Loc.tag @@ IntroNaming (IntroIdentifier id)))) + with _ -> (snd (interp_intro_pattern ist gl (CAst.make @@ IntroNaming (IntroIdentifier id)))).CAst.v ) let get_intro_id = function | IntroNaming (IntroIdentifier id) -> id | _ -> assert false -let rec add_intro_pattern_hyps (loc, ipat) hyps = Misctypes.( +let rec add_intro_pattern_hyps ipat hyps = Misctypes.( + let {CAst.loc=loc;v=ipat} = ipat in match ipat with | IntroNaming (IntroIdentifier id) -> if not_section_id id then SsrHyp (loc, id) :: hyps else @@ -646,7 +647,7 @@ let interp_ipat ist gl = | IPatClear clr -> let add_hyps (SsrHyp (loc, id) as hyp) hyps = if not (ltacvar id) then hyp :: hyps else - add_intro_pattern_hyps (loc, (interp_introid ist gl id)) hyps in + add_intro_pattern_hyps CAst.(make ?loc (interp_introid ist gl id)) hyps in let clr' = List.fold_right add_hyps clr [] in check_hyps_uniq [] clr'; IPatClear clr' | IPatCase(iorpat) -> diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 10e259209..a5b7a9e6f 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -347,7 +347,7 @@ let unify_tomatch_with_patterns evdref env loc typ pats realnames = let find_tomatch_tycon evdref env loc = function (* Try if some 'in I ...' is present and can be used as a constraint *) - | Some (_,(ind,realnal)) -> + | Some {CAst.v=(ind,realnal)} -> mk_tycon (inductive_template evdref env loc ind),Some (List.rev realnal) | None -> empty_tycon,None @@ -1565,7 +1565,7 @@ substituer après par les initiaux *) * and linearizing the _ patterns. * Syntactic correctness has already been done in constrintern *) let matx_of_eqns env eqns = - let build_eqn (loc,(ids,initial_lpat,initial_rhs)) = + let build_eqn {CAst.loc;v=(ids,initial_lpat,initial_rhs)} = let avoid = ids_of_named_context_val (named_context_val env) in let avoid = List.fold_left (fun accu id -> Id.Set.add id accu) avoid ids in let rhs = @@ -1883,8 +1883,8 @@ let extract_arity_signature ?(dolift=true) env0 lvar tomatchl tmsign = | None -> let sign = match bo with | None -> [LocalAssum (na, lift n typ)] | Some b -> [LocalDef (na, lift n b, lift n typ)] in sign,sign - | Some (loc,_) -> - user_err ?loc + | Some {CAst.loc} -> + user_err ?loc (str"Unexpected type annotation for a term of non inductive type.")) | IsInd (term,IndType(indf,realargs),_) -> let indf' = if dolift then lift_inductive_family n indf else indf in @@ -1894,7 +1894,7 @@ let extract_arity_signature ?(dolift=true) env0 lvar tomatchl tmsign = let arsign = List.map (fun d -> map_rel_decl EConstr.of_constr d) arsign in let realnal, realnal' = match t with - | Some (loc,(ind',realnal)) -> + | Some {CAst.loc;v=(ind',realnal)} -> if not (eq_ind ind ind') then user_err ?loc (str "Wrong inductive type."); if not (Int.equal nrealargs_ctxt (List.length realnal)) then diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index f98a3b0db..8fab92779 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -279,7 +279,7 @@ let _ = optwrite = (fun b -> print_allow_match_default_clause := b) } let rec join_eqns (ids,rhs as x) patll = function - | (loc,(ids',patl',rhs') as eqn')::rest -> + | ({CAst.loc; v=(ids',patl',rhs')} as eqn')::rest -> if not !Flags.raw_print && !print_factorize_match_patterns && List.eq_set Id.equal ids ids' && glob_constr_eq rhs rhs' then @@ -290,9 +290,9 @@ let rec join_eqns (ids,rhs as x) patll = function | [] -> patll, [] -let number_of_patterns (_gloc,(_ids,patll,_rhs)) = List.length patll +let number_of_patterns {CAst.v=(_ids,patll,_rhs)} = List.length patll -let is_default_candidate (_gloc,(ids,_patll,_rhs) ) = ids = [] +let is_default_candidate {CAst.v=(ids,_patll,_rhs)} = ids = [] let rec move_more_factorized_default_candidate_to_end eqn n = function | eqn' :: eqns -> @@ -316,22 +316,26 @@ let rec select_default_clause = function | [] -> None, [] let factorize_eqns eqns = + let open CAst in let rec aux found = function - | (loc,(ids,patl,rhs))::rest -> + | {loc;v=(ids,patl,rhs)}::rest -> let patll,rest = join_eqns (ids,rhs) [patl] rest in - aux ((loc,(ids,patll,rhs))::found) rest + aux (CAst.make ?loc (ids,patll,rhs)::found) rest | [] -> found in let eqns = aux [] (List.rev eqns) in let mk_anon patl = List.map (fun _ -> DAst.make @@ PatVar Anonymous) patl in + let open CAst in if not !Flags.raw_print && !print_allow_match_default_clause && eqns <> [] then match select_default_clause eqns with (* At least two clauses and the last one is disjunctive with no variables *) - | Some (gloc,([],patl::_::_,rhs)), (_::_ as eqns) -> eqns@[gloc,([],[mk_anon patl],rhs)] + | Some {loc=gloc;v=([],patl::_::_,rhs)}, (_::_ as eqns) -> + eqns@[CAst.make ?loc:gloc ([],[mk_anon patl],rhs)] (* Only one clause which is disjunctive with no variables: we keep at least one constructor *) (* so that it is not interpreted as a dummy "match" *) - | Some (gloc,([],patl::patl'::_,rhs)), [] -> [gloc,([],[patl;mk_anon patl'],rhs)] - | Some (_,((_::_,_,_ | _,([]|[_]),_))), _ -> assert false + | Some {loc=gloc;v=([],patl::patl'::_,rhs)}, [] -> + [CAst.make ?loc:gloc ([],[patl;mk_anon patl'],rhs)] + | Some {v=((_::_,_,_ | _,([]|[_]),_))}, _ -> assert false | None, eqns -> eqns else eqns @@ -460,7 +464,7 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl = | _ -> Anonymous, typ in let aliastyp = if List.for_all (Name.equal Anonymous) nl then None - else Some (Loc.tag (indsp,nl)) in + else Some (CAst.make (indsp,nl)) in n, aliastyp, Some typ in let constructs = Array.init (Array.length bl) (fun i -> (indsp,i+1)) in @@ -726,7 +730,8 @@ and detype_eqns d flags avoid env sigma ci computable constructs consnargsl bl = try if !Flags.raw_print || not (reverse_matching ()) then raise Exit; let mat = build_tree Anonymous (snd flags) (avoid,env) sigma ci bl in - List.map (fun (ids,pat,((avoid,env),c)) -> Loc.tag (Id.Set.elements ids,[pat],detype d flags avoid env sigma c)) + List.map (fun (ids,pat,((avoid,env),c)) -> + CAst.make (Id.Set.elements ids,[pat],detype d flags avoid env sigma c)) mat with e when CErrors.noncritical e -> Array.to_list @@ -743,7 +748,7 @@ and detype_eqn d (lax,isgoal as flags) avoid env sigma constr construct_nargs br in let rec buildrec ids patlist avoid env l b = match EConstr.kind sigma b, l with - | _, [] -> Loc.tag @@ + | _, [] -> CAst.make @@ (Id.Set.elements ids, [DAst.make @@ PatCstr(constr, List.rev patlist,Anonymous)], detype d flags avoid env sigma b) @@ -934,22 +939,23 @@ let rec subst_glob_constr subst = DAst.map (function GLetIn (n,r1',t',r2') | GCases (sty,rtno,rl,branches) as raw -> + let open CAst in let rtno' = Option.smartmap (subst_glob_constr subst) rtno and rl' = List.smartmap (fun (a,x as y) -> let a' = subst_glob_constr subst a in let (n,topt) = x in let topt' = Option.smartmap - (fun ((loc,((sp,i),y) as t)) -> + (fun ({loc;v=((sp,i),y)} as t) -> let sp' = subst_mind subst sp in - if sp == sp' then t else (loc,((sp',i),y))) topt in + if sp == sp' then t else CAst.(make ?loc ((sp',i),y))) topt in if a == a' && topt == topt' then y else (a',(n,topt'))) rl and branches' = List.smartmap - (fun (loc,(idl,cpl,r) as branch) -> + (fun ({loc;v=(idl,cpl,r)} as branch) -> let cpl' = List.smartmap (subst_cases_pattern subst) cpl and r' = subst_glob_constr subst r in if cpl' == cpl && r' == r then branch else - (loc,(idl,cpl',r'))) + CAst.(make ?loc (idl,cpl',r'))) branches in if rtno' == rtno && rl' == rl && branches' == branches then raw else @@ -1014,9 +1020,9 @@ let simple_cases_matrix_of_branches ind brs = let mkPatVar na = DAst.make @@ PatVar na in let p = DAst.make @@ PatCstr ((ind,i+1),List.map mkPatVar nal,Anonymous) in let ids = List.map_filter Nameops.Name.to_option nal in - Loc.tag @@ (ids,[p],c)) + CAst.make @@ (ids,[p],c)) brs let return_type_of_predicate ind nrealargs_tags pred = let nal,p = it_destRLambda_or_LetIn_names (nrealargs_tags@[false]) pred in - (List.hd nal, Some (Loc.tag (ind, List.tl nal))), Some p + (List.hd nal, Some (CAst.make (ind, List.tl nal))), Some p diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 2280ee2d4..74f2cefab 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -9,6 +9,7 @@ (************************************************************************) open Util +open CAst open Names open Nameops open Globnames @@ -34,7 +35,7 @@ let set_pat_alias id = DAst.map (function let cases_predicate_names tml = List.flatten (List.map (function | (tm,(na,None)) -> [na] - | (tm,(na,Some (_,(_,nal)))) -> na::nal) tml) + | (tm,(na,Some {v=(_,nal)})) -> na::nal) tml) let mkGApp ?loc p t = DAst.make ?loc @@ match DAst.get p with @@ -79,13 +80,13 @@ let matching_var_kind_eq k1 k2 = match k1, k2 with | (FirstOrderPatVar _ | SecondOrderPatVar _), _ -> false let tomatch_tuple_eq f (c1, p1) (c2, p2) = - let eqp (_, (i1, na1)) (_, (i2, na2)) = + let eqp {CAst.v=(i1, na1)} {CAst.v=(i2, na2)} = eq_ind i1 i2 && List.equal Name.equal na1 na2 in let eq_pred (n1, o1) (n2, o2) = Name.equal n1 n2 && Option.equal eqp o1 o2 in f c1 c2 && eq_pred p1 p2 -and cases_clause_eq f (_, (id1, p1, c1)) (_, (id2, p2, c2)) = +and cases_clause_eq f {CAst.v=(id1, p1, c1)} {CAst.v=(id2, p2, c2)} = List.equal Id.equal id1 id2 && List.equal cases_pattern_eq p1 p2 && f c1 c2 let glob_decl_eq f (na1, bk1, c1, t1) (na2, bk2, c2, t2) = @@ -173,7 +174,7 @@ let map_glob_constr_left_to_right f = DAst.map (function | GCases (sty,rtntypopt,tml,pl) -> let comp1 = Option.map f rtntypopt in let comp2 = Util.List.map_left (fun (tm,x) -> (f tm,x)) tml in - let comp3 = Util.List.map_left (fun (loc,(idl,p,c)) -> (loc,(idl,p,f c))) pl in + let comp3 = Util.List.map_left (CAst.map (fun (idl,p,c) -> (idl,p,f c))) pl in GCases (sty,comp1,comp2,comp3) | GLetTuple (nal,(na,po),b,c) -> let comp1 = Option.map f po in @@ -211,7 +212,7 @@ let fold_glob_constr f acc = DAst.with_val (function | GLetIn (_,b,t,c) -> f (Option.fold_left f (f acc b) t) c | GCases (_,rtntypopt,tml,pl) -> - let fold_pattern acc (_,(idl,p,c)) = f acc c in + let fold_pattern acc {CAst.v=(idl,p,c)} = f acc c in List.fold_left fold_pattern (List.fold_left f (Option.fold_left f acc rtntypopt) (List.map fst tml)) pl @@ -244,9 +245,9 @@ let fold_glob_constr_with_binders g f v acc = DAst.(with_val (function | GLetIn (na,b,t,c) -> f (Name.fold_right g na v) (Option.fold_left (f v) (f v acc b) t) c | GCases (_,rtntypopt,tml,pl) -> - let fold_pattern acc (_,(idl,p,c)) = f (List.fold_right g idl v) acc c in + let fold_pattern acc {v=(idl,p,c)} = f (List.fold_right g idl v) acc c in let fold_tomatch (v',acc) (tm,(na,onal)) = - (Option.fold_left (fun v'' (_,(_,nal)) -> List.fold_right (Name.fold_right g) nal v'') + (Option.fold_left (fun v'' {v=(_,nal)} -> List.fold_right (Name.fold_right g) nal v'') (Name.fold_right g na v') onal, f v acc tm) in let (v',acc) = List.fold_left fold_tomatch (v,acc) tml in @@ -336,10 +337,10 @@ let bound_glob_vars = probably be no significant penalty in doing reallocation as pattern-matching expressions are usually rather small. *) -let map_inpattern_binders f ((loc,(id,nal)) as x) = +let map_inpattern_binders f ({loc;v=(id,nal)} as x) = let r = CList.smartmap f nal in if r == nal then x - else loc,(id,r) + else CAst.make ?loc (id,r) let map_tomatch_binders f ((c,(na,inp)) as x) : tomatch_tuple = let r = Option.smartmap (fun p -> map_inpattern_binders f p) inp in @@ -360,14 +361,14 @@ let rec map_case_pattern_binders f = DAst.map (function else PatCstr(c,rps,rna) ) -let map_cases_branch_binders f ((loc,(il,cll,rhs)) as x) : cases_clause = +let map_cases_branch_binders f ({CAst.loc;v=(il,cll,rhs)} as x) : cases_clause = (* spiwack: not sure if I must do something with the list of idents. It is intended to be a superset of the free variable of the right-hand side, if I understand correctly. But I'm not sure when or how they are used. *) let r = List.smartmap (fun cl -> map_case_pattern_binders f cl) cll in if r == cll then x - else loc,(il,r,rhs) + else CAst.make ?loc (il,r,rhs) let map_pattern_binders f tomatch branches = CList.smartmap (fun tm -> map_tomatch_binders f tm) tomatch, @@ -377,8 +378,8 @@ let map_pattern_binders f tomatch branches = let map_tomatch f (c,pp) : tomatch_tuple = f c , pp -let map_cases_branch f (loc,(il,cll,rhs)) : cases_clause = - loc , (il , cll , f rhs) +let map_cases_branch f = + CAst.map (fun (il,cll,rhs) -> (il , cll , f rhs)) let map_pattern f tomatch branches = List.map (fun tm -> map_tomatch f tm) tomatch, @@ -437,11 +438,11 @@ let rec rename_glob_vars l c = force @@ DAst.map_with_loc (fun ?loc -> function (* Lazy strategy: we fail if a collision with renaming occurs, rather than renaming further *) | GCases (ci,po,tomatchl,cls) -> let test_pred_pat (na,ino) = - test_na l na; Option.iter (fun (_,(_,nal)) -> List.iter (test_na l) nal) ino in + test_na l na; Option.iter (fun {v=(_,nal)} -> List.iter (test_na l) nal) ino in let test_clause idl = List.iter (test_id l) idl in let po = Option.map (rename_glob_vars l) po in let tomatchl = Util.List.map_left (fun (tm,x) -> test_pred_pat x; (rename_glob_vars l tm,x)) tomatchl in - let cls = Util.List.map_left (fun (loc,(idl,p,c)) -> test_clause idl; (loc,(idl,p,rename_glob_vars l c))) cls in + let cls = Util.List.map_left (CAst.map (fun (idl,p,c) -> test_clause idl; (idl,p,rename_glob_vars l c))) cls in GCases (ci,po,tomatchl,cls) | GLetTuple (nal,(na,po),c,b) -> List.iter (test_na l) (na::nal); diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml index c5ce0496b..0f0af5409 100644 --- a/pretyping/miscops.ml +++ b/pretyping/miscops.ml @@ -65,7 +65,7 @@ let map_red_expr_gen f g h = function (** Mapping bindings *) let map_explicit_bindings f l = - let map (loc, (hyp, x)) = (loc, (hyp, f x)) in + let map = CAst.map (fun (hyp, x) -> (hyp, f x)) in List.map map l let map_bindings f = function diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 3fab553cb..dcb93bfb6 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -416,17 +416,17 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function | _ -> None in let get_ind = function - | (_,(_,[p],_))::_ -> get_ind p + | {CAst.v=(_,[p],_)}::_ -> get_ind p | _ -> None in let ind_tags,ind = match indnames with - | Some (_,(ind,nal)) -> Some (List.length nal), Some ind + | Some {CAst.v=(ind,nal)} -> Some (List.length nal), Some ind | None -> None, get_ind brs in let ext,brs = pats_of_glob_branches loc metas vars ind brs in let pred = match p,indnames with - | Some p, Some (_,(_,nal)) -> + | Some p, Some {CAst.v=(_,nal)} -> let nvars = na :: List.rev nal @ vars in rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas nvars p)) | None, _ -> PMeta None @@ -462,7 +462,7 @@ and pats_of_glob_branches loc metas vars ind brs = in let rec get_pat indexes = function | [] -> false, [] - | (loc',(_,[p], br)) :: brs -> + | {CAst.loc=loc';v=(_,[p], br)} :: brs -> begin match DAst.get p, DAst.get br, brs with | PatVar Anonymous, GHole _, [] -> true, [] (* ends with _ => _ *) @@ -484,7 +484,7 @@ and pats_of_glob_branches loc metas vars ind brs = | _ -> err ?loc:loc' (Pp.str "Non supported pattern.") end - | (loc,(_,_,_)) :: _ -> err ?loc (Pp.str "Non supported pattern.") + | {CAst.loc;v=(_,_,_)} :: _ -> err ?loc (Pp.str "Non supported pattern.") in get_pat Int.Set.empty brs diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml index 6475388f9..e10c81c24 100644 --- a/pretyping/typeclasses_errors.ml +++ b/pretyping/typeclasses_errors.ml @@ -9,7 +9,6 @@ (************************************************************************) (*i*) -open Names open EConstr open Environ open Constrexpr @@ -20,7 +19,7 @@ type contexts = Parameters | Properties type typeclass_error = | NotAClass of constr - | UnboundMethod of global_reference * Id.t Loc.located (* Class name, method *) + | UnboundMethod of global_reference * Misctypes.lident (* Class name, method *) | MismatchedContextInstance of contexts * constr_expr list * Context.Rel.t (* found, expected *) exception TypeClassError of env * typeclass_error diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli index ce647029f..d98295658 100644 --- a/pretyping/typeclasses_errors.mli +++ b/pretyping/typeclasses_errors.mli @@ -8,8 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Loc -open Names open EConstr open Environ open Constrexpr @@ -19,14 +17,14 @@ type contexts = Parameters | Properties type typeclass_error = | NotAClass of constr - | UnboundMethod of global_reference * Id.t located (** Class name, method *) + | UnboundMethod of global_reference * Misctypes.lident (** Class name, method *) | MismatchedContextInstance of contexts * constr_expr list * Context.Rel.t (** found, expected *) exception TypeClassError of env * typeclass_error val not_a_class : env -> constr -> 'a -val unbound_method : env -> global_reference -> Id.t located -> 'a +val unbound_method : env -> global_reference -> Misctypes.lident -> 'a val mismatched_ctx_inst : env -> contexts -> constr_expr list -> Context.Rel.t -> 'a diff --git a/printing/pputils.ml b/printing/pputils.ml index 010b92f3e..c2846c4cd 100644 --- a/printing/pputils.ml +++ b/printing/pputils.ml @@ -124,7 +124,7 @@ let pr_red_expr_env env sigma (pr_constr,pr_lconstr,pr_ref,pr_pattern) = 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 {CAst.v=(s,sc)} -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc let hov_if_not_empty n p = if Pp.ismt p then p else hov n p diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index ea1ca26fb..5c5b7206a 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -69,7 +69,7 @@ open Decl_kinds let pr_fqid fqid = str (string_of_fqid fqid) - let pr_lfqid (loc,fqid) = + let pr_lfqid {CAst.loc;v=fqid} = match loc with | None -> pr_fqid fqid | Some loc -> let (b,_) = Loc.unloc loc in @@ -238,7 +238,7 @@ open Decl_kinds keyword "Definition" ++ spc() ++ pr_lfqid id ++ pr_universe_decl udecl ++ str" := " ++ p | CWith_Module (id,qid) -> keyword "Module" ++ spc() ++ pr_lfqid id ++ str" := " ++ - pr_located pr_qualid qid + pr_ast pr_qualid qid let rec pr_module_ast leading_space pr_c = function | { loc ; v = CMident qid } -> diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 9da94e42a..cfc5e6b4e 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -838,7 +838,7 @@ let print_any_name env sigma na udecl = let print_name env sigma na udecl = match na with - | ByNotation (loc,(ntn,sc)) -> + | ByNotation {CAst.loc;v=(ntn,sc)} -> print_any_name env sigma (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true) ntn sc)) @@ -891,7 +891,7 @@ let print_about_any ?loc env sigma k udecl = let print_about env sigma na udecl = match na with - | ByNotation (loc,(ntn,sc)) -> + | ByNotation {CAst.loc;v=(ntn,sc)} -> print_about_any ?loc env sigma (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true) ntn sc)) udecl diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 54ba19d6a..03ff580ad 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -416,7 +416,7 @@ let qhyp_eq h1 h2 = match h1, h2 with | _ -> false let check_bindings bl = - match List.duplicates qhyp_eq (List.map (fun x -> fst (snd x)) bl) with + match List.duplicates qhyp_eq (List.map (fun {CAst.v=x} -> fst x) bl) with | NamedHyp s :: _ -> user_err (str "The variable " ++ Id.print s ++ @@ -512,7 +512,7 @@ let clenv_match_args bl clenv = let mvs = clenv_independent clenv in check_bindings bl; List.fold_left - (fun clenv (loc,(b,c)) -> + (fun clenv {CAst.loc;v=(b,c)} -> let k = meta_of_binder clenv loc mvs b in if meta_defined clenv.evd k then if EConstr.eq_constr clenv.evd (EConstr.of_constr (fst (meta_fvalue clenv.evd k)).rebus) c then clenv @@ -710,7 +710,7 @@ let solve_evar_clause env sigma hyp_only clause = function error_not_right_number_missing_arguments len | ExplicitBindings lbind -> let () = check_bindings lbind in - let fold sigma (_, (binder, c)) = + let fold sigma {CAst.v=(binder, c)} = let ev = evar_of_binder clause.cl_holes binder in define_with_type sigma env ev c in diff --git a/proofs/miscprint.ml b/proofs/miscprint.ml index e363af644..1a63ff673 100644 --- a/proofs/miscprint.ml +++ b/proofs/miscprint.ml @@ -14,7 +14,7 @@ open Misctypes (** Printing of [intro_pattern] *) -let rec pr_intro_pattern prc (_,pat) = match pat with +let rec pr_intro_pattern prc {CAst.v=pat} = match pat with | IntroForthcoming true -> str "*" | IntroForthcoming false -> str "**" | IntroNaming p -> pr_intro_pattern_naming p @@ -31,7 +31,7 @@ and pr_intro_pattern_action prc = function | IntroInjection pl -> str "[=" ++ hv 0 (prlist_with_sep spc (pr_intro_pattern prc) pl) ++ str "]" - | IntroApplyOn ((_,c),pat) -> pr_intro_pattern prc pat ++ str "%" ++ prc c + | IntroApplyOn ({CAst.v=c},pat) -> pr_intro_pattern prc pat ++ str "%" ++ prc c | IntroRewrite true -> str "->" | IntroRewrite false -> str "<-" @@ -52,9 +52,9 @@ let pr_move_location pr_id = function | MoveLast -> str " at bottom" (** Printing of bindings *) -let pr_binding prc = function - | loc, (NamedHyp id, c) -> hov 1 (Names.Id.print id ++ str " := " ++ cut () ++ prc c) - | loc, (AnonHyp n, c) -> hov 1 (int n ++ str " := " ++ cut () ++ prc c) +let pr_binding prc = let open CAst in function + | {loc;v=(NamedHyp id, c)} -> hov 1 (Names.Id.print id ++ str " := " ++ cut () ++ prc c) + | {loc;v=(AnonHyp n, c)} -> hov 1 (int n ++ str " := " ++ cut () ++ prc c) let pr_bindings prc prlc = function | ImplicitBindings l -> diff --git a/proofs/miscprint.mli b/proofs/miscprint.mli index 762d7cc87..79790a277 100644 --- a/proofs/miscprint.mli +++ b/proofs/miscprint.mli @@ -13,7 +13,7 @@ open Misctypes (** Printing of [intro_pattern] *) val pr_intro_pattern : - ('a -> Pp.t) -> 'a intro_pattern_expr Loc.located -> Pp.t + ('a -> Pp.t) -> 'a intro_pattern_expr CAst.t -> Pp.t val pr_or_and_intro_pattern : ('a -> Pp.t) -> 'a or_and_intro_pattern_expr -> Pp.t diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 15f34ccc6..d6c0e3341 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -207,7 +207,7 @@ let check_no_pending_proof () = let discard_gen id = pstates := List.filter (fun { pid = id' } -> not (Id.equal id id')) !pstates -let discard (loc,id) = +let discard {CAst.loc;v=id} = let n = List.length !pstates in discard_gen id; if Int.equal (List.length !pstates) n then @@ -297,13 +297,13 @@ let set_used_variables l = match entry with | LocalAssum (x,_) -> if Id.Set.mem x all_safe then orig - else (ctx, all_safe, (Loc.tag x)::to_clear) + else (ctx, all_safe, (CAst.make x)::to_clear) | LocalDef (x,bo, ty) as decl -> if Id.Set.mem x all_safe then orig else let vars = Id.Set.union (vars_of env bo) (vars_of env ty) in if Id.Set.subset vars all_safe then (decl :: ctx, Id.Set.add x all_safe, to_clear) - else (ctx, all_safe, (Loc.tag x) :: to_clear) in + else (ctx, all_safe, (CAst.make x) :: to_clear) in let ctx, _, to_clear = Environ.fold_named_context aux env ~init:(ctx,ctx_set,[]) in let to_clear = if !proof_using_auto_clear then to_clear else [] in diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index fb123fccb..bf35fd659 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -22,7 +22,7 @@ val check_no_pending_proof : unit -> unit val get_current_proof_name : unit -> Names.Id.t val get_all_proof_names : unit -> Names.Id.t list -val discard : Names.Id.t Loc.located -> unit +val discard : Misctypes.lident -> unit val discard_current : unit -> unit val discard_all : unit -> unit @@ -124,7 +124,7 @@ val set_endline_tactic : Genarg.glob_generic_argument -> unit * (w.r.t. type dependencies and let-ins covered by it) + a list of * ids to be cleared *) val set_used_variables : - Names.Id.t list -> Context.Named.t * Names.Id.t Loc.located list + Names.Id.t list -> Context.Named.t * Misctypes.lident list val get_used_variables : unit -> Context.Named.t option (** Get the universe declaration associated to the current proof. *) diff --git a/stm/stm.ml b/stm/stm.ml index b3da97c6e..b1cecc6d1 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1084,7 +1084,7 @@ let stm_vernac_interp ?proof ?route id st { verbose; loc; expr } : Vernacstate.t | VernacShow ShowScript -> ShowScript.show_script (); st (** XX we are ignoring control here *) | _ -> stm_pperr_endline Pp.(fun () -> str "interpreting " ++ Ppvernac.pr_vernac expr); - try Vernacentries.interp ?verbosely:(Some verbose) ?proof ~st (Loc.tag ?loc expr) + try Vernacentries.interp ?verbosely:(Some verbose) ?proof ~st (CAst.make ?loc expr) with e -> let e = CErrors.push e in Exninfo.iraise Hooks.(call_process_error_once e) @@ -2992,7 +2992,7 @@ let parse_sentence ~doc sid pa = try match Pcoq.Gram.entry_parse Pcoq.main_entry pa with | None -> raise End_of_input - | Some (loc, cmd) -> Loc.tag ~loc cmd + | Some (loc, cmd) -> CAst.make ~loc cmd with e when CErrors.noncritical e -> let (e, info) = CErrors.push e in Exninfo.iraise (e, info)) @@ -3033,7 +3033,7 @@ let compute_indentation ?loc sid = Option.cata (fun loc -> eff_indent, len ) (0, 0) loc -let add ~doc ~ontop ?newtip verb (loc, ast) = +let add ~doc ~ontop ?newtip verb { CAst.loc; v=ast } = let cur_tip = VCS.cur_tip () in if not (Stateid.equal ontop cur_tip) then user_err ?loc ~hdr:"Stm.add" @@ -3063,7 +3063,7 @@ let query ~doc ~at ~route s = else Reach.known_state ~cache:`Yes at; try while true do - let loc, ast = parse_sentence ~doc at s in + let { CAst.loc; v=ast } = parse_sentence ~doc at s in let indentation, strlen = compute_indentation ?loc at in CWarnings.set_current_loc loc; let clas = Vernac_classifier.classify_vernac ast in diff --git a/stm/stm.mli b/stm/stm.mli index f967c9815..a8eb10fb3 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -80,7 +80,7 @@ val new_doc : stm_init_options -> doc * Stateid.t (* [parse_sentence sid pa] Reads a sentence from [pa] with parsing state [sid] Returns [End_of_input] if the stream ends *) val parse_sentence : doc:doc -> Stateid.t -> Pcoq.Gram.coq_parsable -> - Vernacexpr.vernac_control Loc.located + Vernacexpr.vernac_control CAst.t (* Reminder: A parsable [pa] is constructed using [Pcoq.Gram.coq_parsable stream], where [stream : char Stream.t]. *) @@ -94,7 +94,7 @@ exception End_of_input If [newtip] is provided, then the returned state id is guaranteed to be [newtip] *) val add : doc:doc -> ontop:Stateid.t -> ?newtip:Stateid.t -> - bool -> Vernacexpr.vernac_control Loc.located -> + bool -> Vernacexpr.vernac_control CAst.t -> doc * Stateid.t * [ `NewTip | `Unfocus of Stateid.t ] (* [query at ?report_with cmd] Executes [cmd] at a given state [at], diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 780de8978..c3857e6b8 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -85,7 +85,7 @@ let print_rewrite_hintdb env sigma bas = Pputils.pr_glb_generic (Global.env()) tac) (mt ()) h.rew_tac) (find_rewrites bas)) -type raw_rew_rule = (constr Univ.in_universe_context_set * bool * Genarg.raw_generic_argument option) Loc.located +type raw_rew_rule = (constr Univ.in_universe_context_set * bool * Genarg.raw_generic_argument option) CAst.t (* Applies all the rules of one base *) let one_base general_rewrite_maybe_in tac_main bas = @@ -275,7 +275,7 @@ let add_rew_rules base lrul = let intern tac = snd (Genintern.generic_intern ist tac) in let lrul = List.fold_left - (fun dn (loc,((c,ctx),b,t)) -> + (fun dn {CAst.loc;v=((c,ctx),b,t)} -> let sigma = Evd.merge_context_set Evd.univ_rigid sigma ctx in let info = find_applied_relation ?loc false env sigma c b in let pat = if b then info.hyp_left else info.hyp_right in diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli index 96c08d58d..03e9414e0 100644 --- a/tactics/autorewrite.mli +++ b/tactics/autorewrite.mli @@ -14,7 +14,7 @@ open Constr open Equality (** Rewriting rules before tactic interpretation *) -type raw_rew_rule = (constr Univ.in_universe_context_set * bool * Genarg.raw_generic_argument option) Loc.located +type raw_rew_rule = (constr Univ.in_universe_context_set * bool * Genarg.raw_generic_argument option) CAst.t (** To add rewriting rules to a base *) val add_rew_rules : string -> raw_rew_rule list -> unit diff --git a/tactics/inv.ml b/tactics/inv.ml index 280efdaec..067fc8941 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -282,16 +282,17 @@ let generalizeRewriteIntros as_mode tac depids id = end let error_too_many_names pats = - let loc = Loc.merge_opt (fst (List.hd pats)) (fst (List.last pats)) in + let loc = Loc.merge_opt (List.hd pats).CAst.loc (List.last pats).CAst.loc in Proofview.tclENV >>= fun env -> Proofview.tclEVARMAP >>= fun sigma -> tclZEROMSG ?loc ( str "Unexpected " ++ str (String.plural (List.length pats) "introduction pattern") ++ - str ": " ++ pr_enum (Miscprint.pr_intro_pattern (fun c -> Printer.pr_constr_env env sigma (EConstr.Unsafe.to_constr (snd (c env Evd.empty))))) pats ++ + str ": " ++ pr_enum (Miscprint.pr_intro_pattern + (fun c -> Printer.pr_constr_env env sigma (EConstr.Unsafe.to_constr (snd (c env Evd.empty))))) pats ++ str ".") -let get_names (allow_conj,issimple) (loc, pat as x) = match pat with +let get_names (allow_conj,issimple) ({CAst.loc;v=pat} as x) = match pat with | IntroNaming IntroAnonymous | IntroForthcoming _ -> user_err Pp.(str "Anonymous pattern not allowed for inversion equations.") | IntroNaming (IntroFresh _) -> @@ -301,7 +302,8 @@ let get_names (allow_conj,issimple) (loc, pat as x) = match pat with | IntroAction (IntroRewrite _) -> user_err Pp.(str "Rewriting pattern not allowed for inversion equations.") | IntroAction (IntroOrAndPattern (IntroAndPattern [])) when allow_conj -> (None, []) - | IntroAction (IntroOrAndPattern (IntroAndPattern ((_,IntroNaming (IntroIdentifier id)) :: _ as l) | IntroOrPattern [(_,IntroNaming (IntroIdentifier id)) :: _ as l ])) + | IntroAction (IntroOrAndPattern (IntroAndPattern ({CAst.v=IntroNaming (IntroIdentifier id)} :: _ as l) + | IntroOrPattern [{CAst.v=IntroNaming (IntroIdentifier id)} :: _ as l])) when allow_conj -> (Some id,l) | IntroAction (IntroOrAndPattern (IntroAndPattern _)) -> if issimple then diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 789cc35ee..958a205a1 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -185,8 +185,8 @@ let check_or_and_pattern_size ?loc check_and names branchsigns = match names with | IntroAndPattern l -> if not (Int.equal n 1) then errn n; - let l' = List.filter (function _,IntroForthcoming _ -> true | _,IntroNaming _ | _,IntroAction _ -> false) l in - if l' != [] then errforthcoming ?loc:(fst (List.hd l')); + let l' = List.filter CAst.(function {v=IntroForthcoming _} -> true | {v=IntroNaming _} | {v=IntroAction _} -> false) l in + if l' != [] then errforthcoming ?loc:(List.hd l').CAst.loc; if check_and then let p1 = List.count (fun x -> x) branchsigns.(0) in let p2 = List.length branchsigns.(0) in @@ -194,7 +194,7 @@ let check_or_and_pattern_size ?loc check_and names branchsigns = if not (Int.equal p p1 || Int.equal p p2) then err1 p1 p2; if Int.equal p p1 then IntroAndPattern - (List.extend branchsigns.(0) (Loc.tag @@ IntroNaming IntroAnonymous) l) + (List.extend branchsigns.(0) (CAst.make @@ IntroNaming IntroAnonymous) l) else names else @@ -218,7 +218,7 @@ let get_and_check_or_and_pattern ?loc = get_and_check_or_and_pattern_gen ?loc tr let compute_induction_names_gen check_and branchletsigns = function | None -> Array.make (Array.length branchletsigns) [] - | Some (loc,names) -> + | Some {CAst.loc;v=names} -> let names = fix_empty_or_and_pattern (Array.length branchletsigns) names in get_and_check_or_and_pattern_gen check_and ?loc names branchletsigns diff --git a/tactics/tactics.ml b/tactics/tactics.ml index b111fd1ef..df3cca144 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -373,11 +373,11 @@ let default_id env sigma decl = type name_flag = | NamingAvoid of Id.Set.t | NamingBasedOn of Id.t * Id.Set.t - | NamingMustBe of Id.t Loc.located + | NamingMustBe of lident let naming_of_name = function | Anonymous -> NamingAvoid Id.Set.empty - | Name id -> NamingMustBe (Loc.tag id) + | Name id -> NamingMustBe (CAst.make id) let find_name mayrepl decl naming gl = match naming with | NamingAvoid idl -> @@ -386,7 +386,7 @@ let find_name mayrepl decl naming gl = match naming with let sigma = Tacmach.New.project gl in new_fresh_id idl (default_id env sigma decl) gl | NamingBasedOn (id,idl) -> new_fresh_id idl id gl - | NamingMustBe (loc,id) -> + | NamingMustBe {CAst.loc;v=id} -> (* When name is given, we allow to hide a global name *) let ids_of_hyps = Tacmach.New.pf_ids_set_of_hyps gl in if not mayrepl && Id.Set.mem id ids_of_hyps then @@ -480,7 +480,7 @@ let assert_before_gen b naming t = assert_before_then_gen b naming t (fun _ -> Proofview.tclUNIT ()) let assert_before na = assert_before_gen false (naming_of_name na) -let assert_before_replacing id = assert_before_gen true (NamingMustBe (Loc.tag id)) +let assert_before_replacing id = assert_before_gen true (NamingMustBe (CAst.make id)) let assert_after_then_gen b naming t tac = let open Context.Rel.Declaration in @@ -495,7 +495,7 @@ let assert_after_gen b naming t = assert_after_then_gen b naming t (fun _ -> (Proofview.tclUNIT ())) let assert_after na = assert_after_gen false (naming_of_name na) -let assert_after_replacing id = assert_after_gen true (NamingMustBe (Loc.tag id)) +let assert_after_replacing id = assert_after_gen true (NamingMustBe (CAst.make id)) (**************************************************************) (* Fixpoints and CoFixpoints *) @@ -984,7 +984,7 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac = end let intro_gen n m f d = intro_then_gen n m f d (fun _ -> Proofview.tclUNIT ()) -let intro_mustbe_force id = intro_gen (NamingMustBe (Loc.tag id)) MoveLast true false +let intro_mustbe_force id = intro_gen (NamingMustBe (CAst.make id)) MoveLast true false let intro_using id = intro_gen (NamingBasedOn (id, Id.Set.empty)) MoveLast false false let intro_then = intro_then_gen (NamingAvoid Id.Set.empty) MoveLast false false @@ -994,7 +994,7 @@ let intro_avoiding l = intro_gen (NamingAvoid l) MoveLast false false let intro_move_avoid idopt avoid hto = match idopt with | None -> intro_gen (NamingAvoid avoid) hto true false - | Some id -> intro_gen (NamingMustBe (Loc.tag id)) hto true false + | Some id -> intro_gen (NamingMustBe (CAst.make id)) hto true false let intro_move idopt hto = intro_move_avoid idopt Id.Set.empty hto @@ -1140,7 +1140,7 @@ let try_intros_until tac = function let rec intros_move = function | [] -> Proofview.tclUNIT () | (hyp,destopt) :: rest -> - Tacticals.New.tclTHEN (intro_gen (NamingMustBe (Loc.tag hyp)) destopt false false) + Tacticals.New.tclTHEN (intro_gen (NamingMustBe (CAst.make hyp)) destopt false false) (intros_move rest) (* Apply a tactic on a quantified hypothesis, an hypothesis in context @@ -1264,7 +1264,7 @@ let check_unresolved_evars_of_metas sigma clenv = (meta_list clenv.evd) let do_replace id = function - | NamingMustBe (_,id') when Option.equal Id.equal id (Some id') -> true + | NamingMustBe {CAst.v=id'} when Option.equal Id.equal id (Some id') -> true | _ -> false (* For a clenv expressing some lemma [C[?1:T1,...,?n:Tn] : P] and some @@ -1288,7 +1288,7 @@ let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) error_uninstantiated_metas new_hyp_typ clenv; let new_hyp_prf = clenv_value clenv in let exact_tac = Proofview.V82.tactic (Tacmach.refine_no_check new_hyp_prf) in - let naming = NamingMustBe (Loc.tag targetid) in + let naming = NamingMustBe (CAst.make targetid) in let with_clear = do_replace (Some id) naming in Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS (clear_metas clenv.evd)) @@ -1633,7 +1633,8 @@ let tclORELSEOPT t k = Proofview.tclZERO ~info e | Some tac -> tac) -let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind : EConstr.constr with_bindings)) = +let general_apply with_delta with_destruct with_evars clear_flag + {CAst.loc;v=(c,lbind : EConstr.constr with_bindings)} = Proofview.Goal.enter begin fun gl -> let concl = Proofview.Goal.concl gl in let sigma = Tacmach.New.project gl in @@ -1714,13 +1715,13 @@ let rec apply_with_bindings_gen b e = function (apply_with_bindings_gen b e cbl) let apply_with_delayed_bindings_gen b e l = - let one k (loc, f) = + let one k {CAst.loc;v=f} = Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in let (sigma, cb) = f env sigma in Tacticals.New.tclWITHHOLES e - (general_apply b b e k (loc,cb)) sigma + (general_apply b b e k CAst.(make ?loc cb)) sigma end in let rec aux = function @@ -1731,13 +1732,13 @@ let apply_with_delayed_bindings_gen b e l = (one k f) (aux cbl) in aux l -let apply_with_bindings cb = apply_with_bindings_gen false false [None,(Loc.tag cb)] +let apply_with_bindings cb = apply_with_bindings_gen false false [None,(CAst.make cb)] -let eapply_with_bindings cb = apply_with_bindings_gen false true [None,(Loc.tag cb)] +let eapply_with_bindings cb = apply_with_bindings_gen false true [None,(CAst.make cb)] -let apply c = apply_with_bindings_gen false false [None,(Loc.tag (c,NoBindings))] +let apply c = apply_with_bindings_gen false false [None,(CAst.make (c,NoBindings))] -let eapply c = apply_with_bindings_gen false true [None,(Loc.tag (c,NoBindings))] +let eapply c = apply_with_bindings_gen false true [None,(CAst.make (c,NoBindings))] let apply_list = function | c::l -> apply_with_bindings (c,ImplicitBindings l) @@ -1796,7 +1797,7 @@ let apply_in_once_main flags innerclause env sigma (loc,d,lbind) = aux (make_clenv_binding env sigma (d,thm) lbind) let apply_in_once sidecond_first with_delta with_destruct with_evars naming - id (clear_flag,(loc,(d,lbind))) tac = + id (clear_flag,{ CAst.loc; v= d,lbind}) tac = let open Context.Rel.Declaration in Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in @@ -1830,14 +1831,14 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming end let apply_in_delayed_once sidecond_first with_delta with_destruct with_evars naming - id (clear_flag,(loc,f)) tac = + id (clear_flag,{CAst.loc;v=f}) tac = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let (sigma, c) = f env sigma in Tacticals.New.tclWITHHOLES with_evars (apply_in_once sidecond_first with_delta with_destruct with_evars - naming id (clear_flag,(loc,c)) tac) + naming id (clear_flag,CAst.(make ?loc c)) tac) sigma end @@ -2032,7 +2033,7 @@ let clear_body ids = end let clear_wildcards ids = - Tacticals.New.tclMAP (fun (loc, id) -> clear [id]) ids + Tacticals.New.tclMAP (fun {CAst.loc;v=id} -> clear [id]) ids (* Takes a list of booleans, and introduces all the variables * quantified in the goal which are associated with a value @@ -2132,7 +2133,7 @@ let constructor_core with_evars cstr lbind = let env = Proofview.Goal.env gl in let (sigma, (cons, u)) = Evd.fresh_constructor_instance env sigma cstr in let cons = mkConstructU (cons, EInstance.make u) in - let apply_tac = general_apply true false with_evars None (Loc.tag (cons,lbind)) in + let apply_tac = general_apply true false with_evars None (CAst.make (cons,lbind)) in Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) apply_tac end @@ -2234,7 +2235,7 @@ let intro_decomp_eq ?loc l thin tac id = match my_find_eq_data_decompose gl t with | Some (eq,u,eq_args) -> !intro_decomp_eq_function - (fun n -> tac ((Loc.tag id)::thin) (Some (true,n)) l) + (fun n -> tac ((CAst.make id)::thin) (Some (true,n)) l) (eq,t,eq_args) (c, t) | None -> Tacticals.New.tclZEROMSG (str "Not a primitive equality here.") @@ -2262,7 +2263,7 @@ let rewrite_hyp_then assert_style with_evars thin l2r id tac = Hook.get forward_subst_one true x (id,rhs,l2r) in let clear_var_and_eq id' = clear [id';id] in let early_clear id' thin = - List.filter (fun (_,id) -> not (Id.equal id id')) thin in + List.filter (fun {CAst.v=id} -> not (Id.equal id id')) thin in Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in @@ -2298,29 +2299,29 @@ let rewrite_hyp_then assert_style with_evars thin l2r id tac = end let prepare_naming ?loc = function - | IntroIdentifier id -> NamingMustBe (Loc.tag ?loc id) + | IntroIdentifier id -> NamingMustBe (CAst.make ?loc id) | IntroAnonymous -> NamingAvoid Id.Set.empty | IntroFresh id -> NamingBasedOn (id, Id.Set.empty) -let rec explicit_intro_names = function -| (_, IntroForthcoming _) :: l -> explicit_intro_names l -| (_, IntroNaming (IntroIdentifier id)) :: l -> Id.Set.add id (explicit_intro_names l) -| (_, IntroAction (IntroOrAndPattern l)) :: l' -> +let rec explicit_intro_names = let open CAst in function +| {v=IntroForthcoming _} :: l -> explicit_intro_names l +| {v=IntroNaming (IntroIdentifier id)} :: l -> Id.Set.add id (explicit_intro_names l) +| {v=IntroAction (IntroOrAndPattern l)} :: l' -> let ll = match l with IntroAndPattern l -> [l] | IntroOrPattern ll -> ll in let fold accu l = Id.Set.union accu (explicit_intro_names (l@l')) in List.fold_left fold Id.Set.empty ll -| (_, IntroAction (IntroInjection l)) :: l' -> +| {v=IntroAction (IntroInjection l)} :: l' -> explicit_intro_names (l@l') -| (_, IntroAction (IntroApplyOn (c,pat))) :: l' -> +| {v=IntroAction (IntroApplyOn (c,pat))} :: l' -> explicit_intro_names (pat::l') -| (_, (IntroNaming (IntroAnonymous | IntroFresh _) - | IntroAction (IntroWildcard | IntroRewrite _))) :: l -> +| {v=(IntroNaming (IntroAnonymous | IntroFresh _) + | IntroAction (IntroWildcard | IntroRewrite _))} :: l -> explicit_intro_names l | [] -> Id.Set.empty -let rec check_name_unicity env ok seen = function -| (_, IntroForthcoming _) :: l -> check_name_unicity env ok seen l -| (loc, IntroNaming (IntroIdentifier id)) :: l -> +let rec check_name_unicity env ok seen = let open CAst in function +| {v=IntroForthcoming _} :: l -> check_name_unicity env ok seen l +| {loc;v=IntroNaming (IntroIdentifier id)} :: l -> (try ignore (if List.mem_f Id.equal id ok then raise Not_found else lookup_named id env); user_err ?loc (Id.print id ++ str" is already used.") @@ -2329,15 +2330,15 @@ let rec check_name_unicity env ok seen = function user_err ?loc (Id.print id ++ str" is used twice.") else check_name_unicity env ok (id::seen) l) -| (_, IntroAction (IntroOrAndPattern l)) :: l' -> +| {v=IntroAction (IntroOrAndPattern l)} :: l' -> let ll = match l with IntroAndPattern l -> [l] | IntroOrPattern ll -> ll in List.iter (fun l -> check_name_unicity env ok seen (l@l')) ll -| (_, IntroAction (IntroInjection l)) :: l' -> +| {v=IntroAction (IntroInjection l)} :: l' -> check_name_unicity env ok seen (l@l') -| (_, IntroAction (IntroApplyOn (c,pat))) :: l' -> +| {v=IntroAction (IntroApplyOn (c,pat))} :: l' -> check_name_unicity env ok seen (pat::l') -| (_, (IntroNaming (IntroAnonymous | IntroFresh _) - | IntroAction (IntroWildcard | IntroRewrite _))) :: l -> +| {v=(IntroNaming (IntroAnonymous | IntroFresh _) + | IntroAction (IntroWildcard | IntroRewrite _))} :: l -> check_name_unicity env ok seen l | [] -> () @@ -2345,13 +2346,13 @@ let wild_id = Id.of_string "_tmp" let rec list_mem_assoc_right id = function | [] -> false - | (x,id')::l -> Id.equal id id' || list_mem_assoc_right id l + | {CAst.v=id'}::l -> Id.equal id id' || list_mem_assoc_right id l let check_thin_clash_then id thin avoid tac = if list_mem_assoc_right id thin then let newid = next_ident_away (add_suffix id "'") avoid in let thin = - List.map (on_snd (fun id' -> if Id.equal id id' then newid else id')) thin in + List.map CAst.(map (fun id' -> if Id.equal id id' then newid else id')) thin in Tacticals.New.tclTHEN (rename_hyp [id,newid]) (tac thin) else tac thin @@ -2364,7 +2365,7 @@ let make_tmp_naming avoid l = function case of IntroFresh, we should use check_thin_clash_then anyway to prevent the case of an IntroFresh precisely using the wild_id *) | IntroWildcard -> NamingBasedOn (wild_id, Id.Set.union avoid (explicit_intro_names l)) - | pat -> NamingAvoid(Id.Set.union avoid (explicit_intro_names ((Loc.tag @@ IntroAction pat)::l))) + | pat -> NamingAvoid(Id.Set.union avoid (explicit_intro_names ((CAst.make @@ IntroAction pat)::l))) let fit_bound n = function | None -> true @@ -2400,8 +2401,8 @@ let rec intro_patterns_core with_evars b avoid ids thin destopt bound n tac = | [] -> (* Behave as IntroAnonymous *) intro_patterns_core with_evars b avoid ids thin destopt bound n tac - [Loc.tag @@ IntroNaming IntroAnonymous] - | (loc,pat) :: l -> + [CAst.make @@ IntroNaming IntroAnonymous] + | {CAst.loc;v=pat} :: l -> if exceed_bound n bound then error_unexpected_extra_pattern loc bound pat else match pat with | IntroForthcoming onlydeps -> @@ -2425,7 +2426,7 @@ and intro_pattern_naming loc with_evars b avoid ids pat thin destopt bound n tac match pat with | IntroIdentifier id -> check_thin_clash_then id thin avoid (fun thin -> - intro_then_gen (NamingMustBe (loc,id)) destopt true false + intro_then_gen (NamingMustBe CAst.(make ?loc id)) destopt true false (fun id -> intro_patterns_core with_evars b avoid (id::ids) thin destopt bound n tac l)) | IntroAnonymous -> intro_then_gen (NamingAvoid (Id.Set.union avoid (explicit_intro_names l))) @@ -2440,24 +2441,24 @@ and intro_pattern_naming loc with_evars b avoid ids pat thin destopt bound n tac and intro_pattern_action ?loc with_evars b style pat thin destopt tac id = match pat with | IntroWildcard -> - tac ((Loc.tag ?loc id)::thin) None [] + tac (CAst.(make ?loc id)::thin) None [] | IntroOrAndPattern ll -> intro_or_and_pattern ?loc with_evars b ll thin tac id | IntroInjection l' -> intro_decomp_eq ?loc l' thin tac id | IntroRewrite l2r -> rewrite_hyp_then style with_evars thin l2r id (fun thin -> tac thin None []) - | IntroApplyOn ((loc',f),(loc,pat)) -> + | IntroApplyOn ({CAst.loc=loc';v=f},{CAst.loc;v=pat}) -> let naming,tac_ipat = prepare_intros ?loc with_evars (IntroIdentifier id) destopt pat in let doclear = - if naming = NamingMustBe (Loc.tag ?loc id) then + if naming = NamingMustBe (CAst.make ?loc id) then Proofview.tclUNIT () (* apply_in_once do a replacement *) else clear [id] in let f env sigma = let (sigma, c) = f env sigma in (sigma,(c, NoBindings)) in - apply_in_delayed_once false true true with_evars naming id (None,(loc',f)) + apply_in_delayed_once false true true with_evars naming id (None,CAst.make ?loc:loc' f) (fun id -> Tacticals.New.tclTHENLIST [doclear; tac_ipat id; tac thin None []]) and prepare_intros ?loc with_evars dft destopt = function @@ -2491,7 +2492,7 @@ let intro_patterns_to with_evars destopt = destopt None let intro_pattern_to with_evars destopt pat = - intro_patterns_to with_evars destopt [Loc.tag pat] + intro_patterns_to with_evars destopt [CAst.make pat] let intro_patterns with_evars = intro_patterns_to with_evars MoveLast @@ -2506,11 +2507,11 @@ let intros_patterns with_evars = function let prepare_intros_opt with_evars dft destopt = function | None -> prepare_naming dft, (fun _id -> Proofview.tclUNIT ()) - | Some (loc,ipat) -> prepare_intros ?loc with_evars dft destopt ipat + | Some {CAst.loc;v=ipat} -> prepare_intros ?loc with_evars dft destopt ipat let ipat_of_name = function | Anonymous -> None - | Name id -> Some (Loc.tag @@ IntroNaming (IntroIdentifier id)) + | Name id -> Some (CAst.make @@ IntroNaming (IntroIdentifier id)) let head_ident sigma c = let c = fst (decompose_app sigma (snd (decompose_lam_assum sigma c))) in @@ -2541,7 +2542,7 @@ let general_apply_in sidecond_first with_delta with_destruct with_evars prepare_intros_opt with_evars (IntroIdentifier id) destopt ipat in let lemmas_target, last_lemma_target = let last,first = List.sep_last lemmas in - List.map (fun lem -> (NamingMustBe (Loc.tag id),lem)) first, (naming,last) + List.map (fun lem -> (NamingMustBe (CAst.make id),lem)) first, (naming,last) in (* We chain apply_in_once, ending with an intro pattern *) List.fold_right tac lemmas_target (tac last_lemma_target ipat_tac) id @@ -2556,7 +2557,7 @@ let general_apply_in sidecond_first with_delta with_destruct with_evars *) let apply_in simple with_evars id lemmas ipat = - let lemmas = List.map (fun (k,(loc,l)) -> k, (loc, (fun _ sigma -> (sigma,l)))) lemmas in + let lemmas = List.map (fun (k,{CAst.loc;v=l}) -> k, CAst.make ?loc (fun _ sigma -> (sigma,l))) lemmas in general_apply_in false simple simple with_evars id lemmas ipat let apply_delayed_in simple with_evars id lemmas ipat = @@ -2590,7 +2591,7 @@ let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty = Evarsolve.refresh_universes ~onlyalg:true (Some false) env sigma t in let (sigma, (newcl, eq_tac)) = match with_eq with - | Some (lr,(loc,ido)) -> + | Some (lr,{CAst.loc;v=ido}) -> let heq = match ido with | IntroAnonymous -> new_fresh_id (Id.Set.singleton id) (add_prefix "Heq" id) gl | IntroFresh heq_base -> new_fresh_id (Id.Set.singleton id) heq_base gl @@ -2608,7 +2609,7 @@ let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty = let ans = term, Tacticals.New.tclTHENLIST [ - intro_gen (NamingMustBe (loc,heq)) (decode_hyp lastlhyp) true false; + intro_gen (NamingMustBe CAst.(make ?loc heq)) (decode_hyp lastlhyp) true false; clear_body [heq;id]] in (sigma, ans) @@ -2618,7 +2619,7 @@ let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty = Tacticals.New.tclTHENLIST [ Proofview.Unsafe.tclEVARS sigma; convert_concl_no_check newcl DEFAULTcast; - intro_gen (NamingMustBe (Loc.tag id)) (decode_hyp lastlhyp) true false; + intro_gen (NamingMustBe (CAst.make id)) (decode_hyp lastlhyp) true false; Tacticals.New.tclMAP convert_hyp_no_check depdecls; eq_tac ] end @@ -2643,7 +2644,7 @@ let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty = else LocalAssum (id,t) in match with_eq with - | Some (lr,(loc,ido)) -> + | Some (lr,{CAst.loc;v=ido}) -> let heq = match ido with | IntroAnonymous -> fresh_id_in_env (Id.Set.singleton id) (add_prefix "Heq" id) env | IntroFresh heq_base -> fresh_id_in_env (Id.Set.singleton id) heq_base env @@ -2957,7 +2958,7 @@ let specialize (c,lbind) ipat = (* TODO: add intro to be more homogeneous. It will break scripts but will be easy to fix *) (Tacticals.New.tclTHENLAST (cut typ) (exact_no_check term)) - | Some (loc,ipat) -> + | Some {CAst.loc;v=ipat} -> (* Like pose proof with extra support for "with" bindings *) (* even though the "with" bindings forces full application *) let naming,tac = prepare_intros ?loc false IntroAnonymous MoveLast ipat in @@ -3047,19 +3048,19 @@ let intropattern_of_name gl avoid = function | Anonymous -> IntroNaming IntroAnonymous | Name id -> IntroNaming (IntroIdentifier (new_fresh_id avoid id gl)) -let rec consume_pattern avoid na isdep gl = function - | [] -> ((Loc.tag @@ intropattern_of_name gl avoid na), []) - | (loc,IntroForthcoming true)::names when not isdep -> +let rec consume_pattern avoid na isdep gl = let open CAst in function + | [] -> ((CAst.make @@ intropattern_of_name gl avoid na), []) + | {loc;v=IntroForthcoming true}::names when not isdep -> consume_pattern avoid na isdep gl names - | (loc,IntroForthcoming _)::names as fullpat -> + | {loc;v=IntroForthcoming _}::names as fullpat -> let avoid = Id.Set.union avoid (explicit_intro_names names) in - ((loc,intropattern_of_name gl avoid na), fullpat) - | (loc,IntroNaming IntroAnonymous)::names -> + (CAst.make ?loc @@ intropattern_of_name gl avoid na, fullpat) + | {loc;v=IntroNaming IntroAnonymous}::names -> let avoid = Id.Set.union avoid (explicit_intro_names names) in - ((loc,intropattern_of_name gl avoid na), names) - | (loc,IntroNaming (IntroFresh id'))::names -> + (CAst.make ?loc @@ intropattern_of_name gl avoid na, names) + | {loc;v=IntroNaming (IntroFresh id')}::names -> let avoid = Id.Set.union avoid (explicit_intro_names names) in - ((loc,IntroNaming (IntroIdentifier (new_fresh_id avoid id' gl))), names) + (CAst.make ?loc @@ IntroNaming (IntroIdentifier (new_fresh_id avoid id' gl)), names) | pat::names -> (pat,names) let re_intro_dependent_hypotheses (lstatus,rstatus) (_,tophyp) = @@ -3123,9 +3124,9 @@ let induct_discharge with_evars dests avoid' tac (avoid,ra) names = (IndArg,_,depind,hyprecname) :: ra' -> Proofview.Goal.enter begin fun gl -> let (recpat,names) = match names with - | [loc,IntroNaming (IntroIdentifier id) as pat] -> + | [{CAst.loc;v=IntroNaming (IntroIdentifier id)} as pat] -> let id' = next_ident_away (add_prefix "IH" id) avoid in - (pat, [Loc.tag @@ IntroNaming (IntroIdentifier id')]) + (pat, [CAst.make @@ IntroNaming (IntroIdentifier id')]) | _ -> consume_pattern avoid (Name recvarname) deprec gl names in let dest = get_recarg_dest dests in dest_intro_patterns with_evars avoid thin dest [recpat] (fun ids thin -> @@ -4468,7 +4469,7 @@ let induction_gen_l isrec with_evars elim names lc = let newlc = ref [] in let lc = List.map (function | (c,None) -> c - | (c,Some(loc,eqname)) -> + | (c,Some{CAst.loc;v=eqname}) -> user_err ?loc (str "Do not know what to do with " ++ Miscprint.pr_intro_pattern_naming eqname)) lc in let rec atomize_list l = @@ -5022,14 +5023,14 @@ module Simple = struct let intro x = intro_move (Some x) MoveLast let apply c = - apply_with_bindings_gen false false [None,(Loc.tag (c,NoBindings))] + apply_with_bindings_gen false false [None,(CAst.make (c,NoBindings))] let eapply c = - apply_with_bindings_gen false true [None,(Loc.tag (c,NoBindings))] + apply_with_bindings_gen false true [None,(CAst.make (c,NoBindings))] let elim c = elim false None (c,NoBindings) None let case c = general_case_analysis false None (c,NoBindings) let apply_in id c = - apply_in false false id [None,(Loc.tag (c, NoBindings))] None + apply_in false false id [None,(CAst.make (c, NoBindings))] None end diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 1c3b75e91..079baa3ef 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -8,7 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Loc open Names open Constr open EConstr @@ -196,10 +195,10 @@ val apply : constr -> unit Proofview.tactic val eapply : constr -> unit Proofview.tactic val apply_with_bindings_gen : - advanced_flag -> evars_flag -> (clear_flag * constr with_bindings located) list -> unit Proofview.tactic + advanced_flag -> evars_flag -> (clear_flag * constr with_bindings CAst.t) list -> unit Proofview.tactic val apply_with_delayed_bindings_gen : - advanced_flag -> evars_flag -> (clear_flag * delayed_open_constr_with_bindings located) list -> unit Proofview.tactic + advanced_flag -> evars_flag -> (clear_flag * delayed_open_constr_with_bindings CAst.t) list -> unit Proofview.tactic val apply_with_bindings : constr with_bindings -> unit Proofview.tactic val eapply_with_bindings : constr with_bindings -> unit Proofview.tactic @@ -208,12 +207,12 @@ val cut_and_apply : constr -> unit Proofview.tactic val apply_in : advanced_flag -> evars_flag -> Id.t -> - (clear_flag * constr with_bindings located) list -> + (clear_flag * constr with_bindings CAst.t) list -> intro_pattern option -> unit Proofview.tactic val apply_delayed_in : advanced_flag -> evars_flag -> Id.t -> - (clear_flag * delayed_open_constr_with_bindings located) list -> + (clear_flag * delayed_open_constr_with_bindings CAst.t) list -> intro_pattern option -> unit Proofview.tactic (** {6 Elimination tactics. } *) diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 56bdcc7e5..fdd0d4ed3 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -20,15 +20,14 @@ open Vernacprop Use the module Coqtoplevel, which catches these exceptions (the exceptions are explained only at the toplevel). *) -let checknav_simple (loc, cmd) = +let checknav_simple {CAst.loc;v=cmd} = if is_navigation_vernac cmd && not (is_reset cmd) then CErrors.user_err ?loc (str "Navigation commands forbidden in files.") -let checknav_deep (loc, ast) = +let checknav_deep {CAst.loc;v=ast} = if is_deep_navigation_vernac ast then CErrors.user_err ?loc (str "Navigation commands forbidden in nested commands.") - let disable_drop = function | Drop -> CErrors.user_err Pp.(str "Drop is forbidden.") | e -> e @@ -45,7 +44,7 @@ let vernac_echo ?loc in_chan = let open Loc in (* For coqtop -time, we display the position in the file, and a glimpse of the executed command *) -let pp_cmd_header ?loc com = +let pp_cmd_header {CAst.loc;v=com} = let shorten s = if Unicode.utf8_length s > 33 then (Unicode.utf8_sub s 0 30) ^ "..." else s in @@ -66,8 +65,8 @@ let pp_cmd_header ?loc com = (* This is a special case where we assume we are in console batch mode and take control of the console. *) -let print_cmd_header ?loc com = - Pp.pp_with !Topfmt.std_ft (pp_cmd_header ?loc com); +let print_cmd_header com = + Pp.pp_with !Topfmt.std_ft (pp_cmd_header com); Format.pp_print_flush !Topfmt.std_ft () (* Reenable when we get back to feedback printing *) @@ -85,14 +84,14 @@ module State = struct end -let interp_vernac ~time ~check ~interactive ~state (loc,com) = +let interp_vernac ~time ~check ~interactive ~state ({CAst.loc;_} as com) = let open State in try (* The -time option is only supported from console-based clients due to the way it prints. *) - if time then print_cmd_header ?loc com; - let com = if time then VernacTime(time,(CAst.make ?loc com)) else com in - let doc, nsid, ntip = Stm.add ~doc:state.doc ~ontop:state.sid (not !Flags.quiet) (loc,com) in + if time then print_cmd_header com; + let com = if time then CAst.make ?loc @@ VernacTime(time,com) else com in + let doc, nsid, ntip = Stm.add ~doc:state.doc ~ontop:state.sid (not !Flags.quiet) com in (* Main STM interaction *) if ntip <> `NewTip then @@ -131,7 +130,7 @@ let load_vernac_core ~time ~echo ~check ~interactive ~state file = (* we go out of the following infinite loop when a End_of_input is * raised, which means that we raised the end of the file being loaded *) while true do - let loc, ast = + let { CAst.loc; _ } as ast = Stm.parse_sentence ~doc:!rstate.doc !rstate.sid in_pa (* If an error in parsing occurs, we propagate the exception so the caller of load_vernac will take care of it. However, @@ -154,8 +153,8 @@ let load_vernac_core ~time ~echo ~check ~interactive ~state file = (* Printing of vernacs *) Option.iter (vernac_echo ?loc) in_echo; - checknav_simple (loc, ast); - let state = Flags.silently (interp_vernac ~time ~check ~interactive ~state:!rstate) (loc, ast) in + checknav_simple ast; + let state = Flags.silently (interp_vernac ~time ~check ~interactive ~state:!rstate) ast in rids := state.sid :: !rids; rstate := state; done; diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli index 19bac45c3..51758642e 100644 --- a/toplevel/vernac.mli +++ b/toplevel/vernac.mli @@ -23,7 +23,7 @@ end expected to handle and print errors in form of exceptions, however care is taken so the state machine is left in a consistent state. *) -val process_expr : time:bool -> state:State.t -> Vernacexpr.vernac_control Loc.located -> State.t +val process_expr : time:bool -> state:State.t -> Vernacexpr.vernac_control CAst.t -> State.t (** [load_vernac echo sid file] Loads [file] on top of [sid], will echo the commands if [echo] is set. Callers are expected to handle diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 2879feba7..1a6b4dcdb 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -86,12 +86,12 @@ let destruct_on c = destruct false None c None None let destruct_on_using c id = destruct false None c - (Some (Loc.tag @@ IntroOrPattern [[Loc.tag @@ IntroNaming IntroAnonymous]; - [Loc.tag @@ IntroNaming (IntroIdentifier id)]])) + (Some (CAst.make @@ IntroOrPattern [[CAst.make @@ IntroNaming IntroAnonymous]; + [CAst.make @@ IntroNaming (IntroIdentifier id)]])) None let destruct_on_as c l = - destruct false None c (Some (Loc.tag l)) None + destruct false None c (Some (CAst.make l)) None let inj_flags = Some { Equality.keep_proof_equalities = true; (* necessary *) @@ -620,8 +620,8 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). Proofview.Goal.enter begin fun gl -> let fresht = fresh_id (Id.of_string "Z") gl in destruct_on_as (EConstr.mkVar freshz) - (IntroOrPattern [[Loc.tag @@ IntroNaming (IntroIdentifier fresht); - Loc.tag @@ IntroNaming (IntroIdentifier freshz)]]) + (IntroOrPattern [[CAst.make @@ IntroNaming (IntroIdentifier fresht); + CAst.make @@ IntroNaming (IntroIdentifier freshz)]]) end ]); (* diff --git a/vernac/classes.ml b/vernac/classes.ml index 192cc8a55..e074e44a4 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -229,8 +229,8 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) | Some (Inl props) -> let get_id = function - | Ident id' -> id' - | Qualid (loc,id') -> (Loc.tag ?loc @@ snd (repr_qualid id')) + | Ident (loc, id') -> CAst.(make ?loc @@ id') + | Qualid (loc,id') -> CAst.(make ?loc @@ snd (repr_qualid id')) in let props, rest = List.fold_left @@ -238,7 +238,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) if is_local_assum decl then try let is_id (id', _) = match RelDecl.get_name decl, get_id id' with - | Name id, (_, id') -> Id.equal id id' + | Name id, {CAst.v=id'} -> Id.equal id id' | Anonymous, _ -> false in let (loc_mid, c) = @@ -247,7 +247,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) let rest' = List.filter (fun v -> not (is_id v)) rest in - let (loc, mid) = get_id loc_mid in + let {CAst.loc;v=mid} = get_id loc_mid in List.iter (fun (n, _, x) -> if Name.equal n (Name mid) then Option.iter (fun x -> Dumpglob.add_glob ?loc (ConstRef x)) x) diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 131b1fab6..249e7893c 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -1015,8 +1015,8 @@ let explain_not_a_class env c = let c = EConstr.to_constr Evd.empty c in pr_constr_env env Evd.empty c ++ str" is not a declared type class." -let explain_unbound_method env cid id = - str "Unbound method name " ++ Id.print (snd id) ++ spc () ++ +let explain_unbound_method env cid { CAst.v = id } = + str "Unbound method name " ++ Id.print (id) ++ spc () ++ str"of class" ++ spc () ++ pr_global cid ++ str "." let pr_constr_exprs exprs = diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 7764920d9..b3eb13fb7 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -907,7 +907,7 @@ let vernac_set_used_variables e = (str "Unknown variable: " ++ Id.print id)) l; let _, to_clear = Proof_global.set_used_variables l in - let to_clear = List.map snd to_clear in + let to_clear = List.map (fun x -> x.CAst.v) to_clear in Proof_global.with_current_proof begin fun _ p -> if List.is_empty to_clear then (p, ()) else @@ -1860,8 +1860,8 @@ let vernac_search ~atts s gopt r = let vernac_locate = function | LocateAny (AN qid) -> print_located_qualid qid | LocateTerm (AN qid) -> print_located_term qid - | LocateAny (ByNotation (_, (ntn, sc))) (** TODO : handle Ltac notations *) - | LocateTerm (ByNotation (_, (ntn, sc))) -> + | LocateAny (ByNotation { CAst.v=(ntn, sc)}) (** TODO : handle Ltac notations *) + | LocateTerm (ByNotation { CAst.v=(ntn, sc)}) -> let _, env = Pfedit.get_current_context () in Notation.locate_notation (Constrextern.without_symbols (pr_lglob_constr_env env)) ntn sc @@ -2259,7 +2259,7 @@ let with_fail st b f = | _ -> assert false end -let interp ?(verbosely=true) ?proof ~st (loc,c) = +let interp ?(verbosely=true) ?proof ~st {CAst.loc;v=c} = let orig_univ_poly = Flags.is_universe_polymorphism () in let orig_program_mode = Flags.is_program_mode () in let flags f atts = diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index 13ecaf37b..f6199e820 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -20,7 +20,7 @@ val vernac_require : val interp : ?verbosely:bool -> ?proof:Proof_global.closed_proof -> - st:Vernacstate.t -> Vernacexpr.vernac_control Loc.located -> Vernacstate.t + st:Vernacstate.t -> Vernacexpr.vernac_control CAst.t -> Vernacstate.t (** Prepare a "match" template for a given inductive type. For each branch of the match, we list the constructor name |