• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
    • Io
    • Defttag
    • Sys-call
    • Save-exec
    • Quicklisp
    • Std/io
    • Oslib
    • Bridge
    • Clex
      • Example-lexer
      • Sin
      • Matching-functions
      • Def-sin-progress
    • Tshell
    • Unsound-eval
    • Hacker
    • ACL2s-interface
    • Startup-banner
    • Command-line
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Interfacing-tools

Clex

Centaur Lexer Library.

This is a rudimentary library for creating lexers for character data in ACL2. It is an outgrowth and revision of lexer support routines that were originally developed as part of the ACL2::vl library.

These routines are based on ACL2 ACL2::characters. They are, accordingly, suitable for processing text in ASCII or ISO-8859-1 or some other 8-bit character set, but not Unicode or other wide character sets. It would generally be a bad idea to use CLEX to write a lexer for a language like Java or XML that needs Unicode support.

Many lexical analyzers like Flex are rather sophisticated and allow you to declare the syntax of your tokens at a relatively high level (e.g., via regular expressions); this description is then compiled into a full-blown scanner function.

In comparison, CLEX is quite primitive. Really, it is nothing more than some functions that tend to be useful when writing lexers "by hand." Even so, this is not so bad. Here are the things that CLEX provides:

• A stream input mechanism that is somewhat efficient and conveniently tracks your position (for good error messages).
• A defcharset macro for describing basic character types (e.g., whitespace, digits, letters, etc).
• Basic matching-functions for tokenizing input.
• Macros like def-sin-progress for proving that your lexers make progress.
• Lemmas about matching functions for proving basic "reconstruction" theorems.

Getting Started

Most users should simply load the top book in the library as follows:

(include-book "centaur/clex/top" :dir :system)

Besides this documentation, you may find it useful to see the example-lexer, located in centaur/clex/example.lisp; note that this example is not included in clex/top.

Subtopics

Example-lexer

A very basic lexer written using some CLEX utilities.

Sin

Abstract ACL2::stobj for a string input stream.

Matching-functions

Functions for matching text from the start of the input stream.

Def-sin-progress

Prove basic progress properties of a lexing function.