package logtk

  1. Overview
  2. Docs
Core types and algorithms for logic

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (4)

Authors

  1. S
    Simon Cruanes
  2. P
    Petar Vukmirovic
  3. A
    Alexander Bentkamp
  4. S
    Sophie Tourret
  5. V
    Visa Nummelin

Maintainers

  1. S
    simon.cruanes.2007@m4x.org

Sources

2.0.tar.gz
md5=7a8e57388083ed763d12d18324c8a086
sha512=5c5ac312ada6b42907d1e91e349454a8375f7bf8165d3459721a40b707a840a3d6b3dc968a66f1040cb4de7aedf5c1c13f3e90b51337eae5ea6de41651d7bd63

doc/logtk/Logtk/UntypedAST/index.html

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