never executed always true always false

    1 {-# LANGUAGE QuasiQuotes #-}
    2 
    3 module Conjure.Rules.Vertical.Sequence.ExplicitBounded where
    4 
    5 import Conjure.Rules.Import
    6 
    7 
    8 rule_Comprehension :: Rule
    9 rule_Comprehension = "sequence-comprehension{ExplicitBounded}" `namedRule` theRule where
   10     theRule (Comprehension body gensOrConds) = do
   11         (gocBefore, (pat, sequ), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of
   12             Generator (GenInExpr pat@Single{} expr) -> return (pat, expr)
   13             _ -> na "rule_Comprehension"
   14         Sequence_ExplicitBounded <- representationOf sequ
   15         TypeSequence{}           <- typeOf sequ
   16         DomainSequence _ (SequenceAttr sizeAttr _) _ <- domainOf sequ
   17         maxSize <- case sizeAttr of
   18                     SizeAttr_Size x -> return x
   19                     SizeAttr_MaxSize x -> return x
   20                     SizeAttr_MinMaxSize _ x -> return x
   21                     _ -> failDoc "rule_Comprehension_Defined maxSize"
   22         [sLength, sValues]         <- downX1 sequ
   23         let upd val old = lambdaToFunction pat old val
   24         return
   25             ( "Mapping over a sequence, ExplicitBounded representation"
   26             , do
   27                 (iPat, i) <- quantifiedVar
   28                 let val = [essence| (&i, &sValues[&i]) |]
   29                 return $ Comprehension
   30                        (upd val body)
   31                        $  gocBefore
   32                        ++ [ Generator (GenDomainNoRepr iPat (mkDomainIntB 1 maxSize))
   33                           , Condition [essence| &i <= &sLength |]
   34                           ]
   35                        ++ transformBi (upd val) gocAfter
   36                )
   37     theRule _ = na "rule_Comprehension"
   38 
   39 
   40 rule_Card :: Rule
   41 rule_Card = "sequence-cardinality{ExplicitBounded}" `namedRule` theRule where
   42     theRule [essence| |&s| |] = do
   43         TypeSequence{}           <- typeOf s
   44         Sequence_ExplicitBounded <- representationOf s
   45         [sLength, _]             <- downX1 s
   46         return
   47             ( "Vertical rule for sequence cardinality."
   48             , return sLength
   49             )
   50     theRule _ = na "rule_Card"
   51 
   52 
   53 rule_Image_NotABool :: Rule
   54 rule_Image_NotABool = "sequence-image{ExplicitBounded}-not-a-bool" `namedRule` theRule where
   55     theRule [essence| image(&sequ,&x) |] = do
   56         Sequence_ExplicitBounded <- representationOf sequ
   57         TypeSequence tyTo        <- typeOf sequ
   58         case tyTo of
   59             TypeBool -> na "sequence of bool"
   60             _        -> return ()
   61         [sLength,sValues] <- downX1 sequ
   62         return
   63             ( "Sequence image, ExplicitBounded representation, not-a-bool"
   64             , return [essence| { &sValues[&x]
   65                                @ such that &x <= &sLength
   66                                }
   67                              |]
   68             )
   69     theRule _ = na "rule_Image_NotABool"
   70 
   71 
   72 rule_Image_Bool :: Rule
   73 rule_Image_Bool = "sequence-image{ExplicitBounded}-bool" `namedRule` theRule where
   74     theRule p = do
   75         let
   76             imageChild ch@[essence| image(&sequ,&x) |] = do
   77                 Sequence_ExplicitBounded <- representationOf sequ
   78                 TypeSequence tyTo        <- typeOf sequ
   79                 case tyTo of
   80                     TypeBool -> do
   81                         [sLength,sValues] <- downX1 sequ
   82                         tell $ return [essence| &x <= &sLength |]
   83                         return [essence| &sValues[&x] |]
   84                     _ -> return ch
   85             imageChild ch = return ch
   86         (p', flags) <- runWriterT (descendM imageChild p)
   87         case flags of
   88             [] -> na "rule_Image_Bool"
   89             _  -> do
   90                 let flagsCombined = make opAnd $ fromList flags
   91                 return
   92                     ( "Sequence image, ExplicitBounded representation, bool"
   93                     , return [essence| { &p' @ such that &flagsCombined } |]
   94                     )
   95 
   96 rule_Leq :: Rule
   97 rule_Leq = "sequence-leq{ExplicitBounded}" `namedRule` theRule where
   98     theRule [essence| &a ~<= &b |] = do
   99         TypeSequence aInnerTy    <- typeOf a
  100         TypeSequence bInnerTy    <- typeOf b
  101         unless (typeCanIndexMatrix aInnerTy && typeCanIndexMatrix bInnerTy) $ na "rule_Leq"
  102         Sequence_ExplicitBounded <- representationOf a
  103         Sequence_ExplicitBounded <- representationOf b
  104         [aLength, aValues]       <- downX1 a
  105         [bLength, bValues]       <- downX1 b
  106         return
  107             ( "Mapping over a sequence, ExplicitBounded representation"
  108             , return [essence|
  109                 flatten([&aValues, [&aLength]]) .<=
  110                 flatten([&bValues, [&bLength]])
  111                              |]
  112                )
  113     theRule _ = na "rule_Leq"
  114 
  115 
  116 rule_Lt :: Rule
  117 rule_Lt = "sequence-lt{ExplicitBounded}" `namedRule` theRule where
  118     theRule [essence| &a ~< &b |] = do
  119         TypeSequence aInnerTy    <- typeOf a
  120         TypeSequence bInnerTy    <- typeOf b
  121         unless (typeCanIndexMatrix aInnerTy && typeCanIndexMatrix bInnerTy) $ na "rule_Lt"
  122         Sequence_ExplicitBounded <- representationOf a
  123         Sequence_ExplicitBounded <- representationOf b
  124         [aLength, aValues]       <- downX1 a
  125         [bLength, bValues]       <- downX1 b
  126         return
  127             ( "Mapping over a sequence, ExplicitBounded representation"
  128             , return [essence|
  129                 flatten([&aValues, [&aLength]]) .<
  130                 flatten([&bValues, [&bLength]])
  131                              |]
  132                )
  133     theRule _ = na "rule_Lt"
  134