module Why3_session: sig
.. end
Not mutated after the creation
From the original file we kept only the reading of a session.
We also discard all the information about how that have been proved
(metas, transformation, proof_attempts) or the order of the goals
module S: Datatype.String
module Xml: Why3_xml
type
goal = {
|
goal_name : string ; |
|
goal_parent : theory ; |
|
mutable goal_verified : bool ; |
}
type
theory = {
|
theory_name : string ; |
|
theory_parent : file ; |
|
theory_goals : goal Datatype.String.Hashtbl.t ; |
|
mutable theory_verified : bool ; |
}
type
file = {
|
file_name : string ; |
|
file_format : string option ; |
|
file_parent : session ; |
|
file_theories : theory Datatype.String.Hashtbl.t ; |
|
mutable file_verified : bool ; |
}
type
session = {
|
session_files : file Datatype.String.Hashtbl.t ; |
|
session_dir : string ; |
}
val db_filename : string
2 Create a session
val session_dir_for_save : string Pervasives.ref
val empty_session : string -> session
val raw_add_no_task : theory -> S.Hashtbl.key -> goal
val raw_add_theory : file -> S.Hashtbl.key -> theory
val raw_add_file : session ->
S.Hashtbl.key -> string option -> file
exception LoadError
Read/Write
val bool_attribute : string -> Xml.element -> bool -> bool
val int_attribute_def : string -> Xml.element -> int -> int
val int_attribute : string -> Xml.element -> int
val string_attribute_def : string -> Xml.element -> string -> string
val string_attribute : string -> Xml.element -> string
val load_option : string -> Xml.element -> string option
val load_ident : Xml.element -> string
val load_goal : theory -> Xml.element -> unit
val load_theory : file -> Xml.element -> unit
val load_file : session -> Xml.element -> unit
val load_session : session -> Xml.element -> unit
type
notask = unit
val read_session : string -> session
Read a session stored on the disk. It returns a session without any
task attached to goals