diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 83 | ||||
| -rw-r--r-- | interp/constrintern.ml | 167 | ||||
| -rw-r--r-- | interp/implicit_quantifiers.ml | 4 | ||||
| -rw-r--r-- | interp/modintern.ml | 8 | ||||
| -rw-r--r-- | interp/notation.ml | 18 | ||||
| -rw-r--r-- | interp/notation_ops.ml | 195 |
6 files changed, 241 insertions, 234 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 = |