db.mli 6.64 KB
Newer Older
MARCHE Claude's avatar
db  
MARCHE Claude committed
1 2 3
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
MARCHE Claude's avatar
MARCHE Claude committed
4 5 6
(*    François Bobot                                                     *)
(*    Jean-Christophe Filliâtre                                          *)
(*    Claude Marché                                                      *)
MARCHE Claude's avatar
db  
MARCHE Claude committed
7 8 9 10 11 12 13 14 15 16 17 18 19
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

20 21
open Why

MARCHE Claude's avatar
db  
MARCHE Claude committed
22 23
(** Proof database *)

24
(** {2 data types} *)
MARCHE Claude's avatar
db  
MARCHE Claude committed
25

MARCHE Claude's avatar
db  
MARCHE Claude committed
26 27 28 29 30 31 32 33 34 35
type prover_id
(** a prover identifier *)

module Hprover : Hashtbl.S with type key = prover_id

type transf_id
(** a transformation identifier *)

module Htransf : Hashtbl.S with type key = transf_id

36 37
type file
(** a database contains a (ordered?) set of files *)
MARCHE Claude's avatar
db  
MARCHE Claude committed
38

39 40 41 42 43 44
type theory
(** each files contains an ordered sequence of theories *)

type goal
(** each theory contains an ordered sequences of goals *)

45
type proof_attempt
46
(** each goal has a set of proof attempts, indeed a map indexed
MARCHE Claude's avatar
db  
MARCHE Claude committed
47
    by prover identifiers *)
48 49 50

type transf
(** each goal also has a set of transformations, indeed a map indexed
MARCHE Claude's avatar
db  
MARCHE Claude committed
51
    by transformation identifiers *)
52

MARCHE Claude's avatar
db  
MARCHE Claude committed
53 54 55

(** status of an external proof attempt *)
type proof_status =
MARCHE Claude's avatar
more db  
MARCHE Claude committed
56
  | Undone
