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