		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Check-sum-construct-expression

Check if a sum construction expression is statically well-formed.

Signature
(check-sum-construct-expression type alternative inits inits-result expr ctxt) → result
Arguments: type — Guard (identifierp type).; alternative — Guard (identifierp alternative).; inits — Guard (initializer-listp inits).; inits-result — Guard (type-resultp inits-result).; expr — Guard (expressionp expr).; ctxt — Guard (contextp ctxt).
Returns: result — Type (type-resultp result).

The first identifier must be the name of a sum type in the context. The second identifier must be the name of one of the alternatives. We retrieve the associated product type and we proceed similarly to check-product-construct-expression.

Definitions and Theorems

Function: check-sum-construct-expression

(defun check-sum-construct-expression
       (type alternative
             inits inits-result expr ctxt)
 (declare (xargs :guard (and (identifierp type)
                             (identifierp alternative)
                             (initializer-listp inits)
                             (type-resultp inits-result)
                             (expressionp expr)
                             (contextp ctxt))))
 (declare
     (xargs :guard (type-result-case inits-result
                                     :err t
                                     :ok (= (len inits-result.types)
                                            (len inits)))))
 (let ((__function__ 'check-sum-construct-expression))
  (declare (ignorable __function__))
  (type-result-case
   inits-result
   :err (type-result-err inits-result.info)
   :ok
   (b*
    ((sum (get-type-sum (type-defined type)
                        (context->tops ctxt)))
     ((when (not sum))
      (type-result-err
         (list :sum-construct-type-mismatch (identifier-fix type))))
     (product
          (get-alternative-product alternative
                                   (type-sum->alternatives sum)))
     ((when (not product))
      (type-result-err (list :sum-construct-no-alternative
                             (identifier-fix type)
                             (identifier-fix alternative))))
     (fields (type-product->fields product))
     ((mv okp obligs unmatched-fields)
      (match-field-list inits inits-result.types fields ctxt))
     ((when (not okp))
      (type-result-err (list :field-type-mismatch
                             (identifier-fix type)
                             (initializer-list-fix inits)
                             fields)))
     ((when (consp unmatched-fields))
      (type-result-err (list :unmatched-fields (identifier-fix type)
                             (initializer-list-fix inits)
                             fields)))
     (inv (type-product->invariant product))
     (inv-oblig?
       (if inv
         (b* ((subst (initializers-to-variable-substitution inits)))
           (non-trivial-proof-obligation
                (context->obligation-vars ctxt)
                (context->obligation-hyps ctxt)
                (subst-expression subst inv)
                expr))
         nil)))
    (make-type-result-ok
         :types (list (type-defined type))
         :obligations (append inits-result.obligations
                              obligs inv-oblig?))))))

Theorem: type-resultp-of-check-sum-construct-expression

(defthm type-resultp-of-check-sum-construct-expression
 (b*
  ((result
     (check-sum-construct-expression type alternative
                                     inits inits-result expr ctxt)))
  (type-resultp result))
 :rule-classes :rewrite)

Theorem: check-sum-construct-expression-of-identifier-fix-type

(defthm check-sum-construct-expression-of-identifier-fix-type
 (equal
     (check-sum-construct-expression (identifier-fix type)
                                     alternative
                                     inits inits-result expr ctxt)
     (check-sum-construct-expression type alternative
                                     inits inits-result expr ctxt)))

Theorem: check-sum-construct-expression-identifier-equiv-congruence-on-type

(defthm
 check-sum-construct-expression-identifier-equiv-congruence-on-type
 (implies
  (identifier-equiv type type-equiv)
  (equal
     (check-sum-construct-expression type alternative
                                     inits inits-result expr ctxt)
     (check-sum-construct-expression type-equiv alternative
                                     inits inits-result expr ctxt)))
 :rule-classes :congruence)

Theorem: check-sum-construct-expression-of-identifier-fix-alternative

(defthm check-sum-construct-expression-of-identifier-fix-alternative
 (equal
   (check-sum-construct-expression type (identifier-fix alternative)
                                   inits inits-result expr ctxt)
   (check-sum-construct-expression type alternative
                                   inits inits-result expr ctxt)))

Theorem: check-sum-construct-expression-identifier-equiv-congruence-on-alternative

(defthm
 check-sum-construct-expression-identifier-equiv-congruence-on-alternative
 (implies
  (identifier-equiv alternative alternative-equiv)
  (equal
     (check-sum-construct-expression type alternative
                                     inits inits-result expr ctxt)
     (check-sum-construct-expression type alternative-equiv
                                     inits inits-result expr ctxt)))
 :rule-classes :congruence)

Theorem: check-sum-construct-expression-of-initializer-list-fix-inits

(defthm check-sum-construct-expression-of-initializer-list-fix-inits
 (equal
     (check-sum-construct-expression
          type
          alternative (initializer-list-fix inits)
          inits-result expr ctxt)
     (check-sum-construct-expression type alternative
                                     inits inits-result expr ctxt)))

Theorem: check-sum-construct-expression-initializer-list-equiv-congruence-on-inits

(defthm
 check-sum-construct-expression-initializer-list-equiv-congruence-on-inits
 (implies
  (initializer-list-equiv inits inits-equiv)
  (equal
       (check-sum-construct-expression type alternative
                                       inits inits-result expr ctxt)
       (check-sum-construct-expression
            type alternative
            inits-equiv inits-result expr ctxt)))
 :rule-classes :congruence)

Theorem: check-sum-construct-expression-of-type-result-fix-inits-result

(defthm
     check-sum-construct-expression-of-type-result-fix-inits-result
 (equal
     (check-sum-construct-expression
          type alternative
          inits (type-result-fix inits-result)
          expr ctxt)
     (check-sum-construct-expression type alternative
                                     inits inits-result expr ctxt)))

Theorem: check-sum-construct-expression-type-result-equiv-congruence-on-inits-result

(defthm
 check-sum-construct-expression-type-result-equiv-congruence-on-inits-result
 (implies
  (type-result-equiv inits-result inits-result-equiv)
  (equal
       (check-sum-construct-expression type alternative
                                       inits inits-result expr ctxt)
       (check-sum-construct-expression
            type alternative
            inits inits-result-equiv expr ctxt)))
 :rule-classes :congruence)

Theorem: check-sum-construct-expression-of-expression-fix-expr

(defthm check-sum-construct-expression-of-expression-fix-expr
 (equal
     (check-sum-construct-expression
          type alternative
          inits inits-result (expression-fix expr)
          ctxt)
     (check-sum-construct-expression type alternative
                                     inits inits-result expr ctxt)))

Theorem: check-sum-construct-expression-expression-equiv-congruence-on-expr

(defthm
 check-sum-construct-expression-expression-equiv-congruence-on-expr
 (implies
  (expression-equiv expr expr-equiv)
  (equal
       (check-sum-construct-expression type alternative
                                       inits inits-result expr ctxt)
       (check-sum-construct-expression
            type alternative
            inits inits-result expr-equiv ctxt)))
 :rule-classes :congruence)

Theorem: check-sum-construct-expression-of-context-fix-ctxt

(defthm check-sum-construct-expression-of-context-fix-ctxt
 (equal
     (check-sum-construct-expression
          type alternative inits
          inits-result expr (context-fix ctxt))
     (check-sum-construct-expression type alternative
                                     inits inits-result expr ctxt)))

Theorem: check-sum-construct-expression-context-equiv-congruence-on-ctxt

(defthm
    check-sum-construct-expression-context-equiv-congruence-on-ctxt
 (implies
  (context-equiv ctxt ctxt-equiv)
  (equal
       (check-sum-construct-expression type alternative
                                       inits inits-result expr ctxt)
       (check-sum-construct-expression
            type alternative
            inits inits-result expr ctxt-equiv)))
 :rule-classes :congruence)