aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/refman/RefMan-pro.tex30
-rw-r--r--intf/vernacexpr.mli10
-rw-r--r--kernel/term_typing.ml35
-rw-r--r--kernel/term_typing.mli2
-rw-r--r--parsing/g_proofs.ml48
-rw-r--r--parsing/g_vernac.ml450
-rw-r--r--proofs/pfedit.mli3
-rw-r--r--proofs/proof_global.ml28
-rw-r--r--proofs/proof_global.mli6
-rw-r--r--proofs/proof_using.ml172
-rw-r--r--proofs/proof_using.mli15
-rw-r--r--stm/stm.ml13
-rw-r--r--test-suite/success/proof_using.v76
-rw-r--r--toplevel/vernacentries.ml13
14 files changed, 301 insertions, 160 deletions
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index 7af87a399..5dbf31553 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -157,6 +157,14 @@ in Section~\ref{ProofWith}.
Use only section variables occurring in the statement.
+\variant {\tt Proof using Type*.}
+
+ The {\tt *} operator computes the forward transitive closure.
+ E.g. if the variable {\tt H} has type {\tt p < 5} then {\tt H} is
+ in {\tt p*} since {\tt p} occurs in the type of {\tt H}.
+ {\tt Type* } is the forward transitive closure of the entire set of
+ section variables occurring in the statement.
+
\variant {\tt Proof using -(} {\ident$_1$} {\ldots} {\ident$_n$} {\tt ).}
Use all section variables except {\ident$_1$} {\ldots} {\ident$_n$}.
@@ -164,14 +172,18 @@ in Section~\ref{ProofWith}.
\variant {\tt Proof using } {\emph collection$_1$} {\tt + } {\emph collection$_2$} {\tt .}
\variant {\tt Proof using } {\emph collection$_1$} {\tt - } {\emph collection$_2$} {\tt .}
\variant {\tt Proof using } {\emph collection$_1$} {\tt - (} {\ident$_1$} {\ldots} {\ident$_n$} {\tt ).}
+\variant {\tt Proof using } {\emph collection$_1$}{\tt* .}
- Use section variables being in the set union or set difference of the two
- colelctions. See Section~\ref{Collection} to know how to form a named
+ Use section variables being, respectively, in the set union, set difference,
+ set complement, set forward transitive closure.
+ See Section~\ref{Collection} to know how to form a named
collection.
+ The {\tt *} operator binds stronger than {\tt +} and {\tt -}.
\subsubsection{{\tt Proof using} options}
-\comindex{Default Proof Using}
-\comindex{Suggest Proof Using}
+\optindex{Default Proof Using}
+\optindex{Suggest Proof Using}
+\optindex{Proof Using Clear Unused}
The following options modify the behavior of {\tt Proof using}.
@@ -186,11 +198,17 @@ The following options modify the behavior of {\tt Proof using}.
When {\tt Qed} is performed, suggest a {\tt using} annotation if
the user did not provide one.
+\variant{\tt Unset Proof Using Clear Unused.}
+
+ When {\tt Proof using a} all section variables but for {\tt a} and
+ the variables used in the type of {\tt a} are cleared.
+ This option can be used to turn off this behavior.
+
\subsubsection[\tt Collection]{Name a set of section hypotheses for {\tt Proof using}}
\comindex{Collection}\label{Collection}
The command {\tt Collection} can be used to name a set of section hypotheses,
-with the purpose of making {\tt Proof using} annotations more compat.
+with the purpose of making {\tt Proof using} annotations more compact.
\variant {\tt Collection Some := x y z.}
@@ -209,7 +227,7 @@ with the purpose of making {\tt Proof using} annotations more compat.
\variant {\tt Collection Many := Fewer - (x y).}
Define the collection named "Many" containing the set difference
- of "Fewer" and the unamed collection {\tt x y}.
+ of "Fewer" and the unnamed collection {\tt x y}.
\subsection[\tt Abort.]{\tt Abort.\comindex{Abort}}
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 9248fa953..fd6e1c6ae 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -225,12 +225,12 @@ type scheme =
| EqualityScheme of reference or_by_notation
type section_subset_expr =
- | SsSet of lident list
+ | SsEmpty
+ | SsSingl of lident
| SsCompl of section_subset_expr
| SsUnion of section_subset_expr * section_subset_expr
| SsSubstr of section_subset_expr * section_subset_expr
-
-type section_subset_descr = SsAll | SsType | SsExpr of section_subset_expr
+ | SsFwdClose of section_subset_expr
(** Extension identifiers for the VERNAC EXTEND mechanism. *)
type extend_name =
@@ -336,7 +336,7 @@ type vernac_expr =
class_rawexpr * class_rawexpr
| VernacIdentityCoercion of obsolete_locality * lident *
class_rawexpr * class_rawexpr
- | VernacNameSectionHypSet of lident * section_subset_descr
+ | VernacNameSectionHypSet of lident * section_subset_expr
(* Type classes *)
| VernacInstance of
@@ -441,7 +441,7 @@ type vernac_expr =
| VernacEndSubproof
| VernacShow of showable
| VernacCheckGuard
- | VernacProof of raw_tactic_expr option * section_subset_descr option
+ | VernacProof of raw_tactic_expr option * section_subset_expr option
| VernacProofMode of string
(* Toplevel control *)
| VernacToplevelControl of exn
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 8eb920fb7..b6df8f454 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -182,14 +182,17 @@ let global_vars_set_constant_type env = function
(fun t c -> Id.Set.union (global_vars_set env t) c))
ctx ~init:Id.Set.empty
-let record_aux env s1 s2 =
+let record_aux env s_ty s_bo suggested_expr =
+ let in_ty = keep_hyps env s_ty in
let v =
String.concat " "
- (List.map (fun (id, _,_) -> Id.to_string id)
- (keep_hyps env (Id.Set.union s1 s2))) in
- Aux_file.record_in_aux "context_used" v
+ (CList.map_filter (fun (id, _,_) ->
+ if List.exists (fun (id',_,_) -> Id.equal id id') in_ty then None
+ else Some (Id.to_string id))
+ (keep_hyps env s_bo)) in
+ Aux_file.record_in_aux "context_used" (v ^ ";" ^ suggested_expr)
-let suggest_proof_using = ref (fun _ _ _ _ _ -> ())
+let suggest_proof_using = ref (fun _ _ _ _ _ -> "")
let set_suggest_proof_using f = suggest_proof_using := f
let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) =
@@ -225,15 +228,17 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
(Opaqueproof.force_proof (opaque_tables env) lc) in
(* we force so that cst are added to the env immediately after *)
ignore(Opaqueproof.force_constraints (opaque_tables env) lc);
- !suggest_proof_using kn env vars ids_typ context_ids;
+ let expr =
+ !suggest_proof_using (Constant.to_string kn)
+ env vars ids_typ context_ids in
if !Flags.compilation_mode = Flags.BuildVo then
- record_aux env ids_typ vars;
+ record_aux env ids_typ vars expr;
vars
in
keep_hyps env (Idset.union ids_typ ids_def), def
| None ->
if !Flags.compilation_mode = Flags.BuildVo then
- record_aux env Id.Set.empty Id.Set.empty;
+ record_aux env Id.Set.empty Id.Set.empty "";
[], def (* Empty section context: no need to check *)
| Some declared ->
(* We use the declared set and chain a check of correctness *)
@@ -307,6 +312,20 @@ let translate_local_def env id centry =
let def,typ,proj,poly,univs,inline_code,ctx =
infer_declaration env None (DefinitionEntry centry) in
let typ = type_of_constant_type env typ in
+ if ctx = None && !Flags.compilation_mode = Flags.BuildVo then begin
+ match def with
+ | Undef _ -> ()
+ | Def _ -> ()
+ | OpaqueDef lc ->
+ let context_ids = List.map pi1 (named_context env) in
+ let ids_typ = global_vars_set env typ in
+ let ids_def = global_vars_set env
+ (Opaqueproof.force_proof (opaque_tables env) lc) in
+ let expr =
+ !suggest_proof_using (Id.to_string id)
+ env ids_def ids_typ context_ids in
+ record_aux env ids_typ ids_def expr
+ end;
def, typ, univs
(* Insertion of inductive types. *)
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 1b54b1ea1..8d92bcc68 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -44,4 +44,4 @@ val build_constant_declaration :
constant -> env -> Cooking.result -> constant_body
val set_suggest_proof_using :
- (constant -> env -> Id.Set.t -> Id.Set.t -> Id.t list -> unit) -> unit
+ (string -> env -> Id.Set.t -> Id.Set.t -> Id.t list -> string) -> unit
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 1e254c16b..7f5459bfa 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -37,12 +37,12 @@ GEXTEND Gram
command:
[ [ IDENT "Goal"; c = lconstr -> VernacGoal c
| IDENT "Proof" ->
- VernacProof (None,hint_proof_using G_vernac.section_subset_descr None)
+ VernacProof (None,hint_proof_using G_vernac.section_subset_expr None)
| IDENT "Proof" ; IDENT "Mode" ; mn = string -> VernacProofMode mn
| IDENT "Proof"; "with"; ta = tactic;
- l = OPT [ "using"; l = G_vernac.section_subset_descr -> l ] ->
- VernacProof (Some ta,hint_proof_using G_vernac.section_subset_descr l)
- | IDENT "Proof"; "using"; l = G_vernac.section_subset_descr;
+ l = OPT [ "using"; l = G_vernac.section_subset_expr -> l ] ->
+ VernacProof (Some ta,hint_proof_using G_vernac.section_subset_expr l)
+ | IDENT "Proof"; "using"; l = G_vernac.section_subset_expr;
ta = OPT [ "with"; ta = tactic -> ta ] ->
VernacProof (ta,Some l)
| IDENT "Proof"; c = lconstr -> VernacExactProof c
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index e9915fceb..fc0a4c8c3 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -46,7 +46,7 @@ let record_field = Gram.entry_create "vernac:record_field"
let of_type_with_opt_coercion = Gram.entry_create "vernac:of_type_with_opt_coercion"
let subgoal_command = Gram.entry_create "proof_mode:subgoal_command"
let instance_name = Gram.entry_create "vernac:instance_name"
-let section_subset_descr = Gram.entry_create "vernac:section_subset_descr"
+let section_subset_expr = Gram.entry_create "vernac:section_subset_expr"
let command_entry = ref noedit_mode
let set_command_entry e = command_entry := e
@@ -447,20 +447,24 @@ GEXTEND Gram
;
END
-let only_identrefs =
- Gram.Entry.of_parser "test_only_identrefs"
+let only_starredidentrefs =
+ Gram.Entry.of_parser "test_only_starredidentrefs"
(fun strm ->
let rec aux n =
match get_tok (Util.stream_nth n strm) with
| KEYWORD "." -> ()
| KEYWORD ")" -> ()
- | IDENT _ -> aux (n+1)
+ | (IDENT _ | KEYWORD "Type" | KEYWORD "*") -> aux (n+1)
| _ -> raise Stream.Failure in
aux 0)
+let starredidentreflist_to_expr l =
+ match l with
+ | [] -> SsEmpty
+ | x :: xs -> List.fold_right (fun i acc -> SsUnion(i,acc)) xs x
(* Modules and Sections *)
GEXTEND Gram
- GLOBAL: gallina_ext module_expr module_type section_subset_descr;
+ GLOBAL: gallina_ext module_expr module_type section_subset_expr;
gallina_ext:
[ [ (* Interactive module declaration *)
@@ -483,7 +487,7 @@ GEXTEND Gram
| IDENT "End"; id = identref -> VernacEndSegment id
(* Naming a set of section hyps *)
- | IDENT "Collection"; id = identref; ":="; expr = section_subset_descr ->
+ | IDENT "Collection"; id = identref; ":="; expr = section_subset_expr ->
VernacNameSectionHypSet (id, expr)
(* Requiring an already compiled module *)
@@ -574,22 +578,32 @@ GEXTEND Gram
CMwith (!@loc,mty,decl)
] ]
;
- section_subset_descr:
- [ [ IDENT "All" -> SsAll
- | "Type" -> SsType
- | only_identrefs; l = LIST0 identref -> SsExpr (SsSet l)
- | e = section_subset_expr -> SsExpr e ] ]
- ;
+ (* Proof using *)
section_subset_expr:
+ [ [ only_starredidentrefs; l = LIST0 starredidentref ->
+ starredidentreflist_to_expr l
+ | e = ssexpr -> e ]]
+ ;
+ starredidentref:
+ [ [ i = identref -> SsSingl i
+ | i = identref; "*" -> SsFwdClose(SsSingl i)
+ | "Type" -> SsSingl (!@loc, Id.of_string "Type")
+ | "Type"; "*" -> SsFwdClose (SsSingl (!@loc, Id.of_string "Type")) ]]
+ ;
+ ssexpr:
[ "35"
- [ "-"; e = section_subset_expr -> SsCompl e ]
+ [ "-"; e = ssexpr -> SsCompl e ]
| "50"
- [ e1 = section_subset_expr; "-"; e2 = section_subset_expr->SsSubstr(e1,e2)
- | e1 = section_subset_expr; "+"; e2 = section_subset_expr->SsUnion(e1,e2)]
+ [ e1 = ssexpr; "-"; e2 = ssexpr->SsSubstr(e1,e2)
+ | e1 = ssexpr; "+"; e2 = ssexpr->SsUnion(e1,e2)]
| "0"
- [ i = identref -> SsSet [i]
- | "("; only_identrefs; l = LIST0 identref; ")"-> SsSet l
- | "("; e = section_subset_expr; ")"-> e ] ]
+ [ i = starredidentref -> i
+ | "("; only_starredidentrefs; l = LIST0 starredidentref; ")"->
+ starredidentreflist_to_expr l
+ | "("; only_starredidentrefs; l = LIST0 starredidentref; ")"; "*" ->
+ SsFwdClose(starredidentreflist_to_expr l)
+ | "("; e = ssexpr; ")"-> e
+ | "("; e = ssexpr; ")"; "*" -> SsFwdClose e ] ]
;
END
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 4aa3c3bfd..b1fba132d 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -117,7 +117,8 @@ val set_end_tac : Tacexpr.raw_tactic_expr -> unit
(** {6 ... } *)
(** [set_used_variables l] declares that section variables [l] will be
used in the proof *)
-val set_used_variables : Id.t list -> Context.section_context
+val set_used_variables :
+ Id.t list -> Context.section_context * (Loc.t * Names.Id.t) list
val get_used_variables : unit -> Context.section_context option
(** {6 ... } *)
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 254aa8f78..f777e6ed7 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -250,17 +250,43 @@ let start_dependent_proof id str goals terminator =
let get_used_variables () = (cur_pstate ()).section_vars
+let proof_using_auto_clear = ref true
+let _ = Goptions.declare_bool_option
+ { Goptions.optsync = true;
+ Goptions.optdepr = false;
+ Goptions.optname = "Proof using Clear Unused";
+ Goptions.optkey = ["Proof";"Using";"Clear";"Unused"];
+ Goptions.optread = (fun () -> !proof_using_auto_clear);
+ Goptions.optwrite = (fun b -> proof_using_auto_clear := b) }
+
let set_used_variables l =
let env = Global.env () in
let ids = List.fold_right Id.Set.add l Id.Set.empty in
let ctx = Environ.keep_hyps env ids in
+ let ctx_set =
+ List.fold_right Id.Set.add (List.map pi1 ctx) Id.Set.empty in
+ let vars_of = Environ.global_vars_set in
+ let aux env entry (ctx, all_safe, to_clear as orig) =
+ match entry with
+ | (x,None,_) ->
+ if Id.Set.mem x all_safe then orig
+ else (ctx, all_safe, (Loc.ghost,x)::to_clear)
+ | (x,Some bo, ty) as decl ->
+ if Id.Set.mem x all_safe then orig else
+ let vars = Id.Set.union (vars_of env bo) (vars_of env ty) in
+ if Id.Set.subset vars all_safe
+ then (decl :: ctx, Id.Set.add x all_safe, to_clear)
+ else (ctx, all_safe, (Loc.ghost,x) :: to_clear) in
+ let ctx, _, to_clear =
+ Environ.fold_named_context aux env ~init:(ctx,ctx_set,[]) in
+ let to_clear = if !proof_using_auto_clear then to_clear else [] in
match !pstates with
| [] -> raise NoCurrentProof
| p :: rest ->
if not (Option.is_empty p.section_vars) then
Errors.error "Used section variables can be declared only once";
pstates := { p with section_vars = Some ctx} :: rest;
- ctx
+ ctx, to_clear
let get_open_goals () =
let gl, gll, shelf , _ , _ = Proof.proof (cur_pstate ()).proof in
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index b5dd5ef85..028116049 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -129,8 +129,10 @@ val set_interp_tac :
-> unit
(** Sets the section variables assumed by the proof, returns its closure
- * (w.r.t. type dependencies *)
-val set_used_variables : Names.Id.t list -> Context.section_context
+ * (w.r.t. type dependencies and let-ins covered by it) + a list of
+ * ids to be cleared *)
+val set_used_variables :
+ Names.Id.t list -> Context.section_context * (Loc.t * Names.Id.t) list
val get_used_variables : unit -> Context.section_context option
(**********************************************************)
diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml
index f66e96571..7eed1cb31 100644
--- a/proofs/proof_using.ml
+++ b/proofs/proof_using.ml
@@ -11,20 +11,15 @@ open Environ
open Util
open Vernacexpr
-let to_string = function
- | SsAll -> "All"
- | SsType -> "Type"
- | SsExpr(SsSet l)-> String.concat " " (List.map Id.to_string (List.map snd l))
- | SsExpr e ->
- let rec aux = function
- | SsSet [] -> "( )"
- | SsSet [_,x] -> Id.to_string x
- | SsSet l ->
- "(" ^ String.concat " " (List.map Id.to_string (List.map snd l)) ^ ")"
- | SsCompl e -> "-" ^ aux e^""
- | SsUnion(e1,e2) -> "("^aux e1 ^" + "^ aux e2^")"
- | SsSubstr(e1,e2) -> "("^aux e1 ^" - "^ aux e2^")"
- in aux e
+let to_string e =
+ let rec aux = function
+ | SsEmpty -> "()"
+ | SsSingl (_,id) -> "("^Id.to_string id^")"
+ | SsCompl e -> "-" ^ aux e^""
+ | SsUnion(e1,e2) -> "("^aux e1 ^" + "^ aux e2^")"
+ | SsSubstr(e1,e2) -> "("^aux e1 ^" - "^ aux e2^")"
+ | SsFwdClose e -> "("^aux e^")*"
+ in aux e
let known_names = Summary.ref [] ~name:"proofusing-nameset"
@@ -36,30 +31,48 @@ let in_nameset =
discharge_function = (fun _ -> None)
}
+let rec close_fwd e s =
+ let s' =
+ List.fold_left (fun s (id,b,ty) ->
+ let vb = Option.(default Id.Set.empty (map (global_vars_set e) b)) in
+ let vty = global_vars_set e ty 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 id (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 rec process_expr env e ty =
- match e with
- | SsAll ->
- List.fold_right Id.Set.add (List.map pi1 (named_context env)) Id.Set.empty
- | SsExpr e ->
- let rec aux = function
- | SsSet l -> set_of_list env (List.map snd l)
- | 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)
- in
- aux e
- | SsType ->
- List.fold_left (fun acc ty ->
+ let rec aux = function
+ | SsEmpty -> Id.Set.empty
+ | SsSingl (_,id) -> set_of_id env ty 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 ty id =
+ if Id.to_string id = "Type" then
+ List.fold_left (fun acc ty ->
Id.Set.union (global_vars_set env ty) acc)
Id.Set.empty ty
-and set_of_list env = function
- | [x] when CList.mem_assoc_f Id.equal x !known_names ->
- process_expr env (CList.assoc_f Id.equal x !known_names) []
- | l -> List.fold_right Id.Set.add l Id.Set.empty
-and full_set env = set_of_list env (List.map pi1 (named_context env))
+ else if Id.to_string id = "All" then
+ List.fold_right Id.Set.add (List.map pi1 (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
+
+and full_set env =
+ List.fold_right Id.Set.add (List.map pi1 (named_context env)) Id.Set.empty
let process_expr env e ty =
- let s = Id.Set.union (process_expr env SsType ty) (process_expr env e []) in
+ let ty_expr = SsSingl(Loc.ghost, Id.of_string "Type") in
+ let v_ty = process_expr env ty_expr 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))
@@ -77,62 +90,49 @@ let minimize_hyps env ids =
in
aux ids
-let minimize_unused_hyps env ids =
- let all_ids = List.map pi1 (named_context env) in
- let deps_of =
- let cache =
- List.map (fun id -> id,really_needed env (Id.Set.singleton id)) all_ids in
- fun id -> List.assoc id cache in
- let inv_dep_of =
- let cache_sum cache id stuff =
- try Id.Map.add id (Id.Set.add stuff (Id.Map.find id cache)) cache
- with Not_found -> Id.Map.add id (Id.Set.singleton stuff) cache in
- let cache =
- List.fold_left (fun cache id ->
- Id.Set.fold (fun d cache -> cache_sum cache d id)
- (Id.Set.remove id (deps_of id)) cache)
- Id.Map.empty all_ids in
- fun id -> try Id.Map.find id cache with Not_found -> Id.Set.empty in
- let rec aux s =
- let s' =
- Id.Set.fold (fun id s ->
- if Id.Set.subset (inv_dep_of id) s then Id.Set.diff s (inv_dep_of id)
- else s)
- s s in
- if Id.Set.equal s s' then s else aux s' in
- aux ids
-
-let suggest_Proof_using kn env vars ids_typ context_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 suggest_Proof_using name env vars ids_typ context_ids =
let module S = Id.Set in
let open Pp in
- let used = S.union vars ids_typ in
- let needed = minimize_hyps env used in
- let all_needed = really_needed env needed in
- let all = List.fold_right S.add context_ids S.empty in
- let unneeded = minimize_unused_hyps env (S.diff all needed) in
- let pr_set s =
+ let print x = prerr_endline (string_of_ppcmds x) in
+ let pr_set parens s =
let wrap ppcmds =
- if S.cardinal s > 1 || S.equal s (S.singleton (Id.of_string "All"))
- then str "(" ++ ppcmds ++ str ")"
+ 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 used = S.union vars ids_typ 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_right S.add context_ids S.empty in
+ let fwd_typ = close_fwd env ids_typ in
if !Flags.debug then begin
- prerr_endline (string_of_ppcmds (str "All " ++ pr_set all));
- prerr_endline (string_of_ppcmds (str "Type" ++ pr_set ids_typ));
- prerr_endline (string_of_ppcmds (str "needed " ++ pr_set needed));
- prerr_endline (string_of_ppcmds (str "unneeded " ++ pr_set unneeded));
+ 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);
msg_info (
- str"The proof of "++
- Names.Constant.print kn ++ spc() ++ str "should start with:"++spc()++
- str"Proof using " ++
- if S.is_empty needed then str "."
- else if S.subset needed ids_typ then str "Type."
- else if S.equal all all_needed then str "All."
- else
- let s1 = string_of_ppcmds (str "-" ++ pr_set unneeded ++ str".") in
- let s2 = string_of_ppcmds (pr_set needed ++ str".") in
- if String.length s1 < String.length s2 then str s1 else str s2)
+ str"The proof of "++ str name ++ 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));
+ string_of_ppcmds (prlist_with_sep (fun _ -> str";") (fun x->x) !valid_exprs)
+;;
let value = ref false
@@ -146,13 +146,13 @@ let _ =
Goptions.optwrite = (fun b ->
value := b;
if b then Term_typing.set_suggest_proof_using suggest_Proof_using
- else Term_typing.set_suggest_proof_using (fun _ _ _ _ _ -> ())
+ else Term_typing.set_suggest_proof_using (fun _ _ _ _ _ -> "")
) }
-let value = ref "_unset_"
+let value = ref None
let _ =
- Goptions.declare_string_option
+ Goptions.declare_stringopt_option
{ Goptions.optsync = true;
Goptions.optdepr = false;
Goptions.optname = "default value for Proof using";
@@ -161,6 +161,4 @@ let _ =
Goptions.optwrite = (fun b -> value := b;) }
-let get_default_proof_using () =
- if !value = "_unset_" then None
- else Some !value
+let get_default_proof_using () = !value
diff --git a/proofs/proof_using.mli b/proofs/proof_using.mli
index fb3497f10..dcf8a0fcd 100644
--- a/proofs/proof_using.mli
+++ b/proofs/proof_using.mli
@@ -6,21 +6,12 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-
-(* [minimize_hyps e s1] gives [s2] s.t. [Id.Set.subset s2 s1] is [true]
- * and [keep_hyps e s1] is equal to [keep_hyps e s2]. Inefficient. *)
-val minimize_hyps : Environ.env -> Names.Id.Set.t -> Names.Id.Set.t
-
-(* [minimize_unused_hyps e s1] gives [s2] s.t. [Id.Set.subset s2 s1] is [true]
- * and s.t. calling [clear s1] would do the same as [clear s2]. Inefficient. *)
-val minimize_unused_hyps : Environ.env -> Names.Id.Set.t -> Names.Id.Set.t
-
val process_expr :
- Environ.env -> Vernacexpr.section_subset_descr -> Constr.types list ->
+ Environ.env -> Vernacexpr.section_subset_expr -> Constr.types list ->
Names.Id.t list
-val name_set : Names.Id.t -> Vernacexpr.section_subset_descr -> unit
+val name_set : Names.Id.t -> Vernacexpr.section_subset_expr -> unit
-val to_string : Vernacexpr.section_subset_descr -> string
+val to_string : Vernacexpr.section_subset_expr -> string
val get_default_proof_using : unit -> string option
diff --git a/stm/stm.ml b/stm/stm.ml
index d25466e08..acbb5f646 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -888,9 +888,16 @@ let set_compilation_hints file =
hints := Aux_file.load_aux_file_for file
let get_hint_ctx loc =
let s = Aux_file.get !hints loc "context_used" in
- let ids = List.map Names.Id.of_string (Str.split (Str.regexp " ") s) in
- let ids = List.map (fun id -> Loc.ghost, id) ids in
- SsExpr (SsSet ids)
+ match Str.split (Str.regexp ";") s with
+ | ids :: _ ->
+ let ids = List.map Names.Id.of_string (Str.split (Str.regexp " ") ids) in
+ let ids = List.map (fun id -> Loc.ghost, id) ids in
+ begin match ids with
+ | [] -> SsEmpty
+ | x :: xs ->
+ List.fold_left (fun a x -> SsUnion (SsSingl x,a)) (SsSingl x) xs
+ end
+ | _ -> raise Not_found
let get_hint_bp_time proof_name =
try float_of_string (Aux_file.get !hints Loc.ghost proof_name)
diff --git a/test-suite/success/proof_using.v b/test-suite/success/proof_using.v
index 61e73f858..c83f45e2a 100644
--- a/test-suite/success/proof_using.v
+++ b/test-suite/success/proof_using.v
@@ -117,5 +117,81 @@ End T1.
Check (bla 7 : 2 = 8).
+Section A.
+Variable a : nat.
+Variable b : nat.
+Variable c : nat.
+Variable H1 : a = 3.
+Variable H2 : a = 3 -> b = 7.
+Variable H3 : c = 3.
+
+Lemma foo : a = a.
+Proof using Type*.
+pose H1 as e1.
+pose H2 as e2.
+reflexivity.
+Qed.
+
+Lemma bar : a = 3 -> b = 7.
+Proof using b*.
+exact H2.
+Qed.
+
+Lemma baz : c=3.
+Proof using c*.
+exact H3.
+Qed.
+
+Lemma baz2 : c=3.
+Proof using c* a.
+exact H3.
+Qed.
+
+End A.
+
+Check (foo 3 7 (refl_equal 3)
+ (fun _ => refl_equal 7)).
+Check (bar 3 7 (refl_equal 3)
+ (fun _ => refl_equal 7)).
+Check (baz2 99 3 (refl_equal 3)).
+Check (baz 3 (refl_equal 3)).
+
+Section Let.
+
+Variables a b : nat.
+Let pa : a = a. Proof. reflexivity. Qed.
+Unset Default Proof Using.
+Set Suggest Proof Using.
+Lemma test_let : a = a.
+Proof using a.
+exact pa.
+Qed.
+
+Let ppa : pa = pa. Proof. reflexivity. Qed.
+
+Lemma test_let2 : pa = pa.
+Proof using Type.
+exact ppa.
+Qed.
+
+End Let.
+
+Check (test_let 3).
+
+Section Clear.
+
+Variable a: nat.
+Hypotheses H : a = 4.
+
+Set Proof Using Clear Unused.
+
+Lemma test_clear : a = a.
+Proof using a.
+Fail rewrite H.
+trivial.
+Qed.
+
+End Clear.
+
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 5147d81bc..72c800f0f 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -874,18 +874,7 @@ let vernac_set_used_variables e =
errorlabstrm "vernac_set_used_variables"
(str "Unknown variable: " ++ pr_id id))
l;
- let closure_l = List.map pi1 (set_used_variables l) in
- let closure_l = List.fold_right Id.Set.add closure_l Id.Set.empty in
- let vars_of = Environ.global_vars_set in
- let aux env entry (all_safe,rest as orig) =
- match entry with
- | (x,None,_) ->
- if Id.Set.mem x all_safe then orig else (all_safe, (Loc.ghost,x)::rest)
- | (x,Some bo, ty) ->
- let vars = Id.Set.union (vars_of env bo) (vars_of env ty) in
- if Id.Set.subset vars all_safe then (Id.Set.add x all_safe, rest)
- else (all_safe, (Loc.ghost,x) :: rest) in
- let _,to_clear = Environ.fold_named_context aux env ~init:(closure_l,[]) in
+ let _, to_clear = set_used_variables l in
vernac_solve
SelectAll None Tacexpr.(TacAtom (Loc.ghost,TacClear(false,to_clear))) false
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-22 10:34:16 +0000