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 4.27 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16




(** {1 New Proof sessions ("Refectoire")} *)


(** {2 upper level structure of sessions}

   A [session] contains a collection of files, a [file] contains a
collection of theories, a [theory] contains a collection of goals. The
structure of goals remain abstract, each goal being identified by
unique identifiers of type [proofNodeId]

*)

Clément Fumex's avatar
Clément Fumex committed
17
type session
18

Clément Fumex's avatar
Clément Fumex committed
19
type proofNodeID
20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43

type theory

val theory_name : theory -> Ident.ident
val theory_goals : theory -> proofNodeID list

type file = private {
  file_name     : string;
  file_format   : string option;
  file_theories : theory list;
}

val get_files : session -> file Stdlib.Hstr.t



(** {2 Proof trees}

Each goal

*)



Clément Fumex's avatar
Clément Fumex committed
44
type proof_attempt
45
type transID
MARCHE Claude's avatar
MARCHE Claude committed
46 47 48 49 50 51 52 53

type trans_arg =
  | TAint      of int
  | TAstring   of string
  | TAterm     of Term.term
  | TAty       of Ty.ty
  | TAtysymbol of Ty.tysymbol
  (* | ... *)
Clément Fumex's avatar
Clément Fumex committed
54 55
(* note: la fonction register des transformations doit permettre de
   declarer les types des arguments
MARCHE Claude's avatar
MARCHE Claude committed
56

Clément Fumex's avatar
Clément Fumex committed
57 58
   type trans_arg_type = TTint | TTstring | TTterm | TTty | TTtysymbol
   | TTlsymbol | TTprsymbol
MARCHE Claude's avatar
MARCHE Claude committed
59 60 61

*)

62
type proof_parent = Trans of transID | Theory of theory
63 64 65 66 67 68 69 70

type tree = {
    tree_node_id : proofNodeID;
    tree_goal_name : string;
    tree_proof_attempts : proof_attempt list; (* proof attempts on this node *)
    tree_transformations : (transID * string * tree list) list;
                                (* transformations on this node *)
  }
MARCHE Claude's avatar
MARCHE Claude committed
71 72 73 74 75
(* 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
76

Clément Fumex's avatar
Clément Fumex committed
77 78 79 80 81

val get_tree : session -> proofNodeID -> tree
(** [get_tree s id] returns the proof tree of the goal identified by
    [id] *)

82 83
val get_task : session -> proofNodeID -> Task.task

Clément Fumex's avatar
Clément Fumex committed
84 85 86 87
(* 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
88
val print_session : Format.formatter -> session -> unit
Clément Fumex's avatar
Clément Fumex committed
89 90 91 92

(* 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
93

94 95 96
val get_proof_parent : session -> proofNodeID -> proof_parent
val get_trans_parent : session -> transID -> proofNodeID

Clément Fumex's avatar
Clément Fumex committed
97
val empty_session : ?shape_version:int -> unit -> session
MARCHE Claude's avatar
MARCHE Claude committed
98 99

val add_file_section :
Clément Fumex's avatar
Clément Fumex committed
100
  session -> string -> (Theory.theory list) -> Env.fformat option -> unit
MARCHE Claude's avatar
MARCHE Claude committed
101 102 103 104
(** [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
105

Clément Fumex's avatar
Clément Fumex committed
106 107 108 109
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
110
    [id]. If there already a proof attempt with the same prover,
Clément Fumex's avatar
Clément Fumex committed
111 112 113
    it updates it with the new timelimit. *)

val update_proof_attempt : session -> proofNodeID -> Whyconf.prover ->
114
  Call_provers.prover_result -> unit
Clément Fumex's avatar
Clément Fumex committed
115 116
(** [update_proof_attempt s id pr st] update the status of the
    corresponding proof attempt with [st]. *)
MARCHE Claude's avatar
MARCHE Claude committed
117

Clément Fumex's avatar
Clément Fumex committed
118
val graft_transf : session -> proofNodeID -> string -> trans_arg list ->
119 120
   Task.task list -> transID
(** [graft_transf s id name l tl] adds the transformation [name] as a
Clément Fumex's avatar
Clément Fumex committed
121
    child of the task [id] of the session [s]. [l] is the list of
122 123
    argument of the transformation, and [tl] is the list of subtasks.
 *)
MARCHE Claude's avatar
MARCHE Claude committed
124

Clément Fumex's avatar
Clément Fumex committed
125 126 127
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
128

Clément Fumex's avatar
Clément Fumex committed
129 130 131
val remove_transformation : session -> transID -> unit
(** [remove_transformation s id] removes the transformation [id]
    from the session [s] *)
132

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

136
val load_session : string -> session
Clément Fumex's avatar
Clément Fumex committed
137 138
(** [load_session f] load a session from a file [f]; all the tasks are
    initialised to None *)