Created
March 28, 2012 18:04
-
-
Save lkuper/2228832 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
;; given a store loc l and two stores S_1 and S_2, return the lub of | |
;; S_1(l) and S_2(l). We know that every l this function gets is | |
;; going to be in the domain of either S_1 or S_2 or both. | |
(define-metafunction lambdapar | |
lubstore-helper : S S l -> D | |
[(lubstore-helper S_1 S_2 l) | |
,(let ([d_1 (term (store-lookup S_1 l))] | |
[d_2 (term (store-lookup S_2 l))]) | |
(cond | |
[(equal? d_1 (term lookupfailed)) d_2] | |
[(equal? d_2 (term lookupfailed)) d_1] | |
[else (term (lub ,d_1 ,d_2))]))]) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment