		Search-engine friendly clone of the ACL2 documentation.

Mapping-to-language-definition

Ldm-stmts

Map statements and related entities to statements and related entities in the language definition.

Definitions and Theorems

Function: ldm-stmt

(defun ldm-stmt (stmt)
 (declare (xargs :guard (stmtp stmt)))
 (declare (xargs :guard (stmt-unambp stmt)))
 (let ((__function__ 'ldm-stmt))
  (declare (ignorable __function__))
  (b* (((reterr) (c::stmt-null)))
   (stmt-case
    stmt :labeled
    (b* (((erp label1) (ldm-label stmt.label))
         ((erp stmt1) (ldm-stmt stmt.stmt)))
      (retok (c::make-stmt-labeled :label label1
                                   :body stmt1)))
    :compound
    (b* (((erp items) (ldm-comp-stmt stmt.stmt)))
      (retok (c::make-stmt-compound :items items)))
    :expr
    (expr-option-case stmt.expr? :some
                      (b* (((erp expr1) (ldm-expr stmt.expr?.val)))
                        (retok (c::stmt-expr expr1)))
                      :none (retok (c::make-stmt-null)))
    :if
    (b* (((erp test1) (ldm-expr stmt.test))
         ((erp then1) (ldm-stmt stmt.then)))
      (retok (c::make-stmt-if :test test1
                              :then then1)))
    :ifelse
    (b* (((erp test1) (ldm-expr stmt.test))
         ((erp then1) (ldm-stmt stmt.then))
         ((erp else1) (ldm-stmt stmt.else)))
      (retok (c::make-stmt-ifelse :test test1
                                  :then then1
                                  :else else1)))
    :switch
    (b* (((erp ctrl1) (ldm-expr stmt.target))
         ((erp body1) (ldm-stmt stmt.body)))
      (retok (c::make-stmt-switch :ctrl ctrl1
                                  :body body1)))
    :while
    (b* (((erp test1) (ldm-expr stmt.test))
         ((erp body1) (ldm-stmt stmt.body)))
      (retok (c::make-stmt-while :test test1
                                 :body body1)))
    :dowhile
    (b* (((erp body1) (ldm-stmt stmt.body))
         ((erp test1) (ldm-expr stmt.test)))
      (retok (c::make-stmt-dowhile :body body1
                                   :test test1)))
    :for-expr
    (b* (((erp init1)
          (ldm-expr-option stmt.init))
         ((erp test1)
          (ldm-expr-option stmt.test))
         ((erp next1)
          (ldm-expr-option stmt.next))
         ((erp body1) (ldm-stmt stmt.body)))
      (retok (c::make-stmt-for :init init1
                               :test test1
                               :next next1
                               :body body1)))
    :for-decl
    (reterr
     (msg
      "Unsupported 'for' loop ~x0 ~
                               with initializing declaration."
      (stmt-fix stmt)))
    :for-ambig
    (prog2$ (impossible) (reterr t))
    :goto
    (b* (((erp ident1) (ldm-ident stmt.label)))
      (retok (c::make-stmt-goto :target ident1)))
    :gotoe
    (reterr (msg "Unsupported 'goto' with expression ~x0."
                 (stmt-fix stmt)))
    :continue (retok (c::stmt-continue))
    :break (retok (c::stmt-break))
    :return
    (b* (((erp expr?)
          (ldm-expr-option stmt.expr?)))
      (retok (c::make-stmt-return :value expr?)))
    :asm (reterr (msg "Unsupported assembler statement ~x0."
                      (stmt-fix stmt)))))))

Function: ldm-comp-stmt

(defun ldm-comp-stmt (cstmt)
  (declare (xargs :guard (comp-stmtp cstmt)))
  (declare (xargs :guard (comp-stmt-unambp cstmt)))
  (let ((__function__ 'ldm-comp-stmt))
    (declare (ignorable __function__))
    (b* (((reterr) nil)
         ((comp-stmt cstmt) cstmt)
         ((when cstmt.labels)
          (reterr (msg "Unsupported label declarations ~x0."
                       cstmt.labels))))
      (ldm-block-item-list cstmt.items))))

Function: ldm-block-item

(defun ldm-block-item (item)
  (declare (xargs :guard (block-itemp item)))
  (declare (xargs :guard (block-item-unambp item)))
  (let ((__function__ 'ldm-block-item))
    (declare (ignorable __function__))
    (b* (((reterr)
          (c::block-item-stmt (c::stmt-null))))
      (block-item-case item :decl
                       (b* (((erp objdeclon)
                             (ldm-decl-obj item.decl)))
                         (retok (c::block-item-declon objdeclon)))
                       :stmt
                       (b* (((erp stmt) (ldm-stmt item.stmt)))
                         (retok (c::block-item-stmt stmt)))
                       :ambig (prog2$ (impossible) (reterr t))))))

Function: ldm-block-item-list

(defun ldm-block-item-list (items)
  (declare (xargs :guard (block-item-listp items)))
  (declare (xargs :guard (block-item-list-unambp items)))
  (let ((__function__ 'ldm-block-item-list))
    (declare (ignorable __function__))
    (b* (((reterr) nil)
         ((when (endp items)) (retok nil))
         ((erp item1)
          (ldm-block-item (car items)))
         ((erp items1)
          (ldm-block-item-list (cdr items))))
      (retok (cons item1 items1)))))

Theorem: return-type-of-ldm-stmt.stmt1

(defthm return-type-of-ldm-stmt.stmt1
  (b* (((mv acl2::?erp ?stmt1)
        (ldm-stmt stmt)))
    (c::stmtp stmt1))
  :rule-classes :rewrite)

Theorem: return-type-of-ldm-comp-stmt.items

(defthm return-type-of-ldm-comp-stmt.items
  (b* (((mv acl2::?erp ?items)
        (ldm-comp-stmt cstmt)))
    (c::block-item-listp items))
  :rule-classes :rewrite)

Theorem: return-type-of-ldm-block-item.item1

(defthm return-type-of-ldm-block-item.item1
  (b* (((mv acl2::?erp ?item1)
        (ldm-block-item item)))
    (c::block-itemp item1))
  :rule-classes :rewrite)

Theorem: return-type-of-ldm-block-item-list.items1

(defthm return-type-of-ldm-block-item-list.items1
  (b* (((mv acl2::?erp ?items1)
        (ldm-block-item-list items)))
    (c::block-item-listp items1))
  :rule-classes :rewrite)

Theorem: ldm-stmt-of-stmt-fix-stmt

(defthm ldm-stmt-of-stmt-fix-stmt
  (equal (ldm-stmt (stmt-fix stmt))
         (ldm-stmt stmt)))

Theorem: ldm-comp-stmt-of-comp-stmt-fix-cstmt

(defthm ldm-comp-stmt-of-comp-stmt-fix-cstmt
  (equal (ldm-comp-stmt (comp-stmt-fix cstmt))
         (ldm-comp-stmt cstmt)))

Theorem: ldm-block-item-of-block-item-fix-item

(defthm ldm-block-item-of-block-item-fix-item
  (equal (ldm-block-item (block-item-fix item))
         (ldm-block-item item)))

Theorem: ldm-block-item-list-of-block-item-list-fix-items

(defthm ldm-block-item-list-of-block-item-list-fix-items
  (equal (ldm-block-item-list (block-item-list-fix items))
         (ldm-block-item-list items)))

Theorem: ldm-stmt-stmt-equiv-congruence-on-stmt

(defthm ldm-stmt-stmt-equiv-congruence-on-stmt
  (implies (stmt-equiv stmt stmt-equiv)
           (equal (ldm-stmt stmt)
                  (ldm-stmt stmt-equiv)))
  :rule-classes :congruence)

Theorem: ldm-comp-stmt-comp-stmt-equiv-congruence-on-cstmt

(defthm ldm-comp-stmt-comp-stmt-equiv-congruence-on-cstmt
  (implies (comp-stmt-equiv cstmt cstmt-equiv)
           (equal (ldm-comp-stmt cstmt)
                  (ldm-comp-stmt cstmt-equiv)))
  :rule-classes :congruence)

Theorem: ldm-block-item-block-item-equiv-congruence-on-item

(defthm ldm-block-item-block-item-equiv-congruence-on-item
  (implies (block-item-equiv item item-equiv)
           (equal (ldm-block-item item)
                  (ldm-block-item item-equiv)))
  :rule-classes :congruence)

Theorem: ldm-block-item-list-block-item-list-equiv-congruence-on-items

(defthm
      ldm-block-item-list-block-item-list-equiv-congruence-on-items
  (implies (block-item-list-equiv items items-equiv)
           (equal (ldm-block-item-list items)
                  (ldm-block-item-list items-equiv)))
  :rule-classes :congruence)

Theorem: ldm-stmt-ok-when-stmt-formalp

(defthm ldm-stmt-ok-when-stmt-formalp
  (implies (stmt-formalp stmt)
           (b* (((mv acl2::?erp ?stmt1)
                 (ldm-stmt stmt)))
             (not erp))))

Theorem: ldm-comp-stmt-ok-when-comp-stmt-formalp

(defthm ldm-comp-stmt-ok-when-comp-stmt-formalp
  (implies (comp-stmt-formalp cstmt)
           (b* (((mv acl2::?erp ?items)
                 (ldm-comp-stmt cstmt)))
             (not erp))))

Theorem: ldm-block-item-ok-when-block-item-formalp

(defthm ldm-block-item-ok-when-block-item-formalp
  (implies (block-item-formalp item)
           (b* (((mv acl2::?erp ?item1)
                 (ldm-block-item item)))
             (not erp))))

Theorem: ldm-block-item-list-ok-when-block-item-list-formalp

(defthm ldm-block-item-list-ok-when-block-item-list-formalp
  (implies (block-item-list-formalp items)
           (b* (((mv acl2::?erp ?items1)
                 (ldm-block-item-list items)))
             (not erp))))

Subtopics

Ldm-comp-stmt: Map a compound statement to a list of block items in the language definition.
Ldm-block-item-list: Map a list of block items to a list of block items in the language definition.
Ldm-stmt: Map a statement to a statement in the language definition.
Ldm-block-item: Map a block item to a block item in the language definition.