session_itp.mli 5.4 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 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50

type theory

val theory_name : theory -> Ident.ident
val theory_goals : theory -> proofNodeID list

type file = private {
  file_name     : string;
  file_format   : string option;
  file_theories : theory list;
}

val get_files : session -> file Stdlib.Hstr.t

(** {2 Proof trees}

Each goal

*)



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

MARCHE Claude's avatar
MARCHE Claude committed
60

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

63
(* This is not needed
64 65 66 67 68 69 70
type tree = {
    tree_node_id : proofNodeID;
    tree_goal_name : string;
    tree_proof_attempts : proof_attempt list; (* proof attempts on this node *)
    tree_transformations : (transID * string * tree list) list;
                                (* transformations on this node *)
  }
MARCHE Claude's avatar
MARCHE Claude committed
71 72 73 74 75
(* a tree is a complete proof whenever at least one proof_attempf or
  one transformation proves the goal, where a transformation proves a
  goal when all subgoals have a complete proof.  In other word, the
  list of proof_attempt and transformation are "disjunctive" but the
  list of tree below a transformation is "conjunctive" *)
76
*)
MARCHE Claude's avatar
MARCHE Claude committed
77

78
(*
Clément Fumex's avatar
Clément Fumex committed
79 80 81
val get_tree : session -> proofNodeID -> tree
(** [get_tree s id] returns the proof tree of the goal identified by
    [id] *)
82
*)
Clément Fumex's avatar
Clément Fumex committed
83

84 85
val get_task : session -> proofNodeID -> Task.task

Clément Fumex's avatar
Clément Fumex committed
86
(* temp *)
87
(*
Clément Fumex's avatar
Clément Fumex committed
88 89
val get_node : session -> int -> proofNodeID
val get_trans : session -> int -> transID
90 91 92 93 94 95 96 97 98 99 100 101 102
*)

(* [print_proof_node s fmt t]: From definition of s, print on fmt the tree
   rooted at element t *)
val print_proof_node : session -> Format.formatter -> proofNodeID -> unit

(* [print_theory s fmt t]: From definition of s, print on fmt the theory t *)
val print_theory : session -> Format.formatter -> theory -> unit

(* [print_trans s fmt tn]: From definition of s, print on fmt the tree originating
   from transformation tn *)
val print_trans_node : session -> Format.formatter -> transID -> unit

MARCHE Claude's avatar
MARCHE Claude committed
103
val print_session : Format.formatter -> session -> unit
Clément Fumex's avatar
Clément Fumex committed
104 105 106

(* val get_proof_attempts : session -> proofNodeID -> proof_attempt Whyconf.Hprover.t *)
val get_transformations : session -> proofNodeID -> transID list
107
val get_proof_attempts : session -> proofNodeID -> proof_attempt list
Clément Fumex's avatar
Clément Fumex committed
108
val get_sub_tasks : session -> transID -> proofNodeID list
MARCHE Claude's avatar
MARCHE Claude committed
109

110 111 112
val get_transf_args : session -> transID -> string list
val get_transf_name : session -> transID -> string

113 114
val get_proof_name : session -> proofNodeID -> Ident.ident

115 116 117
val get_proof_parent : session -> proofNodeID -> proof_parent
val get_trans_parent : session -> transID -> proofNodeID

Clément Fumex's avatar
Clément Fumex committed
118
val empty_session : ?shape_version:int -> unit -> session
MARCHE Claude's avatar
MARCHE Claude committed
119 120

val add_file_section :
MARCHE Claude's avatar
MARCHE Claude committed
121 122 123 124 125 126 127 128 129
  session -> string -> (Theory.theory list) -> Env.fformat option ->
  session -> theory list -> unit
(** [add_file_section s fn ths old_s old_ths] adds a new 'file'
    section in session [s], named [fn], containing fresh theory
    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
    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
130

Clément Fumex's avatar
Clément Fumex committed
131 132 133 134
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
135
    [id]. If there already a proof attempt with the same prover,
Clément Fumex's avatar
Clément Fumex committed
136 137 138
    it updates it with the new timelimit. *)

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 ->
144 145
   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
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.
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

MARCHE Claude's avatar
MARCHE Claude committed
158
val save_session : string -> session -> unit
Clément Fumex's avatar
Clément Fumex committed
159
(** [save_session f s] Save the session [s] in file [f] *)
MARCHE Claude's avatar
MARCHE Claude committed
160

161
val load_session : string -> session
Clément Fumex's avatar
Clément Fumex committed
162 163
(** [load_session f] load a session from a file [f]; all the tasks are
    initialised to None *)