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 5.67 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 54 55 56 57 58

(** status of an external proof attempt *)
type proof_status =
  | 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 *)

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

(** {2 accessors} *)

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

(** proof_attempt accessors *)
MARCHE Claude's avatar
db  
MARCHE Claude committed
76
val prover : proof_attempt -> prover_id
77
(*
MARCHE Claude's avatar
db  
MARCHE Claude committed
78
val proof_goal : proof_attempt -> goal
79
*)
MARCHE Claude's avatar
db  
MARCHE Claude committed
80 81 82 83 84 85
val status : proof_attempt -> proof_status
val proof_obsolete : proof_attempt -> bool
val time : proof_attempt -> float
val edited_as : proof_attempt -> string

(** goal accessors *)
86
(*
MARCHE Claude's avatar
db  
MARCHE Claude committed
87
val parent : goal -> goal_parent
88 89
*)
val task_checksum : goal -> string (** checksum *)
MARCHE Claude's avatar
db  
MARCHE Claude committed
90
val proved : goal -> bool
MARCHE Claude's avatar
db  
MARCHE Claude committed
91 92
val external_proofs: goal -> proof_attempt Hprover.t
val transformations : goal -> transf Htransf.t
MARCHE Claude's avatar
db  
MARCHE Claude committed
93 94

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

(** theory accessors *)        
val theory_name : theory -> string
val goals : theory -> goal list
val verified : theory -> bool

(** file accessors *)
val file_name : file -> string
val theories : file -> theory list

110
(** {2 The persistent database} *)
MARCHE Claude's avatar
db  
MARCHE Claude committed
111 112 113 114 115 116 117 118

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

val files : unit -> file list
(** returns the current set of files *)


119 120 121 122
(** {2 Updates} *)

exception AlreadyExist

MARCHE Claude's avatar
db more  
MARCHE Claude committed
123
(** {3 prover id} *)
MARCHE Claude's avatar
db  
MARCHE Claude committed
124 125 126
val prover_from_name : string -> prover_id
(** retrieves existing prover id from its name.
    creates prover id if not existing yet *)
127

MARCHE Claude's avatar
db more  
MARCHE Claude committed
128 129 130 131 132
(** {3 transf id} *)
val transf_from_name : string -> transf_id
(** retrieves existing transformation id from its name.
    creates it if not existing yet *)

133 134
(** {3 external proof attempts} *)

MARCHE Claude's avatar
db  
MARCHE Claude committed
135
val add_proof_attempt : goal -> prover_id -> proof_attempt
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 171 172 173 174 175 176 177 178 179 180 181 182 183
(** 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_status : proof_attempt -> proof_status -> float -> unit
(** sets the proof status for this prover, and its time.
*)

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

val set_edited_as : proof_attempt -> string -> unit
(** sets the file name where this proof can be edited *)

(** {3 transformations} *)

val add_transformation : goal -> string -> goal list -> transf
(** adds a transformation for this goal, with the given subgoals
    @raise AlreadyExist if a transformation with the same name
    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 *)

(* todo: remove_goal *)

(** {3 theories} *)

val add_theory : file -> string -> string -> unit
(** [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 *)

(* todo: remove_theory *)


(** {3 files} *)

MARCHE Claude's avatar
d  
MARCHE Claude committed
184
val add_file :  string -> file 
185 186 187 188 189 190
(** 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
191 192 193 194