never executed always true always false
    1 {-# LANGUAGE QuasiQuotes #-}
    2 
    3 module Conjure.Rules.Vertical.Matrix where
    4 
    5 import Conjure.Rules.Import
    6 import Conjure.Rules.Definition ( RuleResult(..), QuestionType(..) )
    7 import Conjure.Rules.Vertical.Tuple ( decomposeLexLt, decomposeLexLeq  )
    8 
    9 -- uniplate
   10 import Data.Generics.Uniplate.Zipper ( hole )
   11 import Data.Generics.Uniplate.Zipper as Zipper ( up )
   12 
   13 
   14 rule_Comprehension_Literal :: Rule
   15 rule_Comprehension_Literal = Rule "matrix-comprehension-literal" theRule where
   16     theRule z (Comprehension body gensOrConds) = do
   17         (gocBefore, (pat, expr), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of
   18             Generator (GenInExpr pat expr) -> return (pat, expr)
   19             _ -> na "rule_Comprehension_Literal"
   20         (_, _index, elems) <- match matrixLiteral expr
   21         notInsideMinMax z
   22         tyInner <- typeOf body
   23         let ty = TypeMatrix (TypeInt TagInt) tyInner
   24         return
   25             [ RuleResult
   26                 { ruleResultDescr = "Vertical rule for matrix-comprehension on matrix literal"
   27                 , ruleResultType  = ExpressionRefinement
   28                 , ruleResultHook  = Nothing
   29                 , ruleResult      = return $
   30                     case elems of
   31                         []   -> make matrixLiteral ty (mkDomainIntB 1 0) []
   32                         [el] -> Comprehension body
   33                                     $  gocBefore
   34                                     ++ [ComprehensionLetting pat el]
   35                                     ++ gocAfter
   36                         _    -> make opConcatenate $ AbstractLiteral $ AbsLitMatrix
   37                                     (mkDomainIntB 1 (fromInt $ genericLength elems))
   38                                     [ Comprehension body
   39                                         $  gocBefore
   40                                         ++ [ComprehensionLetting pat el]
   41                                         ++ gocAfter
   42                                     | el <- elems
   43                                     ]
   44                 } ]
   45     theRule _ _ = na "rule_Comprehension_Literal"
   46 
   47     notInsideMinMax z0 =
   48         case Zipper.up z0 of
   49             Nothing -> na "rule_Comprehension_Literal 1"
   50             Just z1 -> do
   51                 let h = hole z1
   52                 case match opReducer h of
   53                     Just (_, False, _, _) -> na "rule_Comprehension_Literal"
   54                     Just (_, True , _, _) -> return ()
   55                     Nothing               -> case Zipper.up z1 of
   56                                                 Nothing -> return ()
   57                                                 Just u  -> notInsideMinMax u
   58 
   59 
   60 rule_Comprehension :: Rule
   61 rule_Comprehension = "matrix-comprehension" `namedRule` theRule where
   62     theRule (Comprehension body gensOrConds) = do
   63         (gocBefore, (pat, expr), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of
   64             Generator (GenInExpr pat expr) -> return (pat, expr)
   65             _ -> na "rule_Comprehension"
   66         case match matrixLiteral expr of
   67             Just{} -> na "rule_Comprehension" -- this case is handled in rule_Comprehension_Literal
   68             Nothing -> return ()
   69         indexDom:_ <- indexDomainsOf expr
   70         case indexDom of
   71             DomainAny{} -> na "rule_Comprehension"
   72             DomainInt _ [RangeLowerBounded _] -> na "rule_Comprehension"
   73             _ -> return ()
   74         return
   75             ( "Comprehension on a matrix"
   76             , do
   77                 (iPat, i) <- quantifiedVar
   78                 return $ Comprehension body
   79                             $ gocBefore
   80                             ++ [ Generator (GenDomainNoRepr iPat indexDom)
   81                                , ComprehensionLetting pat [essence| &expr[&i] |]
   82                                ]
   83                             ++ gocAfter
   84             )
   85     theRule _ = na "rule_Comprehension"
   86 
   87 
   88 rule_Comprehension_Flatten :: Rule
   89 rule_Comprehension_Flatten = "matrix-comprehension-flatten" `namedRule` theRule where
   90     theRule (Comprehension body gensOrConds) = do
   91         (gocBefore, (pat, expr), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of
   92             Generator (GenInExpr pat expr) -> return (pat, expr)
   93             _ -> na "rule_Comprehension_Flatten"
   94         m <- match opFlatten expr
   95         indexDoms <- indexDomainsOf m
   96         forM_ indexDoms $ \case
   97             DomainAny{} -> na "rule_Comprehension_Flatten"
   98             _ -> return ()
   99         when (null indexDoms) $ na "rule_Comprehension_Flatten"
  100         return
  101             ( "Comprehension on a matrix flatten"
  102             , do
  103                 (gens, is) <- unzip <$> sequence
  104                                 [ do
  105                                     (iPat, i) <- quantifiedVar
  106                                     return (Generator (GenDomainNoRepr iPat d), i)
  107                                 | d <- indexDoms
  108                                 ]
  109                 return $ Comprehension body
  110                             $  gocBefore
  111                             ++ gens
  112                             ++ [ ComprehensionLetting pat (make opMatrixIndexing m is) ]
  113                             ++ gocAfter
  114             )
  115     theRule _ = na "rule_Comprehension_Flatten"
  116 
  117 
  118 -- | input:  [ i | i <- m[j] ] with m = [a,b,c]
  119 --   output: [ [ i | i <- a ]
  120 --           , [ i | i <- b ]
  121 --           , [ i | i <- c ]
  122 --           ][j]
  123 --   namely: [ [ m[k]
  124 --             | k : int(1..3)
  125 --             ]
  126 --           , [ i | i <- b ]
  127 --           , [ i | i <- c ]
  128 --           ][j]
  129 
  130 rule_ModifierAroundIndexedMatrixLiteral :: Rule
  131 rule_ModifierAroundIndexedMatrixLiteral = "modifier-around-indexed-matrix-literal" `namedRule` theRule where
  132     theRule p = do
  133         (mkM, p2)         <- match opModifier p
  134         (matrix, indices) <- match opMatrixIndexing p2
  135         case match opMatrixIndexing p of
  136             Nothing -> return ()
  137             Just{}  -> na "rule_ModifierAroundIndexedMatrixLiteral, no modifier"
  138         let
  139             fullyMatrixLiteral 0 _ = return True
  140             fullyMatrixLiteral n m =
  141                 case match matrixLiteral m of
  142                     Nothing            -> return False
  143                     Just (_, _, elems) -> and <$> mapM (fullyMatrixLiteral (n-1)) elems
  144         True <- fullyMatrixLiteral (length indices) matrix
  145         return
  146             ( "Pushing a modifier inwards, through a matrix literal"
  147             , do
  148                 matrix' <- onMatrixLiteral Nothing (return . mkM) matrix
  149                 return $ make opMatrixIndexing matrix' indices
  150             )
  151 
  152 
  153 rule_Comprehension_LiteralIndexed :: Rule
  154 rule_Comprehension_LiteralIndexed = "matrix-comprehension-literal-indexed" `namedRule` theRule where
  155     theRule (Comprehension body gensOrConds) = do
  156         (gocBefore, (pat, expr), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of
  157             Generator (GenInExpr pat@Single{} expr) -> return (pat, expr)
  158             _ -> na "rule_Comprehension_LiteralIndexed"
  159         tyExpr             <- typeOf expr
  160         (matrix, indices)  <- match opMatrixIndexing expr
  161         (_, _index, elems) <- match matrixLiteral matrix
  162         return
  163             ( "Vertical rule for matrix-comprehension on matrix literal"
  164             , case indices of
  165                 [] -> bug "rule_Comprehension_LiteralIndexed indices=[]"
  166                 [index] ->
  167                     return $ make opFlatten $ AbstractLiteral $ AbsLitMatrix
  168                         (mkDomainIntB 1 (fromInt $ genericLength elems))
  169                         [ Comprehension body
  170                             $  gocBefore
  171                             ++ [ Generator (GenInExpr pat el)
  172                                , Condition [essence| &num = &index |]
  173                                ]
  174                             ++ gocAfter
  175                         | (num', el') <- zip [1..] elems
  176                         , let num = fromInt num'
  177                         -- let's not lose the type information for empty collections
  178                         , let el = if emptyCollectionX el'
  179                                     then case el' of Typed{} -> el'
  180                                                      _       -> Typed el' tyExpr
  181                                     else el'
  182                         ]
  183                 (index:rest) ->
  184                     return $ make opFlatten $ AbstractLiteral $ AbsLitMatrix
  185                         (mkDomainIntB 1 (fromInt $ genericLength elems))
  186                         [ Comprehension body
  187                             $  gocBefore
  188                             ++ [ Generator (GenInExpr pat (make opMatrixIndexing el rest))
  189                                , Condition [essence| &num = &index |]
  190                                ]
  191                             ++ gocAfter
  192                         | (num', el') <- zip [1..] elems
  193                         , let num = fromInt num'
  194                         -- let's not lose the type information for empty collections
  195                         , let el = if emptyCollectionX el'
  196                                     then case el' of Typed{} -> el'
  197                                                      _       -> Typed el' tyExpr
  198                                     else el'
  199                         ]
  200             )
  201     theRule _ = na "rule_Comprehension_LiteralIndexed"
  202 
  203 
  204 rule_Comprehension_ToSet_Matrix :: Rule
  205 rule_Comprehension_ToSet_Matrix = "matrix-toSet-matrixInside" `namedRule` theRule where
  206     theRule (Comprehension body gensOrConds) = do
  207         (gocBefore, (pat, expr), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of
  208             Generator (GenInExpr pat@Single{} expr) -> return (pat, expr)
  209             _ -> na "rule_Comprehension_ToSet"
  210         matrix       <- match opToSet expr
  211         TypeMatrix{} <- typeOf matrix
  212         let upd val old = lambdaToFunction pat old val
  213         return
  214             ( "Vertical rule for comprehension over matrix-toSet, matrix inside"
  215             , do
  216                  (iPat, i) <- quantifiedVar
  217                  let val  = make opIndexing i 1
  218                  let over = make opHist matrix
  219                  return $ Comprehension (upd val body)
  220                          $  gocBefore
  221                          ++ [Generator (GenInExpr iPat over)]
  222                          ++ transformBi (upd val) gocAfter
  223             )
  224     theRule _ = na "rule_Comprehension_ToSet"
  225 
  226 
  227 rule_Comprehension_ToSet_List :: Rule
  228 rule_Comprehension_ToSet_List = "matrix-toSet-listInside" `namedRule` theRule where
  229     theRule p = do
  230         -- we cannot assume that the list is duplicate-free
  231         (False, Comprehension body gensOrConds) <- match opToSetWithFlag p
  232         bodyDomain <- domainOf body
  233         let auxDomain = DomainSet () (SetAttr SizeAttr_None) bodyDomain
  234         return
  235             ( "Vertical rule for comprehension over matrix-toSet, list inside"
  236             , do
  237                 (auxName, aux) <- auxiliaryVar
  238                 (iPat, i) <- quantifiedVar
  239                 return $ WithLocals aux $
  240                     AuxiliaryVars
  241                         [ Declaration (FindOrGiven LocalFind auxName auxDomain)
  242                         , SuchThat
  243                             -- forAll i in list . i in aux
  244                             [ make opAnd $ Comprehension
  245                                 [essence| &body in &aux |]
  246                                 gensOrConds
  247                             -- forAll i in aux . exists j in list . i = j
  248                             , make opAnd $ Comprehension
  249                                 (make opOr (Comprehension [essence| &i = &body |] gensOrConds))
  250                                 [Generator (GenInExpr iPat aux)]
  251                             ]
  252                         ]
  253             )
  254 
  255 
  256 rule_Comprehension_ToSet_List_DuplicateFree :: Rule
  257 rule_Comprehension_ToSet_List_DuplicateFree = "matrix-toSet-listInside-nodups" `namedRule` theRule where
  258     theRule (Comprehension body gensOrConds) = do
  259         (gocBefore, (pat, expr), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of
  260             Generator (GenInExpr pat@Single{} expr) -> return (pat, matchDefs [opToMSet] expr)
  261             _ -> na "rule_Comprehension_ToSet"
  262         -- we *can* assume that the list is duplicate-free!
  263         (True, list) <- match opToSetWithFlag expr
  264         TypeList{} <- typeOf list
  265         return
  266             ( "Vertical rule for comprehension over matrix-toSet, list inside, assumed no duplicates"
  267             , return $ Comprehension body
  268                      $  gocBefore
  269                      ++ [Generator (GenInExpr pat list)]
  270                      ++ gocAfter
  271             )
  272     theRule _ = na "rule_Comprehension_ToSet_List_DuplicateFree"
  273 
  274 
  275 -- [ i | ... , i <- [ j | ... j ... ], ... i ... ]
  276 -- [ j | ... , ... j ..., ... j ... ]
  277 rule_Comprehension_Nested :: Rule
  278 rule_Comprehension_Nested = "matrix-comprehension-nested" `namedRule` theRule where
  279     theRule (Comprehension body gensOrConds) = do
  280         (gocBefore, (pat, expr), gocAfter) <- matchFirst gensOrConds $ \case
  281             Generator (GenInExpr pat@Single{} expr) -> return (pat, matchDefs [opToMSet] expr)
  282             _ -> na "rule_Comprehension_Nested"
  283         let
  284             extract (isAlias -> Just x) = extract x
  285             extract (Comprehension innerBody innerGocs) = return (innerBody, innerGocs)
  286             extract _ = na "rule_Comprehension_Nested"
  287         (innerBody, innerGocs) <- extract expr
  288         let upd val old = lambdaToFunction pat old val
  289         let
  290             -- update the quantified variable names inside innerBody&innerGocs_ here,
  291             -- because they may be shadowed.
  292             updateQuantified innerBody_ innerGocs_ = do
  293                 let olds = concatMap collectOldQuantifiers innerGocs_
  294                 if null olds
  295                     then return (innerBody_, innerGocs_)
  296                     else do
  297                         oldnews <- forM olds $ \ old -> do
  298                             (Single new, _) <- quantifiedVar
  299                             return (old, new)
  300                         let
  301                             f :: Name -> Name
  302                             f nm = fromMaybe nm (lookup nm oldnews)
  303                         return (transformBi f (innerBody_, innerGocs_))
  304 
  305             collectOldQuantifiers = \case
  306                 Generator (GenDomainNoRepr  pt _) -> universeBi pt
  307                 Generator (GenDomainHasRepr nm _) -> [nm]
  308                 Generator (GenInExpr        pt _) -> universeBi pt
  309                 Condition _                       -> []
  310                 ComprehensionLetting pt _         -> universeBi pt
  311 
  312         (innerBody', innerGocs') <- updateQuantified innerBody innerGocs
  313         return
  314             ( "Nested matrix comprehension"
  315             , return $ Comprehension (upd innerBody' body)
  316                          $  gocBefore
  317                          ++ innerGocs'
  318                          ++ transformBi (upd innerBody') gocAfter
  319             )
  320     theRule _ = na "rule_Comprehension_Nested"
  321 
  322 
  323 rule_Comprehension_Hist :: Rule
  324 rule_Comprehension_Hist = "matrix-hist" `namedRule` theRule where
  325     theRule (Comprehension body gensOrConds) = do
  326         (gocBefore, (pat, expr), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of
  327             Generator (GenInExpr pat@Single{} expr) -> return (pat, expr)
  328             _ -> na "rule_Comprehension_Hist"
  329         matrix               <- match opHist expr
  330         TypeMatrix{}         <- typeOf matrix
  331         index:_              <- indexDomainsOf matrix
  332         let upd val old = lambdaToFunction pat old val
  333         return
  334             ( "Vertical rule for comprehension over matrix-hist"
  335             , do
  336                  (iPat, i) <- quantifiedVar
  337                  (jPat, j) <- quantifiedVar
  338                  let value = [essence| &matrix[&i] |]
  339                      -- if this is the left-most occurrence of value
  340                      -- count all
  341                      -- otherwise, 0
  342                      count = [essence|
  343                          sum([ 1                            $ number of occurrences of this value in the matrix
  344                              | &jPat : &index
  345                              , &matrix[&i] = &matrix[&j]
  346                              ])
  347                      |]
  348                      val   = AbstractLiteral $ AbsLitTuple [value, count]
  349                      appearsBefore = [essence|
  350                          or([ &matrix[&j] = &matrix[&i]
  351                             | &jPat : &index
  352                             , &j < &i
  353                             ])
  354                     |]
  355                  return $ Comprehension (upd val body)
  356                          $  gocBefore
  357                          ++ [ Generator (GenDomainNoRepr iPat index)
  358                             , Condition [essence| ! &appearsBefore |]
  359                             ]
  360                          ++ transformBi (upd val) gocAfter
  361             )
  362     theRule _ = na "rule_Comprehension_Hist"
  363 
  364 
  365 rule_Matrix_Eq :: Rule
  366 rule_Matrix_Eq = "matrix-eq" `namedRule` theRule where
  367     theRule p = do
  368         (x,y)                 <- match opEq p
  369         TypeMatrix{}          <- typeOf x        -- TODO: check if x and y have the same arity
  370         TypeMatrix{}          <- typeOf y
  371         indexX:_              <- indexDomainsOf x
  372         indexY:_              <- indexDomainsOf y
  373         return
  374             ( "Horizontal rule for matrix ="
  375             , do
  376                  (iPat, i) <- quantifiedVar
  377                  (jPat, j) <- quantifiedVar
  378                  -- avoid generating the index equality constraint, if the indices are literally the same
  379                  if indexX == indexY
  380                      then
  381                          return [essence|
  382                              (forAll &iPat : &indexX . &x[&i] = &y[&i])
  383                                         |]
  384                     else
  385                          return [essence|
  386                              (forAll &iPat : &indexX . &x[&i] = &y[&i])
  387                              /\
  388                              (forAll &iPat : &indexX . exists &jPat : &indexY . &i = &j)
  389                              /\
  390                              (forAll &iPat : &indexY . exists &jPat : &indexX . &i = &j)
  391                                         |]
  392             )
  393 
  394 
  395 rule_Matrix_Neq :: Rule
  396 rule_Matrix_Neq = "matrix-neq" `namedRule` theRule where
  397     theRule p = do
  398         (x,y)                 <- match opNeq p
  399         TypeMatrix{}          <- typeOf x        -- TODO: check if x and y have the same arity
  400         TypeMatrix{}          <- typeOf y
  401         indexX:_              <- indexDomainsOf x
  402         indexY:_              <- indexDomainsOf y
  403         return
  404             ( "Horizontal rule for matrix !="
  405             , do
  406                  (iPat, i) <- quantifiedVar
  407                  return [essence|
  408                      (exists &iPat : &indexX . &x[&i] != &y[&i])
  409                      \/
  410                      (exists &iPat : &indexY . &x[&i] != &y[&i])
  411                                 |]
  412             )
  413 
  414 
  415 rule_Matrix_Lt_Primitive :: Rule
  416 rule_Matrix_Lt_Primitive = "matrix-Lt-primitive" `namedRule` theRule where
  417     theRule p = do
  418         (x,y)           <- case (match opLt p, match opTildeLt p) of
  419                                 (Just a, _) -> return a
  420                                 (_, Just a) -> return a
  421                                 _ -> na "rule_Matrix_Lt_Primitive"
  422         tx <- typeOf x        -- TODO: check if x and y have the same arity
  423         ty <- typeOf y
  424         unless (matrixNumDims tx > 0 && isPrimitiveType tx) $ failDoc ("not a primitive type:" <+> pretty tx)
  425         unless (matrixNumDims ty > 0 && isPrimitiveType ty) $ failDoc ("not a primitive type:" <+> pretty ty)
  426         let x' = flattenIfNeeded (matrixNumDims tx) x
  427         let y' = flattenIfNeeded (matrixNumDims ty) y
  428         return
  429             ( "Horizontal rule for matrix <"
  430             , return [essence| &x' .< &y' |]
  431             )
  432 
  433 
  434 rule_Matrix_Leq_Primitive :: Rule
  435 rule_Matrix_Leq_Primitive = "matrix-Leq-primitive" `namedRule` theRule where
  436     theRule p = do
  437         (x,y)           <- case (match opLeq p, match opTildeLeq p) of
  438                                 (Just a, _) -> return a
  439                                 (_, Just a) -> return a
  440                                 _ -> na "rule_Matrix_Leq_Primitive"
  441         tx <- typeOf x        -- TODO: check if x and y have the same arity
  442         ty <- typeOf y
  443         unless (matrixNumDims tx > 0 && isPrimitiveType tx) $ failDoc ("not a primitive type:" <+> pretty tx)
  444         unless (matrixNumDims ty > 0 && isPrimitiveType ty) $ failDoc ("not a primitive type:" <+> pretty ty)
  445         let x' = flattenIfNeeded (matrixNumDims tx) x
  446         let y' = flattenIfNeeded (matrixNumDims ty) y
  447         return
  448             ( "Horizontal rule for matrix <="
  449             , return [essence| &x' .<= &y' |]
  450             )
  451 
  452 
  453 rule_Matrix_Lt_Decompose :: Rule
  454 rule_Matrix_Lt_Decompose = "matrix-Lt-tuple" `namedRule` theRule where
  455     theRule p = do
  456         (x,y)           <- match opLt p
  457         tx@TypeMatrix{} <- typeOf x     -- TODO: check matrix index & tuple arity
  458         ty@TypeMatrix{} <- typeOf y
  459         when (isPrimitiveType tx) $ failDoc ("this is a primitive type:" <+> pretty tx)
  460         when (isPrimitiveType ty) $ failDoc ("this is a primitive type:" <+> pretty ty)
  461         xs              <- downX1 x
  462         ys              <- downX1 y
  463         return
  464             ( "Horizontal rule for matrix <, decomposing"
  465             , return $ decomposeLexLt p xs ys
  466             )
  467 
  468 
  469 rule_Matrix_Leq_Decompose :: Rule
  470 rule_Matrix_Leq_Decompose = "matrix-Leq-tuple" `namedRule` theRule where
  471     theRule p = do
  472         (x,y)           <- match opLeq p
  473         tx@TypeMatrix{} <- typeOf x     -- TODO: check matrix index & tuple arity
  474         ty@TypeMatrix{} <- typeOf y
  475         when (isPrimitiveType tx) $ failDoc ("this is a primitive type:" <+> pretty tx)
  476         when (isPrimitiveType ty) $ failDoc ("this is a primitive type:" <+> pretty ty)
  477         xs              <- downX1 x
  478         ys              <- downX1 y
  479         return
  480             ( "Horizontal rule for matrix <=, decomposing"
  481             , return $ decomposeLexLeq p xs ys
  482             )
  483 
  484 
  485 rule_Comprehension_SingletonDomain :: Rule
  486 rule_Comprehension_SingletonDomain = "matrix-comprehension-singleton-domain" `namedRule` theRule where
  487     theRule (Comprehension body gensOrConds) = do
  488         (gocBefore, (pat, singleVal), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of
  489             Generator (GenDomainHasRepr patName (singletonDomainInt -> Just a)) -> return (Single patName, a)
  490             _ -> na "rule_Comprehension_SingletonDomain"
  491         let upd val old = lambdaToFunction pat old val
  492         return
  493             ( "Removing matrix-comprehension of a singleton int domain"
  494             , return $
  495                 if null gocBefore && null gocAfter
  496                     then AbstractLiteral $ AbsLitMatrix (mkDomainIntB 1 1) [upd singleVal body]
  497                     else Comprehension (upd singleVal body)
  498                          $  gocBefore
  499                          ++ transformBi (upd singleVal) gocAfter
  500             )
  501     theRule _ = na "rule_Comprehension_SingletonDomain"
  502 
  503 
  504 rule_Comprehension_Singleton :: Rule
  505 rule_Comprehension_Singleton = "matrix-comprehension-singleton" `namedRule` theRule where
  506     theRule p = do
  507         (_, _, _mkQuan, AbstractLiteral (AbsLitMatrix _ [singleVal])) <- match opReducer p
  508         return
  509             ( "Removing quantifier of a single item"
  510             , return singleVal
  511             )
  512 
  513 
  514 rule_Concatenate_Singleton :: Rule
  515 rule_Concatenate_Singleton = "matrix-concatenate-singleton" `namedRule` theRule where
  516     theRule p = do
  517         AbstractLiteral (AbsLitMatrix _ [singleVal]) <- match opConcatenate p
  518         return
  519             ( "Removing concatenate of a single item"
  520             , return singleVal
  521             )
  522 
  523 
  524 rule_MatrixIndexing :: Rule
  525 rule_MatrixIndexing = "matrix-indexing" `namedRule` theRule where
  526     theRule p = do
  527         (matrix, indexer)              <- match opIndexing p
  528         (_, DomainInt _ ranges, elems) <- match matrixLiteral matrix
  529         indexInts                      <- rangesInts ranges
  530         indexerInt                     <- intOut "rule_MatrixIndexing" indexer
  531         if length indexInts == length elems
  532             then
  533                 case lookup indexerInt (zip indexInts elems) of
  534                     Nothing -> na "rule_MatrixIndexing"
  535                     Just v  ->
  536                         return
  537                             ( "Matrix indexing"
  538                             , return v
  539                             )
  540             else na "rule_MatrixIndexing"
  541 
  542 
  543 rule_IndexingIdentical :: Rule
  544 rule_IndexingIdentical = "matrix-indexing-identical" `namedRule` theRule where
  545     theRule p = do
  546         (matrix, indexer)                     <- match opIndexing p
  547         (_, indexDomain, firstElem:restElems) <- match matrixLiteral matrix
  548         indexerDomain <- domainOf indexer
  549         if indexDomain == forgetRepr indexerDomain && all (firstElem==) restElems
  550             then return
  551                     ( "rule_IndexingIdentical"
  552                     , return firstElem
  553                     )
  554             else na "rule_IndexingIdentical"
  555 
  556 
  557 rule_ExpandSlices :: Rule
  558 rule_ExpandSlices = "matrix-expand-slices" `namedRule` theRule where
  559     theRule p = do
  560         (m, is) <- match opMatrixIndexingSlicing p
  561         indexDoms <- indexDomainsOf m
  562         unless (length is == length indexDoms) $ na "rule_ExpandSlices"
  563         (is', gocs) <- unzip <$> sequence
  564             [ case index of
  565                 Left i -> -- indexing
  566                     return
  567                         ( Left i
  568                         , []
  569                         )
  570                 Right (mLowerBound, mUpperBound) -> do -- slicing
  571                     (jPat, j) <- quantifiedVar
  572                     return
  573                         ( Left j
  574                         , concat [ [ Generator (GenDomainNoRepr jPat indexDom) ]
  575                                  , [ Condition [essence| &j >= &lb |] | Just lb <- [mLowerBound] ]
  576                                  , [ Condition [essence| &j <= &ub |] | Just ub <- [mUpperBound] ]
  577                                  ]
  578                         )
  579             | (index, indexDom) <- zip is indexDoms
  580             ]
  581         when (null gocs) $ na "rule_ExpandSlices: this was all indexing and no slicing"
  582         return ( "Expanding a matrix slice"
  583                , return $ Comprehension (make opMatrixIndexingSlicing m is') (concat gocs)
  584                )
  585 
  586 
  587 -- freq(matrix,arg) ~~> sum([ toInt(arg = i) | i in matrix ])
  588 rule_Freq :: Rule
  589 rule_Freq = "matrix-freq" `namedRule` theRule where
  590     theRule p = do
  591         (m, arg) <- match opFreq p
  592         TypeMatrix{}  <- typeOf m
  593         [indexDom] <- indexDomainsOf m
  594         return
  595             ( "Horizontal rule for matrix-freq."
  596             , do
  597                 (iPat, i) <- quantifiedVar
  598                 let mis = (make opMatrixIndexing m [i])
  599                 return $ make opSum $ Comprehension [essence| toInt(&mis = &arg) |]
  600                             [Generator (GenDomainNoRepr iPat indexDom)]
  601             )
  602