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