Mise à jour terminée. Pour connaître les apports de la version 13.8.4 par rapport à notre ancienne version vous pouvez lire les "Release Notes" suivantes :
https://about.gitlab.com/releases/2021/02/11/security-release-gitlab-13-8-4-released/
https://about.gitlab.com/releases/2021/02/05/gitlab-13-8-3-released/

db.mli 6.76 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
  | 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 *)
61
  
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 *)

130 131 132 133
val is_initialized : unit -> bool
(** [is_initialized ()] is true if init_base as been called
    succesively previously *)

MARCHE Claude's avatar
MARCHE Claude committed
134 135
val files : unit -> (file * string) list
(** returns the current set of files, with their filenames *)
MARCHE Claude's avatar
db  
MARCHE Claude committed
136 137


138 139 140 141
(** {2 Updates} *)

exception AlreadyExist

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

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

152 153
(** {3 external proof attempts} *)

MARCHE Claude's avatar
db  
MARCHE Claude committed
154
val add_proof_attempt : goal -> prover_id -> proof_attempt
155 156 157 158
(** 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
159
val remove_proof_attempt : proof_attempt -> unit
MARCHE Claude's avatar
MARCHE Claude committed
160 161
(** removes a proof attempt from the database *)
 
162 163 164
val set_obsolete : proof_attempt -> unit
(** marks this proof as obsolete *)

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

169
val set_edited_as : proof_attempt -> string -> unit
MARCHE Claude's avatar
MARCHE Claude committed
170
(** set the file name where this proof can be edited *)
171 172 173

(** {3 transformations} *)

MARCHE Claude's avatar
MARCHE Claude committed
174 175 176 177
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
178 179
    is already there *)

MARCHE Claude's avatar
MARCHE Claude committed
180 181 182 183 184 185
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. *)
186 187 188 189 190

(** {3 goals} *)

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

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

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

204 205 206 207
(* todo: remove_goal *)

(** {3 theories} *)

MARCHE Claude's avatar
MARCHE Claude committed
208 209 210 211
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 *)
212 213 214 215 216 217

(* todo: remove_theory *)


(** {3 files} *)

218
val add_file :  string -> file
219 220 221 222 223 224
(** 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
225 226 227



228

MARCHE Claude's avatar
MARCHE Claude committed
229 230 231 232 233 234

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