why3 1.3.1 · OCaml Package

why3

exception BadSyntaxKind of char

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 : Ident.ident Wstdlib.Mstr.t;
list_fields : Ident.ident Wstdlib.Mstr.t;
list_records : (string * string) list Wstdlib.Mstr.t;
noarg_constructors : string list;
set_str : Ident.Sattr.t 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_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

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

val syntax_arguments : string -> 'a Pp.pp -> 'a list Pp.pp

val gen_syntax_arguments_prec : 
  Format.formatter ->
  string ->
  (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

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

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