Parse-svtv-to-fsm-thm
- Signature
(parse-svtv-to-fsm-thm thmname args state) → thmobj
Definitions and Theorems
Function: parse-svtv-to-fsm-thm
(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))))
