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.26 KB
Newer Older
MARCHE Claude's avatar
db  
MARCHE Claude committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
(*    Francois Bobot                                                      *)
(*    Jean-Christophe Filliatre                                           *)
(*    Johannes Kanig                                                      *)
(*    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.                  *)
(*                                                                        *)
(**************************************************************************)

(** Proof database *)

22
(** {2 data types} *)
MARCHE Claude's avatar
db  
MARCHE Claude committed
23

MARCHE Claude's avatar
db  
MARCHE Claude committed
24 25 26 27 28 29 30 31 32 33
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

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

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

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

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

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

MARCHE Claude's avatar
db  
MARCHE Claude committed
51 52 53

(** status of an external proof attempt *)
type proof_status =
MARCHE Claude's avatar
more db  
MARCHE Claude committed
54
  | Undone
MARCHE Claude's avatar
db  
MARCHE Claude committed
55 56 57 58 59
  | 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 *)

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

(** {2 accessors} *)

MARCHE Claude's avatar
db  
MARCHE Claude committed
70 71 72 73 74
(** 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
75 76

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

MARCHE Claude's avatar
db  
MARCHE Claude committed
87 88 89
val edited_as : proof_attempt -> string

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

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

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

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

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

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

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


132 133 134 135
(** {2 Updates} *)

exception AlreadyExist

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

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

146 147
(** {3 external proof attempts} *)

MARCHE Claude's avatar
db  
MARCHE Claude committed
148
val add_proof_attempt : goal -> prover_id -> proof_attempt
149 150 151 152 153 154 155 156 157
(** 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 *)

(* todo: remove_proof_attempt *)

val set_obsolete : proof_attempt -> unit
(** marks this proof as obsolete *)

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

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

(** {3 transformations} *)

MARCHE Claude's avatar
MARCHE Claude committed
167 168 169 170
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
171 172 173 174 175 176 177 178
    is already there *)

(* todo: remove_transformation *)

(** {3 goals} *)

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

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

MARCHE Claude's avatar
MARCHE Claude committed
186 187
val add_subgoal : transf -> string -> string -> goal
(** [add_subgoal t id sum] adds to transf [t] a new subgoal named [id], with
188
    [sum] as the checksum of its task.
MARCHE Claude's avatar
MARCHE Claude committed
189 190 191
    @raise AlreadyExist if a goal with the same id already exists
    as subgoal of this transf *)

192 193 194 195
(* todo: remove_goal *)

(** {3 theories} *)

MARCHE Claude's avatar
MARCHE Claude committed
196 197 198 199
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 *)
200 201 202 203 204 205

(* todo: remove_theory *)


(** {3 files} *)

206
val add_file :  string -> file
207 208 209 210 211 212
(** 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
213 214 215



216

MARCHE Claude's avatar
MARCHE Claude committed
217 218 219 220 221 222

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