diff --git a/transformations/ArrayUsageCheck.hs b/transformations/ArrayUsageCheck.hs index 75007de..d212b2c 100644 --- a/transformations/ArrayUsageCheck.hs +++ b/transformations/ArrayUsageCheck.hs @@ -33,6 +33,7 @@ import FlowGraph import Metadata import Omega import Pass +import ShowCode import Types import UsageCheck import Utils @@ -92,11 +93,21 @@ checkArrayUsage graph = sequence_ $ checkPar checkArrayUsage' graph Left err -> dieP m $ "Could not work with array indexes for array \"" ++ userArrName ++ "\": " ++ err Right [] -> return () -- No problems to work with Right problems -> - case mapMaybe (\(vm,p) -> seqPair (return vm,uncurry solveProblem p)) problems of + case mapMaybe solve problems of -- No solutions; no worries! [] -> return () - ((varMapping,vm):_) -> do sol <- formatSolution varMapping (getCounterEqs vm) - dieP m $ "Overlapping indexes of array \"" ++ userArrName ++ "\" when: " ++ sol + (((lx,ly),varMapping,vm):_) -> + do sol <- formatSolution varMapping (getCounterEqs vm) + cx <- showCode lx + cy <- showCode ly + dieP m $ "Overlapping indexes of array \"" ++ userArrName ++ "\"" + ++ "(\"" ++ cx ++ "\" could overlap with \"" ++ cy ++ "\")" + ++ " when: " ++ sol + + solve :: (labels,vm,(EqualityProblem,InequalityProblem)) -> Maybe (labels,vm,VariableMapping) + solve (ls,vm,(eq,ineq)) = case solveProblem eq ineq of + Nothing -> Nothing + Just vm' -> Just (ls,vm,vm') formatSolution :: VarMap -> Map.Map CoeffIndex Integer -> m String formatSolution varToIndex indexToConst = do names <- mapM valOfVar $ Map.assocs varToIndex @@ -170,10 +181,10 @@ onlyConst _ = Nothing -- With a Replicated, each item in the left branch can be paired with each item in the right branch. -- Each item in the left branch can be paired with each other, and each item in the left branch can -- be paired with all other items. -data ArrayAccess = - Single (ArrayAccessType, (EqualityConstraintEquation, EqualityProblem, InequalityProblem)) - | Group [(ArrayAccessType, (EqualityConstraintEquation, EqualityProblem, InequalityProblem))] - | Replicated [ArrayAccess] [ArrayAccess] +data ArrayAccess label = + Single (label, ArrayAccessType, (EqualityConstraintEquation, EqualityProblem, InequalityProblem)) + | Group [(label, ArrayAccessType, (EqualityConstraintEquation, EqualityProblem, InequalityProblem))] + | Replicated [ArrayAccess label] [ArrayAccess label] data ArrayAccessType = AAWrite | AARead @@ -231,30 +242,41 @@ type VarMap = Map.Map FlattenedExp Int -- The remainder of the work (correctly pairing equations) is done by -- squareAndPair. makeReplicatedEquations :: [(A.Variable, A.Expression, A.Expression)] -> ([A.Expression],[A.Expression]) -> A.Expression -> - Either String [(VarMap, (EqualityProblem, InequalityProblem))] + Either String [((A.Expression, A.Expression), VarMap, (EqualityProblem, InequalityProblem))] makeReplicatedEquations repVars accesses bound - = do flattenedAccesses <- applyPairM (mapM flatten) accesses - let flattenedAccessesMirror = applyPair concat $ unzip $ map (\(v,_,_) -> applyPair (map (setIndexVar v 1)) flattenedAccesses) repVars + = do flattenedAccesses <- applyPairM (mapM copyAndFlatten) accesses + let flattenedAccessesMirror = applyPair (map mirrorAllVars) flattenedAccesses bound' <- flatten bound ((v,h,repVars',repVarIndexes),s) <- (flip runStateT) Map.empty $ do repVars' <- mapM (\(v,s,c) -> - do s' <- lift (flatten s) >>= makeEquation (error "Type is irrelevant for replication count") + do s' <- lift (flatten s) >>= makeEquation s (error "Type is irrelevant for replication count") >>= getSingleAccessItem "Modulo or Divide not allowed in replication start" - c' <- lift (flatten c) >>= makeEquation (error "Type is irrelevant for replication count") + c' <- lift (flatten c) >>= makeEquation c (error "Type is irrelevant for replication count") >>= getSingleAccessItem "Modulo or Divide not allowed in replication count" return (v,s',c')) repVars accesses' <- mapM (makeEquationWithPossibleRepBounds repVars') =<< makeEquationsWR flattenedAccesses accesses'' <- mapM (makeEquationWithPossibleRepBounds repVars') =<< makeEquationsWR flattenedAccessesMirror - high <- makeEquation (error "Type is irrelevant for uppper bound") bound' + high <- makeEquation bound (error "Type is irrelevant for uppper bound") bound' >>= getSingleAccessItem "Multiple possible upper bounds not supported" repVarIndexes <- mapM (\(v,_,_) -> seqPair (varIndex (Scale 1 (v,0)), varIndex (Scale 1 (v,1)))) repVars return (Replicated accesses' accesses'',high, repVars',repVarIndexes) return $ squareAndPair repVarIndexes s [v] (amap (const 0) h, addConstant (-1) h) where - makeEquationsWR :: ([[FlattenedExp]],[[FlattenedExp]]) -> StateT (VarMap) (Either String) [ArrayAccess] - makeEquationsWR (w,r) = do w' <- mapM (makeEquation AAWrite) w - r' <- mapM (makeEquation AARead) r + copyAndFlatten :: A.Expression -> Either String (A.Expression, [FlattenedExp]) + copyAndFlatten e = do f <- flatten e + return (e, f) + + -- Mirrors all of repVars in the given equation + mirrorAllVars :: (A.Expression, [FlattenedExp]) -> (A.Expression, [FlattenedExp]) + mirrorAllVars (e, f) = (e, foldl mirror f repVars) + where + mirror :: [FlattenedExp] -> (A.Variable, A.Expression, A.Expression) -> [FlattenedExp] + mirror exp (v,_,_) = setIndexVar v 1 exp + + makeEquationsWR :: ([(A.Expression, [FlattenedExp])],[(A.Expression, [FlattenedExp])]) -> StateT (VarMap) (Either String) [ArrayAccess A.Expression] + makeEquationsWR (w,r) = do w' <- mapM (\(e,f) -> makeEquation e AAWrite f) w + r' <- mapM (\(e,f) -> makeEquation e AARead f) r return (w' ++ r') @@ -269,7 +291,7 @@ makeReplicatedEquations repVars accesses bound setIndexVar' _ _ b e = (b,e) makeEquationWithPossibleRepBounds :: [(A.Variable, EqualityConstraintEquation, EqualityConstraintEquation)] -> - ArrayAccess -> StateT (VarMap) (Either String) ArrayAccess + ArrayAccess label -> StateT (VarMap) (Either String) (ArrayAccess label) makeEquationWithPossibleRepBounds [] item = return item makeEquationWithPossibleRepBounds ((v,lower,upper):vars) item -- We fold over the variables, altering the items one at a time via mapM: @@ -277,15 +299,16 @@ makeReplicatedEquations repVars accesses bound flip addPossibleRepBound' (v,0,lower,upper) item' >>= flip addPossibleRepBound' (v,1,lower,upper) - addPossibleRepBound' :: ArrayAccess -> + addPossibleRepBound' :: ArrayAccess label -> (A.Variable, Int, EqualityConstraintEquation, EqualityConstraintEquation) -> - StateT (VarMap) (Either String) ArrayAccess - addPossibleRepBound' (Group accesses) v = mapM (seqPair . transformPair return (flip addPossibleRepBound v)) accesses >>* Group + StateT (VarMap) (Either String) (ArrayAccess label) +-- addPossibleRepBound' (Group accesses) v = mapM (seqPair . transformPair return (flip addPossibleRepBound v)) accesses >>* Group + addPossibleRepBound' (Group accesses) v = sequence [addPossibleRepBound acc v >>* (\acc' -> (l,t,acc')) | (l,t,acc) <- accesses ] >>* Group addPossibleRepBound' (Replicated acc0 acc1) v = do acc0' <- mapM (flip addPossibleRepBound' v) acc0 acc1' <- mapM (flip addPossibleRepBound' v) acc1 return $ Replicated acc0' acc1' - addPossibleRepBound' (Single (t,acc)) v = addPossibleRepBound acc v >>* (\x -> Single (t,x)) + addPossibleRepBound' (Single (l,t,acc)) v = addPossibleRepBound acc v >>* (\x -> Single (l,t,x)) addPossibleRepBound :: (EqualityConstraintEquation, EqualityProblem, InequalityProblem) -> (A.Variable, Int, EqualityConstraintEquation, EqualityConstraintEquation) -> @@ -397,12 +420,12 @@ flatten other = throwError ("Unhandleable item found in expression: " ++ show ot squareAndPair :: [(CoeffIndex, CoeffIndex)] -> VarMap -> - [ArrayAccess] -> + [ArrayAccess label] -> (EqualityConstraintEquation, EqualityConstraintEquation) -> - [(VarMap, (EqualityProblem, InequalityProblem))] + [((label, label), VarMap, (EqualityProblem, InequalityProblem))] squareAndPair repVars s v lh - = [(s,squareEquations (eq,ineq ++ concat (applyAll (eq,ineq) (map addExtra repVars)))) - | (eq,ineq) <- pairEqsAndBounds v lh + = [(labels, s,squareEquations (eq,ineq ++ concat (applyAll (eq,ineq) (map addExtra repVars)))) + | (labels, eq,ineq) <- pairEqsAndBounds v lh ,and (map (primeImpliesPlain (eq,ineq)) repVars) ] where @@ -434,8 +457,8 @@ getSingles err = mapM getSingle getSingle _ = throwError err -} -getSingleAccessItem :: MonadTrans m => String -> ArrayAccess -> m (Either String) EqualityConstraintEquation -getSingleAccessItem _ (Single (_,(acc,_,_))) = lift $ return acc +getSingleAccessItem :: MonadTrans m => String -> ArrayAccess label -> m (Either String) EqualityConstraintEquation +getSingleAccessItem _ (Single (_,_,(acc,_,_))) = lift $ return acc getSingleAccessItem err _ = lift $ throwError err {- @@ -455,22 +478,24 @@ getSingleItem err _ = lift $ throwError err -- (unique, munged) variable name to variable-index in the equations. -- TODO probably want to take this into the PassM monad at some point, to use the Meta in the error message -- TODO allow "background knowledge" in the form of other equalities and inequalities -makeEquations :: ([A.Expression],[A.Expression]) -> A.Expression -> Either String [(VarMap, (EqualityProblem, InequalityProblem))] +makeEquations :: ([A.Expression],[A.Expression]) -> A.Expression -> Either String [((A.Expression, A.Expression), VarMap, (EqualityProblem, InequalityProblem))] makeEquations (esW,esR) high = makeEquations' >>* uncurry3 (squareAndPair []) where -- | The body of makeEquations; returns the variable mapping, the list of (nx,ex) pairs and a pair -- representing the upper and lower bounds of the array (inclusive). - makeEquations' :: Either String (VarMap, [ArrayAccess], (EqualityConstraintEquation, EqualityConstraintEquation)) + makeEquations' :: Either String (VarMap, [ArrayAccess A.Expression], (EqualityConstraintEquation, EqualityConstraintEquation)) makeEquations' = do ((v,h),s) <- (flip runStateT) Map.empty $ - do eqsW <- mapM (makeEquation AAWrite) =<< lift (mapM flatten esW) - eqsR <- mapM (makeEquation AARead) =<< lift (mapM flatten esR) - high' <- (lift $ flatten high) >>= makeEquation (error "Type irrelevant for upper bound") + do eqsW <- mapM (makeEquationForItem AAWrite) esW + eqsR <- mapM (makeEquationForItem AARead) esR + high' <- (lift $ flatten high) >>= makeEquation high (error "Type irrelevant for upper bound") >>= getSingleAccessItem "Multiple possible upper bounds not supported" return (eqsW ++ eqsR,high') return (s,v,(amap (const 0) h, addConstant (-1) h)) + makeEquationForItem :: ArrayAccessType -> A.Expression -> StateT VarMap (Either String) (ArrayAccess A.Expression) + makeEquationForItem t e = lift (flatten e) >>= makeEquation e t -- | Finds the index associated with a particular variable; either by finding an existing index -- or allocating a new one. @@ -493,25 +518,33 @@ varIndex mod@(Modulo top bottom) return ind -- | Pairs all possible combinations of the list of equations. -pairEqsAndBounds :: [ArrayAccess] -> (EqualityConstraintEquation, EqualityConstraintEquation) -> [(EqualityProblem, InequalityProblem)] +pairEqsAndBounds :: [ArrayAccess label] -> (EqualityConstraintEquation, EqualityConstraintEquation) -> [((label,label),EqualityProblem, InequalityProblem)] pairEqsAndBounds items bounds = (concatMap (uncurry pairEqs) . allPairs) items ++ concatMap pairRep items where - pairEqs :: ArrayAccess - -> ArrayAccess - -> [(EqualityProblem, InequalityProblem)] - pairEqs (Single acc) (Single acc') = maybeToList $ pairEqs' acc acc' - pairEqs (Single acc) (Group accs) = mapMaybe (pairEqs' acc) accs - pairEqs (Group accs) (Single acc) = mapMaybe (pairEqs' acc) accs - pairEqs (Group accs) (Group accs') = mapMaybe (uncurry pairEqs') $ product2 (accs,accs') - pairEqs (Replicated rA rB) acc - = concatMap (pairEqs acc) rA - pairEqs acc (Replicated rA rB) - = concatMap (pairEqs acc) rA + pairEqs :: ArrayAccess label + -> ArrayAccess label + -> [((label,label),EqualityProblem, InequalityProblem)] + pairEqs (Single acc) (Single acc') = maybeToList $ pairEqs'' acc acc' + pairEqs (Single acc) (Group accs) = mapMaybe (pairEqs'' acc) accs + pairEqs (Group accs) (Single acc) = mapMaybe (pairEqs'' acc) accs + pairEqs (Group accs) (Group accs') = mapMaybe (uncurry pairEqs'') $ product2 (accs,accs') + pairEqs (Replicated rA rB) lacc + = concatMap (pairEqs lacc) rA + pairEqs lacc (Replicated rA rB) + = concatMap (pairEqs lacc) rA -- Used to pair the items of a single instance of PAR replication with each other - pairRep :: ArrayAccess -> [(EqualityProblem, InequalityProblem)] - pairRep (Replicated rA rB) = (concatMap (uncurry pairEqs) $ product2 (rA,rB)) ++ concatMap (uncurry pairEqs) (allPairs rA) + pairRep :: ArrayAccess label -> [((label,label),EqualityProblem, InequalityProblem)] + pairRep (Replicated rA rB) = concatMap (uncurry pairEqs) (product2 (rA,rB)) + ++ concatMap (uncurry pairEqs) (allPairs rA) pairRep _ = [] + + pairEqs'' :: (label, ArrayAccessType,(EqualityConstraintEquation, EqualityProblem, InequalityProblem)) + -> (label, ArrayAccessType,(EqualityConstraintEquation, EqualityProblem, InequalityProblem)) + -> Maybe ((label,label), EqualityProblem, InequalityProblem) + pairEqs'' (lx,x,x') (ly,y,y') = case pairEqs' (x,x') (y,y') of + Just (eq,ineq) -> Just ((lx,ly),eq,ineq) + Nothing -> Nothing pairEqs' :: (ArrayAccessType,(EqualityConstraintEquation, EqualityProblem, InequalityProblem)) -> (ArrayAccessType,(EqualityConstraintEquation, EqualityProblem, InequalityProblem)) @@ -535,13 +568,13 @@ getIneqs (low, high) = concatMap getLH addEq = arrayZipWith' 0 (+) -- | Given an expression, forms equations (and accompanying additional equation-sets) and returns it -makeEquation :: ArrayAccessType -> [FlattenedExp] -> StateT VarMap (Either String) ArrayAccess -makeEquation t summedItems +makeEquation :: label -> ArrayAccessType -> [FlattenedExp] -> StateT VarMap (Either String) (ArrayAccess label) +makeEquation l t summedItems = do eqs <- process summedItems - let eqs' = map (transformTriple mapToArray (map mapToArray) (map mapToArray)) eqs + let eqs' = map (transformTriple mapToArray (map mapToArray) (map mapToArray)) eqs :: [(EqualityConstraintEquation, EqualityProblem, InequalityProblem)] return $ case eqs' of - [acc] -> Single (t,acc) - _ -> Group $ zip (repeat t) eqs' + [acc] -> Single (l,t,acc) + _ -> Group [(l,t,e) | e <- eqs'] where process :: [FlattenedExp] -> StateT VarMap (Either String) [(Map.Map Int Integer,[Map.Map Int Integer], [Map.Map Int Integer])] process = foldM makeEquation' empty @@ -662,3 +695,4 @@ squareEquations (eqs,ineqs) = uncurry transformPair (mkPair $ map $ makeSize (0, where highest = maximum $ 0 : (concatMap indices $ eqs ++ ineqs) + diff --git a/transformations/ArrayUsageCheckTest.hs b/transformations/ArrayUsageCheckTest.hs index c0d6ad8..816cc91 100644 --- a/transformations/ArrayUsageCheckTest.hs +++ b/transformations/ArrayUsageCheckTest.hs @@ -23,6 +23,7 @@ import Data.Array.IArray import Data.List import qualified Data.Map as Map import Data.Maybe +import Data.Ord import qualified Data.Set as Set import Prelude hiding ((**),fail) import Test.HUnit @@ -260,20 +261,20 @@ testMakeEquations = TestLabel "testMakeEquations" $ TestList [buildExpr $ Dy (Var "i") A.Mul (Lit $ intLiteral 2),exprVariable "j"],intLiteral 8) -- Testing (i REM 3) vs (4) - ,test (10,[ - (i_mod_mapping 3,[con 0 === con 4, i === con 0], leq [con 0,con 0,con 7] &&& leq [con 0,con 4,con 7]) - ,(i_mod_mapping 3,[i ++ 3 ** j === con 4], leq [con 0,con 4,con 7] &&& leq [con 0,i ++ 3 ** j,con 7] &&& [i >== con 1] &&& [j <== con 0] &&& leq [con 0, i ++ 3 ** j, con 2]) - ,(i_mod_mapping 3,[i ++ 3 ** j === con 4], leq [con 0,con 4,con 7] &&& leq [con 0,i ++ 3 ** j,con 7] &&& [i <== con (-1)] &&& [j >== con 0] &&& leq [con (-2), i ++ 3 ** j, con 0]) + ,test' (10,[ + ((0,1),i_mod_mapping 3,[con 0 === con 4, i === con 0], leq [con 0,con 0,con 7] &&& leq [con 0,con 4,con 7]) + ,((0,1),i_mod_mapping 3,[i ++ 3 ** j === con 4], leq [con 0,con 4,con 7] &&& leq [con 0,i ++ 3 ** j,con 7] &&& [i >== con 1] &&& [j <== con 0] &&& leq [con 0, i ++ 3 ** j, con 2]) + ,((0,1),i_mod_mapping 3,[i ++ 3 ** j === con 4], leq [con 0,con 4,con 7] &&& leq [con 0,i ++ 3 ** j,con 7] &&& [i <== con (-1)] &&& [j >== con 0] &&& leq [con (-2), i ++ 3 ** j, con 0]) ],[buildExpr $ Dy (Var "i") A.Rem (Lit $ intLiteral 3),intLiteral 4],intLiteral 8) -- Testing ((3*i - 2*j REM 11) - 5) vs (i + j) -- Expressed as ((2 * (i - j)) + i) REM 11 - 5, and i + j - ,test (11,[ - (_3i_2j_mod_mapping 11,[con (-5) === i ++ j, 3**i ++ (-2)**j === con 0], leq [con 0,con (-5),con 7] &&& leq [con 0,i ++ j,con 7]) - ,(_3i_2j_mod_mapping 11,[3**i ++ (-2)**j ++ 11 ** k ++ con (-5) === i ++ j], + ,test' (11,[ + ((0,1),_3i_2j_mod_mapping 11,[con (-5) === i ++ j, 3**i ++ (-2)**j === con 0], leq [con 0,con (-5),con 7] &&& leq [con 0,i ++ j,con 7]) + ,((0,1),_3i_2j_mod_mapping 11,[3**i ++ (-2)**j ++ 11 ** k ++ con (-5) === i ++ j], leq [con 0,i ++ j,con 7] &&& leq [con 0,3**i ++ (-2)**j ++ 11 ** k ++ con (-5),con 7] &&& [3**i ++ (-2)**j >== con 1] &&& [k <== con 0] &&& leq [con 0, 3**i ++ (-2)**j ++ 11 ** k, con 10]) - ,(_3i_2j_mod_mapping 11,[3**i ++ (-2)**j ++ 11 ** k ++ con (-5) === i ++ j], + ,((0,1),_3i_2j_mod_mapping 11,[3**i ++ (-2)**j ++ 11 ** k ++ con (-5) === i ++ j], leq [con 0,i ++ j,con 7] &&& leq [con 0,3**i ++ (-2)**j ++ 11 ** k ++ con (-5),con 7] &&& [3**i ++ (-2)**j <== con (-1)] &&& [k >== con 0] &&& leq [con (-10), 3**i ++ (-2)**j ++ 11 ** k, con 0]) ],[buildExpr $ @@ -288,7 +289,7 @@ testMakeEquations = TestLabel "testMakeEquations" $ TestList ,buildExpr $ Dy (Var "i") A.Add (Var "j")],intLiteral 8) -- Testing i REM 2 vs (i + 1) REM 4 - ,test (12,combine (i_ip1_mod_mapping 2 4) + ,test' (12,combine (0,1) (i_ip1_mod_mapping 2 4) [ [([con 0 === con 0],[]),rr_i_zero, rr_ip1_zero] ,[([con 0 === i ++ con 1 ++ 4**k],[]),rr_i_zero,rr_ip1_pos] ,[([con 0 === i ++ con 1 ++ 4**k],[]),rr_i_zero,rr_ip1_neg] @@ -305,72 +306,84 @@ testMakeEquations = TestLabel "testMakeEquations" $ TestList -- TODO test REM + REM vs REM -- 27 combinations! -- Testing i REM j vs 3 - ,test (100,[ + ,test' (100,[ -- i = 0: - (i_mod_j_mapping, [con 0 === con 3, i === con 0], leq [con 0, con 0, con 7] &&& leq [con 0, con 3, con 7]) + ((0,1),i_mod_j_mapping, [con 0 === con 3, i === con 0], leq [con 0, con 0, con 7] &&& leq [con 0, con 3, con 7]) -- i positive, j positive, i REM j = i: - ,(i_mod_j_mapping, [i === con 3], [i >== con 1] &&& leq [con 0, i, j ++ con (-1)] &&& leq [con 0, i, con 7] &&& leq [con 0, con 3, con 7]) + ,((0,1),i_mod_j_mapping, [i === con 3], [i >== con 1] &&& leq [con 0, i, j ++ con (-1)] &&& leq [con 0, i, con 7] &&& leq [con 0, con 3, con 7]) -- i positive, j positive, i REM j = i + k: - ,(i_mod_j_mapping, [i ++ k === con 3], [i >== con 1, k <== (-1)**j] &&& + ,((0,1),i_mod_j_mapping, [i ++ k === con 3], [i >== con 1, k <== (-1)**j] &&& leq [con 0, i ++ k, j ++ con (-1)] &&& leq [con 0, i ++ k, con 7] &&& leq [con 0, con 3, con 7]) -- i positive, j negative, i REM j = i: - ,(i_mod_j_mapping, [i === con 3], [i >== con 1] &&& leq [con 0, i, (-1)**j ++ con (-1)] &&& leq [con 0, i, con 7] &&& leq [con 0, con 3, con 7]) + ,((0,1),i_mod_j_mapping, [i === con 3], [i >== con 1] &&& leq [con 0, i, (-1)**j ++ con (-1)] &&& leq [con 0, i, con 7] &&& leq [con 0, con 3, con 7]) -- i positive, j negative, i REM j = i + k: - ,(i_mod_j_mapping, [i ++ k === con 3], [i >== con 1, k <== j] &&& + ,((0,1),i_mod_j_mapping, [i ++ k === con 3], [i >== con 1, k <== j] &&& leq [con 0, i ++ k, (-1)**j ++ con (-1)] &&& leq [con 0, i ++ k, con 7] &&& leq [con 0, con 3, con 7]) -- i negative, j positive, i REM j = i: - ,(i_mod_j_mapping, [i === con 3], [i <== con (-1)] &&& leq [(-1)**j ++ con 1, i, con 0] &&& leq [con 0, i, con 7] &&& leq [con 0, con 3, con 7]) + ,((0,1),i_mod_j_mapping, [i === con 3], [i <== con (-1)] &&& leq [(-1)**j ++ con 1, i, con 0] &&& leq [con 0, i, con 7] &&& leq [con 0, con 3, con 7]) -- i negative, j positive, i REM j = i + k: - ,(i_mod_j_mapping, [i ++ k === con 3], [i <== con (-1), k >== j] &&& + ,((0,1),i_mod_j_mapping, [i ++ k === con 3], [i <== con (-1), k >== j] &&& leq [(-1)**j ++ con 1, i ++ k, con 0] &&& leq [con 0, i ++ k, con 7] &&& leq [con 0, con 3, con 7]) -- i negative, j negative, i REM j = i: - ,(i_mod_j_mapping, [i === con 3], [i <== con (-1)] &&& leq [j ++ con 1, i, con 0] &&& leq [con 0, i, con 7] &&& leq [con 0, con 3, con 7]) + ,((0,1),i_mod_j_mapping, [i === con 3], [i <== con (-1)] &&& leq [j ++ con 1, i, con 0] &&& leq [con 0, i, con 7] &&& leq [con 0, con 3, con 7]) -- i negative, j negative, i REM j = i + k: - ,(i_mod_j_mapping, [i ++ k === con 3], [i <== con (-1), k >== (-1)**j] &&& + ,((0,1),i_mod_j_mapping, [i ++ k === con 3], [i <== con (-1), k >== (-1)**j] &&& leq [j ++ con 1, i ++ k, con 0] &&& leq [con 0, i ++ k, con 7] &&& leq [con 0, con 3, con 7]) ], [buildExpr $ Dy (Var "i") A.Rem (Var "j"), intLiteral 3], intLiteral 8) - ,testRep (200,[(rep_i_mapping, [i === j], + ,testRep' (200,[((0,0),rep_i_mapping, [i === j], ij_16 &&& [i <== j ++ con (-1)] &&& leq [con 0, i, con 7] &&& leq [con 0, j, con 7])], [(variable "i", intLiteral 1, intLiteral 6)],[exprVariable "i"],intLiteral 8) - ,testRep (201, - [(rep_i_mapping, [i === j], + ,testRep' (201, + [((0,0),rep_i_mapping, [i === j], ij_16 &&& [i <== j ++ con (-1)] &&& leq [con 0, i, con 7] &&& leq [con 0, j, con 7])] - ++ replicate 2 (rep_i_mapping,[i === con 3], leq [con 1,i, con 6] &&& leq [con 0, i, con 7] &&& leq [con 0, con 3, con 7]) - ++ [(rep_i_mapping,[con 3 === con 3],concat $ replicate 2 (leq [con 0, con 3, con 7]))] + ++ replicate 2 ((0,1),rep_i_mapping,[i === con 3], leq [con 1,i, con 6] &&& leq [con 0, i, con 7] &&& leq [con 0, con 3, con 7]) + ++ [((1,1),rep_i_mapping,[con 3 === con 3],concat $ replicate 2 (leq [con 0, con 3, con 7]))] ,[(variable "i", intLiteral 1, intLiteral 6)],[exprVariable "i", intLiteral 3],intLiteral 8) - ,testRep (202,[ - (rep_i_mapping,[i === j ++ con 1],ij_16 &&& [i <== j ++ con (-1)] &&& leq [con 0, i, con 7] &&& leq [con 0, j ++ con 1, con 7]) - ,(rep_i_mapping,[i ++ con 1 === j],ij_16 &&& [i <== j ++ con (-1)] &&& leq [con 0, i ++ con 1, con 7] &&& leq [con 0, j, con 7]) - ,(rep_i_mapping,[i === j],ij_16 &&& [i <== j ++ con (-1)] &&& leq [con 0, i, con 7] &&& leq [con 0, j, con 7]) - ,(rep_i_mapping,[i === j],ij_16 &&& [i <== j ++ con (-1)] &&& leq [con 0, i ++ con 1, con 7] &&& leq [con 0, j ++ con 1, con 7])] - ++ [(rep_i_mapping, [i === i ++ con 1], leq [con 1, i, con 6] &&& leq [con 1, i, con 6] &&& -- deliberate repeat + ,testRep' (202,[ + ((0,1),rep_i_mapping,[i === j ++ con 1],ij_16 &&& [i <== j ++ con (-1)] &&& leq [con 0, i, con 7] &&& leq [con 0, j ++ con 1, con 7]) + ,((0,1),rep_i_mapping,[i ++ con 1 === j],ij_16 &&& [i <== j ++ con (-1)] &&& leq [con 0, i ++ con 1, con 7] &&& leq [con 0, j, con 7]) + ,((0,0),rep_i_mapping,[i === j],ij_16 &&& [i <== j ++ con (-1)] &&& leq [con 0, i, con 7] &&& leq [con 0, j, con 7]) + ,((1,1),rep_i_mapping,[i === j],ij_16 &&& [i <== j ++ con (-1)] &&& leq [con 0, i ++ con 1, con 7] &&& leq [con 0, j ++ con 1, con 7])] + ++ [((0,1),rep_i_mapping, [i === i ++ con 1], leq [con 1, i, con 6] &&& leq [con 1, i, con 6] &&& -- deliberate repeat leq [con 0, i, con 7] &&& leq [con 0,i ++ con 1, con 7])] ,[(variable "i", intLiteral 1, intLiteral 6)],[exprVariable "i", buildExpr $ Dy (Var "i") A.Add (Lit $ intLiteral 1)],intLiteral 8) -- Only a constant: - ,testRep (210,[(rep_i_mapping,[con 4 === con 4],concat $ replicate 2 $ leq [con 0, con 4, con 7])] + ,testRep' (210,[((0,0),rep_i_mapping,[con 4 === con 4],concat $ replicate 2 $ leq [con 0, con 4, con 7])] ,[(variable "i", intLiteral 1, intLiteral 6)],[intLiteral 4],intLiteral 8) ] where + -- These functions assume that you pair each list [x,y,z] as (x,y) (x,z) (y,z) in that order. + -- for more control use the test' and testRep' versions: test :: (Integer,[(VarMap,[HandyEq],[HandyIneq])],[A.Expression],A.Expression) -> Test - test (ind, problems, exprs, upperBound) = - TestCase $ assertEquivalentProblems ("testMakeEquations " ++ show ind) - (map (transformPair id (uncurry makeConsistent)) $ map pairLatterTwo problems) =<< (checkRight $ makeEquations (exprs,[]) upperBound) + test (ind, problems, exprs, upperBound) = test' (ind, zipWith (\n (vm,eq,ineq) -> (n,vm,eq,ineq)) (labelNums 0 $ length exprs) problems, exprs, upperBound) + + -- The ordering for the original list [0,1,2] should be [(0,1),(0,2),(1,2)] + -- So take each number, pair it with each remaining number in order, then increase + labelNums :: Int -> Int -> [(Int,Int)] + labelNums m n | m >= n = [] + | otherwise = [(m,n') | n' <- [(m + 1) .. n]] ++ labelNums (m + 1) n + - testRep :: (Integer,[(VarMap,[HandyEq],[HandyIneq])],[(A.Variable, A.Expression, A.Expression)],[A.Expression],A.Expression) -> Test - testRep (ind, problems, reps, exprs, upperBound) = - TestCase $ assertEquivalentProblems ("testMakeEquations " ++ show ind) - (map (transformPair id (uncurry makeConsistent)) $ map pairLatterTwo problems) + test' :: (Integer,[((Int,Int),VarMap,[HandyEq],[HandyIneq])],[A.Expression],A.Expression) -> Test + test' (ind, problems, exprs, upperBound) = + TestCase $ assertEquivalentProblems ("testMakeEquations " ++ show ind) (zip [0..] exprs) + (map (transformTriple (applyPair (exprs !!)) id (uncurry makeConsistent)) $ map pairLatterTwo problems) =<< (checkRight $ makeEquations (exprs,[]) upperBound) + + testRep' :: (Integer,[((Int, Int), VarMap,[HandyEq],[HandyIneq])],[(A.Variable, A.Expression, A.Expression)],[A.Expression],A.Expression) -> Test + testRep' (ind, problems, reps, exprs, upperBound) = + TestCase $ assertEquivalentProblems ("testMakeEquations " ++ show ind) (zip [0..] exprs) + (map (transformTriple (applyPair (exprs !!)) id (uncurry makeConsistent)) $ map pairLatterTwo problems) =<< (checkRight $ makeReplicatedEquations reps (exprs,[]) upperBound) - pairLatterTwo (a,b,c) = (a,(b,c)) + pairLatterTwo (l,a,b,c) = (l,a,(b,c)) joinMapping :: [VarMap] -> ([HandyEq],[HandyIneq]) -> [(VarMap,[HandyEq],[HandyIneq])] joinMapping vms (eq,ineq) = map (\vm -> (vm,eq,ineq)) vms @@ -407,8 +420,8 @@ testMakeEquations = TestLabel "testMakeEquations" $ TestList rr_i_neg = ([], leq [con 0, i ++ 2**j, con 7] &&& [i <== con (-1), j >== con 0] &&& leq [con (-1), i ++ 2**j, con 0]) rr_ip1_neg = ([], leq [con 0, i ++ con 1 ++ 4**k, con 7] &&& [i ++ con 1 <== con (-1), k >== con 0] &&& leq [con (-3), i ++ con 1 ++ 4**k, con 0]) - combine :: VarMap -> [[([HandyEq],[HandyIneq])]] -> [(VarMap,[HandyEq],[HandyIneq])] - combine vm eq_ineqs = [(vm,e,i) | (e,i) <- map (transformPair concat concat . unzip) eq_ineqs] + combine :: (Int,Int) -> VarMap -> [[([HandyEq],[HandyIneq])]] -> [((Int,Int),VarMap,[HandyEq],[HandyIneq])] + combine l vm eq_ineqs = [(l,vm,e,i) | (e,i) <- map (transformPair concat concat . unzip) eq_ineqs] -- Helper functions for the replication: @@ -547,11 +560,36 @@ translateEquations mp = seqPair . transformPair (mapM swapColumns) (mapM swapCol swapColumns' (x,v) = transformMaybe (\y -> (y,v)) $ transformMaybe fst $ find ((== x) . snd) mp -- | Asserts that the two problems are equivalent, once you take into account the potentially different variable mappings -assertEquivalentProblems :: String -> [(VarMap, (EqualityProblem, InequalityProblem))] -> [(VarMap, (EqualityProblem, InequalityProblem))] -> Assertion -assertEquivalentProblems title exp act +assertEquivalentProblems :: String -> [(Int, A.Expression)] -> [((A.Expression, A.Expression), VarMap, (EqualityProblem, InequalityProblem))] -> + [((A.Expression, A.Expression), VarMap, (EqualityProblem, InequalityProblem))] -> Assertion +assertEquivalentProblems title indExpr exp act = ((uncurry $ assertEqualCustomShow (showPairCustom show $ showListCustom $ showMaybe showProblem) title) - $ pairPairs (length exp, length act) $ transformPair sortProblem sortProblem $ unzip $ map (uncurry transform) $ zip exp act) + $ pairPairs (length exp, length act) $ transformPair sortProblem sortProblem $ unzip $ map (uncurry transform) + $ map (uncurry checkLabel) $ zip (sortByLabels exp) (sortByLabels act)) where + -- Since this is a test, I'm taking the lazy way out and allowing run-time errors in this + -- function rather than putting it all in a monad. In HUnit the effect will be about the same + checkLabel :: ((Int, Int), VarMap, (EqualityProblem, InequalityProblem)) -> + ((Int, Int), VarMap, (EqualityProblem, InequalityProblem)) -> + ((VarMap, (EqualityProblem, InequalityProblem)), (VarMap, (EqualityProblem, InequalityProblem))) + checkLabel (l,vm,p) (l',vm',p') + | l == l' = ((vm,p), (vm',p')) + | otherwise = error $ "Labels did not match, expected: " ++ show l ++ " but actual: " ++ show l' + + sortByLabels :: [((A.Expression, A.Expression), VarMap, (EqualityProblem, InequalityProblem))] -> + [((Int, Int), VarMap, (EqualityProblem, InequalityProblem))] + sortByLabels = sortBy (comparing (\(l,_,_) -> l)) . map lookupIndexes + + sortPair :: (Int,Int) -> (Int, Int) + sortPair (x,y) | x <= y = (x,y) + | otherwise = (y,x) + + lookupIndexes :: ((A.Expression, A.Expression), VarMap, (EqualityProblem, InequalityProblem)) -> + ((Int, Int), VarMap, (EqualityProblem, InequalityProblem)) + lookupIndexes ((e,e'),vm, p) = (sortPair (lookup e, lookup e'), vm, p) + where + lookup e = maybe (-1) fst $ find ((== e) . snd) indExpr + transform :: (VarMap, (EqualityProblem, InequalityProblem)) -> (VarMap, (EqualityProblem, InequalityProblem)) -> ( Maybe (EqualityProblem, InequalityProblem), Maybe (EqualityProblem, InequalityProblem) ) transform exp act = (translatedExp, Just $ sortP $ snd act)