summaryrefslogtreecommitdiff
path: root/src/full/Agda/Utils/Warshall.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/Utils/Warshall.hs')
-rw-r--r--src/full/Agda/Utils/Warshall.hs115
1 files changed, 0 insertions, 115 deletions
diff --git a/src/full/Agda/Utils/Warshall.hs b/src/full/Agda/Utils/Warshall.hs
index 1a67955..da5ee47 100644
--- a/src/full/Agda/Utils/Warshall.hs
+++ b/src/full/Agda/Utils/Warshall.hs
@@ -21,10 +21,7 @@ import Data.List
import Data.Map (Map)
import qualified Data.Map as Map
-import Test.QuickCheck
-
import Agda.Syntax.Common (Nat)
-import Agda.Utils.TestHelpers
import Agda.Utils.SemiRing
type Matrix a = Array (Int,Int) a
@@ -420,115 +417,3 @@ while flexible variables j left
_ -> -- trace ("unusable rigid: " ++ show r ++ " for flex " ++ show f)
Nothing -- NOT: loop3 (col+1) subst
_ -> loop3 (col+1) subst
-
-
-
--- Testing ----------------------------------------------------------------
-
-genGraph :: Ord node => Float -> Gen edge -> [node] -> Gen (AdjList node edge)
-genGraph density edge nodes = do
- Map.fromList . concat <$> mapM neighbours nodes
- where
- k = round (100 * density)
- neighbours n = do
- ns <- concat <$> mapM neighbour nodes
- case ns of
- [] -> elements [[(n, [])], []]
- _ -> return [(n, ns)]
- neighbour n = frequency
- [ (k, do e <- edge
- ns <- neighbour n
- return ((n, e):ns))
- , (100 - k, return [])
- ]
-
-type Distance = Weight
-
-genGraph_ :: Nat -> Gen (AdjList Nat Distance)
-genGraph_ n =
- genGraph 0.2 (Finite <$> natural) [0..n - 1]
-
-lookupEdge :: Ord n => n -> n -> AdjList n e -> Maybe e
-lookupEdge i j g = lookup j =<< Map.lookup i g
-
-edges :: AdjList n e -> [(n,n,e)]
-edges g = do
- (i, ns) <- Map.toList g
- (j, e) <- ns
- return (i, j, e)
-
--- | Check that no edges get longer when completing a graph.
-prop_smaller :: Nat -> Property
-prop_smaller n' =
- forAll (genGraph_ n) $ \g ->
- let g' = warshallG g in
- and [ lookupEdge i j g' =< e
- | (i, j, e) <- edges g
- ]
- where
- n = abs (div n' 2)
- Nothing =< _ = False
- Just x =< y = x <= y
-
-newEdge :: Nat -> Nat -> Distance -> AdjList Nat Distance ->
- AdjList Nat Distance
-newEdge i j e = Map.insertWith (++) i [(j, e)]
-
-genPath :: Nat -> Nat -> Nat -> AdjList Nat Distance ->
- Gen (AdjList Nat Distance)
-genPath n i j g = do
- es <- listOf $ (,) <$> node <*> edge
- v <- edge
- return $ addPath i (es ++ [(j, v)]) g
- where
- edge :: Gen Distance
- edge = Finite <$> natural
-
- node :: Gen Nat
- node = choose (0, n - 1)
-
- addPath :: Nat -> [(Nat, Distance)] -> AdjList Nat Distance ->
- AdjList Nat Distance
- addPath _ [] g = g
- addPath i ((j, v):es) g = newEdge i j v $ addPath j es g
-
--- | Check that all transitive edges are added.
-prop_path :: Nat -> Property
-prop_path n' =
- forAll (genGraph_ n) $ \g ->
- forAll (two $ choose (0, n - 1)) $ \(i, j) ->
- forAll (genPath n i j g) $ \g' ->
- isJust (lookupEdge i j $ warshallG g')
- where
- n = abs (div n' 2) + 1
-
-mapNodes :: Ord node' => (node -> node') -> AdjList node edge -> AdjList node' edge
-mapNodes f = Map.map f' . Map.mapKeys f
- where
- f' es = [ (f n, e) | (n,e) <- es ]
-
--- | Check that no edges are added between components.
-prop_disjoint :: Nat -> Property
-prop_disjoint n' =
- forAll (two $ genGraph_ n) $ \(g1, g2) ->
- let g = Map.union (mapNodes Left g1) (mapNodes Right g2)
- g' = warshallG g
- in all disjoint (Map.assocs g')
- where
- n = abs (div n' 3)
- disjoint (Left i, es) = all (isLeft . fst) es
- disjoint (Right i, es) = all (isRight . fst) es
- isLeft = either (const True) (const False)
- isRight = not . isLeft
-
-prop_stable :: Nat -> Property
-prop_stable n' =
- forAll (genGraph_ n) $ \g ->
- let g' = warshallG g in
- g' =~= warshallG g'
- where
- n = abs (div n' 2)
- g =~= g' = sort (edges g) == sort (edges g')
-
-tests :: IO Bool
-tests = runTests "Agda.Utils.Warshall" []