sig
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 Wp.Tactical.process
type selection =
Empty
| Clause of Wp.Tactical.clause
| Inside of Wp.Tactical.clause * Wp.Lang.F.term
| Compose of Wp.Tactical.compose
and compose = private
Cint of Integer.t
| Range of int * int
| Code of Wp.Lang.F.term * string * Wp.Tactical.selection list
val int : int -> Wp.Tactical.selection
val cint : Integer.t -> Wp.Tactical.selection
val range : int -> int -> Wp.Tactical.selection
val compose : string -> Wp.Tactical.selection list -> Wp.Tactical.selection
val get_int : Wp.Tactical.selection -> int option
val destruct : Wp.Tactical.selection -> Wp.Tactical.selection list
val head : Wp.Tactical.clause -> Wp.Lang.F.pred
val is_empty : Wp.Tactical.selection -> bool
val selected : Wp.Tactical.selection -> Wp.Lang.F.term
val subclause : Wp.Tactical.clause -> Wp.Lang.F.pred -> bool
val pp_clause : Stdlib.Format.formatter -> Wp.Tactical.clause -> unit
val pp_selection : Stdlib.Format.formatter -> Wp.Tactical.selection -> unit
type 'a field
module Fmap :
sig
type t
val create : unit -> Wp.Tactical.Fmap.t
val get : Wp.Tactical.Fmap.t -> 'a Wp.Tactical.field -> 'a
val set : Wp.Tactical.Fmap.t -> 'a Wp.Tactical.field -> 'a -> unit
end
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 Wp.Tactical.named -> unit) -> Wp.Tactical.selection -> unit
type parameter =
Checkbox of bool Wp.Tactical.field
| Spinner of int Wp.Tactical.field * int Wp.Tactical.range
| Composer of Wp.Tactical.selection Wp.Tactical.field *
(Wp.Lang.F.term -> bool)
| Selector : 'a Wp.Tactical.field * 'a Wp.Tactical.named list *
('a -> 'a -> bool) -> Wp.Tactical.parameter
| Search : 'a Wp.Tactical.named option Wp.Tactical.field *
'a Wp.Tactical.browser * (string -> 'a) -> Wp.Tactical.parameter
val ident : 'a Wp.Tactical.field -> string
val default : 'a Wp.Tactical.field -> 'a
val signature : 'a Wp.Tactical.field -> 'a Wp.Tactical.named
val checkbox :
id:string ->
title:string ->
descr:string ->
?default:bool -> unit -> bool Wp.Tactical.field * Wp.Tactical.parameter
val spinner :
id:string ->
title:string ->
descr:string ->
?default:int ->
?vmin:int ->
?vmax:int ->
?vstep:int -> unit -> int Wp.Tactical.field * Wp.Tactical.parameter
val selector :
id:string ->
title:string ->
descr:string ->
?default:'a ->
options:'a Wp.Tactical.named list ->
?equal:('a -> 'a -> bool) ->
unit -> 'a Wp.Tactical.field * Wp.Tactical.parameter
val composer :
id:string ->
title:string ->
descr:string ->
?default:Wp.Tactical.selection ->
?filter:(Wp.Lang.F.term -> bool) ->
unit -> Wp.Tactical.selection Wp.Tactical.field * Wp.Tactical.parameter
val search :
id:string ->
title:string ->
descr:string ->
browse:'a Wp.Tactical.browser ->
find:(string -> 'a) ->
unit ->
'a Wp.Tactical.named option Wp.Tactical.field * Wp.Tactical.parameter
type 'a formatter = ('a, Stdlib.Format.formatter, unit) Stdlib.format -> 'a
class type feedback =
object
method get_title : string
method has_error : bool
method interactive : bool
method pool : Wp.Lang.F.pool
method set_descr : 'a Wp.Tactical.formatter
method set_error : 'a Wp.Tactical.formatter
method set_title : 'a Wp.Tactical.formatter
method update_field :
?enabled:bool ->
?title:string ->
?tooltip:string ->
?range:bool ->
?vmin:int ->
?vmax:int ->
?filter:(Wp.Lang.F.term -> bool) -> 'a Wp.Tactical.field -> unit
end
val at : Wp.Tactical.selection -> int option
val mapi : (int -> int -> 'a -> 'b) -> 'a list -> 'b list
val insert :
?at:int -> (string * Wp.Lang.F.pred) list -> Wp.Tactical.process
val replace :
at:int -> (string * Wp.Conditions.condition) list -> Wp.Tactical.process
val split : (string * Wp.Lang.F.pred) list -> Wp.Tactical.process
val rewrite :
?at:int ->
(string * Wp.Lang.F.pred * Wp.Lang.F.term * Wp.Lang.F.term) list ->
Wp.Tactical.process
val condition :
string -> Wp.Lang.F.pred -> Wp.Tactical.process -> Wp.Tactical.process
class type tactical =
object
method descr : string
method get_field : 'a Wp.Tactical.field -> 'a
method id : string
method params : Wp.Tactical.parameter list
method reset : unit
method select :
Wp.Tactical.feedback -> Wp.Tactical.selection -> Wp.Tactical.status
method set_field : 'a Wp.Tactical.field -> 'a -> unit
method title : string
end
class virtual make :
id:string ->
title:string ->
descr:string ->
params:Wp.Tactical.parameter list ->
object
method descr : string
method get_field : 'a Wp.Tactical.field -> 'a
method id : string
method params : Wp.Tactical.parameter list
method reset : unit
method virtual select :
Wp.Tactical.feedback -> Wp.Tactical.selection -> Wp.Tactical.status
method set_field : 'a Wp.Tactical.field -> 'a -> unit
method title : string
end
class type composer =
object
method arity : int
method compute : Wp.Lang.F.term list -> Wp.Lang.F.term
method descr : string
method filter : Wp.Lang.F.term list -> bool
method group : string
method id : string
method title : string
end
type t = Wp.Tactical.tactical
val register : #Wp.Tactical.tactical -> unit
val export : #Wp.Tactical.tactical -> Wp.Tactical.tactical
val lookup : id:string -> Wp.Tactical.tactical
val iter : (Wp.Tactical.tactical -> unit) -> unit
val add_composer : #Wp.Tactical.composer -> unit
val iter_composer : (Wp.Tactical.composer -> unit) -> unit
end