session_itp.mli 2.43 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 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32
type tree =
  Tree of
    (int * string * int * (int * string * int * tree list) list)

val get_tree : session -> (string * (string * tree list) list) list

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

val empty_session : ?shape_version:int -> string -> session

val add_file_section :
  session -> string -> ?format:string -> Theory.theory list -> unit
(** [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
33

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

Clément Fumex's avatar
Clément Fumex committed
38 39
val graft_transf : session -> proofNodeID -> string -> trans_arg list ->
  Task.task list -> unit
Clément Fumex's avatar
Clément Fumex committed
40
(** [graft_transf s id name l tl] adds the transformation [name] as a
Clément Fumex's avatar
Clément Fumex committed
41 42 43
    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
44

MARCHE Claude's avatar
MARCHE Claude committed
45 46

(*
Clément Fumex's avatar
Clément Fumex committed
47 48 49
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
50

Clément Fumex's avatar
Clément Fumex committed
51 52 53
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
54

MARCHE Claude's avatar
MARCHE Claude committed
55 56 57
(*
val save_session : string -> session -> unit
 *)
Clément Fumex's avatar
Clément Fumex committed
58
(** [save_session f s] Save the session [s] in file [f] *)
MARCHE Claude's avatar
MARCHE Claude committed
59 60
 *)

MARCHE Claude's avatar
MARCHE Claude committed
61

Clément Fumex's avatar
Clément Fumex committed
62
val load_session : string -> session * bool
Clément Fumex's avatar
Clément Fumex committed
63 64
(** [load_session f] load a session from a file [f]; all the tasks are
    initialised to None *)
MARCHE Claude's avatar
MARCHE Claude committed
65 66


MARCHE Claude's avatar
MARCHE Claude committed
67 68
(*

Clément Fumex's avatar
Clément Fumex committed
69 70
  couche au-dessus: "scheduler" cad modifications asynchrones de la
  session
MARCHE Claude's avatar
MARCHE Claude committed
71 72 73

   - gere une file de travaux de modifications a faire

Clément Fumex's avatar
Clément Fumex committed
74 75
   - recupere les resultats de travaux , et les applique s'ils sont
     encore valides
MARCHE Claude's avatar
MARCHE Claude committed
76
*)
Clément Fumex's avatar
Clément Fumex committed
77
(*
MARCHE Claude's avatar
MARCHE Claude committed
78 79 80 81 82 83 84 85 86 87 88 89 90 91
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
92
 *)