Module Printer

module Printer: sig .. end

Register printers

type prelude = string list 
type prelude_map = prelude Ident.Mid.t 
type interface = string list 
type interface_map = interface Ident.Mid.t 
type blacklist = string list 
type printer_mapping = {
   lsymbol_m : string -> Term.lsymbol;
   vc_term_loc : Loc.position option;
   queried_terms : Term.term Wstdlib.Mstr.t;
   list_projections : Wstdlib.Sstr.t;
   list_records : (string * string) list Wstdlib.Mstr.t;
}
type printer_args = {
   env : Env.env;
   prelude : prelude;
   th_prelude : prelude_map;
   blacklist : blacklist;
   mutable printer_mapping : printer_mapping;
}
type printer = printer_args -> ?old:Pervasives.in_channel -> Task.task Pp.pp 
val get_default_printer_mapping : printer_mapping
val register_printer : desc:Pp.formatted -> string -> printer -> unit
val lookup_printer : string -> printer
val list_printers : unit -> (string * Pp.formatted) list

Use printers

val print_prelude : prelude Pp.pp
val print_th_prelude : Task.task -> prelude_map Pp.pp
val print_interface : interface Pp.pp
val meta_syntax_type : Theory.meta
val meta_syntax_logic : Theory.meta
val meta_syntax_converter : 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_realized_theory : Theory.meta
val syntax_type : Ty.tysymbol -> string -> bool -> Theory.tdecl
val syntax_logic : Term.lsymbol -> string -> bool -> Theory.tdecl
val syntax_converter : 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 
type converter_map = (string * int) Term.Mls.t 
val get_syntax_map : Task.task -> syntax_map
val add_syntax_map : Theory.tdecl -> syntax_map -> syntax_map
val get_converter_map : Task.task -> converter_map
val get_rliteral_map : Task.task -> syntax_map
val add_rliteral_map : Theory.tdecl -> syntax_map -> syntax_map
val query_syntax : syntax_map -> Ident.ident -> string option
val query_converter : converter_map -> Term.lsymbol -> string option
val syntax_arguments : string -> 'a Pp.pp -> 'a list Pp.pp

(syntax_arguments templ print_arg fmt l) prints in the formatter fmt the list l using the template templ and the printer print_arg

val gen_syntax_arguments_typed : ('a -> 'b) ->
('a -> 'b array) -> string -> 'a Pp.pp -> 'b Pp.pp -> 'a -> 'a list Pp.pp
val syntax_arguments_typed : string -> Term.term Pp.pp -> Ty.ty Pp.pp -> Term.term -> Term.term list Pp.pp

(syntax_arguments templ print_arg fmt l) prints in the formatter fmt the list l using the template templ and the printer print_arg

val syntax_range_literal : string -> Number.integer_constant Pp.pp
val syntax_float_literal : string -> Number.float_format -> Number.real_constant Pp.pp

pretty-printing transformations (useful for caching)

val on_syntax_map : (syntax_map -> 'a Trans.trans) -> 'a Trans.trans
val on_converter_map : (converter_map -> 'a Trans.trans) -> 'a Trans.trans
val sprint_tdecl : ('a -> Format.formatter -> Theory.tdecl -> 'a * string list) ->
Theory.tdecl -> 'a * string list -> 'a * string list
val sprint_decl : ('a -> Format.formatter -> Decl.decl -> 'a * string list) ->
Theory.tdecl -> 'a * string list -> 'a * string list

Exceptions to use in transformations and printers

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

Functions that catch inner error

exception Unsupported of string

This exception must be raised only inside a call of one of the catch_* functions below

val unsupported : string -> 'a
val catch_unsupportedType : (Ty.ty -> 'a) -> Ty.ty -> 'a

catch_unsupportedType f return a function which applied on arg:

val catch_unsupportedTerm : (Term.term -> 'a) -> Term.term -> 'a

same as Printer.catch_unsupportedType but use UnsupportedExpr instead of UnsupportedType

val catch_unsupportedDecl : (Decl.decl -> 'a) -> Decl.decl -> 'a

same as Printer.catch_unsupportedType but use UnsupportedDecl instead of UnsupportedType