session_itp.mli 1.88 KB
Newer Older
Clément Fumex's avatar
Clément Fumex committed
1
type session
MARCHE Claude's avatar
MARCHE Claude committed
2

Clément Fumex's avatar
Clément Fumex committed
3 4 5 6
type transID
type proofNodeID
type proof_attempt
type trans_arg
MARCHE Claude's avatar
MARCHE Claude committed
7

Clément Fumex's avatar
Clément Fumex committed
8
(* (\** New Proof sessions ("Refectoire") *\) *)
MARCHE Claude's avatar
MARCHE Claude committed
9

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

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

*)

Clément Fumex's avatar
Clément Fumex committed
18
(* Note for big brother Andrei: grafting is the oposite of pruning *)
MARCHE Claude's avatar
MARCHE Claude committed
19

Clément Fumex's avatar
Clément Fumex committed
20 21 22
val graft_proof_attempt : session -> proofNodeID -> proof_attempt -> unit
(** [graft_proof_attempt s id pa] adds the proof attempt [pa] as a
    child of the task [id] of the session [s]. *)
MARCHE Claude's avatar
MARCHE Claude committed
23

Clément Fumex's avatar
Clément Fumex committed
24 25
val graft_transf : session -> proofNodeID -> string -> trans_arg list ->
  Task.task list -> unit
Clément Fumex's avatar
Clément Fumex committed
26
(** [graft_transf s id name l tl] adds the transformation [name] as a
Clément Fumex's avatar
Clément Fumex committed
27 28 29
    child of the task [id] of the session [s]. [l] is the list of
    argument of the transformation; [tl] is the resulting list of
    tasks *)
MARCHE Claude's avatar
MARCHE Claude committed
30

Clément Fumex's avatar
Clément Fumex committed
31 32 33
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
34

Clément Fumex's avatar
Clément Fumex committed
35 36 37
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
38

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

Clément Fumex's avatar
Clément Fumex committed
42
val load_session : string -> session * bool
Clément Fumex's avatar
Clément Fumex committed
43 44
(** [load_session f] load a session from a file [f]; all the tasks are
    initialised to None *)
MARCHE Claude's avatar
MARCHE Claude committed
45 46
(*

Clément Fumex's avatar
Clément Fumex committed
47 48
  couche au-dessus: "scheduler" cad modifications asynchrones de la
  session
MARCHE Claude's avatar
MARCHE Claude committed
49 50 51

   - gere une file de travaux de modifications a faire

Clément Fumex's avatar
Clément Fumex committed
52 53
   - recupere les resultats de travaux , et les applique s'ils sont
     encore valides
MARCHE Claude's avatar
MARCHE Claude committed
54
*)
Clément Fumex's avatar
Clément Fumex committed
55
(*
MARCHE Claude's avatar
MARCHE Claude committed
56 57 58 59 60 61 62 63 64 65 66 67 68 69
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
70
 *)