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

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

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

type theory

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

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

47 48 49 50 51
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

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

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

66 67
val session_iter_proof_attempt:
    (proofAttemptID -> proof_attempt_node -> unit) -> session -> unit
MARCHE Claude's avatar
MARCHE Claude committed
68

Sylvain Dailler's avatar
Sylvain Dailler committed
69 70 71
(* [is_below s a b] true if a is below b in the session tree *)
val is_below: session -> any -> any -> bool

72
type proof_parent = Trans of transID | Theory of theory
73

74
val get_task : session -> proofNodeID -> Task.task
75
val get_table : session -> proofNodeID -> Task.names_table option
76

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

86 87 88
val get_transf_args : session -> transID -> string list
val get_transf_name : session -> transID -> string

89 90
val get_proof_name : session -> proofNodeID -> Ident.ident

91 92 93
val get_proof_parent : session -> proofNodeID -> proof_parent
val get_trans_parent : session -> transID -> proofNodeID

94
val get_detached_trans : session -> proofNodeID -> transID list
Sylvain Dailler's avatar
Sylvain Dailler committed
95 96
val get_any_parent: session -> any -> any option

97 98 99
(* Answers true if a node is in a detached subtree *)
val is_detached: session -> any -> bool

100
exception BadCopyDetached of string
Sylvain Dailler's avatar
Sylvain Dailler committed
101 102 103 104 105

(** [copy s pn] copy pn and add the copy as detached subgoal of its parent *)
val copy_proof_node_as_detached: session -> proofNodeID -> proofNodeID
val copy_structure: notification:(parent:any -> any -> unit) -> session -> any -> any -> unit

Clément Fumex's avatar
Clément Fumex committed
106 107 108
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
109 110

val add_file_section :
111
  session -> string -> (Theory.theory list) ->
112
  Env.fformat option -> unit
113
(** [add_file_section s fn ths] adds a new
Clément Fumex's avatar
Clément Fumex committed
114
    'file' section in session [s], named [fn], containing fresh theory
MARCHE Claude's avatar
MARCHE Claude committed
115
    subsections corresponding to theories [ths]. The tasks of each
116 117 118 119 120 121 122 123 124 125 126 127 128
    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
129

Clément Fumex's avatar
Clément Fumex committed
130
val graft_proof_attempt : session -> proofNodeID -> Whyconf.prover ->
131 132 133
  limit:Call_provers.resource_limit -> proofAttemptID
(** [graft_proof_attempt s id pr l] adds a proof attempt with prover
    [pr] and limits [l] in the session [s] as a child of the task
134
    [id]. If there already a proof attempt with the same prover, it
135
    updates it with the limits. It returns the id of the
136
    generated proof attempt. *)
Clément Fumex's avatar
Clément Fumex committed
137 138

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

143
val graft_transf : session -> proofNodeID -> string -> string list ->
Clément Fumex's avatar
Clément Fumex committed
144
  Task.task list -> transID
145
(** [graft_transf s id name l tl] adds the transformation [name] as a
Clément Fumex's avatar
Clément Fumex committed
146
    child of the task [id] of the session [s]. [l] is the list of
147
    arguments of the transformation, and [tl] is the list of subtasks.
Clément Fumex's avatar
Clément Fumex committed
148
*)
MARCHE Claude's avatar
MARCHE Claude committed
149

Clément Fumex's avatar
Clément Fumex committed
150 151 152
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
153

Clément Fumex's avatar
Clément Fumex committed
154 155 156
val remove_transformation : session -> transID -> unit
(** [remove_transformation s id] removes the transformation [id]
    from the session [s] *)
157

158 159 160
val mark_obsolete: session -> proofAttemptID -> unit
(** [mark_obsolete s id] marks [id] as obsolete in [s] *)

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

Clément Fumex's avatar
Clément Fumex committed
164
val load_session : string -> session * bool
Clément Fumex's avatar
Clément Fumex committed
165
(** [load_session dir] load a session in directory [dir]; all the
Clément Fumex's avatar
Clément Fumex committed
166 167 168 169 170 171 172 173 174 175
    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.
 *)
176 177 178 179 180 181 182 183

exception RemoveError

val remove_subtree: session -> any -> notification:(any -> unit) -> unit
(** [remove_subtree s a notification] remove the subtree originating from a in
    session s then call the notification function (used to notify the ide.

    If called on a theory or proof node, raise RemoveError *)
184 185 186

val fold_all_any: session -> ('a -> any -> 'a) -> 'a -> any -> 'a
(** [fold_all_any s f acc any] folds on all the subnodes of any *)