Turn a list of typed variables into a variable context.
(typed-variables-to-variable-context tvars) → var-ctxt
We just reformat the list into a map. If there are duplicate variable names, the type of the first one in the list prevails; however, well-formed lists of typed variables have unique names.
Function:
(defun typed-variables-to-variable-context (tvars) (declare (xargs :guard (typed-variable-listp tvars))) (let ((__function__ 'typed-variables-to-variable-context)) (declare (ignorable __function__)) (cond ((endp tvars) nil) (t (omap::update (typed-variable->name (car tvars)) (typed-variable->type (car tvars)) (typed-variables-to-variable-context (cdr tvars)))))))
Theorem:
(defthm variable-contextp-of-typed-variables-to-variable-context (b* ((var-ctxt (typed-variables-to-variable-context tvars))) (variable-contextp var-ctxt)) :rule-classes :rewrite)
Theorem:
(defthm typed-variables-to-variable-context-of-typed-variable-list-fix-tvars (equal (typed-variables-to-variable-context (typed-variable-list-fix tvars)) (typed-variables-to-variable-context tvars)))
Theorem:
(defthm typed-variables-to-variable-context-typed-variable-list-equiv-congruence-on-tvars (implies (typed-variable-list-equiv tvars tvars-equiv) (equal (typed-variables-to-variable-context tvars) (typed-variables-to-variable-context tvars-equiv))) :rule-classes :congruence)