sig
  module Loc = ParseLocation
  module T = STerm
  type term = T.t
  type ty = T.t
  type form = T.t
  type data = {
    data_name : string;
    data_vars : string list;
    data_cstors : (string * UntypedAST.ty list) list;
  }
  type attr = A_name of string | A_AC
  type attrs = UntypedAST.attr list
  type statement_view =
      Include of string
    | Decl of string * UntypedAST.ty
    | Def of string * UntypedAST.ty * UntypedAST.term
    | Rewrite of UntypedAST.term
    | Data of UntypedAST.data list
    | Assert of UntypedAST.form
    | Lemma of UntypedAST.form
    | Goal of UntypedAST.form
  type statement = {
    stmt : UntypedAST.statement_view;
    attrs : UntypedAST.attrs;
    loc : Loc.t option;
  }
  val default_attrs : UntypedAST.attrs
  val include_ :
    ?loc:Loc.t -> ?attrs:UntypedAST.attrs -> string -> UntypedAST.statement
  val decl :
    ?loc:Loc.t ->
    ?attrs:UntypedAST.attrs ->
    string -> UntypedAST.ty -> UntypedAST.statement
  val def :
    ?loc:Loc.t ->
    ?attrs:UntypedAST.attrs ->
    string -> UntypedAST.ty -> UntypedAST.term -> UntypedAST.statement
  val data :
    ?loc:Loc.t ->
    ?attrs:UntypedAST.attrs -> UntypedAST.data list -> UntypedAST.statement
  val rewrite :
    ?loc:Loc.t ->
    ?attrs:UntypedAST.attrs -> UntypedAST.term -> UntypedAST.statement
  val assert_ :
    ?loc:Loc.t ->
    ?attrs:UntypedAST.attrs -> UntypedAST.term -> UntypedAST.statement
  val lemma :
    ?loc:Loc.t ->
    ?attrs:UntypedAST.attrs -> UntypedAST.term -> UntypedAST.statement
  val goal :
    ?loc:Loc.t ->
    ?attrs:UntypedAST.attrs -> UntypedAST.term -> UntypedAST.statement
  val name_of_attrs : UntypedAST.attrs -> string option
  val name : UntypedAST.statement -> string option
  val pp_attr : UntypedAST.attr CCFormat.printer
  val pp_attrs : UntypedAST.attrs CCFormat.printer
  val pp_statement : UntypedAST.statement CCFormat.printer
  exception Parse_error of Loc.t * string
  val error : Loc.t -> string -> 'a
  val errorf :
    Loc.t -> ('a, Format.formatter, unit, 'b) Pervasives.format4 -> 'a
end