session_itp.mli 4.57 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16




(** {1 New Proof sessions ("Refectoire")} *)


(** {2 upper level structure of sessions}

   A [session] contains a collection of files, a [file] contains a
collection of theories, a [theory] contains a collection of goals. The
structure of goals remain abstract, each goal being identified by
unique identifiers of type [proofNodeId]

*)

Clément Fumex's avatar
Clément Fumex committed
17
type session
18

19

Clément Fumex's avatar
Clément Fumex committed
20
type proofNodeID
MARCHE Claude's avatar
MARCHE Claude committed
21 22
val print_proofNodeID : Format.formatter -> proofNodeID -> unit

23 24 25 26 27
type transID

module Hpn: Exthtbl.S with type key = proofNodeID
module Htn: Exthtbl.S with type key = transID

Clément Fumex's avatar
Clément Fumex committed
28 29
val init_Hpn: session ->'a Hpn.t -> 'a -> unit
val init_Htn: session ->'a Htn.t -> 'a -> unit
30 31 32 33 34

type theory

val theory_name : theory -> Ident.ident
val theory_goals : theory -> proofNodeID list
Clément Fumex's avatar
Clément Fumex committed
35
val theory_detached_goals : theory -> proofNodeID list
36 37

type file = private {
Clément Fumex's avatar
Clément Fumex committed
38 39 40 41
  file_name              : string;
  file_format            : string option;
  file_theories          : theory list;
  file_detached_theories : theory list;
42 43 44
}

val get_files : session -> file Stdlib.Hstr.t
Clément Fumex's avatar
Clément Fumex committed
45 46
val get_dir : session -> string
val get_shape_version : session -> int
47 48


49 50 51 52 53
type proof_attempt = {
  prover              : Whyconf.prover;
  limit               : Call_provers.resource_limit;
  mutable proof_state : Call_provers.prover_result option;
  (* None means that the call was not done or never returned *)
Clément Fumex's avatar
Clément Fumex committed
54
  mutable proof_obsolete      : bool;
55 56
  proof_script        : string option;  (* non empty for external ITP *)
}
MARCHE Claude's avatar
MARCHE Claude committed
57

58
val session_iter_proof_attempt: (proofNodeID -> proof_attempt -> unit) -> session -> unit
MARCHE Claude's avatar
MARCHE Claude committed
59

60
type proof_parent = Trans of transID | Theory of theory
61

62 63
val get_task : session -> proofNodeID -> Task.task

Clément Fumex's avatar
Clément Fumex committed
64
val get_transformations : session -> proofNodeID -> transID list
65
val get_proof_attempts : session -> proofNodeID -> proof_attempt list
Clément Fumex's avatar
Clément Fumex committed
66
val get_sub_tasks : session -> transID -> proofNodeID list
Clément Fumex's avatar
Clément Fumex committed
67
val get_detached_sub_tasks : session -> transID -> proofNodeID list
MARCHE Claude's avatar
MARCHE Claude committed
68

69 70 71
val get_transf_args : session -> transID -> string list
val get_transf_name : session -> transID -> string

72 73
val get_proof_name : session -> proofNodeID -> Ident.ident

74 75 76
val get_proof_parent : session -> proofNodeID -> proof_parent
val get_trans_parent : session -> transID -> proofNodeID

Clément Fumex's avatar
Clément Fumex committed
77 78 79
val empty_session : ?shape_version:int -> string -> session
(** create an empty_session in the directory specified by the
    argument *)
MARCHE Claude's avatar
MARCHE Claude committed
80 81

val add_file_section :
Clément Fumex's avatar
Clément Fumex committed
82 83
  use_shapes:bool -> ?merge:session*theory list*Env.env -> session ->
  string -> (Theory.theory list) -> Env.fformat option -> unit
Clément Fumex's avatar
Clément Fumex committed
84 85
(** [add_file_section ~merge:(old_s,old_ths,env) s fn ths] adds a new
    'file' section in session [s], named [fn], containing fresh theory
MARCHE Claude's avatar
MARCHE Claude committed
86 87 88
    subsections corresponding to theories [ths]. The tasks of each
    theory nodes generated are computed using [Task.split_theory]. For
    each theory whose name is identical to one theory of old_ths, it
Clément Fumex's avatar
Clément Fumex committed
89 90
    is attempted to associate the old goals, proof_attempts and
    transformations to the goals of the new theory *)
MARCHE Claude's avatar
MARCHE Claude committed
91

Clément Fumex's avatar
Clément Fumex committed
92 93 94 95
val graft_proof_attempt : session -> proofNodeID -> Whyconf.prover ->
  timelimit:int -> unit
(** [graft_proof_attempt s id pr t] adds a proof attempt with prover
    [pr] and timelimit [t] in the session [s] as a child of the task
96
    [id]. If there already a proof attempt with the same prover,
Clément Fumex's avatar
Clément Fumex committed
97 98 99
    it updates it with the new timelimit. *)

val update_proof_attempt : session -> proofNodeID -> Whyconf.prover ->
100
  Call_provers.prover_result -> unit
Clément Fumex's avatar
Clément Fumex committed
101 102
(** [update_proof_attempt s id pr st] update the status of the
    corresponding proof attempt with [st]. *)
MARCHE Claude's avatar
MARCHE Claude committed
103

104
val graft_transf : session -> proofNodeID -> string -> string list ->
Clément Fumex's avatar
Clément Fumex committed
105
  Task.task list -> transID
106
(** [graft_transf s id name l tl] adds the transformation [name] as a
Clément Fumex's avatar
Clément Fumex committed
107
    child of the task [id] of the session [s]. [l] is the list of
108
    arguments of the transformation, and [tl] is the list of subtasks.
Clément Fumex's avatar
Clément Fumex committed
109
*)
MARCHE Claude's avatar
MARCHE Claude committed
110

Clément Fumex's avatar
Clément Fumex committed
111 112 113
val remove_proof_attempt : session -> proofNodeID -> Whyconf.prover -> unit
(** [remove_proof_attempt s id pr] removes the proof attempt from the
    prover [pr] from the proof node [id] of the session [s] *)
MARCHE Claude's avatar
MARCHE Claude committed
114

Clément Fumex's avatar
Clément Fumex committed
115 116 117
val remove_transformation : session -> transID -> unit
(** [remove_transformation s id] removes the transformation [id]
    from the session [s] *)
118

Clément Fumex's avatar
Clément Fumex committed
119 120
val save_session : session -> unit
(** [save_session s] Save the session [s] *)
MARCHE Claude's avatar
MARCHE Claude committed
121

Clément Fumex's avatar
Clément Fumex committed
122
val load_session : string -> session * bool
Clément Fumex's avatar
Clément Fumex committed
123
(** [load_session dir] load a session in directory [dir]; all the
Clément Fumex's avatar
Clément Fumex committed
124 125 126 127 128 129 130 131 132 133
    tasks are initialised to None

    The returned boolean is set when there was shapes read from disk.

    raises [SessionFileError msg] if the database file cannot be read
    correctly.

    raises [ShapesFileError msg] if the database extra file for shapes
    cannot be read.
 *)