summaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrexpr.ml162
-rw-r--r--interp/constrexpr_ops.ml107
-rw-r--r--interp/constrexpr_ops.mli26
-rw-r--r--interp/constrextern.ml285
-rw-r--r--interp/constrextern.mli8
-rw-r--r--interp/constrintern.ml238
-rw-r--r--interp/constrintern.mli14
-rw-r--r--interp/declare.ml117
-rw-r--r--interp/declare.mli6
-rw-r--r--interp/discharge.ml7
-rw-r--r--interp/dumpglob.ml10
-rw-r--r--interp/dumpglob.mli10
-rw-r--r--interp/genintern.ml8
-rw-r--r--interp/genintern.mli8
-rw-r--r--interp/genredexpr.ml65
-rw-r--r--interp/impargs.ml310
-rw-r--r--interp/impargs.mli9
-rw-r--r--interp/implicit_quantifiers.ml25
-rw-r--r--interp/implicit_quantifiers.mli17
-rw-r--r--interp/interp.mllib6
-rw-r--r--interp/modintern.ml12
-rw-r--r--interp/modintern.mli3
-rw-r--r--interp/notation.ml961
-rw-r--r--interp/notation.mli179
-rw-r--r--interp/notation_ops.ml83
-rw-r--r--interp/notation_ops.mli10
-rw-r--r--interp/notation_term.ml98
-rw-r--r--interp/ppextend.ml43
-rw-r--r--interp/redops.ml64
-rw-r--r--interp/redops.mli (renamed from interp/ppextend.mli)28
-rw-r--r--interp/reserve.ml6
-rw-r--r--interp/reserve.mli2
-rw-r--r--interp/smartlocate.ml19
-rw-r--r--interp/smartlocate.mli13
-rw-r--r--interp/stdarg.ml15
-rw-r--r--interp/stdarg.mli38
-rw-r--r--interp/syntax_def.ml4
-rw-r--r--interp/tactypes.ml34
-rw-r--r--interp/topconstr.ml23
-rw-r--r--interp/topconstr.mli53
40 files changed, 2033 insertions, 1093 deletions
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
new file mode 100644
index 00000000..77d612cf
--- /dev/null
+++ b/interp/constrexpr.ml
@@ -0,0 +1,162 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open Names
+open Libnames
+open Decl_kinds
+
+(** {6 Concrete syntax for terms } *)
+
+(** [constr_expr] is the abstract syntax tree produced by the parser *)
+type universe_decl_expr = (lident list, Glob_term.glob_constraint list) UState.gen_universe_decl
+
+type ident_decl = lident * universe_decl_expr option
+type name_decl = lname * universe_decl_expr option
+
+type notation_entry = InConstrEntry | InCustomEntry of string
+type notation_entry_level = InConstrEntrySomeLevel | InCustomEntryLevel of string * int
+type notation_key = string
+type notation = notation_entry_level * notation_key
+
+type 'a or_by_notation_r =
+ | AN of 'a
+ | ByNotation of (string * string option)
+
+type 'a or_by_notation = 'a or_by_notation_r CAst.t
+
+(* NB: the last string in [ByNotation] is actually a [Notation.delimiters],
+ but this formulation avoids a useless dependency. *)
+
+type explicitation =
+ | ExplByPos of int * Id.t option (* a reference to the n-th product starting from left *)
+ | ExplByName of Id.t
+
+type binder_kind =
+ | Default of binding_kind
+ | Generalized of binding_kind * binding_kind * bool
+ (** Inner binding, outer bindings, typeclass-specific flag
+ for implicit generalization of superclasses *)
+
+type abstraction_kind = AbsLambda | AbsPi
+
+type proj_flag = int option (** [Some n] = proj of the n-th visible argument *)
+
+(** Representation of integer literals that appear in Coq scripts.
+ We now use raw strings of digits in base 10 (big-endian), and a separate
+ sign flag. Note that this representation is not unique, due to possible
+ multiple leading zeros, and -0 = +0 *)
+
+type sign = bool
+type raw_natural_number = string
+
+type prim_token =
+ | Numeral of raw_natural_number * sign
+ | String of string
+
+type instance_expr = Glob_term.glob_level list
+
+type cases_pattern_expr_r =
+ | CPatAlias of cases_pattern_expr * lname
+ | CPatCstr of qualid
+ * cases_pattern_expr list option * cases_pattern_expr list
+ (** [CPatCstr (_, c, Some l1, l2)] represents [(@ c l1) l2] *)
+ | CPatAtom of qualid option
+ | CPatOr of cases_pattern_expr list
+ | CPatNotation of notation * cases_pattern_notation_substitution
+ * cases_pattern_expr list (** CPatNotation (_, n, l1 ,l2) represents
+ (notation n applied with substitution l1)
+ applied to arguments l2 *)
+ | CPatPrim of prim_token
+ | CPatRecord of (qualid * cases_pattern_expr) list
+ | CPatDelimiters of string * cases_pattern_expr
+ | CPatCast of cases_pattern_expr * constr_expr
+and cases_pattern_expr = cases_pattern_expr_r CAst.t
+
+and cases_pattern_notation_substitution =
+ cases_pattern_expr list * (** for constr subterms *)
+ cases_pattern_expr list list (** for recursive notations *)
+
+and constr_expr_r =
+ | CRef of qualid * instance_expr option
+ | CFix of lident * fix_expr list
+ | CCoFix of lident * cofix_expr list
+ | CProdN of local_binder_expr list * constr_expr
+ | CLambdaN of local_binder_expr list * constr_expr
+ | CLetIn of lname * constr_expr * constr_expr option * constr_expr
+ | CAppExpl of (proj_flag * qualid * instance_expr option) * constr_expr list
+ | CApp of (proj_flag * constr_expr) *
+ (constr_expr * explicitation CAst.t option) list
+ | CRecord of (qualid * constr_expr) list
+
+ (* representation of the "let" and "match" constructs *)
+ | CCases of Constr.case_style (* determines whether this value represents "let" or "match" construct *)
+ * constr_expr option (* return-clause *)
+ * case_expr list
+ * branch_expr list (* branches *)
+
+ | CLetTuple of lname list * (lname option * constr_expr option) *
+ constr_expr * constr_expr
+ | CIf of constr_expr * (lname option * constr_expr option)
+ * constr_expr * constr_expr
+ | CHole of Evar_kinds.t option * Namegen.intro_pattern_naming_expr * Genarg.raw_generic_argument option
+ | CPatVar of Pattern.patvar
+ | CEvar of Glob_term.existential_name * (Id.t * constr_expr) list
+ | CSort of Glob_term.glob_sort
+ | CCast of constr_expr * constr_expr Glob_term.cast_type
+ | CNotation of notation * constr_notation_substitution
+ | CGeneralization of binding_kind * abstraction_kind option * constr_expr
+ | CPrim of prim_token
+ | CDelimiters of string * constr_expr
+and constr_expr = constr_expr_r CAst.t
+
+and case_expr = constr_expr (* expression that is being matched *)
+ * lname option (* as-clause *)
+ * cases_pattern_expr option (* in-clause *)
+
+and branch_expr =
+ (cases_pattern_expr list list * constr_expr) CAst.t
+
+and fix_expr =
+ lident * (lident option * recursion_order_expr) *
+ local_binder_expr list * constr_expr * constr_expr
+
+and cofix_expr =
+ lident * local_binder_expr list * constr_expr * constr_expr
+
+and recursion_order_expr =
+ | CStructRec
+ | CWfRec of constr_expr
+ | CMeasureRec of constr_expr * constr_expr option (** measure, relation *)
+
+(* Anonymous defs allowed ?? *)
+and local_binder_expr =
+ | CLocalAssum of lname list * binder_kind * constr_expr
+ | CLocalDef of lname * constr_expr * constr_expr option
+ | CLocalPattern of (cases_pattern_expr * constr_expr option) CAst.t
+
+and constr_notation_substitution =
+ constr_expr list * (** for constr subterms *)
+ constr_expr list list * (** for recursive notations *)
+ cases_pattern_expr list * (** for binders *)
+ local_binder_expr list list (** for binder lists (recursive notations) *)
+
+type constr_pattern_expr = constr_expr
+
+(** Concrete syntax for modules and module types *)
+
+type with_declaration_ast =
+ | CWith_Module of Id.t list CAst.t * qualid
+ | CWith_Definition of Id.t list CAst.t * universe_decl_expr option * constr_expr
+
+type module_ast_r =
+ | CMident of qualid
+ | CMapply of module_ast * module_ast
+ | CMwith of module_ast * with_declaration_ast
+and module_ast = module_ast_r CAst.t
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 004c9356..23d0536d 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -10,12 +10,13 @@
open Pp
open Util
-open CAst
open Names
open Nameops
open Libnames
+open Namegen
+open Glob_term
open Constrexpr
-open Misctypes
+open Notation
open Decl_kinds
(***********************)
@@ -72,22 +73,22 @@ let rec cases_pattern_expr_eq p1 p2 =
| CPatAlias(a1,i1), CPatAlias(a2,i2) ->
eq_ast Name.equal i1 i2 && cases_pattern_expr_eq a1 a2
| CPatCstr(c1,a1,b1), CPatCstr(c2,a2,b2) ->
- eq_reference c1 c2 &&
+ qualid_eq c1 c2 &&
Option.equal (List.equal cases_pattern_expr_eq) a1 a2 &&
List.equal cases_pattern_expr_eq b1 b2
| CPatAtom(r1), CPatAtom(r2) ->
- Option.equal eq_reference r1 r2
+ Option.equal qualid_eq r1 r2
| CPatOr a1, CPatOr a2 ->
List.equal cases_pattern_expr_eq a1 a2
| CPatNotation (n1, s1, l1), CPatNotation (n2, s2, l2) ->
- String.equal n1 n2 &&
+ notation_eq n1 n2 &&
cases_pattern_notation_substitution_eq s1 s2 &&
List.equal cases_pattern_expr_eq l1 l2
| CPatPrim i1, CPatPrim i2 ->
prim_token_eq i1 i2
| CPatRecord l1, CPatRecord l2 ->
let equal (r1, e1) (r2, e2) =
- eq_reference r1 r2 && cases_pattern_expr_eq e1 e2
+ qualid_eq r1 r2 && cases_pattern_expr_eq e1 e2
in
List.equal equal l1 l2
| CPatDelimiters(s1,e1), CPatDelimiters(s2,e2) ->
@@ -107,7 +108,7 @@ let eq_universes u1 u2 =
let rec constr_expr_eq e1 e2 =
if CAst.(e1.v == e2.v) then true
else match CAst.(e1.v, e2.v) with
- | CRef (r1,u1), CRef (r2,u2) -> eq_reference r1 r2 && eq_universes u1 u2
+ | CRef (r1,u1), CRef (r2,u2) -> qualid_eq r1 r2 && eq_universes u1 u2
| CFix(id1,fl1), CFix(id2,fl2) ->
eq_ast Id.equal id1 id2 &&
List.equal fix_expr_eq fl1 fl2
@@ -127,7 +128,7 @@ let rec constr_expr_eq e1 e2 =
constr_expr_eq b1 b2
| CAppExpl((proj1,r1,_),al1), CAppExpl((proj2,r2,_),al2) ->
Option.equal Int.equal proj1 proj2 &&
- eq_reference r1 r2 &&
+ qualid_eq r1 r2 &&
List.equal constr_expr_eq al1 al2
| CApp((proj1,e1),al1), CApp((proj2,e2),al2) ->
Option.equal Int.equal proj1 proj2 &&
@@ -135,7 +136,7 @@ let rec constr_expr_eq e1 e2 =
List.equal args_eq al1 al2
| CRecord l1, CRecord l2 ->
let field_eq (r1, e1) (r2, e2) =
- eq_reference r1 r2 && constr_expr_eq e1 e2
+ qualid_eq r1 r2 && constr_expr_eq e1 e2
in
List.equal field_eq l1 l2
| CCases(_,r1,a1,brl1), CCases(_,r2,a2,brl2) ->
@@ -161,11 +162,11 @@ let rec constr_expr_eq e1 e2 =
| CEvar (id1, c1), CEvar (id2, c2) ->
Id.equal id1 id2 && List.equal instance_eq c1 c2
| CSort s1, CSort s2 ->
- Miscops.glob_sort_eq s1 s2
+ Glob_ops.glob_sort_eq s1 s2
| CCast(t1,c1), CCast(t2,c2) ->
constr_expr_eq t1 t2 && cast_expr_eq c1 c2
| CNotation(n1, s1), CNotation(n2, s2) ->
- String.equal n1 n2 &&
+ notation_eq n1 n2 &&
constr_notation_substitution_eq s1 s2
| CPrim i1, CPrim i2 ->
prim_token_eq i1 i2
@@ -179,7 +180,7 @@ let rec constr_expr_eq e1 e2 =
| (CRef _ | CFix _ | CCoFix _ | CProdN _ | CLambdaN _ | CLetIn _ | CAppExpl _
| CApp _ | CRecord _ | CCases _ | CLetTuple _ | CIf _ | CHole _
| CPatVar _ | CEvar _ | CSort _ | CCast _ | CNotation _ | CPrim _
- | CGeneralization _ | CDelimiters _), _ -> false
+ | CGeneralization _ | CDelimiters _ ), _ -> false
and args_eq (a1,e1) (a2,e2) =
Option.equal (eq_ast explicitation_eq) e1 e2 &&
@@ -277,7 +278,9 @@ let rec cases_pattern_fold_names f a pt = match CAst.(pt.v) with
List.fold_left (cases_pattern_fold_names f)
(List.fold_left (cases_pattern_fold_names f) a (patl@List.flatten patll)) patl'
| CPatDelimiters (_,pat) -> cases_pattern_fold_names f a pat
- | CPatAtom (Some {v=Ident id}) when not (is_constructor id) -> f id a
+ | CPatAtom (Some qid)
+ when qualid_is_ident qid && not (is_constructor @@ qualid_basename qid) ->
+ f (qualid_basename qid) a
| CPatPrim _ | CPatAtom _ -> a
| CPatCast ({CAst.loc},_) ->
CErrors.user_err ?loc ~hdr:"cases_pattern_fold_names"
@@ -358,7 +361,9 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function
let free_vars_of_constr_expr c =
let rec aux bdvars l = function
- | { CAst.v = CRef ({v=Ident id},_) } -> if Id.List.mem id bdvars then l else Id.Set.add id l
+ | { CAst.v = CRef (qid, _) } when qualid_is_ident qid ->
+ let id = qualid_basename qid in
+ if Id.List.mem id bdvars then l else Id.Set.add id l
| c -> fold_constr_expr_with_binders (fun a l -> a::l) aux bdvars l c
in aux [] Id.Set.empty c
@@ -391,7 +396,7 @@ let map_constr_expr_with_binders g f e = CAst.map (function
let (e,bl) = map_local_binders f g e bl in CLambdaN (bl,f e b)
| CLetIn (na,a,t,b) ->
CLetIn (na,f e a,Option.map (f e) t,f (Name.fold_right g (na.CAst.v) e) b)
- | CCast (a,c) -> CCast (f e a, Miscops.map_cast_type (f e) c)
+ | CCast (a,c) -> CCast (f e a, Glob_ops.map_cast_type (f e) c)
| CNotation (n,(l,ll,bl,bll)) ->
(* This is an approximation because we don't know what binds what *)
CNotation (n,(List.map (f e) l,List.map (List.map (f e)) ll, bl,
@@ -433,11 +438,13 @@ let map_constr_expr_with_binders g f e = CAst.map (function
)
(* Used in constrintern *)
-let rec replace_vars_constr_expr l = function
- | { CAst.loc; v = CRef ({v=Ident id},us) } as x ->
- (try CAst.make ?loc @@ CRef (make ?loc @@ Ident (Id.Map.find id l),us) with Not_found -> x)
- | c -> map_constr_expr_with_binders Id.Map.remove
- replace_vars_constr_expr l c
+let rec replace_vars_constr_expr l r =
+ match r with
+ | { CAst.loc; v = CRef (qid,us) } as x when qualid_is_ident qid ->
+ let id = qualid_basename qid in
+ (try CAst.make ?loc @@ CRef (qualid_of_ident ?loc (Id.Map.find id l),us)
+ with Not_found -> x)
+ | cn -> map_constr_expr_with_binders Id.Map.remove replace_vars_constr_expr l cn
(* Returns the ranges of locs of the notation that are not occupied by args *)
(* and which are then occupied by proper symbols of the notation (or spaces) *)
@@ -506,7 +513,7 @@ let split_at_annot bl na =
(** Pseudo-constructors *)
-let mkIdentC id = CAst.make @@ CRef (make @@ Ident id,None)
+let mkIdentC id = CAst.make @@ CRef (qualid_of_ident id,None)
let mkRefC r = CAst.make @@ CRef (r,None)
let mkCastC (a,k) = CAst.make @@ CCast (a,k)
let mkLambdaC (idl,bk,a,b) = CAst.make @@ CLambdaN ([CLocalAssum (idl,bk,a)],b)
@@ -525,21 +532,23 @@ let mkCProdN ?loc bll c =
let mkCLambdaN ?loc bll c =
CAst.make ?loc @@ CLambdaN (bll,c)
-let coerce_reference_to_id = CAst.with_loc_val (fun ?loc -> function
- | Ident id -> id
- | Qualid _ ->
- CErrors.user_err ?loc ~hdr:"coerce_reference_to_id"
- (str "This expression should be a simple identifier."))
+let coerce_reference_to_id qid =
+ if qualid_is_ident qid then qualid_basename qid
+ else
+ CErrors.user_err ?loc:qid.CAst.loc ~hdr:"coerce_reference_to_id"
+ (str "This expression should be a simple identifier.")
let coerce_to_id = function
- | { CAst.loc; v = CRef ({v=Ident id},None) } -> CAst.make ?loc id
+ | { CAst.loc; v = CRef (qid,None) } when qualid_is_ident qid ->
+ CAst.make ?loc @@ qualid_basename qid
| { CAst.loc; _ } -> CErrors.user_err ?loc
~hdr:"coerce_to_id"
(str "This expression should be a simple identifier.")
let coerce_to_name = function
- | { CAst.loc; v = CRef ({v=Ident id},None) } -> CAst.make ?loc @@ Name id
- | { CAst.loc; v = CHole (None,Misctypes.IntroAnonymous,None) } -> CAst.make ?loc Anonymous
+ | { CAst.loc; v = CRef (qid,None) } when qualid_is_ident qid ->
+ CAst.make ?loc @@ Name (qualid_basename qid)
+ | { CAst.loc; v = CHole (None,IntroAnonymous,None) } -> CAst.make ?loc Anonymous
| { CAst.loc; _ } -> CErrors.user_err ?loc ~hdr:"coerce_to_name"
(str "This expression should be a name.")
@@ -563,9 +572,10 @@ let mkAppPattern ?loc p lp =
let rec coerce_to_cases_pattern_expr c = CAst.map_with_loc (fun ?loc -> function
| CRef (r,None) ->
CPatAtom (Some r)
- | CHole (None,Misctypes.IntroAnonymous,None) ->
+ | CHole (None,IntroAnonymous,None) ->
CPatAtom None
- | CLetIn ({CAst.loc;v=Name id},b,None,{ CAst.v = CRef ({v=Ident id'},None) }) when Id.equal id id' ->
+ | CLetIn ({CAst.loc;v=Name id},b,None,{ CAst.v = CRef (qid,None) })
+ when qualid_is_ident qid && Id.equal id (qualid_basename qid) ->
CPatAlias (coerce_to_cases_pattern_expr b, CAst.(make ?loc @@ Name id))
| CApp ((None,p),args) when List.for_all (fun (_,e) -> e=None) args ->
(mkAppPattern (coerce_to_cases_pattern_expr p) (List.map (fun (a,_) -> coerce_to_cases_pattern_expr a) args)).CAst.v
@@ -595,7 +605,34 @@ let _ = Goptions.declare_bool_option {
Goptions.optwrite = (fun a -> asymmetric_patterns:=a);
}
-(************************************************************************)
-(* Deprecated *)
-let abstract_constr_expr c bl = mkCLambdaN ?loc:(local_binders_loc bl) bl c
-let prod_constr_expr c bl = mkCProdN ?loc:(local_binders_loc bl) bl c
+(** Local universe and constraint declarations. *)
+
+let interp_univ_constraints env evd cstrs =
+ let interp (evd,cstrs) (u, d, u') =
+ let ul = Pretyping.interp_known_glob_level evd u in
+ let u'l = Pretyping.interp_known_glob_level evd u' in
+ let cstr = (ul,d,u'l) in
+ let cstrs' = Univ.Constraint.add cstr cstrs in
+ try let evd = Evd.add_constraints evd (Univ.Constraint.singleton cstr) in
+ evd, cstrs'
+ with Univ.UniverseInconsistency e ->
+ CErrors.user_err ~hdr:"interp_constraint"
+ (Univ.explain_universe_inconsistency (Termops.pr_evd_level evd) e)
+ in
+ List.fold_left interp (evd,Univ.Constraint.empty) cstrs
+
+let interp_univ_decl env decl =
+ let open UState in
+ let pl : lident list = decl.univdecl_instance in
+ let evd = Evd.from_ctx (UState.make_with_initial_binders (Environ.universes env) pl) in
+ let evd, cstrs = interp_univ_constraints env evd decl.univdecl_constraints in
+ let decl = { univdecl_instance = pl;
+ univdecl_extensible_instance = decl.univdecl_extensible_instance;
+ univdecl_constraints = cstrs;
+ univdecl_extensible_constraints = decl.univdecl_extensible_constraints }
+ in evd, decl
+
+let interp_univ_decl_opt env l =
+ match l with
+ | None -> Evd.from_env env, UState.default_univ_decl
+ | Some decl -> interp_univ_decl env decl
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index d038bd71..61e8aa1b 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -10,7 +10,6 @@
open Names
open Libnames
-open Misctypes
open Constrexpr
(** Constrexpr_ops: utilities on [constr_expr] *)
@@ -42,9 +41,9 @@ val local_binders_loc : local_binder_expr list -> Loc.t option
(** {6 Constructors}*)
val mkIdentC : Id.t -> constr_expr
-val mkRefC : reference -> constr_expr
+val mkRefC : qualid -> constr_expr
val mkAppC : constr_expr * constr_expr list -> constr_expr
-val mkCastC : constr_expr * constr_expr cast_type -> constr_expr
+val mkCastC : constr_expr * constr_expr Glob_term.cast_type -> constr_expr
val mkLambdaC : lname list * binder_kind * constr_expr * constr_expr -> constr_expr
val mkLetInC : lname * constr_expr * constr_expr option * constr_expr -> constr_expr
val mkProdC : lname list * binder_kind * constr_expr * constr_expr -> constr_expr
@@ -60,17 +59,9 @@ val mkCPatOr : ?loc:Loc.t -> cases_pattern_expr list -> cases_pattern_expr
val mkAppPattern : ?loc:Loc.t -> cases_pattern_expr -> cases_pattern_expr list -> cases_pattern_expr
(** Apply a list of pattern arguments to a pattern *)
-(** @deprecated variant of mkCLambdaN *)
-val abstract_constr_expr : constr_expr -> local_binder_expr list -> constr_expr
-[@@ocaml.deprecated "deprecated variant of mkCLambdaN"]
-
-(** @deprecated variant of mkCProdN *)
-val prod_constr_expr : constr_expr -> local_binder_expr list -> constr_expr
-[@@ocaml.deprecated "deprecated variant of mkCProdN"]
-
(** {6 Destructors}*)
-val coerce_reference_to_id : reference -> Id.t
+val coerce_reference_to_id : qualid -> Id.t
(** FIXME: nothing to do here *)
val coerce_to_id : constr_expr -> lident
@@ -116,11 +107,18 @@ val occur_var_constr_expr : Id.t -> constr_expr -> bool
val split_at_annot : local_binder_expr list -> lident option -> local_binder_expr list * local_binder_expr list
-val ntn_loc : ?loc:Loc.t -> constr_notation_substitution -> string -> (int * int) list
-val patntn_loc : ?loc:Loc.t -> cases_pattern_notation_substitution -> string -> (int * int) list
+val ntn_loc : ?loc:Loc.t -> constr_notation_substitution -> notation -> (int * int) list
+val patntn_loc : ?loc:Loc.t -> cases_pattern_notation_substitution -> notation -> (int * int) list
(** For cases pattern parsing errors *)
val error_invalid_pattern_notation : ?loc:Loc.t -> unit -> 'a
(** Placeholder for global option, should be moved to a parameter *)
val asymmetric_patterns : bool ref
+
+(** Local universe and constraint declarations. *)
+val interp_univ_decl : Environ.env -> universe_decl_expr ->
+ Evd.evar_map * UState.universe_decl
+
+val interp_univ_decl_opt : Environ.env -> universe_decl_expr option ->
+ Evd.evar_map * UState.universe_decl
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index af44921e..754fb3b9 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -14,10 +14,10 @@ open CErrors
open Util
open Names
open Nameops
-open Constr
open Termops
open Libnames
open Globnames
+open Namegen
open Impargs
open CAst
open Constrexpr
@@ -29,7 +29,6 @@ open Pattern
open Nametab
open Notation
open Detyping
-open Misctypes
open Decl_kinds
module NamedDecl = Context.Named.Declaration
@@ -102,8 +101,8 @@ let _show_inactive_notations () =
IRuleSet.iter
(function
| NotationRule (scopt, ntn) ->
- Feedback.msg_notice (str ntn ++ show_scope scopt)
- | SynDefRule kn -> Feedback.msg_notice (str (Names.KerName.to_string kn)))
+ Feedback.msg_notice (pr_notation ntn ++ show_scope scopt)
+ | SynDefRule kn -> Feedback.msg_notice (str (string_of_qualid (Nametab.shortest_qualid_of_syndef Id.Set.empty kn))))
!inactive_notations_table
let deactivate_notation nr =
@@ -114,14 +113,14 @@ let deactivate_notation nr =
| NotationRule (scopt, ntn) ->
match availability_of_notation (scopt, ntn) (scopt, []) with
| None -> user_err ~hdr:"Notation"
- (str ntn ++ spc () ++ str "does not exist"
+ (pr_notation ntn ++ spc () ++ str "does not exist"
++ (match scopt with
| None -> spc () ++ str "in the empty scope."
| Some _ -> show_scope scopt ++ str "."))
| Some _ ->
if IRuleSet.mem nr !inactive_notations_table then
Feedback.msg_warning
- (str "Notation" ++ spc () ++ str ntn ++ spc ()
+ (str "Notation" ++ spc () ++ pr_notation ntn ++ spc ()
++ str "is already inactive" ++ show_scope scopt ++ str ".")
else inactive_notations_table := IRuleSet.add nr !inactive_notations_table
@@ -132,12 +131,13 @@ let reactivate_notation nr =
with Not_found ->
match nr with
| NotationRule (scopt, ntn) ->
- Feedback.msg_warning (str "Notation" ++ spc () ++ str ntn ++ spc ()
+ Feedback.msg_warning (str "Notation" ++ spc () ++ pr_notation ntn ++ spc ()
++ str "is already active" ++ show_scope scopt ++
str ".")
| SynDefRule kn ->
+ let s = string_of_qualid (Nametab.shortest_qualid_of_syndef Id.Set.empty kn) in
Feedback.msg_warning
- (str "Notation" ++ spc () ++ str (Names.KerName.to_string kn)
+ (str "Notation" ++ spc () ++ str s
++ spc () ++ str "is already active.")
@@ -261,6 +261,14 @@ let insert_pat_alias ?loc p = function
| Anonymous -> p
| Name _ as na -> CAst.make ?loc @@ CPatAlias (p,(CAst.make ?loc na))
+let rec insert_coercion ?loc l c = match l with
+ | [] -> c
+ | ntn::l -> CAst.make ?loc @@ CNotation (ntn,([insert_coercion ?loc l c],[],[],[]))
+
+let rec insert_pat_coercion ?loc l c = match l with
+ | [] -> c
+ | ntn::l -> CAst.make ?loc @@ CPatNotation (ntn,([insert_pat_coercion ?loc l c],[]),[])
+
(**********************************************************************)
(* conversion of references *)
@@ -271,7 +279,7 @@ let extern_evar n l = CEvar (n,l)
may be inaccurate *)
let default_extern_reference ?loc vars r =
- make @@ Qualid (shortest_qualid_of_global vars r)
+ shortest_qualid_of_global ?loc vars r
let my_extern_reference = ref default_extern_reference
@@ -326,16 +334,16 @@ let is_zero s =
in aux 0
let make_notation_gen loc ntn mknot mkprim destprim l bl =
- match ntn,List.map destprim l with
+ match snd ntn,List.map destprim l with
(* Special case to avoid writing "- 3" for e.g. (Z.opp 3) *)
| "- _", [Some (Numeral (p,true))] when not (is_zero p) ->
assert (bl=[]);
- mknot (loc,ntn,([mknot (loc,"( _ )",l,[])]),[])
+ mknot (loc,ntn,([mknot (loc,(InConstrEntrySomeLevel,"( _ )"),l,[])]),[])
| _ ->
match decompose_notation_key ntn, l with
- | [Terminal "-"; Terminal x], [] when is_number x ->
+ | (InConstrEntrySomeLevel,[Terminal "-"; Terminal x]), [] when is_number x ->
mkprim (loc, Numeral (x,false))
- | [Terminal x], [] when is_number x ->
+ | (InConstrEntrySomeLevel,[Terminal x]), [] when is_number x ->
mkprim (loc, Numeral (x,true))
| _ -> mknot (loc,ntn,l,bl)
@@ -368,31 +376,39 @@ let pattern_printable_in_both_syntax (ind,_ as c) =
(List.for_all is_status_implicit params)&&(List.for_all (fun x -> not (is_status_implicit x)) args)
) impl_st
-let lift f c =
- let loc = c.CAst.loc in
- CAst.make ?loc (f ?loc (DAst.get c))
-
(* Better to use extern_glob_constr composed with injection/retraction ?? *)
-let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
+let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat =
try
if !Flags.in_debugger || !Flags.raw_print || !print_no_symbol then raise No_match;
let (na,sc,p) = uninterp_prim_token_cases_pattern pat in
+ match availability_of_entry_coercion custom InConstrEntrySomeLevel with
+ | None -> raise No_match
+ | Some coercion ->
match availability_of_prim_token p sc scopes with
| None -> raise No_match
| Some key ->
let loc = cases_pattern_loc pat in
- insert_pat_alias ?loc (insert_pat_delimiters ?loc (CAst.make ?loc @@ CPatPrim p) key) na
+ insert_pat_coercion ?loc coercion
+ (insert_pat_alias ?loc (insert_pat_delimiters ?loc (CAst.make ?loc @@ CPatPrim p) key) na)
with No_match ->
try
if !Flags.in_debugger || !Flags.raw_print || !print_no_symbol then raise No_match;
- extern_notation_pattern scopes vars pat
+ extern_notation_pattern allscopes vars pat
(uninterp_cases_pattern_notations pat)
with No_match ->
- lift (fun ?loc -> function
- | PatVar (Name id) -> CPatAtom (Some (make ?loc @@ Ident id))
- | PatVar (Anonymous) -> CPatAtom None
+ let loc = pat.CAst.loc in
+ match DAst.get pat with
+ | PatVar (Name id) when entry_has_ident custom -> CAst.make ?loc (CPatAtom (Some (qualid_of_ident ?loc id)))
+ | pat ->
+ match availability_of_entry_coercion custom InConstrEntrySomeLevel with
+ | None -> raise No_match
+ | Some coercion ->
+ let allscopes = (InConstrEntrySomeLevel,scopes) in
+ let pat = match pat with
+ | PatVar (Name id) -> CAst.make ?loc (CPatAtom (Some (qualid_of_ident ?loc id)))
+ | PatVar (Anonymous) -> CAst.make ?loc (CPatAtom None)
| PatCstr(cstrsp,args,na) ->
- let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
+ let args = List.map (extern_cases_pattern_in_scope allscopes vars) args in
let p =
try
if !Flags.raw_print then raise Exit;
@@ -425,26 +441,32 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
match drop_implicits_in_patt (ConstructRef cstrsp) 0 full_args with
| Some true_args -> CPatCstr (c, None, true_args)
| None -> CPatCstr (c, Some full_args, [])
- in (insert_pat_alias ?loc (CAst.make ?loc p) na).v
- ) pat
+ in
+ insert_pat_alias ?loc (CAst.make ?loc p) na
+ in
+ insert_pat_coercion coercion pat
+
and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
- (tmp_scope, scopes as allscopes) vars =
+ (custom, (tmp_scope, scopes) as allscopes) vars =
function
| NotationRule (sc,ntn) ->
begin
- match availability_of_notation (sc,ntn) allscopes with
+ match availability_of_entry_coercion custom (fst ntn) with
+ | None -> raise No_match
+ | Some coercion ->
+ match availability_of_notation (sc,ntn) (tmp_scope,scopes) with
(* Uninterpretation is not allowed in current context *)
| None -> raise No_match
(* Uninterpretation is allowed in current context *)
| Some (scopt,key) ->
let scopes' = Option.List.cons scopt scopes in
let l =
- List.map (fun (c,(scopt,scl)) ->
- extern_cases_pattern_in_scope (scopt,scl@scopes') vars c)
+ List.map (fun (c,(subentry,(scopt,scl))) ->
+ extern_cases_pattern_in_scope (subentry,(scopt,scl@scopes')) vars c)
subst in
let ll =
- List.map (fun (c,(scopt,scl)) ->
- let subscope = (scopt,scl@scopes') in
+ List.map (fun (c,(subentry,(scopt,scl))) ->
+ let subscope = (subentry,(scopt,scl@scopes')) in
List.map (extern_cases_pattern_in_scope subscope vars) c)
substlist in
let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in
@@ -454,14 +476,18 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
|Some true_args -> true_args
|None -> raise No_match
in
- insert_pat_delimiters ?loc
- (make_pat_notation ?loc ntn (l,ll) l2') key
+ insert_pat_coercion coercion
+ (insert_pat_delimiters ?loc
+ (make_pat_notation ?loc ntn (l,ll) l2') key)
end
| SynDefRule kn ->
- let qid = make ?loc @@ Qualid (shortest_qualid_of_syndef vars kn) in
+ match availability_of_entry_coercion custom InConstrEntrySomeLevel with
+ | None -> raise No_match
+ | Some coercion ->
+ let qid = shortest_qualid_of_syndef ?loc vars kn in
let l1 =
- List.rev_map (fun (c,(scopt,scl)) ->
- extern_cases_pattern_in_scope (scopt,scl@scopes) vars c)
+ List.rev_map (fun (c,(subentry,(scopt,scl))) ->
+ extern_cases_pattern_in_scope (subentry,(scopt,scl@scopes)) vars c)
subst in
let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in
let l2' = if !asymmetric_patterns then l2
@@ -471,8 +497,8 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
|None -> raise No_match
in
assert (List.is_empty substlist);
- mkPat ?loc qid (List.rev_append l1 l2')
-and extern_notation_pattern (tmp_scope,scopes as allscopes) vars t = function
+ insert_pat_coercion ?loc coercion (mkPat ?loc qid (List.rev_append l1 l2'))
+and extern_notation_pattern allscopes vars t = function
| [] -> raise No_match
| (keyrule,pat,n as _rule)::rules ->
try
@@ -485,7 +511,7 @@ and extern_notation_pattern (tmp_scope,scopes as allscopes) vars t = function
(match_notation_constr_cases_pattern t pat) allscopes vars keyrule in
insert_pat_alias ?loc p na
| PatVar Anonymous -> CAst.make ?loc @@ CPatAtom None
- | PatVar (Name id) -> CAst.make ?loc @@ CPatAtom (Some (make ?loc @@ Ident id))
+ | PatVar (Name id) -> CAst.make ?loc @@ CPatAtom (Some (qualid_of_ident ?loc id))
with
No_match -> extern_notation_pattern allscopes vars t rules
@@ -499,35 +525,27 @@ let rec extern_notation_ind_pattern allscopes vars ind args = function
with
No_match -> extern_notation_ind_pattern allscopes vars ind args rules
-let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args =
+let extern_ind_pattern_in_scope (custom,scopes as allscopes) vars ind args =
(* pboutill: There are letins in pat which is incompatible with notations and
not explicit application. *)
if !Flags.in_debugger||Inductiveops.inductive_has_local_defs ind then
let c = extern_reference vars (IndRef ind) in
- let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
+ let args = List.map (extern_cases_pattern_in_scope allscopes vars) args in
CAst.make @@ CPatCstr (c, Some (add_patt_for_params ind args), [])
else
try
if !Flags.raw_print || !print_no_symbol then raise No_match;
- let (sc,p) = uninterp_prim_token_ind_pattern ind args in
- match availability_of_prim_token p sc scopes with
- | None -> raise No_match
- | Some key ->
- insert_pat_delimiters (CAst.make @@ CPatPrim p) key
- with No_match ->
- try
- if !Flags.raw_print || !print_no_symbol then raise No_match;
- extern_notation_ind_pattern scopes vars ind args
+ extern_notation_ind_pattern allscopes vars ind args
(uninterp_ind_pattern_notations ind)
with No_match ->
let c = extern_reference vars (IndRef ind) in
- let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
+ let args = List.map (extern_cases_pattern_in_scope allscopes vars) args in
match drop_implicits_in_patt (IndRef ind) 0 args with
|Some true_args -> CAst.make @@ CPatCstr (c, None, true_args)
|None -> CAst.make @@ CPatCstr (c, Some args, [])
let extern_cases_pattern vars p =
- extern_cases_pattern_in_scope (None,[]) vars p
+ extern_cases_pattern_in_scope (InConstrEntrySomeLevel,(None,[])) vars p
(**********************************************************************)
(* Externalising applications *)
@@ -641,12 +659,12 @@ let extern_app inctx impl (cf,f) us args =
else
explicitize inctx impl (cf, CAst.make @@ CRef (f,us)) args
-let rec fill_arg_scopes args subscopes scopes = match args, subscopes with
+let rec fill_arg_scopes args subscopes (entry,(_,scopes) as all) = match args, subscopes with
| [], _ -> []
| a :: args, scopt :: subscopes ->
- (a, (scopt, scopes)) :: fill_arg_scopes args subscopes scopes
+ (a, (entry, (scopt, scopes))) :: fill_arg_scopes args subscopes all
| a :: args, [] ->
- (a, (None, scopes)) :: fill_arg_scopes args [] scopes
+ (a, (entry, (None, scopes))) :: fill_arg_scopes args [] all
let extern_args extern env args =
let map (arg, argscopes) = lazy (extern argscopes env arg) in
@@ -698,12 +716,15 @@ let rec flatten_application c = match DAst.get c with
(* mapping glob_constr to numerals (in presence of coercions, choose the *)
(* one with no delimiter if possible) *)
-let extern_possible_prim_token scopes r =
+let extern_possible_prim_token (custom,scopes) r =
try
let (sc,n) = uninterp_prim_token r in
+ match availability_of_entry_coercion custom InConstrEntrySomeLevel with
+ | None -> raise No_match
+ | Some coercion ->
match availability_of_prim_token n sc scopes with
| None -> None
- | Some key -> Some (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key)
+ | Some key -> Some (insert_coercion coercion (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key))
with No_match ->
None
@@ -721,7 +742,7 @@ let extended_glob_local_binder_of_decl loc = function
| (p,bk,None,t) -> GLocalAssum (p,bk,t)
| (p,bk,Some x, t) ->
match DAst.get t with
- | GHole (_, Misctypes.IntroAnonymous, None) -> GLocalDef (p,bk,x,None)
+ | GHole (_, IntroAnonymous, None) -> GLocalDef (p,bk,x,None)
| _ -> GLocalDef (p,bk,x,Some t)
let extended_glob_local_binder_of_decl ?loc u = DAst.make ?loc (extended_glob_local_binder_of_decl loc u)
@@ -738,7 +759,13 @@ let extern_glob_sort = function
let extern_universes = function
| Some _ as l when !print_universes -> l
| _ -> None
-
+
+let extern_ref vars ref us =
+ extern_global (select_stronger_impargs (implicits_of_global ref))
+ (extern_reference vars ref) (extern_universes us)
+
+let extern_var ?loc id = CRef (qualid_of_ident ?loc id,None)
+
let rec extern inctx scopes vars r =
let r' = remove_coercions inctx r in
try
@@ -749,20 +776,35 @@ let rec extern inctx scopes vars r =
let r'' = flatten_application r' in
if !Flags.raw_print || !print_no_symbol then raise No_match;
extern_notation scopes vars r'' (uninterp_notations r'')
- with No_match -> lift (fun ?loc -> function
- | GRef (ref,us) ->
- extern_global (select_stronger_impargs (implicits_of_global ref))
- (extern_reference vars ref) (extern_universes us)
+ with No_match ->
+ let loc = r'.CAst.loc in
+ match DAst.get r' with
+ | GRef (ref,us) when entry_has_global (fst scopes) -> CAst.make ?loc (extern_ref vars ref us)
+
+ | GVar id when entry_has_ident (fst scopes) -> CAst.make ?loc (extern_var ?loc id)
+
+ | c ->
- | GVar id -> CRef (make ?loc @@ Ident id,None)
+ match availability_of_entry_coercion (fst scopes) InConstrEntrySomeLevel with
+ | None -> raise No_match
+ | Some coercion ->
- | GEvar (n,[]) when !print_meta_as_hole -> CHole (None, Misctypes.IntroAnonymous, None)
+ let scopes = (InConstrEntrySomeLevel, snd scopes) in
+ let c = match c with
+
+ (* The remaining cases are only for the constr entry *)
+
+ | GRef (ref,us) -> extern_ref vars ref us
+
+ | GVar id -> extern_var ?loc id
+
+ | GEvar (n,[]) when !print_meta_as_hole -> CHole (None, IntroAnonymous, None)
| GEvar (n,l) ->
extern_evar n (List.map (on_snd (extern false scopes vars)) l)
| GPatVar kind ->
- if !print_meta_as_hole then CHole (None, Misctypes.IntroAnonymous, None) else
+ if !print_meta_as_hole then CHole (None, IntroAnonymous, None) else
(match kind with
| Evar_kinds.SecondOrderPatVar n -> CPatVar n
| Evar_kinds.FirstOrderPatVar n -> CEvar (n,[]))
@@ -771,7 +813,7 @@ let rec extern inctx scopes vars r =
(match DAst.get f with
| GRef (ref,us) ->
let subscopes = find_arguments_scope ref in
- let args = fill_arg_scopes args subscopes (snd scopes) in
+ let args = fill_arg_scopes args subscopes scopes in
begin
try
if !Flags.raw_print then raise Exit;
@@ -918,18 +960,19 @@ let rec extern inctx scopes vars r =
| GCast (c, c') ->
CCast (sub_extern true scopes vars c,
- Miscops.map_cast_type (extern_typ scopes vars) c')
- ) r'
+ map_cast_type (extern_typ scopes vars) c')
+
+ in insert_coercion coercion (CAst.make ?loc c)
-and extern_typ (_,scopes) =
- extern true (Notation.current_type_scope_name (),scopes)
+and extern_typ (subentry,(_,scopes)) =
+ extern true (subentry,(Notation.current_type_scope_name (),scopes))
-and sub_extern inctx (_,scopes) = extern inctx (None,scopes)
+and sub_extern inctx (subentry,(_,scopes)) = extern inctx (subentry,(None,scopes))
and factorize_prod scopes vars na bk aty c =
let store, get = set_temporary_memory () in
match na, DAst.get c with
- | Name id, GCases (LetPatternStyle, None, [(e,(Anonymous,None))],(_::_ as eqns))
+ | Name id, GCases (Constr.LetPatternStyle, None, [(e,(Anonymous,None))],(_::_ as eqns))
when is_gvar id e && List.length (store (factorize_eqns eqns)) = 1 ->
(match get () with
| [{CAst.v=(ids,disj_of_patl,b)}] ->
@@ -957,7 +1000,7 @@ and factorize_prod scopes vars na bk aty c =
and factorize_lambda inctx scopes vars na bk aty c =
let store, get = set_temporary_memory () in
match na, DAst.get c with
- | Name id, GCases (LetPatternStyle, None, [(e,(Anonymous,None))],(_::_ as eqns))
+ | Name id, GCases (Constr.LetPatternStyle, None, [(e,(Anonymous,None))],(_::_ as eqns))
when is_gvar id e && List.length (store (factorize_eqns eqns)) = 1 ->
(match get () with
| [{CAst.v=(ids,disj_of_patl,b)}] ->
@@ -1017,7 +1060,7 @@ and extern_eqn inctx scopes vars {CAst.loc;v=(ids,pll,c)} =
let pll = List.map (List.map (extern_cases_pattern_in_scope scopes vars)) pll in
make ?loc (pll,extern inctx scopes vars c)
-and extern_notation (tmp_scope,scopes as allscopes) vars t = function
+and extern_notation (custom,scopes as allscopes) vars t = function
| [] -> raise No_match
| (keyrule,pat,n as _rule)::rules ->
let loc = Glob_ops.loc_of_glob_constr t in
@@ -1064,40 +1107,46 @@ and extern_notation (tmp_scope,scopes as allscopes) vars t = function
let e =
match keyrule with
| NotationRule (sc,ntn) ->
- (match availability_of_notation (sc,ntn) allscopes with
+ (match availability_of_entry_coercion custom (fst ntn) with
+ | None -> raise No_match
+ | Some coercion ->
+ match availability_of_notation (sc,ntn) scopes with
(* Uninterpretation is not allowed in current context *)
| None -> raise No_match
(* Uninterpretation is allowed in current context *)
| Some (scopt,key) ->
- let scopes' = Option.List.cons scopt scopes in
+ let scopes' = Option.List.cons scopt (snd scopes) in
let l =
- List.map (fun (c,(scopt,scl)) ->
+ List.map (fun (c,(subentry,(scopt,scl))) ->
extern (* assuming no overloading: *) true
- (scopt,scl@scopes') vars c)
+ (subentry,(scopt,scl@scopes')) vars c)
terms in
let ll =
- List.map (fun (c,(scopt,scl)) ->
- List.map (extern true (scopt,scl@scopes') vars) c)
+ List.map (fun (c,(subentry,(scopt,scl))) ->
+ List.map (extern true (subentry,(scopt,scl@scopes')) vars) c)
termlists in
let bl =
- List.map (fun (bl,(scopt,scl)) ->
- mkCPatOr (List.map (extern_cases_pattern_in_scope (scopt,scl@scopes') vars) bl))
+ List.map (fun (bl,(subentry,(scopt,scl))) ->
+ mkCPatOr (List.map (extern_cases_pattern_in_scope (subentry,(scopt,scl@scopes')) vars) bl))
binders in
let bll =
- List.map (fun (bl,(scopt,scl)) ->
- pi3 (extern_local_binder (scopt,scl@scopes') vars bl))
+ List.map (fun (bl,(subentry,(scopt,scl))) ->
+ pi3 (extern_local_binder (subentry,(scopt,scl@scopes')) vars bl))
binderlists in
- insert_delimiters (make_notation loc ntn (l,ll,bl,bll)) key)
+ insert_coercion coercion (insert_delimiters (make_notation loc ntn (l,ll,bl,bll)) key))
| SynDefRule kn ->
+ match availability_of_entry_coercion custom InConstrEntrySomeLevel with
+ | None -> raise No_match
+ | Some coercion ->
let l =
- List.map (fun (c,(scopt,scl)) ->
- extern true (scopt,scl@scopes) vars c, None)
+ List.map (fun (c,(subentry,(scopt,scl))) ->
+ extern true (subentry,(scopt,scl@snd scopes)) vars c, None)
terms in
- let a = CRef (make ?loc @@ Qualid (shortest_qualid_of_syndef vars kn),None) in
- CAst.make ?loc @@ if List.is_empty l then a else CApp ((None, CAst.make a),l) in
+ let a = CRef (shortest_qualid_of_syndef ?loc vars kn,None) in
+ insert_coercion coercion (CAst.make ?loc @@ if List.is_empty l then a else CApp ((None, CAst.make a),l)) in
if List.is_empty args then e
else
- let args = fill_arg_scopes args argsscopes scopes in
+ let args = fill_arg_scopes args argsscopes allscopes in
let args = extern_args (extern true) vars args in
CAst.make ?loc @@ explicitize false argsimpls (None,e) args
with
@@ -1111,10 +1160,10 @@ and extern_recursion_order scopes vars = function
let extern_glob_constr vars c =
- extern false (None,[]) vars c
+ extern false (InConstrEntrySomeLevel,(None,[])) vars c
let extern_glob_type vars c =
- extern_typ (None,[]) vars c
+ extern_typ (InConstrEntrySomeLevel,(None,[])) vars c
(******************************************************************)
(* Main translation function from constr -> constr_expr *)
@@ -1130,7 +1179,7 @@ let extern_constr_gen lax goal_concl_style scopt env sigma t =
let avoid = if goal_concl_style then vars_of_env env else Id.Set.empty in
let r = Detyping.detype Detyping.Later ~lax:lax goal_concl_style avoid env sigma t in
let vars = vars_of_env env in
- extern false (scopt,[]) vars r
+ extern false (InConstrEntrySomeLevel,(scopt,[])) vars r
let extern_constr_in_scope goal_concl_style scope env sigma t =
extern_constr_gen false goal_concl_style (Some scope) env sigma t
@@ -1151,14 +1200,14 @@ let extern_closed_glob ?lax goal_concl_style env sigma t =
Detyping.detype_closed_glob ?lax goal_concl_style avoid env sigma t
in
let vars = vars_of_env env in
- extern false (None,[]) vars r
+ extern false (InConstrEntrySomeLevel,(None,[])) vars r
(******************************************************************)
(* Main translation function from pattern -> constr_expr *)
let any_any_branch =
(* | _ => _ *)
- CAst.make ([],[DAst.make @@ PatVar Anonymous], DAst.make @@ GHole (Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None))
+ CAst.make ([],[DAst.make @@ PatVar Anonymous], DAst.make @@ GHole (Evar_kinds.InternalHole,IntroAnonymous,None))
let compute_displayed_name_in_pattern sigma avoid na c =
let open Namegen in
@@ -1182,7 +1231,7 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
anomaly ~label:"glob_constr_of_pattern" (Pp.str "index to an anonymous variable.")
with Not_found -> Id.of_string ("_UNBOUND_REL_"^(string_of_int n)) in
GVar id
- | PMeta None -> GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous,None)
+ | PMeta None -> GHole (Evar_kinds.InternalHole, IntroAnonymous,None)
| PMeta (Some n) -> GPatVar (Evar_kinds.FirstOrderPatVar n)
| PProj (p,c) -> GApp (DAst.make @@ GRef (ConstRef (Projection.constant p),None),
[glob_of_pat avoid env sigma c])
@@ -1207,7 +1256,7 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
| PIf (c,b1,b2) ->
GIf (glob_of_pat avoid env sigma c, (Anonymous,None),
glob_of_pat avoid env sigma b1, glob_of_pat avoid env sigma b2)
- | PCase ({cip_style=LetStyle; cip_ind_tags=None},PMeta None,tm,[(0,n,b)]) ->
+ | PCase ({cip_style=Constr.LetStyle; cip_ind_tags=None},PMeta None,tm,[(0,n,b)]) ->
let nal,b = it_destRLambda_or_LetIn_names n (glob_of_pat avoid env sigma b) in
GLetTuple (nal,(Anonymous,None),glob_of_pat avoid env sigma tm,b)
| PCase (info,p,tm,bl) ->
@@ -1226,16 +1275,44 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
return_type_of_predicate ind nargs (glob_of_pat avoid env sigma p)
| _ -> anomaly (Pp.str "PCase with non-trivial predicate but unknown inductive.")
in
- GCases (RegularStyle,rtn,[glob_of_pat avoid env sigma tm,indnames],mat)
- | PFix f -> DAst.get (Detyping.detype_names false avoid env (Global.env()) sigma (EConstr.of_constr (mkFix f))) (** FIXME bad env *)
- | PCoFix c -> DAst.get (Detyping.detype_names false avoid env (Global.env()) sigma (EConstr.of_constr (mkCoFix c)))
+ GCases (Constr.RegularStyle,rtn,[glob_of_pat avoid env sigma tm,indnames],mat)
+ | PFix ((ln,i),(lna,tl,bl)) ->
+ let def_avoid, def_env, lfi =
+ Array.fold_left
+ (fun (avoid, env, l) na ->
+ let id = Namegen.next_name_away na avoid in
+ (Id.Set.add id avoid, Name id :: env, id::l))
+ (avoid, env, []) lna in
+ let n = Array.length tl in
+ let v = Array.map3
+ (fun c t i -> Detyping.share_pattern_names glob_of_pat (i+1) [] def_avoid def_env sigma c (Patternops.lift_pattern n t))
+ bl tl ln in
+ GRec(GFix (Array.map (fun i -> Some i, GStructRec) ln,i),Array.of_list (List.rev lfi),
+ Array.map (fun (bl,_,_) -> bl) v,
+ Array.map (fun (_,_,ty) -> ty) v,
+ Array.map (fun (_,bd,_) -> bd) v)
+ | PCoFix (ln,(lna,tl,bl)) ->
+ let def_avoid, def_env, lfi =
+ Array.fold_left
+ (fun (avoid, env, l) na ->
+ let id = Namegen.next_name_away na avoid in
+ (Id.Set.add id avoid, Name id :: env, id::l))
+ (avoid, env, []) lna in
+ let ntys = Array.length tl in
+ let v = Array.map2
+ (fun c t -> share_pattern_names glob_of_pat 0 [] def_avoid def_env sigma c (Patternops.lift_pattern ntys t))
+ bl tl in
+ GRec(GCoFix ln,Array.of_list (List.rev lfi),
+ Array.map (fun (bl,_,_) -> bl) v,
+ Array.map (fun (_,_,ty) -> ty) v,
+ Array.map (fun (_,bd,_) -> bd) v)
| PSort s -> GSort s
let extern_constr_pattern env sigma pat =
- extern true (None,[]) Id.Set.empty (glob_of_pat Id.Set.empty env sigma pat)
+ extern true (InConstrEntrySomeLevel,(None,[])) Id.Set.empty (glob_of_pat Id.Set.empty env sigma pat)
let extern_rel_context where env sigma sign =
let a = detype_rel_context Detyping.Later where Id.Set.empty (names_of_rel_context env,env) sigma sign in
let vars = vars_of_env env in
let a = List.map (extended_glob_local_binder_of_decl) a in
- pi3 (extern_local_binder (None,[]) vars a)
+ pi3 (extern_local_binder (InConstrEntrySomeLevel,(None,[])) vars a)
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index 8ab70283..f09b316c 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -13,13 +13,11 @@ open Termops
open EConstr
open Environ
open Libnames
-open Globnames
open Glob_term
open Pattern
open Constrexpr
open Notation_term
open Notation
-open Misctypes
open Ltac_pretype
(** Translation of pattern, cases pattern, glob_constr and term into syntax
@@ -40,7 +38,7 @@ val extern_closed_glob : ?lax:bool -> bool -> env -> Evd.evar_map -> closed_glob
val extern_constr : ?lax:bool -> bool -> env -> Evd.evar_map -> constr -> constr_expr
val extern_constr_in_scope : bool -> scope_name -> env -> Evd.evar_map -> constr -> constr_expr
-val extern_reference : ?loc:Loc.t -> Id.Set.t -> global_reference -> reference
+val extern_reference : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid
val extern_type : bool -> env -> Evd.evar_map -> types -> constr_expr
val extern_sort : Evd.evar_map -> Sorts.t -> glob_sort
val extern_rel_context : constr option -> env -> Evd.evar_map ->
@@ -58,9 +56,9 @@ val print_projections : bool ref
(** Customization of the global_reference printer *)
val set_extern_reference :
- (?loc:Loc.t -> Id.Set.t -> global_reference -> reference) -> unit
+ (?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid) -> unit
val get_extern_reference :
- unit -> (?loc:Loc.t -> Id.Set.t -> global_reference -> reference)
+ unit -> (?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid)
(** WARNING: The following functions are evil due to
side-effects. Think of the following case as used in the printer:
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 83ace93c..d02f5941 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -15,6 +15,7 @@ open CAst
open Names
open Nameops
open Namegen
+open Constr
open Libnames
open Globnames
open Impargs
@@ -95,8 +96,8 @@ let is_global id =
with Not_found ->
false
-let global_reference_of_reference ref =
- locate_reference (qualid_of_reference ref).CAst.v
+let global_reference_of_reference qid =
+ locate_reference qid
let global_reference id =
locate_reference (qualid_of_ident id)
@@ -116,7 +117,7 @@ let global_reference_in_absolute_module dir id =
type internalization_error =
| VariableCapture of Id.t * Id.t
| IllegalMetavariable
- | NotAConstructor of reference
+ | NotAConstructor of qualid
| UnboundFixName of bool * Id.t
| NonLinearPattern of Id.t
| BadPatternsNumber of int * int
@@ -130,8 +131,8 @@ let explain_variable_capture id id' =
let explain_illegal_metavariable =
str "Metavariables allowed only in patterns"
-let explain_not_a_constructor ref =
- str "Unknown constructor: " ++ pr_reference ref
+let explain_not_a_constructor qid =
+ str "Unknown constructor: " ++ pr_qualid qid
let explain_unbound_fix_name is_cofix id =
str "The name" ++ spc () ++ Id.print id ++
@@ -217,30 +218,36 @@ let expand_notation_string ntn n =
(* This contracts the special case of "{ _ }" for sumbool, sumor notations *)
(* Remark: expansion of squash at definition is done in metasyntax.ml *)
let contract_curly_brackets ntn (l,ll,bl,bll) =
+ match ntn with
+ | InCustomEntryLevel _,_ -> ntn,(l,ll,bl,bll)
+ | InConstrEntrySomeLevel, ntn ->
let ntn' = ref ntn in
let rec contract_squash n = function
| [] -> []
- | { CAst.v = CNotation ("{ _ }",([a],[],[],[])) } :: l ->
+ | { CAst.v = CNotation ((InConstrEntrySomeLevel,"{ _ }"),([a],[],[],[])) } :: l ->
ntn' := expand_notation_string !ntn' n;
contract_squash n (a::l)
| a :: l ->
a::contract_squash (n+1) l in
let l = contract_squash 0 l in
(* side effect; don't inline *)
- !ntn',(l,ll,bl,bll)
+ (InConstrEntrySomeLevel,!ntn'),(l,ll,bl,bll)
let contract_curly_brackets_pat ntn (l,ll) =
+ match ntn with
+ | InCustomEntryLevel _,_ -> ntn,(l,ll)
+ | InConstrEntrySomeLevel, ntn ->
let ntn' = ref ntn in
let rec contract_squash n = function
| [] -> []
- | { CAst.v = CPatNotation ("{ _ }",([a],[]),[]) } :: l ->
+ | { CAst.v = CPatNotation ((InConstrEntrySomeLevel,"{ _ }"),([a],[]),[]) } :: l ->
ntn' := expand_notation_string !ntn' n;
contract_squash n (a::l)
| a :: l ->
a::contract_squash (n+1) l in
let l = contract_squash 0 l in
(* side effect; don't inline *)
- !ntn',(l,ll)
+ (InConstrEntrySomeLevel,!ntn'),(l,ll)
type intern_env = {
ids: Names.Id.Set.t;
@@ -393,7 +400,7 @@ let intern_generalized_binder ?(global_level=false) intern_type ntnvars
env fvs in
let bl = List.map
CAst.(map (fun id ->
- (Name id, b, DAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None))))
+ (Name id, b, DAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None))))
fvs
in
let na = match na with
@@ -403,7 +410,8 @@ let intern_generalized_binder ?(global_level=false) intern_type ntnvars
let name =
let id =
match ty with
- | { v = CApp ((_, { v = CRef ({v=Ident id},_) } ), _) } -> id
+ | { v = CApp ((_, { v = CRef (qid,_) } ), _) } when qualid_is_ident qid ->
+ qualid_basename qid
| _ -> default_non_dependent_ident
in Implicit_quantifiers.make_fresh ids' (Global.env ()) id
in Name name
@@ -430,7 +438,7 @@ let glob_local_binder_of_extended = DAst.with_loc_val (fun ?loc -> function
| GLocalAssum (na,bk,t) -> (na,bk,None,t)
| GLocalDef (na,bk,c,Some t) -> (na,bk,Some c,t)
| GLocalDef (na,bk,c,None) ->
- let t = DAst.make ?loc @@ GHole(Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None) in
+ let t = DAst.make ?loc @@ GHole(Evar_kinds.BinderType na,IntroAnonymous,None) in
(na,bk,Some c,t)
| GLocalPattern (_,_,_,_) ->
Loc.raise ?loc (Stream.Error "pattern with quote not allowed here")
@@ -471,7 +479,7 @@ let intern_local_binder_aux ?(global_level=false) intern ntnvars (env,bl) = func
let tyc =
match ty with
| Some ty -> ty
- | None -> CAst.make ?loc @@ CHole(None,Misctypes.IntroAnonymous,None)
+ | None -> CAst.make ?loc @@ CHole(None,IntroAnonymous,None)
in
let env, ((disjpat,il),id),na = intern_cases_pattern_as_binder ?loc ntnvars env p in
let bk = Default Explicit in
@@ -501,11 +509,11 @@ let intern_generalization intern env ntnvars loc bk ak c =
if pi then
(fun {loc=loc';v=id} acc ->
DAst.make ?loc:(Loc.merge_opt loc' loc) @@
- GProd (Name id, bk, DAst.make ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc))
+ GProd (Name id, bk, DAst.make ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None), acc))
else
(fun {loc=loc';v=id} acc ->
DAst.make ?loc:(Loc.merge_opt loc' loc) @@
- GLambda (Name id, bk, DAst.make ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc))
+ GLambda (Name id, bk, DAst.make ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None), acc))
in
List.fold_right (fun ({loc;v=id} as lid) (env, acc) ->
let env' = push_name_env ntnvars (Variable,[],[],[]) env CAst.(make @@ Name id) in
@@ -525,7 +533,7 @@ let rec expand_binders ?loc mk bl c =
let tm = DAst.make ?loc (GVar id) in
(* Distribute the disjunctive patterns over the shared right-hand side *)
let eqnl = List.map (fun pat -> CAst.make ?loc (ids,[pat],c)) disjpat in
- let c = DAst.make ?loc @@ GCases (Misctypes.LetPatternStyle, None, [tm,(Anonymous,None)], eqnl) in
+ let c = DAst.make ?loc @@ GCases (LetPatternStyle, None, [tm,(Anonymous,None)], eqnl) in
expand_binders ?loc mk bl (mk ?loc (Name id,Explicit,ty) c)
(**********************************************************************)
@@ -550,12 +558,13 @@ let find_fresh_name renaming (terms,termlists,binders,binderlists) avoid id =
let is_var store pat =
match DAst.get pat with
- | PatVar na -> store na; true
+ | PatVar na -> ignore(store na); true
| _ -> false
let out_var pat =
match pat.v with
- | CPatAtom (Some ({v=Ident id})) -> Name id
+ | CPatAtom (Some qid) when qualid_is_ident qid ->
+ Name (qualid_basename qid)
| CPatAtom None -> Anonymous
| _ -> assert false
@@ -563,7 +572,7 @@ let term_of_name = function
| Name id -> DAst.make (GVar id)
| Anonymous ->
let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in
- DAst.make (GHole (Evar_kinds.QuestionMark (st,Anonymous), Misctypes.IntroAnonymous, None))
+ DAst.make (GHole (Evar_kinds.QuestionMark { Evar_kinds.default_question_mark with Evar_kinds.qm_obligation=st }, IntroAnonymous, None))
let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renaming,env) = function
| Anonymous -> (renaming,env), None, Anonymous
@@ -605,7 +614,7 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam
(renaming',env), None, Name id'
type binder_action =
-| AddLetIn of Misctypes.lname * constr_expr * constr_expr option
+| AddLetIn of lname * constr_expr * constr_expr option
| AddTermIter of (constr_expr * subscopes) Names.Id.Map.t
| AddPreBinderIter of Id.t * local_binder_expr (* A binder to be internalized *)
| AddBinderIter of Id.t * extended_glob_local_binder (* A binder already internalized - used for generalized binders *)
@@ -621,18 +630,18 @@ let error_cannot_coerce_disjunctive_pattern_term ?loc () =
let terms_of_binders bl =
let rec term_of_pat pt = dmap_with_loc (fun ?loc -> function
- | PatVar (Name id) -> CRef (make @@ Ident id, None)
+ | PatVar (Name id) -> CRef (qualid_of_ident id, None)
| PatVar (Anonymous) -> error_cannot_coerce_wildcard_term ?loc ()
| PatCstr (c,l,_) ->
- let r = make ?loc @@ Qualid (qualid_of_path (path_of_global (ConstructRef c))) in
- let hole = CAst.make ?loc @@ CHole (None,Misctypes.IntroAnonymous,None) in
+ let qid = qualid_of_path ?loc (path_of_global (ConstructRef c)) in
+ let hole = CAst.make ?loc @@ CHole (None,IntroAnonymous,None) in
let params = List.make (Inductiveops.inductive_nparams (fst c)) hole in
- CAppExpl ((None,r,None),params @ List.map term_of_pat l)) pt in
+ CAppExpl ((None,qid,None),params @ List.map term_of_pat l)) pt in
let rec extract_variables l = match l with
| bnd :: l ->
let loc = bnd.loc in
begin match DAst.get bnd with
- | GLocalAssum (Name id,_,_) -> (CAst.make ?loc @@ CRef (make ?loc @@ Ident id, None)) :: extract_variables l
+ | GLocalAssum (Name id,_,_) -> (CAst.make ?loc @@ CRef (qualid_of_ident ?loc id, None)) :: extract_variables l
| GLocalDef (Name id,_,_,_) -> extract_variables l
| GLocalDef (Anonymous,_,_,_)
| GLocalAssum (Anonymous,_,_) -> user_err Pp.(str "Cannot turn \"_\" into a term.")
@@ -707,10 +716,12 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
let arg = match arg with
| None -> None
| Some arg ->
- let mk_env (c, (tmp_scope, subscopes)) =
+ let mk_env id (c, (tmp_scope, subscopes)) map =
let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in
- let gc = intern nenv c in
- (gc, Some c)
+ try
+ let gc = intern nenv c in
+ Id.Map.add id (gc, Some c) map
+ with GlobalizationError _ -> map
in
let mk_env' (c, (onlyident,(tmp_scope,subscopes))) =
let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in
@@ -722,7 +733,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
| [pat] -> (glob_constr_of_cases_pattern pat, None)
| _ -> error_cannot_coerce_disjunctive_pattern_term ?loc:c.loc ()
in
- let terms = Id.Map.map mk_env terms in
+ let terms = Id.Map.fold mk_env terms Id.Map.empty in
let binders = Id.Map.map mk_env' binders in
let bindings = Id.Map.fold Id.Map.add terms binders in
Some (Genintern.generic_substitute_notation bindings arg)
@@ -805,7 +816,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
distinction *)
let cases_pattern_of_name {loc;v=na} =
- let atom = match na with Name id -> Some (make ?loc @@ Ident id) | Anonymous -> None in
+ let atom = match na with Name id -> Some (qualid_of_ident ?loc id) | Anonymous -> None in
CAst.make ?loc (CPatAtom atom)
let split_by_type ids subst =
@@ -814,16 +825,16 @@ let split_by_type ids subst =
| [] -> assert false
| a::l -> l, Id.Map.add id (a,scl) s in
let (terms,termlists,binders,binderlists),subst =
- List.fold_left (fun ((terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')) (id,(scl,typ)) ->
+ List.fold_left (fun ((terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')) (id,((_,scl),typ)) ->
match typ with
| NtnTypeConstr ->
let terms,terms' = bind id scl terms terms' in
(terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')
- | NtnTypeBinder NtnBinderParsedAsConstr (Extend.AsIdentOrPattern | Extend.AsStrictPattern) ->
+ | NtnTypeBinder NtnBinderParsedAsConstr (AsIdentOrPattern | AsStrictPattern) ->
let a,terms = match terms with a::terms -> a,terms | _ -> assert false in
let binders' = Id.Map.add id (coerce_to_cases_pattern_expr a,(false,scl)) binders' in
(terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')
- | NtnTypeBinder NtnBinderParsedAsConstr Extend.AsIdent ->
+ | NtnTypeBinder NtnBinderParsedAsConstr AsIdent ->
let a,terms = match terms with a::terms -> a,terms | _ -> assert false in
let binders' = Id.Map.add id (cases_pattern_of_name (coerce_to_name a),(true,scl)) binders' in
(terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')
@@ -842,10 +853,10 @@ let split_by_type ids subst =
subst
let split_by_type_pat ?loc ids subst =
- let bind id scl l s =
+ let bind id (_,scopes) l s =
match l with
| [] -> assert false
- | a::l -> l, Id.Map.add id (a,scl) s in
+ | a::l -> l, Id.Map.add id (a,scopes) s in
let (terms,termlists),subst =
List.fold_left (fun ((terms,termlists),(terms',termlists')) (id,(scl,typ)) ->
match typ with
@@ -861,7 +872,7 @@ let split_by_type_pat ?loc ids subst =
subst
let make_subst ids l =
- let fold accu (id, scl) a = Id.Map.add id (a, scl) accu in
+ let fold accu (id, scopes) a = Id.Map.add id (a, scopes) accu in
List.fold_left2 fold Id.Map.empty ids l
let intern_notation intern env ntnvars loc ntn fullargs =
@@ -902,7 +913,7 @@ let intern_var env (ltacvars,ntnvars) namedctx loc id us =
try
let ty,expl_impls,impls,argsc = Id.Map.find id env.impls in
let expl_impls = List.map
- (fun id -> CAst.make ?loc @@ CRef (make ?loc @@ Ident id,None), Some (make ?loc @@ ExplByName id)) expl_impls in
+ (fun id -> CAst.make ?loc @@ CRef (qualid_of_ident ?loc id,None), Some (make ?loc @@ ExplByName id)) expl_impls in
let tys = string_of_ty ty in
Dumpglob.dump_reference ?loc "<>" (Id.to_string id) tys;
gvar (loc,id) us, make_implicits_list impls, argsc, expl_impls
@@ -969,28 +980,27 @@ let dump_extended_global loc = function
| TrueGlobal ref -> (*feedback_global loc ref;*) Dumpglob.add_glob ?loc ref
| SynDef sp -> Dumpglob.add_glob_kn ?loc sp
-let intern_extended_global_of_qualid {loc;v=qid} =
- let r = Nametab.locate_extended qid in dump_extended_global loc r; r
+let intern_extended_global_of_qualid qid =
+ let r = Nametab.locate_extended qid in dump_extended_global qid.CAst.loc r; r
-let intern_reference ref =
- let qid = qualid_of_reference ref in
+let intern_reference qid =
let r =
try intern_extended_global_of_qualid qid
with Not_found -> error_global_not_found qid
in
Smartlocate.global_of_extended_global r
-let sort_info_of_level_info (info: Misctypes.level_info) : (Libnames.reference * int) option =
+let sort_info_of_level_info (info: level_info) : (Libnames.qualid * int) option =
match info with
- | Misctypes.UAnonymous -> None
- | Misctypes.UUnknown -> None
- | Misctypes.UNamed id -> Some (id, 0)
+ | UAnonymous -> None
+ | UUnknown -> None
+ | UNamed id -> Some (id, 0)
-let glob_sort_of_level (level: Misctypes.glob_level) : Misctypes.glob_sort =
+let glob_sort_of_level (level: glob_level) : glob_sort =
match level with
- | Misctypes.GProp -> Misctypes.GProp
- | Misctypes.GSet -> Misctypes.GSet
- | Misctypes.GType info -> Misctypes.GType [sort_info_of_level_info info]
+ | GProp -> GProp
+ | GSet -> GSet
+ | GType info -> GType [sort_info_of_level_info info]
(* Is it a global reference or a syntactic definition? *)
let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args =
@@ -1013,7 +1023,7 @@ let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args =
let c = instantiate_notation_constr loc intern intern_cases_pattern_as_binder ntnvars subst infos c in
let loc = c.loc in
let err () =
- user_err ?loc (str "Notation " ++ pr_qualid qid.v
+ 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
@@ -1027,37 +1037,35 @@ let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args =
DAst.make ?loc @@ GApp (DAst.make ?loc:loc' @@ GRef (ref, us), arg)
| _ -> err ()
end
- | Some [s], GSort (Misctypes.GType []) -> DAst.make ?loc @@ GSort (glob_sort_of_level s)
+ | Some [s], GSort (GType []) -> DAst.make ?loc @@ GSort (glob_sort_of_level s)
| Some [_old_level], GSort _new_sort ->
(* TODO: add old_level and new_sort to the error message *)
- user_err ?loc (str "Cannot change universe level of notation " ++ pr_qualid qid.v)
+ user_err ?loc (str "Cannot change universe level of notation " ++ pr_qualid qid)
| Some _, _ -> err ()
in
c, projapp, args2
-let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args =
-function
- | {loc; v=Qualid qid} ->
- let qid = make ?loc qid in
- let r,projapp,args2 =
- try intern_qualid qid intern env ntnvars us args
- with Not_found -> error_global_not_found qid
- in
- let x, imp, scopes, l = find_appl_head_data r in
- (x,imp,scopes,l), args2
- | {loc; v=Ident id} ->
- try intern_var env lvar namedctx loc id us, args
+let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args qid =
+ let loc = qid.CAst.loc in
+ if qualid_is_ident qid then
+ try intern_var env lvar namedctx loc (qualid_basename qid) us, args
with Not_found ->
- let qid = make ?loc @@ qualid_of_ident id in
try
let r, projapp, args2 = intern_qualid ~no_secvar:true qid intern env ntnvars us args in
let x, imp, scopes, l = find_appl_head_data r in
(x,imp,scopes,l), args2
with Not_found ->
- (* Extra allowance for non globalizing functions *)
- if !interning_grammar || env.unb then
- (gvar (loc,id) us, [], [], []), args
+ (* Extra allowance for non globalizing functions *)
+ if !interning_grammar || env.unb then
+ (gvar (loc,qualid_basename qid) us, [], [], []), args
else error_global_not_found qid
+ else
+ let r,projapp,args2 =
+ try intern_qualid qid intern env ntnvars us args
+ with Not_found -> error_global_not_found qid
+ in
+ let x, imp, scopes, l = find_appl_head_data r in
+ (x,imp,scopes,l), args2
let interp_reference vars r =
let (r,_,_,_),_ =
@@ -1072,11 +1080,11 @@ let interp_reference vars r =
(** Private internalization patterns *)
type 'a raw_cases_pattern_expr_r =
- | RCPatAlias of 'a raw_cases_pattern_expr * Misctypes.lname
- | RCPatCstr of Globnames.global_reference
+ | RCPatAlias of 'a raw_cases_pattern_expr * lname
+ | RCPatCstr of GlobRef.t
* 'a raw_cases_pattern_expr list * 'a raw_cases_pattern_expr list
(** [RCPatCstr (loc, c, l1, l2)] represents [((@ c l1) l2)] *)
- | RCPatAtom of (Misctypes.lident * (Notation_term.tmp_scope_name option * Notation_term.scope_name list)) option
+ | RCPatAtom of (lident * (Notation_term.tmp_scope_name option * Notation_term.scope_name list)) option
| RCPatOr of 'a raw_cases_pattern_expr list
and 'a raw_cases_pattern_expr = ('a raw_cases_pattern_expr_r, 'a) DAst.t
@@ -1261,18 +1269,18 @@ let find_constructor loc add_params ref =
List.make nb ([], [(Id.Map.empty, DAst.make @@ PatVar Anonymous)])
| None -> []
-let find_pattern_variable = function
- | {v=Ident id} -> id
- | {loc;v=Qualid _} as x -> raise (InternalizationError(loc,NotAConstructor x))
+let find_pattern_variable qid =
+ if qualid_is_ident qid then qualid_basename qid
+ else raise (InternalizationError(qid.CAst.loc,NotAConstructor qid))
let check_duplicate loc fields =
- let eq (ref1, _) (ref2, _) = eq_reference ref1 ref2 in
+ let eq (ref1, _) (ref2, _) = qualid_eq ref1 ref2 in
let dups = List.duplicates eq fields in
match dups with
| [] -> ()
| (r, _) :: _ ->
user_err ?loc (str "This record defines several times the field " ++
- pr_reference r ++ str ".")
+ pr_qualid r ++ str ".")
(** [sort_fields ~complete loc fields completer] expects a list
[fields] of field assignments [f = e1; g = e2; ...], where [f, g]
@@ -1297,14 +1305,14 @@ let sort_fields ~complete loc fields completer =
(gr, Recordops.find_projection gr)
with Not_found ->
user_err ?loc ~hdr:"intern"
- (pr_reference first_field_ref ++ str": Not a projection")
+ (pr_qualid first_field_ref ++ str": Not a projection")
in
(* the number of parameters *)
let nparams = record.Recordops.s_EXPECTEDPARAM in
(* the reference constructor of the record *)
let base_constructor =
let global_record_id = ConstructRef record.Recordops.s_CONST in
- try make ?loc @@ Qualid (shortest_qualid_of_global Id.Set.empty global_record_id)
+ try shortest_qualid_of_global ?loc Id.Set.empty global_record_id
with Not_found ->
anomaly (str "Environment corruption for records.") in
let () = check_duplicate loc fields in
@@ -1312,14 +1320,14 @@ let sort_fields ~complete loc fields completer =
first_field_index, (* index of the first field of the record *)
proj_list) (* list of projections *)
=
- (* elimitate the first field from the projections,
+ (* eliminate the first field from the projections,
but keep its index *)
let rec build_proj_list projs proj_kinds idx ~acc_first_idx acc =
match projs with
| [] -> (idx, acc_first_idx, acc)
| (Some field_glob_id) :: projs ->
let field_glob_ref = ConstRef field_glob_id in
- let first_field = eq_gr field_glob_ref first_field_glob_ref in
+ let first_field = GlobRef.equal field_glob_ref first_field_glob_ref in
begin match proj_kinds with
| [] -> anomaly (Pp.str "Number of projections mismatch.")
| (_, regular) :: proj_kinds ->
@@ -1355,9 +1363,9 @@ let sort_fields ~complete loc fields completer =
let field_glob_ref = try global_reference_of_reference field_ref
with Not_found ->
user_err ?loc ~hdr:"intern"
- (str "The field \"" ++ pr_reference field_ref ++ str "\" does not exist.") in
+ (str "The field \"" ++ pr_qualid field_ref ++ str "\" does not exist.") in
let remaining_projs, (field_index, _) =
- let the_proj (idx, glob_id) = eq_gr field_glob_ref (ConstRef glob_id) in
+ let the_proj (idx, glob_id) = GlobRef.equal field_glob_ref (ConstRef glob_id) in
try CList.extract_first the_proj remaining_projs
with Not_found ->
user_err ?loc
@@ -1368,7 +1376,8 @@ let sort_fields ~complete loc fields completer =
(* the order does not matter as we sort them next,
List.rev_* is just for efficiency *)
let remaining_fields =
- let complete_field (idx, _field_ref) = (idx, completer idx) in
+ let complete_field (idx, field_ref) = (idx,
+ completer idx field_ref record.Recordops.s_CONST) in
List.rev_map complete_field remaining_projs in
List.rev_append remaining_fields acc
in
@@ -1384,7 +1393,7 @@ let sort_fields ~complete loc fields completer =
(** {6 Manage multiple aliases} *)
type alias = {
- alias_ids : Misctypes.lident list;
+ alias_ids : lident list;
alias_map : Id.t Id.Map.t;
}
@@ -1482,10 +1491,9 @@ let drop_notations_pattern looked_for genv =
end
| _ -> CErrors.anomaly Pp.(str "Invalid return pattern from Notation.interp_prim_token_cases_pattern_expr."))) x
in
- let rec drop_syndef top scopes re pats =
- let qid = qualid_of_reference re in
+ let rec drop_syndef top scopes qid pats =
try
- match locate_extended qid.v with
+ match locate_extended qid with
| SynDef sp ->
let (vars,a) = Syntax_def.search_syntactic_definition sp in
(match a with
@@ -1523,7 +1531,7 @@ let drop_notations_pattern looked_for genv =
| CPatAlias (p, id) -> DAst.make ?loc @@ RCPatAlias (in_pat top scopes p, id)
| CPatRecord l ->
let sorted_fields =
- sort_fields ~complete:false loc l (fun _idx -> CAst.make ?loc @@ CPatAtom None) in
+ sort_fields ~complete:false loc l (fun _idx fieldname constructor -> CAst.make ?loc @@ CPatAtom None) in
begin match sorted_fields with
| None -> DAst.make ?loc @@ RCPatAtom None
| Some (n, head, pl) ->
@@ -1541,10 +1549,10 @@ let drop_notations_pattern looked_for genv =
| Some (a,b,c) -> DAst.make ?loc @@ RCPatCstr(a, b, c)
| None -> raise (InternalizationError (loc,NotAConstructor head))
end
- | CPatCstr (r, Some expl_pl, pl) ->
- let g = try locate (qualid_of_reference r).v
+ | CPatCstr (qid, Some expl_pl, pl) ->
+ let g = try locate qid
with Not_found ->
- raise (InternalizationError (loc,NotAConstructor r)) in
+ raise (InternalizationError (loc,NotAConstructor qid)) in
if expl_pl == [] then
(* Convention: (@r) deactivates all further implicit arguments and scopes *)
DAst.make ?loc @@ RCPatCstr (g, List.map (in_pat false scopes) pl, [])
@@ -1553,11 +1561,11 @@ let drop_notations_pattern looked_for genv =
(* but not scopes in expl_pl *)
let (argscs1,_) = find_remaining_scopes expl_pl pl g in
DAst.make ?loc @@ RCPatCstr (g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat false scopes) pl, [])
- | CPatNotation ("- _",([a],[]),[]) when is_non_zero_pat a ->
+ | CPatNotation ((InConstrEntrySomeLevel,"- _"),([a],[]),[]) when is_non_zero_pat a ->
let p = match a.CAst.v with CPatPrim (Numeral (p, _)) -> p | _ -> assert false in
let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc (ensure_kind false loc) (Numeral (p,false)) scopes in
rcp_of_glob scopes pat
- | CPatNotation ("( _ )",([a],[]),[]) ->
+ | CPatNotation ((InConstrEntrySomeLevel,"( _ )"),([a],[]),[]) ->
in_pat top scopes a
| CPatNotation (ntn,fullargs,extrargs) ->
let ntn,(terms,termlists) = contract_curly_brackets_pat ntn fullargs in
@@ -1724,15 +1732,15 @@ let get_implicit_name n imps =
let set_hole_implicit i b c =
let loc = c.CAst.loc in
match DAst.get c with
- | GRef (r, _) -> Loc.tag ?loc (Evar_kinds.ImplicitArg (r,i,b),Misctypes.IntroAnonymous,None)
+ | GRef (r, _) -> Loc.tag ?loc (Evar_kinds.ImplicitArg (r,i,b),IntroAnonymous,None)
| GApp (r, _) ->
let loc = r.CAst.loc in
begin match DAst.get r with
| GRef (r, _) ->
- Loc.tag ?loc (Evar_kinds.ImplicitArg (r,i,b),Misctypes.IntroAnonymous,None)
+ Loc.tag ?loc (Evar_kinds.ImplicitArg (r,i,b),IntroAnonymous,None)
| _ -> anomaly (Pp.str "Only refs have implicits.")
end
- | GVar id -> Loc.tag ?loc (Evar_kinds.ImplicitArg (VarRef id,i,b),Misctypes.IntroAnonymous,None)
+ | GVar id -> Loc.tag ?loc (Evar_kinds.ImplicitArg (VarRef id,i,b),IntroAnonymous,None)
| _ -> anomaly (Pp.str "Only refs have implicits.")
let exists_implicit_name id =
@@ -1870,10 +1878,10 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
DAst.make ?loc @@
GLetIn (na.CAst.v, inc1, int,
intern (push_name_env ntnvars (impls_term_list inc1) env na) c2)
- | CNotation ("- _", ([a],[],[],[])) when is_non_zero a ->
+ | CNotation ((InConstrEntrySomeLevel,"- _"), ([a],[],[],[])) when is_non_zero a ->
let p = match a.CAst.v with CPrim (Numeral (p, _)) -> p | _ -> assert false in
intern env (CAst.make ?loc @@ CPrim (Numeral (p,false)))
- | CNotation ("( _ )",([a],[],[],[])) -> intern env a
+ | CNotation ((InConstrEntrySomeLevel,"( _ )"),([a],[],[],[])) -> intern env a
| CNotation (ntn,args) ->
intern_notation intern env ntnvars loc ntn args
| CGeneralization (b,a,c) ->
@@ -1889,9 +1897,9 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
intern_applied_reference intern env (Environ.named_context globalenv)
lvar us args ref
in
- (* Rem: GApp(_,f,[]) stands for @f *)
- DAst.make ?loc @@
- GApp (f, intern_args env args_scopes (List.map fst args))
+ (* Rem: GApp(_,f,[]) stands for @f *)
+ if args = [] then DAst.make ?loc @@ GApp (f,[]) else
+ smart_gapp f loc (intern_args env args_scopes (List.map fst args))
| CApp ((isproj,f), args) ->
let f,args = match f.CAst.v with
@@ -1917,14 +1925,22 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in
let fields =
sort_fields ~complete:true loc fs
- (fun _idx -> CAst.make ?loc @@ CHole (Some (Evar_kinds.QuestionMark (st,Anonymous)),
- Misctypes.IntroAnonymous, None))
+ (fun _idx fieldname constructorname ->
+ let open Evar_kinds in
+ let fieldinfo : Evar_kinds.record_field =
+ {fieldname=fieldname; recordname=inductive_of_constructor constructorname}
+ in
+ CAst.make ?loc @@ CHole (Some
+ (Evar_kinds.QuestionMark { Evar_kinds.default_question_mark with
+ Evar_kinds.qm_obligation=st;
+ Evar_kinds.qm_record_field=Some fieldinfo
+ }) , IntroAnonymous, None))
in
begin
match fields with
| None -> user_err ?loc ~hdr:"intern" (str"No constructor inference.")
| Some (n, constrname, args) ->
- let pars = List.make n (CAst.make ?loc @@ CHole (None, Misctypes.IntroAnonymous, None)) in
+ let pars = List.make n (CAst.make ?loc @@ CHole (None, IntroAnonymous, None)) in
let app = CAst.make ?loc @@ CAppExpl ((None, constrname,None), List.rev_append pars args) in
intern env app
end
@@ -1964,13 +1980,13 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
let main_sub_eqn = CAst.make @@
([],thepats, (* "|p1,..,pn" *)
Option.cata (intern_type env')
- (DAst.make ?loc @@ GHole(Evar_kinds.CasesType false,Misctypes.IntroAnonymous,None))
+ (DAst.make ?loc @@ GHole(Evar_kinds.CasesType false,IntroAnonymous,None))
rtnpo) (* "=> P" if there were a return predicate P, and "=> _" otherwise *) in
let catch_all_sub_eqn =
if List.for_all (irrefutable globalenv) thepats then [] else
[CAst.make @@ ([],List.make (List.length thepats) (DAst.make @@ PatVar Anonymous), (* "|_,..,_" *)
- DAst.make @@ GHole(Evar_kinds.ImpossibleCase,Misctypes.IntroAnonymous,None))] (* "=> _" *) in
- Some (DAst.make @@ GCases(Term.RegularStyle,sub_rtn,sub_tms,main_sub_eqn::catch_all_sub_eqn))
+ DAst.make @@ GHole(Evar_kinds.ImpossibleCase,IntroAnonymous,None))] (* "=> _" *) in
+ Some (DAst.make @@ GCases(RegularStyle,sub_rtn,sub_tms,main_sub_eqn::catch_all_sub_eqn))
in
let eqns' = List.map (intern_eqn (List.length tms) env) eqns in
DAst.make ?loc @@
@@ -2000,8 +2016,8 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
| None ->
let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in
(match naming with
- | Misctypes.IntroIdentifier id -> Evar_kinds.NamedHole id
- | _ -> Evar_kinds.QuestionMark (st,Anonymous))
+ | IntroIdentifier id -> Evar_kinds.NamedHole id
+ | _ -> Evar_kinds.QuestionMark { Evar_kinds.default_question_mark with Evar_kinds.qm_obligation=st; })
| Some k -> k
in
let solve = match solve with
@@ -2045,8 +2061,8 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
GSort s
| CCast (c1, c2) ->
DAst.make ?loc @@
- GCast (intern env c1, Miscops.map_cast_type (intern_type env) c2)
- )
+ GCast (intern env c1, map_cast_type (intern_type env) c2)
+ )
and intern_type env = intern (set_type_scope env)
and intern_local_binder env bind : intern_env * Glob_term.extended_glob_local_binder list =
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index f5e32dc4..dd0944cc 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -11,9 +11,7 @@
open Names
open Evd
open Environ
-open Misctypes
open Libnames
-open Globnames
open Glob_term
open Pattern
open EConstr
@@ -143,10 +141,10 @@ val intern_constr_pattern :
constr_pattern_expr -> patvar list * constr_pattern
(** Raise Not_found if syndef not bound to a name and error if unexisting ref *)
-val intern_reference : reference -> global_reference
+val intern_reference : qualid -> GlobRef.t
(** Expands abbreviations (syndef); raise an error if not existing *)
-val interp_reference : ltac_sign -> reference -> glob_constr
+val interp_reference : ltac_sign -> qualid -> glob_constr
(** Interpret binders *)
@@ -175,11 +173,11 @@ val interp_context_evars :
(** Locating references of constructions, possibly via a syntactic definition
(these functions do not modify the glob file) *)
-val locate_reference : Libnames.qualid -> Globnames.global_reference
+val locate_reference : Libnames.qualid -> GlobRef.t
val is_global : Id.t -> bool
-val construct_reference : ('c, 't) Context.Named.pt -> Id.t -> Globnames.global_reference
-val global_reference : Id.t -> Globnames.global_reference
-val global_reference_in_absolute_module : DirPath.t -> Id.t -> Globnames.global_reference
+val construct_reference : ('c, 't) Context.Named.pt -> Id.t -> GlobRef.t
+val global_reference : Id.t -> GlobRef.t
+val global_reference_in_absolute_module : DirPath.t -> Id.t -> GlobRef.t
(** Interprets a term as the left-hand side of a notation. The returned map is
guaranteed to have the same domain as the input one. *)
diff --git a/interp/declare.ml b/interp/declare.ml
index c55a6c69..a82e6b35 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -150,8 +150,8 @@ let register_side_effect (c, role) =
ignore(add_leaf id o);
update_tables c;
match role with
- | Safe_typing.Subproof -> ()
- | Safe_typing.Schema (ind, kind) -> !declare_scheme kind [|ind,c|]
+ | Subproof -> ()
+ | Schema (ind, kind) -> !declare_scheme kind [|ind,c|]
let declare_constant_common id cst =
let o = inConstant cst in
@@ -382,19 +382,44 @@ let inInductive : inductive_obj -> obj =
discharge_function = discharge_inductive;
rebuild_function = infer_inductive_subtyping }
-let declare_projections mind =
- let spec,_ = Inductive.lookup_mind_specif (Global.env ()) (mind,0) in
- match spec.mind_record with
- | Some (Some (_, kns, pjs)) ->
- Array.iteri (fun i kn ->
- let id = Label.to_id (Constant.label kn) in
- let entry = {proj_entry_ind = mind; proj_entry_arg = i} in
- let kn' = declare_constant id (ProjectionEntry entry,
- IsDefinition StructureComponent)
- in
- assert(Constant.equal kn kn')) kns; true,true
- | Some None -> true,false
- | None -> false,false
+let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (term,types) =
+ let id = Label.to_id label in
+ let p = Projection.Repr.make ind ~proj_npars ~proj_arg label in
+ Recordops.declare_primitive_projection p;
+ (* ^ needs to happen before declaring the constant, otherwise
+ Heads gets confused. *)
+ let univs = match univs with
+ | Monomorphic_ind_entry _ ->
+ (** Global constraints already defined through the inductive *)
+ Monomorphic_const_entry Univ.ContextSet.empty
+ | Polymorphic_ind_entry ctx ->
+ Polymorphic_const_entry ctx
+ | Cumulative_ind_entry ctx ->
+ Polymorphic_const_entry (Univ.CumulativityInfo.univ_context ctx)
+ in
+ let term, types = match univs with
+ | Monomorphic_const_entry _ -> term, types
+ | Polymorphic_const_entry ctx ->
+ let u = Univ.UContext.instance ctx in
+ Vars.subst_instance_constr u term, Vars.subst_instance_constr u types
+ in
+ let entry = definition_entry ~types ~univs term in
+ ignore(declare_constant id (DefinitionEntry entry, IsDefinition StructureComponent))
+
+let declare_projections univs mind =
+ let env = Global.env () in
+ let mib = Environ.lookup_mind mind env in
+ match mib.mind_record with
+ | PrimRecord info ->
+ let iter_ind i (_, labs, _) =
+ let ind = (mind, i) in
+ let projs = Inductiveops.compute_projections env ind in
+ Array.iter2_i (declare_one_projection univs ind ~proj_npars:mib.mind_nparams) labs projs
+ in
+ let () = Array.iteri iter_ind info in
+ true
+ | FakeRecord -> false
+ | NotRecord -> false
(* for initial declaration *)
let declare_mind mie =
@@ -403,7 +428,7 @@ let declare_mind mie =
| [] -> anomaly (Pp.str "cannot declare an empty list of inductives.") in
let (sp,kn as oname) = add_leaf id (inInductive ([],mie)) in
let mind = Global.mind_of_delta_kn kn in
- let isrecord,isprim = declare_projections mind in
+ let isprim = declare_projections mie.mind_entry_universes mind in
declare_mib_implicits mind;
declare_inductive_argument_scopes mind mie;
oname, isprim
@@ -446,24 +471,20 @@ let assumption_message id =
discussion on coqdev: "Chapter 4 of the Reference Manual", 8/10/2015) *)
Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is declared")
-(** Global universe names, in a different summary *)
-
-type universe_context_decl = polymorphic * Univ.ContextSet.t
-
-let cache_universe_context (p, ctx) =
- Global.push_context_set p ctx;
- if p then Lib.add_section_context ctx
+(** Monomorphic universes need to survive sections. *)
-let input_universe_context : universe_context_decl -> Libobject.obj =
+let input_universe_context : Univ.ContextSet.t -> Libobject.obj =
declare_object
- { (default_object "Global universe context state") with
- cache_function = (fun (na, pi) -> cache_universe_context pi);
- load_function = (fun _ (_, pi) -> cache_universe_context pi);
- discharge_function = (fun (_, (p, _ as x)) -> if p then None else Some x);
- classify_function = (fun a -> Keep a) }
+ { (default_object "Monomorphic section universes") with
+ cache_function = (fun (na, uctx) -> Global.push_context_set false uctx);
+ discharge_function = (fun (_, x) -> Some x);
+ classify_function = (fun a -> Dispose) }
let declare_universe_context poly ctx =
- Lib.add_anonymous_leaf (input_universe_context (poly, ctx))
+ if poly then
+ (Global.push_context_set true ctx; Lib.add_section_context ctx)
+ else
+ Lib.add_anonymous_leaf (input_universe_context ctx)
(** Global universes are not substitutive objects but global objects
bound at the *library* or *module* level. The polymorphic flag is
@@ -487,7 +508,7 @@ let add_universe src (dp, i) =
Option.iter (fun poly ->
let ctx = Univ.ContextSet.add_universe level Univ.ContextSet.empty in
Global.push_context_set poly ctx;
- Universes.add_global_universe level poly;
+ UnivNames.add_global_universe level poly;
if poly then Lib.add_section_context ctx)
optpoly
@@ -538,7 +559,7 @@ let input_universe : universe_decl -> Libobject.obj =
let declare_univ_binders gr pl =
if Global.is_polymorphic gr then
- Universes.register_universe_binders gr pl
+ UnivNames.register_universe_binders gr pl
else
let l = match gr with
| ConstRef c -> Label.to_id @@ Constant.label c
@@ -564,7 +585,7 @@ let do_universe poly l =
in
let l =
List.map (fun {CAst.v=id} ->
- let lev = Universes.new_univ_id () in
+ let lev = UnivGen.new_univ_id () in
(id, lev)) l
in
let src = if poly then BoundUniv else UnqualifiedUniv in
@@ -572,30 +593,11 @@ let do_universe poly l =
ignore(Lib.add_leaf id (input_universe (src, lev))))
l
-type constraint_decl = polymorphic * Univ.Constraint.t
-
-let cache_constraints (na, (p, c)) =
- let ctx =
- Univ.ContextSet.add_constraints c
- Univ.ContextSet.empty (* No declared universes here, just constraints *)
- in cache_universe_context (p,ctx)
-
-let discharge_constraints (_, (p, c as a)) =
- if p then None else Some a
-
-let input_constraints : constraint_decl -> Libobject.obj =
- let open Libobject in
- declare_object
- { (default_object "Global universe constraints") with
- cache_function = cache_constraints;
- load_function = (fun _ -> cache_constraints);
- discharge_function = discharge_constraints;
- classify_function = (fun a -> Keep a) }
-
let do_constraint poly l =
+ let open Univ in
let u_of_id x =
let level = Pretyping.interp_known_glob_level (Evd.from_env (Global.env ())) x in
- Universes.is_polymorphic level, level
+ UnivNames.is_polymorphic level, level
in
let in_section = Lib.sections_are_opened () in
let () =
@@ -614,7 +616,8 @@ let do_constraint poly l =
let constraints = List.fold_left (fun acc (l, d, r) ->
let p, lu = u_of_id l and p', ru = u_of_id r in
check_poly p p';
- Univ.Constraint.add (lu, d, ru) acc)
- Univ.Constraint.empty l
+ Constraint.add (lu, d, ru) acc)
+ Constraint.empty l
in
- Lib.add_anonymous_leaf (input_constraints (poly, constraints))
+ let uctx = ContextSet.add_constraints constraints ContextSet.empty in
+ declare_universe_context poly uctx
diff --git a/interp/declare.mli b/interp/declare.mli
index 084d746e..02e73cd6 100644
--- a/interp/declare.mli
+++ b/interp/declare.mli
@@ -83,10 +83,10 @@ val recursive_message : bool (** true = fixpoint *) ->
val exists_name : Id.t -> bool
(** Global universe contexts, names and constraints *)
-val declare_univ_binders : Globnames.global_reference -> Universes.universe_binders -> unit
+val declare_univ_binders : GlobRef.t -> UnivNames.universe_binders -> unit
val declare_universe_context : polymorphic -> Univ.ContextSet.t -> unit
-val do_universe : polymorphic -> Misctypes.lident list -> unit
-val do_constraint : polymorphic -> (Misctypes.glob_level * Univ.constraint_type * Misctypes.glob_level) list ->
+val do_universe : polymorphic -> lident list -> unit
+val do_constraint : polymorphic -> (Glob_term.glob_level * Univ.constraint_type * Glob_term.glob_level) list ->
unit
diff --git a/interp/discharge.ml b/interp/discharge.ml
index e16a955d..0e44a8b4 100644
--- a/interp/discharge.ml
+++ b/interp/discharge.ml
@@ -111,9 +111,10 @@ let process_inductive info modlist mib =
let section_decls' = Context.Named.map discharge section_decls in
let (params',inds') = abstract_inductive section_decls' nparamdecls inds in
let record = match mib.mind_record with
- | Some (Some (id, _, _)) -> Some (Some id)
- | Some None -> Some None
- | None -> None
+ | PrimRecord info ->
+ Some (Some (Array.map pi1 info))
+ | FakeRecord -> Some None
+ | NotRecord -> None
in
{ mind_entry_record = record;
mind_entry_finite = mib.mind_finite;
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index bc6a1ef3..ccad6b19 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -113,7 +113,7 @@ let type_of_global_ref gr =
"var" ^ type_of_logical_kind (Decls.variable_kind v)
| Globnames.IndRef ind ->
let (mib,oib) = Inductive.lookup_mind_specif (Global.env ()) ind in
- if mib.Declarations.mind_record <> None then
+ if mib.Declarations.mind_record <> Declarations.NotRecord then
begin match mib.Declarations.mind_finite with
| Finite -> "indrec"
| BiFinite -> "rec"
@@ -167,7 +167,7 @@ let dump_modref ?loc mp ty =
let dump_libref ?loc dp ty =
dump_ref ?loc (Names.DirPath.to_string dp) "<>" "<>" ty
-let cook_notation df sc =
+let cook_notation (from,df) sc =
(* We encode notations so that they are space-free and still human-readable *)
(* - all spaces are replaced by _ *)
(* - all _ denoting a non-terminal symbol are replaced by x *)
@@ -203,7 +203,9 @@ let cook_notation df sc =
if !i <= l then (set ntn !j '_'; incr j; incr i)
done;
let df = Bytes.sub_string ntn 0 !j in
- match sc with Some sc -> ":" ^ sc ^ ":" ^ df | _ -> "::" ^ df
+ let df_sc = match sc with Some sc -> ":" ^ sc ^ ":" ^ df | _ -> "::" ^ df in
+ let from_df_sc = match from with Constrexpr.InCustomEntryLevel (from,_) -> ":" ^ from ^ df_sc | Constrexpr.InConstrEntrySomeLevel -> ":" ^ df_sc in
+ from_df_sc
let dump_notation_location posl df (((path,secpath),_),sc) =
if dump () then
@@ -254,7 +256,7 @@ let dump_def ?loc ty secpath id = Option.iter (fun loc ->
let dump_definition {CAst.loc;v=id} sec s =
dump_def ?loc s (Names.DirPath.to_string (Lib.current_dirpath sec)) (Names.Id.to_string id)
-let dump_constraint (({ CAst.loc; v = n },_), _, _) sec ty =
+let dump_constraint { CAst.loc; v = n } sec ty =
match n with
| Names.Name id -> dump_definition CAst.(make ?loc id) sec ty
| Names.Anonymous -> ()
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index 43c10000..931d05a9 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -24,10 +24,10 @@ val feedback_glob : unit -> unit
val pause : unit -> unit
val continue : unit -> unit
-val add_glob : ?loc:Loc.t -> Globnames.global_reference -> unit
+val add_glob : ?loc:Loc.t -> Names.GlobRef.t -> unit
val add_glob_kn : ?loc:Loc.t -> Names.KerName.t -> unit
-val dump_definition : Misctypes.lident -> bool -> string -> unit
+val dump_definition : Names.lident -> bool -> string -> unit
val dump_moddef : ?loc:Loc.t -> Names.ModPath.t -> string -> unit
val dump_modref : ?loc:Loc.t -> Names.ModPath.t -> string -> unit
val dump_reference : ?loc:Loc.t -> string -> string -> string -> unit
@@ -38,9 +38,9 @@ val dump_binding : ?loc:Loc.t -> Names.Id.Set.elt -> unit
val dump_notation :
(Constrexpr.notation * Notation.notation_location) Loc.located ->
Notation_term.scope_name option -> bool -> unit
-val dump_constraint :
- Vernacexpr.typeclass_constraint -> bool -> string -> unit
+
+val dump_constraint : Names.lname -> bool -> string -> unit
val dump_string : string -> unit
-val type_of_global_ref : Globnames.global_reference -> string
+val type_of_global_ref : Names.GlobRef.t -> string
diff --git a/interp/genintern.ml b/interp/genintern.ml
index 161201c4..d9a0db04 100644
--- a/interp/genintern.ml
+++ b/interp/genintern.ml
@@ -26,9 +26,15 @@ let empty_glob_sign env = {
extra = Store.empty;
}
+(** In globalize tactics, we need to keep the initial [constr_expr] to recompute
+ in the environment by the effective calls to Intro, Inversion, etc
+ The [constr_expr] field is [None] in TacDef though *)
+type glob_constr_and_expr = Glob_term.glob_constr * Constrexpr.constr_expr option
+type glob_constr_pattern_and_expr = Id.Set.t * glob_constr_and_expr * Pattern.constr_pattern
+
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
+type 'glb ntn_subst_fun = glob_constr_and_expr Id.Map.t -> 'glb -> 'glb
module InternObj =
struct
diff --git a/interp/genintern.mli b/interp/genintern.mli
index d818713f..f4f064bc 100644
--- a/interp/genintern.mli
+++ b/interp/genintern.mli
@@ -22,6 +22,12 @@ type glob_sign = {
val empty_glob_sign : Environ.env -> glob_sign
+(** In globalize tactics, we need to keep the initial [constr_expr] to recompute
+ in the environment by the effective calls to Intro, Inversion, etc
+ The [constr_expr] field is [None] in TacDef though *)
+type glob_constr_and_expr = Glob_term.glob_constr * Constrexpr.constr_expr option
+type glob_constr_pattern_and_expr = Id.Set.t * glob_constr_and_expr * Pattern.constr_pattern
+
(** {5 Internalization functions} *)
type ('raw, 'glb) intern_fun = glob_sign -> 'raw -> glob_sign * 'glb
@@ -42,7 +48,7 @@ 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
+type 'glb ntn_subst_fun = glob_constr_and_expr Id.Map.t -> 'glb -> 'glb
val substitute_notation : ('raw, 'glb, 'top) genarg_type -> 'glb ntn_subst_fun
diff --git a/interp/genredexpr.ml b/interp/genredexpr.ml
new file mode 100644
index 00000000..607f2258
--- /dev/null
+++ b/interp/genredexpr.ml
@@ -0,0 +1,65 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(** Reduction expressions *)
+
+(** The parsing produces initially a list of [red_atom] *)
+
+type 'a red_atom =
+ | FBeta
+ | FMatch
+ | FFix
+ | FCofix
+ | FZeta
+ | FConst of 'a list
+ | FDeltaBut of 'a list
+
+(** This list of atoms is immediately converted to a [glob_red_flag] *)
+
+type 'a glob_red_flag = {
+ rBeta : bool;
+ rMatch : bool;
+ rFix : bool;
+ rCofix : bool;
+ rZeta : bool;
+ rDelta : bool; (** true = delta all but rConst; false = delta only on rConst*)
+ rConst : 'a list
+}
+
+(** Generic kinds of reductions *)
+
+type ('a,'b,'c) red_expr_gen =
+ | Red of bool
+ | Hnf
+ | Simpl of 'b glob_red_flag*('b,'c) Util.union Locus.with_occurrences option
+ | Cbv of 'b glob_red_flag
+ | Cbn of 'b glob_red_flag
+ | Lazy of 'b glob_red_flag
+ | Unfold of 'b Locus.with_occurrences list
+ | Fold of 'a list
+ | Pattern of 'a Locus.with_occurrences list
+ | ExtraRedExpr of string
+ | CbvVm of ('b,'c) Util.union Locus.with_occurrences option
+ | CbvNative of ('b,'c) Util.union Locus.with_occurrences option
+
+type ('a,'b,'c) may_eval =
+ | ConstrTerm of 'a
+ | ConstrEval of ('a,'b,'c) red_expr_gen * 'a
+ | ConstrContext of Names.lident * 'a
+ | ConstrTypeOf of 'a
+
+open Libnames
+open Constrexpr
+
+type r_trm = constr_expr
+type r_pat = constr_pattern_expr
+type r_cst = qualid or_by_notation
+
+type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen
diff --git a/interp/impargs.ml b/interp/impargs.ml
index 9ad62c0d..e542b818 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -139,7 +139,7 @@ let argument_less = function
| Hyp _, Conclusion -> true
| Conclusion, _ -> false
-let update pos rig (na,st) =
+let update pos rig st =
let e =
if rig then
match st with
@@ -163,7 +163,7 @@ let update pos rig (na,st) =
| Some (DepFlex fpos as x) ->
if argument_less (pos,fpos) then DepFlex pos else x
| Some Manual -> assert false
- in na, Some e
+ in Some e
(* modified is_rigid_reference with a truncated env *)
let is_flexible_reference env sigma bound depth f =
@@ -214,6 +214,8 @@ let add_free_rels_until strict strongly_strict revpat bound env sigma m pos acc
let () = if not (Vars.noccur_between sigma 1 bound m) then frec true (env,1) m in
acc
+(* compute the list of implicit arguments *)
+
let rec is_rigid_head sigma t = match kind sigma t with
| Rel _ | Evar _ -> false
| Ind _ | Const _ | Var _ | Sort _ -> true
@@ -226,51 +228,69 @@ let rec is_rigid_head sigma t = match kind sigma t with
| Lambda _ | LetIn _ | Construct _ | CoFix _ | Fix _
| Prod _ | Meta _ | Cast _ -> assert false
-(* calcule la liste des arguments implicites *)
+let is_rigid env sigma t =
+ let open Context.Rel.Declaration in
+ let t = whd_all env sigma t in
+ match kind sigma t with
+ | Prod (na,a,b) ->
+ let (_,t) = splay_prod (push_rel (LocalAssum (na,a)) env) sigma b in
+ is_rigid_head sigma t
+ | _ -> true
-let find_displayed_name_in all avoid na (env, b) =
+let find_displayed_name_in sigma all avoid na (env, b) =
let envnames_b = (env, b) in
let flag = RenamingElsewhereFor envnames_b in
- if all then compute_and_force_displayed_name_in Evd.empty flag avoid na b
- else compute_displayed_name_in Evd.empty flag avoid na b
+ if all then compute_and_force_displayed_name_in sigma flag avoid na b
+ else compute_displayed_name_in sigma flag avoid na b
+
+let compute_implicits_names_gen all env sigma t =
+ let open Context.Rel.Declaration in
+ let rec aux env avoid names t =
+ let t = whd_all env sigma t in
+ match kind sigma t with
+ | Prod (na,a,b) ->
+ let na',avoid' = find_displayed_name_in sigma all avoid na (names,b) in
+ aux (push_rel (LocalAssum (na,a)) env) avoid' (na'::names) b
+ | _ -> List.rev names
+ in aux env Id.Set.empty [] t
+
+let compute_implicits_names = compute_implicits_names_gen true
-let compute_implicits_gen strict strongly_strict revpat contextual all env sigma (t : EConstr.t) =
- let rigid = ref true in
+let compute_implicits_explanation_gen strict strongly_strict revpat contextual env sigma t =
let open Context.Rel.Declaration in
- let rec aux env avoid n names (t : EConstr.t) =
+ let rec aux env n t =
let t = whd_all env sigma t in
match kind sigma t with
- | Prod (na,a,b) ->
- let na',avoid' = find_displayed_name_in all avoid na (names,b) in
- add_free_rels_until strict strongly_strict revpat n env sigma a (Hyp (n+1))
- (aux (push_rel (LocalAssum (na',a)) env) avoid' (n+1) (na'::names) b)
- | _ ->
- rigid := is_rigid_head sigma t;
- let names = List.rev names in
- let v = Array.map (fun na -> na,None) (Array.of_list names) in
- if contextual then
- add_free_rels_until strict strongly_strict revpat n env sigma t Conclusion v
- else v
+ | Prod (na,a,b) ->
+ add_free_rels_until strict strongly_strict revpat n env sigma a (Hyp (n+1))
+ (aux (push_rel (LocalAssum (na,a)) env) (n+1) b)
+ | _ ->
+ let v = Array.make n None in
+ if contextual then
+ add_free_rels_until strict strongly_strict revpat n env sigma t Conclusion v
+ else v
in
match kind sigma (whd_all env sigma t) with
- | Prod (na,a,b) ->
- let na',avoid = find_displayed_name_in all Id.Set.empty na ([],b) in
- let v = aux (push_rel (LocalAssum (na',a)) env) avoid 1 [na'] b in
- !rigid, Array.to_list v
- | _ -> true, []
+ | Prod (na,a,b) ->
+ let v = aux (push_rel (LocalAssum (na,a)) env) 1 b in
+ Array.to_list v
+ | _ -> []
-let compute_implicits_flags env sigma f all t =
- compute_implicits_gen
+let compute_implicits_explanation_flags env sigma f t =
+ compute_implicits_explanation_gen
(f.strict || f.strongly_strict) f.strongly_strict
- f.reversible_pattern f.contextual all env sigma t
+ f.reversible_pattern f.contextual env sigma t
-let compute_auto_implicits env sigma flags enriching t =
- if enriching then compute_implicits_flags env sigma flags true t
- else compute_implicits_gen false false false true true env sigma t
+let compute_implicits_flags env sigma f all t =
+ List.combine
+ (compute_implicits_names_gen all env sigma t)
+ (compute_implicits_explanation_flags env sigma f t)
-let compute_implicits_names env sigma t =
- let _, impls = compute_implicits_gen false false false false true env sigma t in
- List.map fst impls
+let compute_auto_implicits env sigma flags enriching t =
+ List.combine
+ (compute_implicits_names env sigma t)
+ (if enriching then compute_implicits_explanation_flags env sigma flags t
+ else compute_implicits_explanation_gen false false false true env sigma t)
(* Extra information about implicit arguments *)
@@ -329,13 +349,16 @@ let rec prepare_implicits f = function
Some (id,imp,(set_maximality imps' f.maximal,true)) :: imps'
| _::imps -> None :: prepare_implicits f imps
-let set_implicit id imp insmax =
- (id,(match imp with None -> Manual | Some imp -> imp),insmax)
-
-let rec assoc_by_pos k = function
- (ExplByPos (k', x), b) :: tl when Int.equal k k' -> (x,b), tl
- | hd :: tl -> let (x, tl) = assoc_by_pos k tl in x, hd :: tl
- | [] -> raise Not_found
+(*
+If found, returns Some (x,(b,fi,fo)) and l with the entry removed,
+otherwise returns None and l unchanged.
+ *)
+let assoc_by_pos k l =
+ let rec aux = function
+ (ExplByPos (k', x), b) :: tl when Int.equal k k' -> Some (x,b), tl
+ | hd :: tl -> let (x, tl) = aux tl in x, hd :: tl
+ | [] -> raise Not_found
+ in try aux l with Not_found -> None, l
let check_correct_manual_implicits autoimps l =
List.iter (function
@@ -352,70 +375,65 @@ let check_correct_manual_implicits autoimps l =
(str "Cannot set implicit argument number " ++ int i ++
str ": it has no name.")) l
-let set_manual_implicits env flags enriching autoimps l =
- let try_forced k l =
- try
- let (id, (b, fi, fo)), l' = assoc_by_pos k l in
- if fo then
- let id = match id with Some id -> id | None -> Id.of_string ("arg_" ^ string_of_int k) in
- l', Some (id,Manual,(b,fi))
- else l, None
- with Not_found -> l, None
- in
+(* Take a list l of explicitations, and map them to positions. *)
+let flatten_explicitations l autoimps =
+ let rec aux k l = function
+ | (Name id,_)::imps ->
+ let value, l' =
+ try
+ let eq = explicitation_eq in
+ let flags = List.assoc_f eq (ExplByName id) l in
+ Some (Some id, flags), List.remove_assoc_f eq (ExplByName id) l
+ with Not_found -> assoc_by_pos k l
+ in value :: aux (k+1) l' imps
+ | (Anonymous,_)::imps ->
+ let value, l' = assoc_by_pos k l
+ in value :: aux (k+1) l' imps
+ | [] when List.is_empty l -> []
+ | [] ->
+ check_correct_manual_implicits autoimps l;
+ []
+ in aux 1 l autoimps
+
+let set_manual_implicits flags enriching autoimps l =
if not (List.distinct l) then
user_err Pp.(str "Some parameters are referred more than once.");
(* Compare with automatic implicits to recover printing data and names *)
- let rec merge k l = function
- | (Name id,imp)::imps ->
- let l',imp,m =
- try
- let eq = explicitation_eq in
- let (b, fi, fo) = List.assoc_f eq (ExplByName id) l in
- List.remove_assoc_f eq (ExplByName id) l, (Some Manual), (Some (b, fi))
- with Not_found ->
- try
- let (id, (b, fi, fo)), l' = assoc_by_pos k l in
- l', (Some Manual), (Some (b,fi))
- with Not_found ->
- let m = match enriching, imp with
- | true, Some _ -> Some (flags.maximal, true)
- | _ -> None
- in
- l, imp, m
- in
- let imps' = merge (k+1) l' imps in
- let m = Option.map (fun (b,f) ->
- (* match imp with Some Manual -> (b,f) *)
- (* | _ -> *)set_maximality imps' b, f) m in
- Option.map (set_implicit id imp) m :: imps'
- | (Anonymous,imp)::imps ->
- let l', forced = try_forced k l in
- forced :: merge (k+1) l' imps
- | [] when begin match l with [] -> true | _ -> false end -> []
- | [] ->
- check_correct_manual_implicits autoimps l;
- []
- in
- merge 1 l autoimps
-
-let compute_semi_auto_implicits env sigma f manual t =
- match manual with
- | [] ->
- if not f.auto then [DefaultImpArgs, []]
- else let _,l = compute_implicits_flags env sigma f false t in
- [DefaultImpArgs, prepare_implicits f l]
- | _ ->
- let _,autoimpls = compute_auto_implicits env sigma f f.auto t in
- [DefaultImpArgs, set_manual_implicits env f f.auto autoimpls manual]
+ let rec merge k autoimps explimps = match autoimps, explimps with
+ | autoimp::autoimps, explimp::explimps ->
+ let imps' = merge (k+1) autoimps explimps in
+ begin match autoimp, explimp with
+ | (Name id,_), Some (_, (b, fi, _)) ->
+ Some (id, Manual, (set_maximality imps' b, fi))
+ | (Name id,Some exp), None when enriching ->
+ Some (id, exp, (set_maximality imps' flags.maximal, true))
+ | (Name _,_), None -> None
+ | (Anonymous,_), Some (Some id, (b, fi, true)) ->
+ Some (id,Manual,(b,fi))
+ | (Anonymous,_), Some (None, (b, fi, true)) ->
+ let id = Id.of_string ("arg_" ^ string_of_int k) in
+ Some (id,Manual,(b,fi))
+ | (Anonymous,_), Some (_, (_, _, false)) -> None
+ | (Anonymous,_), None -> None
+ end :: imps'
+ | [], [] -> []
+ (* flatten_explicitations returns a list of the same length as autoimps *)
+ | _ -> assert false
+ in merge 1 autoimps (flatten_explicitations l autoimps)
+
+let compute_semi_auto_implicits env sigma f t =
+ if not f.auto then [DefaultImpArgs, []]
+ else let l = compute_implicits_flags env sigma f false t in
+ [DefaultImpArgs, prepare_implicits f l]
(*s Constants. *)
-let compute_constant_implicits flags manual cst =
+let compute_constant_implicits flags cst =
let env = Global.env () in
let sigma = Evd.from_env env in
let cb = Environ.lookup_constant cst env in
let ty = of_constr cb.const_type in
- let impls = compute_semi_auto_implicits env sigma flags manual ty in
+ let impls = compute_semi_auto_implicits env sigma flags ty in
impls
(*s Inductives and constructors. Their implicit arguments are stored
@@ -423,7 +441,7 @@ let compute_constant_implicits flags manual cst =
$i$ are the implicit arguments of the inductive and $v$ the array of
implicit arguments of the constructors. *)
-let compute_mib_implicits flags manual kn =
+let compute_mib_implicits flags kn =
let env = Global.env () in
let sigma = Evd.from_env env in
let mib = Environ.lookup_mind kn env in
@@ -439,34 +457,34 @@ let compute_mib_implicits flags manual kn =
let imps_one_inductive i mip =
let ind = (kn,i) in
let ar, _ = Global.type_of_global_in_context env (IndRef ind) in
- ((IndRef ind,compute_semi_auto_implicits env sigma flags manual (of_constr ar)),
+ ((IndRef ind,compute_semi_auto_implicits env sigma flags (of_constr ar)),
Array.mapi (fun j c ->
- (ConstructRef (ind,j+1),compute_semi_auto_implicits env_ar sigma flags manual c))
+ (ConstructRef (ind,j+1),compute_semi_auto_implicits env_ar sigma flags c))
(Array.map of_constr mip.mind_nf_lc))
in
Array.mapi imps_one_inductive mib.mind_packets
-let compute_all_mib_implicits flags manual kn =
- let imps = compute_mib_implicits flags manual kn in
+let compute_all_mib_implicits flags kn =
+ let imps = compute_mib_implicits flags kn in
List.flatten
(Array.map_to_list (fun (ind,cstrs) -> ind::Array.to_list cstrs) imps)
(*s Variables. *)
-let compute_var_implicits flags manual id =
+let compute_var_implicits flags id =
let env = Global.env () in
let sigma = Evd.from_env env in
- compute_semi_auto_implicits env sigma flags manual (NamedDecl.get_type (lookup_named id env))
+ compute_semi_auto_implicits env sigma flags (NamedDecl.get_type (lookup_named id env))
(* Implicits of a global reference. *)
-let compute_global_implicits flags manual = function
- | VarRef id -> compute_var_implicits flags manual id
- | ConstRef kn -> compute_constant_implicits flags manual kn
+let compute_global_implicits flags = function
+ | VarRef id -> compute_var_implicits flags id
+ | ConstRef kn -> compute_constant_implicits flags kn
| IndRef (kn,i) ->
- let ((_,imps),_) = (compute_mib_implicits flags manual kn).(i) in imps
+ let ((_,imps),_) = (compute_mib_implicits flags kn).(i) in imps
| ConstructRef ((kn,i),j) ->
- let (_,cimps) = (compute_mib_implicits flags manual kn).(i) in snd cimps.(j-1)
+ let (_,cimps) = (compute_mib_implicits flags kn).(i) in snd cimps.(j-1)
(* Merge a manual explicitation with an implicit_status list *)
@@ -487,7 +505,7 @@ type implicit_discharge_request =
| ImplLocal
| ImplConstant of Constant.t * implicits_flags
| ImplMutualInductive of MutInd.t * implicits_flags
- | ImplInteractive of global_reference * implicits_flags *
+ | ImplInteractive of GlobRef.t * implicits_flags *
implicit_interactive_request
let implicits_table = Summary.ref Refmap.empty ~name:"implicits"
@@ -520,7 +538,7 @@ let subst_implicits_decl subst (r,imps as o) =
let r' = fst (subst_global subst r) in if r==r' then o else (r',imps)
let subst_implicits (subst,(req,l)) =
- (ImplLocal,List.smartmap (subst_implicits_decl subst) l)
+ (ImplLocal,List.Smart.map (subst_implicits_decl subst) l)
let impls_of_context ctx =
let map (decl, impl) = match impl with
@@ -573,34 +591,34 @@ let rebuild_implicits (req,l) =
| ImplLocal -> assert false
| ImplConstant (con,flags) ->
let oldimpls = snd (List.hd l) in
- let newimpls = compute_constant_implicits flags [] con in
+ let newimpls = compute_constant_implicits flags con in
req, [ConstRef con, List.map2 merge_impls oldimpls newimpls]
| ImplMutualInductive (kn,flags) ->
- let newimpls = compute_all_mib_implicits flags [] kn in
+ let newimpls = compute_all_mib_implicits flags kn in
let rec aux olds news =
- match olds, news with
- | (_, oldimpls) :: old, (gr, newimpls) :: tl ->
- (gr, List.map2 merge_impls oldimpls newimpls) :: aux old tl
- | [], [] -> []
- | _, _ -> assert false
+ match olds, news with
+ | (_, oldimpls) :: old, (gr, newimpls) :: tl ->
+ (gr, List.map2 merge_impls oldimpls newimpls) :: aux old tl
+ | [], [] -> []
+ | _, _ -> assert false
in req, aux l newimpls
| ImplInteractive (ref,flags,o) ->
(if isVarRef ref && is_in_section ref then ImplLocal else req),
match o with
| ImplAuto ->
- let oldimpls = snd (List.hd l) in
- let newimpls = compute_global_implicits flags [] ref in
- [ref,List.map2 merge_impls oldimpls newimpls]
+ let oldimpls = snd (List.hd l) in
+ let newimpls = compute_global_implicits flags ref in
+ [ref,List.map2 merge_impls oldimpls newimpls]
| ImplManual userimplsize ->
- let oldimpls = snd (List.hd l) in
- if flags.auto then
- let newimpls = List.hd (compute_global_implicits flags [] ref) in
- let p = List.length (snd newimpls) - userimplsize in
- let newimpls = on_snd (List.firstn p) newimpls in
- [ref,List.map (fun o -> merge_impls o newimpls) oldimpls]
- else
- [ref,oldimpls]
+ let oldimpls = snd (List.hd l) in
+ if flags.auto then
+ let newimpls = List.hd (compute_global_implicits flags ref) in
+ let p = List.length (snd newimpls) - userimplsize in
+ let newimpls = on_snd (List.firstn p) newimpls in
+ [ref,List.map (fun o -> merge_impls o newimpls) oldimpls]
+ else
+ [ref,oldimpls]
let classify_implicits (req,_ as obj) = match req with
| ImplLocal -> Dispose
@@ -608,7 +626,7 @@ let classify_implicits (req,_ as obj) = match req with
type implicits_obj =
implicit_discharge_request *
- (global_reference * implicits_list list) list
+ (GlobRef.t * implicits_list list) list
let inImplicits : implicits_obj -> obj =
declare_object {(default_object "IMPLICITS") with
@@ -622,7 +640,7 @@ let inImplicits : implicits_obj -> obj =
let is_local local ref = local || isVarRef ref && is_in_section ref
let declare_implicits_gen req flags ref =
- let imps = compute_global_implicits flags [] ref in
+ let imps = compute_global_implicits flags ref in
add_anonymous_leaf (inImplicits (req,[ref,imps]))
let declare_implicits local ref =
@@ -643,7 +661,7 @@ let declare_mib_implicits kn =
let flags = !implicit_args in
let imps = Array.map_to_list
(fun (ind,cstrs) -> ind::(Array.to_list cstrs))
- (compute_mib_implicits flags [] kn) in
+ (compute_mib_implicits flags kn) in
add_anonymous_leaf
(inImplicits (ImplMutualInductive (kn,flags),List.flatten imps))
@@ -653,8 +671,8 @@ type manual_explicitation = Constrexpr.explicitation * (bool * bool * bool)
type manual_implicits = manual_explicitation list
let compute_implicits_with_manual env sigma typ enriching l =
- let _,autoimpls = compute_auto_implicits env sigma !implicit_args enriching typ in
- set_manual_implicits env !implicit_args enriching autoimpls l
+ let autoimpls = compute_auto_implicits env sigma !implicit_args enriching typ in
+ set_manual_implicits !implicit_args enriching autoimpls l
let check_inclusion l =
(* Check strict inclusion *)
@@ -671,34 +689,34 @@ let check_rigidity isrigid =
user_err (strbrk "Multiple sequences of implicit arguments available only for references that cannot be applied to an arbitrarily large number of arguments.")
let projection_implicits env p impls =
- let pb = Environ.lookup_projection p env in
- CList.skipn_at_least pb.Declarations.proj_npars impls
+ let npars = Projection.npars p in
+ CList.skipn_at_least npars impls
let declare_manual_implicits local ref ?enriching l =
let flags = !implicit_args in
let env = Global.env () in
let sigma = Evd.from_env env in
let t, _ = Global.type_of_global_in_context env ref in
+ let t = of_constr t in
let enriching = Option.default flags.auto enriching in
- let isrigid,autoimpls = compute_auto_implicits env sigma flags enriching (of_constr t) in
+ let autoimpls = compute_auto_implicits env sigma flags enriching t in
let l' = match l with
| [] -> assert false
| [l] ->
- [DefaultImpArgs, set_manual_implicits env flags enriching autoimpls l]
+ [DefaultImpArgs, set_manual_implicits flags enriching autoimpls l]
| _ ->
- check_rigidity isrigid;
- let l = List.map (fun imps -> (imps,List.length imps)) l in
- let l = List.sort (fun (_,n1) (_,n2) -> n2 - n1) l in
- check_inclusion l;
- let nargs = List.length autoimpls in
- List.map (fun (imps,n) ->
- (LessArgsThan (nargs-n),
- set_manual_implicits env flags enriching autoimpls imps)) l in
+ check_rigidity (is_rigid env sigma t);
+ let l = List.map (fun imps -> (imps,List.length imps)) l in
+ let l = List.sort (fun (_,n1) (_,n2) -> n2 - n1) l in
+ check_inclusion l;
+ let nargs = List.length autoimpls in
+ List.map (fun (imps,n) ->
+ (LessArgsThan (nargs-n),
+ set_manual_implicits flags enriching autoimpls imps)) l in
let req =
if is_local local ref then ImplLocal
else ImplInteractive(ref,flags,ImplManual (List.length autoimpls))
- in
- add_anonymous_leaf (inImplicits (req,[ref,l']))
+ in add_anonymous_leaf (inImplicits (req,[ref,l']))
let maybe_declare_manual_implicits local ref ?enriching l =
match l with
diff --git a/interp/impargs.mli b/interp/impargs.mli
index 103a4f9e..ea5aa90f 100644
--- a/interp/impargs.mli
+++ b/interp/impargs.mli
@@ -10,7 +10,6 @@
open Names
open EConstr
-open Globnames
open Environ
(** {6 Implicit Arguments } *)
@@ -103,7 +102,7 @@ val declare_var_implicits : variable -> unit
val declare_constant_implicits : Constant.t -> unit
val declare_mib_implicits : MutInd.t -> unit
-val declare_implicits : bool -> global_reference -> unit
+val declare_implicits : bool -> GlobRef.t -> unit
(** [declare_manual_implicits local ref enriching l]
Manual declaration of which arguments are expected implicit.
@@ -111,15 +110,15 @@ val declare_implicits : bool -> global_reference -> unit
implicits depending on the current state.
Unsets implicits if [l] is empty. *)
-val declare_manual_implicits : bool -> global_reference -> ?enriching:bool ->
+val declare_manual_implicits : bool -> GlobRef.t -> ?enriching:bool ->
manual_implicits list -> unit
(** If the list is empty, do nothing, otherwise declare the implicits. *)
-val maybe_declare_manual_implicits : bool -> global_reference -> ?enriching:bool ->
+val maybe_declare_manual_implicits : bool -> GlobRef.t -> ?enriching:bool ->
manual_implicits -> unit
-val implicits_of_global : global_reference -> implicits_list list
+val implicits_of_global : GlobRef.t -> implicits_list list
val extract_impargs_data :
implicits_list list -> ((int * int) option * implicit_status list) list
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 58df9abc..4f3037b1 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -17,12 +17,14 @@ open Glob_term
open Constrexpr
open Libnames
open Typeclasses
-open Typeclasses_errors
open Pp
open Libobject
open Nameops
open Context.Rel.Declaration
+exception MismatchedContextInstance of Environ.env * Typeclasses_errors.contexts * constr_expr list * Constr.rel_context (* found, expected *)
+let mismatched_ctx_inst_err env c n m = raise (MismatchedContextInstance (env, c, n, m))
+
module RelDecl = Context.Rel.Declaration
(*i*)
@@ -51,14 +53,14 @@ let cache_generalizable_type (_,(local,cmd)) =
let load_generalizable_type _ (_,(local,cmd)) =
generalizable_table := add_generalizable cmd !generalizable_table
-let in_generalizable : bool * Misctypes.lident list option -> obj =
+let in_generalizable : bool * lident list option -> obj =
declare_object {(default_object "GENERALIZED-IDENT") with
load_function = load_generalizable_type;
cache_function = cache_generalizable_type;
classify_function = (fun (local, _ as obj) -> if local then Dispose else Keep obj)
}
-let declare_generalizable local gen =
+let declare_generalizable ~local gen =
Lib.add_anonymous_leaf (in_generalizable (local, gen))
let find_generalizable_ident id = Id.Pred.mem (root_of_id id) !generalizable_table
@@ -94,9 +96,11 @@ let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l =
else l
in
let rec aux bdvars l c = match CAst.(c.v) with
- | CRef ({CAst.v=Ident id},_) -> found c.CAst.loc id bdvars l
- | CNotation ("{ _ : _ | _ }", ({ CAst.v = CRef ({CAst.v=Ident id},_) } :: _, [], [], [])) when not (Id.Set.mem id bdvars) ->
- Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux (Id.Set.add id bdvars) l c
+ | CRef (qid,_) when qualid_is_ident qid ->
+ found c.CAst.loc (qualid_basename qid) bdvars l
+ | CNotation ((InConstrEntrySomeLevel,"{ _ : _ | _ }"), ({ CAst.v = CRef (qid,_) } :: _, [], [], [])) when
+ qualid_is_ident qid && not (Id.Set.mem (qualid_basename qid) bdvars) ->
+ Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux (Id.Set.add (qualid_basename qid) bdvars) l c
| _ -> Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux bdvars l c
in aux bound l c
@@ -194,7 +198,7 @@ let combine_params avoid fn applied needed =
let combine_params_freevar =
fun avoid (_, decl) ->
let id' = next_name_away_from (RelDecl.get_name decl) avoid in
- (CAst.make @@ CRef (CAst.make @@ Ident id',None), Id.Set.add id' avoid)
+ (CAst.make @@ CRef (qualid_of_ident id',None), Id.Set.add id' avoid)
let destClassApp cl =
let open CAst in
@@ -216,9 +220,8 @@ let destClassAppExpl cl =
let implicit_application env ?(allow_partial=true) f ty =
let is_class =
try
- let ({CAst.v=(r, _, _)} as clapp) = destClassAppExpl ty in
- let qid = qualid_of_reference r in
- let gr = Nametab.locate qid.CAst.v in
+ let ({CAst.v=(qid, _, _)} as clapp) = destClassAppExpl ty in
+ let gr = Nametab.locate qid in
if Typeclasses.is_class gr then Some (clapp, gr) else None
with Not_found -> None
in
@@ -238,7 +241,7 @@ let implicit_application env ?(allow_partial=true) f ty =
let applen = List.fold_left (fun acc (x, y) -> opt_succ y acc) 0 par in
let needlen = List.fold_left (fun acc x -> opt_succ x acc) 0 ci in
if not (Int.equal needlen applen) then
- Typeclasses_errors.mismatched_ctx_inst (Global.env ()) Parameters (List.map fst par) rd
+ mismatched_ctx_inst_err (Global.env ()) Typeclasses_errors.Parameters (List.map fst par) rd
end;
let pars = List.rev (List.combine ci rd) in
let args, avoid = combine_params avoid f par pars in
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index b9815f34..437fef17 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -12,13 +12,12 @@ open Names
open Glob_term
open Constrexpr
open Libnames
-open Globnames
-val declare_generalizable : Vernacexpr.locality_flag -> Misctypes.lident list option -> unit
+val declare_generalizable : local:bool -> lident list option -> unit
val ids_of_list : Id.t list -> Id.Set.t
-val destClassApp : constr_expr -> (reference * constr_expr list * instance_expr option) CAst.t
-val destClassAppExpl : constr_expr -> (reference * (constr_expr * explicitation CAst.t option) list * instance_expr option) CAst.t
+val destClassApp : constr_expr -> (qualid * constr_expr list * instance_expr option) CAst.t
+val destClassAppExpl : constr_expr -> (qualid * (constr_expr * explicitation CAst.t option) list * instance_expr option) CAst.t
(** Fragile, should be used only for construction a set of identifiers to avoid *)
@@ -32,17 +31,21 @@ val free_vars_of_binders :
order with the location of their first occurrence *)
val generalizable_vars_of_glob_constr : ?bound:Id.Set.t -> ?allowed:Id.Set.t ->
- glob_constr -> Misctypes.lident list
+ glob_constr -> lident list
val make_fresh : Id.Set.t -> Environ.env -> Id.t -> Id.t
val implicits_of_glob_constr : ?with_products:bool -> Glob_term.glob_constr -> Impargs.manual_implicits
val combine_params_freevar :
- Id.Set.t -> global_reference option * Context.Rel.Declaration.t ->
+ Id.Set.t -> GlobRef.t option * Constr.rel_declaration ->
Constrexpr.constr_expr * Id.Set.t
val implicit_application : Id.Set.t -> ?allow_partial:bool ->
- (Id.Set.t -> global_reference option * Context.Rel.Declaration.t ->
+ (Id.Set.t -> GlobRef.t option * Constr.rel_declaration ->
Constrexpr.constr_expr * Id.Set.t) ->
constr_expr -> constr_expr * Id.Set.t
+
+(* Should be likely located elsewhere *)
+exception MismatchedContextInstance of Environ.env * Typeclasses_errors.contexts * constr_expr list * Constr.rel_context (* found, expected *)
+val mismatched_ctx_inst_err : Environ.env -> Typeclasses_errors.contexts -> constr_expr list -> Constr.rel_context -> 'a
diff --git a/interp/interp.mllib b/interp/interp.mllib
index bb22cf46..3668455a 100644
--- a/interp/interp.mllib
+++ b/interp/interp.mllib
@@ -1,14 +1,16 @@
+Constrexpr
+Genredexpr
+Redops
Tactypes
Stdarg
Genintern
+Notation_term
Notation_ops
Notation
Syntax_def
Smartlocate
Constrexpr_ops
-Ppextend
Dumpglob
-Topconstr
Reserve
Impargs
Implicit_quantifiers
diff --git a/interp/modintern.ml b/interp/modintern.ml
index dc93d8dc..c27cc9cc 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -12,7 +12,7 @@ open Declarations
open Libnames
open Constrexpr
open Constrintern
-open Misctypes
+open Declaremods
type module_internalization_error =
| NotAModuleNorModtype of string
@@ -23,7 +23,7 @@ exception ModuleInternalizationError of module_internalization_error
let error_not_a_module_loc kind loc qid =
let s = string_of_qualid qid in
- let e = match kind with
+ let e = let open Declaremods in match kind with
| Module -> Modops.ModuleTypingError (Modops.NotAModule s)
| ModType -> Modops.ModuleTypingError (Modops.NotAModuleType s)
| ModAny -> ModuleInternalizationError (NotAModuleNorModtype s)
@@ -45,7 +45,9 @@ let error_application_to_module_type loc =
or both are searched. The returned kind is never ModAny, and
it is equal to the input kind when this one isn't ModAny. *)
-let lookup_module_or_modtype kind {CAst.loc;v=qid} =
+let lookup_module_or_modtype kind qid =
+ let open Declaremods in
+ let loc = qid.CAst.loc in
try
if kind == ModType then raise Not_found;
let mp = Nametab.locate_module qid in
@@ -63,7 +65,7 @@ let transl_with_decl env = function
| CWith_Module ({CAst.v=fqid},qid) ->
WithMod (fqid,lookup_module qid), Univ.ContextSet.empty
| CWith_Definition ({CAst.v=fqid},udecl,c) ->
- let sigma, udecl = Univdecls.interp_univ_decl_opt env udecl in
+ let sigma, udecl = Constrexpr_ops.interp_univ_decl_opt env udecl in
let c, ectx = interp_constr env sigma c in
begin match UState.check_univ_decl ~poly:(Flags.is_universe_polymorphism()) ectx udecl with
| Entries.Polymorphic_const_entry ctx ->
@@ -83,7 +85,7 @@ let loc_of_module l = l.CAst.loc
let rec interp_module_ast env kind m cst = match m with
| {CAst.loc;v=CMident qid} ->
- let (mp,kind) = lookup_module_or_modtype kind CAst.(make ?loc qid) in
+ let (mp,kind) = lookup_module_or_modtype kind qid in
(MEident mp, kind, cst)
| {CAst.loc;v=CMapply (me1,me2)} ->
let me1',kind1, cst = interp_module_ast env kind me1 cst in
diff --git a/interp/modintern.mli b/interp/modintern.mli
index ef37aead..529c438c 100644
--- a/interp/modintern.mli
+++ b/interp/modintern.mli
@@ -11,7 +11,6 @@
open Environ
open Entries
open Constrexpr
-open Misctypes
(** Module internalization errors *)
@@ -30,4 +29,4 @@ exception ModuleInternalizationError of module_internalization_error
isn't ModAny. *)
val interp_module_ast :
- env -> module_kind -> module_ast -> module_struct_entry * module_kind * Univ.ContextSet.t
+ env -> Declaremods.module_kind -> module_ast -> module_struct_entry * Declaremods.module_kind * Univ.ContextSet.t
diff --git a/interp/notation.ml b/interp/notation.ml
index bb58f00c..e2751865 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -20,7 +20,6 @@ open Constrexpr
open Notation_term
open Glob_term
open Glob_ops
-open Ppextend
open Context.Named.Declaration
(*i*)
@@ -40,6 +39,30 @@ open Context.Named.Declaration
expression, set this scope to be the current scope
*)
+let notation_entry_eq s1 s2 = match (s1,s2) with
+| InConstrEntry, InConstrEntry -> true
+| InCustomEntry s1, InCustomEntry s2 -> String.equal s1 s2
+| (InConstrEntry | InCustomEntry _), _ -> false
+
+let notation_entry_level_eq s1 s2 = match (s1,s2) with
+| InConstrEntrySomeLevel, InConstrEntrySomeLevel -> true
+| InCustomEntryLevel (s1,n1), InCustomEntryLevel (s2,n2) -> String.equal s1 s2 && n1 = n2
+| (InConstrEntrySomeLevel | InCustomEntryLevel _), _ -> false
+
+let notation_eq (from1,ntn1) (from2,ntn2) =
+ notation_entry_level_eq from1 from2 && String.equal ntn1 ntn2
+
+let pr_notation (from,ntn) = qstring ntn ++ match from with InConstrEntrySomeLevel -> mt () | InCustomEntryLevel (s,n) -> str " in custom " ++ str s
+
+module NotationOrd =
+ struct
+ type t = notation
+ let compare = Pervasives.compare
+ end
+
+module NotationSet = Set.Make(NotationOrd)
+module NotationMap = CMap.Make(NotationOrd)
+
(**********************************************************************)
(* Scope of symbols *)
@@ -52,13 +75,10 @@ type notation_data = {
}
type scope = {
- notations: notation_data String.Map.t;
+ notations: notation_data NotationMap.t;
delimiters: delimiters option
}
-(* Uninterpreted notation map: notation -> level * DirPath.t *)
-let notation_level_map = ref String.Map.empty
-
(* Scopes table: scope_name -> symbol_interpretation *)
let scope_map = ref String.Map.empty
@@ -66,7 +86,7 @@ let scope_map = ref String.Map.empty
let delimiters_map = ref String.Map.empty
let empty_scope = {
- notations = String.Map.empty;
+ notations = NotationMap.empty;
delimiters = None
}
@@ -78,41 +98,6 @@ let init_scope_map () =
(**********************************************************************)
(* Operations on scopes *)
-let parenRelation_eq t1 t2 = match t1, t2 with
-| L, L | E, E | Any, Any -> true
-| Prec l1, Prec l2 -> Int.equal l1 l2
-| _ -> false
-
-open Extend
-
-let production_level_eq l1 l2 = true (* (l1 = l2) *)
-
-let production_position_eq pp1 pp2 = true (* pp1 = pp2 *) (* match pp1, pp2 with
-| NextLevel, NextLevel -> true
-| NumLevel n1, NumLevel n2 -> Int.equal n1 n2
-| (NextLevel | NumLevel _), _ -> false *)
-
-let constr_entry_key_eq eq v1 v2 = match v1, v2 with
-| ETName, ETName -> true
-| ETReference, ETReference -> true
-| ETBigint, ETBigint -> true
-| ETBinder b1, ETBinder b2 -> b1 == b2
-| ETConstr lev1, ETConstr lev2 -> eq lev1 lev2
-| ETConstrAsBinder (bk1,lev1), ETConstrAsBinder (bk2,lev2) -> eq lev1 lev2 && bk1 = bk2
-| ETPattern (b1,n1), ETPattern (b2,n2) -> b1 = b2 && Option.equal Int.equal n1 n2
-| ETOther (s1,s1'), ETOther (s2,s2') -> String.equal s1 s2 && String.equal s1' s2'
-| (ETName | ETReference | ETBigint | ETBinder _ | ETConstr _ | ETPattern _ | ETOther _ | ETConstrAsBinder _), _ -> false
-
-let level_eq_gen strict (l1, t1, u1) (l2, t2, u2) =
- let tolerability_eq (i1, r1) (i2, r2) = Int.equal i1 i2 && parenRelation_eq r1 r2 in
- let prod_eq (l1,pp1) (l2,pp2) =
- if strict then production_level_eq l1 l2 && production_position_eq pp1 pp2
- else production_level_eq l1 l2 in
- Int.equal l1 l2 && List.equal tolerability_eq t1 t2
- && List.equal (constr_entry_key_eq prod_eq) u1 u2
-
-let level_eq = level_eq_gen false
-
let declare_scope scope =
try let _ = String.Map.find scope !scope_map in ()
with Not_found ->
@@ -143,12 +128,12 @@ let normalize_scope sc =
(**********************************************************************)
(* The global stack of scopes *)
-type scope_elem = Scope of scope_name | SingleNotation of string
+type scope_elem = Scope of scope_name | SingleNotation of notation
type scopes = scope_elem list
let scope_eq s1 s2 = match s1, s2 with
-| Scope s1, Scope s2
-| SingleNotation s1, SingleNotation s2 -> String.equal s1 s2
+| Scope s1, Scope s2 -> String.equal s1 s2
+| SingleNotation s1, SingleNotation s2 -> notation_eq s1 s2
| Scope _, SingleNotation _
| SingleNotation _, Scope _ -> false
@@ -200,8 +185,6 @@ let push_scope sc scopes = Scope sc :: scopes
let push_scopes = List.fold_right push_scope
-type local_scopes = tmp_scope_name option * scope_name list
-
let make_current_scopes (tmp_scope,scopes) =
Option.fold_right push_scope tmp_scope (push_scopes scopes !scope_stack)
@@ -258,7 +241,7 @@ type interp_rule =
according to the key of the pattern (adapted from Chet Murthy by HH) *)
type key =
- | RefKey of global_reference
+ | RefKey of GlobRef.t
| Oth
let key_compare k1 k2 = match k1, k2 with
@@ -283,16 +266,14 @@ let keymap_find key map =
(* Scopes table : interpretation -> scope_name *)
let notations_key_table = ref (KeyMap.empty : notation_rule list KeyMap.t)
-let prim_token_key_table = ref (KeyMap.empty : (string * (any_glob_constr -> prim_token option) * bool) KeyMap.t)
-
let glob_prim_constr_key c = match DAst.get c with
- | GRef (ref, _) -> RefKey (canonical_gr ref)
+ | GRef (ref, _) -> Some (canonical_gr ref)
| GApp (c, _) ->
begin match DAst.get c with
- | GRef (ref, _) -> RefKey (canonical_gr ref)
- | _ -> Oth
+ | GRef (ref, _) -> Some (canonical_gr ref)
+ | _ -> None
end
- | _ -> Oth
+ | _ -> None
let glob_constr_keys c = match DAst.get c with
| GApp (c, _) ->
@@ -320,77 +301,521 @@ let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
(* Interpreting numbers (not in summary because functional objects) *)
type required_module = full_path * string list
+type rawnum = Constrexpr.raw_natural_number * Constrexpr.sign
-type 'a prim_token_interpreter =
- ?loc:Loc.t -> 'a -> glob_constr
+type prim_token_uid = string
-type cases_pattern_status = bool (* true = use prim token in patterns *)
+type 'a prim_token_interpreter = ?loc:Loc.t -> 'a -> glob_constr
+type 'a prim_token_uninterpreter = any_glob_constr -> 'a option
-type 'a prim_token_uninterpreter =
- glob_constr list * (any_glob_constr -> 'a option) * cases_pattern_status
+type 'a prim_token_interpretation =
+ 'a prim_token_interpreter * 'a prim_token_uninterpreter
-type internal_prim_token_interpreter =
- ?loc:Loc.t -> prim_token -> required_module * (unit -> glob_constr)
+module InnerPrimToken = struct
-let prim_token_interpreter_tab =
- (Hashtbl.create 7 : (scope_name, internal_prim_token_interpreter) Hashtbl.t)
+ type interpreter =
+ | RawNumInterp of (?loc:Loc.t -> rawnum -> glob_constr)
+ | BigNumInterp of (?loc:Loc.t -> Bigint.bigint -> glob_constr)
+ | StringInterp of (?loc:Loc.t -> string -> glob_constr)
-let add_prim_token_interpreter sc interp =
- try
- let cont = Hashtbl.find prim_token_interpreter_tab sc in
- Hashtbl.replace prim_token_interpreter_tab sc (interp cont)
- with Not_found ->
- let cont = (fun ?loc _p -> raise Not_found) in
- Hashtbl.add prim_token_interpreter_tab sc (interp cont)
+ let interp_eq f f' = match f,f' with
+ | RawNumInterp f, RawNumInterp f' -> f == f'
+ | BigNumInterp f, BigNumInterp f' -> f == f'
+ | StringInterp f, StringInterp f' -> f == f'
+ | _ -> false
-let declare_prim_token_interpreter sc interp (patl,uninterp,b) =
- declare_scope sc;
- add_prim_token_interpreter sc interp;
- List.iter (fun pat ->
- prim_token_key_table := KeyMap.add
- (glob_prim_constr_key pat) (sc,uninterp,b) !prim_token_key_table)
- patl
+ let ofNumeral n s =
+ if s then Bigint.of_string n else Bigint.neg (Bigint.of_string n)
+
+ let do_interp ?loc interp primtok =
+ match primtok, interp with
+ | Numeral (n,s), RawNumInterp interp -> interp ?loc (n,s)
+ | Numeral (n,s), BigNumInterp interp -> interp ?loc (ofNumeral n s)
+ | String s, StringInterp interp -> interp ?loc s
+ | _ -> raise Not_found
+
+ type uninterpreter =
+ | RawNumUninterp of (any_glob_constr -> rawnum option)
+ | BigNumUninterp of (any_glob_constr -> Bigint.bigint option)
+ | StringUninterp of (any_glob_constr -> string option)
+
+ let uninterp_eq f f' = match f,f' with
+ | RawNumUninterp f, RawNumUninterp f' -> f == f'
+ | BigNumUninterp f, BigNumUninterp f' -> f == f'
+ | StringUninterp f, StringUninterp f' -> f == f'
+ | _ -> false
+
+ let mkNumeral n =
+ if Bigint.is_pos_or_zero n then Numeral (Bigint.to_string n, true)
+ else Numeral (Bigint.to_string (Bigint.neg n), false)
-let mkNumeral n =
- if Bigint.is_pos_or_zero n then Numeral (Bigint.to_string n, true)
- else Numeral (Bigint.to_string (Bigint.neg n), false)
+ let mkString = function
+ | None -> None
+ | Some s -> if Unicode.is_utf8 s then Some (String s) else None
-let ofNumeral n s =
+ let do_uninterp uninterp g = match uninterp with
+ | RawNumUninterp u -> Option.map (fun (n,s) -> Numeral (n,s)) (u g)
+ | BigNumUninterp u -> Option.map mkNumeral (u g)
+ | StringUninterp u -> mkString (u g)
+
+end
+
+(* The following two tables of (un)interpreters will *not* be
+ synchronized. But their indexes will be checked to be unique.
+ These tables contain primitive token interpreters which are
+ registered in plugins, such as string and ascii syntax. It is
+ essential that only plugins add to these tables, and that
+ vernacular commands do not. See
+ https://github.com/coq/coq/issues/8401 for details of what goes
+ wrong when vernacular commands add to these tables. *)
+let prim_token_interpreters =
+ (Hashtbl.create 7 : (prim_token_uid, InnerPrimToken.interpreter) Hashtbl.t)
+
+let prim_token_uninterpreters =
+ (Hashtbl.create 7 : (prim_token_uid, InnerPrimToken.uninterpreter) Hashtbl.t)
+
+(*******************************************************)
+(* Numeral notation interpretation *)
+type numeral_notation_error =
+ | UnexpectedTerm of Constr.t
+ | UnexpectedNonOptionTerm of Constr.t
+
+exception NumeralNotationError of Environ.env * Evd.evar_map * numeral_notation_error
+
+type numnot_option =
+ | Nop
+ | Warning of raw_natural_number
+ | Abstract of raw_natural_number
+
+type int_ty =
+ { uint : Names.inductive;
+ int : Names.inductive }
+
+type z_pos_ty =
+ { z_ty : Names.inductive;
+ pos_ty : Names.inductive }
+
+type target_kind =
+ | Int of int_ty (* Coq.Init.Decimal.int + uint *)
+ | UInt of Names.inductive (* Coq.Init.Decimal.uint *)
+ | Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *)
+
+type option_kind = Option | Direct
+type conversion_kind = target_kind * option_kind
+
+type numeral_notation_obj =
+ { to_kind : conversion_kind;
+ to_ty : GlobRef.t;
+ of_kind : conversion_kind;
+ of_ty : GlobRef.t;
+ num_ty : Libnames.qualid; (* for warnings / error messages *)
+ warning : numnot_option }
+
+module Numeral = struct
+(** * Numeral notation *)
+
+(** Reduction
+
+ The constr [c] below isn't necessarily well-typed, since we
+ built it via an [mkApp] of a conversion function on a term
+ that starts with the right constructor but might be partially
+ applied.
+
+ At least [c] is known to be evar-free, since it comes from
+ our own ad-hoc [constr_of_glob] or from conversions such
+ as [coqint_of_rawnum].
+*)
+
+let eval_constr env sigma (c : Constr.t) =
+ let c = EConstr.of_constr c in
+ let sigma,t = Typing.type_of env sigma c in
+ let c' = Vnorm.cbv_vm env sigma c t in
+ EConstr.Unsafe.to_constr c'
+
+(* For testing with "compute" instead of "vm_compute" :
+let eval_constr env sigma (c : Constr.t) =
+ let c = EConstr.of_constr c in
+ let c' = Tacred.compute env sigma c in
+ EConstr.Unsafe.to_constr c'
+*)
+
+let eval_constr_app env sigma c1 c2 =
+ eval_constr env sigma (mkApp (c1,[| c2 |]))
+
+exception NotANumber
+
+let warn_large_num =
+ CWarnings.create ~name:"large-number" ~category:"numbers"
+ (fun ty ->
+ strbrk "Stack overflow or segmentation fault happens when " ++
+ strbrk "working with large numbers in " ++ pr_qualid ty ++
+ strbrk " (threshold may vary depending" ++
+ strbrk " on your system limits and on the command executed).")
+
+let warn_abstract_large_num =
+ CWarnings.create ~name:"abstract-large-number" ~category:"numbers"
+ (fun (ty,f) ->
+ strbrk "To avoid stack overflow, large numbers in " ++
+ pr_qualid ty ++ strbrk " are interpreted as applications of " ++
+ Nametab.pr_global_env (Termops.vars_of_env (Global.env ())) f ++ strbrk ".")
+
+(** Comparing two raw numbers (base 10, big-endian, non-negative).
+ A bit nasty, but not critical: only used to decide when a
+ number is considered as large (see warnings above). *)
+
+exception Comp of int
+
+let rec rawnum_compare s s' =
+ let l = String.length s and l' = String.length s' in
+ if l < l' then - rawnum_compare s' s
+ else
+ let d = l-l' in
+ try
+ for i = 0 to d-1 do if s.[i] != '0' then raise (Comp 1) done;
+ for i = d to l-1 do
+ let c = Pervasives.compare s.[i] s'.[i-d] in
+ if c != 0 then raise (Comp c)
+ done;
+ 0
+ with Comp c -> c
+
+(***********************************************************************)
+
+(** ** Conversion between Coq [Decimal.int] and internal raw string *)
+
+(** Decimal.Nil has index 1, then Decimal.D0 has index 2 .. Decimal.D9 is 11 *)
+
+let digit_of_char c =
+ assert ('0' <= c && c <= '9');
+ Char.code c - Char.code '0' + 2
+
+let char_of_digit n =
+ assert (2<=n && n<=11);
+ Char.chr (n-2 + Char.code '0')
+
+let coquint_of_rawnum uint str =
+ let nil = mkConstruct (uint,1) in
+ let rec do_chars s i acc =
+ if i < 0 then acc
+ else
+ let dg = mkConstruct (uint, digit_of_char s.[i]) in
+ do_chars s (i-1) (mkApp(dg,[|acc|]))
+ in
+ do_chars str (String.length str - 1) nil
+
+let coqint_of_rawnum inds (str,sign) =
+ let uint = coquint_of_rawnum inds.uint str in
+ mkApp (mkConstruct (inds.int, if sign then 1 else 2), [|uint|])
+
+let rawnum_of_coquint c =
+ let rec of_uint_loop c buf =
+ match Constr.kind c with
+ | Construct ((_,1), _) (* Nil *) -> ()
+ | App (c, [|a|]) ->
+ (match Constr.kind c with
+ | Construct ((_,n), _) (* D0 to D9 *) ->
+ let () = Buffer.add_char buf (char_of_digit n) in
+ of_uint_loop a buf
+ | _ -> raise NotANumber)
+ | _ -> raise NotANumber
+ in
+ let buf = Buffer.create 64 in
+ let () = of_uint_loop c buf in
+ if Int.equal (Buffer.length buf) 0 then
+ (* To avoid ambiguities between Nil and (D0 Nil), we choose
+ to not display Nil alone as "0" *)
+ raise NotANumber
+ else Buffer.contents buf
+
+let rawnum_of_coqint c =
+ match Constr.kind c with
+ | App (c,[|c'|]) ->
+ (match Constr.kind c with
+ | Construct ((_,1), _) (* Pos *) -> (rawnum_of_coquint c', true)
+ | Construct ((_,2), _) (* Neg *) -> (rawnum_of_coquint c', false)
+ | _ -> raise NotANumber)
+ | _ -> raise NotANumber
+
+
+(***********************************************************************)
+
+(** ** Conversion between Coq [Z] and internal bigint *)
+
+(** First, [positive] from/to bigint *)
+
+let rec pos_of_bigint posty n =
+ match Bigint.div2_with_rest n with
+ | (q, false) ->
+ let c = mkConstruct (posty, 2) in (* xO *)
+ mkApp (c, [| pos_of_bigint posty q |])
+ | (q, true) when not (Bigint.equal q Bigint.zero) ->
+ let c = mkConstruct (posty, 1) in (* xI *)
+ mkApp (c, [| pos_of_bigint posty q |])
+ | (q, true) ->
+ mkConstruct (posty, 3) (* xH *)
+
+let rec bigint_of_pos c = match Constr.kind c with
+ | Construct ((_, 3), _) -> (* xH *) Bigint.one
+ | App (c, [| d |]) ->
+ begin match Constr.kind c with
+ | Construct ((_, n), _) ->
+ begin match n with
+ | 1 -> (* xI *) Bigint.add_1 (Bigint.mult_2 (bigint_of_pos d))
+ | 2 -> (* xO *) Bigint.mult_2 (bigint_of_pos d)
+ | n -> assert false (* no other constructor of type positive *)
+ end
+ | x -> raise NotANumber
+ end
+ | x -> raise NotANumber
+
+(** Now, [Z] from/to bigint *)
+
+let z_of_bigint { z_ty; pos_ty } n =
+ if Bigint.equal n Bigint.zero then
+ mkConstruct (z_ty, 1) (* Z0 *)
+ else
+ let (s, n) =
+ if Bigint.is_pos_or_zero n then (2, n) (* Zpos *)
+ else (3, Bigint.neg n) (* Zneg *)
+ in
+ let c = mkConstruct (z_ty, s) in
+ mkApp (c, [| pos_of_bigint pos_ty n |])
+
+let bigint_of_z z = match Constr.kind z with
+ | Construct ((_, 1), _) -> (* Z0 *) Bigint.zero
+ | App (c, [| d |]) ->
+ begin match Constr.kind c with
+ | Construct ((_, n), _) ->
+ begin match n with
+ | 2 -> (* Zpos *) bigint_of_pos d
+ | 3 -> (* Zneg *) Bigint.neg (bigint_of_pos d)
+ | n -> assert false (* no other constructor of type Z *)
+ end
+ | _ -> raise NotANumber
+ end
+ | _ -> raise NotANumber
+
+(** The uninterp function below work at the level of [glob_constr]
+ which is too low for us here. So here's a crude conversion back
+ to [constr] for the subset that concerns us. *)
+
+let rec constr_of_glob env sigma g = match DAst.get g with
+ | Glob_term.GRef (ConstructRef c, _) ->
+ let sigma,c = Evd.fresh_constructor_instance env sigma c in
+ sigma,mkConstructU c
+ | Glob_term.GApp (gc, gcl) ->
+ let sigma,c = constr_of_glob env sigma gc in
+ let sigma,cl = List.fold_left_map (constr_of_glob env) sigma gcl in
+ sigma,mkApp (c, Array.of_list cl)
+ | _ ->
+ raise NotANumber
+
+let rec glob_of_constr ?loc env sigma c = match Constr.kind c with
+ | App (c, ca) ->
+ let c = glob_of_constr ?loc env sigma c in
+ let cel = List.map (glob_of_constr ?loc env sigma) (Array.to_list ca) in
+ DAst.make ?loc (Glob_term.GApp (c, cel))
+ | Construct (c, _) -> DAst.make ?loc (Glob_term.GRef (ConstructRef c, None))
+ | Const (c, _) -> DAst.make ?loc (Glob_term.GRef (ConstRef c, None))
+ | Ind (ind, _) -> DAst.make ?loc (Glob_term.GRef (IndRef ind, None))
+ | Var id -> DAst.make ?loc (Glob_term.GRef (VarRef id, None))
+ | _ -> Loc.raise ?loc (NumeralNotationError(env,sigma,UnexpectedTerm c))
+
+let no_such_number ?loc ty =
+ CErrors.user_err ?loc
+ (str "Cannot interpret this number as a value of type " ++
+ pr_qualid ty)
+
+let interp_option ty ?loc env sigma c =
+ match Constr.kind c with
+ | App (_Some, [| _; c |]) -> glob_of_constr ?loc env sigma c
+ | App (_None, [| _ |]) -> no_such_number ?loc ty
+ | x -> Loc.raise ?loc (NumeralNotationError(env,sigma,UnexpectedNonOptionTerm c))
+
+let uninterp_option c =
+ match Constr.kind c with
+ | App (_Some, [| _; x |]) -> x
+ | _ -> raise NotANumber
+
+let big2raw n =
+ if Bigint.is_pos_or_zero n then (Bigint.to_string n, true)
+ else (Bigint.to_string (Bigint.neg n), false)
+
+let raw2big (n,s) =
if s then Bigint.of_string n else Bigint.neg (Bigint.of_string n)
-let mkString = function
-| None -> None
-| Some s -> if Unicode.is_utf8 s then Some (String s) else None
+let interp o ?loc n =
+ begin match o.warning with
+ | Warning threshold when snd n && rawnum_compare (fst n) threshold >= 0 ->
+ warn_large_num o.num_ty
+ | _ -> ()
+ end;
+ let c = match fst o.to_kind with
+ | Int int_ty -> coqint_of_rawnum int_ty n
+ | UInt uint_ty when snd n -> coquint_of_rawnum uint_ty (fst n)
+ | UInt _ (* n <= 0 *) -> no_such_number ?loc o.num_ty
+ | Z z_pos_ty -> z_of_bigint z_pos_ty (raw2big n)
+ in
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ let sigma,to_ty = Evd.fresh_global env sigma o.to_ty in
+ let to_ty = EConstr.Unsafe.to_constr to_ty in
+ match o.warning, snd o.to_kind with
+ | Abstract threshold, Direct when rawnum_compare (fst n) threshold >= 0 ->
+ warn_abstract_large_num (o.num_ty,o.to_ty);
+ glob_of_constr ?loc env sigma (mkApp (to_ty,[|c|]))
+ | _ ->
+ let res = eval_constr_app env sigma to_ty c in
+ match snd o.to_kind with
+ | Direct -> glob_of_constr ?loc env sigma res
+ | Option -> interp_option o.num_ty ?loc env sigma res
+
+let uninterp o (Glob_term.AnyGlobConstr n) =
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ let sigma,of_ty = Evd.fresh_global env sigma o.of_ty in
+ let of_ty = EConstr.Unsafe.to_constr of_ty in
+ try
+ let sigma,n = constr_of_glob env sigma n in
+ let c = eval_constr_app env sigma of_ty n in
+ let c = if snd o.of_kind == Direct then c else uninterp_option c in
+ match fst o.of_kind with
+ | Int _ -> Some (rawnum_of_coqint c)
+ | UInt _ -> Some (rawnum_of_coquint c, true)
+ | Z _ -> Some (big2raw (bigint_of_z c))
+ with
+ | Type_errors.TypeError _ | Pretype_errors.PretypeError _ -> None (* cf. eval_constr_app *)
+ | NotANumber -> None (* all other functions except big2raw *)
+end
+
+(* A [prim_token_infos], which is synchronized with the document
+ state, either contains a unique id pointing to an unsynchronized
+ prim token function, or a numeral notation object describing how to
+ interpret and uninterpret. We provide [prim_token_infos] because
+ we expect plugins to provide their own interpretation functions,
+ rather than going through numeral notations, which are available as
+ a vernacular. *)
+
+type prim_token_interp_info =
+ Uid of prim_token_uid
+ | NumeralNotation of numeral_notation_obj
+
+type prim_token_infos = {
+ pt_local : bool; (** Is this interpretation local? *)
+ pt_scope : scope_name; (** Concerned scope *)
+ pt_interp_info : prim_token_interp_info; (** Unique id "pointing" to (un)interp functions, OR a numeral notation object describing (un)interp functions *)
+ pt_required : required_module; (** Module that should be loaded first *)
+ pt_refs : GlobRef.t list; (** Entry points during uninterpretation *)
+ pt_in_match : bool (** Is this prim token legal in match patterns ? *)
+}
-let delay dir int ?loc x = (dir, (fun () -> int ?loc x))
+(* Table from scope_name to backtrack-able informations about interpreters
+ (in particular interpreter unique id). *)
+let prim_token_interp_infos =
+ ref (String.Map.empty : (required_module * prim_token_interp_info) String.Map.t)
+
+(* Table from global_reference to backtrack-able informations about
+ prim_token uninterpretation (in particular uninterpreter unique id). *)
+let prim_token_uninterp_infos =
+ ref (Refmap.empty : (scope_name * prim_token_interp_info * bool) Refmap.t)
+
+let hashtbl_check_and_set allow_overwrite uid f h eq =
+ match Hashtbl.find h uid with
+ | exception Not_found -> Hashtbl.add h uid f
+ | _ when allow_overwrite -> Hashtbl.add h uid f
+ | g when eq f g -> ()
+ | _ ->
+ user_err ~hdr:"prim_token_interpreter"
+ (str "Unique identifier " ++ str uid ++
+ str " already used to register a numeral or string (un)interpreter.")
+
+let register_gen_interpretation allow_overwrite uid (interp, uninterp) =
+ hashtbl_check_and_set
+ allow_overwrite uid interp prim_token_interpreters InnerPrimToken.interp_eq;
+ hashtbl_check_and_set
+ allow_overwrite uid uninterp prim_token_uninterpreters InnerPrimToken.uninterp_eq
+
+let register_rawnumeral_interpretation ?(allow_overwrite=false) uid (interp, uninterp) =
+ register_gen_interpretation allow_overwrite uid
+ (InnerPrimToken.RawNumInterp interp, InnerPrimToken.RawNumUninterp uninterp)
+
+let register_bignumeral_interpretation ?(allow_overwrite=false) uid (interp, uninterp) =
+ register_gen_interpretation allow_overwrite uid
+ (InnerPrimToken.BigNumInterp interp, InnerPrimToken.BigNumUninterp uninterp)
+
+let register_string_interpretation ?(allow_overwrite=false) uid (interp, uninterp) =
+ register_gen_interpretation allow_overwrite uid
+ (InnerPrimToken.StringInterp interp, InnerPrimToken.StringUninterp uninterp)
+
+let cache_prim_token_interpretation (_,infos) =
+ let ptii = infos.pt_interp_info in
+ let sc = infos.pt_scope in
+ declare_scope sc;
+ prim_token_interp_infos :=
+ String.Map.add sc (infos.pt_required,ptii) !prim_token_interp_infos;
+ List.iter (fun r -> prim_token_uninterp_infos :=
+ Refmap.add r (sc,ptii,infos.pt_in_match)
+ !prim_token_uninterp_infos)
+ infos.pt_refs
+
+let subst_prim_token_interpretation (subs,infos) =
+ { infos with
+ pt_refs = List.map (subst_global_reference subs) infos.pt_refs }
+
+let classify_prim_token_interpretation infos =
+ if infos.pt_local then Dispose else Substitute infos
+
+let inPrimTokenInterp : prim_token_infos -> obj =
+ declare_object {(default_object "PRIM-TOKEN-INTERP") with
+ open_function = (fun i o -> if Int.equal i 1 then cache_prim_token_interpretation o);
+ cache_function = cache_prim_token_interpretation;
+ subst_function = subst_prim_token_interpretation;
+ classify_function = classify_prim_token_interpretation}
+
+let enable_prim_token_interpretation infos =
+ Lib.add_anonymous_leaf (inPrimTokenInterp infos)
+
+(** Compatibility.
+ Avoid the next two functions, they will now store unnecessary
+ objects in the library segment. Instead, combine
+ [register_*_interpretation] and [enable_prim_token_interpretation]
+ (the latter inside a [Mltop.declare_cache_obj]).
+*)
-type rawnum = Constrexpr.raw_natural_number * Constrexpr.sign
+let fresh_string_of =
+ let count = ref 0 in
+ fun root -> count := !count+1; (string_of_int !count)^"_"^root
+
+let declare_numeral_interpreter ?(local=false) sc dir interp (patl,uninterp,b) =
+ let uid = fresh_string_of sc in
+ register_bignumeral_interpretation uid (interp,uninterp);
+ enable_prim_token_interpretation
+ { pt_local = local;
+ pt_scope = sc;
+ pt_interp_info = Uid uid;
+ pt_required = dir;
+ pt_refs = List.map_filter glob_prim_constr_key patl;
+ pt_in_match = b }
+let declare_string_interpreter ?(local=false) sc dir interp (patl,uninterp,b) =
+ let uid = fresh_string_of sc in
+ register_string_interpretation uid (interp,uninterp);
+ enable_prim_token_interpretation
+ { pt_local = local;
+ pt_scope = sc;
+ pt_interp_info = Uid uid;
+ pt_required = dir;
+ pt_refs = List.map_filter glob_prim_constr_key patl;
+ pt_in_match = b }
-let declare_rawnumeral_interpreter sc dir interp (patl,uninterp,inpat) =
- declare_prim_token_interpreter sc
- (fun cont ?loc -> function Numeral (n,s) -> delay dir interp ?loc (n,s)
- | p -> cont ?loc p)
- (patl, (fun r -> match uninterp r with
- | None -> None
- | Some (n,s) -> Some (Numeral (n,s))), inpat)
-
-let declare_numeral_interpreter sc dir interp (patl,uninterp,inpat) =
- let interp' ?loc (n,s) = interp ?loc (ofNumeral n s) in
- declare_prim_token_interpreter sc
- (fun cont ?loc -> function Numeral (n,s) -> delay dir interp' ?loc (n,s)
- | p -> cont ?loc p)
- (patl, (fun r -> Option.map mkNumeral (uninterp r)), inpat)
-
-let declare_string_interpreter sc dir interp (patl,uninterp,inpat) =
- declare_prim_token_interpreter sc
- (fun cont ?loc -> function String s -> delay dir interp ?loc s | p -> cont ?loc p)
- (patl, (fun r -> mkString (uninterp r)), inpat)
let check_required_module ?loc sc (sp,d) =
try let _ = Nametab.global_of_path sp in ()
with Not_found ->
- user_err ?loc ~hdr:"prim_token_interpreter"
- (str "Cannot interpret in " ++ str sc ++ str " without requiring first module " ++ str (List.last d) ++ str ".")
+ match d with
+ | [] -> user_err ?loc ~hdr:"prim_token_interpreter"
+ (str "Cannot interpret in " ++ str sc ++ str " because " ++ pr_path sp ++ str " could not be found in the current environment.")
+ | _ -> 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 *)
@@ -418,7 +843,7 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function
end
| SingleNotation ntn' :: scopes ->
begin match ntn_scope, ntn with
- | None, Some ntn when String.equal ntn ntn' ->
+ | None, Some ntn when notation_eq ntn ntn' ->
Some (None, None)
| _ ->
find_without_delimiters find (ntn_scope,ntn) scopes
@@ -427,24 +852,12 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function
(* Can we switch to [scope]? Yes if it has defined delimiters *)
find_with_delimiters ntn_scope
-(* Uninterpreted notation levels *)
-
-let declare_notation_level ?(onlyprint=false) ntn level =
- if String.Map.mem ntn !notation_level_map then
- anomaly (str "Notation " ++ str ntn ++ str " is already assigned a level.");
- notation_level_map := String.Map.add ntn (level,onlyprint) !notation_level_map
-
-let level_of_notation ?(onlyprint=false) ntn =
- let (level,onlyprint') = String.Map.find ntn !notation_level_map in
- if onlyprint' && not onlyprint then raise Not_found;
- level
-
(* The mapping between notations and their interpretation *)
let warn_notation_overridden =
CWarnings.create ~name:"notation-overridden" ~category:"parsing"
(fun (ntn,which_scope) ->
- str "Notation" ++ spc () ++ str ntn ++ spc ()
+ str "Notation" ++ spc () ++ pr_notation ntn ++ spc ()
++ strbrk "was already used" ++ which_scope ++ str ".")
let declare_notation_interpretation ntn scopt pat df ~onlyprint =
@@ -452,7 +865,7 @@ let declare_notation_interpretation ntn scopt pat df ~onlyprint =
let sc = find_scope scope in
if not onlyprint then begin
let () =
- if String.Map.mem ntn sc.notations then
+ if NotationMap.mem ntn sc.notations then
let which_scope = match scopt with
| None -> mt ()
| Some _ -> spc () ++ strbrk "in scope" ++ spc () ++ str scope in
@@ -462,7 +875,7 @@ let declare_notation_interpretation ntn scopt pat df ~onlyprint =
not_interp = pat;
not_location = df;
} in
- let sc = { sc with notations = String.Map.add ntn notdata sc.notations } in
+ let sc = { sc with notations = NotationMap.add ntn notdata sc.notations } in
scope_map := String.Map.add scope sc !scope_map
end;
begin match scopt with
@@ -479,7 +892,7 @@ let rec find_interpretation ntn find = function
| Scope scope :: scopes ->
(try let (pat,df) = find scope in pat,(df,Some scope)
with Not_found -> find_interpretation ntn find scopes)
- | SingleNotation ntn'::scopes when String.equal ntn' ntn ->
+ | SingleNotation ntn'::scopes when notation_eq ntn' ntn ->
(try let (pat,df) = find default_scope in pat,(df,None)
with Not_found ->
(* e.g. because single notation only for constr, not cases_pattern *)
@@ -488,12 +901,12 @@ let rec find_interpretation ntn find = function
find_interpretation ntn find scopes
let find_notation ntn sc =
- let n = String.Map.find ntn (find_scope sc).notations in
+ let n = NotationMap.find ntn (find_scope sc).notations in
(n.not_interp, n.not_location)
let notation_of_prim_token = function
- | Numeral (n,true) -> n
- | Numeral (n,false) -> "- "^n
+ | Numeral (n,true) -> InConstrEntrySomeLevel, n
+ | Numeral (n,false) -> InConstrEntrySomeLevel, "- "^n
| String _ -> raise Not_found
let find_prim_token check_allowed ?loc p sc =
@@ -505,21 +918,25 @@ let find_prim_token check_allowed ?loc p sc =
pat, df
with Not_found ->
(* Try for a primitive numerical notation *)
- let (spdir,interp) = Hashtbl.find prim_token_interpreter_tab sc ?loc p in
+ let (spdir,info) = String.Map.find sc !prim_token_interp_infos in
check_required_module ?loc sc spdir;
- let pat = interp () in
+ let interp = match info with
+ | Uid uid -> Hashtbl.find prim_token_interpreters uid
+ | NumeralNotation o -> InnerPrimToken.RawNumInterp (Numeral.interp o)
+ in
+ let pat = InnerPrimToken.do_interp ?loc interp p in
check_allowed pat;
pat, ((dirpath (fst spdir),DirPath.empty),"")
let interp_prim_token_gen ?loc g 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
+ let p_as_ntn = try notation_of_prim_token p with Not_found -> InConstrEntrySomeLevel,"" in
try find_interpretation p_as_ntn (find_prim_token ?loc g p) scopes
with Not_found ->
user_err ?loc ~hdr:"interp_prim_token"
((match p with
| Numeral _ ->
- str "No interpretation for numeral " ++ str (notation_of_prim_token p)
+ str "No interpretation for numeral " ++ pr_notation (notation_of_prim_token p)
| String s -> str "No interpretation for string " ++ qs s) ++ str ".")
let interp_prim_token ?loc =
@@ -544,7 +961,7 @@ let interp_notation ?loc ntn local_scopes =
try find_interpretation ntn (find_notation ntn) scopes
with Not_found ->
user_err ?loc
- (str "Unknown interpretation for notation \"" ++ str ntn ++ str "\".")
+ (str "Unknown interpretation for notation " ++ pr_notation ntn ++ str ".")
let uninterp_notations c =
List.map_append (fun key -> keymap_find key !notations_key_table)
@@ -558,47 +975,161 @@ let uninterp_ind_pattern_notations ind =
let availability_of_notation (ntn_scope,ntn) scopes =
let f scope =
- String.Map.mem ntn (String.Map.find scope !scope_map).notations in
+ NotationMap.mem ntn (String.Map.find scope !scope_map).notations in
find_without_delimiters f (ntn_scope,Some ntn) (make_current_scopes scopes)
-let uninterp_prim_token c =
+(* We support coercions from a custom entry at some level to an entry
+ at some level (possibly the same), and from and to the constr entry. E.g.:
+
+ Notation "[ expr ]" := expr (expr custom group at level 1).
+ Notation "( x )" := x (in custom group at level 0, x at level 1).
+ Notation "{ x }" := x (in custom group at level 0, x constr).
+
+ Supporting any level is maybe overkill in that coercions are
+ commonly from the lowest level of the source entry to the highest
+ level of the target entry. *)
+
+type entry_coercion = notation list
+
+module EntryCoercionOrd =
+ struct
+ type t = notation_entry * notation_entry
+ let compare = Pervasives.compare
+ end
+
+module EntryCoercionMap = Map.Make(EntryCoercionOrd)
+
+let entry_coercion_map = ref EntryCoercionMap.empty
+
+let level_ord lev lev' =
+ match lev, lev' with
+ | None, _ -> true
+ | _, None -> true
+ | Some n, Some n' -> n <= n'
+
+let rec search nfrom nto = function
+ | [] -> raise Not_found
+ | ((pfrom,pto),coe)::l ->
+ if level_ord pfrom nfrom && level_ord nto pto then coe else search nfrom nto l
+
+let decompose_custom_entry = function
+ | InConstrEntrySomeLevel -> InConstrEntry, None
+ | InCustomEntryLevel (s,n) -> InCustomEntry s, Some n
+
+let availability_of_entry_coercion entry entry' =
+ let entry, lev = decompose_custom_entry entry in
+ let entry', lev' = decompose_custom_entry entry' in
+ if notation_entry_eq entry entry' && level_ord lev' lev then Some []
+ else
+ try Some (search lev lev' (EntryCoercionMap.find (entry,entry') !entry_coercion_map))
+ with Not_found -> None
+
+let better_path ((lev1,lev2),path) ((lev1',lev2'),path') =
+ (* better = shorter and lower source and higher target *)
+ level_ord lev1 lev1' && level_ord lev2' lev2 && List.length path <= List.length path'
+
+let shorter_path (_,path) (_,path') =
+ List.length path <= List.length path'
+
+let rec insert_coercion_path path = function
+ | [] -> [path]
+ | path'::paths as allpaths ->
+ (* If better or equal we keep the more recent one *)
+ if better_path path path' then path::paths
+ else if better_path path' path then allpaths
+ else if shorter_path path path' then path::allpaths
+ else path'::insert_coercion_path path paths
+
+let declare_entry_coercion (entry,_ as ntn) entry' =
+ let entry, lev = decompose_custom_entry entry in
+ let entry', lev' = decompose_custom_entry entry' in
+ (* Transitive closure *)
+ let toaddleft =
+ EntryCoercionMap.fold (fun (entry'',entry''') paths l ->
+ List.fold_right (fun ((lev'',lev'''),path) l ->
+ if notation_entry_eq entry entry''' && level_ord lev lev''' &&
+ not (notation_entry_eq entry' entry'')
+ then ((entry'',entry'),((lev'',lev'),path@[ntn]))::l else l) paths l)
+ !entry_coercion_map [] in
+ let toaddright =
+ EntryCoercionMap.fold (fun (entry'',entry''') paths l ->
+ List.fold_right (fun ((lev'',lev'''),path) l ->
+ if entry' = entry'' && level_ord lev' lev'' && entry <> entry'''
+ then ((entry,entry'''),((lev,lev'''),path@[ntn]))::l else l) paths l)
+ !entry_coercion_map [] in
+ entry_coercion_map :=
+ List.fold_right (fun (pair,path) ->
+ let olds = try EntryCoercionMap.find pair !entry_coercion_map with Not_found -> [] in
+ EntryCoercionMap.add pair (insert_coercion_path path olds))
+ (((entry,entry'),((lev,lev'),[ntn]))::toaddright@toaddleft)
+ !entry_coercion_map
+
+let entry_has_global_map = ref String.Map.empty
+
+let declare_custom_entry_has_global s n =
try
- let (sc,numpr,_) =
- KeyMap.find (glob_prim_constr_key c) !prim_token_key_table in
- match numpr (AnyGlobConstr c) with
- | None -> raise Notation_ops.No_match
- | Some n -> (sc,n)
- with Not_found -> raise Notation_ops.No_match
-
-let uninterp_prim_token_ind_pattern ind args =
- let ref = IndRef ind in
+ let p = String.Map.find s !entry_has_global_map in
+ user_err (str "Custom entry " ++ str s ++
+ str " has already a rule for global references at level " ++ int p ++ str ".")
+ with Not_found ->
+ entry_has_global_map := String.Map.add s n !entry_has_global_map
+
+let entry_has_global = function
+ | InConstrEntrySomeLevel -> true
+ | InCustomEntryLevel (s,n) ->
+ try String.Map.find s !entry_has_global_map <= n with Not_found -> false
+
+let entry_has_ident_map = ref String.Map.empty
+
+let declare_custom_entry_has_ident s n =
try
- let k = RefKey (canonical_gr ref) in
- let (sc,numpr,b) = KeyMap.find k !prim_token_key_table in
- if not b then raise Notation_ops.No_match;
- let args' = List.map
- (fun x -> snd (glob_constr_of_closed_cases_pattern x)) args in
- let ref = DAst.make @@ GRef (ref,None) in
- match numpr (AnyGlobConstr (DAst.make @@ GApp (ref,args'))) with
- | None -> raise Notation_ops.No_match
- | Some n -> (sc,n)
- with Not_found -> raise Notation_ops.No_match
+ let p = String.Map.find s !entry_has_ident_map in
+ user_err (str "Custom entry " ++ str s ++
+ str " has already a rule for global references at level " ++ int p ++ str ".")
+ with Not_found ->
+ entry_has_ident_map := String.Map.add s n !entry_has_ident_map
+
+let entry_has_ident = function
+ | InConstrEntrySomeLevel -> true
+ | InCustomEntryLevel (s,n) ->
+ try String.Map.find s !entry_has_ident_map <= n with Not_found -> false
+
+let uninterp_prim_token c =
+ match glob_prim_constr_key c with
+ | None -> raise Notation_ops.No_match
+ | Some r ->
+ try
+ let (sc,info,_) = Refmap.find r !prim_token_uninterp_infos in
+ let uninterp = match info with
+ | Uid uid -> Hashtbl.find prim_token_uninterpreters uid
+ | NumeralNotation o -> InnerPrimToken.RawNumUninterp (Numeral.uninterp o)
+ in
+ match InnerPrimToken.do_uninterp uninterp (AnyGlobConstr c) with
+ | None -> raise Notation_ops.No_match
+ | Some n -> (sc,n)
+ with Not_found -> raise Notation_ops.No_match
let uninterp_prim_token_cases_pattern c =
- try
- let k = cases_pattern_key c in
- let (sc,numpr,b) = KeyMap.find k !prim_token_key_table in
- if not b then raise Notation_ops.No_match;
- let na,c = glob_constr_of_closed_cases_pattern c in
- match numpr (AnyGlobConstr c) with
- | None -> raise Notation_ops.No_match
- | Some n -> (na,sc,n)
- with Not_found -> raise Notation_ops.No_match
+ match glob_constr_of_closed_cases_pattern c with
+ | exception Not_found -> raise Notation_ops.No_match
+ | na,c -> let (sc,n) = uninterp_prim_token c in (na,sc,n)
let availability_of_prim_token n printer_scope local_scopes =
let f scope =
- try ignore ((Hashtbl.find prim_token_interpreter_tab scope) n); true
- with Not_found -> false in
+ try
+ let uid = snd (String.Map.find scope !prim_token_interp_infos) in
+ let open InnerPrimToken in
+ match n, uid with
+ | Numeral _, NumeralNotation _ -> true
+ | _, NumeralNotation _ -> false
+ | _, Uid uid ->
+ let interp = Hashtbl.find prim_token_interpreters uid in
+ match n, interp with
+ | Numeral _, (RawNumInterp _ | BigNumInterp _) -> true
+ | String _, StringInterp _ -> true
+ | _ -> false
+ with Not_found -> false
+ in
let scopes = make_current_scopes local_scopes in
Option.map snd (find_without_delimiters f (Some printer_scope,None) scopes)
@@ -619,7 +1150,8 @@ let ntpe_eq t1 t2 = match t1, t2 with
| NtnTypeBinderList, NtnTypeBinderList -> true
| (NtnTypeConstr | NtnTypeBinder _ | NtnTypeConstrList | NtnTypeBinderList), _ -> false
-let var_attributes_eq (_, (sc1, tp1)) (_, (sc2, tp2)) =
+let var_attributes_eq (_, ((entry1, sc1), tp1)) (_, ((entry2, sc2), tp2)) =
+ notation_entry_level_eq entry1 entry2 &&
pair_eq (Option.equal String.equal) (List.equal String.equal) sc1 sc2 &&
ntpe_eq tp1 tp2
@@ -631,7 +1163,7 @@ let exists_notation_in_scope scopt ntn onlyprint r =
let scope = match scopt with Some s -> s | None -> default_scope in
try
let sc = String.Map.find scope !scope_map in
- let n = String.Map.find ntn sc.notations in
+ let n = NotationMap.find ntn sc.notations in
interpretation_eq n.not_interp r
with Not_found -> false
@@ -741,7 +1273,7 @@ let subst_arguments_scope (subst,(req,r,n,scl,cls)) =
match subst_scope_class subst cl with
| Some cl' as ocl' when cl' != cl -> ocl'
| _ -> ocl in
- let cls' = List.smartmap subst_cl cls in
+ let cls' = List.Smart.map subst_cl cls in
(ArgsScopeNoDischarge,r',n,scl,cls')
let discharge_arguments_scope (_,(req,r,n,l,_)) =
@@ -778,7 +1310,7 @@ let rebuild_arguments_scope sigma (req,r,n,l,_) =
(req,r,0,l1@l,cls1)
type arguments_scope_obj =
- arguments_scope_discharge_request * global_reference *
+ arguments_scope_discharge_request * GlobRef.t *
(* Used to communicate information from discharge to rebuild *)
(* set to 0 otherwise *) int *
scope_name option list * scope_class option list
@@ -847,10 +1379,10 @@ let rec string_of_symbol = function
let l = List.flatten (List.map string_of_symbol l) in "_"::l@".."::l@["_"]
| Break _ -> []
-let make_notation_key symbols =
- String.concat " " (List.flatten (List.map string_of_symbol symbols))
+let make_notation_key from symbols =
+ (from,String.concat " " (List.flatten (List.map string_of_symbol symbols)))
-let decompose_notation_key s =
+let decompose_notation_key (from,s) =
let len = String.length s in
let rec decomp_ntn dirs n =
if n>=len then List.rev dirs else
@@ -865,7 +1397,7 @@ let decompose_notation_key s =
| s -> Terminal (String.drop_simple_quotes s) in
decomp_ntn (tok::dirs) (pos+1)
in
- decomp_ntn [] 0
+ from, decomp_ntn [] 0
(************)
(* Printing *)
@@ -894,14 +1426,14 @@ let pr_notation_info prglob ntn c =
let pr_named_scope prglob scope sc =
(if String.equal scope default_scope then
- match String.Map.cardinal sc.notations with
+ match NotationMap.cardinal sc.notations with
| 0 -> str "No lonely notation"
| n -> str "Lonely notation" ++ (if Int.equal n 1 then mt() else str"s")
else
str "Scope " ++ str scope ++ fnl () ++ pr_delimiters_info sc.delimiters)
++ fnl ()
++ pr_scope_classes scope
- ++ String.Map.fold
+ ++ NotationMap.fold
(fun ntn { not_interp = (_, r); not_location = (_, df) } strm ->
pr_notation_info prglob df r ++ fnl () ++ strm)
sc.notations (mt ())
@@ -916,11 +1448,11 @@ let pr_scopes prglob =
let rec find_default ntn = function
| [] -> None
| Scope scope :: scopes ->
- if String.Map.mem ntn (find_scope scope).notations then
+ if NotationMap.mem ntn (find_scope scope).notations then
Some scope
else find_default ntn scopes
| SingleNotation ntn' :: scopes ->
- if String.equal ntn ntn' then Some default_scope
+ if notation_eq ntn ntn' then Some default_scope
else find_default ntn scopes
let factorize_entries = function
@@ -929,7 +1461,7 @@ let factorize_entries = function
let (ntn,l_of_ntn,rest) =
List.fold_left
(fun (a',l,rest) (a,c) ->
- if String.equal a a' then (a',c::l,rest) else (a,[c],(a',l)::rest))
+ if notation_eq a a' then (a',c::l,rest) else (a,[c],(a',l)::rest))
(ntn,[c],[]) l in
(ntn,l_of_ntn)::rest
@@ -984,15 +1516,15 @@ let possible_notations ntn =
(* Only "_ U _" format *)
[ntn]
else
- let ntn' = make_notation_key (raw_analyze_notation_tokens toks) in
+ let _,ntn' = make_notation_key None (raw_analyze_notation_tokens toks) in
if String.equal ntn ntn' then (* Only symbols *) [ntn] else [ntn;ntn']
let browse_notation strict ntn map =
let ntns = possible_notations ntn in
- let find ntn' ntn =
+ let find (from,ntn' as fullntn') ntn =
if String.contains ntn ' ' then String.equal ntn ntn'
else
- let toks = decompose_notation_key ntn' in
+ let _,toks = decompose_notation_key fullntn' in
let get_terminals = function Terminal ntn -> Some ntn | _ -> None in
let trms = List.map_filter get_terminals toks in
if strict then String.List.equal [ntn] trms
@@ -1001,10 +1533,10 @@ let browse_notation strict ntn map =
let l =
String.Map.fold
(fun scope_name sc ->
- String.Map.fold (fun ntn { not_interp = (_, r); not_location = df } l ->
+ NotationMap.fold (fun ntn { not_interp = (_, r); not_location = df } l ->
if List.exists (find ntn) ntns then (ntn,(scope_name,r,df))::l else l) sc.notations)
map [] in
- List.sort (fun x y -> String.compare (fst x) (fst y)) l
+ List.sort (fun x y -> String.compare (snd (fst x)) (snd (fst y))) l
let global_reference_of_notation test (ntn,(sc,c,_)) =
match c with
@@ -1065,9 +1597,9 @@ let locate_notation prglob ntn scope =
let collect_notation_in_scope scope sc known =
assert (not (String.equal scope default_scope));
- String.Map.fold
+ NotationMap.fold
(fun ntn { not_interp = (_, r); not_location = (_, df) } (l,known as acc) ->
- if String.List.mem ntn known then acc else ((df,r)::l,ntn::known))
+ if List.mem_f notation_eq ntn known then acc else ((df,r)::l,ntn::known))
sc.notations ([],known)
let collect_notations stack =
@@ -1080,10 +1612,10 @@ let collect_notations stack =
collect_notation_in_scope scope (find_scope scope) knownntn in
((scope,l)::all,knownntn)
| SingleNotation ntn ->
- if String.List.mem ntn knownntn then (all,knownntn)
+ if List.mem_f notation_eq ntn knownntn then (all,knownntn)
else
let { not_interp = (_, r); not_location = (_, df) } =
- String.Map.find ntn (find_scope default_scope).notations in
+ NotationMap.find ntn (find_scope default_scope).notations in
let all' = match all with
| (s,lonelyntn)::rest when String.equal s default_scope ->
(s,(df,r)::lonelyntn)::rest
@@ -1113,64 +1645,35 @@ let pr_visibility prglob = function
| None -> pr_scope_stack prglob !scope_stack
(**********************************************************************)
-(* Mapping notations to concrete syntax *)
-
-type unparsing_rule = unparsing list * precedence
-type extra_unparsing_rules = (string * string) list
-(* Concrete syntax for symbolic-extension table *)
-let notation_rules =
- ref (String.Map.empty : (unparsing_rule * extra_unparsing_rules * notation_grammar) String.Map.t)
-
-let declare_notation_rule ntn ~extra unpl gram =
- notation_rules := String.Map.add ntn (unpl,extra,gram) !notation_rules
-
-let find_notation_printing_rule ntn =
- try pi1 (String.Map.find ntn !notation_rules)
- with Not_found -> anomaly (str "No printing rule found for " ++ str ntn ++ str ".")
-let find_notation_extra_printing_rules ntn =
- try pi2 (String.Map.find ntn !notation_rules)
- with Not_found -> []
-let find_notation_parsing_rules ntn =
- try pi3 (String.Map.find ntn !notation_rules)
- with Not_found -> anomaly (str "No parsing rule found for " ++ str ntn ++ str ".")
-
-let get_defined_notations () =
- String.Set.elements @@ String.Map.domain !notation_rules
-
-let add_notation_extra_printing_rule ntn k v =
- try
- notation_rules :=
- 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 ~hdr:"add_notation_extra_printing_rule"
- (str "No such Notation.")
-
-(**********************************************************************)
(* Synchronisation with reset *)
let freeze _ =
- (!scope_map, !notation_level_map, !scope_stack, !arguments_scope,
- !delimiters_map, !notations_key_table, !notation_rules,
- !scope_class_map)
+ (!scope_map, !scope_stack, !arguments_scope,
+ !delimiters_map, !notations_key_table, !scope_class_map,
+ !prim_token_interp_infos, !prim_token_uninterp_infos,
+ !entry_coercion_map, !entry_has_global_map,
+ !entry_has_ident_map)
-let unfreeze (scm,nlm,scs,asc,dlm,fkm,pprules,clsc) =
+let unfreeze (scm,scs,asc,dlm,fkm,clsc,ptii,ptui,coe,globs,ids) =
scope_map := scm;
- notation_level_map := nlm;
scope_stack := scs;
delimiters_map := dlm;
arguments_scope := asc;
notations_key_table := fkm;
- notation_rules := pprules;
- scope_class_map := clsc
+ scope_class_map := clsc;
+ prim_token_interp_infos := ptii;
+ prim_token_uninterp_infos := ptui;
+ entry_coercion_map := coe;
+ entry_has_global_map := globs;
+ entry_has_ident_map := ids
let init () =
init_scope_map ();
- notation_level_map := String.Map.empty;
delimiters_map := String.Map.empty;
notations_key_table := KeyMap.empty;
- notation_rules := String.Map.empty;
- scope_class_map := initial_scope_class_map
+ scope_class_map := initial_scope_class_map;
+ prim_token_interp_infos := String.Map.empty;
+ prim_token_uninterp_infos := Refmap.empty
let _ =
Summary.declare_summary "symbols"
diff --git a/interp/notation.mli b/interp/notation.mli
index 18671feb..eb080f57 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -8,17 +8,29 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-open Bigint
open Names
open Libnames
-open Globnames
open Constrexpr
open Glob_term
open Notation_term
-open Ppextend
(** Notations *)
+val pr_notation : notation -> Pp.t
+(** Printing *)
+
+val notation_entry_eq : notation_entry -> notation_entry -> bool
+(** Equality on [notation_entry]. *)
+
+val notation_entry_level_eq : notation_entry_level -> notation_entry_level -> bool
+(** Equality on [notation_entry_level]. *)
+
+val notation_eq : notation -> notation -> bool
+(** Equality on [notation]. *)
+
+module NotationSet : Set.S with type elt = notation
+module NotationMap : CMap.ExtS with type key = notation and module Set := NotationSet
+
(** {6 Scopes } *)
(** A scope is a set of interpreters for symbols + optional
interpreter and printers for integers + optional delimiters *)
@@ -27,14 +39,10 @@ type delimiters = string
type scope
type scopes (** = [scope_name list] *)
-type local_scopes = tmp_scope_name option * scope_name list
-
val declare_scope : scope_name -> unit
val current_scopes : unit -> scopes
-val level_eq : level -> level -> bool
-
(** Check where a scope is opened or not in a scope list, or in
* the current opened scopes *)
val scope_is_open_in_scopes : scope_name -> scopes -> bool
@@ -66,33 +74,112 @@ val find_delimiters_scope : ?loc:Loc.t -> delimiters -> scope_name
type notation_location = (DirPath.t * DirPath.t) * string
type required_module = full_path * string list
-type cases_pattern_status = bool (** true = use prim token in patterns *)
+type rawnum = Constrexpr.raw_natural_number * Constrexpr.sign
-type 'a prim_token_interpreter =
- ?loc:Loc.t -> 'a -> glob_constr
+(** The unique id string below will be used to refer to a particular
+ registered interpreter/uninterpreter of numeral or string notation.
+ Using the same uid for different (un)interpreters will fail.
+ If at most one interpretation of prim token is used per scope,
+ then the scope name could be used as unique id. *)
-type 'a prim_token_uninterpreter =
- glob_constr list * (any_glob_constr -> 'a option) * cases_pattern_status
+type prim_token_uid = string
-type rawnum = Constrexpr.raw_natural_number * Constrexpr.sign
+type 'a prim_token_interpreter = ?loc:Loc.t -> 'a -> glob_constr
+type 'a prim_token_uninterpreter = any_glob_constr -> 'a option
+
+type 'a prim_token_interpretation =
+ 'a prim_token_interpreter * 'a prim_token_uninterpreter
+
+val register_rawnumeral_interpretation :
+ ?allow_overwrite:bool -> prim_token_uid -> rawnum prim_token_interpretation -> unit
+
+val register_bignumeral_interpretation :
+ ?allow_overwrite:bool -> prim_token_uid -> Bigint.bigint prim_token_interpretation -> unit
+
+val register_string_interpretation :
+ ?allow_overwrite:bool -> prim_token_uid -> string prim_token_interpretation -> unit
+
+(** * Numeral notation *)
-val declare_rawnumeral_interpreter : scope_name -> required_module ->
- rawnum prim_token_interpreter -> rawnum prim_token_uninterpreter -> unit
+type numeral_notation_error =
+ | UnexpectedTerm of Constr.t
+ | UnexpectedNonOptionTerm of Constr.t
-val declare_numeral_interpreter : scope_name -> required_module ->
- bigint prim_token_interpreter -> bigint prim_token_uninterpreter -> unit
+exception NumeralNotationError of Environ.env * Evd.evar_map * numeral_notation_error
-val declare_string_interpreter : scope_name -> required_module ->
- string prim_token_interpreter -> string prim_token_uninterpreter -> unit
+type numnot_option =
+ | Nop
+ | Warning of raw_natural_number
+ | Abstract of raw_natural_number
+
+type int_ty =
+ { uint : Names.inductive;
+ int : Names.inductive }
+
+type z_pos_ty =
+ { z_ty : Names.inductive;
+ pos_ty : Names.inductive }
+
+type target_kind =
+ | Int of int_ty (* Coq.Init.Decimal.int + uint *)
+ | UInt of Names.inductive (* Coq.Init.Decimal.uint *)
+ | Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *)
+
+type option_kind = Option | Direct
+type conversion_kind = target_kind * option_kind
+
+type numeral_notation_obj =
+ { to_kind : conversion_kind;
+ to_ty : GlobRef.t;
+ of_kind : conversion_kind;
+ of_ty : GlobRef.t;
+ num_ty : Libnames.qualid; (* for warnings / error messages *)
+ warning : numnot_option }
+
+type prim_token_interp_info =
+ Uid of prim_token_uid
+ | NumeralNotation of numeral_notation_obj
+
+type prim_token_infos = {
+ pt_local : bool; (** Is this interpretation local? *)
+ pt_scope : scope_name; (** Concerned scope *)
+ pt_interp_info : prim_token_interp_info; (** Unique id "pointing" to (un)interp functions, OR a numeral notation object describing (un)interp functions *)
+ pt_required : required_module; (** Module that should be loaded first *)
+ pt_refs : GlobRef.t list; (** Entry points during uninterpretation *)
+ pt_in_match : bool (** Is this prim token legal in match patterns ? *)
+}
+
+(** Note: most of the time, the [pt_refs] field above will contain
+ inductive constructors (e.g. O and S for nat). But it could also be
+ injection functions such as IZR for reals. *)
+
+(** Activate a prim token interpretation whose unique id and functions
+ have already been registered. *)
+
+val enable_prim_token_interpretation : prim_token_infos -> unit
+
+(** Compatibility.
+ Avoid the next two functions, they will now store unnecessary
+ objects in the library segment. Instead, combine
+ [register_*_interpretation] and [enable_prim_token_interpretation]
+ (the latter inside a [Mltop.declare_cache_obj]).
+*)
+
+val declare_numeral_interpreter : ?local:bool -> scope_name -> required_module ->
+ Bigint.bigint prim_token_interpreter ->
+ glob_constr list * Bigint.bigint prim_token_uninterpreter * bool -> unit
+val declare_string_interpreter : ?local:bool -> scope_name -> required_module ->
+ string prim_token_interpreter ->
+ glob_constr list * string prim_token_uninterpreter * bool -> unit
(** Return the [term]/[cases_pattern] bound to a primitive token in a
given scope context*)
-val interp_prim_token : ?loc:Loc.t -> prim_token -> local_scopes ->
+val interp_prim_token : ?loc:Loc.t -> prim_token -> subscopes ->
glob_constr * (notation_location * scope_name option)
(* This function returns a glob_const representing a pattern *)
-val interp_prim_token_cases_pattern_expr : ?loc:Loc.t -> (global_reference -> unit) -> prim_token ->
- local_scopes -> glob_constr * (notation_location * scope_name option)
+val interp_prim_token_cases_pattern_expr : ?loc:Loc.t -> (GlobRef.t -> unit) -> prim_token ->
+ subscopes -> glob_constr * (notation_location * scope_name option)
(** Return the primitive token associated to a [term]/[cases_pattern];
raise [No_match] if no such token *)
@@ -101,11 +188,9 @@ val uninterp_prim_token :
'a glob_constr_g -> scope_name * prim_token
val uninterp_prim_token_cases_pattern :
'a cases_pattern_g -> Name.t * scope_name * prim_token
-val uninterp_prim_token_ind_pattern :
- inductive -> cases_pattern list -> scope_name * prim_token
val availability_of_prim_token :
- prim_token -> scope_name -> local_scopes -> delimiters option option
+ prim_token -> scope_name -> subscopes -> delimiters option option
(** {6 Declare and interpret back and forth a notation } *)
@@ -120,7 +205,7 @@ val declare_notation_interpretation : notation -> scope_name option ->
val declare_uninterpretation : interp_rule -> interpretation -> unit
(** Return the interpretation bound to a notation *)
-val interp_notation : ?loc:Loc.t -> notation -> local_scopes ->
+val interp_notation : ?loc:Loc.t -> notation -> subscopes ->
interpretation * (notation_location * scope_name option)
type notation_rule = interp_rule * interpretation * int option
@@ -133,18 +218,13 @@ val uninterp_ind_pattern_notations : inductive -> notation_rule list
(** Test if a notation is available in the scopes
context [scopes]; if available, the result is not None; the first
argument is itself not None if a delimiters is needed *)
-val availability_of_notation : scope_name option * notation -> local_scopes ->
+val availability_of_notation : scope_name option * notation -> subscopes ->
(scope_name option * delimiters option) option
-(** {6 Declare and test the level of a (possibly uninterpreted) notation } *)
-
-val declare_notation_level : ?onlyprint:bool -> notation -> level -> unit
-val level_of_notation : ?onlyprint:bool -> notation -> level (** raise [Not_found] if no level or not respecting onlyprint *)
-
(** {6 Miscellaneous} *)
-val interp_notation_as_global_reference : ?loc:Loc.t -> (global_reference -> bool) ->
- notation -> delimiters option -> global_reference
+val interp_notation_as_global_reference : ?loc:Loc.t -> (GlobRef.t -> bool) ->
+ notation_key -> delimiters option -> GlobRef.t
(** Checks for already existing notations *)
val exists_notation_in_scope : scope_name option -> notation ->
@@ -152,9 +232,9 @@ val exists_notation_in_scope : scope_name option -> notation ->
(** Declares and looks for scopes associated to arguments of a global ref *)
val declare_arguments_scope :
- bool (** true=local *) -> global_reference -> scope_name option list -> unit
+ bool (** true=local *) -> GlobRef.t -> scope_name option list -> unit
-val find_arguments_scope : global_reference -> scope_name option list
+val find_arguments_scope : GlobRef.t -> scope_name option list
type scope_class
@@ -165,7 +245,7 @@ val subst_scope_class :
Mod_subst.substitution -> scope_class -> scope_class option
val declare_scope_class : scope_name -> scope_class -> unit
-val declare_ref_arguments_scope : Evd.evar_map -> global_reference -> unit
+val declare_ref_arguments_scope : Evd.evar_map -> GlobRef.t -> unit
val compute_arguments_scope : Evd.evar_map -> EConstr.types -> scope_name option list
val compute_type_scope : Evd.evar_map -> EConstr.types -> scope_name option
@@ -186,8 +266,8 @@ type symbol =
val symbol_eq : symbol -> symbol -> bool
(** Make/decompose a notation of the form "_ U _" *)
-val make_notation_key : symbol list -> notation
-val decompose_notation_key : notation -> symbol list
+val make_notation_key : notation_entry_level -> symbol list -> notation
+val decompose_notation_key : notation -> notation_entry_level * symbol list
(** Decompose a notation of the form "a 'U' b" *)
val decompose_raw_notation : string -> symbol list
@@ -196,25 +276,20 @@ val decompose_raw_notation : string -> symbol list
val pr_scope_class : scope_class -> Pp.t
val pr_scope : (glob_constr -> Pp.t) -> scope_name -> Pp.t
val pr_scopes : (glob_constr -> Pp.t) -> Pp.t
-val locate_notation : (glob_constr -> Pp.t) -> notation ->
+val locate_notation : (glob_constr -> Pp.t) -> notation_key ->
scope_name option -> Pp.t
val pr_visibility: (glob_constr -> Pp.t) -> scope_name option -> Pp.t
-(** {6 Printing rules for notations} *)
+type entry_coercion = notation list
+val declare_entry_coercion : notation -> notation_entry_level -> unit
+val availability_of_entry_coercion : notation_entry_level -> notation_entry_level -> entry_coercion option
-(** Declare and look for the printing rule for symbolic notations *)
-type unparsing_rule = unparsing list * precedence
-type extra_unparsing_rules = (string * string) list
-val declare_notation_rule :
- notation -> extra:extra_unparsing_rules -> unparsing_rule -> notation_grammar -> unit
-val find_notation_printing_rule : notation -> unparsing_rule
-val find_notation_extra_printing_rules : notation -> extra_unparsing_rules
-val find_notation_parsing_rules : notation -> notation_grammar
-val add_notation_extra_printing_rule : notation -> string -> string -> unit
+val declare_custom_entry_has_global : string -> int -> unit
+val declare_custom_entry_has_ident : string -> int -> unit
-(** Returns notations with defined parsing/printing rules *)
-val get_defined_notations : unit -> notation list
+val entry_has_global : notation_entry_level -> bool
+val entry_has_ident : notation_entry_level -> bool
(** Rem: printing rules for primitive token are canonical *)
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 55e532dc..7a525f84 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -13,9 +13,10 @@ open CErrors
open Util
open Names
open Nameops
+open Constr
open Globnames
open Decl_kinds
-open Misctypes
+open Namegen
open Glob_term
open Glob_ops
open Mod_subst
@@ -28,7 +29,7 @@ open Notation_term
let get_var_ndx id vs = try Some (List.index Id.equal id vs) with Not_found -> None
let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with
-| NRef gr1, NRef gr2 -> eq_gr gr1 gr2
+| NRef gr1, NRef gr2 -> GlobRef.equal gr1 gr2
| NVar id1, NVar id2 -> (
match (get_var_ndx id1 vars1,get_var_ndx id2 vars2) with
| Some n,Some m -> Int.equal n m
@@ -85,12 +86,12 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with
Array.equal (eq_notation_constr vars) us1 us2 &&
Array.equal (eq_notation_constr vars) rs1 rs2
| NSort s1, NSort s2 ->
- Miscops.glob_sort_eq s1 s2
+ glob_sort_eq s1 s2
| NCast (t1, c1), NCast (t2, c2) ->
(eq_notation_constr vars) t1 t2 && cast_type_eq (eq_notation_constr vars) c1 c2
| (NRef _ | NVar _ | NApp _ | NHole _ | NList _ | NLambda _ | NProd _
| NBinderList _ | NLetIn _ | NCases _ | NLetTuple _ | NIf _
- | NRec _ | NSort _ | NCast _), _ -> false
+ | NRec _ | NSort _ | NCast _ ), _ -> false
(**********************************************************************)
(* Re-interpret a notation as a glob_constr, taking care of binders *)
@@ -152,10 +153,12 @@ let protect g e na =
if disjpat <> None then user_err (Pp.str "Unsupported substitution of an arbitrary pattern.");
e',na
-let apply_cases_pattern ?loc ((ids,disjpat),id) c =
- let tm = DAst.make ?loc (GVar id) in
+let apply_cases_pattern_term ?loc (ids,disjpat) tm c =
let eqns = List.map (fun pat -> (CAst.make ?loc (ids,[pat],c))) disjpat in
- DAst.make ?loc @@ GCases (LetPatternStyle, None, [tm,(Anonymous,None)], eqns)
+ DAst.make ?loc @@ GCases (Constr.LetPatternStyle, None, [tm,(Anonymous,None)], eqns)
+
+let apply_cases_pattern ?loc (ids_disjpat,id) c =
+ apply_cases_pattern_term ?loc ids_disjpat (DAst.make ?loc (GVar id)) c
let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
let lt x = DAst.make ?loc x in lt @@ match nc with
@@ -181,7 +184,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
let e',disjpat,na = g e na in
(match disjpat with
| None -> GLetIn (na,f e b,Option.map (f e) t,f e' c)
- | Some disjpat -> DAst.get (apply_cases_pattern ?loc disjpat (f e' c)))
+ | Some (disjpat,_id) -> DAst.get (apply_cases_pattern_term ?loc disjpat (f e b) (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
@@ -213,7 +216,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
(e,(na,Explicit,Option.map (f e) oc,f e b)))) e dll in
let e',idl = Array.fold_left_map (to_id (protect g)) e idl in
GRec (fk,idl,dll,Array.map (f e) tl,Array.map (f e') bl)
- | NCast (c,k) -> GCast (f e c,Miscops.map_cast_type (f e) k)
+ | NCast (c,k) -> GCast (f e c,map_cast_type (f e) k)
| NSort x -> GSort x
| NHole (x, naming, arg) -> GHole (x, naming, arg)
| NRef x -> GRef (x,None)
@@ -430,7 +433,7 @@ let notation_constr_and_vars_of_glob_constr recvars a =
user_err Pp.(str "Binders marked as implicit not allowed in notations.");
add_name found na; (na,Option.map aux oc,aux b))) dll in
NRec (fk,idl,dll,Array.map aux tl,Array.map aux bl)
- | GCast (c,k) -> NCast (aux c,Miscops.map_cast_type aux k)
+ | GCast (c,k) -> NCast (aux c,map_cast_type aux k)
| GSort s -> NSort s
| GHole (w,naming,arg) ->
if arg != None then has_ltac := true;
@@ -505,7 +508,9 @@ let notation_constr_of_glob_constr nenv a =
let notation_constr_of_constr avoiding t =
let t = EConstr.of_constr t in
- let t = Detyping.detype Detyping.Now false avoiding (Global.env()) Evd.empty t in
+ let env = Global.env () in
+ let evd = Evd.from_env env in
+ let t = Detyping.detype Detyping.Now false avoiding env evd t in
let nenv = {
ninterp_var_type = Id.Map.empty;
ninterp_rec_vars = Id.Map.empty;
@@ -517,7 +522,7 @@ let rec subst_pat subst pat =
| PatVar _ -> pat
| PatCstr (((kn,i),j),cpl,n) ->
let kn' = subst_mind subst kn
- and cpl' = List.smartmap (subst_pat subst) cpl in
+ and cpl' = List.Smart.map (subst_pat subst) cpl in
if kn' == kn && cpl' == cpl then pat else
DAst.make ?loc:pat.CAst.loc @@ PatCstr (((kn',i),j),cpl',n)
@@ -532,7 +537,7 @@ let rec subst_notation_constr subst bound raw =
| NApp (r,rl) ->
let r' = subst_notation_constr subst bound r
- and rl' = List.smartmap (subst_notation_constr subst bound) rl in
+ and rl' = List.Smart.map (subst_notation_constr subst bound) rl in
if r' == r && rl' == rl then raw else
NApp(r',rl')
@@ -562,14 +567,14 @@ let rec subst_notation_constr subst bound raw =
| 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 t' = Option.Smart.map (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
- and rl' = List.smartmap
+ let rtntypopt' = Option.Smart.map (subst_notation_constr subst bound) rtntypopt
+ and rl' = List.Smart.map
(fun (a,(n,signopt) as x) ->
let a' = subst_notation_constr subst bound a in
let signopt' = Option.map (fun ((indkn,i),nal as z) ->
@@ -577,9 +582,9 @@ let rec subst_notation_constr subst bound raw =
if indkn == indkn' then z else ((indkn',i),nal)) signopt in
if a' == a && signopt' == signopt then x else (a',(n,signopt')))
rl
- and branches' = List.smartmap
+ and branches' = List.Smart.map
(fun (cpl,r as branch) ->
- let cpl' = List.smartmap (subst_pat subst) cpl
+ let cpl' = List.Smart.map (subst_pat subst) cpl
and r' = subst_notation_constr subst bound r in
if cpl' == cpl && r' == r then branch else
(cpl',r'))
@@ -590,14 +595,14 @@ let rec subst_notation_constr subst bound raw =
NCases (sty,rtntypopt',rl',branches')
| NLetTuple (nal,(na,po),b,c) ->
- let po' = Option.smartmap (subst_notation_constr subst bound) po
+ let po' = Option.Smart.map (subst_notation_constr subst bound) po
and b' = subst_notation_constr subst bound b
and c' = subst_notation_constr subst bound c in
if po' == po && b' == b && c' == c then raw else
NLetTuple (nal,(na,po'),b',c')
| NIf (c,(na,po),b1,b2) ->
- let po' = Option.smartmap (subst_notation_constr subst bound) po
+ let po' = Option.Smart.map (subst_notation_constr subst bound) po
and b1' = subst_notation_constr subst bound b1
and b2' = subst_notation_constr subst bound b2
and c' = subst_notation_constr subst bound c in
@@ -606,12 +611,12 @@ let rec subst_notation_constr subst bound raw =
| NRec (fk,idl,dll,tl,bl) ->
let dll' =
- Array.smartmap (List.smartmap (fun (na,oc,b as x) ->
- let oc' = Option.smartmap (subst_notation_constr subst bound) oc in
+ Array.Smart.map (List.Smart.map (fun (na,oc,b as x) ->
+ let oc' = Option.Smart.map (subst_notation_constr subst bound) oc in
let b' = subst_notation_constr subst bound b in
if oc' == oc && b' == b then x else (na,oc',b'))) dll in
- let tl' = Array.smartmap (subst_notation_constr subst bound) tl in
- let bl' = Array.smartmap (subst_notation_constr subst bound) bl in
+ let tl' = Array.Smart.map (subst_notation_constr subst bound) tl in
+ let bl' = Array.Smart.map (subst_notation_constr subst bound) bl in
if dll' == dll && tl' == tl && bl' == bl then raw else
NRec (fk,idl,dll',tl',bl')
@@ -624,13 +629,13 @@ let rec subst_notation_constr subst bound raw =
if nref == ref then knd else Evar_kinds.ImplicitArg (nref, i, b)
| _ -> knd
in
- let nsolve = Option.smartmap (Genintern.generic_substitute subst) solve in
+ let nsolve = Option.Smart.map (Genintern.generic_substitute subst) solve in
if nsolve == solve && nknd == knd then raw
else NHole (nknd, naming, nsolve)
| NCast (r1,k) ->
let r1' = subst_notation_constr subst bound r1 in
- let k' = Miscops.smartmap_cast_type (subst_notation_constr subst bound) k in
+ let k' = smartmap_cast_type (subst_notation_constr subst bound) k in
if r1' == r1 && k' == k then raw else NCast(r1',k')
let subst_interpretation subst (metas,pat) =
@@ -651,11 +656,11 @@ let abstract_return_type_context pi mklam tml rtno =
let abstract_return_type_context_glob_constr tml rtn =
abstract_return_type_context (fun {CAst.v=(_,nal)} -> nal)
(fun na c -> DAst.make @@
- GLambda(na,Explicit,DAst.make @@ GHole(Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None),c)) tml rtn
+ GLambda(na,Explicit,DAst.make @@ GHole(Evar_kinds.InternalHole,IntroAnonymous,None),c)) tml rtn
let abstract_return_type_context_notation_constr tml rtn =
abstract_return_type_context snd
- (fun na c -> NLambda(na,NHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None),c)) tml rtn
+ (fun na c -> NLambda(na,NHole (Evar_kinds.InternalHole, IntroAnonymous, None),c)) tml rtn
let is_term_meta id metas =
try match Id.List.assoc id metas with _,(NtnTypeConstr | NtnTypeConstrList) -> true | _ -> false
@@ -672,7 +677,7 @@ let is_onlybinding_meta id metas =
let is_onlybinding_pattern_like_meta isvar id metas =
try match Id.List.assoc id metas with
| _,NtnTypeBinder (NtnBinderParsedAsConstr
- (Extend.AsIdentOrPattern | Extend.AsStrictPattern)) -> true
+ (AsIdentOrPattern | AsStrictPattern)) -> true
| _,NtnTypeBinder (NtnParsedAsPattern strict) -> not (strict && isvar)
| _ -> false
with Not_found -> false
@@ -887,7 +892,9 @@ let bind_term_as_binding_env alp (terms,termlists,binders,binderlists as sigma)
| GVar id' ->
(if not (Id.equal id id') then (fst alp,(id,id')::snd alp) else alp),
sigma
- | _ -> anomaly (str "A term which can be a binder has to be a variable.")
+ | t ->
+ (* The term is a non-variable pattern *)
+ raise No_match
with Not_found ->
(* The matching against a term allowing to find the instance has not been found yet *)
(* If it will be a different name, we shall unfortunately fail *)
@@ -995,9 +1002,9 @@ let remove_sigma x (terms,termlists,binders,binderlists) =
let remove_bindinglist_sigma x (terms,termlists,binders,binderlists) =
(terms,termlists,binders,Id.List.remove_assoc x binderlists)
-let add_ldots_var metas = (ldots_var,((None,[]),NtnTypeConstr))::metas
+let add_ldots_var metas = (ldots_var,((Constrexpr.InConstrEntrySomeLevel,(None,[])),NtnTypeConstr))::metas
-let add_meta_bindinglist x metas = (x,((None,[]),NtnTypeBinderList))::metas
+let add_meta_bindinglist x metas = (x,((Constrexpr.InConstrEntrySomeLevel,(None,[])),NtnTypeBinderList))::metas
(* This tells if letins in the middle of binders should be included in
the sequence of binders *)
@@ -1042,7 +1049,7 @@ let match_binderlist match_fun alp metas sigma rest x y iter termin revert =
let alp,sigma = bind_bindinglist_env alp sigma x bl in
match_fun alp metas sigma rest termin
-let add_meta_term x metas = (x,((None,[]),NtnTypeConstr))::metas
+let add_meta_term x metas = (x,((Constrexpr.InConstrEntrySomeLevel,(None,[])),NtnTypeConstr))::metas (* Should reuse the scope of the partner of x! *)
let match_termlist match_fun alp metas sigma rest x y iter termin revert =
let rec aux sigma acc rest =
@@ -1111,7 +1118,7 @@ let rec match_ inner u alp metas sigma a1 a2 =
(* Matching compositionally *)
| GVar id1, NVar id2 when alpha_var id1 id2 (fst alp) -> sigma
- | GRef (r1,_), NRef r2 when (eq_gr r1 r2) -> sigma
+ | GRef (r1,_), NRef r2 when (GlobRef.equal r1 r2) -> sigma
| GApp (f1,l1), NApp (f2,l2) ->
let n1 = List.length l1 and n2 = List.length l2 in
let f1,l1,f2,l2 =
@@ -1179,7 +1186,7 @@ let rec match_ inner u alp metas sigma a1 a2 =
| GCast(t1, c1), NCast(t2, c2) ->
match_cast (match_in u alp metas) (match_in u alp metas sigma t1 t2) c1 c2
| GSort (GType _), NSort (GType _) when not u -> sigma
- | GSort s1, NSort s2 when Miscops.glob_sort_eq s1 s2 -> sigma
+ | GSort s1, NSort s2 when glob_sort_eq s1 s2 -> sigma
| GPatVar _, NHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match
| a, NHole _ -> sigma
@@ -1193,7 +1200,7 @@ let rec match_ inner u alp metas sigma a1 a2 =
let avoid =
Id.Set.union (free_glob_vars a1) (* as in Namegen: *) (glob_visible_short_qualid a1) in
let id' = Namegen.next_ident_away id avoid in
- let t1 = DAst.make @@ GHole(Evar_kinds.BinderType (Name id'),Misctypes.IntroAnonymous,None) in
+ let t1 = DAst.make @@ GHole(Evar_kinds.BinderType (Name id'),IntroAnonymous,None) in
let sigma = match t2 with
| NHole _ -> sigma
| NVar id2 -> bind_term_env alp sigma id2 t1
@@ -1207,7 +1214,7 @@ let rec match_ inner u alp metas sigma a1 a2 =
| (GRef _ | GVar _ | GEvar _ | GPatVar _ | GApp _ | GLambda _ | GProd _
| GLetIn _ | GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _
- | GCast _), _ -> raise No_match
+ | GCast _ ), _ -> raise No_match
and match_in u = match_ true u
@@ -1223,7 +1230,7 @@ and match_extended_binders ?loc isprod u alp metas na1 na2 bk t sigma b1 b2 =
let store, get = set_temporary_memory () in
match na1, DAst.get b1, na2 with
(* Matching individual binders as part of a recursive pattern *)
- | Name p, GCases (LetPatternStyle,None,[(e,_)],(_::_ as eqns)), Name id
+ | Name p, GCases (Constr.LetPatternStyle,None,[(e,_)],(_::_ as eqns)), Name id
when is_gvar p e && is_bindinglist_meta id metas && List.length (store (Detyping.factorize_eqns eqns)) = 1 ->
(match get () with
| [{CAst.v=(ids,disj_of_patl,b1)}] ->
diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index f038b5be..58fa221b 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -53,18 +53,18 @@ val glob_constr_of_notation_constr : ?loc:Loc.t -> notation_constr -> glob_const
exception No_match
val match_notation_constr : bool -> 'a glob_constr_g -> interpretation ->
- ('a glob_constr_g * subscopes) list * ('a glob_constr_g list * subscopes) list *
- ('a cases_pattern_disjunction_g * subscopes) list *
- ('a extended_glob_local_binder_g list * subscopes) list
+ ('a glob_constr_g * extended_subscopes) list * ('a glob_constr_g list * extended_subscopes) list *
+ ('a cases_pattern_disjunction_g * extended_subscopes) list *
+ ('a extended_glob_local_binder_g list * extended_subscopes) list
val match_notation_constr_cases_pattern :
'a cases_pattern_g -> interpretation ->
- (('a cases_pattern_g * subscopes) list * ('a cases_pattern_g list * subscopes) list) *
+ (('a cases_pattern_g * extended_subscopes) list * ('a cases_pattern_g list * extended_subscopes) list) *
(int * 'a cases_pattern_g list)
val match_notation_constr_ind_pattern :
inductive -> 'a cases_pattern_g list -> interpretation ->
- (('a cases_pattern_g * subscopes) list * ('a cases_pattern_g list * subscopes) list) *
+ (('a cases_pattern_g * extended_subscopes) list * ('a cases_pattern_g list * extended_subscopes) list) *
(int * 'a cases_pattern_g list)
(** {5 Matching a notation pattern against a [glob_constr]} *)
diff --git a/interp/notation_term.ml b/interp/notation_term.ml
new file mode 100644
index 00000000..5fb0ca1b
--- /dev/null
+++ b/interp/notation_term.ml
@@ -0,0 +1,98 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open Names
+open Glob_term
+
+(** [notation_constr] *)
+
+(** [notation_constr] is the subtype of [glob_constr] allowed in syntactic
+ extensions (i.e. notations).
+ No location since intended to be substituted at any place of a text.
+ Complex expressions such as fixpoints and cofixpoints are excluded,
+ as well as non global expressions such as existential variables. *)
+
+type notation_constr =
+ (** Part common to [glob_constr] and [cases_pattern] *)
+ | NRef of GlobRef.t
+ | NVar of Id.t
+ | NApp of notation_constr * notation_constr list
+ | NHole of Evar_kinds.t * Namegen.intro_pattern_naming_expr * Genarg.glob_generic_argument option
+ | NList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool
+ (** Part only in [glob_constr] *)
+ | NLambda of Name.t * notation_constr * notation_constr
+ | NProd of Name.t * notation_constr * notation_constr
+ | NBinderList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool
+ | NLetIn of Name.t * notation_constr * notation_constr option * notation_constr
+ | NCases of Constr.case_style * notation_constr option *
+ (notation_constr * (Name.t * (inductive * Name.t list) option)) list *
+ (cases_pattern list * notation_constr) list
+ | NLetTuple of Name.t list * (Name.t * notation_constr option) *
+ notation_constr * notation_constr
+ | NIf of notation_constr * (Name.t * notation_constr option) *
+ notation_constr * notation_constr
+ | NRec of fix_kind * Id.t array *
+ (Name.t * notation_constr option * notation_constr) list array *
+ notation_constr array * notation_constr array
+ | NSort of glob_sort
+ | NCast of notation_constr * notation_constr cast_type
+
+(** Note concerning NList: first constr is iterator, second is terminator;
+ first id is where each argument of the list has to be substituted
+ in iterator and snd id is alternative name just for printing;
+ boolean is associativity *)
+
+(** Types concerning notations *)
+
+type scope_name = string
+
+type tmp_scope_name = scope_name
+
+type subscopes = tmp_scope_name option * scope_name list
+
+type extended_subscopes = Constrexpr.notation_entry_level * subscopes
+
+(** Type of the meta-variables of an notation_constr: in a recursive pattern x..y,
+ x carries the sequence of objects bound to the list x..y *)
+
+type constr_as_binder_kind =
+ | AsIdent
+ | AsIdentOrPattern
+ | AsStrictPattern
+
+type notation_binder_source =
+ (* This accepts only pattern *)
+ (* NtnParsedAsPattern true means only strict pattern (no single variable) at printing *)
+ | NtnParsedAsPattern of bool
+ (* This accepts only ident *)
+ | NtnParsedAsIdent
+ (* This accepts ident, or pattern, or both *)
+ | NtnBinderParsedAsConstr of constr_as_binder_kind
+
+type notation_var_instance_type =
+ | NtnTypeConstr | NtnTypeBinder of notation_binder_source | NtnTypeConstrList | NtnTypeBinderList
+
+(** Type of variables when interpreting a constr_expr as a notation_constr:
+ in a recursive pattern x..y, both x and y carry the individual type
+ of each element of the list x..y *)
+type notation_var_internalization_type =
+ | NtnInternTypeAny | NtnInternTypeOnlyBinder
+
+(** This characterizes to what a notation is interpreted to *)
+type interpretation =
+ (Id.t * (extended_subscopes * notation_var_instance_type)) list *
+ notation_constr
+
+type reversibility_status = APrioriReversible | HasLtac | NonInjective of Id.t list
+
+type notation_interp_env = {
+ ninterp_var_type : notation_var_internalization_type Id.Map.t;
+ ninterp_rec_vars : Id.t Id.Map.t;
+}
diff --git a/interp/ppextend.ml b/interp/ppextend.ml
deleted file mode 100644
index c75d9e12..00000000
--- a/interp/ppextend.ml
+++ /dev/null
@@ -1,43 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(* * (see LICENSE file for the text of the license) *)
-(************************************************************************)
-
-open Pp
-open Notation_term
-
-(*s Pretty-print. *)
-
-type ppbox =
- | PpHB of int
- | PpHOVB of int
- | PpHVB of int
- | PpVB of int
-
-type ppcut =
- | PpBrk of int * int
- | PpFnl
-
-let ppcmd_of_box = function
- | PpHB n -> h n
- | PpHOVB n -> hov n
- | PpHVB n -> hv n
- | PpVB n -> v n
-
-let ppcmd_of_cut = function
- | PpFnl -> fnl ()
- | PpBrk(n1,n2) -> brk(n1,n2)
-
-type unparsing =
- | UnpMetaVar of int * parenRelation
- | UnpBinderMetaVar of int * parenRelation
- | UnpListMetaVar of int * parenRelation * unparsing list
- | UnpBinderListMetaVar of int * bool * unparsing list
- | UnpTerminal of string
- | UnpBox of ppbox * unparsing Loc.located list
- | UnpCut of ppcut
diff --git a/interp/redops.ml b/interp/redops.ml
new file mode 100644
index 00000000..b9a74136
--- /dev/null
+++ b/interp/redops.ml
@@ -0,0 +1,64 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open Genredexpr
+
+let union_consts l1 l2 = Util.List.union Pervasives.(=) l1 l2 (* FIXME *)
+
+let make_red_flag l =
+ let rec add_flag red = function
+ | [] -> red
+ | FBeta :: lf -> add_flag { red with rBeta = true } lf
+ | FMatch :: lf -> add_flag { red with rMatch = true } lf
+ | FFix :: lf -> add_flag { red with rFix = true } lf
+ | FCofix :: lf -> add_flag { red with rCofix = true } lf
+ | FZeta :: lf -> add_flag { red with rZeta = true } lf
+ | FConst l :: lf ->
+ if red.rDelta then
+ CErrors.user_err Pp.(str
+ "Cannot set both constants to unfold and constants not to unfold");
+ add_flag { red with rConst = union_consts red.rConst l } lf
+ | FDeltaBut l :: lf ->
+ if red.rConst <> [] && not red.rDelta then
+ CErrors.user_err Pp.(str
+ "Cannot set both constants to unfold and constants not to unfold");
+ add_flag
+ { red with rConst = union_consts red.rConst l; rDelta = true }
+ lf
+ in
+ add_flag
+ {rBeta = false; rMatch = false; rFix = false; rCofix = false;
+ rZeta = false; rDelta = false; rConst = []}
+ l
+
+
+let all_flags =
+ {rBeta = true; rMatch = true; rFix = true; rCofix = true;
+ rZeta = true; rDelta = true; rConst = []}
+
+(** Mapping [red_expr_gen] *)
+
+let map_flags f flags =
+ { flags with rConst = List.map f flags.rConst }
+
+let map_occs f (occ,e) = (occ,f e)
+
+let map_red_expr_gen f g h = function
+ | Fold l -> Fold (List.map f l)
+ | Pattern occs_l -> Pattern (List.map (map_occs f) occs_l)
+ | Simpl (flags,occs_o) ->
+ Simpl (map_flags g flags, Option.map (map_occs (Util.map_union g h)) occs_o)
+ | Unfold occs_l -> Unfold (List.map (map_occs g) occs_l)
+ | Cbv flags -> Cbv (map_flags g flags)
+ | Lazy flags -> Lazy (map_flags g flags)
+ | CbvVm occs_o -> CbvVm (Option.map (map_occs (Util.map_union g h)) occs_o)
+ | CbvNative occs_o -> CbvNative (Option.map (map_occs (Util.map_union g h)) occs_o)
+ | Cbn flags -> Cbn (map_flags g flags)
+ | ExtraRedExpr _ | Red _ | Hnf as x -> x
diff --git a/interp/ppextend.mli b/interp/redops.mli
index c81058e7..7254f29b 100644
--- a/interp/ppextend.mli
+++ b/interp/redops.mli
@@ -8,29 +8,13 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-open Notation_term
+open Genredexpr
-(** {6 Pretty-print. } *)
+val make_red_flag : 'a red_atom list -> 'a glob_red_flag
-type ppbox =
- | PpHB of int
- | PpHOVB of int
- | PpHVB of int
- | PpVB of int
+val all_flags : 'a glob_red_flag
-type ppcut =
- | PpBrk of int * int
- | PpFnl
+(** Mapping [red_expr_gen] *)
-val ppcmd_of_box : ppbox -> Pp.t -> Pp.t
-
-val ppcmd_of_cut : ppcut -> Pp.t
-
-type unparsing =
- | UnpMetaVar of int * parenRelation
- | UnpBinderMetaVar of int * parenRelation
- | UnpListMetaVar of int * parenRelation * unparsing list
- | UnpBinderListMetaVar of int * bool * unparsing list
- | UnpTerminal of string
- | UnpBox of ppbox * unparsing Loc.located list
- | UnpCut of ppcut
+val map_red_expr_gen : ('a -> 'd) -> ('b -> 'e) -> ('c -> 'f) ->
+ ('a,'b,'c) red_expr_gen -> ('d,'e,'f) red_expr_gen
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 36005121..071248f0 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -22,7 +22,7 @@ open Notation_ops
open Globnames
type key =
- | RefKey of global_reference
+ | RefKey of GlobRef.t
| Oth
(** TODO: share code from Notation *)
@@ -112,7 +112,9 @@ let revert_reserved_type t =
let t = EConstr.Unsafe.to_constr t in
let reserved = KeyMap.find (constr_key t) !reserve_revtable in
let t = EConstr.of_constr t in
- let t = Detyping.detype Detyping.Now false Id.Set.empty (Global.env()) Evd.empty t in
+ let env = Global.env () in
+ let evd = Evd.from_env env in
+ let t = Detyping.detype Detyping.Now false Id.Set.empty env evd t in
(* pedrot: if [Notation_ops.match_notation_constr] may raise [Failure _]
then I've introduced a bug... *)
let filter _ pat =
diff --git a/interp/reserve.mli b/interp/reserve.mli
index daee5863..a10858e7 100644
--- a/interp/reserve.mli
+++ b/interp/reserve.mli
@@ -11,5 +11,5 @@
open Names
open Notation_term
-val declare_reserved_type : Misctypes.lident list -> notation_constr -> unit
+val declare_reserved_type : lident list -> notation_constr -> unit
val find_reserved_type : Id.t -> notation_constr
diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml
index 1f4a93a6..91491bdf 100644
--- a/interp/smartlocate.ml
+++ b/interp/smartlocate.ml
@@ -18,7 +18,6 @@ open Pp
open CErrors
open Libnames
open Globnames
-open Misctypes
open Syntax_def
open Notation_term
@@ -42,36 +41,34 @@ let global_of_extended_global = function
| [],NApp (NRef ref,[]) -> ref
| _ -> raise Not_found
-let locate_global_with_alias ?(head=false) {CAst.loc; v=qid} =
+let locate_global_with_alias ?(head=false) qid =
let ref = Nametab.locate_extended qid in
try
if head then global_of_extended_global_head ref
else global_of_extended_global ref
with Not_found ->
- user_err ?loc (pr_qualid qid ++
+ user_err ?loc:qid.CAst.loc (pr_qualid qid ++
str " is bound to a notation that does not denote a reference.")
-let global_inductive_with_alias ({CAst.loc} as lr) =
- let qid = qualid_of_reference lr in
+let global_inductive_with_alias qid =
try match locate_global_with_alias qid with
| IndRef ind -> ind
| ref ->
- user_err ?loc ~hdr:"global_inductive"
- (pr_reference lr ++ spc () ++ str "is not an inductive type.")
+ user_err ?loc:qid.CAst.loc ~hdr:"global_inductive"
+ (pr_qualid qid ++ spc () ++ str "is not an inductive type.")
with Not_found -> Nametab.error_global_not_found qid
-let global_with_alias ?head r =
- let qid = qualid_of_reference r in
+let global_with_alias ?head qid =
try locate_global_with_alias ?head qid
with Not_found -> Nametab.error_global_not_found qid
-let smart_global ?head = CAst.with_loc_val (fun ?loc -> function
+let smart_global ?head = let open Constrexpr in CAst.with_loc_val (fun ?loc -> function
| AN r ->
global_with_alias ?head r
| ByNotation (ntn,sc) ->
Notation.interp_notation_as_global_reference ?loc (fun _ -> true) ntn sc)
-let smart_global_inductive = CAst.with_loc_val (fun ?loc -> function
+let smart_global_inductive = let open Constrexpr in CAst.with_loc_val (fun ?loc -> function
| AN r ->
global_inductive_with_alias r
| ByNotation (ntn,sc) ->
diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli
index 7ff7e899..e41ef789 100644
--- a/interp/smartlocate.mli
+++ b/interp/smartlocate.mli
@@ -11,29 +11,28 @@
open Names
open Libnames
open Globnames
-open Misctypes
(** [locate_global_with_alias] locates global reference possibly following
a notation if this notation has a role of aliasing; raise [Not_found]
if not bound in the global env; raise a [UserError] if bound to a
syntactic def that does not denote a reference *)
-val locate_global_with_alias : ?head:bool -> qualid CAst.t -> global_reference
+val locate_global_with_alias : ?head:bool -> qualid -> GlobRef.t
(** Extract a global_reference from a reference that can be an "alias" *)
-val global_of_extended_global : extended_global_reference -> global_reference
+val global_of_extended_global : extended_global_reference -> GlobRef.t
(** Locate a reference taking into account possible "alias" notations.
May raise [Nametab.GlobalizationError _] for an unknown reference,
or a [UserError] if bound to a syntactic def that does not denote
a reference. *)
-val global_with_alias : ?head:bool -> reference -> global_reference
+val global_with_alias : ?head:bool -> qualid -> GlobRef.t
(** The same for inductive types *)
-val global_inductive_with_alias : reference -> inductive
+val global_inductive_with_alias : qualid -> inductive
(** Locate a reference taking into account notations and "aliases" *)
-val smart_global : ?head:bool -> reference or_by_notation -> global_reference
+val smart_global : ?head:bool -> qualid Constrexpr.or_by_notation -> GlobRef.t
(** The same for inductive types *)
-val smart_global_inductive : reference or_by_notation -> inductive
+val smart_global_inductive : qualid Constrexpr.or_by_notation -> inductive
diff --git a/interp/stdarg.ml b/interp/stdarg.ml
index e5ed58be..7b01b6dc 100644
--- a/interp/stdarg.ml
+++ b/interp/stdarg.ml
@@ -11,6 +11,8 @@
open Genarg
open Geninterp
+type 'a and_short_name = 'a * Names.lident option
+
let make0 ?dyn name =
let wit = Genarg.make0 name in
let () = register_val0 wit dyn in
@@ -34,9 +36,6 @@ let wit_pre_ident : string uniform_genarg_type =
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"
@@ -45,8 +44,6 @@ let wit_var =
let wit_ref = make0 "ref"
-let wit_quant_hyp = make0 "quant_hyp"
-
let wit_sort_family = make0 "sort_family"
let wit_constr =
@@ -56,12 +53,6 @@ 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_open_constr_with_bindings = make0 "open_constr_with_bindings"
-
-let wit_bindings = make0 "bindings"
-
let wit_red_expr = make0 "redexpr"
let wit_clause_dft_concl =
@@ -74,6 +65,4 @@ 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 53d1a522..5e5e43ed 100644
--- a/interp/stdarg.mli
+++ b/interp/stdarg.mli
@@ -14,13 +14,14 @@ open Loc
open Names
open EConstr
open Libnames
-open Globnames
open Genredexpr
open Pattern
open Constrexpr
-open Misctypes
-open Tactypes
open Genarg
+open Genintern
+open Locus
+
+type 'a and_short_name = 'a * lident option
val wit_unit : unit uniform_genarg_type
@@ -36,15 +37,11 @@ val wit_pre_ident : string uniform_genarg_type
val wit_int_or_var : (int or_var, int or_var, int) genarg_type
-val wit_intro_pattern : (constr_expr intro_pattern_expr CAst.t, glob_constr_and_expr intro_pattern_expr CAst.t, intro_pattern) genarg_type
-
val wit_ident : Id.t uniform_genarg_type
val wit_var : (lident, lident, 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_ref : (qualid, GlobRef.t located or_var, GlobRef.t) genarg_type
val wit_sort_family : (Sorts.family, unit, unit) genarg_type
@@ -55,23 +52,8 @@ val wit_uconstr : (constr_expr , glob_constr_and_expr, Ltac_pretype.closed_glob_
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_open_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,
+ ((constr_expr,qualid 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
@@ -81,12 +63,10 @@ val wit_clause_dft_concl : (lident Locus.clause_expr, lident Locus.clause_expr,
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_reference : (qualid, GlobRef.t located or_var, GlobRef.t) genarg_type
+val wit_global : (qualid, GlobRef.t located or_var, GlobRef.t) genarg_type
val wit_clause : (lident Locus.clause_expr, lident 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 CAst.t, glob_constr_and_expr intro_pattern_expr CAst.t, intro_pattern) genarg_type
val wit_redexpr :
- ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen,
+ ((constr_expr,qualid 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 a4f20fd7..e3d490a1 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -77,8 +77,8 @@ type syndef_interpretation = (Id.t * subscopes) list * notation_constr
(* Coercions to the general format of notation that also supports
variables bound to list of expressions *)
-let in_pat (ids,ac) = (List.map (fun (id,sc) -> (id,(sc,NtnTypeConstr))) ids,ac)
-let out_pat (ids,ac) = (List.map (fun (id,(sc,typ)) -> (id,sc)) ids,ac)
+let in_pat (ids,ac) = (List.map (fun (id,sc) -> (id,((Constrexpr.InConstrEntrySomeLevel,sc),NtnTypeConstr))) ids,ac)
+let out_pat (ids,ac) = (List.map (fun (id,((_,sc),typ)) -> (id,sc)) ids,ac)
let declare_syntactic_definition local id onlyparse pat =
let _ = add_leaf id (in_syntax_constant (local,in_pat pat,onlyparse)) in ()
diff --git a/interp/tactypes.ml b/interp/tactypes.ml
deleted file mode 100644
index 83e42be8..00000000
--- a/interp/tactypes.ml
+++ /dev/null
@@ -1,34 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(* * (see LICENSE file for the text of the license) *)
-(************************************************************************)
-
-(** Tactic-related types that are not totally Ltac specific and still used in
- lower API. It's not clear whether this is a temporary API or if this is
- meant to stay. *)
-
-open Names
-open Constrexpr
-open Pattern
-open Misctypes
-
-(** In globalize tactics, we need to keep the initial [constr_expr] to recompute
- in the environment by the effective calls to Intro, Inversion, etc
- The [constr_expr] field is [None] in TacDef though *)
-type glob_constr_and_expr = Glob_term.glob_constr * constr_expr option
-type glob_constr_pattern_and_expr = Id.Set.t * glob_constr_and_expr * constr_pattern
-
-type 'a delayed_open = Environ.env -> Evd.evar_map -> Evd.evar_map * 'a
-
-type delayed_open_constr = EConstr.constr delayed_open
-type delayed_open_constr_with_bindings = EConstr.constr with_bindings delayed_open
-
-type intro_pattern = delayed_open_constr intro_pattern_expr CAst.t
-type intro_patterns = delayed_open_constr intro_pattern_expr CAst.t list
-type or_and_intro_pattern = delayed_open_constr or_and_intro_pattern_expr CAst.t
-type intro_pattern_naming = intro_pattern_naming_expr CAst.t
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
deleted file mode 100644
index 7d2d75d9..00000000
--- a/interp/topconstr.ml
+++ /dev/null
@@ -1,23 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(* * (see LICENSE file for the text of the license) *)
-(************************************************************************)
-
-open Constrexpr_ops
-
-let asymmetric_patterns = asymmetric_patterns
-let error_invalid_pattern_notation = error_invalid_pattern_notation
-let split_at_annot = split_at_annot
-let ntn_loc = ntn_loc
-let patntn_loc = patntn_loc
-let map_constr_expr_with_binders = map_constr_expr_with_binders
-let fold_constr_expr_with_binders = fold_constr_expr_with_binders
-let ids_of_cases_indtype = ids_of_cases_indtype
-let occur_var_constr_expr = occur_var_constr_expr
-let free_vars_of_constr_expr = free_vars_of_constr_expr
-let replace_vars_constr_expr = replace_vars_constr_expr
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
deleted file mode 100644
index c8650201..00000000
--- a/interp/topconstr.mli
+++ /dev/null
@@ -1,53 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(* * (see LICENSE file for the text of the license) *)
-(************************************************************************)
-
-open Names
-open Constrexpr
-
-(** Topconstr: This whole module is deprecated in favor of Constrexpr_ops *)
-val asymmetric_patterns : bool ref
-[@@ocaml.deprecated "use Constrexpr_ops.asymmetric_patterns"]
-
-(** Utilities on constr_expr *)
-val split_at_annot : local_binder_expr list -> Misctypes.lident option -> local_binder_expr list * local_binder_expr list
-[@@ocaml.deprecated "use Constrexpr_ops.split_at_annot"]
-
-val ntn_loc : ?loc:Loc.t -> constr_notation_substitution -> string -> (int * int) list
-[@@ocaml.deprecated "use Constrexpr_ops.ntn_loc"]
-val patntn_loc : ?loc:Loc.t -> cases_pattern_notation_substitution -> string -> (int * int) list
-[@@ocaml.deprecated "use Constrexpr_ops.patntn_loc"]
-
-(** For cases pattern parsing errors *)
-val error_invalid_pattern_notation : ?loc:Loc.t -> unit -> 'a
-[@@ocaml.deprecated "use Constrexpr_ops.error_invalid_pattern_notation"]
-
-(*************************************************************************)
-val replace_vars_constr_expr : Id.t Id.Map.t -> constr_expr -> constr_expr
-[@@ocaml.deprecated "use Constrexpr_ops.free_vars_of_constr_expr"]
-
-val free_vars_of_constr_expr : constr_expr -> Id.Set.t
-[@@ocaml.deprecated "use Constrexpr_ops.free_vars_of_constr_expr"]
-
-val occur_var_constr_expr : Id.t -> constr_expr -> bool
-[@@ocaml.deprecated "use Constrexpr_ops.occur_var_constr_expr"]
-
-(** Specific function for interning "in indtype" syntax of "match" *)
-val ids_of_cases_indtype : cases_pattern_expr -> Id.Set.t
-[@@ocaml.deprecated "use Constrexpr_ops.ids_of_cases_indtype"]
-
-(** Used in typeclasses *)
-val fold_constr_expr_with_binders : (Id.t -> 'a -> 'a) ->
- ('a -> 'b -> constr_expr -> 'b) -> 'a -> 'b -> constr_expr -> 'b
-[@@ocaml.deprecated "use Constrexpr_ops.fold_constr_expr_with_binders"]
-
-val map_constr_expr_with_binders :
- (Id.t -> 'a -> 'a) -> ('a -> constr_expr -> constr_expr) ->
- 'a -> constr_expr -> constr_expr
-[@@ocaml.deprecated "use Constrexpr_ops.map_constr_expr_with_binders"]