module Printer:sig
..end
Utility functions for implementing printers for various provers
exception BadSyntaxKind of char
Register printers
typeprelude =
string list
typeprelude_map =
prelude Ident.Mid.t
typeprelude_export_map =
prelude Ident.Mid.t
typeinterface =
string list
typeinterface_map =
interface Ident.Mid.t
typeinterface_export_map =
interface Ident.Mid.t
typeblacklist =
string list
type
field_info = {
|
field_name : |
(* | Printed field name | *) |
|
field_trace : |
(* | Model trace of the field, or | *) |
|
field_ident : |
(* | Identifier of the field | *) |
}
type
printing_info = {
|
why3_env : |
(* | The Why3 environment, retrieved from | *) |
|
vc_term_loc : |
(* | The position of the term that triggers the VC | *) |
|
vc_term_attrs : |
(* | The attributes of the term that triggers the VC | *) |
|
queried_terms : |
(* | The list of terms that were queried for the counter-example by the printer | *) |
|
type_coercions : |
(* | For each type, the set of lsymbols defining a coercion to this type. | *) |
|
type_fields : |
(* | For each type, the list of lsymbols defining the fields for this record type and associated to meta_record_def. | *) |
|
type_sorts : |
(* | Sorts defined in the prover output file. | *) |
|
record_fields : |
(* | Descriptions of the fields of all records. | *) |
|
constructors : |
(* | Constructors. | *) |
|
set_str : |
(* | List of attributes corresponding to a printed constants (that was on the immediate term, not inside the ident) | *) |
}
The printing info is collected while printing a task to trace back elements in the output of the printer to elements in the task and the AST.
val default_printing_info : Env.env -> printing_info
Empty mapping
type
printer_args = {
|
env : |
|
prelude : |
|
th_prelude : |
|
blacklist : |
|
printing_info : |
}
typeprinter =
printer_args -> ?old:Stdlib.in_channel -> Task.task Pp.pp
A printer receives a printer_args
which is created from the information
contained in the driver file. old
is used for interactive prover where
users edits the file. In this case the printer should try to keep the user
edited part as much as possible
val register_printer : desc:Pp.formatted -> string -> printer -> unit
register_printer ~desc name printer
Register the printer printer
so that
drivers of prover can mention it using name
.
val lookup_printer : string -> printer
val list_printers : unit -> (string * Pp.formatted) list
List registered printers
val print_prelude : prelude Pp.pp
Print a prelude
val print_th_prelude : Task.task -> prelude_map Pp.pp
print the prelude of the theory present in the task
val print_interface : interface Pp.pp
val meta_syntax_type : Theory.meta
Meta used to mark in a task type that are associated with a syntax. Mainly used for the transformation which eliminate definitions of builtin type.
val meta_syntax_logic : Theory.meta
Meta used to mark in a task function that are associated with a syntax.
val meta_syntax_literal : Theory.meta
Meta used to mark in a task literals that will be printed particularly.
val meta_remove_prop : Theory.meta
Meta used to mark in a task proposition that must be removed before printing
val meta_remove_logic : Theory.meta
Meta used to mark in a task function that must be removed before printing
val meta_remove_type : Theory.meta
Meta used to mark in a task type that must be removed before printing
val meta_remove_def : Theory.meta
Meta used to mark in a task function that must be removed before printing
val meta_realized_theory : Theory.meta
Meta used for implementing modular realization of theories. The meta stores the association between a module and the name that should be used
val syntax_type : Ty.tysymbol -> string -> bool -> Theory.tdecl
create a meta declaration for the builtin syntax of a type
val syntax_logic : Term.lsymbol -> string -> bool -> Theory.tdecl
create a meta declaration for the builtin syntax of a function
val syntax_literal : Ty.tysymbol -> string -> bool -> Theory.tdecl
create a meta declaration for the builtin syntax of a literal
val remove_prop : Decl.prsymbol -> Theory.tdecl
create a meta declaration for a proposition to remove
val check_syntax_type : Ty.tysymbol -> string -> unit
check_syntax_type tys syntax
check that syntax
doesn't mention arguments
that tys
doesn't have
val check_syntax_logic : Term.lsymbol -> string -> unit
check_syntax_logic ls syntax
check that syntax
doesn't mention arguments
that ls
doesn't have
typesyntax_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
syntax_arguments templ print_arg fmt l
prints in the
formatter fmt
the list l
using the syntax templ
, and the printer
print_arg
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
syntax_arguments_typed templ print_arg print_type t fmt l
prints in the formatter fmt
the list l
using the template templ
, the
printers print_arg
and print_type
.
The term t
should be akin to Tapp (_, l)
and is used to fill "%t0"
and "%si"
.
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 : (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
Should be used by the printer for handling the error of an unsupported type
val unsupportedTerm : Term.term -> string -> 'a
Should be used by the printer for handling the error of an unsupported term
val unsupportedPattern : Term.pattern -> string -> 'a
Should be used by the printer for handling the error of an unsupported pattern
val unsupportedDecl : Decl.decl -> string -> 'a
Should be used by the printer for handling the error of an unsupported declaration
val notImplemented : string -> 'a
Should be used by the printer for handling partial implementation
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
:
f arg
if f arg
does not raise Printer.Unsupported
exceptionUnsupportedType (arg,s)
if f arg
raises Unsupported s
val catch_unsupportedTerm : (Term.term -> 'a) -> Term.term -> 'a
same as Printer.catch_unsupportedType
but use Printer.UnsupportedTerm
instead of Printer.UnsupportedType
val catch_unsupportedDecl : (Decl.decl -> 'a) -> Decl.decl -> 'a
same as Printer.catch_unsupportedType
but use Printer.UnsupportedDecl
instead of Printer.UnsupportedType