why3 1.3.1 · OCaml Package

val optional_arg : Ident.attribute

val named_arg : Ident.attribute

val ocaml_remove : Ident.attribute

val is_optional : attrs:Ident.Sattr.t -> bool

val is_named : attrs:Ident.Sattr.t -> bool

val is_ocaml_remove : attrs:Ident.Sattr.t -> bool

val ocaml_keywords : string list

val _is_ocaml_keyword : Wstdlib.Hstr.key -> bool

val char_to_alnumusquote : char -> string

val iprinter : Ident.ident_printer

val aprinter : Ident.ident_printer

val tprinter : Ident.ident_printer

val forget_id : Ident.ident -> unit

val _forget_ids : Ident.ident list -> unit

val forget_var : (Ident.ident * 'a * 'b) -> unit

val forget_vars : (Ident.ident * Mltree.ty * Mltree.is_ghost) list -> unit

val forget_let_defn : Mltree.let_def -> unit

val forget_pat : Mltree.pat -> unit

val print_global_ident : 
  sanitizer:(string -> string) ->
  Format.formatter ->
  Ident.ident ->
  unit

val print_path : 
  sanitizer:(string -> string) ->
  Format.formatter ->
  (string list * Ident.ident) ->
  unit

val remove_prefix : 'a list -> 'a list -> 'a list

val is_local_id : info -> Ident.Sid.elt -> bool

exception Local

val print_qident : 
  sanitizer:(string -> string) ->
  info ->
  Format.formatter ->
  Ident.Sid.elt ->
  unit

val print_lident : info -> Format.formatter -> Ident.Sid.elt -> unit

val print_uident : info -> Format.formatter -> Ident.Sid.elt -> unit

val print_tv : use_quote:bool -> Format.formatter -> Ty.tvsymbol -> unit

val protect_on : 
  ?boxed:bool ->
  ?be:bool ->
  bool ->
  ('a, 'b, 'c, 'd, 'e, 'f) format6 ->
  ('a, 'b, 'c, 'd, 'e, 'f) format6

val star : Format.formatter -> unit -> unit

val print_list2 : 
  ('a -> unit -> 'b) ->
  ('a -> unit -> 'c) ->
  ('a -> 'd -> 'e) ->
  ('a -> 'f -> unit) ->
  'a ->
  ('d list * 'f list) ->
  unit

val complex_syntax : string -> bool

val print_record_proj : info -> Format.formatter -> Expr.rsymbol -> unit

val print_ty : use_quote:bool -> ?paren:bool -> info -> Mltree.ty Pp.pp

val print_vsty_opt : 
  info ->
  Format.formatter ->
  Ident.Sid.elt ->
  Mltree.ty ->
  unit

val print_vs_opt : info -> Format.formatter -> Ident.Sid.elt -> unit

val print_vsty_named : 
  info ->
  Format.formatter ->
  Ident.Sid.elt ->
  Mltree.ty ->
  unit

val print_vs_named : info -> Format.formatter -> Ident.Sid.elt -> unit

val print_vsty : 
  info ->
  Format.formatter ->
  (Ident.Sid.elt * Mltree.ty * 'a) ->
  unit

val print_vsty_opt_fun : 
  info ->
  Format.formatter ->
  Ident.ident ->
  Mltree.ty ->
  unit

val print_vsty_named_fun : 
  info ->
  Format.formatter ->
  Ident.ident ->
  Mltree.ty ->
  unit

val print_vsty_fun : 
  info ->
  Format.formatter ->
  (Ident.ident * Mltree.ty * 'a) ->
  unit

val print_vs_fun : info -> Format.formatter -> Ident.Sid.elt -> unit

val print_tv_arg : use_quote:bool -> Format.formatter -> Ty.tvsymbol -> unit

val print_tv_args : 
  use_quote:bool ->
  Format.formatter ->
  Ty.tvsymbol list ->
  unit

val print_vs_arg : 
  info ->
  Format.formatter ->
  (Ident.Sid.elt * Mltree.ty * 'a) ->
  unit

val get_record : info -> Expr.rsymbol -> Expr.rsymbol list

val print_pat : info -> int -> Mltree.pat Pp.pp

val print_papp : 
  info ->
  Term.lsymbol ->
  Format.formatter ->
  Mltree.pat list ->
  unit

val pv_name : Ity.pvsymbol -> Ident.ident

val print_pv : info -> Format.formatter -> Ity.pvsymbol -> unit

val is_true : Mltree.expr -> bool

val is_false : Mltree.expr -> bool

val is_field : Expr.rsymbol -> bool

val check_val_in_drv : info -> Loc.position option -> Ident.Sid.elt -> unit

val is_mapped_to_int : info -> Ity.ity -> bool

val print_constant : Format.formatter -> Mltree.expr -> unit

val print_for_direction : Format.formatter -> Mltree.for_direction -> unit

val print_apply_args : 
  info ->
  Format.formatter ->
  (Mltree.expr list * Ity.pvsymbol list) ->
  unit

val print_apply : 
  info ->
  int ->
  Expr.rsymbol ->
  Format.formatter ->
  Mltree.expr list ->
  unit

val print_svar : Format.formatter -> Ty.Stv.t -> unit

val print_fun_type_args : 
  info ->
  Format.formatter ->
  (Mltree.var list * Ty.Stv.t * Mltree.ty * Mltree.expr) ->
  unit

val print_let_def : 
  ?functor_arg:bool ->
  info ->
  Format.formatter ->
  Mltree.let_def ->
  unit

val print_expr : 
  ?boxed:bool ->
  ?opr:bool ->
  ?be:bool ->
  info ->
  int ->
  Mltree.expr Pp.pp

val print_branch : info -> Mltree.reg_branch Pp.pp

val print_raise : 
  paren:bool ->
  info ->
  Ity.xsymbol ->
  Format.formatter ->
  Mltree.expr option ->
  unit

val print_xbranch : info -> bool -> Mltree.exn_branch Pp.pp

val print_type_decl : 
  info ->
  bool ->
  Format.formatter ->
  Mltree.its_defn ->
  unit

val is_signature_decl : 'a -> Mltree.decl -> bool

val is_signature : 'a -> Mltree.decl list -> bool

val extract_functor_args : 
  'a ->
  Mltree.decl list ->
  (string * Mltree.decl list) list * Mltree.decl list

val print_top_val : 
  ?functor_arg:bool ->
  info ->
  Format.formatter ->
  (Ity.pvsymbol * Mltree.ty) ->
  unit

val print_functor_args : 
  info ->
  Format.formatter ->
  (string * Mltree.decl list) list ->
  unit

val print_decl : info -> Format.formatter -> Mltree.decl -> unit

package why3