sig
  val ident :
    ?attrs:Ptree.attr list -> ?loc:Loc.position -> string -> Ptree.ident
  val qualid : string list -> Ptree.qualid
  val const : ?kind:Number.int_literal_kind -> int -> Constant.constant
  val unit_binder : ?loc:Loc.position -> unit -> Ptree.binder list
  val one_binder :
    ?loc:Loc.position ->
    ?ghost:bool -> ?pty:Ptree.pty -> string -> Ptree.binder list
  val term : ?loc:Loc.position -> Ptree.term_desc -> Ptree.term
  val tconst : ?loc:Loc.position -> int -> Ptree.term
  val tvar : ?loc:Loc.position -> Ptree.qualid -> Ptree.term
  val tapp :
    ?loc:Loc.position -> Ptree.qualid -> Ptree.term list -> Ptree.term
  val pat : ?loc:Loc.position -> Ptree.pat_desc -> Ptree.pattern
  val pat_var : ?loc:Loc.position -> Ptree.ident -> Ptree.pattern
  val break_id : string
  val continue_id : string
  val return_id : string
  val expr : ?loc:Loc.position -> Ptree.expr_desc -> Ptree.expr
  val econst : ?loc:Loc.position -> int -> Ptree.expr
  val eapp :
    ?loc:Loc.position -> Ptree.qualid -> Ptree.expr list -> Ptree.expr
  val eapply : ?loc:Loc.position -> Ptree.expr -> Ptree.expr -> Ptree.expr
  val evar : ?loc:Loc.position -> Ptree.qualid -> Ptree.expr
  val empty_spec : Ptree.spec
  val use : ?loc:Loc.position -> import:bool -> string list -> Ptree.decl
  val global_var_decl : Ptree.pty -> string -> Ptree.ident * Ptree.decl
  module F :
    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
  module I :
    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
end