|
|
|---|
|
|
|
|---|
Transform a unary expression.
(simpadd0-expr-unary op arg arg-new arg-events arg-thm-name
arg-vartys arg-diffp info gin)
→
(mv expr gout)The resulting expression is obtained by combining the unary operator with the possibly transformed argument expression.
We generate a theorem iff
a theorem was generated for the argument expression,
and the unary operator is among
Function:
(defun simpadd0-expr-unary (op arg arg-new arg-events arg-thm-name arg-vartys arg-diffp info gin) (declare (xargs :guard (and (unopp op) (exprp arg) (exprp arg-new) (pseudo-event-form-listp arg-events) (symbolp arg-thm-name) (ident-type-mapp arg-vartys) (booleanp arg-diffp) (unary-infop info) (simpadd0-ginp gin)))) (declare (xargs :guard (and (expr-unambp arg) (expr-unambp arg-new)))) (let ((__function__ 'simpadd0-expr-unary)) (declare (ignorable __function__)) (b* (((simpadd0-gin gin) gin) (expr (make-expr-unary :op op :arg arg :info info)) (expr-new (make-expr-unary :op op :arg arg-new :info info)) ((unless (and arg-thm-name (type-case (expr-type arg) :sint) (member-eq (unop-kind op) '(:plus :minus :bitnot :lognot)))) (mv expr-new (make-simpadd0-gout :events arg-events :thm-name nil :thm-index gin.thm-index :names-to-avoid gin.names-to-avoid :vartys arg-vartys :diffp arg-diffp))) (hints (cons (cons '"Goal" (cons ':in-theory (cons ''((:e ldm-expr) (:e c::unop-nonpointerp) (:e c::expr-unary) (:e c::type-sint)) (cons ':use (cons (cons arg-thm-name (cons (cons ':instance (cons 'simpadd0-expr-unary-support-lemma-1 (cons (cons 'op (cons (cons 'quote (cons (unop-case op :plus (c::unop-plus) :minus (c::unop-minus) :bitnot (c::unop-bitnot) :lognot (c::unop-lognot) :otherwise (impossible)) 'nil)) 'nil)) (cons (cons 'old-arg (cons (cons 'mv-nth (cons '1 (cons (cons 'ldm-expr (cons (cons 'quote (cons arg 'nil)) 'nil)) 'nil))) 'nil)) (cons (cons 'new-arg (cons (cons 'mv-nth (cons '1 (cons (cons 'ldm-expr (cons (cons 'quote (cons arg-new 'nil)) 'nil)) 'nil))) 'nil)) 'nil))))) (cons (cons ':instance (cons 'simpadd0-expr-unary-support-lemma-2 (cons (cons 'op (cons (cons 'quote (cons (unop-case op :plus (c::unop-plus) :minus (c::unop-minus) :bitnot (c::unop-bitnot) :lognot (c::unop-lognot) :otherwise (impossible)) 'nil)) 'nil)) (cons (cons 'arg (cons (cons 'mv-nth (cons '1 (cons (cons 'ldm-expr (cons (cons 'quote (cons arg 'nil)) 'nil)) 'nil))) 'nil)) 'nil)))) 'nil))) 'nil))))) 'nil)) ((mv thm-event thm-name thm-index) (simpadd0-gen-expr-pure-thm expr expr-new arg-vartys gin.const-new gin.thm-index hints))) (mv expr-new (make-simpadd0-gout :events (append arg-events (list thm-event)) :thm-name thm-name :thm-index thm-index :names-to-avoid (cons thm-name gin.names-to-avoid) :vartys arg-vartys :diffp arg-diffp)))))
Theorem:
(defthm exprp-of-simpadd0-expr-unary.expr (b* (((mv ?expr ?gout) (simpadd0-expr-unary op arg arg-new arg-events arg-thm-name arg-vartys arg-diffp info gin))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm simpadd0-goutp-of-simpadd0-expr-unary.gout (b* (((mv ?expr ?gout) (simpadd0-expr-unary op arg arg-new arg-events arg-thm-name arg-vartys arg-diffp info gin))) (simpadd0-goutp gout)) :rule-classes :rewrite)
Theorem:
(defthm expr-unambp-of-simpadd0-expr-unary (implies (expr-unambp arg-new) (b* (((mv ?expr ?gout) (simpadd0-expr-unary op arg arg-new arg-events arg-thm-name arg-vartys arg-diffp info gin))) (expr-unambp expr))))
Theorem:
(defthm simpadd0-expr-unary-support-lemma-1 (b* ((old (c::expr-unary op old-arg)) (new (c::expr-unary op new-arg)) (old-arg-result (c::exec-expr-pure old-arg compst)) (new-arg-result (c::exec-expr-pure new-arg compst)) (old-arg-value (c::expr-value->value old-arg-result)) (new-arg-value (c::expr-value->value new-arg-result)) (old-result (c::exec-expr-pure old compst)) (new-result (c::exec-expr-pure new compst)) (old-value (c::expr-value->value old-result)) (new-value (c::expr-value->value new-result))) (implies (and (c::unop-nonpointerp op) (not (c::errorp old-result)) (not (c::errorp new-arg-result)) (equal old-arg-value new-arg-value) (equal (c::type-of-value old-arg-value) (c::type-sint)) (equal (c::value-kind old-arg-value) :sint)) (and (not (c::errorp new-result)) (equal old-value new-value) (equal (c::type-of-value old-value) (c::type-sint)) (equal (c::value-kind old-value) :sint)))))
Theorem:
(defthm simpadd0-expr-unary-support-lemma-2 (implies (c::errorp (c::exec-expr-pure arg compst)) (c::errorp (c::exec-expr-pure (c::expr-unary op arg) compst))))