aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/proof_using.ml
blob: 2c489d6ded125d417435c74c3bbc93e26b015c89 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

open Names
open Environ
open Util
open Vernacexpr
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 =
  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.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))

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 suggest_Proof_using name env vars ids_typ context_ids =
  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 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
    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 "++ 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

let _ =
  Goptions.declare_bool_option
    { Goptions.optsync  = true;
      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 _ _ _ _ _ -> "")
      ) }

let value = ref None

let _ =
  Goptions.declare_stringopt_option
    { Goptions.optsync  = true;
      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