pdriver.mli 2.07 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 *)

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

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

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

val lookup_printer : driver -> filename_generator * printer_args * printer
48 49 50

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

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