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