aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrexpr_ops.ml97
-rw-r--r--interp/constrexpr_ops.mli5
-rw-r--r--interp/constrextern.ml33
-rw-r--r--interp/constrintern.ml569
-rw-r--r--interp/constrintern.mli2
-rw-r--r--interp/coqlib.ml2
-rw-r--r--interp/dumpglob.ml9
-rw-r--r--interp/dumpglob.mli2
-rw-r--r--interp/implicit_quantifiers.ml3
-rw-r--r--interp/notation.ml117
-rw-r--r--interp/notation.mli5
-rw-r--r--interp/notation_ops.ml448
-rw-r--r--interp/notation_ops.mli15
-rw-r--r--interp/reserve.ml2
-rw-r--r--interp/smartlocate.ml2
-rw-r--r--interp/syntax_def.ml48
-rw-r--r--interp/syntax_def.mli6
-rw-r--r--interp/topconstr.ml13
18 files changed, 954 insertions, 424 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index c5730e6261..04429851fd 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -40,7 +40,7 @@ let names_of_local_assums bl =
List.flatten (List.map (function LocalRawAssum(l,_,_)->l|_->[]) bl)
let names_of_local_binders bl =
- List.flatten (List.map (function LocalRawAssum(l,_,_)->l|LocalRawDef(l,_)->[l]) bl)
+ List.flatten (List.map (function LocalRawAssum(l,_,_)->l|LocalRawDef(l,_)->[l]|LocalPattern _ -> assert false) bl)
(**********************************************************************)
(* Functions on constr_expr *)
@@ -260,6 +260,7 @@ let cases_pattern_expr_loc = function
| CPatRecord (loc, _) -> loc
| CPatPrim (loc,_) -> loc
| CPatDelimiters (loc,_,_) -> loc
+ | CPatCast(loc,_,_) -> loc
let raw_cases_pattern_expr_loc = function
| RCPatAlias (loc,_,_) -> loc
@@ -271,6 +272,7 @@ let local_binder_loc = function
| LocalRawAssum ((loc,_)::_,_,t)
| LocalRawDef ((loc,_),t) -> Loc.merge loc (constr_loc t)
| LocalRawAssum ([],_,_) -> assert false
+ | LocalPattern (loc,_,_) -> loc
let local_binders_loc bll = match bll with
| [] -> Loc.ghost
@@ -292,23 +294,74 @@ let mkAppC (f,l) =
| CApp (_,g,l') -> CApp (Loc.ghost, g, l' @ l)
| _ -> CApp (Loc.ghost, (None, f), l)
-let rec mkCProdN loc bll c =
- match bll with
- | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll ->
- CProdN (loc,[idl,bk,t],mkCProdN (Loc.merge loc1 loc) bll c)
- | LocalRawDef ((loc1,_) as id,b) :: bll ->
- CLetIn (loc,id,b,mkCProdN (Loc.merge loc1 loc) bll c)
- | [] -> c
- | LocalRawAssum ([],_,_) :: bll -> mkCProdN loc bll c
-
-let rec mkCLambdaN loc bll c =
- match bll with
- | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll ->
- CLambdaN (loc,[idl,bk,t],mkCLambdaN (Loc.merge loc1 loc) bll c)
- | LocalRawDef ((loc1,_) as id,b) :: bll ->
- CLetIn (loc,id,b,mkCLambdaN (Loc.merge loc1 loc) bll c)
- | [] -> c
- | LocalRawAssum ([],_,_) :: bll -> mkCLambdaN loc bll c
+let add_name_in_env env n =
+ match snd n with
+ | Anonymous -> env
+ | Name id -> id :: env
+
+let (fresh_var, fresh_var_hook) = Hook.make ~default:(fun _ _ -> assert false) ()
+
+let expand_pattern_binders mkC bl c =
+ let rec loop bl c =
+ match bl with
+ | [] -> ([], [], c)
+ | b :: bl ->
+ let (env, bl, c) = loop bl c in
+ match b with
+ | LocalRawDef (n, _) ->
+ let env = add_name_in_env env n in
+ (env, b :: bl, c)
+ | LocalRawAssum (nl, _, _) ->
+ let env = List.fold_left add_name_in_env env nl in
+ (env, b :: bl, c)
+ | LocalPattern (loc, p, ty) ->
+ let ni = Hook.get fresh_var env c in
+ let id = (loc, Name ni) in
+ let b =
+ LocalRawAssum
+ ([id], Default Explicit,
+ match ty with
+ | Some ty -> ty
+ | None -> CHole (loc, None, IntroAnonymous, None))
+ in
+ let e = CRef (Libnames.Ident (loc, ni), None) in
+ let c =
+ CCases
+ (loc, LetPatternStyle, None, [(e,None,None)],
+ [(loc, [(loc,[p])], mkC loc bl c)])
+ in
+ (ni :: env, [b], c)
+ in
+ let (_, bl, c) = loop bl c in
+ (bl, c)
+
+let mkCProdN loc bll c =
+ let rec loop loc bll c =
+ match bll with
+ | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll ->
+ CProdN (loc,[idl,bk,t],loop (Loc.merge loc1 loc) bll c)
+ | LocalRawDef ((loc1,_) as id,b) :: bll ->
+ CLetIn (loc,id,b,loop (Loc.merge loc1 loc) bll c)
+ | [] -> c
+ | LocalRawAssum ([],_,_) :: bll -> loop loc bll c
+ | LocalPattern (loc,p,ty) :: bll -> assert false
+ in
+ let (bll, c) = expand_pattern_binders loop bll c in
+ loop loc bll c
+
+let mkCLambdaN loc bll c =
+ let rec loop loc bll c =
+ match bll with
+ | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll ->
+ CLambdaN (loc,[idl,bk,t],loop (Loc.merge loc1 loc) bll c)
+ | LocalRawDef ((loc1,_) as id,b) :: bll ->
+ CLetIn (loc,id,b,loop (Loc.merge loc1 loc) bll c)
+ | [] -> c
+ | LocalRawAssum ([],_,_) :: bll -> loop loc bll c
+ | LocalPattern (loc,p,ty) :: bll -> assert false
+ in
+ let (bll, c) = expand_pattern_binders loop bll c in
+ loop loc bll c
let rec abstract_constr_expr c = function
| [] -> c
@@ -316,6 +369,7 @@ let rec abstract_constr_expr c = function
| LocalRawAssum (idl,bk,t)::bl ->
List.fold_right (fun x b -> mkLambdaC([x],bk,t,b)) idl
(abstract_constr_expr c bl)
+ | LocalPattern _::_ -> assert false
let rec prod_constr_expr c = function
| [] -> c
@@ -323,22 +377,23 @@ let rec prod_constr_expr c = function
| LocalRawAssum (idl,bk,t)::bl ->
List.fold_right (fun x b -> mkProdC([x],bk,t,b)) idl
(prod_constr_expr c bl)
+ | LocalPattern _::_ -> assert false
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/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index 3f5be48559..a92da035f6 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -58,6 +58,11 @@ val mkCLambdaN : Loc.t -> local_binder list -> constr_expr -> constr_expr
val mkCProdN : Loc.t -> local_binder list -> constr_expr -> constr_expr
(** Same as [prod_constr_expr], with location *)
+val fresh_var_hook : (Names.Id.t list -> Constrexpr.constr_expr -> Names.Id.t) Hook.t
+val expand_pattern_binders :
+ (Loc.t -> local_binder list -> constr_expr -> constr_expr) ->
+ local_binder list -> constr_expr -> local_binder list * constr_expr
+
(** {6 Destructors}*)
val coerce_reference_to_id : reference -> Id.t
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 82fa85f69e..dd8a48b85e 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
@@ -149,17 +149,8 @@ let extern_evar loc n l = CEvar (loc,n,l)
For instance, in the debugger the tables of global references
may be inaccurate *)
-let safe_shortest_qualid_of_global vars r =
- try shortest_qualid_of_global vars r
- with Not_found ->
- match r with
- | VarRef v -> make_qualid DirPath.empty v
- | ConstRef c -> make_qualid DirPath.empty Names.(Label.to_id (con_label c))
- | IndRef (i,_) | ConstructRef ((i,_),_) ->
- make_qualid DirPath.empty Names.(Label.to_id (mind_label i))
-
let default_extern_reference loc vars r =
- Qualid (loc,safe_shortest_qualid_of_global vars r)
+ Qualid (loc,shortest_qualid_of_global vars r)
let my_extern_reference = ref default_extern_reference
@@ -481,7 +472,7 @@ let explicitize loc inctx impl (cf,f) args =
(!print_implicits && !print_implicits_explicit_args) ||
(is_needed_for_correct_partial_application tail imp) ||
(!print_implicits_defensive &&
- (not (is_inferable_implicit inctx n imp) || !Flags.beautify_file) &&
+ (not (is_inferable_implicit inctx n imp) || !Flags.beautify) &&
is_significant_implicit (Lazy.force a))
in
if visible then
@@ -765,6 +756,7 @@ let rec extern inctx scopes vars r =
let listdecl =
Array.mapi (fun i fi ->
let (bl,ty,def) = blv.(i), tyv.(i), bv.(i) in
+ let bl = List.map (fun (p,bk,x,t) -> (Inl p,bk,x,t)) bl in
let (assums,ids,bl) = extern_local_binder scopes vars bl in
let vars0 = List.fold_right (name_fold Id.Set.add) ids vars in
let vars1 = List.fold_right (name_fold Id.Set.add) ids vars' in
@@ -781,7 +773,8 @@ let rec extern inctx scopes vars r =
| GCoFix n ->
let listdecl =
Array.mapi (fun i fi ->
- let (_,ids,bl) = extern_local_binder scopes vars blv.(i) in
+ let bl = List.map (fun (p,bk,x,t) -> (Inl p,bk,x,t)) blv.(i) in
+ let (_,ids,bl) = extern_local_binder scopes vars bl in
let vars0 = List.fold_right (name_fold Id.Set.add) ids vars in
let vars1 = List.fold_right (name_fold Id.Set.add) ids vars' in
((Loc.ghost, fi),bl,extern_typ scopes vars0 tyv.(i),
@@ -824,13 +817,13 @@ and factorize_lambda inctx scopes vars na bk aty c =
and extern_local_binder scopes vars = function
[] -> ([],[],[])
- | (na,bk,Some bd,ty)::l ->
+ | (Inl na,bk,Some bd,ty)::l ->
let (assums,ids,l) =
extern_local_binder scopes (name_fold Id.Set.add na vars) l in
(assums,na::ids,
LocalRawDef((Loc.ghost,na), extern false scopes vars bd) :: l)
- | (na,bk,None,ty)::l ->
+ | (Inl na,bk,None,ty)::l ->
let ty = extern_typ scopes vars ty in
(match extern_local_binder scopes (name_fold Id.Set.add na vars) l with
(assums,ids,LocalRawAssum(nal,k,ty')::l)
@@ -843,6 +836,15 @@ and extern_local_binder scopes vars = function
(na::assums,na::ids,
LocalRawAssum([(Loc.ghost,na)],Default bk,ty) :: l))
+ | (Inr p,bk,Some bd,ty)::l -> assert false
+
+ | (Inr p,bk,None,ty)::l ->
+ let ty =
+ if !Flags.raw_print then Some (extern_typ scopes vars ty) else None in
+ let p = extern_cases_pattern vars p in
+ let (assums,ids,l) = extern_local_binder scopes vars l in
+ (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],
extern inctx scopes vars c)
@@ -1050,4 +1052,5 @@ let extern_constr_pattern 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 vars = vars_of_env env in
+ let a = List.map (fun (p,bk,x,t) -> (Inl p,bk,x,t)) a in
pi3 (extern_local_binder (None,[]) vars a)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 0c02c5dab2..e6340646f5 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!
*)
@@ -369,7 +369,7 @@ let check_hidden_implicit_parameters id impls =
errorlabstrm "" (strbrk "A parameter of an inductive type " ++
pr_id id ++ strbrk " is not allowed to be used as a bound variable in the type of its constructor.")
-let push_name_env ?(global_level=false) lvar implargs env =
+let push_name_env ?(global_level=false) ntnvars implargs env =
function
| loc,Anonymous ->
if global_level then
@@ -377,7 +377,6 @@ let push_name_env ?(global_level=false) lvar implargs env =
env
| loc,Name id ->
check_hidden_implicit_parameters id env.impls ;
- let (_,ntnvars) = lvar in
if Id.Map.is_empty ntnvars && Id.equal id ldots_var
then error_ldots_var loc;
set_var_scope loc id false env ntnvars;
@@ -433,14 +432,72 @@ 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 rec free_vars_of_pat il =
+ function
+ | CPatCstr (loc, c, l1, l2) ->
+ let il = List.fold_left free_vars_of_pat il (Option.default [] l1) in
+ List.fold_left free_vars_of_pat il l2
+ | CPatAtom (loc, ro) ->
+ begin match ro with
+ | Some (Ident (loc, i)) -> (loc, i) :: il
+ | Some _ | None -> il
+ end
+ | CPatNotation (loc, n, l1, l2) ->
+ let il = List.fold_left free_vars_of_pat il (fst l1) in
+ List.fold_left (List.fold_left free_vars_of_pat) il (snd l1)
+ | _ -> anomaly (str "free_vars_of_pat")
+
+let intern_local_pattern intern lvar env p =
+ List.fold_left
+ (fun env (loc, i) ->
+ let bk = Default Implicit in
+ let ty = CHole (loc, None, Misctypes.IntroAnonymous, None) in
+ let n = Name i in
+ let env, _ = intern_assumption intern lvar env [(loc, n)] bk ty in
+ env)
+ env (free_vars_of_pat [] p)
+
+type binder_data =
+ | BDRawDef of (Loc.t * glob_binder)
+ | BDPattern of
+ (Loc.t * (cases_pattern * Id.t list) *
+ (bool ref *
+ (Notation_term.tmp_scope_name option *
+ Notation_term.tmp_scope_name list)
+ option ref * Notation_term.notation_var_internalization_type)
+ Names.Id.Map.t *
+ intern_env * constr_expr)
+
+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
| LocalRawAssum(nal,bk,ty) ->
let env, bl' = intern_assumption intern lvar env nal bk ty in
+ 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,
- (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
+ | Some ty -> ty
+ | None -> CHole(loc,None,Misctypes.IntroAnonymous,None)
+ in
+ let env = intern_local_pattern intern lvar env p in
+ let cp =
+ match !intern_cases_pattern_fwd (None,env.scopes) p with
+ | (_, [(_, cp)]) -> cp
+ | _ -> assert false
+ in
+ let il = List.map snd (free_vars_of_pat [] p) in
+ (env, BDPattern(loc,(cp,il),lvar,env,tyc) :: bl)
let intern_generalization intern env lvar loc bk ak c =
let c = intern {env with unb = true} c in
@@ -509,44 +566,85 @@ let traverse_binder (terms,_,_ as subst) avoid (renaming,env) = function
in
(renaming',env), Name id'
-let make_letins = List.fold_right (fun (loc,(na,b,t)) c -> GLetIn (loc,na,b,c))
-
-let rec subordinate_letins letins = function
+type letin_param =
+ | LPLetIn of Loc.t * (Name.t * glob_constr)
+ | LPCases of Loc.t * (cases_pattern * Id.t list) * Id.t
+
+let make_letins =
+ List.fold_right
+ (fun a c ->
+ match a with
+ | LPLetIn (loc,(na,b)) ->
+ GLetIn(loc,na,b,c)
+ | LPCases (loc,(cp,il),id) ->
+ let tt = (GVar(loc,id),(Name id,None)) in
+ GCases(loc,Misctypes.LetPatternStyle,None,[tt],[(loc,il,[cp],c)]))
+
+let rec subordinate_letins intern letins = function
(* binders come in reverse order; the non-let are returned in reverse order together *)
(* with the subordinated let-in in writing order *)
- | (loc,(na,_,Some b,t))::l ->
- subordinate_letins ((loc,(na,b,t))::letins) l
- | (loc,(na,bk,None,t))::l ->
- let letins',rest = subordinate_letins [] l in
+ | BDRawDef (loc,(na,_,Some b,t))::l ->
+ subordinate_letins intern (LPLetIn (loc,(na,b))::letins) l
+ | BDRawDef (loc,(na,bk,None,t))::l ->
+ let letins',rest = subordinate_letins intern [] l in
letins',((loc,(na,bk,t)),letins)::rest
+ | BDPattern (loc,u,lvar,env,tyc) :: l ->
+ let ienv = Id.Set.elements env.ids in
+ let id = Namegen.next_ident_away (Id.of_string "pat") ienv in
+ let na = (loc, Name id) in
+ let bk = Default Explicit in
+ let _, bl' = intern_assumption intern lvar env [na] bk tyc in
+ let bl' = List.map (fun a -> BDRawDef a) bl' in
+ subordinate_letins intern (LPCases (loc,u,id)::letins) (bl'@ l)
| [] ->
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 instantiate_notation_constr loc intern (_,ntnvars as lvar) subst infos c =
+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) ->
@@ -581,26 +679,28 @@ let instantiate_notation_constr loc intern (_,ntnvars as lvar) 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 lvar) (env,[]) bl in
- let letins,bl = subordinate_letins [] bl in
- let termin = aux subst' (renaming,env) terminator 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 (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 ->
anomaly (Pp.str "Inconsistent substitution of recursive notation"))
| NProd (Name id, NHole _, c') when option_mem_assoc id binderopt ->
- let (loc,(na,bk,t)),letins = snd (Option.get binderopt) in
- GProd (loc,na,bk,t,make_letins letins (aux 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
+ GProd (loc,na,bk,t,e)
| NLambda (Name id,NHole _,c') when option_mem_assoc id binderopt ->
- let (loc,(na,bk,t)),letins = snd (Option.get binderopt) in
- GLambda (loc,na,bk,t,make_letins letins (aux subst' infos c'))
+ let a,letins = snd (Option.get binderopt) in
+ let (loc,(na,bk,t)) = a in
+ GLambda (loc,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' ->
@@ -615,7 +715,7 @@ let instantiate_notation_constr loc intern (_,ntnvars as lvar) 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
@@ -628,7 +728,7 @@ let instantiate_notation_constr loc intern (_,ntnvars as lvar) 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) ->
@@ -661,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
@@ -669,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",
@@ -698,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
@@ -763,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
@@ -775,26 +884,26 @@ let intern_non_secvar_qualid loc qid intern env lvar us args =
| GRef (_, VarRef _, _),_,_ -> raise Not_found
| r -> r
-let intern_applied_reference intern env namedctx lvar us args = function
+let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args = function
| Qualid (loc, qid) ->
let r,projapp,args2 =
- try intern_qualid loc qid intern env lvar us args
+ try intern_qualid loc qid intern env ntnvars us args
with Not_found -> error_global_not_found_loc loc qid
in
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
- let r, projapp, args2 = intern_non_secvar_qualid loc qid intern env lvar us args in
+ let r, projapp, args2 = intern_non_secvar_qualid loc qid intern env ntnvars us args in
let x, imp, scopes, l = find_appl_head_data r in
(x,imp,scopes,l), args2
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 =
@@ -952,95 +1061,122 @@ let find_pattern_variable = function
| Ident (loc,id) -> id
| Qualid (loc,_) as x -> raise (InternalizationError(loc,NotAConstructor x))
-let sort_fields mode loc l completer =
-(*mode=false if pattern and true if constructor*)
- match l with
+let check_duplicate loc fields =
+ let eq (ref1, _) (ref2, _) = eq_reference ref1 ref2 in
+ let dups = List.duplicates eq fields in
+ match dups with
+ | [] -> ()
+ | (r, _) :: _ ->
+ user_err_loc (loc, "", str "This record defines several times the field " ++
+ pr_reference r ++ str ".")
+
+(** [sort_fields ~complete loc fields completer] expects a list
+ [fields] of field assignments [f = e1; g = e2; ...], where [f, g]
+ are fields of a record and [e1] are "values" (either terms, when
+ interning a record construction, or patterns, when intering record
+ pattern-matching). It will sort the fields according to the record
+ declaration order (which is important when type-checking them in
+ presence of dependencies between fields). If the parameter
+ [complete] is true, we require the assignment to be complete: all
+ the fields of the record must be present in the
+ assignment. Otherwise the record assignment may be partial
+ (in a pattern, we may match on some fields only), and we call the
+ function [completer] to fill the missing fields; the returned
+ field assignment list is always complete. *)
+let sort_fields ~complete loc fields completer =
+ match fields with
| [] -> None
- | (refer, value)::rem ->
- let (nparams, (* the number of parameters *)
- base_constructor, (* the reference constructor of the record *)
- (max, (* number of params *)
- (first_index, (* index of the first field of the record *)
- list_proj))) (* list of projections *)
- =
- let record =
- try Recordops.find_projection
- (global_reference_of_reference refer)
- with Not_found ->
- user_err_loc (loc_of_reference refer, "intern", pr_reference refer ++ str": Not a projection")
- in
- (* elimination of the first field from the projections *)
- let rec build_patt l m i acc =
- match l with
- | [] -> (i, acc)
- | (Some name) :: b->
- (match m with
- | [] -> anomaly (Pp.str "Number of projections mismatch")
- | (_, regular)::tm ->
- let boolean = not regular in
- begin match global_reference_of_reference refer with
- | ConstRef name' when eq_constant name name' ->
- if boolean && mode then
- user_err_loc (loc, "", str"No local fields allowed in a record construction.")
- else build_patt b tm (i + 1) (i, snd acc) (* we found it *)
- | _ ->
- build_patt b tm (if boolean&&mode then i else i + 1)
- (if boolean && mode then acc
- else fst acc, (i, ConstRef name) :: snd acc)
- end)
- | None :: b-> (* we don't want anonymous fields *)
- if mode then
- user_err_loc (loc, "", str "This record contains anonymous fields.")
- else build_patt b m (i+1) acc
- (* anonymous arguments don't appear in m *)
- in
- let ind = record.Recordops.s_CONST in
- try (* insertion of Constextern.reference_global *)
- (record.Recordops.s_EXPECTEDPARAM,
- Qualid (loc, shortest_qualid_of_global Id.Set.empty (ConstructRef ind)),
- build_patt record.Recordops.s_PROJ record.Recordops.s_PROJKIND 1 (0,[]))
- with Not_found -> anomaly (Pp.str "Environment corruption for records.")
- in
- (* now we want to have all fields of the pattern indexed by their place in
- the constructor *)
- let rec sf patts accpatt =
- match patts with
- | [] -> accpatt
- | p::q->
- let refer, patt = p in
- let glob_refer = try global_reference_of_reference refer
- with |Not_found ->
- user_err_loc (loc_of_reference refer, "intern",
- str "The field \"" ++ pr_reference refer ++ str "\" does not exist.") in
- let rec add_patt l acc =
- match l with
- | [] ->
- user_err_loc
- (loc, "",
- str "This record contains fields of different records.")
- | (i, a) :: b->
- if eq_gr glob_refer a
- then (i,List.rev_append acc l)
- else add_patt b ((i,a)::acc)
- in
- let (index, projs) = add_patt (snd accpatt) [] in
- sf q ((index, patt)::fst accpatt, projs) in
- let (unsorted_indexed_pattern, remainings) =
- sf rem ([first_index, value], list_proj) in
- (* we sort them *)
- let sorted_indexed_pattern =
- List.sort (fun (i, _) (j, _) -> compare i j) unsorted_indexed_pattern in
- (* a function to complete with wildcards *)
- let rec complete_list n l =
- if n <= 1 then l else complete_list (n-1) (completer n l) in
- (* a function to remove indice *)
- let rec clean_list l i acc =
- match l with
- | [] -> complete_list (max - i) acc
- | (k, p)::q-> clean_list q k (p::(complete_list (k - i) acc))
- in
- Some (nparams, base_constructor,
- List.rev (clean_list sorted_indexed_pattern 0 []))
+ | (first_field_ref, first_field_value):: other_fields ->
+ 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")
+ in
+ (* the number of parameters *)
+ let nparams = record.Recordops.s_EXPECTEDPARAM in
+ (* the reference constructor of the record *)
+ 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 (str "Environment corruption for records") in
+ let () = check_duplicate loc fields 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 *)
+ =
+ (* elimitate the first field from the projections,
+ but keep its index *)
+ let rec build_proj_list projs proj_kinds idx ~acc_first_idx acc =
+ match projs with
+ | [] -> (idx, acc_first_idx, acc)
+ | (Some name) :: projs ->
+ let field_glob_ref = ConstRef name in
+ let first_field = eq_gr field_glob_ref first_field_glob_ref in
+ begin match proj_kinds with
+ | [] -> anomaly (Pp.str "Number of projections mismatch")
+ | (_, regular) :: proj_kinds ->
+ (* "regular" is false when the field is defined
+ by a let-in in the record declaration
+ (its value is fixed from other fields). *)
+ if first_field && not regular && complete then
+ user_err_loc (loc, "", str "No local fields allowed in a record construction.")
+ else if first_field then
+ build_proj_list projs proj_kinds (idx+1) ~acc_first_idx:idx acc
+ else if not regular && complete then
+ (* skip non-regular fields *)
+ build_proj_list projs proj_kinds idx ~acc_first_idx acc
+ else
+ build_proj_list projs proj_kinds (idx+1) ~acc_first_idx
+ ((idx, field_glob_ref) :: acc)
+ end
+ | None :: projs ->
+ if complete then
+ (* we don't want anonymous fields *)
+ user_err_loc (loc, "", str "This record contains anonymous fields.")
+ else
+ (* anonymous arguments don't appear in proj_kinds *)
+ build_proj_list projs proj_kinds (idx+1) ~acc_first_idx acc
+ in
+ build_proj_list record.Recordops.s_PROJ record.Recordops.s_PROJKIND 1 ~acc_first_idx:0 []
+ in
+ (* now we want to have all fields assignments indexed by their place in
+ the constructor *)
+ let rec index_fields fields remaining_projs acc =
+ match fields with
+ | (field_ref, field_value) :: fields ->
+ let field_glob_ref = try global_reference_of_reference field_ref
+ with Not_found ->
+ user_err_loc (loc_of_reference field_ref, "intern",
+ str "The field \"" ++ pr_reference field_ref ++ str "\" does not exist.") in
+ let remaining_projs, (field_index, _) =
+ let the_proj (idx, glob_ref) = eq_gr field_glob_ref glob_ref in
+ try CList.extract_first the_proj remaining_projs
+ with Not_found ->
+ user_err_loc
+ (loc, "",
+ str "This record contains fields of different records.")
+ in
+ index_fields fields remaining_projs ((field_index, field_value) :: acc)
+ | [] ->
+ (* the order does not matter as we sort them next,
+ List.rev_* is just for efficiency *)
+ let remaining_fields =
+ let complete_field (idx, _field_ref) = (idx, completer idx) in
+ List.rev_map complete_field remaining_projs in
+ List.rev_append remaining_fields acc
+ in
+ let unsorted_indexed_fields =
+ index_fields other_fields proj_list
+ [(first_field_index, first_field_value)] in
+ let sorted_indexed_fields =
+ let cmp_by_index (i, _) (j, _) = Int.compare i j in
+ List.sort cmp_by_index unsorted_indexed_fields in
+ let sorted_fields = List.map snd sorted_indexed_fields in
+ Some (nparams, base_constructor, sorted_fields)
(** {6 Manage multiple aliases} *)
@@ -1068,10 +1204,6 @@ let alias_of als = match als.alias_ids with
| [] -> Anonymous
| id :: _ -> Name id
-let message_redundant_alias id1 id2 =
- Feedback.msg_warning
- (str "Alias variable " ++ pr_id id1 ++ str " is merged with " ++ pr_id id2)
-
(** {6 Expanding notations }
@returns a raw_case_pattern_expr :
@@ -1140,7 +1272,7 @@ let drop_notations_pattern looked_for =
| CPatAlias (loc, p, id) -> RCPatAlias (loc, in_pat top scopes p, id)
| CPatRecord (loc, l) ->
let sorted_fields =
- sort_fields false loc l (fun _ l -> (CPatAtom (loc, None))::l) in
+ sort_fields ~complete:false loc l (fun _idx -> (CPatAtom (loc, None))) in
begin match sorted_fields with
| None -> RCPatAtom (loc, None)
| Some (n, head, pl) ->
@@ -1195,6 +1327,8 @@ let drop_notations_pattern looked_for =
| CPatAtom (loc,None) -> RCPatAtom (loc,None)
| CPatOr (loc, pl) ->
RCPatOr (loc,List.map (in_pat top scopes) pl)
+ | CPatCast _ ->
+ assert false
and in_pat_sc scopes x = in_pat false (x,snd scopes)
and in_not top loc scopes (subst,substlist as fullsubst) args = function
| NVar id ->
@@ -1219,7 +1353,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
@@ -1227,7 +1361,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
@@ -1276,11 +1410,49 @@ let rec intern_pat genv aliases pat =
check_or_pat_variables loc ids (List.tl idsl);
(ids,List.flatten pl')
+(* [check_no_patcast p] raises an error if [p] contains a cast. This code is a
+ bit ad-hoc, and is due to current restrictions on casts in patterns. We
+ support them only in local binders and only at top level. In fact, they are
+ currently eliminated by the parser. The only reason why they are in the
+ [cases_pattern_expr] type is that the parser needs to factor the "(c : t)"
+ notation with user defined notations (such as the pair). In the long term, we
+ will try to support such casts everywhere, and use them to print the domains
+ of lambdas in the encoding of match in constr. We put this check here and not
+ in the parser because it would require to duplicate the levels of the
+ [pattern] rule. *)
+let rec check_no_patcast = function
+ | CPatCast (loc,_,_) ->
+ CErrors.user_err_loc (loc, "check_no_patcast",
+ Pp.strbrk "Casts are not supported here.")
+ | CPatDelimiters(_,_,p)
+ | CPatAlias(_,p,_) -> check_no_patcast p
+ | CPatCstr(_,_,opl,pl) ->
+ Option.iter (List.iter check_no_patcast) opl;
+ List.iter check_no_patcast pl
+ | CPatOr(_,pl) ->
+ List.iter check_no_patcast pl
+ | CPatNotation(_,_,subst,pl) ->
+ check_no_patcast_subst subst;
+ List.iter check_no_patcast pl
+ | CPatRecord(_,prl) ->
+ List.iter (fun (_,p) -> check_no_patcast p) prl
+ | CPatAtom _ | CPatPrim _ -> ()
+
+and check_no_patcast_subst (pl,pll) =
+ List.iter check_no_patcast pl;
+ List.iter (List.iter check_no_patcast) pll
+
let intern_cases_pattern genv scopes aliases pat =
+ check_no_patcast pat;
intern_pat genv aliases
(drop_notations_pattern (function ConstructRef _ -> () | _ -> raise Not_found) scopes pat)
+let _ =
+ intern_cases_pattern_fwd :=
+ fun scopes p -> intern_cases_pattern (Global.env ()) scopes empty_alias p
+
let intern_ind_pattern genv scopes pat =
+ check_no_patcast pat;
let no_not =
try
drop_notations_pattern (function (IndRef _ | ConstructRef _) -> () | _ -> raise Not_found) scopes pat
@@ -1362,7 +1534,7 @@ let extract_explicit_arg imps args =
(**********************************************************************)
(* Main loop *)
-let internalize globalenv env allow_patvar lvar c =
+let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
let rec intern env = function
| CRef (ref,us) as x ->
let (c,imp,subscopes,l),_ =
@@ -1383,10 +1555,11 @@ let internalize globalenv env allow_patvar lvar c =
(fun (id,(n,order),bl,ty,_) ->
let intern_ro_arg f =
let before, after = split_at_annot bl n in
- let (env',rbefore) =
- List.fold_left intern_local_binder (env,[]) before in
+ let (env',rbefore) = List.fold_left intern_local_binder (env,[]) before in
+ let rbefore = List.map (function BDRawDef a -> a | BDPattern _ -> assert false) rbefore in
let ro = f (intern env') in
let n' = Option.map (fun _ -> List.count (fun (_,(_,_,b,_)) -> (* remove let-ins *) b = None) rbefore) n in
+ let rbefore = List.map (fun a -> BDRawDef a) rbefore in
n', ro, List.fold_left intern_local_binder (env',rbefore) after
in
let n, ro, (env',rbl) =
@@ -1398,12 +1571,18 @@ let internalize globalenv env allow_patvar lvar c =
| CMeasureRec (m,r) ->
intern_ro_arg (fun f -> GMeasureRec (f m, Option.map f r))
in
- ((n, ro), List.rev rbl, intern_type env' ty, env')) dl in
+ let bl =
+ List.rev_map
+ (function
+ | BDRawDef a -> a
+ | BDPattern (loc,_,_,_,_) ->
+ Loc.raise loc (Stream.Error "pattern with quote not allowed after fix")) rbl in
+ ((n, ro), bl, intern_type env' ty, env')) dl in
let idl = Array.map2 (fun (_,_,_,_,bd) (a,b,c,env') ->
let env'' = List.fold_left_i (fun i en name ->
let (_,bli,tyi,_) = idl_temp.(i) in
let fix_args = (List.map (fun (_,(na, bk, _, _)) -> (build_impls bk na)) bli) in
- push_name_env lvar (impls_type_list ~args:fix_args tyi)
+ push_name_env ntnvars (impls_type_list ~args:fix_args tyi)
en (Loc.ghost, Name name)) 0 env' lf in
(a,b,c,intern {env'' with tmp_scope = None} bd)) dl idl_temp in
GRec (loc,GFix
@@ -1422,15 +1601,15 @@ let internalize globalenv env allow_patvar lvar c =
in
let idl_tmp = Array.map
(fun ((loc,id),bl,ty,_) ->
- let (env',rbl) =
- List.fold_left intern_local_binder (env,[]) bl in
+ let (env',rbl) = List.fold_left intern_local_binder (env,[]) bl in
+ let rbl = List.map (function BDRawDef a -> a | BDPattern _ -> assert false) rbl in
(List.rev rbl,
intern_type env' ty,env')) dl in
let idl = Array.map2 (fun (_,_,_,bd) (b,c,env') ->
let env'' = List.fold_left_i (fun i en name ->
let (bli,tyi,_) = idl_tmp.(i) in
let cofix_args = List.map (fun (_, (na, bk, _, _)) -> (build_impls bk na)) bli in
- push_name_env lvar (impls_type_list ~args:cofix_args tyi)
+ push_name_env ntnvars (impls_type_list ~args:cofix_args tyi)
en (Loc.ghost, Name name)) 0 env' lf in
(b,c,intern {env'' with tmp_scope = None} bd)) dl idl_tmp in
GRec (loc,GCoFix n,
@@ -1449,15 +1628,15 @@ let internalize globalenv env allow_patvar lvar c =
| CLetIn (loc,na,c1,c2) ->
let inc1 = intern (reset_tmp_scope env) c1 in
GLetIn (loc, snd na, inc1,
- intern (push_name_env lvar (impls_term_list inc1) env na) c2)
+ intern (push_name_env ntnvars (impls_term_list inc1) env na) c2)
| CNotation (loc,"- _",([CPrim (_,Numeral p)],[],[]))
when Bigint.is_strictly_pos p ->
intern env (CPrim (loc,Numeral (Bigint.neg p)))
| CNotation (_,"( _ )",([a],[],[])) -> intern env a
| CNotation (loc,ntn,args) ->
- intern_notation intern env lvar loc ntn args
+ intern_notation intern env ntnvars loc ntn args
| CGeneralization (loc,b,a,c) ->
- intern_generalization intern env lvar loc b a c
+ intern_generalization intern env ntnvars loc b a c
| CPrim (loc, p) ->
fst (Notation.interp_prim_token loc p (env.tmp_scope,env.scopes))
| CDelimiters (loc, key, e) ->
@@ -1485,7 +1664,7 @@ let internalize globalenv env allow_patvar lvar c =
intern_applied_reference intern env
(Environ.named_context globalenv) lvar us args ref
| CNotation (loc,ntn,([],[],[])) ->
- let c = intern_notation intern env lvar loc ntn ([],[],[]) in
+ let c = intern_notation intern env ntnvars loc ntn ([],[],[]) in
let x, impl, scopes, l = find_appl_head_data c in
(x,impl,scopes,l), args
| x -> (intern env f,[],[],[]), args in
@@ -1493,12 +1672,14 @@ let internalize globalenv env allow_patvar lvar c =
(merge_impargs l args) loc
| CRecord (loc, fs) ->
- let cargs =
- sort_fields true loc fs
- (fun k l -> CHole (loc, Some (Evar_kinds.QuestionMark (Evar_kinds.Define true)), Misctypes.IntroAnonymous, None) :: l)
- in
- begin
- match cargs with
+ 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) ->
let pars = List.make n (CHole (loc, None, Misctypes.IntroAnonymous, None)) in
@@ -1518,7 +1699,7 @@ let internalize globalenv env allow_patvar lvar c =
(tm,ind)::inds, Option.fold_right Id.Set.add extra_id ex_ids, List.rev_append match_td matchs)
tms ([],Id.Set.empty,[]) in
let env' = Id.Set.fold
- (fun var bli -> push_name_env lvar (Variable,[],[],[]) bli (Loc.ghost,Name var))
+ (fun var bli -> push_name_env ntnvars (Variable,[],[],[]) bli (Loc.ghost,Name var))
(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 =
@@ -1552,22 +1733,24 @@ let internalize globalenv env allow_patvar lvar c =
(* "in" is None so no match to add *)
let ((b',(na',_)),_,_) = intern_case_item env' Id.Set.empty (b,na,None) in
let p' = Option.map (fun u ->
- let env'' = push_name_env lvar (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env')
+ let env'' = push_name_env ntnvars (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env')
(Loc.ghost,na') in
intern_type env'' u) po in
GLetTuple (loc, List.map snd nal, (na', p'), b',
- intern (List.fold_left (push_name_env lvar (Variable,[],[],[])) (reset_hidden_inductive_implicit_test env) nal) c)
+ intern (List.fold_left (push_name_env ntnvars (Variable,[],[],[])) (reset_hidden_inductive_implicit_test env) nal) c)
| CIf (loc, c, (na,po), b1, b2) ->
let env' = reset_tmp_scope env in
let ((c',(na',_)),_,_) = intern_case_item env' Id.Set.empty (c,na,None) in (* no "in" no match to ad too *)
let p' = Option.map (fun p ->
- let env'' = push_name_env lvar (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env)
+ let env'' = push_name_env ntnvars (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env)
(Loc.ghost,na') in
intern_type env'' p) po in
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
@@ -1606,7 +1789,7 @@ let internalize globalenv env allow_patvar lvar c =
and intern_type env = intern (set_type_scope env)
and intern_local_binder env bind =
- intern_local_binder_aux intern lvar env bind
+ intern_local_binder_aux intern ntnvars env bind
(* Expands a multiple pattern into a disjunction of multiple patterns *)
and intern_multiple_pattern env n (loc,pl) =
@@ -1631,7 +1814,6 @@ let internalize globalenv env allow_patvar lvar c =
let env_ids = List.fold_right Id.Set.add eqn_ids env.ids in
List.map (fun (asubst,pl) ->
let rhs = replace_vars_constr_expr asubst rhs in
- Id.Map.iter message_redundant_alias asubst;
let rhs' = intern {env with ids = env_ids} rhs in
(loc,eqn_ids,pl,rhs')) pll
@@ -1685,11 +1867,11 @@ let internalize globalenv env allow_patvar lvar c =
(tm',(snd na,typ)), extra_id, match_td
and iterate_prod loc2 env bk ty body nal =
- let env, bl = intern_assumption intern lvar env nal bk ty in
+ let env, bl = intern_assumption intern ntnvars env nal bk ty in
it_mkGProd loc2 bl (intern_type env body)
and iterate_lam loc2 env bk ty body nal =
- let env, bl = intern_assumption intern lvar env nal bk ty in
+ let env, bl = intern_assumption intern ntnvars env nal bk ty in
it_mkGLambda loc2 bl (intern env body)
and intern_impargs c env l subscopes args =
@@ -1865,14 +2047,14 @@ let interp_notation_constr ?(impls=empty_internalization_env) nenv a =
tmp_scope = None; scopes = []; impls = impls}
false (empty_ltac_sign, vl) a in
(* Translate and check that [c] has all its free variables bound in [vars] *)
- let a = notation_constr_of_glob_constr nenv c in
+ let a, reversible = notation_constr_of_glob_constr nenv c in
(* Splits variables into those that are binding, bound, or both *)
(* binding and bound *)
let out_scope = function None -> None,[] | Some (a,l) -> a,l in
let vars = Id.Map.map (fun (isonlybinding, sc, typ) ->
(!isonlybinding, out_scope !sc, typ)) vl in
(* Returns [a] and the ordered list of variables with their scopes *)
- vars, a
+ vars, a, reversible
(* Interpret binders and contexts *)
@@ -1895,7 +2077,16 @@ let intern_context global_level env impl_env binders =
try
let lvar = (empty_ltac_sign, Id.Map.empty) in
let lenv, bl = List.fold_left
- (intern_local_binder_aux ~global_level (my_intern_constr env lvar) lvar)
+ (fun (lenv, bl) b ->
+ let bl = List.map (fun a -> BDRawDef a) bl in
+ let (env, bl) = intern_local_binder_aux ~global_level (my_intern_constr env lvar) Id.Map.empty (lenv, bl) b in
+ let bl =
+ List.map
+ (function
+ | BDRawDef a -> a
+ | BDPattern (loc,_,_,_,_) ->
+ Loc.raise loc (Stream.Error "pattern with quote not allowed here")) bl in
+ (env, bl))
({ids = extract_ids env; unb = false;
tmp_scope = None; scopes = []; impls = impl_env}, []) binders in
(lenv.impls, List.map snd bl)
@@ -1906,11 +2097,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
@@ -1920,8 +2113,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/constrintern.mli b/interp/constrintern.mli
index eea76aa310..61e7c6f5cb 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -186,7 +186,7 @@ val global_reference_in_absolute_module : DirPath.t -> Id.t -> constr
val interp_notation_constr : ?impls:internalization_env ->
notation_interp_env -> constr_expr ->
(bool * subscopes * notation_var_internalization_type) Id.Map.t *
- notation_constr
+ notation_constr * reversibility_flag
(** Globalization options *)
val parsing_explicit : bool ref
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 567150a5d6..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
@@ -112,6 +112,7 @@ let free_vars_of_binders ?(bound=Id.Set.empty) l (binders : local_binder list) =
let l' = free_vars_of_constr_expr c ~bound:bdvars l in
aux (Id.Set.union (ids_of_list bound) bdvars) l' tl
+ | LocalPattern _ :: tl -> assert false
| [] -> bdvars, l
in aux bound l binders
diff --git a/interp/notation.ml b/interp/notation.ml
index 7ad104d036..389a1c9dff 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -7,7 +7,7 @@
(************************************************************************)
(*i*)
-open Errors
+open CErrors
open Util
open Pp
open Bigint
@@ -44,8 +44,14 @@ type level = precedence * tolerability list
type delimiters = string
type notation_location = (DirPath.t * DirPath.t) * string
+type notation_data = {
+ not_interp : interpretation;
+ not_location : notation_location;
+ not_onlyprinting : bool;
+}
+
type scope = {
- notations: (interpretation * notation_location) String.Map.t;
+ notations: notation_data String.Map.t;
delimiters: delimiters option
}
@@ -184,7 +190,8 @@ let declare_delimiters scope key =
| None -> scope_map := String.Map.add scope newsc !scope_map
| Some oldkey when String.equal oldkey key -> ()
| Some oldkey ->
- Feedback.msg_warning
+ (** FIXME: implement multikey scopes? *)
+ Flags.if_verbose Feedback.msg_info
(str "Overwriting previous delimiting key " ++ str oldkey ++ str " in scope " ++ str scope);
scope_map := String.Map.add scope newsc !scope_map
end;
@@ -192,7 +199,7 @@ let declare_delimiters scope key =
let oldscope = String.Map.find key !delimiters_map in
if String.equal oldscope scope then ()
else begin
- Feedback.msg_warning (str "Hiding binding of key " ++ str key ++ str " to " ++ str oldscope);
+ Flags.if_verbose Feedback.msg_info (str "Hiding binding of key " ++ str key ++ str " to " ++ str oldscope);
delimiters_map := String.Map.add key scope !delimiters_map
end
with Not_found -> delimiters_map := String.Map.add key scope !delimiters_map
@@ -201,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 -> Feedback.msg_warning (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
@@ -380,17 +387,28 @@ let level_of_notation ntn =
(* The mapping between notations and their interpretation *)
-let declare_notation_interpretation ntn scopt pat df =
+let warn_notation_overridden =
+ CWarnings.create ~name:"notation-overridden" ~category:"parsing"
+ (fun (ntn,which_scope) ->
+ str "Notation" ++ spc () ++ str ntn ++ spc ()
+ ++ strbrk "was already used" ++ which_scope)
+
+let declare_notation_interpretation ntn scopt pat df ~onlyprint =
let scope = match scopt with Some s -> s | None -> default_scope in
let sc = find_scope scope in
let () =
if String.Map.mem ntn sc.notations then
let which_scope = match scopt with
| None -> mt ()
- | Some _ -> str " in scope " ++ str scope in
- Feedback.msg_warning (str "Notation " ++ str ntn ++ str " was already used" ++ which_scope)
+ | Some _ -> spc () ++ strbrk "in scope" ++ spc () ++ str scope in
+ warn_notation_overridden (ntn,which_scope)
in
- let sc = { sc with notations = String.Map.add ntn (pat,df) sc.notations } in
+ let notdata = {
+ not_interp = pat;
+ not_location = df;
+ not_onlyprinting = onlyprint;
+ } in
+ let sc = { sc with notations = String.Map.add ntn notdata sc.notations } in
let () = scope_map := String.Map.add scope sc !scope_map in
begin match scopt with
| None -> scope_stack := SingleNotation ntn :: !scope_stack
@@ -415,7 +433,9 @@ let rec find_interpretation ntn find = function
find_interpretation ntn find scopes
let find_notation ntn sc =
- String.Map.find ntn (find_scope sc).notations
+ let n = String.Map.find ntn (find_scope sc).notations in
+ let () = if n.not_onlyprinting then raise Not_found in
+ (n.not_interp, n.not_location)
let notation_of_prim_token = function
| Numeral n when is_pos_or_zero n -> to_string n
@@ -533,22 +553,20 @@ let ntpe_eq t1 t2 = match t1, t2 with
| NtnTypeBinderList, NtnTypeBinderList -> true
| (NtnTypeConstr | NtnTypeOnlyBinder | NtnTypeConstrList | NtnTypeBinderList), _ -> false
-
-let vars_eq (id1, (sc1, tp1)) (id2, (sc2, tp2)) =
- Id.equal id1 id2 &&
+let var_attributes_eq (_, (sc1, tp1)) (_, (sc2, tp2)) =
pair_eq (Option.equal String.equal) (List.equal String.equal) sc1 sc2 &&
ntpe_eq tp1 tp2
let interpretation_eq (vars1, t1) (vars2, t2) =
- List.equal vars_eq vars1 vars2 &&
- Notation_ops.eq_notation_constr t1 t2
+ List.equal var_attributes_eq vars1 vars2 &&
+ Notation_ops.eq_notation_constr (List.map fst vars1, List.map fst vars2) t1 t2
let exists_notation_in_scope scopt ntn r =
let scope = match scopt with Some s -> s | None -> default_scope in
try
let sc = String.Map.find scope !scope_map in
- let (r',_) = String.Map.find ntn sc.notations in
- interpretation_eq r' r
+ let n = String.Map.find ntn sc.notations in
+ interpretation_eq n.not_interp r
with Not_found -> false
let isNVar_or_NHole = function NVar _ | NHole _ -> true | _ -> false
@@ -638,7 +656,7 @@ type arguments_scope_discharge_request =
| ArgsScopeManual
| ArgsScopeNoDischarge
-let load_arguments_scope _ (_,(_,r,scl,cls)) =
+let load_arguments_scope _ (_,(_,r,n,scl,cls)) =
List.iter (Option.iter check_scope) scl;
let initial_stamp = ScopeClassMap.empty in
arguments_scope := Refmap.add r (scl,cls,initial_stamp) !arguments_scope
@@ -649,7 +667,7 @@ let cache_arguments_scope o =
let subst_scope_class subst cs =
try Some (subst_cl_typ subst cs) with Not_found -> None
-let subst_arguments_scope (subst,(req,r,scl,cls)) =
+let subst_arguments_scope (subst,(req,r,n,scl,cls)) =
let r' = fst (subst_global subst r) in
let subst_cl ocl = match ocl with
| None -> ocl
@@ -658,34 +676,42 @@ let subst_arguments_scope (subst,(req,r,scl,cls)) =
| Some cl' as ocl' when cl' != cl -> ocl'
| _ -> ocl in
let cls' = List.smartmap subst_cl cls in
- (ArgsScopeNoDischarge,r',scl,cls')
+ (ArgsScopeNoDischarge,r',n,scl,cls')
-let discharge_arguments_scope (_,(req,r,l,_)) =
+let discharge_arguments_scope (_,(req,r,n,l,_)) =
if req == ArgsScopeNoDischarge || (isVarRef r && Lib.is_in_section r) then None
- else Some (req,Lib.discharge_global r,l,[])
+ else
+ let n =
+ try
+ let vars = Lib.variable_section_segment_of_reference r in
+ List.length (List.filter (fun (_,_,b,_) -> b = None) vars)
+ with
+ Not_found (* Not a ref defined in this section *) -> 0 in
+ Some (req,Lib.discharge_global r,n,l,[])
-let classify_arguments_scope (req,_,_,_ as obj) =
+let classify_arguments_scope (req,_,_,_,_ as obj) =
if req == ArgsScopeNoDischarge then Dispose else Substitute obj
-let rebuild_arguments_scope (req,r,l,_) =
+let rebuild_arguments_scope (req,r,n,l,_) =
match req with
| ArgsScopeNoDischarge -> assert false
| ArgsScopeAuto ->
let scs,cls = compute_arguments_scope_full (fst(Universes.type_of_global r)(*FIXME?*)) in
- (req,r,scs,cls)
+ (req,r,List.length scs,scs,cls)
| ArgsScopeManual ->
(* Add to the manually given scopes the one found automatically
for the extra parameters of the section. Discard the classes
of the manually given scopes to avoid further re-computations. *)
- let l',cls = compute_arguments_scope_full (Global.type_of_global_unsafe r) in
- let nparams = List.length l' - List.length l in
- let l1 = List.firstn nparams l' in
- let cls1 = List.firstn nparams cls in
- (req,r,l1@l,cls1)
+ let l',cls = compute_arguments_scope_full (Global.type_of_global_unsafe r) in
+ let l1 = List.firstn n l' in
+ let cls1 = List.firstn n cls in
+ (req,r,0,l1@l,cls1)
type arguments_scope_obj =
arguments_scope_discharge_request * global_reference *
- scope_name option list * scope_class option list
+ (* Used to communicate information from discharge to rebuild *)
+ (* set to 0 otherwise *) int *
+ scope_name option list * scope_class option list
let inArgumentsScope : arguments_scope_obj -> obj =
declare_object {(default_object "ARGUMENTS-SCOPE") with
@@ -698,16 +724,15 @@ let inArgumentsScope : arguments_scope_obj -> obj =
let is_local local ref = local || isVarRef ref && Lib.is_in_section ref
-let declare_arguments_scope_gen req r (scl,cls) =
- Lib.add_anonymous_leaf (inArgumentsScope (req,r,scl,cls))
+let declare_arguments_scope_gen req r n (scl,cls) =
+ Lib.add_anonymous_leaf (inArgumentsScope (req,r,n,scl,cls))
let declare_arguments_scope local r scl =
- let req = if is_local local r then ArgsScopeNoDischarge else ArgsScopeManual
- in
- (* We empty the list of argument classes to disable futher scope
+ let req = if is_local local r then ArgsScopeNoDischarge else ArgsScopeManual in
+ (* We empty the list of argument classes to disable further scope
re-computations and keep these manually given scopes. *)
- declare_arguments_scope_gen req r (scl,[])
-
+ declare_arguments_scope_gen req r 0 (scl,[])
+
let find_arguments_scope r =
try
let (scl,cls,stamp) = Refmap.find r !arguments_scope in
@@ -722,7 +747,8 @@ let find_arguments_scope r =
let declare_ref_arguments_scope ref =
let t = Global.type_of_global_unsafe ref in
- declare_arguments_scope_gen ArgsScopeAuto ref (compute_arguments_scope_full t)
+ let (scs,cls as o) = compute_arguments_scope_full t in
+ declare_arguments_scope_gen ArgsScopeAuto ref (List.length scs) o
(********************************)
@@ -805,7 +831,7 @@ let pr_named_scope prglob scope sc =
++ fnl ()
++ pr_scope_classes scope
++ String.Map.fold
- (fun ntn ((_,r),(_,df)) strm ->
+ (fun ntn { not_interp = (_, r); not_location = (_, df) } strm ->
pr_notation_info prglob df r ++ fnl () ++ strm)
sc.notations (mt ())
@@ -849,7 +875,7 @@ let browse_notation strict ntn map =
let l =
String.Map.fold
(fun scope_name sc ->
- String.Map.fold (fun ntn ((_,r),df) l ->
+ String.Map.fold (fun ntn { not_interp = (_, r); not_location = df } l ->
if find ntn then (ntn,(scope_name,r,df))::l else l) sc.notations)
map [] in
List.sort (fun x y -> String.compare (fst x) (fst y)) l
@@ -915,7 +941,7 @@ let locate_notation prglob ntn scope =
let collect_notation_in_scope scope sc known =
assert (not (String.equal scope default_scope));
String.Map.fold
- (fun ntn ((_,r),(_,df)) (l,known as acc) ->
+ (fun ntn { not_interp = (_, r); not_location = (_, df) } (l,known as acc) ->
if String.List.mem ntn known then acc else ((df,r)::l,ntn::known))
sc.notations ([],known)
@@ -931,7 +957,7 @@ let collect_notations stack =
| SingleNotation ntn ->
if String.List.mem ntn knownntn then (all,knownntn)
else
- let ((_,r),(_,df)) =
+ let { not_interp = (_, r); not_location = (_, df) } =
String.Map.find ntn (find_scope default_scope).notations in
let all' = match all with
| (s,lonelyntn)::rest when String.equal s default_scope ->
@@ -983,6 +1009,9 @@ let find_notation_parsing_rules ntn =
try pi3 (String.Map.find ntn !notation_rules)
with Not_found -> anomaly (str "No parsing rule found for " ++ str ntn)
+let get_defined_notations () =
+ String.Set.elements @@ String.Map.domain !notation_rules
+
let add_notation_extra_printing_rule ntn k v =
try
notation_rules :=
@@ -1028,6 +1057,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.mli b/interp/notation.mli
index a85dc50f2f..2e92a00a8c 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -109,7 +109,7 @@ type interp_rule =
| SynDefRule of kernel_name
val declare_notation_interpretation : notation -> scope_name option ->
- interpretation -> notation_location -> unit
+ interpretation -> notation_location -> onlyprint:bool -> unit
val declare_uninterpretation : interp_rule -> interpretation -> unit
@@ -203,6 +203,9 @@ val find_notation_extra_printing_rules : notation -> extra_unparsing_rules
val find_notation_parsing_rules : notation -> notation_grammar
val add_notation_extra_printing_rule : notation -> string -> string -> unit
+(** Returns notations with defined parsing/printing rules *)
+val get_defined_notations : unit -> notation list
+
(** Rem: printing rules for primitive token are canonical *)
val with_notation_protection : ('a -> 'b) -> 'a -> 'b
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 3efd50b17f..0c5393cf41 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
@@ -47,62 +47,62 @@ let compare_glob_constr f add t1 t2 = match t1,t2 with
| GHole _ | GSort _ | GLetIn _), _
-> false
-let rec eq_notation_constr t1 t2 = match t1, t2 with
+let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with
| NRef gr1, NRef gr2 -> eq_gr gr1 gr2
-| NVar id1, NVar id2 -> Id.equal id1 id2
+| NVar id1, NVar id2 -> Int.equal (List.index Id.equal id1 vars1) (List.index Id.equal id2 vars2)
| NApp (t1, a1), NApp (t2, a2) ->
- eq_notation_constr t1 t2 && List.equal eq_notation_constr a1 a2
+ (eq_notation_constr vars) t1 t2 && List.equal (eq_notation_constr vars) a1 a2
| NHole (_, _, _), NHole (_, _, _) -> true (** FIXME? *)
| NList (i1, j1, t1, u1, b1), NList (i2, j2, t2, u2, b2) ->
- Id.equal i1 i2 && Id.equal j1 j2 && eq_notation_constr t1 t2 &&
- eq_notation_constr u1 u2 && b1 == b2
+ Id.equal i1 i2 && Id.equal j1 j2 && (eq_notation_constr vars) t1 t2 &&
+ (eq_notation_constr vars) u1 u2 && b1 == b2
| NLambda (na1, t1, u1), NLambda (na2, t2, u2) ->
- Name.equal na1 na2 && eq_notation_constr t1 t2 && eq_notation_constr u1 u2
+ Name.equal na1 na2 && (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) u1 u2
| NProd (na1, t1, u1), NProd (na2, t2, u2) ->
- Name.equal na1 na2 && eq_notation_constr t1 t2 && eq_notation_constr u1 u2
+ Name.equal na1 na2 && (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) u1 u2
| NBinderList (i1, j1, t1, u1), NBinderList (i2, j2, t2, u2) ->
- Id.equal i1 i2 && Id.equal j1 j2 && eq_notation_constr t1 t2 &&
- eq_notation_constr u1 u2
+ Id.equal i1 i2 && Id.equal j1 j2 && (eq_notation_constr vars) t1 t2 &&
+ (eq_notation_constr vars) u1 u2
| NLetIn (na1, t1, u1), NLetIn (na2, t2, u2) ->
- Name.equal na1 na2 && eq_notation_constr t1 t2 && eq_notation_constr u1 u2
+ Name.equal na1 na2 && (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) u1 u2
| NCases (_, o1, r1, p1), NCases (_, o2, r2, p2) -> (** FIXME? *)
let eqpat (p1, t1) (p2, t2) =
List.equal cases_pattern_eq p1 p2 &&
- eq_notation_constr t1 t2
+ (eq_notation_constr vars) t1 t2
in
let eqf (t1, (na1, o1)) (t2, (na2, o2)) =
let eq (i1, n1) (i2, n2) = eq_ind i1 i2 && List.equal Name.equal n1 n2 in
- eq_notation_constr t1 t2 && Name.equal na1 na2 && Option.equal eq o1 o2
+ (eq_notation_constr vars) t1 t2 && Name.equal na1 na2 && Option.equal eq o1 o2
in
- Option.equal eq_notation_constr o1 o2 &&
+ Option.equal (eq_notation_constr vars) o1 o2 &&
List.equal eqf r1 r2 &&
List.equal eqpat p1 p2
| NLetTuple (nas1, (na1, o1), t1, u1), NLetTuple (nas2, (na2, o2), t2, u2) ->
List.equal Name.equal nas1 nas2 &&
Name.equal na1 na2 &&
- Option.equal eq_notation_constr o1 o2 &&
- eq_notation_constr t1 t2 &&
- eq_notation_constr u1 u2
+ Option.equal (eq_notation_constr vars) o1 o2 &&
+ (eq_notation_constr vars) t1 t2 &&
+ (eq_notation_constr vars) u1 u2
| NIf (t1, (na1, o1), u1, r1), NIf (t2, (na2, o2), u2, r2) ->
- eq_notation_constr t1 t2 &&
+ (eq_notation_constr vars) t1 t2 &&
Name.equal na1 na2 &&
- Option.equal eq_notation_constr o1 o2 &&
- eq_notation_constr u1 u2 &&
- eq_notation_constr r1 r2
+ Option.equal (eq_notation_constr vars) o1 o2 &&
+ (eq_notation_constr vars) u1 u2 &&
+ (eq_notation_constr vars) r1 r2
| NRec (_, ids1, ts1, us1, rs1), NRec (_, ids2, ts2, us2, rs2) -> (** FIXME? *)
let eq (na1, o1, t1) (na2, o2, t2) =
Name.equal na1 na2 &&
- Option.equal eq_notation_constr o1 o2 &&
- eq_notation_constr t1 t2
+ Option.equal (eq_notation_constr vars) o1 o2 &&
+ (eq_notation_constr vars) t1 t2
in
Array.equal Id.equal ids1 ids2 &&
Array.equal (List.equal eq) ts1 ts2 &&
- Array.equal eq_notation_constr us1 us2 &&
- Array.equal eq_notation_constr rs1 rs2
+ Array.equal (eq_notation_constr vars) us1 us2 &&
+ Array.equal (eq_notation_constr vars) rs1 rs2
| NSort s1, NSort s2 ->
Miscops.glob_sort_eq s1 s2
| NCast (t1, c1), NCast (t2, c2) ->
- eq_notation_constr t1 t2 && cast_type_eq eq_notation_constr c1 c2
+ (eq_notation_constr vars) t1 t2 && cast_type_eq (eq_notation_constr vars) c1 c2
| (NRef _ | NVar _ | NApp _ | NHole _ | NList _ | NLambda _ | NProd _
| NBinderList _ | NLetIn _ | NCases _ | NLetTuple _ | NIf _
| NRec _ | NSort _ | NCast _), _ -> false
@@ -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,13 @@ 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'
+
+type recursive_pattern_kind =
+| RecursiveTerms of bool (* associativity *)
+| RecursiveBinders of glob_constr * glob_constr
+
+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
@@ -258,18 +273,16 @@ let compare_recursive_parts found f (iterator,subc) =
let x,y = if lassoc then y,x else x,y in
begin match !diff with
| None ->
- let () = diff := Some (x, y, Some lassoc) in
+ let () = diff := Some (x, y, RecursiveTerms lassoc) in
true
| Some _ -> false
end
| GLambda (_,Name x,_,t_x,c), GLambda (_,Name y,_,t_y,term)
| GProd (_,Name x,_,t_x,c), GProd (_,Name y,_,t_y,term) ->
(* We found a binding position where it differs *)
- check_is_hole x t_x;
- check_is_hole y t_y;
begin match !diff with
| None ->
- let () = diff := Some (x, y, None) in
+ let () = diff := Some (x, y, RecursiveBinders (t_x,t_y)) in
aux c term
| Some _ -> false
end
@@ -283,29 +296,42 @@ let compare_recursive_parts found f (iterator,subc) =
(* Here, we would need a loc made of several parts ... *)
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
+ | Some (x,y,RecursiveTerms lassoc) ->
+ 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) ->
+ | Some (x,y,RecursiveBinders (t_x,t_y)) ->
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;
+ check_is_hole x t_x;
+ check_is_hole y t_y;
NBinderList (x,y,iterator,f (Option.get !terminator))
else
raise Not_found
let notation_constr_and_vars_of_glob_constr a =
let found = ref ([],[],[]) in
+ let has_ltac = ref false in
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
@@ -347,7 +373,9 @@ let notation_constr_and_vars_of_glob_constr a =
NRec (fk,idl,dll,Array.map aux tl,Array.map aux bl)
| GCast (_,c,k) -> NCast (aux c,Miscops.map_cast_type aux k)
| GSort (_,s) -> NSort s
- | GHole (_,w,naming,arg) -> NHole (w, naming, arg)
+ | GHole (_,w,naming,arg) ->
+ if arg != None then has_ltac := true;
+ NHole (w, naming, arg)
| GRef (_,r,_) -> NRef r
| GEvar _ | GPatVar _ ->
error "Existential variables not allowed in notations."
@@ -355,11 +383,10 @@ let notation_constr_and_vars_of_glob_constr a =
in
let t = aux a in
(* Side effect *)
- t, !found
-
-let pair_equal eq1 eq2 (a,b) (a',b') = eq1 a a' && eq2 b b'
+ t, !found, !has_ltac
-let check_variables nenv (found,foundrec,foundrecbinding) =
+let check_variables_and_reversibility nenv (found,foundrec,foundrecbinding) =
+ let injective = ref true in
let recvars = nenv.ninterp_rec_vars in
let fold _ y accu = Id.Set.add y accu in
let useless_vars = Id.Map.fold fold recvars Id.Set.empty in
@@ -382,7 +409,7 @@ let check_variables nenv (found,foundrec,foundrecbinding) =
error
(Id.to_string x ^
" should not be bound in a recursive pattern of the right-hand side.")
- else nenv.ninterp_only_parse <- true
+ else injective := false
in
let check_pair s x y where =
if not (List.mem_f (pair_equal Id.equal Id.equal) (x,y) where) then
@@ -402,12 +429,13 @@ let check_variables nenv (found,foundrec,foundrecbinding) =
with Not_found -> check_bound x
end
| NtnInternTypeIdent -> check_bound x in
- Id.Map.iter check_type vars
+ Id.Map.iter check_type vars;
+ !injective
let notation_constr_of_glob_constr nenv a =
- let a, found = notation_constr_and_vars_of_glob_constr a in
- let () = check_variables nenv found in
- a
+ let a, found, has_ltac = notation_constr_and_vars_of_glob_constr a in
+ let injective = check_variables_and_reversibility nenv found in
+ a, not has_ltac && injective
(**********************************************************************)
(* Substitution of kernel names, avoiding a list of bound identifiers *)
@@ -417,7 +445,6 @@ let notation_constr_of_constr avoiding t =
let nenv = {
ninterp_var_type = Id.Map.empty;
ninterp_rec_vars = Id.Map.empty;
- ninterp_only_parse = false;
} in
notation_constr_of_glob_constr nenv t
@@ -435,7 +462,7 @@ let rec subst_notation_constr subst bound raw =
| NRef ref ->
let ref',t = subst_global subst ref in
if ref' == ref then raw else
- notation_constr_of_constr bound t
+ fst (notation_constr_of_constr bound t)
| NVar _ -> raw
@@ -585,6 +612,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 +623,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 +642,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 +675,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 +735,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 +861,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,47 +882,69 @@ 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 ((na,bk,None,t)::decls) b
+ 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 ((na,bk,None,t)::decls) b
+ match_iterated_binders islambda ((Inl na,bk,None,t)::decls) b
| GLetIn (loc,na,c,b) when glue_letin_with_decls ->
match_iterated_binders islambda
- ((na,Explicit (*?*), Some c,GHole(loc,Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None))::decls) b
+ ((Inl na,Explicit (*?*), Some c,GHole(loc,Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None))::decls) b
| b -> (decls,b)
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,33 +963,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],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)->
- let (decls,b) = match_iterated_binders true [(na1,bk,None,t1)] b1 in
+ | 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
- | GProd (_,na1,bk,t1,b1), NBinderList (x,_,NProd (Name id2,_,b2),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],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)
when na1 != Anonymous ->
- let (decls,b) = match_iterated_binders false [(na1,bk,None,t1)] b1 in
+ 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 [(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 [(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
@@ -863,7 +1101,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 [(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
@@ -891,6 +1129,10 @@ let term_of_binder = function
| Name id -> GVar (Loc.ghost,id)
| Anonymous -> GHole (Loc.ghost,Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None)
+type glob_decl2 =
+ (name, cases_pattern) Util.union * Decl_kinds.binding_kind *
+ glob_constr option * glob_constr
+
let match_notation_constr u c (metas,pat) =
let terms,binders,termlists,binderlists =
match_ false u ([],[]) metas ([],[],[],[]) c pat in
@@ -904,13 +1146,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 *)
@@ -927,7 +1171,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,[])
@@ -943,9 +1201,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 576c5b943a..c8fcbf7410 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -12,7 +12,7 @@ open Glob_term
(** {5 Utilities about [notation_constr]} *)
-val eq_notation_constr : notation_constr -> notation_constr -> bool
+val eq_notation_constr : Id.t list * Id.t list -> notation_constr -> notation_constr -> bool
(** Substitution of kernel names in interpretation data *)
@@ -23,13 +23,13 @@ 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 *)
val notation_constr_of_glob_constr : notation_interp_env ->
- glob_constr -> notation_constr
+ glob_constr -> notation_constr * reversibility_flag
(** Re-interpret a notation as a [glob_constr], taking care of binders *)
@@ -40,16 +40,19 @@ 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 *)
exception No_match
+type glob_decl2 =
+ (name, cases_pattern) Util.union * Decl_kinds.binding_kind *
+ glob_constr option * glob_constr
val match_notation_constr : bool -> glob_constr -> interpretation ->
(glob_constr * subscopes) list * (glob_constr list * subscopes) list *
- (glob_decl list * subscopes) list
+ (glob_decl2 list * subscopes) list
val match_notation_constr_cases_pattern :
cases_pattern -> interpretation ->
@@ -61,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 891b64fa11..2523063e64 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 ->
@@ -84,23 +84,21 @@ let declare_syntactic_definition local id onlyparse pat =
let pr_syndef kn = pr_qualid (shortest_qualid_of_syndef Id.Set.empty kn)
-let allow_compat_notations = ref true
-let verbose_compat_notations = ref false
+let pr_compat_warning (kn, def, v) =
+ let pp_def = match def with
+ | [], NRef r -> spc () ++ str "is" ++ spc () ++ pr_global_env Id.Set.empty r
+ | _ -> strbrk " is a compatibility notation"
+ in
+ let since = strbrk " since Coq > " ++ str (Flags.pr_version v) ++ str "." in
+ pr_syndef kn ++ pp_def ++ since
-let is_verbose_compat () =
- !verbose_compat_notations || not !allow_compat_notations
+let warn_compatibility_notation =
+ CWarnings.(create ~name:"compatibility-notation"
+ ~category:"deprecated" ~default:Disabled pr_compat_warning)
let verbose_compat kn def = function
- | Some v when is_verbose_compat () && Flags.version_strictly_greater v ->
- let act =
- if !verbose_compat_notations then Feedback.msg_warning else errorlabstrm ""
- in
- let pp_def = match def with
- | [], NRef r -> str " is " ++ pr_global_env Id.Set.empty r
- | _ -> str " is a compatibility notation"
- in
- let since = str " since Coq > " ++ str (Flags.pr_version v) ++ str "." in
- act (pr_syndef kn ++ pp_def ++ since)
+ | Some v when Flags.version_strictly_greater v ->
+ warn_compatibility_notation (kn, def, v)
| _ -> ()
let search_syntactic_definition kn =
@@ -110,21 +108,3 @@ let search_syntactic_definition kn =
def
open Goptions
-
-let set_verbose_compat_notations =
- declare_bool_option
- { optsync = true;
- optdepr = false;
- optname = "verbose compatibility notations";
- optkey = ["Verbose";"Compat";"Notations"];
- optread = (fun () -> !verbose_compat_notations);
- optwrite = ((:=) verbose_compat_notations) }
-
-let set_compat_notations =
- declare_bool_option
- { optsync = true;
- optdepr = false;
- optname = "accept compatibility notations";
- optkey = ["Compat"; "Notations"];
- optread = (fun () -> !allow_compat_notations);
- optwrite = ((:=) allow_compat_notations) }
diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli
index 7a1c9c5cb4..55e2848e69 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.mli
@@ -17,9 +17,3 @@ val declare_syntactic_definition : bool -> Id.t ->
Flags.compat_version option -> syndef_interpretation -> unit
val search_syntactic_definition : kernel_name -> syndef_interpretation
-
-(** Options concerning verbose display of compatibility notations
- or their deactivation *)
-
-val set_verbose_compat_notations : bool -> unit
-val set_compat_notations : bool -> unit
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 91099bbb19..79eeacf354 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
@@ -22,8 +22,7 @@ open Constrexpr_ops
let asymmetric_patterns = ref (false)
let _ = Goptions.declare_bool_option {
Goptions.optsync = true; Goptions.optdepr = false;
- Goptions.optname =
- "Constructors in patterns require all their arguments but no parameters instead of explicit parameters and arguments";
+ Goptions.optname = "no parameters in constructors";
Goptions.optkey = ["Asymmetric";"Patterns"];
Goptions.optread = (fun () -> !asymmetric_patterns);
Goptions.optwrite = (fun a -> asymmetric_patterns:=a);
@@ -59,6 +58,7 @@ let rec cases_pattern_fold_names f a = function
| CPatDelimiters (_,_,pat) -> cases_pattern_fold_names f a pat
| CPatAtom (_,Some (Ident (_,id))) when not (is_constructor id) -> f id a
| CPatPrim _ | CPatAtom _ -> a
+ | CPatCast _ -> assert false
let ids_of_pattern_list =
List.fold_left
@@ -92,6 +92,8 @@ let rec fold_local_binders g f n acc b = function
f n (fold_local_binders g f n' acc b l) t
| LocalRawDef ((_,na),t)::l ->
f n (fold_local_binders g f (name_fold g na n) acc b l) t
+ | LocalPattern _::l ->
+ assert false
| [] ->
f n acc b
@@ -170,6 +172,7 @@ let split_at_annot bl na =
(List.rev ans, LocalRawAssum (r, k, t) :: rest)
end
| LocalRawDef _ as x :: rest -> aux (x :: acc) rest
+ | LocalPattern _ :: rest -> assert false
| [] ->
user_err_loc(loc,"",
str "No parameter named " ++ Nameops.pr_id id ++ str".")
@@ -191,7 +194,9 @@ let map_local_binders f g e bl =
LocalRawAssum(nal,k,ty) ->
(map_binder g e nal, LocalRawAssum(nal,k,f e ty)::bl)
| LocalRawDef((loc,na),ty) ->
- (name_fold g na e, LocalRawDef((loc,na),f e ty)::bl) in
+ (name_fold g na e, LocalRawDef((loc,na),f e ty)::bl)
+ | LocalPattern _ ->
+ assert false in
let (e,rbl) = List.fold_left h (e,[]) bl in
(e, List.rev rbl)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 03:04:29 +0000