pdriver.mli 2.85 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2019   --   Inria - CNRS - Paris-Sud University  *)
5 6 7 8 9 10 11
(*                                                                  *)
(*  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
type driver = private {
  drv_env         : Env.env;
  drv_printer     : string option;
  drv_prelude     : Printer.prelude;
  drv_thprelude   : Printer.prelude_map;
19
  drv_thinterface : Printer.interface_map;
20 21
  drv_blacklist   : Printer.blacklist;
  drv_syntax      : Printer.syntax_map;
22
  drv_literal     : Printer.syntax_map;
23
  drv_prec        : (int list) Ident.Mid.t;
24 25 26 27 28 29 30
}


type printer_args = private {
  env         : Env.env;
  prelude     : Printer.prelude;
  thprelude   : Printer.prelude_map;
31
  thinterface : Printer.interface_map;
32 33
  blacklist   : Printer.blacklist;
  syntax      : Printer.syntax_map;
34
  literal     : Printer.syntax_map;
35
  prec        : (int list) Ident.Mid.t;
36 37 38 39 40 41 42 43
}

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 *)

44 45 46 47 48 49 50 51 52 53 54
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

(** Things to do at the beginning of a module, e.g. open/#include.
    Only used in modular extraction. *)
type prelude_printer =
  printer_args -> ?old:in_channel -> ?fname:string -> flat:bool
55
  -> Pmodule.pmodule list -> Pmodule.pmodule Pp.pp
56 57 58 59

val print_empty_prelude: prelude_printer

type decl_printer =
60
  printer_args -> ?old:in_channel -> ?fname:string -> flat:bool ->
61
  Pmodule.pmodule -> Mltree.decl Pp.pp
62

63 64 65 66 67 68 69
type printer =
  { desc            : Pp.formatted;
    file_gen        : filename_generator;
    decl_printer    : decl_printer;
    interf_gen      : interface_generator option;
    interf_printer  : interf_printer option;
    prelude_printer : prelude_printer; }
70

71
val register_printer : string -> printer -> unit
72

73
val lookup_printer : driver -> printer_args * printer
74 75 76

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

77
(*
78 79
val extract_module : ?old:in_channel ->
   driver -> Format.formatter -> Pmodule.pmodule -> unit
80
 *)