package why3

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
val debug : Debug.flag
type driver = private {
  1. drv_env : Env.env;
  2. drv_printer : string option;
  3. drv_prelude : Printer.prelude;
  4. drv_thprelude : Printer.prelude_map;
  5. drv_thinterface : Printer.interface_map;
  6. drv_blacklist : Printer.blacklist;
  7. drv_syntax : Printer.syntax_map;
  8. drv_converter : Printer.syntax_map;
  9. drv_literal : Printer.syntax_map;
}
type printer_args = private {
  1. env : Env.env;
  2. prelude : Printer.prelude;
  3. thprelude : Printer.prelude_map;
  4. thinterface : Printer.interface_map;
  5. blacklist : Printer.blacklist;
  6. syntax : Printer.syntax_map;
  7. converter : Printer.syntax_map;
  8. literal : Printer.syntax_map;
}
val load_driver : Env.env -> string -> string list -> driver
type filename_generator = ?fname:string -> Pmodule.pmodule -> string
type interface_generator = ?fname:string -> Pmodule.pmodule -> string
type interf_printer = printer_args -> ?old:in_channel -> ?fname:string -> flat:bool -> Pmodule.pmodule -> Mltree.decl Pp.pp
type prelude_printer = printer_args -> ?old:in_channel -> ?fname:string -> flat:bool -> Pmodule.pmodule list -> Pmodule.pmodule Pp.pp
val print_empty_prelude : prelude_printer
type decl_printer = printer_args -> ?old:in_channel -> ?fname:string -> flat:bool -> Pmodule.pmodule -> Mltree.decl Pp.pp
type printer = {
  1. desc : Pp.formatted;
  2. file_gen : filename_generator;
  3. decl_printer : decl_printer;
  4. interf_gen : interface_generator option;
  5. interf_printer : interf_printer option;
  6. prelude_printer : prelude_printer;
}
val register_printer : string -> printer -> unit
val lookup_printer : driver -> printer_args * printer
val list_printers : unit -> (string * Pp.formatted) list
OCaml

Innovation. Community. Security.