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" --- vernac/lemmas.ml | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) (limited to 'vernac') 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. --- vernac/proof_using.ml | 200 ++++++++++++++++++++++++++++++++++++++++++++++++ vernac/proof_using.mli | 23 ++++++ vernac/vernac.mllib | 1 + vernac/vernacentries.ml | 23 ++++-- 4 files changed, 239 insertions(+), 8 deletions(-) create mode 100644 vernac/proof_using.ml create mode 100644 vernac/proof_using.mli (limited to 'vernac') 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(-) (limited to 'vernac') 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. --- vernac/proof_using.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'vernac') 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. --- vernac/proof_using.ml | 36 +++++++++++++----------------------- vernac/proof_using.mli | 2 -- 2 files changed, 13 insertions(+), 25 deletions(-) (limited to 'vernac') 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