|
|
|---|
|
|
|
|---|
Transform a binary expression.
(simpadd0-expr-binary op arg1 arg1-new
arg1-events arg1-thm-name arg1-vars
arg1-diffp arg2 arg2-new arg2-events
arg2-thm-name arg2-vars arg2-diffp 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 use it always in the proof for simplicity.
Function:
(defun simpadd0-expr-binary (op arg1 arg1-new arg1-events arg1-thm-name arg1-vars arg1-diffp arg2 arg2-new arg2-events arg2-thm-name arg2-vars arg2-diffp gin) (declare (xargs :guard (and (c$::binopp op) (exprp arg1) (exprp arg1-new) (pseudo-event-form-listp arg1-events) (symbolp arg1-thm-name) (ident-setp arg1-vars) (booleanp arg1-diffp) (exprp arg2) (exprp arg2-new) (pseudo-event-form-listp arg2-events) (symbolp arg2-thm-name) (ident-setp arg2-vars) (booleanp arg2-diffp) (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)) (expr-new (if (and (c$::binop-case op :add) (expr-case arg1-new :ident) (c$::type-case (c$::var-info->type (c$::coerce-var-info (c$::expr-ident->info arg1-new))) :sint) (c$::expr-zerop arg2-new)) (expr-fix arg1-new) (make-expr-binary :op op :arg1 arg1-new :arg2 arg2-new))) (vars (union arg1-vars arg2-vars)) (diffp (or arg1-diffp arg2-diffp)) ((unless (and arg1-thm-name arg2-thm-name (member-eq (c$::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 :vars vars :diffp diffp))) (hints (cons (cons '"Goal" (cons ':in-theory (cons ''((:e c$::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)) (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 (c$::ldm-binop op) 'nil)) 'nil)) (cons (cons 'old-arg1 (cons (cons 'mv-nth (cons '1 (cons (cons 'c$::ldm-expr (cons (cons 'quote (cons arg1 'nil)) 'nil)) 'nil))) 'nil)) (cons (cons 'old-arg2 (cons (cons 'mv-nth (cons '1 (cons (cons 'c$::ldm-expr (cons (cons 'quote (cons arg2 'nil)) 'nil)) 'nil))) 'nil)) (cons (cons 'new-arg1 (cons (cons 'mv-nth (cons '1 (cons (cons 'c$::ldm-expr (cons (cons 'quote (cons arg1-new 'nil)) 'nil)) 'nil))) 'nil)) (cons (cons 'new-arg2 (cons (cons 'mv-nth (cons '1 (cons (cons 'c$::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 (c$::ldm-binop op) 'nil)) 'nil)) (cons (cons 'arg1 (cons (cons 'mv-nth (cons '1 (cons (cons 'c$::ldm-expr (cons (cons 'quote (cons arg1 'nil)) 'nil)) 'nil))) 'nil)) (cons (cons 'arg2 (cons (cons 'mv-nth (cons '1 (cons (cons 'c$::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 'c$::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 vars 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) :vars vars :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-vars arg1-diffp arg2 arg2-new arg2-events arg2-thm-name arg2-vars arg2-diffp 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-vars arg1-diffp arg2 arg2-new arg2-events arg2-thm-name arg2-vars arg2-diffp 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-vars arg1-diffp arg2 arg2-new arg2-events arg2-thm-name arg2-vars arg2-diffp 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::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::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::value-kind expr-value) :sint)) (equal expr+zero-value expr-value))))