module Strategy: sig
.. end
Term & Predicate Selection
val env : Wp.Conditions.sequent -> Wp.Repr.env
val occurs_x : Wp.Lang.F.var -> Wp.Lang.F.term -> bool
val occurs_y : Wp.Lang.F.var -> Wp.Lang.F.pred -> bool
val occurs_e : Wp.Lang.F.term -> Wp.Lang.F.term -> bool
val occurs_p : Wp.Lang.F.term -> Wp.Lang.F.pred -> bool
val occurs_q : Wp.Lang.F.pred -> Wp.Lang.F.pred -> bool
val select_e : Wp.Conditions.sequent -> Wp.Lang.F.term -> Wp.Tactical.selection
Lookup the first occurrence of term in the sequent and returns
the associated selection. Returns Empty
is not found.
Goal is lookup first.
val select_p : Wp.Conditions.sequent -> Wp.Lang.F.pred -> Wp.Tactical.selection
Same as select_e
but for a predicate.
Strategy
type
argument =
type
strategy = {
}
class pool :
object
.. end
class type heuristic = object
.. end
val register : #heuristic -> unit
val export : #heuristic -> heuristic
val lookup : id:string -> heuristic
val iter : (heuristic -> unit) -> unit
Factory
type
t = strategy
val arg : 'a Wp.Tactical.field -> 'a -> argument
val set_arg : Wp.Tactical.tactical -> argument -> unit
val set_args : Wp.Tactical.tactical -> argument list -> unit
val make : Wp.Tactical.tactical ->
?priority:float -> Wp.Tactical.selection -> strategy