package logtk

  1. Overview
  2. Docs

Module Logtk.UntypedAST

Main AST before Typing

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 = ParseLocation
module T = STerm
type term = T.t
type ty = T.t
type form = T.t
type data = {
  1. data_name : string;
  2. data_vars : string list;
  3. data_cstors : (string * (string option * ty) list) list;
}

Basic definition of inductive types

type attr =
  1. | A_app of string * attr list
  2. | A_quoted of string
  3. | A_list of attr list

Attributes (general terms)

type attrs = attr list
type def = {
  1. def_id : string;
  2. def_ty : ty;
  3. def_rules : term list;
}
type statement_view =
  1. | Include of string
  2. | Decl of string * ty
  3. | Def of def list
  4. | Rewrite of term
  5. | Data of data list
  6. | Assert of form
  7. | Lemma of form
  8. | Goal of form

Statement

type statement = {
  1. stmt : statement_view;
  2. attrs : attrs;
  3. 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) format4 -> 'a