Module Driver

module Driver: sig .. end

Managing the drivers for external provers


Create a driver

type driver 
val load_driver_absolute : Env.env -> string -> string list -> driver

loads a driver from a file

Use a driver

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 call_on_buffer : command:string ->
limit:Call_provers.resource_limit ->
gen_new_file:bool ->
?inplace:bool ->
filename:string ->
printer_mapping:Printer.printer_mapping ->
driver -> Buffer.t -> Call_provers.prover_call
val print_task : ?old:Pervasives.in_channel ->
driver -> Format.formatter -> Task.task -> unit
val print_theory : ?old:Pervasives.in_channel ->
driver -> 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:Pervasives.in_channel ->
driver -> 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