session_itp.mli 3.78 KB
Newer Older
Clément Fumex's avatar
Clément Fumex committed
1 2 3 4 5
type session
type transID
type proofNodeID
type proof_attempt
type trans_arg
MARCHE Claude's avatar
MARCHE Claude committed
6

MARCHE Claude's avatar
MARCHE Claude committed
7
(* New Proof sessions ("Refectoire") *)
MARCHE Claude's avatar
MARCHE Claude committed
8

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

Clément Fumex's avatar
Clément Fumex committed
12 13
   type trans_arg_type = TTint | TTstring | TTterm | TTty | TTtysymbol
   | TTlsymbol | TTprsymbol
MARCHE Claude's avatar
MARCHE Claude committed
14 15 16

*)

MARCHE Claude's avatar
MARCHE Claude committed
17
type tree =
Clément Fumex's avatar
Clément Fumex committed
18
    Tree of
MARCHE Claude's avatar
MARCHE Claude committed
19 20 21
      (proofNodeID * string
       * proof_attempt list (* proof attempts in this node *)
       * (transID * string * tree list) list) (* transformation in this node *)
MARCHE Claude's avatar
MARCHE Claude committed
22

Clément Fumex's avatar
Clément Fumex committed
23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 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
    file name and [l] is a list of pairs [thnmae,l'] where [thname] is
    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
41 42 43

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

Clément Fumex's avatar
Clément Fumex committed
44
val empty_session : ?shape_version:int -> unit -> session
MARCHE Claude's avatar
MARCHE Claude committed
45 46

val add_file_section :
Clément Fumex's avatar
Clément Fumex committed
47
  session -> string -> (Theory.theory list) -> Env.fformat option -> unit
MARCHE Claude's avatar
MARCHE Claude committed
48 49 50 51
(** [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
52

Clément Fumex's avatar
Clément Fumex committed
53 54 55 56 57 58 59 60 61 62 63
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
64

Clément Fumex's avatar
Clément Fumex committed
65
val graft_transf : session -> proofNodeID -> string -> trans_arg list ->
Clément Fumex's avatar
Clément Fumex committed
66 67
   transID
(** [graft_transf s id name l] adds the transformation [name] as a
Clément Fumex's avatar
Clément Fumex committed
68
    child of the task [id] of the session [s]. [l] is the list of
Clément Fumex's avatar
Clément Fumex committed
69 70
    argument of the transformation. The subtasks are initialized to
    the empty list *)
MARCHE Claude's avatar
MARCHE Claude committed
71

Clément Fumex's avatar
Clément Fumex committed
72 73 74
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
75

Clément Fumex's avatar
Clément Fumex committed
76 77 78
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
79

Clément Fumex's avatar
Clément Fumex committed
80 81 82
val remove_transformation : session -> transID -> unit
(** [remove_transformation s id] removes the transformation [id]
    from the session [s] *)
MARCHE Claude's avatar
MARCHE Claude committed
83 84 85
(*
val save_session : string -> session -> unit
 *)
Clément Fumex's avatar
Clément Fumex committed
86
(** [save_session f s] Save the session [s] in file [f] *)
MARCHE Claude's avatar
MARCHE Claude committed
87

Clément Fumex's avatar
Clément Fumex committed
88
val load_session : string -> session * bool
Clément Fumex's avatar
Clément Fumex committed
89 90
(** [load_session f] load a session from a file [f]; all the tasks are
    initialised to None *)
MARCHE Claude's avatar
MARCHE Claude committed
91 92


MARCHE Claude's avatar
MARCHE Claude committed
93 94
(*

Clément Fumex's avatar
Clément Fumex committed
95 96
  couche au-dessus: "scheduler" cad modifications asynchrones de la
  session
MARCHE Claude's avatar
MARCHE Claude committed
97 98 99

   - gere une file de travaux de modifications a faire

Clément Fumex's avatar
Clément Fumex committed
100 101
   - recupere les resultats de travaux , et les applique s'ils sont
     encore valides
MARCHE Claude's avatar
MARCHE Claude committed
102
*)
Clément Fumex's avatar
Clément Fumex committed
103
(*
MARCHE Claude's avatar
MARCHE Claude committed
104 105 106 107 108 109 110 111 112 113 114 115 116 117
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
118
 *)