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                 (kPat, k) <- quantifiedVar
   49                 -- A first differing value with freq_x < freq_y must occur in y.
   50                 -- Check earlier values in x and y separately: duplicates do not
   51                 -- affect universal quantification, so no multiset union is needed.
   52                 return [essence|
   53                     exists &iPat in &y .
   54                         freq(&x, &i) < freq(&y, &i) /\
   55                         (forAll &jPat in &x , &j ~< &i . freq(&x, &j) = freq(&y, &j)) /\
   56                         (forAll &kPat in &y , &k ~< &i . freq(&x, &k) = freq(&y, &k))
   57                                |]
   58             )
   59     theRule _ = na "rule_MSet"
   60 
   61 
   62 rule_ViaMSet :: Rule
   63 rule_ViaMSet = "tildeLt-via-mset" `namedRule` theRule where
   64     theRule [essence| &x ~< &y |] = do
   65         tyX <- typeOf x
   66         tyY <- typeOf y
   67         f   <- case mostDefined [tyX, tyY] of
   68             TypeSet{}       -> return $ \ i ->
   69                 case match opToSetWithFlag i of
   70                     -- if i is a toSet, that doesn't contain any duplicates anyway, stip the toSet
   71                     Just (True, j) -> [essence| toMSet(&j) |]
   72                     _              -> [essence| toMSet(&i) |]
   73             TypeFunction{}  -> return $ \ i -> [essence| toMSet(&i) |]
   74             TypeRelation{}  -> return $ \ i -> [essence| toMSet(&i) |]
   75             TypePartition{} -> return $ \ i -> [essence| toMSet(parts(&i)) |]
   76             _               -> na "rule_ViaMSet"
   77         let fx = f x
   78         let fy = f y
   79         return
   80             ( "set, function, relation, partition ~<"
   81             , return [essence| &fx ~< &fy |]
   82             )
   83     theRule _ = na "rule_ViaMSet"
   84 
   85 
   86 rule_TildeLeq :: Rule
   87 rule_TildeLeq = "tildeLeq" `namedRule` theRule where
   88     theRule [essence| &x ~<= &y |] = do
   89         tyX <- typeOf x
   90         tyY <- typeOf y
   91         case mostDefined [tyX, tyY] of
   92             TypeSet{}       -> return ()
   93             TypeMSet{}      -> return ()
   94             TypeFunction{}  -> return ()
   95             TypeRelation{}  -> return ()
   96             TypePartition{} -> return ()
   97             _               -> na "rule_TildeLeq"
   98         return
   99             ( "~<= to ~<"
  100             , return [essence| or([ &x = &y
  101                                   , &x ~< &y
  102                                   ])
  103                              |]
  104             )
  105     theRule _ = na "rule_TildeLeq"