		Search-engine friendly clone of the ACL2 documentation.

Mapping-to-language-definition

Ldm-exprs

Map expressions to expressions in the language definition.

Definitions and Theorems

Function: ldm-expr

(defun ldm-expr (expr)
 (declare (xargs :guard (exprp expr)))
 (declare (xargs :guard (expr-unambp expr)))
 (let ((__function__ 'ldm-expr))
  (declare (ignorable __function__))
  (b* (((reterr)
        (c::expr-ident (c::ident "irrelevant"))))
   (expr-case
    expr :ident
    (b* (((erp ident1) (ldm-ident expr.ident)))
      (retok (c::expr-ident ident1)))
    :const
    (b* (((erp const1) (ldm-const expr.const)))
      (retok (c::expr-const const1)))
    :string
    (reterr (msg "Unsupported expression ~x0."
                 (expr-fix expr)))
    :paren (ldm-expr expr.inner)
    :gensel
    (reterr (msg "Unsupported expression ~x0."
                 (expr-fix expr)))
    :arrsub
    (b* (((erp arr1) (ldm-expr expr.arg1))
         ((erp sub1) (ldm-expr expr.arg2)))
      (retok (c::make-expr-arrsub :arr arr1
                                  :sub sub1)))
    :funcall
    (b* ((ident (check-expr-ident expr.fun))
         ((when (not ident))
          (reterr (msg "Unsupported non-identifier function ~x0."
                       expr.fun)))
         ((erp ident1) (ldm-ident ident))
         ((erp args1) (ldm-expr-list expr.args)))
      (retok (c::make-expr-call :fun ident1
                                :args args1)))
    :member
    (b* (((erp target1) (ldm-expr expr.arg))
         ((erp ident1) (ldm-ident expr.name)))
      (retok (c::make-expr-member :target target1
                                  :name ident1)))
    :memberp
    (b* (((erp target1) (ldm-expr expr.arg))
         ((erp ident1) (ldm-ident expr.name)))
      (retok (c::make-expr-memberp :target target1
                                   :name ident1)))
    :complit
    (reterr (msg "Unsupported expression ~x0."
                 (expr-fix expr)))
    :unary
    (b* (((erp arg) (ldm-expr expr.arg)))
      (unop-case
           expr.op
           :address (retok (c::make-expr-unary :op (c::unop-address)
                                               :arg arg))
           :indir (retok (c::make-expr-unary :op (c::unop-indir)
                                             :arg arg))
           :plus (retok (c::make-expr-unary :op (c::unop-plus)
                                            :arg arg))
           :minus (retok (c::make-expr-unary :op (c::unop-minus)
                                             :arg arg))
           :bitnot (retok (c::make-expr-unary :op (c::unop-bitnot)
                                              :arg arg))
           :lognot (retok (c::make-expr-unary :op (c::unop-lognot)
                                              :arg arg))
           :preinc (retok (c::expr-preinc arg))
           :predec (retok (c::expr-predec arg))
           :postinc (retok (c::expr-postinc arg))
           :postdec (retok (c::expr-postdec arg))
           :sizeof (reterr (msg "Unsupported sizeof operator."))))
    :sizeof
    (reterr (msg "Unsupported expression ~x0."
                 (expr-fix expr)))
    :sizeof-ambig
    (prog2$ (impossible) (reterr t))
    :alignof
    (reterr (msg "Unsupported expression ~x0."
                 (expr-fix expr)))
    :cast
    (b* (((erp tyname) (ldm-tyname expr.type))
         ((erp arg) (ldm-expr expr.arg)))
      (retok (c::make-expr-cast :type tyname
                                :arg arg)))
    :binary
    (b* (((erp arg1) (ldm-expr expr.arg1))
         ((erp arg2) (ldm-expr expr.arg2))
         (op (ldm-binop expr.op)))
      (retok (c::make-expr-binary :op op
                                  :arg1 arg1
                                  :arg2 arg2)))
    :cond
    (b*
     (((erp test) (ldm-expr expr.test))
      ((when (expr-option-case expr.then :none))
       (reterr
        (msg
         "Unsupported conditional expression ~
                                 with omitted operand ~x0."
         (expr-fix expr))))
      (expr.then (expr-option-some->val expr.then))
      ((erp then) (ldm-expr expr.then))
      ((erp else) (ldm-expr expr.else)))
     (retok (c::make-expr-cond :test test
                               :then then
                               :else else)))
    :comma (reterr (msg "Unsupported expression ~x0."
                        (expr-fix expr)))
    :cast/call-ambig (prog2$ (impossible) (reterr t))
    :cast/mul-ambig (prog2$ (impossible) (reterr t))
    :cast/add-ambig (prog2$ (impossible) (reterr t))
    :cast/sub-ambig (prog2$ (impossible) (reterr t))
    :cast/and-ambig (prog2$ (impossible) (reterr t))
    :stmt (reterr (msg "Unsupported expression ~x0."
                       (expr-fix expr)))
    :tycompat (reterr (msg "Unsupported expression ~x0."
                           (expr-fix expr)))
    :offsetof (reterr (msg "Unsupported expression ~x0."
                           (expr-fix expr)))
    :va-arg (reterr (msg "Unsupported expression ~x0."
                         (expr-fix expr)))
    :extension (reterr (msg "Unsupported expression ~x0."
                            (expr-fix expr)))))))

Function: ldm-expr-list

(defun ldm-expr-list (exprs)
  (declare (xargs :guard (expr-listp exprs)))
  (declare (xargs :guard (expr-list-unambp exprs)))
  (let ((__function__ 'ldm-expr-list))
    (declare (ignorable __function__))
    (b* (((reterr) nil)
         ((when (endp exprs)) (retok nil))
         ((erp expr1) (ldm-expr (car exprs)))
         ((erp exprs1)
          (ldm-expr-list (cdr exprs))))
      (retok (cons expr1 exprs1)))))

Theorem: return-type-of-ldm-expr.expr1

(defthm return-type-of-ldm-expr.expr1
  (b* (((mv acl2::?erp ?expr1)
        (ldm-expr expr)))
    (c::exprp expr1))
  :rule-classes :rewrite)

Theorem: return-type-of-ldm-expr-list.exprs1

(defthm return-type-of-ldm-expr-list.exprs1
  (b* (((mv acl2::?erp ?exprs1)
        (ldm-expr-list exprs)))
    (c::expr-listp exprs1))
  :rule-classes :rewrite)

Theorem: ldm-expr-of-expr-fix-expr

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

Theorem: ldm-expr-list-of-expr-list-fix-exprs

(defthm ldm-expr-list-of-expr-list-fix-exprs
  (equal (ldm-expr-list (expr-list-fix exprs))
         (ldm-expr-list exprs)))

Theorem: ldm-expr-expr-equiv-congruence-on-expr

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

Theorem: ldm-expr-list-expr-list-equiv-congruence-on-exprs

(defthm ldm-expr-list-expr-list-equiv-congruence-on-exprs
  (implies (expr-list-equiv exprs exprs-equiv)
           (equal (ldm-expr-list exprs)
                  (ldm-expr-list exprs-equiv)))
  :rule-classes :congruence)

Theorem: ldm-expr-ok-when-expr-pure-formalp

(defthm ldm-expr-ok-when-expr-pure-formalp
  (implies (expr-pure-formalp expr)
           (b* (((mv acl2::?erp ?expr1)
                 (ldm-expr expr)))
             (not erp))))

Theorem: ldm-expr-list-ok-when-expr-list-pure-formalp

(defthm ldm-expr-list-ok-when-expr-list-pure-formalp
  (implies (expr-list-pure-formalp exprs)
           (b* (((mv acl2::?erp ?exprs1)
                 (ldm-expr-list exprs)))
             (not erp))))

Theorem: ldm-expr-ok-when-expr-call-formalp

(defthm ldm-expr-ok-when-expr-call-formalp
  (implies (expr-call-formalp expr)
           (b* (((mv acl2::?erp ?expr1)
                 (ldm-expr expr)))
             (not erp))))

Theorem: ldm-expr-ok-when-expr-asg-formalp

(defthm ldm-expr-ok-when-expr-asg-formalp
  (implies (expr-asg-formalp expr)
           (b* (((mv acl2::?erp ?expr1)
                 (ldm-expr expr)))
             (not erp))))

Subtopics

Ldm-expr: Map an expression to an expression in the language definition.
Ldm-expr-list: Map a list of expressions to a list of expressions in the language definition.