pdriver.mli 2 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2016   --   INRIA - CNRS - Paris-Sud University  *)
(*                                                                  *)
(*  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.                           *)
(*                                                                  *)
(********************************************************************)

MARCHE Claude's avatar
MARCHE Claude committed
12 13
val debug : Debug.flag

14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39
type driver = private {
  drv_env         : Env.env;
  drv_printer     : string option;
  drv_prelude     : Printer.prelude;
  drv_thprelude   : Printer.prelude_map;
  drv_blacklist   : Printer.blacklist;
  drv_syntax      : Printer.syntax_map;
  drv_converter   : Printer.syntax_map;
}


type printer_args = private {
  env         : Env.env;
  prelude     : Printer.prelude;
  thprelude   : Printer.prelude_map;
  blacklist   : Printer.blacklist;
  syntax      : Printer.syntax_map;
  converter   : Printer.syntax_map;
}

val load_driver : Env.env -> string -> string list -> driver
  (** loads a driver from a file
      @param env    environment to interpret theories and modules
      @param string driver file name
      @param string list additional drivers containing only theories/modules *)

40 41
type printer =
  printer_args -> ?old:in_channel -> ?fname:string -> Pmodule.pmodule ->
Mário Pereira's avatar
Mário Pereira committed
42
  Compile.ML.decl Pp.pp
43

44
type filename_generator = ?fname:string -> Pmodule.pmodule -> string
45

46 47
val register_printer :
  desc:Pp.formatted -> string -> filename_generator -> printer -> unit
48 49

val lookup_printer : driver -> filename_generator * printer_args * printer
50 51 52

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

53
(*
54 55
val extract_module : ?old:in_channel ->
   driver -> Format.formatter -> Pmodule.pmodule -> unit
56
 *)