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" --- proofs/proof_using.ml | 55 +++++++++++++++++++++++++++++++++++++++------------ 1 file changed, 42 insertions(+), 13 deletions(-) (limited to 'proofs/proof_using.ml') 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 -- 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. --- proofs/proof_using.ml | 197 -------------------------------------------------- 1 file changed, 197 deletions(-) delete mode 100644 proofs/proof_using.ml (limited to 'proofs/proof_using.ml') 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 -- cgit v1.2.3