Filtering...

g-primitives-help

books/centaur/gl/g-primitives-help
other
(in-package "GL")
other
(include-book "tools/flag" :dir :system)
other
(include-book "gl-util")
other
(include-book "bvar-db")
other
(include-book "glcp-config")
other
(include-book "std/util/support" :dir :system)
other
(program)
acl2-count-formals-listfunction
(defun acl2-count-formals-list
  (formals)
  (if (atom formals)
    nil
    (cons `(acl2-count ,(CAR GL::FORMALS))
      (acl2-count-formals-list (cdr formals)))))
def-g-fnmacro
(defmacro def-g-fn
  (fn body
    &key
    measure
    hyp-hints
    pres-hints
    hyp-fix-hints
    (replace-g-ifs 't))
  `(make-event (b* ((gfn (gl-fnsym ',GL::FN)) (world (w state))
        (formals (wgetprop ',GL::FN 'formals))
        (params '(hyp clk config bvar-db state))
        (measure (or ',GL::MEASURE
            `(+ . ,(GL::ACL2-COUNT-FORMALS-LIST GL::FORMALS))))
        (?gcall (cons gfn (append formals params)))
        (hyp-hints ,GL::HYP-HINTS)
        (pres-hints ,GL::PRES-HINTS)
        (hyp-fix-hints ,GL::HYP-FIX-HINTS)
        (body ,(IF GL::REPLACE-G-IFS
     `(GL::BODY-REPLACE-G-IFS ,GL::BODY)
     GL::BODY)))
      `(progn (encapsulate nil
          (set-bogus-measure-ok t)
          (defun ,GL::GFN
            (,@GL::FORMALS hyp
              clk
              config
              bvar-db
              state)
            (declare (xargs :guard (and (natp clk) (glcp-config-p config))
                :measure ,GL::MEASURE
                :verify-guards nil
                :stobjs (hyp bvar-db state))
              (ignorable ,@GL::FORMALS . ,GL::PARAMS))
            (let* ((hyp (lbfr-hyp-fix hyp)))
              ,GL::BODY)))
        (def-hyp-congruence ,GL::GFN
          :hints ,GL::HYP-HINTS
          :pres-hints ,GL::PRES-HINTS
          :hyp-fix-hints ,GL::HYP-FIX-HINTS)
        (in-theory (disable (:d ,GL::GFN)))
        (table g-functions ',',GL::FN ',GL::GFN)))))
def-g-binary-op-bodyfunction
(defun def-g-binary-op-body
  (a b fn gfn body)
  `(cond ((and (general-concretep ,GL::A)
       (general-concretep ,GL::B)) (gret (mk-g-concrete (ec-call (,GL::FN (general-concrete-obj ,GL::A)
              (general-concrete-obj ,GL::B))))))
    ((mbe :logic (eq (tag ,GL::A) :g-ite)
       :exec (and (consp ,GL::A) (eq (tag ,GL::A) :g-ite))) (if (zp clk)
        (gret (g-apply ',GL::FN (gl-list ,GL::A ,GL::B)))
        (let* ((test (g-ite->test ,GL::A)) (then (g-ite->then ,GL::A))
            (else (g-ite->else ,GL::A)))
          (g-if (gret test)
            (,GL::GFN then
              ,GL::B
              hyp
              clk
              config
              bvar-db
              state)
            (,GL::GFN else
              ,GL::B
              hyp
              clk
              config
              bvar-db
              state)))))
    ((mbe :logic (eq (tag ,GL::B) :g-ite)
       :exec (and (consp ,GL::B) (eq (tag ,GL::B) :g-ite))) (if (zp clk)
        (gret (g-apply ',GL::FN (gl-list ,GL::A ,GL::B)))
        (let* ((test (g-ite->test ,GL::B)) (then (g-ite->then ,GL::B))
            (else (g-ite->else ,GL::B)))
          (g-if (gret test)
            (,GL::GFN ,GL::A
              then
              hyp
              clk
              config
              bvar-db
              state)
            (,GL::GFN ,GL::A
              else
              hyp
              clk
              config
              bvar-db
              state)))))
    ((mbe :logic (not (member-eq (tag ,GL::A) '(:g-var :g-apply)))
       :exec (or (atom ,GL::A)
         (not (member-eq (tag ,GL::A) '(:g-var :g-apply))))) (cond ((mbe :logic (not (member-eq (tag ,GL::B) '(:g-var :g-apply)))
           :exec (or (atom ,GL::B)
             (not (member-eq (tag ,GL::B) '(:g-var :g-apply))))) ,GL::BODY)
        (t (gret (g-apply ',GL::FN (gl-list ,GL::A ,GL::B))))))
    (t (gret (g-apply ',GL::FN (gl-list ,GL::A ,GL::B))))))
def-g-binary-opmacro
(defmacro def-g-binary-op
  (fn body
    &key
    hyp-hints
    pres-hints
    hyp-fix-hints)
  `(make-event (let* ((fn ',GL::FN) (world (w state))
        (formals (wgetprop ',GL::FN 'formals))
        (a (car formals))
        (b (cadr formals)))
      `(def-g-fn ,GL::FN
        (let ((a ',GL::A) (b ',GL::B) (fn ',GL::FN))
          (def-g-binary-op-body a
            b
            fn
            gfn
            ',',GL::BODY))
        :hyp-hints ,',GL::HYP-HINTS
        :pres-hints ,',GL::PRES-HINTS
        :hyp-fix-hints ,',GL::HYP-FIX-HINTS))))
correct-thmnamefunction
(defun correct-thmname
  (fn)
  (incat 'foo (symbol-name fn) "-CORRECT"))
correct1-thmnamefunction
(defun correct1-thmname
  (fn)
  (incat 'foo (symbol-name fn) "-CORRECT1"))
ev-formals-listfunction
(defun ev-formals-list
  (ev formals)
  (declare (xargs :mode :logic :guard t))
  (if (atom formals)
    nil
    (cons `(,GL::EV ,(CAR GL::FORMALS) env)
      (ev-formals-list ev (cdr formals)))))
def-g-correct-thm-fnfunction
(defun def-g-correct-thm-fn
  (gfn fn ev hints world)
  (b* ((formals (wgetprop fn 'formals)) (thmname (correct-thmname gfn)))
    `(encapsulate nil
      (defthm ,GL::THMNAME
        (implies (bfr-hyp-eval hyp (car env))
          (equal (,GL::EV (mv-nth 0
                (,GL::GFN ,@GL::FORMALS
                  hyp
                  clk
                  config
                  bvar-db
                  state))
              env)
            (,GL::FN . ,(GL::EV-FORMALS-LIST GL::EV GL::FORMALS))))
        :hints ,GL::HINTS)
      (in-theory (disable ,GL::GFN))
      (table sym-counterparts-table
        ',GL::FN
        '(,GL::GFN ,GL::THMNAME))
      (table gl-function-info
        ',GL::FN
        '(,GL::GFN (,GL::THMNAME . ,GL::EV))))))
def-g-correct-thm-macrofunction
(defun def-g-correct-thm-macro
  (fn ev hints)
  `(make-event (b* ((fn ',GL::FN) (gfn (gl-fnsym fn))
        (world (w state))
        (formals (wgetprop fn 'formals))
        (params '(hyp clk config bvar-db state))
        (?gcall (cons gfn (append formals params)))
        (?fcall (cons fn formals)))
      (def-g-correct-thm-fn gfn
        ',GL::FN
        ',GL::EV
        ,GL::HINTS
        (w state)))))
def-g-correct-thmmacro
(defmacro def-g-correct-thm
  (fn ev &key hints)
  (def-g-correct-thm-macro fn ev hints))
verify-g-guardsmacro
(defmacro verify-g-guards
  (fn &key hints)
  `(make-event (let ((gfn (gl-fnsym ',GL::FN)))
      `(encapsulate nil
        (local (in-theory (enable g-if-fn g-or-fn)))
        (verify-guards ,GL::GFN :hints ,,GL::HINTS)))))
not-gobj-depends-on-hypsfunction
(defun not-gobj-depends-on-hyps
  (formals)
  (if (atom formals)
    nil
    (cons `(not (gobj-depends-on badvar
          parambfr
          ,(CAR GL::FORMALS)))
      (not-gobj-depends-on-hyps (cdr formals)))))
dependency-thmnamefunction
(defun dependency-thmname
  (fn)
  (incat 'foo
    (symbol-name fn)
    "-DEPENDENCIES"))
def-gobj-dependency-thm-fnfunction
(defun def-gobj-dependency-thm-fn
  (gcall fn hints world)
  (b* ((formals (wgetprop fn 'formals)) (thmname (dependency-thmname fn)))
    `(encapsulate nil
      (defthm ,GL::THMNAME
        (implies (and . ,(GL::NOT-GOBJ-DEPENDS-ON-HYPS GL::FORMALS))
          (not (gobj-depends-on badvar
              parambfr
              (mv-nth 0 ,GL::GCALL))))
        :hints ,GL::HINTS)
      (table sym-counterpart-dep-thms
        ',GL::FN
        ',GL::THMNAME))))
def-gobj-dependency-thm-macrofunction
(defun def-gobj-dependency-thm-macro
  (fn hints)
  `(make-event (b* ((fn ',GL::FN) (gfn (gl-fnsym fn))
        (world (w state))
        (formals (wgetprop fn 'formals))
        (params '(hyp clk config bvar-db state))
        (gcall (cons gfn (append formals params))))
      (def-gobj-dependency-thm-fn gcall
        ',GL::FN
        ,GL::HINTS
        (w state)))))
def-gobj-dependency-thmmacro
(defmacro def-gobj-dependency-thm
  (fn &key hints)
  (def-gobj-dependency-thm-macro fn hints))