Module Logtk.UntypedAST

Main AST before Typing

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 * (string option * ty) list) list;
}

Basic definition of inductive types

type attr =
| A_app of string * attr list
| A_quoted of string
| A_list of attr list

Attributes (general terms)

type attrs = attr list
type def = {
def_id : string;
def_ty : ty;
def_rules : term list;
}
type statement_view =
| Include of string
| Decl of string * ty
| Def of def list
| Rewrite of term
| Data of data list
| Assert of form
| Lemma of form
| Goal of form

Statement

type statement = {
stmt : statement_view;
attrs : attrs;
loc : Loc.t option;
}
val default_attrs : attrs
val mk_def : string -> ty -> term list -> def
val include_ : ?⁠loc:Loc.t -> ?⁠attrs:attrs -> string -> statement
val decl : ?⁠loc:Loc.t -> ?⁠attrs:attrs -> string -> ty -> statement
val def : ?⁠loc:Loc.t -> ?⁠attrs:attrs -> def list -> statement
val data : ?⁠loc:Loc.t -> ?⁠attrs:attrs -> data list -> statement
val rewrite : ?⁠loc:Loc.t -> ?⁠attrs:attrs -> term -> statement
val assert_ : ?⁠loc:Loc.t -> ?⁠attrs:attrs -> term -> statement
val lemma : ?⁠loc:Loc.t -> ?⁠attrs:attrs -> term -> statement
val goal : ?⁠loc:Loc.t -> ?⁠attrs:attrs -> term -> statement
val name_of_attrs : attrs -> string option
val name : statement -> string option
module A : sig ... end
val attr_name : string -> attr
val attr_ac : attr
val attr_prefix : string -> attr
val attr_infix : string -> attr
val pp_attr : attr CCFormat.printer
val pp_attrs : attrs CCFormat.printer
val pp_attr_zf : attr CCFormat.printer
val pp_attrs_zf : attrs CCFormat.printer
val pp_attr_tstp : attr CCFormat.printer

Print as a TPTP general_term

val pp_statement : statement CCFormat.printer

Errors

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