aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/auto_ind_decl.ml12
-rw-r--r--vernac/classes.ml2
-rw-r--r--vernac/command.ml5
-rw-r--r--vernac/discharge.ml122
-rw-r--r--vernac/himsg.ml27
-rw-r--r--vernac/lemmas.ml32
-rw-r--r--vernac/metasyntax.ml13
-rw-r--r--vernac/mltop.ml1
-rw-r--r--vernac/obligations.ml6
-rw-r--r--vernac/proof_using.ml190
-rw-r--r--vernac/proof_using.mli (renamed from vernac/discharge.mli)17
-rw-r--r--vernac/record.ml2
-rw-r--r--vernac/vernac.mllib1
-rw-r--r--vernac/vernacentries.ml86
-rw-r--r--vernac/vernacentries.mli16
15 files changed, 320 insertions, 212 deletions
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 59920742d..503508fc0 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -533,7 +533,7 @@ open Namegen
let compute_bl_goal ind lnamesparrec nparrec =
let eqI, eff = eqI ind lnamesparrec in
let list_id = list_id lnamesparrec in
- let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in
+ let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> Id.Set.add id l)) (List.map RelDecl.get_name lnamesparrec) Id.Set.empty in
let create_input c =
let x = next_ident_away (Id.of_string "x") avoid and
y = next_ident_away (Id.of_string "y") avoid in
@@ -578,7 +578,7 @@ let compute_bl_tact mode bl_scheme_key ind lnamesparrec nparrec =
( List.map (fun (_,_,sbl,_ ) -> sbl) list_id )
in
let fresh_id s gl =
- let fresh = fresh_id_in_env (!avoid) s (Proofview.Goal.env gl) in
+ let fresh = fresh_id_in_env (Id.Set.of_list !avoid) s (Proofview.Goal.env gl) in
avoid := fresh::(!avoid); fresh
in
Proofview.Goal.enter begin fun gl ->
@@ -676,7 +676,7 @@ let _ = bl_scheme_kind_aux := fun () -> bl_scheme_kind
let compute_lb_goal ind lnamesparrec nparrec =
let list_id = list_id lnamesparrec in
let eq = Lazy.force eq and tt = Lazy.force tt and bb = Lazy.force bb in
- let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in
+ let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> Id.Set.add id l)) (List.map RelDecl.get_name lnamesparrec) Id.Set.empty in
let eqI, eff = eqI ind lnamesparrec in
let create_input c =
let x = next_ident_away (Id.of_string "x") avoid and
@@ -722,7 +722,7 @@ let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec =
( List.map (fun (_,_,_,slb) -> slb) list_id )
in
let fresh_id s gl =
- let fresh = fresh_id_in_env (!avoid) s (Proofview.Goal.env gl) in
+ let fresh = fresh_id_in_env (Id.Set.of_list !avoid) s (Proofview.Goal.env gl) in
avoid := fresh::(!avoid); fresh
in
Proofview.Goal.enter begin fun gl ->
@@ -806,7 +806,7 @@ let compute_dec_goal ind lnamesparrec nparrec =
check_not_is_defined ();
let eq = Lazy.force eq and tt = Lazy.force tt and bb = Lazy.force bb in
let list_id = list_id lnamesparrec in
- let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in
+ let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> Id.Set.add id l)) (List.map RelDecl.get_name lnamesparrec) Id.Set.empty in
let create_input c =
let x = next_ident_away (Id.of_string "x") avoid and
y = next_ident_away (Id.of_string "y") avoid in
@@ -870,7 +870,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
( List.map (fun (_,_,_,slb) -> slb) list_id )
in
let fresh_id s gl =
- let fresh = fresh_id_in_env (!avoid) s (Proofview.Goal.env gl) in
+ let fresh = fresh_id_in_env (Id.Set.of_list !avoid) s (Proofview.Goal.env gl) in
avoid := fresh::(!avoid); fresh
in
Proofview.Goal.enter begin fun gl ->
diff --git a/vernac/classes.ml b/vernac/classes.ml
index c21345a2a..0926c93e5 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -183,7 +183,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
id
| Anonymous ->
let i = Nameops.add_suffix (id_of_class k) "_instance_0" in
- Namegen.next_global_ident_away i (Termops.ids_of_context env)
+ Namegen.next_global_ident_away i (Termops.vars_of_env env)
in
let env' = push_rel_context ctx env in
evars := Evarutil.nf_evar_map !evars;
diff --git a/vernac/command.ml b/vernac/command.ml
index 1668a93f1..f58ed065c 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -79,7 +79,7 @@ let red_constant_entry n ce sigma = function
let (_, c) = redfun env sigma c in
EConstr.Unsafe.to_constr c
in
- { ce with const_entry_body = Future.chain ~pure:true proof_out
+ { ce with const_entry_body = Future.chain proof_out
(fun ((body,ctx),eff) -> (under_binders env sigma redfun n body,ctx),eff) }
let warn_implicits_in_term =
@@ -518,7 +518,8 @@ let check_param = function
| CLocalDef (na, _, _) -> check_named na
| CLocalAssum (nas, Default _, _) -> List.iter check_named nas
| CLocalAssum (nas, Generalized _, _) -> ()
-| CLocalPattern _ -> assert false
+| CLocalPattern (loc,_) ->
+ Loc.raise ?loc (Stream.Error "pattern with quote not allowed here.")
let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
check_all_names_different indl;
diff --git a/vernac/discharge.ml b/vernac/discharge.ml
deleted file mode 100644
index 0e4bbd299..000000000
--- a/vernac/discharge.ml
+++ /dev/null
@@ -1,122 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Names
-open CErrors
-open Util
-open Term
-open Vars
-open Declarations
-open Cooking
-open Entries
-open Context.Rel.Declaration
-
-(********************************)
-(* Discharging mutual inductive *)
-
-let detype_param =
- function
- | LocalAssum (Name id, p) -> id, LocalAssumEntry p
- | LocalDef (Name id, p,_) -> id, LocalDefEntry p
- | _ -> anomaly (Pp.str "Unnamed inductive local variable.")
-
-(* Replace
-
- Var(y1)..Var(yq):C1..Cq |- Ij:Bj
- Var(y1)..Var(yq):C1..Cq; I1..Ip:B1..Bp |- ci : Ti
-
- by
-
- |- Ij: (y1..yq:C1..Cq)Bj
- I1..Ip:(B1 y1..yq)..(Bp y1..yq) |- ci : (y1..yq:C1..Cq)Ti[Ij:=(Ij y1..yq)]
-*)
-
-let abstract_inductive decls nparamdecls inds =
- let ntyp = List.length inds in
- let ndecls = Context.Named.length decls in
- let args = Context.Named.to_instance mkVar (List.rev decls) in
- let args = Array.of_list args in
- let subs = List.init ntyp (fun k -> lift ndecls (mkApp(mkRel (k+1),args))) in
- let inds' =
- List.map
- (function (tname,arity,template,cnames,lc) ->
- let lc' = List.map (substl subs) lc in
- let lc'' = List.map (fun b -> Termops.it_mkNamedProd_wo_LetIn b decls) lc' in
- let arity' = Termops.it_mkNamedProd_wo_LetIn arity decls in
- (tname,arity',template,cnames,lc''))
- inds in
- let nparamdecls' = nparamdecls + Array.length args in
-(* To be sure to be the same as before, should probably be moved to process_inductive *)
- let params' = let (_,arity,_,_,_) = List.hd inds' in
- let (params,_) = decompose_prod_n_assum nparamdecls' arity in
- List.map detype_param params
- in
- let ind'' =
- List.map
- (fun (a,arity,template,c,lc) ->
- let _, short_arity = decompose_prod_n_assum nparamdecls' arity in
- let shortlc =
- List.map (fun c -> snd (decompose_prod_n_assum nparamdecls' c)) lc in
- { mind_entry_typename = a;
- mind_entry_arity = short_arity;
- mind_entry_template = template;
- mind_entry_consnames = c;
- mind_entry_lc = shortlc })
- inds'
- in (params',ind'')
-
-let refresh_polymorphic_type_of_inductive (_,mip) =
- match mip.mind_arity with
- | RegularArity s -> s.mind_user_arity, false
- | TemplateArity ar ->
- let ctx = List.rev mip.mind_arity_ctxt in
- mkArity (List.rev ctx, Type ar.template_level), true
-
-let process_inductive (section_decls,_,_ as info) modlist mib =
- let section_decls = Lib.named_of_variable_context section_decls in
- let nparamdecls = Context.Rel.length mib.mind_params_ctxt in
- let subst, ind_univs =
- match mib.mind_universes with
- | Monomorphic_ind ctx -> Univ.empty_level_subst, Monomorphic_ind_entry ctx
- | Polymorphic_ind auctx ->
- let subst, auctx = Lib.discharge_abstract_universe_context info auctx in
- let auctx = Univ.AUContext.repr auctx in
- subst, Polymorphic_ind_entry auctx
- | Cumulative_ind cumi ->
- let auctx = Univ.ACumulativityInfo.univ_context cumi in
- let subst, auctx = Lib.discharge_abstract_universe_context info auctx in
- let auctx = Univ.AUContext.repr auctx in
- subst, Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context auctx)
- in
- let discharge c = Vars.subst_univs_level_constr subst (expmod_constr modlist c) in
- let inds =
- Array.map_to_list
- (fun mip ->
- let ty, template = refresh_polymorphic_type_of_inductive (mib,mip) in
- let arity = discharge ty in
- let lc = Array.map discharge mip.mind_user_lc in
- (mip.mind_typename,
- arity, template,
- Array.to_list mip.mind_consnames,
- Array.to_list lc))
- mib.mind_packets in
- let section_decls' = Context.Named.map discharge section_decls in
- let (params',inds') = abstract_inductive section_decls' nparamdecls inds in
- let record = match mib.mind_record with
- | Some (Some (id, _, _)) -> Some (Some id)
- | Some None -> Some None
- | None -> None
- in
- { mind_entry_record = record;
- mind_entry_finite = mib.mind_finite;
- mind_entry_params = params';
- mind_entry_inds = inds';
- mind_entry_private = mib.mind_private;
- mind_entry_universes = ind_univs
- }
-
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 12b68fe38..189c47aab 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -84,7 +84,7 @@ let rec contract3' env sigma a b c = function
(** Ad-hoc reductions *)
let j_nf_betaiotaevar sigma j =
- { uj_val = Evarutil.nf_evar sigma j.uj_val;
+ { uj_val = j.uj_val;
uj_type = Reductionops.nf_betaiota sigma j.uj_type }
let jv_nf_betaiotaevar sigma jl =
@@ -173,7 +173,6 @@ let explain_unbound_var env v =
str "No such section variable or assumption: " ++ var ++ str "."
let explain_not_type env sigma j =
- let j = Evarutil.j_nf_evar sigma j in
let pe = pr_ne_context_of (str "In environment") env sigma in
let pc,pt = pr_ljudge_env env sigma j in
pe ++ str "The term" ++ brk(1,1) ++ pc ++ spc () ++
@@ -241,7 +240,6 @@ let explain_elim_arity env sigma ind sorts c pj okinds =
fnl () ++ msg
let explain_case_not_inductive env sigma cj =
- let cj = Evarutil.j_nf_evar sigma cj in
let env = make_all_name_different env sigma in
let pc = pr_leconstr_env env sigma cj.uj_val in
let pct = pr_leconstr_env env sigma cj.uj_type in
@@ -254,7 +252,6 @@ let explain_case_not_inductive env sigma cj =
str "which is not a (co-)inductive type."
let explain_number_branches env sigma cj expn =
- let cj = Evarutil.j_nf_evar sigma cj in
let env = make_all_name_different env sigma in
let pc = pr_leconstr_env env sigma cj.uj_val in
let pct = pr_leconstr_env env sigma cj.uj_type in
@@ -263,7 +260,7 @@ let explain_number_branches env sigma cj expn =
str "expects " ++ int expn ++ str " branches."
let explain_ill_formed_branch env sigma c ci actty expty =
- let simp t = Reductionops.nf_betaiota sigma (Evarutil.nf_evar sigma t) in
+ let simp t = Reductionops.nf_betaiota sigma t in
let env = make_all_name_different env sigma in
let pc = pr_leconstr_env env sigma c in
let pa, pe = pr_explicit env sigma (simp actty) (simp expty) in
@@ -300,10 +297,10 @@ let explain_unification_error env sigma p1 p2 = function
| NotSameArgSize | NotSameHead | NoCanonicalStructure ->
(* Error speaks from itself *) []
| ConversionFailed (env,t1,t2) ->
+ let t1 = Reductionops.nf_betaiota sigma t1 in
+ let t2 = Reductionops.nf_betaiota sigma t2 in
if EConstr.eq_constr sigma t1 p1 && EConstr.eq_constr sigma t2 p2 then [] else
let env = make_all_name_different env sigma in
- let t1 = Evarutil.nf_evar sigma t1 in
- let t2 = Evarutil.nf_evar sigma t2 in
if not (EConstr.eq_constr sigma t1 p1) || not (EConstr.eq_constr sigma t2 p2) then
let t1, t2 = pr_explicit env sigma t1 t2 in
[str "cannot unify " ++ t1 ++ strbrk " and " ++ t2]
@@ -327,8 +324,6 @@ let explain_unification_error env sigma p1 p2 = function
| CannotSolveConstraint ((pb,env,t,u),e) ->
let t = EConstr.of_constr t in
let u = EConstr.of_constr u in
- let t = Evarutil.nf_evar sigma t in
- let u = Evarutil.nf_evar sigma u in
let env = make_all_name_different env sigma in
(strbrk "cannot satisfy constraint " ++ pr_leconstr_env env sigma t ++
str " == " ++ pr_leconstr_env env sigma u)
@@ -359,9 +354,7 @@ let explain_actual_type env sigma j t reason =
let explain_cant_apply_bad_type env sigma (n,exptyp,actualtyp) rator randl =
let randl = jv_nf_betaiotaevar sigma randl in
- let exptyp = Evarutil.nf_evar sigma exptyp in
let actualtyp = Reductionops.nf_betaiota sigma actualtyp in
- let rator = Evarutil.j_nf_evar sigma rator in
let env = make_all_name_different env sigma in
let actualtyp, exptyp = pr_explicit env sigma actualtyp exptyp in
let nargs = Array.length randl in
@@ -386,8 +379,6 @@ let explain_cant_apply_bad_type env sigma (n,exptyp,actualtyp) rator randl =
exptyp ++ str "."
let explain_cant_apply_not_functional env sigma rator randl =
- let randl = Evarutil.jv_nf_evar sigma randl in
- let rator = Evarutil.j_nf_evar sigma rator in
let env = make_all_name_different env sigma in
let nargs = Array.length randl in
(* let pe = pr_ne_context_of (str "in environment") env sigma in*)
@@ -407,8 +398,6 @@ let explain_cant_apply_not_functional env sigma rator randl =
fnl () ++ str " " ++ v 0 appl
let explain_unexpected_type env sigma actual_type expected_type =
- let actual_type = Evarutil.nf_evar sigma actual_type in
- let expected_type = Evarutil.nf_evar sigma expected_type in
let pract, prexp = pr_explicit env sigma actual_type expected_type in
str "Found type" ++ spc () ++ pract ++ spc () ++
str "where" ++ spc () ++ prexp ++ str " was expected."
@@ -510,8 +499,6 @@ let explain_ill_formed_rec_body env sigma err names i fixenv vdefj =
with e when CErrors.noncritical e -> mt ())
let explain_ill_typed_rec_body env sigma i names vdefj vargs =
- let vdefj = Evarutil.jv_nf_evar sigma vdefj in
- let vargs = Array.map (Evarutil.nf_evar sigma) vargs in
let env = make_all_name_different env sigma in
let pvd = pr_leconstr_env env sigma vdefj.(i).uj_val in
let pvdt, pv = pr_explicit env sigma vdefj.(i).uj_type vargs.(i) in
@@ -575,9 +562,9 @@ let rec explain_evar_kind env sigma evk ty = function
| Evar_kinds.SubEvar evk' ->
let evi = Evd.find sigma evk' in
let pc = match evi.evar_body with
- | Evar_defined c -> pr_leconstr_env env sigma (Evarutil.nf_evar sigma (EConstr.of_constr c))
+ | Evar_defined c -> pr_leconstr_env env sigma (EConstr.of_constr c)
| Evar_empty -> assert false in
- let ty' = Evarutil.nf_evar sigma (EConstr.of_constr evi.evar_concl) in
+ let ty' = EConstr.of_constr evi.evar_concl in
pr_existential_key sigma evk ++ str " of type " ++ ty ++
str " in the partial instance " ++ pc ++
str " found for " ++ explain_evar_kind env sigma evk'
@@ -628,8 +615,6 @@ let explain_wrong_case_info env (ind,u) ci =
let explain_cannot_unify env sigma m n e =
let env = make_all_name_different env sigma in
- let m = Evarutil.nf_evar sigma m in
- let n = Evarutil.nf_evar sigma n in
let pm, pn = pr_explicit env sigma m n in
let ppreason = explain_unification_error env sigma m n e in
let pe = pr_ne_context_of (str "In environment") env sigma in
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 4b36c2d07..9ab89c883 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -60,7 +60,7 @@ let adjust_guardness_conditions const = function
(* Try all combinations... not optimal *)
let env = Global.env() in
{ const with const_entry_body =
- Future.chain ~pure:true const.const_entry_body
+ Future.chain const.const_entry_body
(fun ((body, ctx), eff) ->
match kind_of_term body with
| Fix ((nv,0),(_,_,fixdefs as fixdecls)) ->
@@ -180,10 +180,14 @@ let save ?export_seff id const cstrs pl do_guard (locality,poly,kind) hook =
try
let const = adjust_guardness_conditions const do_guard in
let k = Kindops.logical_kind_of_goal_kind kind in
+ let should_suggest = const.const_entry_opaque && Option.is_empty const.const_entry_secctx in
let l,r = match locality with
| Discharge when Lib.sections_are_opened () ->
let c = SectionLocalDef const in
let _ = declare_variable id (Lib.cwd(), c, k) in
+ let () = if should_suggest
+ then Proof_using.suggest_variable (Global.env ()) id
+ in
(Local, VarRef id)
| Local | Global | Discharge ->
let local = match locality with
@@ -192,7 +196,11 @@ let save ?export_seff id const cstrs pl do_guard (locality,poly,kind) hook =
in
let kn =
declare_constant ?export_seff id ~local (DefinitionEntry const, k) in
- (locality, ConstRef kn) in
+ let () = if should_suggest
+ then Proof_using.suggest_constant (Global.env ()) kn
+ in
+ (locality, ConstRef kn)
+ in
definition_message id;
Option.iter (Universes.register_universe_binders r) pl;
call_hook (fun exn -> exn) hook l r
@@ -211,7 +219,8 @@ let compute_proof_name locality = function
user_err ?loc (pr_id id ++ str " already exists.");
id
| None ->
- next_global_ident_away default_thm_id (Proof_global.get_all_proof_names ())
+ let avoid = Id.Set.of_list (Proof_global.get_all_proof_names ()) in
+ next_global_ident_away default_thm_id avoid
let save_remaining_recthms (locality,p,kind) norm ctx binders body opaq i (id,(t_i,(_,imps))) =
let t_i = norm t_i in
@@ -309,12 +318,6 @@ let get_proof proof do_guard hook opacity =
in
id,{const with const_entry_opaque = opacity},univs,do_guard,persistence,hook
-let check_exist =
- List.iter (fun (loc,id) ->
- if not (Nametab.exists_cci (Lib.make_path id)) then
- user_err ?loc (pr_id id ++ str " does not exist.")
- )
-
let universe_proof_terminator compute_guard hook =
let open Proof_global in
make_terminator begin function
@@ -322,17 +325,16 @@ let universe_proof_terminator compute_guard hook =
admit (id,k,pe) pl (hook (Some ctx)) ();
Feedback.feedback Feedback.AddedAxiom
| Proved (opaque,idopt,proof) ->
- let is_opaque, export_seff, exports = match opaque with
- | Vernacexpr.Transparent -> false, true, []
- | Vernacexpr.Opaque None -> true, false, []
- | Vernacexpr.Opaque (Some l) -> true, true, l in
+ let is_opaque, export_seff = match opaque with
+ | Vernacexpr.Transparent -> false, true
+ | Vernacexpr.Opaque -> true, false
+ in
let proof = get_proof proof compute_guard
(hook (Some (fst proof.Proof_global.universes))) is_opaque in
begin match idopt with
| None -> save_named ~export_seff proof
| Some (_,id) -> save_anonymous ~export_seff proof id
- end;
- check_exist exports
+ end
end
let standard_proof_terminator compute_guard hook =
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 587c27209..9376afa8c 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -991,7 +991,7 @@ let is_not_printable onlyparse nonreversible = function
(warn_non_reversible_notation (); true)
else onlyparse
-let find_precedence lev etyps symbols =
+let find_precedence lev etyps symbols onlyprint =
let first_symbol =
let rec aux = function
| Break _ :: t -> aux t
@@ -1009,8 +1009,13 @@ let find_precedence lev etyps symbols =
| None -> [],0
| Some (NonTerminal x) ->
(try match List.assoc x etyps with
- | ETConstr _ ->
- user_err Pp.(str "The level of the leftmost non-terminal cannot be changed.")
+ | ETConstr _ ->
+ if onlyprint then
+ if Option.is_empty lev then
+ user_err Pp.(str "Explicit level needed in only-printing mode when the level of the leftmost non-terminal is given.")
+ else [],Option.get lev
+ else
+ user_err Pp.(str "The level of the leftmost non-terminal cannot be changed.")
| ETName | ETBigint | ETReference ->
begin match lev with
| None ->
@@ -1134,7 +1139,7 @@ let compute_syntax_data df modifiers =
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 in
+ let msgs,n = find_precedence mods.level mods.etyps symbols onlyprint in
(* To globalize... *)
let etyps = join_auxiliary_recursive_types recvars mods.etyps in
let sy_typs, prec =
diff --git a/vernac/mltop.ml b/vernac/mltop.ml
index 1edbd1a85..d3de10235 100644
--- a/vernac/mltop.ml
+++ b/vernac/mltop.ml
@@ -174,6 +174,7 @@ let warn_cannot_use_directory =
let convert_string d =
try Names.Id.of_string d
with UserError _ ->
+ let d = Unicode.escaped_if_non_utf8 d in
warn_cannot_use_directory d;
raise Exit
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 128030f68..785c842ba 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -846,9 +846,9 @@ let obligation_terminator name num guard hook auto pf =
let obl = obls.(num) in
let status =
match obl.obl_status, opq with
- | (_, Evar_kinds.Expand), Vernacexpr.Opaque _ -> err_not_transp ()
- | (true, _), Vernacexpr.Opaque _ -> err_not_transp ()
- | (false, _), Vernacexpr.Opaque _ -> Evar_kinds.Define true
+ | (_, Evar_kinds.Expand), Vernacexpr.Opaque -> err_not_transp ()
+ | (true, _), Vernacexpr.Opaque -> err_not_transp ()
+ | (false, _), Vernacexpr.Opaque -> Evar_kinds.Define true
| (_, Evar_kinds.Define true), Vernacexpr.Transparent -> Evar_kinds.Define false
| (_, status), Vernacexpr.Transparent -> status
in
diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml
new file mode 100644
index 000000000..ffe99cfd8
--- /dev/null
+++ b/vernac/proof_using.ml
@@ -0,0 +1,190 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Names
+open Environ
+open Util
+open Vernacexpr
+open Context.Named.Declaration
+
+module NamedDecl = Context.Named.Declaration
+
+let known_names = Summary.ref [] ~name:"proofusing-nameset"
+
+let in_nameset =
+ let open Libobject in
+ declare_object { (default_object "proofusing-nameset") with
+ cache_function = (fun (_,x) -> known_names := x :: !known_names);
+ classify_function = (fun _ -> Dispose);
+ discharge_function = (fun _ -> None)
+ }
+
+let rec close_fwd e s =
+ let s' =
+ List.fold_left (fun s decl ->
+ let vb = match decl with
+ | LocalAssum _ -> Id.Set.empty
+ | LocalDef (_,b,_) -> global_vars_set e b
+ in
+ let vty = global_vars_set e (NamedDecl.get_type decl) in
+ let vbty = Id.Set.union vb vty in
+ if Id.Set.exists (fun v -> Id.Set.mem v s) vbty
+ then Id.Set.add (NamedDecl.get_id decl) (Id.Set.union s vbty) else s)
+ s (named_context e)
+ in
+ if Id.Set.equal s s' then s else close_fwd e s'
+
+let set_of_type env ty =
+ List.fold_left (fun acc ty ->
+ Id.Set.union (global_vars_set env ty) acc)
+ Id.Set.empty ty
+
+let full_set env =
+ List.fold_right Id.Set.add (List.map NamedDecl.get_id (named_context env)) Id.Set.empty
+
+let rec process_expr env e ty =
+ let rec aux = function
+ | SsEmpty -> Id.Set.empty
+ | SsType -> set_of_type env ty
+ | SsSingl (_,id) -> set_of_id env id
+ | SsUnion(e1,e2) -> Id.Set.union (aux e1) (aux e2)
+ | SsSubstr(e1,e2) -> Id.Set.diff (aux e1) (aux e2)
+ | SsCompl e -> Id.Set.diff (full_set env) (aux e)
+ | SsFwdClose e -> close_fwd env (aux e)
+ in
+ aux e
+
+and set_of_id env id =
+ if Id.to_string id = "All" then
+ List.fold_right Id.Set.add (List.map NamedDecl.get_id (named_context env)) Id.Set.empty
+ else if CList.mem_assoc_f Id.equal id !known_names then
+ process_expr env (CList.assoc_f Id.equal id !known_names) []
+ else Id.Set.singleton id
+
+let process_expr env e ty =
+ let v_ty = set_of_type env ty in
+ let s = Id.Set.union v_ty (process_expr env e ty) in
+ Id.Set.elements s
+
+let name_set id expr = Lib.add_anonymous_leaf (in_nameset (id,expr))
+
+let minimize_hyps env ids =
+ let rec aux ids =
+ let ids' =
+ Id.Set.fold (fun id alive ->
+ let impl_by_id =
+ Id.Set.remove id (really_needed env (Id.Set.singleton id)) in
+ if Id.Set.is_empty impl_by_id then alive
+ else Id.Set.diff alive impl_by_id)
+ ids ids in
+ if Id.Set.equal ids ids' then ids else aux ids'
+ in
+ aux ids
+
+let remove_ids_and_lets env s ids =
+ let not_ids id = not (Id.Set.mem id ids) in
+ let no_body id = named_body id env = None in
+ let deps id = really_needed env (Id.Set.singleton id) in
+ (Id.Set.filter (fun id ->
+ not_ids id &&
+ (no_body id ||
+ Id.Set.exists not_ids (Id.Set.filter no_body (deps id)))) s)
+
+let record_proof_using expr =
+ Aux_file.record_in_aux "suggest_proof_using" expr
+
+(* Variables in [skip] come from after the definition, so don't count
+ for "All". Used in the variable case since the env contains the
+ variable itself. *)
+let suggest_common env ppid used ids_typ skip =
+ let module S = Id.Set in
+ let open Pp in
+ let print x = Feedback.msg_debug x in
+ let pr_set parens s =
+ let wrap ppcmds =
+ if parens && S.cardinal s > 1 then str "(" ++ ppcmds ++ str ")"
+ else ppcmds in
+ wrap (prlist_with_sep (fun _ -> str" ") Id.print (S.elements s)) in
+
+ let needed = minimize_hyps env (remove_ids_and_lets env used ids_typ) in
+ let all_needed = really_needed env needed in
+ let all = List.fold_left (fun all d -> S.add (NamedDecl.get_id d) all)
+ S.empty (named_context env)
+ in
+ let all = S.diff all skip in
+ let fwd_typ = close_fwd env ids_typ in
+ if !Flags.debug then begin
+ print (str "All " ++ pr_set false all);
+ print (str "Type " ++ pr_set false ids_typ);
+ print (str "needed " ++ pr_set false needed);
+ print (str "all_needed " ++ pr_set false all_needed);
+ print (str "Type* " ++ pr_set false fwd_typ);
+ end;
+ let valid_exprs = ref [] in
+ let valid e = valid_exprs := e :: !valid_exprs in
+ if S.is_empty needed then valid (str "Type");
+ if S.equal all_needed fwd_typ then valid (str "Type*");
+ if S.equal all all_needed then valid(str "All");
+ valid (pr_set false needed);
+ Feedback.msg_info (
+ str"The proof of "++ ppid ++ spc() ++
+ str "should start with one of the following commands:"++spc()++
+ v 0 (
+ prlist_with_sep cut (fun x->str"Proof using " ++x++ str". ") !valid_exprs));
+ if !Flags.record_aux_file
+ then
+ let s = string_of_ppcmds (prlist_with_sep (fun _ -> str";") (fun x->x) !valid_exprs) in
+ record_proof_using s
+
+let suggest_proof_using = ref false
+
+let _ =
+ Goptions.declare_bool_option
+ { Goptions.optdepr = false;
+ Goptions.optname = "suggest Proof using";
+ Goptions.optkey = ["Suggest";"Proof";"Using"];
+ Goptions.optread = (fun () -> !suggest_proof_using);
+ Goptions.optwrite = ((:=) suggest_proof_using) }
+
+let suggest_constant env kn =
+ if !suggest_proof_using
+ then begin
+ let open Declarations in
+ let body = lookup_constant kn env in
+ let used = Id.Set.of_list @@ List.map NamedDecl.get_id body.const_hyps in
+ let ids_typ = global_vars_set env body.const_type in
+ suggest_common env (Printer.pr_constant env kn) used ids_typ Id.Set.empty
+ end
+
+let suggest_variable env id =
+ if !suggest_proof_using
+ then begin
+ match lookup_named id env with
+ | LocalDef (_,body,typ) ->
+ let ids_typ = global_vars_set env typ in
+ let ids_body = global_vars_set env body in
+ let used = Id.Set.union ids_body ids_typ in
+ suggest_common env (Id.print id) used ids_typ (Id.Set.singleton id)
+ | LocalAssum _ -> assert false
+ end
+
+let value = ref None
+
+let using_to_string us = Pp.string_of_ppcmds (Ppvernac.pr_using us)
+let using_from_string us = Pcoq.Gram.(entry_parse G_vernac.section_subset_expr (parsable (Stream.of_string us)))
+
+let _ =
+ Goptions.declare_stringopt_option
+ { Goptions.optdepr = false;
+ Goptions.optname = "default value for Proof using";
+ Goptions.optkey = ["Default";"Proof";"Using"];
+ Goptions.optread = (fun () -> Option.map using_to_string !value);
+ Goptions.optwrite = (fun b -> value := Option.map using_from_string b);
+ }
+
+let get_default_proof_using () = !value
diff --git a/vernac/discharge.mli b/vernac/proof_using.mli
index c8c7e3b8b..f63c8e242 100644
--- a/vernac/discharge.mli
+++ b/vernac/proof_using.mli
@@ -6,9 +6,16 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Declarations
-open Entries
-open Opaqueproof
+(** Utility code for section variables handling in Proof using... *)
-val process_inductive :
- Lib.abstr_info -> work_list -> mutual_inductive_body -> mutual_inductive_entry
+val process_expr :
+ Environ.env -> Vernacexpr.section_subset_expr -> Constr.types list ->
+ Names.Id.t list
+
+val name_set : Names.Id.t -> Vernacexpr.section_subset_expr -> unit
+
+val suggest_constant : Environ.env -> Names.Constant.t -> unit
+
+val suggest_variable : Environ.env -> Names.Id.t -> unit
+
+val get_default_proof_using : unit -> Vernacexpr.section_subset_expr option
diff --git a/vernac/record.ml b/vernac/record.ml
index bf32cb6e6..9a8657c3c 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -457,7 +457,7 @@ let declare_class finite def cum poly ctx id idbuild paramimpls params arity
let impls = implicits_of_context params in
List.map (fun x -> impls @ Impargs.lift_implicits (succ len) x) fieldimpls
in
- let binder_name = Namegen.next_ident_away (snd id) (Termops.ids_of_context (Global.env())) in
+ let binder_name = Namegen.next_ident_away (snd id) (Termops.vars_of_env (Global.env())) in
let impl, projs =
match fields with
| [LocalAssum (Name proj_name, field) | LocalDef (Name proj_name, _, field)] when def ->
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index f74073e1f..850902d6b 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -1,4 +1,5 @@
Vernacprop
+Proof_using
Lemmas
Himsg
ExplainErr
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index f05ceb194..e08cb8387 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -125,8 +125,8 @@ let make_cases_aux glob_ref =
| [] -> []
| (n,_)::l ->
let n' = Namegen.next_name_away_with_default (Id.to_string Namegen.default_dependent_ident) n avoid in
- Id.to_string n' :: rename (n'::avoid) l in
- let al' = rename [] al in
+ Id.to_string n' :: rename (Id.Set.add n' avoid) l in
+ let al' = rename Id.Set.empty al in
let consref = ConstructRef (ith_constructor_of_inductive ind (i + 1)) in
(Libnames.string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty consref) :: al') :: l)
tarr []
@@ -507,7 +507,7 @@ let vernac_exact_proof c =
(* spiwack: for simplicity I do not enforce that "Proof proof_term" is
called only at the begining of a proof. *)
let status = Pfedit.by (Tactics.exact_proof c) in
- save_proof (Vernacexpr.(Proved(Opaque None,None)));
+ save_proof (Vernacexpr.(Proved(Opaque,None)));
if not status then Feedback.feedback Feedback.AddedAxiom
let vernac_assumption locality poly (local, kind) l nl =
@@ -1230,7 +1230,7 @@ let vernac_reserve bl =
let env = Global.env() in
let sigma = Evd.from_env env in
let t,ctx = Constrintern.interp_type env sigma c in
- let t = Detyping.detype Detyping.Now false [] env (Evd.from_ctx ctx) (EConstr.of_constr t) in
+ let t = Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_ctx ctx) (EConstr.of_constr t) in
let t,_ = Notation_ops.notation_constr_of_glob_constr (default_env ()) t in
Reserve.declare_reserved_type idl t)
in List.iter sb_decl bl
@@ -1785,7 +1785,7 @@ let vernac_locate = let open Feedback in function
(Constrextern.without_symbols pr_lglob_constr) ntn sc)
| LocateLibrary qid -> print_located_library qid
| LocateModule qid -> msg_notice (print_located_module qid)
- | LocateTactic qid -> msg_notice (print_located_tactic qid)
+ | LocateOther (s, qid) -> msg_notice (print_located_other s qid)
| LocateFile f -> msg_notice (locate_file f)
let vernac_register id r =
@@ -2060,17 +2060,13 @@ let interp ?proof ?loc locality poly c =
| VernacEndSubproof -> vernac_end_subproof ()
| VernacShow s -> vernac_show s
| VernacCheckGuard -> vernac_check_guard ()
- | VernacProof (None, None) ->
- Aux_file.record_in_aux_at ?loc "VernacProof" "tac:no using:no"
- | VernacProof (Some tac, None) ->
- Aux_file.record_in_aux_at ?loc "VernacProof" "tac:yes using:no";
- vernac_set_end_tac tac
- | VernacProof (None, Some l) ->
- Aux_file.record_in_aux_at ?loc "VernacProof" "tac:no using:yes";
- vernac_set_used_variables l
- | VernacProof (Some tac, Some l) ->
- Aux_file.record_in_aux_at ?loc "VernacProof" "tac:yes using:yes";
- vernac_set_end_tac tac; vernac_set_used_variables l
+ | VernacProof (tac, using) ->
+ let using = Option.append using (Proof_using.get_default_proof_using ()) in
+ let tacs = if Option.is_empty tac then "tac:no" else "tac:yes" in
+ let usings = if Option.is_empty using then "using:no" else "using:yes" in
+ Aux_file.record_in_aux_at ?loc "VernacProof" (tacs^" "^usings);
+ Option.iter vernac_set_end_tac tac;
+ Option.iter vernac_set_used_variables using
| VernacProofMode mn -> Proof_global.set_proof_mode mn [@ocaml.warning "-3"]
(* Extensions *)
@@ -2152,23 +2148,48 @@ let locate_if_not_already ?loc (e, info) =
exception HasNotFailed
exception HasFailed of Pp.t
-let with_fail b f =
- if not b then f ()
+type interp_state = { (* TODO: inline records in OCaml 4.03 *)
+ system : States.state; (* summary + libstack *)
+ proof : Proof_global.state; (* proof state *)
+ shallow : bool (* is the state trimmed down (libstack) *)
+}
+
+let s_cache = ref (States.freeze ~marshallable:`No)
+let s_proof = ref (Proof_global.freeze ~marshallable:`No)
+
+let invalidate_cache () =
+ s_cache := Obj.magic 0;
+ s_proof := Obj.magic 0
+
+let freeze_interp_state marshallable =
+ { system = (s_cache := States.freeze ~marshallable; !s_cache);
+ proof = (s_proof := Proof_global.freeze ~marshallable; !s_proof);
+ shallow = marshallable = `Shallow }
+
+let unfreeze_interp_state { system; proof } =
+ if (!s_cache != system) then (s_cache := system; States.unfreeze system);
+ if (!s_proof != proof) then (s_proof := proof; Proof_global.unfreeze proof)
+
+(* XXX STATE: this type hints that restoring the state should be the
+ caller's responsibility *)
+let with_fail st b f =
+ if not b
+ then f ()
else begin try
(* If the command actually works, ignore its effects on the state.
* Note that error has to be printed in the right state, hence
* within the purified function *)
- Future.purify
- (fun v ->
- try f v; raise HasNotFailed
- with
- | HasNotFailed as e -> raise e
- | e ->
- let e = CErrors.push e in
- raise (HasFailed (CErrors.iprint
- (ExplainErr.process_vernac_interp_error ~allow_uncaught:false e))))
- ()
+ try f (); raise HasNotFailed
+ with
+ | HasNotFailed as e -> raise e
+ | e ->
+ let e = CErrors.push e in
+ raise (HasFailed (CErrors.iprint
+ (ExplainErr.process_vernac_interp_error ~allow_uncaught:false e)))
with e when CErrors.noncritical e ->
+ (* Restore the previous state XXX Careful here with the cache! *)
+ invalidate_cache ();
+ unfreeze_interp_state st;
let (e, _) = CErrors.push e in
match e with
| HasNotFailed ->
@@ -2179,7 +2200,7 @@ let with_fail b f =
| _ -> assert false
end
-let interp ?(verbosely=true) ?proof (loc,c) =
+let interp ?(verbosely=true) ?proof st (loc,c) =
let orig_program_mode = Flags.is_program_mode () in
let rec aux ?locality ?polymorphism isprogcmd = function
@@ -2192,7 +2213,7 @@ let interp ?(verbosely=true) ?proof (loc,c) =
| VernacPolymorphic (b, c) -> user_err Pp.(str "Polymorphism specified twice")
| VernacLocal _ -> user_err Pp.(str "Locality specified twice")
| VernacFail v ->
- with_fail true (fun () -> aux ?locality ?polymorphism isprogcmd v)
+ with_fail st true (fun () -> aux ?locality ?polymorphism isprogcmd v)
| VernacTimeout (n,v) ->
current_timeout := Some n;
aux ?locality ?polymorphism isprogcmd v
@@ -2231,3 +2252,8 @@ let interp ?(verbosely=true) ?proof (loc,c) =
in
if verbosely then Flags.verbosely (aux false) c
else aux false c
+
+let interp ?verbosely ?proof st cmd =
+ unfreeze_interp_state st;
+ interp ?verbosely ?proof st cmd;
+ freeze_interp_state `No
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index a09011d24..56635c801 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -14,11 +14,21 @@ val dump_global : Libnames.reference or_by_notation -> unit
val vernac_require :
Libnames.reference option -> bool option -> Libnames.reference list -> unit
+type interp_state = { (* TODO: inline records in OCaml 4.03 *)
+ system : States.state; (* summary + libstack *)
+ proof : Proof_global.state; (* proof state *)
+ shallow : bool (* is the state trimmed down (libstack) *)
+}
+
+val freeze_interp_state : Summary.marshallable -> interp_state
+val unfreeze_interp_state : interp_state -> unit
+
(** The main interpretation function of vernacular expressions *)
val interp :
?verbosely:bool ->
?proof:Proof_global.closed_proof ->
- Vernacexpr.vernac_expr Loc.located -> unit
+ interp_state ->
+ Vernacexpr.vernac_expr Loc.located -> interp_state
(** Prepare a "match" template for a given inductive type.
For each branch of the match, we list the constructor name
@@ -28,7 +38,9 @@ val interp :
val make_cases : string -> string list list
-val with_fail : bool -> (unit -> unit) -> unit
+(* XXX STATE: this type hints that restoring the state should be the
+ caller's responsibility *)
+val with_fail : interp_state -> bool -> (unit -> unit) -> unit
val command_focus : unit Proof.focus_kind
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-20 03:16:56 +0000