Newer
Older
(**************************************************************************)
(* *)
(* This file is part of WP plug-in of Frama-C. *)
(* *)
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
(* CEA (Commissariat a l'energie atomique et aux energies *)
(* alternatives) *)
(* *)
(* you can redistribute it and/or modify it under the terms of the GNU *)
(* Lesser General Public License as published by the Free Software *)
(* Foundation, version 2.1. *)
(* *)
(* It is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
(* GNU Lesser General Public License for more details. *)
(* *)
(* See the GNU Lesser General Public License version 2.1 *)
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)
(**************************************************************************)
open Tactical
(* -------------------------------------------------------------------------- *)
(* --- Selection Composer --- *)
(* -------------------------------------------------------------------------- *)
class type composer =
object
method title : string
method descr : string
method target : selection
method ranged : bool
method is_valid : selection -> bool
method get_value : selection
method set_value : selection -> unit
end
(* -------------------------------------------------------------------------- *)
(* --- Search --- *)
(* -------------------------------------------------------------------------- *)
class type browser =
object
method title : string
method descr : string
method target : selection
method search : (unit named -> unit) -> int -> bool
method choose : string option -> unit
end
(* -------------------------------------------------------------------------- *)
(* --- Tactical Dongle --- *)
(* -------------------------------------------------------------------------- *)
class tactic : Tactical.t -> (Format.formatter -> Tactical.selection -> unit) ->
object
inherit Wpalette.tool
inherit feedback
method clear : unit
method targeted : bool
method select :
process:(tactical -> selection -> process -> unit) ->
browser:(browser -> unit) ->
composer:(composer -> unit) ->
tree:ProofEngine.tree ->
selection -> unit
end
type callback = depth:int -> width:int -> Strategy.heuristic list -> unit
class strategies : unit ->
object
inherit Wpalette.tool
method register : Strategy.heuristic -> unit
method connect : callback option -> unit
end