Mercurial > urweb
comparison src/iflow.sml @ 1205:7cd11380cdf1
WHERE-dependent checking
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sun, 04 Apr 2010 17:18:41 -0400 |
parents | 7af5e2af64f4 |
children | 772760df4c4c |
comparison
equal
deleted
inserted
replaced
1204:7af5e2af64f4 | 1205:7cd11380cdf1 |
---|---|
506 if v' = v then | 506 if v' = v then |
507 (f, Proj (Proj (Lvar rv, v), f)) :: fs | 507 (f, Proj (Proj (Lvar rv, v), f)) :: fs |
508 else | 508 else |
509 fs) [] (#Select r))]))) | 509 fs) [] (#Select r))]))) |
510 True (#From r) | 510 True (#From r) |
511 | |
512 fun expIn e = | |
513 case e of | |
514 Field (v, f) => inl (Proj (Proj (Lvar rv, v), f)) | |
515 | Binop (bo, e1, e2) => | |
516 (case (expIn e1, expIn e2) of | |
517 (inr _, _) => inr Unknown | |
518 | (_, inr _) => inr Unknown | |
519 | (inl e1, inl e2) => | |
520 let | |
521 val bo = case bo of | |
522 "=" => SOME Eq | |
523 | _ => NONE | |
524 in | |
525 case bo of | |
526 NONE => inr Unknown | |
527 | SOME bo => inr (Reln (bo, [e1, e2])) | |
528 end) | |
529 | |
530 val p = case #Where r of | |
531 NONE => p | |
532 | SOME e => | |
533 case expIn e of | |
534 inr p' => And (p, p') | |
535 | _ => p | |
511 in | 536 in |
512 case oe of | 537 case oe of |
513 NONE => p | 538 NONE => p |
514 | SOME oe => | 539 | SOME oe => |
515 And (p, | 540 And (p, foldl (fn ((v, f), p) => |
516 foldl (fn ((v, f), p) => | 541 Or (p, |
517 Or (p, | 542 Reln (Eq, [oe, Proj (Proj (Lvar rv, v), f)]))) |
518 Reln (Eq, [oe, Proj (Proj (Lvar rv, v), f)]))) | 543 False (#Select r)) |
519 False (#Select r)) | |
520 end | 544 end |
521 | 545 |
522 fun evalExp env (e as (_, loc), st as (nv, p, sent)) = | 546 fun evalExp env (e as (_, loc), st as (nv, p, sent)) = |
523 let | 547 let |
524 fun default () = | 548 fun default () = |