		Search-engine friendly clone of the ACL2 documentation.

Concrete-syntax-validation

Validation of the concrete syntax grammar.

We show that rules of the grammar of the ABNF concrete syntax:

Are well-formed.
Are closed.
Generate only strings of ASCII codes.
Are the same (module ordering) as the resulting of plugging the core rules into the concrete syntax rules.

These theorems are in a separate file so that the definition of the concrete syntax does not depend on the grammar operations, as also done for core-rules-validation and for concrete-syntax-rules-validation.

Theorem: rulelist-wfp-of-*grammar*

(defthm rulelist-wfp-of-*grammar*
  (rulelist-wfp *grammar*))

Theorem: rulelist-closedp-of-*grammar*

(defthm rulelist-closedp-of-*grammar*
  (rulelist-closedp *grammar*))

Theorem: ascii-only-*grammar*

(defthm ascii-only-*grammar*
  (rulelist-in-termset-p *grammar* (integers-from-to 0 127)))

Theorem: plugging-yields-*grammar*

(defthm plugging-yields-*grammar*
  (set-equiv (plug-rules *concrete-syntax-rules* *core-rules*)
             *grammar*))