aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/classes.ml113
-rw-r--r--vernac/classes.mli9
-rw-r--r--vernac/comInductive.ml20
-rw-r--r--vernac/comInductive.mli5
-rw-r--r--vernac/egramcoq.ml3
-rw-r--r--vernac/explainErr.ml1
-rw-r--r--vernac/g_vernac.mlg20
-rw-r--r--vernac/himsg.ml31
-rw-r--r--vernac/himsg.mli1
-rw-r--r--vernac/lemmas.ml2
-rw-r--r--vernac/metasyntax.ml9
-rw-r--r--vernac/mltop.ml2
-rw-r--r--vernac/ppvernac.ml17
-rw-r--r--vernac/pvernac.ml38
-rw-r--r--vernac/pvernac.mli28
-rw-r--r--vernac/record.ml4
-rw-r--r--vernac/topfmt.ml21
-rw-r--r--vernac/topfmt.mli1
-rw-r--r--vernac/vernacentries.ml73
-rw-r--r--vernac/vernacentries.mli5
-rw-r--r--vernac/vernacexpr.ml10
-rw-r--r--vernac/vernacextend.ml6
-rw-r--r--vernac/vernacextend.mli6
-rw-r--r--vernac/vernacstate.ml35
-rw-r--r--vernac/vernacstate.mli17
25 files changed, 331 insertions, 146 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 370df615fc..5cac6af4b2 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -28,7 +28,7 @@ module RelDecl = Context.Rel.Declaration
open Decl_kinds
open Entries
-let refine_instance = ref true
+let refine_instance = ref false
let () = Goptions.(declare_bool_option {
optdepr = false;
@@ -105,8 +105,6 @@ let id_of_class cl =
mip.(0).Declarations.mind_typename
| _ -> assert false
-open Pp
-
let instance_hook k info global imps ?hook cst =
Impargs.maybe_declare_manual_implicits false cst ~enriching:false imps;
let info = intern_info info in
@@ -128,7 +126,7 @@ let declare_instance_constant k info global imps ?hook id decl poly sigma term t
Declare.declare_univ_binders (ConstRef kn) (Evd.universe_binders sigma);
instance_hook k info global imps ?hook (ConstRef kn)
-let do_abstract_instance env sigma ?hook ~global ~poly k u ctx ctx' pri decl imps subst id =
+let do_declare_instance env sigma ~global ~poly k u ctx ctx' pri decl imps subst id =
let subst = List.fold_left2
(fun subst' s decl -> if is_local_assum decl then s :: subst' else subst')
[] subst (snd k.cl_context)
@@ -144,7 +142,7 @@ let do_abstract_instance env sigma ?hook ~global ~poly k u ctx ctx' pri decl imp
(None,(termtype,univs),None), Decl_kinds.IsAssumption Decl_kinds.Logical)
in
Declare.declare_univ_binders (ConstRef cst) (Evd.universe_binders sigma);
- instance_hook k pri global imps ?hook (ConstRef cst); id
+ instance_hook k pri global imps (ConstRef cst)
let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl ids term termtype =
let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in
@@ -191,7 +189,7 @@ let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id
else ignore (Pfedit.by (Tactics.auto_intros_tac ids));
(match tac with Some tac -> ignore (Pfedit.by tac) | None -> ())) ()
-let do_transparent_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props =
+let do_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props =
let props =
match props with
| Some (true, { CAst.v = CRecord fs }) ->
@@ -271,76 +269,81 @@ let do_transparent_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~pro
Pretyping.check_evars env (Evd.from_env env) sigma termtype;
let termtype = to_constr sigma termtype in
let term = Option.map (to_constr ~abort_on_undefined_evars:false sigma) term in
- if not (Evd.has_undefined sigma) && not (Option.is_empty term) then
+ if not (Evd.has_undefined sigma) && not (Option.is_empty props) then
declare_instance_constant k pri global imps ?hook id decl poly sigma (Option.get term) termtype
- else if program_mode || refine || Option.is_empty term then
+ else if program_mode || refine || Option.is_empty props then
declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl (List.map RelDecl.get_name ctx) term termtype
else CErrors.user_err Pp.(str "Unsolved obligations remaining.");
id
-let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) ~program_mode
- poly ctx (instid, bk, cl) props
- ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri =
- let env = Global.env() in
- let ({CAst.loc;v=instid}, pl) = instid in
+let interp_instance_context env ctx ?(generalize=false) pl bk cl =
let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env pl in
let tclass, ids =
match bk with
| Decl_kinds.Implicit ->
- Implicit_quantifiers.implicit_application Id.Set.empty ~allow_partial:false
- (fun avoid (clname, _) ->
- match clname with
- | Some cl ->
- let t = CAst.make @@ CHole (None, Namegen.IntroAnonymous, None) in
- t, avoid
- | None -> failwith ("new instance: under-applied typeclass"))
- cl
+ Implicit_quantifiers.implicit_application Id.Set.empty ~allow_partial:false
+ (fun avoid (clname, _) ->
+ match clname with
+ | Some cl ->
+ let t = CAst.make @@ CHole (None, Namegen.IntroAnonymous, None) in
+ t, avoid
+ | None -> failwith ("new instance: under-applied typeclass"))
+ cl
| Explicit -> cl, Id.Set.empty
in
let tclass =
if generalize then CAst.make @@ CGeneralization (Implicit, Some AbsPi, tclass)
else tclass
in
- let sigma, k, u, cty, ctx', ctx, len, imps, subst =
- let sigma, (impls, ((env', ctx), imps)) = interp_context_evars env sigma ctx in
- let sigma, (c', imps') = interp_type_evars_impls ~impls env' sigma tclass in
- let len = List.length ctx in
- let imps = imps @ Impargs.lift_implicits len imps' in
- let ctx', c = decompose_prod_assum sigma c' in
- let ctx'' = ctx' @ ctx in
- let (k, u), args = Typeclasses.dest_class_app (push_rel_context ctx'' env) sigma c in
- let u_s = EInstance.kind sigma u in
- let cl = Typeclasses.typeclass_univ_instance (k, u_s) in
- let args = List.map of_constr args in
- let cl_context = List.map (Termops.map_rel_decl of_constr) (snd cl.cl_context) in
- let _, args =
- List.fold_right (fun decl (args, args') ->
- match decl with
- | LocalAssum _ -> (List.tl args, List.hd args :: args')
+ let sigma, (impls, ((env', ctx), imps)) = interp_context_evars env sigma ctx in
+ let sigma, (c', imps') = interp_type_evars_impls ~impls env' sigma tclass in
+ let len = Context.Rel.nhyps ctx in
+ let imps = imps @ Impargs.lift_implicits len imps' in
+ let ctx', c = decompose_prod_assum sigma c' in
+ let ctx'' = ctx' @ ctx in
+ let (k, u), args = Typeclasses.dest_class_app (push_rel_context ctx'' env) sigma c in
+ let u_s = EInstance.kind sigma u in
+ let cl = Typeclasses.typeclass_univ_instance (k, u_s) in
+ let args = List.map of_constr args in
+ let cl_context = List.map (Termops.map_rel_decl of_constr) (snd cl.cl_context) in
+ let _, args =
+ List.fold_right (fun decl (args, args') ->
+ match decl with
+ | LocalAssum _ -> (List.tl args, List.hd args :: args')
| LocalDef (_,b,_) -> (args, Vars.substl args' b :: args'))
- cl_context (args, [])
- in
- sigma, cl, u, c', ctx', ctx, len, imps, args
+ cl_context (args, [])
+ in
+ let sigma = Evarutil.nf_evar_map sigma in
+ let sigma = resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:true env sigma in
+ sigma, cl, u, c', ctx', ctx, imps, args, decl
+
+
+let new_instance ?(global=false) ?(refine= !refine_instance) ~program_mode
+ poly ctx (instid, bk, cl) props
+ ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri =
+ let env = Global.env() in
+ let ({CAst.loc;v=instid}, pl) = instid in
+ let sigma, k, u, cty, ctx', ctx, imps, subst, decl =
+ interp_instance_context env ~generalize ctx pl bk cl
in
let id =
match instid with
- Name id ->
- let sp = Lib.make_path id in
- if Nametab.exists_cci sp then
- user_err ~hdr:"new_instance" (Id.print id ++ Pp.str " already exists.");
- id
- | Anonymous ->
- let i = Nameops.add_suffix (id_of_class k) "_instance_0" in
- Namegen.next_global_ident_away i (Termops.vars_of_env env)
+ | Name id -> id
+ | Anonymous ->
+ let i = Nameops.add_suffix (id_of_class k) "_instance_0" in
+ Namegen.next_global_ident_away i (Termops.vars_of_env env)
in
let env' = push_rel_context ctx env in
- let sigma = Evarutil.nf_evar_map sigma in
- let sigma = resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:true env sigma in
- if abstract then
- do_abstract_instance env sigma ?hook ~global ~poly k u ctx ctx' pri decl imps subst id
- else
- do_transparent_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode
- cty k u ctx ctx' pri decl imps subst id props
+ do_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode
+ cty k u ctx ctx' pri decl imps subst id props
+
+let declare_new_instance ?(global=false) poly ctx (instid, bk, cl) pri =
+ let env = Global.env() in
+ let ({CAst.loc;v=instid}, pl) = instid in
+ let sigma, k, u, cty, ctx', ctx, imps, subst, decl =
+ interp_instance_context env ctx pl bk cl
+ in
+ do_declare_instance env sigma ~global ~poly k u ctx ctx' pri decl imps subst instid
let named_of_rel_context l =
let open Vars in
diff --git a/vernac/classes.mli b/vernac/classes.mli
index eb6c0c92e1..6f61da66cf 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -40,7 +40,6 @@ val declare_instance_constant :
unit
val new_instance :
- ?abstract:bool (** Not abstract by default. *) ->
?global:bool (** Not global by default. *) ->
?refine:bool (** Allow refinement *) ->
program_mode:bool ->
@@ -54,6 +53,14 @@ val new_instance :
Hints.hint_info_expr ->
Id.t
+val declare_new_instance :
+ ?global:bool (** Not global by default. *) ->
+ Decl_kinds.polymorphic ->
+ local_binder_expr list ->
+ ident_decl * Decl_kinds.binding_kind * constr_expr ->
+ Hints.hint_info_expr ->
+ unit
+
(** Setting opacity *)
val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> unit
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 4af6415a4d..92b1ff7572 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -24,7 +24,7 @@ open Constrexpr_ops
open Constrintern
open Impargs
open Reductionops
-open Indtypes
+open Type_errors
open Pretyping
open Indschemes
open Context.Rel.Declaration
@@ -34,6 +34,13 @@ module RelDecl = Context.Rel.Declaration
(* 3b| Mutual inductive definitions *)
+let warn_auto_template =
+ CWarnings.create ~name:"auto-template" ~category:"vernacular" ~default:CWarnings.Disabled
+ (fun id ->
+ Pp.(strbrk "Automatically declaring " ++ Id.print id ++
+ strbrk " as template polymorphic. Use attributes or " ++
+ strbrk "disable Auto Template Polymorphism to avoid this warning."))
+
let should_auto_template =
let open Goptions in
let auto = ref true in
@@ -44,7 +51,10 @@ let should_auto_template =
optread = (fun () -> !auto);
optwrite = (fun b -> auto := b); }
in
- fun () -> !auto
+ fun id would_auto ->
+ let b = !auto && would_auto in
+ if b then warn_auto_template id;
+ b
let rec complete_conclusion a cs = CAst.map_with_loc (fun ?loc -> function
| CProdN (bl,c) -> CProdN (bl,complete_conclusion a cs c)
@@ -294,7 +304,7 @@ let inductive_levels env evd poly arities inds =
let evd =
if Sorts.is_set du then
if not (Evd.check_leq evd cu Univ.type0_univ) then
- raise (Indtypes.InductiveError Indtypes.LargeNonPropInductiveNotInType)
+ raise (InductiveError LargeNonPropInductiveNotInType)
else evd
else evd
(* Evd.set_leq_sort env evd (Type cu) du *)
@@ -431,8 +441,8 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
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
+ should_auto_template ind.ind_name (not poly &&
+ Option.cata (fun s -> not (Sorts.is_small s)) false concl)
in
{ mind_entry_typename = ind.ind_name;
mind_entry_arity = arity;
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index 9df8f7c341..1d6f652385 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -46,7 +46,10 @@ val declare_mutual_inductive_with_eliminations :
mutual_inductive_entry -> UnivNames.universe_binders -> one_inductive_impls list ->
MutInd.t
-val should_auto_template : unit -> bool
+val should_auto_template : Id.t -> bool -> bool
+(** [should_auto_template x b] is [true] when [b] is [true] and we
+ automatically use template polymorphism. [x] is the name of the
+ inductive under consideration. *)
(** Exported for Funind *)
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index 43abc0a200..1a07d74a0e 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -146,7 +146,8 @@ let register_empty_levels accu forpat levels =
(where, ans) :: rem, save_levels accu where nlev
else rem, accu
in
- filter accu levels
+ let (l,accu) = filter accu levels in
+ List.rev l, accu
let find_position accu custom forpat assoc level =
let accu, (clev, plev) = find_levels accu custom in
diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml
index e1496e58d7..71770a21ca 100644
--- a/vernac/explainErr.ml
+++ b/vernac/explainErr.ml
@@ -10,7 +10,6 @@
open Pp
open CErrors
-open Indtypes
open Type_errors
open Pretype_errors
open Indrec
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 22528a607f..79adefdcf7 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -61,7 +61,8 @@ let make_bullet s =
| _ -> assert false
let parse_compat_version = let open Flags in function
- | "8.9" -> Current
+ | "8.10" -> Current
+ | "8.9" -> V8_9
| "8.8" -> V8_8
| "8.7" -> V8_7
| ("8.6" | "8.5" | "8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s ->
@@ -683,19 +684,19 @@ GRAMMAR EXTEND Gram
info = hint_info ;
props = [ ":="; "{"; r = record_declaration; "}" -> { Some (true,r) } |
":="; c = lconstr -> { Some (false,c) } | -> { None } ] ->
- { VernacInstance (false,snd namesup,(fst namesup,expl,t),props,info) }
+ { VernacInstance (snd namesup,(fst namesup,expl,t),props,info) }
| IDENT "Existing"; IDENT "Instance"; id = global;
info = hint_info ->
- { VernacDeclareInstances [id, info] }
+ { VernacExistingInstance [id, info] }
| IDENT "Existing"; IDENT "Instances"; ids = LIST1 global;
pri = OPT [ "|"; i = natural -> { i } ] ->
{ let info = { Typeclasses.hint_priority = pri; hint_pattern = None } in
let insts = List.map (fun i -> (i, info)) ids in
- VernacDeclareInstances insts }
+ VernacExistingInstance insts }
- | IDENT "Existing"; IDENT "Class"; is = global -> { VernacDeclareClass is }
+ | IDENT "Existing"; IDENT "Class"; is = global -> { VernacExistingClass is }
(* Arguments *)
| IDENT "Arguments"; qid = smart_global;
@@ -809,9 +810,8 @@ GRAMMAR EXTEND Gram
| IDENT "transparent" -> { Conv_oracle.transparent } ] ]
;
instance_name:
- [ [ name = ident_decl; sup = OPT binders ->
- { (CAst.map (fun id -> Name id) (fst name), snd name),
- (Option.default [] sup) }
+ [ [ name = ident_decl; bl = binders ->
+ { (CAst.map (fun id -> Name id) (fst name), snd name), bl }
| -> { ((CAst.make ~loc Anonymous), None), [] } ] ]
;
hint_info:
@@ -845,10 +845,10 @@ GRAMMAR EXTEND Gram
[ [ IDENT "Comments"; l = LIST0 comment -> { VernacComments l }
(* Hack! Should be in grammar_ext, but camlp5 factorizes badly *)
- | IDENT "Declare"; IDENT "Instance"; namesup = instance_name; ":";
+ | IDENT "Declare"; IDENT "Instance"; id = ident_decl; bl = binders; ":";
expl = [ "!" -> { Decl_kinds.Implicit } | -> { Decl_kinds.Explicit } ] ; t = operconstr LEVEL "200";
info = hint_info ->
- { VernacInstance (true, snd namesup, (fst namesup, expl, t), None, info) }
+ { VernacDeclareInstance (bl, (id, expl, t), info) }
(* Should be in syntax, but camlp5 would not factorize *)
| IDENT "Declare"; IDENT "Scope"; sc = IDENT ->
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index a2b5c8d70a..ebbec86b9c 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -15,7 +15,6 @@ open Nameops
open Namegen
open Constr
open Termops
-open Indtypes
open Environ
open Pretype_errors
open Type_errors
@@ -511,7 +510,7 @@ let pr_trailing_ne_context_of env sigma =
if List.is_empty (Environ.rel_context env) &&
List.is_empty (Environ.named_context env)
then str "."
- else (str " in environment:"++ pr_context_unlimited env sigma)
+ else (strbrk " in environment:" ++ pr_context_unlimited env sigma)
let rec explain_evar_kind env sigma evk ty =
let open Evar_kinds in
@@ -551,21 +550,21 @@ let rec explain_evar_kind env sigma evk ty =
strbrk "an instance of type " ++ ty ++
str " for the variable " ++ Id.print id
| Evar_kinds.SubEvar (where,evk') ->
- let evi = Evd.find sigma evk' in
+ let rec find_source evk =
+ let evi = Evd.find sigma evk in
+ match snd evi.evar_source with
+ | Evar_kinds.SubEvar (_,evk) -> find_source evk
+ | src -> evi,src in
+ let evi,src = find_source evk' in
let pc = match evi.evar_body with
| Evar_defined c -> pr_leconstr_env env sigma c
| Evar_empty -> assert false in
let ty' = evi.evar_concl in
- (match where with
- | Some Evar_kinds.Body -> str "the body of "
- | Some Evar_kinds.Domain -> str "the domain of "
- | Some Evar_kinds.Codomain -> str "the codomain of "
- | None ->
- pr_existential_key sigma evk ++ str " of type " ++ ty ++
- str " in the partial instance " ++ pc ++
- str " found for ") ++
- explain_evar_kind env sigma evk'
- (pr_leconstr_env env sigma ty') (snd evi.evar_source)
+ pr_existential_key sigma evk ++
+ strbrk " in the partial instance " ++ pc ++
+ strbrk " found for " ++
+ explain_evar_kind env sigma evk
+ (pr_leconstr_env env sigma ty') src
let explain_typeclass_resolution env sigma evi k =
match Typeclasses.class_of_constr sigma evi.evar_concl with
@@ -1163,6 +1162,9 @@ let error_bad_entry () =
let error_large_non_prop_inductive_not_in_type () =
str "Large non-propositional inductive types must be in Type."
+let error_inductive_bad_univs () =
+ str "Incorrect universe constrains declared for inductive type."
+
(* Recursion schemes errors *)
let error_not_allowed_case_analysis env isrec kind i =
@@ -1199,7 +1201,8 @@ let explain_inductive_error = function
| NotAnArity (env, c) -> error_not_an_arity env c
| BadEntry -> error_bad_entry ()
| LargeNonPropInductiveNotInType ->
- error_large_non_prop_inductive_not_in_type ()
+ error_large_non_prop_inductive_not_in_type ()
+ | BadUnivs -> error_inductive_bad_univs ()
(* Recursion schemes errors *)
diff --git a/vernac/himsg.mli b/vernac/himsg.mli
index bab66b2af4..986906d303 100644
--- a/vernac/himsg.mli
+++ b/vernac/himsg.mli
@@ -8,7 +8,6 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-open Indtypes
open Environ
open Type_errors
open Pretype_errors
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 8f155adb8a..0dfbba0e83 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -340,7 +340,7 @@ let start_proof id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?hook c
| None -> standard_proof_terminator ?hook compute_guard
| Some terminator -> terminator ?hook compute_guard
in
- let sign =
+ let sign =
match sign with
| Some sign -> sign
| None -> initialize_named_context_for_proof ()
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 4e79b50b79..3da12e7714 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -1563,14 +1563,17 @@ let add_notation_extra_printing_rule df k v =
(* Infix notations *)
-let inject_var x = CAst.make @@ CRef (qualid_of_ident (Id.of_string x),None)
+let inject_var x = CAst.make @@ CRef (qualid_of_ident x,None)
let add_infix local env ({CAst.loc;v=inf},modifiers) pr sc =
check_infix_modifiers modifiers;
(* check the precedence *)
- let metas = [inject_var "x"; inject_var "y"] in
+ let vars = names_of_constr_expr pr in
+ let x = Namegen.next_ident_away (Id.of_string "x") vars in
+ let y = Namegen.next_ident_away (Id.of_string "y") vars in
+ let metas = [inject_var x; inject_var y] in
let c = mkAppC (pr,metas) in
- let df = CAst.make ?loc @@ "x "^(quote_notation_token inf)^" y" in
+ let df = CAst.make ?loc @@ Id.to_string x ^" "^(quote_notation_token inf)^" "^Id.to_string y in
add_notation local env c (df,modifiers) sc
(**********************************************************************)
diff --git a/vernac/mltop.ml b/vernac/mltop.ml
index 8d6268753e..78e26c65d4 100644
--- a/vernac/mltop.ml
+++ b/vernac/mltop.ml
@@ -215,7 +215,7 @@ let add_vo_path ~recursive lp =
let () = match lp.has_ml with
| AddNoML -> ()
| AddTopML -> add_ml_dir unix_path
- | AddRecML -> List.iter (fun (lp,_) -> add_ml_dir lp) dirs in
+ | AddRecML -> List.iter (fun (lp,_) -> add_ml_dir lp) dirs; add_ml_dir unix_path in
let add (path, dir) =
Loadpath.add_load_path path ~implicit dir in
let () = List.iter add dirs in
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index e0dd3380f9..5eeeaada2d 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -887,10 +887,9 @@ open Pputils
spc() ++ pr_class_rawexpr c2)
)
- | VernacInstance (abst, sup, (instid, bk, cl), props, info) ->
+ | VernacInstance (sup, (instid, bk, cl), props, info) ->
return (
hov 1 (
- (if abst then keyword "Declare" ++ spc () else mt ()) ++
keyword "Instance" ++
(match instid with
| {loc; v = Name id}, l -> spc () ++ pr_ident_decl (CAst.(make ?loc id),l) ++ spc ()
@@ -906,13 +905,23 @@ open Pputils
| None -> mt()))
)
+ | VernacDeclareInstance (sup, (instid, bk, cl), info) ->
+ return (
+ hov 1 (
+ keyword "Declare Instance" ++ spc () ++ pr_ident_decl instid ++ spc () ++
+ pr_and_type_binders_arg sup ++
+ str":" ++ spc () ++
+ (match bk with Implicit -> str "! " | Explicit -> mt ()) ++
+ pr_constr cl ++ pr_hint_info pr_constr_pattern_expr info)
+ )
+
| VernacContext l ->
return (
hov 1 (
keyword "Context" ++ pr_and_type_binders_arg l)
)
- | VernacDeclareInstances insts ->
+ | VernacExistingInstance insts ->
let pr_inst (id, info) =
pr_qualid id ++ pr_hint_info pr_constr_pattern_expr info
in
@@ -922,7 +931,7 @@ open Pputils
spc () ++ prlist_with_sep (fun () -> str", ") pr_inst insts)
)
- | VernacDeclareClass id ->
+ | VernacExistingClass id ->
return (
hov 1 (keyword "Existing" ++ spc () ++ keyword "Class" ++ spc () ++ pr_qualid id)
)
diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml
index a647b2ef73..0e46df2320 100644
--- a/vernac/pvernac.ml
+++ b/vernac/pvernac.ml
@@ -12,6 +12,27 @@ open Pcoq
let uvernac = create_universe "vernac"
+type proof_mode = string
+
+(* Tactic parsing modes *)
+let register_proof_mode, find_proof_mode, lookup_proof_mode =
+ let proof_mode : (string, Vernacexpr.vernac_expr Entry.t) Hashtbl.t =
+ Hashtbl.create 19 in
+ let register_proof_mode ename e = Hashtbl.add proof_mode ename e; ename in
+ let find_proof_mode ename =
+ try Hashtbl.find proof_mode ename
+ with Not_found ->
+ CErrors.anomaly Pp.(str "proof mode not found: " ++ str ename) in
+ let lookup_proof_mode name =
+ if Hashtbl.mem proof_mode name then Some name
+ else None
+ in
+ register_proof_mode, find_proof_mode, lookup_proof_mode
+
+let proof_mode_to_string name = name
+
+let command_entry_ref = ref None
+
module Vernac_ =
struct
let gec_vernac s = Entry.create ("vernac:" ^ s)
@@ -39,17 +60,24 @@ module Vernac_ =
] in
Pcoq.grammar_extend main_entry None (None, [None, None, rule])
- let command_entry_ref = ref noedit_mode
+ let select_tactic_entry spec =
+ match spec with
+ | None -> noedit_mode
+ | Some ename -> find_proof_mode ename
+
let command_entry =
Pcoq.Entry.of_parser "command_entry"
- (fun strm -> Pcoq.Entry.parse_token_stream !command_entry_ref strm)
+ (fun strm -> Pcoq.Entry.parse_token_stream (select_tactic_entry !command_entry_ref) strm)
end
-let main_entry = Vernac_.main_entry
+module Unsafe = struct
+ let set_tactic_entry oname = command_entry_ref := oname
+end
-let set_command_entry e = Vernac_.command_entry_ref := e
-let get_command_entry () = !Vernac_.command_entry_ref
+let main_entry proof_mode =
+ Unsafe.set_tactic_entry proof_mode;
+ Vernac_.main_entry
let () =
register_grammar Genredexpr.wit_red_expr (Vernac_.red_expr);
diff --git a/vernac/pvernac.mli b/vernac/pvernac.mli
index b2f8f71462..fa251281dc 100644
--- a/vernac/pvernac.mli
+++ b/vernac/pvernac.mli
@@ -14,6 +14,8 @@ open Vernacexpr
val uvernac : gram_universe
+type proof_mode
+
module Vernac_ :
sig
val gallina : vernac_expr Entry.t
@@ -24,13 +26,31 @@ module Vernac_ :
val rec_definition : (fixpoint_expr * decl_notation list) Entry.t
val noedit_mode : vernac_expr Entry.t
val command_entry : vernac_expr Entry.t
+ val main_entry : (Loc.t * vernac_control) option Entry.t
val red_expr : raw_red_expr Entry.t
val hint_info : Hints.hint_info_expr Entry.t
end
+(* To be removed when the parser is made functional wrt the tactic
+ * non terminal *)
+module Unsafe : sig
+ (* To let third party grammar entries reuse Vernac_ and
+ * do something with the proof mode *)
+ val set_tactic_entry : proof_mode option -> unit
+end
+
(** The main entry: reads an optional vernac command *)
-val main_entry : (Loc.t * vernac_control) option Entry.t
+val main_entry : proof_mode option -> (Loc.t * vernac_control) option Entry.t
+
+(** Grammar entry for tactics: proof mode(s).
+ By default Coq's grammar has an empty entry (non-terminal) for
+ tactics. A plugin can register its non-terminal by providing a name
+ and a grammar entry.
+
+ For example the Ltac plugin register the "Classic" grammar
+ entry for parsing its tactics.
+ *)
-(** Handling of the proof mode entry *)
-val get_command_entry : unit -> vernac_expr Entry.t
-val set_command_entry : vernac_expr Entry.t -> unit
+val register_proof_mode : string -> Vernacexpr.vernac_expr Entry.t -> proof_mode
+val lookup_proof_mode : string -> proof_mode option
+val proof_mode_to_string : proof_mode -> string
diff --git a/vernac/record.ml b/vernac/record.ml
index ffd4f654c6..2867ad1437 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -415,9 +415,9 @@ let declare_structure finite ubinders univs paramimpls params template ?(kind=St
template
| None, template ->
(* auto detect template *)
- ComInductive.should_auto_template () && template && not poly &&
+ ComInductive.should_auto_template id (template && not poly &&
let _, s = Reduction.dest_arity (Global.env()) arity in
- not (Sorts.is_small s)
+ not (Sorts.is_small s))
in
{ mind_entry_typename = id;
mind_entry_arity = arity;
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
index 4065bb9c1f..b4b893a3fd 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -406,3 +406,24 @@ let with_output_to_file fname func input =
deep_ft := Util.pi3 old_fmt;
close_out channel;
Exninfo.iraise reraise
+
+(* For coqtop -time, we display the position in the file,
+ and a glimpse of the executed command *)
+
+let pr_cmd_header {CAst.loc;v=com} =
+ let shorten s =
+ if Unicode.utf8_length s > 33 then (Unicode.utf8_sub s 0 30) ^ "..." else s
+ in
+ let noblank s = String.map (fun c ->
+ match c with
+ | ' ' | '\n' | '\t' | '\r' -> '~'
+ | x -> x
+ ) s
+ in
+ let (start,stop) = Option.cata Loc.unloc (0,0) loc in
+ let safe_pr_vernac x =
+ try Ppvernac.pr_vernac x
+ with e -> str (Printexc.to_string e) in
+ let cmd = noblank (shorten (string_of_ppcmds (safe_pr_vernac com)))
+ in str "Chars " ++ int start ++ str " - " ++ int stop ++
+ str " [" ++ str cmd ++ str "] "
diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli
index 0ddf474970..5f84c5edee 100644
--- a/vernac/topfmt.mli
+++ b/vernac/topfmt.mli
@@ -71,3 +71,4 @@ val print_err_exn : exn -> unit
redirected to a file [file] *)
val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b
+val pr_cmd_header : Vernacexpr.vernac_control CAst.t -> Pp.t
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index e6e3db4beb..996fe320f9 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -489,6 +489,28 @@ let vernac_notation ~module_local =
let vernac_custom_entry ~module_local s =
Metasyntax.declare_custom_entry module_local s
+(* Default proof mode, to be set at the beginning of proofs for
+ programs that cannot be statically classified. *)
+let default_proof_mode = ref (Pvernac.register_proof_mode "Noedit" Pvernac.Vernac_.noedit_mode)
+let get_default_proof_mode () = !default_proof_mode
+
+let get_default_proof_mode_opt () = Pvernac.proof_mode_to_string !default_proof_mode
+let set_default_proof_mode_opt name =
+ default_proof_mode :=
+ match Pvernac.lookup_proof_mode name with
+ | Some pm -> pm
+ | None -> CErrors.user_err Pp.(str (Format.sprintf "No proof mode named \"%s\"." name))
+
+let proof_mode_opt_name = ["Default";"Proof";"Mode"]
+let () =
+ Goptions.declare_string_option Goptions.{
+ optdepr = false;
+ optname = "default proof mode" ;
+ optkey = proof_mode_opt_name;
+ optread = get_default_proof_mode_opt;
+ optwrite = set_default_proof_mode_opt;
+ }
+
(***********)
(* Gallina *)
@@ -1005,22 +1027,29 @@ let vernac_identity_coercion ~atts id qids qidt =
(* Type classes *)
-let vernac_instance ~atts abst sup inst props pri =
+let vernac_instance ~atts sup inst props pri =
let open DefAttributes in
let atts = parse atts in
let global = not (make_section_locality atts.locality) in
Dumpglob.dump_constraint (fst (pi1 inst)) false "inst";
let program_mode = Flags.is_program_mode () in
- ignore(Classes.new_instance ~program_mode ~abstract:abst ~global atts.polymorphic sup inst props pri)
+ ignore(Classes.new_instance ~program_mode ~global atts.polymorphic sup inst props pri)
+
+let vernac_declare_instance ~atts sup inst pri =
+ let open DefAttributes in
+ let atts = parse atts in
+ let global = not (make_section_locality atts.locality) in
+ Dumpglob.dump_definition (fst (pi1 inst)) false "inst";
+ Classes.declare_new_instance ~global atts.polymorphic sup inst pri
let vernac_context ~poly l =
if not (Classes.context poly l) then Feedback.feedback Feedback.AddedAxiom
-let vernac_declare_instances ~section_local insts =
+let vernac_existing_instance ~section_local insts =
let glob = not section_local in
List.iter (fun (id, info) -> Classes.existing_instance glob id (Some info)) insts
-let vernac_declare_class id =
+let vernac_existing_class id =
Record.declare_existing_class (Nametab.global id)
(***********)
@@ -2108,13 +2137,9 @@ exception End_of_input
let vernac_load interp fname =
if Proof_global.there_are_pending_proofs () then
CErrors.user_err Pp.(str "Load is not supported inside proofs.");
- let interp x =
- let proof_mode = Proof_global.get_default_proof_mode_name () [@ocaml.warning "-3"] in
- Proof_global.activate_proof_mode proof_mode [@ocaml.warning "-3"];
- interp x in
- let parse_sentence = Flags.with_option Flags.we_are_parsing
+ let parse_sentence proof_mode = Flags.with_option Flags.we_are_parsing
(fun po ->
- match Pcoq.Entry.parse Pvernac.main_entry po with
+ match Pcoq.Entry.parse (Pvernac.main_entry proof_mode) po with
| Some x -> x
| None -> raise End_of_input) in
let fname =
@@ -2125,7 +2150,15 @@ let vernac_load interp fname =
let in_chan = open_utf8_file_in longfname in
Pcoq.Parsable.make ~file:(Loc.InFile longfname) (Stream.of_channel in_chan) in
begin
- try while true do interp (snd (parse_sentence input)) done
+ try while true do
+ let proof_mode =
+ if Proof_global.there_are_pending_proofs () then
+ Some (get_default_proof_mode ())
+ else
+ None
+ in
+ interp (snd (parse_sentence proof_mode input));
+ done
with End_of_input -> ()
end;
(* If Load left a proof open, we fail too. *)
@@ -2227,11 +2260,13 @@ let interp ?proof ~atts ~st c =
vernac_identity_coercion ~atts id s t
(* Type classes *)
- | VernacInstance (abst, sup, inst, props, info) ->
- vernac_instance ~atts abst sup inst props info
+ | VernacInstance (sup, inst, props, info) ->
+ vernac_instance ~atts sup inst props info
+ | VernacDeclareInstance (sup, inst, info) ->
+ vernac_declare_instance ~atts sup inst info
| VernacContext sup -> vernac_context ~poly:(only_polymorphism atts) sup
- | VernacDeclareInstances insts -> with_section_locality ~atts vernac_declare_instances insts
- | VernacDeclareClass id -> unsupported_attributes atts; vernac_declare_class id
+ | VernacExistingInstance insts -> with_section_locality ~atts vernac_existing_instance insts
+ | VernacExistingClass id -> unsupported_attributes atts; vernac_existing_class id
(* Solving *)
| VernacSolveExistential (n,c) -> unsupported_attributes atts; vernac_solve_existential n c
@@ -2303,8 +2338,7 @@ let interp ?proof ~atts ~st c =
Aux_file.record_in_aux_at "VernacProof" (tacs^" "^usings);
Option.iter vernac_set_end_tac tac;
Option.iter vernac_set_used_variables using
- | VernacProofMode mn -> unsupported_attributes atts;
- Proof_global.set_proof_mode mn [@ocaml.warning "-3"]
+ | VernacProofMode mn -> unsupported_attributes atts; ()
(* Extensions *)
| VernacExtend (opn,args) ->
@@ -2388,8 +2422,9 @@ let interp ?(verbosely=true) ?proof ~st {CAst.loc;v=c} =
control v
| VernacRedirect (s, {v}) ->
Topfmt.with_output_to_file s control v
- | VernacTime (batch, {v}) ->
- System.with_time ~batch control v;
+ | VernacTime (batch, com) ->
+ let header = if batch then Topfmt.pr_cmd_header com else Pp.mt () in
+ System.with_time ~batch ~header control com.CAst.v;
and aux ~atts : _ -> unit =
function
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 8d8d7cfcf0..4fbd3849b0 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -10,6 +10,11 @@
val dump_global : Libnames.qualid Constrexpr.or_by_notation -> unit
+(** Default proof mode set by `start_proof` *)
+val get_default_proof_mode : unit -> Pvernac.proof_mode
+
+val proof_mode_opt_name : string list
+
(** Vernacular entries *)
val vernac_require :
Libnames.qualid option -> bool option -> Libnames.qualid list -> unit
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 417c9ebfbd..68a17e316e 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -300,18 +300,22 @@ type nonrec vernac_expr =
(* Type classes *)
| VernacInstance of
- bool * (* abstract instance *)
local_binder_expr list * (* super *)
typeclass_constraint * (* instance name, class name, params *)
(bool * constr_expr) option * (* props *)
Hints.hint_info_expr
+ | VernacDeclareInstance of
+ local_binder_expr list * (* super *)
+ (ident_decl * Decl_kinds.binding_kind * constr_expr) * (* instance name, class name, params *)
+ Hints.hint_info_expr
+
| VernacContext of local_binder_expr list
- | VernacDeclareInstances of
+ | VernacExistingInstance of
(qualid * Hints.hint_info_expr) list (* instances names, priorities and patterns *)
- | VernacDeclareClass of qualid (* inductive or definition name *)
+ | VernacExistingClass of qualid (* inductive or definition name *)
(* Modules and Module Types *)
| VernacDeclareModule of bool option * lident *
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml
index 05687afd8b..f5cf3401d0 100644
--- a/vernac/vernacextend.ml
+++ b/vernac/vernacextend.ml
@@ -29,15 +29,15 @@ type vernac_type =
parallel : [ `Yes of solving_tac * anon_abstracting_tac | `No ];
proof_block_detection : proof_block_name option
}
- (* To be removed *)
- | VtProofMode of string
(* Queries are commands assumed to be "pure", that is to say, they
don't modify the interpretation state. *)
| VtQuery
+ (* Commands that change the current proof mode *)
+ | VtProofMode of string
(* To be removed *)
| VtMeta
| VtUnknown
-and vernac_start = string * opacity_guarantee * Names.Id.t list
+and vernac_start = opacity_guarantee * Names.Id.t list
and vernac_sideff_type = Names.Id.t list
and opacity_guarantee =
| GuaranteesOpacity (** Only generates opaque terms at [Qed] *)
diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli
index 0d43eb1ee8..118907c31b 100644
--- a/vernac/vernacextend.mli
+++ b/vernac/vernacextend.mli
@@ -45,15 +45,15 @@ type vernac_type =
parallel : [ `Yes of solving_tac * anon_abstracting_tac | `No ];
proof_block_detection : proof_block_name option
}
- (* To be removed *)
- | VtProofMode of string
(* Queries are commands assumed to be "pure", that is to say, they
don't modify the interpretation state. *)
| VtQuery
+ (* Commands that change the current proof mode *)
+ | VtProofMode of string
(* To be removed *)
| VtMeta
| VtUnknown
-and vernac_start = string * opacity_guarantee * Names.Id.t list
+and vernac_start = opacity_guarantee * Names.Id.t list
and vernac_sideff_type = Names.Id.t list
and opacity_guarantee =
| GuaranteesOpacity (** Only generates opaque terms at [Qed] *)
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index b40bccf27e..c691dc8559 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -8,10 +8,30 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
+module Parser = struct
+
+ type state = Pcoq.frozen_t
+
+ let init () = Pcoq.freeze ~marshallable:false
+
+ let cur_state () = Pcoq.freeze ~marshallable:false
+
+ let parse ps entry pa =
+ Pcoq.unfreeze ps;
+ Flags.with_option Flags.we_are_parsing (fun () ->
+ try Pcoq.Entry.parse entry pa
+ with e when CErrors.noncritical e ->
+ let (e, info) = CErrors.push e in
+ Exninfo.iraise (e, info))
+ ()
+
+end
+
type t = {
- system : States.state; (* summary + libstack *)
- proof : Proof_global.t; (* proof state *)
- shallow : bool (* is the state trimmed down (libstack) *)
+ parsing: Parser.state;
+ system : States.state; (* summary + libstack *)
+ proof : Proof_global.t; (* proof state *)
+ shallow : bool; (* is the state trimmed down (libstack) *)
}
let s_cache = ref None
@@ -36,11 +56,14 @@ let do_if_not_cached rf f v =
let freeze_interp_state ~marshallable =
{ system = update_cache s_cache (States.freeze ~marshallable);
proof = update_cache s_proof (Proof_global.freeze ~marshallable);
- shallow = marshallable }
+ shallow = false;
+ parsing = Parser.cur_state ();
+ }
-let unfreeze_interp_state { system; proof } =
+let unfreeze_interp_state { system; proof; parsing } =
do_if_not_cached s_cache States.unfreeze system;
- do_if_not_cached s_proof Proof_global.unfreeze proof
+ do_if_not_cached s_proof Proof_global.unfreeze proof;
+ Pcoq.unfreeze parsing
let make_shallow st =
let lib = States.lib_of_state st.system in
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli
index ed20cb935a..581c23386a 100644
--- a/vernac/vernacstate.mli
+++ b/vernac/vernacstate.mli
@@ -8,10 +8,21 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
+module Parser : sig
+ type state
+
+ val init : unit -> state
+ val cur_state : unit -> state
+
+ val parse : state -> 'a Pcoq.Entry.t -> Pcoq.Parsable.t -> 'a
+
+end
+
type t = {
- system : States.state; (* summary + libstack *)
- proof : Proof_global.t; (* proof state *)
- shallow : bool (* is the state trimmed down (libstack) *)
+ parsing: Parser.state;
+ system : States.state; (* summary + libstack *)
+ proof : Proof_global.t; (* proof state *)
+ shallow : bool; (* is the state trimmed down (libstack) *)
}
val freeze_interp_state : marshallable:bool -> t
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 05:51:42 +0000