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)
--
("x" `UntilF` "y")
false
false
("x" `UntilF` "y")
()