why3 1.1.1 · OCaml Package

why3

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: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

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

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

val syntax_range_literal : string -> Number.integer_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 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

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

package why3