Check if a variable is statically well-formed.
(check-variable var ctxt) → result
The variable must be in the (variable) context. We return its contextual type. A variable never engenders any proof obligation. A variable is always single-valued.
Function:
(defun check-variable (var ctxt) (declare (xargs :guard (and (identifierp var) (contextp ctxt)))) (let ((__function__ 'check-variable)) (declare (ignorable __function__)) (b* ((var-ctxt (context->variables ctxt)) (var (identifier-fix var)) (pair? (omap::assoc var var-ctxt)) ((when (not pair?)) (type-result-err (list :variable-not-in-context var var-ctxt))) (type (cdr pair?))) (make-type-result-ok :types (list type) :obligations nil))))
Theorem:
(defthm type-resultp-of-check-variable (b* ((result (check-variable var ctxt))) (type-resultp result)) :rule-classes :rewrite)
Theorem:
(defthm check-variable-of-identifier-fix-var (equal (check-variable (identifier-fix var) ctxt) (check-variable var ctxt)))
Theorem:
(defthm check-variable-identifier-equiv-congruence-on-var (implies (identifier-equiv var var-equiv) (equal (check-variable var ctxt) (check-variable var-equiv ctxt))) :rule-classes :congruence)
Theorem:
(defthm check-variable-of-context-fix-ctxt (equal (check-variable var (context-fix ctxt)) (check-variable var ctxt)))
Theorem:
(defthm check-variable-context-equiv-congruence-on-ctxt (implies (context-equiv ctxt ctxt-equiv) (equal (check-variable var ctxt) (check-variable var ctxt-equiv))) :rule-classes :congruence)