param

(in-package "GL")

(include-book "bfr-param")

(include-book "gtypes")

(include-book "bvar-db")

(include-book "std/stobjs/clone" :dir :system)

(include-book "centaur/ubdds/param" :dir :system)

(include-book "centaur/ubdds/lite" :dir :system)

(include-book "centaur/aig/misc" :dir :system)

(local (include-book "gtype-thms"))

(local (include-book "data-structures/no-duplicates" :dir :system))

(local (include-book "tools/mv-nth" :dir :system))

(local (include-book "ihs/ihs-lemmas" :dir :system))

(local (include-book "centaur/aig/eval-restrict" :dir :system))

(local (include-book "std/util/support" :dir :system))

(local (in-theory (disable append-of-nil)))

(in-theory (disable bfr-to-param-space
    bfr-list-to-param-space))

(mutual-recursion (defun gobj-to-param-space
    (x p)
    (declare (xargs :guard t :verify-guards nil))
    (if (atom x)
      x
      (pattern-match x
        ((g-concrete &) x)
        ((g-boolean b) (mk-g-boolean (bfr-to-param-space p b)))
        ((g-integer bits) (mk-g-integer (bfr-list-to-param-space p bits)))
        ((g-ite if then else) (mk-g-ite (gobj-to-param-space if p)
            (gobj-to-param-space then p)
            (gobj-to-param-space else p)))
        ((g-apply fn args) (g-apply fn
            (gobj-list-to-param-space args p)))
        ((g-var &) x)
        (& (gl-cons (gobj-to-param-space (car x) p)
            (gobj-to-param-space (cdr x) p))))))
  (defun gobj-list-to-param-space
    (x p)
    (declare (xargs :guard t))
    (if (atom x)
      nil
      (cons (gobj-to-param-space (car x) p)
        (gobj-list-to-param-space (cdr x) p)))))

(verify-guards gobj-to-param-space
  :hints (("Goal" :in-theory (e/d nil ((force))))))

(local (defthm nth-open-const-idx
    (implies (syntaxp (quotep n))
      (equal (nth n lst)
        (if (zp n)
          (car lst)
          (nth (1- n) (cdr lst)))))
    :hints (("Goal" :in-theory (enable nth)))))

(local (defthm bfr-eval-list-nil
    (equal (bfr-eval-list nil env) nil)
    :hints (("goal" :in-theory (enable bfr-eval-list)))))

