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.13 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 43 44
type theory
(** each files contains an ordered sequence of theories *)

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

type proof_attempt 
(** 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 61 62
(** parent of a goal: either a theory (for "toplevel" goals) 
    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
*)
MARCHE Claude's avatar
MARCHE Claude committed
83 84 85
val status_and_time : proof_attempt -> proof_status * float * bool
  (* returns status, time and the obsolete flag *)

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

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

(** transf accessors *)
101
(*
MARCHE Claude's avatar
db  
MARCHE Claude committed
102
val parent_goal : transf -> goal
103
*)
MARCHE Claude's avatar
db  
MARCHE Claude committed
104
val transf_id : transf -> transf_id
MARCHE Claude's avatar
db  
MARCHE Claude committed
105 106 107 108
val subgoals : transf -> goal list

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

(** file accessors *)
MARCHE Claude's avatar
MARCHE Claude committed
115
(*
MARCHE Claude's avatar
db  
MARCHE Claude committed
116
val file_name : file -> string
MARCHE Claude's avatar
MARCHE Claude committed
117
*)
MARCHE Claude's avatar
db  
MARCHE Claude committed
118 119
val theories : file -> theory list

120
(** {2 The persistent database} *)
MARCHE Claude's avatar
db  
MARCHE Claude committed
121 122 123 124

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

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


129 130 131 132
(** {2 Updates} *)

exception AlreadyExist

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

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

143 144
(** {3 external proof attempts} *)

MARCHE Claude's avatar
db  
MARCHE Claude committed
145
val add_proof_attempt : goal -> prover_id -> proof_attempt
146 147 148 149 150 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 *)

(* todo: remove_proof_attempt *)

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

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

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

(** {3 transformations} *)

MARCHE Claude's avatar
MARCHE Claude committed
164 165 166 167
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
168 169 170 171 172 173 174 175 176 177 178 179
    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
    [sum] as the checksum of its task. 
    @raise AlreadyExist if a goal with the same id already exists
    in this theory *)

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

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

189 190 191 192
(* todo: remove_goal *)

(** {3 theories} *)

MARCHE Claude's avatar
MARCHE Claude committed
193 194 195 196
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 *)
197 198 199 200 201 202

(* todo: remove_theory *)


(** {3 files} *)

MARCHE Claude's avatar
d  
MARCHE Claude committed
203
val add_file :  string -> file 
204 205 206 207 208 209
(** 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
210 211 212 213