aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-08-29 19:05:57 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-09-04 11:28:49 +0200
commit1db568d3dc88d538f975377bb4d8d3eecd87872c (patch)
treed8e35952cc8f6111875e664d8884dc2c7f908206 /interp
parent3072bd9d080984833f5eb007bf15c6e9305619e3 (diff)
Making detyping potentially lazy.
The internal detype function takes an additional arguments dictating whether it should be eager or lazy. We introduce a new type of delayed `DAst.t` AST nodes and use it for `glob_constr`. Such type, instead of only containing a value, it can contain a lazy computation too. We use a GADT to discriminate between both uses statically, so that no delayed terms ever happen to be marshalled (which would raise anomalies). We also fix a regression in the test-suite: Mixing laziness and effects is a well-known hell. Here, an exception that was raised for mere control purpose was delayed and raised at a later time as an anomaly. We make the offending function eager.
Diffstat (limited to 'interp')
-rw-r--r--interp/constrextern.ml95
-rw-r--r--interp/constrextern.mli6
-rw-r--r--interp/constrintern.ml338
-rw-r--r--interp/implicit_quantifiers.ml11
-rw-r--r--interp/notation.ml47
-rw-r--r--interp/notation.mli10
-rw-r--r--interp/notation_ops.ml266
-rw-r--r--interp/notation_ops.mli18
-rw-r--r--interp/reserve.ml2
9 files changed, 465 insertions, 328 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index e85415bed..f5eff693f 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -298,7 +298,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) (CAst.make @@ PatVar Anonymous) l
+ Util.List.addn (Inductiveops.inductive_nparamdecls ind) (DAst.make @@ PatVar Anonymous) l
let drop_implicits_in_patt cst nb_expl args =
let impl_st = (implicits_of_global cst) in
@@ -376,6 +376,10 @@ let pattern_printable_in_both_syntax (ind,_ as c) =
(List.for_all is_status_implicit params)&&(List.for_all (fun x -> not (is_status_implicit x)) args)
) impl_st
+let lift f c =
+ let loc = c.CAst.loc in
+ CAst.make ?loc (f ?loc (DAst.get c))
+
(* Better to use extern_glob_constr composed with injection/retraction ?? *)
let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
try
@@ -392,7 +396,7 @@ 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 ->
- CAst.map_with_loc (fun ?loc -> function
+ lift (fun ?loc -> function
| PatVar (Name id) -> CPatAtom (Some (Ident (loc,id)))
| PatVar (Anonymous) -> CPatAtom None
| PatCstr(cstrsp,args,na) ->
@@ -482,7 +486,7 @@ and extern_notation_pattern (tmp_scope,scopes as allscopes) vars t = function
try
if is_inactive_rule keyrule then raise No_match;
let loc = t.loc in
- match t.v with
+ match DAst.get t with
| PatCstr (cstr,_,na) ->
let p = apply_notation_to_pattern ?loc (ConstructRef cstr)
(match_notation_constr_cases_pattern t pat) allscopes vars keyrule in
@@ -645,8 +649,12 @@ let extern_args extern env args =
let map (arg, argscopes) = lazy (extern argscopes env arg) in
List.map map args
-let match_coercion_app = function
- | {loc; v = GApp ({ v = GRef (r,_) },args)} -> Some (loc, r, 0, args)
+let match_coercion_app c = match DAst.get c with
+ | GApp (r, args) ->
+ begin match DAst.get r with
+ | GRef (r,_) -> Some (c.CAst.loc, r, 0, args)
+ | _ -> None
+ end
| _ -> None
let rec remove_coercions inctx c =
@@ -668,14 +676,20 @@ 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 CAst.make ?loc @@ GApp (a',l)
+ if List.is_empty l then a' else DAst.make ?loc @@ GApp (a',l)
| _ -> c
with Not_found -> c)
| _ -> c
-let rec flatten_application = function
- | {loc; v = GApp ({ v = GApp(a,l')},l)} -> flatten_application (CAst.make ?loc @@ GApp (a,l'@l))
- | a -> a
+let rec flatten_application c = match DAst.get c with
+ | GApp (f, l) ->
+ begin match DAst.get f with
+ | GApp(a,l') ->
+ let loc = c.CAst.loc in
+ flatten_application (DAst.make ?loc @@ GApp (a,l'@l))
+ | _ -> c
+ end
+ | a -> c
(**********************************************************************)
(* mapping glob_constr to numerals (in presence of coercions, choose the *)
@@ -702,10 +716,12 @@ 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, { v = GHole ( _, Misctypes.IntroAnonymous, None) } ) -> GLocalDef (p,bk,x,None)
- | (p,bk,Some x,t) -> GLocalDef (p,bk,x,Some t)
+ | (p,bk,Some x, t) ->
+ match DAst.get t with
+ | GHole (_, Misctypes.IntroAnonymous, None) -> GLocalDef (p,bk,x,None)
+ | _ -> GLocalDef (p,bk,x,Some t)
-let extended_glob_local_binder_of_decl ?loc u = CAst.make ?loc (extended_glob_local_binder_of_decl loc u)
+let extended_glob_local_binder_of_decl ?loc u = DAst.make ?loc (extended_glob_local_binder_of_decl loc u)
(**********************************************************************)
(* mapping glob_constr to constr_expr *)
@@ -730,7 +746,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_with_loc (fun ?loc -> function
+ with No_match -> lift (fun ?loc -> function
| GRef (ref,us) ->
extern_global (select_stronger_impargs (implicits_of_global ref))
(extern_reference ?loc vars ref) (extern_universes us)
@@ -749,8 +765,9 @@ let rec extern inctx scopes vars r =
| Evar_kinds.FirstOrderPatVar n -> CEvar (n,[]))
| GApp (f,args) ->
- (match f with
- | {loc = rloc; v = GRef (ref,us) } ->
+ (match DAst.get f with
+ | GRef (ref,us) ->
+ let rloc = f.CAst.loc in
let subscopes = find_arguments_scope ref in
let args = fill_arg_scopes args subscopes (snd scopes) in
begin
@@ -825,8 +842,8 @@ let rec extern inctx scopes vars r =
(cases_predicate_names tml) vars in
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, { v = GVar id } ->
+ let na' = match na, DAst.get tm with
+ | Anonymous, GVar id ->
begin match rtntypopt with
| None -> None
| Some ntn ->
@@ -835,12 +852,12 @@ let rec extern inctx scopes vars r =
else None
end
| Anonymous, _ -> None
- | Name id, { v = GVar id' } when Id.equal id id' -> None
+ | Name id, 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 -> CAst.make @@ PatVar x) nal in
+ let args = List.map (fun x -> DAst.make @@ PatVar x) nal in
let fullargs = add_cpatt_for_params ind args in
extern_ind_pattern_in_scope scopes vars ind fullargs
) x))
@@ -931,14 +948,16 @@ and factorize_lambda inctx scopes vars na bk aty c =
and extern_local_binder scopes vars = function
[] -> ([],[],[])
- | { v = GLocalDef (na,bk,bd,ty)}::l ->
+ | b :: l ->
+ match DAst.get b with
+ | GLocalDef (na,bk,bd,ty) ->
let (assums,ids,l) =
extern_local_binder scopes (Name.fold_right 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)
- | { v = GLocalAssum (na,bk,ty)}::l ->
+ | GLocalAssum (na,bk,ty) ->
let ty = extern_typ scopes vars ty in
(match extern_local_binder scopes (Name.fold_right Id.Set.add na vars) l with
(assums,ids,CLocalAssum(nal,k,ty')::l)
@@ -951,7 +970,7 @@ and extern_local_binder scopes vars = function
(na::assums,na::ids,
CLocalAssum([(Loc.tag na)],Default bk,ty) :: l))
- | { v = GLocalPattern ((p,_),_,bk,ty)}::l ->
+ | GLocalPattern ((p,_),_,bk,ty) ->
let ty =
if !Flags.raw_print then Some (extern_typ scopes vars ty) else None in
let p = extern_cases_pattern vars p in
@@ -969,12 +988,12 @@ and extern_notation (tmp_scope,scopes as allscopes) vars t = function
try
if is_inactive_rule keyrule then raise No_match;
(* Adjusts to the number of arguments expected by the notation *)
- let (t,args,argsscopes,argsimpls) = match t.v ,n with
+ let (t,args,argsscopes,argsimpls) = match DAst.get t ,n with
| GApp (f,args), Some n
when List.length args >= n ->
let args1, args2 = List.chop n args in
let subscopes, impls =
- match f.v with
+ match DAst.get f with
| GRef (ref,us) ->
let subscopes =
try List.skipn n (find_arguments_scope ref)
@@ -987,15 +1006,19 @@ and extern_notation (tmp_scope,scopes as allscopes) vars t = function
subscopes,impls
| _ ->
[], [] in
- (if Int.equal n 0 then f else CAst.make @@ GApp (f,args1)),
+ (if Int.equal n 0 then f else DAst.make @@ GApp (f,args1)),
args2, subscopes, impls
- | GApp ({ v = GRef (ref,us) } as f, args), None ->
+ | GApp (f, args), None ->
+ begin match DAst.get f with
+ | GRef (ref,us) ->
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 -> CAst.make @@ GApp (t,[]), [], [], []
+ | _ -> t, [], [], []
+ end
+ | GRef (ref,us), Some 0 -> DAst.make @@ GApp (t,[]), [], [], []
| _, None -> t, [], [], []
| _ -> raise No_match in
(* Try matching ... *)
@@ -1065,7 +1088,7 @@ let extern_constr_gen lax goal_concl_style scopt env sigma t =
(* those goal/section/rel variables that occurs in the subterm under *)
(* consideration; see namegen.ml for further details *)
let avoid = if goal_concl_style then ids_of_context env else [] in
- let r = Detyping.detype ~lax:lax goal_concl_style avoid env sigma t in
+ let r = Detyping.detype Detyping.Later ~lax:lax goal_concl_style avoid env sigma t in
let vars = vars_of_env env in
extern false (scopt,[]) vars r
@@ -1077,7 +1100,7 @@ let extern_constr ?(lax=false) goal_concl_style env sigma t =
let extern_type goal_concl_style env sigma t =
let avoid = if goal_concl_style then ids_of_context env else [] in
- let r = Detyping.detype goal_concl_style avoid env sigma t in
+ let r = Detyping.detype Detyping.Later goal_concl_style avoid env sigma t in
extern_glob_type (vars_of_env env) r
let extern_sort sigma s = extern_glob_sort (detype_sort sigma s)
@@ -1095,9 +1118,9 @@ let extern_closed_glob ?lax goal_concl_style env sigma t =
let any_any_branch =
(* | _ => _ *)
- Loc.tag ([],[CAst.make @@ PatVar Anonymous], CAst.make @@ GHole (Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None))
+ Loc.tag ([],[DAst.make @@ PatVar Anonymous], DAst.make @@ GHole (Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None))
-let rec glob_of_pat env sigma pat = CAst.make @@ match pat with
+let rec glob_of_pat env sigma pat = DAst.make @@ match pat with
| PRef ref -> GRef (ref,None)
| PVar id -> GVar id
| PEvar (evk,l) ->
@@ -1117,12 +1140,12 @@ let rec glob_of_pat env sigma pat = CAst.make @@ match pat with
GVar id
| PMeta None -> GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous,None)
| PMeta (Some n) -> GPatVar (Evar_kinds.FirstOrderPatVar n)
- | PProj (p,c) -> GApp (CAst.make @@ GRef (ConstRef (Projection.constant p),None),
+ | PProj (p,c) -> GApp (DAst.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 (CAst.make @@ GPatVar (Evar_kinds.SecondOrderPatVar n),
+ GApp (DAst.make @@ GPatVar (Evar_kinds.SecondOrderPatVar 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)
@@ -1154,15 +1177,15 @@ let rec glob_of_pat env sigma pat = CAst.make @@ 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 -> (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
+ | PFix f -> DAst.get (Detyping.detype_names false [] env (Global.env()) sigma (EConstr.of_constr (mkFix f))) (** FIXME bad env *)
+ | PCoFix c -> DAst.get (Detyping.detype_names false [] env (Global.env()) sigma (EConstr.of_constr (mkCoFix c)))
| PSort s -> GSort s
let extern_constr_pattern env sigma pat =
extern true (None,[]) Id.Set.empty (glob_of_pat env sigma pat)
let extern_rel_context where env sigma sign =
- let a = detype_rel_context where [] (names_of_rel_context env,env) sigma sign in
+ let a = detype_rel_context Detyping.Later where [] (names_of_rel_context env,env) sigma sign in
let vars = vars_of_env env in
let a = List.map (extended_glob_local_binder_of_decl) a in
pi3 (extern_local_binder (None,[]) vars a)
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index ffa891c50..593580fb7 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -23,9 +23,9 @@ open Misctypes
(** Translation of pattern, cases pattern, glob_constr and term into syntax
trees for printing *)
-val extern_cases_pattern : Id.Set.t -> cases_pattern -> cases_pattern_expr
-val extern_glob_constr : Id.Set.t -> glob_constr -> constr_expr
-val extern_glob_type : Id.Set.t -> glob_constr -> constr_expr
+val extern_cases_pattern : Id.Set.t -> 'a cases_pattern_g -> cases_pattern_expr
+val extern_glob_constr : Id.Set.t -> 'a glob_constr_g -> constr_expr
+val extern_glob_type : Id.Set.t -> 'a glob_constr_g -> constr_expr
val extern_constr_pattern : names_context -> Evd.evar_map ->
constr_pattern -> constr_expr
val extern_closed_glob : ?lax:bool -> bool -> env -> Evd.evar_map -> closed_glob_constr -> constr_expr
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index e465677cd..6f7c6c827 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -15,7 +15,6 @@ open Namegen
open Libnames
open Globnames
open Impargs
-open CAst
open Glob_term
open Glob_ops
open Patternops
@@ -306,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 (CAst.make ?loc:(Loc.merge_opt loc loc2) @@ GProd (na, bk, t, body))
+ (loc2, (na, bk, t)) :: tl -> it_mkGProd ?loc:loc2 tl (DAst.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 (CAst.make ?loc:(Loc.merge_opt loc loc2) @@ GLambda (na, bk, t, body))
+ (loc2, (na, bk, t)) :: tl -> it_mkGLambda ?loc:loc2 tl (DAst.make ?loc:(Loc.merge_opt loc loc2) @@ GLambda (na, bk, t, body))
| [] -> body
(**********************************************************************)
@@ -323,15 +322,15 @@ let build_impls = function
|Explicit -> fun _ -> None
let impls_type_list ?(args = []) =
- let rec aux acc = function
- | { v = GProd (na,bk,_,c) } -> aux ((build_impls bk na)::acc) c
+ let rec aux acc c = match DAst.get c with
+ | 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
- | { v = GLambda (na,bk,_,c) } -> aux ((build_impls bk na)::acc) c
- | { v = GRec (fix_kind, nas, args, tys, bds) } ->
+ let rec aux acc c = match DAst.get c with
+ | GLambda (na,bk,_,c) -> aux ((build_impls bk na)::acc) c
+ | 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)
@@ -347,14 +346,14 @@ let rec check_capture ty = function
| [] ->
()
-let locate_if_hole ?loc na = function
- | { v = GHole (_,naming,arg) } ->
+let locate_if_hole ?loc na c = match DAst.get c with
+ | 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 -> CAst.make ?loc @@ GHole (Evar_kinds.BinderType na, naming, arg))
- | x -> x
+ with Not_found -> DAst.make ?loc @@ GHole (Evar_kinds.BinderType na, naming, arg))
+ | _ -> c
let reset_hidden_inductive_implicit_test env =
{ env with impls = Id.Map.map (function
@@ -400,7 +399,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, CAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None))))
+ (loc, (Name id, b, DAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None))))
fvs
in
let na = match na with
@@ -433,11 +432,11 @@ let intern_assumption intern lvar env nal bk ty =
let env, b = intern_generalized_binder intern_type lvar env (List.hd nal) b b' t ty in
env, b
-let glob_local_binder_of_extended = CAst.with_loc_val (fun ?loc -> function
+let glob_local_binder_of_extended = DAst.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 = CAst.make ?loc @@ GHole(Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None) in
+ let t = DAst.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.")
@@ -448,13 +447,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)) -> CAst.make ?loc @@ GLocalAssum (na,c,t)) bl' in
+ let bl' = List.map (fun (loc,(na,c,t)) -> DAst.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,
- (CAst.make ?loc @@ GLocalDef (na,Explicit,term,ty)) :: bl)
+ (DAst.make ?loc @@ GLocalDef (na,Explicit,term,ty)) :: bl)
| CLocalPattern (loc,(p,ty)) ->
let tyc =
match ty with
@@ -476,7 +475,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, (CAst.make ?loc @@ GLocalPattern((cp,il),id,bk,t)) :: bl)
+ (env, (DAst.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
@@ -499,12 +498,12 @@ let intern_generalization intern env lvar loc bk ak c =
in
if pi then
(fun (loc', id) 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))
+ DAst.make ?loc:(Loc.merge_opt loc' loc) @@
+ GProd (Name id, bk, DAst.make ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc))
else
(fun (loc', id) 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))
+ DAst.make ?loc:(Loc.merge_opt loc' loc) @@
+ GLambda (Name id, bk, DAst.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
@@ -558,27 +557,34 @@ let make_letins =
(fun a c ->
match a with
| loc, LPLetIn (na,b,t) ->
- CAst.make ?loc @@ GLetIn(na,b,t,c)
+ DAst.make ?loc @@ GLetIn(na,b,t,c)
| loc, LPCases ((cp,il),id) ->
- let tt = (CAst.make ?loc @@ GVar id, (Name id,None)) in
- CAst.make ?loc @@ GCases(Misctypes.LetPatternStyle,None,[tt],[(loc,(il,[cp],c))]))
+ let tt = (DAst.make ?loc @@ GVar id, (Name id,None)) in
+ DAst.make ?loc @@ GCases(Misctypes.LetPatternStyle,None,[tt],[(loc,(il,[cp],c))]))
-let rec subordinate_letins letins = function
+let rec subordinate_letins letins l = match l with
+ | bnd :: l ->
+ let loc = bnd.CAst.loc in
+ begin match DAst.get bnd with
(* binders come in reverse order; the non-let are returned in reverse order together *)
(* with the subordinated let-in in writing order *)
- | { loc; v = GLocalDef (na,_,b,t) }::l ->
+ | GLocalDef (na,_,b,t) ->
subordinate_letins ((Loc.tag ?loc @@ LPLetIn (na,b,t))::letins) l
- | { loc; v = GLocalAssum (na,bk,t)}::l ->
+ | GLocalAssum (na,bk,t) ->
let letins',rest = subordinate_letins [] l in
letins',((loc,(na,bk,t)),letins)::rest
- | { loc; v = GLocalPattern (u,id,bk,t)} :: l ->
+ | GLocalPattern (u,id,bk,t) ->
subordinate_letins ((Loc.tag ?loc @@ LPCases (u,id))::letins)
- ([CAst.make ?loc @@ GLocalAssum (Name id,bk,t)] @ l)
+ ([DAst.make ?loc @@ GLocalAssum (Name id,bk,t)] @ l)
+ end
| [] ->
letins,[]
+let dmap_with_loc f n =
+ CAst.map_with_loc (fun ?loc c -> f ?loc (DAst.get_thunk c)) n
+
let terms_of_binders bl =
- let rec term_of_pat pt = CAst.map_with_loc (fun ?loc -> function
+ let rec term_of_pat pt = dmap_with_loc (fun ?loc -> function
| PatVar (Name id) -> CRef (Ident (loc,id), None)
| PatVar (Anonymous) -> user_err Pp.(str "Cannot turn \"_\" into a term.")
| PatCstr (c,l,_) ->
@@ -586,12 +592,16 @@ let terms_of_binders bl =
let hole = CAst.make ?loc @@ CHole (None,Misctypes.IntroAnonymous,None) in
let params = List.make (Inductiveops.inductive_nparams (fst c)) hole in
CAppExpl ((None,r,None),params @ List.map term_of_pat l)) pt in
- let rec extract_variables = function
- | {loc; 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 -> user_err Pp.(str "Cannot turn \"_\" into a term.")
- | {loc; v = GLocalPattern ((u,_),_,_,_)}::l -> term_of_pat u :: extract_variables l
+ let rec extract_variables l = match l with
+ | bnd :: l ->
+ let loc = bnd.CAst.loc in
+ begin match DAst.get bnd with
+ | GLocalAssum (Name id,_,_) -> (CAst.make ?loc @@ CRef (Ident (loc,id), None)) :: extract_variables l
+ | GLocalDef (Name id,_,_,_) -> extract_variables l
+ | GLocalDef (Anonymous,_,_,_)
+ | GLocalAssum (Anonymous,_,_) -> user_err Pp.(str "Cannot turn \"_\" into a term.")
+ | GLocalPattern ((u,_),_,_,_) -> term_of_pat u :: extract_variables l
+ end
| [] -> [] in
extract_variables bl
@@ -647,7 +657,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
- CAst.make ?loc @@ GHole (knd, naming, arg)
+ DAst.make ?loc @@ GHole (knd, naming, arg)
| NBinderList (x,y,iter,terminator) ->
(try
(* All elements of the list are in scopes (scopt,subscopes) *)
@@ -665,22 +675,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
- CAst.make ?loc @@ GProd (na,bk,t,e)
+ DAst.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
- CAst.make ?loc @@ GLambda (na,bk,t,make_letins letins (aux subst' infos c'))
+ DAst.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 = CAst.make ?loc @@ GHole (Evar_kinds.BinderType na,naming,arg) in
- CAst.make ?loc @@ GProd (na,Explicit,ty,aux subst' subinfos c')
+ let ty = DAst.make ?loc @@ GHole (Evar_kinds.BinderType na,naming,arg) in
+ DAst.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 = CAst.make ?loc @@ GHole (Evar_kinds.BinderType na,naming,arg) in
- CAst.make ?loc @@ GLambda (na,Explicit,ty,aux subst' subinfos c')
+ let ty = DAst.make ?loc @@ GHole (Evar_kinds.BinderType na,naming,arg) in
+ DAst.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
@@ -692,7 +702,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 ->
- CAst.make ?loc (
+ DAst.make ?loc (
try
GVar (Id.Map.find id renaming)
with Not_found ->
@@ -732,7 +742,7 @@ let string_of_ty = function
| Variable -> "var"
let gvar (loc, id) us = match us with
-| None -> CAst.make ?loc @@ GVar id
+| None -> DAst.make ?loc @@ GVar id
| Some _ ->
user_err ?loc (str "Variable " ++ pr_id id ++
str " cannot have a universe instance")
@@ -774,24 +784,27 @@ 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";
- CAst.make ?loc @@ GRef (ref, us), impls, scopes, []
+ DAst.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 c.v with
+ match DAst.get c with
| GRef (ref,_) ->
let impls = implicits_of_global ref in
let scopes = find_arguments_scope ref in
c, impls, scopes, []
- | GApp ({ v = GRef (ref,_) },l)
- when l != [] ->
+ | GApp (r, l) ->
+ begin match DAst.get r with
+ | GRef (ref,_) when l != [] ->
let n = List.length l in
let impls = implicits_of_global ref in
let scopes = find_arguments_scope ref in
c, List.map (drop_first_implicits n) impls,
List.skipn_at_least n scopes,[]
+ | _ -> c,[],[],[]
+ end
| _ -> c,[],[],[]
let error_not_enough_arguments ?loc =
@@ -824,7 +837,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 -> (CAst.make ?loc @@ GRef (ref, us)), true, args
+ | TrueGlobal ref -> (DAst.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
@@ -836,23 +849,32 @@ let intern_qualid loc qid intern env lvar us args =
let infos = (Id.Map.empty, env) in
let projapp = match c with NRef _ -> true | _ -> false in
let c = instantiate_notation_constr loc intern lvar subst infos c in
- let c = match us, c with
- | None, _ -> c
- | 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 _, _ ->
+ let loc = c.CAst.loc in
+ let err () =
user_err ?loc (str "Notation " ++ pr_qualid qid
- ++ str " cannot have a universe instance,"
- ++ str " its expanded head does not start with a reference")
+ ++ str " cannot have a universe instance,"
+ ++ str " its expanded head does not start with a reference")
+ in
+ let c = match us, DAst.get c with
+ | None, _ -> c
+ | Some _, GRef (ref, None) -> DAst.make ?loc @@ GRef (ref, us)
+ | Some _, GApp (r, arg) ->
+ let loc' = r.CAst.loc in
+ begin match DAst.get r with
+ | GRef (ref, None) ->
+ DAst.make ?loc @@ GApp (DAst.make ?loc:loc' @@ GRef (ref, us), arg)
+ | _ -> err ()
+ end
+ | Some _, _ -> err ()
in
c, projapp, args2
(* 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
- | { v = GRef (VarRef _, _) },_,_ -> raise Not_found
- | r -> r
+ let c, _, _ as r = intern_qualid loc qid intern env lvar us args in
+ match DAst.get c with
+ | GRef (VarRef _, _) -> raise Not_found
+ | _ -> r
let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args = function
| Qualid (loc, qid) ->
@@ -888,14 +910,14 @@ let interp_reference vars r =
(** {5 Cases } *)
(** Private internalization patterns *)
-type raw_cases_pattern_expr_r =
- | RCPatAlias of raw_cases_pattern_expr * Id.t
+type 'a raw_cases_pattern_expr_r =
+ | RCPatAlias of 'a raw_cases_pattern_expr * Id.t
| RCPatCstr of Globnames.global_reference
- * raw_cases_pattern_expr list * raw_cases_pattern_expr list
+ * 'a raw_cases_pattern_expr list * 'a raw_cases_pattern_expr list
(** [RCPatCstr (loc, c, l1, l2)] represents ((@c l1) l2) *)
| RCPatAtom of Id.t option
- | RCPatOr of raw_cases_pattern_expr list
-and raw_cases_pattern_expr = raw_cases_pattern_expr_r CAst.t
+ | RCPatOr of 'a raw_cases_pattern_expr list
+and 'a raw_cases_pattern_expr = ('a raw_cases_pattern_expr_r, 'a) DAst.t
(** {6 Elementary bricks } *)
let apply_scope_env env = function
@@ -977,7 +999,7 @@ let insert_local_defs_in_pattern (ind,j) l =
let (decls,_) = decompose_prod_assum typi in
let rec aux decls args =
match decls, args with
- | Context.Rel.Declaration.LocalDef _ :: decls, args -> (CAst.make @@ RCPatAtom None) :: aux decls args
+ | Context.Rel.Declaration.LocalDef _ :: decls, args -> (DAst.make @@ RCPatAtom None) :: aux decls args
| _, [] -> [] (* In particular, if there were trailing local defs, they have been inserted *)
| Context.Rel.Declaration.LocalAssum _ :: decls, a :: args -> a :: aux decls args
| _ -> assert false in
@@ -1013,10 +1035,10 @@ let add_implicits_check_length fail nargs nargs_with_letin impls_st len_pl1 pl2
else Int.equal args_len nargs_with_letin || (fst (fail (nargs - List.length impl_list + i))))
,l)
|imp::q as il,[] -> if is_status_implicit imp && maximal_insertion_of imp
- then let (b,out) = aux i (q,[]) in (b,(CAst.make @@ RCPatAtom None)::out)
+ then let (b,out) = aux i (q,[]) in (b,(DAst.make @@ RCPatAtom None)::out)
else fail (remaining_args (len_pl1+i) il)
|imp::q,(hh::tt as l) -> if is_status_implicit imp
- then let (b,out) = aux i (q,l) in (b,(CAst.make @@ RCPatAtom(None))::out)
+ then let (b,out) = aux i (q,l) in (b,(DAst.make @@ RCPatAtom(None))::out)
else let (b,out) = aux (succ i) (q,tt) in (b,hh::out)
in aux 0 (impl_list,pl2)
@@ -1041,8 +1063,9 @@ 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 { v = PatVar Anonymous } -> ()
- | { loc; v = PatVar _ } | { loc; v = PatCstr(_,_,_) } -> error_parameter_not_implicit ?loc) params;
+ List.iter (fun c -> match DAst.get c with
+ | PatVar Anonymous -> ()
+ | PatVar _ | PatCstr(_,_,_) -> error_parameter_not_implicit ?loc:c.CAst.loc) params;
args
let find_constructor loc add_params ref =
@@ -1062,7 +1085,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, CAst.make @@ PatVar Anonymous)])
+ List.make nb ([], [(Id.Map.empty, DAst.make @@ PatVar Anonymous)])
| None -> []
let find_pattern_variable = function
@@ -1235,15 +1258,23 @@ let product_of_cases_patterns aliases idspl =
List.map (fun (subst',ptail) -> (merge_subst subst subst',p::ptail)) ptaill) pl)))
idspl (aliases.alias_ids,[aliases.alias_map,[]])
-let rec subst_pat_iterator y t = CAst.(map (function
+let rec subst_pat_iterator y t = DAst.(map (function
| RCPatAtom id as p ->
- begin match id with Some x when Id.equal x y -> t.v | _ -> p end
+ begin match id with Some x when Id.equal x y -> DAst.get t | _ -> p end
| RCPatCstr (id,l1,l2) ->
RCPatCstr (id,List.map (subst_pat_iterator y t) l1,
List.map (subst_pat_iterator y t) l2)
| RCPatAlias (p,a) -> RCPatAlias (subst_pat_iterator y t p,a)
| RCPatOr pl -> RCPatOr (List.map (subst_pat_iterator y t) pl)))
+let is_non_zero c = match c with
+| { CAst.v = CPrim (Numeral (p, true)) } -> not (is_zero p)
+| _ -> false
+
+let is_non_zero_pat c = match c with
+| { CAst.v = CPatPrim (Numeral (p, true)) } -> not (is_zero p)
+| _ -> false
+
let drop_notations_pattern looked_for genv =
(* At toplevel, Constructors and Inductives are accepted, in recursive calls
only constructor are allowed *)
@@ -1258,11 +1289,16 @@ let drop_notations_pattern looked_for genv =
if top then looked_for else function ConstructRef _ -> () | _ -> raise Not_found
in
(** [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *)
- let rec rcp_of_glob x = CAst.(map (function
+ let rec rcp_of_glob x = DAst.(map (function
| GVar id -> RCPatAtom (Some id)
| GHole (_,_,_) -> RCPatAtom (None)
| GRef (g,_) -> RCPatCstr (g,[],[])
- | GApp ({ v = GRef (g,_) }, l) -> RCPatCstr (g, List.map rcp_of_glob l,[])
+ | GApp (r, l) ->
+ begin match DAst.get r with
+ | GRef (g,_) -> RCPatCstr (g, List.map rcp_of_glob l,[])
+ | _ ->
+ CErrors.anomaly Pp.(str "Invalid return pattern from Notation.interp_prim_token_cases_pattern_expr.")
+ end
| _ -> CErrors.anomaly Pp.(str "Invalid return pattern from Notation.interp_prim_token_cases_pattern_expr."))) x
in
let rec drop_syndef top scopes re pats =
@@ -1303,25 +1339,25 @@ let drop_notations_pattern looked_for genv =
let open CAst in
let loc = pt.loc in
match pt.v with
- | CPatAlias (p, id) -> CAst.make ?loc @@ RCPatAlias (in_pat top scopes p, id)
+ | CPatAlias (p, id) -> DAst.make ?loc @@ RCPatAlias (in_pat top scopes p, id)
| CPatRecord l ->
let sorted_fields =
sort_fields ~complete:false loc l (fun _idx -> CAst.make ?loc @@ CPatAtom None) in
begin match sorted_fields with
- | None -> CAst.make ?loc @@ RCPatAtom None
+ | None -> DAst.make ?loc @@ RCPatAtom None
| Some (n, head, pl) ->
let pl =
if !asymmetric_patterns then pl else
let pars = List.make n (CAst.make ?loc @@ CPatAtom None) in
List.rev_append pars pl in
match drop_syndef top scopes head pl with
- | Some (a,b,c) -> CAst.make ?loc @@ RCPatCstr(a, b, c)
+ | Some (a,b,c) -> DAst.make ?loc @@ RCPatCstr(a, b, c)
| None -> raise (InternalizationError (loc,NotAConstructor head))
end
| CPatCstr (head, None, pl) ->
begin
match drop_syndef top scopes head pl with
- | Some (a,b,c) -> CAst.make ?loc @@ RCPatCstr(a, b, c)
+ | Some (a,b,c) -> DAst.make ?loc @@ RCPatCstr(a, b, c)
| None -> raise (InternalizationError (loc,NotAConstructor head))
end
| CPatCstr (r, Some expl_pl, pl) ->
@@ -1330,14 +1366,14 @@ let drop_notations_pattern looked_for genv =
raise (InternalizationError (loc,NotAConstructor r)) in
if expl_pl == [] then
(* Convention: (@r) deactivates all further implicit arguments and scopes *)
- CAst.make ?loc @@ RCPatCstr (g, List.map (in_pat false scopes) pl, [])
+ DAst.make ?loc @@ RCPatCstr (g, List.map (in_pat false scopes) pl, [])
else
(* Convention: (@r expl_pl) deactivates implicit arguments in expl_pl and in pl *)
(* but not scopes in expl_pl *)
let (argscs1,_) = find_remaining_scopes expl_pl pl g in
- CAst.make ?loc @@ RCPatCstr (g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat false scopes) pl, [])
- | CPatNotation ("- _",([{ CAst.v = CPatPrim(Numeral (p,true)) }],[]),[])
- when not (is_zero p) ->
+ DAst.make ?loc @@ RCPatCstr (g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat false scopes) pl, [])
+ | CPatNotation ("- _",([a],[]),[]) when is_non_zero_pat a ->
+ let p = match a.CAst.v with CPatPrim (Numeral (p, _)) -> p | _ -> assert false in
let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc (ensure_kind false loc) (Numeral (p,false)) scopes in
rcp_of_glob pat
| CPatNotation ("( _ )",([a],[]),[]) ->
@@ -1358,11 +1394,11 @@ let drop_notations_pattern looked_for genv =
| CPatAtom Some id ->
begin
match drop_syndef top scopes id [] with
- | Some (a,b,c) -> CAst.make ?loc @@ RCPatCstr (a, b, c)
- | None -> CAst.make ?loc @@ RCPatAtom (Some (find_pattern_variable id))
+ | Some (a,b,c) -> DAst.make ?loc @@ RCPatCstr (a, b, c)
+ | None -> DAst.make ?loc @@ RCPatAtom (Some (find_pattern_variable id))
end
- | CPatAtom None -> CAst.make ?loc @@ RCPatAtom None
- | CPatOr pl -> CAst.make ?loc @@ RCPatOr (List.map (in_pat top scopes) pl)
+ | CPatAtom None -> DAst.make ?loc @@ RCPatAtom None
+ | CPatOr pl -> DAst.make ?loc @@ RCPatOr (List.map (in_pat top scopes) pl)
| CPatCast (_,_) ->
(* We raise an error if the pattern contains a cast, due to
current restrictions on casts in patterns. Cast in patterns
@@ -1389,19 +1425,19 @@ let drop_notations_pattern looked_for genv =
let (a,(scopt,subscopes)) = Id.Map.find id subst in
in_pat top (scopt,subscopes@snd scopes) a
with Not_found ->
- if Id.equal id ldots_var then CAst.make ?loc @@ RCPatAtom (Some id) else
+ if Id.equal id ldots_var then DAst.make ?loc @@ RCPatAtom (Some id) else
anomaly (str "Unbound pattern notation variable: " ++ Id.print id ++ str ".")
end
| NRef g ->
ensure_kind top loc g;
let (_,argscs) = find_remaining_scopes [] args g in
- CAst.make ?loc @@ RCPatCstr (g, [], List.map2 (in_pat_sc scopes) argscs args)
+ DAst.make ?loc @@ RCPatCstr (g, [], List.map2 (in_pat_sc scopes) argscs args)
| NApp (NRef g,pl) ->
ensure_kind top loc g;
let (argscs1,argscs2) = find_remaining_scopes pl args g in
let pl = List.map2 (fun x -> in_not false loc (x,snd scopes) fullsubst []) argscs1 pl in
let pl = add_local_defs_and_check_length loc genv g pl args in
- CAst.make ?loc @@ RCPatCstr (g, pl @ List.map (in_pat false scopes) args, [])
+ DAst.make ?loc @@ RCPatCstr (g, pl @ List.map (in_pat false scopes) args, [])
| NList (x,y,iter,terminator,lassoc) ->
if not (List.is_empty args) then user_err ?loc
(strbrk "Application of arguments to a recursive notation not supported in patterns.");
@@ -1418,7 +1454,7 @@ let drop_notations_pattern looked_for genv =
anomaly (Pp.str "Inconsistent substitution of recursive notation."))
| NHole _ ->
let () = assert (List.is_empty args) in
- CAst.make ?loc @@ RCPatAtom None
+ DAst.make ?loc @@ RCPatAtom None
| t -> error_invalid_pattern_notation ?loc ()
in in_pat true
@@ -1427,10 +1463,10 @@ 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 (idslpl1@idslpl2) in
let pl' = List.map (fun (asubst,pl) ->
- (asubst, CAst.make ?loc @@ PatCstr (c,chop_params_pattern loc (fst c) pl with_letin,alias_of aliases))) pll in
+ (asubst, DAst.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
+ match DAst.get pat with
| RCPatAlias (p, id) ->
let aliases' = merge_aliases aliases id in
intern_pat genv aliases' p
@@ -1448,10 +1484,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, CAst.make ?loc @@ PatVar (alias_of aliases)])
+ (aliases.alias_ids,[aliases.alias_map, DAst.make ?loc @@ PatVar (alias_of aliases)])
| RCPatAtom (None) ->
let { alias_ids = ids; alias_map = asubst; } = aliases in
- (ids, [asubst, CAst.make ?loc @@ PatVar (alias_of aliases)])
+ (ids, [asubst, DAst.make ?loc @@ PatVar (alias_of aliases)])
| RCPatOr pl ->
assert (not (List.is_empty pl));
let pl' = List.map (intern_pat genv aliases) pl in
@@ -1475,7 +1511,7 @@ let intern_ind_pattern genv scopes pat =
with InternalizationError(loc,NotAConstructor _) -> error_bad_inductive_type ?loc
in
let loc = no_not.CAst.loc in
- match no_not.CAst.v with
+ match DAst.get no_not with
| RCPatCstr (head, expl_pl, pl) ->
let c = (function IndRef ind -> ind | _ -> error_bad_inductive_type ?loc) head in
let with_letin, pl2 = add_implicits_check_ind_length genv loc c
@@ -1506,9 +1542,18 @@ let merge_impargs l args =
let get_implicit_name n imps =
Some (Impargs.name_of_implicit (List.nth imps (n-1)))
-let set_hole_implicit i b = function
- | {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)
+let set_hole_implicit i b c =
+ let loc = c.CAst.loc in
+ match DAst.get c with
+ | GRef (r, _) -> Loc.tag ?loc (Evar_kinds.ImplicitArg (r,i,b),Misctypes.IntroAnonymous,None)
+ | GApp (r, _) ->
+ let loc = r.CAst.loc in
+ begin match DAst.get r with
+ | GRef (r, _) ->
+ Loc.tag ?loc (Evar_kinds.ImplicitArg (r,i,b),Misctypes.IntroAnonymous,None)
+ | _ -> anomaly (Pp.str "Only refs have implicits.")
+ end
+ | 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 =
@@ -1574,7 +1619,8 @@ let internalize globalenv env pattern_mode (_, 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 | { v = GLocalAssum _ } -> true
+ let n' = Option.map (fun _ -> List.count (fun c -> match DAst.get c with
+ | GLocalAssum _ -> true
| _ -> false (* remove let-ins *))
rbefore) n in
n', ro, List.fold_left intern_local_binder (env',rbefore) after
@@ -1597,7 +1643,7 @@ let internalize globalenv env pattern_mode (_, 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
- CAst.make ?loc @@
+ DAst.make ?loc @@
GRec (GFix
(Array.map (fun (ro,_,_,_) -> ro) idl,n),
Array.of_list lf,
@@ -1624,7 +1670,7 @@ let internalize globalenv env pattern_mode (_, 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
- CAst.make ?loc @@
+ DAst.make ?loc @@
GRec (GCoFix n,
Array.of_list lf,
Array.map (fun (bl,_,_) -> bl) idl,
@@ -1641,11 +1687,11 @@ let internalize globalenv env pattern_mode (_, 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
- CAst.make ?loc @@
+ DAst.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,true)) }],[],[]))
- when not (is_zero p) ->
+ | CNotation ("- _", ([a],[],[])) when is_non_zero a ->
+ let p = match a.CAst.v with CPrim (Numeral (p, _)) -> p | _ -> assert false in
intern env (CAst.make ?loc @@ CPrim (Numeral (p,false)))
| CNotation ("( _ )",([a],[],[])) -> intern env a
| CNotation (ntn,args) ->
@@ -1664,13 +1710,13 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
lvar us args ref
in
(* Rem: GApp(_,f,[]) stands for @f *)
- CAst.make ?loc @@
+ DAst.make ?loc @@
GApp (f, intern_args env args_scopes (List.map fst args))
| CApp ((isproj,f), args) ->
- let f,args = match f with
+ let f,args = match f.CAst.v with
(* Compact notations like "t.(f args') args" *)
- | { CAst.v = CApp ((Some _,f), args') } when not (Option.has_some isproj) ->
+ | CApp ((Some _,f), args') when not (Option.has_some isproj) ->
f,args'@args
(* Don't compact "(f args') args" to resolve implicits separately *)
| _ -> f,args in
@@ -1719,9 +1765,13 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
(Id.Set.union ex_ids as_in_vars) (reset_hidden_inductive_implicit_test env) in
(* PatVars before a real pattern do not need to be matched *)
let stripped_match_from_in =
+ let is_patvar c = match DAst.get c with
+ | PatVar _ -> true
+ | _ -> false
+ in
let rec aux = function
| [] -> []
- | (_, { v = PatVar _}) :: q -> aux q
+ | (_, c) :: q when is_patvar c -> aux q
| l -> l
in aux match_from_in in
let rtnpo = match stripped_match_from_in with
@@ -1730,20 +1780,20 @@ let internalize globalenv env pattern_mode (_, 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 -> (CAst.make @@ GVar id),(Name id,None)) thevars (* "match v1,..,vn" *) in
+ let sub_tms = List.map (fun id -> (DAst.make @@ GVar id),(Name id,None)) thevars (* "match v1,..,vn" *) in
let main_sub_eqn = Loc.tag @@
([],thepats, (* "|p1,..,pn" *)
Option.cata (intern_type env')
- (CAst.make ?loc @@ GHole(Evar_kinds.CasesType false,Misctypes.IntroAnonymous,None))
+ (DAst.make ?loc @@ GHole(Evar_kinds.CasesType false,Misctypes.IntroAnonymous,None))
rtnpo) (* "=> P" if there were a return predicate P, and "=> _" otherwise *) in
let catch_all_sub_eqn =
if List.for_all (irrefutable globalenv) thepats then [] else
- [Loc.tag @@ ([],List.make (List.length thepats) (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))
+ [Loc.tag @@ ([],List.make (List.length thepats) (DAst.make @@ PatVar Anonymous), (* "|_,..,_" *)
+ DAst.make @@ GHole(Evar_kinds.ImpossibleCase,Misctypes.IntroAnonymous,None))] (* "=> _" *) in
+ Some (DAst.make @@ GCases(Term.RegularStyle,sub_rtn,sub_tms,main_sub_eqn::catch_all_sub_eqn))
in
let eqns' = List.map (intern_eqn (List.length tms) env) eqns in
- CAst.make ?loc @@
+ DAst.make ?loc @@
GCases (sty, rtnpo, tms, List.flatten eqns')
| CLetTuple (nal, (na,po), b, c) ->
let env' = reset_tmp_scope env in
@@ -1753,7 +1803,7 @@ let internalize globalenv env pattern_mode (_, 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
- CAst.make ?loc @@
+ DAst.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) ->
@@ -1763,7 +1813,7 @@ let internalize globalenv env pattern_mode (_, 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
- CAst.make ?loc @@
+ DAst.make ?loc @@
GIf (c', (na', p'), intern env b1, intern env b2)
| CHole (k, naming, solve) ->
let k = match k with
@@ -1791,28 +1841,28 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
let (_, glb) = Genintern.generic_intern ist gen in
Some glb
in
- CAst.make ?loc @@
+ DAst.make ?loc @@
GHole (k, naming, solve)
(* Parsing pattern variables *)
| CPatVar n when pattern_mode ->
- CAst.make ?loc @@
+ DAst.make ?loc @@
GPatVar (Evar_kinds.SecondOrderPatVar n)
| CEvar (n, []) when pattern_mode ->
- CAst.make ?loc @@
+ DAst.make ?loc @@
GPatVar (Evar_kinds.FirstOrderPatVar n)
(* end *)
(* Parsing existential variables *)
| CEvar (n, l) ->
- CAst.make ?loc @@
+ DAst.make ?loc @@
GEvar (n, List.map (on_snd (intern env)) l)
| CPatVar _ ->
raise (InternalizationError (loc,IllegalMetavariable))
(* end *)
| CSort s ->
- CAst.make ?loc @@
+ DAst.make ?loc @@
GSort s
| CCast (c1, c2) ->
- CAst.make ?loc @@
+ DAst.make ?loc @@
GCast (intern env c1, Miscops.map_cast_type (intern_type env) c2)
)
and intern_type env = intern (set_type_scope env)
@@ -1850,9 +1900,11 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
(* the "match" part *)
let tm' = intern env tm in
(* the "as" part *)
- let extra_id,na = match tm', na with
- | {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)
+ let extra_id,na =
+ let loc = tm'.CAst.loc in
+ match DAst.get tm', na with
+ | GVar id, None when not (Id.Map.mem id (snd lvar)) -> Some id,(loc,Name id)
+ | GRef (VarRef id, _), None -> Some id,(loc,Name id)
| _, None -> None,(Loc.tag Anonymous)
| _, Some (loc,na) -> None,(loc,na) in
(* the "in" part *)
@@ -1871,21 +1923,25 @@ let internalize globalenv env pattern_mode (_, 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, CAst.make ?loc @@ PatVar x) :: l in
+ | loc,(Name y as x) -> (y, DAst.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; 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 ->
- let fresh =
- Namegen.next_name_away_with_default_using_types "iV" cano_name forbidden_names (EConstr.of_constr ty) in
- canonize_args t tt (fresh::forbidden_names)
- ((fresh,c)::match_acc) ((cases_pattern_loc c,Name fresh)::var_acc)
+ begin match DAst.get c with
+ | PatVar x ->
+ let loc = c.CAst.loc in
+ canonize_args t tt forbidden_names
+ (add_name match_acc (loc,x)) ((loc,x)::var_acc)
+ | _ ->
+ let fresh =
+ Namegen.next_name_away_with_default_using_types "iV" cano_name forbidden_names (EConstr.of_constr ty) in
+ canonize_args t tt (fresh::forbidden_names)
+ ((fresh,c)::match_acc) ((cases_pattern_loc c,Name fresh)::var_acc)
+ end
| _ -> assert false in
let _,args_rel =
List.chop nparams (List.rev mip.Declarations.mind_arity_ctxt) in
@@ -1924,7 +1980,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
(* with implicit arguments if maximal insertion is set *)
[]
else
- (CAst.map_from_loc (fun ?loc (a,b,c) -> GHole(a,b,c))
+ (DAst.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
@@ -1950,9 +2006,11 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
and smart_gapp f loc = function
| [] -> f
- | l -> match f with
- | { 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)
+ | l ->
+ let loc' = f.CAst.loc in
+ match DAst.get f with
+ | GApp (g, args) -> DAst.make ?loc:(Loc.merge_opt loc' loc) @@ GApp (g, args@l)
+ | _ -> DAst.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 e498d979d..cae67c3e7 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -119,13 +119,14 @@ let free_vars_of_binders ?(bound=Id.Set.empty) l (binders : local_binder_expr li
in aux bound l binders
let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.empty) =
- let rec vars bound vs t = match t with
- | { loc; CAst.v = GVar id } ->
+ let rec vars bound vs c = match DAst.get c with
+ | GVar id ->
+ let loc = c.CAst.loc in
if is_freevar bound (Global.env ()) id then
if Id.List.mem_assoc_sym id vs then vs
else (Loc.tag ?loc id) :: vs
else vs
- | c -> Glob_ops.fold_glob_constr_with_binders Id.Set.add vars bound vs c
+ | _ -> Glob_ops.fold_glob_constr_with_binders Id.Set.add vars bound vs c
in fun rt ->
let vars = List.rev (vars bound [] rt) in
List.iter (fun (loc, id) ->
@@ -253,11 +254,11 @@ let implicits_of_glob_constr ?(with_products=true) l =
(ExplByPos (i, name), (true, true, true)) :: l
| _ -> l
in
- let rec aux i { loc; CAst.v = c } =
+ let rec aux i c =
let abs na bk b =
add_impl i na bk (aux (succ i) b)
in
- match c with
+ match DAst.get c with
| GProd (na, bk, t, b) ->
if with_products then abs na bk b
else
diff --git a/interp/notation.ml b/interp/notation.ml
index c373faf68..176ac3bf6 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -265,19 +265,28 @@ let keymap_find key map =
(* Scopes table : interpretation -> scope_name *)
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
- | { CAst.v = GApp ({ CAst.v = GRef (ref,_) } ,_) } | { CAst.v = GRef (ref,_) } -> RefKey (canonical_gr ref)
+let prim_token_key_table = ref (KeyMap.empty : (string * (any_glob_constr -> prim_token option) * bool) KeyMap.t)
+
+let glob_prim_constr_key c = match DAst.get c with
+ | GRef (ref, _) -> RefKey (canonical_gr ref)
+ | GApp (c, _) ->
+ begin match DAst.get c with
+ | GRef (ref, _) -> RefKey (canonical_gr ref)
+ | _ -> Oth
+ end
| _ -> Oth
-let glob_constr_keys = function
- | { CAst.v = GApp ({ CAst.v = GRef (ref,_) },_) } -> [RefKey (canonical_gr ref); Oth]
- | { CAst.v = GRef (ref,_) } -> [RefKey (canonical_gr ref)]
+let glob_constr_keys c = match DAst.get c with
+ | GApp (c, _) ->
+ begin match DAst.get c with
+ | GRef (ref, _) -> [RefKey (canonical_gr ref); Oth]
+ | _ -> [Oth]
+ end
+ | GRef (ref,_) -> [RefKey (canonical_gr ref)]
| _ -> [Oth]
-let cases_pattern_key = function
- | { CAst.v = PatCstr (ref,_,_) } -> RefKey (canonical_gr (ConstructRef ref))
+let cases_pattern_key c = match DAst.get c with
+ | PatCstr (ref,_,_) -> RefKey (canonical_gr (ConstructRef ref))
| _ -> Oth
let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
@@ -300,7 +309,7 @@ type 'a prim_token_interpreter =
type cases_pattern_status = bool (* true = use prim token in patterns *)
type 'a prim_token_uninterpreter =
- glob_constr list * (glob_constr -> 'a option) * cases_pattern_status
+ glob_constr list * (any_glob_constr -> 'a option) * cases_pattern_status
type internal_prim_token_interpreter =
?loc:Loc.t -> prim_token -> required_module * (unit -> glob_constr)
@@ -496,11 +505,15 @@ let interp_prim_token_gen ?loc g p local_scopes =
let interp_prim_token ?loc =
interp_prim_token_gen ?loc (fun _ -> ())
-let rec check_allowed_ref_in_pat looked_for = CAst.(with_val (function
+let rec check_allowed_ref_in_pat looked_for = DAst.(with_val (function
| GVar _ | GHole _ -> ()
| GRef (g,_) -> looked_for g
- | GApp ({ v = GRef (g,_) },l) ->
- looked_for g; List.iter (check_allowed_ref_in_pat looked_for) l
+ | GApp (f, l) ->
+ begin match DAst.get f with
+ | GRef (g, _) ->
+ looked_for g; List.iter (check_allowed_ref_in_pat looked_for) l
+ | _ -> raise Not_found
+ end
| _ -> raise Not_found))
let interp_prim_token_cases_pattern_expr ?loc looked_for p =
@@ -532,7 +545,7 @@ let uninterp_prim_token c =
try
let (sc,numpr,_) =
KeyMap.find (glob_prim_constr_key c) !prim_token_key_table in
- match numpr c with
+ match numpr (AnyGlobConstr c) with
| None -> raise Notation_ops.No_match
| Some n -> (sc,n)
with Not_found -> raise Notation_ops.No_match
@@ -545,8 +558,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 = CAst.make @@ GRef (ref,None) in
- match numpr (CAst.make @@ GApp (ref,args')) with
+ let ref = DAst.make @@ GRef (ref,None) in
+ match numpr (AnyGlobConstr (DAst.make @@ GApp (ref,args'))) with
| None -> raise Notation_ops.No_match
| Some n -> (sc,n)
with Not_found -> raise Notation_ops.No_match
@@ -557,7 +570,7 @@ let uninterp_prim_token_cases_pattern c =
let (sc,numpr,b) = KeyMap.find k !prim_token_key_table in
if not b then raise Notation_ops.No_match;
let na,c = glob_constr_of_closed_cases_pattern c in
- match numpr c with
+ match numpr (AnyGlobConstr c) with
| None -> raise Notation_ops.No_match
| Some n -> (na,sc,n)
with Not_found -> raise Notation_ops.No_match
diff --git a/interp/notation.mli b/interp/notation.mli
index f9f247fe1..75c8d5aa5 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -70,7 +70,7 @@ type 'a prim_token_interpreter =
?loc:Loc.t -> 'a -> glob_constr
type 'a prim_token_uninterpreter =
- glob_constr list * (glob_constr -> 'a option) * cases_pattern_status
+ glob_constr list * (any_glob_constr -> 'a option) * cases_pattern_status
type rawnum = Constrexpr.raw_natural_number * Constrexpr.sign
@@ -96,9 +96,9 @@ val interp_prim_token_cases_pattern_expr : ?loc:Loc.t -> (global_reference -> un
raise [No_match] if no such token *)
val uninterp_prim_token :
- glob_constr -> scope_name * prim_token
+ 'a glob_constr_g -> scope_name * prim_token
val uninterp_prim_token_cases_pattern :
- cases_pattern -> Name.t * scope_name * prim_token
+ 'a cases_pattern_g -> Name.t * scope_name * prim_token
val uninterp_prim_token_ind_pattern :
inductive -> cases_pattern list -> scope_name * prim_token
@@ -124,8 +124,8 @@ val interp_notation : ?loc:Loc.t -> notation -> local_scopes ->
type notation_rule = interp_rule * interpretation * int option
(** Return the possible notations for a given term *)
-val uninterp_notations : glob_constr -> notation_rule list
-val uninterp_cases_pattern_notations : cases_pattern -> notation_rule list
+val uninterp_notations : 'a glob_constr_g -> notation_rule list
+val uninterp_cases_pattern_notations : 'a cases_pattern_g -> notation_rule list
val uninterp_ind_pattern_notations : inductive -> notation_rule list
(** Test if a notation is available in the scopes
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 565a7e642..034116731 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -99,43 +99,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 = CAst.with_val (function
+let rec cases_pattern_fold_map ?loc g e = DAst.with_val (function
| PatVar na ->
- let e',na' = g e na in e', CAst.make ?loc @@ PatVar na'
+ let e',na' = g e na in e', DAst.make ?loc @@ PatVar na'
| PatCstr (cstr,patl,na) ->
let e',na' = g e na in
let e',patl' = List.fold_left_map (cases_pattern_fold_map ?loc g) e patl in
- e', CAst.make ?loc @@ PatCstr (cstr,patl',na')
+ e', DAst.make ?loc @@ PatCstr (cstr,patl',na')
)
let subst_binder_type_vars l = function
| Evar_kinds.BinderType (Name id) ->
let id =
- try match Id.List.assoc id l with { CAst.v = GVar id' } -> id' | _ -> id
+ try match DAst.get (Id.List.assoc id l) with GVar id' -> id' | _ -> id
with Not_found -> id in
Evar_kinds.BinderType (Name id)
| e -> e
-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)
+let rec subst_glob_vars l gc = DAst.map (function
+ | GVar id as r -> (try DAst.get (Id.List.assoc id l) with Not_found -> r)
| GProd (Name id,bk,t,c) ->
let id =
- try match Id.List.assoc id l with { CAst.v = GVar id' } -> id' | _ -> id
+ try match DAst.get (Id.List.assoc id l) with 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 Id.List.assoc id l with { CAst.v = GVar id' } -> id' | _ -> id
+ try match DAst.get (Id.List.assoc id l) with 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)
- | _ -> (map_glob_constr (subst_glob_vars l) gc).CAst.v (* assume: id is not binding *)
+ | _ -> DAst.get (map_glob_constr (subst_glob_vars l) gc) (* 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 = CAst.make ?loc x in lt @@ match nc with
+ let lt x = DAst.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) ->
@@ -143,13 +143,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
- (subst_glob_vars outerl it).CAst.v
+ DAst.get (subst_glob_vars outerl it)
| 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
- (subst_glob_vars outerl it).CAst.v
+ DAst.get (subst_glob_vars outerl it)
| NLambda (na,ty,c) ->
let e',na = g e na in GLambda (na,Explicit,f e ty,f e' c)
| NProd (na,ty,c) ->
@@ -201,28 +201,34 @@ let glob_constr_of_notation_constr ?loc x =
let add_id r id = r := (id :: pi1 !r, pi2 !r, pi3 !r)
let add_name r = function Anonymous -> () | Name id -> add_id r id
+let is_gvar id c = match DAst.get c with
+| GVar id' -> Id.equal id id'
+| _ -> false
+
let split_at_recursive_part c =
let sub = ref None in
- let open CAst in
- let rec aux = function
- | { loc = loc0; v = GApp ({ loc; v = GVar v },c::l) } when Id.equal v ldots_var -> (* *)
+ let rec aux c =
+ let loc0 = c.CAst.loc in
+ match DAst.get c with
+ | GApp (f, c::l) when is_gvar ldots_var f -> (* *)
+ let loc = f.CAst.loc in
begin match !sub with
| None ->
let () = sub := Some c in
begin match l with
- | [] -> CAst.make ?loc @@ GVar ldots_var
- | _ :: _ -> CAst.make ?loc:loc0 @@ GApp (CAst.make ?loc @@ GVar ldots_var, l)
+ | [] -> DAst.make ?loc @@ GVar ldots_var
+ | _ :: _ -> DAst.make ?loc:loc0 @@ GApp (DAst.make ?loc @@ GVar ldots_var, l)
end
| Some _ ->
(* Not narrowed enough to find only one recursive part *)
raise Not_found
end
- | c -> map_glob_constr aux c in
+ | _ -> map_glob_constr aux c in
let outer_iterator = aux c in
match !sub with
| None -> (* No recursive pattern found *) raise Not_found
| Some c ->
- match outer_iterator.v with
+ match DAst.get outer_iterator with
| GVar v when Id.equal v ldots_var -> (* Not enough context *) raise Not_found
| _ -> outer_iterator, c
@@ -231,7 +237,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 { CAst.v = GHole _ } -> () | t ->
+let check_is_hole id t = match DAst.get t with GHole _ -> () | _ ->
user_err ?loc:(loc_of_glob_constr t)
(strbrk "In recursive notation with binders, " ++ pr_id id ++
strbrk " is expected to come without type.")
@@ -243,21 +249,24 @@ 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 c1 c2 = match c1.v, c2.v with
+ let rec aux c1 c2 = match DAst.get c1, DAst.get c2 with
| GVar v, term when Id.equal v ldots_var ->
(* We found the pattern *)
assert (match !terminator with None -> true | Some _ -> false);
terminator := Some c2;
true
- | GApp ({ v = GVar v },l1), GApp (term, l2) when Id.equal v ldots_var ->
+ | GApp (f,l1), GApp (term, l2) ->
+ begin match DAst.get f with
+ | GVar v 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);
terminator := Some term;
List.for_all2eq aux l1 l2
+ | _ -> mk_glob_constr_eq aux c1 c2
+ end
| GVar x, GVar y when not (Id.equal x y) ->
(* We found the position where it differs *)
let lassoc = match !terminator with None -> false | Some _ -> true in
@@ -301,13 +310,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, CAst.make @@ GVar y] iterator) in
+ else subst_glob_vars [x, DAst.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, CAst.make @@ GVar y] iterator) in
+ let iterator = f' (subst_glob_vars [x, DAst.make @@ GVar y] iterator) in
(* found have been collected by compare_constr *)
found := newfound;
check_is_hole x t_x;
@@ -325,15 +334,20 @@ 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 c.CAst.v with
- | GApp ({ CAst.v = GVar f; loc},[c]) when Id.equal f ldots_var ->
+ match DAst.get c with
+ | GApp (t, [_]) ->
+ begin match DAst.get t with
+ | GVar f when Id.equal f ldots_var ->
(* Fall on the second part of the recursive pattern w/o having
found the first part *)
+ let loc = t.CAst.loc in
user_err ?loc
(str "Cannot find where the recursive pattern starts.")
+ | _ -> aux' c
+ end
| _c ->
aux' c
- and aux' x = CAst.with_val (function
+ and aux' x = DAst.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)
@@ -433,7 +447,7 @@ let notation_constr_of_glob_constr nenv a =
let notation_constr_of_constr avoiding t =
let t = EConstr.of_constr t in
- let t = Detyping.detype false avoiding (Global.env()) Evd.empty t in
+ let t = Detyping.detype Detyping.Now false avoiding (Global.env()) Evd.empty t in
let nenv = {
ninterp_var_type = Id.Map.empty;
ninterp_rec_vars = Id.Map.empty;
@@ -441,13 +455,13 @@ let notation_constr_of_constr avoiding t =
notation_constr_of_glob_constr nenv t
let rec subst_pat subst pat =
- match pat.CAst.v with
+ match DAst.get pat with
| PatVar _ -> pat
| PatCstr (((kn,i),j),cpl,n) ->
let kn' = subst_mind subst kn
and cpl' = List.smartmap (subst_pat subst) cpl in
if kn' == kn && cpl' == cpl then pat else
- CAst.make ?loc:pat.CAst.loc @@ PatCstr (((kn',i),j),cpl',n)
+ DAst.make ?loc:pat.CAst.loc @@ PatCstr (((kn',i),j),cpl',n)
let rec subst_notation_constr subst bound raw =
match raw with
@@ -576,14 +590,14 @@ let abstract_return_type_context pi mklam tml rtno =
List.fold_right mklam nal rtn)
rtno
-let abstract_return_type_context_glob_constr =
+let abstract_return_type_context_glob_constr tml rtn =
abstract_return_type_context (fun (_,(_,nal)) -> nal)
- (fun na c -> CAst.make @@
- GLambda(na,Explicit,CAst.make @@ GHole(Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None),c))
+ (fun na c -> DAst.make @@
+ GLambda(na,Explicit,DAst.make @@ GHole(Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None),c)) tml rtn
-let abstract_return_type_context_notation_constr =
+let abstract_return_type_context_notation_constr tml rtn =
abstract_return_type_context snd
- (fun na c -> NLambda(na,NHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None),c))
+ (fun na c -> NLambda(na,NHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None),c)) tml rtn
let is_term_meta id metas =
try match Id.List.assoc id metas with _,(NtnTypeConstr | NtnTypeConstrList) -> true | _ -> false
@@ -651,19 +665,23 @@ 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 = CAst.map (function
+let rec pat_binder_of_term t = DAst.map (function
| GVar id -> PatVar (Name id)
- | GApp ({ CAst.v = GRef (ConstructRef cstr,_)}, l) ->
+ | GApp (t, l) ->
+ begin match DAst.get t with
+ | GRef (ConstructRef cstr,_) ->
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)
+ | _ -> raise No_match
+ end
| _ -> raise No_match
) t
let bind_term_env alp (terms,onlybinders,termlists,binderlists as sigma) var v =
try
let v' = Id.List.assoc var terms in
- match CAst.(v.v, v'.v) with
+ match DAst.get v, DAst.get v' with
| GHole _, _ -> sigma
| _, GHole _ ->
let sigma = Id.List.remove_assoc var terms,onlybinders,termlists,binderlists in
@@ -677,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 CAst.(v.v, v'.v) with
+ match DAst.get v, DAst.get v' with
| GHole _, _ -> v'
| _, GHole _ -> v
| _, _ -> if glob_constr_eq (alpha_rename (snd alp) v) v' then v' else raise No_match in
@@ -693,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 Id.List.assoc var terms with
- | { CAst.v = GVar id' } ->
+ match DAst.get (Id.List.assoc var terms) with
+ | 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.")
@@ -702,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 (CAst.make @@ GVar id)
+ alp, add_env alp sigma var (DAst.make @@ GVar id)
let bind_binding_as_term_env alp (terms,onlybinders,termlists,binderlists as sigma) var id =
try
@@ -729,17 +747,19 @@ 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 = CAst.map (function
+let rec map_cases_pattern_name_left f = DAst.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' = 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 rec fold_cases_pattern_eq f x p p' =
+ let loc = p.CAst.loc in
+ match DAst.get p, DAst.get p' with
+ | PatVar na, PatVar na' -> let x,na = f x na na' in x, DAst.make ?loc @@ PatVar na
+ | PatCstr (c,l,na), 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, CAst.make ?loc @@ PatCstr (c,l,na)
+ x, DAst.make ?loc @@ PatCstr (c,l,na)
| _ -> failwith "Not equal"
and fold_cases_pattern_list_eq f x pl pl' = match pl, pl' with
@@ -750,7 +770,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 CAst.(p1.v, p2.v) with
+let rec cases_pattern_eq p1 p2 = match DAst.get p1, DAst.get 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 &&
@@ -771,7 +791,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 CAst.(v.v, v'.v) with
+ match DAst.get v, DAst.get v' with
| GHole _, _ -> v'
| _, GHole _ -> v
| _, _ -> if glob_constr_eq (alpha_rename (snd alp) v) v' then v else raise No_match in
@@ -783,16 +803,16 @@ let bind_bindinglist_env alp (terms,onlybinders,termlists,binderlists as sigma)
let unify_binding_kind bk bk' = if bk == bk' then bk' else raise No_match in
let unify_binder alp b b' =
let loc, loc' = CAst.(b.loc, b'.loc) in
- match CAst.(b.v, b'.v) with
+ match DAst.get b, DAst.get b' with
| GLocalAssum (na,bk,t), GLocalAssum (na',bk',t') ->
let alp, na = unify_name alp na na' in
- alp, CAst.make ?loc @@ GLocalAssum (na, unify_binding_kind bk bk', unify_term alp t t')
+ alp, DAst.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, CAst.make ?loc @@ GLocalDef (na, unify_binding_kind bk bk', unify_term alp c c', unify_opt_term alp t t')
+ alp, DAst.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, CAst.make ?loc @@ GLocalPattern ((p,ids), id, unify_binding_kind bk bk', unify_term alp t t')
+ alp, DAst.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
@@ -819,19 +839,22 @@ 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 = CAst.(map (fun b' ->
- match c, b' with
- | { v = GVar id}, GLocalAssum (na', bk', t') ->
+ let unify_term_binder c = DAst.(map (fun b' ->
+ match DAst.get c, b' with
+ | GVar id, GLocalAssum (na', bk', t') ->
GLocalAssum (unify_id id na', bk', t')
- | c, GLocalPattern ((p',ids), id, bk', t') ->
+ | _, 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
let rec unify cl bl' =
match cl, bl' with
| [], [] -> []
- | c :: cl, { CAst.v = GLocalDef ( _, _, _, t) } :: bl' -> unify cl bl'
- | c :: cl, b' :: bl' -> unify_term_binder c b' :: unify cl bl'
+ | c :: cl, b' :: bl' ->
+ begin match DAst.get b' with
+ | GLocalDef ( _, _, _, t) -> unify cl bl'
+ | _ -> unify_term_binder c b' :: unify cl bl'
+ end
| _ -> raise No_match in
let bl = unify cl bl' in
let sigma = (terms,onlybinders,termlists,Id.List.remove_assoc var binderlists) in
@@ -872,7 +895,7 @@ let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with
| _ -> raise No_match
let rec match_cases_pattern_binders metas acc pat1 pat2 =
- match CAst.(pat1.v, pat2.v) with
+ match DAst.get pat1, DAst.get pat2 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) ->
@@ -882,21 +905,29 @@ let rec match_cases_pattern_binders metas acc pat1 pat2 =
let glue_letin_with_decls = true
-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 ((CAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t))::decls) b
- | GLambda (na,bk,t,b) when islambda ->
- 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 ((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 ((CAst.make ?loc @@ GLocalAssum(na,bk,t))::decls) b
+let rec match_iterated_binders islambda decls bi = DAst.(with_loc_val (fun ?loc -> function
+ | GLambda (na,bk,t,b) as b0 ->
+ begin match na, DAst.get b with
+ | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b))])
+ when islambda && is_gvar p e ->
+ match_iterated_binders islambda ((DAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t))::decls) b
+ | _, _ when islambda ->
+ match_iterated_binders islambda ((DAst.make ?loc @@ GLocalAssum(na,bk,t))::decls) b
+ | _ -> (decls, DAst.make ?loc b0)
+ end
+ | GProd (na,bk,t,b) as b0 ->
+ begin match na, DAst.get b with
+ | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b))])
+ when not islambda && is_gvar p e ->
+ match_iterated_binders islambda ((DAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t))::decls) b
+ | Name _, _ when not islambda ->
+ match_iterated_binders islambda ((DAst.make ?loc @@ GLocalAssum(na,bk,t))::decls) b
+ | _ -> (decls, DAst.make ?loc b0)
+ end
| GLetIn (na,c,t,b) when glue_letin_with_decls ->
match_iterated_binders islambda
- ((CAst.make ?loc @@ GLocalDef (na,Explicit (*?*), c,t))::decls) b
- | b -> (decls, CAst.make ?loc b)
+ ((DAst.make ?loc @@ GLocalDef (na,Explicit (*?*), c,t))::decls) b
+ | b -> (decls, DAst.make ?loc b)
)) bi
let remove_sigma x (terms,onlybinders,termlists,binderlists) =
@@ -948,7 +979,7 @@ let match_termlist match_fun alp metas sigma rest x y iter termin lassoc =
else
bind_termlist_env alp sigma x l
-let does_not_come_from_already_eta_expanded_var =
+let does_not_come_from_already_eta_expanded_var glob =
(* This is hack to avoid looping on a rule with rhs of the form *)
(* "?f (fun ?x => ?g)" since otherwise, matching "F H" expands in *)
(* "F (fun x => H x)" and "H x" is recursively matched against the same *)
@@ -958,12 +989,14 @@ 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 { CAst.v = GVar _ } -> false | _ -> true
+ match DAst.get glob with GVar _ -> false | _ -> true
+
+let is_var c = match DAst.get c with GVar _ -> true | _ -> false
let rec match_ inner u alp metas sigma a1 a2 =
let open CAst in
let loc = a1.loc in
- match a1.v, a2 with
+ match DAst.get a1, 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
@@ -973,50 +1006,62 @@ let rec match_ inner u alp metas sigma a1 a2 =
| r1, NList (x,y,iter,termin,lassoc) ->
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, { 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 [CAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t1)] b1 in
+ | GLambda (na1, bk, t1, b1), NBinderList (x,y,iter,termin) ->
+ begin match na1, DAst.get b1, iter with
+ (* "λ p, let 'cp = p in t" -> "λ 'cp, t" *)
+ | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b1))]), NLambda (Name _, _, _) when is_gvar p e ->
+ let (decls,b) = match_iterated_binders true [DAst.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 [CAst.make ?loc @@ GLocalAssum (na1,bk,t1)] b1 in
+ (* Matching recursive notations for binders: ad hoc cases supporting let-in *)
+ | _, _, NLambda (Name _,_,_) ->
+ let (decls,b) = match_iterated_binders true [DAst.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
+ (* Matching recursive notations for binders: general case *)
+ | _, _, _ ->
+ match_binderlist_with_app (match_hd u) alp metas sigma a1 x y iter termin
+ end
- (* "∀ p, let 'cp = p in t" -> "∀ 'cp, t" *)
- | 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 [CAst.make ?loc @@ GLocalPattern ((cp,ids),p,bk,t1)] b1 in
+ | GProd (na1, bk, t1, b1), NBinderList (x,y,iter,termin) ->
+ (* "∀ p, let 'cp = p in t" -> "∀ 'cp, t" *)
+ begin match na1, DAst.get b1, iter, termin with
+ | Name p, GCases (LetPatternStyle,None,[(e, _)],[(_,(ids,[cp],b1))]), NProd (Name _,_,_), NVar _ when is_gvar p e ->
+ let (decls,b) = match_iterated_binders true [DAst.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 [CAst.make ?loc @@ GLocalAssum (na1,bk,t1)] b1 in
+ | _, _, NProd (Name _,_,_), _ when na1 != Anonymous ->
+ let (decls,b) = match_iterated_binders false [DAst.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
+ (* Matching recursive notations for binders: general case *)
+ | _, _, _, _ ->
+ match_binderlist_with_app (match_hd u) alp metas sigma a1 x y iter termin
+ end
+
(* Matching recursive notations for binders: general case *)
| _r, NBinderList (x,y,iter,termin) ->
- match_binderlist_with_app (match_hd u) alp metas sigma a1 x y iter termin
+ 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, { 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 [CAst.make ?loc @@ GLocalPattern ((cp,ids),p,bk,t)] in
+ | GLambda (na1, bk, t1, b1), NLambda (na2, t2, b2) ->
+ begin match na1, DAst.get b1, na2 with
+ | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b1))]), Name id
+ when is_var e && is_bindinglist_meta id metas ->
+ let alp,sigma = bind_bindinglist_env alp sigma id [DAst.make ?loc @@ GLocalPattern ((cp,ids),p,bk,t1)] 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 [CAst.make ?loc @@ GLocalAssum (na,bk,t)] in
+ | _, _, Name id when is_bindinglist_meta id metas ->
+ let alp,sigma = bind_bindinglist_env alp sigma id [DAst.make ?loc @@ GLocalAssum (na1,bk,t1)] in
match_in u alp metas sigma b1 b2
+ | _ ->
+ match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2
+ end
+
| 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 [CAst.make ?loc @@ GLocalAssum (na,bk,t)] in
+ let alp,sigma = bind_bindinglist_env alp sigma id [DAst.make ?loc @@ GLocalAssum (na,bk,t)] in
match_in u alp metas sigma b1 b2
(* Matching compositionally *)
@@ -1028,13 +1073,11 @@ 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 CAst.make ?loc @@ GApp (f1,l11),l12, f2,l2
+ let l11,l12 = List.chop (n1-n2) l1 in DAst.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)
(match_in u alp metas sigma f1 f2) l1 l2
- | GLambda (na1,_,t1,b1), NLambda (na2,t2,b2) ->
- match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2
| GProd (na1,_,t1,b1), NProd (na2,t2,b2) ->
match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2
| GLetIn (na1,b1,_,c1), NLetIn (na2,b2,None,c2)
@@ -1101,17 +1144,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 = CAst.make @@ GHole(Evar_kinds.BinderType (Name id'),Misctypes.IntroAnonymous,None) in
+ let t1 = DAst.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 [CAst.make @@ GLocalAssum (Name id',Explicit,t1)]
+ bind_bindinglist_env alp sigma id [DAst.make @@ GLocalAssum (Name id',Explicit,t1)]
else
match_names metas (alp,sigma) (Name id') na in
- match_in u alp metas sigma (mkGApp a1 (CAst.make @@ GVar id')) b2
+ match_in u alp metas sigma (mkGApp a1 (DAst.make @@ GVar id')) b2
| (GRec _ | GEvar _), _
| _,_ -> raise No_match
@@ -1132,7 +1175,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 = CAst.make @@ match bi with
+let term_of_binder bi = DAst.make @@ match bi with
| Name id -> GVar id
| Anonymous -> GHole (Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None)
@@ -1145,7 +1188,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... *)
- CAst.make @@GVar x in
+ DAst.make @@GVar x in
List.fold_right (fun (x,(scl,typ)) (terms',termlists',binders') ->
match typ with
| NtnTypeConstr ->
@@ -1185,8 +1228,7 @@ let match_cases_pattern_list match_fun metas sigma rest x y iter termin lassoc =
(terms,onlybinders,(x,if lassoc then l else List.rev l)::termlists, binderlists)
let rec match_cases_pattern metas (terms,(),termlists,() as sigma) a1 a2 =
- let open CAst in
- match a1.v, a2 with
+ match DAst.get a1, 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 ->
diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index 3154fd7ad..0904a4ea3 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -47,19 +47,19 @@ val glob_constr_of_notation_constr : ?loc:Loc.t -> notation_constr -> glob_const
exception No_match
-val match_notation_constr : bool -> glob_constr -> interpretation ->
- (glob_constr * subscopes) list * (glob_constr list * subscopes) list *
- (extended_glob_local_binder list * subscopes) list
+val match_notation_constr : bool -> 'a glob_constr_g -> interpretation ->
+ ('a glob_constr_g * subscopes) list * ('a glob_constr_g list * subscopes) list *
+ ('a extended_glob_local_binder_g list * subscopes) list
val match_notation_constr_cases_pattern :
- cases_pattern -> interpretation ->
- ((cases_pattern * subscopes) list * (cases_pattern list * subscopes) list) *
- (int * cases_pattern list)
+ 'a cases_pattern_g -> interpretation ->
+ (('a cases_pattern_g * subscopes) list * ('a cases_pattern_g list * subscopes) list) *
+ (int * 'a cases_pattern_g list)
val match_notation_constr_ind_pattern :
- inductive -> cases_pattern list -> interpretation ->
- ((cases_pattern * subscopes) list * (cases_pattern list * subscopes) list) *
- (int * cases_pattern list)
+ inductive -> 'a cases_pattern_g list -> interpretation ->
+ (('a cases_pattern_g * subscopes) list * ('a cases_pattern_g list * subscopes) list) *
+ (int * 'a cases_pattern_g list)
(** {5 Matching a notation pattern against a [glob_constr]} *)
diff --git a/interp/reserve.ml b/interp/reserve.ml
index b05f05283..a1e5bd0ea 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -110,7 +110,7 @@ let revert_reserved_type t =
let t = EConstr.Unsafe.to_constr t in
let reserved = KeyMap.find (constr_key t) !reserve_revtable in
let t = EConstr.of_constr t in
- let t = Detyping.detype false [] (Global.env()) Evd.empty t in
+ let t = Detyping.detype Detyping.Now false [] (Global.env()) Evd.empty t in
(* pedrot: if [Notation_ops.match_notation_constr] may raise [Failure _]
then I've introduced a bug... *)
let filter _ pat =
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 06:52:13 +0000