diff options
Diffstat (limited to 'proofs/proof_using.ml')
| -rw-r--r-- | proofs/proof_using.ml | 172 |
1 files changed, 85 insertions, 87 deletions
diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml index f66e9657..7eed1cb3 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 |