aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-04-09 03:35:20 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-04-25 00:33:36 +0200
commitee2197096fe75a63b4d92cb3a1bb05122c5c625b (patch)
tree3b40c06375a463625a2675b90e009fcb0b64a7d2
parent054d2736c1c1b55cb7708ff0444af521cd0fe2ba (diff)
[location] [ast] Port module AST to CAst
Diffstat
-rw-r--r--interp/constrextern.ml83
-rw-r--r--interp/constrintern.ml167
-rw-r--r--interp/implicit_quantifiers.ml4
-rw-r--r--interp/modintern.ml8
-rw-r--r--interp/notation.ml18
-rw-r--r--interp/notation_ops.ml195
-rw-r--r--intf/constrexpr.mli2
-rw-r--r--intf/glob_term.mli6
-rw-r--r--parsing/g_vernac.ml410
-rw-r--r--plugins/funind/glob_term_to_relation.ml84
-rw-r--r--plugins/funind/glob_termops.ml146
-rw-r--r--plugins/funind/indfun.ml2
-rw-r--r--plugins/funind/indfun_common.ml4
-rw-r--r--plugins/funind/merge.ml42
-rw-r--r--plugins/funind/recdef.ml10
-rw-r--r--plugins/ltac/extratactics.ml48
-rw-r--r--plugins/ltac/g_rewrite.ml42
-rw-r--r--plugins/ltac/pptactic.ml2
-rw-r--r--plugins/ltac/tacintern.ml10
-rw-r--r--plugins/ltac/tacinterp.ml4
-rw-r--r--plugins/setoid_ring/newring.ml2
-rw-r--r--plugins/ssrmatching/ssrmatching.ml433
-rw-r--r--plugins/syntax/ascii_syntax.ml12
-rw-r--r--plugins/syntax/nat_syntax.ml12
-rw-r--r--plugins/syntax/numbers_syntax.ml64
-rw-r--r--plugins/syntax/r_syntax.ml32
-rw-r--r--plugins/syntax/string_syntax.ml12
-rw-r--r--plugins/syntax/z_syntax.ml59
-rw-r--r--pretyping/cases.ml79
-rw-r--r--pretyping/coercion.ml4
-rw-r--r--pretyping/detyping.ml110
-rw-r--r--pretyping/detyping.mli8
-rw-r--r--pretyping/glob_ops.ml52
-rw-r--r--pretyping/patternops.ml20
-rw-r--r--pretyping/pretyping.ml7
-rw-r--r--printing/ppvernac.ml10
-rw-r--r--tactics/hipattern.ml14
-rw-r--r--vernac/command.ml2
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<n then (Loc.tag ?loc @@ Glob_term.PatVar Anonymous) else pat in
- Loc.tag ?loc @@ Glob_term.PatCstr (co, List.init (n+1) f, Anonymous))
+ if i<n then (CAst.make ?loc @@ Glob_term.PatVar Anonymous) else pat in
+ CAst.make ?loc @@ Glob_term.PatCstr (co, List.init (n+1) f, Anonymous))
pat p
(* raise Not_found if no coercion found *)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 721d1d749..2bfd67f6f 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -283,7 +283,7 @@ let rec decomp_branch tags nal b (avoid,env as e) sigma c =
(avoid', add_name_opt na' body t env) sigma c
let rec build_tree na isgoal e sigma ci cl =
- let mkpat n rhs pl = Loc.tag @@ PatCstr((ci.ci_ind,n+1),pl,update_name sigma na rhs) in
+ let mkpat n rhs pl = CAst.make @@ PatCstr((ci.ci_ind,n+1),pl,update_name sigma na rhs) in
let cnl = ci.ci_pp_info.cstr_tags in
let cna = ci.ci_cstr_nargs in
List.flatten
@@ -306,7 +306,7 @@ and align_tree nal isgoal (e,c as rhs) sigma = match nal with
List.map (fun (hd,rest) -> 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)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 02:19:32 +0000