sig
  type 'ty data = {
    data_id : ID.t;
    data_args : 'ty Var.t list;
    data_ty : 'ty;
    data_cstors : (ID.t * 'ty) list;
  }
  type attr = A_AC
  type attrs = Statement.attr list
  type ('f, 't, 'ty) view =
      TyDecl of ID.t * 'ty
    | Data of 'ty Statement.data list
    | Def of ID.t * 'ty * 't
    | RewriteTerm of ID.t * 'ty * 't list * 't
    | RewriteForm of 't SLiteral.t * 'f list
    | Assert of 'f
    | Lemma of 'f list
    | Goal of 'f
    | NegatedGoal of 'f list
  type ('f, 't, 'ty, 'meta) t = {
    view : ('f, 't, 'ty) Statement.view;
    attrs : Statement.attrs;
    src : 'meta;
  }
  type ('f, 't, 'ty) sourced_t = ('f, 't, 'ty, StatementSrc.t) Statement.t
  type clause = FOTerm.t SLiteral.t list
  type clause_t = (Statement.clause, FOTerm.t, Type.t) Statement.sourced_t
  val view : ('f, 't, 'ty, 'a) Statement.t -> ('f, 't, 'ty) Statement.view
  val attrs : ('a, 'b, 'c, 'd) Statement.t -> Statement.attrs
  val src : ('a, 'b, 'c, 'src) Statement.t -> 'src
  val mk_data :
    ID.t ->
    args:'ty Var.t list -> 'ty -> (ID.t * 'ty) list -> 'ty Statement.data
  val ty_decl :
    ?attrs:Statement.attrs ->
    src:'src -> ID.t -> 'ty -> ('a, 'b, 'ty, 'src) Statement.t
  val def :
    ?attrs:Statement.attrs ->
    src:'src -> ID.t -> 'ty -> 't -> ('a, 't, 'ty, 'src) Statement.t
  val rewrite_term :
    ?attrs:Statement.attrs ->
    src:'src ->
    ID.t -> 'ty -> 't list -> 't -> ('a, 't, 'ty, 'src) Statement.t
  val rewrite_form :
    ?attrs:Statement.attrs ->
    src:'src -> 't SLiteral.t -> 'f list -> ('f, 't, 'a, 'src) Statement.t
  val data :
    ?attrs:Statement.attrs ->
    src:'src -> 'ty Statement.data list -> ('a, 'b, 'ty, 'src) Statement.t
  val assert_ :
    ?attrs:Statement.attrs ->
    src:'src -> 'f -> ('f, 'a, 'b, 'src) Statement.t
  val lemma :
    ?attrs:Statement.attrs ->
    src:'src -> 'f list -> ('f, 'a, 'b, 'src) Statement.t
  val goal :
    ?attrs:Statement.attrs ->
    src:'src -> 'f -> ('f, 'a, 'b, 'src) Statement.t
  val neg_goal :
    ?attrs:Statement.attrs ->
    src:'src -> 'f list -> ('f, 'a, 'b, 'src) Statement.t
  val signature :
    ?init:Signature.t ->
    ('a, 'b, Type.t, 'c) Statement.t Sequence.t -> Signature.t
  val add_src :
    file:string ->
    ('f, 't, 'ty, UntypedAST.attrs) Statement.t ->
    ('f, 't, 'ty, StatementSrc.t) Statement.t
  val map_data :
    ty:('ty1 -> 'ty2) -> 'ty1 Statement.data -> 'ty2 Statement.data
  val map :
    form:('f1 -> 'f2) ->
    term:('t1 -> 't2) ->
    ty:('ty1 -> 'ty2) ->
    ('f1, 't1, 'ty1, 'src) Statement.t -> ('f2, 't2, 'ty2, 'src) Statement.t
  val map_src :
    f:('a -> 'b) ->
    ('f, 't, 'ty, 'a) Statement.t -> ('f, 't, 'ty, 'b) Statement.t
  val as_defined_cst : ID.t -> int option
  val is_defined_cst : ID.t -> bool
  val declare_defined_cst : ID.t -> int -> unit
  val scan_stmt_for_defined_cst : ('a, FOTerm.t, 'b, 'c) Statement.t -> unit
  exception Payload_defined_cst of int
  module Seq :
    sig
      val ty_decls : ('a, 'b, 'ty, 'c) Statement.t -> (ID.t * 'ty) Sequence.t
      val forms : ('f, 'a, 'b, 'c) Statement.t -> 'f Sequence.t
      val lits :
        (Statement.clause, 'a, 'b, 'c) Statement.t ->
        FOTerm.t SLiteral.t Sequence.t
      val terms :
        (Statement.clause, 'a, 'b, 'c) Statement.t -> FOTerm.t Sequence.t
      val symbols :
        (Statement.clause, FOTerm.t, Type.t, 'a) Statement.t ->
        ID.t Sequence.t
    end
  val pp :
    'a CCFormat.printer ->
    'b CCFormat.printer ->
    'c CCFormat.printer -> ('a, 'b, 'c, 'd) Statement.t CCFormat.printer
  val to_string :
    'a CCFormat.printer ->
    'b CCFormat.printer ->
    'c CCFormat.printer -> ('a, 'b, 'c, 'd) Statement.t -> string
  val pp_clause : Statement.clause_t CCFormat.printer
  module TPTP :
    sig
      val pp :
        'a CCFormat.printer ->
        'b CCFormat.printer ->
        'c CCFormat.printer -> ('a, 'b, 'c) sourced_t CCFormat.printer
      val to_string :
        'a CCFormat.printer ->
        'b CCFormat.printer ->
        'c CCFormat.printer -> ('a, 'b, 'c) sourced_t -> string
    end
end