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_literal : Printer.syntax_map;
  9. drv_prec : int list Ident.Mid.t;
}
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. literal : Printer.syntax_map;
  8. prec : int list Ident.Mid.t;
}
val load_driver : Env.env -> string -> string list -> driver
type filename_generator = ?fname:string -> Pmodule.pmodule -> string
type decl_printer = printer_args -> ?old:in_channel -> ?fname:string -> flat:bool -> Pmodule.pmodule -> Mltree.decl Pp.pp
type border_printer = printer_args -> ?old:in_channel -> ?fname:string -> flat:bool -> Pmodule.pmodule Pp.pp
type prelude_printer = printer_args -> ?old:in_channel -> ?fname:string -> flat:bool -> Pmodule.pmodule list -> Pmodule.pmodule Pp.pp
type file_printer = {
  1. filename_generator : filename_generator;
  2. decl_printer : decl_printer;
  3. header_printer : border_printer;
  4. prelude_printer : prelude_printer;
  5. footer_printer : border_printer;
}
type printer = {
  1. desc : Pp.formatted;
  2. implem_printer : file_printer;
  3. interf_printer : file_printer option;
}
val dummy_prelude_printer : prelude_printer
val dummy_border_printer : border_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.