package why3

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
val black_list : string list
val fresh_printer : unit -> Ident.ident_printer
val iprinter : Ident.ident_printer
val forget_all : unit -> unit
val tv_set : Ident.Sid.t ref
val thprinter : Ident.ident_printer
val print_tv : Format.formatter -> Ty.tvsymbol -> unit
val print_tv_binder : Format.formatter -> Ty.tvsymbol -> unit
val print_params_list : Format.formatter -> Ty.tvsymbol list -> unit
val print_params : Format.formatter -> Ty.Stv.t -> unit
val forget_tvs : unit -> unit
val print_vs : Format.formatter -> Term.vsymbol -> unit
val forget_var : Term.vsymbol -> unit
val print_ts : Format.formatter -> Ty.tysymbol -> unit
val print_ls : Format.formatter -> Term.lsymbol -> unit
val print_pr : Format.formatter -> Decl.prsymbol -> unit
val print_name : Format.formatter -> Ident.ident -> unit
val get_th_name : Ident.ident -> string
type info = {
  1. info_syn : Printer.syntax_map;
  2. symbol_printers : (string * Theory.theory * Ident.ident_printer) Ident.Mid.t;
  3. realization : bool;
}
val print_path : string list Pp.pp
val print_id : Format.formatter -> Ident.ident -> unit
val print_id_real : info -> Format.formatter -> Ident.Mid.key -> unit
val print_ls_real : info -> Format.formatter -> Term.lsymbol -> unit
val print_ts_real : info -> Format.formatter -> Ty.tysymbol -> unit
val print_pr_real : info -> Format.formatter -> Decl.prsymbol -> unit
val print_ty : info -> Ty.ty Pp.pp
val unambig_fs : Term.lsymbol -> bool
val lparen_l : Format.formatter -> unit -> unit
val lparen_r : Format.formatter -> unit -> unit
val print_paren_l : 'a Pp.pp -> Format.formatter -> 'a list -> unit
val print_paren_r : 'a Pp.pp -> Format.formatter -> 'a list -> unit
val arrow : Format.formatter -> unit -> unit
val print_arrow_list : 'a Pp.pp -> Format.formatter -> 'a list -> unit
val print_space_list : 'a Pp.pp -> Format.formatter -> 'a list -> unit
val print_comma_list : 'a Pp.pp -> Format.formatter -> 'a list -> unit
val print_or_list : 'a Pp.pp -> Format.formatter -> 'a list -> unit
val comma_newline : Format.formatter -> unit -> unit
val print_pat : info -> Term.pattern Pp.pp
val print_vsty_nopar : info -> Format.formatter -> Term.vsymbol -> unit
val print_vsty : info -> Format.formatter -> Term.vsymbol -> unit
val is_tuple0_ty : Ty.ty option -> bool
val is_tuple_ty : Ty.ty option -> bool
val print_binop : Format.formatter -> Term.binop -> unit
val print_attr : 'a -> ('b * 'c) -> unit
val protect_on : bool -> ('a, 'b, 'c, 'd, 'e, 'f) format6 -> ('a, 'b, 'c, 'd, 'e, 'f) format6
val print_term : info -> Term.term Pp.pp
val print_fmla : info -> Term.term Pp.pp
val print_opl_term : info -> Format.formatter -> Term.term -> unit
val print_opl_fmla : info -> Format.formatter -> Term.term -> unit
val print_opr_term : info -> Format.formatter -> Term.term -> unit
val print_opr_fmla : info -> Format.formatter -> Term.term -> unit
val print_lrterm : bool -> bool -> info -> Format.formatter -> Term.term -> unit
val print_lrfmla : bool -> bool -> info -> Format.formatter -> Term.term -> unit
val print_tnode : bool -> bool -> info -> Format.formatter -> Term.term -> unit
val print_fnode : bool -> bool -> info -> Format.formatter -> Term.term -> unit
val print_tuple_pat : info -> Term.term -> Format.formatter -> Term.pattern -> unit
val print_branch : (info -> Format.formatter -> Term.term -> unit) -> info -> Format.formatter -> Term.term_branch -> unit
val print_branches : ?first:bool -> (info -> Term.term Pp.pp) -> info -> Format.formatter -> Term.term_branch list -> unit
val print_expr : info -> Format.formatter -> Term.term -> unit
val print_constr : info -> 'a -> Format.formatter -> (Term.lsymbol * 'b) -> unit
val ls_ty_vars : Term.lsymbol -> Ty.Stv.t * Ty.Stv.t * Ty.Stv.t
val clean_line : string -> string
type contents = string list
type chunk =
  1. | Edition of string * contents
  2. | Other of contents
val re_blank : Str.regexp
val re_why3 : Str.regexp
val read_old_script : in_channel -> chunk list
val print_contents : Format.formatter -> string list -> unit
val output_till_statement : Format.formatter -> chunk list ref -> string -> chunk option
val print_contents_in_comment : Format.formatter -> string list -> unit
val output_remaining : Format.formatter -> chunk list -> unit
val print_user_def : Format.formatter -> string list -> unit
val realization : Format.formatter -> info -> chunk option -> unit
val print_type_decl : prev:chunk option -> info -> Format.formatter -> Ty.tysymbol -> unit
val print_data_decl : info -> Format.formatter -> (Ty.tysymbol * (Term.lsymbol * 'a) list) -> unit
val print_ls_type : info -> Format.formatter -> Ty.ty option -> unit
val create_argument : Ty.ty -> Term.vsymbol
val print_arguments : info -> Format.formatter -> Term.vsymbol list -> unit
val re_macro : Str.regexp
val has_macro : string -> bool
val is_macro : info -> Format.formatter -> chunk option -> unit
val print_param_decl : prev:chunk option -> info -> Format.formatter -> Term.lsymbol -> unit
val print_logic_decl : prev:'a -> info -> Format.formatter -> (Term.lsymbol * Decl.ls_defn) -> unit
val print_recursive_decl : info -> Format.formatter -> (Term.lsymbol * Decl.ls_defn) -> unit
val print_ind : info -> Format.formatter -> (Decl.prsymbol * Term.term) -> unit
val print_ind_decl : info -> Format.formatter -> (Term.lsymbol * ('a * Term.term) list) -> unit
val re_lemma : Str.regexp
val find_lemma : string list -> string
val axiom_or_lemma : chunk option -> string
val print_prop_decl : prev:'a -> info -> Format.formatter -> (Decl.prop_kind * Decl.prsymbol * Term.term) -> unit
val print_decl : old:chunk list ref -> info -> Format.formatter -> Decl.decl -> unit
val print_decls : old:chunk list ref -> info -> Format.formatter -> Decl.decl list -> unit
val init_printer : Theory.theory -> Ident.ident_printer
val print_task : Printer.printer_args -> bool -> ?old:in_channel -> Format.formatter -> Task.task -> unit
val print_task_full : Printer.printer_args -> ?old:in_channel -> Format.formatter -> Task.task -> unit
val print_task_real : Printer.printer_args -> ?old:in_channel -> Format.formatter -> Task.task -> unit
OCaml

Innovation. Community. Security.