session_itp.mli 5.27 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
val print_proofNodeID : Format.formatter -> proofNodeID -> unit
22
type transID
23
type proofAttemptID
24 25 26

module Hpn: Exthtbl.S with type key = proofNodeID
module Htn: Exthtbl.S with type key = transID
27
module Hpan: Exthtbl.S with type key = proofAttemptID
28

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

type theory

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

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

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


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

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

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

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

Clément Fumex's avatar
Clément Fumex committed
65
val get_transformations : session -> proofNodeID -> transID list
66 67
val get_proof_attempt_ids :
  session -> proofNodeID -> proofAttemptID Whyconf.Hprover.t
MARCHE Claude's avatar
MARCHE Claude committed
68 69
val get_proof_attempt : session -> proofAttemptID -> proof_attempt
val get_proof_attempt_parent : session -> proofAttemptID -> proofNodeID
70
val get_proof_attempts : session -> proofNodeID -> proof_attempt list
Clément Fumex's avatar
Clément Fumex committed
71
val get_sub_tasks : session -> transID -> proofNodeID list
Clément Fumex's avatar
Clément Fumex committed
72
val get_detached_sub_tasks : session -> transID -> proofNodeID list
MARCHE Claude's avatar
MARCHE Claude committed
73

74 75 76
val get_transf_args : session -> transID -> string list
val get_transf_name : session -> transID -> string

77 78
val get_proof_name : session -> proofNodeID -> Ident.ident

79 80 81
val get_proof_parent : session -> proofNodeID -> proof_parent
val get_trans_parent : session -> transID -> proofNodeID

Clément Fumex's avatar
Clément Fumex committed
82 83 84
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
85 86

val add_file_section :
87 88
  use_shapes:bool -> session -> string -> (Theory.theory list) ->
  Env.fformat option -> unit
Clément Fumex's avatar
Clément Fumex committed
89 90
(** [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
91
    subsections corresponding to theories [ths]. The tasks of each
92 93 94 95 96 97 98 99 100 101 102 103 104
    theory nodes generated are computed using [Task.split_theory]. *)

val merge_file_section :
  use_shapes:bool -> old_ses:session -> old_theories:theory list ->
  env:Env.env -> session -> string -> Theory.theory list ->
  Env.fformat option -> unit
(** [merge_file_section ~old_s ~old_theories ~env ~pn_callpack s fn
    ths] adds a new 'file' section in session [s], named [fn],
    containing fresh theory subsections corresponding to theories
    [ths]. For each theory whose name is identical to one theory of
    old_ths, it 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
105

Clément Fumex's avatar
Clément Fumex committed
106
val graft_proof_attempt : session -> proofNodeID -> Whyconf.prover ->
107
  timelimit:int -> proofAttemptID
Clément Fumex's avatar
Clément Fumex committed
108 109
(** [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
110 111 112
    [id]. If there already a proof attempt with the same prover, it
    updates it with the new timelimit. It returns the id of the
    generated proof attempt. *)
Clément Fumex's avatar
Clément Fumex committed
113 114

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

119
val graft_transf : session -> proofNodeID -> string -> string list ->
Clément Fumex's avatar
Clément Fumex committed
120
  Task.task list -> transID
121
(** [graft_transf s id name l tl] adds the transformation [name] as a
Clément Fumex's avatar
Clément Fumex committed
122
    child of the task [id] of the session [s]. [l] is the list of
123
    arguments of the transformation, and [tl] is the list of subtasks.
Clément Fumex's avatar
Clément Fumex committed
124
*)
MARCHE Claude's avatar
MARCHE Claude committed
125

Clément Fumex's avatar
Clément Fumex committed
126 127 128
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
129

Clément Fumex's avatar
Clément Fumex committed
130 131 132
val remove_transformation : session -> transID -> unit
(** [remove_transformation s id] removes the transformation [id]
    from the session [s] *)
133

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

Clément Fumex's avatar
Clément Fumex committed
137
val load_session : string -> session * bool
Clément Fumex's avatar
Clément Fumex committed
138
(** [load_session dir] load a session in directory [dir]; all the
Clément Fumex's avatar
Clément Fumex committed
139 140 141 142 143 144 145 146 147 148
    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.
 *)