(parse-svtv-to-fsm-thm thmname args state) → thmobj
Function:
(defun parse-svtv-to-fsm-thm (thmname args state) (declare (xargs :stobjs (state))) (declare (xargs :stobjs state)) (declare (xargs :guard t)) (let ((__function__ 'parse-svtv-to-fsm-thm)) (declare (ignorable __function__)) (b* ((defaults (table-alist 'svtv-to-fsm-thm-defaults (w state))) (ctx (cons 'def-svtv-to-fsm-thm (cons thmname 'nil))) (full-args args) (args (if (keywordp (car args)) args (cdr args))) ((std::extract-keyword-args :defaults defaults :ctx ctx svtv-spec-thmname eliminate-override-vars eliminate-override-signals (rule-classes ':rewrite) (cycle-num-rewrite-strategy ':by-cycle) (base-cycle-var 'base-cycle) primary-output-var (pkg-sym thmname)) args) (svtv-spec-thmname (or svtv-spec-thmname (and (not (keywordp (car full-args))) (car full-args)))) ((unless (and svtv-spec-thmname (symbolp svtv-spec-thmname))) (er hard ctx "~x0 must be specified" :svtv-spec-thmname)) (svtv-thm (cdr (assoc-eq svtv-spec-thmname (table-alist 'svtv-generalized-thm-table (w state))))) ((unless svtv-thm) (er hard ctx "No entry in the ~x0 for svtv-spec-thm ~x1" 'svtv-generalized-thm-table svtv-spec-thmname)) ((unless (member-eq cycle-num-rewrite-strategy '(:all-free :by-cycle :single-var))) (er hard ctx "Unknown :cycle-num-rewrite-strategy argument ~x0: possible values are ~&1~%" cycle-num-rewrite-strategy '(:all-free :by-cycle :single-var))) ((svtv-generalized-thm svtv-thm)) ((with-fast svtv-thm.triple-val-alist)) ((unless svtv-thm.svtv-spec) (er hard ctx "The ~x0 must be about an svtv-spec, but ~x1 is not" :svtv-spec-thmname svtv-spec-thmname)) (fsm (cdr (assoc svtv-thm.svtv-spec (table-alist 'svtv-spec-to-fsm-table (w state))))) ((unless fsm) (er hard ctx "The svtv-spec ~x0 associated with theorem ~x1 doesn't ~ have an associated FSM. Ensure that the svtv-spec was ~ defined using ~x2 with the ~x3 option." svtv-thm.svtv-spec svtv-spec-thmname 'def-svtv-refinement :fsm)) ((mv err svtv-spec-val) (magic-ev-fncall svtv-thm.svtv-spec nil state t t)) ((when err) (er hard ctx "Couldn't evaluate ~x0" (list svtv-thm.svtv-spec))) ((svtv-spec svtv-spec-val)) ((with-fast svtv-spec-val.namemap)) (primary-output-var (or primary-output-var (car svtv-thm.output-vars))) (svtv-actual-override-vars (svex-alistlist-vars svtv-spec-val.override-val-alists)) (svtv-actual-input-vars (svex-alistlist-vars svtv-spec-val.in-alists)) (svtv-actual-override-signals (svex-alistlist-all-keys svtv-spec-val.override-val-alists)) (thm-spec-override-vars (append (strip-cars svtv-thm.spec-override-var-bindings) svtv-thm.spec-override-vars)) (thm-input-vars (append (strip-cars svtv-thm.input-var-bindings) svtv-thm.input-vars)) (thm-override-vars (append (strip-cars svtv-thm.override-var-bindings) svtv-thm.override-vars)) (real-spec-override-vars (acl2::hons-intersection (append thm-input-vars thm-spec-override-vars) svtv-actual-override-vars)) (real-input-vars (acl2::hons-intersection thm-input-vars svtv-actual-input-vars)) (eliminate-all-overrides (or (eq eliminate-override-signals :all) (eq eliminate-override-vars :all))) ((unless (or eliminate-all-overrides (acl2::hons-subset eliminate-override-vars real-spec-override-vars))) (let ((missing (hons-set-diff eliminate-override-vars real-spec-override-vars))) (er hard? ctx "The ~x0 must be a subset of the theorem's spec-override-vars, but the following are not: ~x1" :eliminate-override-vars missing))) ((unless (or eliminate-all-overrides (acl2::hons-subset eliminate-override-signals svtv-actual-override-signals))) (let ((missing (hons-set-diff eliminate-override-signals svtv-actual-override-signals))) (er hard? "The ~x0 must be a subset of the SVTV's overridden signals, but the following are not: ~x1" :eliminate-override-signals missing))) (hyps (append (svtv-genthm-hyp-to-list svtv-thm.user-final-hyp) (svtv-genthm-input-binding-hyp-termlist svtv-thm.input-var-bindings) (svtv-genthm-input-binding-hyp-termlist (append svtv-thm.spec-override-var-bindings svtv-thm.override-var-bindings)) (svtv-genthm-hyp-to-list svtv-thm.final-hyp) (svtv-genthm-hyp-to-list svtv-thm.hyp))) (remaining-override-vars (and (not eliminate-all-overrides) (hons-set-diff real-spec-override-vars eliminate-override-vars))) (new-eliminated-override-vars (if eliminate-all-overrides real-spec-override-vars eliminate-override-vars)) (all-eliminated-override-vars (append thm-override-vars new-eliminated-override-vars)) (override-test-svtv-env (svtv-genthm-override-test-alist remaining-override-vars nil svtv-thm.triple-val-alist svtv-thm.triples-name)) (override-test-envs (if eliminate-all-overrides (make-list (len svtv-spec-val.override-test-alists) :initial-element nil) (with-fast-alist override-test-svtv-env (svex-envlist-1mask (svex-alistlist-eval (svtv-fsm-namemap-alistlist (svex-alistlist-removekeys eliminate-override-signals svtv-spec-val.override-test-alists) svtv-spec-val.namemap :test) override-test-svtv-env)))))) (make-svtv-to-fsm-thm :thmname thmname :svtv-spec-thmname svtv-spec-thmname :fsmname fsm :svtv svtv-thm.svtv :svtv-spec svtv-thm.svtv-spec :triples-name svtv-thm.triples-name :input-vars real-input-vars :override-vars thm-override-vars :spec-override-vars real-spec-override-vars :output-vars svtv-thm.output-vars :remaining-override-vars remaining-override-vars :new-eliminated-override-vars new-eliminated-override-vars :all-eliminated-override-vars all-eliminated-override-vars :override-test-envs override-test-envs :outmap (svtv-probealist-to-lhprobe-map svtv-spec-val.probes svtv-spec-val.namemap) :bindings (svtv-spec-fsm-bindings svtv-spec-val) :triple-val-alist svtv-thm.triple-val-alist :run-length (len (svtv-probealist-outvars svtv-spec-val.probes)) :hyp (cons 'and hyps) :concl svtv-thm.concl :rule-classes rule-classes :cycle-num-rewrite-strategy cycle-num-rewrite-strategy :base-cycle-var base-cycle-var :primary-output-var primary-output-var :pkg-sym pkg-sym))))