sig
  type state
  val create : unit -> Ptree_helpers.F.state
  val begin_module :
    Ptree_helpers.F.state ->
    ?loc:Why3.Loc.position ->
    ?intf:Why3.Ptree.qualid -> string -> Ptree_helpers.F.state
  val use :
    Ptree_helpers.F.state ->
    ?loc:Why3.Loc.position ->
    import:bool -> string list -> Ptree_helpers.F.state
  val add_prop :
    Ptree_helpers.F.state ->
    Why3.Decl.prop_kind ->
    ?loc:Why3.Loc.position ->
    string -> Why3.Ptree.term -> Ptree_helpers.F.state
  val add_global_var_decl :
    Ptree_helpers.F.state ->
    Why3.Ptree.pty -> string -> Why3.Ptree.ident * Ptree_helpers.F.state
  val begin_let :
    Ptree_helpers.F.state ->
    ?ghost:bool ->
    ?diverges:bool ->
    ?ret_type:Why3.Ptree.pty ->
    string -> Why3.Ptree.binder list -> Ptree_helpers.F.state
  val add_pre :
    Ptree_helpers.F.state -> Why3.Ptree.term -> Ptree_helpers.F.state
  val add_writes :
    Ptree_helpers.F.state -> Why3.Ptree.term list -> Ptree_helpers.F.state
  val add_post :
    Ptree_helpers.F.state -> Why3.Ptree.term -> Ptree_helpers.F.state
  val add_body :
    Ptree_helpers.F.state -> Why3.Ptree.expr -> Ptree_helpers.F.state
  val end_module : Ptree_helpers.F.state -> Ptree_helpers.F.state
  val get_mlw_file : Ptree_helpers.F.state -> Why3.Ptree.mlw_file
end