driver.mli 2.83 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2018   --   Inria - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
5 6 7 8 9 10
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)
11

MARCHE Claude's avatar
MARCHE Claude committed
12
(** Managing the drivers for external provers *)
MARCHE Claude's avatar
API doc  
MARCHE Claude committed
13

Piotr Trojanek's avatar
Piotr Trojanek committed
14
(** {2 Create a driver} *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
15

Andrei Paskevich's avatar
Andrei Paskevich committed
16
type driver
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
17

18
val load_driver_absolute :  Env.env -> string -> string list -> driver
MARCHE Claude's avatar
API doc  
MARCHE Claude committed
19
(** loads a driver from a file
20
    @param env    environment to interpret theories
21
    @param string driver file name (absolute path name)
22
    @param string list additional driver files containing only theories
MARCHE Claude's avatar
API doc  
MARCHE Claude committed
23
*)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
24

Piotr Trojanek's avatar
Piotr Trojanek committed
25
(** {2 Use a driver} *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
26

27
val file_of_task : driver -> string -> string -> Task.task -> string
MARCHE Claude's avatar
MARCHE Claude committed
28
(** [file_of_task d f th t] produces a filename
29 30
    for the prover of driver [d], for a task [t] generated
    from  a goal in theory named [th] of filename [f]
MARCHE Claude's avatar
MARCHE Claude committed
31
*)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
32

33 34 35 36
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] *)

37
val call_on_buffer :
38 39
  command      : string ->
  limit        : Call_provers.resource_limit ->
40
  gen_new_file : bool ->
41 42
  ?inplace     : bool ->
  filename     : string ->
43
  printer_mapping : Printer.printer_mapping ->
Andrei Paskevich's avatar
Andrei Paskevich committed
44
  driver -> Buffer.t -> Call_provers.prover_call
45

46

47
val print_task :
48
  ?old       : in_channel ->
49
  driver -> Format.formatter -> Task.task -> unit
50

51 52 53 54 55
val print_theory :
  ?old       : in_channel ->
  driver -> Format.formatter -> Theory.theory -> unit
  (** produce a realization of the given theory using the given driver *)

56
val prove_task :
57 58 59 60
  command      : string ->
  limit        : Call_provers.resource_limit ->
  ?old         : string ->
  ?inplace     : bool ->
61
  ?interactive : bool ->
Andrei Paskevich's avatar
Andrei Paskevich committed
62
  driver -> Task.task -> Call_provers.prover_call
63

64
(** Split the previous function in two simpler functions *)
65 66

(* Apply driver's transformations to the task *)
67
val prepare_task : driver -> Task.task -> Task.task
68

69 70
val print_task_prepared :
  ?old       : in_channel ->
71
  driver -> Format.formatter -> Task.task -> Printer.printer_mapping
72 73

val prove_task_prepared :
74 75 76 77
  command      : string ->
  limit        : Call_provers.resource_limit ->
  ?old         : string ->
  ?inplace     : bool ->
78
  ?interactive : bool ->
Andrei Paskevich's avatar
Andrei Paskevich committed
79
  driver -> Task.task -> Call_provers.prover_call
MARCHE Claude's avatar
MARCHE Claude committed
80

81 82 83 84

(** Traverse all metas from a driver *)

val syntax_map: driver -> Printer.syntax_map