Mise à jour terminée. Pour connaître les apports de la version 13.8.4 par rapport à notre ancienne version vous pouvez lire les "Release Notes" suivantes :
https://about.gitlab.com/releases/2021/02/11/security-release-gitlab-13-8-4-released/
https://about.gitlab.com/releases/2021/02/05/gitlab-13-8-3-released/

session_itp.mli 3.68 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 19
    Tree of
      (proofNodeID * string * (transID * string * tree list) list)
MARCHE Claude's avatar
MARCHE Claude committed
20

Clément Fumex's avatar
Clément Fumex committed
21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38
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
39 40 41

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

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

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

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

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

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

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

Clément Fumex's avatar
Clément Fumex committed
78 79 80
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
81 82 83
(*
val save_session : string -> session -> unit
 *)
Clément Fumex's avatar
Clément Fumex committed
84
(** [save_session f s] Save the session [s] in file [f] *)
MARCHE Claude's avatar
MARCHE Claude committed
85

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


MARCHE Claude's avatar
MARCHE Claude committed
91 92
(*

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

   - gere une file de travaux de modifications a faire

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