Filtering...

cgen-state

books/acl2s/cgen/cgen-state
other
(in-package "CGEN")
other
(include-book "acl2s-parameter")
other
(include-book "utilities")
other
(include-book "basis")
other
(defrec gcs%
  ((runs dups . vacs) (cts . wts))
  nil)
other
(def-const *initial-gcs%*
  (make gcs% :cts 0 :wts 0 :runs 0 :vacs 0 :dups 0))
other
(def-const *gcs-fields*
  '(cts wts runs dups vacs))
gcs%-pfunction
(defun gcs%-p
  (v)
  (declare (xargs :guard t))
  (case-match v
    (('gcs% (runs dups . vacs)
       (cts . wts)) (and (unsigned-60bits-p cts)
        (unsigned-60bits-p wts)
        (unsigned-60bits-p runs)
        (unsigned-60bits-p dups)
        (unsigned-60bits-p vacs)))))
gcs-1+macro
(defmacro gcs-1+
  (fld-nm)
  `(change gcs%
    ,CGEN::FLD-NM
    (1+f (access gcs% ,CGEN::FLD-NM))))
other
(def-const *cgen-state-givens*
  '(start-time user-supplied-term
    displayed-goal
    top-ctx
    params))
other
(def-const *cgen-state-derived*
  '(top-vt-alist))
other
(def-const *cgen-state-transient*
  '(gcs processor-hist
    s-hist
    stopping-condition-p
    proof-aborted-p
    end-time))
other
(def-const *cgen-state-fields*
  (append *cgen-state-transient*
    *cgen-state-givens*
    *cgen-state-derived*))
cgen-state-pfunction
(defun cgen-state-p
  (v)
  (declare (xargs :guard t))
  (and (symbol-alistp v)
    (assoc-eq 'user-supplied-term v)
    (assoc-eq 'displayed-goal v)
    (assoc-eq 'start-time v)
    (assoc-eq 'params v)
    (symbol-alistp (cdr (assoc-eq 'params v)))
    (assoc-eq 'top-ctx v)
    (gcs%-p (cdr (assoc-eq 'gcs v)))))
cget-fnfunction
(defun cget-fn
  (key cgen-state)
  (declare (xargs :guard (and (cgen-state-p cgen-state)
        (member-eq key *cgen-state-fields*))))
  (let ((entry (assoc-eq key cgen-state)))
    (if (consp entry)
      (cdr entry)
      nil)))
cget-param-fnfunction
(defun cget-param-fn
  (key cgen-state)
  (declare (xargs :guard (and (cgen-state-p cgen-state)
        (acl2s-parameter-p key))))
  (let* ((params (cget-fn 'params cgen-state)) (entry (assoc-eq (keywordify key) params)))
    (if (consp entry)
      (cdr entry)
      nil)))
cgetmacro
(defmacro cget
  (key)
  "get value of key from cgen-state. if key is a param-key is acl2s-parameters,
then appropriately get the corresponding value stored in the param field of
cgen-state"
  (cond ((member-eq key *cgen-state-fields*) (list 'cget-fn
        (kwote key)
        'cgen-state))
    ((acl2s-parameter-p key) (list 'cget-param-fn
        (kwote key)
        'cgen-state))
    (t (er hard
        'cget
        "~| Unsupported cgen-state field/key: ~x0~%"
        key))))
cput-fnfunction
(defun cput-fn
  (key val cgen-state)
  (declare (xargs :guard (and (cgen-state-p cgen-state)
        (member-eq key *cgen-state-fields*))))
  (put-assoc-eq key val cgen-state))
cputmacro
(defmacro cput
  (key val)
  "put value into key entry of cgen-state (acl2s-parameter keys not allowed, unlike cget)"
  (list 'cput-fn
    (kwote key)
    val
    'cgen-state))
var-pfunction
(defun var-p
  (x)
  (declare (xargs :guard t))
  (and (symbolp x)
    (not (or (keywordp x)
        (booleanp x)
        (legal-constantp x)))))
var-listpfunction
(defun var-listp
  (x)
  (declare (xargs :guard t))
  (if (consp x)
    (and (var-p (car x))
      (var-listp (cdr x)))
    (null x)))
var-alistpfunction
(defun var-alistp
  (x)
  (declare (xargs :guard t))
  (if (consp x)
    (and (consp (car x))
      (var-p (caar x))
      (var-alistp (cdr x)))
    (null x)))
other
(defstub allowed-cgen-event-ctx-p
  (*)
  =>
  *)
allowed-cgen-event-ctx-p-no-defunfunction
(defun allowed-cgen-event-ctx-p-no-defun
  (ctx)
  (declare (xargs :guard t))
  (cond ((equal ctx "( THM ...)") t)
    ((equal ctx :undefined) t)
    ((member-equal ctx '(thm defthm verify-guards)))
    ((and (consp ctx)
       (member-equal (car ctx) '(defthm verify-guards))) t)
    ((and (consp ctx)
       (member-equal (car ctx)
         (list "( VERIFY-GUARDS ~x0)"))) t)
    (t nil)))
other
(defattach allowed-cgen-event-ctx-p
  allowed-cgen-event-ctx-p-no-defun)
cgen-params-p1function
(defun cgen-params-p1
  (v)
  "alist capturing key-value pair from acl2s-defaults-table"
  (declare (xargs :verify-guards nil :guard t))
  (b* (((assocs (num-trials :num-trials)
        (verbosity-level :verbosity-level)
        (num-counterexamples :num-counterexamples)
        (num-witnesses :num-witnesses)
        (sampling-method :sampling-method)
        (backtrack-limit :backtrack-limit)
        (search-strategy :search-strategy)
        (testing-enabled :testing-enabled)
        (cgen-local-timeout :cgen-local-timeout)
        (cgen-single-test-timeout :cgen-single-test-timeout)
        (print-cgen-summary :print-cgen-summary)
        (use-fixers :use-fixers)
        (recursively-fix :recursively-fix)
        (num-print-counterexamples :num-print-counterexamples)
        (num-print-witnesses :num-print-witnesses)) v))
    (and (fixnump num-trials)
      (fixnump verbosity-level)
      (fixnump num-counterexamples)
      (fixnump num-witnesses)
      (member-eq sampling-method
        *sampling-method-values*)
      (fixnump backtrack-limit)
      (member-eq search-strategy
        *search-strategy-values*)
      (member-eq testing-enabled
        *testing-enabled-values*)
      (rationalp cgen-local-timeout)
      (rationalp cgen-single-test-timeout)
      (booleanp print-cgen-summary)
      (booleanp use-fixers)
      (booleanp recursively-fix)
      (fixnump num-print-counterexamples)
      (fixnump num-print-witnesses))))
cgen-params-pfunction
(defun cgen-params-p
  (v)
  (declare (xargs :guard t))
  (ec-call (cgen-params-p1 v)))
other
(defrec test-outcomes%
  ((|#cts| cts cts-hyp-vals-list) (|#wts| wts wts-hyp-vals-list)
    (|#vacs| vacs vacs-hyp-vals-list)
    |#dups|
    disp-enum-alist
    elim-bindings)
  nil)
test-outcomes%-pfunction
(defun test-outcomes%-p
  (v)
  (declare (xargs :guard t))
  (case-match v
    (('test-outcomes% (|#cts| cts cts-hyp-vals-list)
       (|#wts| wts wts-hyp-vals-list)
       (|#vacs| vacs vacs-hyp-vals-list)
       |#dups|
       disp-enum-alist
       elim-bindings) (and (symbol-doublet-list-listp cts)
        (symbol-doublet-list-listp wts)
        (symbol-doublet-list-listp vacs)
        (true-list-listp cts-hyp-vals-list)
        (true-list-listp wts-hyp-vals-list)
        (true-list-listp vacs-hyp-vals-list)
        (unsigned-60bits-p |#wts|)
        (unsigned-60bits-p |#cts|)
        (unsigned-60bits-p |#vacs|)
        (unsigned-60bits-p |#dups|)
        (symbol-alistp disp-enum-alist)
        (alistp elim-bindings)))))
test-outcomes-1+macro
(defmacro test-outcomes-1+
  (fld)
  "increments the number-valued fields of test-outcomes%"
  (declare (xargs :guard (member-eq fld
        '(cts wts vacs dups))))
  (let* ((fld-dc (string-downcase (symbol-name fld))) (fld-nm (fix-intern-in-pkg-of-sym (concatenate-names (list "#" fld-dc))
          'test-outcomes%)))
    `(change test-outcomes%
      ,CGEN::FLD-NM
      (1+f (access test-outcomes% ,CGEN::FLD-NM)))))
