Previous  Up  Next

Module Tactical

module Tactical: sig .. end

Tactical

Tactical Selection

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 process 
type selection =
| Empty
| Clause of clause
| Inside of clause * Lang.F.term
| Compose of compose
| Multi of selection list 
type compose = private
| Cint of Integer.t
| Range of int * int
| Code of 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 multi : 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

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 * (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:(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, Stdlib.Format.formatter, unit) Stdlib.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 * 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

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