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 -> 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