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