session_itp.mli 4.31 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
    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] *)

48 49
val get_task : session -> proofNodeID -> Task.task

Clément Fumex's avatar
Clément Fumex committed
50 51 52 53
(* temp *)
val get_node : session -> int -> proofNodeID
val get_trans : session -> int -> transID
val print_tree : session -> Format.formatter -> tree -> unit
MARCHE Claude's avatar
MARCHE Claude committed
54
val print_session : Format.formatter -> session -> unit
Clément Fumex's avatar
Clément Fumex committed
55 56 57 58

(* 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
59 60 61

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

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

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

Clément Fumex's avatar
Clément Fumex committed
71 72 73 74
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
75
    [id]. If there already a proof attempt with the same prover,
Clément Fumex's avatar
Clément Fumex committed
76 77 78 79 80 81
    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
82

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

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

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

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

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

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


MARCHE Claude's avatar
MARCHE Claude committed
110 111
(*

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

   - gere une file de travaux de modifications a faire

Clément Fumex's avatar
Clément Fumex committed
117 118
   - recupere les resultats de travaux , et les applique s'ils sont
     encore valides
MARCHE Claude's avatar
MARCHE Claude committed
119
*)
Clément Fumex's avatar
Clément Fumex committed
120
(*
MARCHE Claude's avatar
MARCHE Claude committed
121 122 123 124 125 126 127 128 129 130 131 132 133 134
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
135
 *)