diff options
Diffstat (limited to 'interp')
-rw-r--r-- | interp/constrarg.ml | 74 | ||||
-rw-r--r-- | interp/constrarg.mli | 87 | ||||
-rw-r--r-- | interp/constrexpr_ops.ml | 130 | ||||
-rw-r--r-- | interp/constrexpr_ops.mli | 30 | ||||
-rw-r--r-- | interp/constrextern.ml | 71 | ||||
-rw-r--r-- | interp/constrextern.mli | 2 | ||||
-rw-r--r-- | interp/constrintern.ml | 296 | ||||
-rw-r--r-- | interp/constrintern.mli | 34 | ||||
-rw-r--r-- | interp/coqlib.ml | 2 | ||||
-rw-r--r-- | interp/coqlib.mli | 2 | ||||
-rw-r--r-- | interp/dumpglob.ml | 17 | ||||
-rw-r--r-- | interp/genintern.ml | 18 | ||||
-rw-r--r-- | interp/genintern.mli | 11 | ||||
-rw-r--r-- | interp/implicit_quantifiers.ml | 44 | ||||
-rw-r--r-- | interp/implicit_quantifiers.mli | 2 | ||||
-rw-r--r-- | interp/interp.mllib | 1 | ||||
-rw-r--r-- | interp/modintern.ml | 8 | ||||
-rw-r--r-- | interp/notation.ml | 53 | ||||
-rw-r--r-- | interp/notation_ops.ml | 126 | ||||
-rw-r--r-- | interp/notation_ops.mli | 5 | ||||
-rw-r--r-- | interp/ppextend.ml | 6 | ||||
-rw-r--r-- | interp/ppextend.mli | 3 | ||||
-rw-r--r-- | interp/reserve.ml | 10 | ||||
-rw-r--r-- | interp/smartlocate.ml | 12 | ||||
-rw-r--r-- | interp/stdarg.ml | 45 | ||||
-rw-r--r-- | interp/stdarg.mli | 61 | ||||
-rw-r--r-- | interp/syntax_def.ml | 2 | ||||
-rw-r--r-- | interp/topconstr.ml | 50 | ||||
-rw-r--r-- | interp/topconstr.mli | 4 |
29 files changed, 580 insertions, 626 deletions
diff --git a/interp/constrarg.ml b/interp/constrarg.ml deleted file mode 100644 index ca828102b..000000000 --- a/interp/constrarg.ml +++ /dev/null @@ -1,74 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Loc -open Tacexpr -open Misctypes -open Genarg -open Geninterp - -let make0 ?dyn name = - let wit = Genarg.make0 name in - let () = Geninterp.register_val0 wit dyn in - wit - -(** This is a hack for now, to break the dependency of Genarg on constr-related - types. We should use dedicated functions someday. *) - -let loc_of_or_by_notation f = function - | AN c -> f c - | ByNotation (loc,s,_) -> loc - -let wit_int_or_var = - make0 ~dyn:(val_tag (topwit Stdarg.wit_int)) "int_or_var" - -let wit_intro_pattern : (Constrexpr.constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type = - make0 "intropattern" - -let wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type = - make0 "tactic" - -let wit_ltac = make0 ~dyn:(val_tag (topwit Stdarg.wit_unit)) "ltac" - -let wit_ident = - make0 "ident" - -let wit_var = - make0 ~dyn:(val_tag (topwit wit_ident)) "var" - -let wit_ref = make0 "ref" - -let wit_quant_hyp = make0 "quant_hyp" - -let wit_constr = - make0 "constr" - -let wit_uconstr = make0 "uconstr" - -let wit_open_constr = make0 ~dyn:(val_tag (topwit wit_constr)) "open_constr" - -let wit_constr_with_bindings = make0 "constr_with_bindings" - -let wit_bindings = make0 "bindings" - -let wit_red_expr = make0 "redexpr" - -let wit_clause_dft_concl = - make0 "clause_dft_concl" - -let wit_destruction_arg = - make0 "destruction_arg" - -(** Aliases *) - -let wit_reference = wit_ref -let wit_global = wit_ref -let wit_clause = wit_clause_dft_concl -let wit_quantified_hypothesis = wit_quant_hyp -let wit_intropattern = wit_intro_pattern -let wit_redexpr = wit_red_expr diff --git a/interp/constrarg.mli b/interp/constrarg.mli deleted file mode 100644 index 6ccd944d4..000000000 --- a/interp/constrarg.mli +++ /dev/null @@ -1,87 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(** Generic arguments based on [constr]. We put them here to avoid a dependency - of Genarg in [constr]-related interfaces. *) - -open Loc -open Names -open Term -open Libnames -open Globnames -open Genredexpr -open Pattern -open Constrexpr -open Tacexpr -open Misctypes -open Genarg - -(** FIXME: nothing to do there. *) -val loc_of_or_by_notation : ('a -> Loc.t) -> 'a or_by_notation -> Loc.t - -(** {5 Additional generic arguments} *) - -val wit_int_or_var : (int or_var, int or_var, int) genarg_type - -val wit_intro_pattern : (constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type - -val wit_ident : Id.t uniform_genarg_type - -val wit_var : (Id.t located, Id.t located, Id.t) genarg_type - -val wit_ref : (reference, global_reference located or_var, global_reference) genarg_type - -val wit_quant_hyp : quantified_hypothesis uniform_genarg_type - -val wit_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type - -val wit_uconstr : (constr_expr , glob_constr_and_expr, Glob_term.closed_glob_constr) genarg_type - -val wit_open_constr : - (constr_expr, glob_constr_and_expr, constr) genarg_type - -val wit_constr_with_bindings : - (constr_expr with_bindings, - glob_constr_and_expr with_bindings, - constr with_bindings delayed_open) genarg_type - -val wit_bindings : - (constr_expr bindings, - glob_constr_and_expr bindings, - constr bindings delayed_open) genarg_type - -val wit_red_expr : - ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen, - (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen, - (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type - -val wit_tactic : (raw_tactic_expr, glob_tactic_expr, Geninterp.Val.t) genarg_type - -(** [wit_ltac] is subtly different from [wit_tactic]: they only change for their - toplevel interpretation. The one of [wit_ltac] forces the tactic and - discards the result. *) -val wit_ltac : (raw_tactic_expr, glob_tactic_expr, unit) genarg_type - -val wit_clause_dft_concl : (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) genarg_type - -val wit_destruction_arg : - (constr_expr with_bindings destruction_arg, - glob_constr_and_expr with_bindings destruction_arg, - delayed_open_constr_with_bindings destruction_arg) genarg_type - -(** Aliases for compatibility *) - -val wit_reference : (reference, global_reference located or_var, global_reference) genarg_type -val wit_global : (reference, global_reference located or_var, global_reference) genarg_type -val wit_clause : (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) genarg_type -val wit_quantified_hypothesis : quantified_hypothesis uniform_genarg_type -val wit_intropattern : (constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type -val wit_redexpr : - ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen, - (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen, - (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 04429851f..a592b4cff 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -37,10 +37,10 @@ let binder_kind_eq b1 b2 = match b1, b2 with let default_binder_kind = Default Explicit let names_of_local_assums bl = - List.flatten (List.map (function LocalRawAssum(l,_,_)->l|_->[]) bl) + List.flatten (List.map (function CLocalAssum(l,_,_)->l|_->[]) bl) let names_of_local_binders bl = - List.flatten (List.map (function LocalRawAssum(l,_,_)->l|LocalRawDef(l,_)->[l]|LocalPattern _ -> assert false) bl) + List.flatten (List.map (function CLocalAssum(l,_,_)->l|CLocalDef(l,_,_)->[l]|CLocalPattern _ -> assert false) bl) (**********************************************************************) (* Functions on constr_expr *) @@ -113,9 +113,10 @@ let rec constr_expr_eq e1 e2 = | CLambdaN(_,bl1,a1), CLambdaN(_,bl2,a2) -> List.equal binder_expr_eq bl1 bl2 && constr_expr_eq a1 a2 - | CLetIn(_,(_,na1),a1,b1), CLetIn(_,(_,na2),a2,b2) -> + | CLetIn(_,(_,na1),a1,t1,b1), CLetIn(_,(_,na2),a2,t2,b2) -> Name.equal na1 na2 && constr_expr_eq a1 a2 && + Option.equal constr_expr_eq t1 t2 && constr_expr_eq b1 b2 | CAppExpl(_,(proj1,r1,_),al1), CAppExpl(_,(proj2,r2,_),al2) -> Option.equal Int.equal proj1 proj2 && @@ -212,9 +213,9 @@ and recursion_order_expr_eq r1 r2 = match r1, r2 with | _ -> false and local_binder_eq l1 l2 = match l1, l2 with -| LocalRawDef (n1, e1), LocalRawDef (n2, e2) -> - eq_located Name.equal n1 n2 && constr_expr_eq e1 e2 -| LocalRawAssum (n1, _, e1), LocalRawAssum (n2, _, e2) -> +| CLocalDef (n1, e1, t1), CLocalDef (n2, e2, t2) -> + eq_located Name.equal n1 n2 && constr_expr_eq e1 e2 && Option.equal constr_expr_eq t1 t2 +| CLocalAssum (n1, _, e1), CLocalAssum (n2, _, e2) -> (** Don't care about the [binder_kind] *) List.equal (eq_located Name.equal) n1 n2 && constr_expr_eq e1 e2 | _ -> false @@ -234,7 +235,7 @@ let constr_loc = function | CCoFix (loc,_,_) -> loc | CProdN (loc,_,_) -> loc | CLambdaN (loc,_,_) -> loc - | CLetIn (loc,_,_,_) -> loc + | CLetIn (loc,_,_,_,_) -> loc | CAppExpl (loc,_,_) -> loc | CApp (loc,_,_) -> loc | CRecord (loc,_) -> loc @@ -269,10 +270,11 @@ let raw_cases_pattern_expr_loc = function | RCPatOr (loc,_) -> loc let local_binder_loc = function - | LocalRawAssum ((loc,_)::_,_,t) - | LocalRawDef ((loc,_),t) -> Loc.merge loc (constr_loc t) - | LocalRawAssum ([],_,_) -> assert false - | LocalPattern (loc,_,_) -> loc + | CLocalAssum ((loc,_)::_,_,t) + | CLocalDef ((loc,_),t,None) -> Loc.merge loc (constr_loc t) + | CLocalDef ((loc,_),b,Some t) -> Loc.merge loc (Loc.merge (constr_loc b) (constr_loc t)) + | CLocalAssum ([],_,_) -> assert false + | CLocalPattern (loc,_,_) -> loc let local_binders_loc bll = match bll with | [] -> Loc.ghost @@ -285,7 +287,7 @@ let mkIdentC id = CRef (Ident (Loc.ghost, id),None) let mkRefC r = CRef (r,None) let mkCastC (a,k) = CCast (Loc.ghost,a,k) let mkLambdaC (idl,bk,a,b) = CLambdaN (Loc.ghost,[idl,bk,a],b) -let mkLetInC (id,a,b) = CLetIn (Loc.ghost,id,a,b) +let mkLetInC (id,a,t,b) = CLetIn (Loc.ghost,id,a,t,b) let mkProdC (idl,bk,a,b) = CProdN (Loc.ghost,[idl,bk,a],b) let mkAppC (f,l) = @@ -301,99 +303,67 @@ let add_name_in_env env n = let (fresh_var, fresh_var_hook) = Hook.make ~default:(fun _ _ -> assert false) () -let expand_pattern_binders mkC bl c = - let rec loop bl c = +let expand_binders mkC loc bl c = + let rec loop loc bl c = match bl with - | [] -> ([], [], c) + | [] -> ([], c) | b :: bl -> - let (env, bl, c) = loop bl c in match b with - | LocalRawDef (n, _) -> + | CLocalDef ((loc1,_) as n, oty, b) -> + let env, c = loop (Loc.merge loc1 loc) bl c in let env = add_name_in_env env n in - (env, b :: bl, c) - | LocalRawAssum (nl, _, _) -> + (env, CLetIn (loc,n,oty,b,c)) + | CLocalAssum ((loc1,_)::_ as nl, bk, t) -> + let env, c = loop (Loc.merge loc1 loc) bl c in let env = List.fold_left add_name_in_env env nl in - (env, b :: bl, c) - | LocalPattern (loc, p, ty) -> + (env, mkC loc (nl,bk,t) c) + | CLocalAssum ([],_,_) -> loop loc bl c + | CLocalPattern (loc1, p, ty) -> + let env, c = loop (Loc.merge loc1 loc) bl c in let ni = Hook.get fresh_var env c in - let id = (loc, Name ni) in - let b = - LocalRawAssum - ([id], Default Explicit, - match ty with + let id = (loc1, Name ni) in + let ty = match ty with | Some ty -> ty - | None -> CHole (loc, None, IntroAnonymous, None)) + | None -> CHole (loc1, None, IntroAnonymous, None) in - let e = CRef (Libnames.Ident (loc, ni), None) in + let e = CRef (Libnames.Ident (loc1, ni), None) in let c = CCases (loc, LetPatternStyle, None, [(e,None,None)], - [(loc, [(loc,[p])], mkC loc bl c)]) + [(loc1, [(loc1,[p])], c)]) in - (ni :: env, [b], c) + (ni :: env, mkC loc ([id],Default Explicit,ty) c) in - let (_, bl, c) = loop bl c in - (bl, c) + let (_, c) = loop loc bl c in + 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 mk loc b c = CProdN (loc,[b],c) in + expand_binders mk 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 - | LocalRawDef (x,b)::bl -> mkLetInC(x,b,abstract_constr_expr c bl) - | 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 - | LocalRawDef (x,b)::bl -> mkLetInC(x,b,prod_constr_expr c bl) - | 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 mk loc b c = CLambdaN (loc,[b],c) in + expand_binders mk loc bll c + +(* Deprecated *) +let abstract_constr_expr c bl = mkCLambdaN (local_binders_loc bl) bl c +let prod_constr_expr c bl = mkCProdN (local_binders_loc bl) bl c let coerce_reference_to_id = function | Ident (_,id) -> id | Qualid (loc,_) -> - CErrors.user_err_loc (loc, "coerce_reference_to_id", - str "This expression should be a simple identifier.") + CErrors.user_err ~loc ~hdr:"coerce_reference_to_id" + (str "This expression should be a simple identifier.") let coerce_to_id = function | CRef (Ident (loc,id),_) -> (loc,id) - | a -> CErrors.user_err_loc - (constr_loc a,"coerce_to_id", - str "This expression should be a simple identifier.") + | a -> CErrors.user_err ~loc:(constr_loc a) + ~hdr:"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 -> CErrors.user_err_loc - (constr_loc a,"coerce_to_name", - str "This expression should be a name.") + | a -> CErrors.user_err + ~loc:(constr_loc a) ~hdr:"coerce_to_name" + (str "This expression should be a name.") diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index a92da035f..f6d97e107 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -23,8 +23,8 @@ val constr_expr_eq : constr_expr -> constr_expr -> bool (** Equality on [constr_expr]. This is a syntactical one, which is oblivious to some parsing details, including locations. *) -val local_binder_eq : local_binder -> local_binder -> bool -(** Equality on [local_binder]. Same properties as [constr_expr_eq]. *) +val local_binder_eq : local_binder_expr -> local_binder_expr -> bool +(** Equality on [local_binder_expr]. Same properties as [constr_expr_eq]. *) val binding_kind_eq : Decl_kinds.binding_kind -> Decl_kinds.binding_kind -> bool (** Equality on [binding_kind] *) @@ -37,7 +37,7 @@ val binder_kind_eq : binder_kind -> binder_kind -> bool val constr_loc : constr_expr -> Loc.t val cases_pattern_expr_loc : cases_pattern_expr -> Loc.t val raw_cases_pattern_expr_loc : raw_cases_pattern_expr -> Loc.t -val local_binders_loc : local_binder list -> Loc.t +val local_binders_loc : local_binder_expr list -> Loc.t (** {6 Constructors}*) @@ -46,22 +46,22 @@ val mkRefC : reference -> constr_expr val mkAppC : constr_expr * constr_expr list -> constr_expr val mkCastC : constr_expr * constr_expr cast_type -> constr_expr val mkLambdaC : Name.t located list * binder_kind * constr_expr * constr_expr -> constr_expr -val mkLetInC : Name.t located * constr_expr * constr_expr -> constr_expr +val mkLetInC : Name.t located * constr_expr * constr_expr option * constr_expr -> constr_expr val mkProdC : Name.t located list * binder_kind * constr_expr * constr_expr -> constr_expr -val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr -val prod_constr_expr : constr_expr -> local_binder list -> constr_expr - -val mkCLambdaN : Loc.t -> local_binder list -> constr_expr -> constr_expr +val mkCLambdaN : Loc.t -> local_binder_expr list -> constr_expr -> constr_expr (** Same as [abstract_constr_expr], with location *) -val mkCProdN : Loc.t -> local_binder list -> constr_expr -> constr_expr +val mkCProdN : Loc.t -> local_binder_expr list -> constr_expr -> constr_expr (** Same as [prod_constr_expr], with location *) +(** @deprecated variant of mkCLambdaN *) +val abstract_constr_expr : constr_expr -> local_binder_expr list -> constr_expr + +(** @deprecated variant of mkCProdN *) +val prod_constr_expr : constr_expr -> local_binder_expr list -> constr_expr + 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}*) @@ -78,9 +78,9 @@ val coerce_to_name : constr_expr -> Name.t located val default_binder_kind : binder_kind -val names_of_local_binders : local_binder list -> Name.t located list +val names_of_local_binders : local_binder_expr list -> Name.t located list (** Retrieve a list of binding names from a list of binders. *) -val names_of_local_assums : local_binder list -> Name.t located list -(** Same as [names_of_local_binders], but does not take the [let] bindings into +val names_of_local_assums : local_binder_expr list -> Name.t located list +(** Same as [names_of_local_binder_exprs], but does not take the [let] bindings into account. *) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index dd8a48b85..59b8b4e5b 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -85,6 +85,20 @@ let without_specific_symbols l f = (**********************************************************************) (* Control printing of records *) +(* Set Record Printing flag *) +let record_print = ref true + +let _ = + let open Goptions in + declare_bool_option + { optsync = true; + optdepr = false; + optname = "record printing"; + optkey = ["Printing";"Records"]; + optread = (fun () -> !record_print); + optwrite = (fun b -> record_print := b) } + + let is_record indsp = try let _ = Recordops.lookup_structure indsp in @@ -94,8 +108,8 @@ let is_record indsp = let encode_record r = let indsp = global_inductive r in if not (is_record indsp) then - user_err_loc (loc_of_reference r,"encode_record", - str "This type is not a structure type."); + user_err ~loc:(loc_of_reference r) ~hdr:"encode_record" + (str "This type is not a structure type."); indsp module PrintingRecordRecord = @@ -598,6 +612,14 @@ let extern_optimal_prim_token scopes r r' = | _ -> raise No_match (**********************************************************************) +(* mapping decl *) + +let extended_glob_local_binder_of_decl loc = function + | (p,bk,None,t) -> GLocalAssum (loc,p,bk,t) + | (p,bk,Some x,GHole (_, _, Misctypes.IntroAnonymous, None)) -> GLocalDef (loc,p,bk,x,None) + | (p,bk,Some x,t) -> GLocalDef (loc,p,bk,x,Some t) + +(**********************************************************************) (* mapping glob_constr to constr_expr *) let extern_glob_sort = function @@ -650,7 +672,7 @@ let rec extern inctx scopes vars r = () else if PrintingConstructor.active (fst cstrsp) then raise Exit - else if not !Flags.record_print then + else if not !record_print then raise Exit; let projs = struc.Recordops.s_PROJ in let locals = struc.Recordops.s_PROJKIND in @@ -692,8 +714,9 @@ let rec extern inctx scopes vars r = explicitize loc inctx [] (None,sub_extern false scopes vars f) (List.map (fun c -> lazy (sub_extern true scopes vars c)) args)) - | GLetIn (loc,na,t,c) -> - CLetIn (loc,(loc,na),sub_extern false scopes vars t, + | GLetIn (loc,na,b,t,c) -> + CLetIn (loc,(loc,na),sub_extern false scopes vars b, + Option.map (extern_typ scopes vars) t, extern inctx scopes (add_vname vars na) c) | GProd (loc,na,bk,t,c) -> @@ -756,7 +779,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 bl = List.map (extended_glob_local_binder_of_decl loc) 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 @@ -773,7 +796,7 @@ let rec extern inctx scopes vars r = | GCoFix n -> let listdecl = Array.mapi (fun i fi -> - let bl = List.map (fun (p,bk,x,t) -> (Inl p,bk,x,t)) blv.(i) in + let bl = List.map (extended_glob_local_binder_of_decl loc) 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 @@ -817,33 +840,32 @@ and factorize_lambda inctx scopes vars na bk aty c = and extern_local_binder scopes vars = function [] -> ([],[],[]) - | (Inl na,bk,Some bd,ty)::l -> + | GLocalDef (_,na,bk,bd,ty)::l -> let (assums,ids,l) = extern_local_binder scopes (name_fold Id.Set.add na vars) l in (assums,na::ids, - LocalRawDef((Loc.ghost,na), extern false scopes vars bd) :: l) + CLocalDef((Loc.ghost,na), extern false scopes vars bd, + Option.map (extern false scopes vars) ty) :: l) - | (Inl na,bk,None,ty)::l -> + | GLocalAssum (_,na,bk,ty)::l -> let ty = extern_typ scopes vars ty in (match extern_local_binder scopes (name_fold Id.Set.add na vars) l with - (assums,ids,LocalRawAssum(nal,k,ty')::l) + (assums,ids,CLocalAssum(nal,k,ty')::l) when constr_expr_eq ty ty' && match na with Name id -> not (occur_var_constr_expr id ty') | _ -> true -> (na::assums,na::ids, - LocalRawAssum((Loc.ghost,na)::nal,k,ty')::l) + CLocalAssum((Loc.ghost,na)::nal,k,ty')::l) | (assums,ids,l) -> (na::assums,na::ids, - LocalRawAssum([(Loc.ghost,na)],Default bk,ty) :: l)) - - | (Inr p,bk,Some bd,ty)::l -> assert false + CLocalAssum([(Loc.ghost,na)],Default bk,ty) :: l)) - | (Inr p,bk,None,ty)::l -> + | GLocalPattern (_,(p,_),_,bk,ty)::l -> let ty = if !Flags.raw_print then Some (extern_typ scopes vars ty) else None in let p = extern_cases_pattern vars p in let (assums,ids,l) = extern_local_binder scopes vars l in - (assums,ids, LocalPattern(Loc.ghost,p,ty) :: l) + (assums,ids, CLocalPattern(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], @@ -953,6 +975,7 @@ let extern_constr_gen lax goal_concl_style scopt env sigma t = (* Not "goal_concl_style" means do alpha-conversion avoiding only *) (* those goal/section/rel variables that occurs in the subterm under *) (* consideration; see namegen.ml for further details *) + let t = EConstr.of_constr t in let avoid = if goal_concl_style then ids_of_context env else [] in let r = Detyping.detype ~lax:lax goal_concl_style avoid env sigma t in let vars = vars_of_env env in @@ -965,6 +988,7 @@ let extern_constr ?(lax=false) goal_concl_style env sigma t = extern_constr_gen lax goal_concl_style None env sigma t let extern_type goal_concl_style env sigma t = + let t = EConstr.of_constr t in let avoid = if goal_concl_style then ids_of_context env else [] in let r = Detyping.detype goal_concl_style avoid env sigma t in extern_glob_type (vars_of_env env) r @@ -1015,8 +1039,9 @@ let rec glob_of_pat env sigma = function List.map (glob_of_pat env sigma) args) | PProd (na,t,c) -> GProd (loc,na,Explicit,glob_of_pat env sigma t,glob_of_pat (na::env) sigma c) - | PLetIn (na,t,c) -> - GLetIn (loc,na,glob_of_pat env sigma t, glob_of_pat (na::env) sigma c) + | PLetIn (na,b,t,c) -> + GLetIn (loc,na,glob_of_pat env sigma b, Option.map (glob_of_pat env sigma) t, + glob_of_pat (na::env) sigma c) | PLambda (na,t,c) -> GLambda (loc,na,Explicit,glob_of_pat env sigma t, glob_of_pat (na::env) sigma c) | PIf (c,b1,b2) -> @@ -1042,15 +1067,17 @@ let rec glob_of_pat env sigma = function | _ -> anomaly (Pp.str "PCase with non-trivial predicate but unknown inductive") in GCases (loc,RegularStyle,rtn,[glob_of_pat env sigma tm,indnames],mat) - | PFix f -> Detyping.detype_names false [] env (Global.env()) sigma (mkFix f) (** FIXME bad env *) - | PCoFix c -> Detyping.detype_names false [] env (Global.env()) sigma (mkCoFix c) + | PFix f -> Detyping.detype_names false [] env (Global.env()) sigma (EConstr.of_constr (mkFix f)) (** FIXME bad env *) + | PCoFix c -> Detyping.detype_names false [] env (Global.env()) sigma (EConstr.of_constr (mkCoFix c)) | PSort s -> GSort (loc,s) let extern_constr_pattern env sigma pat = extern true (None,[]) Id.Set.empty (glob_of_pat env sigma pat) let extern_rel_context where env sigma sign = + let sign = List.map (fun d -> Termops.map_rel_decl EConstr.of_constr d) sign in + let where = Option.map EConstr.of_constr where in 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 + let a = List.map (extended_glob_local_binder_of_decl Loc.ghost) a in pi3 (extern_local_binder (None,[]) vars a) diff --git a/interp/constrextern.mli b/interp/constrextern.mli index f617faa38..b39339450 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -41,7 +41,7 @@ val extern_reference : Loc.t -> Id.Set.t -> global_reference -> reference val extern_type : bool -> env -> Evd.evar_map -> types -> constr_expr val extern_sort : Evd.evar_map -> sorts -> glob_sort val extern_rel_context : constr option -> env -> Evd.evar_map -> - Context.Rel.t -> local_binder list + Context.Rel.t -> local_binder_expr list (** Printing options *) val print_implicits : bool ref diff --git a/interp/constrintern.ml b/interp/constrintern.ml index c916fcd88..d75487ecf 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -65,8 +65,6 @@ type var_internalization_data = type internalization_env = (var_internalization_data) Id.Map.t -type glob_binder = (Name.t * binding_kind * glob_constr option * glob_constr) - type ltac_sign = { ltac_vars : Id.Set.t; ltac_bound : Id.Set.t; @@ -154,17 +152,17 @@ let explain_internalization_error e = | BadPatternsNumber (n1,n2) -> explain_bad_patterns_number n1 n2 in pp ++ str "." -let error_bad_inductive_type loc = - user_err_loc (loc,"",str +let error_bad_inductive_type ?loc = + user_err ?loc (str "This should be an inductive type applied to patterns.") -let error_parameter_not_implicit loc = - user_err_loc (loc,"", str +let error_parameter_not_implicit ?loc = + user_err ?loc (str "The parameters do not bind in patterns;" ++ spc () ++ str "they must be replaced by '_'.") -let error_ldots_var loc = - user_err_loc (loc,"",str "Special token " ++ pr_id ldots_var ++ +let error_ldots_var ?loc = + user_err ?loc (str "Special token " ++ pr_id ldots_var ++ str " is for use in the Notation command.") (**********************************************************************) @@ -262,15 +260,15 @@ let pr_scope_stack = function | l -> str "scope stack " ++ str "[" ++ prlist_with_sep pr_comma str l ++ str "]" -let error_inconsistent_scope loc id scopes1 scopes2 = - user_err_loc (loc,"set_var_scope", - pr_id id ++ str " is here used in " ++ +let error_inconsistent_scope ?loc id scopes1 scopes2 = + user_err ?loc ~hdr:"set_var_scope" + (pr_id id ++ str " is here used in " ++ pr_scope_stack scopes2 ++ strbrk " while it was elsewhere used in " ++ pr_scope_stack scopes1) -let error_expect_binder_notation_type loc id = - user_err_loc (loc,"", - pr_id id ++ +let error_expect_binder_notation_type ?loc id = + user_err ?loc + (pr_id id ++ str " is expected to occur in binding position in the right-hand side.") let set_var_scope loc id istermvar env ntnvars = @@ -284,12 +282,12 @@ let set_var_scope loc id istermvar env ntnvars = | Some (tmp, scope) -> let s1 = make_current_scope tmp scope in let s2 = make_current_scope env.tmp_scope env.scopes in - if not (List.equal String.equal s1 s2) then error_inconsistent_scope loc id s1 s2 + if not (List.equal String.equal s1 s2) then error_inconsistent_scope ~loc id s1 s2 end in match typ with | NtnInternTypeBinder -> - if istermvar then error_expect_binder_notation_type loc id + if istermvar then error_expect_binder_notation_type ~loc id | NtnInternTypeConstr -> (* We need sometimes to parse idents at a constr level for factorization and we cannot enforce this constraint: @@ -306,12 +304,12 @@ let reset_tmp_scope env = {env with tmp_scope = None} let rec it_mkGProd loc2 env body = match env with - (loc1, (na, bk, _, t)) :: tl -> it_mkGProd loc2 tl (GProd (Loc.merge loc1 loc2, na, bk, t, body)) + (loc1, (na, bk, t)) :: tl -> it_mkGProd loc2 tl (GProd (Loc.merge loc1 loc2, na, bk, t, body)) | [] -> body let rec it_mkGLambda loc2 env body = match env with - (loc1, (na, bk, _, t)) :: tl -> it_mkGLambda loc2 tl (GLambda (Loc.merge loc1 loc2, na, bk, t, body)) + (loc1, (na, bk, t)) :: tl -> it_mkGLambda loc2 tl (GLambda (Loc.merge loc1 loc2, na, bk, t, body)) | [] -> body (**********************************************************************) @@ -366,19 +364,19 @@ let check_hidden_implicit_parameters id impls = | (Inductive indparams,_,_,_) -> Id.List.mem id indparams | _ -> false) impls then - errorlabstrm "" (strbrk "A parameter of an inductive type " ++ + user_err (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) ntnvars implargs env = function | loc,Anonymous -> if global_level then - user_err_loc (loc,"", str "Anonymous variables not allowed"); + user_err ~loc (str "Anonymous variables not allowed"); env | loc,Name id -> check_hidden_implicit_parameters id env.impls ; if Id.Map.is_empty ntnvars && Id.equal id ldots_var - then error_ldots_var loc; + then error_ldots_var ~loc; set_var_scope loc id false env ntnvars; if global_level then Dumpglob.dump_definition (loc,id) true "var" else Dumpglob.dump_binding loc id; @@ -399,7 +397,7 @@ let intern_generalized_binder ?(global_level=false) intern_type lvar env fvs in let bl = List.map (fun (id, loc) -> - (loc, (Name id, b, None, GHole (loc, Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None)))) + (loc, (Name id, b, GHole (loc, Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None)))) fvs in let na = match na with @@ -414,7 +412,7 @@ let intern_generalized_binder ?(global_level=false) intern_type lvar in Implicit_quantifiers.make_fresh ids' (Global.env ()) id in Name name | _ -> na - in (push_name_env ~global_level lvar (impls_type_list ty')(*?*) env' (loc,na)), (loc,(na,b',None,ty')) :: List.rev bl + in (push_name_env ~global_level lvar (impls_type_list ty')(*?*) env' (loc,na)), (loc,(na,b',ty')) :: List.rev bl let intern_assumption intern lvar env nal bk ty = let intern_type env = intern (set_type_scope env) in @@ -426,7 +424,7 @@ let intern_assumption intern lvar env nal bk ty = List.fold_left (fun (env, bl) (loc, na as locna) -> (push_name_env lvar impls env locna, - (loc,(na,k,None,locate_if_hole loc na ty))::bl)) + (loc,(na,k,locate_if_hole loc na ty))::bl)) (env, []) nal | Generalized (b,b',t) -> let env, b = intern_generalized_binder intern_type lvar env (List.hd nal) b b' t ty in @@ -457,47 +455,47 @@ let intern_local_pattern intern lvar env p = 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 glob_local_binder_of_extended = function + | GLocalAssum (loc,na,bk,t) -> (na,bk,None,t) + | GLocalDef (loc,na,bk,c,Some t) -> (na,bk,Some c,t) + | GLocalDef (loc,na,bk,c,None) -> + let t = GHole(loc,Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None) in + (na,bk,Some c,t) + | GLocalPattern (loc,_,_,_,_) -> + Loc.raise ~loc (Stream.Error "pattern with quote not allowed here.") 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) -> + | CLocalAssum(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 + let bl' = List.map (fun (loc,(na,c,t)) -> GLocalAssum (loc,na,c,t)) bl' in env, bl' @ bl - | LocalRawDef((loc,na as locna),def) -> - let indef = intern env def in - let term, ty = - match indef with - | GCast (loc, b, Misctypes.CastConv t) -> b, t - | _ -> indef, GHole(loc,Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None) - in - (push_name_env lvar (impls_term_list indef) env locna, - (BDRawDef ((loc,(na,Explicit,Some(term),ty))))::bl) - | LocalPattern (loc,p,ty) -> + | CLocalDef((loc,na as locna),def,ty) -> + let term = intern env def in + let ty = Option.map (intern env) ty in + (push_name_env lvar (impls_term_list term) env locna, + GLocalDef (loc,na,Explicit,term,ty) :: bl) + | CLocalPattern (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 il = List.map snd (free_vars_of_pat [] 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 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 _,(_,bk,t) = List.hd bl' in + (env, GLocalPattern(loc,(cp,il),id,bk,t) :: bl) let intern_generalization intern env lvar loc bk ak c = let c = intern {env with unb = true} c in @@ -567,35 +565,29 @@ let traverse_binder (terms,_,_ as subst) avoid (renaming,env) = function (renaming',env), Name id' type letin_param = - | LPLetIn of Loc.t * (Name.t * glob_constr) + | LPLetIn of Loc.t * (Name.t * glob_constr * glob_constr option) | 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) + | LPLetIn (loc,(na,b,t)) -> + GLetIn(loc,na,b,t,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 +let rec subordinate_letins letins = function (* binders come in reverse order; the non-let are returned in reverse order together *) (* with the subordinated let-in in writing order *) - | 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 + | GLocalDef (loc,na,_,b,t)::l -> + subordinate_letins (LPLetIn (loc,(na,b,t))::letins) l + | GLocalAssum (loc,na,bk,t)::l -> + let letins',rest = subordinate_letins [] 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) + | GLocalPattern (loc,u,id,bk,t) :: l -> + subordinate_letins (LPCases (loc,u,id)::letins) ([GLocalAssum (loc,Name id,bk,t)] @ l) | [] -> letins,[] @@ -609,10 +601,11 @@ let terms_of_binders bl = 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 + | GLocalAssum (loc,Name id,_,_)::l -> CRef (Ident (loc,id), None) :: extract_variables l + | GLocalDef (loc,Name id,_,_,_)::l -> extract_variables l + | GLocalDef (loc,Anonymous,_,_,_)::l + | GLocalAssum (loc,Anonymous,_,_)::l -> error "Cannot turn \"_\" into a term." + | GLocalPattern (loc,(u,_),_,_,_) :: l -> term_of_pat u :: extract_variables l | [] -> [] in extract_variables bl @@ -660,23 +653,13 @@ let instantiate_notation_constr loc intern ntnvars subst infos c = let arg = match arg with | None -> None | Some arg -> - let open Tacexpr in - let open Genarg in - let wit = glbwit Constrarg.wit_tactic in - let body = - if has_type arg wit then out_gen wit arg - else assert false (** FIXME *) - in - let mk_env id (c, (tmp_scope, subscopes)) accu = + let mk_env (c, (tmp_scope, subscopes)) = let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in let gc = intern nenv c in - let c = ConstrMayEval (Genredexpr.ConstrTerm (gc, Some c)) in - ((loc, id), c) :: accu + (gc, Some c) in - let bindings = Id.Map.fold mk_env terms [] in - let tac = TacLetIn (false, bindings, body) in - let arg = in_gen wit tac in - Some arg + let bindings = Id.Map.map mk_env terms in + Some (Genintern.generic_substitute_notation bindings arg) in GHole (loc, knd, naming, arg) | NBinderList (x,y,iter,terminator) -> @@ -684,7 +667,7 @@ let instantiate_notation_constr loc intern ntnvars subst infos c = (* All elements of the list are in scopes (scopt,subscopes) *) let (bl,(scopt,subscopes)) = Id.Map.find x binders in let env,bl = List.fold_left (intern_local_binder_aux intern ntnvars) (env,[]) bl in - let letins,bl = subordinate_letins intern [] bl in + let letins,bl = subordinate_letins [] bl in let termin = aux (terms,None,None) (renaming,env) terminator in let res = List.fold_left (fun t binder -> aux (terms,Some(y,binder),Some t) subinfos iter) @@ -764,7 +747,7 @@ let string_of_ty = function let gvar (loc, id) us = match us with | None -> GVar (loc, id) | Some _ -> - user_err_loc (loc, "", str "Variable " ++ pr_id id ++ + user_err ~loc (str "Variable " ++ pr_id id ++ str " cannot have a universe instance") let intern_var genv (ltacvars,ntnvars) namedctx loc id us = @@ -788,12 +771,12 @@ let intern_var genv (ltacvars,ntnvars) namedctx 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 + then error_ldots_var ~loc 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", - str "variable " ++ pr_id id ++ str " should be bound to a term.") + user_err ~loc ~hdr:"intern_var" + (str "variable " ++ pr_id id ++ str " should be bound to a term.") else (* Is [id] a goal or section variable *) let _ = Context.Named.lookup id namedctx in @@ -825,7 +808,7 @@ let find_appl_head_data c = | x -> x,[],[],[] let error_not_enough_arguments loc = - user_err_loc (loc,"",str "Abbreviation is not applied enough.") + user_err ~loc (str "Abbreviation is not applied enough.") let check_no_explicitation l = let is_unset (a, b) = match b with None -> false | Some _ -> true in @@ -834,7 +817,7 @@ let check_no_explicitation l = | [] -> () | (_, None) :: _ -> assert false | (_, Some (loc, _)) :: _ -> - user_err_loc (loc,"",str"Unexpected explicitation of the argument of an abbreviation.") + user_err ~loc (str"Unexpected explicitation of the argument of an abbreviation.") let dump_extended_global loc = function | TrueGlobal ref -> (*feedback_global loc ref;*) Dumpglob.add_glob loc ref @@ -847,7 +830,7 @@ let intern_reference ref = let qid = qualid_of_reference ref in let r = try intern_extended_global_of_qualid qid - with Not_found -> error_global_not_found_loc (fst qid) (snd qid) + with Not_found -> error_global_not_found ~loc:(fst qid) (snd qid) in Smartlocate.global_of_extended_global r @@ -872,7 +855,7 @@ let intern_qualid loc qid intern env lvar us args = | 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 ++ + user_err ~loc (str "Notation " ++ pr_qualid qid ++ str " cannot have a universe instance, its expanded head does not start with a reference") in @@ -888,7 +871,7 @@ let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args = | Qualid (loc, qid) -> let r,projapp,args2 = try intern_qualid loc qid intern env ntnvars us args - with Not_found -> error_global_not_found_loc loc qid + with Not_found -> error_global_not_found ~loc qid in let x, imp, scopes, l = find_appl_head_data r in (x,imp,scopes,l), args2 @@ -904,7 +887,7 @@ let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args = (* Extra allowance for non globalizing functions *) if !interning_grammar || env.unb then (gvar (loc,id) us, [], [], []), args - else error_global_not_found_loc loc qid + else error_global_not_found ~loc qid let interp_reference vars r = let (r,_,_,_),_ = @@ -982,7 +965,7 @@ let check_number_of_pattern loc n l = let check_or_pat_variables loc ids idsl = if List.exists (fun ids' -> not (List.eq_set Id.equal ids ids')) idsl then - user_err_loc (loc, "", str + user_err ~loc (str "The components of this disjunctive pattern must bind the same variables.") (** Use only when params were NOT asked to the user. @@ -991,7 +974,7 @@ let check_constructor_length env loc cstr len_pl pl0 = let n = len_pl + List.length pl0 in if Int.equal n (Inductiveops.constructor_nallargs cstr) then false else (Int.equal n (Inductiveops.constructor_nalldecls cstr) || - (error_wrong_numarg_constructor_loc loc env cstr + (error_wrong_numarg_constructor ~loc env cstr (Inductiveops.constructor_nrealargs cstr))) let add_implicits_check_length fail nargs nargs_with_letin impls_st len_pl1 pl2 = @@ -1016,14 +999,14 @@ let add_implicits_check_constructor_length env loc c len_pl1 pl2 = let nargs = Inductiveops.constructor_nallargs c in let nargs' = Inductiveops.constructor_nalldecls c in let impls_st = implicits_of_global (ConstructRef c) in - add_implicits_check_length (error_wrong_numarg_constructor_loc loc env c) + add_implicits_check_length (error_wrong_numarg_constructor ~loc env c) nargs nargs' impls_st len_pl1 pl2 let add_implicits_check_ind_length env loc c len_pl1 pl2 = let nallargs = inductive_nallargs_env env c in let nalldecls = inductive_nalldecls_env env c in let impls_st = implicits_of_global (IndRef c) in - add_implicits_check_length (error_wrong_numarg_inductive_loc loc env c) + add_implicits_check_length (error_wrong_numarg_inductive ~loc env c) nallargs nalldecls impls_st len_pl1 pl2 (** Do not raise NotEnoughArguments thanks to preconditions*) @@ -1034,7 +1017,7 @@ let chop_params_pattern loc ind args with_letin = assert (nparams <= List.length args); let params,args = List.chop nparams args in List.iter (function PatVar(_,Anonymous) -> () - | PatVar (loc',_) | PatCstr(loc',_,_,_) -> error_parameter_not_implicit loc') params; + | PatVar (loc',_) | PatCstr(loc',_,_,_) -> error_parameter_not_implicit ~loc:loc') params; args let find_constructor loc add_params ref = @@ -1042,10 +1025,10 @@ let find_constructor loc add_params ref = | ConstructRef cstr -> cstr | IndRef _ -> let error = str "There is an inductive name deep in a \"in\" clause." in - user_err_loc (loc, "find_constructor", error) + user_err ~loc ~hdr:"find_constructor" error | ConstRef _ | VarRef _ -> let error = str "This reference is not a constructor." in - user_err_loc (loc, "find_constructor", error) + user_err ~loc ~hdr:"find_constructor" error in cstr, match add_params with | Some nb_args -> @@ -1067,7 +1050,7 @@ let check_duplicate loc fields = match dups with | [] -> () | (r, _) :: _ -> - user_err_loc (loc, "", str "This record defines several times the field " ++ + user_err ~loc (str "This record defines several times the field " ++ pr_reference r ++ str ".") (** [sort_fields ~complete loc fields completer] expects a list @@ -1092,8 +1075,8 @@ let sort_fields ~complete loc fields completer = 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") + user_err ~loc:(loc_of_reference first_field_ref) ~hdr:"intern" + (pr_reference first_field_ref ++ str": Not a projection") in (* the number of parameters *) let nparams = record.Recordops.s_EXPECTEDPARAM in @@ -1123,7 +1106,7 @@ let sort_fields ~complete loc fields completer = 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.") + user_err ~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 @@ -1136,7 +1119,7 @@ let sort_fields ~complete loc fields completer = | None :: projs -> if complete then (* we don't want anonymous fields *) - user_err_loc (loc, "", str "This record contains anonymous fields.") + user_err ~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 @@ -1150,15 +1133,14 @@ let sort_fields ~complete loc fields completer = | (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 + user_err ~loc:(loc_of_reference field_ref) ~hdr:"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.") + user_err ~loc + (str "This record contains fields of different records.") in index_fields fields remaining_projs ((field_index, field_value) :: acc) | [] -> @@ -1229,7 +1211,7 @@ let drop_notations_pattern looked_for = if top then looked_for g else match g with ConstructRef _ -> () | _ -> raise Not_found with Not_found -> - error_invalid_pattern_notation loc + error_invalid_pattern_notation ~loc () in let test_kind top = if top then looked_for else function ConstructRef _ -> () | _ -> raise Not_found @@ -1354,8 +1336,8 @@ let drop_notations_pattern looked_for = List.map2 (fun x -> in_not false loc (x,snd scopes) fullsubst []) argscs1 pl @ List.map (in_pat false scopes) args, []) | 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."); + if not (List.is_empty args) then user_err ~loc + (strbrk "Application of arguments to a recursive notation not supported in patterns."); (try (* All elements of the list are in scopes (scopt,subscopes) *) let (l,(scopt,subscopes)) = Id.Map.find x substlist in @@ -1370,7 +1352,7 @@ let drop_notations_pattern looked_for = | NHole _ -> let () = assert (List.is_empty args) in RCPatAtom (loc, None) - | t -> error_invalid_pattern_notation loc + | t -> error_invalid_pattern_notation ~loc () in in_pat true let rec intern_pat genv aliases pat = @@ -1422,8 +1404,8 @@ let rec intern_pat genv aliases pat = [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.") + CErrors.user_err ~loc ~hdr:"check_no_patcast" + (Pp.strbrk "Casts are not supported here.") | CPatDelimiters(_,_,p) | CPatAlias(_,p,_) -> check_no_patcast p | CPatCstr(_,_,opl,pl) -> @@ -1456,11 +1438,11 @@ let intern_ind_pattern genv scopes pat = let no_not = try drop_notations_pattern (function (IndRef _ | ConstructRef _) -> () | _ -> raise Not_found) scopes pat - with InternalizationError(loc,NotAConstructor _) -> error_bad_inductive_type loc + with InternalizationError(loc,NotAConstructor _) -> error_bad_inductive_type ~loc in match no_not with | RCPatCstr (loc, head, expl_pl, pl) -> - let c = (function IndRef ind -> ind | _ -> error_bad_inductive_type loc) head in + let c = (function IndRef ind -> ind | _ -> error_bad_inductive_type ~loc) head in let with_letin, pl2 = add_implicits_check_ind_length genv loc c (List.length expl_pl) pl in let idslpl1 = List.rev_map (intern_pat genv empty_alias) expl_pl in @@ -1468,8 +1450,8 @@ let intern_ind_pattern genv scopes pat = (with_letin, match product_of_cases_patterns [] (List.rev_append idslpl1 idslpl2) with | _,[_,pl] -> (c,chop_params_pattern loc c pl with_letin) - | _ -> error_bad_inductive_type loc) - | x -> error_bad_inductive_type (raw_cases_pattern_expr_loc x) + | _ -> error_bad_inductive_type ~loc) + | x -> error_bad_inductive_type ~loc:(raw_cases_pattern_expr_loc x) (**********************************************************************) (* Utilities for application *) @@ -1508,10 +1490,10 @@ let extract_explicit_arg imps args = let id = match pos with | ExplByName id -> if not (exists_implicit_name id imps) then - user_err_loc - (loc,"",str "Wrong argument name: " ++ pr_id id ++ str "."); + user_err ~loc + (str "Wrong argument name: " ++ pr_id id ++ str "."); if Id.Map.mem id eargs then - user_err_loc (loc,"",str "Argument name " ++ pr_id id + user_err ~loc (str "Argument name " ++ pr_id id ++ str " occurs more than once."); id | ExplByPos (p,_id) -> @@ -1521,11 +1503,11 @@ let extract_explicit_arg imps args = if not (is_status_implicit imp) then failwith "imp"; name_of_implicit imp with Failure _ (* "nth" | "imp" *) -> - user_err_loc - (loc,"",str"Wrong argument position: " ++ int p ++ str ".") + user_err ~loc + (str"Wrong argument position: " ++ int p ++ str ".") in if Id.Map.mem id eargs then - user_err_loc (loc,"",str"Argument at position " ++ int p ++ + user_err ~loc (str"Argument at position " ++ int p ++ str " is mentioned more than once."); id in (Id.Map.add id (loc, a) eargs, rargs) @@ -1556,10 +1538,8 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = 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 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 + let n' = Option.map (fun _ -> List.count (function GLocalAssum _ -> true | _ -> false (* remove let-ins *)) rbefore) n in n', ro, List.fold_left intern_local_binder (env',rbefore) after in let n, ro, (env',rbl) = @@ -1571,24 +1551,19 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = | CMeasureRec (m,r) -> intern_ro_arg (fun f -> GMeasureRec (f m, Option.map f r)) 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 bl = List.rev (List.map glob_local_binder_of_extended 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 + let fix_args = (List.map (fun (na, bk, _, _) -> (build_impls bk na)) bli) in 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 (Array.map (fun (ro,_,_,_) -> ro) idl,n), Array.of_list lf, - Array.map (fun (_,bl,_,_) -> List.map snd bl) idl, + Array.map (fun (_,bl,_,_) -> bl) idl, Array.map (fun (_,_,ty,_) -> ty) idl, Array.map (fun (_,_,_,bd) -> bd) idl) | CCoFix (loc, (locid,iddef), dl) -> @@ -1602,20 +1577,18 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = let idl_tmp = Array.map (fun ((loc,id),bl,ty,_) -> let (env',rbl) = List.fold_left intern_local_binder (env,[]) bl in - let rbl = List.map (function BDRawDef a -> a | BDPattern _ -> - Loc.raise loc (Stream.Error "pattern with quote not allowed after cofix")) rbl in - (List.rev rbl, + (List.rev (List.map glob_local_binder_of_extended 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 + let cofix_args = List.map (fun (na, bk, _, _) -> (build_impls bk na)) bli in 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, Array.of_list lf, - Array.map (fun (bl,_,_) -> List.map snd bl) idl, + Array.map (fun (bl,_,_) -> bl) idl, Array.map (fun (_,ty,_) -> ty) idl, Array.map (fun (_,_,bd) -> bd) idl) | CProdN (loc,[],c2) -> @@ -1626,9 +1599,10 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = intern env c2 | CLambdaN (loc,(nal,bk,ty)::bll,c2) -> iterate_lam loc (reset_tmp_scope env) bk ty (CLambdaN (loc, bll, c2)) nal - | CLetIn (loc,na,c1,c2) -> + | CLetIn (loc,na,c1,t,c2) -> let inc1 = intern (reset_tmp_scope env) c1 in - GLetIn (loc, snd na, inc1, + let int = Option.map (intern_type env) t in + GLetIn (loc, snd na, inc1, int, intern (push_name_env ntnvars (impls_term_list inc1) env na) c2) | CNotation (loc,"- _",([CPrim (_,Numeral p)],[],[])) when Bigint.is_strictly_pos p -> @@ -1681,7 +1655,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = in begin match fields with - | None -> user_err_loc (loc, "intern", str"No constructor inference.") + | None -> user_err ~loc ~hdr:"intern" (str"No constructor inference.") | Some (n, constrname, args) -> let pars = List.make n (CHole (loc, None, Misctypes.IntroAnonymous, None)) in let app = CAppExpl (loc, (None, constrname,None), List.rev_append pars args) in @@ -1751,7 +1725,9 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = let k = match k with | None -> let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in - Evar_kinds.QuestionMark st + (match naming with + | Misctypes.IntroIdentifier id -> Evar_kinds.NamedHole id + | _ -> Evar_kinds.QuestionMark st) | Some k -> k in let solve = match solve with @@ -1855,7 +1831,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = (add_name match_acc (loc,x)) ((loc,x)::var_acc) | (LocalAssum (cano_name,ty) | LocalDef (cano_name,_,ty)) :: t, c::tt -> let fresh = - Namegen.next_name_away_with_default_using_types "iV" cano_name forbidden_names ty in + Namegen.next_name_away_with_default_using_types "iV" cano_name forbidden_names (EConstr.of_constr ty) in canonize_args t tt (fresh::forbidden_names) ((fresh,c)::match_acc) ((cases_pattern_loc c,Name fresh)::var_acc) | _ -> assert false in @@ -1904,7 +1880,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = | (imp::impl', []) -> if not (Id.Map.is_empty eargs) then (let (id,(loc,_)) = Id.Map.choose eargs in - user_err_loc (loc,"",str "Not enough non implicit \ + user_err ~loc (str "Not enough non implicit \ arguments to accept the argument bound to " ++ pr_id id ++ str".")); [] @@ -1935,8 +1911,8 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = intern env c with InternalizationError (loc,e) -> - user_err_loc (loc,"internalize", - explain_internalization_error e) + user_err ~loc ~hdr:"internalize" + (explain_internalization_error e) (**************************************************************************) (* Functions to translate constr_expr into glob_constr *) @@ -1949,7 +1925,7 @@ let extract_ids env = let scope_of_type_kind = function | IsType -> Notation.current_type_scope_name () - | OfType typ -> compute_type_scope typ + | OfType typ -> compute_type_scope (EConstr.Unsafe.to_constr typ) | WithoutTypeConstraint -> None let empty_ltac_sign = { @@ -1975,7 +1951,7 @@ let intern_pattern globalenv patt = intern_cases_pattern globalenv (None,[]) empty_alias patt with InternalizationError (loc,e) -> - user_err_loc (loc,"internalize",explain_internalization_error e) + user_err ~loc ~hdr:"internalize" (explain_internalization_error e) (*********************************************************************) @@ -2028,7 +2004,7 @@ let interp_constr_evars env evdref ?(impls=empty_internalization_env) c = interp_constr_evars_gen env evdref WithoutTypeConstraint ~impls c let interp_casted_constr_evars env evdref ?(impls=empty_internalization_env) c typ = - interp_constr_evars_gen env evdref ~impls (OfType typ) c + interp_constr_evars_gen env evdref ~impls (OfType (EConstr.of_constr typ)) c let interp_type_evars env evdref ?(impls=empty_internalization_env) c = interp_constr_evars_gen env evdref IsType ~impls c @@ -2079,22 +2055,16 @@ let intern_context global_level env impl_env binders = let lvar = (empty_ltac_sign, Id.Map.empty) in let lenv, bl = List.fold_left (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) + (lenv.impls, List.map glob_local_binder_of_extended bl) with InternalizationError (loc,e) -> - user_err_loc (loc,"internalize", explain_internalization_error e) + user_err ~loc ~hdr:"internalize" (explain_internalization_error e) let interp_rawcontext_evars env evdref k bl = + let open EConstr in let (env, par, _, impls) = List.fold_left (fun (env,params,n,impls) (na, k, b, t) -> diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 61e7c6f5c..758d4e650 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -75,8 +75,6 @@ type ltac_sign = { val empty_ltac_sign : ltac_sign -type glob_binder = (Name.t * binding_kind * glob_constr option * glob_constr) - (** {6 Internalization performs interpretation of global names and notations } *) val intern_constr : env -> constr_expr -> glob_constr @@ -90,7 +88,7 @@ val intern_gen : typing_constraint -> env -> val intern_pattern : env -> cases_pattern_expr -> Id.t list * (Id.t Id.Map.t * cases_pattern) list -val intern_context : bool -> env -> internalization_env -> local_binder list -> internalization_env * glob_binder list +val intern_context : bool -> env -> internalization_env -> local_binder_expr list -> internalization_env * glob_decl list (** {6 Composing internalization with type inference (pretyping) } *) @@ -101,7 +99,7 @@ val interp_constr : env -> evar_map -> ?impls:internalization_env -> constr_expr -> constr Evd.in_evar_universe_context val interp_casted_constr : env -> evar_map -> ?impls:internalization_env -> - constr_expr -> types -> constr Evd.in_evar_universe_context + constr_expr -> EConstr.types -> constr Evd.in_evar_universe_context val interp_type : env -> evar_map -> ?impls:internalization_env -> constr_expr -> types Evd.in_evar_universe_context @@ -109,32 +107,32 @@ val interp_type : env -> evar_map -> ?impls:internalization_env -> (** Main interpretation function expecting all postponed problems to be resolved, but possibly leaving evars. *) -val interp_open_constr : env -> evar_map -> constr_expr -> evar_map * constr +val interp_open_constr : env -> evar_map -> constr_expr -> evar_map * EConstr.constr (** Accepting unresolved evars *) val interp_constr_evars : env -> evar_map ref -> - ?impls:internalization_env -> constr_expr -> constr + ?impls:internalization_env -> constr_expr -> EConstr.constr val interp_casted_constr_evars : env -> evar_map ref -> - ?impls:internalization_env -> constr_expr -> types -> constr + ?impls:internalization_env -> constr_expr -> types -> EConstr.constr val interp_type_evars : env -> evar_map ref -> - ?impls:internalization_env -> constr_expr -> types + ?impls:internalization_env -> constr_expr -> EConstr.types (** Accepting unresolved evars and giving back the manual implicit arguments *) val interp_constr_evars_impls : env -> evar_map ref -> ?impls:internalization_env -> constr_expr -> - constr * Impargs.manual_implicits + EConstr.constr * Impargs.manual_implicits val interp_casted_constr_evars_impls : env -> evar_map ref -> - ?impls:internalization_env -> constr_expr -> types -> - constr * Impargs.manual_implicits + ?impls:internalization_env -> constr_expr -> EConstr.types -> + EConstr.constr * Impargs.manual_implicits val interp_type_evars_impls : env -> evar_map ref -> ?impls:internalization_env -> constr_expr -> - types * Impargs.manual_implicits + EConstr.types * Impargs.manual_implicits (** Interprets constr patterns *) @@ -153,22 +151,22 @@ val interp_reference : ltac_sign -> reference -> glob_constr val interp_binder : env -> evar_map -> Name.t -> constr_expr -> types Evd.in_evar_universe_context -val interp_binder_evars : env -> evar_map ref -> Name.t -> constr_expr -> types +val interp_binder_evars : env -> evar_map ref -> Name.t -> constr_expr -> EConstr.types (** Interpret contexts: returns extended env and context *) val interp_context_evars : ?global_level:bool -> ?impl_env:internalization_env -> ?shift:int -> - env -> evar_map ref -> local_binder list -> - internalization_env * ((env * Context.Rel.t) * Impargs.manual_implicits) + env -> evar_map ref -> local_binder_expr list -> + internalization_env * ((env * EConstr.rel_context) * Impargs.manual_implicits) (* val interp_context_gen : (env -> glob_constr -> unsafe_type_judgment Evd.in_evar_universe_context) -> *) (* (env -> Evarutil.type_constraint -> glob_constr -> unsafe_judgment Evd.in_evar_universe_context) -> *) (* ?global_level:bool -> ?impl_env:internalization_env -> *) -(* env -> evar_map -> local_binder list -> internalization_env * ((env * Evd.evar_universe_context * rel_context * sorts list) * Impargs.manual_implicits) *) +(* env -> evar_map -> local_binder_expr list -> internalization_env * ((env * Evd.evar_universe_context * rel_context * sorts list) * Impargs.manual_implicits) *) (* val interp_context : ?global_level:bool -> ?impl_env:internalization_env -> *) -(* env -> evar_map -> local_binder list -> *) +(* env -> evar_map -> local_binder_expr list -> *) (* internalization_env * *) (* ((env * Evd.evar_universe_context * rel_context * sorts list) * Impargs.manual_implicits) *) @@ -177,7 +175,7 @@ val interp_context_evars : val locate_reference : Libnames.qualid -> Globnames.global_reference val is_global : Id.t -> bool -val construct_reference : Context.Named.t -> Id.t -> constr +val construct_reference : ('c, 't) Context.Named.pt -> Id.t -> constr val global_reference : Id.t -> constr val global_reference_in_absolute_module : DirPath.t -> Id.t -> constr diff --git a/interp/coqlib.ml b/interp/coqlib.ml index 588637b76..9539980f0 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -86,7 +86,7 @@ let check_required_library d = (Loc.ghost,make_qualid (DirPath.make (List.rev prefix)) m) *) (* or failing ...*) - errorlabstrm "Coqlib.check_required_library" + user_err ~hdr:"Coqlib.check_required_library" (str "Library " ++ pr_dirpath dir ++ str " has to be required first.") (************************************************************************) diff --git a/interp/coqlib.mli b/interp/coqlib.mli index 5ba26d828..1facb47e1 100644 --- a/interp/coqlib.mli +++ b/interp/coqlib.mli @@ -19,7 +19,7 @@ open Util (** [find_reference caller_message [dir;subdir;...] s] returns a global reference to the name dir.subdir.(...).s; the corresponding module must have been required or in the process of being compiled so that - it must be used lazyly; it raises an anomaly with the given message + it must be used lazily; it raises an anomaly with the given message if not found *) type message = string diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index b020f8945..9f549b0c0 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -173,32 +173,33 @@ let cook_notation df sc = (* - all single quotes in terminal tokens are doubled *) (* - characters < 32 are represented by '^A, '^B, '^C, etc *) (* The output is decoded in function Index.prepare_entry of coqdoc *) - let ntn = String.make (String.length df * 5) '_' in + let ntn = Bytes.make (String.length df * 5) '_' in let j = ref 0 in let l = String.length df - 1 in let i = ref 0 in + let open Bytes in (* Bytes.set *) while !i <= l do assert (df.[!i] != ' '); if df.[!i] == '_' && (Int.equal !i l || df.[!i+1] == ' ') then (* Next token is a non-terminal *) - (ntn.[!j] <- 'x'; incr j; incr i) + (set ntn !j 'x'; incr j; incr i) else begin (* Next token is a terminal *) - ntn.[!j] <- '\''; incr j; + set ntn !j '\''; incr j; while !i <= l && df.[!i] != ' ' do if df.[!i] < ' ' then let c = char_of_int (int_of_char 'A' + int_of_char df.[!i] - 1) in (String.blit ("'^" ^ String.make 1 c) 0 ntn !j 3; j := !j+3; incr i) else begin - if df.[!i] == '\'' then (ntn.[!j] <- '\''; incr j); - ntn.[!j] <- df.[!i]; incr j; incr i + if df.[!i] == '\'' then (set ntn !j '\''; incr j); + set ntn !j df.[!i]; incr j; incr i end done; - ntn.[!j] <- '\''; incr j + set ntn !j '\''; incr j end; - if !i <= l then (ntn.[!j] <- '_'; incr j; incr i) + if !i <= l then (set ntn !j '_'; incr j; incr i) done; - let df = String.sub ntn 0 !j in + let df = Bytes.sub_string ntn 0 !j in match sc with Some sc -> ":" ^ sc ^ ":" ^ df | _ -> "::" ^ df let dump_notation_location posl df (((path,secpath),_),sc) = diff --git a/interp/genintern.ml b/interp/genintern.ml index d6bfd347f..be7abfa99 100644 --- a/interp/genintern.ml +++ b/interp/genintern.ml @@ -16,6 +16,7 @@ type glob_sign = { type ('raw, 'glb) intern_fun = glob_sign -> 'raw -> glob_sign * 'glb type 'glb subst_fun = substitution -> 'glb -> 'glb +type 'glb ntn_subst_fun = Tactypes.glob_constr_and_expr Id.Map.t -> 'glb -> 'glb module InternObj = struct @@ -31,8 +32,16 @@ struct let default _ = None end +module NtnSubstObj = +struct + type ('raw, 'glb, 'top) obj = 'glb ntn_subst_fun + let name = "notation_subst" + let default _ = None +end + module Intern = Register (InternObj) module Subst = Register (SubstObj) +module NtnSubst = Register (NtnSubstObj) let intern = Intern.obj let register_intern0 = Intern.register0 @@ -50,3 +59,12 @@ let generic_substitute subs (GenArg (Glbwit wit, v)) = in_gen (glbwit wit) (substitute wit subs v) let () = Hook.set Detyping.subst_genarg_hook generic_substitute + +(** Notation substitution *) + +let substitute_notation = NtnSubst.obj +let register_ntn_subst0 = NtnSubst.register0 + +let generic_substitute_notation env (GenArg (Glbwit wit, v)) = + let v = substitute_notation wit env v in + in_gen (glbwit wit) v diff --git a/interp/genintern.mli b/interp/genintern.mli index 4b244b38d..4b0354be3 100644 --- a/interp/genintern.mli +++ b/interp/genintern.mli @@ -32,6 +32,14 @@ val substitute : ('raw, 'glb, 'top) genarg_type -> 'glb subst_fun val generic_substitute : glob_generic_argument subst_fun +(** {5 Notation functions} *) + +type 'glb ntn_subst_fun = Tactypes.glob_constr_and_expr Id.Map.t -> 'glb -> 'glb + +val substitute_notation : ('raw, 'glb, 'top) genarg_type -> 'glb ntn_subst_fun + +val generic_substitute_notation : glob_generic_argument ntn_subst_fun + (** Registering functions *) val register_intern0 : ('raw, 'glb, 'top) genarg_type -> @@ -39,3 +47,6 @@ val register_intern0 : ('raw, 'glb, 'top) genarg_type -> val register_subst0 : ('raw, 'glb, 'top) genarg_type -> 'glb subst_fun -> unit + +val register_ntn_subst0 : ('raw, 'glb, 'top) genarg_type -> + 'glb ntn_subst_fun -> unit diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 10cfbe58f..7f11c0a3b 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -21,18 +21,20 @@ open Libobject open Nameops open Misctypes open Context.Rel.Declaration + +module RelDecl = Context.Rel.Declaration (*i*) let generalizable_table = Summary.ref Id.Pred.empty ~name:"generalizable-ident" let declare_generalizable_ident table (loc,id) = if not (Id.equal id (root_of_id id)) then - user_err_loc(loc,"declare_generalizable_ident", - (pr_id id ++ str + user_err ~loc ~hdr:"declare_generalizable_ident" + ((pr_id id ++ str " is not declarable as generalizable identifier: it must have no trailing digits, quote, or _")); if Id.Pred.mem id table then - user_err_loc(loc,"declare_generalizable_ident", - (pr_id id++str" is already declared as a generalizable identifier")) + user_err ~loc ~hdr:"declare_generalizable_ident" + ((pr_id id++str" is already declared as a generalizable identifier")) else Id.Pred.add id table let add_generalizable gen table = @@ -78,8 +80,8 @@ let is_freevar ids env x = (* Auxiliary functions for the inference of implicitly quantified variables. *) let ungeneralizable loc id = - user_err_loc (loc, "Generalization", - str "Unbound and ungeneralizable variable " ++ pr_id id) + user_err ~loc ~hdr:"Generalization" + (str "Unbound and ungeneralizable variable " ++ pr_id id) let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l = let found loc id bdvars l = @@ -100,19 +102,20 @@ let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l = let ids_of_names l = List.fold_left (fun acc x -> match snd x with Name na -> na :: acc | Anonymous -> acc) [] l -let free_vars_of_binders ?(bound=Id.Set.empty) l (binders : local_binder list) = +let free_vars_of_binders ?(bound=Id.Set.empty) l (binders : local_binder_expr list) = let rec aux bdvars l c = match c with - ((LocalRawAssum (n, _, c)) :: tl) -> + ((CLocalAssum (n, _, c)) :: tl) -> let bound = ids_of_names n in let l' = free_vars_of_constr_expr c ~bound:bdvars l in aux (Id.Set.union (ids_of_list bound) bdvars) l' tl - | ((LocalRawDef (n, c)) :: tl) -> + | ((CLocalDef (n, c, t)) :: tl) -> let bound = match snd n with Anonymous -> [] | Name n -> [n] in let l' = free_vars_of_constr_expr c ~bound:bdvars l in - aux (Id.Set.union (ids_of_list bound) bdvars) l' tl + let l'' = Option.fold_left (fun l t -> free_vars_of_constr_expr t ~bound:bdvars l) l' t in + aux (Id.Set.union (ids_of_list bound) bdvars) l'' tl - | LocalPattern _ :: tl -> assert false + | CLocalPattern _ :: tl -> assert false | [] -> bdvars, l in aux bound l binders @@ -129,10 +132,15 @@ let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.emp else (id, loc) :: vs else vs | GApp (loc,f,args) -> List.fold_left (vars bound) vs (f::args) - | GLambda (loc,na,_,ty,c) | GProd (loc,na,_,ty,c) | GLetIn (loc,na,ty,c) -> + | GLambda (loc,na,_,ty,c) | GProd (loc,na,_,ty,c) -> let vs' = vars bound vs ty in let bound' = add_name_to_ids bound na in vars bound' vs' c + | GLetIn (loc,na,b,ty,c) -> + let vs' = vars bound vs b in + let vs'' = Option.fold_left (vars bound) vs' ty in + let bound' = add_name_to_ids bound na in + vars bound' vs'' c | GCases (loc,sty,rtntypopt,tml,pl) -> let vs1 = vars_option bound vs rtntypopt in let vs2 = List.fold_left (fun vs (tm,_) -> vars bound vs tm) vs1 tml in @@ -186,7 +194,7 @@ let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.emp vars let rec make_fresh ids env x = - if is_freevar ids env x then x else make_fresh ids env (Nameops.lift_subscript x) + if is_freevar ids env x then x else make_fresh ids env (Nameops.increment_subscript x) let next_name_away_from na avoid = match na with @@ -198,12 +206,12 @@ let combine_params avoid fn applied needed = List.partition (function (t, Some (loc, ExplByName id)) -> - let is_id (_, decl) = match get_name decl with + let is_id (_, decl) = match RelDecl.get_name decl with | Name id' -> Id.equal id id' | Anonymous -> false in if not (List.exists is_id needed) then - user_err_loc (loc,"",str "Wrong argument name: " ++ Nameops.pr_id id); + user_err ~loc (str "Wrong argument name: " ++ Nameops.pr_id id); true | _ -> false) applied in @@ -237,12 +245,12 @@ let combine_params avoid fn applied needed = aux (t' :: ids) avoid' app need | (x,_) :: _, [] -> - user_err_loc (Constrexpr_ops.constr_loc x,"",str "Typeclass does not expect more arguments") + user_err ~loc:(Constrexpr_ops.constr_loc x) (str "Typeclass does not expect more arguments") in aux [] avoid applied needed let combine_params_freevar = fun avoid (_, decl) -> - let id' = next_name_away_from (get_name decl) avoid in + let id' = next_name_away_from (RelDecl.get_name decl) avoid in (CRef (Ident (Loc.ghost, id'),None), Id.Set.add id' avoid) let destClassApp cl = @@ -316,7 +324,7 @@ let implicits_of_glob_constr ?(with_products=true) l = | _ -> () in [] | GLambda (loc, na, bk, t, b) -> abs na bk b - | GLetIn (loc, na, t, b) -> aux i b + | GLetIn (loc, na, b, t, c) -> aux i c | GRec (_, fix_kind, nas, args, tys, bds) -> let nb = match fix_kind with |GFix (_, n) -> n | GCoFix n -> n in List.fold_left_i (fun i l (na,bk,_,_) -> add_impl i na bk l) i (aux (List.length args.(nb) + i) bds.(nb)) args.(nb) diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index d0327e506..71009ec3c 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -25,7 +25,7 @@ val free_vars_of_constr_expr : constr_expr -> ?bound:Id.Set.t -> Id.t list -> Id.t list val free_vars_of_binders : - ?bound:Id.Set.t -> Id.t list -> local_binder list -> Id.Set.t * Id.t list + ?bound:Id.Set.t -> Id.t list -> local_binder_expr list -> Id.Set.t * Id.t list (** Returns the generalizable free ids in left-to-right order with the location of their first occurrence *) diff --git a/interp/interp.mllib b/interp/interp.mllib index 96b52959a..607af82a0 100644 --- a/interp/interp.mllib +++ b/interp/interp.mllib @@ -1,5 +1,4 @@ Stdarg -Constrarg Genintern Constrexpr_ops Notation_ops diff --git a/interp/modintern.ml b/interp/modintern.ml index e5dce5ccf..d4ade7058 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -26,16 +26,16 @@ let error_not_a_module_loc kind loc qid = | ModType -> Modops.ModuleTypingError (Modops.NotAModuleType s) | ModAny -> ModuleInternalizationError (NotAModuleNorModtype s) in - Loc.raise loc e + Loc.raise ~loc e let error_application_to_not_path loc me = - Loc.raise loc (Modops.ModuleTypingError (Modops.ApplicationToNotPath me)) + Loc.raise ~loc (Modops.ModuleTypingError (Modops.ApplicationToNotPath me)) let error_incorrect_with_in_module loc = - Loc.raise loc (ModuleInternalizationError IncorrectWithInModule) + Loc.raise ~loc (ModuleInternalizationError IncorrectWithInModule) let error_application_to_module_type loc = - Loc.raise loc (ModuleInternalizationError IncorrectModuleApplication) + Loc.raise ~loc (ModuleInternalizationError IncorrectModuleApplication) (** Searching for a module name in the Nametab. diff --git a/interp/notation.ml b/interp/notation.ml index 389a1c9df..90ac7f729 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -20,6 +20,9 @@ open Notation_term open Glob_term open Glob_ops open Ppextend +open Context.Named.Declaration + +module NamedDecl = Context.Named.Declaration (*i*) (*s A scope is a set of notations; it includes @@ -95,7 +98,7 @@ let declare_scope scope = scope_map := String.Map.add scope empty_scope !scope_map let error_unknown_scope sc = - errorlabstrm "Notation" + user_err ~hdr:"Notation" (str "Scope " ++ str sc ++ str " is not declared.") let find_scope scope = @@ -208,7 +211,7 @@ let remove_delimiters scope = let sc = find_scope scope in let newsc = { sc with delimiters = None } in match sc.delimiters with - | None -> CErrors.errorlabstrm "" (str "No bound key for scope " ++ str scope ++ str ".") + | None -> CErrors.user_err (str "No bound key for scope " ++ str scope ++ str ".") | Some key -> scope_map := String.Map.add scope newsc !scope_map; try @@ -220,8 +223,8 @@ let remove_delimiters scope = let find_delimiters_scope loc key = try String.Map.find key !delimiters_map with Not_found -> - user_err_loc - (loc, "find_delimiters", str "Unknown scope delimiting key " ++ str key ++ str ".") + user_err ~loc ~hdr:"find_delimiters" + (str "Unknown scope delimiting key " ++ str key ++ str ".") (* Uninterpretation tables *) @@ -337,8 +340,8 @@ let declare_string_interpreter sc dir interp (patl,uninterp,inpat) = let check_required_module loc sc (sp,d) = try let _ = Nametab.global_of_path sp in () with Not_found -> - user_err_loc (loc,"prim_token_interpreter", - str "Cannot interpret in " ++ str sc ++ str " without requiring first module " ++ str (List.last d) ++ str ".") + user_err ~loc ~hdr:"prim_token_interpreter" + (str "Cannot interpret in " ++ str sc ++ str " without requiring first module " ++ str (List.last d) ++ str ".") (* Look if some notation or numeral printer in [scope] can be used in the scope stack [scopes], and if yes, using delimiters or not *) @@ -458,8 +461,8 @@ let interp_prim_token_gen g loc p local_scopes = let p_as_ntn = try notation_of_prim_token p with Not_found -> "" in try find_interpretation p_as_ntn (find_prim_token g loc p) scopes with Not_found -> - user_err_loc (loc,"interp_prim_token", - (match p with + user_err ~loc ~hdr:"interp_prim_token" + ((match p with | Numeral n -> str "No interpretation for numeral " ++ str (to_string n) | String s -> str "No interpretation for string " ++ qs s) ++ str ".") @@ -483,8 +486,8 @@ let interp_notation loc ntn local_scopes = let scopes = make_current_scopes local_scopes in try find_interpretation ntn (find_notation ntn) scopes with Not_found -> - user_err_loc - (loc,"",str "Unknown interpretation for notation \"" ++ str ntn ++ str "\".") + user_err ~loc + (str "Unknown interpretation for notation \"" ++ str ntn ++ str "\".") let uninterp_notations c = List.map_append (fun key -> keymap_find key !notations_key_table) @@ -582,7 +585,7 @@ let scope_class_compare : scope_class -> scope_class -> int = cl_typ_ord let compute_scope_class t = - let (cl,_,_) = find_class_type Evd.empty t in + let (cl,_,_) = find_class_type Evd.empty (EConstr.of_constr t) in cl module ScopeClassOrd = @@ -612,7 +615,7 @@ let find_scope_class_opt = function (* Special scopes associated to arguments of a global reference *) let rec compute_arguments_classes t = - match kind_of_term (Reductionops.whd_betaiotazeta Evd.empty t) with + match kind_of_term (EConstr.Unsafe.to_constr (Reductionops.whd_betaiotazeta Evd.empty (EConstr.of_constr t))) with | Prod (_,t,u) -> let cl = try Some (compute_scope_class t) with Not_found -> None in cl :: compute_arguments_classes u @@ -684,7 +687,7 @@ let discharge_arguments_scope (_,(req,r,n,l,_)) = let n = try let vars = Lib.variable_section_segment_of_reference r in - List.length (List.filter (fun (_,_,b,_) -> b = None) vars) + vars |> List.map fst |> List.filter is_local_assum |> List.length with Not_found (* Not a ref defined in this section *) -> 0 in Some (req,Lib.discharge_global r,n,l,[]) @@ -888,11 +891,11 @@ let global_reference_of_notation test (ntn,(sc,c,_)) = | _ -> None let error_ambiguous_notation loc _ntn = - user_err_loc (loc,"",str "Ambiguous notation.") + user_err ~loc (str "Ambiguous notation.") let error_notation_not_reference loc ntn = - user_err_loc (loc,"", - str "Unable to interpret " ++ quote (str ntn) ++ + user_err ~loc + (str "Unable to interpret " ++ quote (str ntn) ++ str " as a reference.") let interp_notation_as_global_reference loc test ntn sc = @@ -924,19 +927,19 @@ let locate_notation prglob ntn scope = match ntns with | [] -> str "Unknown notation" | _ -> - t (str "Notation " ++ - tab () ++ str "Scope " ++ tab () ++ fnl () ++ + str "Notation" ++ fnl () ++ prlist (fun (ntn,l) -> let scope = find_default ntn scopes in prlist (fun (sc,r,(_,df)) -> hov 0 ( - pr_notation_info prglob df r ++ tbrk (1,2) ++ - (if String.equal sc default_scope then mt () else (str ": " ++ str sc)) ++ - tbrk (1,2) ++ - (if Option.equal String.equal (Some sc) scope then str "(default interpretation)" else mt ()) + pr_notation_info prglob df r ++ + (if String.equal sc default_scope then mt () + else (spc () ++ str ": " ++ str sc)) ++ + (if Option.equal String.equal (Some sc) scope + then spc () ++ str "(default interpretation)" else mt ()) ++ fnl ())) - l) ntns) + l) ntns let collect_notation_in_scope scope sc known = assert (not (String.equal scope default_scope)); @@ -1018,8 +1021,8 @@ let add_notation_extra_printing_rule ntn k v = let p, pp, gr = String.Map.find ntn !notation_rules in String.Map.add ntn (p, (k,v) :: pp, gr) !notation_rules with Not_found -> - user_err_loc (Loc.ghost,"add_notation_extra_printing_rule", - str "No such Notation.") + user_err ~hdr:"add_notation_extra_printing_rule" + (str "No such Notation.") (**********************************************************************) (* Synchronisation with reset *) diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 0c5393cf4..8b4fadb5a 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -36,7 +36,7 @@ let compare_glob_constr f add t1 t2 = match t1,t2 with on_true_do (f ty1 ty2 && f c1 c2) add na1 | GHole _, GHole _ -> true | GSort (_,s1), GSort (_,s2) -> Miscops.glob_sort_eq s1 s2 - | GLetIn (_,na1,b1,c1), GLetIn (_,na2,b2,c2) when Name.equal na1 na2 -> + | GLetIn (_,na1,b1,t1,c1), GLetIn (_,na2,b2,t2,c2) when Name.equal na1 na2 -> on_true_do (f b1 b2 && f c1 c2) add na1 | (GCases _ | GRec _ | GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _),_ @@ -63,8 +63,9 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with | NBinderList (i1, j1, t1, u1), NBinderList (i2, j2, t2, 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 vars) t1 t2 && (eq_notation_constr vars) u1 u2 +| NLetIn (na1, b1, t1, u1), NLetIn (na2, b2, t2, u2) -> + Name.equal na1 na2 && eq_notation_constr vars b1 b2 && + Option.equal (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 && @@ -168,8 +169,8 @@ let glob_constr_of_notation_constr_with_binders loc g f e = function let e',na = g e na in GLambda (loc,na,Explicit,f e ty,f e' c) | NProd (na,ty,c) -> let e',na = g e na in GProd (loc,na,Explicit,f e ty,f e' c) - | NLetIn (na,b,c) -> - let e',na = g e na in GLetIn (loc,na,f e b,f e' c) + | NLetIn (na,b,t,c) -> + let e',na = g e na in GLetIn (loc,na,f e b,Option.map (f e) t,f e' c) | NCases (sty,rtntypopt,tml,eqnl) -> let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') -> let e',t' = match t with @@ -242,8 +243,8 @@ let split_at_recursive_part c = let subtract_loc loc1 loc2 = Loc.make_loc (fst (Loc.unloc loc1),fst (Loc.unloc loc2)-1) let check_is_hole id = function GHole _ -> () | t -> - user_err_loc (loc_of_glob_constr t,"", - strbrk "In recursive notation with binders, " ++ pr_id id ++ + user_err ~loc:(loc_of_glob_constr t) + (strbrk "In recursive notation with binders, " ++ pr_id id ++ strbrk " is expected to come without type.") let pair_equal eq1 eq2 (a,b) (a',b') = eq1 a a' && eq2 b b' @@ -294,8 +295,8 @@ let compare_recursive_parts found f f' (iterator,subc) = let loc1 = loc_of_glob_constr iterator in let loc2 = loc_of_glob_constr (Option.get !terminator) in (* 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.") + user_err ~loc:(subtract_loc loc1 loc2) + (str "Both ends of the recursive pattern are the same.") | Some (x,y,RecursiveTerms lassoc) -> let newfound,x,y,lassoc = if List.mem_f (pair_equal Id.equal Id.equal) (x,y) (pi2 !found) || @@ -338,8 +339,8 @@ let notation_constr_and_vars_of_glob_constr a = | GApp (_,GVar (loc,f),[c]) when Id.equal f ldots_var -> (* Fall on the second part of the recursive pattern w/o having found the first part *) - user_err_loc (loc,"", - str "Cannot find where the recursive pattern starts.") + user_err ~loc + (str "Cannot find where the recursive pattern starts.") | c -> aux' c and aux' = function @@ -347,7 +348,7 @@ let notation_constr_and_vars_of_glob_constr a = | GApp (_,g,args) -> NApp (aux g, List.map aux args) | GLambda (_,na,bk,ty,c) -> add_name found na; NLambda (na,aux ty,aux c) | GProd (_,na,bk,ty,c) -> add_name found na; NProd (na,aux ty,aux c) - | GLetIn (_,na,b,c) -> add_name found na; NLetIn (na,aux b,aux c) + | GLetIn (_,na,b,t,c) -> add_name found na; NLetIn (na,aux b,Option.map aux t,aux c) | GCases (_,sty,rtntypopt,tml,eqnl) -> let f (_,idl,pat,rhs) = List.iter (add_id found) idl; (pat,aux rhs) in NCases (sty,Option.map aux rtntypopt, @@ -394,7 +395,7 @@ let check_variables_and_reversibility nenv (found,foundrec,foundrecbinding) = let vars = Id.Map.filter filter nenv.ninterp_var_type in let check_recvar x = if Id.List.mem x found then - errorlabstrm "" (pr_id x ++ + user_err (pr_id x ++ strbrk " should only be used in the recursive part of a pattern.") in let check (x, y) = check_recvar x; check_recvar y in let () = List.iter check foundrec in @@ -413,7 +414,7 @@ let check_variables_and_reversibility nenv (found,foundrec,foundrecbinding) = in let check_pair s x y where = if not (List.mem_f (pair_equal Id.equal Id.equal) (x,y) where) then - errorlabstrm "" (strbrk "in the right-hand side, " ++ pr_id x ++ + user_err (strbrk "in the right-hand side, " ++ pr_id x ++ str " and " ++ pr_id y ++ strbrk " should appear in " ++ str s ++ str " position as part of a recursive pattern.") in let check_type x typ = @@ -441,6 +442,7 @@ let notation_constr_of_glob_constr nenv a = (* Substitution of kernel names, avoiding a list of bound identifiers *) let notation_constr_of_constr avoiding t = + let t = EConstr.of_constr t in let t = Detyping.detype false avoiding (Global.env()) Evd.empty t in let nenv = { ninterp_var_type = Id.Map.empty; @@ -496,11 +498,12 @@ let rec subst_notation_constr subst bound raw = if r1' == r1 && r2' == r2 then raw else NBinderList (id1,id2,r1',r2') - | NLetIn (n,r1,r2) -> - let r1' = subst_notation_constr subst bound r1 - and r2' = subst_notation_constr subst bound r2 in - if r1' == r1 && r2' == r2 then raw else - NLetIn (n,r1',r2') + | NLetIn (n,r1,t,r2) -> + let r1' = subst_notation_constr subst bound r1 in + let t' = Option.smartmap (subst_notation_constr subst bound) t in + let r2' = subst_notation_constr subst bound r2 in + if r1' == r1 && t == t' && r2' == r2 then raw else + NLetIn (n,r1',t',r2') | NCases (sty,rtntypopt,rl,branches) -> let rtntypopt' = Option.smartmap (subst_notation_constr subst bound) rtntypopt @@ -780,18 +783,23 @@ let bind_bindinglist_env alp (terms,onlybinders,termlists,binderlists as sigma) | GHole _, _ -> v' | _, GHole _ -> v | _, _ -> if glob_constr_eq (alpha_rename (snd alp) v) v' then v else raise No_match in + let unify_opt_term alp v v' = + match v, v' with + | Some t, Some t' -> Some (unify_term alp t t') + | (Some _ as x), None | None, (Some _ as x) -> x + | None, None -> None in let unify_binding_kind bk bk' = if bk == bk' then bk' else raise No_match in let unify_binder alp b b' = match b, b' with - | (Inl na, bk, None, t), (Inl na', bk', None, t') (* assum *) -> + | GLocalAssum (loc,na,bk,t), GLocalAssum (_,na',bk',t') -> 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 *) -> + alp, GLocalAssum (loc, na, unify_binding_kind bk bk', unify_term alp t t') + | GLocalDef (loc,na,bk,c,t), GLocalDef (_,na',bk',c',t') -> 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 *) -> + alp, GLocalDef (loc, na, unify_binding_kind bk bk', unify_term alp c c', unify_opt_term alp t t') + | GLocalPattern (loc,(p,ids),id,bk,t), GLocalPattern (_,(p',_),_,bk',t') -> let alp, p = unify_pat alp p p' in - alp, (Inr p, unify_binding_kind bk bk', None, unify_term alp t t') + alp, GLocalPattern (loc, (p,ids), id, unify_binding_kind bk bk', unify_term alp t t') | _ -> raise No_match in let rec unify alp bl bl' = match bl, bl' with @@ -820,16 +828,16 @@ let bind_bindinglist_as_term_env alp (terms,onlybinders,termlists,binderlists) v 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 *) -> + | GVar (loc, id), GLocalAssum (_, na', bk', t') -> + GLocalAssum (loc, unify_id id na', bk', t') + | c, GLocalPattern (loc, (p',ids), id, bk', t') -> let p = pat_binder_of_term c in - (Inr (unify_pat p p'), bk', None, t') + GLocalPattern (loc, (unify_pat p p',ids), id, bk', 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, GLocalDef (_, _, _, _, t) :: bl' -> unify cl bl' | c :: cl, b' :: bl' -> unify_term_binder c b' :: unify cl bl' | _ -> raise No_match in let bl = unify cl bl' in @@ -882,19 +890,19 @@ 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)])) + | GLambda (loc,Name p,bk,t,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,ids,[cp],b)])) when islambda && Id.equal p e -> - match_iterated_binders islambda ((Inr cp,bk,None,t)::decls) b - | GLambda (_,na,bk,t,b) when islambda -> - match_iterated_binders islambda ((Inl na,bk,None,t)::decls) b - | GProd (_,Name p,bk,t,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],b)])) + match_iterated_binders islambda (GLocalPattern (loc,(cp,ids),p,bk,t)::decls) b + | GLambda (loc,na,bk,t,b) when islambda -> + match_iterated_binders islambda (GLocalAssum (loc,na,bk,t)::decls) b + | GProd (loc,Name p,bk,t,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,ids,[cp],b)])) when not islambda && Id.equal p e -> - match_iterated_binders islambda ((Inr cp,bk,None,t)::decls) b - | GProd (_,(Name _ as na),bk,t,b) when not islambda -> - match_iterated_binders islambda ((Inl na,bk,None,t)::decls) b - | GLetIn (loc,na,c,b) when glue_letin_with_decls -> + match_iterated_binders islambda (GLocalPattern (loc,(cp,ids),p,bk,t)::decls) b + | GProd (loc,(Name _ as na),bk,t,b) when not islambda -> + match_iterated_binders islambda (GLocalAssum (loc,na,bk,t)::decls) b + | GLetIn (loc,na,c,t,b) when glue_letin_with_decls -> match_iterated_binders islambda - ((Inl na,Explicit (*?*), Some c,GHole(loc,Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None))::decls) b + (GLocalDef (loc,na,Explicit (*?*), c,t)::decls) b | b -> (decls,b) let remove_sigma x (terms,onlybinders,termlists,binderlists) = @@ -971,29 +979,29 @@ let rec match_ inner u alp metas sigma a1 a2 = 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)])), + | GLambda (loc,Name p,bk,t1,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,ids,[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 (decls,b) = match_iterated_binders true [GLocalPattern(loc,(cp,ids),p,bk,t1)] b1 in let alp,sigma = bind_bindinglist_env alp sigma x decls in match_in u alp metas sigma b termin (* Matching recursive notations for binders: ad hoc cases supporting let-in *) - | GLambda (_,na1,bk,t1,b1), NBinderList (x,_,NLambda (Name _id2,_,b2),termin)-> - let (decls,b) = match_iterated_binders true [(Inl na1,bk,None,t1)] b1 in + | GLambda (loc,na1,bk,t1,b1), NBinderList (x,_,NLambda (Name _id2,_,b2),termin)-> + let (decls,b) = match_iterated_binders true [GLocalAssum (loc,na1,bk,t1)] b1 in (* TODO: address the possibility that termin is a Lambda itself *) let alp,sigma = bind_bindinglist_env alp sigma x decls in match_in u alp metas sigma b termin (* "∀ p, let 'cp = p in t" -> "∀ 'cp, t" *) - | GProd (_,Name p,bk,t1,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],b1)])), + | GProd (loc,Name p,bk,t1,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,ids,[cp],b1)])), NBinderList (x,_,NProd (Name _id2,_,b2),(NVar v as termin)) when Id.equal p e -> - let (decls,b) = match_iterated_binders true [(Inr cp,bk,None,t1)] b1 in + let (decls,b) = match_iterated_binders true [GLocalPattern (loc,(cp,ids),p,bk,t1)] b1 in let alp,sigma = bind_bindinglist_env alp sigma x decls in match_in u alp metas sigma b termin - | GProd (_,na1,bk,t1,b1), NBinderList (x,_,NProd (Name _id2,_,b2),termin) + | GProd (loc,na1,bk,t1,b1), NBinderList (x,_,NProd (Name _id2,_,b2),termin) when na1 != Anonymous -> - let (decls,b) = match_iterated_binders false [(Inl na1,bk,None,t1)] b1 in + let (decls,b) = match_iterated_binders false [GLocalAssum (loc,na1,bk,t1)] b1 in (* TODO: address the possibility that termin is a Prod itself *) let alp,sigma = bind_bindinglist_env alp sigma x decls in match_in u alp metas sigma b termin @@ -1002,18 +1010,18 @@ let rec match_ inner u alp metas sigma a1 a2 = 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)])), + | GLambda (loc,Name p,bk,t,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,ids,[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 + let alp,sigma = bind_bindinglist_env alp sigma id [GLocalPattern (loc,(cp,ids),p,bk,t)] in match_in u alp metas sigma b1 b2 - | GLambda (_,na,bk,t,b1), NLambda (Name id,_,b2) + | GLambda (loc,na,bk,t,b1), NLambda (Name id,_,b2) when is_bindinglist_meta id metas -> - let alp,sigma = bind_bindinglist_env alp sigma id [(Inl na,bk,None,t)] in + let alp,sigma = bind_bindinglist_env alp sigma id [GLocalAssum (loc,na,bk,t)] in match_in u alp metas sigma b1 b2 - | GProd (_,na,bk,t,b1), NProd (Name id,_,b2) + | GProd (loc,na,bk,t,b1), NProd (Name id,_,b2) when is_bindinglist_meta id metas && na != Anonymous -> - let alp,sigma = bind_bindinglist_env alp sigma id [(Inl na,bk,None,t)] in + let alp,sigma = bind_bindinglist_env alp sigma id [GLocalAssum (loc,na,bk,t)] in match_in u alp metas sigma b1 b2 (* Matching compositionally *) @@ -1034,8 +1042,12 @@ let rec match_ inner u alp metas sigma a1 a2 = match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2 | GProd (_,na1,_,t1,b1), NProd (na2,t2,b2) -> match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2 - | GLetIn (_,na1,t1,b1), NLetIn (na2,t2,b2) -> - match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2 + | GLetIn (_,na1,b1,_,c1), NLetIn (na2,b2,None,c2) + | GLetIn (_,na1,b1,None,c1), NLetIn (na2,b2,_,c2) -> + match_binders u alp metas na1 na2 (match_in u alp metas sigma b1 b2) c1 c2 + | GLetIn (_,na1,b1,Some t1,c1), NLetIn (na2,b2,Some t2,c2) -> + match_binders u alp metas na1 na2 + (match_in u alp metas (match_in u alp metas sigma b1 b2) t1 t2) c1 c2 | GCases (_,sty1,rtno1,tml1,eqnl1), NCases (sty2,rtno2,tml2,eqnl2) when sty1 == sty2 && Int.equal (List.length tml1) (List.length tml2) @@ -1101,7 +1113,7 @@ let rec match_ inner u alp metas sigma a1 a2 = | _ -> assert false in let (alp,sigma) = if is_bindinglist_meta id metas then - bind_bindinglist_env alp sigma id [(Inl (Name id'),Explicit,None,t1)] + bind_bindinglist_env alp sigma id [GLocalAssum (Loc.ghost,Name id',Explicit,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 diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli index c8fcbf741..a61ba172e 100644 --- a/interp/notation_ops.mli +++ b/interp/notation_ops.mli @@ -47,12 +47,9 @@ val glob_constr_of_notation_constr : Loc.t -> notation_constr -> glob_constr 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_decl2 list * subscopes) list + (extended_glob_local_binder list * subscopes) list val match_notation_constr_cases_pattern : cases_pattern -> interpretation -> diff --git a/interp/ppextend.ml b/interp/ppextend.ml index 37bbe0ce8..87ca25325 100644 --- a/interp/ppextend.ml +++ b/interp/ppextend.ml @@ -23,12 +23,9 @@ type ppbox = | PpHOVB of int | PpHVB of int | PpVB of int - | PpTB type ppcut = | PpBrk of int * int - | PpTbrk of int * int - | PpTab | PpFnl let ppcmd_of_box = function @@ -36,13 +33,10 @@ let ppcmd_of_box = function | PpHOVB n -> hov n | PpHVB n -> hv n | PpVB n -> v n - | PpTB -> t let ppcmd_of_cut = function - | PpTab -> tab () | PpFnl -> fnl () | PpBrk(n1,n2) -> brk(n1,n2) - | PpTbrk(n1,n2) -> tbrk(n1,n2) type unparsing = | UnpMetaVar of int * parenRelation diff --git a/interp/ppextend.mli b/interp/ppextend.mli index de7a42eee..09dc36943 100644 --- a/interp/ppextend.mli +++ b/interp/ppextend.mli @@ -23,12 +23,9 @@ type ppbox = | PpHOVB of int | PpHVB of int | PpVB of int - | PpTB type ppcut = | PpBrk of int * int - | PpTbrk of int * int - | PpTab | PpFnl val ppcmd_of_box : ppbox -> std_ppcmds -> std_ppcmds diff --git a/interp/reserve.ml b/interp/reserve.ml index 388ca0805..1565ba4a9 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -86,13 +86,13 @@ let in_reserved : Id.t * notation_constr -> obj = let declare_reserved_type_binding (loc,id) t = if not (Id.equal id (root_of_id id)) then - user_err_loc(loc,"declare_reserved_type", - (pr_id id ++ str + user_err ~loc ~hdr:"declare_reserved_type" + ((pr_id id ++ str " is not reservable: it must have no trailing digits, quote, or _")); begin try let _ = Id.Map.find id !reserve_table in - user_err_loc(loc,"declare_reserved_type", - (pr_id id++str" is already bound to a type")) + user_err ~loc ~hdr:"declare_reserved_type" + ((pr_id id++str" is already bound to a type")) with Not_found -> () end; add_anonymous_leaf (in_reserved (id,t)) @@ -107,7 +107,9 @@ let constr_key c = let revert_reserved_type t = try + let t = EConstr.Unsafe.to_constr t in let reserved = KeyMap.find (constr_key t) !reserve_revtable in + let t = EConstr.of_constr t in let t = Detyping.detype false [] (Global.env()) Evd.empty t in (* pedrot: if [Notation_ops.match_notation_constr] may raise [Failure _] then I've introduced a bug... *) diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml index 478774219..d863e0561 100644 --- a/interp/smartlocate.ml +++ b/interp/smartlocate.ml @@ -28,7 +28,7 @@ let global_of_extended_global_head = function | NRef ref -> ref | NApp (rc, _) -> head_of rc | NCast (rc, _) -> head_of rc - | NLetIn (_, _, rc) -> head_of rc + | NLetIn (_, _, _, rc) -> head_of rc | _ -> raise Not_found in head_of syn_def @@ -46,7 +46,7 @@ let locate_global_with_alias ?(head=false) (loc,qid) = if head then global_of_extended_global_head ref else global_of_extended_global ref with Not_found -> - user_err_loc (loc,"",pr_qualid qid ++ + user_err ~loc (pr_qualid qid ++ str " is bound to a notation that does not denote a reference.") let global_inductive_with_alias r = @@ -54,14 +54,14 @@ let global_inductive_with_alias r = try match locate_global_with_alias lqid with | IndRef ind -> ind | ref -> - user_err_loc (loc_of_reference r,"global_inductive", - pr_reference r ++ spc () ++ str "is not an inductive type.") - with Not_found -> Nametab.error_global_not_found_loc loc qid + user_err ~loc:(loc_of_reference r) ~hdr:"global_inductive" + (pr_reference r ++ spc () ++ str "is not an inductive type.") + with Not_found -> Nametab.error_global_not_found ~loc qid let global_with_alias ?head r = let (loc,qid as lqid) = qualid_of_reference r in try locate_global_with_alias ?head lqid - with Not_found -> Nametab.error_global_not_found_loc loc qid + with Not_found -> Nametab.error_global_not_found ~loc qid let smart_global ?head = function | AN r -> diff --git a/interp/stdarg.ml b/interp/stdarg.ml index 2a7d52e3a..341ff5662 100644 --- a/interp/stdarg.ml +++ b/interp/stdarg.ml @@ -6,6 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Loc +open Misctypes +open Tactypes open Genarg open Geninterp @@ -29,7 +32,49 @@ let wit_string : string uniform_genarg_type = let wit_pre_ident : string uniform_genarg_type = make0 ~dyn:(val_tag (topwit wit_string)) "preident" +let loc_of_or_by_notation f = function + | AN c -> f c + | ByNotation (loc,s,_) -> loc + +let wit_int_or_var = + make0 ~dyn:(val_tag (topwit wit_int)) "int_or_var" + +let wit_intro_pattern = + make0 "intropattern" + +let wit_ident = + make0 "ident" + +let wit_var = + make0 ~dyn:(val_tag (topwit wit_ident)) "var" + +let wit_ref = make0 "ref" + +let wit_quant_hyp = make0 "quant_hyp" + +let wit_constr = + make0 "constr" + +let wit_uconstr = make0 "uconstr" + +let wit_open_constr = make0 ~dyn:(val_tag (topwit wit_constr)) "open_constr" + +let wit_constr_with_bindings = make0 "constr_with_bindings" + +let wit_bindings = make0 "bindings" + +let wit_red_expr = make0 "redexpr" + +let wit_clause_dft_concl = + make0 "clause_dft_concl" + (** Aliases for compatibility *) let wit_integer = wit_int let wit_preident = wit_pre_ident +let wit_reference = wit_ref +let wit_global = wit_ref +let wit_clause = wit_clause_dft_concl +let wit_quantified_hypothesis = wit_quant_hyp +let wit_intropattern = wit_intro_pattern +let wit_redexpr = wit_red_expr diff --git a/interp/stdarg.mli b/interp/stdarg.mli index e1f648d7f..113fe40ba 100644 --- a/interp/stdarg.mli +++ b/interp/stdarg.mli @@ -8,8 +8,22 @@ (** Basic generic arguments. *) +open Loc +open Names +open Term +open EConstr +open Libnames +open Globnames +open Genredexpr +open Pattern +open Constrexpr +open Misctypes +open Tactypes open Genarg +(** FIXME: nothing to do there. *) +val loc_of_or_by_notation : ('a -> Loc.t) -> 'a or_by_notation -> Loc.t + val wit_unit : unit uniform_genarg_type val wit_bool : bool uniform_genarg_type @@ -20,7 +34,54 @@ val wit_string : string uniform_genarg_type val wit_pre_ident : string uniform_genarg_type +(** {5 Additional generic arguments} *) + +val wit_int_or_var : (int or_var, int or_var, int) genarg_type + +val wit_intro_pattern : (constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type + +val wit_ident : Id.t uniform_genarg_type + +val wit_var : (Id.t located, Id.t located, Id.t) genarg_type + +val wit_ref : (reference, global_reference located or_var, global_reference) genarg_type + +val wit_quant_hyp : quantified_hypothesis uniform_genarg_type + +val wit_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type + +val wit_uconstr : (constr_expr , glob_constr_and_expr, Glob_term.closed_glob_constr) genarg_type + +val wit_open_constr : + (constr_expr, glob_constr_and_expr, constr) genarg_type + +val wit_constr_with_bindings : + (constr_expr with_bindings, + glob_constr_and_expr with_bindings, + constr with_bindings delayed_open) genarg_type + +val wit_bindings : + (constr_expr bindings, + glob_constr_and_expr bindings, + constr bindings delayed_open) genarg_type + +val wit_red_expr : + ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen, + (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen, + (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type + +val wit_clause_dft_concl : (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) genarg_type + (** Aliases for compatibility *) val wit_integer : int uniform_genarg_type val wit_preident : string uniform_genarg_type +val wit_reference : (reference, global_reference located or_var, global_reference) genarg_type +val wit_global : (reference, global_reference located or_var, global_reference) genarg_type +val wit_clause : (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) genarg_type +val wit_quantified_hypothesis : quantified_hypothesis uniform_genarg_type +val wit_intropattern : (constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type +val wit_redexpr : + ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen, + (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen, + (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index 2523063e6..c3f4c4f30 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -30,7 +30,7 @@ let add_syntax_constant kn c onlyparse = let load_syntax_constant i ((sp,kn),(_,pat,onlyparse)) = if Nametab.exists_cci sp then - errorlabstrm "cache_syntax_constant" + user_err ~hdr:"cache_syntax_constant" (pr_id (basename sp) ++ str " already exists"); add_syntax_constant kn pat onlyparse; Nametab.push_syndef (Nametab.Until i) sp kn diff --git a/interp/topconstr.ml b/interp/topconstr.ml index bf0ce60d8..d3142e7f0 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -31,8 +31,8 @@ let _ = Goptions.declare_bool_option { (**********************************************************************) (* Miscellaneous *) -let error_invalid_pattern_notation loc = - user_err_loc (loc,"",str "Invalid notation for pattern.") +let error_invalid_pattern_notation ?loc () = + user_err ?loc (str "Invalid notation for pattern.") (**********************************************************************) (* Functions on constr_expr *) @@ -59,8 +59,8 @@ let rec cases_pattern_fold_names f a = function | CPatAtom (_,Some (Ident (_,id))) when not (is_constructor id) -> f id a | CPatPrim _ | CPatAtom _ -> a | CPatCast (loc,_,_) -> - CErrors.user_err_loc (loc, "cases_pattern_fold_names", - Pp.strbrk "Casts are not supported here.") + CErrors.user_err ~loc ~hdr:"cases_pattern_fold_names" + (Pp.strbrk "Casts are not supported here.") let ids_of_pattern = cases_pattern_fold_names Id.Set.add Id.Set.empty @@ -91,13 +91,13 @@ let rec fold_constr_expr_binders g f n acc b = function f n acc b let rec fold_local_binders g f n acc b = function - | LocalRawAssum (nal,bk,t)::l -> + | CLocalAssum (nal,bk,t)::l -> let nal = snd (List.split nal) in let n' = List.fold_right (name_fold g) nal n in 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 (_,pat,t)::l -> + | CLocalDef ((_,na),c,t)::l -> + Option.fold_left (f n) (f n (fold_local_binders g f (name_fold g na n) acc b l) c) t + | CLocalPattern (_,pat,t)::l -> let acc = fold_local_binders g f (cases_pattern_fold_names g n pat) acc b l in Option.fold_left (f n) acc t | [] -> @@ -107,7 +107,8 @@ let fold_constr_expr_with_binders g f n acc = function | CAppExpl (loc,(_,_,_),l) -> List.fold_left (f n) acc l | CApp (loc,(_,t),l) -> List.fold_left (f n) (f n acc t) (List.map fst l) | CProdN (_,l,b) | CLambdaN (_,l,b) -> fold_constr_expr_binders g f n acc b l - | CLetIn (_,na,a,b) -> fold_constr_expr_binders g f n acc b [[na],default_binder_kind,a] + | CLetIn (_,na,a,t,b) -> + f (name_fold g (snd na) n) (Option.fold_left (f n) (f n acc a) t) b | CCast (loc,a,(CastConv b|CastVM b|CastNative b)) -> f n (f n acc a) b | CCast (loc,a,CastCoerce) -> f n acc a | CNotation (_,_,(l,ll,bll)) -> @@ -162,7 +163,7 @@ let split_at_annot bl na = end | Some (loc, id) -> let rec aux acc = function - | LocalRawAssum (bls, k, t) as x :: rest -> + | CLocalAssum (bls, k, t) as x :: rest -> let test (_, na) = match na with | Name id' -> Id.equal id id' | Anonymous -> false @@ -173,16 +174,16 @@ let split_at_annot bl na = | _ -> let ans = match l with | [] -> acc - | _ -> LocalRawAssum (l, k, t) :: acc + | _ -> CLocalAssum (l, k, t) :: acc in - (List.rev ans, LocalRawAssum (r, k, t) :: rest) + (List.rev ans, CLocalAssum (r, k, t) :: rest) end - | LocalRawDef _ as x :: rest -> aux (x :: acc) rest - | LocalPattern (loc,_,_) :: rest -> - Loc.raise loc (Stream.Error "pattern with quote not allowed after fix") + | CLocalDef _ as x :: rest -> aux (x :: acc) rest + | CLocalPattern (loc,_,_) :: rest -> + Loc.raise ~loc (Stream.Error "pattern with quote not allowed after fix") | [] -> - user_err_loc(loc,"", - str "No parameter named " ++ Nameops.pr_id id ++ str".") + user_err ~loc + (str "No parameter named " ++ Nameops.pr_id id ++ str".") in aux [] bl (* Used in correctness and interface *) @@ -198,13 +199,13 @@ let map_binders f g e bl = let map_local_binders f g e bl = (* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *) let h (e,bl) = function - 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) - | LocalPattern (loc,pat,t) -> + CLocalAssum(nal,k,ty) -> + (map_binder g e nal, CLocalAssum(nal,k,f e ty)::bl) + | CLocalDef((loc,na),c,ty) -> + (name_fold g na e, CLocalDef((loc,na),f e c,Option.map (f e) ty)::bl) + | CLocalPattern (loc,pat,t) -> let ids = ids_of_pattern pat in - (Id.Set.fold g ids e, LocalPattern (loc,pat,Option.map (f e) t)::bl) in + (Id.Set.fold g ids e, CLocalPattern (loc,pat,Option.map (f e) t)::bl) in let (e,rbl) = List.fold_left h (e,[]) bl in (e, List.rev rbl) @@ -216,7 +217,8 @@ let map_constr_expr_with_binders g f e = function let (e,bl) = map_binders f g e bl in CProdN (loc,bl,f e b) | CLambdaN (loc,bl,b) -> let (e,bl) = map_binders f g e bl in CLambdaN (loc,bl,f e b) - | CLetIn (loc,na,a,b) -> CLetIn (loc,na,f e a,f (name_fold g (snd na) e) b) + | CLetIn (loc,na,a,t,b) -> + CLetIn (loc,na,f e a,Option.map (f e) t,f (name_fold g (snd na) e) b) | CCast (loc,a,c) -> CCast (loc,f e a, Miscops.map_cast_type (f e) c) | CNotation (loc,n,(l,ll,bll)) -> (* This is an approximation because we don't know what binds what *) diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 58edd4ddf..b6ac40041 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -25,7 +25,7 @@ val occur_var_constr_expr : Id.t -> constr_expr -> bool (** Specific function for interning "in indtype" syntax of "match" *) val ids_of_cases_indtype : cases_pattern_expr -> Id.Set.t -val split_at_annot : local_binder list -> Id.t located option -> local_binder list * local_binder list +val split_at_annot : local_binder_expr list -> Id.t located option -> local_binder_expr list * local_binder_expr list (** Used in typeclasses *) @@ -46,4 +46,4 @@ val patntn_loc : (** For cases pattern parsing errors *) -val error_invalid_pattern_notation : Loc.t -> 'a +val error_invalid_pattern_notation : ?loc:Loc.t -> unit -> 'a |