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 () =