Module Ptree_helpers.I

module I: sig .. end

Extra helpers for creating declarations in top-down style, imperative interface. Beware that these functions are not thread-safe

val begin_module : ?loc:Why3.Loc.position -> ?intf:Why3.Ptree.qualid -> string -> unit

see begin_module above

val use : ?loc:Why3.Loc.position -> import:bool -> string list -> unit

see use_import above

val add_prop : Why3.Decl.prop_kind ->
       ?loc:Why3.Loc.position -> string -> Why3.Ptree.term -> unit

val add_global_var_decl : Why3.Ptree.pty -> string -> Why3.Ptree.ident

val begin_let : ?ghost:bool ->
       ?diverges:bool ->
       ?ret_type:Why3.Ptree.pty -> string -> Why3.Ptree.binder list -> unit

val add_pre : Why3.Ptree.term -> unit

val add_writes : Why3.Ptree.term list -> unit

val add_post : Why3.Ptree.term -> unit

val add_body : Why3.Ptree.expr -> unit

val end_module : unit -> unit

val get_mlw_file : unit -> Why3.Ptree.mlw_file