Module Printer

module Printer: sig .. end

exception BadSyntaxKind of char

Register printers

type prelude = string list 
type prelude_map = prelude Ident.Mid.t 
type prelude_export_map = prelude Ident.Mid.t 
type interface = string list 
type interface_map = interface Ident.Mid.t 
type interface_export_map = interface Ident.Mid.t 
type blacklist = string list 
type field_info = {
   field_name : string; (*

Printed field name

*)
   field_trace : string; (*

Model trace of the field, or ""

*)
   field_ident : Ident.ident option; (*

Identifier of the field

*)
}
type printer_mapping = {
   lsymbol_m : string -> Term.lsymbol;
   vc_term_loc : Loc.position option;
   vc_term_attrs : Ident.Sattr.t;
   queried_terms : Term.term Wstdlib.Mstr.t;
   list_projections : Ident.ident Wstdlib.Mstr.t;
   list_fields : Ident.ident Wstdlib.Mstr.t;
   list_records : field_info list Wstdlib.Mstr.t;
   noarg_constructors : string list;
   set_str : Ident.Sattr.t Wstdlib.Mstr.t;
}
val list_projs : printer_mapping -> Ident.ident Wstdlib.Mstr.t

Return the union of projections and fields of a printer_mapping

type printer_args = {
   env : Env.env;
   prelude : prelude;
   th_prelude : prelude_map;
   blacklist : blacklist;
   mutable printer_mapping : printer_mapping;
}
type printer = printer_args -> ?old:Stdlib.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_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_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 -> syntax_map
val add_syntax_map : Theory.tdecl -> syntax_map -> syntax_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 syntax_arity : string -> int

syntax_arity s returns the largest i such that the parameter %i occurs in s. Formatting an argument list for s will only succeed if the argument list has size syntax_arity s or more.

val syntax_arguments_prec : string -> (int -> 'a Pp.pp) -> int list -> 'a list Pp.pp

syntax_arguments_prec templ print_arg prec_list fmt l prints in the formatter fmt the list l using the template templ, the printer print_arg, and the precedence list prec_list

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

syntax_arguments_typed_prec templ print_arg print_type t prec_list fmt l prints in the formatter fmt the list l using the template templ, the printers print_arg and print_type, and the precedence list prec_list. The term t should be akin to Tapp (_, l) and is used to fill "%t0" and "%si".

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

pretty-printing transformations (useful for caching)

val on_syntax_map : (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

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