diff options
-rw-r--r-- | intf/vernacexpr.mli | 10 | ||||
-rw-r--r-- | kernel/term_typing.ml | 4 | ||||
-rw-r--r-- | kernel/term_typing.mli | 3 | ||||
-rw-r--r-- | parsing/g_proofs.ml4 | 44 | ||||
-rw-r--r-- | printing/ppvernac.ml | 8 | ||||
-rw-r--r-- | proofs/proof_using.ml | 148 | ||||
-rw-r--r-- | proofs/proof_using.mli | 24 | ||||
-rw-r--r-- | proofs/proofs.mllib | 1 | ||||
-rw-r--r-- | toplevel/stm.ml | 2 | ||||
-rw-r--r-- | toplevel/vernac_classifier.ml | 3 | ||||
-rw-r--r-- | toplevel/vernacentries.ml | 8 |
11 files changed, 241 insertions, 14 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 4f666a801..ee51a7694 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -214,6 +214,14 @@ type scheme = | CaseScheme of bool * reference or_by_notation * sort_expr | EqualityScheme of reference or_by_notation +type section_subset_expr = + | SsSet of lident list + | 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 + (* This type allows to register inline of constants in native compiler. It will be extended with primitive inductive types and operators *) type register_kind = @@ -412,7 +420,7 @@ type vernac_expr = | VernacEndSubproof | VernacShow of showable | VernacCheckGuard - | VernacProof of raw_tactic_expr option * lident list option + | VernacProof of raw_tactic_expr option * section_subset_descr option | VernacProofMode of string (* Toplevel control *) | VernacToplevelControl of exn diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 80da45767..55901bce9 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -135,6 +135,9 @@ let record_aux env s1 s2 = (keep_hyps env (Id.Set.union s1 s2))) in Aux_file.record_in_aux "context_used" v +let suggest_proof_using = ref (fun _ _ _ _ _ -> ()) +let set_suggest_proof_using f = suggest_proof_using := f + let build_constant_declaration kn env (def,typ,cst,inline_code,ctx) = let check declared inferred = let mk_set l = List.fold_right Id.Set.add (List.map pi1 l) Id.Set.empty in @@ -159,6 +162,7 @@ let build_constant_declaration kn env (def,typ,cst,inline_code,ctx) = ignore(Future.join cst); let vars = global_vars_set env (Lazyconstr.force_opaque (Future.join lc)) in + !suggest_proof_using kn env vars ids_typ context_ids; if !Flags.compilation_mode = Flags.BuildVo then record_aux env ids_typ vars; vars diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 59706bb83..6f71ecd82 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -35,3 +35,6 @@ val translate_recipe : env -> constant -> Cooking.recipe -> constant_body val infer_declaration : ?what:string -> env -> constant_entry -> Cooking.result 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 diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index e2be4b607..dc545c691 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -21,6 +21,23 @@ open Pcoq.Vernac_ let thm_token = G_vernac.thm_token +let only_identrefs = + Gram.Entry.of_parser "test_only_identrefs" + (fun strm -> + let rec aux n = + match get_tok (Util.stream_nth n strm) with + | KEYWORD "." -> () + | KEYWORD ")" -> () + | IDENT _ -> aux (n+1) + | _ -> raise Stream.Failure in + aux 0) + +let hint_proof_using e = function + | Some _ as x -> x + | None -> match Proof_using.get_default_proof_using () with + | None -> None + | Some s -> Some (Gram.entry_parse e (Gram.parsable (Stream.of_string s))) + (* Proof commands *) GEXTEND Gram GLOBAL: command; @@ -31,12 +48,13 @@ GEXTEND Gram ; command: [ [ IDENT "Goal"; c = lconstr -> VernacGoal c - | IDENT "Proof" -> VernacProof (None,None) + | IDENT "Proof" -> + VernacProof (None,hint_proof_using section_subset_descr None) | IDENT "Proof" ; IDENT "Mode" ; mn = string -> VernacProofMode mn | IDENT "Proof"; "with"; ta = tactic; - l = OPT [ "using"; l = LIST0 identref -> l ] -> - VernacProof (Some ta, l) - | IDENT "Proof"; "using"; l = LIST0 identref; + l = OPT [ "using"; l = section_subset_descr -> l ] -> + VernacProof (Some ta, hint_proof_using section_subset_descr l) + | IDENT "Proof"; "using"; l = section_subset_descr; ta = OPT [ "with"; ta = tactic -> ta ] -> VernacProof (ta,Some l) | IDENT "Proof"; c = lconstr -> VernacExactProof c @@ -97,7 +115,23 @@ GEXTEND Gram VernacHints (false,dbnames, HintsResolve (List.map (fun x -> (pri, true, x)) lc)) ] ]; - + section_subset_descr: + [ [ IDENT "All" -> SsAll + | "Type" -> SsType + | only_identrefs; l = LIST0 identref -> SsExpr (SsSet l) + | e = section_subset_expr -> SsExpr e ] ] + ; + section_subset_expr: + [ "35" + [ "-"; e = section_subset_expr -> 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)] + | "0" + [ i = identref -> SsSet [i] + | "("; only_identrefs; l = LIST0 identref; ")"-> SsSet l + | "("; e = section_subset_expr; ")"-> e ] ] + ; obsolete_locality: [ [ IDENT "Local" -> true | -> false ] ] ; diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 4ece6cb24..6ea34185f 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -471,6 +471,8 @@ let pr_printable = function | PrintNamespace dp -> str "Print Namespace" ++ pr_dirpath dp in +let pr_using e = str (Proof_using.to_string e) in + let rec pr_vernac = function | VernacProgram v -> str"Program" ++ spc() ++ pr_vernac v | VernacLocal (local, v) -> pr_locality local ++ spc() ++ pr_vernac v @@ -944,10 +946,10 @@ let rec pr_vernac = function (* For extension *) | VernacExtend (s,c) -> pr_extend s c | VernacProof (None, None) -> str "Proof" - | VernacProof (None, Some l) -> str "Proof using" ++spc()++ prlist pr_lident l + | VernacProof (None, Some e) -> str "Proof " ++ pr_using e | VernacProof (Some te, None) -> str "Proof with" ++ spc() ++ pr_raw_tactic te - | VernacProof (Some te, Some l) -> - str "Proof using" ++spc()++ prlist pr_lident l ++ spc() ++ + | VernacProof (Some te, Some e) -> + str "Proof " ++ pr_using e ++ spc() ++ str "with" ++ spc() ++pr_raw_tactic te | VernacProofMode s -> str ("Proof Mode "^s) | VernacBullet b -> begin match b with diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml new file mode 100644 index 000000000..746daf273 --- /dev/null +++ b/proofs/proof_using.ml @@ -0,0 +1,148 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013 *) +(* \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 + +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 set_of_list l = List.fold_right Id.Set.add l Id.Set.empty + +let full_set env = set_of_list (List.map pi1 (named_context env)) + +let process_expr env e ty = + match e with + | SsAll -> List.map pi1 (named_context env) + | SsExpr e -> + let rec aux = function + | SsSet l -> set_of_list (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 + Id.Set.elements (aux e) + | SsType -> + match ty with + | [ty] -> Id.Set.elements (global_vars_set env ty) + | _ -> Errors.error"Proof using on a multiple lemma is not supported" + +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 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 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 wrap ppcmds = + if S.cardinal s > 1 || S.equal s (S.singleton (Id.of_string "All")) + then str "(" ++ ppcmds ++ str ")" + else ppcmds in + wrap (prlist_with_sep (fun _ -> str" ") Id.print (S.elements s)) 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)); + end; + 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) + +let value = ref false + +let _ = + Goptions.declare_bool_option + { Goptions.optsync = true; + Goptions.optdepr = false; + Goptions.optname = "suggest Proof using"; + Goptions.optkey = ["Suggest";"Proof";"Using"]; + Goptions.optread = (fun () -> !value); + 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 _ _ _ _ _ -> ()) + ) } + +let value = ref "_unset_" + +let _ = + Goptions.declare_string_option + { Goptions.optsync = true; + Goptions.optdepr = false; + Goptions.optname = "default value for Proof using"; + Goptions.optkey = ["Default";"Proof";"Using"]; + Goptions.optread = (fun () -> !value); + Goptions.optwrite = (fun b -> value := b;) } + + +let get_default_proof_using () = + if !value = "_unset_" then None + else Some !value diff --git a/proofs/proof_using.mli b/proofs/proof_using.mli new file mode 100644 index 000000000..f1731621d --- /dev/null +++ b/proofs/proof_using.mli @@ -0,0 +1,24 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * 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 -> + Names.Id.t list + +val to_string : Vernacexpr.section_subset_descr -> string + +val get_default_proof_using : unit -> string option diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib index 4a7efb029..96b9a89a3 100644 --- a/proofs/proofs.mllib +++ b/proofs/proofs.mllib @@ -1,5 +1,6 @@ Goal Evar_refiner +Proof_using Proof_type Proof_errors Proofview_gen diff --git a/toplevel/stm.ml b/toplevel/stm.ml index 57bbafac3..c0ad01758 100644 --- a/toplevel/stm.ml +++ b/toplevel/stm.ml @@ -581,7 +581,7 @@ 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 - ids + SsExpr (SsSet ids) (* Slave processes (if initialized, otherwise local lazy evaluation) *) module Slaves : sig diff --git a/toplevel/vernac_classifier.ml b/toplevel/vernac_classifier.ml index 37ab694b6..3c14d5922 100644 --- a/toplevel/vernac_classifier.ml +++ b/toplevel/vernac_classifier.ml @@ -92,6 +92,9 @@ let rec classify_vernac e = | VernacCheckGuard | VernacUnfocused | VernacSolveExistential _ -> VtProofStep, VtLater + (* Options changing parser *) + | VernacUnsetOption (["Default";"Proof";"Using"]) + | VernacSetOption (["Default";"Proof";"Using"],_) -> VtSideff [], VtNow (* StartProof *) | VernacDefinition (_,(_,i),ProveBody _) -> VtStartProof("Classic",GuaranteesOpacity,[i]), VtLater diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index b8a368c82..90d2029ea 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -798,10 +798,10 @@ let vernac_set_end_tac tac = | _ -> set_end_tac tac (* TO DO verifier s'il faut pas mettre exist s | TacId s ici*) -let vernac_set_used_variables l = - let l = List.map snd l in - if not (List.distinct_f Id.compare l) - then error "Used variables list contains duplicates"; +let vernac_set_used_variables e = + let tys = + List.map snd (Proof.initial_goals (Proof_global.give_me_the_proof ())) in + let l = Proof_using.process_expr (Global.env ()) e tys in let vars = Environ.named_context (Global.env ()) in List.iter (fun id -> if not (List.exists (fun (id',_,_) -> Id.equal id id') vars) then |