From ffc91e6fcc7a1f3d719b7ad95dbbd3293e26c653 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Wed, 27 Sep 2017 15:05:36 +0200 Subject: Take Suggest Proof Using outside the kernel. Also add an output test for Suggest Proof Using. This changes the .aux output: instead of getting a key >context_used "$hyps;$suggest" where $hyps is a list of the used hypotheses and $suggest is the ;-separated suggestions (or the empty string if Suggest Proof Using is unset), there is a key >context_used "$hyps" and if Suggest Proof Using is set also a key >suggest_proof_using "$suggest" For instance instead of 112 116 context_used "B A;A B;All" we get 112 116 context_used "B A" 112 116 suggest_proof_using "A B;All" --- kernel/term_typing.ml | 20 +++--------- kernel/term_typing.mli | 3 -- proofs/proof_using.ml | 55 +++++++++++++++++++++++++-------- proofs/proof_using.mli | 4 +++ test-suite/output/SuggestProofUsing.out | 7 +++++ test-suite/output/SuggestProofUsing.v | 31 +++++++++++++++++++ vernac/lemmas.ml | 10 +++++- 7 files changed, 98 insertions(+), 32 deletions(-) create mode 100644 test-suite/output/SuggestProofUsing.out create mode 100644 test-suite/output/SuggestProofUsing.v diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 0c0b910e1d..22e109b01c 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -367,7 +367,7 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry cook_context = None; } -let record_aux env s_ty s_bo suggested_expr = +let record_aux env s_ty s_bo = let in_ty = keep_hyps env s_ty in let v = String.concat " " @@ -376,10 +376,7 @@ let record_aux env s_ty s_bo suggested_expr = if List.exists (NamedDecl.get_id %> Id.equal 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 set_suggest_proof_using f = suggest_proof_using := f + Aux_file.record_in_aux "context_used" v let build_constant_declaration kn env result = let open Cooking in @@ -425,16 +422,13 @@ let build_constant_declaration kn env result = (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); - let expr = - !suggest_proof_using (Constant.to_string kn) - env vars ids_typ context_ids in - if !Flags.record_aux_file then record_aux env ids_typ vars expr; + if !Flags.record_aux_file then record_aux env ids_typ vars; vars in keep_hyps env (Idset.union ids_typ ids_def), def | None -> if !Flags.record_aux_file 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 *) @@ -618,14 +612,10 @@ let translate_local_def mb env id centry = | Undef _ -> () | Def _ -> () | OpaqueDef lc -> - let context_ids = List.map NamedDecl.get_id (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 + record_aux env ids_typ ids_def end; let univs = match decl.cook_universes with | Monomorphic_const ctx -> ctx diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 24153343e7..b16f81c5a6 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -77,6 +77,3 @@ val infer_declaration : trust:'a trust -> env -> constant option -> val build_constant_declaration : constant -> env -> Cooking.result -> constant_body - -val set_suggest_proof_using : - (string -> env -> Id.Set.t -> Id.Set.t -> Id.t list -> string) -> unit diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml index 1a321120c6..9bfc8bada8 100644 --- a/proofs/proof_using.ml +++ b/proofs/proof_using.ml @@ -105,7 +105,13 @@ let remove_ids_and_lets env s ids = (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 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 @@ -114,10 +120,13 @@ let suggest_Proof_using name env vars ids_typ context_ids = 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 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); @@ -133,26 +142,46 @@ let suggest_Proof_using name env vars ids_typ context_ids = if S.equal all all_needed then valid(str "All"); valid (pr_set false needed); Feedback.msg_info ( - str"The proof of "++ str name ++ spc() ++ + 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)); - string_of_ppcmds (prlist_with_sep (fun _ -> str";") (fun x->x) !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 value = ref false +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 () -> !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 _ _ _ _ _ -> "") - ) } + 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 (Constant.print 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 diff --git a/proofs/proof_using.mli b/proofs/proof_using.mli index c882b1827a..ac2795f806 100644 --- a/proofs/proof_using.mli +++ b/proofs/proof_using.mli @@ -16,4 +16,8 @@ val name_set : Names.Id.t -> Vernacexpr.section_subset_expr -> unit val to_string : Vernacexpr.section_subset_expr -> string +val suggest_constant : Environ.env -> Names.Constant.t -> unit + +val suggest_variable : Environ.env -> Names.Id.t -> unit + val get_default_proof_using : unit -> string option diff --git a/test-suite/output/SuggestProofUsing.out b/test-suite/output/SuggestProofUsing.out new file mode 100644 index 0000000000..97cb0fdd89 --- /dev/null +++ b/test-suite/output/SuggestProofUsing.out @@ -0,0 +1,7 @@ +The proof of Top#Sec#nat should start with one of the following commands: +Proof using . +Proof using Type*. +Proof using Type. +The proof of foo should start with one of the following commands: +Proof using A B. +Proof using All. diff --git a/test-suite/output/SuggestProofUsing.v b/test-suite/output/SuggestProofUsing.v new file mode 100644 index 0000000000..b0b514a52b --- /dev/null +++ b/test-suite/output/SuggestProofUsing.v @@ -0,0 +1,31 @@ +Set Suggest Proof Using. + +Section Sec. + Variables A B : Type. + + (* Some normal lemma. Sadly the internal name gets printed. *) + Lemma nat : Set. + Proof. + exact nat. + Qed. + + (* Make sure All is suggested even though we add an unused variable + to the context. *) + Let foo : Type. + Proof. + exact (A -> B). + Qed. + + (* Having a [Proof using] disables the suggestion message. *) + Definition bar : Type. + Proof using A. + exact A. + Qed. + + (* Transparent definitions don't get a suggestion message. *) + Definition baz : Type. + Proof. + exact A. + Defined. + +End Sec. diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 2c8f6ec9d6..d45665dd4c 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -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 -- cgit v1.2.3 From 7f1635816588ae200c8eed381d726bd29f57d899 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 27 Sep 2017 16:12:58 +0200 Subject: [vernac] Remove "Proof using" hacks from parser. We place `Proof_using` in the proper place [`vernac`] and we remove gross parsing hacks. The new placement should allow to use the printers and more convenient structure, and reduce strange coupling between parsing and internal representation. --- API/API.mli | 1 - parsing/g_proofs.ml4 | 9 +-- plugins/ltac/g_ltac.ml4 | 2 +- printing/ppvernac.ml | 10 ++- printing/ppvernac.mli | 3 + proofs/proof_using.ml | 197 ----------------------------------------------- proofs/proof_using.mli | 23 ------ proofs/proofs.mllib | 1 - vernac/proof_using.ml | 200 ++++++++++++++++++++++++++++++++++++++++++++++++ vernac/proof_using.mli | 23 ++++++ vernac/vernac.mllib | 1 + vernac/vernacentries.ml | 23 ++++-- 12 files changed, 253 insertions(+), 240 deletions(-) delete mode 100644 proofs/proof_using.ml delete mode 100644 proofs/proof_using.mli create mode 100644 vernac/proof_using.ml create mode 100644 vernac/proof_using.mli diff --git a/API/API.mli b/API/API.mli index 04c69b025f..879323a37d 100644 --- a/API/API.mli +++ b/API/API.mli @@ -4914,7 +4914,6 @@ module G_proofs : sig val hint : Vernacexpr.hints_expr Pcoq.Gram.entry - val hint_proof_using : 'a Pcoq.Gram.entry -> 'a option -> 'a option end diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index e2c87bbbf6..f10d746770 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -17,12 +17,6 @@ open Pcoq.Vernac_ let thm_token = G_vernac.thm_token -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))) - let hint = Gram.entry_create "hint" (* Proof commands *) @@ -35,8 +29,7 @@ GEXTEND Gram ; command: [ [ IDENT "Goal"; c = lconstr -> VernacGoal c - | IDENT "Proof" -> - VernacProof (None,hint_proof_using G_vernac.section_subset_expr None) + | IDENT "Proof" -> VernacProof (None,None) | IDENT "Proof" ; IDENT "Mode" ; mn = string -> VernacProofMode mn | IDENT "Proof"; c = lconstr -> VernacExactProof c | IDENT "Abort" -> VernacAbort None diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index d639dd0e1c..c577cb2198 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -340,7 +340,7 @@ GEXTEND Gram command: [ [ IDENT "Proof"; "with"; ta = Pltac.tactic; l = OPT [ "using"; l = G_vernac.section_subset_expr -> l ] -> - Vernacexpr.VernacProof (Some (in_tac ta), G_proofs.hint_proof_using G_vernac.section_subset_expr l) + Vernacexpr.VernacProof (Some (in_tac ta), l) | IDENT "Proof"; "using"; l = G_vernac.section_subset_expr; ta = OPT [ "with"; ta = Pltac.tactic -> in_tac ta ] -> Vernacexpr.VernacProof (ta,Some l) ] ] diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index a1cdfdbaa2..4c68285f3f 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -524,7 +524,15 @@ open Decl_kinds | PrintStrategy (Some qid) -> keyword "Print Strategy" ++ pr_smart_global qid - let pr_using e = str (Proof_using.to_string e) + let pr_using 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 Pp.str (aux e) let rec pr_vernac_body v = let return = tag_vernac v in diff --git a/printing/ppvernac.mli b/printing/ppvernac.mli index b88eed4843..cf27b413c0 100644 --- a/printing/ppvernac.mli +++ b/printing/ppvernac.mli @@ -15,5 +15,8 @@ val pr_rec_definition : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation lis (** Prints a vernac expression *) val pr_vernac_body : Vernacexpr.vernac_expr -> Pp.t +(** Prints a "proof using X" clause. *) +val pr_using : Vernacexpr.section_subset_expr -> Pp.t + (** Prints a vernac expression and closes it with a dot. *) val pr_vernac : Vernacexpr.vernac_expr -> Pp.t diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml deleted file mode 100644 index 9bfc8bada8..0000000000 --- a/proofs/proof_using.ml +++ /dev/null @@ -1,197 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* "()" - | 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" - -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 rec process_expr env e 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 - else 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 - -and full_set env = - List.fold_right Id.Set.add (List.map NamedDecl.get_id (named_context env)) Id.Set.empty - -let process_expr env e ty = - let ty_expr = SsSingl(Loc.tag @@ 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)) - -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 (Constant.print 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 _ = - Goptions.declare_stringopt_option - { 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 () = !value diff --git a/proofs/proof_using.mli b/proofs/proof_using.mli deleted file mode 100644 index ac2795f806..0000000000 --- a/proofs/proof_using.mli +++ /dev/null @@ -1,23 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Vernacexpr.section_subset_expr -> Constr.types list -> - Names.Id.t list - -val name_set : Names.Id.t -> Vernacexpr.section_subset_expr -> unit - -val to_string : Vernacexpr.section_subset_expr -> string - -val suggest_constant : Environ.env -> Names.Constant.t -> unit - -val suggest_variable : Environ.env -> Names.Id.t -> unit - -val get_default_proof_using : unit -> string option diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib index eaf0c693e1..058e839b47 100644 --- a/proofs/proofs.mllib +++ b/proofs/proofs.mllib @@ -1,7 +1,6 @@ Miscprint Goal Evar_refiner -Proof_using Proof_type Logic Refine diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml new file mode 100644 index 0000000000..5cc348095e --- /dev/null +++ b/vernac/proof_using.ml @@ -0,0 +1,200 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* "()" + | 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" + +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 rec process_expr env e 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 + else 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 + +and full_set env = + List.fold_right Id.Set.add (List.map NamedDecl.get_id (named_context env)) Id.Set.empty + +let process_expr env e ty = + let ty_expr = SsSingl(Loc.tag @@ 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)) + +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 (Constant.print 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/proof_using.mli b/vernac/proof_using.mli new file mode 100644 index 0000000000..ddab2742d7 --- /dev/null +++ b/vernac/proof_using.mli @@ -0,0 +1,23 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* Vernacexpr.section_subset_expr -> Constr.types list -> + Names.Id.t list + +val name_set : Names.Id.t -> Vernacexpr.section_subset_expr -> unit + +val to_string : Vernacexpr.section_subset_expr -> string + +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/vernac.mllib b/vernac/vernac.mllib index f74073e1f7..850902d6ba 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 203d913db8..4af4b642ca 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2060,17 +2060,24 @@ let interp ?proof ?loc locality poly c = | VernacEndSubproof -> vernac_end_subproof () | VernacShow s -> vernac_show s | VernacCheckGuard -> vernac_check_guard () - | VernacProof (None, None) -> + | VernacProof (None, using) -> + begin match Option.append using (Proof_using.get_default_proof_using ()) with + | 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) -> + | 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 + end + | VernacProof (Some tac, using) -> + begin match Option.append using (Proof_using.get_default_proof_using ()) with + | None -> + Aux_file.record_in_aux_at ?loc "VernacProof" "tac:yes using:no"; + vernac_set_end_tac 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 + end | VernacProofMode mn -> Proof_global.set_proof_mode mn [@ocaml.warning "-3"] (* Extensions *) -- cgit v1.2.3 From 3b640b68c89f1e9fcbb0f98c8865819189409382 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Wed, 27 Sep 2017 16:37:03 +0200 Subject: Code factorization Vernacentries.interp on VernacProof. --- vernac/vernacentries.ml | 25 +++++++------------------ 1 file changed, 7 insertions(+), 18 deletions(-) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 4af4b642ca..66427b7093 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2060,24 +2060,13 @@ let interp ?proof ?loc locality poly c = | VernacEndSubproof -> vernac_end_subproof () | VernacShow s -> vernac_show s | VernacCheckGuard -> vernac_check_guard () - | VernacProof (None, using) -> - begin match Option.append using (Proof_using.get_default_proof_using ()) with - | None -> - Aux_file.record_in_aux_at ?loc "VernacProof" "tac:no using:no" - | Some l -> - Aux_file.record_in_aux_at ?loc "VernacProof" "tac:no using:yes"; - vernac_set_used_variables l - end - | VernacProof (Some tac, using) -> - begin match Option.append using (Proof_using.get_default_proof_using ()) with - | None -> - Aux_file.record_in_aux_at ?loc "VernacProof" "tac:yes using:no"; - vernac_set_end_tac 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 - end + | 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 *) -- cgit v1.2.3 From a627891e0505e7da7afcb56c79d2058ebf058694 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Wed, 27 Sep 2017 16:45:29 +0200 Subject: Use a nice printer for constant names in Suggest Proof Using. --- test-suite/output/SuggestProofUsing.out | 2 +- test-suite/output/SuggestProofUsing.v | 2 +- vernac/proof_using.ml | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/test-suite/output/SuggestProofUsing.out b/test-suite/output/SuggestProofUsing.out index 97cb0fdd89..8d67a4a4b7 100644 --- a/test-suite/output/SuggestProofUsing.out +++ b/test-suite/output/SuggestProofUsing.out @@ -1,4 +1,4 @@ -The proof of Top#Sec#nat should start with one of the following commands: +The proof of nat should start with one of the following commands: Proof using . Proof using Type*. Proof using Type. diff --git a/test-suite/output/SuggestProofUsing.v b/test-suite/output/SuggestProofUsing.v index b0b514a52b..00b6f8e183 100644 --- a/test-suite/output/SuggestProofUsing.v +++ b/test-suite/output/SuggestProofUsing.v @@ -3,7 +3,7 @@ Set Suggest Proof Using. Section Sec. Variables A B : Type. - (* Some normal lemma. Sadly the internal name gets printed. *) + (* Some normal lemma. *) Lemma nat : Set. Proof. exact nat. diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml index 5cc348095e..ade132ae1a 100644 --- a/vernac/proof_using.ml +++ b/vernac/proof_using.ml @@ -168,7 +168,7 @@ let suggest_constant env kn = 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 (Constant.print kn) used ids_typ Id.Set.empty + suggest_common env (Printer.pr_constant env kn) used ids_typ Id.Set.empty end let suggest_variable env id = -- cgit v1.2.3 From 74826c1869a423b4e7224d3f69180584bdef1726 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Wed, 27 Sep 2017 16:54:41 +0200 Subject: Parse [Proof using Type] without translating Type to an id. --- intf/vernacexpr.ml | 1 + parsing/g_vernac.ml4 | 4 ++-- printing/ppvernac.ml | 1 + vernac/proof_using.ml | 36 +++++++++++++----------------------- vernac/proof_using.mli | 2 -- 5 files changed, 17 insertions(+), 27 deletions(-) diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index 4a471d4a2b..bc7146884c 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -236,6 +236,7 @@ type scheme = type section_subset_expr = | SsEmpty + | SsType | SsSingl of lident | SsCompl of section_subset_expr | SsUnion of section_subset_expr * section_subset_expr diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 3e0b85b54a..a5b58b8553 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -580,8 +580,8 @@ GEXTEND Gram starredidentref: [ [ i = identref -> SsSingl i | i = identref; "*" -> SsFwdClose(SsSingl i) - | "Type" -> SsSingl (Loc.tag ~loc:!@loc @@ Id.of_string "Type") - | "Type"; "*" -> SsFwdClose (SsSingl (Loc.tag ~loc:!@loc @@ Id.of_string "Type")) ]] + | "Type" -> SsType + | "Type"; "*" -> SsFwdClose SsType ]] ; ssexpr: [ "35" diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 4c68285f3f..d1158b3d6f 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -527,6 +527,7 @@ open Decl_kinds let pr_using e = let rec aux = function | SsEmpty -> "()" + | SsType -> "(Type)" | SsSingl (_,id) -> "("^Id.to_string id^")" | SsCompl e -> "-" ^ aux e^"" | SsUnion(e1,e2) -> "("^aux e1 ^" + "^ aux e2^")" diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml index ade132ae1a..ffe99cfd81 100644 --- a/vernac/proof_using.ml +++ b/vernac/proof_using.ml @@ -14,16 +14,6 @@ open Context.Named.Declaration module NamedDecl = Context.Named.Declaration -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" let in_nameset = @@ -48,12 +38,20 @@ let rec close_fwd e 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 - | SsSingl (_,id) -> set_of_id env ty id + | 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) @@ -61,23 +59,15 @@ let rec process_expr env e ty = 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 - else if Id.to_string id = "All" then +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 -and full_set env = - List.fold_right Id.Set.add (List.map NamedDecl.get_id (named_context env)) Id.Set.empty - let process_expr env e ty = - let ty_expr = SsSingl(Loc.tag @@ Id.of_string "Type") in - let v_ty = process_expr env ty_expr ty in + 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 diff --git a/vernac/proof_using.mli b/vernac/proof_using.mli index ddab2742d7..f63c8e2424 100644 --- a/vernac/proof_using.mli +++ b/vernac/proof_using.mli @@ -14,8 +14,6 @@ val process_expr : val name_set : Names.Id.t -> Vernacexpr.section_subset_expr -> unit -val to_string : Vernacexpr.section_subset_expr -> string - val suggest_constant : Environ.env -> Names.Constant.t -> unit val suggest_variable : Environ.env -> Names.Id.t -> unit -- cgit v1.2.3 From 4e016b91f59d3bb13681a53c35fbf4a979140b83 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Wed, 27 Sep 2017 17:09:56 +0200 Subject: Stm.get_hint_ctx: remove unused Str.split With suggest proof using out of the kernel the format of context_used in .aux is just the list of ids wanted by get_hint_ctx. (split x s when x doesn't appear in s just returns the singleton list [s]) --- stm/stm.ml | 16 ++++++---------- 1 file changed, 6 insertions(+), 10 deletions(-) diff --git a/stm/stm.ml b/stm/stm.ml index 220ed9be4e..26b3320aab 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1145,16 +1145,12 @@ let set_compilation_hints file = let get_hint_ctx loc = let s = Aux_file.get ?loc !hints "context_used" in - 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.tag 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 ids = List.map Names.Id.of_string (Str.split (Str.regexp " ") s) in + let ids = List.map (fun id -> Loc.tag id) ids in + match ids with + | [] -> SsEmpty + | x :: xs -> + List.fold_left (fun a x -> SsUnion (SsSingl x,a)) (SsSingl x) xs let get_hint_bp_time proof_name = try float_of_string (Aux_file.get !hints proof_name) -- cgit v1.2.3