other
(defrec s-hist-entry%
  (test-outcomes (hyps vars . concl)
    (elide-map)
    (start-time . end-time) . name)
  nil)
s-hist-entry%-pfunction
(defun s-hist-entry%-p
  (v)
  (declare (xargs :guard t))
  (case-match v
    (('s-hist-entry% test-outcomes
       (hyps vars . concl)
       (elide-map)
       (start-time . end-time) . name) (and (test-outcomes%-p test-outcomes)
        (pseudo-term-listp hyps)
        (pseudo-termp concl)
        (symbol-listp vars)
        (symbol-alistp elide-map)
        (stringp name)
        (rationalp start-time)
        (rationalp end-time)))))
s-hist-pfunction
(defun s-hist-p
  (v)
  "is a alist mapping strings to s-hist-entry% records"
  (declare (xargs :guard t))
  (if (atom v)
    (null v)
    (and (consp (car v))
      (stringp (caar v))
      (s-hist-entry%-p (cdar v))
      (s-hist-p (cdr v)))))
valid-cgen-state-p1function
(defun valid-cgen-state-p1
  (v)
  (declare (xargs :verify-guards nil :guard t))
  (b* (((assocs gcs
        processor-hist
        s-hist
        stopping-condition-p
        proof-aborted-p
        start-time
        user-supplied-term
        displayed-goal
        top-ctx
        params
        top-vt-alist) v))
    (and (gcs%-p gcs)
      (subsetp-eq processor-hist
        *preprocess-clause-ledge*)
      (s-hist-p s-hist)
      (booleanp stopping-condition-p)
      (booleanp proof-aborted-p)
      (rationalp start-time)
      (pseudo-termp user-supplied-term)
      (not (eq :undefined displayed-goal))
      (or (member-eq top-ctx
          '(:user-defined test? itest? itest?))
        (not (null top-ctx)))
      (cgen-params-p params)
      (var-alistp top-vt-alist))))
valid-cgen-state-pfunction
(defun valid-cgen-state-p
  (v)
  (declare (xargs :guard t))
  (ec-call (valid-cgen-state-p1 v)))
other
(encapsulate ((stopping-condition? (gcs% nc nw)
     t
     :guard (and (gcs%-p gcs%)
       (natp nc)
       (natp nw))))
  (local (defun stopping-condition?
      (x y z)
      (list x y z))))
stopping-condition?-builtinfunction
(defun stopping-condition?-builtin
  (gcs% num-cts num-wts)
  (declare (xargs :guard (and (natp num-cts)
        (natp num-wts)
        (gcs%-p gcs%))))
  (and (>= (access gcs% cts)
      (nfix num-cts))
    (>= (access gcs% wts)
      (nfix num-wts))))
other
(defattach stopping-condition?
  stopping-condition?-builtin)
other
(table builtin-relations
  nil
  '((:member member-equal member-eq member) (:assoc assoc-equal
      assoc
      assoc-eq
      assoc-eql)
    (:equal =
      equal
      eq
      eql
      int=
      string-equal
      hons-equal
      ==)
    (:less < <=)
    (:greater > >=))
  :clear)
