		Search-engine friendly clone of the ACL2 documentation.

Flattening

Flatten-statements/branches

Flatten statements and branches.

Definitions and Theorems

Function: flatten-statement

(defun flatten-statement (stmt env)
 (declare (xargs :guard (and (statementp stmt) (fenvp env))))
 (let ((__function__ 'flatten-statement))
  (declare (ignorable __function__))
  (statement-case
   stmt :let
   (b* (((vardecl decl) stmt.get)
        ((okf new-init)
         (flatten-expression decl.init env)))
     (statement-let (change-vardecl stmt.get
                                    :init new-init)))
   :const
   (reserrf (list :static :unreachable))
   :assign
   (b* (((okf new-left)
         (flatten-expression stmt.left env))
        ((okf new-right)
         (flatten-expression stmt.right env)))
     (make-statement-assign :op stmt.op
                            :left new-left
                            :right new-right))
   :return
   (b* (((okf new-value)
         (flatten-expression stmt.value env)))
     (make-statement-return :value new-value))
   :for (reserrf (list :dynamic :todo-for))
   :if
   (b* (((okf new-branches)
         (flatten-branch-list stmt.branches env))
        ((okf new-else)
         (flatten-statement-list stmt.else env)))
     (simplify-flattened-if new-branches new-else))
   :console
   (console-case
    stmt.get :assert
    (b* (((okf new-arg)
          (flatten-expression stmt.get.arg env)))
      (statement-console (console-assert new-arg)))
    :error
    (b* (((okf new-exprs)
          (flatten-expression-list stmt.get.exprs env)))
      (statement-console (make-console-error :string stmt.get.string
                                             :exprs new-exprs)))
    :log
    (b* (((okf new-exprs)
          (flatten-expression-list stmt.get.exprs env)))
      (statement-console (make-console-log :string stmt.get.string
                                           :exprs new-exprs))))
   :finalize
   (reserrf :flattening-finalize-statement-not-yet-implemented)
   :increment
   (reserrf :flattening-increment-statement-not-yet-implemented)
   :decrement
   (reserrf :flattening-decrement-statement-not-yet-implemented)
   :block
   (b* (((okf new-stmts)
         (flatten-statement-list stmt.get env)))
     (statement-block new-stmts)))))

Function: flatten-statement-list

(defun flatten-statement-list (stmts env)
 (declare (xargs :guard (and (statement-listp stmts)
                             (fenvp env))))
 (let ((__function__ 'flatten-statement-list))
   (declare (ignorable __function__))
   (b* (((when (endp stmts)) nil)
        (stmt (car stmts)))
     (if (statement-case stmt :const)
         (b* (((constdecl decl)
               (statement-const->get stmt))
              ((okf new-init)
               (flatten-expression decl.init env))
              ((unless (expression-valuep new-init))
               (reserrf (list :static :const-init-not-value)))
              (val (value-expr-to-value new-init (fenv->curve env)))
              ((when (reserrp val))
               (reserrf (list :static val)))
              (env (fenv-const-add decl.name val env))
              ((unless env)
               (reserrf (list :static :duplicate-const))))
           (flatten-statement-list (cdr stmts)
                                   env))
       (b* (((okf new-stmt)
             (flatten-statement stmt env))
            ((okf new-stmts)
             (flatten-statement-list (cdr stmts)
                                     env)))
         (cons new-stmt new-stmts))))))

Function: flatten-branch

(defun flatten-branch (branch env)
  (declare (xargs :guard (and (branchp branch) (fenvp env))))
  (let ((__function__ 'flatten-branch))
    (declare (ignorable __function__))
    (b* (((okf new-test)
          (flatten-expression (branch->test branch)
                              env))
         ((okf new-body)
          (flatten-statement-list (branch->body branch)
                                  env)))
      (make-branch :test new-test
                   :body new-body))))

Function: flatten-branch-list

(defun flatten-branch-list (branches env)
  (declare (xargs :guard (and (branch-listp branches)
                              (fenvp env))))
  (let ((__function__ 'flatten-branch-list))
    (declare (ignorable __function__))
    (b* (((when (endp branches)) nil)
         ((okf new-branch)
          (flatten-branch (car branches) env))
         ((okf new-branches)
          (flatten-branch-list (cdr branches)
                               env)))
      (cons new-branch new-branches))))

Theorem: return-type-of-flatten-statement.new-stmt

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

Theorem: return-type-of-flatten-statement-list.new-stmts

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

Theorem: return-type-of-flatten-branch.new-branch

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

Theorem: return-type-of-flatten-branch-list.new-branches

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

Theorem: flatten-statement-of-statement-fix-stmt

(defthm flatten-statement-of-statement-fix-stmt
  (equal (flatten-statement (statement-fix stmt)
                            env)
         (flatten-statement stmt env)))

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

(defthm flatten-statement-of-fenv-fix-env
  (equal (flatten-statement stmt (fenv-fix env))
         (flatten-statement stmt env)))

Theorem: flatten-statement-list-of-statement-list-fix-stmts

(defthm flatten-statement-list-of-statement-list-fix-stmts
  (equal (flatten-statement-list (statement-list-fix stmts)
                                 env)
         (flatten-statement-list stmts env)))

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

(defthm flatten-statement-list-of-fenv-fix-env
  (equal (flatten-statement-list stmts (fenv-fix env))
         (flatten-statement-list stmts env)))

Theorem: flatten-branch-of-branch-fix-branch

(defthm flatten-branch-of-branch-fix-branch
  (equal (flatten-branch (branch-fix branch) env)
         (flatten-branch branch env)))

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

(defthm flatten-branch-of-fenv-fix-env
  (equal (flatten-branch branch (fenv-fix env))
         (flatten-branch branch env)))

Theorem: flatten-branch-list-of-branch-list-fix-branches

(defthm flatten-branch-list-of-branch-list-fix-branches
  (equal (flatten-branch-list (branch-list-fix branches)
                              env)
         (flatten-branch-list branches env)))

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

(defthm flatten-branch-list-of-fenv-fix-env
  (equal (flatten-branch-list branches (fenv-fix env))
         (flatten-branch-list branches env)))

Theorem: flatten-statement-statement-equiv-congruence-on-stmt

(defthm flatten-statement-statement-equiv-congruence-on-stmt
  (implies (statement-equiv stmt stmt-equiv)
           (equal (flatten-statement stmt env)
                  (flatten-statement stmt-equiv env)))
  :rule-classes :congruence)

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

(defthm flatten-statement-fenv-equiv-congruence-on-env
  (implies (fenv-equiv env env-equiv)
           (equal (flatten-statement stmt env)
                  (flatten-statement stmt env-equiv)))
  :rule-classes :congruence)

Theorem: flatten-statement-list-statement-list-equiv-congruence-on-stmts

(defthm
    flatten-statement-list-statement-list-equiv-congruence-on-stmts
  (implies (statement-list-equiv stmts stmts-equiv)
           (equal (flatten-statement-list stmts env)
                  (flatten-statement-list stmts-equiv env)))
  :rule-classes :congruence)

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

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

Theorem: flatten-branch-branch-equiv-congruence-on-branch

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

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

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

Theorem: flatten-branch-list-branch-list-equiv-congruence-on-branches

(defthm flatten-branch-list-branch-list-equiv-congruence-on-branches
  (implies (branch-list-equiv branches branches-equiv)
           (equal (flatten-branch-list branches env)
                  (flatten-branch-list branches-equiv env)))
  :rule-classes :congruence)

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

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

Subtopics

Flatten-statement: Flatten a statement.
Flatten-statement-list: Flatten a list of statements.
Flatten-branch-list: Flatten a list of branches.
Flatten-branch: Flatten a branch.