session_itp.mli 4.21 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

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

22 23 24 25 26
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
27 28
val init_Hpn: session ->'a Hpn.t -> 'a -> unit
val init_Htn: session ->'a Htn.t -> 'a -> unit
29 30 31 32 33

type theory

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

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

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


48 49 50 51 52
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
53
  mutable proof_obsolete      : bool;
54 55
  proof_script        : string option;  (* non empty for external ITP *)
}
MARCHE Claude's avatar
MARCHE Claude committed
56

MARCHE Claude's avatar
MARCHE Claude committed
57

58
type proof_parent = Trans of transID | Theory of theory
59

60 61
val get_task : session -> proofNodeID -> Task.task

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

67 68 69
val get_transf_args : session -> transID -> string list
val get_transf_name : session -> transID -> string

70 71
val get_proof_name : session -> proofNodeID -> Ident.ident

72 73 74
val get_proof_parent : session -> proofNodeID -> proof_parent
val get_trans_parent : session -> transID -> proofNodeID

Clément Fumex's avatar
Clément Fumex committed
75 76 77
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
78 79

val add_file_section :
Clément Fumex's avatar
Clément Fumex committed
80 81 82 83
  ?merge:session*theory list*Env.env -> session -> string ->
  (Theory.theory list) -> Env.fformat option -> unit
(** [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
84 85 86
    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
87 88
    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
89

Clément Fumex's avatar
Clément Fumex committed
90 91 92 93
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
94
    [id]. If there already a proof attempt with the same prover,
Clément Fumex's avatar
Clément Fumex committed
95 96 97
    it updates it with the new timelimit. *)

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

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

Clément Fumex's avatar
Clément Fumex committed
109 110 111
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
112

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

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

120
val load_session : string -> session
Clément Fumex's avatar
Clément Fumex committed
121 122
(** [load_session dir] load a session in directory [dir]; all the
    tasks are initialised to None *)