|
|
|---|
|
|
|
|---|
Transform a binary expression.
(simpadd0-expr-binary op arg1 arg1-new arg1-events
arg1-thm-name arg1-vartys arg1-diffp
arg2 arg2-new arg2-events arg2-thm-name
arg2-vartys arg2-diffp info gin)
→
(mv expr gout)The resulting expression is obtained by
combining the binary operator with
the possibly transformed argument expressions,
unless the binary operator is
We generate a theorem iff theorems were generated for both argument expressions, and the binary operator is pure and non-strict. The theorem is proved via three general ones that we prove below; the third one is only needed if there is an actual simplification, but we always use it in the proof for simplicity.
Function:
(defun simpadd0-expr-binary (op arg1 arg1-new arg1-events arg1-thm-name arg1-vartys arg1-diffp arg2 arg2-new arg2-events arg2-thm-name arg2-vartys arg2-diffp info gin) (declare (xargs :guard (and (binopp op) (exprp arg1) (exprp arg1-new) (pseudo-event-form-listp arg1-events) (symbolp arg1-thm-name) (ident-type-mapp arg1-vartys) (booleanp arg1-diffp) (exprp arg2) (exprp arg2-new) (pseudo-event-form-listp arg2-events) (symbolp arg2-thm-name) (ident-type-mapp arg2-vartys) (booleanp arg2-diffp) (binary-infop info) (simpadd0-ginp gin)))) (declare (xargs :guard (and (expr-unambp arg1) (expr-unambp arg1-new) (expr-unambp arg2) (expr-unambp arg2-new)))) (let ((__function__ 'simpadd0-expr-binary)) (declare (ignorable __function__)) (b* (((simpadd0-gin gin) gin) (expr (make-expr-binary :op op :arg1 arg1 :arg2 arg2 :info info)) (simpp (and (binop-case op :add) (type-case (expr-type arg1-new) :sint) (expr-zerop arg2-new))) (expr-new (if simpp (expr-fix arg1-new) (make-expr-binary :op op :arg1 arg1-new :arg2 arg2-new :info info))) (arg1-vartys (ident-type-map-fix arg1-vartys)) (arg2-vartys (ident-type-map-fix arg2-vartys)) ((unless (omap::compatiblep arg1-vartys arg2-vartys)) (raise "Internal error: ~ incompatible variable-type maps ~x0 and ~x1." arg1-vartys arg2-vartys) (mv (irr-expr) (irr-simpadd0-gout))) (vartys (omap::update* arg1-vartys arg2-vartys)) (diffp (or arg1-diffp arg2-diffp simpp)) ((unless (and arg1-thm-name arg2-thm-name (type-case (expr-type arg1) :sint) (type-case (expr-type arg2) :sint) (member-eq (binop-kind op) '(:mul :div :rem :add :sub :shl :shr :lt :gt :le :ge :eq :ne :bitand :bitxor :bitior)))) (mv expr-new (make-simpadd0-gout :events (append arg1-events arg2-events) :thm-name nil :thm-index gin.thm-index :names-to-avoid gin.names-to-avoid :vartys vartys :diffp diffp))) (hints (cons (cons '"Goal" (cons ':in-theory (cons ''((:e ldm-expr) (:e c::iconst-length-none) (:e c::iconst-base-oct) (:e c::iconst) (:e c::const-int) (:e c::expr-const) (:e c::binop-add) (:e c::binop-purep) (:e c::binop-strictp) (:e c::expr-binary) (:e c::type-sint)) (cons ':use (cons (cons arg1-thm-name (cons arg2-thm-name (cons (cons ':instance (cons 'simpadd0-expr-binary-support-lemma-1 (cons (cons 'op (cons (cons 'quote (cons (ldm-binop op) 'nil)) 'nil)) (cons (cons 'old-arg1 (cons (cons 'mv-nth (cons '1 (cons (cons 'ldm-expr (cons (cons 'quote (cons arg1 'nil)) 'nil)) 'nil))) 'nil)) (cons (cons 'old-arg2 (cons (cons 'mv-nth (cons '1 (cons (cons 'ldm-expr (cons (cons 'quote (cons arg2 'nil)) 'nil)) 'nil))) 'nil)) (cons (cons 'new-arg1 (cons (cons 'mv-nth (cons '1 (cons (cons 'ldm-expr (cons (cons 'quote (cons arg1-new 'nil)) 'nil)) 'nil))) 'nil)) (cons (cons 'new-arg2 (cons (cons 'mv-nth (cons '1 (cons (cons 'ldm-expr (cons (cons 'quote (cons arg2-new 'nil)) 'nil)) 'nil))) 'nil)) 'nil))))))) (cons (cons ':instance (cons 'simpadd0-expr-binary-support-lemma-2 (cons (cons 'op (cons (cons 'quote (cons (ldm-binop op) 'nil)) 'nil)) (cons (cons 'arg1 (cons (cons 'mv-nth (cons '1 (cons (cons 'ldm-expr (cons (cons 'quote (cons arg1 'nil)) 'nil)) 'nil))) 'nil)) (cons (cons 'arg2 (cons (cons 'mv-nth (cons '1 (cons (cons 'ldm-expr (cons (cons 'quote (cons arg2 'nil)) 'nil)) 'nil))) 'nil)) 'nil))))) (cons (cons ':instance (cons 'simpadd0-expr-binary-support-lemma-3 (cons (cons 'expr (cons (cons 'mv-nth (cons '1 (cons (cons 'ldm-expr (cons (cons 'quote (cons arg1-new 'nil)) 'nil)) 'nil))) 'nil)) 'nil))) 'nil))))) 'nil))))) 'nil)) ((mv thm-event thm-name thm-index) (simpadd0-gen-expr-pure-thm expr expr-new vartys gin.const-new gin.thm-index hints))) (mv expr-new (make-simpadd0-gout :events (append arg1-events arg2-events (list thm-event)) :thm-name thm-name :thm-index thm-index :names-to-avoid (cons thm-name gin.names-to-avoid) :vartys vartys :diffp diffp)))))
Theorem:
(defthm exprp-of-simpadd0-expr-binary.expr (b* (((mv ?expr ?gout) (simpadd0-expr-binary op arg1 arg1-new arg1-events arg1-thm-name arg1-vartys arg1-diffp arg2 arg2-new arg2-events arg2-thm-name arg2-vartys arg2-diffp info gin))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm simpadd0-goutp-of-simpadd0-expr-binary.gout (b* (((mv ?expr ?gout) (simpadd0-expr-binary op arg1 arg1-new arg1-events arg1-thm-name arg1-vartys arg1-diffp arg2 arg2-new arg2-events arg2-thm-name arg2-vartys arg2-diffp info gin))) (simpadd0-goutp gout)) :rule-classes :rewrite)
Theorem:
(defthm expr-unamp-of-simpadd0-expr-binary (implies (and (expr-unambp arg1-new) (expr-unambp arg2-new)) (b* (((mv ?expr ?gout) (simpadd0-expr-binary op arg1 arg1-new arg1-events arg1-thm-name arg1-vartys arg1-diffp arg2 arg2-new arg2-events arg2-thm-name arg2-vartys arg2-diffp info gin))) (expr-unambp expr))))
Theorem:
(defthm simpadd0-expr-binary-support-lemma-1 (b* ((old (c::expr-binary op old-arg1 old-arg2)) (new (c::expr-binary op new-arg1 new-arg2)) (old-arg1-result (c::exec-expr-pure old-arg1 compst)) (old-arg2-result (c::exec-expr-pure old-arg2 compst)) (new-arg1-result (c::exec-expr-pure new-arg1 compst)) (new-arg2-result (c::exec-expr-pure new-arg2 compst)) (old-arg1-value (c::expr-value->value old-arg1-result)) (old-arg2-value (c::expr-value->value old-arg2-result)) (new-arg1-value (c::expr-value->value new-arg1-result)) (new-arg2-value (c::expr-value->value new-arg2-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::binop-purep op) (c::binop-strictp op) (not (c::errorp old-result)) (not (c::errorp new-arg1-result)) (not (c::errorp new-arg2-result)) (equal old-arg1-value new-arg1-value) (equal old-arg2-value new-arg2-value) (equal (c::type-of-value old-arg1-value) (c::type-sint)) (equal (c::type-of-value old-arg2-value) (c::type-sint)) (equal (c::value-kind old-arg1-value) :sint) (equal (c::value-kind old-arg2-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-binary-support-lemma-2 (implies (and (c::binop-strictp op) (or (c::errorp (c::exec-expr-pure arg1 compst)) (c::errorp (c::exec-expr-pure arg2 compst)))) (c::errorp (c::exec-expr-pure (c::expr-binary op arg1 arg2) compst))))
Theorem:
(defthm simpadd0-expr-binary-support-lemma-3 (b* ((zero (c::expr-const (c::const-int (c::make-iconst :value 0 :base (c::iconst-base-oct) :unsignedp nil :length (c::iconst-length-none))))) (expr+zero (c::expr-binary (c::binop-add) expr zero)) (expr-result (c::exec-expr-pure expr compst)) (expr-value (c::expr-value->value expr-result)) (expr+zero-result (c::exec-expr-pure expr+zero compst)) (expr+zero-value (c::expr-value->value expr+zero-result))) (implies (and (not (c::errorp expr-result)) (equal (c::type-of-value expr-value) (c::type-sint)) (equal (c::value-kind expr-value) :sint)) (equal expr+zero-value expr-value))))