sig
  exception BadSyntaxKind of char
  type prelude = string list
  type prelude_map = Printer.prelude Ident.Mid.t
  type prelude_export_map = Printer.prelude Ident.Mid.t
  type interface = string list
  type interface_map = Printer.interface Ident.Mid.t
  type interface_export_map = Printer.interface Ident.Mid.t
  type blacklist = string list
  type field_info = {
    field_name : string;
    field_trace : string;
    field_ident : Ident.ident option;
  }
  type printing_info = {
    why3_env : Env.env;
    vc_term_loc : Loc.position option;
    vc_term_attrs : Ident.Sattr.t;
    queried_terms :
      (Term.lsymbol * Loc.position option * Ident.Sattr.t) Wstdlib.Mstr.t;
    type_coercions : Term.Sls.t Ty.Mty.t;
    type_fields : Term.lsymbol list Ty.Mty.t;
    type_sorts : Ty.ty Wstdlib.Mstr.t;
    record_fields : Term.lsymbol list Term.Mls.t;
    constructors : Term.lsymbol Wstdlib.Mstr.t;
    set_str : Ident.Sattr.t Wstdlib.Mstr.t;
  }
  val default_printing_info : Env.env -> Printer.printing_info
  type printer_args = {
    env : Env.env;
    prelude : Printer.prelude;
    th_prelude : Printer.prelude_map;
    blacklist : Printer.blacklist;
    printing_info : Printer.printing_info option Stdlib.ref;
  }
  type printer =
      Printer.printer_args -> ?old:Stdlib.in_channel -> Task.task Pp.pp
  val register_printer :
    desc:Pp.formatted -> string -> Printer.printer -> unit
  val lookup_printer : string -> Printer.printer
  val list_printers : unit -> (string * Pp.formatted) list
  val print_prelude : Printer.prelude Pp.pp
  val print_th_prelude : Task.task -> Printer.prelude_map Pp.pp
  val print_interface : Printer.interface Pp.pp
  val meta_syntax_type : Theory.meta
  val meta_syntax_logic : Theory.meta
  val meta_syntax_literal : Theory.meta
  val meta_remove_prop : Theory.meta
  val meta_remove_logic : Theory.meta
  val meta_remove_type : Theory.meta
  val meta_remove_def : Theory.meta
  val meta_realized_theory : Theory.meta
  val syntax_type : Ty.tysymbol -> string -> bool -> Theory.tdecl
  val syntax_logic : Term.lsymbol -> string -> bool -> Theory.tdecl
  val syntax_literal : Ty.tysymbol -> string -> bool -> Theory.tdecl
  val remove_prop : Decl.prsymbol -> Theory.tdecl
  val check_syntax_type : Ty.tysymbol -> string -> unit
  val check_syntax_logic : Term.lsymbol -> string -> unit
  type syntax_map = (string * int) Ident.Mid.t
  val get_syntax_map : Task.task -> Printer.syntax_map
  val add_syntax_map :
    Theory.tdecl -> Printer.syntax_map -> Printer.syntax_map
  val get_rliteral_map : Task.task -> Printer.syntax_map
  val add_rliteral_map :
    Theory.tdecl -> Printer.syntax_map -> Printer.syntax_map
  val query_syntax : Printer.syntax_map -> Ident.ident -> string option
  val syntax_arity : string -> int
  val syntax_arguments_prec :
    string -> (int -> 'a Pp.pp) -> int list -> 'a list Pp.pp
  val syntax_arguments : string -> 'a Pp.pp -> 'a list Pp.pp
  val gen_syntax_arguments_prec :
    Stdlib.Format.formatter ->
    string ->
    (Stdlib.Format.formatter -> int -> char option -> int -> unit) ->
    int list -> unit
  val syntax_arguments_typed_prec :
    string ->
    (int -> Term.term Pp.pp) ->
    Ty.ty Pp.pp -> Term.term -> int list -> Term.term list Pp.pp
  val syntax_arguments_typed :
    string ->
    Term.term Pp.pp -> Ty.ty Pp.pp -> Term.term -> Term.term list Pp.pp
  val syntax_range_literal :
    ?cb:Number.int_constant Pp.pp option ->
    string -> Number.int_constant Pp.pp
  val syntax_float_literal :
    string -> Number.float_format -> Number.real_constant Pp.pp
  val on_syntax_map :
    (Printer.syntax_map -> 'a Trans.trans) -> 'a Trans.trans
  val sprint_tdecl :
    ('a -> Stdlib.Format.formatter -> Theory.tdecl -> 'a * string list) ->
    Theory.tdecl -> 'a * string list -> 'a * string list
  val sprint_decl :
    ('a -> Stdlib.Format.formatter -> Decl.decl -> 'a * string list) ->
    Theory.tdecl -> 'a * string list -> 'a * string list
  exception UnsupportedType of Ty.ty * string
  exception UnsupportedTerm of Term.term * string
  exception UnsupportedDecl of Decl.decl * string
  exception NotImplemented of string
  val unsupportedType : Ty.ty -> string -> 'a
  val unsupportedTerm : Term.term -> string -> 'a
  val unsupportedPattern : Term.pattern -> string -> 'a
  val unsupportedDecl : Decl.decl -> string -> 'a
  val notImplemented : string -> 'a
  exception Unsupported of string
  val unsupported : string -> 'a
  val catch_unsupportedType : (Ty.ty -> 'a) -> Ty.ty -> 'a
  val catch_unsupportedTerm : (Term.term -> 'a) -> Term.term -> 'a
  val catch_unsupportedDecl : (Decl.decl -> 'a) -> Decl.decl -> 'a
end