module Tactical:sig
..end
Tactical
type
clause =
| |
Goal of |
| |
Step of |
typeprocess =
Conditions.sequent -> (string * Conditions.sequent) list
type
status =
| |
Not_applicable |
| |
Not_configured |
| |
Applicable of |
type
selection =
| |
Empty |
| |
Clause of |
| |
Inside of |
| |
Compose of |
type
compose = private
| |
Cint of |
| |
Range of |
| |
Code of |
val int : int -> selection
val cint : Integer.t -> selection
val range : int -> int -> selection
val compose : string -> selection list -> selection
val get_int : selection -> int option
val destruct : selection -> selection list
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
type 'a
field
module Fmap:sig
..end
type 'a
named = {
|
title : |
|
descr : |
|
vid : |
|
value : |
type 'a
range = {
|
vmin : |
|
vmax : |
|
vstep : |
type'a
browser =('a named -> unit) -> selection -> unit
type
parameter =
| |
Checkbox of |
| |
Spinner of |
| |
Composer of |
| |
Selector : |
| |
Search : |
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:(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.type'a
formatter =('a, Stdlib.Format.formatter, unit) Stdlib.format -> 'a
class type feedback =object
..end
val at : selection -> int option
val mapi : (int -> int -> 'a -> 'b) -> 'a list -> 'b list
val insert : ?at:int -> (string * Lang.F.pred) list -> process
val replace : at:int -> (string * 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
.
class type tactical =object
..end
class virtual make :id:string -> title:string -> descr:string -> params:parameter list ->
object
..end
class type composer =object
..end
typet =
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