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