From 4af41a12a0e7e6b17d25a71568641bd03d5e1f94 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 14 Feb 2018 06:57:40 +0100 Subject: [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. --- interp/constrextern.ml | 10 +++++----- interp/constrintern.ml | 20 ++++++++++---------- interp/modintern.ml | 16 ++++++++-------- interp/notation_ops.ml | 22 +++++++++++----------- interp/smartlocate.ml | 6 +++--- interp/stdarg.ml | 2 +- interp/stdarg.mli | 4 ++-- interp/tactypes.ml | 9 ++++----- 8 files changed, 44 insertions(+), 45 deletions(-) (limited to 'interp') 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 -- cgit v1.2.3