|
|
|---|
|
|
|
|---|
Transform a cast expression.
(simpadd0-expr-cast type type-new type-events
type-thm-name type-vartys type-diffp
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 possibly transformed type name with the possibly transformed argument expression.
For now, we generate no theorem for the transformation of the type name, but we double-check that here. We generate a theorem only if we generated one for the argument expression and the old and new type names are the same (i.e. no transformation).
Function:
(defun simpadd0-expr-cast (type type-new type-events type-thm-name type-vartys type-diffp arg arg-new arg-events arg-thm-name arg-vartys arg-diffp info gin) (declare (xargs :guard (and (tynamep type) (tynamep type-new) (pseudo-event-form-listp type-events) (symbolp type-thm-name) (ident-type-mapp type-vartys) (booleanp type-diffp) (exprp arg) (exprp arg-new) (pseudo-event-form-listp arg-events) (symbolp arg-thm-name) (ident-type-mapp arg-vartys) (booleanp arg-diffp) (tyname-infop info) (simpadd0-ginp gin)))) (declare (xargs :guard (and (tyname-unambp type) (tyname-unambp type-new) (expr-unambp arg) (expr-unambp arg-new)))) (let ((__function__ 'simpadd0-expr-cast)) (declare (ignorable __function__)) (b* (((simpadd0-gin gin) gin) (expr (make-expr-cast :type type :arg arg)) (expr-new (make-expr-cast :type type-new :arg arg-new)) (type-vartys (ident-type-map-fix type-vartys)) (arg-vartys (ident-type-map-fix arg-vartys)) ((unless (omap::compatiblep type-vartys arg-vartys)) (raise "Internal error: ~ incompatible variable-type maps ~x0 and ~x1." type-vartys arg-vartys) (mv (irr-expr) (irr-simpadd0-gout))) (vartys (omap::update* type-vartys arg-vartys)) (diffp (or type-diffp arg-diffp)) ((when type-thm-name) (raise "Internal error: ~ unexpected type name transformation theorem ~x0." type-thm-name) (mv (irr-expr) (irr-simpadd0-gout))) ((c$::tyname-info info) info) ((unless (and arg-thm-name (not type-diffp) (type-formalp info.type) (not (type-case info.type :void)) (not (type-case info.type :char)))) (mv expr-new (make-simpadd0-gout :events (append type-events arg-events) :thm-name nil :thm-index gin.thm-index :names-to-avoid gin.names-to-avoid :vartys vartys :diffp diffp))) ((unless (equal type type-new)) (raise "Internal error: ~ type names ~x0 and ~x1 differ." type type-new) (mv (irr-expr) (irr-simpadd0-gout))) (hints (cons (cons '"Goal" (cons ':in-theory (cons ''((:e ldm-expr) (:e ldm-tyname) (:e c::expr-cast) (:e c::tyname-to-type) (:e c::type-nonchar-integerp)) (cons ':use (cons (cons arg-thm-name (cons (cons ':instance (cons 'simpadd0-expr-cast-support-lemma-1 (cons (cons 'tyname (cons (cons 'mv-nth (cons '1 (cons (cons 'ldm-tyname (cons (cons 'quote (cons type 'nil)) 'nil)) '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-cast-support-lemma-2 (cons (cons 'tyname (cons (cons 'mv-nth (cons '1 (cons (cons 'ldm-tyname (cons (cons 'quote (cons type 'nil)) 'nil)) '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 type-events arg-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-cast.expr (b* (((mv ?expr ?gout) (simpadd0-expr-cast type type-new type-events type-thm-name type-vartys type-diffp 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-cast.gout (b* (((mv ?expr ?gout) (simpadd0-expr-cast type type-new type-events type-thm-name type-vartys type-diffp 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-cast (implies (and (tyname-unambp type-new) (expr-unambp arg-new)) (b* (((mv ?expr ?gout) (simpadd0-expr-cast type type-new type-events type-thm-name type-vartys type-diffp arg arg-new arg-events arg-thm-name arg-vartys arg-diffp info gin))) (expr-unambp expr))))
Theorem:
(defthm simpadd0-expr-cast-support-lemma-1 (b* ((old (c::expr-cast tyname old-arg)) (new (c::expr-cast tyname 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)) (type (c::type-of-value old-arg-value)) (type1 (c::tyname-to-type tyname))) (implies (and (not (c::errorp old-result)) (not (c::errorp new-arg-result)) (equal old-arg-value new-arg-value) (c::type-nonchar-integerp type) (c::type-nonchar-integerp type1)) (and (not (c::errorp new-result)) (equal old-value new-value) (equal (c::type-of-value old-value) type1)))))
Theorem:
(defthm simpadd0-expr-cast-support-lemma-2 (implies (c::errorp (c::exec-expr-pure arg compst)) (c::errorp (c::exec-expr-pure (c::expr-cast tyname arg) compst))))