db.mli 7.4 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
(* autogenerated by sql_orm *)
(** Use the [[Init]] module to open a new database handle.  Each object type has its own module with functions to create, modify, save and destroy objects of that type into the SQLite database
  *)
module Init : sig
  type t
  type transaction_mode = [`Exclusive |`Deferred |`Immediate ]
  (** Database handle which can be used to create and retrieve objects
    *)
  val t :
    ?busyfn:(Sqlite3.db -> unit) -> ?mode:transaction_mode ->
    string -> t
  (** [t db_name] open a Sqlite3 database with filename [db_name] and create any tables if they are missing. @return a database handle which can be used to create and retrieve objects in the database.
   @raise Sql_error if a database error is encountered
    *)
  val db: t -> Sqlite3.db
  (** [db handle] @return the underlying Sqlite3 database handle for the connection, for advanced queries.
    *)
end
MARCHE Claude's avatar
db    
MARCHE Claude committed
19
module Loc : sig
MARCHE Claude's avatar
MARCHE Claude committed
20
21
22
  type t = <
    id : int64 option;
    set_id : int64 option -> unit;
MARCHE Claude's avatar
db    
MARCHE Claude committed
23
24
25
26
27
28
29
30
    file : string;
    set_file : string -> unit;
    line : int64;
    set_line : int64 -> unit;
    start : int64;
    set_start : int64 -> unit;
    stop : int64;
    set_stop : int64 -> unit;
MARCHE Claude's avatar
MARCHE Claude committed
31
32
33
34
35
36
37
38
    save: int64; delete: unit
  >

  (** An object which can be stored in the database with the [save] method call, or removed by calling [delete].  Fields can be accessed via the approriate named method and set via the [set_] methods.  Changes are not committed to the database until [save] is invoked.
    *)

  val t :
    ?id:int64 option ->
MARCHE Claude's avatar
db    
MARCHE Claude committed
39
40
41
42
    file:string ->
    line:int64 ->
    start:int64 ->
    stop:int64 ->
MARCHE Claude's avatar
MARCHE Claude committed
43
44
45
46
47
48
49
    Init.t -> t
  (** Can be used to construct a new object.  If [id] is not specified, it will be automatically assigned the first time [save] is called on the object.  The object is not committed to the database until [save] is invoked.  The [save] method will also return the [id] assigned to the object.
   @raise Sql_error if a database error is encountered
    *)

  val get :
    ?id:int64 option ->
MARCHE Claude's avatar
db    
MARCHE Claude committed
50
51
52
53
    ?file:string option ->
    ?line:int64 option ->
    ?start:int64 option ->
    ?stop:int64 option ->
MARCHE Claude's avatar
MARCHE Claude committed
54
55
56
57
58
59
    ?custom_where:string * Sqlite3.Data.t list -> Init.t -> t list
  (** Used to retrieve objects from the database.  If an argument is specified, it is included in the search criteria (all fields are ANDed together).
   @raise Sql_error if a database error is encountered
    *)

end
MARCHE Claude's avatar
db    
MARCHE Claude committed
60
module External_proof : sig
MARCHE Claude's avatar
MARCHE Claude committed
61
62
63
  type t = <
    id : int64 option;
    set_id : int64 option -> unit;
MARCHE Claude's avatar
db    
MARCHE Claude committed
64
65
66
67
68
69
70
71
72
73
74
75
76
77
    prover : string;
    set_prover : string -> unit;
    timelimit : int64;
    set_timelimit : int64 -> unit;
    memlimit : int64;
    set_memlimit : int64 -> unit;
    status : int64;
    set_status : int64 -> unit;
    result_time : float;
    set_result_time : float -> unit;
    trace : string;
    set_trace : string -> unit;
    obsolete : int64;
    set_obsolete : int64 -> unit;
MARCHE Claude's avatar
MARCHE Claude committed
78
79
80
81
82
83
84
85
    save: int64; delete: unit
  >

  (** An object which can be stored in the database with the [save] method call, or removed by calling [delete].  Fields can be accessed via the approriate named method and set via the [set_] methods.  Changes are not committed to the database until [save] is invoked.
    *)

  val t :
    ?id:int64 option ->
MARCHE Claude's avatar
db    
MARCHE Claude committed
86
87
88
89
90
91
92
    prover:string ->
    timelimit:int64 ->
    memlimit:int64 ->
    status:int64 ->
    result_time:float ->
    trace:string ->
    obsolete:int64 ->
MARCHE Claude's avatar
MARCHE Claude committed
93
94
95
96
97
98
99
    Init.t -> t
  (** Can be used to construct a new object.  If [id] is not specified, it will be automatically assigned the first time [save] is called on the object.  The object is not committed to the database until [save] is invoked.  The [save] method will also return the [id] assigned to the object.
   @raise Sql_error if a database error is encountered
    *)

  val get :
    ?id:int64 option ->
MARCHE Claude's avatar
db    
MARCHE Claude committed
100
101
102
103
104
105
106
    ?prover:string option ->
    ?timelimit:int64 option ->
    ?memlimit:int64 option ->
    ?status:int64 option ->
    ?result_time:float option ->
    ?trace:string option ->
    ?obsolete:int64 option ->
MARCHE Claude's avatar
MARCHE Claude committed
107
108
109
110
111
112
    ?custom_where:string * Sqlite3.Data.t list -> Init.t -> t list
  (** Used to retrieve objects from the database.  If an argument is specified, it is included in the search criteria (all fields are ANDed together).
   @raise Sql_error if a database error is encountered
    *)

end
MARCHE Claude's avatar
MARCHE Claude committed
113
module Goal : sig
MARCHE Claude's avatar
MARCHE Claude committed
114
115
116
  type t = <
    id : int64 option;
    set_id : int64 option -> unit;
MARCHE Claude's avatar
db    
MARCHE Claude committed
117
118
119
120
121
122
123
124
125
126
127
128
129
130
    task_checksum : string;
    set_task_checksum : string -> unit;
    parent : Transf.t;
    set_parent : Transf.t -> unit;
    name : string;
    set_name : string -> unit;
    pos : Loc.t;
    set_pos : Loc.t -> unit;
    external_proofs : External_proof.t list;
    set_external_proofs : External_proof.t list -> unit;
    transformations : Transf.t list;
    set_transformations : Transf.t list -> unit;
    proved : int64;
    set_proved : int64 -> unit;
MARCHE Claude's avatar
MARCHE Claude committed
131
132
133
134
135
136
137
138
    save: int64; delete: unit
  >

  (** An object which can be stored in the database with the [save] method call, or removed by calling [delete].  Fields can be accessed via the approriate named method and set via the [set_] methods.  Changes are not committed to the database until [save] is invoked.
    *)

  val t :
    ?id:int64 option ->
MARCHE Claude's avatar
db    
MARCHE Claude committed
139
140
141
142
143
144
145
    task_checksum:string ->
    parent:Transf.t ->
    name:string ->
    pos:Loc.t ->
    external_proofs:External_proof.t list ->
    transformations:Transf.t list ->
    proved:int64 ->
MARCHE Claude's avatar
MARCHE Claude committed
146
147
148
149
150
151
152
    Init.t -> t
  (** Can be used to construct a new object.  If [id] is not specified, it will be automatically assigned the first time [save] is called on the object.  The object is not committed to the database until [save] is invoked.  The [save] method will also return the [id] assigned to the object.
   @raise Sql_error if a database error is encountered
    *)

  val get :
    ?id:int64 option ->
MARCHE Claude's avatar
db    
MARCHE Claude committed
153
154
155
    ?task_checksum:string option ->
    ?name:string option ->
    ?proved:int64 option ->
MARCHE Claude's avatar
MARCHE Claude committed
156
157
158
159
160
161
    ?custom_where:string * Sqlite3.Data.t list -> Init.t -> t list
  (** Used to retrieve objects from the database.  If an argument is specified, it is included in the search criteria (all fields are ANDed together).
   @raise Sql_error if a database error is encountered
    *)

end
MARCHE Claude's avatar
MARCHE Claude committed
162
module Transf : sig
MARCHE Claude's avatar
MARCHE Claude committed
163
164
165
  type t = <
    id : int64 option;
    set_id : int64 option -> unit;
MARCHE Claude's avatar
db    
MARCHE Claude committed
166
167
168
169
170
171
    name : string;
    set_name : string -> unit;
    obsolete : int64;
    set_obsolete : int64 -> unit;
    subgoals : Goal.t list;
    set_subgoals : Goal.t list -> unit;
MARCHE Claude's avatar
MARCHE Claude committed
172
173
174
175
176
177
178
179
    save: int64; delete: unit
  >

  (** An object which can be stored in the database with the [save] method call, or removed by calling [delete].  Fields can be accessed via the approriate named method and set via the [set_] methods.  Changes are not committed to the database until [save] is invoked.
    *)

  val t :
    ?id:int64 option ->
MARCHE Claude's avatar
db    
MARCHE Claude committed
180
181
182
    name:string ->
    obsolete:int64 ->
    subgoals:Goal.t list ->
MARCHE Claude's avatar
MARCHE Claude committed
183
184
185
186
187
188
189
    Init.t -> t
  (** Can be used to construct a new object.  If [id] is not specified, it will be automatically assigned the first time [save] is called on the object.  The object is not committed to the database until [save] is invoked.  The [save] method will also return the [id] assigned to the object.
   @raise Sql_error if a database error is encountered
    *)

  val get :
    ?id:int64 option ->
MARCHE Claude's avatar
db    
MARCHE Claude committed
190
191
    ?name:string option ->
    ?obsolete:int64 option ->
MARCHE Claude's avatar
MARCHE Claude committed
192
193
194
195
196
197
    ?custom_where:string * Sqlite3.Data.t list -> Init.t -> t list
  (** Used to retrieve objects from the database.  If an argument is specified, it is included in the search criteria (all fields are ANDed together).
   @raise Sql_error if a database error is encountered
    *)

end