From ee2197096fe75a63b4d92cb3a1bb05122c5c625b Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 9 Apr 2017 03:35:20 +0200 Subject: [location] [ast] Port module AST to CAst --- interp/constrextern.ml | 83 +++++++------- interp/constrintern.ml | 167 +++++++++++++-------------- interp/implicit_quantifiers.ml | 4 +- interp/modintern.ml | 8 +- interp/notation.ml | 18 +-- interp/notation_ops.ml | 195 ++++++++++++++++---------------- intf/constrexpr.mli | 2 +- intf/glob_term.mli | 6 +- parsing/g_vernac.ml4 | 10 +- plugins/funind/glob_term_to_relation.ml | 84 +++++++------- plugins/funind/glob_termops.ml | 146 ++++++++++++------------ plugins/funind/indfun.ml | 2 +- plugins/funind/indfun_common.ml | 4 +- plugins/funind/merge.ml | 42 +++---- plugins/funind/recdef.ml | 10 +- plugins/ltac/extratactics.ml4 | 8 +- plugins/ltac/g_rewrite.ml4 | 2 +- plugins/ltac/pptactic.ml | 2 +- plugins/ltac/tacintern.ml | 10 +- plugins/ltac/tacinterp.ml | 4 +- plugins/setoid_ring/newring.ml | 2 +- plugins/ssrmatching/ssrmatching.ml4 | 33 +++--- plugins/syntax/ascii_syntax.ml | 12 +- plugins/syntax/nat_syntax.ml | 12 +- plugins/syntax/numbers_syntax.ml | 64 +++++------ plugins/syntax/r_syntax.ml | 32 +++--- plugins/syntax/string_syntax.ml | 12 +- plugins/syntax/z_syntax.ml | 59 +++++----- pretyping/cases.ml | 79 ++++++------- pretyping/coercion.ml | 4 +- pretyping/detyping.ml | 110 +++++++++--------- pretyping/detyping.mli | 8 -- pretyping/glob_ops.ml | 52 ++++----- pretyping/patternops.ml | 20 ++-- pretyping/pretyping.ml | 7 +- printing/ppvernac.ml | 10 +- tactics/hipattern.ml | 14 +-- vernac/command.ml | 2 +- 38 files changed, 673 insertions(+), 666 deletions(-) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index e8a5b5265..692a0872b 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -17,6 +17,7 @@ open Termops open Libnames open Globnames open Impargs +open CAst open Constrexpr open Constrexpr_ops open Notation_ops @@ -182,7 +183,7 @@ let add_patt_for_params ind l = let add_cpatt_for_params ind l = if !Flags.in_debugger then l else - Util.List.addn (Inductiveops.inductive_nparamdecls ind) (Loc.tag @@ PatVar Anonymous) l + Util.List.addn (Inductiveops.inductive_nparamdecls ind) (CAst.make @@ PatVar Anonymous) l let drop_implicits_in_patt cst nb_expl args = let impl_st = (implicits_of_global cst) in @@ -291,7 +292,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = (* pboutill: There are letins in pat which is incompatible with notations and not explicit application. *) match pat with - | loc, PatCstr(cstrsp,args,na) + | { loc; v = PatCstr(cstrsp,args,na) } 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 @@ -311,10 +312,10 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = extern_notation_pattern scopes vars pat (uninterp_cases_pattern_notations pat) with No_match -> - match pat with - | 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) -> + CAst.map_with_loc (fun ?loc -> function + | PatVar (Name id) -> CPatAtom (Some (Ident (loc,id))) + | PatVar (Anonymous) -> CPatAtom None + | PatCstr(cstrsp,args,na) -> let args = List.map (extern_cases_pattern_in_scope scopes vars) args in let p = try @@ -337,20 +338,21 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = | head :: tail -> ip q tail ((extern_reference ?loc Id.Set.empty (ConstRef c), head) :: acc) in - CAst.make ?loc @@ CPatRecord(List.rev (ip projs args [])) + 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 CAst.make ?loc @@ CPatCstr (c, None, args) - else CAst.make ?loc @@ CPatCstr (c, Some (add_patt_for_params (fst cstrsp) args), []) + then CPatCstr (c, None, args) + else 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 -> CAst.make ?loc @@ CPatCstr (c, None, true_args) - | None -> CAst.make ?loc @@ CPatCstr (c, Some full_args, []) - in insert_pat_alias ?loc p na + | Some true_args -> CPatCstr (c, None, true_args) + | None -> CPatCstr (c, Some full_args, []) + in (insert_pat_alias ?loc (CAst.make ?loc p) na).v + ) pat and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) (tmp_scope, scopes as allscopes) vars = function @@ -396,20 +398,21 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) in assert (List.is_empty substlist); mkPat ?loc qid (List.rev_append l1 l2') -and extern_notation_pattern (tmp_scope,scopes as allscopes) vars (loc, t) = function +and extern_notation_pattern (tmp_scope,scopes as allscopes) vars t = function | [] -> raise No_match | (keyrule,pat,n as _rule)::rules -> try if List.mem keyrule !print_non_active_notations then raise No_match; - match t with + let loc = t.loc in + match t.v with | PatCstr (cstr,_,na) -> let p = apply_notation_to_pattern ?loc (ConstructRef cstr) - (match_notation_constr_cases_pattern (loc, t) pat) allscopes vars keyrule in + (match_notation_constr_cases_pattern t pat) allscopes vars keyrule in insert_pat_alias ?loc p na | 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 + No_match -> extern_notation_pattern allscopes vars t rules let rec extern_notation_ind_pattern allscopes vars ind args = function | [] -> raise No_match @@ -565,7 +568,7 @@ let extern_args extern env args = List.map map args let match_coercion_app = function - | (loc, GApp ((_, GRef (r,_)),args)) -> Some (loc, r, 0, args) + | {loc; v = GApp ({ v = GRef (r,_) },args)} -> Some (loc, r, 0, args) | _ -> None let rec remove_coercions inctx c = @@ -587,13 +590,13 @@ let rec remove_coercions inctx c = been confused with ordinary application or would have need a surrounding context and the coercion to funclass would have been made explicit to match *) - if List.is_empty l then a' else Loc.tag ?loc @@ GApp (a',l) + if List.is_empty l then a' else CAst.make ?loc @@ GApp (a',l) | _ -> c with Not_found -> c) | _ -> c let rec flatten_application = function - | (loc, GApp ((_, GApp(a,l')),l)) -> flatten_application (Loc.tag ?loc @@ GApp (a,l'@l)) + | {loc; v = GApp ({ v = GApp(a,l')},l)} -> flatten_application (CAst.make ?loc @@ GApp (a,l'@l)) | a -> a (**********************************************************************) @@ -621,10 +624,10 @@ let extern_optimal_prim_token scopes r r' = let extended_glob_local_binder_of_decl loc = function | (p,bk,None,t) -> GLocalAssum (p,bk,t) - | (p,bk,Some x,(_,GHole ( _, Misctypes.IntroAnonymous, None))) -> GLocalDef (p,bk,x,None) + | (p,bk,Some x, { v = GHole ( _, Misctypes.IntroAnonymous, None) } ) -> GLocalDef (p,bk,x,None) | (p,bk,Some x,t) -> GLocalDef (p,bk,x,Some t) -let extended_glob_local_binder_of_decl ?loc u = Loc.tag ?loc (extended_glob_local_binder_of_decl loc u) +let extended_glob_local_binder_of_decl ?loc u = CAst.make ?loc (extended_glob_local_binder_of_decl loc u) (**********************************************************************) (* mapping glob_constr to constr_expr *) @@ -649,7 +652,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 -> CAst.map_from_loc (fun ?loc -> function + with No_match -> CAst.map_with_loc (fun ?loc -> function | GRef (ref,us) -> extern_global (select_stronger_impargs (implicits_of_global ref)) (extern_reference ?loc vars ref) (extern_universes us) @@ -667,7 +670,7 @@ let rec extern inctx scopes vars r = | GApp (f,args) -> (match f with - | (rloc, GRef (ref,us)) -> + | {loc = rloc; v = GRef (ref,us) } -> let subscopes = find_arguments_scope ref in let args = fill_arg_scopes args subscopes (snd scopes) in begin @@ -743,7 +746,7 @@ let rec extern inctx scopes vars r = let rtntypopt' = Option.map (extern_typ scopes vars') rtntypopt in let tml = List.map (fun (tm,(na,x)) -> let na' = match na,tm with - | Anonymous, (_, GVar id) -> + | Anonymous, { v = GVar id } -> begin match rtntypopt with | None -> None | Some ntn -> @@ -752,12 +755,12 @@ let rec extern inctx scopes vars r = else None end | Anonymous, _ -> None - | Name id, (_, GVar id') when Id.equal id id' -> None + | Name id, { v = GVar id' } when Id.equal id id' -> None | Name _, _ -> Some (Loc.tag na) in (sub_extern false scopes vars tm, na', Option.map (fun (loc,(ind,nal)) -> - let args = List.map (fun x -> Loc.tag @@ PatVar x) nal in + let args = List.map (fun x -> CAst.make @@ PatVar x) nal in let fullargs = add_cpatt_for_params ind args in extern_ind_pattern_in_scope scopes vars ind fullargs ) x)) @@ -848,14 +851,14 @@ and factorize_lambda inctx scopes vars na bk aty c = and extern_local_binder scopes vars = function [] -> ([],[],[]) - | (_, GLocalDef (na,bk,bd,ty))::l -> + | { v = GLocalDef (na,bk,bd,ty)}::l -> let (assums,ids,l) = extern_local_binder scopes (name_fold Id.Set.add na vars) l in (assums,na::ids, CLocalDef((Loc.tag na), extern false scopes vars bd, Option.map (extern false scopes vars) ty) :: l) - | (_, GLocalAssum (na,bk,ty))::l -> + | { v = GLocalAssum (na,bk,ty)}::l -> let ty = extern_typ scopes vars ty in (match extern_local_binder scopes (name_fold Id.Set.add na vars) l with (assums,ids,CLocalAssum(nal,k,ty')::l) @@ -868,7 +871,7 @@ and extern_local_binder scopes vars = function (na::assums,na::ids, CLocalAssum([(Loc.tag na)],Default bk,ty) :: l)) - | (_, GLocalPattern ((p,_),_,bk,ty))::l -> + | { v = GLocalPattern ((p,_),_,bk,ty)}::l -> let ty = if !Flags.raw_print then Some (extern_typ scopes vars ty) else None in let p = extern_cases_pattern vars p in @@ -886,12 +889,12 @@ and extern_notation (tmp_scope,scopes as allscopes) vars t = function try if List.mem keyrule !print_non_active_notations then raise No_match; (* Adjusts to the number of arguments expected by the notation *) - let (t,args,argsscopes,argsimpls) = match snd t,n with + let (t,args,argsscopes,argsimpls) = match t.v ,n with | GApp (f,args), Some n when List.length args >= n -> let args1, args2 = List.chop n args in let subscopes, impls = - match snd f with + match f.v with | GRef (ref,us) -> let subscopes = try List.skipn n (find_arguments_scope ref) @@ -904,15 +907,15 @@ and extern_notation (tmp_scope,scopes as allscopes) vars t = function subscopes,impls | _ -> [], [] in - (if Int.equal n 0 then f else Loc.tag @@ GApp (f,args1)), + (if Int.equal n 0 then f else CAst.make @@ GApp (f,args1)), args2, subscopes, impls - | GApp ((_, GRef (ref,us) as f),args), None -> + | GApp ({ v = GRef (ref,us) } as f, args), None -> let subscopes = find_arguments_scope ref in let impls = select_impargs_size (List.length args) (implicits_of_global ref) in f, args, subscopes, impls - | GRef (ref,us), Some 0 -> Loc.tag @@ GApp (t,[]), [], [], [] + | GRef (ref,us), Some 0 -> CAst.make @@ GApp (t,[]), [], [], [] | _, None -> t, [], [], [] | _ -> raise No_match in (* Try matching ... *) @@ -1014,9 +1017,9 @@ let extern_closed_glob ?lax goal_concl_style env sigma t = let any_any_branch = (* | _ => _ *) - Loc.tag ([],[Loc.tag @@ PatVar Anonymous], Loc.tag @@ GHole (Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None)) + Loc.tag ([],[CAst.make @@ PatVar Anonymous], CAst.make @@ GHole (Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None)) -let rec glob_of_pat env sigma pat = Loc.tag @@ match pat with +let rec glob_of_pat env sigma pat = CAst.make @@ match pat with | PRef ref -> GRef (ref,None) | PVar id -> GVar id | PEvar (evk,l) -> @@ -1036,12 +1039,12 @@ let rec glob_of_pat env sigma pat = Loc.tag @@ match pat with GVar id | PMeta None -> GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous,None) | PMeta (Some n) -> GPatVar (false,n) - | PProj (p,c) -> GApp (Loc.tag @@ GRef (ConstRef (Projection.constant p),None), + | PProj (p,c) -> GApp (CAst.make @@ GRef (ConstRef (Projection.constant p),None), [glob_of_pat env sigma c]) | PApp (f,args) -> GApp (glob_of_pat env sigma f,Array.map_to_list (glob_of_pat env sigma) args) | PSoApp (n,args) -> - GApp (Loc.tag @@ GPatVar (true,n), + GApp (CAst.make @@ GPatVar (true,n), List.map (glob_of_pat env sigma) args) | PProd (na,t,c) -> GProd (na,Explicit,glob_of_pat env sigma t,glob_of_pat (na::env) sigma c) @@ -1073,8 +1076,8 @@ let rec glob_of_pat env sigma pat = Loc.tag @@ match pat with | _ -> anomaly (Pp.str "PCase with non-trivial predicate but unknown inductive") in GCases (RegularStyle,rtn,[glob_of_pat env sigma tm,indnames],mat) - | PFix f -> Loc.obj @@ Detyping.detype_names false [] env (Global.env()) sigma (EConstr.of_constr (mkFix f)) (** FIXME bad env *) - | PCoFix c -> Loc.obj @@ Detyping.detype_names false [] env (Global.env()) sigma (EConstr.of_constr (mkCoFix c)) + | PFix f -> (Detyping.detype_names false [] env (Global.env()) sigma (EConstr.of_constr (mkFix f))).v (** FIXME bad env *) + | PCoFix c -> (Detyping.detype_names false [] env (Global.env()) sigma (EConstr.of_constr (mkCoFix c))).v | PSort s -> GSort s let extern_constr_pattern env sigma pat = diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 541b52972..bd7c05e6f 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -15,6 +15,7 @@ open Namegen open Libnames open Globnames open Impargs +open CAst open Glob_term open Glob_ops open Patternops @@ -304,12 +305,12 @@ let reset_tmp_scope env = {env with tmp_scope = None} let rec it_mkGProd ?loc env body = match env with - (loc2, (na, bk, t)) :: tl -> it_mkGProd ?loc:loc2 tl (Loc.tag ?loc:(Loc.merge_opt loc loc2) @@ GProd (na, bk, t, body)) + (loc2, (na, bk, t)) :: tl -> it_mkGProd ?loc:loc2 tl (CAst.make ?loc:(Loc.merge_opt loc loc2) @@ GProd (na, bk, t, body)) | [] -> body let rec it_mkGLambda ?loc env body = match env with - (loc2, (na, bk, t)) :: tl -> it_mkGLambda ?loc:loc2 tl (Loc.tag ?loc:(Loc.merge_opt loc loc2) @@ GLambda (na, bk, t, body)) + (loc2, (na, bk, t)) :: tl -> it_mkGLambda ?loc:loc2 tl (CAst.make ?loc:(Loc.merge_opt loc loc2) @@ GLambda (na, bk, t, body)) | [] -> body (**********************************************************************) @@ -322,14 +323,14 @@ let build_impls = function let impls_type_list ?(args = []) = let rec aux acc = function - |_, GProd (na,bk,_,c) -> aux ((build_impls bk na)::acc) c - |_ -> (Variable,[],List.append args (List.rev acc),[]) + | { v = GProd (na,bk,_,c) } -> aux ((build_impls bk na)::acc) c + | _ -> (Variable,[],List.append args (List.rev acc),[]) in aux [] let impls_term_list ?(args = []) = let rec aux acc = function - |_, GLambda (na,bk,_,c) -> aux ((build_impls bk na)::acc) c - |_, GRec (fix_kind, nas, args, tys, bds) -> + | { v = GLambda (na,bk,_,c) } -> aux ((build_impls bk na)::acc) c + | { v = GRec (fix_kind, nas, args, tys, bds) } -> let nb = match fix_kind with |GFix (_, n) -> n | GCoFix n -> n in let acc' = List.fold_left (fun a (na, bk, _, _) -> (build_impls bk na)::a) acc args.(nb) in aux acc' bds.(nb) @@ -346,12 +347,12 @@ let rec check_capture ty = function () let locate_if_hole ?loc na = function - | _, GHole (_,naming,arg) -> + | { v = GHole (_,naming,arg) } -> (try match na with | Name id -> glob_constr_of_notation_constr ?loc (Reserve.find_reserved_type id) | Anonymous -> raise Not_found - with Not_found -> Loc.tag ?loc @@ GHole (Evar_kinds.BinderType na, naming, arg)) + with Not_found -> CAst.make ?loc @@ GHole (Evar_kinds.BinderType na, naming, arg)) | x -> x let reset_hidden_inductive_implicit_test env = @@ -397,7 +398,7 @@ let intern_generalized_binder ?(global_level=false) intern_type lvar env fvs in let bl = List.map (fun (loc, id) -> - (loc, (Name id, b, Loc.tag ?loc @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None)))) + (loc, (Name id, b, CAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None)))) fvs in let na = match na with @@ -454,11 +455,11 @@ let intern_local_pattern intern lvar env p = env) env (free_vars_of_pat [] p) -let glob_local_binder_of_extended = Loc.with_loc (fun ?loc -> function +let glob_local_binder_of_extended = CAst.with_loc_val (fun ?loc -> function | GLocalAssum (na,bk,t) -> (na,bk,None,t) | GLocalDef (na,bk,c,Some t) -> (na,bk,Some c,t) | GLocalDef (na,bk,c,None) -> - let t = Loc.tag ?loc @@ GHole(Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None) in + let t = CAst.make ?loc @@ GHole(Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None) in (na,bk,Some c,t) | GLocalPattern (_,_,_,_) -> Loc.raise ?loc (Stream.Error "pattern with quote not allowed here.") @@ -469,13 +470,13 @@ let intern_cases_pattern_fwd = ref (fun _ -> failwith "intern_cases_pattern_fwd" let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = function | CLocalAssum(nal,bk,ty) -> let env, bl' = intern_assumption intern lvar env nal bk ty in - let bl' = List.map (fun (loc,(na,c,t)) -> Loc.tag ?loc @@ GLocalAssum (na,c,t)) bl' in + let bl' = List.map (fun (loc,(na,c,t)) -> CAst.make ?loc @@ GLocalAssum (na,c,t)) bl' in env, bl' @ bl | CLocalDef((loc,na as locna),def,ty) -> let term = intern env def in let ty = Option.map (intern env) ty in (push_name_env lvar (impls_term_list term) env locna, - (Loc.tag ?loc @@ GLocalDef (na,Explicit,term,ty)) :: bl) + (CAst.make ?loc @@ GLocalDef (na,Explicit,term,ty)) :: bl) | CLocalPattern (loc,(p,ty)) -> let tyc = match ty with @@ -495,7 +496,7 @@ let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = functio let bk = Default Explicit in let _, bl' = intern_assumption intern lvar env [na] bk tyc in let _,(_,bk,t) = List.hd bl' in - (env, (Loc.tag ?loc @@ GLocalPattern((cp,il),id,bk,t)) :: bl) + (env, (CAst.make ?loc @@ GLocalPattern((cp,il),id,bk,t)) :: bl) let intern_generalization intern env lvar loc bk ak c = let c = intern {env with unb = true} c in @@ -518,12 +519,12 @@ let intern_generalization intern env lvar loc bk ak c = in if pi then (fun (loc', id) acc -> - Loc.tag ?loc:(Loc.merge_opt loc' loc) @@ - GProd (Name id, bk, Loc.tag ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc)) + CAst.make ?loc:(Loc.merge_opt loc' loc) @@ + GProd (Name id, bk, CAst.make ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc)) else (fun (loc', id) acc -> - Loc.tag ?loc:(Loc.merge_opt loc' loc) @@ - GLambda (Name id, bk, Loc.tag ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc)) + CAst.make ?loc:(Loc.merge_opt loc' loc) @@ + GLambda (Name id, bk, CAst.make ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc)) in List.fold_right (fun (loc, id as lid) (env, acc) -> let env' = push_name_env lvar (Variable,[],[],[]) env (loc, Name id) in @@ -576,27 +577,27 @@ let make_letins = (fun a c -> match a with | loc, LPLetIn (na,b,t) -> - Loc.tag ?loc @@ GLetIn(na,b,t,c) + CAst.make ?loc @@ GLetIn(na,b,t,c) | loc, LPCases ((cp,il),id) -> - let tt = (Loc.tag ?loc @@ GVar id, (Name id,None)) in - Loc.tag ?loc @@ GCases(Misctypes.LetPatternStyle,None,[tt],[(loc,(il,[cp],c))])) + let tt = (CAst.make ?loc @@ GVar id, (Name id,None)) in + CAst.make ?loc @@ GCases(Misctypes.LetPatternStyle,None,[tt],[(loc,(il,[cp],c))])) let rec subordinate_letins letins = function (* binders come in reverse order; the non-let are returned in reverse order together *) (* with the subordinated let-in in writing order *) - | (loc, GLocalDef (na,_,b,t))::l -> + | { loc; v = GLocalDef (na,_,b,t) }::l -> subordinate_letins ((Loc.tag ?loc @@ LPLetIn (na,b,t))::letins) l - | (loc, GLocalAssum (na,bk,t))::l -> + | { loc; v = GLocalAssum (na,bk,t)}::l -> let letins',rest = subordinate_letins [] l in letins',((loc,(na,bk,t)),letins)::rest - | (loc, GLocalPattern (u,id,bk,t)) :: l -> + | { loc; v = GLocalPattern (u,id,bk,t)} :: l -> subordinate_letins ((Loc.tag ?loc @@ LPCases (u,id))::letins) - ([Loc.tag ?loc @@ GLocalAssum (Name id,bk,t)] @ l) + ([CAst.make ?loc @@ GLocalAssum (Name id,bk,t)] @ l) | [] -> letins,[] let terms_of_binders bl = - let rec term_of_pat pt = CAst.map_from_loc (fun ?loc -> function + let rec term_of_pat pt = CAst.map_with_loc (fun ?loc -> function | PatVar (Name id) -> CRef (Ident (loc,id), None) | PatVar (Anonymous) -> error "Cannot turn \"_\" into a term." | PatCstr (c,l,_) -> @@ -605,11 +606,11 @@ let terms_of_binders bl = 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 -> (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." - | (loc, GLocalPattern ((u,_),_,_,_)) :: l -> term_of_pat u :: extract_variables l + | {loc; v = GLocalAssum (Name id,_,_)}::l -> (CAst.make ?loc @@ CRef (Ident (loc,id), None)) :: extract_variables l + | {loc; v = GLocalDef (Name id,_,_,_)}::l -> extract_variables l + | {loc; v = GLocalDef (Anonymous,_,_,_)}::l + | {loc; v = GLocalAssum (Anonymous,_,_)}::l -> error "Cannot turn \"_\" into a term." + | {loc; v = GLocalPattern ((u,_),_,_,_)}::l -> term_of_pat u :: extract_variables l | [] -> [] in extract_variables bl @@ -665,7 +666,7 @@ let instantiate_notation_constr loc intern ntnvars subst infos c = let bindings = Id.Map.map mk_env terms in Some (Genintern.generic_substitute_notation bindings arg) in - Loc.tag ?loc @@ GHole (knd, naming, arg) + CAst.make ?loc @@ GHole (knd, naming, arg) | NBinderList (x,y,iter,terminator) -> (try (* All elements of the list are in scopes (scopt,subscopes) *) @@ -683,22 +684,22 @@ let instantiate_notation_constr loc intern ntnvars subst infos c = let a,letins = snd (Option.get binderopt) in let e = make_letins letins (aux subst' infos c') in let (loc,(na,bk,t)) = a in - Loc.tag ?loc @@ GProd (na,bk,t,e) + CAst.make ?loc @@ GProd (na,bk,t,e) | NLambda (Name id,NHole _,c') when option_mem_assoc id binderopt -> let a,letins = snd (Option.get binderopt) in let (loc,(na,bk,t)) = a in - Loc.tag ?loc @@ GLambda (na,bk,t,make_letins letins (aux subst' infos c')) + CAst.make ?loc @@ GLambda (na,bk,t,make_letins letins (aux subst' infos c')) (* Two special cases to keep binder name synchronous with BinderType *) | NProd (na,NHole(Evar_kinds.BinderType na',naming,arg),c') when Name.equal na na' -> let subinfos,na = traverse_binder subst avoid subinfos na in - let ty = Loc.tag ?loc @@ GHole (Evar_kinds.BinderType na,naming,arg) in - Loc.tag ?loc @@ GProd (na,Explicit,ty,aux subst' subinfos c') + let ty = CAst.make ?loc @@ GHole (Evar_kinds.BinderType na,naming,arg) in + CAst.make ?loc @@ GProd (na,Explicit,ty,aux subst' subinfos c') | NLambda (na,NHole(Evar_kinds.BinderType na',naming,arg),c') when Name.equal na na' -> let subinfos,na = traverse_binder subst avoid subinfos na in - let ty = Loc.tag ?loc @@ GHole (Evar_kinds.BinderType na,naming,arg) in - Loc.tag ?loc @@ GLambda (na,Explicit,ty,aux subst' subinfos c') + let ty = CAst.make ?loc @@ GHole (Evar_kinds.BinderType na,naming,arg) in + CAst.make ?loc @@ GLambda (na,Explicit,ty,aux subst' subinfos c') | t -> glob_constr_of_notation_constr_with_binders ?loc (traverse_binder subst avoid) (aux subst') subinfos t @@ -710,7 +711,7 @@ let instantiate_notation_constr loc intern ntnvars subst infos c = intern {env with tmp_scope = scopt; scopes = subscopes @ env.scopes} a with Not_found -> - Loc.tag ?loc ( + CAst.make ?loc ( try GVar (Id.Map.find id renaming) with Not_found -> @@ -750,7 +751,7 @@ let string_of_ty = function | Variable -> "var" let gvar (loc, id) us = match us with -| None -> Loc.tag ?loc @@ GVar id +| None -> CAst.make ?loc @@ GVar id | Some _ -> user_err ?loc (str "Variable " ++ pr_id id ++ str " cannot have a universe instance") @@ -792,18 +793,18 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id us = let impls = implicits_of_global ref in let scopes = find_arguments_scope ref in Dumpglob.dump_reference ?loc "<>" (string_of_qualid (Decls.variable_secpath id)) "var"; - Loc.tag ?loc @@ GRef (ref, us), impls, scopes, [] + CAst.make ?loc @@ GRef (ref, us), impls, scopes, [] with e when CErrors.noncritical e -> (* [id] a goal variable *) gvar (loc,id) us, [], [], [] let find_appl_head_data c = - match Loc.obj c with + match c.v with | GRef (ref,_) -> let impls = implicits_of_global ref in let scopes = find_arguments_scope ref in c, impls, scopes, [] - | GApp ((_, GRef (ref,_)),l) + | GApp ({ v = GRef (ref,_) },l) when l != [] && Flags.version_strictly_greater Flags.V8_2 -> let n = List.length l in let impls = implicits_of_global ref in @@ -842,7 +843,7 @@ let intern_reference ref = (* Is it a global reference or a syntactic definition? *) let intern_qualid loc qid intern env lvar us args = match intern_extended_global_of_qualid (loc,qid) with - | TrueGlobal ref -> (Loc.tag ?loc @@ GRef (ref, us)), true, args + | TrueGlobal ref -> (CAst.make ?loc @@ GRef (ref, us)), true, args | SynDef sp -> let (ids,c) = Syntax_def.search_syntactic_definition sp in let nids = List.length ids in @@ -856,9 +857,9 @@ let intern_qualid loc qid intern env lvar us args = let c = instantiate_notation_constr loc intern lvar subst infos c in let c = match us, c with | None, _ -> c - | Some _, (loc, GRef (ref, None)) -> Loc.tag ?loc @@ GRef (ref, us) - | Some _, (loc, GApp ((loc', GRef (ref, None)), arg)) -> - Loc.tag ?loc @@ GApp (Loc.tag ?loc:loc' @@ GRef (ref, us), arg) + | Some _, { loc; v = GRef (ref, None) } -> CAst.make ?loc @@ GRef (ref, us) + | Some _, { loc; v = GApp ({ loc = loc' ; v = GRef (ref, None) }, arg) } -> + CAst.make ?loc @@ GApp (CAst.make ?loc:loc' @@ GRef (ref, us), arg) | Some _, _ -> user_err ?loc (str "Notation " ++ pr_qualid qid ++ str " cannot have a universe instance, its expanded head @@ -869,7 +870,7 @@ let intern_qualid loc qid intern env lvar us args = (* Rule out section vars since these should have been found by intern_var *) let intern_non_secvar_qualid loc qid intern env lvar us args = match intern_qualid loc qid intern env lvar us args with - | (_, GRef (VarRef _, _)),_,_ -> raise Not_found + | { v = GRef (VarRef _, _) },_,_ -> raise Not_found | r -> r let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args = function @@ -1021,8 +1022,8 @@ let chop_params_pattern loc ind args with_letin = else Inductiveops.inductive_nparams ind in assert (nparams <= List.length args); let params,args = List.chop nparams args in - List.iter (function _, PatVar Anonymous -> () - | loc', PatVar _ | loc', PatCstr(_,_,_) -> error_parameter_not_implicit ?loc:loc') params; + List.iter (function { v = PatVar Anonymous } -> () + | { loc; v = PatVar _ } | { loc; v = PatCstr(_,_,_) } -> error_parameter_not_implicit ?loc) params; args let find_constructor loc add_params ref = @@ -1042,7 +1043,7 @@ let find_constructor loc add_params ref = then Inductiveops.inductive_nparamdecls ind else Inductiveops.inductive_nparams ind in - List.make nb ([], [(Id.Map.empty, Loc.tag @@ PatVar Anonymous)]) + List.make nb ([], [(Id.Map.empty, CAst.make @@ PatVar Anonymous)]) | None -> [] let find_pattern_variable = function @@ -1368,7 +1369,7 @@ let rec intern_pat genv aliases pat = let idslpl2 = List.map (intern_pat genv empty_alias) pl2 in let (ids',pll) = product_of_cases_patterns aliases.alias_ids (idslpl1@idslpl2) in 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 + (asubst, CAst.make ?loc @@ PatCstr (c,chop_params_pattern loc (fst c) pl with_letin,alias_of aliases))) pll in ids',pl' in let loc = CAst.(pat.loc) in match CAst.(pat.v) with @@ -1389,10 +1390,10 @@ let rec intern_pat genv aliases pat = intern_cstr_with_all_args loc c with_letin idslpl1 (expl_pl@pl2) | RCPatAtom (Some id) -> let aliases = merge_aliases aliases id in - (aliases.alias_ids,[aliases.alias_map, Loc.tag ?loc @@ PatVar (alias_of aliases)]) + (aliases.alias_ids,[aliases.alias_map, CAst.make ?loc @@ PatVar (alias_of aliases)]) | RCPatAtom (None) -> let { alias_ids = ids; alias_map = asubst; } = aliases in - (ids, [asubst, Loc.tag ?loc @@ PatVar (alias_of aliases)]) + (ids, [asubst, CAst.make ?loc @@ PatVar (alias_of aliases)]) | RCPatOr pl -> assert (not (List.is_empty pl)); let pl' = List.map (intern_pat genv aliases) pl in @@ -1482,8 +1483,8 @@ let get_implicit_name n imps = Some (Impargs.name_of_implicit (List.nth imps (n-1))) let set_hole_implicit i b = function - | (loc, GRef (r,_)) | (_, GApp ((loc, (GRef (r,_))),_)) -> Loc.tag ?loc (Evar_kinds.ImplicitArg (r,i,b),Misctypes.IntroAnonymous,None) - | (loc, GVar id) -> Loc.tag ?loc (Evar_kinds.ImplicitArg (VarRef id,i,b),Misctypes.IntroAnonymous,None) + | {loc; v = GRef (r,_) } | { v = GApp ({loc; v = GRef (r,_)},_) } -> Loc.tag ?loc (Evar_kinds.ImplicitArg (r,i,b),Misctypes.IntroAnonymous,None) + | {loc; v = GVar id } -> Loc.tag ?loc (Evar_kinds.ImplicitArg (VarRef id,i,b),Misctypes.IntroAnonymous,None) | _ -> anomaly (Pp.str "Only refs have implicits") let exists_implicit_name id = @@ -1549,7 +1550,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = let before, after = split_at_annot bl n in let (env',rbefore) = List.fold_left intern_local_binder (env,[]) before in let ro = f (intern env') in - let n' = Option.map (fun _ -> List.count (function | _, GLocalAssum _ -> true + let n' = Option.map (fun _ -> List.count (function | { v = GLocalAssum _ } -> true | _ -> false (* remove let-ins *)) rbefore) n in n', ro, List.fold_left intern_local_binder (env',rbefore) after @@ -1572,7 +1573,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = push_name_env ntnvars (impls_type_list ~args:fix_args tyi) en (Loc.tag @@ Name name)) 0 env' lf in (a,b,c,intern {env'' with tmp_scope = None} bd)) dl idl_temp in - Loc.tag ?loc @@ + CAst.make ?loc @@ GRec (GFix (Array.map (fun (ro,_,_,_) -> ro) idl,n), Array.of_list lf, @@ -1599,7 +1600,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = push_name_env ntnvars (impls_type_list ~args:cofix_args tyi) en (Loc.tag @@ Name name)) 0 env' lf in (b,c,intern {env'' with tmp_scope = None} bd)) dl idl_tmp in - Loc.tag ?loc @@ + CAst.make ?loc @@ GRec (GCoFix n, Array.of_list lf, Array.map (fun (bl,_,_) -> bl) idl, @@ -1616,7 +1617,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = | 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 @@ + CAst.make ?loc @@ GLetIn (snd na, inc1, int, intern (push_name_env ntnvars (impls_term_list inc1) env na) c2) | CNotation ("- _",([{ CAst.v = CPrim (Numeral p) }],[],[])) @@ -1639,7 +1640,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = lvar us args ref in (* Rem: GApp(_,f,[]) stands for @f *) - Loc.tag ?loc @@ + CAst.make ?loc @@ GApp (f, intern_args env args_scopes (List.map fst args)) | CApp ((isproj,f), args) -> @@ -1696,7 +1697,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = let stripped_match_from_in = let rec aux = function | [] -> [] - | (_, (_loc, PatVar _)) :: q -> aux q + | (_, { v = PatVar _}) :: q -> aux q | l -> l in aux match_from_in in let rtnpo = match stripped_match_from_in with @@ -1705,20 +1706,20 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = (* Build a return predicate by expansion of the patterns of the "in" clause *) let thevars, thepats = List.split l in let sub_rtn = (* Some (GSort (Loc.ghost,GType None)) *) None in - let sub_tms = List.map (fun id -> (Loc.tag @@ GVar id),(Name id,None)) thevars (* "match v1,..,vn" *) in + let sub_tms = List.map (fun id -> (CAst.make @@ GVar id),(Name id,None)) thevars (* "match v1,..,vn" *) in let main_sub_eqn = Loc.tag @@ ([],thepats, (* "|p1,..,pn" *) Option.cata (intern_type env') - (Loc.tag ?loc @@ GHole(Evar_kinds.CasesType false,Misctypes.IntroAnonymous,None)) + (CAst.make ?loc @@ GHole(Evar_kinds.CasesType false,Misctypes.IntroAnonymous,None)) rtnpo) (* "=> P" if there were a return predicate P, and "=> _" otherwise *) in let catch_all_sub_eqn = if List.for_all (irrefutable globalenv) thepats then [] else - [Loc.tag @@ ([],List.make (List.length thepats) (Loc.tag @@ PatVar Anonymous), (* "|_,..,_" *) - Loc.tag @@ GHole(Evar_kinds.ImpossibleCase,Misctypes.IntroAnonymous,None))] (* "=> _" *) in - Some (Loc.tag @@ GCases(Term.RegularStyle,sub_rtn,sub_tms,main_sub_eqn::catch_all_sub_eqn)) + [Loc.tag @@ ([],List.make (List.length thepats) (CAst.make @@ PatVar Anonymous), (* "|_,..,_" *) + CAst.make @@ GHole(Evar_kinds.ImpossibleCase,Misctypes.IntroAnonymous,None))] (* "=> _" *) in + Some (CAst.make @@ GCases(Term.RegularStyle,sub_rtn,sub_tms,main_sub_eqn::catch_all_sub_eqn)) in let eqns' = List.map (intern_eqn (List.length tms) env) eqns in - Loc.tag ?loc @@ + CAst.make ?loc @@ GCases (sty, rtnpo, tms, List.flatten eqns') | CLetTuple (nal, (na,po), b, c) -> let env' = reset_tmp_scope env in @@ -1728,7 +1729,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = let env'' = push_name_env ntnvars (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env') (Loc.tag na') in intern_type env'' u) po in - Loc.tag ?loc @@ + CAst.make ?loc @@ GLetTuple (List.map snd nal, (na', p'), b', intern (List.fold_left (push_name_env ntnvars (Variable,[],[],[])) (reset_hidden_inductive_implicit_test env) nal) c) | CIf (c, (na,po), b1, b2) -> @@ -1738,7 +1739,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = let env'' = push_name_env ntnvars (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env) (Loc.tag na') in intern_type env'' p) po in - Loc.tag ?loc @@ + CAst.make ?loc @@ GIf (c', (na', p'), intern env b1, intern env b2) | CHole (k, naming, solve) -> let k = match k with @@ -1764,28 +1765,28 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = let (_, glb) = Genintern.generic_intern ist gen in Some glb in - Loc.tag ?loc @@ + CAst.make ?loc @@ GHole (k, naming, solve) (* Parsing pattern variables *) | CPatVar n when allow_patvar -> - Loc.tag ?loc @@ + CAst.make ?loc @@ GPatVar (true,n) | CEvar (n, []) when allow_patvar -> - Loc.tag ?loc @@ + CAst.make ?loc @@ GPatVar (false,n) (* end *) (* Parsing existential variables *) | CEvar (n, l) -> - Loc.tag ?loc @@ + CAst.make ?loc @@ GEvar (n, List.map (on_snd (intern env)) l) | CPatVar _ -> raise (InternalizationError (loc,IllegalMetavariable)) (* end *) | CSort s -> - Loc.tag ?loc @@ + CAst.make ?loc @@ GSort s | CCast (c1, c2) -> - Loc.tag ?loc @@ + CAst.make ?loc @@ GCast (intern env c1, Miscops.map_cast_type (intern_type env) c2) ) and intern_type env = intern (set_type_scope env) @@ -1824,8 +1825,8 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = let tm' = intern env tm in (* the "as" part *) let extra_id,na = match tm', na with - | (loc , GVar id), None when not (Id.Map.mem id (snd lvar)) -> Some id,(loc,Name id) - | (loc, GRef (VarRef id, _)), None -> Some id,(loc,Name id) + | {loc; v = GVar id}, None when not (Id.Map.mem id (snd lvar)) -> Some id,(loc,Name id) + | {loc; v = GRef (VarRef id, _)}, None -> Some id,(loc,Name id) | _, None -> None,(Loc.tag Anonymous) | _, Some (loc,na) -> None,(loc,na) in (* the "in" part *) @@ -1844,14 +1845,14 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = let rec canonize_args case_rel_ctxt arg_pats forbidden_names match_acc var_acc = let add_name l = function | _,Anonymous -> l - | loc,(Name y as x) -> (y, Loc.tag ?loc @@ PatVar x) :: l in + | loc,(Name y as x) -> (y, CAst.make ?loc @@ PatVar x) :: l in match case_rel_ctxt,arg_pats with (* LetIn in the rel_context *) | LocalDef _ :: t, l when not with_letin -> canonize_args t l forbidden_names match_acc ((Loc.tag Anonymous)::var_acc) | [],[] -> (add_name match_acc na, var_acc) - | _::t, (loc, PatVar x)::tt -> + | _::t, { loc; v = PatVar x}::tt -> canonize_args t tt forbidden_names (add_name match_acc (loc,x)) ((loc,x)::var_acc) | (LocalAssum (cano_name,ty) | LocalDef (cano_name,_,ty)) :: t, c::tt -> @@ -1897,7 +1898,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = (* with implicit arguments if maximal insertion is set *) [] else - (Loc.map (fun (a,b,c) -> GHole(a,b,c)) + (CAst.map_from_loc (fun ?loc (a,b,c) -> GHole(a,b,c)) (set_hole_implicit (n,get_implicit_name n l) (force_inference_of imp) c) ) :: aux (n+1) impl' subscopes' eargs rargs end @@ -1924,8 +1925,8 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = and smart_gapp f loc = function | [] -> f | l -> match f with - | (loc', GApp (g, args)) -> Loc.tag ?loc:(Loc.merge_opt loc' loc) @@ GApp (g, args@l) - | _ -> Loc.tag ?loc:(Loc.merge_opt (loc_of_glob_constr f) loc) @@ GApp (f, l) + | { loc = loc'; v = GApp (g, args) } -> CAst.make ?loc:(Loc.merge_opt loc' loc) @@ GApp (g, args@l) + | _ -> CAst.make ?loc:(Loc.merge_opt (loc_of_glob_constr f) loc) @@ GApp (f, l) and intern_args env subscopes = function | [] -> [] diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 52a6c450b..deb567865 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -125,7 +125,7 @@ let add_name_to_ids set na = | Name id -> Id.Set.add id set let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.empty) = - let rec vars bound vs (loc, t) = match t with + let rec vars bound vs { loc; CAst.v = t } = match t with | GVar id -> if is_freevar bound (Global.env ()) id then if Id.List.mem_assoc_sym id vs then vs @@ -314,7 +314,7 @@ let implicits_of_glob_constr ?(with_products=true) l = (ExplByPos (i, name), (true, true, true)) :: l | _ -> l in - let rec aux i (loc, c) = + let rec aux i { loc; CAst.v = c } = let abs na bk b = add_impl i na bk (aux (succ i) b) in diff --git a/interp/modintern.ml b/interp/modintern.ml index 45e6cd06c..3115c2bcb 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -65,14 +65,14 @@ let transl_with_decl env = function let ctx = Evd.evar_context_universe_context ectx in WithDef (fqid,(c,ctx)) -let loc_of_module (l, _) = l +let loc_of_module l = l.CAst.loc (* Invariant : the returned kind is never ModAny, and it is equal to the input kind when this one isn't ModAny. *) -let rec interp_module_ast env kind (loc, m) = match m with +let rec interp_module_ast env kind m = match m.CAst.v with | CMident qid -> - let (mp,kind) = lookup_module_or_modtype kind (loc,qid) in + let (mp,kind) = lookup_module_or_modtype kind (m.CAst.loc,qid) in (MEident mp, kind) | CMapply (me1,me2) -> let me1',kind1 = interp_module_ast env kind me1 in @@ -86,6 +86,6 @@ let rec interp_module_ast env kind (loc, m) = match m with (MEapply (me1',mp2), kind1) | CMwith (me,decl) -> let me,kind = interp_module_ast env kind me in - if kind == Module then error_incorrect_with_in_module loc; + if kind == Module then error_incorrect_with_in_module m.CAst.loc; let decl = transl_with_decl env decl in (MEwith(me,decl), kind) diff --git a/interp/notation.ml b/interp/notation.ml index 03dffa6ee..6b963b8c8 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -264,16 +264,16 @@ let notations_key_table = ref (KeyMap.empty : notation_rule list KeyMap.t) let prim_token_key_table = ref KeyMap.empty let glob_prim_constr_key = function - | _, GApp ((_, GRef (ref,_)),_) | _, GRef (ref,_) -> RefKey (canonical_gr ref) + | { CAst.v = GApp ({ CAst.v = GRef (ref,_) } ,_) } | { CAst.v = GRef (ref,_) } -> RefKey (canonical_gr ref) | _ -> Oth let glob_constr_keys = function - | _, GApp ((_, GRef (ref,_)),_) -> [RefKey (canonical_gr ref); Oth] - | _, GRef (ref,_) -> [RefKey (canonical_gr ref)] + | { CAst.v = GApp ({ CAst.v = GRef (ref,_) },_) } -> [RefKey (canonical_gr ref); Oth] + | { CAst.v = GRef (ref,_) } -> [RefKey (canonical_gr ref)] | _ -> [Oth] let cases_pattern_key = function - | _, PatCstr (ref,_,_) -> RefKey (canonical_gr (ConstructRef ref)) + | { CAst.v = PatCstr (ref,_,_) } -> RefKey (canonical_gr (ConstructRef ref)) | _ -> Oth let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *) @@ -471,14 +471,14 @@ let interp_prim_token = (** [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *) -let rec rcp_of_glob looked_for gt = CAst.map_from_loc (fun ?loc -> function +let rec rcp_of_glob looked_for = CAst.map (function | GVar id -> RCPatAtom (Some id) | GHole (_,_,_) -> RCPatAtom None | GRef (g,_) -> looked_for g; RCPatCstr (g,[],[]) - | GApp ((_, GRef (g,_)),l) -> + | GApp ({ CAst.v = GRef (g,_)},l) -> looked_for g; RCPatCstr (g, List.map (rcp_of_glob looked_for) l,[]) | _ -> raise Not_found - ) gt + ) let interp_prim_token_cases_pattern_expr ?loc looked_for p = interp_prim_token_gen (rcp_of_glob looked_for) ?loc p @@ -522,8 +522,8 @@ let uninterp_prim_token_ind_pattern ind args = if not b then raise Notation_ops.No_match; let args' = List.map (fun x -> snd (glob_constr_of_closed_cases_pattern x)) args in - let ref = Loc.tag @@ GRef (ref,None) in - match numpr (Loc.tag @@ GApp (ref,args')) with + let ref = CAst.make @@ GRef (ref,None) in + match numpr (CAst.make @@ GApp (ref,args')) with | None -> raise Notation_ops.No_match | Some n -> (sc,n) with Not_found -> raise Notation_ops.No_match diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 328fdd519..dd3043803 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -24,7 +24,7 @@ open Notation_term let on_true_do b f c = if b then (f c; b) else b -let compare_glob_constr f add (_l1, t1) (_l2, t2) = match t1,t2 with +let compare_glob_constr f add t1 t2 = match CAst.(t1.v,t2.v) with | GRef (r1,_), GRef (r2,_) -> eq_gr r1 r2 | GVar v1, GVar v2 -> on_true_do (Id.equal v1 v2) add (Name v1) | GApp (f1,l1), GApp (f2,l2) -> f f1 f2 && List.for_all2eq f l1 l2 @@ -117,43 +117,43 @@ let name_to_ident = function let to_id g e id = let e,na = g e (Name id) in e,name_to_ident na -let rec cases_pattern_fold_map ?loc g e = Loc.with_unloc (function +let rec cases_pattern_fold_map ?loc g e = CAst.with_val (function | PatVar na -> - let e',na' = g e na in e', Loc.tag ?loc @@ PatVar na' + let e',na' = g e na in e', CAst.make ?loc @@ PatVar na' | PatCstr (cstr,patl,na) -> let e',na' = g e na in let e',patl' = List.fold_map (cases_pattern_fold_map ?loc g) e patl in - e', Loc.tag ?loc @@ PatCstr (cstr,patl',na') + e', CAst.make ?loc @@ PatCstr (cstr,patl',na') ) let subst_binder_type_vars l = function | Evar_kinds.BinderType (Name id) -> let id = - try match snd @@ Id.List.assoc id l with GVar id' -> id' | _ -> id + try match Id.List.assoc id l with { CAst.v = GVar id' } -> id' | _ -> id with Not_found -> id in Evar_kinds.BinderType (Name id) | e -> e -let rec subst_glob_vars l gc = Loc.map (function - | GVar id as r -> (try snd @@ Id.List.assoc id l with Not_found -> r) +let rec subst_glob_vars l gc = CAst.map (function + | GVar id as r -> (try (Id.List.assoc id l).CAst.v with Not_found -> r) | GProd (Name id,bk,t,c) -> let id = - try match snd @@ Id.List.assoc id l with GVar id' -> id' | _ -> id + try match Id.List.assoc id l with { CAst.v = GVar id' } -> id' | _ -> id with Not_found -> id in GProd (Name id,bk,subst_glob_vars l t,subst_glob_vars l c) | GLambda (Name id,bk,t,c) -> let id = - try match snd @@ Id.List.assoc id l with GVar id' -> id' | _ -> id + try match Id.List.assoc id l with { CAst.v = GVar id' } -> id' | _ -> id with Not_found -> id in GLambda (Name id,bk,subst_glob_vars l t,subst_glob_vars l c) | GHole (x,naming,arg) -> GHole (subst_binder_type_vars l x,naming,arg) - | _ -> snd @@ map_glob_constr (subst_glob_vars l) gc (* assume: id is not binding *) + | _ -> (map_glob_constr (subst_glob_vars l) gc).CAst.v (* assume: id is not binding *) ) gc let ldots_var = Id.of_string ".." let glob_constr_of_notation_constr_with_binders ?loc g f e nc = - let lt x = Loc.tag ?loc x in lt @@ match nc with + let lt x = CAst.make ?loc x in lt @@ match nc with | NVar id -> GVar id | NApp (a,args) -> GApp (f e a, List.map (f e) args) | NList (x,y,iter,tail,swap) -> @@ -161,13 +161,13 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc = let innerl = (ldots_var,t)::(if swap then [] else [x, lt @@ GVar y]) in let inner = lt @@ GApp (lt @@ GVar (ldots_var),[subst_glob_vars innerl it]) in let outerl = (ldots_var,inner)::(if swap then [x, lt @@ GVar y] else []) in - Loc.obj @@ subst_glob_vars outerl it + (subst_glob_vars outerl it).CAst.v | NBinderList (x,y,iter,tail) -> let t = f e tail in let it = f e iter in let innerl = [(ldots_var,t);(x, lt @@ GVar y)] in let inner = lt @@ GApp (lt @@ GVar ldots_var,[subst_glob_vars innerl it]) in let outerl = [(ldots_var,inner)] in - Loc.obj @@ subst_glob_vars outerl it + (subst_glob_vars outerl it).CAst.v | NLambda (na,ty,c) -> let e',na = g e na in GLambda (na,Explicit,f e ty,f e' c) | NProd (na,ty,c) -> @@ -188,7 +188,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc = let eqnl' = List.map (fun (patl,rhs) -> let ((idl,e),patl) = List.fold_map (cases_pattern_fold_map ?loc fold) ([],e) patl in - lt (idl,patl,f e rhs)) eqnl in + Loc.tag (idl,patl,f e rhs)) eqnl in GCases (sty,Option.map (f e') rtntypopt,tml',eqnl') | NLetTuple (nal,(na,po),b,c) -> let e',nal = List.fold_map g e nal in @@ -221,14 +221,15 @@ let add_name r = function Anonymous -> () | Name id -> add_id r id let split_at_recursive_part c = let sub = ref None in + let open CAst in let rec aux = function - | loc0, GApp ((loc,GVar v),c::l) when Id.equal v ldots_var -> + | { loc = loc0; v = GApp ({ loc; v = GVar v },c::l) } when Id.equal v ldots_var -> (* *) begin match !sub with | None -> let () = sub := Some c in begin match l with - | [] -> Loc.tag ?loc @@ GVar ldots_var - | _ :: _ -> Loc.tag ?loc:loc0 @@ GApp (Loc.tag ?loc @@ GVar ldots_var, l) + | [] -> CAst.make ?loc @@ GVar ldots_var + | _ :: _ -> CAst.make ?loc:loc0 @@ GApp (CAst.make ?loc @@ GVar ldots_var, l) end | Some _ -> (* Not narrowed enough to find only one recursive part *) @@ -239,7 +240,7 @@ let split_at_recursive_part c = match !sub with | None -> (* No recursive pattern found *) raise Not_found | Some c -> - match Loc.obj outer_iterator with + match outer_iterator.v with | GVar v when Id.equal v ldots_var -> (* Not enough context *) raise Not_found | _ -> outer_iterator, c @@ -248,7 +249,7 @@ let subtract_loc loc1 loc2 = let l2 = fst (Option.cata Loc.unloc (0,0) loc2) in Some (Loc.make_loc (l1,l2-1)) -let check_is_hole id = function _, GHole _ -> () | t -> +let check_is_hole id = function { CAst.v = GHole _ } -> () | t -> user_err ?loc:(loc_of_glob_constr t) (strbrk "In recursive notation with binders, " ++ pr_id id ++ strbrk " is expected to come without type.") @@ -260,15 +261,16 @@ type recursive_pattern_kind = | RecursiveBinders of glob_constr * glob_constr let compare_recursive_parts found f f' (iterator,subc) = + let open CAst in let diff = ref None in let terminator = ref None in - let rec aux (l1, c1) (l2, c2) = match c1, c2 with + let rec aux c1 c2 = match c1.v, c2.v with | GVar v, term when Id.equal v ldots_var -> (* We found the pattern *) assert (match !terminator with None -> true | Some _ -> false); - terminator := Some (l2, term); + terminator := Some c2; true - | GApp ((_, GVar v),l1), GApp (term, l2) when Id.equal v ldots_var -> + | GApp ({ v = GVar v },l1), GApp (term, l2) when Id.equal v ldots_var -> (* We found the pattern, but there are extra arguments *) (* (this allows e.g. alternative (recursive) notation of application) *) assert (match !terminator with None -> true | Some _ -> false); @@ -294,7 +296,7 @@ let compare_recursive_parts found f f' (iterator,subc) = | Some _ -> false end | _ -> - compare_glob_constr aux (add_name found) (l1, c1) (l2, c2) in + compare_glob_constr aux (add_name found) c1 c2 in if aux iterator subc then match !diff with | None -> @@ -317,13 +319,13 @@ let compare_recursive_parts found f f' (iterator,subc) = (pi1 !found, (x,y) :: pi2 !found, pi3 !found),x,y,lassoc in let iterator = f' (if lassoc then iterator - else subst_glob_vars [x, Loc.tag @@ GVar y] iterator) in + else subst_glob_vars [x, CAst.make @@ GVar y] iterator) in (* found have been collected by compare_constr *) found := newfound; NList (x,y,iterator,f (Option.get !terminator),lassoc) | Some (x,y,RecursiveBinders (t_x,t_y)) -> let newfound = (pi1 !found, pi2 !found, (x,y) :: pi3 !found) in - let iterator = f' (subst_glob_vars [x, Loc.tag @@ GVar y] iterator) in + let iterator = f' (subst_glob_vars [x, CAst.make @@ GVar y] iterator) in (* found have been collected by compare_constr *) found := newfound; check_is_hole x t_x; @@ -341,15 +343,15 @@ let notation_constr_and_vars_of_glob_constr a = try compare_recursive_parts found aux aux' (split_at_recursive_part c) with Not_found -> found := keepfound; - match snd c with - | GApp ((loc, GVar f),[c]) when Id.equal f ldots_var -> + match c.CAst.v with + | GApp ({ CAst.v = GVar f; loc},[c]) when Id.equal f ldots_var -> (* Fall on the second part of the recursive pattern w/o having found the first part *) user_err ?loc (str "Cannot find where the recursive pattern starts.") | _c -> aux' c - and aux' x = Loc.with_unloc (function + and aux' x = CAst.with_val (function | GVar id -> add_id found id; NVar id | GApp (g,args) -> NApp (aux g, List.map aux args) | GLambda (na,bk,ty,c) -> add_name found na; NLambda (na,aux ty,aux c) @@ -456,15 +458,14 @@ let notation_constr_of_constr avoiding t = } in notation_constr_of_glob_constr nenv t -let rec subst_pat subst (loc, pat) = - match pat with - | PatVar _ -> (loc, pat) +let rec subst_pat subst pat = + match pat.CAst.v with + | PatVar _ -> pat | PatCstr (((kn,i),j),cpl,n) -> let kn' = subst_mind subst kn and cpl' = List.smartmap (subst_pat subst) cpl in - Loc.tag ?loc @@ - if kn' == kn && cpl' == cpl then pat else - PatCstr (((kn',i),j),cpl',n) + if kn' == kn && cpl' == cpl then pat else + CAst.make ?loc:pat.CAst.loc @@ PatCstr (((kn',i),j),cpl',n) let rec subst_notation_constr subst bound raw = match raw with @@ -595,8 +596,8 @@ let abstract_return_type_context pi mklam tml rtno = let abstract_return_type_context_glob_constr = abstract_return_type_context (fun (_,(_,nal)) -> nal) - (fun na c -> Loc.tag @@ - GLambda(na,Explicit,Loc.tag @@ GHole(Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None),c)) + (fun na c -> CAst.make @@ + GLambda(na,Explicit,CAst.make @@ GHole(Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None),c)) let abstract_return_type_context_notation_constr = abstract_return_type_context snd @@ -668,9 +669,9 @@ let add_binding_env alp (terms,onlybinders,termlists,binderlists) var v = let add_bindinglist_env (terms,onlybinders,termlists,binderlists) x bl = (terms,onlybinders,termlists,(x,bl)::binderlists) -let rec pat_binder_of_term t = Loc.map (function +let rec pat_binder_of_term t = CAst.map (function | GVar id -> PatVar (Name id) - | GApp ((_, GRef (ConstructRef cstr,_)), l) -> + | GApp ({ CAst.v = GRef (ConstructRef cstr,_)}, l) -> let nparams = Inductiveops.inductive_nparams (fst cstr) in let _,l = List.chop nparams l in PatCstr (cstr, List.map pat_binder_of_term l, Anonymous) @@ -680,7 +681,7 @@ let rec pat_binder_of_term t = Loc.map (function let bind_term_env alp (terms,onlybinders,termlists,binderlists as sigma) var v = try let v' = Id.List.assoc var terms in - match Loc.obj v, Loc.obj v' with + match CAst.(v.v, v'.v) with | GHole _, _ -> sigma | _, GHole _ -> let sigma = Id.List.remove_assoc var terms,onlybinders,termlists,binderlists in @@ -694,7 +695,7 @@ let bind_termlist_env alp (terms,onlybinders,termlists,binderlists as sigma) var try let vl' = Id.List.assoc var termlists in let unify_term v v' = - match Loc.obj v, Loc.obj v' with + match CAst.(v.v, v'.v) with | GHole _, _ -> v' | _, GHole _ -> v | _, _ -> if glob_constr_eq (alpha_rename (snd alp) v) v' then v' else raise No_match in @@ -710,8 +711,8 @@ let bind_termlist_env alp (terms,onlybinders,termlists,binderlists as sigma) var let bind_term_as_binding_env alp (terms,onlybinders,termlists,binderlists as sigma) var id = try - match Loc.obj @@ Id.List.assoc var terms with - | GVar id' -> + match Id.List.assoc var terms with + | { CAst.v = GVar id' } -> (if not (Id.equal id id') then (fst alp,(id,id')::snd alp) else alp), sigma | _ -> anomaly (str "A term which can be a binder has to be a variable") @@ -719,7 +720,7 @@ let bind_term_as_binding_env alp (terms,onlybinders,termlists,binderlists as sig (* The matching against a term allowing to find the instance has not been found yet *) (* If it will be a different name, we shall unfortunately fail *) (* TODO: look at the consequences for alp *) - alp, add_env alp sigma var (Loc.tag @@ GVar id) + alp, add_env alp sigma var (CAst.make @@ GVar id) let bind_binding_as_term_env alp (terms,onlybinders,termlists,binderlists as sigma) var id = try @@ -746,17 +747,17 @@ let bind_binding_env alp (terms,onlybinders,termlists,binderlists as sigma) var else (fst alp,(id1,id2)::snd alp),sigma with Not_found -> alp, add_binding_env alp sigma var v -let rec map_cases_pattern_name_left f = Loc.map (function +let rec map_cases_pattern_name_left f = CAst.map (function | PatVar na -> PatVar (f na) | PatCstr (c,l,na) -> PatCstr (c,List.map_left (map_cases_pattern_name_left f) l,f na) ) -let rec fold_cases_pattern_eq f x p p' = match p, p' with - | (loc, PatVar na), (_, PatVar na') -> let x,na = f x na na' in x, Loc.tag ?loc @@ PatVar na - | (loc, PatCstr (c,l,na)), (_, PatCstr (c',l',na')) when eq_constructor c c' -> +let rec fold_cases_pattern_eq f x p p' = let open CAst in match p, p' with + | { loc; v = PatVar na}, { v = PatVar na' } -> let x,na = f x na na' in x, CAst.make ?loc @@ PatVar na + | { loc; v = PatCstr (c,l,na)}, { v = PatCstr (c',l',na') } when eq_constructor c c' -> let x,l = fold_cases_pattern_list_eq f x l l' in let x,na = f x na na' in - x, Loc.tag ?loc @@ PatCstr (c,l,na) + x, CAst.make ?loc @@ PatCstr (c,l,na) | _ -> failwith "Not equal" and fold_cases_pattern_list_eq f x pl pl' = match pl, pl' with @@ -767,7 +768,7 @@ and fold_cases_pattern_list_eq f x pl pl' = match pl, pl' with x, p :: pl | _ -> assert false -let rec cases_pattern_eq (_,p1) (_,p2) = match p1, p2 with +let rec cases_pattern_eq p1 p2 = match CAst.(p1.v, p2.v) with | PatVar na1, PatVar na2 -> Name.equal na1 na2 | PatCstr (c1, pl1, na1), PatCstr (c2, pl2, na2) -> eq_constructor c1 c2 && List.equal cases_pattern_eq pl1 pl2 && @@ -788,7 +789,7 @@ let bind_bindinglist_env alp (terms,onlybinders,termlists,binderlists as sigma) let unify_pat alp p p' = try fold_cases_pattern_eq unify_name alp p p' with Failure _ -> raise No_match in let unify_term alp v v' = - match Loc.obj v, Loc.obj v' with + match CAst.(v.v, v'.v) with | GHole _, _ -> v' | _, GHole _ -> v | _, _ -> if glob_constr_eq (alpha_rename (snd alp) v) v' then v else raise No_match in @@ -798,17 +799,18 @@ let bind_bindinglist_env alp (terms,onlybinders,termlists,binderlists as sigma) | (Some _ as x), None | None, (Some _ as x) -> x | None, None -> None in let unify_binding_kind bk bk' = if bk == bk' then bk' else raise No_match in - let unify_binder alp (loc, b) (loc', b') = - match b, b' with + let unify_binder alp b b' = + let loc, loc' = CAst.(b.loc, b'.loc) in + match CAst.(b.v, b'.v) with | GLocalAssum (na,bk,t), GLocalAssum (na',bk',t') -> let alp, na = unify_name alp na na' in - alp, Loc.tag ?loc @@ GLocalAssum (na, unify_binding_kind bk bk', unify_term alp t t') + alp, CAst.make ?loc @@ GLocalAssum (na, unify_binding_kind bk bk', unify_term alp t t') | GLocalDef (na,bk,c,t), GLocalDef (na',bk',c',t') -> let alp, na = unify_name alp na na' in - alp, Loc.tag ?loc @@ GLocalDef (na, unify_binding_kind bk bk', unify_term alp c c', unify_opt_term alp t t') + alp, CAst.make ?loc @@ GLocalDef (na, unify_binding_kind bk bk', unify_term alp c c', unify_opt_term alp t t') | GLocalPattern ((p,ids),id,bk,t), GLocalPattern ((p',_),_,bk',t') -> let alp, p = unify_pat alp p p' in - alp, Loc.tag ?loc @@ GLocalPattern ((p,ids), id, unify_binding_kind bk bk', unify_term alp t t') + alp, CAst.make ?loc @@ GLocalPattern ((p,ids), id, unify_binding_kind bk bk', unify_term alp t t') | _ -> raise No_match in let rec unify alp bl bl' = match bl, bl' with @@ -835,18 +837,18 @@ let bind_bindinglist_as_term_env alp (terms,onlybinders,termlists,binderlists) v let unify_pat p p' = if cases_pattern_eq (map_cases_pattern_name_left (name_app (rename_var (snd alp))) p) p' then p' else raise No_match in - let unify_term_binder c (loc, b') = Loc.tag ?loc @@ + let unify_term_binder c = CAst.(map (fun b' -> match c, b' with - | (_, GVar id), GLocalAssum (na', bk', t') -> + | { v = GVar id}, GLocalAssum (na', bk', t') -> GLocalAssum (unify_id id na', bk', t') | c, GLocalPattern ((p',ids), id, bk', t') -> let p = pat_binder_of_term c in GLocalPattern ((unify_pat p p',ids), id, bk', t') - | _ -> raise No_match in + | _ -> raise No_match )) in let rec unify cl bl' = match cl, bl' with | [], [] -> [] - | c :: cl, (_loc, GLocalDef ( _, _, _, t)) :: bl' -> unify cl bl' + | c :: cl, { CAst.v = GLocalDef ( _, _, _, t) } :: bl' -> unify cl bl' | c :: cl, b' :: bl' -> unify_term_binder c b' :: unify cl bl' | _ -> raise No_match in let bl = unify cl bl' in @@ -887,8 +889,8 @@ let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with | (Anonymous,Anonymous) -> alp,sigma | _ -> raise No_match -let rec match_cases_pattern_binders metas acc (_, pat1) (_, pat2) = - match pat1, pat2 with +let rec match_cases_pattern_binders metas acc pat1 pat2 = + match CAst.(pat1.v, pat2.v) with | PatVar na1, PatVar na2 -> match_names metas acc na1 na2 | PatCstr (c1,patl1,na1), PatCstr (c2,patl2,na2) when eq_constructor c1 c2 && Int.equal (List.length patl1) (List.length patl2) -> @@ -898,22 +900,22 @@ let rec match_cases_pattern_binders metas acc (_, pat1) (_, pat2) = let glue_letin_with_decls = true -let rec match_iterated_binders islambda decls bi = Loc.with_loc (fun ?loc -> function - | GLambda (Name p,bk,t,(_, GCases (LetPatternStyle,None,[((_, GVar e),_)],[(_,(ids,[cp],b))]))) +let rec match_iterated_binders islambda decls bi = CAst.(with_loc_val (fun ?loc -> function + | GLambda (Name p,bk,t, { v = GCases (LetPatternStyle,None,[({ v = GVar e },_)],[(_,(ids,[cp],b))])}) when islambda && Id.equal p e -> - match_iterated_binders islambda ((Loc.tag ?loc @@ GLocalPattern((cp,ids),p,bk,t))::decls) b + match_iterated_binders islambda ((CAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t))::decls) b | GLambda (na,bk,t,b) when islambda -> - match_iterated_binders islambda ((Loc.tag ?loc @@ GLocalAssum(na,bk,t))::decls) b - | GProd (Name p,bk,t,(_, GCases (LetPatternStyle,None,[((_, GVar e),_)],[(_,(ids,[cp],b))]))) + match_iterated_binders islambda ((CAst.make ?loc @@ GLocalAssum(na,bk,t))::decls) b + | GProd (Name p,bk,t, { v = GCases (LetPatternStyle,None,[({ v = GVar e },_)],[(_,(ids,[cp],b))]) } ) when not islambda && Id.equal p e -> - match_iterated_binders islambda ((Loc.tag ?loc @@ GLocalPattern((cp,ids),p,bk,t))::decls) b + match_iterated_binders islambda ((CAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t))::decls) b | GProd ((Name _ as na),bk,t,b) when not islambda -> - match_iterated_binders islambda ((Loc.tag ?loc @@ GLocalAssum(na,bk,t))::decls) b + match_iterated_binders islambda ((CAst.make ?loc @@ GLocalAssum(na,bk,t))::decls) b | GLetIn (na,c,t,b) when glue_letin_with_decls -> match_iterated_binders islambda - ((Loc.tag ?loc @@ GLocalDef (na,Explicit (*?*), c,t))::decls) b - | b -> (decls, Loc.tag ?loc b) - ) bi + ((CAst.make ?loc @@ GLocalDef (na,Explicit (*?*), c,t))::decls) b + | b -> (decls, CAst.make ?loc b) + )) bi let remove_sigma x (terms,onlybinders,termlists,binderlists) = (Id.List.remove_assoc x terms,onlybinders,termlists,binderlists) @@ -974,12 +976,12 @@ let does_not_come_from_already_eta_expanded_var = (* The following test is then an approximation of what can be done *) (* optimally (whether other looping situations can occur remains to be *) (* checked). *) - function _loc, GVar _ -> false | _ -> true + function { CAst.v = GVar _ } -> false | _ -> true let rec match_ inner u alp metas sigma a1 a2 = - let loc, a1_val = Loc.to_pair a1 in - match a1_val, a2 with - + let open CAst in + let loc = a1.loc in + match a1.v, a2 with (* Matching notation variable *) | r1, NVar id2 when is_term_meta id2 metas -> bind_term_env alp sigma id2 a1 | GVar id1, NVar id2 when is_onlybinding_meta id2 metas -> bind_binding_as_term_env alp sigma id2 id1 @@ -990,29 +992,29 @@ let rec match_ inner u alp metas sigma a1 a2 = match_termlist (match_hd u alp) alp metas sigma a1 x y iter termin lassoc (* "λ p, let 'cp = p in t" -> "λ 'cp, t" *) - | GLambda (Name p,bk,t1,(_, GCases (LetPatternStyle,None,[((_, GVar e),_)],[(_,(ids,[cp],b1))]))), + | GLambda (Name p,bk,t1, { v = GCases (LetPatternStyle,None,[({ v = GVar e},_)],[(_,(ids,[cp],b1))])}), NBinderList (x,_,NLambda (Name _id2,_,b2),termin) when Id.equal p e -> - let (decls,b) = match_iterated_binders true [Loc.tag ?loc @@ GLocalPattern((cp,ids),p,bk,t1)] b1 in + let (decls,b) = match_iterated_binders true [CAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t1)] b1 in let alp,sigma = bind_bindinglist_env alp sigma x decls in match_in u alp metas sigma b termin (* Matching recursive notations for binders: ad hoc cases supporting let-in *) | GLambda (na1,bk,t1,b1), NBinderList (x,_,NLambda (Name _id2,_,b2),termin)-> - let (decls,b) = match_iterated_binders true [Loc.tag ?loc @@ GLocalAssum (na1,bk,t1)] b1 in + let (decls,b) = match_iterated_binders true [CAst.make ?loc @@ GLocalAssum (na1,bk,t1)] b1 in (* TODO: address the possibility that termin is a Lambda itself *) let alp,sigma = bind_bindinglist_env alp sigma x decls in match_in u alp metas sigma b termin (* "∀ p, let 'cp = p in t" -> "∀ 'cp, t" *) - | GProd (Name p,bk,t1,(_, GCases (LetPatternStyle,None,[((_, GVar e),_)],[(_,(ids,[cp],b1))]))), + | GProd (Name p,bk,t1, { v = GCases (LetPatternStyle,None,[({ v = GVar e },_)],[(_,(ids,[cp],b1))]) } ), NBinderList (x,_,NProd (Name _id2,_,b2),(NVar v as termin)) when Id.equal p e -> - let (decls,b) = match_iterated_binders true [Loc.tag ?loc @@ GLocalPattern ((cp,ids),p,bk,t1)] b1 in + let (decls,b) = match_iterated_binders true [CAst.make ?loc @@ GLocalPattern ((cp,ids),p,bk,t1)] b1 in let alp,sigma = bind_bindinglist_env alp sigma x decls in match_in u alp metas sigma b termin | GProd (na1,bk,t1,b1), NBinderList (x,_,NProd (Name _id2,_,b2),termin) when na1 != Anonymous -> - let (decls,b) = match_iterated_binders false [Loc.tag ?loc @@ GLocalAssum (na1,bk,t1)] b1 in + let (decls,b) = match_iterated_binders false [CAst.make ?loc @@ GLocalAssum (na1,bk,t1)] b1 in (* TODO: address the possibility that termin is a Prod itself *) let alp,sigma = bind_bindinglist_env alp sigma x decls in match_in u alp metas sigma b termin @@ -1021,18 +1023,18 @@ let rec match_ inner u alp metas sigma a1 a2 = match_binderlist_with_app (match_hd u) alp metas sigma a1 x y iter termin (* Matching individual binders as part of a recursive pattern *) - | GLambda (Name p,bk,t,(_, GCases (LetPatternStyle,None,[((_, GVar e),_)],[(_,(ids,[cp],b1))]))), + | GLambda (Name p,bk,t, { v = GCases (LetPatternStyle,None,[({ v = GVar e },_)],[(_,(ids,[cp],b1))])}), NLambda (Name id,_,b2) when is_bindinglist_meta id metas -> - let alp,sigma = bind_bindinglist_env alp sigma id [Loc.tag ?loc @@ GLocalPattern ((cp,ids),p,bk,t)] in + let alp,sigma = bind_bindinglist_env alp sigma id [CAst.make ?loc @@ GLocalPattern ((cp,ids),p,bk,t)] in match_in u alp metas sigma b1 b2 | GLambda (na,bk,t,b1), NLambda (Name id,_,b2) when is_bindinglist_meta id metas -> - let alp,sigma = bind_bindinglist_env alp sigma id [Loc.tag ?loc @@ GLocalAssum (na,bk,t)] in + let alp,sigma = bind_bindinglist_env alp sigma id [CAst.make ?loc @@ GLocalAssum (na,bk,t)] in match_in u alp metas sigma b1 b2 | GProd (na,bk,t,b1), NProd (Name id,_,b2) when is_bindinglist_meta id metas && na != Anonymous -> - let alp,sigma = bind_bindinglist_env alp sigma id [Loc.tag ?loc @@ GLocalAssum (na,bk,t)] in + let alp,sigma = bind_bindinglist_env alp sigma id [CAst.make ?loc @@ GLocalAssum (na,bk,t)] in match_in u alp metas sigma b1 b2 (* Matching compositionally *) @@ -1044,7 +1046,7 @@ let rec match_ inner u alp metas sigma a1 a2 = if n1 < n2 then let l21,l22 = List.chop (n2-n1) l2 in f1,l1, NApp (f2,l21), l22 else if n1 > n2 then - let l11,l12 = List.chop (n1-n2) l1 in Loc.tag ?loc @@ GApp (f1,l11),l12, f2,l2 + let l11,l12 = List.chop (n1-n2) l1 in CAst.make ?loc @@ GApp (f1,l11),l12, f2,l2 else f1,l1, f2, l2 in let may_use_eta = does_not_come_from_already_eta_expanded_var f1 in List.fold_left2 (match_ may_use_eta u alp metas) @@ -1117,17 +1119,17 @@ let rec match_ inner u alp metas sigma a1 a2 = let avoid = free_glob_vars a1 @ (* as in Namegen: *) glob_visible_short_qualid a1 in let id' = Namegen.next_ident_away id avoid in - let t1 = Loc.tag @@ GHole(Evar_kinds.BinderType (Name id'),Misctypes.IntroAnonymous,None) in + let t1 = CAst.make @@ GHole(Evar_kinds.BinderType (Name id'),Misctypes.IntroAnonymous,None) in let sigma = match t2 with | NHole _ -> sigma | NVar id2 -> bind_term_env alp sigma id2 t1 | _ -> assert false in let (alp,sigma) = if is_bindinglist_meta id metas then - bind_bindinglist_env alp sigma id [Loc.tag @@ GLocalAssum (Name id',Explicit,t1)] + bind_bindinglist_env alp sigma id [CAst.make @@ GLocalAssum (Name id',Explicit,t1)] else match_names metas (alp,sigma) (Name id') na in - match_in u alp metas sigma (mkGApp a1 (Loc.tag @@ GVar id')) b2 + match_in u alp metas sigma (mkGApp a1 (CAst.make @@ GVar id')) b2 | (GRec _ | GEvar _), _ | _,_ -> raise No_match @@ -1148,7 +1150,7 @@ and match_equations u alp metas sigma (_,(_,patl1,rhs1)) (patl2,rhs2) = (alp,sigma) patl1 patl2 in match_in u alp metas sigma rhs1 rhs2 -let term_of_binder bi = Loc.tag @@ match bi with +let term_of_binder bi = CAst.make @@ match bi with | Name id -> GVar id | Anonymous -> GHole (Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None) @@ -1165,7 +1167,7 @@ let match_notation_constr u c (metas,pat) = with Not_found -> (* Happens for binders bound to Anonymous *) (* Find a better way to propagate Anonymous... *) - Loc.tag @@GVar x in + CAst.make @@GVar x in List.fold_right (fun (x,(scl,typ)) (terms',termlists',binders') -> match typ with | NtnTypeConstr -> @@ -1184,7 +1186,7 @@ let match_notation_constr u c (metas,pat) = let add_patterns_for_params ind l = let mib,_ = Global.lookup_inductive ind in let nparams = mib.Declarations.mind_nparams in - Util.List.addn nparams (Loc.tag @@ PatVar Anonymous) l + Util.List.addn nparams (CAst.make @@ PatVar Anonymous) l let bind_env_cases_pattern (terms,x,termlists,y as sigma) var v = try @@ -1208,9 +1210,10 @@ let match_cases_pattern_list match_fun metas sigma rest x y iter termin lassoc = let l,(terms,onlybinders,termlists,binderlists as sigma) = aux sigma [] rest in (terms,onlybinders,(x,if lassoc then l else List.rev l)::termlists, binderlists) -let rec match_cases_pattern metas (terms,(),termlists,() as sigma) (loc, a1) a2 = - match a1, a2 with - | r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 (loc, r1)),(0,[]) +let rec match_cases_pattern metas (terms,(),termlists,() as sigma) a1 a2 = + let open CAst in + match a1.v, a2 with + | r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 a1),(0,[]) | PatVar Anonymous, NHole _ -> sigma,(0,[]) | PatCstr ((ind,_ as r1),largs,_), NRef (ConstructRef r2) when eq_constructor r1 r2 -> sigma,(0,add_patterns_for_params (fst r1) largs) @@ -1226,7 +1229,7 @@ let rec match_cases_pattern metas (terms,(),termlists,() as sigma) (loc, a1) a2 (List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(le2,more_args) | r1, NList (x,y,iter,termin,lassoc) -> (match_cases_pattern_list (match_cases_pattern_no_more_args) - metas (terms,(),termlists,()) (loc, r1) x y iter termin lassoc),(0,[]) + metas (terms,(),termlists,()) a1 x y iter termin lassoc),(0,[]) | _ -> raise No_match and match_cases_pattern_no_more_args metas sigma a1 a2 = diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli index 4f1e9d8e6..5366a302e 100644 --- a/intf/constrexpr.mli +++ b/intf/constrexpr.mli @@ -149,4 +149,4 @@ type module_ast_r = | CMident of qualid | CMapply of module_ast * module_ast | CMwith of module_ast * with_declaration_ast -and module_ast = module_ast_r Loc.located +and module_ast = module_ast_r CAst.ast diff --git a/intf/glob_term.mli b/intf/glob_term.mli index 5aa5bdeeb..aefccd518 100644 --- a/intf/glob_term.mli +++ b/intf/glob_term.mli @@ -28,7 +28,7 @@ type cases_pattern_r = | PatVar of Name.t | PatCstr of constructor * cases_pattern list * Name.t (** [PatCstr(p,C,l,x)] = "|'C' 'l' as 'x'" *) -and cases_pattern = cases_pattern_r Loc.located +and cases_pattern = cases_pattern_r CAst.ast (** Representation of an internalized (or in other words globalized) term. *) type glob_constr_r = @@ -53,7 +53,7 @@ type glob_constr_r = | GSort of glob_sort | GHole of Evar_kinds.t * intro_pattern_naming_expr * Genarg.glob_generic_argument option | GCast of glob_constr * glob_constr cast_type -and glob_constr = glob_constr_r Loc.located +and glob_constr = glob_constr_r CAst.ast and glob_decl = Name.t * binding_kind * glob_constr option * glob_constr @@ -83,7 +83,7 @@ type extended_glob_local_binder_r = | GLocalAssum of Name.t * binding_kind * glob_constr | GLocalDef of Name.t * binding_kind * glob_constr * glob_constr option | GLocalPattern of (cases_pattern * Id.t list) * Id.t * binding_kind * glob_constr -and extended_glob_local_binder = extended_glob_local_binder_r Loc.located +and extended_glob_local_binder = extended_glob_local_binder_r CAst.ast (** A globalised term together with a closure representing the value of its free variables. Intended for use when these variables are taken diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 27f879154..7239bc23b 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -511,11 +511,11 @@ GEXTEND Gram (* Module expressions *) module_expr: [ [ me = module_expr_atom -> me - | me1 = module_expr; me2 = module_expr_atom -> Loc.tag ~loc:!@loc @@ CMapply (me1,me2) + | me1 = module_expr; me2 = module_expr_atom -> CAst.make ~loc:!@loc @@ CMapply (me1,me2) ] ] ; module_expr_atom: - [ [ qid = qualid -> Loc.tag ~loc:!@loc @@ CMident (snd qid) | "("; me = module_expr; ")" -> me ] ] + [ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident (snd qid) | "("; me = module_expr; ")" -> me ] ] ; with_declaration: [ [ "Definition"; fqid = fullyqualid; ":="; c = Constr.lconstr -> @@ -525,12 +525,12 @@ GEXTEND Gram ] ] ; module_type: - [ [ qid = qualid -> Loc.tag ~loc:!@loc @@ CMident (snd qid) + [ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident (snd qid) | "("; mt = module_type; ")" -> mt | mty = module_type; me = module_expr_atom -> - Loc.tag ~loc:!@loc @@ CMapply (mty,me) + CAst.make ~loc:!@loc @@ CMapply (mty,me) | mty = module_type; "with"; decl = with_declaration -> - Loc.tag ~loc:!@loc @@ CMwith (mty,decl) + CAst.make ~loc:!@loc @@ CMwith (mty,decl) ] ] ; (* Proof using *) diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 938fe5237..7f2b21e79 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -345,10 +345,10 @@ let raw_push_named (na,raw_value,raw_typ) env = let add_pat_variables pat typ env : Environ.env = - let rec add_pat_variables env (loc, pat) typ : Environ.env = + let rec add_pat_variables env pat typ : Environ.env = observe (str "new rel env := " ++ Printer.pr_rel_context_of env (Evd.from_env env)); - match pat with + match pat.CAst.v with | PatVar na -> Environ.push_rel (RelDecl.LocalAssum (na,typ)) env | PatCstr(c,patl,na) -> let Inductiveops.IndType(indf,indargs) = @@ -398,7 +398,7 @@ let add_pat_variables pat typ env : Environ.env = -let rec pattern_to_term_and_type env typ = Loc.with_unloc (function +let rec pattern_to_term_and_type env typ = CAst.with_val (function | PatVar Anonymous -> assert false | PatVar (Name id) -> mkGVar id @@ -466,11 +466,12 @@ let rec pattern_to_term_and_type env typ = Loc.with_unloc (function let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = observe (str " Entering : " ++ Printer.pr_glob_constr rt); - match rt with - | _, GRef _ | _, GVar _ | _, GEvar _ | _, GPatVar _ | _, GSort _ | _, GHole _ -> + let open CAst in + match rt.v with + | GRef _ | GVar _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> (* do nothing (except changing type of course) *) mk_result [] rt avoid - | _, GApp(_,_) -> + | GApp(_,_) -> let f,args = glob_decompose_app rt in let args_res : (glob_constr list) build_entry_return = List.fold_right (* create the arguments lists of constructors and combine them *) @@ -482,14 +483,14 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = (mk_result [] [] avoid) in begin - match Loc.obj f with + match f.v with | GLambda _ -> let rec aux t l = match l with | [] -> t - | u::l -> Loc.tag @@ - match t with - | loc, GLambda(na,_,nat,b) -> + | u::l -> CAst.make @@ + match t.v with + | GLambda(na,_,nat,b) -> GLetIn(na,u,None,aux b l) | _ -> GApp(t,l) @@ -550,7 +551,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = let new_b = replace_var_by_term id - (Loc.tag @@ GVar id) + (CAst.make @@ GVar id) b in (Name new_id,new_b,new_avoid) @@ -579,7 +580,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = | GProd _ -> error "Cannot apply a type" end (* end of the application treatement *) - | _, GLambda(n,_,t,b) -> + | GLambda(n,_,t,b) -> (* we first compute the list of constructor corresponding to the body of the function, then the one corresponding to the type @@ -594,7 +595,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = let new_env = raw_push_named (new_n,None,t) env in let b_res = build_entry_lc new_env funnames avoid b in combine_results (combine_lam new_n) t_res b_res - | _, GProd(n,_,t,b) -> + | GProd(n,_,t,b) -> (* we first compute the list of constructor corresponding to the body of the function, then the one corresponding to the type @@ -604,13 +605,13 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = let new_env = raw_push_named (n,None,t) env in let b_res = build_entry_lc new_env funnames avoid b in combine_results (combine_prod n) t_res b_res - | loc, GLetIn(n,v,typ,b) -> + | GLetIn(n,v,typ,b) -> (* we first compute the list of constructor corresponding to the body of the function, then the one corresponding to the value [t] and combine the two result *) - let v = match typ with None -> v | Some t -> Loc.tag ?loc @@ GCast (v,CastConv t) in + let v = match typ with None -> v | Some t -> CAst.make ?loc:rt.loc @@ GCast (v,CastConv t) in let v_res = build_entry_lc env funnames avoid v in let v_as_constr,ctx = Pretyping.understand env (Evd.from_env env) v in let v_type = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr v_as_constr) in @@ -622,13 +623,13 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = in let b_res = build_entry_lc new_env funnames avoid b in combine_results (combine_letin n) v_res b_res - | _, GCases(_,_,el,brl) -> + | GCases(_,_,el,brl) -> (* we create the discrimination function and treat the case itself *) let make_discr = make_discr_match brl in build_entry_lc_from_case env funnames make_discr el brl avoid - | _, GIf(b,(na,e_option),lhs,rhs) -> + | GIf(b,(na,e_option),lhs,rhs) -> let b_as_constr,ctx = Pretyping.understand env (Evd.from_env env) b in let b_typ = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr b_as_constr) in let (ind,_) = @@ -651,7 +652,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = in (* Pp.msgnl (str "new case := " ++ Printer.pr_glob_constr match_expr); *) build_entry_lc env funnames avoid match_expr - | _, GLetTuple(nal,_,b,e) -> + | GLetTuple(nal,_,b,e) -> begin let nal_as_glob_constr = List.map @@ -677,8 +678,8 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = build_entry_lc env funnames avoid match_expr end - | _, GRec _ -> error "Not handled GRec" - | _, GCast(b,_) -> + | GRec _ -> error "Not handled GRec" + | GCast(b,_) -> build_entry_lc env funnames avoid b and build_entry_lc_from_case env funname make_discr (el:tomatch_tuples) @@ -860,8 +861,8 @@ let is_res id = -let same_raw_term (_,rt1) (_,rt2) = - match rt1,rt2 with +let same_raw_term rt1 rt2 = + match CAst.(rt1.v, rt2.v) with | GRef(r1,_), GRef (r2,_) -> Globnames.eq_gr r1 r2 | GHole _, GHole _ -> true | _ -> false @@ -894,16 +895,17 @@ exception Continue let rec rebuild_cons env nb_args relname args crossed_types depth rt = observe (str "rebuilding : " ++ pr_glob_constr rt); let open Context.Rel.Declaration in - match rt with - | _, GProd(n,k,t,b) -> + let open CAst in + match rt.v with + | GProd(n,k,t,b) -> let not_free_in_t id = not (is_free_in id t) in let new_crossed_types = t::crossed_types in begin match t with - | _, GApp(((_, GVar(res_id)) as res_rt),args') when is_res res_id -> + | { v = GApp(({ v = GVar res_id } as res_rt),args') } when is_res res_id -> begin match args' with - | (_, (GVar this_relname))::args' -> + | { v = GVar this_relname }::args' -> (*i The next call to mk_rel_id is valid since we are constructing the graph Ensures by: obvious @@ -925,7 +927,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = | _ -> (* the first args is the name of the function! *) assert false end - | loc1, GApp((loc2, GRef(eq_as_ref,_)),[ty;(loc3, GVar id);rt]) + | { loc = loc1; v = GApp({ loc = loc2; v = GRef(eq_as_ref,_) },[ty; { loc = loc3; v = GVar id};rt]) } when Globnames.eq_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous -> begin @@ -962,8 +964,8 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let params,arg' = ((Util.List.chop nparam args')) in - let rt_typ = Loc.tag @@ - GApp(Loc.tag @@ GRef (Globnames.IndRef (fst ind),None), + let rt_typ = CAst.make @@ + GApp(CAst.make @@ GRef (Globnames.IndRef (fst ind),None), (List.map (fun p -> Detyping.detype false [] env (Evd.from_env env) @@ -973,7 +975,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = (mkGHole ())))) in let eq' = - Loc.tag ?loc:loc1 @@ GApp(Loc.tag ?loc:loc2 @@GRef(jmeq,None),[ty;Loc.tag ?loc:loc3 @@ GVar id;rt_typ;rt]) + CAst.make ?loc:loc1 @@ GApp(CAst.make ?loc:loc2 @@GRef(jmeq,None),[ty;CAst.make ?loc:loc3 @@ GVar id;rt_typ;rt]) in observe (str "computing new type for jmeq : " ++ pr_glob_constr eq'); let eq'_as_constr,ctx = Pretyping.understand env (Evd.from_env env) eq' in @@ -1042,7 +1044,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = mkGProd(n,t,new_b),id_to_exclude else new_b, Id.Set.add id id_to_exclude *) - | loc1, GApp((loc2, GRef(eq_as_ref,_)),[ty;rt1;rt2]) + | { loc = loc1; v = GApp({ loc = loc2; v = GRef(eq_as_ref,_) },[ty;rt1;rt2]) } when Globnames.eq_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous -> begin @@ -1093,7 +1095,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = (Id.Set.filter not_free_in_t id_to_exclude) | _ -> mkGProd(n,t,new_b),Id.Set.filter not_free_in_t id_to_exclude end - | _, GLambda(n,k,t,b) -> + | GLambda(n,k,t,b) -> begin let not_free_in_t id = not (is_free_in id t) in let new_crossed_types = t :: crossed_types in @@ -1112,14 +1114,14 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = then new_b, Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude) else - Loc.tag @@ GProd(n,k,t,new_b),Id.Set.filter not_free_in_t id_to_exclude + CAst.make @@ GProd(n,k,t,new_b),Id.Set.filter not_free_in_t id_to_exclude | _ -> anomaly (Pp.str "Should not have an anonymous function here") (* We have renamed all the anonymous functions during alpha_renaming phase *) end - | loc, GLetIn(n,v,t,b) -> + | GLetIn(n,v,t,b) -> begin - let t = match t with None -> v | Some t -> Loc.tag ?loc @@ GCast (v,CastConv t) in + let t = match t with None -> v | Some t -> CAst.make ?loc:rt.loc @@ GCast (v,CastConv t) in let not_free_in_t id = not (is_free_in id t) in let evd = (Evd.from_env env) in let t',ctx = Pretyping.understand env evd t in @@ -1135,10 +1137,10 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = match n with | Name id when Id.Set.mem id id_to_exclude && depth >= nb_args -> new_b,Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude) - | _ -> Loc.tag @@ GLetIn(n,t,None,new_b), (* HOPING IT WOULD WORK *) + | _ -> CAst.make @@ GLetIn(n,t,None,new_b), (* HOPING IT WOULD WORK *) Id.Set.filter not_free_in_t id_to_exclude end - | _, GLetTuple(nal,(na,rto),t,b) -> + | GLetTuple(nal,(na,rto),t,b) -> assert (Option.is_empty rto); begin let not_free_in_t id = not (is_free_in id t) in @@ -1161,7 +1163,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = (* | Name id when Id.Set.mem id id_to_exclude -> *) (* new_b,Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude) *) (* | _ -> *) - Loc.tag @@ GLetTuple(nal,(na,None),t,new_b), + CAst.make @@ GLetTuple(nal,(na,None),t,new_b), Id.Set.filter not_free_in_t (Id.Set.union id_to_exclude id_to_exclude') end @@ -1187,9 +1189,9 @@ let rebuild_cons env nb_args relname args crossed_types rt = TODO: Find a valid way to deal with implicit arguments here! *) -let rec compute_cst_params relnames params gt = Loc.with_unloc (function +let rec compute_cst_params relnames params gt = CAst.with_val (function | GRef _ | GVar _ | GEvar _ | GPatVar _ -> params - | GApp((_, GVar relname'),rtl) when Id.Set.mem relname' relnames -> + | GApp({ CAst.v = GVar relname' },rtl) when Id.Set.mem relname' relnames -> compute_cst_params_from_app [] (params,rtl) | GApp(f,args) -> List.fold_left (compute_cst_params relnames) params (f::args) @@ -1211,7 +1213,7 @@ let rec compute_cst_params relnames params gt = Loc.with_unloc (function and compute_cst_params_from_app acc (params,rtl) = match params,rtl with | _::_,[] -> assert false (* the rel has at least nargs + 1 arguments ! *) - | ((Name id,_,None) as param)::params',(_, GVar id')::rtl' + | ((Name id,_,None) as param)::params', { CAst.v = GVar id' }::rtl' when Id.compare id id' == 0 -> compute_cst_params_from_app (param::acc) (params',rtl') | _ -> List.rev acc diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 66b9897d0..5abcb100f 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -10,16 +10,16 @@ open Misctypes Some basic functions to rebuild glob_constr In each of them the location is Loc.ghost *) -let mkGRef ref = Loc.tag @@ GRef(ref,None) -let mkGVar id = Loc.tag @@ GVar(id) -let mkGApp(rt,rtl) = Loc.tag @@ GApp(rt,rtl) -let mkGLambda(n,t,b) = Loc.tag @@ GLambda(n,Explicit,t,b) -let mkGProd(n,t,b) = Loc.tag @@ GProd(n,Explicit,t,b) -let mkGLetIn(n,b,t,c) = Loc.tag @@ GLetIn(n,b,t,c) -let mkGCases(rto,l,brl) = Loc.tag @@ GCases(Term.RegularStyle,rto,l,brl) -let mkGSort s = Loc.tag @@ GSort(s) -let mkGHole () = Loc.tag @@ GHole(Evar_kinds.BinderType Anonymous,Misctypes.IntroAnonymous,None) -let mkGCast(b,t) = Loc.tag @@ GCast(b,CastConv t) +let mkGRef ref = CAst.make @@ GRef(ref,None) +let mkGVar id = CAst.make @@ GVar(id) +let mkGApp(rt,rtl) = CAst.make @@ GApp(rt,rtl) +let mkGLambda(n,t,b) = CAst.make @@ GLambda(n,Explicit,t,b) +let mkGProd(n,t,b) = CAst.make @@ GProd(n,Explicit,t,b) +let mkGLetIn(n,b,t,c) = CAst.make @@ GLetIn(n,b,t,c) +let mkGCases(rto,l,brl) = CAst.make @@ GCases(Term.RegularStyle,rto,l,brl) +let mkGSort s = CAst.make @@ GSort(s) +let mkGHole () = CAst.make @@ GHole(Evar_kinds.BinderType Anonymous,Misctypes.IntroAnonymous,None) +let mkGCast(b,t) = CAst.make @@ GCast(b,CastConv t) (* Some basic functions to decompose glob_constrs @@ -27,7 +27,7 @@ let mkGCast(b,t) = Loc.tag @@ GCast(b,CastConv t) *) let glob_decompose_prod = let rec glob_decompose_prod args = function - | _, GProd(n,k,t,b) -> + | { CAst.v = GProd(n,k,t,b) } -> glob_decompose_prod ((n,t)::args) b | rt -> args,rt in @@ -35,9 +35,9 @@ let glob_decompose_prod = let glob_decompose_prod_or_letin = let rec glob_decompose_prod args = function - | _, GProd(n,k,t,b) -> + | { CAst.v = GProd(n,k,t,b) } -> glob_decompose_prod ((n,None,Some t)::args) b - | _, GLetIn(n,b,t,c) -> + | { CAst.v = GLetIn(n,b,t,c) } -> glob_decompose_prod ((n,Some b,t)::args) c | rt -> args,rt in @@ -59,7 +59,7 @@ let glob_decompose_prod_n n = if i<=0 then args,c else match c with - | _, GProd(n,_,t,b) -> + | { CAst.v = GProd(n,_,t,b) } -> glob_decompose_prod (i-1) ((n,t)::args) b | rt -> args,rt in @@ -71,9 +71,9 @@ let glob_decompose_prod_or_letin_n n = if i<=0 then args,c else match c with - | _, GProd(n,_,t,b) -> + | { CAst.v = GProd(n,_,t,b) } -> glob_decompose_prod (i-1) ((n,None,Some t)::args) b - | _, GLetIn(n,b,t,c) -> + | { CAst.v = GLetIn(n,b,t,c) } -> glob_decompose_prod (i-1) ((n,Some b,t)::args) c | rt -> args,rt in @@ -84,7 +84,7 @@ let glob_decompose_app = let rec decompose_rapp acc rt = (* msgnl (str "glob_decompose_app on : "++ Printer.pr_glob_constr rt); *) match rt with - | _, GApp(rt,rtl) -> + | { CAst.v = GApp(rt,rtl) } -> decompose_rapp (List.fold_left (fun y x -> x::y) acc rtl) rt | rt -> rt,List.rev acc in @@ -120,7 +120,7 @@ let remove_name_from_mapping mapping na = let change_vars = let rec change_vars mapping rt = - Loc.map (function + CAst.map (function | GRef _ as x -> x | GVar id -> let new_id = @@ -189,18 +189,19 @@ let change_vars = -let rec alpha_pat excluded (loc, pat) = - match pat with +let rec alpha_pat excluded pat = + let loc = pat.CAst.loc in + match pat.CAst.v with | PatVar Anonymous -> let new_id = Indfun_common.fresh_id excluded "_x" in - (Loc.tag ?loc @@ PatVar(Name new_id)),(new_id::excluded),Id.Map.empty + (CAst.make ?loc @@ PatVar(Name new_id)),(new_id::excluded),Id.Map.empty | PatVar(Name id) -> if Id.List.mem id excluded then let new_id = Namegen.next_ident_away id excluded in - (Loc.tag ?loc @@ PatVar(Name new_id)),(new_id::excluded), + (CAst.make ?loc @@ PatVar(Name new_id)),(new_id::excluded), (Id.Map.add id new_id Id.Map.empty) - else (Loc.tag ?loc pat),excluded,Id.Map.empty + else pat, excluded,Id.Map.empty | PatCstr(constr,patl,na) -> let new_na,new_excluded,map = match na with @@ -218,7 +219,7 @@ let rec alpha_pat excluded (loc, pat) = ([],new_excluded,map) patl in - (Loc.tag ?loc @@ PatCstr(constr,List.rev new_patl,new_na)),new_excluded,new_map + (CAst.make ?loc @@ PatCstr(constr,List.rev new_patl,new_na)),new_excluded,new_map let alpha_patl excluded patl = let patl,new_excluded,map = @@ -236,8 +237,8 @@ let alpha_patl excluded patl = let raw_get_pattern_id pat acc = - let rec get_pattern_id (loc, pat) = - match pat with + let rec get_pattern_id pat = + match pat.CAst.v with | PatVar(Anonymous) -> assert false | PatVar(Name id) -> [id] @@ -254,10 +255,11 @@ let raw_get_pattern_id pat acc = let get_pattern_id pat = raw_get_pattern_id pat [] -let rec alpha_rt excluded (loc, rt) = - let new_rt = Loc.tag ?loc @@ - match rt with - | GRef _ | GVar _ | GEvar _ | GPatVar _ -> rt +let rec alpha_rt excluded rt = + let loc = rt.CAst.loc in + let new_rt = CAst.make ?loc @@ + match rt.CAst.v with + | GRef _ | GVar _ | GEvar _ | GPatVar _ as rt -> rt | GLambda(Anonymous,k,t,b) -> let new_id = Namegen.next_ident_away (Id.of_string "_x") excluded in let new_excluded = new_id :: excluded in @@ -351,8 +353,8 @@ let rec alpha_rt excluded (loc, rt) = alpha_rt excluded rhs ) | GRec _ -> error "Not handled GRec" - | GSort _ -> rt - | GHole _ -> rt + | GSort _ + | GHole _ as rt -> rt | GCast (b,c) -> GCast(alpha_rt excluded b, Miscops.map_cast_type (alpha_rt excluded) c) @@ -375,7 +377,7 @@ and alpha_br excluded (loc,(ids,patl,res)) = [is_free_in id rt] checks if [id] is a free variable in [rt] *) let is_free_in id = - let rec is_free_in (loc, gt) = match gt with + let rec is_free_in x = CAst.with_loc_val (fun ?loc -> function | GRef _ -> false | GVar id' -> Id.compare id' id == 0 | GEvar _ -> false @@ -411,6 +413,7 @@ let is_free_in id = | GHole _ -> false | GCast (b,(CastConv t|CastVM t|CastNative t)) -> is_free_in b || is_free_in t | GCast (b,CastCoerce) -> is_free_in b + ) x and is_free_in_br (_,(ids,_,rt)) = (not (Id.List.mem id ids)) && is_free_in rt in @@ -418,7 +421,7 @@ let is_free_in id = -let rec pattern_to_term pt = Loc.with_unloc (function +let rec pattern_to_term pt = CAst.with_val (function | PatVar Anonymous -> assert false | PatVar(Name id) -> mkGVar id @@ -445,39 +448,38 @@ let rec pattern_to_term pt = Loc.with_unloc (function let replace_var_by_term x_id term = - let rec replace_var_by_pattern (loc, rt) = Loc.tag ?loc @@ - match rt with - | GRef _ -> rt - | GVar id when Id.compare id x_id == 0 -> Loc.obj term - | GVar _ -> rt - | GEvar _ -> rt - | GPatVar _ -> rt + let rec replace_var_by_pattern x = CAst.map (function + | GVar id when Id.compare id x_id == 0 -> term.CAst.v + | GRef _ + | GVar _ + | GEvar _ + | GPatVar _ as rt -> rt | GApp(rt',rtl) -> GApp(replace_var_by_pattern rt', List.map replace_var_by_pattern rtl ) - | GLambda(Name id,_,_,_) when Id.compare id x_id == 0 -> rt + | GLambda(Name id,_,_,_) as rt when Id.compare id x_id == 0 -> rt | GLambda(name,k,t,b) -> GLambda(name, k, replace_var_by_pattern t, replace_var_by_pattern b ) - | GProd(Name id,_,_,_) when Id.compare id x_id == 0 -> rt + | GProd(Name id,_,_,_) as rt when Id.compare id x_id == 0 -> rt | GProd(name,k,t,b) -> GProd( name, k, replace_var_by_pattern t, replace_var_by_pattern b ) - | GLetIn(Name id,_,_,_) when Id.compare id x_id == 0 -> rt + | GLetIn(Name id,_,_,_) as rt when Id.compare id x_id == 0 -> rt | GLetIn(name,def,typ,b) -> GLetIn(name, replace_var_by_pattern def, Option.map (replace_var_by_pattern) typ, replace_var_by_pattern b ) - | GLetTuple(nal,_,_,_) + | GLetTuple(nal,_,_,_) as rt when List.exists (function Name id -> Id.equal id x_id | _ -> false) nal -> rt | GLetTuple(nal,(na,rto),def,b) -> @@ -499,11 +501,12 @@ let replace_var_by_term x_id term = replace_var_by_pattern rhs ) | GRec _ -> raise (UserError(None,str "Not handled GRec")) - | GSort _ -> rt - | GHole _ -> rt + | GSort _ + | GHole _ as rt -> rt | GCast(b,c) -> GCast(replace_var_by_pattern b, Miscops.map_cast_type replace_var_by_pattern c) + ) x and replace_var_by_pattern_br ((loc,(idl,patl,res)) as br) = if List.exists (fun id -> Id.compare id x_id == 0) idl then br @@ -520,9 +523,10 @@ exception NotUnifiable let rec are_unifiable_aux = function | [] -> () | eq::eqs -> + let open CAst in match eq with - | (_,PatVar _),_ | _,(_,PatVar _) -> are_unifiable_aux eqs - | (_,PatCstr(constructor1,cpl1,_)),(_,PatCstr(constructor2,cpl2,_)) -> + | { v = PatVar _ },_ | _, { v = PatVar _ } -> are_unifiable_aux eqs + | { v = PatCstr(constructor1,cpl1,_) }, { v = PatCstr(constructor2,cpl2,_) } -> if not (eq_constructor constructor2 constructor1) then raise NotUnifiable else @@ -542,9 +546,10 @@ let are_unifiable pat1 pat2 = let rec eq_cases_pattern_aux = function | [] -> () | eq::eqs -> + let open CAst in match eq with - | (_,PatVar _),(_,PatVar _) -> eq_cases_pattern_aux eqs - | (_,PatCstr(constructor1,cpl1,_)),(_,PatCstr(constructor2,cpl2,_)) -> + | { v = PatVar _ }, { v = PatVar _ } -> eq_cases_pattern_aux eqs + | { v = PatCstr(constructor1,cpl1,_) }, { v = PatCstr(constructor2,cpl2,_) } -> if not (eq_constructor constructor2 constructor1) then raise NotUnifiable else @@ -564,7 +569,7 @@ let eq_cases_pattern pat1 pat2 = let ids_of_pat = - let rec ids_of_pat ids = Loc.with_unloc (function + let rec ids_of_pat ids = CAst.with_val (function | PatVar Anonymous -> ids | PatVar(Name id) -> Id.Set.add id ids | PatCstr(_,patl,_) -> List.fold_left ids_of_pat ids patl @@ -578,7 +583,7 @@ let id_of_name = function (* TODO: finish Rec caes *) let ids_of_glob_constr c = - let rec ids_of_glob_constr acc (loc, c) = + let rec ids_of_glob_constr acc {loc; CAst.v = c} = let idof = id_of_name in match c with | GVar id -> id::acc @@ -605,12 +610,11 @@ let ids_of_glob_constr c = let zeta_normalize = - let rec zeta_normalize_term (loc, rt) = Loc.tag ?loc @@ - match rt with - | GRef _ -> rt - | GVar _ -> rt - | GEvar _ -> rt - | GPatVar _ -> rt + let rec zeta_normalize_term x = CAst.map (function + | GRef _ + | GVar _ + | GEvar _ + | GPatVar _ as rt -> rt | GApp(rt',rtl) -> GApp(zeta_normalize_term rt', List.map zeta_normalize_term rtl @@ -628,9 +632,9 @@ let zeta_normalize = zeta_normalize_term b ) | GLetIn(Name id,def,typ,b) -> - Loc.obj @@ zeta_normalize_term (replace_var_by_term id def b) + (zeta_normalize_term (replace_var_by_term id def b)).CAst.v | GLetIn(Anonymous,def,typ,b) -> - Loc.obj @@ zeta_normalize_term b + (zeta_normalize_term b).CAst.v | GLetTuple(nal,(na,rto),def,b) -> GLetTuple(nal, (na,Option.map zeta_normalize_term rto), @@ -650,11 +654,12 @@ let zeta_normalize = zeta_normalize_term rhs ) | GRec _ -> raise (UserError(None,str "Not handled GRec")) - | GSort _ -> rt - | GHole _ -> rt + | GSort _ + | GHole _ as rt -> rt | GCast(b,c) -> GCast(zeta_normalize_term b, Miscops.map_cast_type zeta_normalize_term c) + ) x and zeta_normalize_br (loc,(idl,patl,res)) = (loc,(idl,patl,zeta_normalize_term res)) in @@ -665,21 +670,19 @@ let zeta_normalize = let expand_as = - let rec add_as map (loc, pat) = + let rec add_as map ({loc; CAst.v = pat } as rt) = match pat with | PatVar _ -> map | PatCstr(_,patl,Name id) -> - Id.Map.add id (pattern_to_term (loc, pat)) (List.fold_left add_as map patl) + Id.Map.add id (pattern_to_term rt) (List.fold_left add_as map patl) | PatCstr(_,patl,_) -> List.fold_left add_as map patl in - let rec expand_as map (loc, rt) = - Loc.tag ?loc @@ - match rt with - | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> rt - | GVar id -> + let rec expand_as map = CAst.map (function + | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ as rt -> rt + | GVar id as rt -> begin try - Loc.obj @@ Id.Map.find id map + (Id.Map.find id map).CAst.v with Not_found -> rt end | GApp(f,args) -> GApp(expand_as map f,List.map (expand_as map) args) @@ -699,6 +702,7 @@ let expand_as = | GCases(sty,po,el,brl) -> GCases(sty, Option.map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el, List.map (expand_as_br map) brl) + ) and expand_as_br map (loc,(idl,cpl,rt)) = (loc,(idl,cpl, expand_as (List.fold_left add_as map cpl) rt)) in diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index f4e9aa372..ab83cb15a 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -190,7 +190,7 @@ let build_newrecursive l = let is_rec names = let names = List.fold_right Id.Set.add names Id.Set.empty in let check_id id names = Id.Set.mem id names in - let rec lookup names (loc, gt) = match gt with + let rec lookup names gt = match gt.CAst.v with | GVar(id) -> check_id id names | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> false | GCast(b,_) -> lookup names b diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index de8dc53f1..394b252aa 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -69,7 +69,7 @@ let chop_rlambda_n = if n == 0 then List.rev acc,rt else - match Loc.obj rt with + match rt.CAst.v with | Glob_term.GLambda(name,k,t,b) -> chop_lambda_n ((name,t,None)::acc) (n-1) b | Glob_term.GLetIn(name,v,t,b) -> chop_lambda_n ((name,v,t)::acc) (n-1) b | _ -> @@ -83,7 +83,7 @@ let chop_rprod_n = if n == 0 then List.rev acc,rt else - match Loc.obj rt with + match rt.CAst.v with | Glob_term.GProd(name,k,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b | _ -> raise (CErrors.UserError(Some "chop_rprod_n",str "chop_rprod_n: Not enough products")) in diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 5b51a213a..d4865bf5e 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -66,7 +66,7 @@ let string_of_name = id_of_name %> Id.to_string (** [isVarf f x] returns [true] if term [x] is of the form [(Var f)]. *) let isVarf f x = match x with - | _, GVar x -> Id.equal x f + | { CAst.v = GVar x } -> Id.equal x f | _ -> false (** [ident_global_exist id] returns true if identifier [id] is linked @@ -504,40 +504,40 @@ let shift_linked_params mib1 mib2 (lnk1:linked_var array) (lnk2:linked_var array exception NoMerge -let rec merge_app (loc1, c1) (loc2, c2) id1 id2 shift filter_shift_stable = +let rec merge_app c1 c2 id1 id2 shift filter_shift_stable = let lnk = Array.append shift.lnk1 shift.lnk2 in - match c1, c2 with + match CAst.(c1.v, c2.v) with | GApp(f1, arr1), GApp(f2,arr2) when isVarf id1 f1 && isVarf id2 f2 -> let _ = prstr "\nICI1!\n" in let args = filter_shift_stable lnk (arr1 @ arr2) in - Loc.tag @@ GApp ((Loc.tag @@ GVar shift.ident) , args) + CAst.make @@ GApp ((CAst.make @@ GVar shift.ident) , args) | GApp(f1, arr1), GApp(f2,arr2) -> raise NoMerge | GLetIn(nme,bdy,typ,trm) , _ -> let _ = prstr "\nICI2!\n" in - let newtrm = merge_app trm (loc2, c2) id1 id2 shift filter_shift_stable in - Loc.tag @@ GLetIn(nme,bdy,typ,newtrm) + let newtrm = merge_app trm c2 id1 id2 shift filter_shift_stable in + CAst.make @@ GLetIn(nme,bdy,typ,newtrm) | _, GLetIn(nme,bdy,typ,trm) -> let _ = prstr "\nICI3!\n" in - let newtrm = merge_app (loc1, c1) trm id1 id2 shift filter_shift_stable in - Loc.tag @@ GLetIn(nme,bdy,typ,newtrm) + let newtrm = merge_app c1 trm id1 id2 shift filter_shift_stable in + CAst.make @@ GLetIn(nme,bdy,typ,newtrm) | _ -> let _ = prstr "\nICI4!\n" in raise NoMerge -let rec merge_app_unsafe (l1, c1) (l2, c2) shift filter_shift_stable = +let rec merge_app_unsafe c1 c2 shift filter_shift_stable = let lnk = Array.append shift.lnk1 shift.lnk2 in - match c1 , c2 with + match CAst.(c1.v, c2.v) with | GApp(f1, arr1), GApp(f2,arr2) -> let args = filter_shift_stable lnk (arr1 @ arr2) in - Loc.tag @@ GApp (Loc.tag @@ GVar shift.ident, args) + CAst.make @@ GApp (CAst.make @@ GVar shift.ident, args) (* FIXME: what if the function appears in the body of the let? *) | GLetIn(nme,bdy,typ,trm) , _ -> let _ = prstr "\nICI2 '!\n" in - let newtrm = merge_app_unsafe trm (l2, c2) shift filter_shift_stable in - Loc.tag @@ GLetIn(nme,bdy,typ,newtrm) + let newtrm = merge_app_unsafe trm c2 shift filter_shift_stable in + CAst.make @@ GLetIn(nme,bdy,typ,newtrm) | _, GLetIn(nme,bdy,typ,trm) -> let _ = prstr "\nICI3 '!\n" in - let newtrm = merge_app_unsafe (l1, c1) trm shift filter_shift_stable in - Loc.tag @@ GLetIn(nme,bdy,typ,newtrm) + let newtrm = merge_app_unsafe c1 trm shift filter_shift_stable in + CAst.make @@ GLetIn(nme,bdy,typ,newtrm) | _ -> let _ = prstr "\nICI4 '!\n" in raise NoMerge @@ -550,14 +550,14 @@ let rec merge_rec_hyps shift accrec filter_shift_stable : (Name.t * glob_constr option * glob_constr option) list = let mergeonehyp t reldecl = match reldecl with - | (nme,x,Some (_, GApp(i,args) as ind)) + | (nme,x,Some ({ CAst.v = GApp(i,args)} as ind)) -> nme,x, Some (merge_app_unsafe ind t shift filter_shift_stable) | (nme,Some _,None) -> error "letins with recursive calls not treated yet" | (nme,None,Some _) -> assert false | (nme,None,None) | (nme,Some _,Some _) -> assert false in match ltyp with | [] -> [] - | (nme,None,Some (_, GApp(f, largs) as t)) :: lt when isVarf ind2name f -> + | (nme,None,Some ({ CAst. v = GApp(f, largs) } as t)) :: lt when isVarf ind2name f -> let rechyps = List.map (mergeonehyp t) accrec in rechyps @ merge_rec_hyps shift accrec lt filter_shift_stable | e::lt -> e :: merge_rec_hyps shift accrec lt filter_shift_stable @@ -573,7 +573,7 @@ let find_app (nme:Id.t) ltyp = (List.map (fun x -> match x with - | _,None,Some (_, GApp(f,_)) when isVarf nme f -> raise (Found 0) + | _,None,Some { CAst.v = GApp(f,_)} when isVarf nme f -> raise (Found 0) | _ -> ()) ltyp); false @@ -632,8 +632,8 @@ let rec merge_types shift accrec1 rechyps , concl | (nme,None, Some t1)as e ::lt1 -> - (match t1 with - | _, GApp(f,carr) when isVarf ind1name f -> + (match t1.CAst.v with + | GApp(f,carr) when isVarf ind1name f -> merge_types shift (e::accrec1) lt1 concl1 ltyp2 concl2 | _ -> let recres, recconcl2 = @@ -864,7 +864,7 @@ let mkProd_reldecl (rdecl:Context.Rel.Declaration.t) (t2:glob_constr) = | LocalAssum (nme,t) -> let t = EConstr.of_constr t in let traw = Detyping.detype false [] (Global.env()) Evd.empty t in - Loc.tag @@ GProd (nme,Explicit,traw,t2) + CAst.make @@ GProd (nme,Explicit,traw,t2) | LocalDef _ -> assert false diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 9e469c756..8c8839944 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -188,15 +188,15 @@ let (value_f:Constr.constr list -> global_reference -> Constr.constr) = in let env = Environ.push_rel_context context (Global.env ()) in let glob_body = - Loc.tag @@ + CAst.make @@ GCases (RegularStyle,None, - [Loc.tag @@ GApp(Loc.tag @@ GRef(fterm,None), List.rev_map (fun x_id -> Loc.tag @@ GVar x_id) rev_x_id_l), + [CAst.make @@ GApp(CAst.make @@ GRef(fterm,None), List.rev_map (fun x_id -> CAst.make @@ GVar x_id) rev_x_id_l), (Anonymous,None)], - [Loc.tag ([v_id], [Loc.tag @@ PatCstr ((destIndRef (delayed_force coq_sig_ref),1), - [Loc.tag @@ PatVar(Name v_id); Loc.tag @@ PatVar Anonymous], + [Loc.tag ([v_id], [CAst.make @@ PatCstr ((destIndRef (delayed_force coq_sig_ref),1), + [CAst.make @@ PatVar(Name v_id); CAst.make @@ PatVar Anonymous], Anonymous)], - Loc.tag @@ GVar v_id)]) + CAst.make @@ GVar v_id)]) in let body = fst (understand env (Evd.from_env env) glob_body)(*FIXME*) in it_mkLambda_or_LetIn body context diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index dc43930e4..9d50b6e6f 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -631,14 +631,14 @@ let subst_var_with_hole occ tid t = let occref = if occ > 0 then ref occ else Find_subterm.error_invalid_occurrence [occ] in let locref = ref 0 in let rec substrec = function - | (_, GVar id) as x -> + | { CAst.v = GVar id } as x -> if Id.equal id tid then (decr occref; if Int.equal !occref 0 then x else (incr locref; - Loc.tag ~loc:(Loc.make_loc (!locref,0)) @@ + CAst.make ~loc:(Loc.make_loc (!locref,0)) @@ GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true), Misctypes.IntroAnonymous, None))) else x @@ -651,12 +651,12 @@ let subst_hole_with_term occ tc t = let locref = ref 0 in let occref = ref occ in let rec substrec = function - | _, GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true),Misctypes.IntroAnonymous,s) -> + | { CAst.v = GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true),Misctypes.IntroAnonymous,s) } -> decr occref; if Int.equal !occref 0 then tc else (incr locref; - Loc.tag ~loc:(Loc.make_loc (!locref,0)) @@ + CAst.make ~loc:(Loc.make_loc (!locref,0)) @@ GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true),Misctypes.IntroAnonymous,s)) | c -> map_glob_constr_left_to_right substrec c in diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4 index 1f40c67b5..b4a0e46ae 100644 --- a/plugins/ltac/g_rewrite.ml4 +++ b/plugins/ltac/g_rewrite.ml4 @@ -123,7 +123,7 @@ TACTIC EXTEND rewrite_strat END let clsubstitute o c = - let is_tac id = match fst (fst (snd c)) with (_, GVar id') when Id.equal id' id -> true | _ -> false in + let is_tac id = match fst (fst (snd c)) with { CAst.v = GVar id'} when Id.equal id' id -> true | _ -> false in Tacticals.onAllHypsAndConcl (fun cl -> match cl with diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 58473d7dd..87b79374e 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -1085,7 +1085,7 @@ type 'a extra_genarg_printer = let strip_prod_binders_glob_constr n (ty,_) = let rec strip_ty acc n ty = if Int.equal n 0 then (List.rev acc, (ty,None)) else - match Loc.obj ty with + match ty.CAst.v with Glob_term.GProd(na,Explicit,a,b) -> strip_ty (([Loc.tag na],(a,None))::acc) (n-1) b | _ -> error "Cannot translate fix tactic: not enough products" in diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 566dd8ed7..8751a14c7 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -108,12 +108,12 @@ 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 (CAst.make @@ CRef (r,None)) + (CAst.make @@ 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 (CAst.make @@ CRef (r,None)) + (CAst.make @@ GVar id), if strict then None else Some (CAst.make @@ CRef (r,None)) | r -> let loc,_ as lqid = qualid_of_reference r in - Loc.tag @@ GRef (locate_global_with_alias lqid,None), + CAst.make @@ GRef (locate_global_with_alias lqid,None), if strict then None else Some (CAst.make @@ CRef (r,None)) let intern_move_location ist = function @@ -272,7 +272,7 @@ let intern_destruction_arg ist = function if !strict_check then (* If in a defined tactic, no intros-until *) match intern_constr ist (CAst.make @@ CRef (Ident (Loc.tag id), None)) with - | (loc, GVar id), _ -> clear,ElimOnIdent (loc,id) + | {loc; CAst.v = GVar id}, _ -> clear,ElimOnIdent (loc,id) | c -> clear,ElimOnConstr (c,NoBindings) else clear,ElimOnIdent (loc,id) @@ -350,7 +350,7 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) = | _ -> Qualid (loc,qualid_of_path (path_of_global (smart_global r))) in let sign = { Constrintern.ltac_vars = ist.ltacvars; Constrintern.ltac_bound = Id.Set.empty } in let c = Constrintern.interp_reference sign r in - match Loc.obj c with + match c.CAst.v with | GRef (r,None) -> Inl (ArgArg (evaluable_of_global_reference ist.genv r,None)) | GVar id -> diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 449027b52..91bc46fe7 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -697,7 +697,7 @@ let interp_typed_pattern ist env sigma (_,c,_) = let interp_constr_in_compound_list inj_fun dest_fun interp_fun ist env sigma l = let try_expand_ltac_var sigma x = try match dest_fun x with - | (_, GVar id), _ -> + | { CAst.v = GVar id }, _ -> let v = Id.Map.find id ist.lfun in sigma, List.map inj_fun (coerce_to_constr_list env v) | _ -> @@ -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 (CAst.make @@ CRef (Ident (loc,id),None))) in + let c = (CAst.make ?loc @@ GVar id,Some (CAst.make @@ CRef (Ident (loc,id),None))) in let f = { delayed = fun env sigma -> let sigma = Sigma.to_evar_map sigma in let (sigma,c) = interp_open_constr ist env sigma c in diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index e2a6ad55c..2b64204c9 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -131,7 +131,7 @@ let closed_term_ast l = let l = List.map (fun gr -> ArgArg(Loc.tag gr)) l in TacFun([Name(Id.of_string"t")], TacML(Loc.tag (tacname, - [TacGeneric (Genarg.in_gen (Genarg.glbwit Stdarg.wit_constr) (Loc.tag @@ GVar(Id.of_string"t"),None)); + [TacGeneric (Genarg.in_gen (Genarg.glbwit Stdarg.wit_constr) (CAst.make @@ GVar(Id.of_string"t"),None)); TacGeneric (Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Stdarg.wit_ref)) l)]))) (* let _ = add_tacdef false ((Loc.ghost,Id.of_string"ring_closed_term" diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index c11c9f83b..9a0dfbf1c 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -158,10 +158,10 @@ let mkCLetIn ?loc name bo t = CAst.make ?loc @@ CLetIn ((Loc.tag ?loc name), bo, None, t) let mkCCast ?loc t ty = CAst.make ?loc @@ CCast (t, dC ty) (** Constructors for rawconstr *) -let mkRHole = Loc.tag @@ GHole (InternalHole, IntroAnonymous, None) -let mkRApp f args = if args = [] then f else Loc.tag @@ GApp (f, args) -let mkRCast rc rt = Loc.tag @@ GCast (rc, dC rt) -let mkRLambda n s t = Loc.tag @@ GLambda (n, Explicit, s, t) +let mkRHole = CAst.make @@ GHole (InternalHole, IntroAnonymous, None) +let mkRApp f args = if args = [] then f else CAst.make @@ GApp (f, args) +let mkRCast rc rt = CAst.make @@ GCast (rc, dC rt) +let mkRLambda n s t = CAst.make @@ GLambda (n, Explicit, s, t) (* ssrterm conbinators *) let combineCG t1 t2 f g = match t1, t2 with @@ -1022,7 +1022,7 @@ type pattern = Evd.evar_map * (constr, constr) ssrpattern 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 + | _,({ v = GRef (VarRef x, _)} ,None) -> Some x | _ -> None let id_of_Cterm t = match id_of_cpattern t with | Some x -> x @@ -1121,9 +1121,10 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty = let eAsXInT e x t = E_As_X_In_T(e,x,t) in let mkG ?(k=' ') x = k,(x,None) in let decode ist t ?reccall f g = + let open CAst in try match (pf_intern_term ist gl t) with - | _, GCast((_, GHole _),CastConv((_, GLambda(Name x,_,_,c)))) -> f x (' ',(c,None)) - | _, GVar id + | { v = GCast({ v = GHole _},CastConv({ v = GLambda(Name x,_,_,c)})) } -> f x (' ',(c,None)) + | { v = GVar id } when Id.Map.mem id ist.lfun && not(Option.is_empty reccall) && not(Option.is_empty wit_ssrpatternarg) -> @@ -1164,18 +1165,18 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty = thin name sigma e) sigma new_evars in sigma in - let red = let rec decode_red (ist,red) = match red with - | T(k,((_, GCast ((_, GHole _),CastConv((_, GLambda (Name id,_,_,t))))),None)) + let red = let rec decode_red (ist,red) = let open CAst in match red with + | T(k,({ v = GCast ({ v = GHole _ },CastConv({ v = GLambda (Name id,_,_,t)}))},None)) when let id = string_of_id id in let len = String.length id in (len > 8 && String.sub id 0 8 = "_ssrpat_") -> let id = string_of_id id in let len = String.length id in (match String.sub id 8 (len - 8), t with - | "In", (_, GApp( _, [t])) -> decodeG t xInT (fun x -> T x) - | "In", (_, GApp( _, [e; t])) -> decodeG t (eInXInT (mkG e)) (bad_enc id) - | "In", (_, GApp( _, [e; t; e_in_t])) -> + | "In", { v = GApp( _, [t]) } -> decodeG t xInT (fun x -> T x) + | "In", { v = GApp( _, [e; t]) } -> decodeG t (eInXInT (mkG e)) (bad_enc id) + | "In", { v = GApp( _, [e; t; e_in_t]) } -> decodeG t (eInXInT (mkG e)) (fun _ -> decodeG e_in_t xInT (fun _ -> assert false)) - | "As", (_, GApp(_, [e; t])) -> decodeG t (eAsXInT (mkG e)) (bad_enc id) + | "As", { v = GApp(_, [e; t]) } -> decodeG t (eAsXInT (mkG e)) (bad_enc id) | _ -> bad_enc id ()) | T t -> decode ist ~reccall:decode_red t xInT (fun x -> T x) | In_T t -> decode ist t inXInT inT @@ -1201,7 +1202,7 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty = pp(lazy(str"typed as: " ++ pr_pattern_w_ids red)); let mkXLetIn ?loc x (a,(g,c)) = match c with | Some b -> a,(g,Some (mkCLetIn ?loc x (mkCHole ?loc) b)) - | None -> a,(Loc.tag ?loc @@ GLetIn (x, Loc.tag ?loc @@ GHole (BinderType x, IntroAnonymous, None), None, g), None) in + | None -> a,(CAst.make ?loc @@ GLetIn (x, CAst.make ?loc @@ GHole (BinderType x, IntroAnonymous, None), None, g), None) in match red with | T t -> let sigma, t = interp_term ist gl t in sigma, T t | In_T t -> let sigma, t = interp_term ist gl t in sigma, In_T t @@ -1374,10 +1375,10 @@ let pf_fill_occ_term gl occ t = let cl,(_,t) = fill_occ_term env concl occ sigma0 t in cl, t -let cpattern_of_id id = ' ', (Loc.tag @@ GRef (VarRef id, None), None) +let cpattern_of_id id = ' ', (CAst.make @@ GRef (VarRef id, None), None) let is_wildcard : cpattern -> bool = function - | _,(_,Some { CAst.v = CHole _ } | (_, GHole _),None) -> true + | _,(_,Some { CAst.v = CHole _ } | { CAst.v = GHole _ } ,None) -> true | _ -> false (* "ssrpattern" *) diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml index ed977c416..e7eea0284 100644 --- a/plugins/syntax/ascii_syntax.ml +++ b/plugins/syntax/ascii_syntax.ml @@ -41,9 +41,9 @@ let interp_ascii ?loc p = let rec aux n p = if Int.equal n 0 then [] else let mp = p mod 2 in - (Loc.tag ?loc @@ GRef ((if Int.equal mp 0 then glob_false else glob_true),None)) + (CAst.make ?loc @@ GRef ((if Int.equal mp 0 then glob_false else glob_true),None)) :: (aux (n-1) (p/2)) in - Loc.tag ?loc @@ GApp (Loc.tag ?loc @@ GRef(force glob_Ascii,None), aux 8 p) + CAst.make ?loc @@ GApp (CAst.make ?loc @@ GRef(force glob_Ascii,None), aux 8 p) let interp_ascii_string ?loc s = let p = @@ -59,12 +59,12 @@ let interp_ascii_string ?loc s = let uninterp_ascii r = let rec uninterp_bool_list n = function | [] when Int.equal n 0 -> 0 - | (_, GRef (k,_))::l when Globnames.eq_gr k glob_true -> 1+2*(uninterp_bool_list (n-1) l) - | (_, GRef (k,_))::l when Globnames.eq_gr k glob_false -> 2*(uninterp_bool_list (n-1) l) + | { CAst.v = GRef (k,_)}::l when Globnames.eq_gr k glob_true -> 1+2*(uninterp_bool_list (n-1) l) + | { CAst.v = GRef (k,_)}::l when Globnames.eq_gr k glob_false -> 2*(uninterp_bool_list (n-1) l) | _ -> raise Non_closed_ascii in try let aux = function - | _, GApp ((_, GRef (k,_)),l) when Globnames.eq_gr k (force glob_Ascii) -> uninterp_bool_list 8 l + | { CAst.v = GApp ({ CAst.v = GRef (k,_)},l) } when Globnames.eq_gr k (force glob_Ascii) -> uninterp_bool_list 8 l | _ -> raise Non_closed_ascii in Some (aux r) with @@ -80,4 +80,4 @@ let _ = Notation.declare_string_interpreter "char_scope" (ascii_path,ascii_module) interp_ascii_string - ([Loc.tag @@ GRef (static_glob_Ascii,None)], uninterp_ascii_string, true) + ([CAst.make @@ GRef (static_glob_Ascii,None)], uninterp_ascii_string, true) diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml index 5cdd82024..9a4cd6c25 100644 --- a/plugins/syntax/nat_syntax.ml +++ b/plugins/syntax/nat_syntax.ml @@ -36,11 +36,11 @@ let warn_large_nat = let nat_of_int ?loc n = if is_pos_or_zero n then begin if less_than threshold n then warn_large_nat (); - let ref_O = Loc.tag ?loc @@ GRef (glob_O, None) in - let ref_S = Loc.tag ?loc @@ GRef (glob_S, None) in + let ref_O = CAst.make ?loc @@ GRef (glob_O, None) in + let ref_S = CAst.make ?loc @@ GRef (glob_S, None) in let rec mk_nat acc n = if n <> zero then - mk_nat (Loc.tag ?loc @@ GApp (ref_S, [acc])) (sub_1 n) + mk_nat (CAst.make ?loc @@ GApp (ref_S, [acc])) (sub_1 n) else acc in @@ -55,8 +55,8 @@ let nat_of_int ?loc n = exception Non_closed_number -let rec int_of_nat x = Loc.with_unloc (function - | GApp ((_, GRef (s,_)),[a]) when Globnames.eq_gr s glob_S -> add_1 (int_of_nat a) +let rec int_of_nat x = CAst.with_val (function + | GApp ({ CAst.v = GRef (s,_) } ,[a]) when Globnames.eq_gr s glob_S -> add_1 (int_of_nat a) | GRef (z,_) when Globnames.eq_gr z glob_O -> zero | _ -> raise Non_closed_number ) x @@ -74,4 +74,4 @@ let _ = Notation.declare_numeral_interpreter "nat_scope" (nat_path,datatypes_module_name) nat_of_int - ([Loc.tag @@ GRef (glob_S,None); Loc.tag @@ GRef (glob_O,None)], uninterp_nat, true) + ([CAst.make @@ GRef (glob_S,None); CAst.make @@ GRef (glob_O,None)], uninterp_nat, true) diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml index 3ee64ba7e..e23852bf8 100644 --- a/plugins/syntax/numbers_syntax.ml +++ b/plugins/syntax/numbers_syntax.ml @@ -87,9 +87,9 @@ exception Non_closed (* parses a *non-negative* integer (from bigint.ml) into an int31 wraps modulo 2^31 *) let int31_of_pos_bigint ?loc n = - let ref_construct = Loc.tag ?loc @@ GRef (int31_construct, None) in - let ref_0 = Loc.tag ?loc @@ GRef (int31_0, None) in - let ref_1 = Loc.tag ?loc @@ GRef (int31_1, None) in + let ref_construct = CAst.make ?loc @@ GRef (int31_construct, None) in + let ref_0 = CAst.make ?loc @@ GRef (int31_0, None) in + let ref_1 = CAst.make ?loc @@ GRef (int31_1, None) in let rec args counter n = if counter <= 0 then [] @@ -97,7 +97,7 @@ let int31_of_pos_bigint ?loc n = let (q,r) = div2_with_rest n in (if r then ref_1 else ref_0)::(args (counter-1) q) in - Loc.tag ?loc @@ GApp (ref_construct, List.rev (args 31 n)) + CAst.make ?loc @@ GApp (ref_construct, List.rev (args 31 n)) let error_negative ?loc = CErrors.user_err ?loc ~hdr:"interp_int31" (Pp.str "int31 are only non-negative numbers.") @@ -114,12 +114,12 @@ let bigint_of_int31 = let rec args_parsing args cur = match args with | [] -> cur - | (_, GRef (b,_))::l when eq_gr b int31_0 -> args_parsing l (mult_2 cur) - | (_, GRef (b,_))::l when eq_gr b int31_1 -> args_parsing l (add_1 (mult_2 cur)) + | { CAst.v = GRef (b,_) }::l when eq_gr b int31_0 -> args_parsing l (mult_2 cur) + | { CAst.v = GRef (b,_) }::l when eq_gr b int31_1 -> args_parsing l (add_1 (mult_2 cur)) | _ -> raise Non_closed in function - | _, GApp ((_, GRef (c, _)), args) when eq_gr c int31_construct -> args_parsing args zero + | { CAst.v = GApp ({ CAst.v = GRef (c, _)}, args) } when eq_gr c int31_construct -> args_parsing args zero | _ -> raise Non_closed let uninterp_int31 i = @@ -132,7 +132,7 @@ let uninterp_int31 i = let _ = Notation.declare_numeral_interpreter int31_scope (int31_path, int31_module) interp_int31 - ([Loc.tag @@ GRef (int31_construct, None)], + ([CAst.make @@ GRef (int31_construct, None)], uninterp_int31, true) @@ -163,16 +163,16 @@ let height bi = (* n must be a non-negative integer (from bigint.ml) *) let word_of_pos_bigint ?loc hght n = - let ref_W0 = Loc.tag ?loc @@ GRef (zn2z_W0, None) in - let ref_WW = Loc.tag ?loc @@ GRef (zn2z_WW, None) in + let ref_W0 = CAst.make ?loc @@ GRef (zn2z_W0, None) in + let ref_WW = CAst.make ?loc @@ GRef (zn2z_WW, None) in let rec decomp hgt n = if hgt <= 0 then int31_of_pos_bigint ?loc n else if equal n zero then - Loc.tag ?loc @@ GApp (ref_W0, [Loc.tag ?loc @@ GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None)]) + CAst.make ?loc @@ GApp (ref_W0, [CAst.make ?loc @@ GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None)]) else let (h,l) = split_at hgt n in - Loc.tag ?loc @@ GApp (ref_WW, [Loc.tag ?loc @@ GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None); + CAst.make ?loc @@ GApp (ref_WW, [CAst.make ?loc @@ GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None); decomp (hgt-1) h; decomp (hgt-1) l]) in @@ -180,13 +180,13 @@ let word_of_pos_bigint ?loc hght n = let bigN_of_pos_bigint ?loc n = let h = height n in - let ref_constructor = Loc.tag ?loc @@ GRef (bigN_constructor h, None) in + let ref_constructor = CAst.make ?loc @@ GRef (bigN_constructor h, None) in let word = word_of_pos_bigint ?loc h n in let args = if h < n_inlined then [word] else [Nat_syntax_plugin.Nat_syntax.nat_of_int ?loc (of_int (h-n_inlined));word] in - Loc.tag ?loc @@ GApp (ref_constructor, args) + CAst.make ?loc @@ GApp (ref_constructor, args) let bigN_error_negative ?loc = CErrors.user_err ?loc ~hdr:"interp_bigN" (Pp.str "bigN are only non-negative numbers.") @@ -203,14 +203,14 @@ let interp_bigN ?loc n = let bigint_of_word = let rec get_height rc = match rc with - | _, GApp ((_, GRef(c,_)), [_;lft;rght]) when eq_gr c zn2z_WW -> + | { CAst.v = GApp ({ CAst.v = GRef(c,_)}, [_;lft;rght]) } when eq_gr c zn2z_WW -> 1+max (get_height lft) (get_height rght) | _ -> 0 in let rec transform hght rc = match rc with - | _, GApp ((_, GRef(c,_)),_) when eq_gr c zn2z_W0-> zero - | _, GApp ((_, GRef(c,_)), [_;lft;rght]) when eq_gr c zn2z_WW-> + | { CAst.v = GApp ({ CAst.v = GRef(c,_)},_)} when eq_gr c zn2z_W0-> zero + | { CAst.v = GApp ({ CAst.v = GRef(c,_)}, [_;lft;rght]) } when eq_gr c zn2z_WW-> let new_hght = hght-1 in add (mult (rank new_hght) (transform new_hght lft)) @@ -223,8 +223,8 @@ let bigint_of_word = let bigint_of_bigN rc = match rc with - | _, GApp (_,[one_arg]) -> bigint_of_word one_arg - | _, GApp (_,[_;second_arg]) -> bigint_of_word second_arg + | { CAst.v = GApp (_,[one_arg]) } -> bigint_of_word one_arg + | { CAst.v = GApp (_,[_;second_arg]) } -> bigint_of_word second_arg | _ -> raise Non_closed let uninterp_bigN rc = @@ -240,7 +240,7 @@ let uninterp_bigN rc = let bigN_list_of_constructors = let rec build i = if i < n_inlined+1 then - (Loc.tag @@ GRef (bigN_constructor i,None))::(build (i+1)) + (CAst.make @@ GRef (bigN_constructor i,None))::(build (i+1)) else [] in @@ -257,17 +257,17 @@ let _ = Notation.declare_numeral_interpreter bigN_scope (*** Parsing for bigZ in digital notation ***) let interp_bigZ ?loc n = - let ref_pos = Loc.tag ?loc @@ GRef (bigZ_pos, None) in - let ref_neg = Loc.tag ?loc @@ GRef (bigZ_neg, None) in + let ref_pos = CAst.make ?loc @@ GRef (bigZ_pos, None) in + let ref_neg = CAst.make ?loc @@ GRef (bigZ_neg, None) in if is_pos_or_zero n then - Loc.tag ?loc @@ GApp (ref_pos, [bigN_of_pos_bigint ?loc n]) + CAst.make ?loc @@ GApp (ref_pos, [bigN_of_pos_bigint ?loc n]) else - Loc.tag ?loc @@ GApp (ref_neg, [bigN_of_pos_bigint ?loc (neg n)]) + CAst.make ?loc @@ GApp (ref_neg, [bigN_of_pos_bigint ?loc (neg n)]) (* pretty printing functions for bigZ *) let bigint_of_bigZ = function - | _, GApp ((_, GRef(c,_)), [one_arg]) when eq_gr c bigZ_pos -> bigint_of_bigN one_arg - | _, GApp ((_, GRef(c,_)), [one_arg]) when eq_gr c bigZ_neg -> + | { CAst.v = GApp ({ CAst.v = GRef(c,_) }, [one_arg])} when eq_gr c bigZ_pos -> bigint_of_bigN one_arg + | { CAst.v = GApp ({ CAst.v = GRef(c,_) }, [one_arg])} when eq_gr c bigZ_neg -> let opp_val = bigint_of_bigN one_arg in if equal opp_val zero then raise Non_closed @@ -286,19 +286,19 @@ let uninterp_bigZ rc = let _ = Notation.declare_numeral_interpreter bigZ_scope (bigZ_path, bigZ_module) interp_bigZ - ([Loc.tag @@ GRef (bigZ_pos, None); - Loc.tag @@ GRef (bigZ_neg, None)], + ([CAst.make @@ GRef (bigZ_pos, None); + CAst.make @@ GRef (bigZ_neg, None)], uninterp_bigZ, true) (*** Parsing for bigQ in digital notation ***) let interp_bigQ ?loc n = - let ref_z = Loc.tag ?loc @@ GRef (bigQ_z, None) in - Loc.tag ?loc @@ GApp (ref_z, [interp_bigZ ?loc n]) + let ref_z = CAst.make ?loc @@ GRef (bigQ_z, None) in + CAst.make ?loc @@ GApp (ref_z, [interp_bigZ ?loc n]) let uninterp_bigQ rc = try match rc with - | _, GApp ((_, GRef(c,_)), [one_arg]) when eq_gr c bigQ_z -> + | { CAst.v = GApp ({ CAst.v = GRef(c,_)}, [one_arg]) } when eq_gr c bigQ_z -> Some (bigint_of_bigZ one_arg) | _ -> None (* we don't pretty-print yet fractions *) with Non_closed -> None @@ -307,5 +307,5 @@ let uninterp_bigQ rc = let _ = Notation.declare_numeral_interpreter bigQ_scope (bigQ_path, bigQ_module) interp_bigQ - ([Loc.tag @@ GRef (bigQ_z, None)], uninterp_bigQ, + ([CAst.make @@ GRef (bigQ_z, None)], uninterp_bigQ, true) diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index b7041d045..7ce066c59 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -42,13 +42,13 @@ let glob_xO = ConstructRef path_of_xO let glob_xH = ConstructRef path_of_xH let pos_of_bignat ?loc x = - let ref_xI = Loc.tag @@ GRef (glob_xI, None) in - let ref_xH = Loc.tag @@ GRef (glob_xH, None) in - let ref_xO = Loc.tag @@ GRef (glob_xO, None) in + let ref_xI = CAst.make @@ GRef (glob_xI, None) in + let ref_xH = CAst.make @@ GRef (glob_xH, None) in + let ref_xO = CAst.make @@ GRef (glob_xO, None) in let rec pos_of x = match div2_with_rest x with - | (q,false) -> Loc.tag @@ GApp (ref_xO,[pos_of q]) - | (q,true) when not (Bigint.equal q zero) -> Loc.tag @@ GApp (ref_xI,[pos_of q]) + | (q,false) -> CAst.make @@ GApp (ref_xO,[pos_of q]) + | (q,true) when not (Bigint.equal q zero) -> CAst.make @@ GApp (ref_xI,[pos_of q]) | (q,true) -> ref_xH in pos_of x @@ -58,9 +58,9 @@ let pos_of_bignat ?loc x = (**********************************************************************) let rec bignat_of_pos = function - | _, GApp ((_, GRef (b,_)),[a]) when Globnames.eq_gr b glob_xO -> mult_2(bignat_of_pos a) - | _, GApp ((_, GRef (b,_)),[a]) when Globnames.eq_gr b glob_xI -> add_1(mult_2(bignat_of_pos a)) - | _, GRef (a, _) when Globnames.eq_gr a glob_xH -> Bigint.one + | { CAst.v = GApp ({ CAst.v = GRef (b,_)},[a]) } when Globnames.eq_gr b glob_xO -> mult_2(bignat_of_pos a) + | { CAst.v = GApp ({ CAst.v = GRef (b,_)},[a]) } when Globnames.eq_gr b glob_xI -> add_1(mult_2(bignat_of_pos a)) + | { CAst.v = GRef (a, _) } when Globnames.eq_gr a glob_xH -> Bigint.one | _ -> raise Non_closed_number (**********************************************************************) @@ -81,18 +81,18 @@ let z_of_int ?loc n = if not (Bigint.equal n zero) then let sgn, n = if is_pos_or_zero n then glob_POS, n else glob_NEG, Bigint.neg n in - Loc.tag @@ GApp(Loc.tag @@ GRef (sgn,None), [pos_of_bignat ?loc n]) + CAst.make @@ GApp(CAst.make @@ GRef (sgn,None), [pos_of_bignat ?loc n]) else - Loc.tag @@ GRef (glob_ZERO, None) + CAst.make @@ GRef (glob_ZERO, None) (**********************************************************************) (* Printing Z via scopes *) (**********************************************************************) let bigint_of_z = function - | _, GApp ((_, GRef (b,_)),[a]) when Globnames.eq_gr b glob_POS -> bignat_of_pos a - | _, GApp ((_, GRef (b,_)),[a]) when Globnames.eq_gr b glob_NEG -> Bigint.neg (bignat_of_pos a) - | _, GRef (a, _) when Globnames.eq_gr a glob_ZERO -> Bigint.zero + | { CAst.v = GApp ({ CAst.v = GRef (b,_)},[a]) } when Globnames.eq_gr b glob_POS -> bignat_of_pos a + | { CAst.v = GApp ({ CAst.v = GRef (b,_)},[a]) } when Globnames.eq_gr b glob_NEG -> Bigint.neg (bignat_of_pos a) + | { CAst.v = GRef (a, _) } when Globnames.eq_gr a glob_ZERO -> Bigint.zero | _ -> raise Non_closed_number (**********************************************************************) @@ -108,14 +108,14 @@ let make_path dir id = Globnames.encode_con dir (Id.of_string id) let glob_IZR = ConstRef (make_path (make_dir rdefinitions) "IZR") let r_of_int ?loc z = - Loc.tag @@ GApp (Loc.tag @@ GRef(glob_IZR,None), [z_of_int ?loc z]) + CAst.make @@ GApp (CAst.make @@ GRef(glob_IZR,None), [z_of_int ?loc z]) (**********************************************************************) (* Printing R via scopes *) (**********************************************************************) let bigint_of_r = function - | _, GApp ((_, GRef (o,_)), [a]) when Globnames.eq_gr o glob_IZR -> + | { CAst.v = GApp ({ CAst.v = GRef (o,_) }, [a]) } when Globnames.eq_gr o glob_IZR -> bigint_of_z a | _ -> raise Non_closed_number @@ -128,6 +128,6 @@ let uninterp_r p = let _ = Notation.declare_numeral_interpreter "R_scope" (r_path,["Coq";"Reals";"Rdefinitions"]) r_of_int - ([Loc.tag @@ GRef (glob_IZR, None)], + ([CAst.make @@ GRef (glob_IZR, None)], uninterp_r, false) diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml index 49cb9355c..b7f13b040 100644 --- a/plugins/syntax/string_syntax.ml +++ b/plugins/syntax/string_syntax.ml @@ -36,8 +36,8 @@ open Lazy let interp_string ?loc s = let le = String.length s in let rec aux n = - if n = le then Loc.tag ?loc @@ GRef (force glob_EmptyString, None) else - Loc.tag ?loc @@ GApp (Loc.tag ?loc @@ GRef (force glob_String, None), + if n = le then CAst.make ?loc @@ GRef (force glob_EmptyString, None) else + CAst.make ?loc @@ GApp (CAst.make ?loc @@ GRef (force glob_String, None), [interp_ascii ?loc (int_of_char s.[n]); aux (n+1)]) in aux 0 @@ -45,11 +45,11 @@ let uninterp_string r = try let b = Buffer.create 16 in let rec aux = function - | _, GApp ((_, GRef (k,_)),[a;s]) when eq_gr k (force glob_String) -> + | { CAst.v = GApp ({ CAst.v = GRef (k,_) },[a;s]) } when eq_gr k (force glob_String) -> (match uninterp_ascii a with | Some c -> Buffer.add_char b (Char.chr c); aux s | _ -> raise Non_closed_string) - | _, GRef (z,_) when eq_gr z (force glob_EmptyString) -> + | { CAst.v = GRef (z,_) } when eq_gr z (force glob_EmptyString) -> Some (Buffer.contents b) | _ -> raise Non_closed_string @@ -61,6 +61,6 @@ let _ = Notation.declare_string_interpreter "string_scope" (string_path,["Coq";"Strings";"String"]) interp_string - ([Loc.tag @@ GRef (static_glob_String,None); - Loc.tag @@ GRef (static_glob_EmptyString,None)], + ([CAst.make @@ GRef (static_glob_String,None); + CAst.make @@ GRef (static_glob_EmptyString,None)], uninterp_string, true) diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml index 96c1f3e39..479448e06 100644 --- a/plugins/syntax/z_syntax.ml +++ b/plugins/syntax/z_syntax.ml @@ -45,13 +45,13 @@ let glob_xO = ConstructRef path_of_xO let glob_xH = ConstructRef path_of_xH let pos_of_bignat ?loc x = - let ref_xI = Loc.tag ?loc @@ GRef (glob_xI, None) in - let ref_xH = Loc.tag ?loc @@ GRef (glob_xH, None) in - let ref_xO = Loc.tag ?loc @@ GRef (glob_xO, None) in + let ref_xI = CAst.make ?loc @@ GRef (glob_xI, None) in + let ref_xH = CAst.make ?loc @@ GRef (glob_xH, None) in + let ref_xO = CAst.make ?loc @@ GRef (glob_xO, None) in let rec pos_of x = match div2_with_rest x with - | (q,false) -> Loc.tag ?loc @@ GApp (ref_xO,[pos_of q]) - | (q,true) when not (Bigint.equal q zero) -> Loc.tag ?loc @@ GApp (ref_xI,[pos_of q]) + | (q,false) -> CAst.make ?loc @@ GApp (ref_xO,[pos_of q]) + | (q,true) when not (Bigint.equal q zero) -> CAst.make ?loc @@ GApp (ref_xI,[pos_of q]) | (q,true) -> ref_xH in pos_of x @@ -68,11 +68,12 @@ let interp_positive ?loc n = (* Printing positive via scopes *) (**********************************************************************) -let rec bignat_of_pos = function - | _, GApp ((_, GRef (b,_)),[a]) when Globnames.eq_gr b glob_xO -> mult_2(bignat_of_pos a) - | _, GApp ((_, GRef (b,_)),[a]) when Globnames.eq_gr b glob_xI -> add_1(mult_2(bignat_of_pos a)) - | _, GRef (a, _) when Globnames.eq_gr a glob_xH -> Bigint.one +let rec bignat_of_pos x = CAst.with_val (function + | GApp ({ CAst.v = GRef (b,_) },[a]) when Globnames.eq_gr b glob_xO -> mult_2(bignat_of_pos a) + | GApp ({ CAst.v = GRef (b,_) },[a]) when Globnames.eq_gr b glob_xI -> add_1(mult_2(bignat_of_pos a)) + | GRef (a, _) when Globnames.eq_gr a glob_xH -> Bigint.one | _ -> raise Non_closed_number + ) x let uninterp_positive p = try @@ -87,9 +88,9 @@ let uninterp_positive p = let _ = Notation.declare_numeral_interpreter "positive_scope" (positive_path,binnums) interp_positive - ([Loc.tag @@ GRef (glob_xI, None); - Loc.tag @@ GRef (glob_xO, None); - Loc.tag @@ GRef (glob_xH, None)], + ([CAst.make @@ GRef (glob_xI, None); + CAst.make @@ GRef (glob_xO, None); + CAst.make @@ GRef (glob_xH, None)], uninterp_positive, true) @@ -106,9 +107,9 @@ let glob_Npos = ConstructRef path_of_Npos let n_path = make_path binnums "N" -let n_of_binnat ?loc pos_or_neg n = Loc.tag ?loc @@ +let n_of_binnat ?loc pos_or_neg n = CAst.make ?loc @@ if not (Bigint.equal n zero) then - GApp(Loc.tag @@ GRef (glob_Npos,None), [pos_of_bignat ?loc n]) + GApp(CAst.make @@ GRef (glob_Npos,None), [pos_of_bignat ?loc n]) else GRef(glob_N0, None) @@ -123,10 +124,11 @@ let n_of_int ?loc n = (* Printing N via scopes *) (**********************************************************************) -let bignat_of_n = function - | _, GApp ((_, GRef (b,_)),[a]) when Globnames.eq_gr b glob_Npos -> bignat_of_pos a - | _, GRef (a,_) when Globnames.eq_gr a glob_N0 -> Bigint.zero +let bignat_of_n = CAst.with_val (function + | GApp ({ CAst.v = GRef (b,_)},[a]) when Globnames.eq_gr b glob_Npos -> bignat_of_pos a + | GRef (a,_) when Globnames.eq_gr a glob_N0 -> Bigint.zero | _ -> raise Non_closed_number + ) let uninterp_n p = try Some (bignat_of_n p) @@ -138,8 +140,8 @@ let uninterp_n p = let _ = Notation.declare_numeral_interpreter "N_scope" (n_path,binnums) n_of_int - ([Loc.tag @@ GRef (glob_N0, None); - Loc.tag @@ GRef (glob_Npos, None)], + ([CAst.make @@ GRef (glob_N0, None); + CAst.make @@ GRef (glob_Npos, None)], uninterp_n, true) @@ -161,19 +163,20 @@ let z_of_int ?loc n = if not (Bigint.equal n zero) then let sgn, n = if is_pos_or_zero n then glob_POS, n else glob_NEG, Bigint.neg n in - Loc.tag ?loc @@ GApp(Loc.tag ?loc @@ GRef(sgn,None), [pos_of_bignat ?loc n]) + CAst.make ?loc @@ GApp(CAst.make ?loc @@ GRef(sgn,None), [pos_of_bignat ?loc n]) else - Loc.tag ?loc @@ GRef(glob_ZERO, None) + CAst.make ?loc @@ GRef(glob_ZERO, None) (**********************************************************************) (* Printing Z via scopes *) (**********************************************************************) -let bigint_of_z = function - | _, GApp ((_, GRef (b,_)),[a]) when Globnames.eq_gr b glob_POS -> bignat_of_pos a - | _, GApp ((_, GRef (b,_)),[a]) when Globnames.eq_gr b glob_NEG -> Bigint.neg (bignat_of_pos a) - | _, GRef (a, _) when Globnames.eq_gr a glob_ZERO -> Bigint.zero +let bigint_of_z = CAst.with_val (function + | GApp ({ CAst.v = GRef (b,_)},[a]) when Globnames.eq_gr b glob_POS -> bignat_of_pos a + | GApp ({ CAst.v = GRef (b,_)},[a]) when Globnames.eq_gr b glob_NEG -> Bigint.neg (bignat_of_pos a) + | GRef (a, _) when Globnames.eq_gr a glob_ZERO -> Bigint.zero | _ -> raise Non_closed_number + ) let uninterp_z p = try @@ -186,8 +189,8 @@ let uninterp_z p = let _ = Notation.declare_numeral_interpreter "Z_scope" (z_path,binnums) z_of_int - ([Loc.tag @@ GRef (glob_ZERO, None); - Loc.tag @@ GRef (glob_POS, None); - Loc.tag @@ GRef (glob_NEG, None)], + ([CAst.make @@ GRef (glob_ZERO, None); + CAst.make @@ GRef (glob_POS, None); + CAst.make @@ GRef (glob_NEG, None)], uninterp_z, true) diff --git a/pretyping/cases.ml b/pretyping/cases.ml index eb0d01718..3beef7773 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -95,7 +95,7 @@ let msg_may_need_inversion () = (* Utils *) let make_anonymous_patvars n = - List.make n (Loc.tag @@ PatVar Anonymous) + List.make n (CAst.make @@ PatVar Anonymous) (* We have x1:t1...xn:tn,xi':ti,y1..yk |- c and re-generalize over xi:ti to get x1:t1...xn:tn,xi':ti,y1..yk |- c[xi:=xi'] *) @@ -178,7 +178,7 @@ and build_glob_pattern args = function | Top -> args | MakeConstructor (pci, rh) -> glob_pattern_of_partial_history - [Loc.tag @@ PatCstr (pci, args, Anonymous)] rh + [CAst.make @@ PatCstr (pci, args, Anonymous)] rh let complete_history = glob_pattern_of_partial_history [] @@ -188,12 +188,12 @@ let pop_history_pattern = function | Continuation (0, l, Top) -> Result (List.rev l) | Continuation (0, l, MakeConstructor (pci, rh)) -> - feed_history (Loc.tag @@ PatCstr (pci,List.rev l,Anonymous)) rh + feed_history (CAst.make @@ PatCstr (pci,List.rev l,Anonymous)) rh | _ -> anomaly (Pp.str "Constructor not yet filled with its arguments") let pop_history h = - feed_history (Loc.tag @@ PatVar Anonymous) h + feed_history (CAst.make @@ PatVar Anonymous) h (* Builds a continuation expecting [n] arguments and building [ci] applied to this [n] arguments *) @@ -273,8 +273,8 @@ type 'a pattern_matching_problem = let rec find_row_ind = function [] -> None - | (_, PatVar _) :: l -> find_row_ind l - | (loc, PatCstr(c,_,_)) :: _ -> Some (loc,c) + | { CAst.v = PatVar _ } :: l -> find_row_ind l + | { CAst.v = PatCstr(c,_,_) ; loc } :: _ -> Some (loc,c) let inductive_template evdref env tmloc ind = let indu = evd_comb1 (Evd.fresh_inductive_instance env) evdref ind in @@ -427,7 +427,7 @@ let current_pattern eqn = | pat::_ -> pat | [] -> anomaly (Pp.str "Empty list of patterns") -let alias_of_pat = Loc.with_loc (fun ?loc -> function +let alias_of_pat = CAst.with_val (function | PatVar name -> name | PatCstr(_,_,name) -> name ) @@ -473,13 +473,13 @@ let rec adjust_local_defs ?loc = function | (pat :: pats, LocalAssum _ :: decls) -> pat :: adjust_local_defs ?loc (pats,decls) | (pats, LocalDef _ :: decls) -> - (Loc.tag ?loc @@ PatVar Anonymous) :: adjust_local_defs ?loc (pats,decls) + (CAst.make ?loc @@ PatVar Anonymous) :: adjust_local_defs ?loc (pats,decls) | [], [] -> [] | _ -> raise NotAdjustable let check_and_adjust_constructor env ind cstrs = function - | _, PatVar _ as pat -> pat - | loc, PatCstr (((_,i) as cstr),args,alias) as pat -> + | { CAst.v = PatVar _ } as pat -> pat + | { CAst.v = PatCstr (((_,i) as cstr),args,alias) ; loc } as pat -> (* Check it is constructor of the right type *) let ind' = inductive_of_constructor cstr in if eq_ind ind' ind then @@ -490,7 +490,7 @@ let check_and_adjust_constructor env ind cstrs = function else try let args' = adjust_local_defs ?loc (args, List.rev ci.cs_args) - in Loc.tag ?loc @@ PatCstr (cstr, args', alias) + in CAst.make ?loc @@ PatCstr (cstr, args', alias) with NotAdjustable -> error_wrong_numarg_constructor ?loc env cstr nb_args_constr else @@ -503,8 +503,8 @@ let check_and_adjust_constructor env ind cstrs = function let check_all_variables env sigma typ mat = List.iter (fun eqn -> match current_pattern eqn with - | _, PatVar id -> () - | loc, PatCstr (cstr_sp,_,_) -> + | { CAst.v = PatVar id } -> () + | { CAst.v = PatCstr (cstr_sp,_,_); loc } -> error_bad_pattern ?loc env sigma cstr_sp typ) mat @@ -530,8 +530,8 @@ let occur_in_rhs na rhs = | Name id -> Id.List.mem id rhs.rhs_vars let is_dep_patt_in eqn = function - | _, PatVar name -> Flags.is_program_mode () || occur_in_rhs name eqn.rhs - | _, PatCstr _ -> true + | { CAst.v = PatVar name } -> Flags.is_program_mode () || occur_in_rhs name eqn.rhs + | { CAst.v = PatCstr _ } -> true let mk_dep_patt_row (pats,_,eqn) = List.map (is_dep_patt_in eqn) pats @@ -751,7 +751,7 @@ let recover_and_adjust_alias_names names sign = | x::names, LocalAssum (_,t)::sign -> (x, LocalAssum (alias_of_pat x,t)) :: aux (names,sign) | names, (LocalDef (na,_,_) as decl)::sign -> - (Loc.tag @@ PatVar na, decl) :: aux (names,sign) + (CAst.make @@ PatVar na, decl) :: aux (names,sign) | _ -> assert false in List.split (aux (names,sign)) @@ -968,7 +968,7 @@ let use_unit_judge evd = evd', j let add_assert_false_case pb tomatch = - let pats = List.map (fun _ -> Loc.tag @@ PatVar Anonymous) tomatch in + let pats = List.map (fun _ -> CAst.make @@ PatVar Anonymous) tomatch in let aliasnames = List.map_filter (function Alias _ | NonDepAlias -> Some Anonymous | _ -> None) tomatch in @@ -1166,8 +1166,8 @@ let postprocess_dependencies evd tocheck brs tomatch pred deps cs = (* Sorting equations by constructor *) let rec irrefutable env = function - | _, PatVar name -> true - | _, PatCstr (cstr,args,_) -> + | { CAst.v = PatVar name } -> true + | { CAst.v = PatCstr (cstr,args,_) } -> let ind = inductive_of_constructor cstr in let (_,mip) = Inductive.lookup_mind_specif env ind in let one_constr = Int.equal (Array.length mip.mind_user_lc) 1 in @@ -1188,14 +1188,14 @@ let group_equations pb ind current cstrs mat = let rest = remove_current_pattern eqn in let pat = current_pattern eqn in match check_and_adjust_constructor pb.env ind cstrs pat with - | _, PatVar name -> + | { CAst.v = PatVar name } -> (* This is a default clause that we expand *) for i=1 to Array.length cstrs do let args = make_anonymous_patvars cstrs.(i-1).cs_nargs in brs.(i-1) <- (args, name, rest) :: brs.(i-1) done; if !only_default == None then only_default := Some true - | loc, PatCstr (((_,i)),args,name) -> + | { CAst.v = PatCstr (((_,i)),args,name) ; loc } -> (* This is a regular clause *) only_default := Some false; brs.(i-1) <- (args, name, rest) :: brs.(i-1)) mat () in @@ -1719,16 +1719,16 @@ let build_tycon ?loc env tycon_env s subst tycon extenv evdref t = let build_inversion_problem loc env sigma tms t = let make_patvar t (subst,avoid) = let id = next_name_away (named_hd env sigma t Anonymous) avoid in - Loc.tag @@ PatVar (Name id), ((id,t)::subst, id::avoid) in + CAst.make @@ PatVar (Name id), ((id,t)::subst, id::avoid) in let rec reveal_pattern t (subst,avoid as acc) = match EConstr.kind sigma (whd_all env sigma t) with - | Construct (cstr,u) -> Loc.tag (PatCstr (cstr,[],Anonymous)), acc + | Construct (cstr,u) -> CAst.make (PatCstr (cstr,[],Anonymous)), acc | App (f,v) when isConstruct sigma f -> let cstr,u = destConstruct sigma f in let n = constructor_nrealargs_env env cstr in let l = List.lastn n (Array.to_list v) in let l,acc = List.fold_map' reveal_pattern l acc in - Loc.tag (PatCstr (cstr,l,Anonymous)), acc + CAst.make (PatCstr (cstr,l,Anonymous)), acc | _ -> make_patvar t acc in let rec aux n env acc_sign tms acc = match tms with @@ -1804,7 +1804,7 @@ let build_inversion_problem loc env sigma tms t = (* No need for a catch all clause *) [] else - [ { patterns = List.map (fun _ -> Loc.tag @@ PatVar Anonymous) patl; + [ { patterns = List.map (fun _ -> CAst.make @@ PatVar Anonymous) patl; alias_stack = []; eqn_loc = None; used = ref false; @@ -2059,13 +2059,14 @@ let mk_JMeq evdref typ x typ' y = let mk_JMeq_refl evdref typ x = papp evdref coq_JMeq_refl [| typ; x |] -let hole = Loc.tag @@ +let hole = CAst.make @@ GHole (Evar_kinds.QuestionMark (Evar_kinds.Define false), Misctypes.IntroAnonymous, None) let constr_of_pat env evdref arsign pat avoid = - let rec typ env (ty, realargs) (loc, pat) avoid = - match pat with + let rec typ env (ty, realargs) pat avoid = + let loc = pat.CAst.loc in + match pat.CAst.v with | PatVar name -> let name, avoid = match name with Name n -> name, avoid @@ -2073,7 +2074,7 @@ let constr_of_pat env evdref arsign pat avoid = let previd, id = prime avoid (Name (Id.of_string "wildcard")) in Name id, id :: avoid in - ((Loc.tag ?loc @@ PatVar name), [LocalAssum (name, ty)] @ realargs, mkRel 1, ty, + ((CAst.make ?loc @@ PatVar name), [LocalAssum (name, ty)] @ realargs, mkRel 1, ty, (List.map (fun x -> mkRel 1) realargs), 1, avoid) | PatCstr (((_, i) as cstr),args,alias) -> let cind = inductive_of_constructor cstr in @@ -2104,7 +2105,7 @@ let constr_of_pat env evdref arsign pat avoid = in let args = List.rev args in let patargs = List.rev patargs in - let pat' = Loc.tag ?loc @@ PatCstr (cstr, patargs, alias) in + let pat' = CAst.make ?loc @@ PatCstr (cstr, patargs, alias) in let cstr = mkConstructU (on_snd EInstance.make ci.cs_cstr) in let app = applist (cstr, List.map (lift (List.length sign)) params) in let app = applist (app, args) in @@ -2160,18 +2161,18 @@ let vars_of_ctx sigma ctx = match decl with | LocalDef (na,t',t) when is_topvar sigma t' -> prev, - (Loc.tag @@ GApp ( - (Loc.tag @@ GRef (delayed_force coq_eq_refl_ref, None)), - [hole; Loc.tag @@ GVar prev])) :: vars + (CAst.make @@ GApp ( + (CAst.make @@ GRef (delayed_force coq_eq_refl_ref, None)), + [hole; CAst.make @@ GVar prev])) :: vars | _ -> match RelDecl.get_name decl with Anonymous -> invalid_arg "vars_of_ctx" - | Name n -> n, (Loc.tag @@ GVar n) :: vars) + | Name n -> n, (CAst.make @@ GVar n) :: vars) ctx (Id.of_string "vars_of_ctx_error", []) in List.rev y -let rec is_included (loc_x, x) (loc_y, y) = - match x, y with +let rec is_included x y = + match CAst.(x.v, y.v) with | PatVar _, _ -> true | _, PatVar _ -> true | PatCstr ((_, i), args, alias), PatCstr ((_, i'), args', alias') -> @@ -2289,13 +2290,13 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity = let branch_name = Id.of_string ("program_branch_" ^ (string_of_int !i)) in let branch_decl = LocalDef (Name branch_name, lift !i bbody, lift !i btype) in let branch = - let bref = Loc.tag @@ GVar branch_name in + let bref = CAst.make @@ GVar branch_name in match vars_of_ctx !evdref rhs_rels with [] -> bref - | l -> Loc.tag @@ GApp (bref, l) + | l -> CAst.make @@ GApp (bref, l) in let branch = match ineqs with - Some _ -> Loc.tag @@ GApp (branch, [ hole ]) + Some _ -> CAst.make @@ GApp (branch, [ hole ]) | None -> branch in incr i; diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index acccfc125..a93653f32 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -79,8 +79,8 @@ let apply_pattern_coercion ?loc pat p = List.fold_left (fun pat (co,n) -> let f i = - if i pat::hd,rest) lines) clauses) | _ -> - let pat = Loc.tag @@ PatVar(update_name sigma na rhs) in + let pat = CAst.make @@ PatVar(update_name sigma na rhs) in let mat = align_tree nal isgoal rhs sigma in List.map (fun (hd,rest) -> pat::hd,rest) mat @@ -329,7 +329,7 @@ let is_nondep_branch sigma c l = let extract_nondep_branches test c b l = let rec strip l r = - match snd r,l with + match r.CAst.v, l with | r', [] -> r | GLambda (_,_,_,t), false::l -> strip l t | GLetIn (_,_,_,t), true::l -> strip l t @@ -339,7 +339,7 @@ let extract_nondep_branches test c b l = let it_destRLambda_or_LetIn_names l c = let rec aux l nal c = - match snd c, l with + match c.CAst.v, l with | _, [] -> (List.rev nal,c) | GLambda (na,_,_,c), false::l -> aux l (na::nal) c | GLetIn (na,_,_,c), true::l -> aux l (na::nal) c @@ -353,11 +353,11 @@ let it_destRLambda_or_LetIn_names l c = x in let x = next (free_glob_vars c) in - let a = Loc.tag @@ GVar x in + let a = CAst.make @@ GVar x in aux l (Name x :: nal) (match c with - | loc, GApp (p,l) -> (loc, GApp (p,l@[a])) - | _ -> Loc.tag @@ GApp (c,[a])) + | { loc; CAst.v = GApp (p,l) } -> CAst.make ?loc @@ GApp (p,l@[a]) + | _ -> CAst.make @@ GApp (c,[a])) in aux l [] c let detype_case computable detype detype_eqns testdep avoid data p c bl = @@ -373,7 +373,7 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl = | None -> Anonymous, None, None | Some p -> let nl,typ = it_destRLambda_or_LetIn_names k p in - let n,typ = match snd typ with + let n,typ = match typ.CAst.v with | GLambda (x,_,t,c) -> x, c | _ -> Anonymous, typ in let aliastyp = @@ -395,7 +395,7 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl = else st with Not_found -> st - in Loc.tag @@ + in match tag, aliastyp with | LetStyle, None -> let bl' = Array.map detype bl in @@ -440,12 +440,12 @@ let detype_instance sigma l = if Univ.Instance.is_empty l then None else Some (List.map (detype_level sigma) (Array.to_list (Univ.Instance.to_array l))) -let rec detype flags avoid env sigma t = Loc.tag @@ +let rec detype flags avoid env sigma t = CAst.make @@ match EConstr.kind sigma (collapse_appl sigma t) with | Rel n -> (try match lookup_name_of_rel n (fst env) with | Name id -> GVar id - | Anonymous -> snd @@ !detype_anonymous n + | Anonymous -> (!detype_anonymous n).CAst.v with Not_found -> let s = "_UNBOUND_REL_"^(string_of_int n) in GVar (Id.of_string s)) @@ -458,7 +458,7 @@ let rec detype flags avoid env sigma t = Loc.tag @@ with Not_found -> GVar id) | Sort s -> GSort (detype_sort sigma (ESorts.kind sigma s)) | Cast (c1,REVERTcast,c2) when not !Flags.raw_print -> - snd (detype flags avoid env sigma c1) + (detype flags avoid env sigma c1).CAst.v | Cast (c1,k,c2) -> let d1 = detype flags avoid env sigma c1 in let d2 = detype flags avoid env sigma c2 in @@ -468,12 +468,12 @@ let rec detype flags avoid env sigma t = Loc.tag @@ | _ -> CastConv d2 in GCast(d1,cast) - | Prod (na,ty,c) -> snd @@ detype_binder flags BProd avoid env sigma na None ty c - | Lambda (na,ty,c) -> snd @@ detype_binder flags BLambda avoid env sigma na None ty c - | LetIn (na,b,ty,c) -> snd @@ detype_binder flags BLetIn avoid env sigma na (Some b) ty c + | Prod (na,ty,c) -> detype_binder flags BProd avoid env sigma na None ty c + | Lambda (na,ty,c) -> detype_binder flags BLambda avoid env sigma na None ty c + | LetIn (na,b,ty,c) -> detype_binder flags BLetIn avoid env sigma na (Some b) ty c | App (f,args) -> let mkapp f' args' = - match snd f' with + match f'.CAst.v with | GApp (f',args'') -> GApp (f',args''@args') | _ -> GApp (f',args') @@ -485,16 +485,16 @@ let rec detype flags avoid env sigma t = Loc.tag @@ let noparams () = let pb = Environ.lookup_projection p (snd env) in let pars = pb.Declarations.proj_npars in - let hole = Loc.tag @@ GHole(Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None) in + let hole = CAst.make @@ GHole(Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None) in let args = List.make pars hole in - GApp (Loc.tag @@ GRef (ConstRef (Projection.constant p), None), + GApp (CAst.make @@ GRef (ConstRef (Projection.constant p), None), (args @ [detype flags avoid env sigma c])) in if fst flags || !Flags.in_debugger || !Flags.in_toplevel then try noparams () with _ -> (* lax mode, used by debug printers only *) - GApp (Loc.tag @@ GRef (ConstRef (Projection.constant p), None), + GApp (CAst.make @@ GRef (ConstRef (Projection.constant p), None), [detype flags avoid env sigma c]) else if print_primproj_compatibility () && Projection.unfolded p then @@ -512,12 +512,12 @@ let rec detype flags avoid env sigma t = Loc.tag @@ substl (c :: List.rev args) body' with Retyping.RetypeError _ | Not_found -> anomaly (str"Cannot detype an unfolded primitive projection.") - in snd @@ detype flags avoid env sigma c' + in (detype flags avoid env sigma c').CAst.v else if print_primproj_params () then try let c = Retyping.expand_projection (snd env) sigma p c [] in - snd @@ detype flags avoid env sigma c + (detype flags avoid env sigma c).CAst.v with Retyping.RetypeError _ -> noparams () else noparams () @@ -552,7 +552,6 @@ let rec detype flags avoid env sigma t = Loc.tag @@ GRef (ConstructRef cstr_sp, detype_instance sigma u) | Case (ci,p,c,bl) -> let comp = computable sigma p (List.length (ci.ci_pp_info.ind_tags)) in - snd @@ detype_case comp (detype flags avoid env sigma) (detype_eqns flags avoid env sigma ci comp) (is_nondep_branch sigma) avoid @@ -643,17 +642,17 @@ and detype_eqns flags avoid env sigma ci computable constructs consnargsl bl = and detype_eqn (lax,isgoal as flags) avoid env sigma constr construct_nargs branch = let make_pat x avoid env b body ty ids = if force_wildcard () && noccurn sigma 1 b then - Loc.tag @@ PatVar Anonymous,avoid,(add_name Anonymous body ty env),ids + CAst.make @@ PatVar Anonymous,avoid,(add_name Anonymous body ty env),ids else let flag = if isgoal then RenamingForGoal else RenamingForCasesPattern (fst env,b) in let na,avoid' = compute_displayed_name_in sigma flag avoid x b in - Loc.tag @@ PatVar na,avoid',(add_name na body ty env),add_vname ids na + CAst.make (PatVar na),avoid',(add_name na body ty env),add_vname ids na in let rec buildrec ids patlist avoid env l b = match EConstr.kind sigma b, l with | _, [] -> Loc.tag @@ (Id.Set.elements ids, - [Loc.tag @@ PatCstr(constr, List.rev patlist,Anonymous)], + [CAst.make @@ PatCstr(constr, List.rev patlist,Anonymous)], detype flags avoid env sigma b) | Lambda (x,t,b), false::l -> let pat,new_avoid,new_env,new_ids = make_pat x avoid env b None t ids in @@ -667,7 +666,7 @@ and detype_eqn (lax,isgoal as flags) avoid env sigma constr construct_nargs bran buildrec ids patlist avoid env l c | _, true::l -> - let pat = Loc.tag @@ PatVar Anonymous in + let pat = CAst.make @@ PatVar Anonymous in buildrec ids (pat::patlist) avoid env l b | _, false::l -> @@ -682,7 +681,7 @@ and detype_eqn (lax,isgoal as flags) avoid env sigma constr construct_nargs bran in buildrec Id.Set.empty [] avoid env construct_nargs branch -and detype_binder (lax,isgoal as flags) bk avoid env sigma na body ty c = Loc.tag @@ +and detype_binder (lax,isgoal as flags) bk avoid env sigma na body ty c = let flag = if isgoal then RenamingForGoal else RenamingElsewhereFor (fst env,c) in let na',avoid' = match bk with | BLetIn -> compute_displayed_let_name_in sigma flag avoid na c @@ -740,7 +739,7 @@ let detype_closed_glob ?lax isgoal avoid env sigma t = | Name id -> Name (convert_id cl id) | Anonymous -> Anonymous in - let rec detype_closed_glob cl cg = Loc.map (function + let rec detype_closed_glob cl cg : Glob_term.glob_constr = CAst.map (function | GVar id -> (* if [id] is bound to a name. *) begin try @@ -754,11 +753,11 @@ let detype_closed_glob ?lax isgoal avoid env sigma t = [Printer.pr_constr_under_binders_env] does. *) let assums = List.map (fun id -> LocalAssum (Name id,(* dummy *) mkProp)) b in let env = push_rel_context assums env in - snd @@ detype ?lax isgoal avoid env sigma c + (detype ?lax isgoal avoid env sigma c).CAst.v (* if [id] is bound to a [closed_glob_constr]. *) with Not_found -> try let {closure;term} = Id.Map.find id cl.untyped in - snd @@ detype_closed_glob closure term + (detype_closed_glob closure term).CAst.v (* Otherwise [id] stands for itself *) with Not_found -> GVar id @@ -785,7 +784,7 @@ let detype_closed_glob ?lax isgoal avoid env sigma t = in GCases(sty,po,tml,eqns) | c -> - snd @@ Glob_ops.map_glob_constr (detype_closed_glob cl) cg + (Glob_ops.map_glob_constr (detype_closed_glob cl) cg).CAst.v ) cg in detype_closed_glob t.closure t.term @@ -793,52 +792,52 @@ let detype_closed_glob ?lax isgoal avoid env sigma t = (**********************************************************************) (* Module substitution: relies on detyping *) -let rec subst_cases_pattern subst (loc, pat) = Loc.tag ?loc @@ - match pat with - | PatVar _ -> pat - | PatCstr (((kn,i),j),cpl,n) -> +let rec subst_cases_pattern subst = CAst.map (function + | PatVar _ as pat -> pat + | PatCstr (((kn,i),j),cpl,n) as pat -> let kn' = subst_mind subst kn and cpl' = List.smartmap (subst_cases_pattern subst) cpl in if kn' == kn && cpl' == cpl then pat else PatCstr (((kn',i),j),cpl',n) + ) let (f_subst_genarg, subst_genarg_hook) = Hook.make () -let rec subst_glob_constr subst (loc, raw) = Loc.tag ?loc @@ - match raw with - | GRef (ref,u) -> +let rec subst_glob_constr subst = CAst.map (function + | GRef (ref,u) as raw -> let ref',t = subst_global subst ref in if ref' == ref then raw else - snd @@ detype false [] (Global.env()) Evd.empty (EConstr.of_constr t) + (detype false [] (Global.env()) Evd.empty (EConstr.of_constr t)).CAst.v - | GVar _ -> raw - | GEvar _ -> raw - | GPatVar _ -> raw + | GSort _ + | GVar _ + | GEvar _ + | GPatVar _ as raw -> raw - | GApp (r,rl) -> + | GApp (r,rl) as raw -> let r' = subst_glob_constr subst r and rl' = List.smartmap (subst_glob_constr subst) rl in if r' == r && rl' == rl then raw else GApp(r',rl') - | GLambda (n,bk,r1,r2) -> + | GLambda (n,bk,r1,r2) as raw -> let r1' = subst_glob_constr subst r1 and r2' = subst_glob_constr subst r2 in if r1' == r1 && r2' == r2 then raw else GLambda (n,bk,r1',r2') - | GProd (n,bk,r1,r2) -> + | GProd (n,bk,r1,r2) as raw -> let r1' = subst_glob_constr subst r1 and r2' = subst_glob_constr subst r2 in if r1' == r1 && r2' == r2 then raw else GProd (n,bk,r1',r2') - | GLetIn (n,r1,t,r2) -> + | GLetIn (n,r1,t,r2) as raw -> let r1' = subst_glob_constr subst r1 in let r2' = subst_glob_constr subst r2 in let t' = Option.smartmap (subst_glob_constr subst) t in if r1' == r1 && t == t' && r2' == r2 then raw else GLetIn (n,r1',t',r2') - | GCases (sty,rtno,rl,branches) -> + | GCases (sty,rtno,rl,branches) as raw -> let rtno' = Option.smartmap (subst_glob_constr subst) rtno and rl' = List.smartmap (fun (a,x as y) -> let a' = subst_glob_constr subst a in @@ -860,14 +859,14 @@ let rec subst_glob_constr subst (loc, raw) = Loc.tag ?loc @@ if rtno' == rtno && rl' == rl && branches' == branches then raw else GCases (sty,rtno',rl',branches') - | GLetTuple (nal,(na,po),b,c) -> + | GLetTuple (nal,(na,po),b,c) as raw -> let po' = Option.smartmap (subst_glob_constr subst) po and b' = subst_glob_constr subst b and c' = subst_glob_constr subst c in if po' == po && b' == b && c' == c then raw else GLetTuple (nal,(na,po'),b',c') - | GIf (c,(na,po),b1,b2) -> + | GIf (c,(na,po),b1,b2) as raw -> let po' = Option.smartmap (subst_glob_constr subst) po and b1' = subst_glob_constr subst b1 and b2' = subst_glob_constr subst b2 @@ -875,7 +874,7 @@ let rec subst_glob_constr subst (loc, raw) = Loc.tag ?loc @@ if c' == c && po' == po && b1' == b1 && b2' == b2 then raw else GIf (c',(na,po'),b1',b2') - | GRec (fix,ida,bl,ra1,ra2) -> + | GRec (fix,ida,bl,ra1,ra2) as raw -> let ra1' = Array.smartmap (subst_glob_constr subst) ra1 and ra2' = Array.smartmap (subst_glob_constr subst) ra2 in let bl' = Array.smartmap @@ -887,9 +886,7 @@ let rec subst_glob_constr subst (loc, raw) = Loc.tag ?loc @@ if ra1' == ra1 && ra2' == ra2 && bl'==bl then raw else GRec (fix,ida,bl',ra1',ra2') - | GSort _ -> raw - - | GHole (knd, naming, solve) -> + | GHole (knd, naming, solve) as raw -> let nknd = match knd with | Evar_kinds.ImplicitArg (ref, i, b) -> let nref, _ = subst_global subst ref in @@ -900,18 +897,19 @@ let rec subst_glob_constr subst (loc, raw) = Loc.tag ?loc @@ if nsolve == solve && nknd == knd then raw else GHole (nknd, naming, nsolve) - | GCast (r1,k) -> + | GCast (r1,k) as raw -> let r1' = subst_glob_constr subst r1 in let k' = Miscops.smartmap_cast_type (subst_glob_constr subst) k in if r1' == r1 && k' == k then raw else GCast (r1',k') + ) (* Utilities to transform kernel cases to simple pattern-matching problem *) let simple_cases_matrix_of_branches ind brs = List.map (fun (i,n,b) -> let nal,c = it_destRLambda_or_LetIn_names n b in - let mkPatVar na = Loc.tag @@ PatVar na in - let p = Loc.tag @@ PatCstr ((ind,i+1),List.map mkPatVar nal,Anonymous) in + let mkPatVar na = CAst.make @@ PatVar na in + let p = CAst.make @@ PatCstr ((ind,i+1),List.map mkPatVar nal,Anonymous) in let map name = try Some (Nameops.out_name name) with Failure _ -> None in let ids = List.map_filter map nal in Loc.tag @@ (ids,[p],c)) diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 84da3652f..da287ae9f 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -35,14 +35,6 @@ val detype_names : bool -> Id.t list -> names_context -> env -> evar_map -> cons val detype : ?lax:bool -> bool -> Id.t list -> env -> evar_map -> constr -> glob_constr -val detype_case : - bool -> (constr -> glob_constr) -> - (constructor array -> bool list array -> constr array -> - (Id.t list * cases_pattern list * glob_constr) Loc.located list) -> - (constr -> bool list -> bool) -> - Id.t list -> inductive * case_style * bool list array * bool list -> - constr option -> constr -> constr array -> glob_constr - val detype_sort : evar_map -> sorts -> glob_sort val detype_rel_context : ?lax:bool -> constr option -> Id.t list -> (names_context * env) -> diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 7e6b063d0..94bc24e3c 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -15,15 +15,15 @@ open Glob_term (* Untyped intermediate terms, after ASTs and before constr. *) -let cases_pattern_loc (loc, _) = loc +let cases_pattern_loc c = c.CAst.loc let cases_predicate_names tml = List.flatten (List.map (function | (tm,(na,None)) -> [na] | (tm,(na,Some (_,(_,nal)))) -> na::nal) tml) -let mkGApp ?loc p t = Loc.tag ?loc @@ - match snd p with +let mkGApp ?loc p t = CAst.make ?loc @@ + match p.CAst.v with | GApp (f,l) -> GApp (f,l@[t]) | _ -> GApp (p,[t]) @@ -45,7 +45,7 @@ let case_style_eq s1 s2 = match s1, s2 with | RegularStyle, RegularStyle -> true | _ -> false -let rec cases_pattern_eq (_loc1, p1) (_loc2, p2) = match p1, p2 with +let rec cases_pattern_eq { CAst.v = p1} { CAst.v = p2 } = match p1, p2 with | PatVar na1, PatVar na2 -> Name.equal na1 na2 | PatCstr (c1, pl1, na1), PatCstr (c2, pl2, na2) -> eq_constructor c1 c2 && List.equal cases_pattern_eq pl1 pl2 && @@ -59,7 +59,7 @@ let cast_type_eq eq t1 t2 = match t1, t2 with | CastNative t1, CastNative t2 -> eq t1 t2 | _ -> false -let rec glob_constr_eq (_loc1, c1) (_loc2, c2) = match c1, c2 with +let rec glob_constr_eq { CAst.v = c1 } { CAst.v = c2 } = match c1, c2 with | GRef (gr1, _), GRef (gr2, _) -> eq_gr gr1 gr2 | GVar id1, GVar id2 -> Id.equal id1 id2 | GEvar (id1, arg1), GEvar (id2, arg2) -> @@ -137,7 +137,7 @@ and fix_recursion_order_eq o1 o2 = match o1, o2 with and instance_eq (x1,c1) (x2,c2) = Id.equal x1 x2 && glob_constr_eq c1 c2 -let map_glob_constr_left_to_right f = Loc.map (function +let map_glob_constr_left_to_right f = CAst.map (function | GApp (g,args) -> let comp1 = f g in let comp2 = Util.List.map_left f args in @@ -186,7 +186,7 @@ let map_glob_constr = map_glob_constr_left_to_right let fold_return_type f acc (na,tyopt) = Option.fold_left f acc tyopt -let fold_glob_constr f acc = Loc.with_unloc (function +let fold_glob_constr f acc = CAst.with_val (function | GVar _ -> acc | GApp (c,args) -> List.fold_left f (f acc c) args | GLambda (_,_,b,c) | GProd (_,_,b,c) -> @@ -221,7 +221,7 @@ let same_id na id = match na with | Name id' -> Id.equal id id' let occur_glob_constr id = - let rec occur gt = Loc.with_unloc (function + let rec occur gt = CAst.with_val (function | GVar (id') -> Id.equal id id' | GApp (f,args) -> (occur f) || (List.exists occur args) | GLambda (na,bk,ty,c) -> @@ -270,7 +270,7 @@ let add_name_to_ids set na = | Name id -> Id.Set.add id set let free_glob_vars = - let rec vars bounded vs = Loc.with_unloc @@ (function + let rec vars bounded vs = CAst.with_val @@ (function | GVar (id') -> if Id.Set.mem id' bounded then vs else Id.Set.add id' vs | GApp (f,args) -> List.fold_left (vars bounded) vs (f::args) | GLambda (na,_,ty,c) | GProd (na,_,ty,c) -> @@ -335,7 +335,7 @@ let free_glob_vars = let glob_visible_short_qualid c = let rec aux acc = function - | _, GRef (c,_) -> + | { CAst.v = GRef (c,_) } -> let qualid = Nametab.shortest_qualid_of_global Id.Set.empty c in let dir,id = Libnames.repr_qualid qualid in if DirPath.is_empty dir then id :: acc else acc @@ -354,10 +354,10 @@ let add_and_check_ident id set = Id.Set.add id set let bound_glob_vars = - let rec vars bound = Loc.with_loc (fun ?loc -> function - | GLambda (na,_,_,_) | GProd (na,_,_,_) | GLetIn (na,_,_,_) as c -> + let rec vars bound c = match c.CAst.v with + | GLambda (na,_,_,_) | GProd (na,_,_,_) | GLetIn (na,_,_,_) -> let bound = name_fold add_and_check_ident na bound in - fold_glob_constr vars bound (loc, c) + fold_glob_constr vars bound c | GCases (sty,rtntypopt,tml,pl) -> let bound = vars_option bound rtntypopt in let bound = @@ -391,8 +391,7 @@ let bound_glob_vars = in Array.fold_left_i vars_fix bound idl | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GVar _) -> bound - | GApp _ | GCast _ as c -> fold_glob_constr vars bound (loc, c) - ) + | GApp _ | GCast _ -> fold_glob_constr vars bound c and vars_pattern bound (loc,(idl,p,c)) = let bound = List.fold_right add_and_check_ident idl bound in @@ -425,7 +424,7 @@ let map_tomatch_binders f ((c,(na,inp)) as x) : tomatch_tuple = if r == inp then x else c,(f na, r) -let rec map_case_pattern_binders f = Loc.map (function +let rec map_case_pattern_binders f = CAst.map (function | PatVar na as x -> let r = f na in if r == na then x @@ -463,7 +462,7 @@ let map_pattern f tomatch branches = List.map (fun tm -> map_tomatch f tm) tomatch, List.map (fun br -> map_cases_branch f br) branches -let loc_of_glob_constr (loc, _) = loc +let loc_of_glob_constr c = c.CAst.loc (**********************************************************************) (* Alpha-renaming *) @@ -495,7 +494,7 @@ let rename_var l id = if List.exists (fun (_,id') -> Id.equal id id') l then raise UnsoundRenaming else id -let rec rename_glob_vars l = Loc.map_with_loc (fun ?loc -> function +let rec rename_glob_vars l c = CAst.map_with_loc (fun ?loc -> function | GVar id as r -> let id' = rename_var l id in if id == id' then r else GVar id' @@ -535,14 +534,13 @@ let rec rename_glob_vars l = Loc.map_with_loc (fun ?loc -> function test_na l na; (na,k,Option.map (rename_glob_vars l) bbd,rename_glob_vars l bty))) decls, Array.map (rename_glob_vars l) bs, Array.map (rename_glob_vars l) ts) - (* XXX: This located use case should be improved. *) - | r -> snd @@ map_glob_constr (rename_glob_vars l) (loc, r) - ) + | _ -> (map_glob_constr (rename_glob_vars l) c).CAst.v + ) c (**********************************************************************) (* Conversion from glob_constr to cases pattern, if possible *) -let rec cases_pattern_of_glob_constr na = Loc.map (function +let rec cases_pattern_of_glob_constr na = CAst.map (function | GVar id -> begin match na with | Name _ -> @@ -552,22 +550,22 @@ let rec cases_pattern_of_glob_constr na = Loc.map (function end | GHole (_,_,_) -> PatVar na | GRef (ConstructRef cstr,_) -> PatCstr (cstr,[],na) - | GApp ((_loc, GRef (ConstructRef cstr,_)),l) -> + | GApp ( { CAst.v = GRef (ConstructRef cstr,_) }, l) -> PatCstr (cstr,List.map (cases_pattern_of_glob_constr Anonymous) l,na) | _ -> raise Not_found ) (* Turn a closed cases pattern into a glob_constr *) -let rec glob_constr_of_closed_cases_pattern_aux x = Loc.map_with_loc (fun ?loc -> function +let rec glob_constr_of_closed_cases_pattern_aux x = CAst.map_with_loc (fun ?loc -> function | PatCstr (cstr,[],Anonymous) -> GRef (ConstructRef cstr,None) | PatCstr (cstr,l,Anonymous) -> - let ref = Loc.tag ?loc @@ GRef (ConstructRef cstr,None) in + let ref = CAst.make ?loc @@ GRef (ConstructRef cstr,None) in GApp (ref, List.map glob_constr_of_closed_cases_pattern_aux l) | _ -> raise Not_found ) x let glob_constr_of_closed_cases_pattern = function - | loc, PatCstr (cstr,l,na) -> - na,glob_constr_of_closed_cases_pattern_aux (loc, PatCstr (cstr,l,Anonymous)) + | { CAst.loc ; v = PatCstr (cstr,l,na) } -> + na,glob_constr_of_closed_cases_pattern_aux (CAst.make ?loc @@ PatCstr (cstr,l,Anonymous)) | _ -> raise Not_found diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 84d846afd..1884b6927 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -324,7 +324,7 @@ let warn_cast_in_pattern = CWarnings.create ~name:"cast-in-pattern" ~category:"automation" (fun () -> Pp.strbrk "Casts are ignored in patterns") -let rec pat_of_raw metas vars = Loc.with_loc (fun ?loc -> function +let rec pat_of_raw metas vars = CAst.with_loc_val (fun ?loc -> function | GVar id -> (try PRel (List.index Name.equal (Name id) vars) with Not_found -> PVar id) @@ -333,7 +333,7 @@ let rec pat_of_raw metas vars = Loc.with_loc (fun ?loc -> function | GRef (gr,_) -> PRef (canonical_gr gr) (* Hack to avoid rewriting a complete interpretation of patterns *) - | GApp ((_, GPatVar (true,n)), cl) -> + | GApp ({ CAst.v = GPatVar (true,n) }, cl) -> metas := n::!metas; PSoApp (n, List.map (pat_of_raw metas vars) cl) | GApp (c,cl) -> PApp (pat_of_raw metas vars c, @@ -362,8 +362,8 @@ let rec pat_of_raw metas vars = Loc.with_loc (fun ?loc -> function PIf (pat_of_raw metas vars c, pat_of_raw metas vars b1,pat_of_raw metas vars b2) | GLetTuple (nal,(_,None),b,c) -> - let mkGLambda c na = Loc.tag ?loc @@ - GLambda (na,Explicit, Loc.tag @@ GHole (Evar_kinds.InternalHole, IntroAnonymous, None),c) in + let mkGLambda c na = CAst.make ?loc @@ + GLambda (na,Explicit, CAst.make @@ GHole (Evar_kinds.InternalHole, IntroAnonymous, None),c) in let c = List.fold_left mkGLambda c nal in let cip = { cip_style = LetStyle; @@ -376,7 +376,7 @@ let rec pat_of_raw metas vars = Loc.with_loc (fun ?loc -> function [0,tags,pat_of_raw metas vars c]) | GCases (sty,p,[c,(na,indnames)],brs) -> let get_ind = function - | (_,(_,[_, PatCstr((ind,_),_,_)],_))::_ -> Some ind + | (_,(_,[{ CAst.v = PatCstr((ind,_),_,_) }],_))::_ -> Some ind | _ -> None in let ind_tags,ind = match indnames with @@ -389,7 +389,7 @@ let rec pat_of_raw metas vars = Loc.with_loc (fun ?loc -> function | Some p, Some (_,(_,nal)) -> let nvars = na :: List.rev nal @ vars in rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas nvars p)) - | (None | Some (_, GHole _)), _ -> PMeta None + | (None | Some { CAst.v = GHole _}), _ -> PMeta None | Some p, None -> user_err ?loc (strbrk "Clause \"in\" expected in patterns over \"match\" expressions with an explicit \"return\" clause.") in @@ -409,15 +409,15 @@ let rec pat_of_raw metas vars = Loc.with_loc (fun ?loc -> function and pats_of_glob_branches loc metas vars ind brs = let get_arg = function - | _, PatVar na -> + | { CAst.v = PatVar na } -> name_iter (fun n -> metas := n::!metas) na; na - | loc, PatCstr(_,_,_) -> err ?loc (Pp.str "Non supported pattern.") + | { CAst.v = PatCstr(_,_,_) ; loc } -> err ?loc (Pp.str "Non supported pattern.") in let rec get_pat indexes = function | [] -> false, [] - | [(_,(_,[_, PatVar(Anonymous)],(_,GHole _)))] -> true, [] (* ends with _ => _ *) - | (_,(_,[_, PatCstr((indsp,j),lv,_)],br)) :: brs -> + | [(_,(_,[{ CAst.v = PatVar Anonymous }], { CAst.v = GHole _}))] -> true, [] (* ends with _ => _ *) + | (_,(_,[{ CAst.v = PatCstr((indsp,j),lv,_) }],br)) :: brs -> let () = match ind with | Some sp when eq_ind sp indsp -> () | _ -> diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index a256eaa5d..76df89a26 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -567,12 +567,13 @@ let (f_genarg_interp, genarg_interp_hook) = Hook.make () (* in environment [env], with existential variables [evdref] and *) (* the type constraint tycon *) -let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdref (lvar : ltac_var_map) (loc, t) = +let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdref (lvar : ltac_var_map) t = let inh_conv_coerce_to_tycon ?loc = inh_conv_coerce_to_tycon ?loc resolve_tc in let pretype_type = pretype_type k0 resolve_tc in let pretype = pretype k0 resolve_tc in let open Context.Rel.Declaration in - match t with + let loc = t.CAst.loc in + match t.CAst.v with | GRef (ref,u) -> inh_conv_coerce_to_tycon ?loc env evdref (pretype_ref ?loc evdref env ref u) @@ -1097,7 +1098,7 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update = (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *) and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function - | loc, GHole (knd, naming, None) -> + | { loc; CAst.v = GHole (knd, naming, None) } -> let rec is_Type c = match EConstr.kind !evdref c with | Sort s -> begin match ESorts.kind !evdref s with diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 8928d83b0..fded0a60b 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -201,19 +201,19 @@ open Decl_kinds keyword "Module" ++ spc() ++ pr_lfqid id ++ str" := " ++ pr_located pr_qualid qid - let rec pr_module_ast leading_space pr_c = function - | loc, CMident qid -> + let rec pr_module_ast leading_space pr_c = let open CAst in function + | { loc ; v = CMident qid } -> if leading_space then spc () ++ pr_located pr_qualid (loc, qid) else pr_located pr_qualid (loc,qid) - | _loc, CMwith (mty,decl) -> + | { v = CMwith (mty,decl) } -> let m = pr_module_ast leading_space pr_c mty in let p = pr_with_declaration pr_c decl in m ++ spc() ++ keyword "with" ++ spc() ++ p - | _loc, CMapply (me1,(_, CMident _ as me2)) -> + | { v = CMapply (me1, ( { v = CMident _ } as me2 ) ) } -> pr_module_ast leading_space pr_c me1 ++ spc() ++ pr_module_ast false pr_c me2 - | _loc, CMapply (me1,me2) -> + | { v = CMapply (me1,me2) } -> pr_module_ast leading_space pr_c me1 ++ spc() ++ hov 1 (str"(" ++ pr_module_ast false pr_c me2 ++ str")") diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 2c331ba56..309691e39 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -253,16 +253,16 @@ open Decl_kinds open Evar_kinds let mkPattern c = snd (Patternops.pattern_of_glob_constr c) -let mkGApp f args = Loc.tag @@ GApp (f, args) -let mkGHole = Loc.tag @@ +let mkGApp f args = CAst.make @@ GApp (f, args) +let mkGHole = CAst.make @@ GHole (QuestionMark (Define false), Misctypes.IntroAnonymous, None) -let mkGProd id c1 c2 = Loc.tag @@ +let mkGProd id c1 c2 = CAst.make @@ GProd (Name (Id.of_string id), Explicit, c1, c2) -let mkGArrow c1 c2 = Loc.tag @@ +let mkGArrow c1 c2 = CAst.make @@ GProd (Anonymous, Explicit, c1, c2) -let mkGVar id = Loc.tag @@ GVar (Id.of_string id) -let mkGPatVar id = Loc.tag @@ GPatVar((false, Id.of_string id)) -let mkGRef r = Loc.tag @@ GRef (Lazy.force r, None) +let mkGVar id = CAst.make @@ GVar (Id.of_string id) +let mkGPatVar id = CAst.make @@ GPatVar((false, Id.of_string id)) +let mkGRef r = CAst.make @@ GRef (Lazy.force r, None) let mkGAppRef r args = mkGApp (mkGRef r) args (** forall x : _, _ x x *) diff --git a/vernac/command.ml b/vernac/command.ml index 12df344c2..cae33f316 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -422,7 +422,7 @@ let prepare_param = function let rec check_anonymous_type ind = let open Glob_term in - match snd ind with + match ind.CAst.v with | GSort (GType []) -> true | GProd ( _, _, _, e) | GLetIn (_, _, _, e) -- cgit v1.2.3