Abs-raw-input-character
Abstract a raw-input-character tree to a Unicode character.
- Signature
(abs-raw-input-character tree) → unicode
- Arguments
- tree — Guard (abnf-tree-with-root-p tree "raw-input-character").
- Returns
- unicode — Type (unicodep unicode), given the guard.
A raw-input-character tree is essentially a single Unicode character,
which is unchanged by Java's first lexical translation step.
In other words, we abstract this kind of tree
to its single Unicode character.
A raw-input-character has a single subtree,
accessible via caar.
That subtree is a terminal leaf tree
with a single terminal (natural number)
in the range of Java Unicode characters.
That is the result.
Definitions and Theorems
Function: abs-raw-input-character
(defun abs-raw-input-character (tree)
(declare
(xargs :guard (abnf-tree-with-root-p tree "raw-input-character")))
(let ((__function__ 'abs-raw-input-character))
(declare (ignorable __function__))
(b* ((subtree (caar (abnf::tree-nonleaf->branches tree)))
(string (abnf::tree-leafterm->get subtree)))
(car string))))
Theorem: unicodep-of-abs-raw-input-character
(defthm unicodep-of-abs-raw-input-character
(implies (and (abnf-tree-with-root-p tree '"raw-input-character"))
(b* ((unicode (abs-raw-input-character tree)))
(unicodep unicode)))
:rule-classes :rewrite)
