diff options
31 files changed, 423 insertions, 360 deletions
diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml index 071861e271..ddb62313ff 100644 --- a/ide/texmacspp.ml +++ b/ide/texmacspp.ml @@ -218,8 +218,8 @@ let rec pp_bindlist bl = (List.map (fun (loc, name) -> xmlCst ?loc (string_of_name name)) loc_names) in - match e with - | _, CHole _ -> names + match e.CAst.v with + | CHole _ -> names | _ -> names @ [pp_expr e]) bl) in match tlist with @@ -232,7 +232,7 @@ and pp_local_binder lb = (* don't know what it is for now *) | CLocalDef ((loc, nam), ce, ty) -> let attrs = ["name", string_of_name nam] in let value = match ty with - Some t -> Loc.tag ?loc:(Loc.merge_opt (constr_loc ce) (constr_loc t)) @@ CCast (ce, CastConv t) + Some t -> CAst.make ?loc:(Loc.merge_opt (constr_loc ce) (constr_loc t)) @@ CCast (ce, CastConv t) | None -> ce in pp_expr ~attr:attrs value | CLocalAssum (namll, _, ce) -> @@ -302,7 +302,7 @@ and pp_cofixpoint_expr (((loc, id), pl), lbl, ce, ceo) = (* cofixpoint_expr *) end and pp_lident (loc, id) = xmlCst ?loc (Id.to_string id) and pp_simple_binder (idl, ce) = List.map pp_lident idl @ [pp_expr ce] -and pp_cases_pattern_expr (loc, cpe) = +and pp_cases_pattern_expr {loc ; CAst.v = cpe} = match cpe with | CPatAlias (cpe, id) -> xmlApply ?loc @@ -390,7 +390,7 @@ and pp_local_binder_list lbl = and pp_const_expr_list cel = let l = List.map pp_expr cel in Element ("recurse", (backstep_loc l), l) -and pp_expr ?(attr=[]) (loc, e) = +and pp_expr ?(attr=[]) { loc; CAst.v = e } = match e with | CRef (r, _) -> xmlCst ?loc:(Libnames.loc_of_reference r) ~attr (Libnames.string_of_reference r) @@ -469,13 +469,13 @@ and pp_expr ?(attr=[]) (loc, e) = [pp_branch_expr_list bel])) | CRecord _ -> assert false | CLetIn ((varloc, var), value, typ, body) -> - let (loc, value) = match typ with + let value = match typ with | Some t -> - Loc.tag ?loc:(Loc.merge_opt (constr_loc value) (constr_loc t)) (CCast (value, CastConv t)) + CAst.make ?loc:(Loc.merge_opt (constr_loc value) (constr_loc t)) (CCast (value, CastConv t)) | None -> value in xmlApply ?loc (xmlOperator ?loc "let" :: - [xmlCst ?loc:varloc (string_of_name var) ; pp_expr (Loc.tag ?loc value); pp_expr body]) + [xmlCst ?loc:varloc (string_of_name var) ; pp_expr value; pp_expr body]) | CLambdaN (bl, e) -> xmlApply ?loc (xmlOperator ?loc "lambda" :: [pp_bindlist bl] @ [pp_expr e]) diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index ce349a63fd..b11972cd39 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -59,9 +59,9 @@ let explicitation_eq ex1 ex2 = match ex1, ex2 with let eq_located f (_, x) (_, y) = f x y -let rec cases_pattern_expr_eq (l1, p1) (l2, p2) = - if p1 == p2 then true - else match p1, p2 with +let rec cases_pattern_expr_eq p1 p2 = + if CAst.(p1.v == p2.v) then true + else match CAst.(p1.v, p2.v) with | CPatAlias(a1,i1), CPatAlias(a2,i2) -> Id.equal i1 i2 && cases_pattern_expr_eq a1 a2 | CPatCstr(c1,a1,b1), CPatCstr(c2,a2,b2) -> @@ -97,9 +97,9 @@ let eq_universes u1 u2 = | Some l, Some l' -> l = l' | _, _ -> false -let rec constr_expr_eq (_loc1, e1) (_loc2, e2) = - if e1 == e2 then true - else match e1, e2 with +let rec constr_expr_eq e1 e2 = + if CAst.(e1.v == e2.v) then true + else match CAst.(e1.v, e2.v) with | CRef (r1,u1), CRef (r2,u2) -> eq_reference r1 r2 && eq_universes u1 u2 | CFix(id1,fl1), CFix(id2,fl2) -> eq_located Id.equal id1 id2 && @@ -228,11 +228,11 @@ and constr_notation_substitution_eq (e1, el1, bl1) (e2, el2, bl2) = and instance_eq (x1,c1) (x2,c2) = Id.equal x1 x2 && constr_expr_eq c1 c2 -let constr_loc (l,_) = l +let constr_loc c = CAst.(c.loc) -let cases_pattern_expr_loc (l,_) = l +let cases_pattern_expr_loc cp = CAst.(cp.loc) -let raw_cases_pattern_expr_loc (l, _) = l +let raw_cases_pattern_expr_loc pe = CAst.(pe.loc) let local_binder_loc = function | CLocalAssum ((loc,_)::_,_,t) @@ -247,18 +247,18 @@ let local_binders_loc bll = match bll with (** Pseudo-constructors *) -let mkIdentC id = Loc.tag @@ CRef (Ident (Loc.tag id),None) -let mkRefC r = Loc.tag @@ CRef (r,None) -let mkCastC (a,k) = Loc.tag @@ CCast (a,k) -let mkLambdaC (idl,bk,a,b) = Loc.tag @@ CLambdaN ([idl,bk,a],b) -let mkLetInC (id,a,t,b) = Loc.tag @@ CLetIn (id,a,t,b) -let mkProdC (idl,bk,a,b) = Loc.tag @@ CProdN ([idl,bk,a],b) +let mkIdentC id = CAst.make @@ CRef (Ident (Loc.tag id),None) +let mkRefC r = CAst.make @@ CRef (r,None) +let mkCastC (a,k) = CAst.make @@ CCast (a,k) +let mkLambdaC (idl,bk,a,b) = CAst.make @@ CLambdaN ([idl,bk,a],b) +let mkLetInC (id,a,t,b) = CAst.make @@ CLetIn (id,a,t,b) +let mkProdC (idl,bk,a,b) = CAst.make @@ CProdN ([idl,bk,a],b) let mkAppC (f,l) = let l = List.map (fun x -> (x,None)) l in - match f with - | _loc, CApp (g,l') -> Loc.tag @@ CApp (g, l' @ l) - | _ -> Loc.tag @@ CApp ((None, f), l) + match CAst.(f.v) with + | CApp (g,l') -> CAst.make @@ CApp (g, l' @ l) + | _ -> CAst.make @@ CApp ((None, f), l) let add_name_in_env env n = match snd n with @@ -276,7 +276,7 @@ let expand_binders ?loc mkC bl c = | CLocalDef ((loc1,_) as n, oty, b) -> let env, c = loop ?loc:(Loc.merge_opt loc1 loc) bl c in let env = add_name_in_env env n in - (env, Loc.tag ?loc @@ CLetIn (n,oty,b,c)) + (env, CAst.make ?loc @@ CLetIn (n,oty,b,c)) | CLocalAssum ((loc1,_)::_ as nl, bk, t) -> let env, c = loop ?loc:(Loc.merge_opt loc1 loc) bl c in let env = List.fold_left add_name_in_env env nl in @@ -288,10 +288,10 @@ let expand_binders ?loc mkC bl c = let id = (loc1, Name ni) in let ty = match ty with | Some ty -> ty - | None -> Loc.tag ?loc:loc1 @@ CHole (None, IntroAnonymous, None) + | None -> CAst.make ?loc:loc1 @@ CHole (None, IntroAnonymous, None) in - let e = Loc.tag @@ CRef (Libnames.Ident (loc1, ni), None) in - let c = Loc.tag ?loc @@ + let e = CAst.make @@ CRef (Libnames.Ident (loc1, ni), None) in + let c = CAst.make ?loc @@ CCases (LetPatternStyle, None, [(e,None,None)], [(Loc.tag ?loc:loc1 ([(loc1,[p])], c))]) @@ -302,11 +302,11 @@ let expand_binders ?loc mkC bl c = c let mkCProdN ?loc bll c = - let mk ?loc b c = Loc.tag ?loc @@ CProdN ([b],c) in + let mk ?loc b c = CAst.make ?loc @@ CProdN ([b],c) in expand_binders ?loc mk bll c let mkCLambdaN ?loc bll c = - let mk ?loc b c = Loc.tag ?loc @@ CLambdaN ([b],c) in + let mk ?loc b c = CAst.make ?loc @@ CLambdaN ([b],c) in expand_binders ?loc mk bll c (* Deprecated *) @@ -320,14 +320,13 @@ let coerce_reference_to_id = function (str "This expression should be a simple identifier.") let coerce_to_id = function - | _loc, CRef (Ident (loc,id),_) -> (loc,id) - | a -> CErrors.user_err ?loc:(constr_loc a) + | { CAst.v = CRef (Ident (loc,id),_); _ } -> (loc,id) + | { CAst.loc; _ } -> CErrors.user_err ?loc ~hdr:"coerce_to_id" (str "This expression should be a simple identifier.") let coerce_to_name = function - | _loc, CRef (Ident (loc,id),_) -> (loc,Name id) - | loc, CHole (_,_,_) -> (loc,Anonymous) - | a -> CErrors.user_err - ?loc:(constr_loc a) ~hdr:"coerce_to_name" - (str "This expression should be a name.") + | { CAst.v = CRef (Ident (loc,id),_) } -> (loc,Name id) + | { CAst.loc; CAst.v = CHole (_,_,_) } -> (loc,Anonymous) + | { CAst.loc; _ } -> CErrors.user_err ?loc ~hdr:"coerce_to_name" + (str "This expression should be a name.") diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 30b81ecc4a..e8a5b52651 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -144,15 +144,15 @@ module PrintingConstructor = Goptions.MakeRefTable(PrintingRecordConstructor) let insert_delimiters e = function | None -> e - | Some sc -> Loc.tag @@ CDelimiters (sc,e) + | Some sc -> CAst.make @@ CDelimiters (sc,e) let insert_pat_delimiters ?loc p = function | None -> p - | Some sc -> Loc.tag ?loc @@ CPatDelimiters (sc,p) + | Some sc -> CAst.make ?loc @@ CPatDelimiters (sc,p) let insert_pat_alias ?loc p = function | Anonymous -> p - | Name id -> Loc.tag ?loc @@ CPatAlias (p,id) + | Name id -> CAst.make ?loc @@ CPatAlias (p,id) (**********************************************************************) (* conversion of references *) @@ -178,7 +178,7 @@ let extern_reference ?loc vars l = !my_extern_reference ?loc vars l let add_patt_for_params ind l = if !Flags.in_debugger then l else - Util.List.addn (Inductiveops.inductive_nparamdecls ind) (Loc.tag @@ CPatAtom None) l + Util.List.addn (Inductiveops.inductive_nparamdecls ind) (CAst.make @@ CPatAtom None) l let add_cpatt_for_params ind l = if !Flags.in_debugger then l else @@ -190,7 +190,7 @@ let drop_implicits_in_patt cst nb_expl args = let rec impls_fit l = function |[],t -> Some (List.rev_append l t) |_,[] -> None - |h::t,(_loc, CPatAtom None)::tt when is_status_implicit h -> impls_fit l (t,tt) + |h::t, { CAst.v = CPatAtom None }::tt when is_status_implicit h -> impls_fit l (t,tt) |h::_,_ when is_status_implicit h -> None |_::t,hh::tt -> impls_fit (hh::l) (t,tt) in let rec aux = function @@ -236,8 +236,8 @@ let expand_curly_brackets loc mknot ntn l = (* side effect *) mknot (loc,!ntn',l) -let destPrim = function _loc, CPrim t -> Some t | _ -> None -let destPatPrim = function _loc, CPatPrim t -> Some t | _ -> None +let destPrim = function { CAst.v = CPrim t } -> Some t | _ -> None +let destPatPrim = function { CAst.v = CPatPrim t } -> Some t | _ -> None let make_notation_gen loc ntn mknot mkprim destprim l = if has_curly_brackets ntn @@ -259,21 +259,21 @@ let make_notation_gen loc ntn mknot mkprim destprim l = let make_notation loc ntn (terms,termlists,binders as subst) = if not (List.is_empty termlists) || not (List.is_empty binders) then - Loc.tag ?loc @@ CNotation (ntn,subst) + CAst.make ?loc @@ CNotation (ntn,subst) else make_notation_gen loc ntn - (fun (loc,ntn,l) -> Loc.tag ?loc @@ CNotation (ntn,(l,[],[]))) - (fun (loc,p) -> Loc.tag ?loc @@ CPrim p) + (fun (loc,ntn,l) -> CAst.make ?loc @@ CNotation (ntn,(l,[],[]))) + (fun (loc,p) -> CAst.make ?loc @@ CPrim p) destPrim terms let make_pat_notation ?loc ntn (terms,termlists as subst) args = - if not (List.is_empty termlists) then (Loc.tag ?loc @@ CPatNotation (ntn,subst,args)) else + if not (List.is_empty termlists) then (CAst.make ?loc @@ CPatNotation (ntn,subst,args)) else make_notation_gen loc ntn - (fun (loc,ntn,l) -> Loc.tag ?loc @@ CPatNotation (ntn,(l,[]),args)) - (fun (loc,p) -> Loc.tag ?loc @@ CPatPrim p) + (fun (loc,ntn,l) -> CAst.make ?loc @@ CPatNotation (ntn,(l,[]),args)) + (fun (loc,p) -> CAst.make ?loc @@ CPatPrim p) destPatPrim terms -let mkPat ?loc qid l = Loc.tag ?loc @@ +let mkPat ?loc qid l = CAst.make ?loc @@ (* Normally irrelevant test with v8 syntax, but let's do it anyway *) if List.is_empty l then CPatAtom (Some qid) else CPatCstr (qid,None,l) @@ -295,7 +295,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = when !Flags.in_debugger||Inductiveops.constructor_has_local_defs cstrsp -> let c = extern_reference ?loc Id.Set.empty (ConstructRef cstrsp) in let args = List.map (extern_cases_pattern_in_scope scopes vars) args in - Loc.tag ?loc @@ CPatCstr (c, Some (add_patt_for_params (fst cstrsp) args), []) + CAst.make ?loc @@ CPatCstr (c, Some (add_patt_for_params (fst cstrsp) args), []) | _ -> try if !Flags.raw_print || !print_no_symbol then raise No_match; @@ -304,7 +304,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = | None -> raise No_match | Some key -> let loc = cases_pattern_loc pat in - insert_pat_alias ?loc (insert_pat_delimiters ?loc (Loc.tag ?loc @@ CPatPrim p) key) na + insert_pat_alias ?loc (insert_pat_delimiters ?loc (CAst.make ?loc @@ CPatPrim p) key) na with No_match -> try if !Flags.raw_print || !print_no_symbol then raise No_match; @@ -312,8 +312,8 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = (uninterp_cases_pattern_notations pat) with No_match -> match pat with - | loc, PatVar (Name id) -> Loc.tag ?loc @@ CPatAtom (Some (Ident (loc,id))) - | loc, PatVar (Anonymous) -> Loc.tag ?loc @@ CPatAtom None + | loc, PatVar (Name id) -> CAst.make ?loc @@ CPatAtom (Some (Ident (loc,id))) + | loc, PatVar (Anonymous) -> CAst.make ?loc @@ CPatAtom None | loc, PatCstr(cstrsp,args,na) -> let args = List.map (extern_cases_pattern_in_scope scopes vars) args in let p = @@ -327,24 +327,29 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = | Some c :: q -> match args with | [] -> raise No_match - | (_loc, CPatAtom(None)) :: tail -> ip q tail acc + + + + + + | { CAst.v = CPatAtom None } :: tail -> ip q tail acc (* we don't want to have 'x = _' in our patterns *) | head :: tail -> ip q tail ((extern_reference ?loc Id.Set.empty (ConstRef c), head) :: acc) in - Loc.tag ?loc @@ CPatRecord(List.rev (ip projs args [])) + CAst.make ?loc @@ CPatRecord(List.rev (ip projs args [])) with Not_found | No_match | Exit -> let c = extern_reference ?loc Id.Set.empty (ConstructRef cstrsp) in if !Topconstr.asymmetric_patterns then if pattern_printable_in_both_syntax cstrsp - then Loc.tag ?loc @@ CPatCstr (c, None, args) - else Loc.tag ?loc @@ CPatCstr (c, Some (add_patt_for_params (fst cstrsp) args), []) + then CAst.make ?loc @@ CPatCstr (c, None, args) + else CAst.make ?loc @@ CPatCstr (c, Some (add_patt_for_params (fst cstrsp) args), []) else let full_args = add_patt_for_params (fst cstrsp) args in match drop_implicits_in_patt (ConstructRef cstrsp) 0 full_args with - | Some true_args -> Loc.tag ?loc @@ CPatCstr (c, None, true_args) - | None -> Loc.tag ?loc @@ CPatCstr (c, Some full_args, []) + | Some true_args -> CAst.make ?loc @@ CPatCstr (c, None, true_args) + | None -> CAst.make ?loc @@ CPatCstr (c, Some full_args, []) in insert_pat_alias ?loc p na and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) (tmp_scope, scopes as allscopes) vars = @@ -401,8 +406,8 @@ and extern_notation_pattern (tmp_scope,scopes as allscopes) vars (loc, t) = func let p = apply_notation_to_pattern ?loc (ConstructRef cstr) (match_notation_constr_cases_pattern (loc, t) pat) allscopes vars keyrule in insert_pat_alias ?loc p na - | PatVar Anonymous -> Loc.tag ?loc @@ CPatAtom None - | PatVar (Name id) -> Loc.tag ?loc @@ CPatAtom (Some (Ident (loc,id))) + | PatVar Anonymous -> CAst.make ?loc @@ CPatAtom None + | PatVar (Name id) -> CAst.make ?loc @@ CPatAtom (Some (Ident (loc,id))) with No_match -> extern_notation_pattern allscopes vars (loc, t) rules @@ -422,7 +427,7 @@ let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args = if !Flags.in_debugger||Inductiveops.inductive_has_local_defs ind then let c = extern_reference vars (IndRef ind) in let args = List.map (extern_cases_pattern_in_scope scopes vars) args in - Loc.tag @@ CPatCstr (c, Some (add_patt_for_params ind args), []) + CAst.make @@ CPatCstr (c, Some (add_patt_for_params ind args), []) else try if !Flags.raw_print || !print_no_symbol then raise No_match; @@ -430,7 +435,7 @@ let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args = match availability_of_prim_token p sc scopes with | None -> raise No_match | Some key -> - insert_pat_delimiters (Loc.tag @@ CPatPrim p) key + insert_pat_delimiters (CAst.make @@ CPatPrim p) key with No_match -> try if !Flags.raw_print || !print_no_symbol then raise No_match; @@ -440,8 +445,8 @@ let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args = let c = extern_reference vars (IndRef ind) in let args = List.map (extern_cases_pattern_in_scope scopes vars) args in match drop_implicits_in_patt (IndRef ind) 0 args with - |Some true_args -> Loc.tag @@ CPatCstr (c, None, true_args) - |None -> Loc.tag @@ CPatCstr (c, Some args, []) + |Some true_args -> CAst.make @@ CPatCstr (c, None, true_args) + |None -> CAst.make @@ CPatCstr (c, Some args, []) let extern_cases_pattern vars p = extern_cases_pattern_in_scope (None,[]) vars p @@ -466,7 +471,7 @@ let is_projection nargs = function let is_hole = function CHole _ | CEvar _ -> true | _ -> false let is_significant_implicit a = - not (is_hole (snd a)) + not (is_hole (a.CAst.v)) let is_needed_for_correct_partial_application tail imp = List.is_empty tail && not (maximal_insertion_of imp) @@ -515,11 +520,11 @@ let explicitize inctx impl (cf,f) args = CApp ((ip,f),args1@args2) | None -> let args = exprec 1 (args,impl) in - if List.is_empty args then snd f else CApp ((None, f), args) + if List.is_empty args then f.CAst.v else CApp ((None, f), args) in try expl () with Expl -> - let f',us = match f with (_loc, CRef (f,us)) -> f,us | _ -> assert false in + let f',us = match f with { CAst.v = CRef (f,us) } -> f,us | _ -> assert false in let ip = if !print_projections then ip else None in CAppExpl ((ip, f', us), List.map Lazy.force args) @@ -546,7 +551,7 @@ let extern_app inctx impl (cf,f) us args = let args = List.map Lazy.force args in CAppExpl ((is_projection (List.length args) cf,f,us), args) else - explicitize inctx impl (cf, Loc.tag @@ CRef (f,us)) args + explicitize inctx impl (cf, CAst.make @@ CRef (f,us)) args let rec fill_arg_scopes args subscopes scopes = match args, subscopes with | [], _ -> [] @@ -600,7 +605,7 @@ let extern_possible_prim_token scopes r = let (sc,n) = uninterp_prim_token r in match availability_of_prim_token n sc scopes with | None -> None - | Some key -> Some (insert_delimiters (Loc.tag ?loc:(loc_of_glob_constr r) @@ CPrim n) key) + | Some key -> Some (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key) with No_match -> None @@ -608,7 +613,7 @@ let extern_optimal_prim_token scopes r r' = let c = extern_possible_prim_token scopes r in let c' = if r==r' then None else extern_possible_prim_token scopes r' in match c,c' with - | Some n, (Some ((_, CDelimiters _)) | None) | _, Some n -> n + | Some n, (Some ({ CAst.v = CDelimiters _}) | None) | _, Some n -> n | _ -> raise No_match (**********************************************************************) @@ -644,7 +649,7 @@ let rec extern inctx scopes vars r = let r'' = flatten_application r' in if !Flags.raw_print || !print_no_symbol then raise No_match; extern_notation scopes vars r'' (uninterp_notations r'') - with No_match -> Loc.map_with_loc (fun ?loc -> function + with No_match -> CAst.map_from_loc (fun ?loc -> function | GRef (ref,us) -> extern_global (select_stronger_impargs (implicits_of_global ref)) (extern_reference ?loc vars ref) (extern_universes us) @@ -824,7 +829,7 @@ and sub_extern inctx (_,scopes) = extern inctx (None,scopes) and factorize_prod scopes vars na bk aty c = let c = extern_typ scopes vars c in match na, c with - | Name id, (loc, CProdN ([nal,Default bk',ty],c)) + | Name id, { CAst.loc ; v = CProdN ([nal,Default bk',ty],c) } when binding_kind_eq bk bk' && constr_expr_eq aty ty && not (occur_var_constr_expr id ty) (* avoid na in ty escapes scope *) -> nal,c @@ -834,7 +839,7 @@ and factorize_prod scopes vars na bk aty c = and factorize_lambda inctx scopes vars na bk aty c = let c = sub_extern inctx scopes vars c in match c with - | loc, CLambdaN ([nal,Default bk',ty],c) + | { CAst.loc; v = CLambdaN ([nal,Default bk',ty],c) } when binding_kind_eq bk bk' && constr_expr_eq aty ty && not (occur_name na ty) (* avoid na in ty escapes scope *) -> nal,c @@ -943,12 +948,12 @@ and extern_notation (tmp_scope,scopes as allscopes) vars t = function extern true (scopt,scl@scopes) vars c, None) terms in let a = CRef (Qualid (loc, shortest_qualid_of_syndef vars kn),None) in - Loc.tag ?loc @@ if List.is_empty l then a else CApp ((None, Loc.tag a),l) in + CAst.make ?loc @@ if List.is_empty l then a else CApp ((None, CAst.make a),l) in if List.is_empty args then e else let args = fill_arg_scopes args argsscopes scopes in let args = extern_args (extern true) vars args in - Loc.tag ?loc @@ explicitize false argsimpls (None,e) args + CAst.make ?loc @@ explicitize false argsimpls (None,e) args with No_match -> extern_notation allscopes vars t rules diff --git a/interp/constrintern.ml b/interp/constrintern.ml index a672771b14..541b529729 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -217,7 +217,7 @@ let contract_notation ntn (l,ll,bll) = let ntn' = ref ntn in let rec contract_squash n = function | [] -> [] - | (_loc, CNotation ("{ _ }",([a],[],[]))) :: l -> + | { CAst.v = CNotation ("{ _ }",([a],[],[])) } :: l -> ntn' := expand_notation_string !ntn' n; contract_squash n (a::l) | a :: l -> @@ -230,7 +230,7 @@ let contract_pat_notation ntn (l,ll) = let ntn' = ref ntn in let rec contract_squash n = function | [] -> [] - | (_, CPatNotation ("{ _ }",([a],[]),[])) :: l -> + | { CAst.v = CPatNotation ("{ _ }",([a],[]),[]) } :: l -> ntn' := expand_notation_string !ntn' n; contract_squash n (a::l) | a :: l -> @@ -407,7 +407,7 @@ let intern_generalized_binder ?(global_level=false) intern_type lvar let name = let id = match ty with - | _, CApp ((_, (_, CRef (Ident (loc,id),_))), _) -> id + | { CAst.v = CApp ((_, { CAst.v = CRef (Ident (loc,id),_) } ), _) } -> id | _ -> default_non_dependent_ident in Implicit_quantifiers.make_fresh ids' (Global.env ()) id in Name name @@ -430,7 +430,7 @@ let intern_assumption intern lvar env nal bk ty = let env, b = intern_generalized_binder intern_type lvar env (List.hd nal) b b' t ty in env, b -let rec free_vars_of_pat il (loc, pt) = match pt with +let rec free_vars_of_pat il pt = match CAst.(pt.v) with | CPatCstr (c, l1, l2) -> let il = List.fold_left free_vars_of_pat il (Option.default [] l1) in List.fold_left free_vars_of_pat il l2 @@ -448,7 +448,7 @@ let intern_local_pattern intern lvar env p = List.fold_left (fun env (loc, i) -> let bk = Default Implicit in - let ty = Loc.tag ?loc @@ CHole (None, Misctypes.IntroAnonymous, None) in + let ty = CAst.make ?loc @@ CHole (None, Misctypes.IntroAnonymous, None) in let n = Name i in let env, _ = intern_assumption intern lvar env [(loc, n)] bk ty in env) @@ -480,7 +480,7 @@ let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = functio let tyc = match ty with | Some ty -> ty - | None -> Loc.tag ?loc @@ CHole(None,Misctypes.IntroAnonymous,None) + | None -> CAst.make ?loc @@ CHole(None,Misctypes.IntroAnonymous,None) in let env = intern_local_pattern intern lvar env p in let il = List.map snd (free_vars_of_pat [] p) in @@ -596,16 +596,16 @@ let rec subordinate_letins letins = function letins,[] let terms_of_binders bl = - let rec term_of_pat pt = Loc.map_with_loc (fun ?loc -> function + let rec term_of_pat pt = CAst.map_from_loc (fun ?loc -> function | PatVar (Name id) -> CRef (Ident (loc,id), None) | PatVar (Anonymous) -> error "Cannot turn \"_\" into a term." | PatCstr (c,l,_) -> let r = Qualid (loc,qualid_of_path (path_of_global (ConstructRef c))) in - let hole = Loc.tag ?loc @@ CHole (None,Misctypes.IntroAnonymous,None) in + let hole = CAst.make ?loc @@ CHole (None,Misctypes.IntroAnonymous,None) in let params = List.make (Inductiveops.inductive_nparams (fst c)) hole in CAppExpl ((None,r,None),params @ List.map term_of_pat l)) pt in let rec extract_variables = function - | (loc, GLocalAssum (Name id,_,_))::l -> (Loc.tag ?loc @@ CRef (Ident (loc,id), None)) :: extract_variables l + | (loc, GLocalAssum (Name id,_,_))::l -> (CAst.make ?loc @@ CRef (Ident (loc,id), None)) :: extract_variables l | (loc, GLocalDef (Name id,_,_,_))::l -> extract_variables l | (loc, GLocalDef (Anonymous,_,_,_))::l | (loc, GLocalAssum (Anonymous,_,_))::l -> error "Cannot turn \"_\" into a term." @@ -760,7 +760,7 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id us = try let ty,expl_impls,impls,argsc = Id.Map.find id genv.impls in let expl_impls = List.map - (fun id -> Loc.tag ?loc @@ CRef (Ident (loc,id),None), Some (loc,ExplByName id)) expl_impls in + (fun id -> CAst.make ?loc @@ CRef (Ident (loc,id),None), Some (loc,ExplByName id)) expl_impls in let tys = string_of_ty ty in Dumpglob.dump_reference ?loc "<>" (Id.to_string id) tys; gvar (loc,id) us, make_implicits_list impls, argsc, expl_impls @@ -993,10 +993,10 @@ let add_implicits_check_length fail nargs nargs_with_letin impls_st len_pl1 pl2 else Int.equal args_len nargs_with_letin || (fst (fail (nargs - List.length impl_list + i)))) ,l) |imp::q as il,[] -> if is_status_implicit imp && maximal_insertion_of imp - then let (b,out) = aux i (q,[]) in (b,(Loc.tag @@ RCPatAtom(None))::out) + then let (b,out) = aux i (q,[]) in (b,(CAst.make @@ RCPatAtom(None))::out) else fail (remaining_args (len_pl1+i) il) |imp::q,(hh::tt as l) -> if is_status_implicit imp - then let (b,out) = aux i (q,l) in (b,(Loc.tag @@ RCPatAtom(None))::out) + then let (b,out) = aux i (q,l) in (b,(CAst.make @@ RCPatAtom(None))::out) else let (b,out) = aux (succ i) (q,tt) in (b,hh::out) in aux 0 (impl_list,pl2) @@ -1199,14 +1199,15 @@ let alias_of als = match als.alias_ids with *) -let rec subst_pat_iterator y t (loc, p) = match p with - | RCPatAtom id -> - begin match id with Some x when Id.equal x y -> t | _ -> Loc.tag ?loc p end +let rec subst_pat_iterator y t = CAst.map (function + | RCPatAtom id as p -> + begin match id with Some x when Id.equal x y -> t.CAst.v | _ -> p end | RCPatCstr (id,l1,l2) -> - Loc.tag ?loc @@ RCPatCstr (id, List.map (subst_pat_iterator y t) l1, - List.map (subst_pat_iterator y t) l2) - | RCPatAlias (p,a) -> Loc.tag ?loc @@ RCPatAlias (subst_pat_iterator y t p,a) - | RCPatOr pl -> Loc.tag ?loc @@ RCPatOr (List.map (subst_pat_iterator y t) pl) + RCPatCstr (id, List.map (subst_pat_iterator y t) l1, + List.map (subst_pat_iterator y t) l2) + | RCPatAlias (p,a) -> RCPatAlias (subst_pat_iterator y t p,a) + | RCPatOr pl -> RCPatOr (List.map (subst_pat_iterator y t) pl) + ) let drop_notations_pattern looked_for = (* At toplevel, Constructors and Inductives are accepted, in recursive calls @@ -1255,26 +1256,29 @@ let drop_notations_pattern looked_for = let (_,argscs) = find_remaining_scopes [] pats g in Some (g,[],List.map2 (fun x -> in_pat false (x,snd scopes)) argscs pats) with Not_found -> None - and in_pat top scopes (loc, pt) = match pt with - | CPatAlias (p, id) -> Loc.tag ?loc @@ RCPatAlias (in_pat top scopes p, id) + and in_pat top scopes pt = + let open CAst in + let loc = pt.loc in + match pt.v with + | CPatAlias (p, id) -> CAst.make ?loc @@ RCPatAlias (in_pat top scopes p, id) | CPatRecord l -> let sorted_fields = - sort_fields ~complete:false loc l (fun _idx -> (loc, CPatAtom None)) in + sort_fields ~complete:false loc l (fun _idx -> CAst.make ?loc @@ CPatAtom None) in begin match sorted_fields with - | None -> Loc.tag ?loc @@ RCPatAtom None + | None -> CAst.make ?loc @@ RCPatAtom None | Some (n, head, pl) -> let pl = if !asymmetric_patterns then pl else - let pars = List.make n (loc, CPatAtom None) in + let pars = List.make n (CAst.make ?loc @@ CPatAtom None) in List.rev_append pars pl in match drop_syndef top scopes head pl with - |Some (a,b,c) -> (loc, RCPatCstr(a, b, c)) - |None -> raise (InternalizationError (loc,NotAConstructor head)) + | Some (a,b,c) -> CAst.make ?loc @@ RCPatCstr(a, b, c) + | None -> raise (InternalizationError (loc,NotAConstructor head)) end | CPatCstr (head, None, pl) -> begin match drop_syndef top scopes head pl with - | Some (a,b,c) -> Loc.tag ?loc @@ RCPatCstr(a, b, c) + | Some (a,b,c) -> CAst.make ?loc @@ RCPatCstr(a, b, c) | None -> raise (InternalizationError (loc,NotAConstructor head)) end | CPatCstr (r, Some expl_pl, pl) -> @@ -1283,13 +1287,13 @@ let drop_notations_pattern looked_for = raise (InternalizationError (loc,NotAConstructor r)) in if expl_pl == [] then (* Convention: (@r) deactivates all further implicit arguments and scopes *) - Loc.tag ?loc @@ RCPatCstr (g, List.map (in_pat false scopes) pl, []) + CAst.make ?loc @@ RCPatCstr (g, List.map (in_pat false scopes) pl, []) else (* Convention: (@r expl_pl) deactivates implicit arguments in expl_pl and in pl *) (* but not scopes in expl_pl *) let (argscs1,_) = find_remaining_scopes expl_pl pl g in - Loc.tag ?loc @@ RCPatCstr (g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat false scopes) pl, []) - | CPatNotation ("- _",([_loc,CPatPrim(Numeral p)],[]),[]) + CAst.make ?loc @@ RCPatCstr (g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat false scopes) pl, []) + | CPatNotation ("- _",([{ CAst.v = CPatPrim(Numeral p) }],[]),[]) when Bigint.is_strictly_pos p -> fst (Notation.interp_prim_token_cases_pattern_expr ?loc (ensure_kind false loc) (Numeral (Bigint.neg p)) scopes) | CPatNotation ("( _ )",([a],[]),[]) -> @@ -1308,11 +1312,11 @@ let drop_notations_pattern looked_for = | CPatAtom Some id -> begin match drop_syndef top scopes id [] with - | Some (a,b,c) -> Loc.tag ?loc @@ RCPatCstr (a, b, c) - | None -> Loc.tag ?loc @@ RCPatAtom (Some (find_pattern_variable id)) + | Some (a,b,c) -> CAst.make ?loc @@ RCPatCstr (a, b, c) + | None -> CAst.make ?loc @@ RCPatAtom (Some (find_pattern_variable id)) end - | CPatAtom None -> Loc.tag ?loc @@ RCPatAtom None - | CPatOr pl -> Loc.tag ?loc @@ RCPatOr (List.map (in_pat top scopes) pl) + | CPatAtom None -> CAst.make ?loc @@ RCPatAtom None + | CPatOr pl -> CAst.make ?loc @@ RCPatOr (List.map (in_pat top scopes) pl) | CPatCast _ -> assert false and in_pat_sc scopes x = in_pat false (x,snd scopes) @@ -1326,17 +1330,17 @@ let drop_notations_pattern looked_for = let (a,(scopt,subscopes)) = Id.Map.find id subst in in_pat top (scopt,subscopes@snd scopes) a with Not_found -> - if Id.equal id ldots_var then Loc.tag ?loc @@ RCPatAtom (Some id) else + if Id.equal id ldots_var then CAst.make ?loc @@ RCPatAtom (Some id) else anomaly (str "Unbound pattern notation variable: " ++ Id.print id) end | NRef g -> ensure_kind top loc g; let (_,argscs) = find_remaining_scopes [] args g in - Loc.tag ?loc @@ RCPatCstr (g, [], List.map2 (in_pat_sc scopes) argscs args) + CAst.make ?loc @@ RCPatCstr (g, [], List.map2 (in_pat_sc scopes) argscs args) | NApp (NRef g,pl) -> ensure_kind top loc g; let (argscs1,argscs2) = find_remaining_scopes pl args g in - Loc.tag ?loc @@ RCPatCstr (g, + CAst.make ?loc @@ RCPatCstr (g, List.map2 (fun x -> in_not false loc (x,snd scopes) fullsubst []) argscs1 pl @ List.map (in_pat false scopes) args, []) | NList (x,y,iter,terminator,lassoc) -> @@ -1355,7 +1359,7 @@ let drop_notations_pattern looked_for = anomaly (Pp.str "Inconsistent substitution of recursive notation")) | NHole _ -> let () = assert (List.is_empty args) in - Loc.tag ?loc @@ RCPatAtom None + CAst.make ?loc @@ RCPatAtom None | t -> error_invalid_pattern_notation ?loc () in in_pat true @@ -1366,11 +1370,12 @@ let rec intern_pat genv aliases pat = let pl' = List.map (fun (asubst,pl) -> (asubst, Loc.tag ?loc @@ PatCstr (c,chop_params_pattern loc (fst c) pl with_letin,alias_of aliases))) pll in ids',pl' in - match pat with - | loc, RCPatAlias (p, id) -> + let loc = CAst.(pat.loc) in + match CAst.(pat.v) with + | RCPatAlias (p, id) -> let aliases' = merge_aliases aliases id in intern_pat genv aliases' p - | loc, RCPatCstr (head, expl_pl, pl) -> + | RCPatCstr (head, expl_pl, pl) -> if !asymmetric_patterns then let len = if List.is_empty expl_pl then Some (List.length pl) else None in let c,idslpl1 = find_constructor loc len head in @@ -1382,13 +1387,13 @@ let rec intern_pat genv aliases pat = let with_letin, pl2 = add_implicits_check_constructor_length genv loc c (List.length idslpl1 + List.length expl_pl) pl in intern_cstr_with_all_args loc c with_letin idslpl1 (expl_pl@pl2) - | loc, RCPatAtom (Some id) -> + | RCPatAtom (Some id) -> let aliases = merge_aliases aliases id in (aliases.alias_ids,[aliases.alias_map, Loc.tag ?loc @@ PatVar (alias_of aliases)]) - | loc, RCPatAtom (None) -> + | RCPatAtom (None) -> let { alias_ids = ids; alias_map = asubst; } = aliases in (ids, [asubst, Loc.tag ?loc @@ PatVar (alias_of aliases)]) - | loc, RCPatOr pl -> + | RCPatOr pl -> assert (not (List.is_empty pl)); let pl' = List.map (intern_pat genv aliases) pl in let (idsl,pl') = List.split pl' in @@ -1406,9 +1411,9 @@ let rec intern_pat genv aliases pat = of lambdas in the encoding of match in constr. We put this check here and not in the parser because it would require to duplicate the levels of the [pattern] rule. *) -let rec check_no_patcast (loc, pt) = match pt with +let rec check_no_patcast pt = match CAst.(pt.v) with | CPatCast (_,_) -> - CErrors.user_err ?loc ~hdr:"check_no_patcast" + CErrors.user_err ?loc:pt.CAst.loc ~hdr:"check_no_patcast" (Pp.strbrk "Casts are not supported here.") | CPatDelimiters(_,p) | CPatAlias(p,_) -> check_no_patcast p @@ -1444,8 +1449,9 @@ let intern_ind_pattern genv scopes pat = drop_notations_pattern (function (IndRef _ | ConstructRef _) -> () | _ -> raise Not_found) scopes pat with InternalizationError(loc,NotAConstructor _) -> error_bad_inductive_type ?loc in - match no_not with - | loc, RCPatCstr (head, expl_pl, pl) -> + let loc = no_not.CAst.loc in + match no_not.CAst.v with + | RCPatCstr (head, expl_pl, pl) -> let c = (function IndRef ind -> ind | _ -> error_bad_inductive_type ?loc) head in let with_letin, pl2 = add_implicits_check_ind_length genv loc c (List.length expl_pl) pl in @@ -1455,7 +1461,7 @@ let intern_ind_pattern genv scopes pat = match product_of_cases_patterns [] (List.rev_append idslpl1 idslpl2) with | _,[_,pl] -> (c,chop_params_pattern loc c pl with_letin) | _ -> error_bad_inductive_type ?loc) - | x -> error_bad_inductive_type ?loc:(raw_cases_pattern_expr_loc x) + | x -> error_bad_inductive_type ?loc (**********************************************************************) (* Utilities for application *) @@ -1521,7 +1527,7 @@ let extract_explicit_arg imps args = (* Main loop *) let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = - let rec intern env = Loc.with_loc (fun ?loc -> function + let rec intern env = CAst.with_loc_val (fun ?loc -> function | CRef (ref,us) -> let (c,imp,subscopes,l),_ = intern_applied_reference intern env (Environ.named_context globalenv) @@ -1602,20 +1608,20 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = | CProdN ([],c2) -> intern_type env c2 | CProdN ((nal,bk,ty)::bll,c2) -> - iterate_prod ?loc env bk ty (Loc.tag ?loc @@ CProdN (bll, c2)) nal + iterate_prod ?loc env bk ty (CAst.make ?loc @@ CProdN (bll, c2)) nal | CLambdaN ([],c2) -> intern env c2 | CLambdaN ((nal,bk,ty)::bll,c2) -> - iterate_lam loc (reset_tmp_scope env) bk ty (Loc.tag ?loc @@ CLambdaN (bll, c2)) nal + iterate_lam loc (reset_tmp_scope env) bk ty (CAst.make ?loc @@ CLambdaN (bll, c2)) nal | CLetIn (na,c1,t,c2) -> let inc1 = intern (reset_tmp_scope env) c1 in let int = Option.map (intern_type env) t in Loc.tag ?loc @@ GLetIn (snd na, inc1, int, intern (push_name_env ntnvars (impls_term_list inc1) env na) c2) - | CNotation ("- _",([_, CPrim (Numeral p)],[],[])) + | CNotation ("- _",([{ CAst.v = CPrim (Numeral p) }],[],[])) when Bigint.is_strictly_pos p -> - intern env (Loc.tag ?loc @@ CPrim (Numeral (Bigint.neg p))) + intern env (CAst.make ?loc @@ CPrim (Numeral (Bigint.neg p))) | CNotation ("( _ )",([a],[],[])) -> intern env a | CNotation (ntn,args) -> intern_notation intern env ntnvars loc ntn args @@ -1639,20 +1645,20 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = | CApp ((isproj,f), args) -> let f,args = match f with (* Compact notations like "t.(f args') args" *) - | _loc, CApp ((Some _,f), args') when not (Option.has_some isproj) -> + | { CAst.v = CApp ((Some _,f), args') } when not (Option.has_some isproj) -> f,args'@args (* Don't compact "(f args') args" to resolve implicits separately *) | _ -> f,args in let (c,impargs,args_scopes,l),args = - match f with - | _loc, CRef (ref,us) -> + match f.CAst.v with + | CRef (ref,us) -> intern_applied_reference intern env (Environ.named_context globalenv) lvar us args ref - | _loc, CNotation (ntn,([],[],[])) -> + | CNotation (ntn,([],[],[])) -> let c = intern_notation intern env ntnvars loc ntn ([],[],[]) in let x, impl, scopes, l = find_appl_head_data c in (x,impl,scopes,l), args - | x -> (intern env f,[],[],[]), args in + | _ -> (intern env f,[],[],[]), args in apply_impargs c env impargs args_scopes (merge_impargs l args) loc @@ -1660,15 +1666,15 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in let fields = sort_fields ~complete:true loc fs - (fun _idx -> Loc.tag ?loc @@ CHole (Some (Evar_kinds.QuestionMark st), - Misctypes.IntroAnonymous, None)) + (fun _idx -> CAst.make ?loc @@ CHole (Some (Evar_kinds.QuestionMark st), + Misctypes.IntroAnonymous, None)) in begin match fields with | None -> user_err ?loc ~hdr:"intern" (str"No constructor inference.") | Some (n, constrname, args) -> - let pars = List.make n (Loc.tag ?loc @@ CHole (None, Misctypes.IntroAnonymous, None)) in - let app = Loc.tag ?loc @@ CAppExpl ((None, constrname,None), List.rev_append pars args) in + let pars = List.make n (CAst.make ?loc @@ CHole (None, Misctypes.IntroAnonymous, None)) in + let app = CAst.make ?loc @@ CAppExpl ((None, constrname,None), List.rev_append pars args) in intern env app end | CCases (sty, rtnpo, tms, eqns) -> @@ -1910,6 +1916,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = in aux 1 l subscopes eargs rargs and apply_impargs c env imp subscopes l loc = + let l : (Constrexpr.constr_expr * Constrexpr.explicitation Loc.located option) list = l in let imp = select_impargs_size (List.length (List.filter (fun (_,x) -> x == None) l)) imp in let l = intern_impargs c env imp subscopes l in smart_gapp c loc l diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index dd04e20306..52a6c450b6 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -92,11 +92,11 @@ let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l = else ungeneralizable loc id else l in - let rec aux bdvars l (loc, c) = match c with + let rec aux bdvars l c = match CAst.(c.v) with | CRef (Ident (loc,id),_) -> found loc id bdvars l - | CNotation ("{ _ : _ | _ }", ((_, CRef (Ident (_, id),_)) :: _, [], [])) when not (Id.Set.mem id bdvars) -> - Topconstr.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux (Id.Set.add id bdvars) l (loc, c) - | c -> Topconstr.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux bdvars l (loc, c) + | CNotation ("{ _ : _ | _ }", ({ CAst.v = CRef (Ident (_, id),_) } :: _, [], [])) when not (Id.Set.mem id bdvars) -> + Topconstr.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux (Id.Set.add id bdvars) l c + | _ -> Topconstr.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux bdvars l c in aux bound l c let ids_of_names l = @@ -252,18 +252,22 @@ let combine_params avoid fn applied needed = let combine_params_freevar = fun avoid (_, decl) -> let id' = next_name_away_from (RelDecl.get_name decl) avoid in - (Loc.tag @@ CRef (Ident (Loc.tag id'),None), Id.Set.add id' avoid) + (CAst.make @@ CRef (Ident (Loc.tag id'),None), Id.Set.add id' avoid) -let destClassApp (loc, cl) = - match cl with - | CApp ((None, (_loc, CRef (ref, inst))), l) -> Loc.tag ?loc (ref, List.map fst l, inst) +let destClassApp cl = + let open CAst in + let loc = cl.loc in + match cl.v with + | CApp ((None, { v = CRef (ref, inst) }), l) -> Loc.tag ?loc (ref, List.map fst l, inst) | CAppExpl ((None, ref, inst), l) -> Loc.tag ?loc (ref, l, inst) | CRef (ref, inst) -> Loc.tag ?loc:(loc_of_reference ref) (ref, [], inst) | _ -> raise Not_found -let destClassAppExpl (loc, cl) = - match cl with - | CApp ((None, (_loc, CRef (ref, inst))), l) -> Loc.tag ?loc (ref, l, inst) +let destClassAppExpl cl = + let open CAst in + let loc = cl.loc in + match cl.v with + | CApp ((None, { v = CRef (ref, inst) } ), l) -> Loc.tag ?loc (ref, l, inst) | CRef (ref, inst) -> Loc.tag ?loc:(loc_of_reference ref) (ref, [], inst) | _ -> raise Not_found @@ -296,7 +300,7 @@ let implicit_application env ?(allow_partial=true) f ty = end; let pars = List.rev (List.combine ci rd) in let args, avoid = combine_params avoid f par pars in - Loc.tag ?loc @@ CAppExpl ((None, id, inst), args), avoid + CAst.make ?loc @@ CAppExpl ((None, id, inst), args), avoid in c, avoid let implicits_of_glob_constr ?(with_products=true) l = diff --git a/interp/notation.ml b/interp/notation.ml index 150be040f3..03dffa6eef 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -471,7 +471,7 @@ let interp_prim_token = (** [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *) -let rec rcp_of_glob looked_for gt = Loc.map (function +let rec rcp_of_glob looked_for gt = CAst.map_from_loc (fun ?loc -> function | GVar id -> RCPatAtom (Some id) | GHole (_,_,_) -> RCPatAtom None | GRef (g,_) -> looked_for g; RCPatCstr (g,[],[]) diff --git a/interp/topconstr.ml b/interp/topconstr.ml index a74e641725..eb89b2ef24 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -43,7 +43,7 @@ let is_constructor id = (Nametab.locate_extended (qualid_of_ident id))) with Not_found -> false -let rec cases_pattern_fold_names f a pt = match snd pt with +let rec cases_pattern_fold_names f a pt = match CAst.(pt.v) with | CPatRecord l -> List.fold_left (fun acc (r, cp) -> cases_pattern_fold_names f acc cp) a l | CPatAlias (pat,id) -> f id a @@ -58,7 +58,7 @@ let rec cases_pattern_fold_names f a pt = match snd pt with | CPatDelimiters (_,pat) -> cases_pattern_fold_names f a pat | CPatAtom (Some (Ident (_,id))) when not (is_constructor id) -> f id a | CPatPrim _ | CPatAtom _ -> a - | CPatCast ((loc,_),_) -> + | CPatCast ({CAst.loc},_) -> CErrors.user_err ?loc ~hdr:"cases_pattern_fold_names" (Pp.strbrk "Casts are not supported here.") @@ -103,7 +103,7 @@ let rec fold_local_binders g f n acc b = function | [] -> f n acc b -let fold_constr_expr_with_binders g f n acc = Loc.with_loc (fun ?loc -> function +let fold_constr_expr_with_binders g f n acc = CAst.with_val (function | CAppExpl ((_,_,_),l) -> List.fold_left (f n) acc l | CApp ((_,t),l) -> List.fold_left (f n) (f n acc t) (List.map fst l) | CProdN (l,b) | CLambdaN (l,b) -> fold_constr_expr_binders g f n acc b l @@ -115,7 +115,7 @@ let fold_constr_expr_with_binders g f n acc = Loc.with_loc (fun ?loc -> function (* The following is an approximation: we don't know exactly if an ident is binding nor to which subterms bindings apply *) let acc = List.fold_left (f n) acc (l@List.flatten ll) in - List.fold_left (fun acc bl -> fold_local_binders g f n acc (Loc.tag @@ CHole (None,IntroAnonymous,None)) bl) acc bll + List.fold_left (fun acc bl -> fold_local_binders g f n acc (CAst.make @@ CHole (None,IntroAnonymous,None)) bl) acc bll | CGeneralization (_,_,c) -> f n acc c | CDelimiters (_,a) -> f n acc a | CHole _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CRef _ -> @@ -146,7 +146,7 @@ let fold_constr_expr_with_binders g f n acc = Loc.with_loc (fun ?loc -> function let free_vars_of_constr_expr c = let rec aux bdvars l = function - | _loc, CRef (Ident (_,id),_) -> if Id.List.mem id bdvars then l else Id.Set.add id l + | { CAst.v = CRef (Ident (_,id),_) } -> if Id.List.mem id bdvars then l else Id.Set.add id l | c -> fold_constr_expr_with_binders (fun a l -> a::l) aux bdvars l c in aux [] Id.Set.empty c @@ -210,7 +210,7 @@ let map_local_binders f g e bl = let (e,rbl) = List.fold_left h (e,[]) bl in (e, List.rev rbl) -let map_constr_expr_with_binders g f e = Loc.map (function +let map_constr_expr_with_binders g f e = CAst.map (function | CAppExpl (r,l) -> CAppExpl (r,List.map (f e) l) | CApp ((p,a),l) -> CApp ((p,f e a),List.map (fun (a,i) -> (f e a,i)) l) @@ -263,8 +263,8 @@ let map_constr_expr_with_binders g f e = Loc.map (function (* Used in constrintern *) let rec replace_vars_constr_expr l = function - | loc, CRef (Ident (loc_id,id),us) as x -> - (try loc, CRef (Ident (loc_id,Id.Map.find id l),us) with Not_found -> x) + | { CAst.loc; v = CRef (Ident (loc_id,id),us) } as x -> + (try CAst.make ?loc @@ CRef (Ident (loc_id,Id.Map.find id l),us) with Not_found -> x) | c -> map_constr_expr_with_binders Id.Map.remove replace_vars_constr_expr l c diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli index 23223173e1..4f1e9d8e62 100644 --- a/intf/constrexpr.mli +++ b/intf/constrexpr.mli @@ -42,7 +42,7 @@ type raw_cases_pattern_expr_r = (** [CPatCstr (_, c, l1, l2)] represents ((@c l1) l2) *) | RCPatAtom of Id.t option | RCPatOr of raw_cases_pattern_expr list -and raw_cases_pattern_expr = raw_cases_pattern_expr_r Loc.located +and raw_cases_pattern_expr = raw_cases_pattern_expr_r CAst.ast type instance_expr = Misctypes.glob_level list @@ -61,7 +61,7 @@ type cases_pattern_expr_r = | CPatRecord of (reference * cases_pattern_expr) list | CPatDelimiters of string * cases_pattern_expr | CPatCast of cases_pattern_expr * constr_expr -and cases_pattern_expr = cases_pattern_expr_r Loc.located +and cases_pattern_expr = cases_pattern_expr_r CAst.ast and cases_pattern_notation_substitution = cases_pattern_expr list * (** for constr subterms *) @@ -98,7 +98,7 @@ and constr_expr_r = | CGeneralization of binding_kind * abstraction_kind option * constr_expr | CPrim of prim_token | CDelimiters of string * constr_expr -and constr_expr = constr_expr_r Loc.located +and constr_expr = constr_expr_r CAst.ast and case_expr = constr_expr (* expression that is being matched *) * Name.t Loc.located option (* as-clause *) diff --git a/lib/cAst.ml b/lib/cAst.ml new file mode 100644 index 0000000000..5916c9ec12 --- /dev/null +++ b/lib/cAst.ml @@ -0,0 +1,24 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** The ast type contains generic metadata for AST nodes. *) +type 'a ast = { + v : 'a; + loc : Loc.t option; +} + +let make ?loc v = { v; loc } + +let map f n = { n with v = f n.v } +let map_with_loc f n = { n with v = f ?loc:n.loc n.v } +let map_from_loc f n = + let loc, v = Loc.to_pair n in + { v = f ?loc v ; loc } + +let with_val f n = f n.v +let with_loc_val f n = f ?loc:n.loc n.v diff --git a/lib/cAst.mli b/lib/cAst.mli new file mode 100644 index 0000000000..291536d123 --- /dev/null +++ b/lib/cAst.mli @@ -0,0 +1,22 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** The ast type contains generic metadata for AST nodes *) +type 'a ast = private { + v : 'a; + loc : Loc.t option; +} + +val make : ?loc:Loc.t -> 'a -> 'a ast + +val map : ('a -> 'b) -> 'a ast -> 'b ast +val map_with_loc : (?loc:Loc.t -> 'a -> 'b) -> 'a ast -> 'b ast +val map_from_loc : (?loc:Loc.t -> 'a -> 'b) -> 'a Loc.located -> 'b ast + +val with_val : ('a -> 'b) -> 'a ast -> 'b +val with_loc_val : (?loc:Loc.t -> 'a -> 'b) -> 'a ast -> 'b diff --git a/lib/clib.mllib b/lib/clib.mllib index c73ae9b904..9eb479fcc9 100644 --- a/lib/clib.mllib +++ b/lib/clib.mllib @@ -18,6 +18,7 @@ IStream Flags Control Loc +CAst CList CString Deque diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 49bf267db7..712d10a969 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -313,11 +313,11 @@ let interp_entry forpat e = match e with | ETBinderList (true, _) -> assert false | ETBinderList (false, tkl) -> TTAny (TTBinderListF tkl) -let constr_expr_of_name (loc,na) = Loc.tag ?loc @@ match na with +let constr_expr_of_name (loc,na) = CAst.make ?loc @@ match na with | Anonymous -> CHole (None,Misctypes.IntroAnonymous,None) | Name id -> CRef (Ident (Loc.tag ?loc id), None) -let cases_pattern_expr_of_name (loc,na) = Loc.tag ?loc @@ match na with +let cases_pattern_expr_of_name (loc,na) = CAst.make ?loc @@ match na with | Anonymous -> CPatAtom None | Name id -> CPatAtom (Some (Ident (Loc.tag ?loc id))) @@ -342,13 +342,13 @@ match e with | TTBinderListF _ -> { subst with binders = (List.flatten v, false) :: subst.binders } | TTBigint -> begin match forpat with - | ForConstr -> push_constr subst (Loc.tag @@ CPrim (Numeral v)) - | ForPattern -> push_constr subst (Loc.tag @@ CPatPrim (Numeral v)) + | ForConstr -> push_constr subst (CAst.make @@ CPrim (Numeral v)) + | ForPattern -> push_constr subst (CAst.make @@ CPatPrim (Numeral v)) end | TTReference -> begin match forpat with - | ForConstr -> push_constr subst (Loc.tag @@ CRef (v, None)) - | ForPattern -> push_constr subst (Loc.tag @@ CPatAtom (Some v)) + | ForConstr -> push_constr subst (CAst.make @@ CRef (v, None)) + | ForPattern -> push_constr subst (CAst.make @@ CPatAtom (Some v)) end | TTConstrList _ -> { subst with constrlists = v :: subst.constrlists } @@ -431,12 +431,12 @@ let rec pure_sublevels : type a b c. int option -> (a, b, c) rule -> int list = let make_act : type r. r target -> _ -> r gen_eval = function | ForConstr -> fun notation loc env -> let env = (env.constrs, env.constrlists, List.map fst env.binders) in - Loc.tag ~loc @@ CNotation (notation , env) + CAst.make ~loc @@ CNotation (notation , env) | ForPattern -> fun notation loc env -> let invalid = List.exists (fun (_, b) -> not b) env.binders in let () = if invalid then Topconstr.error_invalid_pattern_notation ~loc () in let env = (env.constrs, env.constrlists) in - Loc.tag ~loc @@ CPatNotation (notation, env, []) + CAst.make ~loc @@ CPatNotation (notation, env, []) let extend_constr state forpat ng = let n = ng.notgram_level in diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 45585d9ce7..a44aa5400c 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -34,11 +34,11 @@ let mk_cast = function (c,(_,None)) -> c | (c,(_,Some ty)) -> let loc = Loc.merge_opt (constr_loc c) (constr_loc ty) - in Loc.tag ?loc @@ CCast(c, CastConv ty) + in CAst.make ?loc @@ CCast(c, CastConv ty) let binder_of_name expl (loc,na) = CLocalAssum ([loc, na], Default expl, - Loc.tag ?loc @@ CHole (Some (Evar_kinds.BinderType na), IntroAnonymous, None)) + CAst.make ?loc @@ CHole (Some (Evar_kinds.BinderType na), IntroAnonymous, None)) let binders_of_names l = List.map (binder_of_name Explicit) l @@ -46,7 +46,7 @@ let binders_of_names l = let mk_fixb (id,bl,ann,body,(loc,tyc)) = let ty = match tyc with Some ty -> ty - | None -> Loc.tag @@ CHole (None, IntroAnonymous, None) in + | None -> CAst.make @@ CHole (None, IntroAnonymous, None) in (id,ann,bl,ty,body) let mk_cofixb (id,bl,ann,body,(loc,tyc)) = @@ -56,16 +56,16 @@ let mk_cofixb (id,bl,ann,body,(loc,tyc)) = (Pp.str"Annotation forbidden in cofix expression.")) (fst ann) in let ty = match tyc with Some ty -> ty - | None -> Loc.tag @@ CHole (None, IntroAnonymous, None) in + | None -> CAst.make @@ CHole (None, IntroAnonymous, None) in (id,bl,ty,body) let mk_fix(loc,kw,id,dcls) = if kw then let fb = List.map mk_fixb dcls in - Loc.tag ~loc @@ CFix(id,fb) + CAst.make ~loc @@ CFix(id,fb) else let fb = List.map mk_cofixb dcls in - Loc.tag ~loc @@ CCoFix(id,fb) + CAst.make ~loc @@ CCoFix(id,fb) let mk_single_fix (loc,kw,dcl) = let (id,_,_,_,_) = dcl in mk_fix(loc,kw,id,[dcl]) @@ -120,7 +120,7 @@ let name_colon = | _ -> err ()) | _ -> err ()) -let aliasvar = function loc, CPatAlias (_, id) -> Some (loc,Name id) | _ -> None +let aliasvar = function { CAst.loc = loc; CAst.v = CPatAlias (_, id) } -> Some (loc,Name id) | _ -> None GEXTEND Gram GLOBAL: binder_constr lconstr constr operconstr universe_level sort global @@ -159,62 +159,62 @@ GEXTEND Gram ; constr: [ [ c = operconstr LEVEL "8" -> c - | "@"; f=global; i = instance -> Loc.tag ~loc:!@loc @@ CAppExpl((None,f,i),[]) ] ] + | "@"; f=global; i = instance -> CAst.make ~loc:!@loc @@ CAppExpl((None,f,i),[]) ] ] ; operconstr: [ "200" RIGHTA [ c = binder_constr -> c ] | "100" RIGHTA [ c1 = operconstr; "<:"; c2 = binder_constr -> - Loc.tag ~loc:(!@loc) @@ CCast(c1, CastVM c2) + CAst.make ~loc:(!@loc) @@ CCast(c1, CastVM c2) | c1 = operconstr; "<:"; c2 = SELF -> - Loc.tag ~loc:(!@loc) @@ CCast(c1, CastVM c2) + CAst.make ~loc:(!@loc) @@ CCast(c1, CastVM c2) | c1 = operconstr; "<<:"; c2 = binder_constr -> - Loc.tag ~loc:(!@loc) @@ CCast(c1, CastNative c2) + CAst.make ~loc:(!@loc) @@ CCast(c1, CastNative c2) | c1 = operconstr; "<<:"; c2 = SELF -> - Loc.tag ~loc:(!@loc) @@ CCast(c1, CastNative c2) + CAst.make ~loc:(!@loc) @@ CCast(c1, CastNative c2) | c1 = operconstr; ":";c2 = binder_constr -> - Loc.tag ~loc:(!@loc) @@ CCast(c1, CastConv c2) + CAst.make ~loc:(!@loc) @@ CCast(c1, CastConv c2) | c1 = operconstr; ":"; c2 = SELF -> - Loc.tag ~loc:(!@loc) @@ CCast(c1, CastConv c2) + CAst.make ~loc:(!@loc) @@ CCast(c1, CastConv c2) | c1 = operconstr; ":>" -> - Loc.tag ~loc:(!@loc) @@ CCast(c1, CastCoerce) ] + CAst.make ~loc:(!@loc) @@ CCast(c1, CastCoerce) ] | "99" RIGHTA [ ] | "90" RIGHTA [ ] | "10" LEFTA - [ f=operconstr; args=LIST1 appl_arg -> Loc.tag ~loc:(!@loc) @@ CApp((None,f),args) - | "@"; f=global; i = instance; args=LIST0 NEXT -> Loc.tag ~loc:!@loc @@ CAppExpl((None,f,i),args) + [ f=operconstr; args=LIST1 appl_arg -> CAst.make ~loc:(!@loc) @@ CApp((None,f),args) + | "@"; f=global; i = instance; args=LIST0 NEXT -> CAst.make ~loc:!@loc @@ CAppExpl((None,f,i),args) | "@"; (locid,id) = pattern_identref; args=LIST1 identref -> - let args = List.map (fun x -> Loc.tag @@ CRef (Ident x,None), None) args in - Loc.tag ~loc:(!@loc) @@ CApp((None, Loc.tag ?loc:locid @@ CPatVar id),args) ] + let args = List.map (fun x -> CAst.make @@ CRef (Ident x,None), None) args in + CAst.make ~loc:(!@loc) @@ CApp((None, CAst.make ?loc:locid @@ CPatVar id),args) ] | "9" [ ".."; c = operconstr LEVEL "0"; ".." -> - Loc.tag ~loc:!@loc @@ CAppExpl ((None, Ident (Loc.tag ~loc:!@loc ldots_var),None),[c]) ] + CAst.make ~loc:!@loc @@ CAppExpl ((None, Ident (Loc.tag ~loc:!@loc ldots_var),None),[c]) ] | "8" [ ] | "1" LEFTA [ c=operconstr; ".("; f=global; args=LIST0 appl_arg; ")" -> - Loc.tag ~loc:(!@loc) @@ CApp((Some (List.length args+1), Loc.tag @@ CRef (f,None)),args@[c,None]) + CAst.make ~loc:(!@loc) @@ CApp((Some (List.length args+1), CAst.make @@ CRef (f,None)),args@[c,None]) | c=operconstr; ".("; "@"; f=global; args=LIST0 (operconstr LEVEL "9"); ")" -> - Loc.tag ~loc:(!@loc) @@ CAppExpl((Some (List.length args+1),f,None),args@[c]) - | c=operconstr; "%"; key=IDENT -> Loc.tag ~loc:(!@loc) @@ CDelimiters (key,c) ] + CAst.make ~loc:(!@loc) @@ CAppExpl((Some (List.length args+1),f,None),args@[c]) + | c=operconstr; "%"; key=IDENT -> CAst.make ~loc:(!@loc) @@ CDelimiters (key,c) ] | "0" [ c=atomic_constr -> c | c=match_constr -> c | "("; c = operconstr LEVEL "200"; ")" -> - (match snd c with + (match c.CAst.v with CPrim (Numeral z) when Bigint.is_pos_or_zero z -> - Loc.tag ~loc:(!@loc) @@ CNotation("( _ )",([c],[],[])) + CAst.make ~loc:(!@loc) @@ CNotation("( _ )",([c],[],[])) | _ -> c) | "{|"; c = record_declaration; "|}" -> c | "`{"; c = operconstr LEVEL "200"; "}" -> - Loc.tag ~loc:(!@loc) @@ CGeneralization (Implicit, None, c) + CAst.make ~loc:(!@loc) @@ CGeneralization (Implicit, None, c) | "`("; c = operconstr LEVEL "200"; ")" -> - Loc.tag ~loc:(!@loc) @@ CGeneralization (Explicit, None, c) + CAst.make ~loc:(!@loc) @@ CGeneralization (Explicit, None, c) ] ] ; record_declaration: - [ [ fs = record_fields -> Loc.tag ~loc:(!@loc) @@ CRecord fs ] ] + [ [ fs = record_fields -> CAst.make ~loc:(!@loc) @@ CRecord fs ] ] ; record_fields: @@ -236,40 +236,40 @@ GEXTEND Gram | "let"; id=name; bl = binders; ty = type_cstr; ":="; c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" -> let ty,c1 = match ty, c1 with - | (_,None), (_, CCast(c, CastConv t)) -> (Loc.tag ?loc:(constr_loc t) @@ Some t), c (* Tolerance, see G_vernac.def_body *) + | (_,None), { CAst.v = CCast(c, CastConv t) } -> (Loc.tag ?loc:(constr_loc t) @@ Some t), c (* Tolerance, see G_vernac.def_body *) | _, _ -> ty, c1 in - Loc.tag ~loc:!@loc @@ CLetIn(id,mkCLambdaN ?loc:(constr_loc c1) bl c1, + CAst.make ~loc:!@loc @@ CLetIn(id,mkCLambdaN ?loc:(constr_loc c1) bl c1, Option.map (mkCProdN ?loc:(fst ty) bl) (snd ty), c2) | "let"; fx = single_fix; "in"; c = operconstr LEVEL "200" -> let fixp = mk_single_fix fx in - let (li,id) = match snd fixp with + let (li,id) = match fixp.CAst.v with CFix(id,_) -> id | CCoFix(id,_) -> id | _ -> assert false in - Loc.tag ~loc:!@loc @@ CLetIn((li,Name id),fixp,None,c) + CAst.make ~loc:!@loc @@ CLetIn((li,Name id),fixp,None,c) | "let"; lb = ["("; l=LIST0 name SEP ","; ")" -> l | "()" -> []]; po = return_type; ":="; c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" -> - Loc.tag ~loc:!@loc @@ CLetTuple (lb,po,c1,c2) + CAst.make ~loc:!@loc @@ CLetTuple (lb,po,c1,c2) | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" -> - Loc.tag ~loc:!@loc @@ + CAst.make ~loc:!@loc @@ CCases (LetPatternStyle, None, [c1, None, None], [Loc.tag ~loc:!@loc ([(Loc.tag ~loc:!@loc [p])], c2)]) | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200"; rt = case_type; "in"; c2 = operconstr LEVEL "200" -> - Loc.tag ~loc:!@loc @@ + CAst.make ~loc:!@loc @@ CCases (LetPatternStyle, Some rt, [c1, aliasvar p, None], [Loc.tag ~loc:!@loc ([(Loc.tag ~loc:!@loc [p])], c2)]) | "let"; "'"; p=pattern; "in"; t = pattern LEVEL "200"; ":="; c1 = operconstr LEVEL "200"; rt = case_type; "in"; c2 = operconstr LEVEL "200" -> - Loc.tag ~loc:!@loc @@ + CAst.make ~loc:!@loc @@ CCases (LetPatternStyle, Some rt, [c1, aliasvar p, Some t], [Loc.tag ~loc:!@loc ([(Loc.tag ~loc:!@loc [p])], c2)]) | "if"; c=operconstr LEVEL "200"; po = return_type; "then"; b1=operconstr LEVEL "200"; "else"; b2=operconstr LEVEL "200" -> - Loc.tag ~loc:(!@loc) @@ CIf (c, po, b1, b2) + CAst.make ~loc:(!@loc) @@ CIf (c, po, b1, b2) | c=fix_constr -> c ] ] ; appl_arg: @@ -278,14 +278,14 @@ GEXTEND Gram | c=operconstr LEVEL "9" -> (c,None) ] ] ; atomic_constr: - [ [ g=global; i=instance -> Loc.tag ~loc:!@loc @@ CRef (g,i) - | s=sort -> Loc.tag ~loc:!@loc @@ CSort s - | n=INT -> Loc.tag ~loc:!@loc @@ CPrim (Numeral (Bigint.of_string n)) - | s=string -> Loc.tag ~loc:!@loc @@ CPrim (String s) - | "_" -> Loc.tag ~loc:!@loc @@ CHole (None, IntroAnonymous, None) - | "?"; "["; id=ident; "]" -> Loc.tag ~loc:!@loc @@ CHole (None, IntroIdentifier id, None) - | "?"; "["; id=pattern_ident; "]" -> Loc.tag ~loc:!@loc @@ CHole (None, IntroFresh id, None) - | id=pattern_ident; inst = evar_instance -> Loc.tag ~loc:!@loc @@ CEvar(id,inst) ] ] + [ [ g=global; i=instance -> CAst.make ~loc:!@loc @@ CRef (g,i) + | s=sort -> CAst.make ~loc:!@loc @@ CSort s + | n=INT -> CAst.make ~loc:!@loc @@ CPrim (Numeral (Bigint.of_string n)) + | s=string -> CAst.make ~loc:!@loc @@ CPrim (String s) + | "_" -> CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, None) + | "?"; "["; id=ident; "]" -> CAst.make ~loc:!@loc @@ CHole (None, IntroIdentifier id, None) + | "?"; "["; id=pattern_ident; "]" -> CAst.make ~loc:!@loc @@ CHole (None, IntroFresh id, None) + | id=pattern_ident; inst = evar_instance -> CAst.make ~loc:!@loc @@ CEvar(id,inst) ] ] ; inst: [ [ id = ident; ":="; c = lconstr -> (id,c) ] ] @@ -326,7 +326,7 @@ GEXTEND Gram ; match_constr: [ [ "match"; ci=LIST1 case_item SEP ","; ty=OPT case_type; "with"; - br=branches; "end" -> Loc.tag ~loc:!@loc @@ CCases(RegularStyle,ty,ci,br) ] ] + br=branches; "end" -> CAst.make ~loc:!@loc @@ CCases(RegularStyle,ty,ci,br) ] ] ; case_item: [ [ c=operconstr LEVEL "100"; @@ -368,46 +368,46 @@ GEXTEND Gram pattern: [ "200" RIGHTA [ ] | "100" RIGHTA - [ p = pattern; "|"; pl = LIST1 pattern SEP "|" -> Loc.tag ~loc:!@loc @@ CPatOr (p::pl) ] + [ p = pattern; "|"; pl = LIST1 pattern SEP "|" -> CAst.make ~loc:!@loc @@ CPatOr (p::pl) ] | "99" RIGHTA [ ] | "11" LEFTA [ p = pattern; "as"; id = ident -> - Loc.tag ~loc:!@loc @@ CPatAlias (p, id) ] + CAst.make ~loc:!@loc @@ CPatAlias (p, id) ] | "10" RIGHTA [ p = pattern; lp = LIST1 NEXT -> - (match p with - | _, CPatAtom (Some r) -> Loc.tag ~loc:!@loc @@ CPatCstr (r, None, lp) - | loc, CPatCstr (r, None, l2) -> + (let open CAst in match p with + | { v = CPatAtom (Some r) } -> CAst.make ~loc:!@loc @@ CPatCstr (r, None, lp) + | { v = CPatCstr (r, None, l2); loc } -> CErrors.user_err ?loc ~hdr:"compound_pattern" (Pp.str "Nested applications not supported.") - | _, CPatCstr (r, l1, l2) -> Loc.tag ~loc:!@loc @@ CPatCstr (r, l1 , l2@lp) - | _, CPatNotation (n, s, l) -> Loc.tag ~loc:!@loc @@ CPatNotation (n , s, l@lp) + | { v = CPatCstr (r, l1, l2) } -> CAst.make ~loc:!@loc @@ CPatCstr (r, l1 , l2@lp) + | { v = CPatNotation (n, s, l) } -> CAst.make ~loc:!@loc @@ CPatNotation (n , s, l@lp) | _ -> CErrors.user_err ?loc:(cases_pattern_expr_loc p) ~hdr:"compound_pattern" (Pp.str "Such pattern cannot have arguments.")) |"@"; r = Prim.reference; lp = LIST0 NEXT -> - Loc.tag ~loc:!@loc @@ CPatCstr (r, Some lp, []) ] + CAst.make ~loc:!@loc @@ CPatCstr (r, Some lp, []) ] | "1" LEFTA - [ c = pattern; "%"; key=IDENT -> Loc.tag ~loc:!@loc @@ CPatDelimiters (key,c) ] + [ c = pattern; "%"; key=IDENT -> CAst.make ~loc:!@loc @@ CPatDelimiters (key,c) ] | "0" - [ r = Prim.reference -> Loc.tag ~loc:!@loc @@ CPatAtom (Some r) - | "{|"; pat = record_patterns; "|}" -> Loc.tag ~loc:!@loc @@ CPatRecord pat - | "_" -> Loc.tag ~loc:!@loc @@ CPatAtom None + [ r = Prim.reference -> CAst.make ~loc:!@loc @@ CPatAtom (Some r) + | "{|"; pat = record_patterns; "|}" -> CAst.make ~loc:!@loc @@ CPatRecord pat + | "_" -> CAst.make ~loc:!@loc @@ CPatAtom None | "("; p = pattern LEVEL "200"; ")" -> - (match p with - | _, CPatPrim (Numeral z) when Bigint.is_pos_or_zero z -> - Loc.tag ~loc:!@loc @@ CPatNotation("( _ )",([p],[]),[]) + (match p.CAst.v with + | CPatPrim (Numeral z) when Bigint.is_pos_or_zero z -> + CAst.make ~loc:!@loc @@ CPatNotation("( _ )",([p],[]),[]) | _ -> p) | "("; p = pattern LEVEL "200"; ":"; ty = lconstr; ")" -> let p = match p with - | _, CPatPrim (Numeral z) when Bigint.is_pos_or_zero z -> - Loc.tag ~loc:!@loc @@ CPatNotation("( _ )",([p],[]),[]) + | { CAst.v = CPatPrim (Numeral z) } when Bigint.is_pos_or_zero z -> + CAst.make ~loc:!@loc @@ CPatNotation("( _ )",([p],[]),[]) | _ -> p in - Loc.tag ~loc:!@loc @@ CPatCast (p, ty) - | n = INT -> Loc.tag ~loc:!@loc @@ CPatPrim (Numeral (Bigint.of_string n)) - | s = string -> Loc.tag ~loc:!@loc @@ CPatPrim (String s) ] ] + CAst.make ~loc:!@loc @@ CPatCast (p, ty) + | n = INT -> CAst.make ~loc:!@loc @@ CPatPrim (Numeral (Bigint.of_string n)) + | s = string -> CAst.make ~loc:!@loc @@ CPatPrim (String s) ] ] ; impl_ident_tail: [ [ "}" -> binder_of_name Implicit @@ -415,7 +415,7 @@ GEXTEND Gram (fun na -> CLocalAssum (na::nal,Default Implicit,c)) | nal=LIST1 name; "}" -> (fun na -> CLocalAssum (na::nal,Default Implicit, - Loc.tag ?loc:(Loc.merge_opt (fst na) (Some !@loc)) @@ CHole (Some (Evar_kinds.BinderType (snd na)), IntroAnonymous, None))) + CAst.make ?loc:(Loc.merge_opt (fst na) (Some !@loc)) @@ CHole (Some (Evar_kinds.BinderType (snd na)), IntroAnonymous, None))) | ":"; c=lconstr; "}" -> (fun na -> CLocalAssum ([na],Default Implicit,c)) ] ] @@ -449,7 +449,7 @@ GEXTEND Gram binders_of_names (id::idl) @ bl | id1 = name; ".."; id2 = name -> [CLocalAssum ([id1;(Loc.tag ~loc:!@loc (Name ldots_var));id2], - Default Explicit, Loc.tag ~loc:!@loc @@ CHole (None, IntroAnonymous, None))] + Default Explicit, CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, None))] | bl = closed_binder; bl' = binders -> bl@bl' ] ] @@ -458,7 +458,7 @@ GEXTEND Gram [ [ l = LIST0 binder -> List.flatten l ] ] ; binder: - [ [ id = name -> [CLocalAssum ([id],Default Explicit, Loc.tag ~loc:!@loc @@ CHole (None, IntroAnonymous, None))] + [ [ id = name -> [CLocalAssum ([id],Default Explicit, CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, None))] | bl = closed_binder -> bl ] ] ; closed_binder: @@ -467,27 +467,27 @@ GEXTEND Gram | "("; id=name; ":"; c=lconstr; ")" -> [CLocalAssum ([id],Default Explicit,c)] | "("; id=name; ":="; c=lconstr; ")" -> - (match c with - | (_, CCast(c, CastConv t)) -> [CLocalDef (id,c,Some t)] + (match c.CAst.v with + | CCast(c, CastConv t) -> [CLocalDef (id,c,Some t)] | _ -> [CLocalDef (id,c,None)]) | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" -> [CLocalDef (id,c,Some t)] | "{"; id=name; "}" -> - [CLocalAssum ([id],Default Implicit, Loc.tag ~loc:!@loc @@ CHole (None, IntroAnonymous, None))] + [CLocalAssum ([id],Default Implicit, CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, None))] | "{"; id=name; idl=LIST1 name; ":"; c=lconstr; "}" -> [CLocalAssum (id::idl,Default Implicit,c)] | "{"; id=name; ":"; c=lconstr; "}" -> [CLocalAssum ([id],Default Implicit,c)] | "{"; id=name; idl=LIST1 name; "}" -> - List.map (fun id -> CLocalAssum ([id],Default Implicit, Loc.tag ~loc:!@loc @@ CHole (None, IntroAnonymous, None))) (id::idl) + List.map (fun id -> CLocalAssum ([id],Default Implicit, CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, None))) (id::idl) | "`("; tc = LIST1 typeclass_constraint SEP "," ; ")" -> List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Implicit, Explicit, b), t)) tc | "`{"; tc = LIST1 typeclass_constraint SEP "," ; "}" -> List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Implicit, Implicit, b), t)) tc | "'"; p = pattern LEVEL "0" -> let (p, ty) = - match p with - | _, CPatCast (p, ty) -> (p, Some ty) + match p.CAst.v with + | CPatCast (p, ty) -> (p, Some ty) | _ -> (p, None) in [CLocalPattern (Loc.tag ~loc:!@loc (p, ty))] diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 4889952012..ee0f06fe0e 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -120,7 +120,7 @@ GEXTEND Gram ; constr_body: [ [ ":="; c = lconstr -> c - | ":"; t = lconstr; ":="; c = lconstr -> Loc.tag ~loc:!@loc @@ CCast(c,CastConv t) ] ] + | ":"; t = lconstr; ":="; c = lconstr -> CAst.make ~loc:!@loc @@ CCast(c,CastConv t) ] ] ; mode: [ [ l = LIST1 [ "+" -> ModeInput diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index c8101875dc..27f879154e 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -233,14 +233,14 @@ GEXTEND Gram DefineBody ([], red, c, None) else (match c with - | _, CCast(c, CastConv t) -> DefineBody (bl, red, c, Some t) + | { CAst.v = CCast(c, CastConv t) } -> DefineBody (bl, red, c, Some t) | _ -> DefineBody (bl, red, c, None)) | bl = binders; ":"; t = lconstr; ":="; red = reduce; c = lconstr -> let ((bl, c), tyo) = if List.exists (function CLocalPattern _ -> true | _ -> false) bl then (* FIXME: "red" will be applied to types in bl and Cast with remain *) - let c = Loc.tag ~loc:!@loc @@ CCast (c, CastConv t) in + let c = CAst.make ~loc:!@loc @@ CCast (c, CastConv t) in (([],mkCLambdaN ~loc:!@loc bl c), None) else ((bl, c), Some t) in @@ -305,7 +305,7 @@ GEXTEND Gram ; type_cstr: [ [ ":"; c=lconstr -> c - | -> Loc.tag ~loc:!@loc @@ CHole (None, Misctypes.IntroAnonymous, None) ] ] + | -> CAst.make ~loc:!@loc @@ CHole (None, Misctypes.IntroAnonymous, None) ] ] ; (* Inductive schemes *) scheme: @@ -354,14 +354,14 @@ GEXTEND Gram t = lconstr; ":="; b = lconstr -> fun id -> (oc,DefExpr (id,mkCLambdaN ~loc:!@loc l b,Some (mkCProdN ~loc:!@loc l t))) | l = binders; ":="; b = lconstr -> fun id -> - match snd b with + match b.CAst.v with | CCast(b', (CastConv t|CastVM t|CastNative t)) -> (None,DefExpr(id,mkCLambdaN ~loc:!@loc l b',Some (mkCProdN ~loc:!@loc l t))) | _ -> (None,DefExpr(id,mkCLambdaN ~loc:!@loc l b,None)) ] ] ; record_binder: - [ [ id = name -> (None,AssumExpr(id, Loc.tag ~loc:!@loc @@ CHole (None, Misctypes.IntroAnonymous, None))) + [ [ id = name -> (None,AssumExpr(id, CAst.make ~loc:!@loc @@ CHole (None, Misctypes.IntroAnonymous, None))) | id = name; f = record_binder_body -> f id ] ] ; assum_list: @@ -380,7 +380,7 @@ GEXTEND Gram t= [ coe = of_type_with_opt_coercion; c = lconstr -> fun l id -> (not (Option.is_empty coe),(id,mkCProdN ~loc:!@loc l c)) | -> - fun l id -> (false,(id,mkCProdN ~loc:!@loc l (Loc.tag ~loc:!@loc @@ CHole (None, Misctypes.IntroAnonymous, None)))) ] + fun l id -> (false,(id,mkCProdN ~loc:!@loc l (CAst.make ~loc:!@loc @@ CHole (None, Misctypes.IntroAnonymous, None)))) ] -> t l ]] ; diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 48ab3dd57c..938fe52373 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1246,15 +1246,16 @@ let compute_params_name relnames (args : (Name.t * Glob_term.glob_constr * glob_ in List.rev !l -let rec rebuild_return_type (loc, rt) = - match rt with +let rec rebuild_return_type rt = + let loc = rt.CAst.loc in + match rt.CAst.v with | Constrexpr.CProdN(n,t') -> - Loc.tag ?loc @@ Constrexpr.CProdN(n,rebuild_return_type t') + CAst.make ?loc @@ Constrexpr.CProdN(n,rebuild_return_type t') | Constrexpr.CLetIn(na,v,t,t') -> - Loc.tag ?loc @@ Constrexpr.CLetIn(na,v,t,rebuild_return_type t') - | _ -> Loc.tag ?loc @@ Constrexpr.CProdN([[Loc.tag Anonymous], - Constrexpr.Default Decl_kinds.Explicit,Loc.tag ?loc rt], - Loc.tag @@ Constrexpr.CSort(GType [])) + CAst.make ?loc @@ Constrexpr.CLetIn(na,v,t,rebuild_return_type t') + | _ -> CAst.make ?loc @@ Constrexpr.CProdN([[Loc.tag Anonymous], + Constrexpr.Default Decl_kinds.Explicit, rt], + CAst.make @@ Constrexpr.CSort(GType [])) let do_build_inductive evd (funconstants: Term.pconstant list) (funsargs: (Name.t * glob_constr * glob_constr option) list list) @@ -1305,11 +1306,11 @@ let do_build_inductive (fun (n,t,typ) acc -> match typ with | Some typ -> - Loc.tag @@ Constrexpr.CLetIn((Loc.tag n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t, + CAst.make @@ Constrexpr.CLetIn((Loc.tag n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t, Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ), acc) | None -> - Loc.tag @@ Constrexpr.CProdN + CAst.make @@ Constrexpr.CProdN ([[(Loc.tag n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t], acc ) @@ -1372,11 +1373,11 @@ let do_build_inductive (fun (n,t,typ) acc -> match typ with | Some typ -> - Loc.tag @@ Constrexpr.CLetIn((Loc.tag n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t, + CAst.make @@ Constrexpr.CLetIn((Loc.tag n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t, Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ), acc) | None -> - Loc.tag @@ Constrexpr.CProdN + CAst.make @@ Constrexpr.CProdN ([[(Loc.tag n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t], acc ) diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 3dc16626ce..f4e9aa3720 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -469,7 +469,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas in let unbounded_eq = let f_app_args = - Loc.tag @@ Constrexpr.CAppExpl( + CAst.make @@ Constrexpr.CAppExpl( (None,(Ident (Loc.tag fname)),None) , (List.map (function @@ -480,7 +480,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas ) ) in - Loc.tag @@ Constrexpr.CApp ((None,Constrexpr_ops.mkRefC (Qualid (Loc.tag (qualid_of_string "Logic.eq")))), + CAst.make @@ Constrexpr.CApp ((None,Constrexpr_ops.mkRefC (Qualid (Loc.tag (qualid_of_string "Logic.eq")))), [(f_app_args,None);(body,None)]) in let eq = Constrexpr_ops.mkCProdN args unbounded_eq in @@ -588,12 +588,12 @@ let rec rebuild_bl (aux,assoc) bl typ = | [], _ -> (List.rev aux,replace_vars_constr_expr assoc typ,assoc) | (Constrexpr.CLocalAssum(nal,bk,_))::bl',typ -> rebuild_nal (aux,assoc) bk bl' nal (List.length nal) typ - | (Constrexpr.CLocalDef(na,_,_))::bl',(_loc, Constrexpr.CLetIn(_,nat,ty,typ')) -> + | (Constrexpr.CLocalDef(na,_,_))::bl',{ CAst.v = Constrexpr.CLetIn(_,nat,ty,typ') } -> rebuild_bl ((Constrexpr.CLocalDef(na,replace_vars_constr_expr assoc nat,Option.map (replace_vars_constr_expr assoc) ty (* ??? *))::aux),assoc) bl' typ' | _ -> assert false and rebuild_nal (aux,assoc) bk bl' nal lnal typ = - match nal, snd typ with + match nal, typ.CAst.v with | [], _ -> rebuild_bl (aux,assoc) bl' typ | _,CProdN([],typ) -> rebuild_nal (aux,assoc) bk bl' nal lnal typ | _,CProdN((nal',bk',nal't)::rest,typ') -> @@ -606,7 +606,7 @@ let rec rebuild_bl (aux,assoc) bl typ = rebuild_bl ((assum :: aux), nassoc) bl' (if List.is_empty new_nal' && List.is_empty rest then typ' - else Loc.tag @@ if List.is_empty new_nal' + else CAst.make @@ if List.is_empty new_nal' then CProdN(rest,typ') else CProdN(((new_nal',bk',nal't)::rest),typ')) else @@ -614,7 +614,7 @@ let rec rebuild_bl (aux,assoc) bl typ = let nassoc = make_assoc assoc nal' captured_nal in let assum = CLocalAssum(captured_nal,bk,replace_vars_constr_expr assoc nal't) in rebuild_nal ((assum :: aux), nassoc) - bk bl' non_captured_nal (lnal - lnal') (Loc.tag @@ CProdN(rest,typ')) + bk bl' non_captured_nal (lnal - lnal') (CAst.make @@ CProdN(rest,typ')) | _ -> assert false let rebuild_bl (aux,assoc) bl typ = rebuild_bl (aux,assoc) bl typ @@ -725,7 +725,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof in () -let rec add_args id new_args = Loc.map (function +let rec add_args id new_args = CAst.map (function | CRef (r,_) as b -> begin match r with | Libnames.Ident(loc,fname) when Id.equal fname id -> @@ -794,7 +794,7 @@ let rec chop_n_arrow n t = if n <= 0 then t (* If we have already removed all the arrows then return the type *) else (* If not we check the form of [t] *) - match snd t with + match t.CAst.v with | Constrexpr.CProdN(nal_ta',t') -> (* If we have a forall, to result are possible : either we need to discard more than the number of arrows contained in this product declaration then we just recall [chop_n_arrow] on @@ -813,7 +813,7 @@ let rec chop_n_arrow n t = then aux (n - nal_l) nal_ta' else - let new_t' = Loc.tag @@ + let new_t' = CAst.make @@ Constrexpr.CProdN( ((snd (List.chop n nal)),k,t'')::nal_ta',t') in @@ -829,7 +829,7 @@ let rec chop_n_arrow n t = let rec get_args b t : Constrexpr.local_binder_expr list * Constrexpr.constr_expr * Constrexpr.constr_expr = - match snd b with + match b.CAst.v with | Constrexpr.CLambdaN ((nal_ta), b') -> begin let n = @@ -869,7 +869,7 @@ let make_graph (f_ref:global_reference) = in let (nal_tas,b,t) = get_args extern_body extern_type in let expr_list = - match snd b with + match b.CAst.v with | Constrexpr.CFix(l_id,fixexprl) -> let l = List.map @@ -882,7 +882,7 @@ let make_graph (f_ref:global_reference) = | Constrexpr.CLocalDef (na,_,_)-> [] | Constrexpr.CLocalAssum (nal,_,_) -> List.map - (fun (loc,n) -> Loc.tag ?loc @@ + (fun (loc,n) -> CAst.make ?loc @@ CRef(Libnames.Ident(loc, Nameops.out_name n),None)) nal | Constrexpr.CLocalPattern _ -> assert false diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index f2654b5de8..5b51a213a1 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -73,7 +73,7 @@ let isVarf f x = in global environment. *) let ident_global_exist id = try - let ans = Loc.tag @@ CRef (Libnames.Ident (Loc.tag id), None) in + let ans = CAst.make @@ CRef (Libnames.Ident (Loc.tag id), None) in let _ = ignore (Constrintern.intern_constr (Global.env()) ans) in true with e when CErrors.noncritical e -> false @@ -835,7 +835,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) = let c = RelDecl.get_type decl in let typ = Constrextern.extern_constr false env Evd.empty c in let newenv = Environ.push_rel (LocalAssum (nm,c)) env in - Loc.tag @@ CProdN ([[(Loc.tag nm)],Constrexpr_ops.default_binder_kind,typ] , acc) , newenv) + CAst.make @@ CProdN ([[(Loc.tag nm)],Constrexpr_ops.default_binder_kind,typ] , acc) , newenv) (concl,Global.env()) (shift.funresprms2 @ shift.funresprms1 @ shift.args2 @ shift.args1 @ shift.otherprms2 @ shift.otherprms1) in diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index e20beae963..5fc22cb4ad 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -187,7 +187,7 @@ GEXTEND Gram (* Tactic arguments to the right of an application *) tactic_arg_compat: [ [ a = tactic_arg -> a - | c = Constr.constr -> (match c with _loc, CRef (r,None) -> Reference r | c -> ConstrMayEval (ConstrTerm c)) + | c = Constr.constr -> (match c with { CAst.v = CRef (r,None) } -> Reference r | c -> ConstrMayEval (ConstrTerm c)) (* Unambiguous entries: tolerated w/o "ltac:" modifier *) | "()" -> TacGeneric (genarg_of_unit ()) ] ] ; @@ -255,10 +255,10 @@ GEXTEND Gram let t, ty = match mpv with | Term t -> (match t with - | _loc, CCast (t, (CastConv ty | CastVM ty | CastNative ty)) -> Term t, Some (Term ty) + | { CAst.v = CCast (t, (CastConv ty | CastVM ty | CastNative ty)) } -> Term t, Some (Term ty) | _ -> mpv, None) | _ -> mpv, None - in Def (na, t, Option.default (Term (Loc.tag @@ CHole (None, IntroAnonymous, None))) ty) + in Def (na, t, Option.default (Term (CAst.make @@ CHole (None, IntroAnonymous, None))) ty) ] ] ; match_context_rule: @@ -353,7 +353,7 @@ GEXTEND Gram operconstr: LEVEL "0" [ [ IDENT "ltac"; ":"; "("; tac = Pltac.tactic_expr; ")" -> let arg = Genarg.in_gen (Genarg.rawwit Tacarg.wit_tactic) tac in - Loc.tag ~loc:!@loc @@ CHole (None, IntroAnonymous, Some arg) ] ] + CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, Some arg) ] ] ; END diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4 index 8aaad05666..60deb443a9 100644 --- a/plugins/ltac/g_tactic.ml4 +++ b/plugins/ltac/g_tactic.ml4 @@ -130,14 +130,14 @@ let mk_fix_tac (loc,id,bl,ann,ty) = (try List.index Names.Name.equal (snd x) ids with Not_found -> error "No such fix variable.") | _ -> error "Cannot guess decreasing argument of fix." in - (id,n, Loc.tag ~loc @@ CProdN(bl,ty)) + (id,n, CAst.make ~loc @@ CProdN(bl,ty)) let mk_cofix_tac (loc,id,bl,ann,ty) = let _ = Option.map (fun (aloc,_) -> user_err ~loc:aloc ~hdr:"Constr:mk_cofix_tac" (Pp.str"Annotation forbidden in cofix expression.")) ann in - (id,Loc.tag ~loc @@ CProdN(bl,ty)) + (id,CAst.make ~loc @@ CProdN(bl,ty)) (* Functions overloaded by quotifier *) let destruction_arg_of_constr (c,lbind as clbind) = match lbind with @@ -154,12 +154,12 @@ let mkTacCase with_evar = function (* Reinterpret numbers as a notation for terms *) | [(clear,ElimOnAnonHyp n),(None,None),None],None -> TacCase (with_evar, - (clear,(Loc.tag @@ CPrim (Numeral (Bigint.of_int n)), + (clear,(CAst.make @@ CPrim (Numeral (Bigint.of_int n)), NoBindings))) (* Reinterpret ident as notations for variables in the context *) (* because we don't know if they are quantified or not *) | [(clear,ElimOnIdent id),(None,None),None],None -> - TacCase (with_evar,(clear,(Loc.tag @@ CRef (Ident id,None),NoBindings))) + TacCase (with_evar,(clear,(CAst.make @@ CRef (Ident id,None),NoBindings))) | ic -> if List.exists (function ((_, ElimOnAnonHyp _),_,_) -> true | _ -> false) (fst ic) then @@ -169,7 +169,7 @@ let mkTacCase with_evar = function let rec mkCLambdaN_simple_loc ?loc bll c = match bll with | ((loc1,_)::_ as idl,bk,t) :: bll -> - Loc.tag ?loc @@ CLambdaN ([idl,bk,t],mkCLambdaN_simple_loc ?loc:(Loc.merge_opt loc1 loc) bll c) + CAst.make ?loc @@ CLambdaN ([idl,bk,t],mkCLambdaN_simple_loc ?loc:(Loc.merge_opt loc1 loc) bll c) | ([],_,_) :: bll -> mkCLambdaN_simple_loc ?loc bll c | [] -> c @@ -440,7 +440,7 @@ GEXTEND Gram | -> true ]] ; simple_binder: - [ [ na=name -> ([na],Default Explicit, Loc.tag ~loc:!@loc @@ CHole (Some (Evar_kinds.BinderType (snd na)), IntroAnonymous, None)) + [ [ na=name -> ([na],Default Explicit, CAst.make ~loc:!@loc @@ CHole (Some (Evar_kinds.BinderType (snd na)), IntroAnonymous, None)) | "("; nal=LIST1 name; ":"; c=lconstr; ")" -> (nal,Default Explicit,c) ] ] ; diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index bdafbdc78c..58473d7ddf 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -340,7 +340,7 @@ type 'a extra_genarg_printer = let strip_prod_binders_expr n ty = let rec strip_ty acc n ty = - match snd ty with + match ty.CAst.v with Constrexpr.CProdN(bll,a) -> let nb = List.fold_left (fun i (nal,_,_) -> i + List.length nal) 0 bll in diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 19c2eaf0a7..2ef435b6ba 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1787,18 +1787,18 @@ let rec strategy_of_ast = function (* By default the strategy for "rewrite_db" is top-down *) -let mkappc s l = Loc.tag @@ CAppExpl ((None,(Libnames.Ident (Loc.tag @@ Id.of_string s)),None),l) +let mkappc s l = CAst.make @@ CAppExpl ((None,(Libnames.Ident (Loc.tag @@ Id.of_string s)),None),l) let declare_an_instance n s args = (((Loc.tag @@ Name n),None), Explicit, - Loc.tag @@ CAppExpl ((None, Qualid (Loc.tag @@ qualid_of_string s),None), + CAst.make @@ CAppExpl ((None, Qualid (Loc.tag @@ qualid_of_string s),None), args)) let declare_instance a aeq n s = declare_an_instance n s [a;aeq] let anew_instance global binders instance fields = new_instance (Flags.is_universe_polymorphism ()) - binders instance (Some (true, Loc.tag @@ CRecord (fields))) + binders instance (Some (true, CAst.make @@ CRecord (fields))) ~global ~generalize:false ~refine:false Hints.empty_hint_info let declare_instance_refl global binders a aeq n lemma = @@ -1859,7 +1859,7 @@ let declare_relation ?(binders=[]) a aeq n refl symm trans = (Ident (Loc.tag @@ Id.of_string "Equivalence_Symmetric"), lemma2); (Ident (Loc.tag @@ Id.of_string "Equivalence_Transitive"), lemma3)]) -let cHole = Loc.tag @@ CHole (None, Misctypes.IntroAnonymous, None) +let cHole = CAst.make @@ CHole (None, Misctypes.IntroAnonymous, None) let proper_projection sigma r ty = let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i)) in @@ -2012,13 +2012,13 @@ let add_morphism glob binders m s n = let instance_id = add_suffix n "_Proper" in let instance = (((Loc.tag @@ Name instance_id),None), Explicit, - Loc.tag @@ CAppExpl ( + CAst.make @@ CAppExpl ( (None, Qualid (Loc.tag @@ Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper"),None), [cHole; s; m])) in let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in ignore(new_instance ~global:glob poly binders instance - (Some (true, Loc.tag @@ CRecord [])) + (Some (true, CAst.make @@ CRecord [])) ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info) (** Bind to "rewrite" too *) diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 44ea3ff1d6..566dd8ed7b 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -108,13 +108,13 @@ let intern_ltac_variable ist = function let intern_constr_reference strict ist = function | Ident (_,id) as r when not strict && find_hyp id ist -> - (Loc.tag @@ GVar id), Some (Loc.tag @@ CRef (r,None)) + (Loc.tag @@ GVar id), Some (CAst.make @@ CRef (r,None)) | Ident (_,id) as r when find_var id ist -> - (Loc.tag @@ GVar id), if strict then None else Some (Loc.tag @@ CRef (r,None)) + (Loc.tag @@ GVar id), if strict then None else Some (CAst.make @@ CRef (r,None)) | r -> let loc,_ as lqid = qualid_of_reference r in Loc.tag @@ GRef (locate_global_with_alias lqid,None), - if strict then None else Some (Loc.tag @@ CRef (r,None)) + if strict then None else Some (CAst.make @@ CRef (r,None)) let intern_move_location ist = function | MoveAfter id -> MoveAfter (intern_hyp ist id) @@ -271,7 +271,7 @@ let intern_destruction_arg ist = function | clear,ElimOnIdent (loc,id) -> if !strict_check then (* If in a defined tactic, no intros-until *) - match intern_constr ist (Loc.tag @@ CRef (Ident (Loc.tag id), None)) with + match intern_constr ist (CAst.make @@ CRef (Ident (Loc.tag id), None)) with | (loc, GVar id), _ -> clear,ElimOnIdent (loc,id) | c -> clear,ElimOnConstr (c,NoBindings) else @@ -361,7 +361,7 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) = Inr (bound_names,(c,None),dummy_pat) in (l, match p with | Inl r -> interp_ref r - | Inr (_, CAppExpl((None,r,None),[])) -> + | Inr { CAst.v = CAppExpl((None,r,None),[]) } -> (* We interpret similarly @ref and ref *) interp_ref (AN r) | Inr c -> diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 4d5b844550..449027b52e 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1072,7 +1072,7 @@ let interp_destruction_arg ist gl arg = if Tactics.is_quantified_hypothesis id gl then keep,ElimOnIdent (loc,id) else - let c = (Loc.tag ?loc @@ GVar id,Some (Loc.tag @@ CRef (Ident (loc,id),None))) in + let c = (Loc.tag ?loc @@ GVar id,Some (CAst.make @@ CRef (Ident (loc,id),None))) in let f = { delayed = fun env sigma -> let sigma = Sigma.to_evar_map sigma in let (sigma,c) = interp_open_constr ist env sigma c in diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 0bc3f502ca..c11c9f83b7 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -148,15 +148,15 @@ let add_genarg tag pr = (** Constructors for cast type *) let dC t = CastConv t (** Constructors for constr_expr *) -let isCVar = function _loc, CRef (Ident _, _) -> true | _ -> false -let destCVar = function _loc, CRef (Ident (_, id), _) -> id | _ -> +let isCVar = function { CAst.v = CRef (Ident _, _) } -> true | _ -> false +let destCVar = function { CAst.v = CRef (Ident (_, id), _) } -> id | _ -> CErrors.anomaly (str"not a CRef") -let mkCHole ~loc = Loc.tag ?loc @@ CHole (None, IntroAnonymous, None) -let mkCLambda ?loc name ty t = Loc.tag ?loc @@ +let mkCHole ~loc = CAst.make ?loc @@ CHole (None, IntroAnonymous, None) +let mkCLambda ?loc name ty t = CAst.make ?loc @@ CLambdaN ([[Loc.tag ?loc name], Default Explicit, ty], t) -let mkCLetIn ?loc name bo t = Loc.tag ?loc @@ +let mkCLetIn ?loc name bo t = CAst.make ?loc @@ CLetIn ((Loc.tag ?loc name), bo, None, t) -let mkCCast ?loc t ty = Loc.tag ?loc @@ CCast (t, dC ty) +let mkCCast ?loc t ty = CAst.make ?loc @@ CCast (t, dC ty) (** Constructors for rawconstr *) let mkRHole = Loc.tag @@ GHole (InternalHole, IntroAnonymous, None) let mkRApp f args = if args = [] then f else Loc.tag @@ GApp (f, args) @@ -951,7 +951,7 @@ let glob_cpattern gs p = | _, (_, None) as x -> x | k, (v, Some t) as orig -> if k = 'x' then glob_ssrterm gs ('(', (v, Some t)) else - match snd (Loc.to_pair t) with + match t.CAst.v with | CNotation("( _ in _ )", ([t1; t2], [], [])) -> (try match glob t1, glob t2 with | (r1, None), (r2, None) -> encode k "In" [r1;r2] @@ -1019,9 +1019,9 @@ let pr_rpattern = pr_pattern type pattern = Evd.evar_map * (constr, constr) ssrpattern -let id_of_cpattern = function - | _,(_,Some (_loc, CRef (Ident (_, x), _))) -> Some x - | _,(_,Some (_loc, CAppExpl ((_, Ident (_, x), _), []))) -> Some x +let id_of_cpattern = let open CAst in function + | _,(_,Some { v = CRef (Ident (_, x), _) } ) -> Some x + | _,(_,Some { v = CAppExpl ((_, Ident (_, x), _), []) } ) -> Some x | _,((_, GRef (VarRef x, _)) ,None) -> Some x | _ -> None let id_of_Cterm t = match id_of_cpattern t with @@ -1377,7 +1377,7 @@ let pf_fill_occ_term gl occ t = let cpattern_of_id id = ' ', (Loc.tag @@ GRef (VarRef id, None), None) let is_wildcard : cpattern -> bool = function - | _,(_,Some (_, CHole _)| (_, GHole _),None) -> true + | _,(_,Some { CAst.v = CHole _ } | (_, GHole _),None) -> true | _ -> false (* "ssrpattern" *) diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 900bf2dafd..1f3593a71a 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -217,7 +217,7 @@ let tag_var = tag Tag.variable | t -> cut () ++ str ":" ++ pr t let pr_opt_type_spc pr = function - | _loc, CHole (_,Misctypes.IntroAnonymous,_) -> mt () + | { CAst.v = CHole (_,Misctypes.IntroAnonymous,_) } -> mt () | t -> str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t let pr_lident (loc,id) = @@ -251,8 +251,8 @@ let tag_var = tag Tag.variable let lpator = 100 let lpatrec = 0 - let rec pr_patt sep inh (loc, p) = - let (strm,prec) = match p with + let rec pr_patt sep inh p = + let (strm,prec) = match CAst.(p.v) with | CPatRecord l -> let pp (c, p) = pr_reference c ++ spc() ++ str ":=" ++ pr_patt spc (lpatrec, Any) p @@ -300,7 +300,7 @@ let tag_var = tag Tag.variable | CPatCast _ -> assert false in - let loc = cases_pattern_expr_loc (loc, p) in + let loc = p.CAst.loc in pr_with_comments ?loc (sep() ++ if prec_less prec inh then strm else surround strm) @@ -353,7 +353,7 @@ let tag_var = tag Tag.variable end | Default b -> match t with - | _loc, CHole (_,Misctypes.IntroAnonymous,_) -> + | { CAst.v = CHole (_,Misctypes.IntroAnonymous,_) } -> let s = prlist_with_sep spc pr_lname nal in hov 1 (surround_implicit b s) | _ -> @@ -391,42 +391,42 @@ let tag_var = tag Tag.variable if is_open then pr_delimited_binders pr_com_at sep pr_c else pr_undelimited_binders sep pr_c - let rec extract_prod_binders = function + let rec extract_prod_binders = let open CAst in function (* | CLetIn (loc,na,b,c) as x -> let bl,c = extract_prod_binders c in if bl = [] then [], x else CLocalDef (na,b) :: bl, c*) - | _loc, CProdN ([],c) -> + | { v = CProdN ([],c) } -> extract_prod_binders c - | loc, CProdN ([[_,Name id],bk,t], - (_loc', CCases (LetPatternStyle,None, [(_loc'', CRef (Ident (_,id'),None)),None,None],[(_,([_,[p]],b))]))) + | { loc; v = CProdN ([[_,Name id],bk,t], + { v = CCases (LetPatternStyle,None, [{ v = CRef (Ident (_,id'),None)},None,None],[(_,([_,[p]],b))])} ) } when Id.equal id id' && not (Id.Set.mem id (Topconstr.free_vars_of_constr_expr b)) -> let bl,c = extract_prod_binders b in CLocalPattern (loc, (p,None)) :: bl, c - | loc, CProdN ((nal,bk,t)::bl,c) -> - let bl,c = extract_prod_binders (loc, CProdN(bl,c)) in + | { loc; v = CProdN ((nal,bk,t)::bl,c) } -> + let bl,c = extract_prod_binders (CAst.make ?loc @@ CProdN(bl,c)) in CLocalAssum (nal,bk,t) :: bl, c | c -> [], c - let rec extract_lam_binders (loc, ce) = match ce with + let rec extract_lam_binders ce = let open CAst in match ce.v with (* | CLetIn (loc,na,b,c) as x -> let bl,c = extract_lam_binders c in if bl = [] then [], x else CLocalDef (na,b) :: bl, c*) | CLambdaN ([],c) -> extract_lam_binders c | CLambdaN ([[_,Name id],bk,t], - (_loc, CCases (LetPatternStyle,None, [(_loc', CRef (Ident (_,id'),None)),None,None],[(_,([_,[p]],b))]))) + { v = CCases (LetPatternStyle,None, [{ v = CRef (Ident (_,id'),None)},None,None],[(_,([_,[p]],b))])} ) when Id.equal id id' && not (Id.Set.mem id (Topconstr.free_vars_of_constr_expr b)) -> let bl,c = extract_lam_binders b in - CLocalPattern (loc,(p,None)) :: bl, c + CLocalPattern (ce.loc,(p,None)) :: bl, c | CLambdaN ((nal,bk,t)::bl,c) -> - let bl,c = extract_lam_binders (loc, CLambdaN(bl,c)) in + let bl,c = extract_lam_binders (CAst.make ?loc:ce.loc @@ CLambdaN(bl,c)) in CLocalAssum (nal,bk,t) :: bl, c - | c -> [], Loc.tag ?loc c + | _ -> [], ce - let split_lambda = Loc.with_loc (fun ?loc -> function + let split_lambda = CAst.with_loc_val (fun ?loc -> function | CLambdaN ([[na],bk,t],c) -> (na,t,c) - | CLambdaN (([na],bk,t)::bl,c) -> (na,t,Loc.tag ?loc @@ CLambdaN(bl,c)) - | CLambdaN ((na::nal,bk,t)::bl,c) -> (na,t,Loc.tag ?loc @@ CLambdaN((nal,bk,t)::bl,c)) + | CLambdaN (([na],bk,t)::bl,c) -> (na,t, CAst.make ?loc @@ CLambdaN(bl,c)) + | CLambdaN ((na::nal,bk,t)::bl,c) -> (na,t, CAst.make ?loc @@ CLambdaN((nal,bk,t)::bl,c)) | _ -> anomaly (Pp.str "ill-formed fixpoint body") ) @@ -437,11 +437,11 @@ let tag_var = tag Tag.variable | (_,Name id), (_,Anonymous) -> (na,t,c) | _ -> (na',t,c) - let split_product na' = Loc.with_loc (fun ?loc -> function + let split_product na' = CAst.with_loc_val (fun ?loc -> function | CProdN ([[na],bk,t],c) -> rename na na' t c - | CProdN (([na],bk,t)::bl,c) -> rename na na' t (Loc.tag ?loc @@ CProdN(bl,c)) + | CProdN (([na],bk,t)::bl,c) -> rename na na' t (CAst.make ?loc @@ CProdN(bl,c)) | CProdN ((na::nal,bk,t)::bl,c) -> - rename na na' t (Loc.tag ?loc @@ CProdN((nal,bk,t)::bl,c)) + rename na na' t (CAst.make ?loc @@ CProdN((nal,bk,t)::bl,c)) | _ -> anomaly (Pp.str "ill-formed fixpoint body") ) @@ -509,7 +509,7 @@ let tag_var = tag Tag.variable let pr_case_type pr po = match po with - | None | Some (_, CHole (_,Misctypes.IntroAnonymous,_)) -> mt() + | None | Some { CAst.v = CHole (_,Misctypes.IntroAnonymous,_) } -> mt() | Some p -> spc() ++ hov 2 (keyword "return" ++ pr_sep_com spc (pr lsimpleconstr) p) @@ -546,7 +546,7 @@ let tag_var = tag Tag.variable let pr_fun_sep = spc () ++ str "=>" let pr_dangling_with_for sep pr inherited a = - match snd a with + match a.CAst.v with | (CFix (_,[_])|CCoFix(_,[_])) -> pr sep (latom,E) a | _ -> @@ -554,7 +554,7 @@ let tag_var = tag Tag.variable let pr pr sep inherited a = let return (cmds, prec) = (tag_constr_expr a cmds, prec) in - let (strm, prec) = match snd @@ Loc.to_pair a with + let (strm, prec) = match CAst.(a.v) with | CRef (r, us) -> return (pr_cref r us, latom) | CFix (id,fix) -> @@ -589,8 +589,8 @@ let tag_var = tag Tag.variable pr_fun_sep ++ pr spc ltop a), llambda ) - | CLetIn ((_,Name x), ((_loc, CFix((_,x'),[_])) - | (_loc, CCoFix((_,x'),[_])) as fx), t, b) + | CLetIn ((_,Name x), ({ CAst.v = CFix((_,x'),[_])} + | { CAst.v = CCoFix((_,x'),[_]) } as fx), t, b) when Id.equal x x' -> return ( hv 0 ( @@ -619,7 +619,7 @@ let tag_var = tag Tag.variable else return (p, lproj) | CAppExpl ((None,Ident (_,var),us),[t]) - | CApp ((_,(_, CRef(Ident(_,var),us))),[t,None]) + | CApp ((_, {CAst.v = CRef(Ident(_,var),us)}),[t,None]) when Id.equal var Notation_ops.ldots_var -> return ( hov 0 (str ".." ++ pr spc (latom,E) t ++ spc () ++ str ".."), @@ -755,7 +755,7 @@ let tag_var = tag Tag.variable let pr prec c = pr prec (transf (Global.env()) c) let pr_simpleconstr = function - | _lock, CAppExpl ((None,f,us),[]) -> str "@" ++ pr_cref f us + | { CAst.v = CAppExpl ((None,f,us),[]) } -> str "@" ++ pr_cref f us | c -> pr lsimpleconstr c let default_term_pr = { diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 5b6c5580ad..8928d83b09 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -252,7 +252,7 @@ open Decl_kinds prlist_strict (pr_module_vardecls pr_c) l let pr_type_option pr_c = function - | _loc, CHole (k, Misctypes.IntroAnonymous, _) -> mt() + | { CAst.v = CHole (k, Misctypes.IntroAnonymous, _) } -> mt() | _ as c -> brk(0,2) ++ str" :" ++ pr_c c let pr_decl_notation prc ((loc,ntn),c,scopt) = @@ -883,7 +883,7 @@ open Decl_kinds (match bk with Implicit -> str "! " | Explicit -> mt ()) ++ pr_constr cl ++ pr_hint_info pr_constr_pattern_expr info ++ (match props with - | Some (true, (_loc, CRecord l)) -> spc () ++ str":=" ++ spc () ++ str"{" ++ pr_record_body l ++ str "}" + | Some (true, { CAst.v = CRecord l}) -> spc () ++ str":=" ++ spc () ++ str"{" ++ pr_record_body l ++ str "}" | Some (true,_) -> assert false | Some (false,p) -> spc () ++ str":=" ++ spc () ++ pr_constr p | None -> mt())) diff --git a/vernac/classes.ml b/vernac/classes.ml index fb300dbc1d..f9a3b01b62 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -147,14 +147,14 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p (fun avoid (clname, _) -> match clname with | Some (cl, b) -> - let t = Loc.tag @@ CHole (None, Misctypes.IntroAnonymous, None) in + let t = CAst.make @@ CHole (None, Misctypes.IntroAnonymous, None) in t, avoid | None -> failwith ("new instance: under-applied typeclass")) cl | Explicit -> cl, Id.Set.empty in let tclass = - if generalize then Loc.tag @@ CGeneralization (Implicit, Some AbsPi, tclass) + if generalize then CAst.make @@ CGeneralization (Implicit, Some AbsPi, tclass) else tclass in let k, u, cty, ctx', ctx, len, imps, subst = @@ -217,7 +217,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p else ( let props = match props with - | Some (true, (_loc, CRecord fs)) -> + | Some (true, { CAst.v = CRecord fs }) -> if List.length fs > List.length k.cl_props then mismatched_props env' (List.map snd fs) k.cl_props; Some (Inl fs) @@ -261,7 +261,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p k.cl_projs; c :: props, rest' with Not_found -> - ((Loc.tag @@ CHole (None(* Some Evar_kinds.GoalEvar *), Misctypes.IntroAnonymous, None)) :: props), rest + ((CAst.make @@ CHole (None(* Some Evar_kinds.GoalEvar *), Misctypes.IntroAnonymous, None)) :: props), rest else props, rest) ([], props) k.cl_props in diff --git a/vernac/command.ml b/vernac/command.ml index 82d7b19d7a..12df344c23 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -53,7 +53,7 @@ let rec under_binders env sigma f n c = mkLetIn (x,b,t,under_binders (push_rel (LocalDef (x,b,t)) env) sigma f (n-1) c) | _ -> assert false -let rec complete_conclusion a cs = Loc.map_with_loc (fun ?loc -> function +let rec complete_conclusion a cs = CAst.map_with_loc (fun ?loc -> function | CProdN (bl,c) -> CProdN (bl,complete_conclusion a cs c) | CLetIn (na,b,t,c) -> CLetIn (na,b,t,complete_conclusion a cs c) | CHole (k, _, _) -> @@ -62,7 +62,7 @@ let rec complete_conclusion a cs = Loc.map_with_loc (fun ?loc -> function user_err ?loc (strbrk"Cannot infer the non constant arguments of the conclusion of " ++ pr_id cs ++ str "."); - let args = List.map (fun id -> Loc.tag ?loc @@ CRef(Ident(loc,id),None)) params in + let args = List.map (fun id -> CAst.make ?loc @@ CRef(Ident(loc,id),None)) params in CAppExpl ((None,Ident(loc,name),None),List.rev args) | c -> c ) @@ -683,7 +683,7 @@ let extract_params indl = let extract_inductive indl = List.map (fun (((_,indname),pl),_,ar,lc) -> { ind_name = indname; ind_univs = pl; - ind_arity = Option.cata (fun x -> x) (Loc.tag @@ CSort (GType [])) ar; + ind_arity = Option.cata (fun x -> x) (CAst.make @@ CSort (GType [])) ar; ind_lc = List.map (fun (_,((_,id),t)) -> (id,t)) lc }) indl @@ -1354,7 +1354,7 @@ let do_program_fixpoint local poly l = | [(n, CMeasureRec (m, r))], [((((_,id),pl),_,bl,typ,def),ntn)] -> build_wellfounded (id, pl, n, bl, typ, out_def def) poly - (Option.default (Loc.tag @@ CRef (lt_ref,None)) r) m ntn + (Option.default (CAst.make @@ CRef (lt_ref,None)) r) m ntn | _, _ when List.for_all (fun (n, ro) -> ro == CStructRec) g -> let fixl,ntns = extract_fixpoint_components true l in diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index feacfe915d..83896992c5 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -1416,7 +1416,7 @@ let add_notation_extra_printing_rule df k v = (* Infix notations *) -let inject_var x = Loc.tag @@ CRef (Ident (Loc.tag @@ Id.of_string x),None) +let inject_var x = CAst.make @@ CRef (Ident (Loc.tag @@ Id.of_string x),None) let add_infix local ((loc,inf),modifiers) pr sc = check_infix_modifiers modifiers; @@ -1477,7 +1477,7 @@ let add_class_scope scope cl = (* Check if abbreviation to a name and avoid early insertion of maximal implicit arguments *) let try_interp_name_alias = function - | [], (_loc, CRef (ref,_)) -> intern_reference ref + | [], { CAst.v = CRef (ref,_) } -> intern_reference ref | _ -> raise Not_found let add_syntactic_definition ident (vars,c) local onlyparse = diff --git a/vernac/record.ml b/vernac/record.ml index 8bd583b81f..43a24e167c 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -94,7 +94,7 @@ let compute_constructor_level evars env l = let binder_of_decl = function | Vernacexpr.AssumExpr(n,t) -> (n,None,t) | Vernacexpr.DefExpr(n,c,t) -> (n,Some c, match t with Some c -> c - | None -> Loc.tag ?loc:(fst n) @@ CHole (None, Misctypes.IntroAnonymous, None)) + | None -> CAst.make ?loc:(fst n) @@ CHole (None, Misctypes.IntroAnonymous, None)) let binders_of_decls = List.map binder_of_decl @@ -121,8 +121,8 @@ let typecheck_params_and_fields def id pl t ps nots fs = | Some t -> let env = push_rel_context newps env0 in let poly = - match snd t with - | CSort (Misctypes.GType []) -> true | _ -> false in + match t with + | { CAst.v = CSort (Misctypes.GType []) } -> true | _ -> false in let s = interp_type_evars env evars ~impls:empty_internalization_env t in let sred = Reductionops.whd_all env !evars s in let s = EConstr.Unsafe.to_constr s in |