tests/org.simantics.scl.compiler.tests/src/org/simantics/scl/compiler/tests/scl/Formula.scl

   1 import "Prelude"
   2
   3 data Formula a = TrueF
   4                | FalseF
   5                | XorF (Formula a) (Formula a)
   6                | AndF (Formula a) (Formula a)
   7                | ConditionF a
   8                | NextF (Formula a)
   9                | UntilF (Formula a) (Formula a)
  10
  11 deriving instance (Ord a) => Ord (Formula a)
  12
  13 instance (Show a) => Show (Formula a) where
  14     sb <+ TrueF = sb << "true"
  15     sb <+ FalseF = sb << "false"
  16     sb <+ XorF a b = sb << "(" <+ a << " `XorF` " <+ b << ")"
  17     sb <+ AndF a b = sb  << "(" <+ a << " &&& " <+ b << ")"
  18     sb <+ ConditionF c = sb  <+ c
  19     sb <+ NextF a = sb  << "(next " <+ a << ")"
  20     sb <+ UntilF a b = sb << "(" <+ a << " `UntilF` " <+ b << ")"
  21
  22 xorF FalseF f2 = f2
  23 xorF f1 FalseF = f1
  24 xorF f1@(XorF h1 t1) f2@(XorF h2 t2) =
  25     let cmp = compare h1 h2
  26     in  if cmp < 0
  27         then XorF h1 (xorF t1 f2)
  28         else if cmp > 0
  29         then XorF h2 (xorF f1 t2)
  30         else xorF t1 t2
  31 xorF f1@(XorF h1 t1) f2 =
  32     let cmp = compare h1 f2
  33     in  if cmp < 0
  34         then XorF h1 (xorF t1 f2)
  35         else if cmp > 0
  36         then XorF f2 f1
  37         else t1
  38 xorF f1 f2@(XorF h2 t2) =
  39     let cmp = compare f1 h2
  40     in  if cmp < 0
  41         then XorF f1 f2
  42         else if cmp > 0
  43         then XorF h2 (xorF f1 t2)
  44         else t2
  45 xorF f1 f2 =
  46     let cmp = compare f1 f2
  47     in  if cmp < 0
  48         then XorF f1 f2
  49         else if cmp > 0
  50         then XorF f2 f1
  51         else TrueF
  52
  53 notF f = xorF TrueF f
  54
  55 TrueF &&& f2 = f2
  56 f1 &&& TrueF = f1
  57 FalseF &&& _ = FalseF
  58 _ &&& FalseF = FalseF
  59 XorF h1 t1 &&& f2 = xorF (h1 &&& f2) (t1 &&& f2)
  60 f1 &&& XorF h2 t2 = xorF (f1 &&& h2) (f1 &&& t2)
  61 f1@(AndF h1 t1) &&& f2@(AndF h2 t2) =
  62     let cmp = compare h1 h2
  63     in  if cmp < 0
  64         then AndF h1 (t1 &&& f2)
  65         else if cmp > 0
  66         then AndF h2 (f1 &&& t2)
  67         else AndF h1 (t1 &&& t2)
  68 f1@(AndF h1 t1) &&& f2 =
  69     let cmp = compare h1 f2
  70     in  if cmp < 0
  71         then AndF h1 (t1 &&& f2)
  72         else if cmp > 0
  73         then AndF f2 f1
  74         else f1
  75 f1 &&& f2@(AndF h2 t2) =
  76     let cmp = compare f1 h2
  77     in  if cmp < 0
  78         then AndF f1 f2
  79         else if cmp > 0
  80         then AndF h2 (f1 &&& t2)
  81         else f2
  82 f1 &&& f2 =
  83     let cmp = compare f1 f2
  84     in  if cmp < 0
  85         then AndF f1 f2
  86         else if cmp > 0
  87         then AndF f2 f1
  88         else f1
  89
  90 f1 ||| f2 = xorF (xorF f1 f2) (f1 &&& f2)
  91
  92 eval :: Ord a => (a -> <e> Boolean) -> Formula a -> <e> Formula a
  93 eval s TrueF = TrueF
  94 eval s FalseF = FalseF
  95 eval s (XorF f1 f2) = xorF (eval s f1) (eval s f2)
  96 eval s (AndF f1 f2) = eval s f1 &&& eval s f2
  97 eval s (ConditionF c) = if s c then TrueF else FalseF
  98 eval s (NextF f) = f
  99 eval s (UntilF f1 f2) = eval s f2 ||| (eval s f1 &&& UntilF f1 f2)
 100
 101 // Concrete conditions
 102
 103 data V = V String (Ref Boolean)
 104
 105 instance Ord V where
 106     compare (V a _) (V b _) = compare a b
 107 instance Show V where
 108     sb <+ V a _ = sb <+ a
 109
 110 cond :: String -> Ref Boolean -> Formula V
 111 cond name ref = ConditionF (V name ref)
 112
 113 // Testing
 114
 115 x = ref True
 116 y = ref False
 117
 118 f = cond "x" x `UntilF` cond "y" y
 119
 120 evalV = eval (\(V _ c) -> getRef c)
 121
 122 main = do
 123     print (evalV f)
 124     x := False
 125     print (evalV f)
 126     y = ref True
 127     print (evalV f)
 128     x := True
 129     print (evalV f)
 130 --
 131 ("x" `UntilF` "y")
 132 false
 133 false
 134 ("x" `UntilF` "y")
 135 ()