gify - ACL2 Book

other

(in-package "GL")

other

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

other

(include-book "defapply")

other

(include-book "misc/hons-help" :dir :system)

other

(include-book "factor-fns")

other

(include-book "g-primitives-help")

other

(include-book "tools/templates" :dir :system)

other

(program)

other

(mutual-recursion (defun collect-fns
    (term clique acc)
    (cond ((or (atom term) (eq (car term) 'quote)) acc)
      ((eq (car term) 'if) (collect-fns-lst (cdr term) clique acc))
      ((symbolp (car term)) (let ((acc (collect-fns-lst (cdr term) clique acc)))
          (if (or (hons-get (car term) acc)
              (member-eq (car term) clique))
            acc
            (hons-acons (car term) t acc))))
      (t (collect-fns (caddar term)
          clique
          (collect-fns-lst (cdr term) clique acc)))))
  (defun collect-fns-lst
    (lst clique acc)
    (if (atom lst)
      acc
      (collect-fns-lst (cdr lst)
        clique
        (collect-fns (car lst) clique acc)))))

clique-bodiesfunction

(defun clique-bodies
  (clique world)
  (if (atom clique)
    nil
    (cons (norm-function-body (car clique) world)
      (clique-bodies (cdr clique) world))))

other

(mutual-recursion (defun collect-fns-fn
    (fn done acc world)
    (if (hons-get fn done)
      (mv done acc)
      (b* ((clique (or (wgetprop fn 'recursivep) (list fn))) (bodies (clique-bodies clique world))
          (body-fns (collect-fns-lst bodies clique nil))
          (body-fns (strip-cars (flush-hons-get-hash-table-link body-fns)))
          (done (hons-put-list clique t done))
          ((mv done acc) (collect-fns-list body-fns
              done
              acc
              world)))
        (mv done (cons (car clique) acc)))))
  (defun collect-fns-list
    (lst done acc world)
    (if (atom lst)
      (mv done acc)
      (mv-let (done acc)
        (collect-fns-fn (car lst)
          done
          acc
          world)
        (collect-fns-list (cdr lst)
          done
          acc
          world)))))

collect-fn-deps-with-exclusionsfunction

(defun collect-fn-deps-with-exclusions
  (fns done-fal world)
  (mv-let (done acc)
    (collect-fns-list fns done-fal nil world)
    (prog2$ (flush-hons-get-hash-table-link done)
      (reverse acc))))

collect-fn-depsfunction

(defun collect-fn-deps
  (fns world)
  (mv-let (done acc)
    (collect-fns-list fns
      (make-fal (append '((return-last))
          (table-alist 'gl-function-info world))
        nil)
      nil
      world)
    (prog2$ (flush-hons-get-hash-table-link done)
      (reverse acc))))

other

(mutual-recursion (defun gify-term
    (x fn)
    (cond ((atom x) (if (constant-syntax-p x)
          `(mk-g-concrete ,GL::X)
          x))
      ((eq (car x) 'quote) `(g-concrete-quote ,GL::X))
      ((eq (car x) 'return-last) (cond ((eq (cadr x) ''time$1-raw) `(time$ ,(GL::GIFY-TERM (CAR (LAST GL::X)) GL::FN)))
          (t (gify-term (car (last x)) fn))))
      ((eq (car x) 'gl-aside) `(gl-aside (hide ,(CADR GL::X))))
      ((eq (car x) 'gl-error) `(gl-error ,(GL::GIFY-TERM (CADR GL::X) GL::FN)))
      ((eq (car x) 'if) (if (equal (cadr x) (caddr x))
          (let* ((test (gify-term (cadr x) fn)) (else (gify-term (cadddr x) fn)))
            `(g-or ,GL::TEST ,GL::ELSE))
          (let* ((test (gify-term (cadr x) fn)) (then (gify-term (caddr x) fn))
              (else (gify-term (cadddr x) fn)))
            `(g-if ,GL::TEST ,GL::THEN ,GL::ELSE))))
      ((consp (car x)) (er hard
          'gify-term
          "We expect lambdas to all have been factored out of functions to
be gified.  If not, implement this case.  Culprit (in function ~x0): ~x1~%"
          fn
          (car x)))
      (t (cons (gl-fnsym (car x))
          (append (gify-term-list (cdr x) fn)
            '(hyp clk config bvar-db state))))))
  (defun gify-term-list
    (x fn)
    (if (endp x)
      nil
      (cons (gify-term (car x) fn)
        (gify-term-list (cdr x) fn)))))

gify-bodyfunction

(defun gify-body
  (x fn)
  (let ((body (cond ((throw-nonexec-error-p x nil nil) (car (last x)))
         (t x))))
    (gify-term body fn)))

eval-thm-bindingsfunction

(defun eval-thm-bindings
  (vars ev)
  (if (atom vars)
    nil
    (if (not (or (eq (car vars) 'hyp)
          (eq (car vars) 'clk)))
      (cons (list (car vars) `(,GL::EV ,(CAR GL::VARS) env))
        (eval-thm-bindings (cdr vars) ev))
      (eval-thm-bindings (cdr vars) ev))))

formals-general-concretepfunction

(defun formals-general-concretep
  (formals)
  (if (atom formals)
    nil
    (cons `(general-concretep ,(CAR GL::FORMALS))
      (formals-general-concretep (cdr formals)))))

formals-general-concrete-objfunction

(defun formals-general-concrete-obj
  (formals)
  (if (atom formals)
    nil
    (cons `(general-concrete-obj ,(CAR GL::FORMALS))
      (formals-general-concrete-obj (cdr formals)))))

gify-factored-fnsfunction

(defun gify-factored-fns
  (top-fn fns idx world defuns)
  (if (endp fns)
    (er hard
      'gify-factored-fns
      "Empty list of functions; top: ~x0~%"
      top-fn)
    (b* ((fn (car fns)) (endp (endp (cdr fns)))
        (body (body (car fns) nil world))
        (gbody (gify-body body (car fns)))
        (formals (wgetprop fn 'formals))
        (recursivep (wgetprop top-fn 'recursivep))
        (guards `(and (natp clk) (glcp-config-p config)))
        (name (gl-fnsym (if endp
              top-fn
              fn)))
        (defun `(defun ,GL::NAME
            ,(APPEND GL::FORMALS '(GL::HYP GL::CLK GL::CONFIG GL::BVAR-DB GL::STATE))
            (declare (xargs :guard ,GL::GUARDS
                :stobjs (bvar-db state)
                :verify-guards nil . ,(AND GL::RECURSIVEP
      `(:MEASURE
        (TWO-NATS-MEASURE GL::CLK
         ,(IF ENDP
              0
              GL::IDX))
        . ,(AND ENDP
                `(:HINTS
                  (("goal" :IN-THEORY
                    (GL::E/D** ((:RULESET GL::CLK-MEASURE-RULES))))))))))
              (ignorable hyp
                clk
                config
                bvar-db
                state . ,GL::FORMALS))
            ,(IF ENDP
     (LET ((GL::CLKBODY
            `(IF (GL::ZP GL::CLK)
                 (GL::PROG2$
                  (GL::CW "~
Warning: Clock ran out in ~x0~%"
                   ',(GL::GL-FNSYM GL::TOP-FN))
                  (GL::G-APPLY ',GL::TOP-FN (GL::GL-LIST . ,GL::FORMALS)))
                 (LET ((GL::CLK (1- GL::CLK)))
                   (DECLARE (IGNORABLE GL::CLK))
                   ,GL::GBODY))))
       (IF (OR (GL::WGETPROP GL::TOP-FN 'GL::NON-EXECUTABLEP)
               (GL::WGETPROP GL::TOP-FN 'GL::CONSTRAINEDP)
               (GL::ASSOC-EQ GL::TOP-FN
                (GL::TABLE-ALIST 'GL::DO-NOT-EXECUTE GL::WORLD)))
           GL::CLKBODY
           `(IF (AND . ,(GL::FORMALS-GENERAL-CONCRETEP GL::FORMALS))
                (GL::MK-G-CONCRETE
                 ,(GL::MAKE-MV-CALL GL::TOP-FN
                   (GL::FORMALS-GENERAL-CONCRETE-OBJ GL::FORMALS) GL::WORLD))
                ,GL::CLKBODY)))
     GL::GBODY))))
      (if endp
        (cons defun defuns)
        (gify-factored-fns top-fn
          (cdr fns)
          (1+ idx)
          world
          (cons defun defuns))))))

factored-fnsmacro

(defmacro factored-fns
  (fn)
  `(cdr (assoc-eq ,GL::FN
      (table-alist 'factored-fns world))))

gify-fn-cliquefunction

(defun gify-fn-clique
  (clique world defuns)
  (if (atom clique)
    defuns
    (gify-fn-clique (cdr clique)
      world
      (gify-factored-fns (car clique)
        (or (factored-fns (car clique))
          (list (car clique)))
        1
        world
        defuns))))

gify-fnfunction

(defun gify-fn
  (fn world)
  (let* ((recp (wgetprop fn 'recursivep)) (clique (or recp (list fn)))
      (defuns (gify-fn-clique clique world nil)))
    (if (and recp (<= 2 (length defuns)))
      `(mutual-recursion . ,GL::DEFUNS)
      `(progn . ,(REVERSE GL::DEFUNS)))))

gify-stubfunction

(defun gify-stub
  (fn world)
  (let* ((formals (wgetprop fn 'formals)) (name (gl-fnsym fn))
      (nonexec (or (wgetprop fn 'constrainedp)
          (wgetprop fn 'non-executablep)
          (assoc-eq fn
            (table-alist 'do-not-execute world)))))
    `(defun ,GL::NAME
      (,@GL::FORMALS hyp
        clk
        config
        bvar-db
        state)
      (declare (xargs :guard (and (natp clk) (glcp-config-p config))
          :stobjs (bvar-db state)
          :verify-guards nil))
      ,(IF GL::NONEXEC
     `(GL::G-APPLY ',GL::FN (GL::GL-LIST . ,GL::FORMALS))
     `(IF (AND . ,(GL::FORMALS-GENERAL-CONCRETEP GL::FORMALS))
          (GL::MK-G-CONCRETE
           ,(GL::MAKE-MV-CALL GL::FN
             (GL::FORMALS-GENERAL-CONCRETE-OBJ GL::FORMALS) GL::WORLD))
          (GL::G-APPLY ',GL::FN (GL::GL-LIST . ,GL::FORMALS)))))))

other

(defconst *no-factor-fns* '(return-last))

gify-fns-and-deps1function

(defun gify-fns-and-deps1
  (deps world)
  (if (endp deps)
    nil
    (if (and (norm-function-body (car deps) world)
        (not (member (car deps) '(return-last))))
      `(,@(AND (NOT (MEMBER (CAR GL::DEPS) GL::*NO-FACTOR-FNS*))
       `((GL::FACTOR-FN ,(CAR GL::DEPS)))) (make-event (gify-fn ',(CAR GL::DEPS) (w state))) . ,(GL::GIFY-FNS-AND-DEPS1 (CDR GL::DEPS) GL::WORLD))
      (prog2$ (cw "Warning: GIFYing undefined function ~x0~%"
          (car deps))
        (cons `(make-event (gify-stub ',(CAR GL::DEPS) (w state)))
          (gify-fns-and-deps1 (cdr deps) world))))))

gify-fns-and-depsfunction

(defun gify-fns-and-deps
  (fns world)
  (let ((deps (collect-fn-deps fns world)))
    `(progn . ,(GL::GIFY-FNS-AND-DEPS1 GL::DEPS GL::WORLD))))

defnamemacro

(defmacro defname
  (name)
  `(or (cdr (assoc-eq ,GL::NAME
        (table-alist 'preferred-defs world)))
    ,GL::NAME))

g-factored-fn-namesfunction

(defun g-factored-fn-names
  (top-fn fns acc)
  (if (endp fns)
    (er hard
      'g-factored-fn-names
      "Empty list of functions; top: ~x0~%"
      top-fn)
    (if (endp (cdr fns))
      (cons (gl-fnsym top-fn) acc)
      (g-factored-fn-names top-fn
        (cdr fns)
        (cons (gl-fnsym (car fns)) acc)))))

g-clique-fn-namesfunction

(defun g-clique-fn-names
  (clique world)
  (wgetprop (car clique) 'recursivep))

clique-fn-namesfunction

(defun clique-fn-names
  (clique world)
  (if (endp clique)
    nil
    (append (factored-fns (car clique))
      (clique-fn-names (cdr clique) world))))

make-expand-listfunction

(defun make-expand-list
  (terms world)
  (if (atom terms)
    nil
    (let ((defname (defname (caar terms))))
      (cons `(:with (:definition ,GL::DEFNAME) ,(CAR GL::TERMS))
        (make-expand-list (cdr terms) world)))))

expand-calls-computed-hintfunction

(defun expand-calls-computed-hint
  (clause fns world)
  (let ((expand-list (find-calls-of-fns-term (car (last clause))
         fns
         nil)))
    `(:expand ,(GL::MAKE-EXPAND-LIST GL::EXPAND-LIST GL::WORLD))))

gl-fnsym-listfunction

(defun gl-fnsym-list
  (lst)
  (if (atom lst)
    nil
    (cons (gl-fnsym (car lst))
      (gl-fnsym-list (cdr lst)))))

make-redundant-listfunction

(defun make-redundant-list
  (names)
  (if (atom names)
    nil
    (cons `(make-redundant ,(CAR GL::NAMES))
      (make-redundant-list (cdr names)))))

flag-fnfunction

(defun flag-fn
  (top-fn)
  (incat 'foo (symbol-name top-fn) "-IND"))

flagify-g-fns-and-deps1function

(defun flagify-g-fns-and-deps1
  (deps world)
  (if (endp deps)
    nil
    (let* ((gfn (gl-fnsym (car deps))) (gfn-recp (wgetprop gfn 'recursivep))
        (rest (flagify-g-fns-and-deps1 (cdr deps) world))
        (rest (if (and (<= 1 (length gfn-recp))
              (not (flag-present gfn world)))
            (let ((gfn (car gfn-recp)))
              (cons `(make-flag ,(GL::FLAG-FN GL::GFN)
                  ,GL::GFN
                  :local t
                  :hints (("goal" :in-theory (e/d** ((:ruleset clk-measure-rules))))))
                rest))
            rest)))
      rest)))

flagify-g-fns-and-depsfunction

(defun flagify-g-fns-and-deps
  (fns world)
  (let ((deps (collect-fn-deps fns world)))
    `(progn . ,(GL::FLAGIFY-G-FNS-AND-DEPS1 GL::DEPS GL::WORLD))))

flagify-fns-and-deps1function

(defun flagify-fns-and-deps1
  (deps world)
  (if (endp deps)
    nil
    (let* ((fn-recp (wgetprop (car deps) 'recursivep)) (rest (flagify-fns-and-deps1 (cdr deps) world))
        (rest (if (and (<= 2 (length fn-recp))
              (not (flag-present (car deps) world)))
            (let ((fn (car fn-recp)))
              (cons `(make-flag ,(GL::FLAG-FN GL::FN) ,GL::FN :local t)
                rest))
            rest)))
      rest)))

flagify-fns-and-depsfunction

(defun flagify-fns-and-deps
  (fns world)
  (let ((deps (collect-fn-deps fns world)))
    `(progn . ,(GL::FLAGIFY-FNS-AND-DEPS1 GL::DEPS GL::WORLD))))

g-factored-fns-verify-guardsfunction

(defun g-factored-fns-verify-guards
  (top-fn fns world)
  (if (endp fns)
    (er hard
      'g-factored-fns-verify-guards
      "Empty list of functions; top: ~x0~%"
      top-fn)
    (if (endp (cdr fns))
      (let ((stobjs-out (wgetprop top-fn 'stobjs-out)))
        `((verify-guards ,(GL::GL-FNSYM GL::TOP-FN)
           ,@(AND GL::STOBJS-OUT (<= 2 (LENGTH GL::STOBJS-OUT))
       (RUNEP `(:TYPE-PRESCRIPTION ,GL::TOP-FN) GL::WORLD)
       `(:HINTS
         (("Goal" :IN-THEORY (GL::ENABLE (:TYPE-PRESCRIPTION ,GL::TOP-FN)))))))))
      `((verify-guards ,(GL::GL-FNSYM (CAR GL::FNS))) . ,(GL::G-FACTORED-FNS-VERIFY-GUARDS GL::TOP-FN (CDR GL::FNS) GL::WORLD)))))

type-prescriptions-of-mv-fnsfunction

(defun type-prescriptions-of-mv-fns
  (clique world)
  (if (atom clique)
    nil
    (let ((stobjs-out (wgetprop (car clique) 'stobjs-out)))
      (if (and stobjs-out
          (<= 2 (length stobjs-out))
          (runep `(:type-prescription ,(CAR GL::CLIQUE)) world))
        (cons `(:type-prescription ,(CAR GL::CLIQUE))
          (type-prescriptions-of-mv-fns (cdr clique)
            world))
        (type-prescriptions-of-mv-fns (cdr clique)
          world)))))

g-guards-fns-and-deps1function

(defun g-guards-fns-and-deps1
  (deps world)
  (if (endp deps)
    nil
    (let* ((gfn (gl-fnsym (car deps))) (recp (wgetprop gfn 'recursivep)))
      (if recp
        (let ((mvtyps (type-prescriptions-of-mv-fns (or (wgetprop (car deps) 'recursivep)
                 (list (car deps)))
               world)))
          (cons `(verify-guards ,(CAR GL::RECP)
              ,@(AND GL::MVTYPS `(:HINTS (("goal" :IN-THEORY (GL::ENABLE . ,GL::MVTYPS))))))
            (g-guards-fns-and-deps1 (cdr deps) world)))
        (append (g-factored-fns-verify-guards (car deps)
            (or (factored-fns (car deps)) (list (car deps)))
            world)
          (g-guards-fns-and-deps1 (cdr deps) world))))))

g-guards-fns-and-depsfunction

(defun g-guards-fns-and-deps
  (fns world)
  (let ((deps (collect-fn-deps fns world)))
    `(progn (logic)
      (local (in-theory (e/d** (minimal-theory (:ruleset g-guard-lemmas)
              zp
              natp)
            ((immediate-force-modep) not)))) . ,(GL::G-GUARDS-FNS-AND-DEPS1 GL::DEPS GL::WORLD))))

ruleset-for-evalfunction

(defun ruleset-for-eval
  (ev)
  (incat ev (symbol-name ev) "-RULESET"))

eval-list-envfunction

(defun eval-list-env
  (ev lst)
  (if (endp lst)
    nil
    (cons `(,GL::EV ,(CAR GL::LST) env)
      (eval-list-env ev (cdr lst)))))

g-correct-factored-thm-bodies-recfunction

(defun g-correct-factored-thm-bodies-rec
  (top-fn fns ev world entries)
  (if (endp fns)
    (er hard
      'g-correct-factored-thm-bodies-rec
      "Empty list of functions; top: ~x0~%"
      top-fn)
    (b* ((endp (endp (cdr fns))) (fn (if endp
            top-fn
            (car fns)))
        (formals (wgetprop fn 'formals))
        (name (gl-fnsym fn))
        (g-correct-thm `(,GL::NAME (implies (bfr-eval hyp (car env))
              (equal (,GL::EV (,GL::NAME ,@GL::FORMALS
                    hyp
                    clk
                    config
                    bvar-db
                    state)
                  env)
                (,GL::FN . ,(GL::EVAL-LIST-ENV GL::EV GL::FORMALS)))) . ,(IF ENDP
     `(:NAME ,(GL::CORRECT-THMNAME GL::NAME))
     `(:SKIP T)))))
      (if endp
        (cons g-correct-thm entries)
        (g-correct-factored-thm-bodies-rec top-fn
          (cdr fns)
          ev
          world
          (cons g-correct-thm entries))))))

g-correct-clique-thm-bodiesfunction

(defun g-correct-clique-thm-bodies
  (clique ev world entries)
  (if (endp clique)
    entries
    (b* ((fn (car clique)) (fns (factored-fns fn))
        (entries (g-correct-factored-thm-bodies-rec fn
            fns
            ev
            world
            entries)))
      (g-correct-clique-thm-bodies (cdr clique)
        ev
        world
        entries))))

factored-fn-correct-thmsfunction

(defun factored-fn-correct-thms
  (clique world)
  (if (atom clique)
    nil
    (if (factored-fns (car clique))
      (cons (correct-thmname (factored-fnname (car clique)))
        (factored-fn-correct-thms (cdr clique) world))
      (factored-fn-correct-thms (cdr clique) world))))

g-correct-factored-thmsfunction

(defun g-correct-factored-thms
  (top-fn fns ev world thms)
  (if (endp fns)
    (er hard
      'g-correct-factored-thms
      "Empty list of functions; top: ~x0~%"
      top-fn)
    (b* ((endp (endp (cdr fns))) (fn (if endp
            top-fn
            (car fns)))
        (definedp (norm-function-body fn world))
        (formals (wgetprop fn 'formals))
        (name (gl-fnsym fn))
        (g-correct-name (correct-thmname name))
        (g-correct-thm `(defthm ,GL::G-CORRECT-NAME
            (implies (bfr-eval hyp (car env))
              (equal (,GL::EV (,GL::NAME ,@GL::FORMALS
                    hyp
                    clk
                    config
                    bvar-db
                    state)
                  env)
                (,GL::FN . ,(GL::EVAL-LIST-ENV GL::EV GL::FORMALS))))
            :hints (("goal" :expand ((,GL::NAME ,@GL::FORMALS
                  hyp
                  clk
                  config
                  bvar-db
                  state))
               ,@(AND ENDP GL::DEFINEDP
       `(:IN-THEORY
         (GL::E/D NIL
          ,(GL::FACTORED-FN-CORRECT-THMS (LIST GL::TOP-FN) GL::WORLD))))) ,@(AND ENDP GL::DEFINEDP
       `((AND GL::STABLE-UNDER-SIMPLIFICATIONP
              '(:IN-THEORY
                (GL::E/D
                 ,(GL::FACTORED-FN-CORRECT-THMS (LIST GL::TOP-FN)
                   GL::WORLD))))))
              ,@(AND GL::DEFINEDP
       `((AND GL::STABLE-UNDER-SIMPLIFICATIONP
              (LET ((GL::LIT (CAR (LAST GL::CLAUSE))))
                (GL::CASE-MATCH GL::LIT
                 (('EQUAL GL::TERM ('QUOTE GL::&))
                  (AND (CONSP GL::TERM) (NOT (EQ (CAR GL::TERM) 'QUOTE))
                       `(:EXPAND (,GL::TERM))))
                 (('EQUAL GL::& GL::TERM)
                  (AND (CONSP GL::TERM) (NOT (EQ (CAR GL::TERM) 'QUOTE))
                       `(:EXPAND (,GL::TERM))))
                 (('NOT GL::TERM)
                  (AND (CONSP GL::TERM) (NOT (EQ (CAR GL::TERM) 'QUOTE))
                       `(:EXPAND (,GL::TERM)))))))))
              (and stable-under-simplificationp
                '(:expand ((:free (x) (hide x))))))))
        (g-correct-thm (if endp
            g-correct-thm
            `(local ,GL::G-CORRECT-THM))))
      (if endp
        (cons g-correct-thm thms)
        (g-correct-factored-thms top-fn
          (cdr fns)
          ev
          world
          (cons g-correct-thm thms))))))

g-correct-flag-lemmafunction

(defun g-correct-flag-lemma
  (fn)
  (incat 'foo
    (symbol-name fn)
    "-CORRECT-LEMMA"))

g-correct-thmnamesfunction

(defun g-correct-thmnames
  (fns)
  (if (endp fns)
    nil
    (cons (correct-thmname (car fns))
      (g-correct-thmnames (cdr fns)))))

clique-gl-function-info-table-eventsfunction

(defun clique-gl-function-info-table-events
  (clique ev)
  (if (atom clique)
    nil
    (cons `(table gl-function-info
        ',(CAR GL::CLIQUE)
        '(,(GL::GL-FNSYM (CAR GL::CLIQUE)) (,(GL::CORRECT-THMNAME (GL::GL-FNSYM (CAR GL::CLIQUE))) . ,GL::EV)))
      (clique-gl-function-info-table-events (cdr clique)
        ev))))

g-correct-thmsfunction

(defun g-correct-thms
  (top-fn ev world)
  (declare (xargs :mode :program))
  (b* ((recp (wgetprop top-fn 'recursivep)) (definedp (norm-function-body top-fn world)))
    (if recp
      (b* ((entries (g-correct-clique-thm-bodies recp
             ev
             world
             nil)) (gfn1 (gl-fnsym (car recp)))
          (gfns (wgetprop gfn1 'recursivep))
          (gfn (car gfns))
          (flag-fn (flag-fn-name gfn world))
          (flag-formals (wgetprop flag-fn 'formals))
          (thmnames (g-correct-thmnames (gl-fnsym-list recp))))
        `(progn (local (in-theory (e/d** (minimal-theory car-cons
                  cdr-cons
                  (cons)
                  (not)
                  (equal)
                  kwote-lst
                  kwote
                  (:ruleset g-correct-lemmas)
                  (:ruleset ,(GL::RULESET-FOR-EVAL GL::EV))
                  (:ruleset apply-rewrites)
                  ,@(GL::FACTORED-FN-CORRECT-THMS GL::RECP GL::WORLD)
                  (:induction ,GL::FLAG-FN)
                  ,(GL::FLAG-EQUIVS-NAME GL::GFN GL::WORLD))
                ((immediate-force-modep) not))))
          (,(GL::FLAG-DEFTHM-MACRO GL::GFN GL::WORLD) ,(GL::G-CORRECT-FLAG-LEMMA GL::GFN)
            ,@GL::ENTRIES
            :hints (("goal" :induct (,GL::FLAG-FN . ,GL::FLAG-FORMALS)
               :in-theory (e/d nil
                 ,@(AND GL::DEFINEDP `(,(GL::FACTORED-FN-CORRECT-THMS GL::RECP GL::WORLD))))) ,@(AND GL::DEFINEDP
       `((GL::EXPAND-CALLS-COMPUTED-HINT CLAUSE '(,@GL::GFNS) GL::WORLD)
         (AND GL::STABLE-UNDER-SIMPLIFICATIONP
              '(:IN-THEORY
                (GL::ENABLE
                 . ,(GL::FACTORED-FN-CORRECT-THMS GL::RECP GL::WORLD))))
         (AND GL::STABLE-UNDER-SIMPLIFICATIONP
              (LET ((GL::LIT (CAR (LAST GL::CLAUSE))))
                (GL::CASE-MATCH GL::LIT
                 (('EQUAL GL::TERM ('QUOTE GL::&))
                  (AND (CONSP GL::TERM) (NOT (EQ (CAR GL::TERM) 'QUOTE))
                       `(:EXPAND (,GL::TERM))))
                 (('EQUAL GL::& GL::TERM)
                  (AND (CONSP GL::TERM) (NOT (EQ (CAR GL::TERM) 'QUOTE))
                       `(:EXPAND (,GL::TERM))))
                 (('NOT GL::TERM)
                  (AND (CONSP GL::TERM) (NOT (EQ (CAR GL::TERM) 'QUOTE))
                       `(:EXPAND (,GL::TERM)))))))
         (AND GL::STABLE-UNDER-SIMPLIFICATIONP
              '(:EXPAND ((:FREE (GL::X) (GL::HIDE GL::X)))))))))
          (add-to-ruleset ,(GL::RULESET-FOR-EVAL GL::EV)
            ',GL::THMNAMES) . ,(GL::CLIQUE-GL-FUNCTION-INFO-TABLE-EVENTS GL::RECP GL::EV)))
      (b* ((fns (or (factored-fns top-fn) (list top-fn))) (thms (g-correct-factored-thms top-fn
              fns
              ev
              world
              nil)))
        `(progn (local (in-theory (e/d** (minimal-theory car-cons
                  cdr-cons
                  (cons)
                  (not)
                  (equal)
                  kwote-lst
                  kwote
                  (:ruleset g-correct-lemmas)
                  (:ruleset ,(GL::RULESET-FOR-EVAL GL::EV))
                  ,@(AND
   (GL::MEMBER-EQ (GL::CORRECT-THMNAME (GL::FACTORED-FNNAME GL::TOP-FN))
    (RULESET 'GL::FACTOR-RULESET))
   (LIST (GL::CORRECT-THMNAME (GL::FACTORED-FNNAME GL::TOP-FN))))
                  (:ruleset apply-rewrites))
                ((immediate-force-modep) not))))
          ,@(REVERSE GL::THMS)
          (add-to-ruleset ,(GL::RULESET-FOR-EVAL GL::EV)
            '(,(GL::CORRECT-THMNAME (GL::GL-FNSYM GL::TOP-FN))))
          (table gl-function-info
            ',GL::TOP-FN
            '(,(GL::GL-FNSYM GL::TOP-FN) (,(GL::CORRECT-THMNAME (GL::GL-FNSYM GL::TOP-FN)) . ,GL::EV))))))))

g-correct-fns-and-deps1function

(defun g-correct-fns-and-deps1
  (deps ev)
  (if (endp deps)
    nil
    `((make-event (g-correct-thms ',(CAR GL::DEPS)
         ',GL::EV
         (w state))) . ,(GL::G-CORRECT-FNS-AND-DEPS1 (CDR GL::DEPS) GL::EV))))

g-correct-fns-and-depsfunction

(defun g-correct-fns-and-deps
  (fns ev world)
  (let ((deps (collect-fn-deps fns world)))
    `(progn . ,(GL::G-CORRECT-FNS-AND-DEPS1 GL::DEPS GL::EV))))

hons-get-anyfunction

(defun hons-get-any
  (lst al)
  (if (atom lst)
    nil
    (or (hons-get (car lst) al)
      (hons-get-any (cdr lst) al))))

remove-cliques-in-alfunction

(defun remove-cliques-in-al
  (fns al world)
  (if (atom fns)
    nil
    (b* ((fn (car fns)) (clique (or (wgetprop fn 'recursivep) (list fn))))
      (if (hons-get-any clique al)
        (remove-cliques-in-al (cdr fns) al world)
        (cons fn
          (remove-cliques-in-al (cdr fns) al world))))))

lambda-for-apply-stub-fifunction

(defun lambda-for-apply-stub-fi
  (oldfns newfns world)
  `(lambda (f args)
    (cond ,@(GL::MAKE-APPLY-ENTRIES
   (GL::REMOVE-CLIQUES-IN-AL GL::NEWFNS (HONS-PUT-LIST GL::OLDFNS T NIL)
    GL::WORLD)
   GL::WORLD NIL)
      (t (apply-stub f args)))))

other

(mutual-recursion (defun subst-fns-term
    (term subst)
    (cond ((or (atom term) (eq (car term) 'quote)) term)
      ((atom (car term)) (let ((lookup (assoc (car term) subst)))
          (cons (if lookup
              (cdr lookup)
              (car term))
            (subst-fns-list (cdr term) subst))))
      (t (cons (list 'lambda
            (cadar term)
            (subst-fns-term (caddar term) subst))
          (subst-fns-list (cdr term) subst)))))
  (defun subst-fns-list
    (lst subst)
    (if (atom lst)
      nil
      (cons (subst-fns-term (car lst) subst)
        (subst-fns-list (cdr lst) subst)))))

equal-f-fnsfunction

(defun equal-f-fns
  (lst)
  (if (atom lst)
    nil
    (cons `(equal f ',(CAR GL::LST))
      (equal-f-fns (cdr lst)))))

eval-g-fifunction

(defun eval-g-fi
  (eval oldeval thmname world)
  (b* (((list eval-list new-ev new-evlst) (cdr (assoc eval (table-alist 'eval-g-table world)))) ((list oldeval-list old-ev old-evlst) (cdr (assoc oldeval
            (table-alist 'eval-g-table world)))))
    `(:functional-instance ,GL::THMNAME
      (,GL::OLD-EV ,GL::NEW-EV)
      (,GL::OLD-EVLST ,GL::NEW-EVLST)
      (,GL::OLDEVAL ,EVAL)
      (,GL::OLDEVAL-LIST ,GL::EVAL-LIST))))

other

(defconst *eval-g-prove-f-i-template*
  '(:computed-hint-replacement ((and stable-under-simplificationp
       '(:expand ((:free (f ar) (_oldgeval_-apply f ar)) (:free (f ar) (_newgeval_-apply f ar))))))
    :use ((:functional-instance _theorem_
       (_oldgeval_ _newgeval_)
       (_oldgeval_-list _newgeval_-list)
       (_oldgeval_-ev _newgeval_-ev)
       (_oldgeval_-ev-lst _newgeval_-ev-lst)))
    :in-theory (e/d** (car-to-nth-meta-correct nth-of-cdr
        list-fix-when-true-listp
        kwote-list-list-fix
        (:t list-fix)
        _oldgeval_-apply-agrees-with-_oldgeval_-ev-rev
        _newgeval_-apply-agrees-with-_newgeval_-ev-rev
        _oldgeval_-ev-rules
        _newgeval_-ev-rules
        _newgeval_-ev-of-fncall-args
        _oldgeval_-ev-of-fncall-args
        _newgeval_-ev-of-nonsymbol-atom
        _oldgeval_-ev-of-nonsymbol-atom
        _newgeval_-ev-of-bad-fncall
        _oldgeval_-ev-of-bad-fncall
        car-cons
        cdr-cons
        nth-0-cons
        (nfix)))
    :expand ((:with _newgeval_ (_newgeval_ x env)) (:with _newgeval_-list
        (_newgeval_-list x env)))
    :do-not-induct t))

eval-g-prove-f-i-fnfunction

(defun eval-g-prove-f-i-fn
  (eval oldeval thmname)
  (declare (xargs :mode :program))
  `(defthm ,GL::THMNAME
    t
    :hints (',(TEMPLATE-SUBST GL::*EVAL-G-PROVE-F-I-TEMPLATE* :ATOM-ALIST
  `((GL::_THEOREM_ :THEOREM
     (EQUAL (,GL::OLDEVAL GL::X GL::ENV) (,GL::OLDEVAL GL::X GL::ENV)))
    (GL::_OLDGEVAL_ . ,GL::OLDEVAL) (GL::_NEWGEVAL_ . ,EVAL))
  :STR-ALIST
  `(("_OLDGEVAL_" ,(SYMBOL-NAME GL::OLDEVAL) . ,GL::OLDEVAL)
    ("_NEWGEVAL_" ,(SYMBOL-NAME EVAL) . ,EVAL))))
    :rule-classes nil))

eval-g-prove-f-imacro

(defmacro eval-g-prove-f-i
  (thmname eval
    oldeval
    &key
    (output '(:off (warning warning!
          observation
          prove
          proof-builder
          history
          event
          proof-tree))))
  `(with-output ,@GL::OUTPUT
    (make-event (eval-g-prove-f-i-fn ',EVAL ',GL::OLDEVAL ',GL::THMNAME))))

f-i-thmnamefunction

(defun f-i-thmname
  (thm eval)
  (incat 'foo
    (symbol-name thm)
    "-FOR-"
    (symbol-name eval)))

eval-g-functional-instance-fnfunction

(defun eval-g-functional-instance-fn
  (eval oldeval thmname world)
  (b* (((list neweval-list
        new-ev
        new-evlst
        new-apply) (cdr (assoc eval (table-alist 'eval-g-table world)))) ((list oldeval-list
         old-ev
         old-evlst
         old-apply) (cdr (assoc oldeval
            (table-alist 'eval-g-table world))))
      (thmbody (wgetprop thmname 'theorem))
      (subst-body (subst-fns-term thmbody
          (list (cons oldeval eval)
            (cons old-apply new-apply)
            (cons oldeval-list neweval-list)
            (cons old-ev new-ev)
            (cons old-evlst new-evlst))))
      (newthmname (f-i-thmname thmname eval)))
    `(defthm ,GL::NEWTHMNAME
      ,GL::SUBST-BODY
      :hints (("goal" :in-theory (theory 'minimal-theory)
         :use (,(GL::EVAL-G-FI EVAL GL::OLDEVAL GL::THMNAME GL::WORLD)))))))

eval-g-functional-instancemacro

(defmacro eval-g-functional-instance
  (thmname eval oldeval)
  `(make-event (eval-g-functional-instance-fn ',EVAL
      ',GL::OLDEVAL
      ',GL::THMNAME
      (w state))))

correctness-lemmas-for-new-apply11function

(defun correctness-lemmas-for-new-apply11
  (alist eval
    world
    done-finsts
    thms
    theory)
  (declare (ignorable world))
  (if (atom alist)
    (mv done-finsts thms theory)
    (b* ((thmbase (caar alist)) (thmeval (cdar alist)))
      (if (cdar alist)
        (b* ((newthmname (f-i-thmname thmbase eval)) ((mv thms done-finsts) (if (member thmeval done-finsts)
                (mv thms done-finsts)
                (mv (cons `(local (eval-g-prove-f-i ,(GL::INCAT 'GL-THM::FOO (SYMBOL-NAME EVAL) "-IS-FUNCTIONAL-INSTANCE-OF-"
  (SYMBOL-NAME GL::THMEVAL))
                        ,EVAL
                        ,GL::THMEVAL))
                    thms)
                  (cons thmeval done-finsts))))
            (thms (cons `(eval-g-functional-instance ,GL::THMBASE
                  ,EVAL
                  ,GL::THMEVAL)
                thms))
            (theory (cons newthmname theory)))
          (correctness-lemmas-for-new-apply11 (cdr alist)
            eval
            world
            done-finsts
            thms
            theory))
        (correctness-lemmas-for-new-apply11 (cdr alist)
          eval
          world
          done-finsts
          thms
          (cons thmbase theory))))))

correctness-lemmas-for-new-apply1function

(defun correctness-lemmas-for-new-apply1
  (alist eval
    world
    done-finsts
    thms
    theory)
  (if (atom alist)
    (mv (reverse thms) theory)
    (mv-let (done-finsts thms theory)
      (correctness-lemmas-for-new-apply11 (cddar alist)
        eval
        world
        done-finsts
        thms
        theory)
      (correctness-lemmas-for-new-apply1 (cdr alist)
        eval
        world
        done-finsts
        thms
        theory))))

pair-ontofunction

(defun pair-onto
  (lst name)
  (if (atom lst)
    nil
    (cons (cons (car lst) name)
      (pair-onto (cdr lst) name))))

correctness-lemmas-for-new-applyfunction

(defun correctness-lemmas-for-new-apply
  (eval world)
  (let ((ruleset (get-ruleset 'generic-geval-g-correct-lemmas world)))
    (mv-let (done thms theory)
      (correctness-lemmas-for-new-apply11 (pair-onto ruleset 'generic-geval)
        eval
        world
        nil
        nil
        nil)
      (correctness-lemmas-for-new-apply1 (table-alist 'gl-function-info world)
        eval
        world
        done
        thms
        theory))))

geval-thm-namesfunction

(defun geval-thm-names
  (names eval)
  (if (atom names)
    nil
    (cons (intern-in-package-of-symbol (concatenate 'string
          (symbol-name (car names))
          "-"
          (symbol-name eval))
        eval)
      (geval-thm-names (cdr names) eval))))

correctness-lemmasmacro

(defmacro correctness-lemmas
  (eval)
  `(make-event (mv-let (events theory)
      (correctness-lemmas-for-new-apply ',EVAL
        (w state))
      (cons 'progn
        (append events
          `((def-ruleset! ,',(GL::RULESET-FOR-EVAL EVAL)
             '(,@'NIL . ,GL::THEORY))))))))

find-definition-numefunction

(defun find-definition-nume
  (pairs)
  (if (atom pairs)
    nil
    (if (eq (cadar pairs) :definition)
      (caar pairs)
      (find-definition-nume (cdr pairs)))))

find-lemma-entryfunction

(defun find-lemma-entry
  (props nume)
  (if (atom props)
    nil
    (if (and (eq (cadar props) 'lemmas)
        (eql (access rewrite-rule (caddar props) :nume)
          nume))
      (car props)
      (find-lemma-entry (cdr props) nume))))

clique-and-controller-alistfunction

(defun clique-and-controller-alist
  (fn world)
  (declare (xargs :mode :program))
  (let* ((props (actual-props (world-to-next-event (cdr (decode-logical-name fn world)))
         nil
         nil)) (nume (find-definition-nume (getprop fn
            'runic-mapping-pairs
            nil
            'current-acl2-world
            world)))
      (lemma (find-lemma-entry props nume)))
    (access rewrite-rule (caddr lemma) :heuristic-info)))

make-unnorm-preferred-defs1function

(defun make-unnorm-preferred-defs1
  (fns world)
  (declare (xargs :mode :program))
  (if (atom fns)
    nil
    (b* ((fn (car fns)) (entry (assoc fn
            (table-alist 'preferred-defs world)))
        (formals (wgetprop fn 'formals 'none))
        (body (wgetprop fn 'unnormalized-body))
        ((when (or entry (not body) (eq formals 'none))) (make-unnorm-preferred-defs1 (cdr fns) world))
        ((when (member fn *definition-minimal-theory*)) (make-unnorm-preferred-defs1 (cdr fns) world))
        (thmname (incat 'foo
            (symbol-package-name fn)
            "::"
            (symbol-name fn)
            "-UNNORM-DEF")))
      (list* `(defthm ,GL::THMNAME
          (equal (,GL::FN . ,GL::FORMALS) ,GL::BODY)
          :hints (("goal" :by ,GL::FN))
          :rule-classes ((:definition :install-body t . ,(AND (GL::WGETPROP GL::FN 'GL::RECURSIVEP)
      (LET ((GL::PAIR (GL::CLIQUE-AND-CONTROLLER-ALIST GL::FN GL::WORLD)))
        `(:CLIQUE ,(CAR GL::PAIR) :CONTROLLER-ALIST ,(CDR GL::PAIR)))))))
        `(in-theory (disable ,GL::THMNAME))
        `(table preferred-defs ',GL::FN ',GL::THMNAME)
        (make-unnorm-preferred-defs1 (cdr fns) world)))))

make-unnorm-preferred-defsfunction

(defun make-unnorm-preferred-defs
  (fns world)
  `(progn . ,(GL::MAKE-UNNORM-PREFERRED-DEFS1 GL::FNS GL::WORLD)))

union-eq-listsfunction

(defun union-eq-lists
  (a)
  (if (atom a)
    nil
    (union-eq (car a) (union-eq-lists (cdr a)))))

strip-nthcdrsfunction

(defun strip-nthcdrs
  (n a)
  (if (atom a)
    nil
    (cons (nthcdr n (car a))
      (strip-nthcdrs n (cdr a)))))

prev-apply-fnsfunction

(defun prev-apply-fns
  (world)
  (declare (xargs :mode :program))
  (union-eq-lists (strip-nthcdrs 6
      (table-alist 'eval-g-table world))))

make-g-world-fnfunction

(defun make-g-world-fn
  (fns ev state)
  (declare (xargs :stobjs state :mode :program))
  (b* ((world (w state)) (new-fns (set-difference-eq (collect-fn-deps fns world)
          '(return-last)))
      (apply-fns (union-eq new-fns
          (prev-apply-fns world)
          (strip-cars (table-alist 'gl-function-info world)))))
    `(encapsulate nil
      (logic)
      (local (table theory-invariant-table nil nil :clear))
      (local (in-theory nil))
      (local (set-default-hints nil))
      (set-bogus-mutual-recursion-ok t)
      (set-bogus-defun-hints-ok t)
      (set-ignore-ok t)
      (set-irrelevant-formals-ok t)
      (local (make-event (make-unnorm-preferred-defs ',GL::NEW-FNS
            (w state))))
      (def-eval-g ,GL::EV ,GL::APPLY-FNS)
      (make-event (gify-fns-and-deps ',GL::NEW-FNS (w state)))
      (make-event (flagify-g-fns-and-deps ',GL::NEW-FNS (w state)))
      (make-event (g-guards-fns-and-deps ',GL::NEW-FNS (w state)))
      (local (def-ruleset! apply-rewrites
          (ruleset ',(GL::INTERN-IN-PACKAGE-OF-SYMBOL
  (CONCATENATE 'STRING (SYMBOL-NAME GL::EV) "-EV-RULES") GL::EV))))
      (correctness-lemmas ,GL::EV)
      (make-event (g-correct-fns-and-deps ',GL::NEW-FNS
          ',GL::EV
          (w state))))))

make-g-worldmacro

(defmacro make-g-world
  (fns ev
    &key
    (output '(:off (warning warning!
          observation
          prove
          proof-builder
          history
          event
          proof-tree)
        :summary-off (:other-than form)
        :gag-mode nil)))
  `(with-output ,@GL::OUTPUT
    (make-event (make-g-world-fn ',GL::FNS ',GL::EV state))))

make-geval-fnfunction

(defun make-geval-fn
  (geval new-fns state)
  (declare (xargs :stobjs state :mode :program))
  (b* ((world (w state)) (new-fns (set-difference-eq (collect-fn-deps new-fns world)
          '(return-last)))
      (fns (union-eq new-fns
          (strip-cars (table-alist 'gl-function-info world))
          (prev-apply-fns world))))
    `(encapsulate nil
      (logic)
      (local (table theory-invariant-table nil nil :clear))
      (local (in-theory nil))
      (set-bogus-mutual-recursion-ok t)
      (set-bogus-defun-hints-ok t)
      (set-ignore-ok t)
      (set-irrelevant-formals-ok t)
      (def-eval-g ,GL::GEVAL ,GL::FNS)
      (correctness-lemmas ,GL::GEVAL))))

make-gevalmacro

(defmacro make-geval
  (geval fns
    &key
    (output '(:off (warning warning!
          observation
          prove
          proof-builder
          history
          event
          proof-tree)
        :summary-off (:other-than form)
        :gag-mode nil)))
  `(with-output ,@GL::OUTPUT
    (make-event (make-geval-fn ',GL::GEVAL ',GL::FNS state))))