aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrarg.ml74
-rw-r--r--interp/constrarg.mli87
-rw-r--r--interp/constrexpr_ops.ml136
-rw-r--r--interp/constrexpr_ops.mli31
-rw-r--r--interp/constrextern.ml71
-rw-r--r--interp/constrextern.mli2
-rw-r--r--interp/constrintern.ml387
-rw-r--r--interp/constrintern.mli35
-rw-r--r--interp/coqlib.ml2
-rw-r--r--interp/coqlib.mli2
-rw-r--r--interp/dumpglob.ml17
-rw-r--r--interp/genintern.ml18
-rw-r--r--interp/genintern.mli11
-rw-r--r--interp/implicit_quantifiers.ml94
-rw-r--r--interp/implicit_quantifiers.mli2
-rw-r--r--interp/interp.mllib1
-rw-r--r--interp/modintern.ml8
-rw-r--r--interp/notation.ml77
-rw-r--r--interp/notation.mli4
-rw-r--r--interp/notation_ops.ml130
-rw-r--r--interp/notation_ops.mli5
-rw-r--r--interp/ppextend.ml6
-rw-r--r--interp/ppextend.mli3
-rw-r--r--interp/reserve.ml10
-rw-r--r--interp/smartlocate.ml12
-rw-r--r--interp/stdarg.ml43
-rw-r--r--interp/stdarg.mli60
-rw-r--r--interp/syntax_def.ml4
-rw-r--r--interp/topconstr.ml55
-rw-r--r--interp/topconstr.mli4
30 files changed, 639 insertions, 752 deletions
diff --git a/interp/constrarg.ml b/interp/constrarg.ml
deleted file mode 100644
index ca828102b9..0000000000
--- 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 6ccd944d43..0000000000
--- 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 04429851fd..542f9feaf6 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
@@ -262,17 +263,12 @@ let cases_pattern_expr_loc = function
| CPatDelimiters (loc,_,_) -> loc
| CPatCast(loc,_,_) -> loc
-let raw_cases_pattern_expr_loc = function
- | RCPatAlias (loc,_,_) -> loc
- | RCPatCstr (loc,_,_,_) -> loc
- | RCPatAtom (loc,_) -> loc
- | 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 +281,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 +297,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 a92da035f6..b547288e3f 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] *)
@@ -36,8 +36,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 +45,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 +77,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 dd8a48b85e..59b8b4e5b9 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 f617faa38a..b39339450a 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 4e76fe9aae..2426366c62 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,40 +424,34 @@ 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
env, b
-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
@@ -469,12 +461,18 @@ let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = functio
match !intern_cases_pattern_fwd (None,env.scopes) p with
| (il, [(subst,cp)]) ->
if not (Id.Map.equal Id.equal subst Id.Map.empty) then
- user_err_loc (loc,"",str "Unsupported nested \"as\" clause.");
+ user_err ~loc (str "Unsupported nested \"as\" clause.");
il,cp
| _ -> assert false
in
let env = {env with ids = List.fold_right Id.Set.add il env.ids} 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
@@ -544,35 +542,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,[]
@@ -586,10 +578,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
@@ -637,23 +630,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) ->
@@ -661,7 +644,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)
@@ -741,7 +724,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 =
@@ -765,12 +748,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
@@ -802,7 +785,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
@@ -811,7 +794,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
@@ -824,7 +807,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
@@ -849,9 +832,9 @@ 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 ++
- str " cannot have a universe instance, its expanded head
- does not start with a reference")
+ user_err ~loc (str "Notation " ++ pr_qualid qid
+ ++ str " cannot have a universe instance,"
+ ++ str " its expanded head does not start with a reference")
in
c, projapp, args2
@@ -865,7 +848,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
@@ -881,7 +864,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,_,_,_),_ =
@@ -894,7 +877,22 @@ let interp_reference vars r =
(**********************************************************************)
(** {5 Cases } *)
-(** {6 Elemtary bricks } *)
+(** Private internalization patterns *)
+type raw_cases_pattern_expr =
+ | RCPatAlias of Loc.t * raw_cases_pattern_expr * Id.t
+ | RCPatCstr of Loc.t * Globnames.global_reference
+ * raw_cases_pattern_expr list * raw_cases_pattern_expr list
+ (** [RCPatCstr (loc, c, l1, l2)] represents ((@c l1) l2) *)
+ | RCPatAtom of Loc.t * Id.t option
+ | RCPatOr of Loc.t * raw_cases_pattern_expr list
+
+let raw_cases_pattern_expr_loc = function
+ | RCPatAlias (loc,_,_) -> loc
+ | RCPatCstr (loc,_,_,_) -> loc
+ | RCPatAtom (loc,_) -> loc
+ | RCPatOr (loc,_) -> loc
+
+(** {6 Elementary bricks } *)
let apply_scope_env env = function
| [] -> {env with tmp_scope = None}, []
| sc::scl -> {env with tmp_scope = sc}, scl
@@ -948,7 +946,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.
@@ -957,7 +955,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 =
@@ -982,14 +980,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*)
@@ -1000,7 +998,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 =
@@ -1008,10 +1006,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 ->
@@ -1033,7 +1031,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
@@ -1058,8 +1056,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
@@ -1089,7 +1087,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
@@ -1102,7 +1100,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
@@ -1116,15 +1114,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)
| [] ->
@@ -1193,8 +1190,8 @@ let rec subst_pat_iterator y t p = match p with
| RCPatAtom (_,id) ->
begin match id with Some x when Id.equal x y -> t | _ -> p end
| RCPatCstr (loc,id,l1,l2) ->
- RCPatCstr (loc,id,List.map (subst_pat_iterator y t) l1,
- List.map (subst_pat_iterator y t) l2)
+ RCPatCstr (loc,id,List.map (subst_pat_iterator y t) l1,
+ List.map (subst_pat_iterator y t) l2)
| RCPatAlias (l,p,a) -> RCPatAlias (l,subst_pat_iterator y t p,a)
| RCPatOr (l,pl) -> RCPatOr (l,List.map (subst_pat_iterator y t) pl)
@@ -1206,11 +1203,19 @@ 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
in
+ (** [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *)
+ let rec rcp_of_glob = function
+ | GVar (loc,id) -> RCPatAtom (loc,Some id)
+ | GHole (loc,_,_,_) -> RCPatAtom (loc,None)
+ | GRef (loc,g,_) -> RCPatCstr (loc, g,[],[])
+ | GApp (loc,GRef (_,g,_),l) -> RCPatCstr (loc, g, List.map rcp_of_glob l,[])
+ | _ -> CErrors.anomaly Pp.(str "Invalid return pattern from Notation.interp_prim_token_cases_pattern_expr ")
+ in
let rec drop_syndef top scopes re pats =
let (loc,qid) = qualid_of_reference re in
try
@@ -1280,8 +1285,9 @@ let drop_notations_pattern looked_for =
let (argscs1,_) = find_remaining_scopes expl_pl pl g in
RCPatCstr (loc, g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat false scopes) pl, [])
| CPatNotation (loc,"- _",([CPatPrim(_,Numeral p)],[]),[])
- when Bigint.is_strictly_pos p ->
- fst (Notation.interp_prim_token_cases_pattern_expr loc (ensure_kind false loc) (Numeral (Bigint.neg p)) scopes)
+ when Bigint.is_strictly_pos p ->
+ let (pat, _df) = Notation.interp_prim_token_cases_pattern_expr loc (ensure_kind false loc) (Numeral (Bigint.neg p)) scopes in
+ rcp_of_glob pat
| CPatNotation (_,"( _ )",([a],[]),[]) ->
in_pat top scopes a
| CPatNotation (loc, ntn, fullargs,extrargs) ->
@@ -1294,7 +1300,9 @@ let drop_notations_pattern looked_for =
in_not top loc scopes (subst,substlist) extrargs c
| CPatDelimiters (loc, key, e) ->
in_pat top (None,find_delimiters_scope loc key::snd scopes) e
- | CPatPrim (loc,p) -> fst (Notation.interp_prim_token_cases_pattern_expr loc (test_kind false) p scopes)
+ | CPatPrim (loc,p) ->
+ let (pat, _df) = Notation.interp_prim_token_cases_pattern_expr loc (test_kind false) p scopes in
+ rcp_of_glob pat
| CPatAtom (loc, Some id) ->
begin
match drop_syndef top scopes id [] with
@@ -1304,8 +1312,21 @@ let drop_notations_pattern looked_for =
| CPatAtom (loc,None) -> RCPatAtom (loc,None)
| CPatOr (loc, pl) ->
RCPatOr (loc,List.map (in_pat top scopes) pl)
- | CPatCast _ ->
- assert false
+ | CPatCast (loc,_,_) ->
+ (* We raise an error if the pattern contains a cast, due to
+ current restrictions on casts in patterns. Cast in patterns
+ are supportted only in local binders and only at top
+ level. In fact, they are currently eliminated by the
+ parser. The only reason why they are in the
+ [cases_pattern_expr] type is that the parser needs to factor
+ the "(c : t)" notation with user defined notations (such as
+ the pair). In the long term, we will try to support such
+ casts everywhere, and use them to print the domains of
+ lambdas in the encoding of match in constr. This check is
+ here and not in the parser because it would require
+ duplicating the levels of the [pattern] rule. *)
+ CErrors.user_err ~loc ~hdr:"drop_notations_pattern"
+ (Pp.strbrk "Casts are not supported in this pattern.")
and in_pat_sc scopes x = in_pat false (x,snd scopes)
and in_not top loc scopes (subst,substlist as fullsubst) args = function
| NVar id ->
@@ -1331,8 +1352,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
@@ -1347,7 +1368,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 =
@@ -1387,40 +1408,7 @@ let rec intern_pat genv aliases pat =
check_or_pat_variables loc ids (List.tl idsl);
(ids,List.flatten pl')
-(* [check_no_patcast p] raises an error if [p] contains a cast. This code is a
- bit ad-hoc, and is due to current restrictions on casts in patterns. We
- support them only in local binders and only at top level. In fact, they are
- currently eliminated by the parser. The only reason why they are in the
- [cases_pattern_expr] type is that the parser needs to factor the "(c : t)"
- notation with user defined notations (such as the pair). In the long term, we
- will try to support such casts everywhere, and use them to print the domains
- of lambdas in the encoding of match in constr. We put this check here and not
- in the parser because it would require to duplicate the levels of the
- [pattern] rule. *)
-let rec check_no_patcast = function
- | CPatCast (loc,_,_) ->
- CErrors.user_err_loc (loc, "check_no_patcast",
- Pp.strbrk "Casts are not supported here.")
- | CPatDelimiters(_,_,p)
- | CPatAlias(_,p,_) -> check_no_patcast p
- | CPatCstr(_,_,opl,pl) ->
- Option.iter (List.iter check_no_patcast) opl;
- List.iter check_no_patcast pl
- | CPatOr(_,pl) ->
- List.iter check_no_patcast pl
- | CPatNotation(_,_,subst,pl) ->
- check_no_patcast_subst subst;
- List.iter check_no_patcast pl
- | CPatRecord(_,prl) ->
- List.iter (fun (_,p) -> check_no_patcast p) prl
- | CPatAtom _ | CPatPrim _ -> ()
-
-and check_no_patcast_subst (pl,pll) =
- List.iter check_no_patcast pl;
- List.iter (List.iter check_no_patcast) pll
-
let intern_cases_pattern genv scopes aliases pat =
- check_no_patcast pat;
intern_pat genv aliases
(drop_notations_pattern (function ConstructRef _ -> () | _ -> raise Not_found) scopes pat)
@@ -1429,15 +1417,14 @@ let _ =
fun scopes p -> intern_cases_pattern (Global.env ()) scopes empty_alias p
let intern_ind_pattern genv scopes pat =
- check_no_patcast pat;
let no_not =
try
drop_notations_pattern (function (IndRef _ | ConstructRef _) -> () | _ -> raise Not_found) scopes pat
- 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
@@ -1445,8 +1432,8 @@ let intern_ind_pattern genv scopes pat =
(with_letin,
match product_of_cases_patterns empty_alias (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 *)
@@ -1485,10 +1472,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) ->
@@ -1498,11 +1485,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)
@@ -1533,10 +1520,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) =
@@ -1548,24 +1533,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) ->
@@ -1579,20 +1559,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) ->
@@ -1603,9 +1581,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 ->
@@ -1658,7 +1637,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
@@ -1728,7 +1707,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
@@ -1832,7 +1813,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
@@ -1881,7 +1862,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"."));
[]
@@ -1912,8 +1893,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 *)
@@ -1926,7 +1907,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 = {
@@ -1952,7 +1933,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)
(*********************************************************************)
@@ -2005,7 +1986,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
@@ -2046,8 +2027,6 @@ let interp_binder_evars env evdref na t =
let t' = locate_if_hole (loc_of_glob_constr t) na t in
understand_tcc_evars env evdref ~expected_type:IsType t'
-open Environ
-
let my_intern_constr env lvar acc c =
internalize env acc false lvar c
@@ -2056,22 +2035,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 61e7c6f5cb..fdd50c6a1e 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -18,7 +18,6 @@ open Constrexpr
open Notation_term
open Pretyping
open Misctypes
-open Decl_kinds
(** Translation from front abstract syntax of term to untyped terms (glob_constr) *)
@@ -75,8 +74,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 +87,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 +98,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 +106,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 +150,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 +174,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 588637b76e..9539980f04 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 5ba26d8286..1facb47e1e 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 b020f89457..9f549b0c0f 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 d6bfd347ff..be7abfa995 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 4b244b38d8..4b0354be39 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 10cfbe58fa..19c872b310 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -19,20 +19,21 @@ open Typeclasses_errors
open Pp
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 +79,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,27 +101,23 @@ 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
-let add_name_to_ids set na =
- match na with
- | Anonymous -> set
- | Name id -> Id.Set.add id set
-
let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.empty) =
let rec vars bound vs = function
| GVar (loc,id) ->
@@ -128,56 +125,7 @@ let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.emp
if Id.List.mem_assoc id vs then vs
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) ->
- let vs' = 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
- List.fold_left (vars_pattern bound) vs2 pl
- | GLetTuple (loc,nal,rtntyp,b,c) ->
- let vs1 = vars_return_type bound vs rtntyp in
- let vs2 = vars bound vs1 b in
- let bound' = List.fold_left add_name_to_ids bound nal in
- vars bound' vs2 c
- | GIf (loc,c,rtntyp,b1,b2) ->
- let vs1 = vars_return_type bound vs rtntyp in
- let vs2 = vars bound vs1 c in
- let vs3 = vars bound vs2 b1 in
- vars bound vs3 b2
- | GRec (loc,fk,idl,bl,tyl,bv) ->
- let bound' = Array.fold_right Id.Set.add idl bound in
- let vars_fix i vs fid =
- let vs1,bound1 =
- List.fold_left
- (fun (vs,bound) (na,k,bbd,bty) ->
- let vs' = vars_option bound vs bbd in
- let vs'' = vars bound vs' bty in
- let bound' = add_name_to_ids bound na in
- (vs'',bound')
- )
- (vs,bound')
- bl.(i)
- in
- let vs2 = vars bound1 vs1 tyl.(i) in
- vars bound1 vs2 bv.(i)
- in
- Array.fold_left_i vars_fix vs idl
- | GCast (loc,c,k) -> let v = vars bound vs c in
- (match k with CastConv t | CastVM t -> vars bound v t | _ -> v)
- | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> vs
-
- and vars_pattern bound vs (loc,idl,p,c) =
- let bound' = List.fold_right Id.Set.add idl bound in
- vars bound' vs c
-
- and vars_option bound vs = function None -> vs | Some p -> vars bound vs p
-
- and vars_return_type bound vs (na,tyopt) =
- let bound' = add_name_to_ids bound na in
- vars_option bound' vs tyopt
+ | c -> Glob_ops.fold_glob_constr_with_binders Id.Set.add vars bound vs c
in fun rt ->
let vars = List.rev (vars bound [] rt) in
List.iter (fun (id, loc) ->
@@ -186,7 +134,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 +146,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 +185,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 +264,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 d0327e5068..71009ec3c2 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 96b52959a0..607af82a03 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 e5dce5ccf3..d4ade7058a 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 389a1c9dff..7be2fe0f01 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -20,6 +20,8 @@ open Notation_term
open Glob_term
open Glob_ops
open Ppextend
+open Context.Named.Declaration
+
(*i*)
(*s A scope is a set of notations; it includes
@@ -95,7 +97,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 +210,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 +222,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 +339,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 *)
@@ -442,49 +444,50 @@ let notation_of_prim_token = function
| Numeral n -> "- "^(to_string (neg n))
| String _ -> raise Not_found
-let find_prim_token g loc p sc =
+let find_prim_token check_allowed loc p sc =
(* Try for a user-defined numerical notation *)
try
let (_,c),df = find_notation (notation_of_prim_token p) sc in
- g (Notation_ops.glob_constr_of_notation_constr loc c),df
+ let pat = Notation_ops.glob_constr_of_notation_constr loc c in
+ check_allowed pat;
+ pat, df
with Not_found ->
(* Try for a primitive numerical notation *)
let (spdir,interp) = Hashtbl.find prim_token_interpreter_tab sc loc p in
check_required_module loc sc spdir;
- g (interp ()), ((dirpath (fst spdir),DirPath.empty),"")
+ let pat = interp () in
+ check_allowed pat;
+ pat, ((dirpath (fst spdir),DirPath.empty),"")
let interp_prim_token_gen g loc p local_scopes =
let scopes = make_current_scopes local_scopes in
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 ".")
let interp_prim_token =
- interp_prim_token_gen (fun x -> x)
-
-(** [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *)
+ interp_prim_token_gen (fun _ -> ())
-let rec rcp_of_glob looked_for = function
- | GVar (loc,id) -> RCPatAtom (loc,Some id)
- | GHole (loc,_,_,_) -> RCPatAtom (loc,None)
- | GRef (loc,g,_) -> looked_for g; RCPatCstr (loc, g,[],[])
+let rec check_allowed_ref_in_pat looked_for = function
+ | GVar _ | GHole _ -> ()
+ | GRef (_,g,_) -> looked_for g
| GApp (loc,GRef (_,g,_),l) ->
- looked_for g; RCPatCstr (loc, g, List.map (rcp_of_glob looked_for) l,[])
+ looked_for g; List.iter (check_allowed_ref_in_pat looked_for) l
| _ -> raise Not_found
let interp_prim_token_cases_pattern_expr loc looked_for p =
- interp_prim_token_gen (rcp_of_glob looked_for) loc p
+ interp_prim_token_gen (check_allowed_ref_in_pat looked_for) loc p
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.mli b/interp/notation.mli
index 2e92a00a8c..300480ff1c 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -85,8 +85,10 @@ val declare_string_interpreter : scope_name -> required_module ->
val interp_prim_token : Loc.t -> prim_token -> local_scopes ->
glob_constr * (notation_location * scope_name option)
+
+(* This function returns a glob_const representing a pattern *)
val interp_prim_token_cases_pattern_expr : Loc.t -> (global_reference -> unit) -> prim_token ->
- local_scopes -> raw_cases_pattern_expr * (notation_location * scope_name option)
+ local_scopes -> glob_constr * (notation_location * scope_name option)
(** Return the primitive token associated to a [term]/[cases_pattern];
raise [No_match] if no such token *)
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 0c5393cf41..d08fb107be 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
@@ -1129,10 +1141,6 @@ let term_of_binder = function
| Name id -> GVar (Loc.ghost,id)
| Anonymous -> GHole (Loc.ghost,Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None)
-type glob_decl2 =
- (name, cases_pattern) Util.union * Decl_kinds.binding_kind *
- glob_constr option * glob_constr
-
let match_notation_constr u c (metas,pat) =
let terms,binders,termlists,binderlists =
match_ false u ([],[]) metas ([],[],[],[]) c pat in
diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index c8fcbf7410..a61ba172ee 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 37bbe0ce87..87ca253253 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 de7a42eee5..09dc369437 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 388ca08050..1565ba4a92 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 478774219e..d863e05616 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 2a7d52e3af..5920b0d508 100644
--- a/interp/stdarg.ml
+++ b/interp/stdarg.ml
@@ -6,6 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open Misctypes
open Genarg
open Geninterp
@@ -29,7 +30,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 e1f648d7fc..ac40a23281 100644
--- a/interp/stdarg.mli
+++ b/interp/stdarg.mli
@@ -8,8 +8,21 @@
(** Basic generic arguments. *)
+open Loc
+open Names
+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 +33,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 2523063e64..ed7b0b70d4 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
@@ -106,5 +106,3 @@ let search_syntactic_definition kn =
let def = out_pat pat in
verbose_compat kn def v;
def
-
-open Goptions
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index bf0ce60d88..e05be65fb0 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,21 @@ 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 ((_,na),_,_) as x :: rest ->
+ if Name.equal (Name id) na then
+ user_err ~loc
+ (Nameops.pr_id id ++ str" must be a proper parameter and not a local definition.")
+ else
+ 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 +204,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 +222,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 58edd4ddf8..b6ac40041e 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 00:14:40 +0000