session_itp.mli 4.24 KB
Newer Older
Clément Fumex's avatar
Clément Fumex committed
1 2 3 4
type session
type transID
type proofNodeID
type proof_attempt
MARCHE Claude's avatar
MARCHE Claude committed
5 6 7 8 9 10 11 12 13 14 15 16

type trans_arg =
  | TAint      of int
  | TAstring   of string
  | TAterm     of Term.term
  | TAty       of Ty.ty
  | TAtysymbol of Ty.tysymbol
  (* | ... *)




MARCHE Claude's avatar
MARCHE Claude committed
17

MARCHE Claude's avatar
MARCHE Claude committed
18
(* New Proof sessions ("Refectoire") *)
MARCHE Claude's avatar
MARCHE Claude committed
19

Clément Fumex's avatar
Clément Fumex committed
20 21
(* note: la fonction register des transformations doit permettre de
   declarer les types des arguments
MARCHE Claude's avatar
MARCHE Claude committed
22

Clément Fumex's avatar
Clément Fumex committed
23 24
   type trans_arg_type = TTint | TTstring | TTterm | TTty | TTtysymbol
   | TTlsymbol | TTprsymbol
MARCHE Claude's avatar
MARCHE Claude committed
25 26 27

*)

MARCHE Claude's avatar
MARCHE Claude committed
28
type tree =
Clément Fumex's avatar
Clément Fumex committed
29
    Tree of
MARCHE Claude's avatar
MARCHE Claude committed
30
      (proofNodeID * string
MARCHE Claude's avatar
MARCHE Claude committed
31 32 33 34 35 36 37
       * proof_attempt list (* proof attempts on this node *)
       * (transID * string * tree list) list) (* transformations on this node *)
(* 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" *)
MARCHE Claude's avatar
MARCHE Claude committed
38

Clément Fumex's avatar
Clément Fumex committed
39 40
val get_theories : session -> (string * (string * proofNodeID list) list) list
(** [get_theories s] returns a list of pairs [name,l] where [name] is a
MARCHE Claude's avatar
MARCHE Claude committed
41
    file name and [l] is a list of pairs [thname,l'] where [thname] is
Clément Fumex's avatar
Clément Fumex committed
42 43 44 45 46 47 48 49 50 51 52 53 54 55 56
    a theory name and [l'] is the list of goal ids *)

val get_tree : session -> proofNodeID -> tree
(** [get_tree s id] returns the proof tree of the goal identified by
    [id] *)

(* temp *)
val get_node : session -> int -> proofNodeID
val get_trans : session -> int -> transID
val print_tree : session -> Format.formatter -> tree -> unit
val print_session : session -> unit

(* val get_proof_attempts : session -> proofNodeID -> proof_attempt Whyconf.Hprover.t *)
val get_transformations : session -> proofNodeID -> transID list
val get_sub_tasks : session -> transID -> proofNodeID list
MARCHE Claude's avatar
MARCHE Claude committed
57 58 59

(* Note for big brother Andrei: grafting is the opposite of pruning *)

Clément Fumex's avatar
Clément Fumex committed
60
val empty_session : ?shape_version:int -> unit -> session
MARCHE Claude's avatar
MARCHE Claude committed
61 62

val add_file_section :
Clément Fumex's avatar
Clément Fumex committed
63
  session -> string -> (Theory.theory list) -> Env.fformat option -> unit
MARCHE Claude's avatar
MARCHE Claude committed
64 65 66 67
(** [add_file_section s fn 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] *)
MARCHE Claude's avatar
MARCHE Claude committed
68

Clément Fumex's avatar
Clément Fumex committed
69 70 71 72 73 74 75 76 77 78 79
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
    [id]. If there allready a proof attempt with the same prover,
    it updates it with the new timelimit. *)

val update_proof_attempt : session -> proofNodeID -> Whyconf.prover ->
  Call_provers.prover_result option -> unit
(** [update_proof_attempt s id pr st] update the status of the
    corresponding proof attempt with [st]. *)
MARCHE Claude's avatar
MARCHE Claude committed
80

Clément Fumex's avatar
Clément Fumex committed
81
val graft_transf : session -> proofNodeID -> string -> trans_arg list ->
Clément Fumex's avatar
Clément Fumex committed
82 83
   transID
(** [graft_transf s id name l] adds the transformation [name] as a
Clément Fumex's avatar
Clément Fumex committed
84
    child of the task [id] of the session [s]. [l] is the list of
Clément Fumex's avatar
Clément Fumex committed
85 86
    argument of the transformation. The subtasks are initialized to
    the empty list *)
MARCHE Claude's avatar
MARCHE Claude committed
87

Clément Fumex's avatar
Clément Fumex committed
88 89 90
val set_transf_tasks : session -> transID -> Task.task list -> unit
(** [set_transf_tasks s id tl] sets the tasks of the transformation node
    [id] to [tl] *)
MARCHE Claude's avatar
MARCHE Claude committed
91

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

Clément Fumex's avatar
Clément Fumex committed
96 97 98
val remove_transformation : session -> transID -> unit
(** [remove_transformation s id] removes the transformation [id]
    from the session [s] *)
99

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

103
val load_session : string -> session
Clément Fumex's avatar
Clément Fumex committed
104 105
(** [load_session f] load a session from a file [f]; all the tasks are
    initialised to None *)
MARCHE Claude's avatar
MARCHE Claude committed
106 107


MARCHE Claude's avatar
MARCHE Claude committed
108 109
(*

Clément Fumex's avatar
Clément Fumex committed
110 111
  couche au-dessus: "scheduler" cad modifications asynchrones de la
  session
MARCHE Claude's avatar
MARCHE Claude committed
112 113 114

   - gere une file de travaux de modifications a faire

Clément Fumex's avatar
Clément Fumex committed
115 116
   - recupere les resultats de travaux , et les applique s'ils sont
     encore valides
MARCHE Claude's avatar
MARCHE Claude committed
117
*)
Clément Fumex's avatar
Clément Fumex committed
118
(*
MARCHE Claude's avatar
MARCHE Claude committed
119 120 121 122 123 124 125 126 127 128 129 130 131 132
type theory =
  {
    goals : sequence of task
  }

type file =
  {
    theories = sequence of theories
  }

type session =
  {
    session_files : set of files
  }
Clément Fumex's avatar
Clément Fumex committed
133
 *)