		Search-engine friendly clone of the ACL2 documentation.

Rule-utilities

Rule-simple-subs

See if a rule could be used to define a type/subtype relationship.

Signature
(rule-simple-subs rule-name grammar) → sub-rule-names
Arguments: rule-name — Guard (common-lisp::stringp rule-name).; grammar — Guard (rulelistp grammar).
Returns: sub-rule-names — Type (acl2::string-list-resultp sub-rule-names).

This uses a very restrictive definition of whether the rule names in a rule are being used like a type/subtype relationship:

There must be only one rule with the given name in grammar.
It is not an incremental rule.
The rule must consist solely of an alternation of unadorned rule names. By unadorned we mean the concatenation and repetition are singular in the abstract syntax.

For example:

integer-type = unsigned-type / signed-type

If all of the requirements are satisified, the return value is a list of the "sub" rulenames. Otherwise a reserrp is returned.

Definitions and Theorems

Function: rule-simple-subs

(defun rule-simple-subs (rule-name grammar)
 (declare (xargs :guard (and (common-lisp::stringp rule-name)
                             (rulelistp grammar))))
 (let ((__function__ 'rule-simple-subs))
   (declare (ignorable __function__))
   (b* (((mv rules ?not-rules)
         (rules-of-name (rulename (str-fix rule-name))
                        grammar))
        ((unless (equal (len rules) 1))
         (reserrf (cons :not-exactly-one-rule-with-name rule-name)))
        (the-rule (car rules))
        ((when (rule->incremental the-rule))
         (reserrf (cons :the-rule-is-incremental the-rule)))
        (alt (rule->definiens the-rule))
        ((unless (alternationp alt))
         (reserrf (cons :impossible alt))))
     (rulenames-from-singular-conc-and-rep
          (rule->definiens the-rule)))))

Theorem: string-list-resultp-of-rule-simple-subs

(defthm string-list-resultp-of-rule-simple-subs
  (b* ((sub-rule-names (rule-simple-subs rule-name grammar)))
    (acl2::string-list-resultp sub-rule-names))
  :rule-classes :rewrite)