From 9ea8867a0fa8f2a52df102732fdc1a931c659826 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 30 Sep 2015 22:12:25 +0200 Subject: Proof using: let-in policy, optional auto-clear, forward closure* - "Proof using p*" means: use p and any section var about p. - Simplify the grammar/parser for proof using . - Section variables with a body (let-in) are pulled in automatically since they are safe to be used (add no extra quantification) - automatic clear of "unused" section variables made optional: Set Proof Using Clear Unused. since clearing section hypotheses does not "always work" (e.g. hint databases are not really cleaned) - term_typing: trigger a "suggest proof using" message also for Let theorems. --- proofs/proof_using.ml | 172 +++++++++++++++++++++++++------------------------- 1 file changed, 85 insertions(+), 87 deletions(-) (limited to 'proofs/proof_using.ml') diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml index f66e965712..7eed1cb317 100644 --- a/proofs/proof_using.ml +++ b/proofs/proof_using.ml @@ -11,20 +11,15 @@ 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 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" @@ -36,30 +31,48 @@ let in_nameset = discharge_function = (fun _ -> None) } +let rec close_fwd e s = + let s' = + List.fold_left (fun s (id,b,ty) -> + let vb = Option.(default Id.Set.empty (map (global_vars_set e) b)) in + let vty = global_vars_set e ty 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 id (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 = - match e with - | SsAll -> - List.fold_right Id.Set.add (List.map pi1 (named_context env)) Id.Set.empty - | SsExpr e -> - let rec aux = function - | SsSet l -> set_of_list env (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 - aux e - | SsType -> - List.fold_left (fun acc 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 -and set_of_list env = function - | [x] when CList.mem_assoc_f Id.equal x !known_names -> - process_expr env (CList.assoc_f Id.equal x !known_names) [] - | l -> List.fold_right Id.Set.add l Id.Set.empty -and full_set env = set_of_list env (List.map pi1 (named_context env)) + else if Id.to_string id = "All" then + List.fold_right Id.Set.add (List.map pi1 (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 pi1 (named_context env)) Id.Set.empty let process_expr env e ty = - let s = Id.Set.union (process_expr env SsType ty) (process_expr env e []) in + let ty_expr = SsSingl(Loc.ghost, 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)) @@ -77,62 +90,49 @@ let minimize_hyps env 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 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 suggest_Proof_using name 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 print x = prerr_endline (string_of_ppcmds x) in + let pr_set parens s = let wrap ppcmds = - if S.cardinal s > 1 || S.equal s (S.singleton (Id.of_string "All")) - then str "(" ++ ppcmds ++ str ")" + 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 fwd_typ = close_fwd env ids_typ 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)); + 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); 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) + str"The proof of "++ str name ++ 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) +;; let value = ref false @@ -146,13 +146,13 @@ let _ = 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 _ _ _ _ _ -> ()) + else Term_typing.set_suggest_proof_using (fun _ _ _ _ _ -> "") ) } -let value = ref "_unset_" +let value = ref None let _ = - Goptions.declare_string_option + Goptions.declare_stringopt_option { Goptions.optsync = true; Goptions.optdepr = false; Goptions.optname = "default value for Proof using"; @@ -161,6 +161,4 @@ let _ = Goptions.optwrite = (fun b -> value := b;) } -let get_default_proof_using () = - if !value = "_unset_" then None - else Some !value +let get_default_proof_using () = !value -- cgit v1.2.3 From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Jan 2016 17:25:10 +0100 Subject: Update copyright headers. --- proofs/proof_using.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'proofs/proof_using.ml') diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml index 7eed1cb317..a69645b116 100644 --- a/proofs/proof_using.ml +++ b/proofs/proof_using.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* match (prod_assum (snd (decompose_prod_n_assum n c))) with | [_,None,c] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc Suppose that you do not know about rel-context and named-context. (that is the case of people who just started to read the source code) Merlin would tell you that the type of the value you are destructing by "match" is: 'a * 'b option * Constr.t (* worst-case scenario *) or Named.Name.t * Constr.t option * Constr.t (* best-case scenario (?) *) To me, this is akin to wearing an opaque veil. It is hard to figure out the meaning of the values you are looking at. In particular, it is hard to discover the connection between the value we are destructing above and the datatypes and functions defined in the "kernel/context.ml" file. In this case, the connection is there, but it is not visible (between the function above and the "Context" module). ------------------------------------------------------------------------ Now consider, what happens when the reader see the same function presented in the following form: let test_strict_disjunction n lc = Array.for_all_i (fun i c -> match (prod_assum (snd (decompose_prod_n_assum n c))) with | [LocalAssum (_,c)] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc If the reader haven't seen "LocalAssum" before, (s)he can use Merlin to jump to the corresponding definition and learn more. In this case, the connection is there, and it is directly visible (between the function above and the "Context" module). (2) Also, if we already have the concepts such as: - local declaration - local assumption - local definition and we describe these notions meticulously in the Reference Manual, then it is a real pity not to reinforce the connection of the actual code with the abstract description we published. --- proofs/proof_using.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'proofs/proof_using.ml') diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml index a69645b116..681a7fa1ad 100644 --- a/proofs/proof_using.ml +++ b/proofs/proof_using.ml @@ -10,6 +10,7 @@ open Names open Environ open Util open Vernacexpr +open Context.Named.Declaration let to_string e = let rec aux = function @@ -33,7 +34,8 @@ let in_nameset = let rec close_fwd e s = let s' = - List.fold_left (fun s (id,b,ty) -> + List.fold_left (fun s decl -> + let (id,b,ty) = Context.Named.Declaration.to_tuple decl in let vb = Option.(default Id.Set.empty (map (global_vars_set e) b)) in let vty = global_vars_set e ty in let vbty = Id.Set.union vb vty in @@ -61,13 +63,13 @@ and set_of_id env ty id = 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 pi1 (named_context env)) Id.Set.empty + List.fold_right Id.Set.add (List.map 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 pi1 (named_context env)) Id.Set.empty + List.fold_right Id.Set.add (List.map get_id (named_context env)) Id.Set.empty let process_expr env e ty = let ty_expr = SsSingl(Loc.ghost, Id.of_string "Type") in -- cgit v1.2.3