aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/assumptions.ml38
-rw-r--r--vernac/assumptions.mli5
-rw-r--r--vernac/auto_ind_decl.ml4
-rw-r--r--vernac/class.ml13
-rw-r--r--vernac/comInductive.ml94
-rw-r--r--vernac/comInductive.mli7
-rw-r--r--vernac/dune16
-rw-r--r--vernac/egramcoq.ml133
-rw-r--r--vernac/egramcoq.mli3
-rw-r--r--vernac/egramml.ml9
-rw-r--r--vernac/egramml.mli2
-rw-r--r--vernac/explainErr.ml2
-rw-r--r--vernac/g_proofs.mlg1
-rw-r--r--vernac/g_vernac.mlg47
-rw-r--r--vernac/himsg.ml33
-rw-r--r--vernac/himsg.mli2
-rw-r--r--vernac/lemmas.ml18
-rw-r--r--vernac/metasyntax.ml444
-rw-r--r--vernac/metasyntax.mli11
-rw-r--r--vernac/obligations.ml6
-rw-r--r--vernac/ppvernac.ml46
-rw-r--r--vernac/record.ml71
-rw-r--r--vernac/record.mli4
-rw-r--r--vernac/topfmt.ml124
-rw-r--r--vernac/vernacentries.ml258
-rw-r--r--vernac/vernacentries.mli30
-rw-r--r--vernac/vernacexpr.ml44
-rw-r--r--vernac/vernacinterp.ml5
-rw-r--r--vernac/vernacinterp.mli4
29 files changed, 1024 insertions, 450 deletions
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index 765f962e99..b000745961 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -70,8 +70,8 @@ let rec fields_of_functor f subs mp0 args = function
let rec lookup_module_in_impl mp =
match mp with
- | MPfile _ -> raise Not_found
- | MPbound _ -> assert false
+ | MPfile _ -> Global.lookup_module mp
+ | MPbound _ -> Global.lookup_module mp
| MPdot (mp',lab') ->
if ModPath.equal mp' (Global.current_modpath ()) then
Global.lookup_module mp
@@ -213,25 +213,25 @@ let rec traverse current ctx accu t = match Constr.kind t with
and traverse_object ?inhabits (curr, data, ax2ty) body obj =
let data, ax2ty =
- let already_in = Refmap_env.mem obj data in
+ let already_in = GlobRef.Map_env.mem obj data in
match body () with
| None ->
let data =
- if not already_in then Refmap_env.add obj Refset_env.empty data else data in
+ if not already_in then GlobRef.Map_env.add obj GlobRef.Set_env.empty data else data in
let ax2ty =
if Option.is_empty inhabits then ax2ty else
let ty = Option.get inhabits in
- try let l = Refmap_env.find obj ax2ty in Refmap_env.add obj (ty::l) ax2ty
- with Not_found -> Refmap_env.add obj [ty] ax2ty in
+ try let l = GlobRef.Map_env.find obj ax2ty in GlobRef.Map_env.add obj (ty::l) ax2ty
+ with Not_found -> GlobRef.Map_env.add obj [ty] ax2ty in
data, ax2ty
| Some body ->
if already_in then data, ax2ty else
let contents,data,ax2ty =
traverse (label_of obj) Context.Rel.empty
- (Refset_env.empty,data,ax2ty) body in
- Refmap_env.add obj contents data, ax2ty
+ (GlobRef.Set_env.empty,data,ax2ty) body in
+ GlobRef.Map_env.add obj contents data, ax2ty
in
- (Refset_env.add obj curr, data, ax2ty)
+ (GlobRef.Set_env.add obj curr, data, ax2ty)
(** Collects the references occurring in the declaration of mutual inductive
definitions. All the constructors and names of a mutual inductive
@@ -244,14 +244,14 @@ and traverse_inductive (curr, data, ax2ty) mind obj =
(* Invariant : I_0 \in data iff I_i \in data iff c_ij \in data
where I_0, I_1, ... are in the same mutual definition and c_ij
are all their constructors. *)
- if Refmap_env.mem firstind_ref data then data, ax2ty else
+ if GlobRef.Map_env.mem firstind_ref data then data, ax2ty else
let mib = lookup_mind mind in
(* Collects references of parameters *)
let param_ctx = mib.mind_params_ctxt in
let nparam = List.length param_ctx in
let accu =
traverse_context label Context.Rel.empty
- (Refset_env.empty, data, ax2ty) param_ctx
+ (GlobRef.Set_env.empty, data, ax2ty) param_ctx
in
(* Build the context of all arities *)
let arities_ctx =
@@ -283,14 +283,14 @@ and traverse_inductive (curr, data, ax2ty) mind obj =
(* Maps all these dependencies to inductives and constructors*)
let data = Array.fold_left_i (fun n data oib ->
let ind = (mind, n) in
- let data = Refmap_env.add (IndRef ind) contents data in
+ let data = GlobRef.Map_env.add (IndRef ind) contents data in
Array.fold_left_i (fun k data _ ->
- Refmap_env.add (ConstructRef (ind, k+1)) contents data
+ GlobRef.Map_env.add (ConstructRef (ind, k+1)) contents data
) data oib.mind_consnames) data mib.mind_packets
in
data, ax2ty
in
- (Refset_env.add obj curr, data, ax2ty)
+ (GlobRef.Set_env.add obj curr, data, ax2ty)
(** Collects references in a rel_context. *)
and traverse_context current ctx accu ctxt =
@@ -307,7 +307,7 @@ and traverse_context current ctx accu ctxt =
let traverse current t =
let () = modcache := MPmap.empty in
- traverse current Context.Rel.empty (Refset_env.empty, Refmap_env.empty, Refmap_env.empty) t
+ traverse current Context.Rel.empty (GlobRef.Set_env.empty, GlobRef.Map_env.empty, GlobRef.Map_env.empty) t
(** Hopefully bullet-proof function to recover the type of a constant. It just
ignores all the universe stuff. There are many issues that can arise when
@@ -330,12 +330,12 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t =
let accu =
if cb.const_typing_flags.check_guarded then accu
else
- let l = try Refmap_env.find obj ax2ty with Not_found -> [] in
+ let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
ContextObjectMap.add (Axiom (Guarded kn, l)) Constr.mkProp accu
in
if not (Declareops.constant_has_body cb) || not cb.const_typing_flags.check_universes then
let t = type_of_constant cb in
- let l = try Refmap_env.find obj ax2ty with Not_found -> [] in
+ let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
ContextObjectMap.add (Axiom (Constant kn,l)) t accu
else if add_opaque && (Declareops.is_opaque cb || not (Cpred.mem kn knst)) then
let t = type_of_constant cb in
@@ -350,7 +350,7 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t =
if mind.mind_typing_flags.check_guarded then
accu
else
- let l = try Refmap_env.find obj ax2ty with Not_found -> [] in
+ let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
ContextObjectMap.add (Axiom (Positive m, l)) Constr.mkProp accu
in
- Refmap_env.fold fold graph ContextObjectMap.empty
+ GlobRef.Map_env.fold fold graph ContextObjectMap.empty
diff --git a/vernac/assumptions.mli b/vernac/assumptions.mli
index 751e79d89c..aead345d8c 100644
--- a/vernac/assumptions.mli
+++ b/vernac/assumptions.mli
@@ -10,7 +10,6 @@
open Names
open Constr
-open Globnames
open Printer
(** Collects all the objects on which a term directly relies, bypassing kernel
@@ -22,8 +21,8 @@ open Printer
*)
val traverse :
Label.t -> constr ->
- (Refset_env.t * Refset_env.t Refmap_env.t *
- (Label.t * Constr.rel_context * types) list Refmap_env.t)
+ (GlobRef.Set_env.t * GlobRef.Set_env.t GlobRef.Map_env.t *
+ (Label.t * Constr.rel_context * types) list GlobRef.Map_env.t)
(** Collects all the assumptions (optionally including opaque definitions)
on which a term relies (together with their type). The above warning of
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index ee578669c2..3bf3925b4b 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -355,7 +355,7 @@ let destruct_ind sigma c =
then avoid should be
[| lb_An ... lb _A1 (resp. bl_An ... bl_A1)
eq_An .... eq_A1 An ... A1 |]
-so from Ai we can find the the correct eq_Ai bl_ai or lb_ai
+so from Ai we can find the correct eq_Ai bl_ai or lb_ai
*)
(* used in the leib -> bool side*)
let do_replace_lb mode lb_scheme_key aavoid narg p q =
@@ -543,7 +543,7 @@ let eqI ind l =
and e, eff =
try let c, eff = find_scheme beq_scheme_kind ind in mkConst c, eff
with Not_found -> user_err ~hdr:"AutoIndDecl.eqI"
- (str "The boolean equality on " ++ MutInd.print (fst ind) ++ str " is needed.");
+ (str "The boolean equality on " ++ Printer.pr_inductive (Global.env ()) ind ++ str " is needed.");
in (if Array.equal Constr.equal eA [||] then e else mkApp(e,eA)), eff
(**********************************************************************)
diff --git a/vernac/class.ml b/vernac/class.ml
index e425e6474d..614b2181d9 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -73,7 +73,7 @@ let check_reference_arity ref =
let check_arity = function
| CL_FUN | CL_SORT -> ()
| CL_CONST cst -> check_reference_arity (ConstRef cst)
- | CL_PROJ cst -> check_reference_arity (ConstRef cst)
+ | CL_PROJ p -> check_reference_arity (ConstRef (Projection.Repr.constant p))
| CL_SECVAR id -> check_reference_arity (VarRef id)
| CL_IND kn -> check_reference_arity (IndRef kn)
@@ -92,8 +92,8 @@ let uniform_cond sigma ctx lt =
let class_of_global = function
| ConstRef sp ->
- if Environ.is_projection sp (Global.env ())
- then CL_PROJ sp else CL_CONST sp
+ (match Recordops.find_primitive_projection sp with
+ | Some p -> CL_PROJ p | None -> CL_CONST sp)
| IndRef sp -> CL_IND sp
| VarRef id -> CL_SECVAR id
| ConstructRef _ as c ->
@@ -143,8 +143,8 @@ let get_target t ind =
CL_FUN
else
match pi1 (find_class_type Evd.empty (EConstr.of_constr t)) with
- | CL_CONST p when Environ.is_projection p (Global.env ()) ->
- CL_PROJ p
+ | CL_CONST p when Recordops.is_primitive_projection p ->
+ CL_PROJ (Option.get @@ Recordops.find_primitive_projection p)
| x -> x
let strength_of_cl = function
@@ -165,7 +165,8 @@ let get_strength stre ref cls clt =
let ident_key_of_class = function
| CL_FUN -> "Funclass"
| CL_SORT -> "Sortclass"
- | CL_CONST sp | CL_PROJ sp -> Label.to_string (Constant.label sp)
+ | CL_CONST sp -> Label.to_string (Constant.label sp)
+ | CL_PROJ sp -> Label.to_string (Projection.Repr.label sp)
| CL_IND (sp,_) -> Label.to_string (MutInd.label sp)
| CL_SECVAR id -> Id.to_string id
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index ad1ffa35a1..7b28895814 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -35,6 +35,18 @@ module RelDecl = Context.Rel.Declaration
(* 3b| Mutual inductive definitions *)
+let should_auto_template =
+ let open Goptions in
+ let auto = ref true in
+ let _ = declare_bool_option
+ { optdepr = false;
+ optname = "Automatically make some inductive types template polymorphic";
+ optkey = ["Auto";"Template";"Polymorphism"];
+ optread = (fun () -> !auto);
+ optwrite = (fun b -> auto := b); }
+ in
+ fun () -> !auto
+
let rec complete_conclusion a cs = CAst.map_with_loc (fun ?loc -> function
| CProdN (bl,c) -> CProdN (bl,complete_conclusion a cs c)
| CLetIn (na,b,t,c) -> CLetIn (na,b,t,complete_conclusion a cs c)
@@ -55,7 +67,6 @@ let push_types env idl tl =
type structured_one_inductive_expr = {
ind_name : Id.t;
- ind_univs : universe_decl_expr option;
ind_arity : constr_expr;
ind_lc : (Id.t * constr_expr) list
}
@@ -113,17 +124,16 @@ let rec check_anonymous_type ind =
| GCast (e, _) -> check_anonymous_type e
| _ -> false
-let make_conclusion_flexible sigma ty poly =
- if poly && Term.isArity ty then
- let _, concl = Term.destArity ty in
- match concl with
- | Type u ->
- (match Univ.universe_level u with
+let make_conclusion_flexible sigma = function
+ | None -> sigma
+ | Some s ->
+ (match EConstr.ESorts.kind sigma s with
+ | Type u ->
+ (match Univ.universe_level u with
| Some u ->
Evd.make_flexible_variable sigma ~algebraic:true u
| None -> sigma)
- | _ -> sigma
- else sigma
+ | _ -> sigma)
let is_impredicative env u =
u = Prop || (is_impredicative_set env && u = Set)
@@ -133,10 +143,12 @@ let interp_ind_arity env sigma ind =
let impls = Implicit_quantifiers.implicits_of_glob_constr ~with_products:true c in
let sigma,t = understand_tcc env sigma ~expected_type:IsType c in
let pseudo_poly = check_anonymous_type c in
- let () = if not (Reductionops.is_arity env sigma t) then
+ match Reductionops.sort_of_arity env sigma t with
+ | exception Invalid_argument _ ->
user_err ?loc:(constr_loc ind.ind_arity) (str "Not an arity")
- in
- sigma, (t, pseudo_poly, impls)
+ | s ->
+ let concl = if pseudo_poly then Some s else None in
+ sigma, (t, concl, impls)
let interp_cstrs env sigma impls mldata arity ind =
let cnames,ctyps = List.split ind.ind_lc in
@@ -326,13 +338,21 @@ let check_param = function
| CLocalPattern {CAst.loc} ->
Loc.raise ?loc (Stream.Error "pattern with quote not allowed here")
-let interp_mutual_inductive_gen env0 (uparamsl,paramsl,indl) notations cum poly prv finite =
+let restrict_inductive_universes sigma ctx_params arities constructors =
+ let merge_universes_of_constr c =
+ Univ.LSet.union (EConstr.universes_of_constr sigma (EConstr.of_constr c)) in
+ let uvars = Univ.LSet.empty in
+ let uvars = Context.Rel.(fold_outside (Declaration.fold_constr merge_universes_of_constr) ctx_params ~init:uvars) in
+ let uvars = List.fold_right merge_universes_of_constr arities uvars in
+ let uvars = List.fold_right (fun (_,ctypes,_) -> List.fold_right merge_universes_of_constr ctypes) constructors uvars in
+ Evd.restrict_universe_context sigma uvars
+
+let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) notations cum poly prv finite =
check_all_names_different indl;
List.iter check_param paramsl;
if not (List.is_empty uparamsl) && not (List.is_empty notations)
then user_err (str "Inductives with uniform parameters may not have attached notations.");
- let pl = (List.hd indl).ind_univs in
- let sigma, decl = interp_univ_decl_opt env0 pl in
+ let sigma, udecl = interp_univ_decl_opt env0 udecl in
let sigma, (uimpls, ((env_uparams, ctx_uparams), useruimpls)) =
interp_context_evars env0 sigma uparamsl in
let sigma, (impls, ((env_params, ctx_params), userimpls)) =
@@ -354,7 +374,7 @@ let interp_mutual_inductive_gen env0 (uparamsl,paramsl,indl) notations cum poly
(* Compute interpretation metadatas *)
let indimpls = List.map (fun (_, _, impls) -> userimpls @
lift_implicits (Context.Rel.nhyps ctx_params) impls) arities in
- let arities = List.map pi1 arities and aritypoly = List.map pi2 arities in
+ let arities = List.map pi1 arities and arityconcl = List.map pi2 arities in
let impls = compute_internalization_env env_uparams sigma ~impls (Inductive (params,true)) indnames fullarities indimpls in
let ntn_impls = compute_internalization_env env_uparams sigma (Inductive (params,true)) indnames fullarities indimpls in
let mldatas = List.map2 (mk_mltype_data sigma env_params params) arities indnames in
@@ -393,14 +413,16 @@ let interp_mutual_inductive_gen env0 (uparamsl,paramsl,indl) notations cum poly
let nf = Evarutil.nf_evars_universes sigma in
let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf cl,impsl)) constructors in
let arities = List.map EConstr.(to_constr sigma) arities in
- let sigma = List.fold_left2 (fun sigma ty poly -> make_conclusion_flexible sigma ty poly) sigma arities aritypoly in
+ let sigma = List.fold_left make_conclusion_flexible sigma arityconcl in
let sigma, arities = inductive_levels env_ar_params sigma poly arities constructors in
let sigma = Evd.minimize_universes sigma in
let nf = Evarutil.nf_evars_universes sigma in
let arities = List.map nf arities in
let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf cl,impsl)) constructors in
let ctx_params = List.map Termops.(map_rel_decl (EConstr.to_constr sigma)) ctx_params in
- let uctx = Evd.check_univ_decl ~poly sigma decl in
+ let arityconcl = List.map (Option.map (EConstr.ESorts.kind sigma)) arityconcl in
+ let sigma = restrict_inductive_universes sigma ctx_params arities constructors in
+ let uctx = Evd.check_univ_decl ~poly sigma udecl in
List.iter (fun c -> check_evars env_params (Evd.from_env env_params) sigma (EConstr.of_constr c)) arities;
Context.Rel.iter (fun c -> check_evars env0 (Evd.from_env env0) sigma (EConstr.of_constr c)) ctx_params;
List.iter (fun (_,ctyps,_) ->
@@ -408,13 +430,23 @@ let interp_mutual_inductive_gen env0 (uparamsl,paramsl,indl) notations cum poly
constructors;
(* Build the inductive entries *)
- let entries = List.map4 (fun ind arity template (cnames,ctypes,cimpls) -> {
- mind_entry_typename = ind.ind_name;
- mind_entry_arity = arity;
- mind_entry_template = template;
- mind_entry_consnames = cnames;
- mind_entry_lc = ctypes
- }) indl arities aritypoly constructors in
+ let entries = List.map4 (fun ind arity concl (cnames,ctypes,cimpls) ->
+ let template = match template with
+ | Some template ->
+ if poly && template then user_err Pp.(strbrk "template and polymorphism not compatible");
+ template
+ | None ->
+ should_auto_template () && not poly &&
+ Option.cata (fun s -> not (Sorts.is_small s)) false concl
+ in
+ { mind_entry_typename = ind.ind_name;
+ mind_entry_arity = arity;
+ mind_entry_template = template;
+ mind_entry_consnames = cnames;
+ mind_entry_lc = ctypes
+ })
+ indl arities arityconcl constructors
+ in
let impls =
let len = Context.Rel.nhyps ctx_params in
List.map2 (fun indimpls (_,_,cimpls) ->
@@ -444,8 +476,8 @@ let interp_mutual_inductive_gen env0 (uparamsl,paramsl,indl) notations cum poly
InferCumulativity.infer_inductive env_ar mind_ent
else mind_ent), Evd.universe_binders sigma, impls
-let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
- interp_mutual_inductive_gen (Global.env()) ([],paramsl,indl) notations cum poly prv finite
+let interp_mutual_inductive ~template udecl (paramsl,indl) notations cum poly prv finite =
+ interp_mutual_inductive_gen (Global.env()) ~template udecl ([],paramsl,indl) notations cum poly prv finite
(* Very syntactical equality *)
let eq_local_binders bl1 bl2 =
@@ -466,8 +498,8 @@ let extract_params indl =
params
let extract_inductive indl =
- List.map (fun (({CAst.v=indname},pl),_,ar,lc) -> {
- ind_name = indname; ind_univs = pl;
+ List.map (fun ({CAst.v=indname},_,ar,lc) -> {
+ ind_name = indname;
ind_arity = Option.cata (fun x -> x) (CAst.make @@ CSort (Glob_term.GType [])) ar;
ind_lc = List.map (fun (_,({CAst.v=id},t)) -> (id,t)) lc
}) indl
@@ -533,11 +565,11 @@ type uniform_inductive_flag =
| UniformParameters
| NonUniformParameters
-let do_mutual_inductive indl cum poly prv ~uniform finite =
+let do_mutual_inductive ~template udecl indl cum poly prv ~uniform finite =
let (params,indl),coes,ntns = extract_mutual_inductive_declaration_components indl in
(* Interpret the types *)
let indl = match uniform with UniformParameters -> (params, [], indl) | NonUniformParameters -> ([], params, indl) in
- let mie,pl,impls = interp_mutual_inductive_gen (Global.env()) indl ntns cum poly prv finite in
+ let mie,pl,impls = interp_mutual_inductive_gen (Global.env()) ~template udecl indl ntns cum poly prv finite in
(* Declare the mutual inductive block with its associated schemes *)
ignore (declare_mutual_inductive_with_eliminations mie pl impls);
(* Declare the possible notations of inductive types *)
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index 4e30ed7de5..f23085a538 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -24,6 +24,7 @@ type uniform_inductive_flag =
| NonUniformParameters
val do_mutual_inductive :
+ template:bool option -> universe_decl_expr option ->
(one_inductive_expr * decl_notation list) list -> cumulative_inductive_flag ->
polymorphic -> private_flag -> uniform:uniform_inductive_flag ->
Declarations.recursivity_kind -> unit
@@ -45,6 +46,8 @@ val declare_mutual_inductive_with_eliminations :
mutual_inductive_entry -> UnivNames.universe_binders -> one_inductive_impls list ->
MutInd.t
+val should_auto_template : unit -> bool
+
(** Exported for Funind *)
(** Extracting the semantical components out of the raw syntax of mutual
@@ -52,7 +55,6 @@ val declare_mutual_inductive_with_eliminations :
type structured_one_inductive_expr = {
ind_name : Id.t;
- ind_univs : universe_decl_expr option;
ind_arity : constr_expr;
ind_lc : (Id.t * constr_expr) list
}
@@ -67,6 +69,7 @@ val extract_mutual_inductive_declaration_components :
(** Typing mutual inductive definitions *)
val interp_mutual_inductive :
- structured_inductive_expr -> decl_notation list -> cumulative_inductive_flag ->
+ template:bool option -> universe_decl_expr option -> structured_inductive_expr ->
+ decl_notation list -> cumulative_inductive_flag ->
polymorphic -> private_flag -> Declarations.recursivity_kind ->
mutual_inductive_entry * UnivNames.universe_binders * one_inductive_impls list
diff --git a/vernac/dune b/vernac/dune
new file mode 100644
index 0000000000..45b567d631
--- /dev/null
+++ b/vernac/dune
@@ -0,0 +1,16 @@
+(library
+ (name vernac)
+ (synopsis "Coq's Vernacular Language")
+ (public_name coq.vernac)
+ (wrapped false)
+ (libraries tactics parsing))
+
+(rule
+ (targets g_proofs.ml)
+ (deps (:mlg-file g_proofs.mlg))
+ (action (run coqpp %{mlg-file})))
+
+(rule
+ (targets g_vernac.ml)
+ (deps (:mlg-file g_vernac.mlg))
+ (action (run coqpp %{mlg-file})))
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index 3281b75aaa..16101396cf 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -54,6 +54,17 @@ let default_pattern_levels =
let default_constr_levels = (default_levels, default_pattern_levels)
+let find_levels levels = function
+ | InConstrEntry -> levels, String.Map.find "constr" levels
+ | InCustomEntry s ->
+ try levels, String.Map.find s levels
+ with Not_found ->
+ String.Map.add s ([],[]) levels, ([],[])
+
+let save_levels levels custom lev =
+ let s = match custom with InConstrEntry -> "constr" | InCustomEntry s -> s in
+ String.Map.add s lev levels
+
(* At a same level, LeftA takes precedence over RightA and NoneA *)
(* In case, several associativity exists for a level, we make two levels, *)
(* first LeftA, then RightA and NoneA together *)
@@ -125,24 +136,24 @@ let rec list_mem_assoc_triple x = function
let register_empty_levels accu forpat levels =
let rec filter accu = function
| [] -> ([], accu)
- | n :: rem ->
+ | (where,n) :: rem ->
let rem, accu = filter accu rem in
- let (clev, plev) = accu in
+ let accu, (clev, plev) = find_levels accu where in
let levels = if forpat then plev else clev in
if not (list_mem_assoc_triple n levels) then
let nlev, ans = find_position_gen levels true None (Some n) in
let nlev = if forpat then (clev, nlev) else (nlev, plev) in
- ans :: rem, nlev
+ (where, ans) :: rem, save_levels accu where nlev
else rem, accu
in
filter accu levels
-let find_position accu forpat assoc level =
- let (clev, plev) = accu in
+let find_position accu custom forpat assoc level =
+ let accu, (clev, plev) = find_levels accu custom in
let levels = if forpat then plev else clev in
let nlev, ans = find_position_gen levels false assoc level in
let nlev = if forpat then (clev, nlev) else (nlev, plev) in
- (ans, nlev)
+ (ans, save_levels accu custom nlev)
(**************************************************************************)
(*
@@ -231,7 +242,7 @@ type (_, _) entry =
| TTName : ('self, lname) entry
| TTReference : ('self, qualid) entry
| TTBigint : ('self, Constrexpr.raw_natural_number) entry
-| TTConstr : prod_info * 'r target -> ('r, 'r) entry
+| TTConstr : notation_entry * prod_info * 'r target -> ('r, 'r) entry
| TTConstrList : prod_info * Tok.t list * 'r target -> ('r, 'r list) entry
| TTPattern : int -> ('self, cases_pattern_expr) entry
| TTOpenBinderList : ('self, local_binder_expr list) entry
@@ -239,17 +250,58 @@ type (_, _) entry =
type _ any_entry = TTAny : ('s, 'r) entry -> 's any_entry
+let constr_custom_entry : (string, Constrexpr.constr_expr) entry_command =
+ create_entry_command "constr" (fun s st -> [s], st)
+let pattern_custom_entry : (string, Constrexpr.cases_pattern_expr) entry_command =
+ create_entry_command "pattern" (fun s st -> [s], st)
+
+let custom_entry_locality = Summary.ref ~name:"LOCAL-CUSTOM-ENTRY" String.Set.empty
+(** If the entry is present then local *)
+
+let create_custom_entry ~local s =
+ if List.mem s ["constr";"pattern";"ident";"global";"binder";"bigint"] then
+ user_err Pp.(quote (str s) ++ str " is a reserved entry name.");
+ let sc = "constr:"^s in
+ let sp = "pattern:"^s in
+ let _ = extend_entry_command constr_custom_entry sc in
+ let _ = extend_entry_command pattern_custom_entry sp in
+ let () = if local then custom_entry_locality := String.Set.add s !custom_entry_locality in
+ ()
+
+let find_custom_entry s =
+ let sc = "constr:"^s in
+ let sp = "pattern:"^s in
+ try (find_custom_entry constr_custom_entry sc, find_custom_entry pattern_custom_entry sp)
+ with Not_found -> user_err Pp.(str "Undeclared custom entry: " ++ str s ++ str ".")
+
+let locality_of_custom_entry s = String.Set.mem s !custom_entry_locality
+
(* This computes the name of the level where to add a new rule *)
-let interp_constr_entry_key : type r. r target -> int -> r Entry.t * int option =
- fun forpat level -> match forpat with
+let interp_constr_entry_key : type r. _ -> r target -> int -> r Entry.t * int option =
+ fun custom forpat level ->
+ match custom with
+ | InCustomEntry s ->
+ (let (entry_for_constr, entry_for_patttern) = find_custom_entry s in
+ match forpat with
+ | ForConstr -> entry_for_constr, Some level
+ | ForPattern -> entry_for_patttern, Some level)
+ | InConstrEntry ->
+ match forpat with
| ForConstr ->
if level = 200 then Constr.binder_constr, None
else Constr.operconstr, Some level
| ForPattern -> Constr.pattern, Some level
-let target_entry : type s. s target -> s Entry.t = function
-| ForConstr -> Constr.operconstr
-| ForPattern -> Constr.pattern
+let target_entry : type s. notation_entry -> s target -> s Entry.t = function
+| InConstrEntry ->
+ (function
+ | ForConstr -> Constr.operconstr
+ | ForPattern -> Constr.pattern)
+| InCustomEntry s ->
+ let (entry_for_constr, entry_for_patttern) = find_custom_entry s in
+ function
+ | ForConstr -> entry_for_constr
+ | ForPattern -> entry_for_patttern
let is_self from e = match e with
| (NumLevel n, BorderProd (Right, _ (* Some(NonA|LeftA) *))) -> false
@@ -273,11 +325,11 @@ let make_sep_rules = function
let r = mkrule (List.rev tkl) in
Arules [r]
-let symbol_of_target : type s. _ -> _ -> _ -> s target -> (s, s) symbol = fun p assoc from forpat ->
- if is_binder_level from p then Aentryl (target_entry forpat, "200")
+let symbol_of_target : type s. _ -> _ -> _ -> _ -> s target -> (s, s) symbol = fun custom p assoc from forpat ->
+ if custom = InConstrEntry && is_binder_level from p then Aentryl (target_entry InConstrEntry forpat, "200")
else if is_self from p then Aself
else
- let g = target_entry forpat in
+ let g = target_entry custom forpat in
let lev = adjust_level assoc from p in
begin match lev with
| None -> Aentry g
@@ -286,11 +338,11 @@ let symbol_of_target : type s. _ -> _ -> _ -> s target -> (s, s) symbol = fun p
end
let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) symbol = fun assoc from typ -> match typ with
-| TTConstr (p, forpat) -> symbol_of_target p assoc from forpat
+| TTConstr (s, p, forpat) -> symbol_of_target s p assoc from forpat
| TTConstrList (typ', [], forpat) ->
- Alist1 (symbol_of_target typ' assoc from forpat)
+ Alist1 (symbol_of_target InConstrEntry typ' assoc from forpat)
| TTConstrList (typ', tkl, forpat) ->
- Alist1sep (symbol_of_target typ' assoc from forpat, make_sep_rules tkl)
+ Alist1sep (symbol_of_target InConstrEntry typ' assoc from forpat, make_sep_rules tkl)
| TTPattern p -> Aentryl (Constr.pattern, string_of_int p)
| TTClosedBinderList [] -> Alist1 (Aentry Constr.binder)
| TTClosedBinderList tkl -> Alist1sep (Aentry Constr.binder, make_sep_rules tkl)
@@ -303,9 +355,8 @@ let interp_entry forpat e = match e with
| ETProdName -> TTAny TTName
| ETProdReference -> TTAny TTReference
| ETProdBigint -> TTAny TTBigint
-| ETProdConstr p -> TTAny (TTConstr (p, forpat))
+| ETProdConstr (s,p) -> TTAny (TTConstr (s, p, forpat))
| ETProdPattern p -> TTAny (TTPattern p)
-| ETProdOther _ -> assert false (** not used *)
| ETProdConstrList (p, tkl) -> TTAny (TTConstrList (p, tkl, forpat))
| ETProdBinderList ETBinderOpen -> TTAny TTOpenBinderList
| ETProdBinderList (ETBinderClosed tkl) -> TTAny (TTClosedBinderList tkl)
@@ -420,21 +471,23 @@ let target_to_bool : type r. r target -> bool = function
| ForConstr -> false
| ForPattern -> true
-let prepare_empty_levels forpat (pos,p4assoc,name,reinit) =
+let prepare_empty_levels forpat (where,(pos,p4assoc,name,reinit)) =
let empty = (pos, [(name, p4assoc, [])]) in
- if forpat then ExtendRule (Constr.pattern, reinit, empty)
- else ExtendRule (Constr.operconstr, reinit, empty)
-
-let rec pure_sublevels : type a b c. int option -> (a, b, c) rule -> int list = fun level r -> match r with
-| Stop -> []
-| Next (rem, Aentryl (_, i)) ->
- let i = int_of_string i in
- let rem = pure_sublevels level rem in
- begin match level with
- | Some j when Int.equal i j -> rem
- | _ -> i :: rem
- end
-| Next (rem, _) -> pure_sublevels level rem
+ ExtendRule (target_entry where forpat, reinit, empty)
+
+let rec pure_sublevels' custom assoc from forpat level = function
+| [] -> []
+| GramConstrNonTerminal (e,_) :: rem ->
+ let rem = pure_sublevels' custom assoc from forpat level rem in
+ let push where p rem =
+ match symbol_of_target custom p assoc from forpat with
+ | Aentryl (_,i) when level <> Some (int_of_string i) -> (where,int_of_string i) :: rem
+ | _ -> rem in
+ (match e with
+ | ETProdPattern i -> push InConstrEntry (NumLevel i,InternalProd) rem
+ | ETProdConstr (s,p) -> push s p rem
+ | _ -> rem)
+| (GramConstrTerminal _ | GramConstrListMark _) :: rem -> pure_sublevels' custom assoc from forpat level rem
let make_act : type r. r target -> _ -> r gen_eval = function
| ForConstr -> fun notation loc env ->
@@ -445,17 +498,17 @@ let make_act : type r. r target -> _ -> r gen_eval = function
CAst.make ~loc @@ CPatNotation (notation, env, [])
let extend_constr state forpat ng =
- let n,_,_ = ng.notgram_level in
+ let custom,n,_,_ = ng.notgram_level in
let assoc = ng.notgram_assoc in
- let (entry, level) = interp_constr_entry_key forpat n in
+ let (entry, level) = interp_constr_entry_key custom forpat n in
let fold (accu, state) pt =
let AnyTyRule r = make_ty_rule assoc n forpat pt in
let symbs = ty_erase r in
- let pure_sublevels = pure_sublevels level symbs in
+ let pure_sublevels = pure_sublevels' custom assoc n forpat level pt in
let isforpat = target_to_bool forpat in
let needed_levels, state = register_empty_levels state isforpat pure_sublevels in
- let (pos,p4assoc,name,reinit), state = find_position state isforpat assoc level in
- let empty_rules = List.map (prepare_empty_levels isforpat) needed_levels in
+ let (pos,p4assoc,name,reinit), state = find_position state custom isforpat assoc level in
+ let empty_rules = List.map (prepare_empty_levels forpat) needed_levels in
let empty = { constrs = []; constrlists = []; binders = []; binderlists = [] } in
let act = ty_eval r (make_act forpat ng.notgram_notation) empty in
let rule = (name, p4assoc, [Rule (symbs, act)]) in
@@ -468,7 +521,7 @@ let constr_levels = GramState.field ()
let extend_constr_notation ng state =
let levels = match GramState.get state constr_levels with
- | None -> default_constr_levels
+ | None -> String.Map.add "constr" default_constr_levels String.Map.empty
| Some lev -> lev
in
(* Add the notation in constr *)
diff --git a/vernac/egramcoq.mli b/vernac/egramcoq.mli
index b0341e6a17..3a6f8ae015 100644
--- a/vernac/egramcoq.mli
+++ b/vernac/egramcoq.mli
@@ -17,3 +17,6 @@
val extend_constr_grammar : Notation_gram.one_notation_grammar -> unit
(** Add a term notation rule to the parsing system. *)
+
+val create_custom_entry : local:bool -> string -> unit
+val locality_of_custom_entry : string -> bool
diff --git a/vernac/egramml.ml b/vernac/egramml.ml
index 048d4d93a0..c5dedc880e 100644
--- a/vernac/egramml.ml
+++ b/vernac/egramml.ml
@@ -64,6 +64,15 @@ let make_rule f prod =
let act = ty_eval ty_rule f in
Extend.Rule (symb, act)
+let rec proj_symbol : type a b c. (a, b, c) ty_user_symbol -> (a, b, c) genarg_type = function
+| TUentry a -> ExtraArg a
+| TUentryl (a,l) -> ExtraArg a
+| TUopt(o) -> OptArg (proj_symbol o)
+| TUlist1 l -> ListArg (proj_symbol l)
+| TUlist1sep (l,_) -> ListArg (proj_symbol l)
+| TUlist0 l -> ListArg (proj_symbol l)
+| TUlist0sep (l,_) -> ListArg (proj_symbol l)
+
(** Vernac grammar extensions *)
let vernac_exts = ref []
diff --git a/vernac/egramml.mli b/vernac/egramml.mli
index a5ee036db5..c4f4fcfaa4 100644
--- a/vernac/egramml.mli
+++ b/vernac/egramml.mli
@@ -26,6 +26,8 @@ val extend_vernac_command_grammar :
val get_extend_vernac_rule : Vernacexpr.extend_name -> vernac_expr grammar_prod_item list
+val proj_symbol : ('a, 'b, 'c) Extend.ty_user_symbol -> ('a, 'b, 'c) Genarg.genarg_type
+
(** Utility function reused in Egramcoq : *)
val make_rule :
diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml
index 504e7095b0..7cf4e64805 100644
--- a/vernac/explainErr.ml
+++ b/vernac/explainErr.ml
@@ -64,6 +64,8 @@ let process_vernac_interp_error exn = match fst exn with
wrap_vernac_error exn (Himsg.explain_type_error ctx Evd.empty te)
| PretypeError(ctx,sigma,te) ->
wrap_vernac_error exn (Himsg.explain_pretype_error ctx sigma te)
+ | Notation.NumeralNotationError(ctx,sigma,te) ->
+ wrap_vernac_error exn (Himsg.explain_numeral_notation_error ctx sigma te)
| Typeclasses_errors.TypeClassError(env, te) ->
wrap_vernac_error exn (Himsg.explain_typeclass_error env te)
| Implicit_quantifiers.MismatchedContextInstance(e,c,l,x) ->
diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg
index dacef6e211..ecc7d3ff88 100644
--- a/vernac/g_proofs.mlg
+++ b/vernac/g_proofs.mlg
@@ -13,6 +13,7 @@
open Glob_term
open Constrexpr
open Vernacexpr
+open Hints
open Proof_global
open Pcoq
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index a35a1998d3..7dd5471f3f 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -59,7 +59,7 @@ let make_bullet s =
| '*' -> Star n
| _ -> assert false
-let parse_compat_version ?(allow_old = true) = let open Flags in function
+let parse_compat_version = let open Flags in function
| "8.8" -> Current
| "8.7" -> V8_7
| "8.6" -> V8_6
@@ -83,11 +83,10 @@ GRAMMAR EXTEND Gram
]
;
decorated_vernac:
- [ [ a = attributes ; fv = vernac -> { let (f, v) = fv in (List.append a f, v) }
- | fv = vernac -> { fv } ]
- ]
+ [ [ a = LIST0 quoted_attributes ; fv = vernac ->
+ { let (f, v) = fv in (List.append (List.flatten a) f, v) } ] ]
;
- attributes:
+ quoted_attributes:
[ [ "#[" ; a = attribute_list ; "]" -> { a } ]
]
;
@@ -212,8 +211,10 @@ GRAMMAR EXTEND Gram
| IDENT "Scheme"; l = LIST1 scheme SEP "with" -> { VernacScheme l }
| IDENT "Combined"; IDENT "Scheme"; id = identref; IDENT "from";
l = LIST1 identref SEP "," -> { VernacCombinedScheme (id, l) }
- | IDENT "Register"; IDENT "Inline"; id = identref ->
- { VernacRegister(id, RegisterInline) }
+ | IDENT "Register"; g = global; "as"; quid = qualid ->
+ { VernacRegister(g, RegisterRetroknowledge quid) }
+ | IDENT "Register"; IDENT "Inline"; g = global ->
+ { VernacRegister(g, RegisterInline) }
| IDENT "Universe"; l = LIST1 identref -> { VernacUniverse l }
| IDENT "Universes"; l = LIST1 identref -> { VernacUniverse l }
| IDENT "Constraint"; l = LIST1 univ_constraint SEP "," -> { VernacConstraint l }
@@ -846,6 +847,10 @@ GRAMMAR EXTEND Gram
info = hint_info ->
{ VernacInstance (true, snd namesup, (fst namesup, expl, t), None, info) }
+ (* Should be in syntax, but camlp5 would not factorize *)
+ | IDENT "Declare"; IDENT "Scope"; sc = IDENT ->
+ { VernacDeclareScope sc }
+
(* System directory *)
| IDENT "Pwd" -> { VernacChdir None }
| IDENT "Cd" -> { VernacChdir None }
@@ -1087,6 +1092,11 @@ GRAMMAR EXTEND Gram
r = red_expr ->
{ VernacDeclareReduction (s,r) }
+(* factorized here, though relevant for syntax extensions *)
+
+ | IDENT "Declare"; IDENT "Custom"; IDENT "Entry"; s = IDENT ->
+ { VernacDeclareCustomEntry s }
+
] ];
END
@@ -1136,8 +1146,8 @@ GRAMMAR EXTEND Gram
l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> { l } | -> { [] } ]
-> { VernacSyntaxExtension (false, (s,l)) }
- (* "Print" "Grammar" should be here but is in "command" entry in order
- to factorize with other "Print"-based vernac entries *)
+ (* "Print" "Grammar" and "Declare" "Scope" should be here but are in "command" entry in order
+ to factorize with other "Print"-based or "Declare"-based vernac entries *)
] ]
;
only_parsing:
@@ -1153,6 +1163,9 @@ GRAMMAR EXTEND Gram
;
syntax_modifier:
[ [ "at"; IDENT "level"; n = natural -> { SetLevel n }
+ | "in"; IDENT "custom"; x = IDENT -> { SetCustomEntry (x,None) }
+ | "in"; IDENT "custom"; x = IDENT; "at"; IDENT "level"; n = natural ->
+ { SetCustomEntry (x,Some n) }
| IDENT "left"; IDENT "associativity" -> { SetAssoc LeftA }
| IDENT "right"; IDENT "associativity" -> { SetAssoc RightA }
| IDENT "no"; IDENT "associativity" -> { SetAssoc NonA }
@@ -1166,23 +1179,27 @@ GRAMMAR EXTEND Gram
| { CAst.v = k }, Some s -> SetFormat(k,s)
| s, None -> SetFormat ("text",s) end }
| x = IDENT; ","; l = LIST1 [id = IDENT -> { id } ] SEP ","; "at";
- lev = level -> { SetItemLevel (x::l,lev) }
- | x = IDENT; "at"; lev = level -> { SetItemLevel ([x],lev) }
- | x = IDENT; "at"; lev = level; b = constr_as_binder_kind -> { SetItemLevelAsBinder ([x],b,Some lev) }
- | x = IDENT; b = constr_as_binder_kind -> { SetItemLevelAsBinder ([x],b,None) }
+ lev = level -> { SetItemLevel (x::l,None,Some lev) }
+ | x = IDENT; "at"; lev = level -> { SetItemLevel ([x],None,Some lev) }
+ | x = IDENT; "at"; lev = level; b = constr_as_binder_kind ->
+ { SetItemLevel ([x],Some b,Some lev) }
+ | x = IDENT; b = constr_as_binder_kind -> { SetItemLevel ([x],Some b,None) }
| x = IDENT; typ = syntax_extension_type -> { SetEntryType (x,typ) }
] ]
;
syntax_extension_type:
- [ [ IDENT "ident" -> { ETName } | IDENT "global" -> { ETReference }
+ [ [ IDENT "ident" -> { ETIdent } | IDENT "global" -> { ETGlobal }
| IDENT "bigint" -> { ETBigint }
| IDENT "binder" -> { ETBinder true }
- | IDENT "constr"; n = OPT at_level; b = constr_as_binder_kind -> { ETConstrAsBinder (b,n) }
+ | IDENT "constr" -> { ETConstr (InConstrEntry,None,None) }
+ | IDENT "constr"; n = OPT at_level; b = OPT constr_as_binder_kind -> { ETConstr (InConstrEntry,b,n) }
| IDENT "pattern" -> { ETPattern (false,None) }
| IDENT "pattern"; "at"; IDENT "level"; n = natural -> { ETPattern (false,Some n) }
| IDENT "strict"; IDENT "pattern" -> { ETPattern (true,None) }
| IDENT "strict"; IDENT "pattern"; "at"; IDENT "level"; n = natural -> { ETPattern (true,Some n) }
| IDENT "closed"; IDENT "binder" -> { ETBinder false }
+ | IDENT "custom"; x = IDENT; n = OPT at_level; b = OPT constr_as_binder_kind ->
+ { ETConstr (InCustomEntry x,b,n) }
] ]
;
at_level:
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index c49ffe2679..e7b2a0e8a6 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -194,12 +194,6 @@ let rec pr_disjunction pr = function
| a::l -> pr a ++ str "," ++ spc () ++ pr_disjunction pr l
| [] -> assert false
-let pr_puniverses f env (c,u) =
- f env c ++
- (if Flags.is_universe_polymorphism () && not (Univ.Instance.is_empty u) then
- str"(*" ++ Univ.Instance.pr UnivNames.pr_with_global_universes u ++ str"*)"
- else mt())
-
let explain_elim_arity env sigma ind sorts c pj okinds =
let open EConstr in
let env = make_all_name_different env sigma in
@@ -262,7 +256,7 @@ let explain_ill_formed_branch env sigma c ci actty expty =
let pa, pe = pr_explicit env sigma (simp actty) (simp expty) in
strbrk "In pattern-matching on term" ++ brk(1,1) ++ pc ++
spc () ++ strbrk "the branch for constructor" ++ spc () ++
- quote (pr_puniverses pr_constructor env ci) ++
+ quote (pr_pconstructor env sigma ci) ++
spc () ++ str "has type" ++ brk(1,1) ++ pa ++ spc () ++
str "which should be" ++ brk(1,1) ++ pe ++ str "."
@@ -685,6 +679,11 @@ let explain_unsatisfied_constraints env sigma cst =
Univ.pr_constraints (Termops.pr_evd_level sigma) cst ++
spc () ++ str "(maybe a bugged tactic)."
+let explain_undeclared_universe env sigma l =
+ strbrk "Undeclared universe: " ++
+ Termops.pr_evd_level sigma l ++
+ spc () ++ str "(maybe a bugged tactic)."
+
let explain_type_error env sigma err =
let env = make_all_name_different env sigma in
match err with
@@ -722,6 +721,8 @@ let explain_type_error env sigma err =
explain_wrong_case_info env ind ci
| UnsatisfiedConstraints cst ->
explain_unsatisfied_constraints env sigma cst
+ | UndeclaredUniverse l ->
+ explain_undeclared_universe env sigma l
let pr_position (cl,pos) =
let clpos = match cl with
@@ -1233,12 +1234,7 @@ let explain_wrong_numarg_inductive env ind n =
str " expects " ++ decline_string n "argument" ++ str "."
let explain_unused_clause env pats =
-(* Without localisation
- let s = if List.length pats > 1 then "s" else "" in
- (str ("Unused clause with pattern"^s) ++ spc () ++
- hov 0 (pr_sequence pr_cases_pattern pats) ++ str ")")
-*)
- str "This clause is redundant."
+ str "Pattern \"" ++ hov 0 (prlist_with_sep pr_comma pr_cases_pattern pats) ++ strbrk "\" is redundant in this clause."
let explain_non_exhaustive env pats =
str "Non exhaustive pattern-matching: no clause found for " ++
@@ -1310,6 +1306,7 @@ let map_ptype_error f = function
| IllTypedRecBody (n, na, jv, t) ->
IllTypedRecBody (n, na, Array.map (on_judgment f) jv, Array.map f t)
| UnsatisfiedConstraints g -> UnsatisfiedConstraints g
+| UndeclaredUniverse l -> UndeclaredUniverse l
let explain_reduction_tactic_error = function
| Tacred.InvalidAbstraction (env,sigma,c,(env',e)) ->
@@ -1318,3 +1315,13 @@ let explain_reduction_tactic_error = function
quote (pr_goal_concl_style_env env sigma c) ++
spc () ++ str "is not well typed." ++ fnl () ++
explain_type_error env' (Evd.from_env env') e
+
+let explain_numeral_notation_error env sigma = function
+ | Notation.UnexpectedTerm c ->
+ (strbrk "Unexpected term " ++
+ pr_constr_env env sigma c ++
+ strbrk " while parsing a numeral notation.")
+ | Notation.UnexpectedNonOptionTerm c ->
+ (strbrk "Unexpected non-option term " ++
+ pr_constr_env env sigma c ++
+ strbrk " while parsing a numeral notation.")
diff --git a/vernac/himsg.mli b/vernac/himsg.mli
index 91caddcf13..02b3c45501 100644
--- a/vernac/himsg.mli
+++ b/vernac/himsg.mli
@@ -46,3 +46,5 @@ val explain_module_internalization_error :
val map_pguard_error : ('c -> 'd) -> 'c pguard_error -> 'd pguard_error
val map_ptype_error : ('c -> 'd) -> ('c, 'c) ptype_error -> ('d, 'd) ptype_error
+
+val explain_numeral_notation_error : env -> Evd.evar_map -> Notation.numeral_notation_error -> Pp.t
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index ce74f2344a..880a11becd 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -71,17 +71,13 @@ let adjust_guardness_conditions const = function
List.interval 0 (List.length ((lam_assum c))))
lemma_guard (Array.to_list fixdefs) in
*)
- let add c cb e =
- let exists c e =
- try ignore(Environ.lookup_constant c e); true
- with Not_found -> false in
- if exists c e then e else Environ.add_constant c cb e in
- let env = List.fold_left (fun env { eff } ->
- match eff with
- | SEsubproof (c, cb,_) -> add c cb env
- | SEscheme (l,_) ->
- List.fold_left (fun e (_,c,cb,_) -> add c cb e) env l)
- env (Safe_typing.side_effects_of_private_constants eff) in
+ let fold env eff =
+ try
+ let _ = Environ.lookup_constant eff.seff_constant env in
+ env
+ with Not_found -> Environ.add_constant eff.seff_constant eff.seff_body env
+ in
+ let env = List.fold_left fold env (Safe_typing.side_effects_of_private_constants eff) in
let indexes =
search_guard env
possible_indexes fixdecls in
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 33e6229b29..2e5e11bb09 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -283,20 +283,30 @@ let error_not_same_scope x y =
(**********************************************************************)
(* Build pretty-printing rules *)
+let pr_notation_entry = function
+ | InConstrEntry -> str "constr"
+ | InCustomEntry s -> str "custom " ++ str s
+
let prec_assoc = function
| RightA -> (L,E)
| LeftA -> (E,L)
| NonA -> (L,L)
-let precedence_of_position_and_level from = function
+let precedence_of_position_and_level from_level = function
| NumLevel n, BorderProd (_,None) -> n, Prec n
| NumLevel n, BorderProd (b,Some a) ->
n, let (lp,rp) = prec_assoc a in if b == Left then lp else rp
| NumLevel n, InternalProd -> n, Prec n
- | NextLevel, _ -> from, L
-
-let precedence_of_entry_type from = function
- | ETConstr x | ETConstrAsBinder (_,x) -> precedence_of_position_and_level from x
+ | NextLevel, _ -> from_level, L
+
+let precedence_of_entry_type (from_custom,from_level) = function
+ | ETConstr (custom,_,x) when notation_entry_eq custom from_custom ->
+ precedence_of_position_and_level from_level x
+ | ETConstr (custom,_,(NumLevel n,_)) -> n, Prec n
+ | ETConstr (custom,_,(NextLevel,_)) ->
+ user_err (strbrk "\"next level\" is only for sub-expressions in the same entry as where the notation is (" ++
+ quote (pr_notation_entry custom) ++ strbrk " is different from " ++
+ quote (pr_notation_entry from_custom) ++ str ").")
| ETPattern (_,n) -> let n = match n with None -> 0 | Some n -> n in n, Prec n
| _ -> 0, E (* should not matter *)
@@ -367,15 +377,14 @@ let unparsing_metavar i from typs =
let x = List.nth typs (i-1) in
let prec = snd (precedence_of_entry_type from x) in
match x with
- | ETConstr _ | ETConstrAsBinder _ | ETReference | ETBigint ->
+ | ETConstr _ | ETGlobal | ETBigint ->
UnpMetaVar (i,prec)
| ETPattern _ ->
UnpBinderMetaVar (i,prec)
- | ETName ->
- UnpBinderMetaVar (i,Prec 0)
+ | ETIdent ->
+ UnpBinderMetaVar (i,prec)
| ETBinder isopen ->
assert false
- | ETOther _ -> failwith "TODO"
(* Heuristics for building default printing rules *)
@@ -561,11 +570,10 @@ let hunks_of_format (from,(vars,typs)) symfmt =
(**********************************************************************)
(* Build parsing rules *)
-let assoc_of_type n (_,typ) = precedence_of_entry_type n typ
+let assoc_of_type from n (_,typ) = precedence_of_entry_type (from,n) typ
let is_not_small_constr = function
ETProdConstr _ -> true
- | ETProdOther("constr","binder_constr") -> true
| _ -> false
let rec define_keywords_aux = function
@@ -595,9 +603,9 @@ let distribute a ll = List.map (fun l -> a @ l) ll
t;sep;t;...;t;sep;t;...;t;sep;t (p+n times)
t;sep;t;...;t;sep;t;...;t;sep;t;LIST1(t,sep) *)
-let expand_list_rule typ tkl x n p ll =
+let expand_list_rule s typ tkl x n p ll =
let camlp5_message_name = Some (add_suffix x ("_"^string_of_int n)) in
- let main = GramConstrNonTerminal (ETProdConstr typ, camlp5_message_name) in
+ let main = GramConstrNonTerminal (ETProdConstr (s,typ), camlp5_message_name) in
let tks = List.map (fun x -> GramConstrTerminal x) tkl in
let rec aux i hds ll =
if i < p then aux (i+1) (main :: tks @ hds) ll
@@ -613,7 +621,7 @@ let expand_list_rule typ tkl x n p ll =
let is_constr_typ typ x etyps =
match List.assoc x etyps with
- | ETConstr typ' | ETConstrAsBinder (_,typ') -> typ = typ'
+ | ETConstr (_,_,typ') -> typ = typ'
| _ -> false
let include_possible_similar_trailing_pattern typ etyps sl l =
@@ -627,13 +635,12 @@ let include_possible_similar_trailing_pattern typ etyps sl l =
try_aux 0 l
let prod_entry_type = function
- | ETName -> ETProdName
- | ETReference -> ETProdReference
+ | ETIdent -> ETProdName
+ | ETGlobal -> ETProdReference
| ETBigint -> ETProdBigint
| ETBinder _ -> assert false (* See check_binder_type *)
- | ETConstr p | ETConstrAsBinder (_,p) -> ETProdConstr p
+ | ETConstr (s,_,p) -> ETProdConstr (s,p)
| ETPattern (_,n) -> ETProdPattern (match n with None -> 0 | Some n -> n)
- | ETOther (s,t) -> ETProdOther (s,t)
let make_production etyps symbols =
let rec aux = function
@@ -651,9 +658,9 @@ let make_production etyps symbols =
| Break _ -> []
| _ -> anomaly (Pp.str "Found a non terminal token in recursive notation separator.")) sl) in
match List.assoc x etyps with
- | ETConstr typ ->
+ | ETConstr (s,_,typ) ->
let p,l' = include_possible_similar_trailing_pattern typ etyps sl l in
- expand_list_rule typ tkl x 1 p (aux l')
+ expand_list_rule s typ tkl x 1 p (aux l')
| ETBinder o ->
check_open_binder o sl x;
let typ = if o then (assert (tkl = []); ETBinderOpen) else ETBinderClosed tkl in
@@ -675,8 +682,7 @@ let rec find_symbols c_current c_next c_last = function
(x,c_next)::(find_symbols c_next c_next c_last sl')
let border = function
- | (_,ETConstr(_,BorderProd (_,a))) :: _ -> a
- | (_,(ETConstrAsBinder(_,(_,BorderProd (_,a))))) :: _ -> a
+ | (_,(ETConstr(_,_,(_,BorderProd (_,a))))) :: _ -> a
| _ -> None
let recompute_assoc typs =
@@ -698,23 +704,24 @@ let pr_arg_level from (lev,typ) =
| (n,_) -> str "Unknown level" in
Ppvernac.pr_set_entry_type (fun _ -> (*TO CHECK*) mt()) typ ++
(match typ with
- | ETConstr _ | ETConstrAsBinder _ | ETPattern _ -> spc () ++ pplev lev
+ | ETConstr _ | ETPattern _ -> spc () ++ pplev lev
| _ -> mt ())
-let pr_level ntn (from,args,typs) =
- str "at level " ++ int from ++ spc () ++ str "with arguments" ++ spc() ++
- prlist_with_sep pr_comma (pr_arg_level from) (List.combine args typs)
+let pr_level ntn (from,fromlevel,args,typs) =
+ (match from with InConstrEntry -> mt () | InCustomEntry s -> str "in " ++ str s ++ spc()) ++
+ str "at level " ++ int fromlevel ++ spc () ++ str "with arguments" ++ spc() ++
+ prlist_with_sep pr_comma (pr_arg_level fromlevel) (List.combine args typs)
let error_incompatible_level ntn oldprec prec =
user_err
- (str "Notation " ++ qstring ntn ++ str " is already defined" ++ spc() ++
+ (str "Notation " ++ pr_notation ntn ++ str " is already defined" ++ spc() ++
pr_level ntn oldprec ++
spc() ++ str "while it is now required to be" ++ spc() ++
pr_level ntn prec ++ str ".")
let error_parsing_incompatible_level ntn ntn' oldprec prec =
user_err
- (str "Notation " ++ qstring ntn ++ str " relies on a parsing rule for " ++ qstring ntn' ++ spc() ++
+ (str "Notation " ++ pr_notation ntn ++ str " relies on a parsing rule for " ++ pr_notation ntn' ++ spc() ++
str " which is already defined" ++ spc() ++
pr_level ntn oldprec ++
spc() ++ str "while it is now required to be" ++ spc() ++
@@ -738,7 +745,7 @@ type syntax_extension_obj = locality_flag * syntax_extension
let check_and_extend_constr_grammar ntn rule =
try
let ntn_for_grammar = rule.notgram_notation in
- if String.equal ntn ntn_for_grammar then raise Not_found;
+ if notation_eq ntn ntn_for_grammar then raise Not_found;
let prec = rule.notgram_level in
let oldprec = Notgram_ops.level_of_notation ntn_for_grammar in
if not (Notgram_ops.level_eq prec oldprec) then error_parsing_incompatible_level ntn ntn_for_grammar oldprec prec;
@@ -760,7 +767,7 @@ let cache_one_syntax_extension se =
if not onlyprint then List.iter (check_and_extend_constr_grammar ntn) se.synext_notgram.notgram_rules;
(* Declare the notation rule *)
declare_notation_rule ntn
- ~extra:se.synext_extra (se.synext_unparsing, pi1 prec) se.synext_notgram
+ ~extra:se.synext_extra (se.synext_unparsing, let (_,lev,_,_) = prec in lev) se.synext_notgram
end
let cache_syntax_extension (_, (_, sy)) =
@@ -797,7 +804,9 @@ module NotationMods = struct
type notation_modifier = {
assoc : gram_assoc option;
level : int option;
+ custom : notation_entry;
etyps : (Id.t * simple_constr_prod_entry_key) list;
+ subtyps : (Id.t * production_level) list;
(* common to syn_data below *)
only_parsing : bool;
@@ -810,7 +819,9 @@ type notation_modifier = {
let default = {
assoc = None;
level = None;
+ custom = InConstrEntry;
etyps = [];
+ subtyps = [];
only_parsing = false;
only_printing = false;
compat = None;
@@ -821,53 +832,75 @@ let default = {
end
let interp_modifiers modl = let open NotationMods in
- let rec interp acc = function
- | [] -> acc
+ let rec interp subtyps acc = function
+ | [] -> subtyps, acc
| SetEntryType (s,typ) :: l ->
let id = Id.of_string s in
if Id.List.mem_assoc id acc.etyps then
user_err ~hdr:"Metasyntax.interp_modifiers"
(str s ++ str " is already assigned to an entry or constr level.");
- interp { acc with etyps = (id,typ) :: acc.etyps; } l
- | SetItemLevel ([],n) :: l ->
- interp acc l
- | SetItemLevelAsBinder ([],_,_) :: l ->
- interp acc l
- | SetItemLevel (s::idl,n) :: l ->
+ interp subtyps { acc with etyps = (id,typ) :: acc.etyps; } l
+ | SetItemLevel ([],bko,n) :: l ->
+ interp subtyps acc l
+ | SetItemLevel (s::idl,bko,n) :: l ->
let id = Id.of_string s in
if Id.List.mem_assoc id acc.etyps then
user_err ~hdr:"Metasyntax.interp_modifiers"
(str s ++ str " is already assigned to an entry or constr level.");
- let typ = ETConstr (Some n) in
- interp { acc with etyps = (id,typ)::acc.etyps; } (SetItemLevel (idl,n)::l)
- | SetItemLevelAsBinder (s::idl,bk,n) :: l ->
- let id = Id.of_string s in
- if Id.List.mem_assoc id acc.etyps then
- user_err ~hdr:"Metasyntax.interp_modifiers"
- (str s ++ str " is already assigned to an entry or constr level.");
- let typ = ETConstrAsBinder (bk,n) in
- interp { acc with etyps = (id,typ)::acc.etyps; } (SetItemLevelAsBinder (idl,bk,n)::l)
+ interp ((id,bko,n)::subtyps) acc (SetItemLevel (idl,bko,n)::l)
| SetLevel n :: l ->
- interp { acc with level = Some n; } l
+ (match acc.custom with
+ | InCustomEntry s ->
+ if acc.level <> None then
+ user_err (str ("isolated \"at level " ^ string_of_int n ^ "\" unexpected."))
+ else
+ user_err (str ("use \"in custom " ^ s ^ " at level " ^ string_of_int n ^
+ "\"") ++ spc () ++ str "rather than" ++ spc () ++
+ str ("\"at level " ^ string_of_int n ^ "\"") ++
+ spc () ++ str "isolated.")
+ | InConstrEntry ->
+ if acc.level <> None then
+ user_err (str "A level is already assigned.");
+ interp subtyps { acc with level = Some n; } l)
+ | SetCustomEntry (s,n) :: l ->
+ if acc.level <> None then
+ (if n = None then
+ user_err (str ("use \"in custom " ^ s ^ " at level " ^
+ string_of_int (Option.get acc.level) ^
+ "\"") ++ spc () ++ str "rather than" ++ spc () ++
+ str ("\"at level " ^
+ string_of_int (Option.get acc.level) ^ "\"") ++
+ spc () ++ str "isolated.")
+ else
+ user_err (str ("isolated \"at level " ^ string_of_int (Option.get acc.level) ^ "\" unexpected.")));
+ if acc.custom <> InConstrEntry then
+ user_err (str "Entry is already assigned to custom " ++ str s ++ (match acc.level with None -> mt () | Some lev -> str " at level " ++ int lev) ++ str ".");
+ interp subtyps { acc with custom = InCustomEntry s; level = n } l
| SetAssoc a :: l ->
if not (Option.is_empty acc.assoc) then user_err Pp.(str "An associativity is given more than once.");
- interp { acc with assoc = Some a; } l
+ interp subtyps { acc with assoc = Some a; } l
| SetOnlyParsing :: l ->
- interp { acc with only_parsing = true; } l
+ interp subtyps { acc with only_parsing = true; } l
| SetOnlyPrinting :: l ->
- interp { acc with only_printing = true; } l
+ interp subtyps { acc with only_printing = true; } l
| SetCompatVersion v :: l ->
- interp { acc with compat = Some v; } l
+ interp subtyps { acc with compat = Some v; } l
| SetFormat ("text",s) :: l ->
if not (Option.is_empty acc.format) then user_err Pp.(str "A format is given more than once.");
- interp { acc with format = Some s; } l
- | SetFormat (k,{CAst.v=s}) :: l ->
- interp { acc with extra = (k,s)::acc.extra; } l
- in interp default modl
+ interp subtyps { acc with format = Some s; } l
+ | SetFormat (k,s) :: l ->
+ interp subtyps { acc with extra = (k,s.CAst.v)::acc.extra; } l
+ in
+ let subtyps,mods = interp [] default modl in
+ (* interpret item levels wrt to main entry *)
+ let extra_etyps = List.map (fun (id,bko,n) -> (id,ETConstr (mods.custom,bko,n))) subtyps in
+ { mods with etyps = extra_etyps@mods.etyps }
let check_infix_modifiers modifiers =
- let t = (interp_modifiers modifiers).NotationMods.etyps in
- if not (List.is_empty t) then
+ let mods = interp_modifiers modifiers in
+ let t = mods.NotationMods.etyps in
+ let u = mods.NotationMods.subtyps in
+ if not (List.is_empty t) || not (List.is_empty u) then
user_err Pp.(str "Explicit entry level or type unexpected in infix notation.")
let check_useless_entry_types recvars mainvars etyps =
@@ -908,21 +941,18 @@ let get_compat_version mods =
(* Compute precedences from modifiers (or find default ones) *)
-let set_entry_type etyps (x,typ) =
+let set_entry_type from etyps (x,typ) =
let typ = try
match List.assoc x etyps, typ with
- | ETConstr (Some n), (_,BorderProd (left,_)) ->
- ETConstr (n,BorderProd (left,None))
- | ETConstr (Some n), (_,InternalProd) -> ETConstr (n,InternalProd)
- | ETConstrAsBinder (bk, Some n), (_,BorderProd (left,_)) ->
- ETConstrAsBinder (bk, (n,BorderProd (left,None)))
- | ETConstrAsBinder (bk, Some n), (_,InternalProd) ->
- ETConstrAsBinder (bk, (n,InternalProd))
+ | ETConstr (s,bko,Some n), (_,BorderProd (left,_)) ->
+ ETConstr (s,bko,(n,BorderProd (left,None)))
+ | ETConstr (s,bko,Some n), (_,InternalProd) ->
+ ETConstr (s,bko,(n,InternalProd))
| ETPattern (b,n), _ -> ETPattern (b,n)
- | (ETName | ETBigint | ETReference | ETBinder _ | ETOther _ as x), _ -> x
- | ETConstr None, _ -> ETConstr typ
- | ETConstrAsBinder (bk,None), _ -> ETConstrAsBinder (bk,typ)
- with Not_found -> ETConstr typ
+ | (ETIdent | ETBigint | ETGlobal | ETBinder _ as x), _ -> x
+ | ETConstr (s,bko,None), _ -> ETConstr (s,bko,typ)
+ with Not_found ->
+ ETConstr (from,None,typ)
in (x,typ)
let join_auxiliary_recursive_types recvars etyps =
@@ -942,8 +972,8 @@ let join_auxiliary_recursive_types recvars etyps =
let internalization_type_of_entry_type = function
| ETBinder _ -> NtnInternTypeOnlyBinder
- | ETConstr _ | ETConstrAsBinder _ | ETBigint | ETReference
- | ETName | ETPattern _ | ETOther _ -> NtnInternTypeAny
+ | ETConstr _ | ETBigint | ETGlobal
+ | ETIdent | ETPattern _ -> NtnInternTypeAny
let set_internalization_type typs =
List.map (fun (_, e) -> internalization_type_of_entry_type e) typs
@@ -954,20 +984,28 @@ let make_internalization_vars recvars mainvars typs =
maintyps @ extratyps
let make_interpretation_type isrec isonlybinding = function
- | ETConstr _ ->
- if isrec then NtnTypeConstrList else
- if isonlybinding then
- (* Parsed as constr, but interpreted as a binder: default is to parse it as an ident only *)
- NtnTypeBinder (NtnBinderParsedAsConstr AsIdent)
- else NtnTypeConstr
- | ETConstrAsBinder (bk,_) -> NtnTypeBinder (NtnBinderParsedAsConstr bk)
- | ETName -> NtnTypeBinder NtnParsedAsIdent
+ (* Parsed as constr list *)
+ | ETConstr (_,None,_) when isrec -> NtnTypeConstrList
+ (* Parsed as constr, but interpreted as a binder: default is to parse it as an ident only *)
+ | ETConstr (_,Some bk,_) -> NtnTypeBinder (NtnBinderParsedAsConstr bk)
+ | ETConstr (_,None,_) when isonlybinding -> NtnTypeBinder (NtnBinderParsedAsConstr AsIdent)
+ (* Parsed as constr, interpreted as constr *)
+ | ETConstr (_,None,_) -> NtnTypeConstr
+ (* Others *)
+ | ETIdent -> NtnTypeBinder NtnParsedAsIdent
| ETPattern (ppstrict,_) -> NtnTypeBinder (NtnParsedAsPattern ppstrict) (* Parsed as ident/pattern, primarily interpreted as binder; maybe strict at printing *)
- | ETBigint | ETReference | ETOther _ -> NtnTypeConstr
+ | ETBigint | ETGlobal -> NtnTypeConstr
| ETBinder _ ->
if isrec then NtnTypeBinderList
else anomaly Pp.(str "Type binder is only for use in recursive notations for binders.")
+let subentry_of_constr_prod_entry = function
+ | ETConstr (InCustomEntry s,_,(NumLevel n,_)) -> InCustomEntryLevel (s,n)
+ (* level and use of parentheses for coercion is hard-wired for "constr";
+ we don't remember the level *)
+ | ETConstr (InConstrEntry,_,_) -> InConstrEntrySomeLevel
+ | _ -> InConstrEntrySomeLevel
+
let make_interpretation_vars recvars allvars typs =
let eq_subscope (sc1, l1) (sc2, l2) =
Option.equal String.equal sc1 sc2 &&
@@ -983,7 +1021,9 @@ let make_interpretation_vars recvars allvars typs =
let mainvars =
Id.Map.filter (fun x _ -> not (Id.List.mem x useless_recvars)) allvars in
Id.Map.mapi (fun x (isonlybinding, sc) ->
- (sc, make_interpretation_type (Id.List.mem_assoc x recvars) isonlybinding (Id.List.assoc x typs))) mainvars
+ let typ = Id.List.assoc x typs in
+ ((subentry_of_constr_prod_entry typ,sc),
+ make_interpretation_type (Id.List.mem_assoc x recvars) isonlybinding typ)) mainvars
let check_rule_productivity l =
if List.for_all (function NonTerminal _ | Break _ -> true | _ -> false) l then
@@ -1009,17 +1049,42 @@ let warn_non_reversible_notation =
str " not occur in the right-hand side." ++ spc() ++
strbrk "The notation will not be used for printing as it is not reversible.")
-let is_not_printable onlyparse reversibility = function
-| NVar _ ->
- if not onlyparse then warn_notation_bound_to_variable ();
- true
+let make_custom_entry custom level =
+ match custom with
+ | InConstrEntry -> InConstrEntrySomeLevel
+ | InCustomEntry s -> InCustomEntryLevel (s,level)
+
+type entry_coercion_kind =
+ | IsEntryCoercion of notation_entry_level
+ | IsEntryGlobal of string * int
+ | IsEntryIdent of string * int
+
+let is_coercion = function
+ | Some (custom,n,_,[e]) ->
+ (match e, custom with
+ | ETConstr _, _ ->
+ let customkey = make_custom_entry custom n in
+ let subentry = subentry_of_constr_prod_entry e in
+ if notation_entry_level_eq subentry customkey then None
+ else Some (IsEntryCoercion subentry)
+ | ETGlobal, InCustomEntry s -> Some (IsEntryGlobal (s,n))
+ | ETIdent, InCustomEntry s -> Some (IsEntryIdent (s,n))
+ | _ -> None)
+ | Some _ -> assert false
+ | None -> None
+
+let printability level onlyparse reversibility = function
+| NVar _ when reversibility = APrioriReversible ->
+ let coe = is_coercion level in
+ if not onlyparse && coe = None then
+ warn_notation_bound_to_variable ();
+ true, coe
| _ ->
- if not onlyparse && reversibility <> APrioriReversible then
+ (if not onlyparse && reversibility <> APrioriReversible then
(warn_non_reversible_notation reversibility; true)
- else onlyparse
-
+ else onlyparse),None
-let find_precedence lev etyps symbols onlyprint =
+let find_precedence custom lev etyps symbols onlyprint =
let first_symbol =
let rec aux = function
| Break _ :: t -> aux t
@@ -1043,10 +1108,9 @@ let find_precedence lev etyps symbols onlyprint =
else [],Option.get lev
else
user_err Pp.(str "The level of the leftmost non-terminal cannot be changed.") in
- (try match List.assoc x etyps with
- | ETConstr _ -> test ()
- | ETConstrAsBinder (_,Some _) -> test ()
- | (ETName | ETBigint | ETReference) ->
+ (try match List.assoc x etyps, custom with
+ | ETConstr (s,_,Some _), s' when s = s' -> test ()
+ | (ETIdent | ETBigint | ETGlobal), _ ->
begin match lev with
| None ->
([Feedback.msg_info ?loc:None ,strbrk "Setting notation at level 0."],0)
@@ -1055,7 +1119,7 @@ let find_precedence lev etyps symbols onlyprint =
| _ ->
user_err Pp.(str "A notation starting with an atomic expression must be at level 0.")
end
- | (ETPattern _ | ETBinder _ | ETOther _ | ETConstrAsBinder _) ->
+ | (ETPattern _ | ETBinder _ | ETConstr _), _ ->
(* Give a default ? *)
if Option.is_empty lev then
user_err Pp.(str "Need an explicit level.")
@@ -1073,7 +1137,7 @@ let find_precedence lev etyps symbols onlyprint =
[],Option.get lev
let check_curly_brackets_notation_exists () =
- try let _ = Notgram_ops.level_of_notation "{ _ }" in ()
+ try let _ = Notgram_ops.level_of_notation (InConstrEntrySomeLevel,"{ _ }") in ()
with Not_found ->
user_err Pp.(str "Notations involving patterns of the form \"{ _ }\" are treated \n\
specially and require that the notation \"{ _ }\" is already reserved.")
@@ -1103,7 +1167,7 @@ let remove_curly_brackets l =
module SynData = struct
- type subentry_types = (Id.t * (production_level * production_position) constr_entry_key_gen) list
+ type subentry_types = (Id.t * constr_entry_key) list
(* XXX: Document *)
type syn_data = {
@@ -1137,7 +1201,7 @@ module SynData = struct
end
-let find_subentry_types n assoc etyps symbols =
+let find_subentry_types from n assoc etyps symbols =
let innerlevel = NumLevel 200 in
let typs =
find_symbols
@@ -1145,11 +1209,21 @@ let find_subentry_types n assoc etyps symbols =
(innerlevel,InternalProd)
(NumLevel n,BorderProd(Right,assoc))
symbols in
- let sy_typs = List.map (set_entry_type etyps) typs in
- let prec = List.map (assoc_of_type n) sy_typs in
+ let sy_typs = List.map (set_entry_type from etyps) typs in
+ let prec = List.map (assoc_of_type from n) sy_typs in
sy_typs, prec
-let compute_syntax_data df modifiers =
+let check_locality_compatibility local custom i_typs =
+ if not local then
+ let subcustom = List.map_filter (function _,ETConstr (InCustomEntry s,_,_) -> Some s | _ -> None) i_typs in
+ let allcustoms = match custom with InCustomEntry s -> s::subcustom | _ -> subcustom in
+ List.iter (fun s ->
+ if Egramcoq.locality_of_custom_entry s then
+ user_err (strbrk "Notation has to be declared local as it depends on custom entry " ++ str s ++
+ strbrk " which is local."))
+ (List.uniquize allcustoms)
+
+let compute_syntax_data local df modifiers =
let open SynData in
let open NotationMods in
let mods = interp_modifiers modifiers in
@@ -1162,25 +1236,28 @@ let compute_syntax_data df modifiers =
let _ = check_binder_type recvars mods.etyps in
(* Notations for interp and grammar *)
- let ntn_for_interp = make_notation_key symbols in
- let symbols_for_grammar = remove_curly_brackets symbols in
+ let msgs,n = find_precedence mods.custom mods.level mods.etyps symbols onlyprint in
+ let custom = make_custom_entry mods.custom n in
+ let ntn_for_interp = make_notation_key custom symbols in
+ let symbols_for_grammar =
+ if custom = InConstrEntrySomeLevel then remove_curly_brackets symbols else symbols in
let need_squash = not (List.equal Notation.symbol_eq symbols symbols_for_grammar) in
- let ntn_for_grammar = if need_squash then make_notation_key symbols_for_grammar else ntn_for_interp in
- if not onlyprint then check_rule_productivity symbols_for_grammar;
- let msgs,n = find_precedence mods.level mods.etyps symbols onlyprint in
+ let ntn_for_grammar = if need_squash then make_notation_key custom symbols_for_grammar else ntn_for_interp in
+ if mods.custom = InConstrEntry && not onlyprint then check_rule_productivity symbols_for_grammar;
(* To globalize... *)
let etyps = join_auxiliary_recursive_types recvars mods.etyps in
let sy_typs, prec =
- find_subentry_types n assoc etyps symbols in
+ find_subentry_types mods.custom n assoc etyps symbols in
let sy_typs_for_grammar, prec_for_grammar =
if need_squash then
- find_subentry_types n assoc etyps symbols_for_grammar
+ find_subentry_types mods.custom n assoc etyps symbols_for_grammar
else
sy_typs, prec in
let i_typs = set_internalization_type sy_typs in
+ check_locality_compatibility local mods.custom sy_typs;
let pa_sy_data = (sy_typs_for_grammar,symbols_for_grammar) in
let pp_sy_data = (sy_typs,symbols) in
- let sy_fulldata = (ntn_for_grammar,(n,prec_for_grammar,List.map snd sy_typs_for_grammar),need_squash) in
+ let sy_fulldata = (ntn_for_grammar,(mods.custom,n,prec_for_grammar,List.map snd sy_typs_for_grammar),need_squash) in
let df' = ((Lib.library_dp(),Lib.current_dirpath true),df) in
let i_data = ntn_for_interp, df' in
@@ -1199,15 +1276,15 @@ let compute_syntax_data df modifiers =
mainvars;
intern_typs = i_typs;
- level = (n,prec,List.map snd sy_typs);
+ level = (mods.custom,n,prec,List.map snd sy_typs);
pa_syntax_data = pa_sy_data;
pp_syntax_data = pp_sy_data;
not_data = sy_fulldata;
}
-let compute_pure_syntax_data df mods =
+let compute_pure_syntax_data local df mods =
let open SynData in
- let sd = compute_syntax_data df mods in
+ let sd = compute_syntax_data local df mods in
let msgs =
if sd.only_parsing then
(Feedback.msg_warning ?loc:None,
@@ -1222,14 +1299,25 @@ type notation_obj = {
notobj_local : bool;
notobj_scope : scope_name option;
notobj_interp : interpretation;
+ notobj_coercion : entry_coercion_kind option;
notobj_onlyparse : bool;
notobj_onlyprint : bool;
notobj_compat : Flags.compat_version option;
notobj_notation : notation * notation_location;
}
-let load_notation _ (_, nobj) =
- Option.iter Notation.declare_scope nobj.notobj_scope
+let load_notation_common silently_define_scope_if_undefined _ (_, nobj) =
+ (* When the default shall be to require that a scope already exists *)
+ (* the call to ensure_scope will have to be removed *)
+ if silently_define_scope_if_undefined then
+ (* Don't warn if the scope is not defined: *)
+ (* there was already a warning at "cache" time *)
+ Option.iter Notation.declare_scope nobj.notobj_scope
+ else
+ Option.iter Notation.ensure_scope nobj.notobj_scope
+
+let load_notation =
+ load_notation_common true
let open_notation i (_, nobj) =
let scope = nobj.notobj_scope in
@@ -1243,11 +1331,17 @@ let open_notation i (_, nobj) =
let () = Notation.declare_notation_interpretation ntn scope pat df ~onlyprint in
(* Declare the uninterpretation *)
if not nobj.notobj_onlyparse then
- Notation.declare_uninterpretation (NotationRule (scope, ntn)) pat
+ Notation.declare_uninterpretation (NotationRule (scope, ntn)) pat;
+ (* Declare a possible coercion *)
+ (match nobj.notobj_coercion with
+ | Some (IsEntryCoercion entry) -> Notation.declare_entry_coercion ntn entry
+ | Some (IsEntryGlobal (entry,n)) -> Notation.declare_custom_entry_has_global entry n
+ | Some (IsEntryIdent (entry,n)) -> Notation.declare_custom_entry_has_ident entry n
+ | None -> ())
end
let cache_notation o =
- load_notation 1 o;
+ load_notation_common false 1 o;
open_notation 1 o
let subst_notation (subst, nobj) =
@@ -1301,7 +1395,7 @@ let recover_notation_syntax ntn =
raise NoSyntaxRule
let recover_squash_syntax sy =
- let sq = recover_notation_syntax "{ _ }" in
+ let sq = recover_notation_syntax (InConstrEntrySomeLevel,"{ _ }") in
sy :: sq.synext_notgram.notgram_rules
(**********************************************************************)
@@ -1336,8 +1430,9 @@ let make_pp_rule level (typs,symbols) fmt =
(* let make_syntax_rules i_typs (ntn,prec,need_squash) sy_data fmt extra onlyprint compat = *)
let make_syntax_rules (sd : SynData.syn_data) = let open SynData in
let ntn_for_grammar, prec_for_grammar, need_squash = sd.not_data in
+ let custom,level,_,_ = sd.level in
let pa_rule = make_pa_rule prec_for_grammar sd.pa_syntax_data ntn_for_grammar need_squash in
- let pp_rule = make_pp_rule (pi1 sd.level) sd.pp_syntax_data sd.format in {
+ let pp_rule = make_pp_rule (custom,level) sd.pp_syntax_data sd.format in {
synext_level = sd.level;
synext_notation = fst sd.info;
synext_notgram = { notgram_onlyprinting = sd.only_printing; notgram_rules = pa_rule };
@@ -1355,7 +1450,7 @@ let to_map l =
let add_notation_in_scope local df env c mods scope =
let open SynData in
- let sd = compute_syntax_data df mods in
+ let sd = compute_syntax_data local df mods in
(* Prepare the interpretation *)
(* Prepare the parsing and printing rules *)
let sy_rules = make_syntax_rules sd in
@@ -1367,13 +1462,14 @@ let add_notation_in_scope local df env c mods scope =
let (acvars, ac, reversibility) = interp_notation_constr env nenv c in
let interp = make_interpretation_vars sd.recvars acvars (fst sd.pa_syntax_data) in
let map (x, _) = try Some (x, Id.Map.find x interp) with Not_found -> None in
- let onlyparse = is_not_printable sd.only_parsing reversibility ac in
+ let onlyparse,coe = printability (Some sd.level) sd.only_parsing reversibility ac in
let notation = {
notobj_local = local;
notobj_scope = scope;
notobj_interp = (List.map_filter map i_vars, ac);
(** Order is important here! *)
notobj_onlyparse = onlyparse;
+ notobj_coercion = coe;
notobj_onlyprint = sd.only_printing;
notobj_compat = sd.compat;
notobj_notation = sd.info;
@@ -1387,16 +1483,17 @@ let add_notation_in_scope local df env c mods scope =
let add_notation_interpretation_core local df env ?(impls=empty_internalization_env) c scope onlyparse onlyprint compat =
let (recvars,mainvars,symbs) = analyze_notation_tokens ~onlyprint df in
(* Recover types of variables and pa/pp rules; redeclare them if needed *)
- let i_typs, onlyprint = if not (is_numeral symbs) then begin
- let sy = recover_notation_syntax (make_notation_key symbs) in
+ let level, i_typs, onlyprint = if not (is_numeral symbs) then begin
+ let sy = recover_notation_syntax (make_notation_key InConstrEntrySomeLevel symbs) in
let () = Lib.add_anonymous_leaf (inSyntaxExtension (local,sy)) in
(** If the only printing flag has been explicitly requested, put it back *)
let onlyprint = onlyprint || sy.synext_notgram.notgram_onlyprinting in
- pi3 sy.synext_level, onlyprint
- end else [], false in
+ let _,_,_,typs = sy.synext_level in
+ Some sy.synext_level, typs, onlyprint
+ end else None, [], false in
(* Declare interpretation *)
let path = (Lib.library_dp(), Lib.current_dirpath true) in
- let df' = (make_notation_key symbs, (path,df)) in
+ let df' = (make_notation_key InConstrEntrySomeLevel symbs, (path,df)) in
let i_vars = make_internalization_vars recvars mainvars (List.map internalization_type_of_entry_type i_typs) in
let nenv = {
ninterp_var_type = to_map i_vars;
@@ -1405,13 +1502,14 @@ let add_notation_interpretation_core local df env ?(impls=empty_internalization_
let (acvars, ac, reversibility) = interp_notation_constr env ~impls nenv c in
let interp = make_interpretation_vars recvars acvars (List.combine mainvars i_typs) in
let map (x, _) = try Some (x, Id.Map.find x interp) with Not_found -> None in
- let onlyparse = is_not_printable onlyparse reversibility ac in
+ let onlyparse,coe = printability level onlyparse reversibility ac in
let notation = {
notobj_local = local;
notobj_scope = scope;
notobj_interp = (List.map_filter map i_vars, ac);
(** Order is important here! *)
notobj_onlyparse = onlyparse;
+ notobj_coercion = coe;
notobj_onlyprint = onlyprint;
notobj_compat = compat;
notobj_notation = df';
@@ -1422,7 +1520,7 @@ let add_notation_interpretation_core local df env ?(impls=empty_internalization_
(* Notations without interpretation (Reserved Notation) *)
let add_syntax_extension local ({CAst.loc;v=df},mods) = let open SynData in
- let psd = compute_pure_syntax_data df mods in
+ let psd = compute_pure_syntax_data local df mods in
let sy_rules = make_syntax_rules {psd with compat = None} in
Flags.if_verbose (List.iter (fun (f,x) -> f x)) psd.msgs;
Lib.add_anonymous_leaf (inSyntaxExtension(local,sy_rules))
@@ -1462,7 +1560,7 @@ let add_notation local env c ({CAst.loc;v=df},modifiers) sc =
let add_notation_extra_printing_rule df k v =
let notk =
let _,_, symbs = analyze_notation_tokens ~onlyprint:true df in
- make_notation_key symbs in
+ make_notation_key InConstrEntrySomeLevel symbs in
add_notation_extra_printing_rule notk k v
(* Infix notations *)
@@ -1478,52 +1576,72 @@ let add_infix local env ({CAst.loc;v=inf},modifiers) pr sc =
add_notation local env c (df,modifiers) sc
(**********************************************************************)
-(* Delimiters and classes bound to scopes *)
+(* Scopes, delimiters and classes bound to scopes *)
type scope_command =
- | ScopeDelim of string
+ | ScopeDeclare
+ | ScopeDelimAdd of string
+ | ScopeDelimRemove
| ScopeClasses of scope_class list
- | ScopeRemove
-
-let load_scope_command _ (_,(scope,dlm)) =
- Notation.declare_scope scope
-let open_scope_command i (_,(scope,o)) =
+let load_scope_command_common silently_define_scope_if_undefined _ (_,(local,scope,o)) =
+ let declare_scope_if_needed =
+ if silently_define_scope_if_undefined then Notation.declare_scope
+ else Notation.ensure_scope in
+ match o with
+ | ScopeDeclare -> Notation.declare_scope scope
+ (* When the default shall be to require that a scope already exists *)
+ (* the call to declare_scope_if_needed will have to be removed below *)
+ | ScopeDelimAdd dlm -> declare_scope_if_needed scope
+ | ScopeDelimRemove -> declare_scope_if_needed scope
+ | ScopeClasses cl -> declare_scope_if_needed scope
+
+let load_scope_command =
+ load_scope_command_common true
+
+let open_scope_command i (_,(local,scope,o)) =
if Int.equal i 1 then
match o with
- | ScopeDelim dlm -> Notation.declare_delimiters scope dlm
+ | ScopeDeclare -> ()
+ | ScopeDelimAdd dlm -> Notation.declare_delimiters scope dlm
+ | ScopeDelimRemove -> Notation.remove_delimiters scope
| ScopeClasses cl -> List.iter (Notation.declare_scope_class scope) cl
- | ScopeRemove -> Notation.remove_delimiters scope
let cache_scope_command o =
- load_scope_command 1 o;
+ load_scope_command_common false 1 o;
open_scope_command 1 o
-let subst_scope_command (subst,(scope,o as x)) = match o with
+let subst_scope_command (subst,(local,scope,o as x)) = match o with
| ScopeClasses cl ->
let cl' = List.map_filter (subst_scope_class subst) cl in
let cl' =
if List.for_all2eq (==) cl cl' then cl
else cl' in
- scope, ScopeClasses cl'
+ local, scope, ScopeClasses cl'
| _ -> x
-let inScopeCommand : scope_name * scope_command -> obj =
+let classify_scope_command (local, _, _ as o) =
+ if local then Dispose else Substitute o
+
+let inScopeCommand : locality_flag * scope_name * scope_command -> obj =
declare_object {(default_object "DELIMITERS") with
cache_function = cache_scope_command;
open_function = open_scope_command;
load_function = load_scope_command;
subst_function = subst_scope_command;
- classify_function = (fun obj -> Substitute obj)}
+ classify_function = classify_scope_command}
+
+let declare_scope local scope =
+ Lib.add_anonymous_leaf (inScopeCommand(local,scope,ScopeDeclare))
-let add_delimiters scope key =
- Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeDelim key))
+let add_delimiters local scope key =
+ Lib.add_anonymous_leaf (inScopeCommand(local,scope,ScopeDelimAdd key))
-let remove_delimiters scope =
- Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeRemove))
+let remove_delimiters local scope =
+ Lib.add_anonymous_leaf (inScopeCommand(local,scope,ScopeDelimRemove))
-let add_class_scope scope cl =
- Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeClasses cl))
+let add_class_scope local scope cl =
+ Lib.add_anonymous_leaf (inScopeCommand(local,scope,ScopeClasses cl))
(* Check if abbreviation to a name and avoid early insertion of
maximal implicit arguments *)
@@ -1546,7 +1664,35 @@ let add_syntactic_definition env ident (vars,c) local onlyparse =
List.map map vars, reversibility, pat
in
let onlyparse = match onlyparse with
- | None when (is_not_printable false reversibility pat) -> Some Flags.Current
+ | None when fst (printability None false reversibility pat) -> Some Flags.Current
| p -> p
in
Syntax_def.declare_syntactic_definition local ident onlyparse (vars,pat)
+
+(**********************************************************************)
+(* Declaration of custom entry *)
+
+let load_custom_entry _ _ = ()
+
+let open_custom_entry _ (_,(local,s)) =
+ Egramcoq.create_custom_entry ~local s
+
+let cache_custom_entry o =
+ load_custom_entry 1 o;
+ open_custom_entry 1 o
+
+let subst_custom_entry (subst,x) = x
+
+let classify_custom_entry (local,s as o) =
+ if local then Dispose else Substitute o
+
+let inCustomEntry : locality_flag * string -> obj =
+ declare_object {(default_object "CUSTOM-ENTRIES") with
+ cache_function = cache_custom_entry;
+ open_function = open_custom_entry;
+ load_function = load_custom_entry;
+ subst_function = subst_custom_entry;
+ classify_function = classify_custom_entry}
+
+let declare_custom_entry local s =
+ Lib.add_anonymous_leaf (inCustomEntry (local,s))
diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli
index f6de75b079..38dbdf7e41 100644
--- a/vernac/metasyntax.mli
+++ b/vernac/metasyntax.mli
@@ -27,11 +27,12 @@ val add_notation : locality_flag -> env -> constr_expr ->
val add_notation_extra_printing_rule : string -> string -> string -> unit
-(** Declaring delimiter keys and default scopes *)
+(** Declaring scopes, delimiter keys and default scopes *)
-val add_delimiters : scope_name -> string -> unit
-val remove_delimiters : scope_name -> unit
-val add_class_scope : scope_name -> scope_class list -> unit
+val declare_scope : locality_flag -> scope_name -> unit
+val add_delimiters : locality_flag -> scope_name -> string -> unit
+val remove_delimiters : locality_flag -> scope_name -> unit
+val add_class_scope : locality_flag -> scope_name -> scope_class list -> unit
(** Add only the interpretation of a notation that already has pa/pp rules *)
@@ -60,3 +61,5 @@ val pr_grammar : string -> Pp.t
val check_infix_modifiers : syntax_modifier list -> unit
val with_syntax_protection : ('a -> 'b) -> 'a -> 'b
+
+val declare_custom_entry : locality_flag -> string -> unit
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 14d7642328..3987e53bc7 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -523,11 +523,11 @@ let declare_mutual_definition l =
(List.map (fun x ->
let subs, typ = (subst_body true x) in
let env = Global.env () in
- let sigma = Evd.from_env env in
+ let sigma = Evd.from_ctx x.prg_ctx in
let term = snd (Reductionops.splay_lam_n env sigma len (EConstr.of_constr subs)) in
let typ = snd (Reductionops.splay_prod_n env sigma len (EConstr.of_constr typ)) in
- let term = EConstr.Unsafe.to_constr term in
- let typ = EConstr.Unsafe.to_constr typ in
+ let term = EConstr.to_constr sigma term in
+ let typ = EConstr.to_constr sigma typ in
x.prg_reduce term, x.prg_reduce typ, x.prg_implicits) l)
in
(* let fixdefs = List.map reduce_fix fixdefs in *)
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index e5547d9b75..b4b3aead91 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -97,25 +97,27 @@ open Pputils
let sep = fun _ -> spc()
let sep_v2 = fun _ -> str"," ++ spc()
+ let pr_notation_entry = function
+ | InConstrEntry -> keyword "constr"
+ | InCustomEntry s -> keyword "custom" ++ spc () ++ str s
+
let pr_at_level = function
| NumLevel n -> keyword "at" ++ spc () ++ keyword "level" ++ spc () ++ int n
| NextLevel -> keyword "at" ++ spc () ++ keyword "next" ++ spc () ++ keyword "level"
let pr_constr_as_binder_kind = let open Notation_term in function
- | AsIdent -> keyword "as ident"
- | AsIdentOrPattern -> keyword "as pattern"
- | AsStrictPattern -> keyword "as strict pattern"
+ | AsIdent -> spc () ++ keyword "as ident"
+ | AsIdentOrPattern -> spc () ++ keyword "as pattern"
+ | AsStrictPattern -> spc () ++ keyword "as strict pattern"
let pr_strict b = if b then str "strict " else mt ()
let pr_set_entry_type pr = function
- | ETName -> str"ident"
- | ETReference -> str"global"
+ | ETIdent -> str"ident"
+ | ETGlobal -> str"global"
| ETPattern (b,None) -> pr_strict b ++ str"pattern"
| ETPattern (b,Some n) -> pr_strict b ++ str"pattern" ++ spc () ++ pr_at_level (NumLevel n)
- | ETConstr lev -> str"constr" ++ pr lev
- | ETOther (_,e) -> str e
- | ETConstrAsBinder (bk,lev) -> pr lev ++ spc () ++ pr_constr_as_binder_kind bk
+ | ETConstr (s,bko,lev) -> pr_notation_entry s ++ pr lev ++ pr_opt pr_constr_as_binder_kind bko
| ETBigint -> str "bigint"
| ETBinder true -> str "binder"
| ETBinder false -> str "closed binder"
@@ -176,11 +178,11 @@ open Pputils
| [] -> mt()
| _ as z -> str":" ++ spc() ++ prlist_with_sep sep str z
- let pr_reference_or_constr pr_c = function
+ let pr_reference_or_constr pr_c = let open Hints in function
| HintsReference r -> pr_qualid r
| HintsConstr c -> pr_c c
- let pr_hint_mode = function
+ let pr_hint_mode = let open Hints in function
| ModeInput -> str"+"
| ModeNoHeadEvar -> str"!"
| ModeOutput -> str"-"
@@ -192,6 +194,7 @@ open Pputils
let pr_hints db h pr_c pr_pat =
let opth = pr_opt_hintbases db in
let pph =
+ let open Hints in
match h with
| HintsResolve l ->
keyword "Resolve " ++ prlist_with_sep sep
@@ -378,12 +381,11 @@ open Pputils
let pr_thm_token k = keyword (Kindops.string_of_theorem_kind k)
let pr_syntax_modifier = function
- | SetItemLevel (l,n) ->
- prlist_with_sep sep_v2 str l ++ spc () ++ pr_at_level n
- | SetItemLevelAsBinder (l,bk,n) ->
- prlist_with_sep sep_v2 str l ++
- spc() ++ pr_at_level_opt n ++ spc() ++ pr_constr_as_binder_kind bk
+ | SetItemLevel (l,bko,n) ->
+ prlist_with_sep sep_v2 str l ++ spc () ++ pr_at_level_opt n ++
+ pr_opt pr_constr_as_binder_kind bko
| SetLevel n -> pr_at_level (NumLevel n)
+ | SetCustomEntry (s,n) -> keyword "in" ++ spc() ++ keyword "custom" ++ spc() ++ str s ++ (match n with None -> mt () | Some n -> pr_at_level (NumLevel n))
| SetAssoc LeftA -> keyword "left associativity"
| SetAssoc RightA -> keyword "right associativity"
| SetAssoc NonA -> keyword "no associativity"
@@ -634,6 +636,10 @@ open Pputils
keyword (if opening then "Open " else "Close ") ++
keyword "Scope" ++ spc() ++ str sc
)
+ | VernacDeclareScope sc ->
+ return (
+ keyword "Declare Scope" ++ spc () ++ str sc
+ )
| VernacDelimiters (sc,Some key) ->
return (
keyword "Delimit Scope" ++ spc () ++ str sc ++
@@ -674,6 +680,10 @@ open Pputils
return (
keyword "Format Notation " ++ qs s ++ spc () ++ qs k ++ spc() ++ qs v
)
+ | VernacDeclareCustomEntry s ->
+ return (
+ keyword "Declare Custom Entry " ++ str s
+ )
(* Gallina *)
| VernacDefinition ((discharge,kind),id,b) -> (* A verifier... *)
@@ -1152,7 +1162,11 @@ open Pputils
| VernacRegister (id, RegisterInline) ->
return (
hov 2
- (keyword "Register Inline" ++ spc() ++ pr_lident id)
+ (keyword "Register Inline" ++ spc() ++ pr_qualid id)
+ )
+ | VernacRegister (id, RegisterRetroknowledge n) ->
+ return (
+ hov 2 (keyword "Register" ++ spc () ++ pr_qualid id ++ spc () ++ keyword "as" ++ pr_qualid n)
)
| VernacComments l ->
return (
diff --git a/vernac/record.ml b/vernac/record.ml
index 7a8ce7d25a..724b6e62fe 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -324,12 +324,16 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers u
| Name fid -> try
let kn, term =
if is_local_assum decl && primitive then
- (** Already defined in the kernel silently *)
- let gr = Nametab.locate (Libnames.qualid_of_ident fid) in
- let kn = destConstRef gr in
+ let p = Projection.Repr.make indsp
+ ~proj_npars:mib.mind_nparams
+ ~proj_arg:i
+ (Label.of_id fid)
+ in
+ (** Already defined by declare_mind silently *)
+ let kn = Projection.Repr.constant p in
Declare.definition_message fid;
- UnivNames.register_universe_binders gr ubinders;
- kn, mkProj (Projection.make kn false,mkRel 1)
+ UnivNames.register_universe_binders (ConstRef kn) ubinders;
+ kn, mkProj (Projection.make p false,mkRel 1)
else
let ccl = subst_projection fid subst ti in
let body = match decl with
@@ -389,14 +393,14 @@ open Typeclasses
let declare_structure finite ubinders univs paramimpls params template ?(kind=StructureComponent) ?name record_data =
let nparams = List.length params in
- let template, ctx =
+ let poly, ctx =
match univs with
| Monomorphic_ind_entry ctx ->
- template, Monomorphic_const_entry Univ.ContextSet.empty
+ false, Monomorphic_const_entry Univ.ContextSet.empty
| Polymorphic_ind_entry ctx ->
- false, Polymorphic_const_entry ctx
+ true, Polymorphic_const_entry ctx
| Cumulative_ind_entry cumi ->
- false, Polymorphic_const_entry (Univ.CumulativityInfo.univ_context cumi)
+ true, Polymorphic_const_entry (Univ.CumulativityInfo.univ_context cumi)
in
let binder_name =
match name with
@@ -413,6 +417,18 @@ let declare_structure finite ubinders univs paramimpls params template ?(kind=St
let args = Context.Rel.to_extended_list mkRel nfields params in
let ind = applist (mkRel (ntypes - i + nparams + nfields), args) in
let type_constructor = it_mkProd_or_LetIn ind fields in
+ let template =
+ match template with
+ | Some template, _ ->
+ (* templateness explicitly requested *)
+ if poly && template then user_err Pp.(strbrk "template and polymorphism not compatible");
+ template
+ | None, template ->
+ (* auto detect template *)
+ ComInductive.should_auto_template () && template && not poly &&
+ let _, s = Reduction.dest_arity (Global.env()) arity in
+ not (Sorts.is_small s)
+ in
{ mind_entry_typename = id;
mind_entry_arity = arity;
mind_entry_template = template;
@@ -437,7 +453,6 @@ let declare_structure finite ubinders univs paramimpls params template ?(kind=St
let cstr = (rsp, 1) in
let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name.(i) coers ubinders fieldimpls fields in
let build = ConstructRef cstr in
- let poly = match ctx with | Polymorphic_const_entry _ -> true | Monomorphic_const_entry _ -> false in
let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in
let () = Recordops.declare_structure(rsp,cstr,List.rev kinds,List.rev sp_projs) in
rsp
@@ -472,10 +487,11 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari
let cst = Declare.declare_constant id
(DefinitionEntry class_entry, IsDefinition Definition)
in
- let cstu = (cst, match univs with
- | Polymorphic_const_entry univs -> Univ.UContext.instance univs
- | Monomorphic_const_entry _ -> Univ.Instance.empty)
+ let inst, univs = match univs with
+ | Polymorphic_const_entry uctx -> Univ.UContext.instance uctx, univs
+ | Monomorphic_const_entry _ -> Univ.Instance.empty, Monomorphic_const_entry Univ.ContextSet.empty
in
+ let cstu = (cst, inst) in
let inst_type = appvectc (mkConstU cstu)
(Termops.rel_vect 0 (List.length params)) in
let proj_type =
@@ -612,7 +628,7 @@ let check_unique_names records =
| Vernacexpr.DefExpr ({CAst.v=Name id},_,_) -> id::acc
| _ -> acc in
let allnames =
- List.fold_left (fun acc (_, id, _, _, cfs, _, _) ->
+ List.fold_left (fun acc (_, id, _, cfs, _, _) ->
id.CAst.v :: (List.fold_left extract_name acc cfs)) [] records
in
match List.duplicates Id.equal allnames with
@@ -621,19 +637,19 @@ let check_unique_names records =
let check_priorities kind records =
let isnot_class = match kind with Class false -> false | _ -> true in
- let has_priority (_, _, _, _, cfs, _, _) =
+ let has_priority (_, _, _, cfs, _, _) =
List.exists (fun ((_, pri), _) -> not (Option.is_empty pri)) cfs
in
if isnot_class && List.exists has_priority records then
user_err Pp.(str "Priorities only allowed for type class substructures")
let extract_record_data records =
- let map (is_coe, id, _, _, cfs, idbuild, s) =
+ let map (is_coe, id, _, cfs, idbuild, s) =
let fs = List.map (fun (((_, f), _), _) -> f) cfs in
id.CAst.v, s, List.map snd cfs, fs
in
let data = List.map map records in
- let pss = List.map (fun (_, _, _, ps, _, _, _) -> ps) records in
+ let pss = List.map (fun (_, _, ps, _, _, _) -> ps) records in
let ps = match pss with
| [] -> CErrors.anomaly (str "Empty record block")
| ps :: rem ->
@@ -645,29 +661,28 @@ let extract_record_data records =
in
ps
in
- (** FIXME: Same issue as #7754 *)
- let _, _, pl, _, _, _, _ = List.hd records in
- pl, ps, data
+ ps, data
(* [fs] corresponds to fields and [ps] to parameters; [coers] is a
list telling if the corresponding fields must me declared as coercions
or subinstances. *)
-let definition_structure kind cum poly finite records =
+let definition_structure udecl kind ~template cum poly finite records =
let () = check_unique_names records in
let () = check_priorities kind records in
- let pl, ps, data = extract_record_data records in
- let pl, univs, template, params, implpars, data =
+ let ps, data = extract_record_data records in
+ let ubinders, univs, auto_template, params, implpars, data =
States.with_state_protection (fun () ->
- typecheck_params_and_fields finite (kind = Class true) poly pl ps data) () in
+ typecheck_params_and_fields finite (kind = Class true) poly udecl ps data) () in
+ let template = template, auto_template in
match kind with
| Class def ->
- let (_, id, _, _, cfs, idbuild, _), (arity, implfs, fields) = match records, data with
+ let (_, id, _, cfs, idbuild, _), (arity, implfs, fields) = match records, data with
| [r], [d] -> r, d
| _, _ -> CErrors.user_err (str "Mutual definitional classes are not handled")
in
let priorities = List.map (fun ((_, id), _) -> {hint_priority = id; hint_pattern = None}) cfs in
let coers = List.map (fun (((coe, _), _), _) -> coe) cfs in
- declare_class finite def cum pl univs id.CAst.v idbuild
+ declare_class finite def cum ubinders univs id.CAst.v idbuild
implpars params arity template implfs fields coers priorities
| _ ->
let map impls = implpars @ Impargs.lift_implicits (succ (List.length params)) impls in
@@ -682,11 +697,11 @@ let definition_structure kind cum poly finite records =
| Monomorphic_const_entry univs ->
Monomorphic_ind_entry univs
in
- let map (arity, implfs, fields) (is_coe, id, _, _, cfs, idbuild, _) =
+ let map (arity, implfs, fields) (is_coe, id, _, cfs, idbuild, _) =
let coers = List.map (fun (((coe, _), _), _) -> coe) cfs in
let coe = List.map (fun coe -> not (Option.is_empty coe)) coers in
id.CAst.v, idbuild, arity, implfs, fields, is_coe, coe
in
let data = List.map2 map data records in
- let inds = declare_structure finite pl univs implpars params template data in
+ let inds = declare_structure finite ubinders univs implpars params template data in
List.map (fun ind -> IndRef ind) inds
diff --git a/vernac/record.mli b/vernac/record.mli
index 567f2b3138..953d5ec3b6 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -26,11 +26,11 @@ val declare_projections :
(Name.t * bool) list * Constant.t option list
val definition_structure :
- inductive_kind -> Decl_kinds.cumulative_inductive_flag -> Decl_kinds.polymorphic ->
+ universe_decl_expr option -> inductive_kind -> template:bool option ->
+ Decl_kinds.cumulative_inductive_flag -> Decl_kinds.polymorphic ->
Declarations.recursivity_kind ->
(coercion_flag *
Names.lident *
- universe_decl_expr option *
local_binder_expr list *
(local_decl_expr with_instance with_priority with_notation) list *
Id.t * constr_expr option) list ->
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
index 609dac69aa..f842ca5ead 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -181,6 +181,10 @@ let default_tag_map () = let open Terminal in [
; "tactic.keyword" , make ~bold:true ()
; "tactic.primitive" , make ~fg_color:`LIGHT_GREEN ()
; "tactic.string" , make ~fg_color:`LIGHT_RED ()
+ ; "diff.added" , make ~bg_color:(`RGB(0,141,0)) ~underline:true ()
+ ; "diff.removed" , make ~bg_color:(`RGB(170,0,0)) ~underline:true ()
+ ; "diff.added.bg" , make ~bg_color:(`RGB(0,91,0)) ()
+ ; "diff.removed.bg" , make ~bg_color:(`RGB(91,0,0)) ()
]
let tag_map = ref CString.Map.empty
@@ -198,72 +202,103 @@ let parse_color_config file =
let dump_tags () = CString.Map.bindings !tag_map
+let empty = Terminal.make ()
+let default_style = Terminal.reset_style
+
+let get_style tag =
+ try CString.Map.find tag !tag_map
+ with Not_found -> empty;;
+
+let get_open_seq tags =
+ let style = List.fold_left (fun a b -> Terminal.merge a (get_style b)) default_style tags in
+ Terminal.eval (Terminal.diff default_style style);;
+
+let get_close_seq tags =
+ let style = List.fold_left (fun a b -> Terminal.merge a (get_style b)) default_style tags in
+ Terminal.eval (Terminal.diff style default_style);;
+
+let diff_tag_stack = ref [] (* global, just like std_ft *)
+
(** Not thread-safe. We should put a lock somewhere if we print from
different threads. Do we? *)
let make_style_stack () =
(** Default tag is to reset everything *)
- let empty = Terminal.make () in
- let default_tag = Terminal.({
- fg_color = Some `DEFAULT;
- bg_color = Some `DEFAULT;
- bold = Some false;
- italic = Some false;
- underline = Some false;
- negative = Some false;
- prefix = None;
- suffix = None;
- })
- in
let style_stack = ref [] in
let peek () = match !style_stack with
- | [] -> default_tag (** Anomalous case, but for robustness *)
+ | [] -> default_style (** Anomalous case, but for robustness *)
| st :: _ -> st
in
- let push tag =
- let style =
- try CString.Map.find tag !tag_map
- with | Not_found -> empty
- in
- (** Use the merging of the latest tag and the one being currently pushed.
- This may be useful if for instance the latest tag changes the background and
- the current one the foreground, so that the two effects are additioned. *)
+ let open_tag tag =
+ let (tpfx, ttag) = split_tag tag in
+ if tpfx = end_pfx then "" else
+ let style = get_style ttag in
+ (** Merge the current settings and the style being pushed. This allows
+ restoring the previous settings correctly in a pop when both set the same
+ attribute. Example: current settings have red FG, the pushed style has
+ green FG. When popping the style, we should set red FG, not default FG. *)
let style = Terminal.merge (peek ()) style in
+ let diff = Terminal.diff (peek ()) style in
style_stack := style :: !style_stack;
- Terminal.eval style
+ if tpfx = start_pfx then diff_tag_stack := ttag :: !diff_tag_stack;
+ Terminal.eval diff
in
- let pop _ = match !style_stack with
- | [] -> (** Something went wrong, we fallback *)
- Terminal.eval default_tag
- | _ :: rem -> style_stack := rem;
- Terminal.eval (peek ())
+ let close_tag tag =
+ let (tpfx, _) = split_tag tag in
+ if tpfx = start_pfx then "" else begin
+ if tpfx = end_pfx then diff_tag_stack := (try List.tl !diff_tag_stack with tl -> []);
+ match !style_stack with
+ | [] -> (** Something went wrong, we fallback *)
+ Terminal.eval default_style
+ | cur :: rem -> style_stack := rem;
+ if cur = (peek ()) then "" else
+ if rem = [] then Terminal.reset else
+ Terminal.eval (Terminal.diff cur (peek ()))
+ end
in
let clear () = style_stack := [] in
- push, pop, clear
+ open_tag, close_tag, clear
let make_printing_functions () =
- let empty = Terminal.make () in
let print_prefix ft tag =
- let style =
- try CString.Map.find tag !tag_map
- with | Not_found -> empty
- in
- match style.Terminal.prefix with Some s -> Format.pp_print_string ft s | None -> ()
- in
+ let (tpfx, ttag) = split_tag tag in
+ if tpfx <> end_pfx then
+ let style = get_style ttag in
+ match style.Terminal.prefix with Some s -> Format.pp_print_string ft s | None -> () in
+
let print_suffix ft tag =
- let style =
- try CString.Map.find tag !tag_map
- with | Not_found -> empty
- in
- match style.Terminal.suffix with Some s -> Format.pp_print_string ft s | None -> ()
- in
+ let (tpfx, ttag) = split_tag tag in
+ if tpfx <> start_pfx then
+ let style = get_style ttag in
+ match style.Terminal.suffix with Some s -> Format.pp_print_string ft s | None -> () in
+
print_prefix, print_suffix
+let init_output_fns () =
+ let reopen_highlight = ref "" in
+ let open Format in
+ let fns = Format.pp_get_formatter_out_functions !std_ft () in
+ let newline () =
+ if !diff_tag_stack <> [] then begin
+ let close = get_close_seq !diff_tag_stack in
+ fns.out_string close 0 (String.length close);
+ reopen_highlight := get_open_seq (List.rev !diff_tag_stack);
+ end;
+ fns.out_string "\n" 0 1 in
+ let string s off n =
+ if !reopen_highlight <> "" && String.trim (String.sub s off n) <> "" then begin
+ fns.out_string !reopen_highlight 0 (String.length !reopen_highlight);
+ reopen_highlight := ""
+ end;
+ fns.out_string s off n in
+ let new_fns = { fns with out_string = string; out_newline = newline } in
+ Format.pp_set_formatter_out_functions !std_ft new_fns;;
+
let init_terminal_output ~color =
- let push_tag, pop_tag, clear_tag = make_style_stack () in
+ let open_tag, close_tag, clear_tag = make_style_stack () in
let print_prefix, print_suffix = make_printing_functions () in
let tag_handler ft = {
- Format.mark_open_tag = push_tag;
- Format.mark_close_tag = pop_tag;
+ Format.mark_open_tag = open_tag;
+ Format.mark_close_tag = close_tag;
Format.print_open_tag = print_prefix ft;
Format.print_close_tag = print_suffix ft;
} in
@@ -271,6 +306,7 @@ let init_terminal_output ~color =
(* Use 0-length markers *)
begin
std_logger_cleanup := clear_tag;
+ init_output_fns ();
Format.pp_set_mark_tags !std_ft true;
Format.pp_set_mark_tags !err_ft true
end
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index b6bc76a2ed..015d5fabef 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -403,17 +403,24 @@ let dump_global r =
(**********)
(* Syntax *)
-let vernac_syntax_extension atts infix l =
+let vernac_syntax_extension ~atts infix l =
let local = enforce_module_locality atts.locality in
if infix then Metasyntax.check_infix_modifiers (snd l);
Metasyntax.add_syntax_extension local l
-let vernac_delimiters sc = function
- | Some lr -> Metasyntax.add_delimiters sc lr
- | None -> Metasyntax.remove_delimiters sc
+let vernac_declare_scope ~atts sc =
+ let local = enforce_module_locality atts.locality in
+ Metasyntax.declare_scope local sc
-let vernac_bind_scope sc cll =
- Metasyntax.add_class_scope sc (List.map scope_class_of_qualid cll)
+let vernac_delimiters ~atts sc action =
+ let local = enforce_module_locality atts.locality in
+ match action with
+ | Some lr -> Metasyntax.add_delimiters local sc lr
+ | None -> Metasyntax.remove_delimiters local sc
+
+let vernac_bind_scope ~atts sc cll =
+ let local = enforce_module_locality atts.locality in
+ Metasyntax.add_class_scope local sc (List.map scope_class_of_qualid cll)
let vernac_open_close_scope ~atts (b,s) =
let local = enforce_section_locality atts.locality in
@@ -431,6 +438,10 @@ let vernac_notation ~atts =
let local = enforce_module_locality atts.locality in
Metasyntax.add_notation local (Global.env())
+let vernac_custom_entry ~atts s =
+ let local = enforce_module_locality atts.locality in
+ Metasyntax.declare_custom_entry local s
+
(***********)
(* Gallina *)
@@ -544,9 +555,9 @@ let should_treat_as_uniform () =
then ComInductive.UniformParameters
else ComInductive.NonUniformParameters
-let vernac_record cum k poly finite records =
+let vernac_record ~template udecl cum k poly finite records =
let is_cumulative = should_treat_as_cumulative cum poly in
- let map ((coe, (id, pl)), binders, sort, nameopt, cfs) =
+ let map ((coe, id), binders, sort, nameopt, cfs) =
let const = match nameopt with
| None -> add_prefix "Build_" id.v
| Some lid ->
@@ -563,10 +574,22 @@ let vernac_record cum k poly finite records =
in
List.iter iter cfs
in
- coe, id, pl, binders, cfs, const, sort
+ coe, id, binders, cfs, const, sort
in
let records = List.map map records in
- ignore(Record.definition_structure k is_cumulative poly finite records)
+ ignore(Record.definition_structure ~template udecl k is_cumulative poly finite records)
+
+let extract_inductive_udecl (indl:(inductive_expr * decl_notation list) list) =
+ match indl with
+ | [] -> assert false
+ | (((coe,(id,udecl)),b,c,k,d),e) :: rest ->
+ let rest = List.map (fun (((coe,(id,udecl)),b,c,k,d),e) ->
+ if Option.has_some udecl
+ then user_err ~hdr:"inductive udecl" Pp.(strbrk "Universe binders must be on the first inductive of the block.")
+ else (((coe,id),b,c,k,d),e))
+ rest
+ in
+ udecl, (((coe,id),b,c,k,d),e) :: rest
(** When [poly] is true the type is declared polymorphic. When [lo] is true,
then the type is declared private (as per the [Private] keyword). [finite]
@@ -574,8 +597,9 @@ let vernac_record cum k poly finite records =
neither. *)
let vernac_inductive ~atts cum lo finite indl =
let open Pp in
+ let udecl, indl = extract_inductive_udecl indl in
if Dumpglob.dump () then
- List.iter (fun (((coe,(lid,_)), _, _, _, cstrs), _) ->
+ List.iter (fun (((coe,lid), _, _, _, cstrs), _) ->
match cstrs with
| Constructors cstrs ->
Dumpglob.dump_definition lid false "ind";
@@ -583,6 +607,7 @@ let vernac_inductive ~atts cum lo finite indl =
Dumpglob.dump_definition lid false "constr") cstrs
| _ -> () (* dumping is done by vernac_record (called below) *) )
indl;
+
let is_record = function
| ((_ , _ , _ , _, RecordDecl _), _) -> true
| _ -> false
@@ -595,13 +620,14 @@ let vernac_inductive ~atts cum lo finite indl =
| [ ( id , bl , c , Class _, Constructors [l]), [] ] -> Some (id, bl, c, l)
| _ -> None
in
+ let template = atts.template in
if Option.has_some is_defclass then
(** Definitional class case *)
let (id, bl, c, l) = Option.get is_defclass in
let (coe, (lid, ce)) = l in
let coe' = if coe then Some true else None in
let f = (((coe', AssumExpr ((make ?loc:lid.loc @@ Name lid.v), ce)), None), []) in
- vernac_record cum (Class true) atts.polymorphic finite [id, bl, c, None, [f]]
+ vernac_record ~template udecl cum (Class true) atts.polymorphic finite [id, bl, c, None, [f]]
else if List.for_all is_record indl then
(** Mutual record case *)
let check_kind ((_, _, _, kind, _), _) = match kind with
@@ -624,7 +650,7 @@ let vernac_inductive ~atts cum lo finite indl =
let ((_, _, _, kind, _), _) = List.hd indl in
let kind = match kind with Class _ -> Class false | _ -> kind in
let recordl = List.map unpack indl in
- vernac_record cum kind atts.polymorphic finite recordl
+ vernac_record ~template udecl cum kind atts.polymorphic finite recordl
else if List.for_all is_constructor indl then
(** Mutual inductive case *)
let check_kind ((_, _, _, kind, _), _) = match kind with
@@ -650,7 +676,7 @@ let vernac_inductive ~atts cum lo finite indl =
let indl = List.map unpack indl in
let is_cumulative = should_treat_as_cumulative cum atts.polymorphic in
let uniform = should_treat_as_uniform () in
- ComInductive.do_mutual_inductive indl is_cumulative atts.polymorphic lo ~uniform finite
+ ComInductive.do_mutual_inductive ~template udecl indl is_cumulative atts.polymorphic lo ~uniform finite
else
user_err (str "Mixed record-inductive definitions are not allowed")
(*
@@ -1501,8 +1527,8 @@ let _ =
{ optdepr = false;
optname = "kernel term sharing";
optkey = ["Kernel"; "Term"; "Sharing"];
- optread = (fun () -> !CClosure.share);
- optwrite = (fun b -> CClosure.share := b) }
+ optread = (fun () -> (Global.typing_flags ()).Declarations.share_reduction);
+ optwrite = (fun b -> Global.set_reduction_sharing b) }
let _ =
declare_bool_option
@@ -1688,36 +1714,37 @@ let query_command_selector ?loc = function
let vernac_check_may_eval ~atts redexp glopt rc =
let glopt = query_command_selector ?loc:atts.loc glopt in
let (sigma, env) = get_current_context_of_args glopt in
- let sigma', c = interp_open_constr env sigma rc in
- let sigma' = Evarconv.solve_unif_constraints_with_heuristics env sigma' in
- Evarconv.check_problems_are_solved env sigma';
- let sigma' = Evd.minimize_universes sigma' in
- let uctx = Evd.universe_context_set sigma' in
- let env = Environ.push_context_set uctx (Evarutil.nf_env_evar sigma' env) in
+ let sigma, c = interp_open_constr env sigma rc in
+ let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in
+ Evarconv.check_problems_are_solved env sigma;
+ let sigma = Evd.minimize_universes sigma in
+ let uctx = Evd.universe_context_set sigma in
+ let env = Environ.push_context_set uctx (Evarutil.nf_env_evar sigma env) in
let j =
- if Evarutil.has_undefined_evars sigma' c then
- Evarutil.j_nf_evar sigma' (Retyping.get_judgment_of env sigma' c)
+ if Evarutil.has_undefined_evars sigma c then
+ Evarutil.j_nf_evar sigma (Retyping.get_judgment_of env sigma c)
else
- let c = EConstr.to_constr sigma' c in
+ let c = EConstr.to_constr sigma c in
(* OK to call kernel which does not support evars *)
Termops.on_judgment EConstr.of_constr (Arguments_renaming.rename_typing env c)
in
- match redexp with
+ let pp = match redexp with
| None ->
- let evars_of_term c = Evarutil.undefined_evars_of_term sigma' c in
+ let evars_of_term c = Evarutil.undefined_evars_of_term sigma c in
let l = Evar.Set.union (evars_of_term j.Environ.uj_val) (evars_of_term j.Environ.uj_type) in
- let j = { j with Environ.uj_type = Reductionops.nf_betaiota env sigma' j.Environ.uj_type } in
- print_judgment env sigma' j ++
- pr_ne_evar_set (fnl () ++ str "where" ++ fnl ()) (mt ()) sigma' l ++
- Printer.pr_universe_ctx_set sigma uctx
+ let j = { j with Environ.uj_type = Reductionops.nf_betaiota env sigma j.Environ.uj_type } in
+ print_judgment env sigma j ++
+ pr_ne_evar_set (fnl () ++ str "where" ++ fnl ()) (mt ()) sigma l
| Some r ->
- let (sigma',r_interp) = Hook.get f_interp_redexp env sigma' r in
+ let (sigma,r_interp) = Hook.get f_interp_redexp env sigma r in
let redfun env evm c =
let (redfun, _) = reduction_of_red_expr env r_interp in
let (_, c) = redfun env evm c in
c
in
- print_eval redfun env sigma' rc j
+ print_eval redfun env sigma rc j
+ in
+ pp ++ Printer.pr_universe_ctx_set sigma uctx
let vernac_declare_reduction ~atts s r =
let local = make_locality atts.locality in
@@ -1797,13 +1824,13 @@ let vernac_print ~atts env sigma =
| PrintName (qid,udecl) ->
dump_global qid;
print_name env sigma qid udecl
- | PrintGraph -> Prettyp.print_graph env sigma
+ | PrintGraph -> Prettyp.print_graph ()
| PrintClasses -> Prettyp.print_classes()
| PrintTypeClasses -> Prettyp.print_typeclasses()
| PrintInstances c -> Prettyp.print_instances (smart_global c)
- | PrintCoercions -> Prettyp.print_coercions env sigma
+ | PrintCoercions -> Prettyp.print_coercions ()
| PrintCoercionPaths (cls,clt) ->
- Prettyp.print_path_between env sigma (cl_of_qualid cls) (cl_of_qualid clt)
+ Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt)
| PrintCanonicalConversions -> Prettyp.print_canonical_projections env sigma
| PrintUniverses (b, dst) ->
let univ = Global.universes () in
@@ -1937,14 +1964,23 @@ let vernac_locate = function
| LocateOther (s, qid) -> print_located_other s qid
| LocateFile f -> locate_file f
-let vernac_register id r =
+let vernac_register qid r =
+ let gr = Smartlocate.global_with_alias qid in
if Proof_global.there_are_pending_proofs () then
user_err Pp.(str "Cannot register a primitive while in proof editing mode.");
- let kn = Constrintern.global_reference id.v in
- if not (isConstRef kn) then
- user_err Pp.(str "Register inline: a constant is expected");
match r with
- | RegisterInline -> Global.register_inline (destConstRef kn)
+ | RegisterInline ->
+ if not (isConstRef gr) then
+ user_err Pp.(str "Register inline: a constant is expected");
+ Global.register_inline (destConstRef gr)
+ | RegisterRetroknowledge n ->
+ let path, id = Libnames.repr_qualid n in
+ if DirPath.equal path Retroknowledge.int31_path
+ then
+ let f = Retroknowledge.(KInt31 (int31_field_of_string (Id.to_string id))) in
+ Global.register f gr
+ else
+ user_err Pp.(str "Register in unknown namespace: " ++ str (DirPath.to_string path))
(********************)
(* Proof management *)
@@ -1983,8 +2019,9 @@ let vernac_subproof gln =
match gln with
| None -> Proof.focus subproof_cond () 1 p
| Some (Goal_select.SelectNth n) -> Proof.focus subproof_cond () n p
+ | Some (Goal_select.SelectId id) -> Proof.focus_id subproof_cond () id p
| _ -> user_err ~hdr:"bracket_selector"
- (str "Brackets only support the single numbered goal selector."))
+ (str "Brackets do not support multi-goal selectors."))
let vernac_end_subproof () =
Proof_global.simple_with_current_proof (fun _ p ->
@@ -2087,15 +2124,18 @@ let interp ?proof ~atts ~st c =
(* Syntax *)
| VernacSyntaxExtension (infix, sl) ->
- vernac_syntax_extension atts infix sl
- | VernacDelimiters (sc,lr) -> vernac_delimiters sc lr
- | VernacBindScope (sc,rl) -> vernac_bind_scope sc rl
+ vernac_syntax_extension ~atts infix sl
+ | VernacDeclareScope sc -> vernac_declare_scope ~atts sc
+ | VernacDelimiters (sc,lr) -> vernac_delimiters ~atts sc lr
+ | VernacBindScope (sc,rl) -> vernac_bind_scope ~atts sc rl
| VernacOpenCloseScope (b, s) -> vernac_open_close_scope ~atts (b,s)
| VernacInfix (mv,qid,sc) -> vernac_infix ~atts mv qid sc
| VernacNotation (c,infpl,sc) ->
vernac_notation ~atts c infpl sc
| VernacNotationAddFormat(n,k,v) ->
Metasyntax.add_notation_extra_printing_rule n k v
+ | VernacDeclareCustomEntry s ->
+ vernac_custom_entry ~atts s
(* Gallina *)
| VernacDefinition ((discharge,kind),lid,d) ->
@@ -2224,6 +2264,8 @@ let check_vernac_supports_locality c l =
| Some _, (
VernacOpenCloseScope _
| VernacSyntaxExtension _ | VernacInfix _ | VernacNotation _
+ | VernacDeclareScope _ | VernacDelimiters _ | VernacBindScope _
+ | VernacDeclareCustomEntry _
| VernacDefinition _ | VernacFixpoint _ | VernacCoFixpoint _
| VernacAssumption _ | VernacStartTheoremProof _
| VernacCoercion _ | VernacIdentityCoercion _
@@ -2340,6 +2382,14 @@ let attributes_of_flags f atts =
(Some false, atts)
| ("polymorphic" | "monomorphic") ->
user_err Pp.(str "Polymorphism specified twice")
+ | "template" when atts.template = None ->
+ assert_empty k v;
+ polymorphism, { atts with template = Some true }
+ | "notemplate" when atts.template = None ->
+ assert_empty k v;
+ polymorphism, { atts with template = Some false }
+ | "template" | "notemplate" ->
+ user_err Pp.(str "Templateness specified twice")
| "local" when Option.is_empty atts.locality ->
assert_empty k v;
(polymorphism, { atts with locality = Some true })
@@ -2436,3 +2486,121 @@ let interp ?verbosely ?proof ~st cmd =
let exn = CErrors.push exn in
Vernacstate.invalidate_cache ();
iraise exn
+
+(** VERNAC EXTEND registering *)
+
+open Genarg
+open Extend
+
+type classifier = Genarg.raw_generic_argument list -> vernac_classification
+
+type (_, _) ty_sig =
+| TyNil : (atts:atts -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig
+| TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig
+| TyNonTerminal :
+ string option * ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig -> ('a -> 'r, 'a -> 's) ty_sig
+
+type ty_ml = TyML : bool * ('r, 's) ty_sig * 'r * 's option -> ty_ml
+
+let type_error () = CErrors.anomaly (Pp.str "Ill-typed VERNAC EXTEND")
+
+let rec untype_classifier : type r s. (r, s) ty_sig -> s -> classifier = function
+| TyNil -> fun f args ->
+ begin match args with
+ | [] -> f
+ | _ :: _ -> type_error ()
+ end
+| TyTerminal (_, ty) -> fun f args -> untype_classifier ty f args
+| TyNonTerminal (_, tu, ty) -> fun f args ->
+ begin match args with
+ | [] -> type_error ()
+ | Genarg.GenArg (Rawwit tag, v) :: args ->
+ match Genarg.genarg_type_eq tag (Egramml.proj_symbol tu) with
+ | None -> type_error ()
+ | Some Refl -> untype_classifier ty (f v) args
+ end
+
+(** Stupid GADTs forces us to duplicate the definition just for typing *)
+let rec untype_command : type r s. (r, s) ty_sig -> r -> plugin_args vernac_command = function
+| TyNil -> fun f args ->
+ begin match args with
+ | [] -> f
+ | _ :: _ -> type_error ()
+ end
+| TyTerminal (_, ty) -> fun f args -> untype_command ty f args
+| TyNonTerminal (_, tu, ty) -> fun f args ->
+ begin match args with
+ | [] -> type_error ()
+ | Genarg.GenArg (Rawwit tag, v) :: args ->
+ match Genarg.genarg_type_eq tag (Egramml.proj_symbol tu) with
+ | None -> type_error ()
+ | Some Refl -> untype_command ty (f v) args
+ end
+
+let rec untype_user_symbol : type s a b c. (a, b, c) Extend.ty_user_symbol -> (s, a) Extend.symbol = function
+| TUlist1 l -> Alist1 (untype_user_symbol l)
+| TUlist1sep (l, s) -> Alist1sep (untype_user_symbol l, Atoken (CLexer.terminal s))
+| TUlist0 l -> Alist0 (untype_user_symbol l)
+| TUlist0sep (l, s) -> Alist0sep (untype_user_symbol l, Atoken (CLexer.terminal s))
+| TUopt o -> Aopt (untype_user_symbol o)
+| TUentry a -> Aentry (Pcoq.genarg_grammar (ExtraArg a))
+| TUentryl (a, i) -> Aentryl (Pcoq.genarg_grammar (ExtraArg a), string_of_int i)
+
+let rec untype_grammar : type r s. (r, s) ty_sig -> vernac_expr Egramml.grammar_prod_item list = function
+| TyNil -> []
+| TyTerminal (tok, ty) -> Egramml.GramTerminal tok :: untype_grammar ty
+| TyNonTerminal (id, tu, ty) ->
+ let t = Option.map (fun _ -> rawwit (Egramml.proj_symbol tu)) id in
+ let symb = untype_user_symbol tu in
+ Egramml.GramNonTerminal (Loc.tag (t, symb)) :: untype_grammar ty
+
+let _ = untype_classifier, untype_command, untype_grammar, untype_user_symbol
+
+let classifiers : classifier array String.Map.t ref = ref String.Map.empty
+
+let get_vernac_classifier (name, i) args =
+ (String.Map.find name !classifiers).(i) args
+
+let declare_vernac_classifier name f =
+ classifiers := String.Map.add name f !classifiers
+
+let vernac_extend ~command ?classifier ?entry ext =
+ let get_classifier (TyML (_, ty, _, cl)) = match cl with
+ | Some cl -> untype_classifier ty cl
+ | None ->
+ match classifier with
+ | Some cl -> fun _ -> cl command
+ | None ->
+ let e = match entry with
+ | None -> "COMMAND"
+ | Some e -> Pcoq.Gram.Entry.name e
+ in
+ let msg = Printf.sprintf "\
+ Vernac entry \"%s\" misses a classifier. \
+ A classifier is a function that returns an expression \
+ of type vernac_classification (see Vernacexpr). You can: \n\
+ - Use '... EXTEND %s CLASSIFIED AS QUERY ...' if the \
+ new vernacular command does not alter the system state;\n\
+ - Use '... EXTEND %s CLASSIFIED AS SIDEFF ...' if the \
+ new vernacular command alters the system state but not the \
+ parser nor it starts a proof or ends one;\n\
+ - Use '... EXTEND %s CLASSIFIED BY f ...' to specify \
+ a global function f. The function f will be called passing\
+ \"%s\" as the only argument;\n\
+ - Add a specific classifier in each clause using the syntax:\n\
+ '[...] => [ f ] -> [...]'.\n\
+ Specific classifiers have precedence over global \
+ classifiers. Only one classifier is called."
+ command e e e command
+ in
+ CErrors.user_err (Pp.strbrk msg)
+ in
+ let cl = Array.map_of_list get_classifier ext in
+ let iter i (TyML (depr, ty, f, _)) =
+ let f = untype_command ty f in
+ let r = untype_grammar ty in
+ let () = vinterp_add depr (command, i) f in
+ Egramml.extend_vernac_command_grammar (command, i) entry r
+ in
+ let () = declare_vernac_classifier command cl in
+ List.iteri iter ext
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 79f9c05ad8..fb2a30bac7 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -42,3 +42,33 @@ val universe_polymorphism_option_name : string list
(** Elaborate a [atts] record out of a list of flags.
Also returns whether polymorphism is explicitly (un)set. *)
val attributes_of_flags : Vernacexpr.vernac_flags -> Vernacinterp.atts -> bool option * Vernacinterp.atts
+
+(** {5 VERNAC EXTEND} *)
+
+type classifier = Genarg.raw_generic_argument list -> Vernacexpr.vernac_classification
+
+type (_, _) ty_sig =
+| TyNil : (atts:Vernacinterp.atts -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig
+| TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig
+| TyNonTerminal :
+ string option *
+ ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig ->
+ ('a -> 'r, 'a -> 's) ty_sig
+
+type ty_ml = TyML : bool (** deprecated *) * ('r, 's) ty_sig * 'r * 's option -> ty_ml
+
+(** Wrapper to dynamically extend vernacular commands. *)
+val vernac_extend :
+ command:string ->
+ ?classifier:(string -> Vernacexpr.vernac_classification) ->
+ ?entry:Vernacexpr.vernac_expr Pcoq.Entry.t ->
+ ty_ml list -> unit
+
+(** {5 STM classifiers} *)
+
+val get_vernac_classifier :
+ Vernacexpr.extend_name -> classifier
+
+(** Low-level API, not for casual user. *)
+val declare_vernac_classifier :
+ string -> classifier array -> unit
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index e97cac818a..13c8830b84 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -16,11 +16,11 @@ open Libnames
type class_rawexpr = FunClass | SortClass | RefClass of qualid or_by_notation
type goal_selector = Goal_select.t =
- | SelectAlreadyFocused
- | SelectNth of int
- | SelectList of (int * int) list
- | SelectId of Id.t
- | SelectAll
+ | SelectAlreadyFocused [@ocaml.deprecated "Use Goal_select.SelectAlreadyFocused"]
+ | SelectNth of int [@ocaml.deprecated "Use Goal_select.SelectNth"]
+ | SelectList of (int * int) list [@ocaml.deprecated "Use Goal_select.SelectList"]
+ | SelectId of Id.t [@ocaml.deprecated "Use Goal_select.SelectId"]
+ | SelectAll [@ocaml.deprecated "Use Goal_select.SelectAll"]
[@@ocaml.deprecated "Use Goal_select.t"]
type goal_identifier = string
@@ -103,14 +103,14 @@ type comment =
| CommentInt of int
type reference_or_constr = Hints.reference_or_constr =
- | HintsReference of qualid
- | HintsConstr of constr_expr
+ | HintsReference of qualid [@ocaml.deprecated "Use Hints.HintsReference"]
+ | HintsConstr of constr_expr [@ocaml.deprecated "Use Hints.HintsConstr"]
[@@ocaml.deprecated "Please use [Hints.reference_or_constr]"]
type hint_mode = Hints.hint_mode =
- | ModeInput (* No evars *)
- | ModeNoHeadEvar (* No evar at the head *)
- | ModeOutput (* Anything *)
+ | ModeInput [@ocaml.deprecated "Use Hints.ModeInput"]
+ | ModeNoHeadEvar [@ocaml.deprecated "Use Hints.ModeNoHeadEvar"]
+ | ModeOutput [@ocaml.deprecated "Use Hints.ModeOutput"]
[@@ocaml.deprecated "Please use [Hints.hint_mode]"]
type 'a hint_info_gen = 'a Typeclasses.hint_info_gen =
@@ -128,13 +128,21 @@ type 'a hints_transparency_target = 'a Hints.hints_transparency_target =
type hints_expr = Hints.hints_expr =
| HintsResolve of (Hints.hint_info_expr * bool * Hints.reference_or_constr) list
+ [@ocaml.deprecated "Use the constructor in module [Hints]"]
| HintsResolveIFF of bool * qualid list * int option
+ [@ocaml.deprecated "Use the constructor in module [Hints]"]
| HintsImmediate of Hints.reference_or_constr list
+ [@ocaml.deprecated "Use the constructor in module [Hints]"]
| HintsUnfold of qualid list
+ [@ocaml.deprecated "Use the constructor in module [Hints]"]
| HintsTransparency of qualid hints_transparency_target * bool
+ [@ocaml.deprecated "Use the constructor in module [Hints]"]
| HintsMode of qualid * Hints.hint_mode list
+ [@ocaml.deprecated "Use the constructor in module [Hints]"]
| HintsConstructors of qualid list
+ [@ocaml.deprecated "Use the constructor in module [Hints]"]
| HintsExtern of int * constr_expr option * Genarg.raw_generic_argument
+ [@ocaml.deprecated "Use the constructor in module [Hints]"]
[@@ocaml.deprecated "Please use [Hints.hints_expr]"]
type search_restriction =
@@ -202,7 +210,7 @@ type inductive_expr =
constructor_list_or_record_decl_expr
type one_inductive_expr =
- ident_decl * local_binder_expr list * constr_expr option * constructor_expr list
+ lident * local_binder_expr list * constr_expr option * constructor_expr list
type typeclass_constraint = name_decl * Decl_kinds.binding_kind * constr_expr
and typeclass_context = typeclass_constraint list
@@ -211,9 +219,9 @@ type proof_expr =
ident_decl * (local_binder_expr list * constr_expr)
type syntax_modifier =
- | SetItemLevel of string list * Extend.production_level
- | SetItemLevelAsBinder of string list * Notation_term.constr_as_binder_kind * Extend.production_level option
+ | SetItemLevel of string list * Notation_term.constr_as_binder_kind option * Extend.production_level option
| SetLevel of int
+ | SetCustomEntry of string * int option
| SetAssoc of Extend.gram_assoc
| SetEntryType of string * Extend.simple_constr_prod_entry_key
| SetOnlyParsing
@@ -278,6 +286,7 @@ type extend_name =
It will be extended with primitive inductive types and operators *)
type register_kind =
| RegisterInline
+ | RegisterRetroknowledge of qualid
type bullet = Proof_bullet.t
[@@ocaml.deprecated "Alias type, please use [Proof_bullet.t]"]
@@ -288,7 +297,9 @@ type bullet = Proof_bullet.t
type 'a module_signature = 'a Declaremods.module_signature =
| Enforce of 'a (** ... : T *)
+ [@ocaml.deprecated "Use the constructor in module [Declaremods]"]
| Check of 'a list (** ... <: T1 <: T2, possibly empty *)
+ [@ocaml.deprecated "Use the constructor in module [Declaremods]"]
[@@ocaml.deprecated "please use [Declaremods.module_signature]."]
(** Which module inline annotations should we honor,
@@ -297,8 +308,11 @@ type 'a module_signature = 'a Declaremods.module_signature =
type inline = Declaremods.inline =
| NoInline
+ [@ocaml.deprecated "Use the constructor in module [Declaremods]"]
| DefaultInline
+ [@ocaml.deprecated "Use the constructor in module [Declaremods]"]
| InlineAt of int
+ [@ocaml.deprecated "Use the constructor in module [Declaremods]"]
[@@ocaml.deprecated "please use [Declaremods.inline]."]
type module_ast_inl = module_ast * Declaremods.inline
@@ -325,6 +339,7 @@ type nonrec vernac_expr =
(* Syntax *)
| VernacSyntaxExtension of bool * (lstring * syntax_modifier list)
| VernacOpenCloseScope of bool * scope_name
+ | VernacDeclareScope of scope_name
| VernacDelimiters of scope_name * string option
| VernacBindScope of scope_name * class_rawexpr list
| VernacInfix of (lstring * syntax_modifier list) *
@@ -333,6 +348,7 @@ type nonrec vernac_expr =
constr_expr * (lstring * syntax_modifier list) *
scope_name option
| VernacNotationAddFormat of string * string * string
+ | VernacDeclareCustomEntry of string
(* Gallina *)
| VernacDefinition of (Decl_kinds.discharge * Decl_kinds.definition_object_kind) * name_decl * definition_expr
@@ -436,7 +452,7 @@ type nonrec vernac_expr =
| VernacPrint of printable
| VernacSearch of searchable * Goal_select.t option * search_restriction
| VernacLocate of locatable
- | VernacRegister of lident * register_kind
+ | VernacRegister of qualid * register_kind
| VernacComments of comment list
(* Proof management *)
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index 1bb1414f3d..2746cbd144 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -21,12 +21,13 @@ type atts = {
loc : Loc.t option;
locality : bool option;
polymorphic : bool;
+ template : bool option;
program : bool;
deprecated : deprecation option;
}
-let mk_atts ?(loc=None) ?(locality=None) ?(polymorphic=false) ?(program=false) ?(deprecated=None) () : atts =
- { loc ; locality ; polymorphic ; program ; deprecated }
+let mk_atts ?(loc=None) ?(locality=None) ?(polymorphic=false) ?(template=None) ?(program=false) ?(deprecated=None) () : atts =
+ { loc ; locality ; polymorphic ; program ; deprecated; template }
type 'a vernac_command = 'a -> atts:atts -> st:Vernacstate.t -> Vernacstate.t
diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli
index 46468b3098..62a178b555 100644
--- a/vernac/vernacinterp.mli
+++ b/vernac/vernacinterp.mli
@@ -18,12 +18,14 @@ type atts = {
loc : Loc.t option;
locality : bool option;
polymorphic : bool;
+ template : bool option;
program : bool;
deprecated : deprecation option;
}
val mk_atts : ?loc: Loc.t option -> ?locality: bool option ->
- ?polymorphic: bool -> ?program: bool -> ?deprecated: deprecation option -> unit -> atts
+ ?polymorphic: bool -> ?template:bool option ->
+ ?program: bool -> ?deprecated: deprecation option -> unit -> atts
type 'a vernac_command = 'a -> atts:atts -> st:Vernacstate.t -> Vernacstate.t
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 06:34:41 +0000