membership-relationpfunction
(defun membership-relationp
  (r wrld)
  (or (member-equal r
      '(member-eq member
        member-eql
        member-equal
        in
        in))
    (b* ((br-tbl (table-alist 'builtin-relations wrld)) (mem-relations (get1 :member br-tbl)))
      (member-equal r mem-relations))))
add-builtin-relationfunction
(defun add-builtin-relation
  (key r wrld)
  (b* ((br-tbl (table-alist 'builtin-relations wrld)) (relations (get1 key br-tbl))
      (new-val (append relations (list r))))
    new-val))
add-member-builtin-relationmacro
(defmacro add-member-builtin-relation
  (r)
  `(table builtin-relations
    :member (add-builtin-relation :member ',CGEN::R world)
    :put))
other
(defstub fixer-arrangement
  (* * * * state)
  =>
  (mv * * state))
fixer-arrangement/dummyfunction
(defun fixer-arrangement/dummy
  (hyps concl vl ctx state)
  (declare (ignore hyps concl vl ctx))
  (declare (xargs :stobjs (state)))
  (mv nil (list nil nil) state))
other
(defattach (fixer-arrangement fixer-arrangement/dummy))
other
(defstub fxri-let*-soln
  (* * * * * state)
  =>
  (mv * * state))
fxri-let*-soln/dummyfunction
(defun fxri-let*-soln/dummy
  (flits term->f-lits-lst
    relevant-terms
    |FXRI{}|
    vl
    state)
  (declare (ignore flits
      term->f-lits-lst
      relevant-terms
      |FXRI{}|
      vl))
  (declare (xargs :stobjs (state)))
  (mv nil (list nil nil) state))
other
(defattach (fxri-let*-soln fxri-let*-soln/dummy))
get-hypfunction
(defun get-hyp
  (form)
  (declare (xargs :guard t))
  (if (atom form)
    t
    (if (and (consp (cdr form))
        (eq 'implies (first form)))
      (second form)
      t)))
get-hypsfunction
(defun get-hyps
  (pform)
  (declare (xargs :guard t))
  (b* ((hyp (get-hyp pform)) ((when (eq hyp 't)) nil)
      ((unless (and (consp hyp)
           (consp (cdr hyp))
           (eq (car hyp) 'and))) (list hyp))
      (rst (cdr hyp)))
    rst))
get-conclfunction
(defun get-concl
  (form)
  (declare (xargs :guard t))
  (if (atom form)
    form
    (if (and (consp (cdr form))
        (consp (cddr form))
        (eq 'implies (first form)))
      (third form)
      form)))
other
(program)
other
(mutual-recursion (defun strip-return-last
    (term)
    (declare (xargs :verify-guards nil
        :guard (pseudo-termp term)))
    (cond ((variablep term) term)
      ((fquotep term) term)
      ((eq (ffn-symb term) 'hide) term)
      (t (let* ((stripped-args (strip-return-last-lst (fargs term))) (fn (ffn-symb term)))
          (cond ((eq fn 'return-last) (car (last stripped-args)))
            (t (cons-term fn stripped-args)))))))
  (defun strip-return-last-lst
    (term-lst)
    (declare (xargs :guard (pseudo-term-listp term-lst)))
    (cond ((endp term-lst) 'nil)
      (t (cons (strip-return-last (car term-lst))
          (strip-return-last-lst (cdr term-lst)))))))
other
(mutual-recursion (defun strip-force
    (term)
    (declare (xargs :verify-guards nil
        :guard (pseudo-termp term)))
    (cond ((variablep term) term)
      ((fquotep term) term)
      ((eq (ffn-symb term) 'hide) term)
      (t (let* ((stripped-args (strip-force-lst (fargs term))) (fn (ffn-symb term)))
          (cond ((eq fn 'force) (first stripped-args))
            (t (cons-term fn stripped-args)))))))
  (defun strip-force-lst
    (term-lst)
    (declare (xargs :guard (pseudo-term-listp term-lst)))
    (cond ((endp term-lst) 'nil)
      (t (cons (strip-force (car term-lst))
          (strip-force-lst (cdr term-lst)))))))
orient-equalityfunction
(defun orient-equality
  (term)
  (declare (xargs :guard (pseudo-termp term)))
  (if (and (consp term)
      (member-eq (car term) '(equal eq eql =))
      (consp (cdr term))
      (consp (cddr term))
      (variablep (third term)))
    (list (first term)
      (third term)
      (second term))
    term))
other
(include-book "acl2s/defdata/defdata-util" :dir :system)
other
(defloop orient-equalities
  (terms)
  (for ((term in terms))
    (collect (orient-equality term))))
partition-hyps-conclfunction
(defun partition-hyps-concl
  (term str state)
  (declare (xargs :stobjs (state)))
  (b* ((term (expand-lambda term)) (wrld (w state))
      (pform (prettyify-clause (list term) nil wrld))
      ((mv phyps pconcl) (mv (get-hyps pform)
          (get-concl pform)))
      ((er hyps) (translate-term-lst phyps
          t
          nil
          t
          str
          wrld
          state))
      ((er concl) (translate pconcl
          t
          nil
          t
          str
          wrld
          state)))
    (mv hyps concl state)))
partition-into-hyps-concl-and-preprocessfunction
(defun partition-into-hyps-concl-and-preprocess
  (term str state)
  (declare (xargs :stobjs (state)))
  (b* ((term (expand-lambda term)) (wrld (w state))
      (pform (prettyify-clause (list term) nil wrld))
      ((mv phyps pconcl) (mv (get-hyps pform)
          (get-concl pform)))
      ((er hyps) (translate-term-lst phyps
          t
          nil
          t
          str
          wrld
          state))
      ((er concl) (translate pconcl
          t
          nil
          t
          str
          wrld
          state))
      (hyps (strip-return-last-lst hyps))
      (hyps (strip-force-lst hyps))
      (concl (strip-return-last concl))
      (concl (strip-force concl))
      (hyps (orient-equalities hyps))
      (concl (orient-equality concl)))
    (mv hyps concl state)))