module Driver:sig
..end
Managing the drivers for external provers
type
driver
val load_driver_absolute : Env.env -> string -> string list -> driver
load_driver_absolute env f extras
loads the driver from a file
f
, completed with extra files from list extras
, in the context
of the environment env
val file_of_task : driver -> string -> string -> Task.task -> string
file_of_task d f th t
produces a filename
for the prover of driver d
, for a task t
generated
from a goal in theory named th
of filename f
val file_of_theory : driver -> string -> Theory.theory -> string
file_of_theory d f th
produces a filename
for the prover of driver d
, for a theory th
from filename f
val print_task : ?old:Stdlib.in_channel ->
driver -> Stdlib.Format.formatter -> Task.task -> unit
val print_theory : ?old:Stdlib.in_channel ->
driver -> Stdlib.Format.formatter -> Theory.theory -> unit
produce a realization of the given theory using the given driver
val prove_task : command:string ->
limit:Call_provers.resource_limit ->
?old:string ->
?inplace:bool ->
?interactive:bool -> driver -> Task.task -> Call_provers.prover_call
Split the previous function in two simpler functions
val prepare_task : driver -> Task.task -> Task.task
val print_task_prepared : ?old:Stdlib.in_channel ->
driver ->
Stdlib.Format.formatter -> Task.task -> Printer.printer_mapping
val prove_task_prepared : command:string ->
limit:Call_provers.resource_limit ->
?old:string ->
?inplace:bool ->
?interactive:bool -> driver -> Task.task -> Call_provers.prover_call
Traverse all metas from a driver
val syntax_map : driver -> Printer.syntax_map