--- /dev/null
+import "Prelude"
+
+data Formula a = TrueF
+ | FalseF
+ | XorF (Formula a) (Formula a)
+ | AndF (Formula a) (Formula a)
+ | ConditionF a
+ | NextF (Formula a)
+ | UntilF (Formula a) (Formula a)
+
+deriving instance (Ord a) => Ord (Formula a)
+
+instance (Show a) => Show (Formula a) where
+ sb <+ TrueF = sb << "true"
+ sb <+ FalseF = sb << "false"
+ sb <+ XorF a b = sb << "(" <+ a << " `XorF` " <+ b << ")"
+ sb <+ AndF a b = sb << "(" <+ a << " &&& " <+ b << ")"
+ sb <+ ConditionF c = sb <+ c
+ sb <+ NextF a = sb << "(next " <+ a << ")"
+ sb <+ UntilF a b = sb << "(" <+ a << " `UntilF` " <+ b << ")"
+
+xorF FalseF f2 = f2
+xorF f1 FalseF = f1
+xorF f1@(XorF h1 t1) f2@(XorF h2 t2) =
+ let cmp = compare h1 h2
+ in if cmp < 0
+ then XorF h1 (xorF t1 f2)
+ else if cmp > 0
+ then XorF h2 (xorF f1 t2)
+ else xorF t1 t2
+xorF f1@(XorF h1 t1) f2 =
+ let cmp = compare h1 f2
+ in if cmp < 0
+ then XorF h1 (xorF t1 f2)
+ else if cmp > 0
+ then XorF f2 f1
+ else t1
+xorF f1 f2@(XorF h2 t2) =
+ let cmp = compare f1 h2
+ in if cmp < 0
+ then XorF f1 f2
+ else if cmp > 0
+ then XorF h2 (xorF f1 t2)
+ else t2
+xorF f1 f2 =
+ let cmp = compare f1 f2
+ in if cmp < 0
+ then XorF f1 f2
+ else if cmp > 0
+ then XorF f2 f1
+ else TrueF
+
+notF f = xorF TrueF f
+
+TrueF &&& f2 = f2
+f1 &&& TrueF = f1
+FalseF &&& _ = FalseF
+_ &&& FalseF = FalseF
+XorF h1 t1 &&& f2 = xorF (h1 &&& f2) (t1 &&& f2)
+f1 &&& XorF h2 t2 = xorF (f1 &&& h2) (f1 &&& t2)
+f1@(AndF h1 t1) &&& f2@(AndF h2 t2) =
+ let cmp = compare h1 h2
+ in if cmp < 0
+ then AndF h1 (t1 &&& f2)
+ else if cmp > 0
+ then AndF h2 (f1 &&& t2)
+ else AndF h1 (t1 &&& t2)
+f1@(AndF h1 t1) &&& f2 =
+ let cmp = compare h1 f2
+ in if cmp < 0
+ then AndF h1 (t1 &&& f2)
+ else if cmp > 0
+ then AndF f2 f1
+ else f1
+f1 &&& f2@(AndF h2 t2) =
+ let cmp = compare f1 h2
+ in if cmp < 0
+ then AndF f1 f2
+ else if cmp > 0
+ then AndF h2 (f1 &&& t2)
+ else f2
+f1 &&& f2 =
+ let cmp = compare f1 f2
+ in if cmp < 0
+ then AndF f1 f2
+ else if cmp > 0
+ then AndF f2 f1
+ else f1
+
+f1 ||| f2 = xorF (xorF f1 f2) (f1 &&& f2)
+
+eval :: Ord a => (a -> <e> Boolean) -> Formula a -> <e> Formula a
+eval s TrueF = TrueF
+eval s FalseF = FalseF
+eval s (XorF f1 f2) = xorF (eval s f1) (eval s f2)
+eval s (AndF f1 f2) = eval s f1 &&& eval s f2
+eval s (ConditionF c) = if s c then TrueF else FalseF
+eval s (NextF f) = f
+eval s (UntilF f1 f2) = eval s f2 ||| (eval s f1 &&& UntilF f1 f2)
+
+// Concrete conditions
+
+data V = V String (Ref Boolean)
+
+instance Ord V where
+ compare (V a _) (V b _) = compare a b
+instance Show V where
+ sb <+ V a _ = sb <+ a
+
+cond :: String -> Ref Boolean -> Formula V
+cond name ref = ConditionF (V name ref)
+
+// Testing
+
+x = ref True
+y = ref False
+
+f = cond "x" x `UntilF` cond "y" y
+
+evalV = eval (\(V _ c) -> getRef c)
+
+main = do
+ print (evalV f)
+ x := False
+ print (evalV f)
+ y = ref True
+ print (evalV f)
+ x := True
+ print (evalV f)
+--
+()
\ No newline at end of file