comparison src/mono_reduce.sml @ 601:7c3c21eb5b4c

Initial experiments with nested <dyn>
author Adam Chlipala <adamc@hcoop.net>
date Tue, 13 Jan 2009 15:17:11 -0500
parents 0094e0242100
children 330a7de47914
comparison
equal deleted inserted replaced
600:d1cce194180d 601:7c3c21eb5b4c
477 | WritePage => not writesPage andalso verifyCompatible effs 477 | WritePage => not writesPage andalso verifyCompatible effs
478 | ReadDb => not writesDb andalso verifyCompatible effs 478 | ReadDb => not writesDb andalso verifyCompatible effs
479 | WriteDb => not writesDb andalso not readsDb andalso verifyCompatible effs 479 | WriteDb => not writesDb andalso not readsDb andalso verifyCompatible effs
480 in 480 in
481 (*Print.prefaces "verifyCompatible" 481 (*Print.prefaces "verifyCompatible"
482 [("e'", MonoPrint.p_exp env e'), 482 [("e'", MonoPrint.p_exp env e'),
483 ("b", MonoPrint.p_exp (E.pushERel env x t NONE) b), 483 ("b", MonoPrint.p_exp (E.pushERel env x t NONE) b),
484 ("effs_e'", Print.p_list p_event effs_e'), 484 ("effs_e'", Print.p_list p_event effs_e'),
485 ("effs_b", Print.p_list p_event effs_b)];*) 485 ("effs_b", Print.p_list p_event effs_b)];*)
486 if List.null effs_e' orelse verifyCompatible effs_b then 486 if List.null effs_e' orelse (List.all (fn eff => eff <> Unsure) effs_e'
487 andalso verifyCompatible effs_b) then
487 trySub () 488 trySub ()
488 else 489 else
489 e 490 e
490 end 491 end
491 else 492 else