session_itp.mli 5.15 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
20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43

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

*)



44 45 46 47 48 49 50 51
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 *)
}
52
type transID
MARCHE Claude's avatar
MARCHE Claude committed
53

MARCHE Claude's avatar
MARCHE Claude committed
54

55
type proof_parent = Trans of transID | Theory of theory
56

57
(* This is not needed
58 59 60 61 62 63 64
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
65 66 67 68 69
(* 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" *)
70
*)
MARCHE Claude's avatar
MARCHE Claude committed
71

72
(*
Clément Fumex's avatar
Clément Fumex committed
73 74 75
val get_tree : session -> proofNodeID -> tree
(** [get_tree s id] returns the proof tree of the goal identified by
    [id] *)
76
*)
Clément Fumex's avatar
Clément Fumex committed
77

78 79
val get_task : session -> proofNodeID -> Task.task

Clément Fumex's avatar
Clément Fumex committed
80
(* temp *)
81
(*
Clément Fumex's avatar
Clément Fumex committed
82 83
val get_node : session -> int -> proofNodeID
val get_trans : session -> int -> transID
84 85 86 87 88 89 90 91 92 93 94 95 96
*)

(* [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
97
val print_session : Format.formatter -> session -> unit
Clément Fumex's avatar
Clément Fumex committed
98 99 100

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

104 105 106
val get_transf_args : session -> transID -> string list
val get_transf_name : session -> transID -> string

107 108
val get_proof_name : session -> proofNodeID -> Ident.ident

109 110 111
val get_proof_parent : session -> proofNodeID -> proof_parent
val get_trans_parent : session -> transID -> proofNodeID

Clément Fumex's avatar
Clément Fumex committed
112
val empty_session : ?shape_version:int -> unit -> session
MARCHE Claude's avatar
MARCHE Claude committed
113 114

val add_file_section :
MARCHE Claude's avatar
MARCHE Claude committed
115 116 117 118 119 120 121 122 123
  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
124

Clément Fumex's avatar
Clément Fumex committed
125 126 127 128
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
129
    [id]. If there already a proof attempt with the same prover,
Clément Fumex's avatar
Clément Fumex committed
130 131 132
    it updates it with the new timelimit. *)

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

137
val graft_transf : session -> proofNodeID -> string -> string list ->
138 139
   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
140
    child of the task [id] of the session [s]. [l] is the list of
141
    arguments of the transformation, and [tl] is the list of subtasks.
142
 *)
MARCHE Claude's avatar
MARCHE Claude committed
143

Clément Fumex's avatar
Clément Fumex committed
144 145 146
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
147

Clément Fumex's avatar
Clément Fumex committed
148 149 150
val remove_transformation : session -> transID -> unit
(** [remove_transformation s id] removes the transformation [id]
    from the session [s] *)
151

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

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