Filtering...

g-if

books/centaur/gl/g-if
other
(in-package "GL")
other
(include-book "ite-merge")
other
(include-book "gtests")
other
(local (include-book "gtype-thms"))
g-if-execmacro
(defmacro g-if-exec
  (test then else)
  `(b* (((mv test-res hyp) ,GL::TEST) ((mv test-true test-unknown test-obj hyp) (gtests test-res hyp))
      ((mv contra1 hyp undo) (bfr-assume (bfr-or test-true test-unknown)
          hyp))
      ((mv then-res hyp) (if contra1
          (mv nil hyp)
          ,GL::THEN))
      (hyp (bfr-unassume hyp undo))
      ((mv contra0 hyp undo) (bfr-assume (bfr-or (bfr-not test-true) test-unknown)
          hyp))
      ((mv else-res hyp) (if contra0
          (mv nil hyp)
          ,GL::ELSE))
      (hyp (bfr-unassume hyp undo))
      ((when contra1) (mv else-res hyp))
      ((when contra0) (mv then-res hyp))
      ((mv contra hyp undo) (bfr-assume (bfr-not test-unknown) hyp))
      ((when contra) (b* ((hyp (bfr-unassume hyp undo)))
          (mv (mk-g-ite test-obj then-res else-res)
            hyp)))
      ((mv merge hyp) (gobj-ite-merge test-true
          then-res
          else-res
          hyp))
      (hyp (bfr-unassume hyp undo)))
    (mv (mk-g-bdd-ite test-unknown
        (mk-g-ite test-obj then-res else-res)
        merge
        hyp)
      hyp)))
g-or-execmacro
(defmacro g-or-exec
  (test else)
  `(b* (((mv test-res hyp) ,GL::TEST) ((mv test-true test-unknown test-obj hyp) (gtests test-res hyp))
      ((mv contra0 hyp undo) (bfr-assume (bfr-or (bfr-not test-true) test-unknown)
          hyp))
      ((mv else-res hyp) (if contra0
          (mv nil hyp)
          ,GL::ELSE))
      (hyp (bfr-unassume hyp undo))
      ((when contra0) (mv test-res hyp))
      ((mv contra hyp undo) (bfr-assume (bfr-not test-unknown) hyp))
      ((when contra) (b* ((hyp (bfr-unassume hyp undo)))
          (mv (mk-g-ite test-obj test-res else-res)
            hyp)))
      ((mv merge hyp) (gobj-ite-merge test-true
          test-res
          else-res
          hyp))
      (hyp (bfr-unassume hyp undo)))
    (mv (mk-g-bdd-ite test-unknown
        (mk-g-ite test-obj test-res else-res)
        merge
        hyp)
      hyp)))
other
(define g-if-fn
  (test-res then-res else-res hyp)
  :non-executable t
  :verify-guards nil
  (b* ((hyp (bfr-hyp-fix hyp)) ((mv test-true
         test-unknown
         ?test-obj
         hyp) (gtests test-res hyp))
      ((mv contra1 ?hyp1 ?undo) (bfr-assume (bfr-or test-true test-unknown)
          hyp))
      ((mv contra0 ?hyp0 ?undo) (bfr-assume (bfr-or (bfr-not test-true) test-unknown)
          hyp))
      ((when contra1) (mv (and (not contra0) else-res) hyp))
      ((when contra0) (mv then-res hyp))
      ((mv contra ?hypu ?undo) (bfr-assume (bfr-not test-unknown) hyp))
      ((when contra) (mv (mk-g-ite test-obj then-res else-res)
          hyp))
      ((mv merge ?hypu) (gobj-ite-merge test-true
          then-res
          else-res
          hypu)))
    (mv (mk-g-bdd-ite test-unknown
        (mk-g-ite test-obj then-res else-res)
        merge
        hyp)
      hyp))
  ///
  (def-hyp-congruence g-if-fn :retval 1)
  (defthm g-if-fn-correct
    (implies (bfr-hyp-eval hyp (car env))
      (equal (generic-geval (mv-nth 0
            (g-if-fn test then else hyp))
          env)
        (if (generic-geval test env)
          (generic-geval then env)
          (generic-geval else env)))))
  (defthm gobj-depends-on-of-g-if-fn
    (implies (and (not (gobj-depends-on k p test-res))
        (not (gobj-depends-on k p then-res))
        (not (gobj-depends-on k p else-res)))
      (not (gobj-depends-on k
          p
          (mv-nth 0
            (g-if-fn test-res then-res else-res hyp)))))))
