Wp.Tactical
Tactics Entry Points
Tactical
type process = Conditions.sequent -> (string * Conditions.sequent) list
type selection =
| Empty |
| Clause of clause |
| Inside of clause * Lang.F.term |
| Compose of compose |
| Multi of selection list |
and compose = private
| Cint of Frama_c_kernel.Integer.t |
| Range of int * int |
| Code of Lang.F.term * string * selection list |
val int : int -> selection
val cint : Frama_c_kernel.Integer.t -> selection
val range : int -> int -> selection
val get_int : selection -> int option
val head : clause -> Lang.F.pred
val is_empty : selection -> bool
val selected : selection -> Lang.F.term
val subclause : clause -> Lang.F.pred -> bool
When subclause clause p
, we have clause = Step H
and H -> p
, or clause = Goal G
and p -> G
.
val pp_clause : Stdlib.Format.formatter -> clause -> unit
Debug only
val pp_selection : Stdlib.Format.formatter -> selection -> unit
Debug only
module Fmap : sig ... end
val ident : 'a field -> string
val default : 'a field -> 'a
val checkbox :
id:string ->
title:string ->
descr:string ->
?default:bool ->
unit ->
bool field * parameter
Unless specified, default is false
.
val spinner :
id:string ->
title:string ->
descr:string ->
?default:int ->
?vmin:int ->
?vmax:int ->
?vstep:int ->
unit ->
int field * parameter
Unless specified, default is vmin
or 0
or vmax
, whichever fits. Range must be non-empty, and default shall fit in.
val selector :
id:string ->
title:string ->
descr:string ->
?default:'a ->
options:'a named list ->
?equal:( 'a -> 'a -> bool ) ->
unit ->
'a field * parameter
Unless specified, default is head option. Default equality is (=)
. Options must be non-empty.
val composer :
id:string ->
title:string ->
descr:string ->
?default:selection ->
?filter:( Lang.F.term -> bool ) ->
unit ->
selection field * parameter
Unless specified, default is Empty selection.
val search :
id:string ->
title:string ->
descr:string ->
browse:'a browser ->
find:( string -> 'a ) ->
unit ->
'a named option field * parameter
Search field.
browse s n
is the lookup function, used in the GUI only. Shall returns at most n
results applying to selection s
.find n
is used at script replay, and shall retrieve the selected item's id
later on.class type feedback = object ... end
val at : selection -> int option
val insert : ?at:int -> (string * Lang.F.pred) list -> process
val replace : at:int -> (string * Conditions.condition) list -> process
val replace_single :
at:int ->
(string * Conditions.condition) ->
Conditions.sequent ->
string * Conditions.sequent
val replace_step : at:int -> Conditions.condition list -> process
val split : (string * Lang.F.pred) list -> process
val rewrite :
?at:int ->
(string * Lang.F.pred * Lang.F.term * Lang.F.term) list ->
process
For each pattern (descr,guard,src,tgt)
replace src
with tgt
under condition guard
, inserted in position at
.
val condition : string -> Lang.F.pred -> process -> process
Apply process, but only after proving some condition
class type tactical = object ... end
class type composer = object ... end
type t = tactical
val register : tactical -> unit
val lookup : id:string -> tactical
val iter : ( tactical -> unit ) -> unit
val add_composer : composer -> unit
val iter_composer : ( composer -> unit ) -> unit