(local (defthm bfr-eval-list-t
    (equal (bfr-eval-list '(t) env) '(t))
    :hints (("goal" :in-theory (enable bfr-eval-list)))))

(defthm-gobj-flag (defthm gobj-to-param-space-correct
    (implies (bfr-eval p (car env))
      (equal (generic-geval (gobj-to-param-space x p)
          (genv-param p env))
        (generic-geval x env)))
    :flag gobj)
  (defthm gobj-list-to-param-space-correct
    (implies (bfr-eval p (car env))
      (equal (generic-geval-list (gobj-list-to-param-space x p)
          (genv-param p env))
        (generic-geval-list x env)))
    :flag list)
  :hints (("Goal" :in-theory (e/d* (genv-param default-car default-cdr)
       ((force) bfr-eval-list
         boolean-listp
         bfr-eval
         (:rules-of-class :type-prescription :here)
         bfr-to-param-space
         bfr-list-to-param-space
         bfr-param-env
         generic-geval
         hons-assoc-equal)
       ((:type-prescription len)))
     :expand ((gobj-to-param-space x p) (gobj-list-to-param-space x p))
     :do-not-induct t) (and stable-under-simplificationp
      '(:expand ((:free (env) (generic-geval x env)))))
    (and stable-under-simplificationp
      (expand-calls-computed-hint clause
        '(generic-geval generic-geval-list)))))

(defthm-gobj-flag (defthm gobj-to-param-space-correct-with-unparam-env
    (implies (and (syntaxp (not (and (consp env) (eq (car env) 'genv-param))))
        (bdd-mode-or-p-true p (car env)))
      (equal (generic-geval (gobj-to-param-space x p)
          env)
        (generic-geval x (genv-unparam p env))))
    :flag gobj)
  (defthm gobj-list-to-param-space-correct-with-unparam-env
    (implies (and (syntaxp (not (and (consp env) (eq (car env) 'genv-param))))
        (bdd-mode-or-p-true p (car env)))
      (equal (generic-geval-list (gobj-list-to-param-space x p)
          env)
        (generic-geval-list x
          (genv-unparam p env))))
    :flag list)
  :hints (("Goal" :in-theory (e/d* (genv-unparam default-car default-cdr)
       ((force) bfr-eval-list
         boolean-listp
         bfr-eval
         (:rules-of-class :type-prescription :here)
         bfr-to-param-space
         bfr-list-to-param-space
         bfr-param-env
         generic-geval
         hons-assoc-equal)
       ((:type-prescription len)))
     :expand ((gobj-to-param-space x p) (gobj-list-to-param-space x p))
     :do-not-induct t) (and stable-under-simplificationp
      '(:expand ((:free (env) (generic-geval x env)))))
    (and stable-under-simplificationp
      (expand-calls-computed-hint clause
        '(generic-geval generic-geval-list)))))

(defthm eval-bfr-to-param-space-self
  (implies (bfr-eval x (car env))
    (bfr-eval (bfr-to-param-space x x)
      (car (genv-param x env))))
  :hints (("Goal" :in-theory (enable bfr-eval
       bfr-to-param-space
       genv-param
       bfr-param-env
       bfr-unparam-env
       default-car))))

(defun gobj-alist-to-param-space
  (alist p)
  (declare (xargs :guard t))
  (if (atom alist)
    nil
    (if (consp (car alist))
      (cons (cons (caar alist)
          (gobj-to-param-space (cdar alist) p))
        (gobj-alist-to-param-space (cdr alist) p))
      (gobj-alist-to-param-space (cdr alist) p))))

(defthm alistp-gobj-alist-to-param-space
  (alistp (gobj-alist-to-param-space x pathcond)))

(defstobj-clone bvar-db1 bvar-db :suffix "1")

(defund parametrize-bvar-db-aux
  (n p bvar-db bvar-db1)
  (declare (xargs :stobjs (bvar-db bvar-db1)
      :guard (and (natp n)
        (<= (base-bvar bvar-db) n)
        (<= n (next-bvar bvar-db)))
      :measure (nfix (- (next-bvar bvar-db) (nfix n)))))
  (b* (((when (mbe :logic (zp (- (next-bvar bvar-db) (nfix n)))
          :exec (int= (next-bvar bvar-db) n))) bvar-db1) (gobj (get-bvar->term n bvar-db))
      (pgobj (gobj-to-param-space gobj p))
      (bvar-db1 (add-term-bvar pgobj bvar-db1)))
    (parametrize-bvar-db-aux (+ 1 (lnfix n))
      p
      bvar-db
      bvar-db1)))

(defund parametrize-term-equivs
  (p x)
  (declare (xargs :guard (alistp x)))
  (if (atom x)
    nil
    (hons-acons (gobj-to-param-space (caar x) p)
      (cdar x)
      (parametrize-term-equivs p (cdr x)))))

(defund parametrize-bvar-db
  (p bvar-db bvar-db1)
  (declare (xargs :stobjs (bvar-db bvar-db1)
      :verify-guards nil))
  (b* ((base (base-bvar bvar-db)) (bvar-db1 (init-bvar-db base bvar-db1))
      (bvar-db1 (parametrize-bvar-db-aux base
          p
          bvar-db
          bvar-db1)))
    (update-term-equivs (parametrize-term-equivs p
        (term-equivs bvar-db))
      bvar-db1)))

(defsection parametrize-bvar-db
  (local (in-theory (enable parametrize-bvar-db
        parametrize-bvar-db-aux)))
  (local (include-book "arithmetic/top-with-meta" :dir :system))
  (local (include-book "std/basic/arith-equivs" :dir :system))
  (local (defthm alistp-when-term-equivsp
      (implies (and (bind-free '((bvar-db . bvar-db)) (bvar-db))
          (term-equivsp$a x bvar-db))
        (alistp x))
      :hints (("Goal" :in-theory (enable alistp)))))
  (defthm get-bvar->term-of-parametrize-bvar-db-aux
    (implies (and (<= (base-bvar$a bvar-db1) (nfix m))
        (< (nfix m)
          (+ (next-bvar$a bvar-db1)
            (- (next-bvar$a bvar-db) (nfix n)))))
      (equal (get-bvar->term$a m
          (parametrize-bvar-db-aux n
            p
            bvar-db
            bvar-db1))
        (if (<= (next-bvar$a bvar-db1) (nfix m))
          (gobj-to-param-space (get-bvar->term$a (+ (- (nfix m) (next-bvar$a bvar-db1))
                (nfix n))
              bvar-db)
            p)
          (get-bvar->term$a m bvar-db1)))))
  (defthm base-bvar-of-parametrize-bvar-db-aux
    (equal (base-bvar$a (parametrize-bvar-db-aux n
          p
          bvar-db
          bvar-db1))
      (base-bvar$a bvar-db1)))
  (defthm next-bvar-of-parametrize-bvar-db-aux
    (equal (next-bvar$a (parametrize-bvar-db-aux n
          p
          bvar-db
          bvar-db1))
      (+ (nfix (- (next-bvar$a bvar-db) (nfix n)))
        (next-bvar$a bvar-db1))))
  (local (defthm bvar-listp-when-same-next/base
      (implies (and (bvar-listp$a x bvar-db)
          (equal (base-bvar$a bvar-db)
            (base-bvar$a bvar-db1))
          (equal (next-bvar$a bvar-db)
            (next-bvar$a bvar-db1)))
        (bvar-listp$a x bvar-db1))
      :hints (("Goal" :induct (len x)))))
  (local (defthm term-equivsp-when-same-next/base
      (implies (and (term-equivsp$a x bvar-db)
          (equal (base-bvar$a bvar-db)
            (base-bvar$a bvar-db1))
          (equal (next-bvar$a bvar-db)
            (next-bvar$a bvar-db1)))
        (term-equivsp$a x bvar-db1))
      :hints (("Goal" :induct (len x)))))
  (defthm term-equivsp-of-parametrize-term-equivs
    (implies (and (bind-free (and (consp x)
            (equal (car x) 'term-equivs$a)
            `((bvar-db . ,(CADR GL::X))))
          (bvar-db))
        (term-equivsp x bvar-db)
        (equal (base-bvar$a bvar-db)
          (base-bvar$a bvar-db1))
        (equal (next-bvar$a bvar-db)
          (next-bvar$a bvar-db1)))
      (term-equivsp$a (parametrize-term-equivs p x)
        bvar-db1))
    :hints (("Goal" :in-theory (enable parametrize-term-equivs))))
  (verify-guards parametrize-bvar-db)
  (defthm normalize-parametrize-bvar-db
    (implies (syntaxp (not (equal bvar-db1 ''nil)))
      (equal (parametrize-bvar-db p bvar-db bvar-db1)
        (parametrize-bvar-db p bvar-db nil))))
  (defthm base-bvar-of-parametrize-bvar-db
    (equal (base-bvar$a (parametrize-bvar-db p bvar-db bvar-db1))
      (base-bvar$a bvar-db)))
  (defthm next-bvar-of-parametrize-bvar-db
    (equal (next-bvar$a (parametrize-bvar-db p bvar-db bvar-db1))
      (next-bvar$a bvar-db)))
  (defthm get-bvar->term-of-parametrize-bvar-db
    (implies (and (<= (base-bvar$a bvar-db) (nfix n))
        (< (nfix n) (next-bvar$a bvar-db)))
      (equal (get-bvar->term$a n
          (parametrize-bvar-db p bvar-db bvar-db1))
        (gobj-to-param-space (get-bvar->term$a n bvar-db)
          p)))))