Module Ptree_helpers.F

module F: sig .. end

Extra helpers for creating declarations in top-down style, functional interface

type state

val create : unit -> state

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

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

see use_import above

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

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

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

val add_pre : state -> Why3.Ptree.term -> state

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

val add_post : state -> Why3.Ptree.term -> state

val add_body : state -> Why3.Ptree.expr -> state

val end_module : state -> state

val get_mlw_file : state -> Why3.Ptree.mlw_file