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