Module Wp.Tactical

module Tactical: sig .. end


Tactical

Tactical Selection


type clause = 
| Goal of Wp.Lang.F.pred
| Step of Wp.Conditions.step
type process = Wp.Conditions.sequent -> (string * Wp.Conditions.sequent) list 
type status = 
| Not_applicable
| Not_configured
| Applicable of process
type selection = 
| Empty
| Clause of clause
| Inside of clause * Wp.Lang.F.term
| Compose of compose
type compose = private 
| Cint of Integer.t
| Range of int * int
| Code of Wp.Lang.F.term * string * selection list
val int : int -> selection
val cint : Integer.t -> selection
val range : int -> int -> selection
val compose : string -> selection list -> selection
val destruct : selection -> selection list
val head : clause -> Wp.Lang.F.pred
val is_empty : selection -> bool
val selected : selection -> Wp.Lang.F.term
val subclause : clause -> Wp.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 : Format.formatter -> clause -> unit
Debug only
val pp_selection : Format.formatter -> selection -> unit
Debug only

Tactical Parameters


type 'a field 
module Fmap: sig .. end

Tactical Parameter Editors


type 'a named = {
   title : string;
   descr : string;
   vid : string;
   value : 'a;
}
type 'a range = {
   vmin : 'a option;
   vmax : 'a option;
   vstep : 'a;
}
type 'a browser = ('a named -> unit) -> selection -> unit 
type parameter = 
| Checkbox of bool field
| Spinner of int field * int range
| Composer of selection field * (Wp.Lang.F.term -> bool)
| Selector : 'a field * 'a named list * ('a -> 'a -> bool) -> parameter
| Search : 'a0 named option field * 'a0 browser
* (string -> 'a0)
-> parameter
val ident : 'a field -> string
val default : 'a field -> 'a
val signature : 'a field -> 'a named
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:(Wp.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.
type 'a formatter = ('a, Format.formatter, unit) Pervasives.format -> 'a 
class type feedback = object .. end

Tactical Utilities


val at : selection -> int option
val mapi : (int -> int -> 'a -> 'b) -> 'a list -> 'b list
val insert : ?at:int -> (string * Wp.Lang.F.pred) list -> process
val replace : at:int -> (string * Wp.Conditions.condition) list -> process
val split : (string * Wp.Lang.F.pred) list -> process
val rewrite : ?at:int ->
(string * Wp.Lang.F.pred * Wp.Lang.F.term * Wp.Lang.F.term) list ->
process
For each pattern (descr,guard,src,tgt) replace src with tgt under condition guard, inserted in position at.

Tactical Plug-in


class type tactical = object .. end
class virtual make : id:string -> title:string -> descr:string -> params:parameter list -> object .. end

Composer Factory


class type composer = object .. end

Global Registry


type t = tactical 
val register : #tactical -> unit
val export : #tactical -> tactical
Register and returns the tactical
val lookup : id:string -> tactical
val iter : (tactical -> unit) -> unit
val add_composer : #composer -> unit
val iter_composer : (composer -> unit) -> unit