session_itp.mli 5.58 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
val dummy_session: session
20

Clément Fumex's avatar
Clément Fumex committed
21
type proofNodeID
MARCHE Claude's avatar
MARCHE Claude committed
22
val print_proofNodeID : Format.formatter -> proofNodeID -> unit
23
type transID
24
type proofAttemptID
25 26 27

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

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

type theory

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

42 43 44 45 46 47 48
type any =
  | AFile of file
  | ATh of theory
  | ATn of transID
  | APn of proofNodeID
  | APa of proofAttemptID

49 50 51 52 53
val theory_name : theory -> Ident.ident
val theory_goals : theory -> proofNodeID list
val theory_detached_goals : theory -> proofNodeID list
val theory_parent : session -> theory -> file

54
val get_files : session -> file Stdlib.Hstr.t
Clément Fumex's avatar
Clément Fumex committed
55 56
val get_dir : session -> string
val get_shape_version : session -> int
57

58 59
type proof_attempt_node = {
  parent              : proofNodeID;
60 61 62 63
  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
64
  mutable proof_obsolete      : bool;
65 66
  proof_script        : string option;  (* non empty for external ITP *)
}
MARCHE Claude's avatar
MARCHE Claude committed
67

68
val session_iter_proof_attempt: (proofNodeID -> proof_attempt_node -> unit) -> session -> unit
MARCHE Claude's avatar
MARCHE Claude committed
69

70
type proof_parent = Trans of transID | Theory of theory
71

72
val get_task : session -> proofNodeID -> Task.task
73
val get_tables: session -> proofNodeID -> Task.name_tables option
74

Clément Fumex's avatar
Clément Fumex committed
75
val get_transformations : session -> proofNodeID -> transID list
76 77
val get_proof_attempt_ids :
  session -> proofNodeID -> proofAttemptID Whyconf.Hprover.t
78
val get_proof_attempt_node : session -> proofAttemptID -> proof_attempt_node
MARCHE Claude's avatar
MARCHE Claude committed
79
val get_proof_attempt_parent : session -> proofAttemptID -> proofNodeID
80
val get_proof_attempts : session -> proofNodeID -> proof_attempt_node list
Clément Fumex's avatar
Clément Fumex committed
81
val get_sub_tasks : session -> transID -> proofNodeID list
Clément Fumex's avatar
Clément Fumex committed
82
val get_detached_sub_tasks : session -> transID -> proofNodeID list
MARCHE Claude's avatar
MARCHE Claude committed
83

84 85 86
val get_transf_args : session -> transID -> string list
val get_transf_name : session -> transID -> string

87 88
val get_proof_name : session -> proofNodeID -> Ident.ident

89 90 91
val get_proof_parent : session -> proofNodeID -> proof_parent
val get_trans_parent : session -> transID -> proofNodeID

Clément Fumex's avatar
Clément Fumex committed
92 93 94
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
95 96

val add_file_section :
97 98
  use_shapes:bool -> session -> string -> (Theory.theory list) ->
  Env.fformat option -> unit
Clément Fumex's avatar
Clément Fumex committed
99 100
(** [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
101
    subsections corresponding to theories [ths]. The tasks of each
102 103 104 105 106 107 108 109 110 111 112 113 114
    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
115

Clément Fumex's avatar
Clément Fumex committed
116
val graft_proof_attempt : session -> proofNodeID -> Whyconf.prover ->
117
  timelimit:int -> proofAttemptID
Clément Fumex's avatar
Clément Fumex committed
118 119
(** [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
120 121 122
    [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
123 124

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

129
val graft_transf : session -> proofNodeID -> string -> string list ->
Clément Fumex's avatar
Clément Fumex committed
130
  Task.task list -> transID
131
(** [graft_transf s id name l tl] adds the transformation [name] as a
Clément Fumex's avatar
Clément Fumex committed
132
    child of the task [id] of the session [s]. [l] is the list of
133
    arguments of the transformation, and [tl] is the list of subtasks.
Clément Fumex's avatar
Clément Fumex committed
134
*)
MARCHE Claude's avatar
MARCHE Claude committed
135

Clément Fumex's avatar
Clément Fumex committed
136 137 138
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
139

Clément Fumex's avatar
Clément Fumex committed
140 141 142
val remove_transformation : session -> transID -> unit
(** [remove_transformation s id] removes the transformation [id]
    from the session [s] *)
143

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

Clément Fumex's avatar
Clément Fumex committed
147
val load_session : string -> session * bool
Clément Fumex's avatar
Clément Fumex committed
148
(** [load_session dir] load a session in directory [dir]; all the
Clément Fumex's avatar
Clément Fumex committed
149 150 151 152 153 154 155 156 157 158
    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.
 *)