Parsers eventually output this AST, that uses simple terms (STerm) for types, terms, and formulas.
Everything is possibly annotated with a parse location so that error messages can be properly localized.
module Loc = ParseLocationmodule T = STermtype term = T.ttype ty = T.ttype form = T.ttype data = {data_name : string;data_vars : string list;data_cstors : (string * (string option * ty) list) list;}Basic definition of inductive types
Attributes (general terms)
type attrs = attr listval default_attrs : attrsval name_of_attrs : attrs -> string optionval name : statement -> string optionmodule A : sig ... endval attr_name : string -> attrval attr_ac : attrval attr_prefix : string -> attrval attr_infix : string -> attrval pp_attr : attr CCFormat.printerval pp_attrs : attrs CCFormat.printerval pp_attr_zf : attr CCFormat.printerval pp_attrs_zf : attrs CCFormat.printerval pp_attr_tstp : attr CCFormat.printerPrint as a TPTP general_term
val pp_statement : statement CCFormat.printerexception Parse_error of Loc.t * stringval error : Loc.t -> string -> 'aval errorf :
Loc.t ->
('a, Stdlib.Format.formatter, unit, 'b) Stdlib.format4 ->
'a