never executed always true always false

    1 {-# LANGUAGE QuasiQuotes #-}
    2 
    3 module Conjure.Rules.TildeOrdering where
    4 
    5 import Conjure.Rules.Import
    6 
    7 
    8 rule_BoolInt :: Rule
    9 rule_BoolInt = "tildeOrd-bool-int" `namedRule` theRule where
   10     theRule [essence| &x ~< &y |] = do
   11         tyx <- typeOf x
   12         tyy <- typeOf y
   13         case mostDefined [tyx, tyy] of
   14             TypeBool  -> return ()
   15             TypeInt _ -> return ()
   16             _ -> na "rule_BoolInt"
   17         return
   18             ( "~< to <"
   19             , return [essence| &x < &y |]
   20             )
   21     theRule [essence| &x ~<= &y |] = do
   22         tyx <- typeOf x
   23         tyy <- typeOf y
   24         case mostDefined [tyx, tyy] of
   25             TypeBool  -> return ()
   26             TypeInt _ -> return ()
   27             _ -> na "rule_BoolInt"
   28         return
   29             ( "~<= to <="
   30             , return [essence| &x <= &y |]
   31             )
   32     theRule _ = na "rule_BoolInt"
   33 
   34 
   35 rule_MSet :: Rule
   36 rule_MSet = "tildeLt-mset" `namedRule` theRule where
   37     theRule [essence| &x ~< &y |] = do
   38         tyX <- typeOf x
   39         tyY <- typeOf y
   40         case mostDefined [tyX, tyY] of
   41             TypeMSet{} -> return ()
   42             _ -> na "rule_MSet"
   43         return
   44             ( "mset ~<"
   45             , do
   46                 (iPat, i) <- quantifiedVar
   47                 (jPat, j) <- quantifiedVar
   48                 let z = [essence| &x union &y |]
   49                 -- there exists an i, where freq_x is smaller than freq_y
   50                 -- and all j's (s.t. j<i), freq_x = freq_y
   51                 -- i.e. all those that are smaller than the ith occur equal nb times
   52                 return [essence|
   53                     exists &iPat in &z .
   54                         freq(&x, &i) < freq(&y, &i) /\
   55                         (forAll &jPat in &z , &j ~< &i . freq(&x, &j) = freq(&y, &j))
   56                                |]
   57             )
   58     theRule _ = na "rule_MSet"
   59 
   60 
   61 rule_ViaMSet :: Rule
   62 rule_ViaMSet = "tildeLt-via-mset" `namedRule` theRule where
   63     theRule [essence| &x ~< &y |] = do
   64         tyX <- typeOf x
   65         tyY <- typeOf y
   66         f   <- case mostDefined [tyX, tyY] of
   67             TypeSet{}       -> return $ \ i ->
   68                 case match opToSetWithFlag i of
   69                     -- if i is a toSet, that doesn't contain any duplicates anyway, stip the toSet
   70                     Just (True, j) -> [essence| toMSet(&j) |]
   71                     _              -> [essence| toMSet(&i) |]
   72             TypeFunction{}  -> return $ \ i -> [essence| toMSet(&i) |]
   73             TypeRelation{}  -> return $ \ i -> [essence| toMSet(&i) |]
   74             TypePartition{} -> return $ \ i -> [essence| toMSet(parts(&i)) |]
   75             _               -> na "rule_ViaMSet"
   76         let fx = f x
   77         let fy = f y
   78         return
   79             ( "set, function, relation, partition ~<"
   80             , return [essence| &fx ~< &fy |]
   81             )
   82     theRule _ = na "rule_ViaMSet"
   83 
   84 
   85 rule_TildeLeq :: Rule
   86 rule_TildeLeq = "tildeLeq" `namedRule` theRule where
   87     theRule [essence| &x ~<= &y |] = do
   88         tyX <- typeOf x
   89         tyY <- typeOf y
   90         case mostDefined [tyX, tyY] of
   91             TypeSet{}       -> return ()
   92             TypeMSet{}      -> return ()
   93             TypeFunction{}  -> return ()
   94             TypeRelation{}  -> return ()
   95             TypePartition{} -> return ()
   96             _               -> na "rule_TildeLeq"
   97         return
   98             ( "~<= to ~<"
   99             , return [essence| or([ &x = &y
  100                                   , &x ~< &y
  101                                   ])
  102                              |]
  103             )
  104     theRule _ = na "rule_TildeLeq"