Module Wp.StrategySource

Strategies Entry Points

Term & Predicate Selection

Sourceval occurs_x : Lang.F.var -> Lang.F.term -> bool
Sourceval occurs_y : Lang.F.var -> Lang.F.pred -> bool
Sourceval occurs_e : Lang.F.term -> Lang.F.term -> bool
Sourceval occurs_p : Lang.F.term -> Lang.F.pred -> bool
Sourceval occurs_q : Lang.F.pred -> Lang.F.pred -> bool

Lookup the first occurrence of term in the sequent and returns the associated selection. Returns Empty is not found. Goal is lookup first.

Same as select_e but for a predicate.

Strategy

Sourcetype argument =
  1. | ARG : 'a Tactical.field * 'a -> argument
Sourcetype strategy = {
  1. priority : float;
  2. tactical : Tactical.tactical;
  3. selection : Tactical.selection;
  4. arguments : argument list;
}
Sourceclass pool : object ... end
Sourceclass type heuristic = object ... end
Sourceval register : heuristic -> unit
Sourceval export : heuristic -> heuristic
Sourceval lookup : id:string -> heuristic
Sourceval iter : (heuristic -> unit) -> unit

Factory

Sourceval arg : 'a Tactical.field -> 'a -> argument
Sourceval make : Tactical.tactical -> ?priority:float -> ?arguments:argument list -> Tactical.selection -> strategy