MARCHE Claude's avatar
db  
MARCHE Claude committed
57 58 59 60 61
  | Success (** external proof attempt succeeded *)
  | Timeout (** external proof attempt was interrupted *)
  | Unknown (** external prover answered ``don't know'' or equivalent *)
  | Failure (** external prover call failed *)

62
(** parent of a goal: either a theory (for "toplevel" goals)
63 64
    or a transformation (for "subgoals") *)
(* useful ?
MARCHE Claude's avatar
db  
MARCHE Claude committed
65 66 67
type goal_parent =
  | Theory of theory
  | Transf of transf
68 69 70 71
*)

(** {2 accessors} *)

MARCHE Claude's avatar
db  
MARCHE Claude committed
72 73 74 75 76
(** prover_id accessors *)
val prover_name : prover_id -> string

(** transf_id accessors *)
val transf_name : transf_id -> string
MARCHE Claude's avatar
db  
MARCHE Claude committed
77 78

(** proof_attempt accessors *)
MARCHE Claude's avatar
MARCHE Claude committed
79
(*
MARCHE Claude's avatar
db  
MARCHE Claude committed
80
val prover : proof_attempt -> prover_id
MARCHE Claude's avatar
MARCHE Claude committed
81
*)
82
(*
MARCHE Claude's avatar
db  
MARCHE Claude committed
83
val proof_goal : proof_attempt -> goal
84
*)
85
val status_and_time :
MARCHE Claude's avatar
MARCHE Claude committed
86 87
  proof_attempt -> proof_status * float * bool * string
  (** returns (status, time, obsolete flag, edited file name) *)
MARCHE Claude's avatar
MARCHE Claude committed
88

MARCHE Claude's avatar
db  
MARCHE Claude committed
89 90 91
val edited_as : proof_attempt -> string

(** goal accessors *)
92
(*
MARCHE Claude's avatar
db  
MARCHE Claude committed
93
val parent : goal -> goal_parent
94
*)
MARCHE Claude's avatar
MARCHE Claude committed
95
val goal_name : goal -> string
96
val task_checksum : goal -> string (** checksum *)
MARCHE Claude's avatar
MARCHE Claude committed
97
(*
MARCHE Claude's avatar
db  
MARCHE Claude committed
98
val proved : goal -> bool
MARCHE Claude's avatar
MARCHE Claude committed
99
*)
MARCHE Claude's avatar
db  
MARCHE Claude committed
100 101
val external_proofs: goal -> proof_attempt Hprover.t
val transformations : goal -> transf Htransf.t
MARCHE Claude's avatar
db  
MARCHE Claude committed
102 103

(** transf accessors *)
104
(*
MARCHE Claude's avatar
db  
MARCHE Claude committed
105
val parent_goal : transf -> goal
106
*)
107
(*
MARCHE Claude's avatar
db  
MARCHE Claude committed
108
val transf_id : transf -> transf_id
109
*)
110
val subgoals : transf -> goal Util.Mstr.t
MARCHE Claude's avatar
db  
MARCHE Claude committed
111

112
(** theory accessors *)
MARCHE Claude's avatar
db  
MARCHE Claude committed
113
val theory_name : theory -> string
114
val goals : theory -> goal Util.Mstr.t
MARCHE Claude's avatar
MARCHE Claude committed
115
(*
MARCHE Claude's avatar
db  
MARCHE Claude committed
116
val verified : theory -> bool
MARCHE Claude's avatar
MARCHE Claude committed
117
*)
MARCHE Claude's avatar
db  
MARCHE Claude committed
118 119

(** file accessors *)
MARCHE Claude's avatar
MARCHE Claude committed
120
(*
MARCHE Claude's avatar
db  
MARCHE Claude committed
121
val file_name : file -> string
MARCHE Claude's avatar
MARCHE Claude committed
122
*)
123
val theories : file -> theory Util.Mstr.t
MARCHE Claude's avatar
db  
MARCHE Claude committed
124

125
(** {2 The persistent database} *)
MARCHE Claude's avatar
db  
MARCHE Claude committed
126 127 128 129

val init_base : string -> unit
(** opens or creates the current database, from given file name *)

MARCHE Claude's avatar
MARCHE Claude committed
130 131
val files : unit -> (file * string) list
(** returns the current set of files, with their filenames *)
MARCHE Claude's avatar
db  
MARCHE Claude committed
132 133


134 135 136 137
(** {2 Updates} *)

exception AlreadyExist

MARCHE Claude's avatar
db more  
MARCHE Claude committed
138
(** {3 prover id} *)
MARCHE Claude's avatar
db  
MARCHE Claude committed
139 140 141
val prover_from_name : string -> prover_id
(** retrieves existing prover id from its name.
    creates prover id if not existing yet *)
142

MARCHE Claude's avatar
db more  
MARCHE Claude committed
143 144 145 146 147
(** {3 transf id} *)
val transf_from_name : string -> transf_id
(** retrieves existing transformation id from its name.
    creates it if not existing yet *)

148 149
(** {3 external proof attempts} *)

MARCHE Claude's avatar
db  
MARCHE Claude committed
150
val add_proof_attempt : goal -> prover_id -> proof_attempt
151 152 153 154
(** adds a proof attempt for this prover, with status is set to Unknown.
    @raise AlreadyExist if an attempt for the same prover
    is already there *)

MARCHE Claude's avatar
MARCHE Claude committed
155
val remove_proof_attempt : proof_attempt -> unit
MARCHE Claude's avatar
MARCHE Claude committed
156 157
(** removes a proof attempt from the database *)
 
158 159 160
val set_obsolete : proof_attempt -> unit
(** marks this proof as obsolete *)

MARCHE Claude's avatar
MARCHE Claude committed
161 162 163 164
val set_status : proof_attempt -> proof_status -> float -> unit
(** set the proof status for this prover, and its time.
    also unset the obsolete flag *)

165
val set_edited_as : proof_attempt -> string -> unit
MARCHE Claude's avatar
MARCHE Claude committed
166
(** set the file name where this proof can be edited *)
167 168 169

(** {3 transformations} *)

MARCHE Claude's avatar
MARCHE Claude committed
170 171 172 173
val add_transformation : goal -> transf_id -> transf
(** adds a transformation for this goal.
    subgoals must be added afterwards by [add_subgoal]
    @raise AlreadyExist if a transformation with the same id
174 175
    is already there *)

MARCHE Claude's avatar
MARCHE Claude committed
176 177 178 179 180 181
val remove_transformation : transf -> unit 
  (** Removes a proof attempt from the database.  Beware that the
      subgoals are not removed by this function, you must remove them
      first using [remove_subgoal]. In other words, this function
      assumes there are no subgoals left under the transformation, but
      it does not protect against that. *)
182 183 184 185 186

(** {3 goals} *)

val add_goal : theory -> string -> string -> goal
(** [add_goal th id sum] adds to theory [th] a new goal named [id], with
187
    [sum] as the checksum of its task.
188 189 190
    @raise AlreadyExist if a goal with the same id already exists
    in this theory *)

MARCHE Claude's avatar
MARCHE Claude committed
191 192 193
val change_checksum: goal -> string -> unit
(** [change_checksum g sum] replaces checksum of [g] by [sum] *)

MARCHE Claude's avatar
MARCHE Claude committed
194 195
val add_subgoal : transf -> string -> string -> goal
(** [add_subgoal t id sum] adds to transf [t] a new subgoal named [id], with
196
    [sum] as the checksum of its task.
MARCHE Claude's avatar
MARCHE Claude committed
197 198 199
    @raise AlreadyExist if a goal with the same id already exists
    as subgoal of this transf *)

200 201 202 203
(* todo: remove_goal *)

(** {3 theories} *)

MARCHE Claude's avatar
MARCHE Claude committed
204 205 206 207
val add_theory : file -> string -> theory
(** [add_theory f id] adds to file f a theory named [th].
    @raise AlreadyExist if a theory with the same id already exists
    in this file *)
208 209 210 211 212 213

(* todo: remove_theory *)


(** {3 files} *)

214
val add_file :  string -> file
215 216 217 218 219 220
(** adds a file to the database.
    @raise AlreadyExist if a file with the same id already exists *)

(* todo: remove_file *)


MARCHE Claude's avatar
db  
MARCHE Claude committed
221 222 223



224

MARCHE Claude's avatar
MARCHE Claude committed
225 226 227 228 229 230

(*
Local Variables:
compile-command: "unset LANG; make -C ../.. bin/whyide.byte"
End:
*)