• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
      • Isar
      • Wp-gen
      • Dimacs-reader
      • Pfcs
      • Legacy-defrstobj
      • Proof-checker-array
      • Soft
      • C
      • Farray
      • Rp-rewriter
      • Instant-runoff-voting
      • Imp-language
      • Sidekick
      • Leftist-trees
      • Java
      • Riscv
      • Taspi
      • Bitcoin
      • Des
      • Ethereum
      • X86isa
      • Sha-2
      • Yul
      • Zcash
      • Proof-checker-itp13
      • Regex
      • ACL2-programming-language
      • Json
      • Jfkr
      • Equational
      • Cryptography
      • Poseidon
      • Where-do-i-place-my-book
      • Axe
      • Aleo
        • Aleobft
        • Aleovm
        • Leo
          • Grammar
          • Early-version
            • Json2ast
            • Testing
            • Definition
              • Flattening
                • Flatten-statements/branches
                • Simplify-flattened-if
                • Flatten-expression
                  • Flatten-expression-list
                • Fenv-option
                • Flatten-fundecl
                • Fenv-const-add
                • Fenv
                • Fenv-const-lookup
                • Init-fenv
                • Const-fenv
              • Abstract-syntax
              • Dynamic-semantics
              • Compilation
              • Static-semantics
              • Concrete-syntax
      • Bigmems
      • Builtins
      • Execloader
      • Solidity
      • Paco
      • Concurrent-programs
      • Bls12-377-curves
    • Debugging
    • Community
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Flattening

Flatten-expression

Flatten an expression.

Signature
(flatten-expression expr env) → new-expr
Arguments
expr — Guard (expressionp expr).
env — Guard (fenvp env).
Returns
new-expr — Type (expression-resultp new-expr).

A variable or constant is looked up in the flattening environment. If it is found, it is regarded as a constant, and it is replaced with an expression for its value. If it is not found, it is regarded as a variable, and left unchanged.

A literal is left unchanged.

For a unary expression, first we transform the operand. If the transformed operand is a value expression, we apply the operator to the denoted value, and then we replace the whole unary expression with the value expression that denotes the result value. If the transformed operand is not a value expression, we leave the unary operator applied to the transformed operand.

Binary expressions are handled similarly to unary ones, but both operands must be value expressions in order to apply the operator to the denoted values.

For a conditional expression, we first transform the test. If the transformed test is a value expression that evaluates to true, we transform and return the true branch, ignoring the false branch. If the transformed test is a value expression that evaluates to false, we transform and return the flse branch, ignoring the true branch. If the transformed test is a value expression that evaluates to a non-boolean, it is a static error; this should never happen with type-checked code. If the transformed test is not a value expression, we transform both true and false branches, and return a conditional with the transformed operands.

For a tuple expression, we first transform the components. If they are all value expressions, we evaluate them, obtaining a tuple, and turn that into its value expression.

For a tuple component expression, we first transform the sub-expression. If it is a value expression, we extract the component.

For now we reject function calls; we will cover them later.

Theorem: return-type-of-flatten-expression.new-expr

(defthm return-type-of-flatten-expression.new-expr
  (b* ((?new-expr (flatten-expression expr env)))
    (expression-resultp new-expr))
  :rule-classes :rewrite)

Theorem: return-type-of-flatten-expression-list.new-exprs

(defthm return-type-of-flatten-expression-list.new-exprs
  (b* ((?new-exprs (flatten-expression-list exprs env)))
    (expression-list-resultp new-exprs))
  :rule-classes :rewrite)

Theorem: flatten-expression-of-expression-fix-expr

(defthm flatten-expression-of-expression-fix-expr
  (equal (flatten-expression (expression-fix expr)
                             env)
         (flatten-expression expr env)))

Theorem: flatten-expression-of-fenv-fix-env

(defthm flatten-expression-of-fenv-fix-env
  (equal (flatten-expression expr (fenv-fix env))
         (flatten-expression expr env)))

Theorem: flatten-expression-list-of-expression-list-fix-exprs

(defthm flatten-expression-list-of-expression-list-fix-exprs
  (equal (flatten-expression-list (expression-list-fix exprs)
                                  env)
         (flatten-expression-list exprs env)))

Theorem: flatten-expression-list-of-fenv-fix-env

(defthm flatten-expression-list-of-fenv-fix-env
  (equal (flatten-expression-list exprs (fenv-fix env))
         (flatten-expression-list exprs env)))

Theorem: flatten-expression-expression-equiv-congruence-on-expr

(defthm flatten-expression-expression-equiv-congruence-on-expr
  (implies (expression-equiv expr expr-equiv)
           (equal (flatten-expression expr env)
                  (flatten-expression expr-equiv env)))
  :rule-classes :congruence)

Theorem: flatten-expression-fenv-equiv-congruence-on-env

(defthm flatten-expression-fenv-equiv-congruence-on-env
  (implies (fenv-equiv env env-equiv)
           (equal (flatten-expression expr env)
                  (flatten-expression expr env-equiv)))
  :rule-classes :congruence)

Theorem: flatten-expression-list-expression-list-equiv-congruence-on-exprs

(defthm
  flatten-expression-list-expression-list-equiv-congruence-on-exprs
  (implies (expression-list-equiv exprs exprs-equiv)
           (equal (flatten-expression-list exprs env)
                  (flatten-expression-list exprs-equiv env)))
  :rule-classes :congruence)

Theorem: flatten-expression-list-fenv-equiv-congruence-on-env

(defthm flatten-expression-list-fenv-equiv-congruence-on-env
  (implies (fenv-equiv env env-equiv)
           (equal (flatten-expression-list exprs env)
                  (flatten-expression-list exprs env-equiv)))
  :rule-classes :congruence)

Subtopics

Flatten-expression-list
Flatten a list of expressions.