Module Wp.Strategy

module Strategy: sig .. end


Term & Predicate Selection


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 = 
| ARG : 'a Wp.Tactical.field * 'a -> argument
type strategy = {
   priority : float;
   tactical : Wp.Tactical.tactical;
   selection : Wp.Tactical.selection;
   arguments : argument list;
}
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 make : Wp.Tactical.tactical ->
?priority:float ->
?arguments:argument list ->
Wp.Tactical.selection -> strategy