		Search-engine friendly clone of the ACL2 documentation.

Lexing-and-parsing

Token-fringe

Token fringe.

Signature
(token-fringe tree identifiers) → token-trees
Arguments: tree — Guard (abnf::treep tree).; identifiers — Guard (string-listp identifiers).
Returns: token-trees — Type (abnf::tree-listp token-trees).

Parsing organizes the sequence of tokens resulting from lexing into expressions, statements, etc. It would be thus natural to define the parsing of a Leo file via a parsing predicate that, analogously to grammar-lexp, relates a sequence of token CSTs to a file CST by saying that the sequence of token CSTs is at the fringe of the file CST.

However, the function abnf::tree->string returns a sequence of naturals, not a sequence of token CSTs. Thus, we need to define a function that returns the sequence of token CSTs at the fringe of a CST; this could be defined similarly to abnf::tree->string, but stopping the recursion when a token tree is encountered, instead of stopping the recursion when a leaf tree is encountered.

But this function cannot be defined exactly as described, because token CSTs do not actually appear in file CSTs. Instead, a file CST has subtrees of token CST, such as identifier CSTs; the reason should be clear looking at the syntactic grammar, which never references token directly, but rather identifier and other kinds of tokens. This means that the function must stop the recursion at these CSTs instead, and must also complete them to be token CSTs.

The following function, and its mutually recursive companions, formalizes the token fringe of a CST in the sense explained above:

A leaf CST that is a sequence of naturals that are a possible fringe of a keyword CST (i.e. a Unicode character sequence forming a keyword) yields the singleton sequence of the token CST whose subtree is the keyword subtree whose subtree is the original leaf CST.
A leaf CST that is a sequence of naturals that are a possible fringe of a symbol CST (i.e. a Unicode character sequence forming a symbol) yields the singleton sequence of the token CST whose subtree is the symbol subtree whose subtree is the initial leaf CST.
A leaf CST that is a sequence of naturals that are a possible fringe of an identifier CST (i.e. a Unicode character sequence forming an identifier) among a list explicitly passed to this ACL2 function yields the singleton sequence of the token CST whose subtree is the identifier subtree whose subtree is the original leaf CST.
For any other leaf CST, that is either a sequence of naturals or a rule name, we return nil, but this never happens in the course of a recursion that starts with a file CST.
An identifier or atomic literal or numeral CST yields a singleton sequence of the token CST whose subtree is the original CST.
Any other CST yields the token fringe of its subtrees (the recursion does not stop at the CST).
The token fringe of a list of CSTs is the concatenation of the token fringes of the CSTs.
The token fringe of a list of lists of CSTs is the concatenation of the token fringes of the CST lists.

Note that the special treatment, explained above, of leaf CSTs whose strings are identifiers (when the list of identifiers is not empty) does not affect the treatment of identifier CSTs, which are not leaf CSTs. For concrete motivations for this special treatment, see input-file-parsep and output-file-parsep.

Theorem: return-type-of-token-fringe.token-trees

(defthm return-type-of-token-fringe.token-trees
  (b* ((?token-trees (token-fringe tree identifiers)))
    (abnf::tree-listp token-trees))
  :rule-classes :rewrite)

Theorem: return-type-of-token-fringe-list.token-trees

(defthm return-type-of-token-fringe-list.token-trees
  (b* ((?token-trees (token-fringe-list trees identifiers)))
    (abnf::tree-listp token-trees))
  :rule-classes :rewrite)

Theorem: return-type-of-token-fringe-list-list.token-trees

(defthm return-type-of-token-fringe-list-list.token-trees
  (b* ((?token-trees (token-fringe-list-list treess identifiers)))
    (abnf::tree-listp token-trees))
  :rule-classes :rewrite)

Theorem: token-fringe-of-tree-fix-tree

(defthm token-fringe-of-tree-fix-tree
  (equal (token-fringe (abnf::tree-fix tree)
                       identifiers)
         (token-fringe tree identifiers)))

Theorem: token-fringe-of-string-list-fix-identifiers

(defthm token-fringe-of-string-list-fix-identifiers
  (equal (token-fringe tree (str::string-list-fix identifiers))
         (token-fringe tree identifiers)))

Theorem: token-fringe-list-of-tree-list-fix-trees

(defthm token-fringe-list-of-tree-list-fix-trees
  (equal (token-fringe-list (abnf::tree-list-fix trees)
                            identifiers)
         (token-fringe-list trees identifiers)))

Theorem: token-fringe-list-of-string-list-fix-identifiers

(defthm token-fringe-list-of-string-list-fix-identifiers
  (equal (token-fringe-list trees
                            (str::string-list-fix identifiers))
         (token-fringe-list trees identifiers)))

Theorem: token-fringe-list-list-of-tree-list-list-fix-treess

(defthm token-fringe-list-list-of-tree-list-list-fix-treess
  (equal (token-fringe-list-list (abnf::tree-list-list-fix treess)
                                 identifiers)
         (token-fringe-list-list treess identifiers)))

Theorem: token-fringe-list-list-of-string-list-fix-identifiers

(defthm token-fringe-list-list-of-string-list-fix-identifiers
  (equal (token-fringe-list-list treess
                                 (str::string-list-fix identifiers))
         (token-fringe-list-list treess identifiers)))

Theorem: token-fringe-tree-equiv-congruence-on-tree

(defthm token-fringe-tree-equiv-congruence-on-tree
  (implies (abnf::tree-equiv tree tree-equiv)
           (equal (token-fringe tree identifiers)
                  (token-fringe tree-equiv identifiers)))
  :rule-classes :congruence)

Theorem: token-fringe-string-list-equiv-congruence-on-identifiers

(defthm token-fringe-string-list-equiv-congruence-on-identifiers
  (implies (str::string-list-equiv identifiers identifiers-equiv)
           (equal (token-fringe tree identifiers)
                  (token-fringe tree identifiers-equiv)))
  :rule-classes :congruence)

Theorem: token-fringe-list-tree-list-equiv-congruence-on-trees

(defthm token-fringe-list-tree-list-equiv-congruence-on-trees
  (implies (abnf::tree-list-equiv trees trees-equiv)
           (equal (token-fringe-list trees identifiers)
                  (token-fringe-list trees-equiv identifiers)))
  :rule-classes :congruence)

Theorem: token-fringe-list-string-list-equiv-congruence-on-identifiers

(defthm
      token-fringe-list-string-list-equiv-congruence-on-identifiers
  (implies (str::string-list-equiv identifiers identifiers-equiv)
           (equal (token-fringe-list trees identifiers)
                  (token-fringe-list trees identifiers-equiv)))
  :rule-classes :congruence)

Theorem: token-fringe-list-list-tree-list-list-equiv-congruence-on-treess

(defthm
   token-fringe-list-list-tree-list-list-equiv-congruence-on-treess
 (implies (abnf::tree-list-list-equiv treess treess-equiv)
          (equal (token-fringe-list-list treess identifiers)
                 (token-fringe-list-list treess-equiv identifiers)))
 :rule-classes :congruence)

Theorem: token-fringe-list-list-string-list-equiv-congruence-on-identifiers

(defthm
 token-fringe-list-list-string-list-equiv-congruence-on-identifiers
 (implies (str::string-list-equiv identifiers identifiers-equiv)
          (equal (token-fringe-list-list treess identifiers)
                 (token-fringe-list-list treess identifiers-equiv)))
 :rule-classes :congruence)

Subtopics

Token-fringe-list-list
Token-fringe-list