sig
  type state
  val create : unit -> Ptree_helpers.F.state
  val begin_module :
    Ptree_helpers.F.state ->
    ?loc:Loc.position -> string -> Ptree_helpers.F.state
  val use :
    Ptree_helpers.F.state ->
    ?loc:Loc.position -> import:bool -> string list -> Ptree_helpers.F.state
  val add_prop :
    Ptree_helpers.F.state ->
    Decl.prop_kind ->
    ?loc:Loc.position -> string -> Ptree.term -> Ptree_helpers.F.state
  val add_global_var_decl :
    Ptree_helpers.F.state ->
    Ptree.pty -> string -> Ptree.ident * Ptree_helpers.F.state
  val begin_let :
    Ptree_helpers.F.state ->
    ?ghost:bool ->
    ?diverges:bool ->
    ?ret_type:Ptree.pty ->
    string -> Ptree.binder list -> Ptree_helpers.F.state
  val add_pre : Ptree_helpers.F.state -> Ptree.term -> Ptree_helpers.F.state
  val add_writes :
    Ptree_helpers.F.state -> Ptree.term list -> Ptree_helpers.F.state
  val add_post : Ptree_helpers.F.state -> Ptree.term -> Ptree_helpers.F.state
  val add_body : Ptree_helpers.F.state -> 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 -> Ptree.mlw_file
end