other
(define g-or-fn
  (test-res else-res hyp)
  :non-executable t
  :verify-guards nil
  (b* ((hyp (bfr-hyp-fix hyp)) ((mv test-true
         test-unknown
         ?test-obj
         hyp) (gtests test-res hyp))
      ((mv contra0 ?hyp0 ?undo) (bfr-assume (bfr-or (bfr-not test-true) test-unknown)
          hyp))
      ((when contra0) (mv test-res hyp))
      ((mv contra ?hypu ?undo) (bfr-assume (bfr-not test-unknown) hyp))
      ((when contra) (mv (mk-g-ite test-obj test-res else-res)
          hyp))
      ((mv merge ?hypu) (gobj-ite-merge test-true
          test-res
          else-res
          hypu)))
    (mv (mk-g-bdd-ite test-unknown
        (mk-g-ite test-obj test-res else-res)
        merge
        hyp)
      hyp))
  ///
  (def-hyp-congruence g-or-fn :retval 1)
  (defthm g-or-fn-correct
    (implies (bfr-hyp-eval hyp (car env))
      (equal (generic-geval (mv-nth 0 (g-or-fn test else hyp))
          env)
        (or (generic-geval test env)
          (generic-geval else env)))))
  (defthm gobj-depends-on-of-g-or-fn
    (implies (and (not (gobj-depends-on k p test-res))
        (not (gobj-depends-on k p else-res)))
      (not (gobj-depends-on k
          p
          (mv-nth 0
            (g-or-fn test-res else-res hyp)))))))
g-ifmacro
(defmacro g-if
  (test then else)
  `(non-exec (b* (((mv test-res hyp) ,GL::TEST) ((mv test-true
           test-unknown
           ?test-obj
           hyp) (gtests test-res hyp))
        ((mv ?contra1 hyp1 ?undo) (bfr-assume (bfr-or test-true test-unknown)
            hyp))
        ((mv then-res ?hyp1) (let ((hyp hyp1))
            ,GL::THEN))
        ((mv ?contra0 hyp0 ?undo) (bfr-assume (bfr-or (bfr-not test-true) test-unknown)
            hyp))
        ((mv else-res ?hyp0) (let ((hyp hyp0))
            ,GL::ELSE)))
      (g-if-fn test-res then-res else-res hyp))))
g-ormacro
(defmacro g-or
  (test else)
  `(non-exec (b* (((mv test-res hyp) ,GL::TEST) ((mv test-true
           test-unknown
           ?test-obj
           hyp) (gtests test-res hyp))
        ((mv ?contra0 hyp0 ?undo) (bfr-assume (bfr-or (bfr-not test-true) test-unknown)
            hyp))
        ((mv else-res ?hyp0) (let ((hyp hyp0))
            ,GL::ELSE)))
      (g-or-fn test-res else-res hyp))))
body-replace-g-ifsfunction
(defun body-replace-g-ifs
  (x)
  `(mbe :logic ,GL::X
    :exec ,(SUBLIS `((GL::G-IF . GL::G-IF-EXEC) (GL::G-OR . GL::G-OR-EXEC)) GL::X)))
replace-g-ifsmacro
(defmacro replace-g-ifs
  (x)
  (body-replace-g-ifs x))
g-if-mbemacro
(defmacro g-if-mbe
  (test then else)
  `(mbe :logic (g-if ,GL::TEST ,GL::THEN ,GL::ELSE)
    :exec (g-if-exec ,GL::TEST ,GL::THEN ,GL::ELSE)))
g-or-mbemacro
(defmacro g-or-mbe
  (test else)
  `(mbe :logic (g-or ,GL::TEST ,GL::ELSE)
    :exec (g-or-exec ,GL::TEST ,GL::ELSE)))
gretmacro
(defmacro gret (x) `(mv ,GL::X hyp))
other
(def-b*-binder gret
  :body `(b* (((mv ,(CAR ARGS) hyp) . ,FORMS))
    ,REST-EXPR))