Module Strategy

module Strategy: sig .. end

Proof strategies

Basic strategies

A basic strategy is defined by a program declared under a simple assembly-like form: instructions are indexed by integers starting from 0 (the initial instruction counter). An instruction is either

1) a call to a prover, with given time and mem limits

. on success, the program execution ends

. on any other result, the program execution continues on the next index

2) an application of a transformation

. on success, the execution continues to a explicitly given index

. on failure, execution continues on the next index

3) a goto instruction.

The execution halts when reaching a non-existing instruction number

type instruction =

`\|`	`Icall_prover of (Whyconf.prover * float option * int option * int option) list`	`(*`	timelimit (if none use default timelimit), memlimit (if none use default memlimit) steplimit (if none use no step limit)	`*)`
`\|`	`Itransform of string * int`	`(*`	successor state on success	`*)`
`\|`	`Igoto of int`	`(*`	goto state	`*)`

type t = instruction array

Strategies programmed in OCaml

type proof_tree =

`\|`	`Sdo_nothing`
`\|`	`Sapply_trans of string * string list * proof_tree list`	`(*`	`Sapply_trans(trans, trans_args, strats)` : execute the transformation with the specified args, then for each generated subgoals execute the corresponding strat in strats. The length of the strat list must match the length of the generated subgoal list.	`*)`
`\|`	`Scont of string * string list * (Env.env -> Task.task -> proof_tree)`	`(*`	`Scont(trans, trans_args, strat_fn)` : execute the transformation with the specified args, then for each generated subgoals generate a new strat by applying `strat_fn` to the task of the subgoal. The new strat is then executed of the subgoal. Note that unlike with `Sapply_trans`, you don't need to know in advance the number of subgoals generated by the transformation.	`*)`
`\|`	`Scall_prover of (Whyconf.prover * float option * int option * int option) list * proof_tree`	`(*`	`Scall_prover((prover, timelimit, memlimit, steplimit) list, strat)` : Try to prove the goal with the specified provers. If no value is given for the limits, the default one is used. If no prover proves the goal, then strat is applied on it.	`*)`

exception StratFailure of string * exn

exception UnknownStrat of string

exception KnownStrat of string

type strat = Env.env -> Task.task -> proof_tree

type strat_with_args = string list ->
       Env.env ->
       Trans.naming_table -> Env.fformat -> Task.task -> proof_tree

val register_strat : desc:Pp.formatted -> string -> strat -> unit

val register_strat_with_args : desc:Pp.formatted -> string -> strat_with_args -> unit

type gen_strat =

`\|`	`Strat of strat`
`\|`	`StratWithArgs of strat_with_args`

val lookup_strat : string -> gen_strat

val list_strats : unit -> (string * Pp.formatted) list