aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrexpr_ops.ml6
-rw-r--r--interp/constrextern.ml7
-rw-r--r--interp/constrintern.ml160
-rw-r--r--interp/coqlib.ml2
-rw-r--r--interp/dumpglob.ml9
-rw-r--r--interp/dumpglob.mli2
-rw-r--r--interp/implicit_quantifiers.ml2
-rw-r--r--interp/notation.ml6
-rw-r--r--interp/notation_ops.ml347
-rw-r--r--interp/notation_ops.mli6
-rw-r--r--interp/reserve.ml2
-rw-r--r--interp/smartlocate.ml2
-rw-r--r--interp/syntax_def.ml4
-rw-r--r--interp/topconstr.ml2
14 files changed, 413 insertions, 144 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index f49ed9a5f4..04429851fd 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -382,18 +382,18 @@ let rec prod_constr_expr c = function
let coerce_reference_to_id = function
| Ident (_,id) -> id
| Qualid (loc,_) ->
- Errors.user_err_loc (loc, "coerce_reference_to_id",
+ CErrors.user_err_loc (loc, "coerce_reference_to_id",
str "This expression should be a simple identifier.")
let coerce_to_id = function
| CRef (Ident (loc,id),_) -> (loc,id)
- | a -> Errors.user_err_loc
+ | a -> CErrors.user_err_loc
(constr_loc a,"coerce_to_id",
str "This expression should be a simple identifier.")
let coerce_to_name = function
| CRef (Ident (loc,id),_) -> (loc,Name id)
| CHole (loc,_,_,_) -> (loc,Anonymous)
- | a -> Errors.user_err_loc
+ | a -> CErrors.user_err_loc
(constr_loc a,"coerce_to_name",
str "This expression should be a name.")
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 99b2292515..e71daef999 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -8,7 +8,7 @@
(*i*)
open Pp
-open Errors
+open CErrors
open Util
open Names
open Nameops
@@ -848,10 +848,11 @@ and extern_local_binder scopes vars = function
| (Inr p,bk,Some bd,ty)::l -> assert false
| (Inr p,bk,None,ty)::l ->
- let ty = extern_typ scopes vars ty in
+ let ty =
+ if !Flags.raw_print then Some (extern_typ scopes vars ty) else None in
let p = extern_cases_pattern vars p in
let (assums,ids,l) = extern_local_binder scopes vars l in
- (assums,ids, LocalPattern(Loc.ghost,p,Some ty) :: l)
+ (assums,ids, LocalPattern(Loc.ghost,p,ty) :: l)
and extern_eqn inctx scopes vars (loc,ids,pl,c) =
(loc,[loc,List.map (extern_cases_pattern_in_scope scopes vars) pl],
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 74de6f67ff..4502aa7ace 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
open Util
open Names
open Nameops
@@ -33,10 +33,10 @@ open Context.Rel.Declaration
(** constr_expr -> glob_constr translation:
- it adds holes for implicit arguments
- - it remplaces notations by their value (scopes stuff are here)
+ - it replaces notations by their value (scopes stuff are here)
- it recognizes global vars from local ones
- - it prepares pattern maching problems (a pattern becomes a tree where nodes
- are constructor/variable pairs and leafs are variables)
+ - it prepares pattern matching problems (a pattern becomes a tree
+ where nodes are constructor/variable pairs and leafs are variables)
All that at once, fasten your seatbelt!
*)
@@ -432,11 +432,6 @@ 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 obj_string x =
- if Obj.is_block (Obj.repr x) then
- "tag = " ^ string_of_int (Obj.tag (Obj.repr x))
- else "int_val = " ^ string_of_int (Obj.magic x)
-
let rec free_vars_of_pat il =
function
| CPatCstr (loc, c, l1, l2) ->
@@ -481,9 +476,14 @@ let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = functio
let bl' = List.map (fun a -> BDRawDef a) bl' in
env, bl' @ bl
| LocalRawDef((loc,na as locna),def) ->
- let indef = intern env def in
+ let indef = intern env def in
+ let term, ty =
+ match indef with
+ | GCast (loc, b, Misctypes.CastConv t) -> b, t
+ | _ -> indef, GHole(loc,Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None)
+ in
(push_name_env lvar (impls_term_list indef) env locna,
- (BDRawDef ((loc,(na,Explicit,Some(indef),GHole(loc,Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None)))))::bl)
+ (BDRawDef ((loc,(na,Explicit,Some(term),ty))))::bl)
| LocalPattern (loc,p,ty) ->
let tyc =
match ty with
@@ -599,31 +599,52 @@ let rec subordinate_letins intern letins = function
| [] ->
letins,[]
-let rec subst_iterator y t = function
- | GVar (_,id) as x -> if Id.equal id y then t else x
- | x -> map_glob_constr (subst_iterator y t) x
+let terms_of_binders bl =
+ let rec term_of_pat = function
+ | PatVar (loc,Name id) -> CRef (Ident (loc,id), None)
+ | PatVar (loc,Anonymous) -> error "Cannot turn \"_\" into a term."
+ | PatCstr (loc,c,l,_) ->
+ let r = Qualid (loc,qualid_of_path (path_of_global (ConstructRef c))) in
+ let hole = CHole (loc,None,Misctypes.IntroAnonymous,None) in
+ let params = List.make (Inductiveops.inductive_nparams (fst c)) hole in
+ CAppExpl (loc,(None,r,None),params @ List.map term_of_pat l) in
+ let rec extract_variables = function
+ | BDRawDef (loc,(Name id,_,None,_))::l -> CRef (Ident (loc,id), None) :: extract_variables l
+ | BDRawDef (loc,(Name id,_,Some _,_))::l -> extract_variables l
+ | BDRawDef (loc,(Anonymous,_,_,_))::l -> error "Cannot turn \"_\" into a term."
+ | BDPattern (loc,(u,_),lvar,env,tyc) :: l -> term_of_pat u :: extract_variables l
+ | [] -> [] in
+ extract_variables bl
let instantiate_notation_constr loc intern ntnvars subst infos c =
let (terms,termlists,binders) = subst in
(* when called while defining a notation, avoid capturing the private binders
of the expression by variables bound by the notation (see #3892) *)
let avoid = Id.Map.domain ntnvars in
- let rec aux (terms,binderopt as subst') (renaming,env) c =
+ let rec aux (terms,binderopt,terminopt as subst') (renaming,env) c =
let subinfos = renaming,{env with tmp_scope = None} in
match c with
+ | NVar id when Id.equal id ldots_var -> Option.get terminopt
| NVar id -> subst_var subst' (renaming, env) id
- | NList (x,_,iter,terminator,lassoc) ->
- (try
+ | NList (x,y,iter,terminator,lassoc) ->
+ let l,(scopt,subscopes) =
(* All elements of the list are in scopes (scopt,subscopes) *)
- let (l,(scopt,subscopes)) = Id.Map.find x termlists in
- let termin = aux subst' subinfos terminator in
- let fold a t =
- let nterms = Id.Map.add x (a, (scopt, subscopes)) terms in
- subst_iterator ldots_var t (aux (nterms, binderopt) subinfos iter)
- in
- List.fold_right fold (if lassoc then List.rev l else l) termin
- with Not_found ->
- anomaly (Pp.str "Inconsistent substitution of recursive notation"))
+ try
+ let l,scopes = Id.Map.find x termlists in
+ (if lassoc then List.rev l else l),scopes
+ with Not_found ->
+ try
+ let (bl,(scopt,subscopes)) = Id.Map.find x binders in
+ let env,bl' = List.fold_left (intern_local_binder_aux intern ntnvars) (env,[]) bl in
+ terms_of_binders (if lassoc then bl' else List.rev bl'),(None,[])
+ with Not_found ->
+ anomaly (Pp.str "Inconsistent substitution of recursive notation") in
+ let termin = aux (terms,None,None) subinfos terminator in
+ let fold a t =
+ let nterms = Id.Map.add y (a, (scopt, subscopes)) terms in
+ aux (nterms,None,Some t) subinfos iter
+ in
+ List.fold_right fold l termin
| NHole (knd, naming, arg) ->
let knd = match knd with
| Evar_kinds.BinderType (Name id as na) ->
@@ -658,16 +679,15 @@ let instantiate_notation_constr loc intern ntnvars subst infos c =
Some arg
in
GHole (loc, knd, naming, arg)
- | NBinderList (x,_,iter,terminator) ->
+ | NBinderList (x,y,iter,terminator) ->
(try
(* All elements of the list are in scopes (scopt,subscopes) *)
let (bl,(scopt,subscopes)) = Id.Map.find x binders in
let env,bl = List.fold_left (intern_local_binder_aux intern ntnvars) (env,[]) bl in
let letins,bl = subordinate_letins intern [] bl in
- let termin = aux subst' (renaming,env) terminator in
+ let termin = aux (terms,None,None) (renaming,env) terminator in
let res = List.fold_left (fun t binder ->
- subst_iterator ldots_var t
- (aux (terms,Some(x,binder)) subinfos iter))
+ aux (terms,Some(y,binder),Some t) subinfos iter)
termin bl in
make_letins letins res
with Not_found ->
@@ -695,7 +715,7 @@ let instantiate_notation_constr loc intern ntnvars subst infos c =
| t ->
glob_constr_of_notation_constr_with_binders loc
(traverse_binder subst avoid) (aux subst') subinfos t
- and subst_var (terms, binderopt) (renaming, env) id =
+ and subst_var (terms, _binderopt, _terminopt) (renaming, env) id =
(* subst remembers the delimiters stack in the interpretation *)
(* of the notations *)
try
@@ -708,7 +728,7 @@ let instantiate_notation_constr loc intern ntnvars subst infos c =
with Not_found ->
(* Happens for local notation joint with inductive/fixpoint defs *)
GVar (loc,id)
- in aux (terms,None) infos c
+ in aux (terms,None,None) infos c
let split_by_type ids =
List.fold_right (fun (x,(scl,typ)) (l1,l2,l3) ->
@@ -741,7 +761,13 @@ let string_of_ty = function
| Method -> "meth"
| Variable -> "var"
-let intern_var genv (ltacvars,ntnvars) namedctx loc id =
+let gvar (loc, id) us = match us with
+| None -> GVar (loc, id)
+| Some _ ->
+ user_err_loc (loc, "", str "Variable " ++ pr_id id ++
+ str " cannot have a universe instance")
+
+let intern_var genv (ltacvars,ntnvars) namedctx loc id us =
(* Is [id] an inductive type potentially with implicit *)
try
let ty,expl_impls,impls,argsc = Id.Map.find id genv.impls in
@@ -749,21 +775,21 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id =
(fun id -> CRef (Ident (loc,id),None), Some (loc,ExplByName id)) expl_impls in
let tys = string_of_ty ty in
Dumpglob.dump_reference loc "<>" (Id.to_string id) tys;
- GVar (loc,id), make_implicits_list impls, argsc, expl_impls
+ gvar (loc,id) us, make_implicits_list impls, argsc, expl_impls
with Not_found ->
(* Is [id] bound in current term or is an ltac var bound to constr *)
if Id.Set.mem id genv.ids || Id.Set.mem id ltacvars.ltac_vars
then
- GVar (loc,id), [], [], []
+ gvar (loc,id) us, [], [], []
(* Is [id] a notation variable *)
else if Id.Map.mem id ntnvars
then
- (set_var_scope loc id true genv ntnvars; GVar (loc,id), [], [], [])
+ (set_var_scope loc id true genv ntnvars; gvar (loc,id) us, [], [], [])
(* Is [id] the special variable for recursive notations *)
else if Id.equal id ldots_var
then if Id.Map.is_empty ntnvars
then error_ldots_var loc
- else GVar (loc,id), [], [], []
+ else gvar (loc,id) us, [], [], []
else if Id.Set.mem id ltacvars.ltac_bound then
(* Is [id] bound to a free name in ltac (this is an ltac error message) *)
user_err_loc (loc,"intern_var",
@@ -778,10 +804,10 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id =
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";
- GRef (loc, ref, None), impls, scopes, []
- with e when Errors.noncritical e ->
+ GRef (loc, ref, us), impls, scopes, []
+ with e when CErrors.noncritical e ->
(* [id] a goal variable *)
- GVar (loc,id), [], [], []
+ gvar (loc,id) us, [], [], []
let find_appl_head_data c =
match c with
@@ -843,9 +869,12 @@ let intern_qualid loc qid intern env lvar us args =
let c = match us, c with
| None, _ -> c
| Some _, GRef (loc, ref, None) -> GRef (loc, ref, us)
+ | Some _, GApp (loc, GRef (loc', ref, None), arg) ->
+ GApp (loc, GRef (loc', ref, us), arg)
| Some _, _ ->
user_err_loc (loc, "", str "Notation " ++ pr_qualid qid ++
- str " cannot have a universe instance")
+ str " cannot have a universe instance, its expanded head
+ does not start with a reference")
in
c, projapp, args2
@@ -864,7 +893,7 @@ let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args =
let x, imp, scopes, l = find_appl_head_data r in
(x,imp,scopes,l), args2
| Ident (loc, id) ->
- try intern_var env lvar namedctx loc id, args
+ try intern_var env lvar namedctx loc id us, args
with Not_found ->
let qid = qualid_of_ident id in
try
@@ -874,7 +903,7 @@ let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args =
with Not_found ->
(* Extra allowance for non globalizing functions *)
if !interning_grammar || env.unb then
- (GVar (loc,id), [], [], []), args
+ (gvar (loc,id) us, [], [], []), args
else error_global_not_found_loc loc qid
let interp_reference vars r =
@@ -1049,12 +1078,10 @@ let sort_fields ~complete loc fields completer =
match fields with
| [] -> None
| (first_field_ref, first_field_value):: other_fields ->
- let env_error_msg = "Environment corruption for records." in
- let first_field_glob_ref =
- try global_reference_of_reference first_field_ref
- with Not_found -> anomaly (Pp.str env_error_msg) in
- let record =
- try Recordops.find_projection first_field_glob_ref
+ let (first_field_glob_ref, record) =
+ try
+ let gr = global_reference_of_reference first_field_ref in
+ (gr, Recordops.find_projection gr)
with Not_found ->
user_err_loc (loc_of_reference first_field_ref, "intern",
pr_reference first_field_ref ++ str": Not a projection")
@@ -1065,7 +1092,8 @@ let sort_fields ~complete loc fields completer =
let base_constructor =
let global_record_id = ConstructRef record.Recordops.s_CONST in
try Qualid (loc, shortest_qualid_of_global Id.Set.empty global_record_id)
- with Not_found -> anomaly (Pp.str env_error_msg) in
+ with Not_found ->
+ anomaly (str "Environment corruption for records") in
let (end_index, (* one past the last field index *)
first_field_index, (* index of the first field of the record *)
proj_list) (* list of projections *)
@@ -1315,7 +1343,7 @@ let drop_notations_pattern looked_for =
RCPatCstr (loc, g,
List.map2 (fun x -> in_not false loc (x,snd scopes) fullsubst []) argscs1 pl @
List.map (in_pat false scopes) args, [])
- | NList (x,_,iter,terminator,lassoc) ->
+ | NList (x,y,iter,terminator,lassoc) ->
if not (List.is_empty args) then user_err_loc
(loc,"",strbrk "Application of arguments to a recursive notation not supported in patterns.");
(try
@@ -1323,7 +1351,7 @@ let drop_notations_pattern looked_for =
let (l,(scopt,subscopes)) = Id.Map.find x substlist in
let termin = in_not top loc scopes fullsubst [] terminator in
List.fold_right (fun a t ->
- let nsubst = Id.Map.add x (a, (scopt, subscopes)) subst in
+ let nsubst = Id.Map.add y (a, (scopt, subscopes)) subst in
let u = in_not false loc scopes (nsubst, substlist) [] iter in
subst_pat_iterator ldots_var t u)
(if lassoc then List.rev l else l) termin
@@ -1600,11 +1628,13 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
(merge_impargs l args) loc
| CRecord (loc, fs) ->
- let fields =
- sort_fields ~complete:true loc fs
- (fun _idx -> CHole (loc, Some (Evar_kinds.QuestionMark (Evar_kinds.Define true)), Misctypes.IntroAnonymous, None))
- in
- begin
+ let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in
+ let fields =
+ sort_fields ~complete:true loc fs
+ (fun _idx -> CHole (loc, Some (Evar_kinds.QuestionMark st),
+ Misctypes.IntroAnonymous, None))
+ in
+ begin
match fields with
| None -> user_err_loc (loc, "intern", str"No constructor inference.")
| Some (n, constrname, args) ->
@@ -1674,7 +1704,9 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
GIf (loc, c', (na', p'), intern env b1, intern env b2)
| CHole (loc, k, naming, solve) ->
let k = match k with
- | None -> Evar_kinds.QuestionMark (Evar_kinds.Define true)
+ | None ->
+ let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in
+ Evar_kinds.QuestionMark st
| Some k -> k
in
let solve = match solve with
@@ -2021,11 +2053,13 @@ let interp_rawcontext_evars env evdref k bl =
let (env, par, _, impls) =
List.fold_left
(fun (env,params,n,impls) (na, k, b, t) ->
+ let t' =
+ if Option.is_empty b then locate_if_hole (loc_of_glob_constr t) na t
+ else t
+ in
+ let t = understand_tcc_evars env evdref ~expected_type:IsType t' in
match b with
None ->
- let t' = locate_if_hole (loc_of_glob_constr t) na t in
- let t =
- understand_tcc_evars env evdref ~expected_type:IsType t' in
let d = LocalAssum (na,t) in
let impls =
if k == Implicit then
@@ -2035,8 +2069,8 @@ let interp_rawcontext_evars env evdref k bl =
in
(push_rel d env, d::params, succ n, impls)
| Some b ->
- let c = understand_judgment_tcc env evdref b in
- let d = LocalDef (na, c.uj_val, c.uj_type) in
+ let c = understand_tcc_evars env evdref ~expected_type:(OfType t) b in
+ let d = LocalDef (na, c, t) in
(push_rel d env, d::params, n, impls))
(env,[],k+1,[]) (List.rev bl)
in (env, par), impls
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 23bcddaea2..588637b76e 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Errors
+open CErrors
open Util
open Pp
open Names
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 931fc1ca40..b020f89457 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -45,10 +45,10 @@ let dump_string s =
if dump () && !glob_output != Feedback then
Pervasives.output_string !glob_file s
-let start_dump_glob vfile =
+let start_dump_glob ~vfile ~vofile =
match !glob_output with
| MultFiles ->
- open_glob_file (Filename.chop_extension vfile ^ ".glob");
+ open_glob_file (Filename.chop_extension vofile ^ ".glob");
output_string !glob_file "DIGEST ";
output_string !glob_file (Digest.to_hex (Digest.file vfile));
output_char !glob_file '\n'
@@ -127,9 +127,10 @@ let type_of_global_ref gr =
| Globnames.ConstructRef _ -> "constr"
let remove_sections dir =
- if Libnames.is_dirpath_prefix_of dir (Lib.cwd ()) then
+ let cwd = Lib.cwd_except_section () in
+ if Libnames.is_dirpath_prefix_of cwd dir then
(* Not yet (fully) discharged *)
- Libnames.pop_dirpath_n (Lib.sections_depth ()) (Lib.cwd ())
+ cwd
else
(* Theorem/Lemma outside its outer section of definition *)
dir
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index a7c799114b..e84a640521 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -9,7 +9,7 @@
val open_glob_file : string -> unit
val close_glob_file : unit -> unit
-val start_dump_glob : string -> unit
+val start_dump_glob : vfile:string -> vofile:string -> unit
val end_dump_glob : unit -> unit
val dump : unit -> bool
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index b50732e4e9..10cfbe58fa 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -9,7 +9,7 @@
(*i*)
open Names
open Decl_kinds
-open Errors
+open CErrors
open Util
open Glob_term
open Constrexpr
diff --git a/interp/notation.ml b/interp/notation.ml
index d42307040d..0798d385d4 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -7,7 +7,7 @@
(************************************************************************)
(*i*)
-open Errors
+open CErrors
open Util
open Pp
open Bigint
@@ -208,7 +208,7 @@ let remove_delimiters scope =
let sc = find_scope scope in
let newsc = { sc with delimiters = None } in
match sc.delimiters with
- | None -> Errors.errorlabstrm "" (str "No bound key for scope " ++ str scope ++ str ".")
+ | None -> CErrors.errorlabstrm "" (str "No bound key for scope " ++ str scope ++ str ".")
| Some key ->
scope_map := String.Map.add scope newsc !scope_map;
try
@@ -1056,6 +1056,6 @@ let with_notation_protection f x =
let fs = freeze false in
try let a = f x in unfreeze fs; a
with reraise ->
- let reraise = Errors.push reraise in
+ let reraise = CErrors.push reraise in
let () = unfreeze fs in
iraise reraise
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index d8e022ce65..1f29a2948f 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
open Util
open Names
open Nameops
@@ -111,7 +111,7 @@ let rec eq_notation_constr t1 t2 = match t1, t2 with
(* Re-interpret a notation as a glob_constr, taking care of binders *)
let name_to_ident = function
- | Anonymous -> Errors.error "This expression should be a simple identifier."
+ | Anonymous -> CErrors.error "This expression should be a simple identifier."
| Name id -> id
let to_id g e id = let e,na = g e (Name id) in e,name_to_ident na
@@ -124,6 +124,14 @@ let rec cases_pattern_fold_map loc g e = function
let e',patl' = List.fold_map (cases_pattern_fold_map loc g) e patl in
e', PatCstr (loc,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 GVar(_,id') -> id' | _ -> id
+ with Not_found -> id in
+ Evar_kinds.BinderType (Name id)
+ | e -> e
+
let rec subst_glob_vars l = function
| GVar (_,id) as r -> (try Id.List.assoc id l with Not_found -> r)
| GProd (loc,Name id,bk,t,c) ->
@@ -136,6 +144,7 @@ let rec subst_glob_vars l = function
try match Id.List.assoc id l with GVar(_,id') -> id' | _ -> id
with Not_found -> id in
GLambda (loc,Name id,bk,subst_glob_vars l t,subst_glob_vars l c)
+ | GHole (loc,x,naming,arg) -> GHole (loc,subst_binder_type_vars l x,naming,arg)
| r -> map_glob_constr (subst_glob_vars l) r (* assume: id is not binding *)
let ldots_var = Id.of_string ".."
@@ -237,7 +246,9 @@ let check_is_hole id = function GHole _ -> () | t ->
strbrk "In recursive notation with binders, " ++ pr_id id ++
strbrk " is expected to come without type.")
-let compare_recursive_parts found f (iterator,subc) =
+let pair_equal eq1 eq2 (a,b) (a',b') = eq1 a a' && eq2 b b'
+
+let compare_recursive_parts found f f' (iterator,subc) =
let diff = ref None in
let terminator = ref None in
let rec aux c1 c2 = match c1,c2 with
@@ -284,16 +295,26 @@ let compare_recursive_parts found f (iterator,subc) =
user_err_loc (subtract_loc loc1 loc2,"",
str "Both ends of the recursive pattern are the same.")
| Some (x,y,Some lassoc) ->
- let newfound = (pi1 !found, (x,y) :: pi2 !found, pi3 !found) in
+ let newfound,x,y,lassoc =
+ if List.mem_f (pair_equal Id.equal Id.equal) (x,y) (pi2 !found) ||
+ List.mem_f (pair_equal Id.equal Id.equal) (x,y) (pi3 !found)
+ then
+ !found,x,y,lassoc
+ else if List.mem_f (pair_equal Id.equal Id.equal) (y,x) (pi2 !found) ||
+ List.mem_f (pair_equal Id.equal Id.equal) (y,x) (pi3 !found)
+ then
+ !found,y,x,not lassoc
+ else
+ (pi1 !found, (x,y) :: pi2 !found, pi3 !found),x,y,lassoc in
let iterator =
- f (if lassoc then subst_glob_vars [y,GVar(Loc.ghost,x)] iterator
- else iterator) in
+ f' (if lassoc then iterator
+ else subst_glob_vars [x,GVar(Loc.ghost,y)] iterator) in
(* found have been collected by compare_constr *)
found := newfound;
NList (x,y,iterator,f (Option.get !terminator),lassoc)
| Some (x,y,None) ->
let newfound = (pi1 !found, pi2 !found, (x,y) :: pi3 !found) in
- let iterator = f iterator in
+ let iterator = f' (subst_glob_vars [x,GVar(Loc.ghost,y)] iterator) in
(* found have been collected by compare_constr *)
found := newfound;
NBinderList (x,y,iterator,f (Option.get !terminator))
@@ -305,7 +326,7 @@ let notation_constr_and_vars_of_glob_constr a =
let rec aux c =
let keepfound = !found in
(* n^2 complexity but small and done only once per notation *)
- try compare_recursive_parts found aux' (split_at_recursive_part c)
+ try compare_recursive_parts found aux aux' (split_at_recursive_part c)
with Not_found ->
found := keepfound;
match c with
@@ -357,8 +378,6 @@ let notation_constr_and_vars_of_glob_constr a =
(* Side effect *)
t, !found
-let pair_equal eq1 eq2 (a,b) (a',b') = eq1 a a' && eq2 b b'
-
let check_variables nenv (found,foundrec,foundrecbinding) =
let recvars = nenv.ninterp_rec_vars in
let fold _ y accu = Id.Set.add y accu in
@@ -585,6 +604,10 @@ let rec alpha_var id1 id2 = function
| _::idl -> alpha_var id1 id2 idl
| [] -> Id.equal id1 id2
+let alpha_rename alpmetas v =
+ if alpmetas == [] then v
+ else try rename_glob_vars alpmetas v with UnsoundRenaming -> raise No_match
+
let add_env (alp,alpmetas) (terms,onlybinders,termlists,binderlists) var v =
(* Check that no capture of binding variables occur *)
(* [alp] is used when matching a pattern "fun x => ... x ... ?var ... x ..."
@@ -592,7 +615,8 @@ let add_env (alp,alpmetas) (terms,onlybinders,termlists,binderlists) var v =
notation, as in "Notation "'twice_upto' y" := (fun x => x + x + y)". Then
we keep (z,x) in alp, and we have to check that what the [v] which is bound
to [var] does not contain z *)
- if List.exists (fun (id,_) ->occur_glob_constr id v) alp then raise No_match;
+ if not (Id.equal ldots_var var) &&
+ List.exists (fun (id,_) -> occur_glob_constr id v) alp then raise No_match;
(* [alpmetas] is used when matching a pattern "fun x => ... x ... ?var ... x ..."
with an actual term "fun z => ... z ..." when "x" is bound in the
notation and the name "x" cannot be changed to "z", e.g. because
@@ -610,16 +634,29 @@ let add_env (alp,alpmetas) (terms,onlybinders,termlists,binderlists) var v =
glob_constr_eq in bind_term_env to be postponed in match_notation_constr, and the
choice of exact variable be done there; but again, this would be a non-trivial
refinement *)
- if alpmetas != [] then raise No_match;
+ let v = alpha_rename alpmetas v in
(* TODO: handle the case of multiple occs in different scopes *)
((var,v)::terms,onlybinders,termlists,binderlists)
+let add_termlist_env (alp,alpmetas) (terms,onlybinders,termlists,binderlists) var vl =
+ if List.exists (fun (id,_) -> List.exists (occur_glob_constr id) vl) alp then raise No_match;
+ let vl = List.map (alpha_rename alpmetas) vl in
+ (terms,onlybinders,(var,vl)::termlists,binderlists)
+
let add_binding_env alp (terms,onlybinders,termlists,binderlists) var v =
(* TODO: handle the case of multiple occs in different scopes *)
(terms,(var,v)::onlybinders,termlists,binderlists)
let add_bindinglist_env (terms,onlybinders,termlists,binderlists) x bl =
- (terms,onlybinders,termlists,(x,List.rev bl)::binderlists)
+ (terms,onlybinders,termlists,(x,bl)::binderlists)
+
+let rec pat_binder_of_term = function
+ | GVar (loc, id) -> PatVar (loc, Name id)
+ | GApp (loc, GRef (_,ConstructRef cstr,_), l) ->
+ let nparams = Inductiveops.inductive_nparams (fst cstr) in
+ let _,l = List.chop nparams l in
+ PatCstr (loc, cstr, List.map pat_binder_of_term l, Anonymous)
+ | _ -> raise No_match
let bind_term_env alp (terms,onlybinders,termlists,binderlists as sigma) var v =
try
@@ -630,10 +667,53 @@ let bind_term_env alp (terms,onlybinders,termlists,binderlists as sigma) var v =
let sigma = Id.List.remove_assoc var terms,onlybinders,termlists,binderlists in
add_env alp sigma var v
| _, _ ->
- if glob_constr_eq v v' then sigma
+ if glob_constr_eq (alpha_rename (snd alp) v) v' then sigma
else raise No_match
with Not_found -> add_env alp sigma var v
+let bind_termlist_env alp (terms,onlybinders,termlists,binderlists as sigma) var vl =
+ try
+ let vl' = Id.List.assoc var termlists in
+ let unify_term v v' =
+ match v, v' with
+ | GHole _, _ -> v'
+ | _, GHole _ -> v
+ | _, _ -> if glob_constr_eq (alpha_rename (snd alp) v) v' then v' else raise No_match in
+ let rec unify vl vl' =
+ match vl, vl' with
+ | [], [] -> []
+ | v :: vl, v' :: vl' -> unify_term v v' :: unify vl vl'
+ | _ -> raise No_match in
+ let vl = unify vl vl' in
+ let sigma = (terms,onlybinders,Id.List.remove_assoc var termlists,binderlists) in
+ add_termlist_env alp sigma var vl
+ with Not_found -> add_termlist_env alp sigma var vl
+
+let bind_term_as_binding_env alp (terms,onlybinders,termlists,binderlists as sigma) var id =
+ try
+ match 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")
+ with Not_found ->
+ (* 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 (GVar (Loc.ghost,id))
+
+let bind_binding_as_term_env alp (terms,onlybinders,termlists,binderlists as sigma) var id =
+ try
+ let v' = Id.List.assoc var onlybinders in
+ match v' with
+ | Anonymous ->
+ (* Should not occur, since the term has to be bound upwards *)
+ let sigma = (terms,Id.List.remove_assoc var onlybinders,termlists,binderlists) in
+ add_binding_env alp sigma var (Name id)
+ | Name id' ->
+ if Id.equal (rename_var (snd alp) id) id' then sigma else raise No_match
+ with Not_found -> add_binding_env alp sigma var (Name id)
+
let bind_binding_env alp (terms,onlybinders,termlists,binderlists as sigma) var v =
try
let v' = Id.List.assoc var onlybinders in
@@ -647,6 +727,109 @@ 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 = function
+ | PatVar (loc,na) -> PatVar (loc,f na)
+ | PatCstr (loc,c,l,na) -> PatCstr (loc,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
+ | PatVar (loc,na), PatVar (_,na') -> let x,na = f x na na' in x, PatVar (loc,na)
+ | PatCstr (loc,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, PatCstr (loc,c,l,na)
+ | _ -> failwith "Not equal"
+
+and fold_cases_pattern_list_eq f x pl pl' = match pl, pl' with
+ | [], [] -> x, []
+ | p::pl, p'::pl' ->
+ let x, p = fold_cases_pattern_eq f x p p' in
+ let x, pl = fold_cases_pattern_list_eq f x pl pl' in
+ x, p :: pl
+ | _ -> assert false
+
+let rec cases_pattern_eq p1 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 &&
+ Name.equal na1 na2
+| _ -> false
+
+let bind_bindinglist_env alp (terms,onlybinders,termlists,binderlists as sigma) var bl =
+ let bl = List.rev bl in
+ try
+ let bl' = Id.List.assoc var binderlists in
+ let unify_name alp na na' =
+ match na, na' with
+ | Anonymous, na' -> alp, na'
+ | na, Anonymous -> alp, na
+ | Name id, Name id' ->
+ if Id.equal id id' then alp, na'
+ else (fst alp,(id,id')::snd alp), na' in
+ 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 v, v' with
+ | GHole _, _ -> v'
+ | _, GHole _ -> v
+ | _, _ -> if glob_constr_eq (alpha_rename (snd alp) v) v' then v else raise No_match in
+ let unify_binding_kind bk bk' = if bk == bk' then bk' else raise No_match in
+ let unify_binder alp b b' =
+ match b, b' with
+ | (Inl na, bk, None, t), (Inl na', bk', None, t') (* assum *) ->
+ let alp, na = unify_name alp na na' in
+ alp, (Inl na, unify_binding_kind bk bk', None, unify_term alp t t')
+ | (Inl na, bk, Some c, t), (Inl na', bk', Some c', t') (* let *) ->
+ let alp, na = unify_name alp na na' in
+ alp, (Inl na, unify_binding_kind bk bk', Some (unify_term alp c c'), unify_term alp t t')
+ | (Inr p, bk, None, t), (Inr p', bk', None, t') (* pattern *) ->
+ let alp, p = unify_pat alp p p' in
+ alp, (Inr p, unify_binding_kind bk bk', None, unify_term alp t t')
+ | _ -> raise No_match in
+ let rec unify alp bl bl' =
+ match bl, bl' with
+ | [], [] -> alp, []
+ | b :: bl, b' :: bl' ->
+ let alp,b = unify_binder alp b b' in
+ let alp,bl = unify alp bl bl' in
+ alp, b :: bl
+ | _ -> raise No_match in
+ let alp, bl = unify alp bl bl' in
+ let sigma = (terms,Id.List.remove_assoc var onlybinders,termlists,binderlists) in
+ alp, add_bindinglist_env sigma var bl
+ with Not_found ->
+ alp, add_bindinglist_env sigma var bl
+
+let bind_bindinglist_as_term_env alp (terms,onlybinders,termlists,binderlists) var cl =
+ try
+ let bl' = Id.List.assoc var binderlists in
+ let unify_id id na' =
+ match na' with
+ | Anonymous -> Name (rename_var (snd alp) id)
+ | Name id' ->
+ if Id.equal (rename_var (snd alp) id) id' then na' else raise No_match in
+ 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 b' =
+ match c, b' with
+ | GVar (_, id), (Inl na', bk', None, t') (* assum *) ->
+ (Inl (unify_id id na'), bk', None, t')
+ | c, (Inr p', bk', None, t') (* pattern *) ->
+ let p = pat_binder_of_term c in
+ (Inr (unify_pat p p'), bk', None, t')
+ | _ -> raise No_match in
+ let rec unify cl bl' =
+ match cl, bl' with
+ | [], [] -> []
+ | c :: cl, (Inl _, _, Some _,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
+ let sigma = (terms,onlybinders,termlists,Id.List.remove_assoc var binderlists) in
+ add_bindinglist_env sigma var bl
+ with Not_found ->
+ anomaly (str "There should be a binder list bindings this list of terms")
+
let match_fix_kind fk1 fk2 =
match (fk1,fk2) with
| GCoFix n1, GCoFix n2 -> Int.equal n1 n2
@@ -670,8 +853,8 @@ let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with
bind_binding_env alp sigma id2 na1
| (Name id1,Name id2) when is_term_meta id2 metas ->
(* We let the non-binding occurrence define the rhs and hence reason up to *)
- (* alpha-conversion for the given occurrence of the name (see #)) *)
- (fst alp,(id1,id2)::snd alp), sigma
+ (* alpha-conversion for the given occurrence of the name (see #4592)) *)
+ bind_term_as_binding_env alp sigma id2 id1
| (Anonymous,Name id2) when is_term_meta id2 metas ->
(* We let the non-binding occurrence define the rhs *)
alp, sigma
@@ -691,8 +874,14 @@ let rec match_cases_pattern_binders metas acc pat1 pat2 =
let glue_letin_with_decls = true
let rec match_iterated_binders islambda decls = function
+ | GLambda (_,Name p,bk,t,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],b)]))
+ when islambda && Id.equal p e ->
+ match_iterated_binders islambda ((Inr cp,bk,None,t)::decls) b
| GLambda (_,na,bk,t,b) when islambda ->
match_iterated_binders islambda ((Inl na,bk,None,t)::decls) b
+ | GProd (_,Name p,bk,t,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],b)]))
+ when not islambda && Id.equal p e ->
+ match_iterated_binders islambda ((Inr cp,bk,None,t)::decls) b
| GProd (_,(Name _ as na),bk,t,b) when not islambda ->
match_iterated_binders islambda ((Inl na,bk,None,t)::decls) b
| GLetIn (loc,na,c,b) when glue_letin_with_decls ->
@@ -703,35 +892,51 @@ let rec match_iterated_binders islambda decls = function
let remove_sigma x (terms,onlybinders,termlists,binderlists) =
(Id.List.remove_assoc x terms,onlybinders,termlists,binderlists)
+let remove_bindinglist_sigma x (terms,onlybinders,termlists,binderlists) =
+ (terms,onlybinders,termlists,Id.List.remove_assoc x binderlists)
+
let add_ldots_var metas = (ldots_var,((None,[]),NtnTypeConstr))::metas
-let match_abinderlist_with_app match_fun metas sigma rest x iter termin =
- let rec aux sigma acc rest =
+let add_meta_bindinglist x metas = (x,((None,[]),NtnTypeBinderList))::metas
+
+let match_binderlist_with_app match_fun alp metas sigma rest x y iter termin =
+ let rec aux sigma bl rest =
try
- let (terms,_,_,binderlists as sigma) = match_fun (add_ldots_var metas) sigma rest iter in
+ let metas = add_ldots_var (add_meta_bindinglist y metas) in
+ let (terms,_,_,binderlists as sigma) = match_fun alp metas sigma rest iter in
let rest = Id.List.assoc ldots_var terms in
let b =
- match Id.List.assoc x binderlists with [b] -> b | _ ->assert false
+ match Id.List.assoc y binderlists with [b] -> b | _ ->assert false
in
- let sigma = remove_sigma x (remove_sigma ldots_var sigma) in
- aux sigma (b::acc) rest
- with No_match when not (List.is_empty acc) ->
- acc, match_fun metas sigma rest termin in
- let bl,sigma = aux sigma [] rest in
- add_bindinglist_env sigma x bl
+ let sigma = remove_bindinglist_sigma y (remove_sigma ldots_var sigma) in
+ aux sigma (b::bl) rest
+ with No_match when not (List.is_empty bl) ->
+ bl, rest, sigma in
+ let bl,rest,sigma = aux sigma [] rest in
+ let alp,sigma = bind_bindinglist_env alp sigma x bl in
+ match_fun alp metas sigma rest termin
+
+let add_meta_term x metas = (x,((None,[]),NtnTypeConstr))::metas
-let match_alist match_fun metas sigma rest x iter termin lassoc =
+let match_termlist match_fun alp metas sigma rest x y iter termin lassoc =
let rec aux sigma acc rest =
try
- let (terms,_,_,_ as sigma) = match_fun (add_ldots_var metas) sigma rest iter in
+ let metas = add_ldots_var (add_meta_term y metas) in
+ let (terms,_,_,_ as sigma) = match_fun metas sigma rest iter in
let rest = Id.List.assoc ldots_var terms in
- let t = Id.List.assoc x terms in
- let sigma = remove_sigma x (remove_sigma ldots_var sigma) in
+ let t = Id.List.assoc y terms in
+ let sigma = remove_sigma y (remove_sigma ldots_var sigma) in
aux sigma (t::acc) rest
with No_match when not (List.is_empty acc) ->
acc, match_fun metas sigma rest termin in
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 l = if lassoc then l else List.rev l in
+ if is_bindinglist_meta x metas then
+ (* This is a recursive pattern for both bindings and terms; it is *)
+ (* registered for binders *)
+ bind_bindinglist_as_term_env alp sigma x l
+ else
+ bind_termlist_env alp sigma x l
let does_not_come_from_already_eta_expanded_var =
(* This is hack to avoid looping on a rule with rhs of the form *)
@@ -750,46 +955,58 @@ let rec match_ inner u alp metas sigma a1 a2 =
(* Matching notation variable *)
| r1, NVar id2 when is_term_meta id2 metas -> bind_term_env alp sigma id2 r1
- | GVar (_,id1), NVar id2 when is_onlybinding_meta id2 metas -> snd (bind_binding_env alp sigma id2 (Name id1))
+ | GVar (_,id1), NVar id2 when is_onlybinding_meta id2 metas -> bind_binding_as_term_env alp sigma id2 id1
+ | r1, NVar id2 when is_bindinglist_meta id2 metas -> bind_term_env alp sigma id2 r1
(* Matching recursive notations for terms *)
- | r1, NList (x,_,iter,termin,lassoc) ->
- match_alist (match_hd u alp) metas sigma r1 x iter termin lassoc
+ | r1, NList (x,y,iter,termin,lassoc) ->
+ match_termlist (match_hd u alp) alp metas sigma r1 x y iter termin lassoc
(* "λ p, let 'cp = p in t" -> "λ 'cp, t" *)
- | GLambda (_,Name p,bk,t1,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],t)])),
- NBinderList (x,_,NLambda (Name id2,_,b2),(NVar v as termin)) when p = e ->
- let decls = [(Inr cp,bk,None,t1)] in
- match_in u alp metas (add_bindinglist_env sigma x decls) t termin
+ | GLambda (_,Name p,bk,t1,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],b1)])),
+ NBinderList (x,_,NLambda (Name _id2,_,b2),termin) when Id.equal p e ->
+ let (decls,b) = match_iterated_binders true [(Inr cp,bk,None,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)->
+ | GLambda (_,na1,bk,t1,b1), NBinderList (x,_,NLambda (Name _id2,_,b2),termin)->
let (decls,b) = match_iterated_binders true [(Inl na1,bk,None,t1)] b1 in
(* TODO: address the possibility that termin is a Lambda itself *)
- match_in u alp metas (add_bindinglist_env sigma x decls) b termin
+ 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),_)],[(_,_,[cp],t)])),
- NBinderList (x,_,NProd (Name id2,_,b2),(NVar v as termin)) when p = e ->
- let decls = [(Inr cp,bk,None,t1)] in
- match_in u alp metas (add_bindinglist_env sigma x decls) t termin
+ | GProd (_,Name p,bk,t1,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],b1)])),
+ NBinderList (x,_,NProd (Name _id2,_,b2),(NVar v as termin)) when Id.equal p e ->
+ let (decls,b) = match_iterated_binders true [(Inr cp,bk,None,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)
+ | GProd (_,na1,bk,t1,b1), NBinderList (x,_,NProd (Name _id2,_,b2),termin)
when na1 != Anonymous ->
let (decls,b) = match_iterated_binders false [(Inl na1,bk,None,t1)] b1 in
(* TODO: address the possibility that termin is a Prod itself *)
- match_in u alp metas (add_bindinglist_env sigma x decls) b termin
+ 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 *)
- | r, NBinderList (x,_,iter,termin) ->
- match_abinderlist_with_app (match_hd u alp) metas sigma r x iter termin
+ | r, NBinderList (x,y,iter,termin) ->
+ match_binderlist_with_app (match_hd u) alp metas sigma r x y iter termin
(* Matching individual binders as part of a recursive pattern *)
+ | GLambda (_,Name p,bk,t,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],b1)])),
+ NLambda (Name id,_,b2)
+ when is_bindinglist_meta id metas ->
+ let alp,sigma = bind_bindinglist_env alp sigma id [(Inr cp,bk,None,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 ->
- match_in u alp metas (add_bindinglist_env sigma id [(Inl na,bk,None,t)]) b1 b2
+ let alp,sigma = bind_bindinglist_env alp sigma id [(Inl na,bk,None,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 ->
- match_in u alp metas (add_bindinglist_env sigma id [(Inl na,bk,None,t)]) b1 b2
+ let alp,sigma = bind_bindinglist_env alp sigma id [(Inl na,bk,None,t)] in
+ match_in u alp metas sigma b1 b2
(* Matching compositionally *)
| GVar (_,id1), NVar id2 when alpha_var id1 id2 (fst alp) -> sigma
@@ -876,7 +1093,7 @@ let rec match_ inner u alp metas sigma a1 a2 =
| _ -> assert false in
let (alp,sigma) =
if is_bindinglist_meta id metas then
- alp, add_bindinglist_env sigma id [(Inl (Name id'),Explicit,None,t1)]
+ bind_bindinglist_env alp sigma id [(Inl (Name id'),Explicit,None,t1)]
else
match_names metas (alp,sigma) (Name id') na in
match_in u alp metas sigma (mkGApp Loc.ghost b1 (GVar (Loc.ghost,id'))) b2
@@ -921,13 +1138,15 @@ let match_notation_constr u c (metas,pat) =
List.fold_right (fun (x,(scl,typ)) (terms',termlists',binders') ->
match typ with
| NtnTypeConstr ->
- ((Id.List.assoc x terms, scl)::terms',termlists',binders')
+ let term = try Id.List.assoc x terms with Not_found -> raise No_match in
+ ((term, scl)::terms',termlists',binders')
| NtnTypeOnlyBinder ->
((find_binder x, scl)::terms',termlists',binders')
| NtnTypeConstrList ->
(terms',(Id.List.assoc x termlists,scl)::termlists',binders')
| NtnTypeBinderList ->
- (terms',termlists',(Id.List.assoc x binderlists,scl)::binders'))
+ let bl = try Id.List.assoc x binderlists with Not_found -> raise No_match in
+ (terms',termlists',(bl, scl)::binders'))
metas ([],[],[])
(* Matching cases pattern *)
@@ -944,7 +1163,21 @@ let bind_env_cases_pattern (terms,x,termlists,y as sigma) var v =
(* TODO: handle the case of multiple occs in different scopes *)
(var,v)::terms,x,termlists,y
-let rec match_cases_pattern metas (terms,x,termlists,y as sigma) a1 a2 =
+let match_cases_pattern_list match_fun metas sigma rest x y iter termin lassoc =
+ let rec aux sigma acc rest =
+ try
+ let metas = add_ldots_var (add_meta_term y metas) in
+ let (terms,_,_,_ as sigma) = match_fun metas sigma rest iter in
+ let rest = Id.List.assoc ldots_var terms in
+ let t = Id.List.assoc y terms in
+ let sigma = remove_sigma y (remove_sigma ldots_var sigma) in
+ aux sigma (t::acc) rest
+ with No_match when not (List.is_empty acc) ->
+ acc, match_fun metas sigma rest termin in
+ 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) a1 a2 =
match (a1,a2) with
| r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 r1),(0,[])
| PatVar (_,Anonymous), NHole _ -> sigma,(0,[])
@@ -960,9 +1193,9 @@ let rec match_cases_pattern metas (terms,x,termlists,y as sigma) a1 a2 =
else
let l1',more_args = Util.List.chop le2 l1 in
(List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(le2,more_args)
- | r1, NList (x,_,iter,termin,lassoc) ->
- (match_alist (match_cases_pattern_no_more_args)
- metas (terms,(),termlists,()) r1 x iter termin lassoc),(0,[])
+ | r1, NList (x,y,iter,termin,lassoc) ->
+ (match_cases_pattern_list (match_cases_pattern_no_more_args)
+ metas (terms,(),termlists,()) r1 x y iter termin lassoc),(0,[])
| _ -> raise No_match
and match_cases_pattern_no_more_args metas sigma a1 a2 =
diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index 0f1b1a8756..854e222e30 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -23,7 +23,7 @@ val subst_interpretation :
val ldots_var : Id.t
-(** {5 Translation back and forth between [glob_constr] and [notation_constr] *)
+(** {5 Translation back and forth between [glob_constr] and [notation_constr]} *)
(** Translate a [glob_constr] into a notation given the list of variables
bound by the notation; also interpret recursive patterns *)
@@ -40,7 +40,7 @@ val glob_constr_of_notation_constr_with_binders : Loc.t ->
val glob_constr_of_notation_constr : Loc.t -> notation_constr -> glob_constr
-(** {5 Matching a notation pattern against a [glob_constr] *)
+(** {5 Matching a notation pattern against a [glob_constr]} *)
(** [match_notation_constr] matches a [glob_constr] against a notation
interpretation; raise [No_match] if the matching fails *)
@@ -64,5 +64,5 @@ val match_notation_constr_ind_pattern :
((cases_pattern * subscopes) list * (cases_pattern list * subscopes) list) *
(int * cases_pattern list)
-(** {5 Matching a notation pattern against a [glob_constr] *)
+(** {5 Matching a notation pattern against a [glob_constr]} *)
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 7e42c1a227..388ca08050 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -8,7 +8,7 @@
(* Reserved names *)
-open Errors
+open CErrors
open Util
open Pp
open Names
diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml
index 1f28ba6569..478774219e 100644
--- a/interp/smartlocate.ml
+++ b/interp/smartlocate.ml
@@ -13,7 +13,7 @@
(* *)
open Pp
-open Errors
+open CErrors
open Libnames
open Globnames
open Misctypes
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index 7170fd14a5..d2dcbd92aa 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Errors
+open CErrors
open Util
open Pp
open Names
@@ -43,7 +43,7 @@ let is_alias_of_already_visible_name sp = function
false
let open_syntax_constant i ((sp,kn),(_,pat,onlyparse)) =
- if not (is_alias_of_already_visible_name sp pat) then begin
+ if not (Int.equal i 1 && is_alias_of_already_visible_name sp pat) then begin
Nametab.push_syndef (Nametab.Exactly i) sp kn;
match onlyparse with
| None ->
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 4109bdb7f5..2b860173a6 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -8,7 +8,7 @@
(*i*)
open Pp
-open Errors
+open CErrors
open Util
open Names
open Nameops
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 09:29:38 +0000