summaryrefslogtreecommitdiff
path: root/src/full/Agda/Utils
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/Utils')
-rw-r--r--src/full/Agda/Utils/AssocList.hs1
-rw-r--r--src/full/Agda/Utils/Bag.hs72
-rw-r--r--src/full/Agda/Utils/Benchmark.hs35
-rw-r--r--src/full/Agda/Utils/BiMap.hs32
-rw-r--r--src/full/Agda/Utils/Cluster.hs105
-rw-r--r--src/full/Agda/Utils/Either.hs23
-rw-r--r--src/full/Agda/Utils/Empty.hs1
-rw-r--r--src/full/Agda/Utils/Environment.hs38
-rw-r--r--src/full/Agda/Utils/Except.hs4
-rw-r--r--src/full/Agda/Utils/Favorites.hs68
-rw-r--r--src/full/Agda/Utils/FileName.hs57
-rw-r--r--src/full/Agda/Utils/Function.hs1
-rw-r--r--src/full/Agda/Utils/Functor.hs1
-rw-r--r--src/full/Agda/Utils/Graph/AdjacencyMap/Unidirectional.hs36
-rw-r--r--src/full/Agda/Utils/Graph/AdjacencyMap/Unidirectional/Tests.hs362
-rw-r--r--src/full/Agda/Utils/Hash.hs11
-rw-r--r--src/full/Agda/Utils/Haskell/Syntax.hs110
-rw-r--r--src/full/Agda/Utils/Lens.hs1
-rw-r--r--src/full/Agda/Utils/List.hs175
-rw-r--r--src/full/Agda/Utils/ListT.hs13
-rw-r--r--src/full/Agda/Utils/ListT/Tests.hs47
-rw-r--r--src/full/Agda/Utils/Maybe/Strict.hs22
-rw-r--r--src/full/Agda/Utils/Memo.hs38
-rw-r--r--src/full/Agda/Utils/Monad.hs16
-rw-r--r--src/full/Agda/Utils/Null.hs1
-rw-r--r--src/full/Agda/Utils/Parser/MemoisedCPS.hs273
-rw-r--r--src/full/Agda/Utils/Parser/ReadP.hs2
-rw-r--r--src/full/Agda/Utils/PartialOrd.hs173
-rw-r--r--src/full/Agda/Utils/Permutation.hs22
-rw-r--r--src/full/Agda/Utils/Permutation/Tests.hs117
-rw-r--r--src/full/Agda/Utils/Pretty.hs6
-rw-r--r--src/full/Agda/Utils/QuickCheck.hs16
-rw-r--r--src/full/Agda/Utils/Singleton.hs3
-rw-r--r--src/full/Agda/Utils/Suffix.hs1
-rw-r--r--src/full/Agda/Utils/TestHelpers.hs169
-rw-r--r--src/full/Agda/Utils/Trie.hs76
-rw-r--r--src/full/Agda/Utils/Tuple.hs4
-rw-r--r--src/full/Agda/Utils/Warshall.hs115
38 files changed, 474 insertions, 1773 deletions
diff --git a/src/full/Agda/Utils/AssocList.hs b/src/full/Agda/Utils/AssocList.hs
index 671effa..d5e3ee7 100644
--- a/src/full/Agda/Utils/AssocList.hs
+++ b/src/full/Agda/Utils/AssocList.hs
@@ -1,5 +1,4 @@
{-# LANGUAGE CPP #-}
-{-# LANGUAGE TupleSections #-}
-- | Additional functions for association lists.
diff --git a/src/full/Agda/Utils/Bag.hs b/src/full/Agda/Utils/Bag.hs
index 002ba8d..310a970 100644
--- a/src/full/Agda/Utils/Bag.hs
+++ b/src/full/Agda/Utils/Bag.hs
@@ -1,6 +1,5 @@
{-# LANGUAGE CPP #-}
{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TemplateHaskell #-}
-- | A simple overlay over Data.Map to manage unordered sets with duplicates.
@@ -16,12 +15,11 @@ import Data.Functor.Identity
import qualified Data.List as List
import Data.Map (Map)
import qualified Data.Map as Map
-import Data.Monoid
+import Data.Semigroup
import qualified Data.Set as Set
import Data.Traversable
import Agda.Utils.Functor
-import Agda.Utils.QuickCheck
#include "undefined.h"
import Agda.Utils.Impossible
@@ -142,9 +140,12 @@ traverse' f = (Bag . Map.fromListWith (++)) <.> traverse trav . Map.elems . bag
instance Show a => Show (Bag a) where
showsPrec _ (Bag b) = ("Agda.Utils.Bag.Bag (" ++) . showsPrec 0 b . (')':)
+instance Ord a => Semigroup (Bag a) where
+ (<>) = union
+
instance Ord a => Monoid (Bag a) where
mempty = empty
- mappend = union
+ mappend = (<>)
mconcat = unions
instance Foldable Bag where
@@ -152,66 +153,3 @@ instance Foldable Bag where
-- not a Functor (only works for 'Ord'ered types)
-- not Traversable (only works for 'Ord'ered types)
-
-------------------------------------------------------------------------
--- * Properties
-------------------------------------------------------------------------
-
-instance (Ord a, Arbitrary a) => Arbitrary (Bag a) where
- arbitrary = fromList <$> arbitrary
-
-prop_count_empty :: Ord a => a -> Bool
-prop_count_empty a = count a empty == 0
-
-prop_count_singleton :: Ord a => a -> Bool
-prop_count_singleton a = count a (singleton a) == 1
-
-prop_count_insert :: Ord a => a -> Bag a -> Bool
-prop_count_insert a b = count a (insert a b) == 1 + count a b
-
-prop_size_union :: Ord a => Bag a -> Bag a -> Bool
-prop_size_union b c = size (b `union` c) == size b + size c
-
-prop_size_fromList :: Ord a => [a] -> Bool
-prop_size_fromList l = size (fromList l) == length l
-
-prop_fromList_toList :: Ord a => Bag a -> Bool
-prop_fromList_toList b = fromList (toList b) == b
-
-prop_toList_fromList :: Ord a => [a] -> Bool
-prop_toList_fromList l = toList (fromList l) == List.sort l
-
-prop_keys_fromList :: Ord a => [a] -> Bool
-prop_keys_fromList l = keys (fromList l) == Set.toList (Set.fromList l)
-
-prop_nonempty_groups :: Bag a -> Bool
-prop_nonempty_groups b = all (not . List.null) $ groups b
-
-prop_map_id :: Ord a => Bag a -> Bool
-prop_map_id b = map id b == b
-
-prop_map_compose :: (Ord b, Ord c) =>
- (b -> c) -> (a -> b) -> Bag a -> Bool
-prop_map_compose f g b = map f (map g b) == map (f . g) b
-
-prop_traverse_id :: Ord a => Bag a -> Bool
-prop_traverse_id b = traverse' Identity b == Identity b
-
-------------------------------------------------------------------------
--- * All tests
-------------------------------------------------------------------------
-
--- Template Haskell hack to make the following $quickCheckAll work
--- under ghc-7.8.
-return [] -- KEEP!
-
--- | All tests as collected by 'quickCheckAll'.
---
--- Using 'quickCheckAll' is convenient and superior to the manual
--- enumeration of tests, since the name of the property is
--- added automatically.
-
-tests :: IO Bool
-tests = do
- putStrLn "Agda.Utils.Favorites"
- $quickCheckAll
diff --git a/src/full/Agda/Utils/Benchmark.hs b/src/full/Agda/Utils/Benchmark.hs
index 9f0cece..24039d6 100644
--- a/src/full/Agda/Utils/Benchmark.hs
+++ b/src/full/Agda/Utils/Benchmark.hs
@@ -1,9 +1,5 @@
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE FunctionalDependencies #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE UndecidableInstances #-}
-{-# LANGUAGE TupleSections #-}
-- | Tools for benchmarking and accumulating results.
-- Nothing Agda-specific in here.
@@ -16,8 +12,10 @@ import qualified Control.Exception as E (evaluate)
import Control.Monad.Reader
import Control.Monad.State
+import Data.Foldable (foldMap)
import Data.Functor
import qualified Data.List as List
+import Data.Monoid
import qualified Text.PrettyPrint.Boxes as Boxes
@@ -77,14 +75,25 @@ mapTimings f b = b { timings = f (timings b) }
addCPUTime :: Ord a => Account a -> CPUTime -> Benchmark a -> Benchmark a
addCPUTime acc t = mapTimings (Trie.insertWith (+) acc t)
--- | Print benchmark as two-column table with totals.
+-- | Print benchmark as three-column table with totals.
instance (Ord a, Pretty a) => Pretty (Benchmark a) where
pretty b = text $ Boxes.render table
where
- (accounts, times) = unzip $ Trie.toList $ timings b
+ trie = timings b
+ (accounts, times) = unzip $ Trie.toList trie
+ aggrTimes = do
+ a <- accounts
+ let t = Trie.lookupTrie a trie
+ hasChildren =
+ case foldMap (:[]) t of
+ _:_:_ -> True
+ _ -> False
+ return $ if not (null a) && hasChildren
+ then Boxes.text $ "(" ++ prettyShow (getSum $ foldMap Sum t) ++ ")"
+ else Boxes.text ""
-- Generate a table.
- table = Boxes.hsep 1 Boxes.left [col1, col2]
+ table = Boxes.hsep 1 Boxes.left [col1, col2, col3]
-- First column: Accounts.
col1 = Boxes.vcat Boxes.left $
@@ -94,6 +103,9 @@ instance (Ord a, Pretty a) => Pretty (Benchmark a) where
col2 = Boxes.vcat Boxes.right $
map (Boxes.text . prettyShow) $
sum times : times
+ -- Thid column: Aggregate times.
+ col3 = Boxes.vcat Boxes.right $
+ Boxes.text "" : aggrTimes
showAccount [] = "Miscellaneous"
showAccount ks = List.intercalate "." $ map prettyShow ks
@@ -174,6 +186,15 @@ billTo account m = ifNotM (getsBenchmark benchmarkOn) m $ do
-- Compute and switch back to old account.
(liftIO . E.evaluate =<< m) `finally` switchBenchmarking old
+-- | Bill a CPS function to an account. Can't handle exceptions.
+billToCPS :: MonadBench a m => Account a -> ((b -> m c) -> m c) -> (b -> m c) -> m c
+billToCPS account f k = ifNotM (getsBenchmark benchmarkOn) (f k) $ do
+ -- Switch to new account.
+ old <- switchBenchmarking $ Strict.Just account
+ f $ \ x -> x `seq` do
+ _ <- switchBenchmarking old
+ k x
+
-- | Bill a pure computation to a specific account.
billPureTo :: MonadBench a m => Account a -> c -> m c
billPureTo account = billTo account . return
diff --git a/src/full/Agda/Utils/BiMap.hs b/src/full/Agda/Utils/BiMap.hs
index 0a544df..ab4e058 100644
--- a/src/full/Agda/Utils/BiMap.hs
+++ b/src/full/Agda/Utils/BiMap.hs
@@ -1,9 +1,5 @@
{-# LANGUAGE DeriveDataTypeable #-}
-{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-{-# LANGUAGE PatternGuards #-}
-{-# LANGUAGE TemplateHaskell #-}
-{-# LANGUAGE TupleSections #-}
-- | Finite bijections (implemented as a pair of maps).
@@ -21,8 +17,6 @@ import qualified Data.Map as Map
import Data.Tuple
import Data.Typeable ( Typeable )
-import Test.QuickCheck
-
-- | Finite bijective map from @a@ to @b@. There, and back again.
data BiMap a b = BiMap
{ biMapThere :: Map a b
@@ -77,29 +71,3 @@ instance (Ord a, Ord b) => Ord (BiMap a b) where
instance (Show a, Show b) => Show (BiMap a b) where
show bimap = "Agda.Utils.BiMap.fromList " ++ show (toList bimap)
-instance (Ord a, Ord b, Arbitrary a, Arbitrary b) => Arbitrary (BiMap a b) where
- arbitrary = fromList <$> do List.zip <$> alist <*> blist
- where
- alist = List.nub <$> arbitrary
- blist = List.nub <$> arbitrary
-
-------------------------------------------------------------------------
--- * Properties
-------------------------------------------------------------------------
-
-prop_BiMap_invariant :: (Ord a, Ord b) => BiMap a b -> Bool
-prop_BiMap_invariant (BiMap t u) =
- Map.toAscList t == List.sort (List.map swap (Map.toList u))
-
-------------------------------------------------------------------------
--- * All tests
-------------------------------------------------------------------------
-
--- Template Haskell hack to make the following $quickCheckAll work
--- under ghc-7.8.
-return [] -- KEEP!
-
-tests :: IO Bool
-tests = do
- putStrLn "Agda.Utils.BiMap"
- $quickCheckAll
diff --git a/src/full/Agda/Utils/Cluster.hs b/src/full/Agda/Utils/Cluster.hs
index 00c895a..9e5dc97 100644
--- a/src/full/Agda/Utils/Cluster.hs
+++ b/src/full/Agda/Utils/Cluster.hs
@@ -1,13 +1,10 @@
--- {-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE TemplateHaskell #-}
--- {-# LANGUAGE TupleSections #-}
-- | Create clusters of non-overlapping things.
module Agda.Utils.Cluster
- ( cluster
+ ( C
+ , cluster
, cluster'
- , tests
) where
import Control.Monad
@@ -20,9 +17,6 @@ import Data.Functor
import qualified Data.IntMap as IntMap
import Data.List
-import Test.QuickCheck
-import Test.QuickCheck.Function
-
-- | Characteristic identifiers.
type C = Int
@@ -47,98 +41,3 @@ cluster' acs = runEquivM id const $ do
let m = IntMap.unionsWith (++) cas
-- Return the values of the map
return $ IntMap.elems m
-
-------------------------------------------------------------------------
--- * Properties
-------------------------------------------------------------------------
-
--- instance Show (Int -> (C, [C])) where
--- show f = "function " ++ show (map (\ x -> (x, f x)) [-10..10])
-
--- Fundamental properties: soundness and completeness
-
--- | Not too many clusters. (Algorithm equated all it could.)
---
--- Each element in a cluster shares a characteristic with at least one
--- other element in the same cluster.
-prop_cluster_complete :: Fun Int (C, [C]) -> [Int] -> Bool
-prop_cluster_complete (Fun _ f) as =
- (`all` cluster f as) $ \ cl ->
- (`all` cl) $ \ a ->
- let csa = uncurry (:) $ f a in
- let cl' = delete a cl in
- -- Either a is the single element of the cluster, or it shares a characteristic c
- -- with some other element b of the same cluster.
- null cl' || not (null [ (b,c) | b <- cl', c <- uncurry (:) (f b), c `elem` csa ])
-
--- | Not too few clusters. (Algorithm did not equate too much.)
---
--- Elements of different clusters share no characteristics.
-prop_cluster_sound :: Fun Int (C, [C]) -> [Int] -> Bool
-prop_cluster_sound (Fun _ f) as =
- (`all` [ (c, d) | let cs = cluster f as, c <- cs, d <- cs, c /= d]) $ \ (c, d) ->
- (`all` c) $ \ a ->
- (`all` d) $ \ b ->
- null $ (uncurry (:) $ f a) `intersect` (uncurry (:) $ f b)
-
-neToList :: (a, [a]) -> [a]
-neToList = uncurry (:)
-
-isSingleton, exactlyTwo, atLeastTwo :: [a] -> Bool
-isSingleton x = length x == 1
-exactlyTwo x = length x == 2
-atLeastTwo x = length x >= 2
-
-prop_cluster_empty :: Bool
-prop_cluster_empty =
- null (cluster (const (0,[])) [])
-
-prop_cluster_permutation :: Fun Int (C, [C]) -> [Int] -> Bool
-prop_cluster_permutation (Fun _ f) as =
- sort as == sort (concat (cluster f as))
-
-prop_cluster_single :: a -> [a] -> Bool
-prop_cluster_single a as =
- isSingleton $ cluster (const (0,[])) $ (a:as)
-
-prop_cluster_idem :: Fun a (C, [C]) -> a -> [a] -> Bool
-prop_cluster_idem (Fun _ f) a as =
- isSingleton $ cluster f $ head $ cluster f (a:as)
-
-prop_two_clusters :: [Int] -> Bool
-prop_two_clusters as =
- atLeastTwo $ cluster (\ x -> (x, [x])) (-1:1:as)
-
--- | An example.
---
--- "anabel" is related to "babel" (common letter 'a' in 2-letter prefix)
--- which is related to "bond" (common letter 'b').
---
--- "hurz", "furz", and "kurz" are all related (common letter 'u').
-test :: [[String]]
-test = cluster (\ (x:y:_) -> (ord x,[ord y]))
- ["anabel","bond","babel","hurz","furz","kurz"]
-
-prop_test :: Bool
-prop_test = test == [["anabel","bond","babel"],["hurz","furz","kurz"]]
-
--- | Modified example (considering only the first letter).
-test1 :: [[String]]
-test1 = cluster (\ (x:_:_) -> (ord x,[]))
- ["anabel","bond","babel","hurz","furz","kurz"]
-
-prop_test1 :: Bool
-prop_test1 = test1 == [["anabel"],["bond","babel"],["furz"],["hurz"],["kurz"]]
-
-------------------------------------------------------------------------
--- * All tests
-------------------------------------------------------------------------
-
--- Template Haskell hack to make the following $quickCheckAll work
--- under ghc-7.8.
-return [] -- KEEP!
-
-tests :: IO Bool
-tests = do
- putStrLn "Agda.Utils.Cluster"
- $quickCheckAll
diff --git a/src/full/Agda/Utils/Either.hs b/src/full/Agda/Utils/Either.hs
index 4676690..bf02161 100644
--- a/src/full/Agda/Utils/Either.hs
+++ b/src/full/Agda/Utils/Either.hs
@@ -10,12 +10,9 @@ module Agda.Utils.Either
, fromLeft, fromRight
, maybeLeft, maybeRight
, allLeft, allRight
- , tests
+ , maybeToEither
) where
-import Agda.Utils.QuickCheck
-import Agda.Utils.TestHelpers
-
-- | Loop while we have an exception.
whileLeft :: Monad m => (a -> Either b c) -> (a -> b -> m a) -> (a -> c -> m d) -> a -> m d
@@ -105,18 +102,6 @@ allLeft = mapM maybeLeft
allRight :: [Either a b] -> Maybe [b]
allRight = mapM maybeRight
-prop_allRight :: Eq b => [Either t b] -> Bool
-prop_allRight xs =
- allRight xs ==
- if all isRight xs then
- Just $ map (\ (Right x) -> x) xs
- else
- Nothing
-
-------------------------------------------------------------------------
--- All tests
-
-tests :: IO Bool
-tests = runTests "Agda.Utils.Either"
- [ quickCheck' (prop_allRight :: [Either Integer Bool] -> Bool)
- ]
+-- | Convert 'Maybe' to @'Either' ()'@
+maybeToEither :: Maybe a -> Either () a
+maybeToEither = maybe (Left ()) Right
diff --git a/src/full/Agda/Utils/Empty.hs b/src/full/Agda/Utils/Empty.hs
index 084b2c8..d523cab 100644
--- a/src/full/Agda/Utils/Empty.hs
+++ b/src/full/Agda/Utils/Empty.hs
@@ -1,5 +1,4 @@
{-# LANGUAGE CPP #-}
-{-# LANGUAGE EmptyDataDecls #-}
-- | An empty type with some useful instances.
module Agda.Utils.Empty where
diff --git a/src/full/Agda/Utils/Environment.hs b/src/full/Agda/Utils/Environment.hs
index 7142d0f..1f3b96f 100644
--- a/src/full/Agda/Utils/Environment.hs
+++ b/src/full/Agda/Utils/Environment.hs
@@ -5,34 +5,42 @@ module Agda.Utils.Environment ( expandEnvironmentVariables ) where
import Data.Char
import Data.Maybe
import System.Environment
+import System.Directory ( getHomeDirectory )
expandEnvironmentVariables :: String -> IO String
expandEnvironmentVariables s = do
env <- getEnvironment
- return $ expandVars env s
+ home <- getHomeDirectory
+ return $ expandVars home env s
-expandVars :: [(String, String)] -> String -> String
-expandVars env s = concatMap repl $ tokens s
+expandVars :: String -> [(String, String)] -> String -> String
+expandVars home env s = concatMap repl $ tokens s
where
+ repl Home = home ++ "/"
repl (Var x) = fromMaybe "" $ lookup x env
repl (Str s) = s
-data Token = Var String | Str String
+data Token = Home | Var String | Str String
deriving (Eq, Show)
tokens :: String -> [Token]
-tokens s =
- case s of
- '$' : '$' : s -> cons '$' $ tokens s
- '$' : s@(c : _) | isAlpha c -> Var x : tokens s'
- where (x, s') = span isAlphaNum s
- '$' : '{' : s ->
- case break (== '}') s of
- (x, '}' : s) -> Var x : tokens s
- _ -> [Str $ "${" ++ s] -- abort on unterminated '{'
- c : s -> cons c $ tokens s
- "" -> []
+tokens s = case s of
+ '~' : '/' : s -> Home : tokens' s
+ '\\' : '~' : s -> cons '~' $ tokens' s
+ _ -> tokens' s
where
+ tokens' :: String -> [Token]
+ tokens' s =
+ case s of
+ '$' : '$' : s -> cons '$' $ tokens' s
+ '$' : s@(c : _) | c == '_' || isAlpha c -> Var x : tokens' s'
+ where (x, s') = span (\ c -> c == '_' || isAlphaNum c) s
+ '$' : '{' : s ->
+ case break (== '}') s of
+ (x, '}' : s) -> Var x : tokens' s
+ _ -> [Str $ "${" ++ s] -- abort on unterminated '{'
+ c : s -> cons c $ tokens' s
+ "" -> []
cons c (Str s : ts) = Str (c : s) : ts
cons c ts = Str [c] : ts
diff --git a/src/full/Agda/Utils/Except.hs b/src/full/Agda/Utils/Except.hs
index c1dda3e..0f36b24 100644
--- a/src/full/Agda/Utils/Except.hs
+++ b/src/full/Agda/Utils/Except.hs
@@ -1,5 +1,4 @@
{-# LANGUAGE CPP #-}
-{-# LANGUAGE FlexibleInstances #-}
#if !(MIN_VERSION_mtl(2,2,1))
{-# OPTIONS_GHC -fno-warn-orphans #-}
@@ -73,7 +72,6 @@ mapExceptT = mapErrorT
instance Error Doc where
noMsg = empty
strMsg = text
-#endif
-- | To simulate @MaybeT@ by @ExceptT@.
instance Error () where
@@ -82,3 +80,5 @@ instance Error () where
-- Stupid ErrorT!
instance Error (a, b, c) where
noMsg = __IMPOSSIBLE__
+
+#endif
diff --git a/src/full/Agda/Utils/Favorites.hs b/src/full/Agda/Utils/Favorites.hs
index 673623d..add5a44 100644
--- a/src/full/Agda/Utils/Favorites.hs
+++ b/src/full/Agda/Utils/Favorites.hs
@@ -1,7 +1,4 @@
-{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TemplateHaskell #-}
-- | Maintaining a list of favorites of some partially ordered type.
-- Only the best elements are kept.
@@ -18,20 +15,18 @@ import Prelude hiding ( null )
import Data.Foldable (Foldable)
import Data.Functor
-import Data.Monoid
+import Data.Semigroup
import qualified Data.List as List
import qualified Data.Set as Set
-import Test.QuickCheck
-
import Agda.Utils.Null
-import Agda.Utils.PartialOrd hiding (tests)
+import Agda.Utils.PartialOrd
import Agda.Utils.Singleton
import Agda.Utils.Tuple
-- | A list of incomparable favorites.
newtype Favorites a = Favorites { toList :: [a] }
- deriving (Foldable, Show, CoArbitrary, Null, Singleton a)
+ deriving (Foldable, Show, Null, Singleton a)
-- | Equality checking is a bit expensive, since we need to sort!
-- Maybe use a 'Set' of favorites in the first place?
@@ -115,59 +110,8 @@ fromList :: PartialOrd a => [a] -> Favorites a
fromList = List.foldl' (flip insert) empty
-- | 'Favorites' forms a 'Monoid' under 'empty' and 'union.
+instance PartialOrd a => Semigroup (Favorites a) where
+ (<>) = union
instance PartialOrd a => Monoid (Favorites a) where
mempty = empty
- mappend = union
-
-------------------------------------------------------------------------
--- * Properties
-------------------------------------------------------------------------
-
-instance (PartialOrd a, Arbitrary a) => Arbitrary (Favorites a) where
- arbitrary = fromList <$> arbitrary
-
-property_null_empty :: Bool
-property_null_empty = null (empty :: Favorites ())
-
-property_not_null_singleton :: forall a. a -> Bool
-property_not_null_singleton x = not $ null (singleton x :: Favorites a)
-
--- Remember: less is better!
-
-prop_compareWithFavorites :: ISet -> Favorites ISet -> Bool
-prop_compareWithFavorites a@ISet{} as =
- case compareWithFavorites a as of
- Dominates dominated notDominated ->
- all (related a POLT) dominated &&
- all (related a POAny) notDominated
- IsDominated dominator ->
- related a POGE dominator
-
-prop_fromList_after_toList :: Favorites ISet -> Bool
-prop_fromList_after_toList as =
- fromList (toList as) == as
-
--- | A second way to compute the 'union' is to use 'compareFavorites'.
-prop_union_union2 :: Favorites ISet -> Favorites ISet -> Bool
-prop_union_union2 as bs =
- union as bs == union2 as bs
- where union2 as bs = unionCompared $ compareFavorites as bs
-
-------------------------------------------------------------------------
--- * All tests
-------------------------------------------------------------------------
-
--- Template Haskell hack to make the following $quickCheckAll work
--- under ghc-7.8.
-return [] -- KEEP!
-
--- | All tests as collected by 'quickCheckAll'.
---
--- Using 'quickCheckAll' is convenient and superior to the manual
--- enumeration of tests, since the name of the property is
--- added automatically.
-
-tests :: IO Bool
-tests = do
- putStrLn "Agda.Utils.Favorites"
- $quickCheckAll
+ mappend = (<>)
diff --git a/src/full/Agda/Utils/FileName.hs b/src/full/Agda/Utils/FileName.hs
index 9e60192..9122a98 100644
--- a/src/full/Agda/Utils/FileName.hs
+++ b/src/full/Agda/Utils/FileName.hs
@@ -4,14 +4,13 @@
{-| Operations on file names. -}
module Agda.Utils.FileName
- ( AbsolutePath
+ ( AbsolutePath(AbsolutePath)
, filePath
- , rootName
, mkAbsolute
, absolute
, (===)
, doesFileExistCaseSensitive
- , tests
+ , rootPath
) where
import Control.Applicative
@@ -29,9 +28,8 @@ import Data.Function
import Data.Hashable
import Data.Typeable (Typeable)
+import Agda.Utils.Monad
import Agda.Utils.Pretty
-import Agda.Utils.TestHelpers
-import Agda.Utils.QuickCheck
#include "undefined.h"
import Agda.Utils.Impossible
@@ -58,17 +56,6 @@ instance Show AbsolutePath where
instance Pretty AbsolutePath where
pretty = text . filePath
--- | The paths have to be absolute, valid and normalised, without
--- trailing path separators.
-
-absolutePathInvariant :: AbsolutePath -> Bool
-absolutePathInvariant x =
- isAbsolute f &&
- isValid f &&
- f == normalise f &&
- f == dropTrailingPathSeparator f
- where f = filePath x
-
-- | Constructs 'AbsolutePath's.
--
-- Precondition: The path must be absolute and valid.
@@ -79,11 +66,6 @@ mkAbsolute f
AbsolutePath $ Text.pack $ dropTrailingPathSeparator $ normalise f
| otherwise = __IMPOSSIBLE__
-prop_mkAbsolute :: FilePath -> Property
-prop_mkAbsolute f =
- let path = rootPath ++ f
- in isValid path ==> absolutePathInvariant $ mkAbsolute $ path
-
rootPath :: FilePath
#if mingw32_HOST_OS
rootPath = joinDrive "C:" [pathSeparator]
@@ -123,38 +105,19 @@ infix 4 ===
(===) :: AbsolutePath -> AbsolutePath -> Bool
(===) = equalFilePath `on` filePath
--- | Case-sensitive doesFileExist for Windows.
+-- | Case-sensitive 'doesFileExist' for Windows.
+--
-- This is case-sensitive only on the file name part, not on the directory part.
-- (Ideally, path components coming from module name components should be
-- checked case-sensitively and the other path components should be checked
--- case insenstively.)
+-- case insensitively.)
+
doesFileExistCaseSensitive :: FilePath -> IO Bool
#if mingw32_HOST_OS
doesFileExistCaseSensitive f = do
- ex <- doesFileExist f
- if ex then bracket (findFirstFile f) (findClose . fst) $
- fmap (takeFileName f ==) . getFindDataFileName . snd
- else return False
+ doesFileExist f `and2M` do
+ bracket (findFirstFile f) (findClose . fst) $
+ fmap (takeFileName f ==) . getFindDataFileName . snd
#else
doesFileExistCaseSensitive f = doesFileExist f
#endif
-
-------------------------------------------------------------------------
--- Generators
-
-instance Arbitrary AbsolutePath where
- arbitrary = mk . take 3 . map (take 2) <$>
- listOf (listOf1 (elements "a1"))
- where mk ps = mkAbsolute (joinPath $ rootPath : ps)
-
-instance CoArbitrary AbsolutePath where
- coarbitrary (AbsolutePath t) = coarbitrary (Text.unpack t)
-
-------------------------------------------------------------------------
--- All tests
-
-tests :: IO Bool
-tests = runTests "Agda.Utils.FileName"
- [ quickCheck' absolutePathInvariant
- , quickCheck' prop_mkAbsolute
- ]
diff --git a/src/full/Agda/Utils/Function.hs b/src/full/Agda/Utils/Function.hs
index d229817..389e70b 100644
--- a/src/full/Agda/Utils/Function.hs
+++ b/src/full/Agda/Utils/Function.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE TupleSections #-}
module Agda.Utils.Function where
diff --git a/src/full/Agda/Utils/Functor.hs b/src/full/Agda/Utils/Functor.hs
index ec2afd4..746c237 100644
--- a/src/full/Agda/Utils/Functor.hs
+++ b/src/full/Agda/Utils/Functor.hs
@@ -1,5 +1,4 @@
{-# LANGUAGE CPP #-}
-{-# LANGUAGE TupleSections #-}
-- | Utilities for functors.
diff --git a/src/full/Agda/Utils/Graph/AdjacencyMap/Unidirectional.hs b/src/full/Agda/Utils/Graph/AdjacencyMap/Unidirectional.hs
index db86ba5..b35e4cb 100644
--- a/src/full/Agda/Utils/Graph/AdjacencyMap/Unidirectional.hs
+++ b/src/full/Agda/Utils/Graph/AdjacencyMap/Unidirectional.hs
@@ -1,12 +1,7 @@
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}
-{-# LANGUAGE DeriveFunctor #-}
-{-# LANGUAGE DoAndIfThenElse #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TupleSections #-}
-- | Directed graphs (can of course simulate undirected graphs).
--
@@ -90,8 +85,6 @@ import qualified Data.Set as Set
import Data.Set (Set)
import qualified Data.Tree as Tree
-import Test.QuickCheck hiding (label)
-
import Agda.Utils.Function
import Agda.Utils.Functor
import Agda.Utils.List (headMaybe)
@@ -100,7 +93,6 @@ import qualified Agda.Utils.Null as Null
import Agda.Utils.SemiRing
import Agda.Utils.Singleton (Singleton)
import qualified Agda.Utils.Singleton as Singleton
-import Agda.Utils.TestHelpers
import Agda.Utils.Tuple
#include "undefined.h"
@@ -765,31 +757,3 @@ gaussJordanFloydWarshallMcNaughtonYamada g =
lookup' s t = case lookup s t g of
Nothing -> ozero
Just e -> e
-
-------------------------------------------------------------------------
--- Generators
-
-instance (Arbitrary s, Arbitrary t, Arbitrary e) => Arbitrary (Edge s t e) where
- arbitrary = Edge <$> arbitrary <*> arbitrary <*> arbitrary
-
-instance (CoArbitrary s, CoArbitrary t, CoArbitrary e) => CoArbitrary (Edge s t e) where
- coarbitrary (Edge s t e) = coarbitrary s . coarbitrary t . coarbitrary e
-
-instance (Ord n, Arbitrary n, Arbitrary e) =>
- Arbitrary (Graph n n e) where
- arbitrary = do
- nodes <- sized $ \ n -> resize (2 * isqrt n) arbitrary
- edges <- mapM (\ (n1, n2) -> Edge n1 n2 <$> arbitrary) =<<
- listOfElements ((,) <$> nodes <*> nodes)
- let g1 = fromList edges
- g2 = g1 `union` fromNodes nodes
- elements [ g1 -- Does not contain empty outermost node maps.
- , g2 -- May contain empty outermost node maps.
- ]
- where
- isqrt :: Int -> Int
- isqrt = round . sqrt . fromIntegral
-
- shrink g =
- [ removeNode n g | n <- Set.toList $ nodes g ] ++
- [ removeEdge n1 n2 g | Edge n1 n2 _ <- edges g ]
diff --git a/src/full/Agda/Utils/Graph/AdjacencyMap/Unidirectional/Tests.hs b/src/full/Agda/Utils/Graph/AdjacencyMap/Unidirectional/Tests.hs
deleted file mode 100644
index f8065c3..0000000
--- a/src/full/Agda/Utils/Graph/AdjacencyMap/Unidirectional/Tests.hs
+++ /dev/null
@@ -1,362 +0,0 @@
-{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
-
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE DoAndIfThenElse #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-{-# LANGUAGE NoMonomorphismRestriction #-}
-{-# LANGUAGE TemplateHaskell #-}
-
--- | Properties for graph library.
-
-module Agda.Utils.Graph.AdjacencyMap.Unidirectional.Tests (tests) where
-
-import Prelude hiding (null)
-
-
-import Control.Monad
-
-import qualified Data.Foldable as Fold
-import Data.Function
-import qualified Data.Graph as Graph
-import qualified Data.List as List
-import Data.Maybe
-import qualified Data.Map as Map
-import qualified Data.Set as Set
-
-import Test.QuickCheck as QuickCheck
-
-import Agda.TypeChecking.Positivity.Occurrence hiding (tests)
-
-import Agda.Utils.Function (iterateUntil)
-import Agda.Utils.Functor
-import Agda.Utils.Graph.AdjacencyMap.Unidirectional as Graph
-import Agda.Utils.List (distinct)
-import Agda.Utils.Null as Null
-import Agda.Utils.SemiRing
-import Agda.Utils.Singleton (Singleton)
-import qualified Agda.Utils.Singleton as Singleton
-import Agda.Utils.TestHelpers
-
-#include "undefined.h"
-import Agda.Utils.Impossible
-
-------------------------------------------------------------------------
--- * Generating random graphs
-------------------------------------------------------------------------
-
--- | Generates a node from the graph. (Unless the graph is empty.)
-
-nodeIn :: (Ord n, Arbitrary n) => Graph n n e -> Gen n
-nodeIn g = elementsUnlessEmpty (Set.toList $ nodes g)
-
--- | Generates an edge from the graph. (Unless the graph contains no
--- edges.)
-
-edgeIn :: (Arbitrary n, Arbitrary e) =>
- Graph n n e -> Gen (Edge n n e)
-edgeIn g = elementsUnlessEmpty (edges g)
-
--- | Sample graph type used to test some graph algorithms.
-
-type G = Graph N N E
-
--- | Sample edge type used to test some graph algorithms.
-
-type E = Occurrence
-
--- | Sample node type used to test some graph algorithms.
-
-newtype N = N (Positive Int)
- deriving (Arbitrary, Eq, Ord)
-
-n :: Int -> N
-n = N . Positive
-
-instance Show N where
- show (N (Positive n)) = "n " ++ show n
-
--- | 'gaussJordanFloydWarshallMcNaughtonYamada' can be used to check
--- if any two nodes in a graph are connected.
-
-data Connected = Disconnected | Connected
- deriving (Eq, Show)
-
-instance SemiRing Connected where
- ozero = Disconnected
- oone = Connected
-
- Disconnected `oplus` c = c
- Connected `oplus` _ = Connected
-
- Disconnected `otimes` _ = Disconnected
- Connected `otimes` c = c
-
-instance StarSemiRing Connected where
- ostar _ = Connected
-
-connectivityGraph :: Ord n => Graph n n e -> Graph n n Connected
-connectivityGraph =
- fst . gaussJordanFloydWarshallMcNaughtonYamada .
- fmap (const oone)
-
-connected :: Ord n => Graph n n Connected -> n -> n -> Bool
-connected g i j = Graph.lookup i j g == Just Connected
-
-------------------------------------------------------------------------
--- * Graph properties
-------------------------------------------------------------------------
-
--- prop_neighbours :: (Ord s, Ord t, Eq e) => s -> Graph s t e -> Bool
-prop_neighbours :: N -> G -> Bool
-prop_neighbours s g =
- neighbours s g == map (\ (Edge s t e) -> (t, e)) (edgesFrom g [s])
-
--- prop_nodes_fromNodes :: Ord n => [n] -> Bool
-prop_nodes_fromNodes :: [N] -> Bool
-prop_nodes_fromNodes ns = sourceNodes (fromNodes ns) == Set.fromList ns
-
-prop_clean_discrete :: G -> Bool
-prop_clean_discrete g =
- discrete g == (null . graph . clean) g
-
--- prop_insertWith :: (Eq e, Ord s, Ord t) =>
--- (e -> e -> e) -> s -> t -> e -> Graph s t e -> Bool
-prop_insertWith :: (E -> E -> E) -> N -> N -> E -> G -> Bool
-prop_insertWith f s t e g =
- insertWith f s t e g == unionWith (flip f) g (singleton s t e)
-
--- -- This property only holds only if the edge is new.
--- prop_insert :: (Ord s, Ord t) => s -> t -> e -> Graph s t e -> Bool
--- prop_insert s t e g = insert s t e g == union g (singleton s t e)
-
-prop_sccs' :: G -> Bool
-prop_sccs' g =
- nodes g == Set.fromList (concat components)
- &&
- all distinct components
- &&
- all (not . null) components
- &&
- disjoint (map Set.fromList components)
- &&
- all stronglyConnected components'
- &&
- noMissingStronglyConnectedNodes components
- &&
- reverseTopologicalOrder
- where
- components' = sccs' g
- components = map Graph.flattenSCC components'
-
- disjoint [] = True
- disjoint (s : ss) = all (Set.null . Set.intersection s) ss
- &&
- disjoint ss
-
- connected' = connected (connectivityGraph g)
-
- stronglyConnected (Graph.AcyclicSCC n) = not (connected' n n)
- stronglyConnected (Graph.CyclicSCC ns) = and
- [ connected' i j
- | i <- ns
- , j <- ns
- ]
-
- noMissingStronglyConnectedNodes [] = True
- noMissingStronglyConnectedNodes (ns : nss) =
- and [ not (connected' j i && connected' i j)
- | i <- ns
- , j <- concat nss
- ]
- &&
- noMissingStronglyConnectedNodes nss
-
- reverseTopologicalOrder = and
- [ component i <= component j
- | Edge i j _ <- edges g
- ]
- where
- component k =
- head [ i
- | (i, ns) <- zip [1..] (reverse components)
- , k `elem` ns
- ]
-
-prop_sccDAG :: G -> Bool
-prop_sccDAG g =
- dagInvariant dag
- &&
- nodes g == Map.keysSet (dagNodeMap dag)
- where
- dag = sccDAG g
-
-prop_oppositeDAG :: G -> Bool
-prop_oppositeDAG g =
- dagInvariant (oppositeDAG (sccDAG g))
-
--- | @isWalk g from to es@ is 'True' iff @es@ is a walk from @from@ to
--- @to@ in @g@.
-
-isWalk :: G -> N -> N -> [Edge N N E] -> Bool
-isWalk g from to [] =
- from == to
- &&
- from `Set.member` nodes g
-isWalk g from to es =
- map source es ++ [to] == [from] ++ map target es
- &&
- all validEdge es
- where
- validEdge e = e `elem` edgesFrom g [source e]
-
-prop_reachableFrom :: G -> Property
-prop_reachableFrom g =
- not (Set.null (nodes g)) ==>
- forAll (nodeIn g) $ \u ->
- let reachableFromU = reachableFrom g u in
- -- Every list is a walk of the given length.
- all (\(v, (n, es)) -> isWalk g u v es && length es == n)
- (Map.toList reachableFromU)
- &&
- -- Every walk is a simple path.
- Fold.all (distinct . map source . snd) reachableFromU
- &&
- -- A path is found from u to v iff u = v or there is a non-empty
- -- path from u to v (according to 'connectivityGraph' and
- -- 'connected').
- Fold.all (\v -> Map.member v reachableFromU
- ==
- (u == v || connected cg u v))
- (nodes g)
- where
- cg = connectivityGraph g
-
-prop_walkSatisfying ::
- G -> (Occurrence -> Bool) -> (Occurrence -> Bool) -> Property
-prop_walkSatisfying g every some =
- forAll (nodeIn g) $ \from ->
- forAll (nodeIn g) $ \to ->
- case walkSatisfying every some g from to of
- Nothing -> QuickCheck.label "no walk" True
- Just es -> QuickCheck.label (show (length es) ++ " steps") $
- isWalk g from to es
- &&
- all every es' && any some es'
- where es' = map Graph.label es
-
--- | A property for
--- 'Agda.TypeChecking.Positivity.Occurrence.productOfEdgesInBoundedWalk'.
-
-prop_productOfEdgesInBoundedWalk :: G -> Property
-prop_productOfEdgesInBoundedWalk g =
- forAll (nodeIn g) $ \u ->
- forAll (nodeIn g) $ \v ->
- forAll (elements (Map.keys boundToEverySome)) $ \bound ->
- case productOfEdgesInBoundedWalk id g u v bound of
- Nothing -> Nothing
- Just o -> Just (o <= bound)
- ==
- case Graph.lookup u v
- (fst (gaussJordanFloydWarshallMcNaughtonYamada g)) of
- Just o | o <= bound -> Just True
- _ -> Nothing
-
--- | Computes the transitive closure of the graph.
---
--- Note that this algorithm is not guaranteed to be correct (or
--- terminate) for arbitrary semirings.
---
--- This function operates on the entire graph at once.
-
-transitiveClosure1 :: (Eq e, SemiRing e, Ord n) =>
- Graph n n e -> Graph n n e
-transitiveClosure1 = completeUntilWith (==) otimes oplus
-
--- | Computes the transitive closure of the graph.
---
--- Note that this algorithm is not guaranteed to be correct (or
--- terminate) for arbitrary semirings.
---
--- This function operates on the entire graph at once.
-
-completeUntilWith :: (Ord n) => (Graph n n e -> Graph n n e -> Bool) ->
- (e -> e -> e) -> (e -> e -> e) -> Graph n n e -> Graph n n e
-completeUntilWith done otimes oplus = iterateUntil done growGraph where
-
- -- @growGraph g@ unions @g@ with @(s --> t) `compose` g@ for each
- -- edge @s --> t@ in @g@
- growGraph g = List.foldl' (unionWith oplus) g $ for (edges g) $ \ (Edge s t e) ->
- case Map.lookup t (graph g) of
- Just es -> Graph $ Map.singleton s $ Map.map (otimes e) es
- Nothing -> Graph.empty
-
--- | Equality modulo empty edges.
-(~~) :: (Eq e, Ord s, Ord t, Null e) => Graph s t e -> Graph s t e -> Bool
-(~~) = (==) `on` clean
-
-prop_gaussJordanFloydWarshallMcNaughtonYamadaReference :: G -> Bool
-prop_gaussJordanFloydWarshallMcNaughtonYamadaReference g =
- gaussJordanFloydWarshallMcNaughtonYamadaReference g ~~
- transitiveClosure1 g
-
-prop_gaussJordanFloydWarshallMcNaughtonYamada :: G -> Property
-prop_gaussJordanFloydWarshallMcNaughtonYamada g =
- QuickCheck.label sccInfo $
- fst (gaussJordanFloydWarshallMcNaughtonYamada g) ~~
- transitiveClosure1 g
- where
- sccInfo =
- (if noSCCs <= 3 then " " ++ show noSCCs
- else ">= 4") ++
- " strongly connected component(s)"
- where noSCCs = length (sccs g)
-
-prop_complete :: G -> Bool
-prop_complete g =
- complete g ~~ transitiveClosure1 g
-
-------------------------------------------------------------------------
--- * All tests
-------------------------------------------------------------------------
-
--- Template Haskell hack to make the following $quickCheckAll work
--- under ghc-7.8.
-return [] -- KEEP!
-
--- | All tests as collected by 'quickCheckAll'.
---
--- Using 'quickCheckAll' is convenient and superior to the manual
--- enumeration of tests, since the name of the property is
--- added automatically.
-
-tests :: IO Bool
-tests = do
- putStrLn "Agda.Utils.Graph.AdjacencyMap.Unidirectional"
- $quickCheckAll
-
-
--- Abbreviations for testing in interpreter
-
-g1, g2, g3, g4 :: Graph N N E
-g1 = Graph $ Map.fromList
- [ (n 1, Map.fromList [(n 2,Unused)])
- , (n 2, Map.fromList [(n 1,Unused)])
- ]
-
-g2 = Graph $ Map.fromList
- [ (n 1, Map.fromList [(n 2,StrictPos)])
- , (n 2, Map.fromList [(n 1,StrictPos)])
- ]
-
-g3 = Graph $ Map.fromList
- [ (n 1, Map.fromList [(n 2,StrictPos)])
- , (n 2, Map.fromList [])
- , (n 4, Map.fromList [(n 1,StrictPos)])
- ]
-
-g4 = Graph $ Map.fromList
- [ (n 1, Map.fromList [(n 6,Unused)])
- , (n 6, Map.fromList [(n 8,StrictPos)])
- , (n 8, Map.fromList [(n 3,Unused)])
- ]
diff --git a/src/full/Agda/Utils/Hash.hs b/src/full/Agda/Utils/Hash.hs
index a2b8569..09079a6 100644
--- a/src/full/Agda/Utils/Hash.hs
+++ b/src/full/Agda/Utils/Hash.hs
@@ -8,6 +8,7 @@ import Data.ByteString as B
import Data.Word
import qualified Data.Hash as H
import qualified Data.List as L
+import Data.Digest.Murmur64
import Agda.Utils.FileName
@@ -25,12 +26,6 @@ combineHashes :: [Hash] -> Hash
combineHashes hs = H.asWord64 $ L.foldl' H.combine (H.hashWord8 0) $ L.map H.hash hs
-- | Hashing a module name for unique identifiers.
-hashString :: String -> Integer
-hashString = Prelude.foldr step 0
- where
- step c n = mod (fromIntegral (fromEnum c) * prime1 + n * prime2) prime3
-
- prime1 = 1230371
- prime2 = 446441
- prime3 = 275604541
+hashString :: String -> Word64
+hashString = asWord64 . hash64
diff --git a/src/full/Agda/Utils/Haskell/Syntax.hs b/src/full/Agda/Utils/Haskell/Syntax.hs
new file mode 100644
index 0000000..abd1e77
--- /dev/null
+++ b/src/full/Agda/Utils/Haskell/Syntax.hs
@@ -0,0 +1,110 @@
+
+module Agda.Utils.Haskell.Syntax where
+
+-- Modules --
+
+data Module = Module ModuleName [ModulePragma] [ImportDecl] [Decl]
+
+data ModulePragma = LanguagePragma [Name]
+
+data ImportDecl = ImportDecl
+ { importModule :: ModuleName
+ , importQualified :: Bool
+ , importSpecs :: Maybe (Bool, [ImportSpec]) }
+
+data ImportSpec = IVar Name
+
+-- Declarations --
+
+data Decl = TypeDecl Name [TyVarBind] Type
+ | DataDecl DataOrNew Name [TyVarBind] [ConDecl] [Deriving]
+ | TypeSig [Name] Type
+ | FunBind [Match]
+ | FakeDecl String
+ deriving (Eq)
+
+data DataOrNew = DataType | NewType
+ deriving (Eq)
+
+data ConDecl = ConDecl Name [Type]
+ deriving (Eq)
+
+type Deriving = (QName, [Type])
+
+data Binds = BDecls [Decl]
+ deriving (Eq)
+
+data Rhs = UnGuardedRhs Exp
+ | GuardedRhss [GuardedRhs]
+ deriving (Eq)
+
+data GuardedRhs = GuardedRhs [Stmt] Exp
+ deriving (Eq)
+
+data Match = Match Name [Pat] Rhs (Maybe Binds)
+ deriving (Eq)
+
+-- Expressions --
+
+data Type = TyForall [TyVarBind] Type
+ | TyFun Type Type
+ | TyCon QName
+ | TyVar Name
+ | TyApp Type Type
+ | FakeType String
+ deriving (Eq)
+
+data Pat = PVar Name
+ | PLit Literal
+ | PAsPat Name Pat
+ | PWildCard
+ | PBangPat Pat
+ | PApp QName [Pat]
+ | PatTypeSig Pat Type
+ | PIrrPat Pat
+ deriving (Eq)
+
+
+data Stmt = Qualifier Exp
+ | Generator Pat Exp
+ deriving (Eq)
+
+data Exp = Var QName
+ | Con QName
+ | Lit Literal
+ | InfixApp Exp QOp Exp
+ | App Exp Exp
+ | Lambda [Pat] Exp
+ | Let Binds Exp
+ | If Exp Exp Exp
+ | Case Exp [Alt]
+ | ExpTypeSig Exp Type
+ | NegApp Exp
+ | FakeExp String
+ deriving (Eq)
+
+data Alt = Alt Pat Rhs (Maybe Binds)
+ deriving (Eq)
+
+data Literal = Int Integer | Frac Rational | Char Char | String String
+ deriving (Eq)
+
+-- Names --
+
+data ModuleName = ModuleName String
+ deriving (Eq, Ord)
+
+data QName = Qual ModuleName Name | UnQual Name
+ deriving (Eq)
+
+data Name = Ident String | Symbol String
+ deriving (Eq)
+
+data QOp = QVarOp QName
+ deriving (Eq)
+
+data TyVarBind = UnkindedVar Name
+ deriving (Eq)
+
+unit_con :: Exp
+unit_con = Con (UnQual (Ident "()"))
diff --git a/src/full/Agda/Utils/Lens.hs b/src/full/Agda/Utils/Lens.hs
index ebb6f54..e181b2a 100644
--- a/src/full/Agda/Utils/Lens.hs
+++ b/src/full/Agda/Utils/Lens.hs
@@ -1,6 +1,5 @@
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}
-{-# LANGUAGE RankNTypes #-}
-- | A cut-down implementation of lenses, with names taken from
-- Edward Kmett's lens package.
diff --git a/src/full/Agda/Utils/List.hs b/src/full/Agda/Utils/List.hs
index 27d3826..5ddfe9c 100644
--- a/src/full/Agda/Utils/List.hs
+++ b/src/full/Agda/Utils/List.hs
@@ -1,13 +1,11 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE PatternGuards #-}
-{-# LANGUAGE TemplateHaskell #-}
-
-{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
+{-# LANGUAGE CPP #-}
{-| Utitlity functions on lists.
-}
module Agda.Utils.List where
+import Control.Arrow (first)
+
import Data.Functor ((<$>))
import Data.Function
import Data.List
@@ -16,12 +14,9 @@ import qualified Data.Map as Map
import qualified Data.Set as Set
import Text.Show.Functions ()
-import Test.QuickCheck
import qualified Agda.Utils.Bag as Bag
-import Agda.Utils.TestHelpers
--- import Agda.Utils.QuickCheck -- Andreas, 2014-04-27 Inconvenient
--- because cabal-only CPP directive
+
import Agda.Utils.Tuple
#include "undefined.h"
@@ -73,7 +68,6 @@ initLast as = Just $ loop as where
-- | Lookup function (partially safe).
(!!!) :: [a] -> Int -> Maybe a
-_ !!! n | n < 0 = __IMPOSSIBLE__
[] !!! _ = Nothing
(x : _) !!! 0 = Just x
(_ : xs) !!! n = xs !!! (n - 1)
@@ -88,18 +82,12 @@ updateHead :: (a -> a) -> [a] -> [a]
updateHead f [] = []
updateHead f (a : as) = f a : as
-spec_updateHead f as = let (bs, cs) = splitAt 1 as in map f bs ++ cs
-prop_updateHead f as = updateHead f as == spec_updateHead f as
-
-- | Update the last element of a list, if it exists.
updateLast :: (a -> a) -> [a] -> [a]
updateLast f [] = []
updateLast f [a] = [f a]
updateLast f (a : as@(_ : _)) = a : updateLast f as
-spec_updateLast f as = let (bs, cs) = splitAt (length as - 1) as in bs ++ map f cs
-prop_updateLast f as = updateLast f as == spec_updateLast f as
-
-- | Update nth element of a list, if it exists.
-- Precondition: the index is >= 0.
updateAt :: Int -> (a -> a) -> [a] -> [a]
@@ -107,9 +95,6 @@ updateAt _ f [] = []
updateAt 0 f (a : as) = f a : as
updateAt n f (a : as) = a : updateAt (n-1) f as
-spec_updateAt n f as = let (bs, cs) = splitAt n as in bs ++ updateHead f cs
-prop_updateAt (NonNegative n) f as = updateAt n f as == spec_updateAt n f as
-
-- | A generalized version of @partition@.
-- (Cf. @mapMaybe@ vs. @filter@).
mapEither :: (a -> Either b c) -> [a] -> ([b],[c])
@@ -146,6 +131,25 @@ partitionMaybe f = loop
Nothing -> mapFst (a :) $ loop as
Just b -> mapSnd (b :) $ loop as
+-- | Like 'filter', but additionally return the last partition
+-- of the list where the predicate is @False@ everywhere.
+filterAndRest :: (a -> Bool) -> [a] -> ([a],[a])
+filterAndRest p = mapMaybeAndRest $ \ a -> if p a then Just a else Nothing
+
+-- | Like 'mapMaybe', but additionally return the last partition
+-- of the list where the function always returns @Nothing@.
+mapMaybeAndRest :: (a -> Maybe b) -> [a] -> ([b],[a])
+mapMaybeAndRest f = loop [] where
+ loop acc = \case
+ [] -> ([], reverse acc)
+ x:xs | Just y <- f x -> first (y:) $ loop [] xs
+ | otherwise -> loop (x:acc) xs
+
+-- | Drops from both lists simultaneously until one list is empty.
+dropCommon :: [a] -> [b] -> ([a],[b])
+dropCommon (x : xs) (y : ys) = dropCommon xs ys
+dropCommon xs ys = (xs, ys)
+
-- | Sublist relation.
isSublistOf :: Eq a => [a] -> [a] -> Bool
isSublistOf [] ys = True
@@ -159,12 +163,14 @@ type Suffix a = [a]
-- | Check if a list has a given prefix. If so, return the list
-- minus the prefix.
-maybePrefixMatch :: Eq a => Prefix a -> [a] -> Maybe (Suffix a)
-maybePrefixMatch [] rest = Just rest
-maybePrefixMatch (_:_) [] = Nothing
-maybePrefixMatch (p:pat) (r:rest)
- | p == r = maybePrefixMatch pat rest
- | otherwise = Nothing
+stripPrefixBy :: (a -> a -> Bool) -> Prefix a -> [a] -> Maybe (Suffix a)
+stripPrefixBy eq = loop
+ where
+ loop [] rest = Just rest
+ loop (_:_) [] = Nothing
+ loop (p:pat) (r:rest)
+ | eq p r = loop pat rest
+ | otherwise = Nothing
-- | Result of 'preOrSuffix'.
data PreOrSuffix a
@@ -214,12 +220,6 @@ chopWhen p xs =
(w, [_]) -> [w, []]
(w, _ : ys) -> w : chopWhen p ys
-prop_chop_intercalate :: Property
-prop_chop_intercalate =
- forAllShrink (choose (0, 4 :: Int)) shrink $ \ d ->
- forAllShrink (listOf (choose (0, 4 :: Int))) shrink $ \ xs ->
- xs === intercalate [d] (chopWhen (== d) xs)
-
-- | All ways of removing one element from a list.
holes :: [a] -> [(a, [a])]
holes [] = []
@@ -247,9 +247,6 @@ distinct (x:xs) = x `notElem` xs && distinct xs
fastDistinct :: Ord a => [a] -> Bool
fastDistinct xs = Set.size (Set.fromList xs) == length xs
-prop_distinct_fastDistinct :: [Integer] -> Bool
-prop_distinct_fastDistinct xs = distinct xs == fastDistinct xs
-
-- | Checks if all the elements in the list are equal. Assumes that
-- the 'Eq' instance stands for an equivalence relation.
allEqual :: Eq a => [a] -> Bool
@@ -277,19 +274,6 @@ groupBy' p xxs@(x : xs) = grp x $ zipWith (\x y -> (p x y, y)) xxs xs
[] -> []
((_, z) : zs) -> grp z zs
-prop_groupBy' :: (Bool -> Bool -> Bool) -> [Bool] -> Property
-prop_groupBy' p xs =
- classify (length xs - length gs >= 3) "interesting" $
- concat gs == xs
- &&
- and [not (null zs) | zs <- gs]
- &&
- and [and (pairInitTail zs zs) | zs <- gs]
- &&
- (null gs || not (or (pairInitTail (map last gs) (map head gs))))
- where gs = groupBy' p xs
- pairInitTail xs ys = zipWith p (init xs) (tail ys)
-
-- | @'groupOn' f = 'groupBy' (('==') \`on\` f) '.' 'sortBy' ('compare' \`on\` f)@.
groupOn :: Ord b => (a -> b) -> [a] -> [[a]]
@@ -302,25 +286,6 @@ splitExactlyAt 0 xs = return ([], xs)
splitExactlyAt n [] = Nothing
splitExactlyAt n (x : xs) = mapFst (x :) <$> splitExactlyAt (n-1) xs
--- | @'extractNthElement' n xs@ gives the @n@-th element in @xs@
--- (counting from 0), plus the remaining elements (preserving order).
-
-extractNthElement' :: Integral i => i -> [a] -> ([a], a, [a])
-extractNthElement' n xs = (left, el, right)
- where
- (left, el : right) = genericSplitAt n xs
-
-extractNthElement :: Integral i => i -> [a] -> (a, [a])
-extractNthElement n xs = (el, left ++ right)
- where
- (left, el, right) = extractNthElement' n xs
-
-prop_extractNthElement :: Integer -> [Integer] -> Property
-prop_extractNthElement n xs =
- 0 <= n && n < genericLength xs ==>
- genericTake n rest ++ [elem] ++ genericDrop n rest == xs
- where (elem, rest) = extractNthElement n xs
-
-- | A generalised variant of 'elemIndex'.
genericElemIndex :: (Eq a, Integral i) => a -> [a] -> Maybe i
@@ -331,11 +296,6 @@ genericElemIndex x xs =
zip [0..] $
map (== x) xs
-prop_genericElemIndex :: Integer -> [Integer] -> Property
-prop_genericElemIndex x xs =
- classify (x `elem` xs) "members" $
- genericElemIndex x xs == elemIndex x xs
-
-- | Requires both lists to have the same length.
zipWith' :: (a -> b -> c) -> [a] -> [b] -> [c]
@@ -344,12 +304,6 @@ zipWith' f (x : xs) (y : ys) = f x y : zipWith' f xs ys
zipWith' f [] (_ : _) = {- ' -} __IMPOSSIBLE__
zipWith' f (_ : _) [] = {- ' -} __IMPOSSIBLE__
-prop_zipWith' :: (Integer -> Integer -> Integer) -> Property
-prop_zipWith' f =
- forAll natural $ \n ->
- forAll (two $ vector n) $ \(xs, ys) ->
- zipWith' f xs ys == zipWith f xs ys
-
{- UNUSED; a better type would be
zipWithTails :: (a -> b -> c) -> [a] -> [b] -> ([c], Either [a] [b])
@@ -376,9 +330,6 @@ nubOn tag =
. map (\p@(_, x) -> (tag x, p))
. zip [1..]
-prop_nubOn :: (Integer -> Integer) -> [Integer] -> Bool
-prop_nubOn f xs = nubOn f xs == nubBy ((==) `on` f) xs
-
-- | Efficient variant of 'nubBy' for finite lists.
--
-- Specification: For each list @xs@ there is a list @ys@ which is a
@@ -392,26 +343,6 @@ prop_nubOn f xs = nubOn f xs == nubBy ((==) `on` f) xs
uniqOn :: Ord b => (a -> b) -> [a] -> [a]
uniqOn key = Map.elems . Map.fromList . map (\ a -> (key a, a))
-prop_uniqOn1 :: (Integer -> Integer) -> [Integer] -> Bool
-prop_uniqOn1 f xs' =
- or [ uniqOn f xs == nubBy ((==) `on` f) ys
- | ys <- permutations xs
- ]
- where
- xs = take 5 xs'
-
- permutations [] = [[]]
- permutations (x : xs) =
- [ ys1 ++ x : ys2
- | ys <- permutations xs
- , n <- [0..length ys]
- , let (ys1, ys2) = splitAt n ys
- ]
-
-prop_uniqOn2 :: (Integer -> Integer) -> [Integer] -> Bool
-prop_uniqOn2 f xs =
- sortBy (compare `on` f) (uniqOn f xs) == uniqOn f xs
-
-- | Compute the common suffix of two lists.
commonSuffix :: Eq a => [a] -> [a] -> [a]
commonSuffix xs ys = reverse $ (commonPrefix `on` reverse) xs ys
@@ -424,22 +355,6 @@ commonPrefix (x:xs) (y:ys)
| x == y = x : commonPrefix xs ys
| otherwise = []
-prop_commonPrefix :: [Integer] -> [Integer] -> [Integer] -> Bool
-prop_commonPrefix xs ys zs =
- and [ isPrefixOf zs zs'
- , isPrefixOf zs' (zs ++ xs)
- , isPrefixOf zs' (zs ++ ys) ]
- where
- zs' = commonPrefix (zs ++ xs) (zs ++ ys)
-
-prop_commonSuffix :: [Integer] -> [Integer] -> [Integer] -> Bool
-prop_commonSuffix xs ys zs =
- and [ isSuffixOf zs zs'
- , isSuffixOf zs' (xs ++ zs)
- , isSuffixOf zs' (ys ++ zs) ]
- where
- zs' = commonSuffix (xs ++ zs) (ys ++ zs)
-
editDistanceSpec :: Eq a => [a] -> [a] -> Int
editDistanceSpec [] ys = length ys
editDistanceSpec xs [] = length xs
@@ -462,31 +377,3 @@ editDistance xs ys = editD 0 0
(x : xs, y : ys)
| x == y -> editD (i + 1) (j + 1)
| otherwise -> 1 + minimum [ editD (i + 1) j, editD i (j + 1), editD (i + 1) (j + 1) ]
-
-prop_editDistance :: Property
-prop_editDistance =
- forAllShrink (choose (0, 10)) shrink $ \ n ->
- forAllShrink (choose (0, 10)) shrink $ \ m ->
- forAllShrink (vector n) shrink $ \ xs ->
- forAllShrink (vector m) shrink $ \ ys ->
- editDistanceSpec xs ys == editDistance xs (ys :: [Integer])
-
--- Hack to make $quickCheckAll work under ghc-7.8
-return []
-
-------------------------------------------------------------------------
--- All tests
-
-tests :: IO Bool
-tests = do
- putStrLn "Agda.Utils.List"
- $quickCheckAll
-
--- tests = runTests "Agda.Utils.List"
--- [ quickCheck' prop_distinct_fastDistinct
--- , quickCheck' prop_groupBy'
--- , quickCheck' prop_extractNthElement
--- , quickCheck' prop_genericElemIndex
--- , quickCheck' prop_zipWith'
--- , quickCheck' prop_uniqOn
--- ]
diff --git a/src/full/Agda/Utils/ListT.hs b/src/full/Agda/Utils/ListT.hs
index adea6e0..da232a3 100644
--- a/src/full/Agda/Utils/ListT.hs
+++ b/src/full/Agda/Utils/ListT.hs
@@ -1,9 +1,4 @@
{-# LANGUAGE CPP #-}
-{-# LANGUAGE DeriveFunctor #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE TupleSections #-}
{-# LANGUAGE UndecidableInstances #-} -- Due to limitations of funct.dep.
-- | @ListT@ done right,
@@ -20,7 +15,7 @@ import Control.Monad
import Control.Monad.Reader
import Control.Monad.State
-import Data.Monoid
+import Data.Semigroup
import Agda.Utils.Maybe
@@ -108,10 +103,12 @@ liftListT lift xs = runMListT $ caseMaybeM (lift $ runListT xs) (return nilListT
-- Instances
+instance Monad m => Semigroup (ListT m a) where
+ l1 <> l2 = ListT $ foldListT cons (runListT l2) l1
+ where cons a = runListT . consListT a . ListT
instance Monad m => Monoid (ListT m a) where
mempty = nilListT
- mappend l1 l2 = ListT $ foldListT cons (runListT l2) l1
- where cons a = runListT . consListT a . ListT
+ mappend = (<>)
instance (Functor m, Applicative m, Monad m) => Alternative (ListT m) where
empty = mempty
diff --git a/src/full/Agda/Utils/ListT/Tests.hs b/src/full/Agda/Utils/ListT/Tests.hs
deleted file mode 100644
index d6bf006..0000000
--- a/src/full/Agda/Utils/ListT/Tests.hs
+++ /dev/null
@@ -1,47 +0,0 @@
-{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
-
-{-# LANGUAGE TemplateHaskell #-}
-
--- | Quickcheck properties for 'Agda.Utils.ListT'.
-
-module Agda.Utils.ListT.Tests (tests) where
-
-import Control.Applicative
-
-import Data.Functor.Identity
-
-import Test.QuickCheck
-
-import Text.Show.Functions
-
-import Agda.Utils.ListT
-
--- * Identity monad instance of ListT (simply lists)
-
-type List = ListT Identity
-
-foldList :: (a -> b -> b) -> b -> List a -> b
-foldList cons nil l = runIdentity $ foldListT c (Identity nil) l
- where c a = Identity . cons a . runIdentity
-
-fromList :: [a] -> List a
-fromList = foldr consListT nilListT
-
-toList :: List a -> [a]
-toList = foldList (:) []
-
-prop_concat xxs = toList (concatListT (fromList (map fromList xxs))) == concat xxs
-
-prop_idiom fs xs = toList (fromList fs <*> fromList xs) == (fs <*> xs)
-
-prop_concatMap f xs = toList (fromList . f =<< fromList xs) == (f =<< xs)
-
--- Template Haskell hack to make the following $quickCheckAll work
--- under ghc-7.8.
-return [] -- KEEP!
-
--- | All tests as collected by 'quickCheckAll'.
-tests :: IO Bool
-tests = do
- putStrLn "Agda.Utils.Permutation"
- $quickCheckAll
diff --git a/src/full/Agda/Utils/Maybe/Strict.hs b/src/full/Agda/Utils/Maybe/Strict.hs
index 4c30d39..05c5376 100644
--- a/src/full/Agda/Utils/Maybe/Strict.hs
+++ b/src/full/Agda/Utils/Maybe/Strict.hs
@@ -5,8 +5,6 @@
{-# LANGUAGE DeriveGeneric #-}
#endif
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE StandaloneDeriving #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
@@ -38,7 +36,7 @@ import Control.Applicative (pure, (<$>))
import Control.DeepSeq (NFData (..))
import Data.Binary (Binary (..))
import Data.Data (Data (..))
-import Data.Monoid (Monoid (..))
+import Data.Semigroup (Semigroup, Monoid, (<>), mempty, mappend)
import Data.Foldable (Foldable (..))
import Data.Traversable (Traversable (..))
#if MIN_VERSION_base(4,7,0)
@@ -51,7 +49,6 @@ import Data.Strict.Maybe (Maybe (Nothing, Just), fromJust,
#if __GLASGOW_HASKELL__ >= 706
import GHC.Generics (Generic (..))
#endif
-import Test.QuickCheck (Arbitrary (..), CoArbitrary (..))
import Agda.Utils.Null
@@ -80,12 +77,14 @@ instance Null (Maybe a) where
-- The monoid instance was fixed in strict-base-types 0.5.0. See
-- Issue 1805.
+instance Monoid a => Semigroup (Maybe a) where
+ Nothing <> m = m
+ m <> Nothing = m
+ Just x1 <> Just x2 = Just (x1 `mappend` x2)
+
instance Monoid a => Monoid (Maybe a) where
mempty = Nothing
-
- Nothing `mappend` m = m
- m `mappend` Nothing = m
- Just x1 `mappend` Just x2 = Just (x1 `mappend` x2)
+ mappend = (<>)
instance Foldable Maybe where
foldMap _ Nothing = mempty
@@ -102,13 +101,6 @@ instance Binary a => Binary (Maybe a) where
put = put . toLazy
get = toStrict <$> get
-instance Arbitrary a => Arbitrary (Maybe a) where
- arbitrary = toStrict <$> arbitrary
- shrink = map toStrict . shrink . toLazy
-
-instance CoArbitrary a => CoArbitrary (Maybe a) where
- coarbitrary = coarbitrary . toLazy
-
-- | Analogous to 'Lazy.listToMaybe' in "Data.Maybe".
listToMaybe :: [a] -> Maybe a
listToMaybe [] = Nothing
diff --git a/src/full/Agda/Utils/Memo.hs b/src/full/Agda/Utils/Memo.hs
index 55f42b2..498258b 100644
--- a/src/full/Agda/Utils/Memo.hs
+++ b/src/full/Agda/Utils/Memo.hs
@@ -1,10 +1,15 @@
{-# LANGUAGE CPP #-}
-{-# LANGUAGE RankNTypes #-}
module Agda.Utils.Memo where
import Control.Applicative
import Control.Monad.State
+import System.IO.Unsafe
+import Data.IORef
+import qualified Data.Map as Map
+import qualified Agda.Utils.HashMap as HMap
+import Data.Hashable
+
import Agda.Utils.Lens
-- Simple memoisation in a state monad
@@ -42,3 +47,34 @@ memoRec tbl ih compute = do
tbl .= Just ih
x <- compute
x <$ (tbl .= Just x)
+
+{-# NOINLINE memoUnsafe #-}
+memoUnsafe :: Ord a => (a -> b) -> (a -> b)
+memoUnsafe f = unsafePerformIO $ do
+ tbl <- newIORef Map.empty
+ return (unsafePerformIO . f' tbl)
+ where
+ f' tbl x = do
+ m <- readIORef tbl
+ case Map.lookup x m of
+ Just y -> return y
+ Nothing -> do
+ let y = f x
+ writeIORef tbl (Map.insert x y m)
+ return y
+
+{-# NOINLINE memoUnsafeH #-}
+memoUnsafeH :: (Eq a, Hashable a) => (a -> b) -> (a -> b)
+memoUnsafeH f = unsafePerformIO $ do
+ tbl <- newIORef HMap.empty
+ return (unsafePerformIO . f' tbl)
+ where
+ f' tbl x = do
+ m <- readIORef tbl
+ case HMap.lookup x m of
+ Just y -> return y
+ Nothing -> do
+ let y = f x
+ writeIORef tbl (HMap.insert x y m)
+ return y
+
diff --git a/src/full/Agda/Utils/Monad.hs b/src/full/Agda/Utils/Monad.hs
index ac1cd24..63f1f6a 100644
--- a/src/full/Agda/Utils/Monad.hs
+++ b/src/full/Agda/Utils/Monad.hs
@@ -50,7 +50,9 @@ whenM c m = c >>= (`when_` m)
unlessM :: Monad m => m Bool -> m a -> m ()
unlessM c m = c >>= (`unless_` m)
--- whenJust, whenJustM moved to Utils.Maybe
+-- | Monadic guard.
+guardM :: (Monad m, MonadPlus m) => m Bool -> m ()
+guardM c = guard =<< c
-- | Monadic if-then-else.
ifM :: Monad m => m Bool -> m a -> m a -> m a
@@ -149,6 +151,13 @@ dropWhileM :: Monad m => (a -> m Bool) -> [a] -> m [a]
dropWhileM p [] = return []
dropWhileM p (x : xs) = ifM (p x) (dropWhileM p xs) (return (x : xs))
+-- | A ``monadic'' version of @'partition' :: (a -> Bool) -> [a] -> ([a],[a])
+partitionM :: (Functor m, Applicative m) => (a -> m Bool) -> [a] -> m ([a],[a])
+partitionM f [] =
+ pure ([], [])
+partitionM f (x:xs) =
+ (\ b (l, r) -> if b then (x:l, r) else (l, x:r)) <$> f x <*> partitionM f xs
+
-- Error monad ------------------------------------------------------------
-- | Finally for the 'Error' class. Errors in the finally part take
@@ -162,6 +171,11 @@ first `finally` after = do
Left e -> throwError e
Right r -> return r
+-- | Try a computation, return 'Nothing' if an 'Error' occurs.
+
+tryMaybe :: (MonadError e m, Functor m) => m a -> m (Maybe a)
+tryMaybe m = (Just <$> m) `catchError` \ _ -> return Nothing
+
-- State monad ------------------------------------------------------------
-- | Bracket without failure. Typically used to preserve state.
diff --git a/src/full/Agda/Utils/Null.hs b/src/full/Agda/Utils/Null.hs
index 9919ff3..32f634b 100644
--- a/src/full/Agda/Utils/Null.hs
+++ b/src/full/Agda/Utils/Null.hs
@@ -1,7 +1,6 @@
{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# LANGUAGE CPP #-}
-{-# LANGUAGE DefaultSignatures #-}
-- | Overloaded @null@ and @empty@ for collections and sequences.
diff --git a/src/full/Agda/Utils/Parser/MemoisedCPS.hs b/src/full/Agda/Utils/Parser/MemoisedCPS.hs
index 6a57ea8..6224ddc 100644
--- a/src/full/Agda/Utils/Parser/MemoisedCPS.hs
+++ b/src/full/Agda/Utils/Parser/MemoisedCPS.hs
@@ -21,38 +21,33 @@
-- non-termination for grammars that are not cyclic.)
{-# LANGUAGE CPP #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE RankNTypes #-}
-
-#if __GLASGOW_HASKELL__ >= 710
-{-# LANGUAGE FlexibleContexts #-}
-#endif
module Agda.Utils.Parser.MemoisedCPS
- ( Parser
- , parse
- , token
- , tok
- , sat
- , chainl1
- , chainr1
- , memoise
+ ( ParserClass(..)
+ , Parser
+ , ParserWithGrammar
) where
import Control.Applicative
import Control.Monad (ap, liftM2)
-import Control.Monad.State.Strict (State, evalState, get)
+import Control.Monad.State.Strict (State, evalState, get, put)
import Data.Array
import Data.Hashable
import qualified Data.HashMap.Strict as Map
import Data.HashMap.Strict (HashMap)
+import qualified Data.HashSet as Set
+import Data.HashSet (HashSet)
import qualified Data.IntMap.Strict as IntMap
import Data.IntMap.Strict (IntMap)
import Data.List
+import Text.PrettyPrint.HughesPJ hiding (empty)
+import qualified Text.PrettyPrint.HughesPJ as PP
import Agda.Utils.Monad (modify')
+#include "undefined.h"
+import Agda.Utils.Impossible
+
-- | Positions.
type Pos = Int
@@ -111,94 +106,89 @@ instance Alternative (Parser k r tok) where
P p1 <|> P p2 = P $ \input i k ->
liftM2 (++) (p1 input i k) (p2 input i k)
--- | Runs the parser.
-
-parse :: Parser k r tok a -> [tok] -> [a]
-parse p toks =
- flip evalState IntMap.empty $
- unP p (listArray (0, n - 1) toks) 0 $ \j x ->
- if j == n then return [x] else return []
- where n = genericLength toks
-
--- | Parses a single token.
-
-token :: Parser k r tok tok
-token = P $ \input i k ->
- if inRange (bounds input) i then
- (k $! (i + 1)) $! (input ! i)
- else
- return []
-
--- | Parses a token satisfying the given predicate.
-
-sat :: (tok -> Bool) -> Parser k r tok tok
-sat p = do
- t <- token
- if p t then return t else empty
-
--- | Parses a given token.
-
-tok :: Eq tok => tok -> Parser k r tok tok
-tok t = sat (t ==)
-
--- | Parses one or more things, separated by separators.
---
--- Combines the results in a right-associative way.
-
-chainr1
- :: Parser k r tok a
- -- ^ Parser for a thing.
- -> Parser k r tok (a -> a -> a)
- -- ^ Parser for a separator.
- -> Parser k r tok a
-chainr1 p op = c
- where c = (\x f -> f x) <$> p <*>
- (pure id <|> flip <$> op <*> c)
-
--- | Parses one or more things, separated by separators.
---
--- Combines the results in a left-associative way.
-
-chainl1
- :: Parser k r tok a
- -- ^ Parser for a thing.
- -> Parser k r tok (a -> a -> a)
- -- ^ Parser for a separator.
- -> Parser k r tok a
-chainl1 p op = (\x f -> f x) <$> p <*> c
- where
- c = pure (\x -> x)
- <|> (\f y g x -> g (f x y)) <$> op <*> p <*> c
-
--- | Memoises the given parser.
---
--- Every memoised parser must be annotated with a /unique/ key.
--- (Parametrised parsers must use distinct keys for distinct inputs.)
-
-memoise ::
- (Eq k, Hashable k) =>
- k -> Parser k r tok r -> Parser k r tok r
-memoise key p = P $ \input i k -> do
-
- let alter j zero f m =
- IntMap.alter (Just . f . maybe zero id) j m
-
- lookupTable = fmap (\m -> Map.lookup key =<<
- IntMap.lookup i m) get
- insertTable v = modify' $ alter i Map.empty (Map.insert key v)
-
- v <- lookupTable
- case v of
- Nothing -> do
- insertTable (Value IntMap.empty [k])
- unP p input i $ \j r -> do
- Just (Value rs ks) <- lookupTable
- insertTable (Value (alter j [] (r :) rs) ks)
- concat <$> mapM (\k -> k j r) ks -- See note [Reverse ks?].
- Just (Value rs ks) -> do
- insertTable (Value rs (k : ks))
- concat . concat <$>
- mapM (\(i, rs) -> mapM (k i) rs) (IntMap.toList rs)
+class (Functor p, Applicative p, Alternative p, Monad p) =>
+ ParserClass p k r tok | p -> k, p -> r, p -> tok where
+ -- | Runs the parser.
+ parse :: p a -> [tok] -> [a]
+
+ -- | Tries to print the parser, or returns 'PP.empty', depending on
+ -- the implementation. This function might not terminate.
+ grammar :: p a -> Doc
+
+ -- | Parses a single token.
+ token :: p tok
+
+ -- | Parses a token satisfying the given predicate.
+ sat :: (tok -> Bool) -> p tok
+
+ -- | Parses a given token.
+ tok :: (Eq tok, Show tok) => tok -> p tok
+
+ -- | Uses the given function to modify the printed representation
+ -- (if any) of the given parser.
+ annotate :: (Doc -> Doc) -> p a -> p a
+
+ -- | Memoises the given parser.
+ --
+ -- Every memoised parser must be annotated with a /unique/ key.
+ -- (Parametrised parsers must use distinct keys for distinct
+ -- inputs.)
+ memoise :: (Eq k, Hashable k, Show k) => k -> p r -> p r
+
+ -- | Memoises the given parser, but only if printing, not if
+ -- parsing.
+ --
+ -- Every memoised parser must be annotated with a /unique/ key.
+ -- (Parametrised parsers must use distinct keys for distinct
+ -- inputs.)
+ memoiseIfPrinting :: (Eq k, Hashable k, Show k) => k -> p r -> p r
+
+instance ParserClass (Parser k r tok) k r tok where
+ parse p toks =
+ flip evalState IntMap.empty $
+ unP p (listArray (0, n - 1) toks) 0 $ \j x ->
+ if j == n then return [x] else return []
+ where n = genericLength toks
+
+ grammar _ = PP.empty
+
+ token = P $ \input i k ->
+ if inRange (bounds input) i then
+ (k $! (i + 1)) $! (input ! i)
+ else
+ return []
+
+ sat p = do
+ t <- token
+ if p t then return t else empty
+
+ tok t = sat (t ==)
+
+ annotate _ p = p
+
+ memoiseIfPrinting _ p = p
+
+ memoise key p = P $ \input i k -> do
+
+ let alter j zero f m =
+ IntMap.alter (Just . f . maybe zero id) j m
+
+ lookupTable = fmap (\m -> Map.lookup key =<<
+ IntMap.lookup i m) get
+ insertTable v = modify' $ alter i Map.empty (Map.insert key v)
+
+ v <- lookupTable
+ case v of
+ Nothing -> do
+ insertTable (Value IntMap.empty [k])
+ unP p input i $ \j r -> do
+ Just (Value rs ks) <- lookupTable
+ insertTable (Value (alter j [] (r :) rs) ks)
+ concat <$> mapM (\k -> k j r) ks -- See note [Reverse ks?].
+ Just (Value rs ks) -> do
+ insertTable (Value rs (k : ks))
+ concat . concat <$>
+ mapM (\(i, rs) -> mapM (k i) rs) (IntMap.toList rs)
-- [Reverse ks?]
--
@@ -206,3 +196,78 @@ memoise key p = P $ \input i k -> do
-- infinitely ambiguous grammars, including S ∷= S | ε. However, in
-- some cases the results would not be fair (some valid results would
-- never be returned).
+
+-- | An extended parser type, with some support for printing parsers.
+
+data ParserWithGrammar k r tok a =
+ PG (Bool -> Either (Parser k r tok a)
+ (State (HashSet k) Doc))
+ -- ^ Invariant: If the boolean is 'True', then the result must be
+ -- @'Left' something@, and if the boolean is 'False', then the
+ -- result must be @'Right' something@.
+
+-- | A smart constructor.
+
+pg :: Parser k r tok a ->
+ State (HashSet k) Doc ->
+ ParserWithGrammar k r tok a
+pg p d = PG $ \b -> if b then Left p else Right d
+
+-- | Extracts the parser.
+
+parser :: ParserWithGrammar k r tok a -> Parser k r tok a
+parser (PG p) = either id __IMPOSSIBLE__ (p True)
+
+-- | Extracts the document.
+
+doc :: ParserWithGrammar k r tok a -> State (HashSet k) Doc
+doc (PG p) = either __IMPOSSIBLE__ id (p False)
+
+instance Monad (ParserWithGrammar k r tok) where
+ return = pure
+ p >>= f = pg (parser p >>= parser . f)
+ ((\d -> parens (d <+> text ">>= ?")) <$> doc p)
+
+instance Functor (ParserWithGrammar k r tok) where
+ fmap f p = pg (fmap f (parser p)) (doc p)
+
+instance Applicative (ParserWithGrammar k r tok) where
+ pure x = pg (pure x) (return (text "ε"))
+ p1 <*> p2 =
+ pg (parser p1 <*> parser p2)
+ (liftM2 (\d1 d2 -> parens (sep [d1, d2])) (doc p1) (doc p2))
+
+instance Alternative (ParserWithGrammar k r tok) where
+ empty = pg empty (return (text "∅"))
+ p1 <|> p2 =
+ pg (parser p1 <|> parser p2)
+ (liftM2 (\d1 d2 -> parens (sep [d1, text "|", d2])) (doc p1) (doc p2))
+
+ many p = pg (many (parser p)) ((<+> text "⋆") . parens <$> doc p)
+ some p = pg (some (parser p)) ((<+> text "+") . parens <$> doc p)
+
+-- | A helper function.
+
+memoiseDoc ::
+ (Eq k, Hashable k, Show k) =>
+ k -> ParserWithGrammar k r tok r -> State (HashSet k) Doc
+memoiseDoc key p = do
+ s <- get
+ if Set.member key s then
+ return (text ("<" ++ show key ++ ">"))
+ else do
+ put (Set.insert key s)
+ (\d -> parens $
+ text ("μ " ++ show key ++ ".") $+$ nest 2 d) <$>
+ doc p
+
+instance ParserClass (ParserWithGrammar k r tok) k r tok where
+ parse p = parse (parser p)
+ grammar p = evalState (doc p) Set.empty
+ token = pg token (return (text "·"))
+ sat p = pg (sat p) (return (text "sat ?"))
+ tok t = pg (tok t) (return (text (show t)))
+ annotate f p = pg (parser p) (f <$> doc p)
+ memoise key p = pg (memoise key (parser p))
+ (memoiseDoc key p)
+ memoiseIfPrinting key p = pg (parser p) (memoiseDoc key p)
diff --git a/src/full/Agda/Utils/Parser/ReadP.hs b/src/full/Agda/Utils/Parser/ReadP.hs
index 9b6defc..1b1cf2e 100644
--- a/src/full/Agda/Utils/Parser/ReadP.hs
+++ b/src/full/Agda/Utils/Parser/ReadP.hs
@@ -1,6 +1,4 @@
-{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE MagicHash #-}
-{-# LANGUAGE Rank2Types #-}
-----------------------------------------------------------------------------
-- |
diff --git a/src/full/Agda/Utils/PartialOrd.hs b/src/full/Agda/Utils/PartialOrd.hs
index 0f1e331..1b1608c 100644
--- a/src/full/Agda/Utils/PartialOrd.hs
+++ b/src/full/Agda/Utils/PartialOrd.hs
@@ -1,22 +1,14 @@
-{-# LANGUAGE DeriveFunctor #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-{-# LANGUAGE TemplateHaskell #-}
module Agda.Utils.PartialOrd where
import Data.Functor
import Data.Maybe
-import Data.Monoid
import Data.List
+import Data.Semigroup
import Data.Set (Set)
import qualified Data.Set as Set
-import Test.QuickCheck.All
-
-- import Agda.Utils.List
-import Agda.Utils.TestHelpers
-import Agda.Utils.QuickCheck
-- | The result of comparing two things (of the same type).
data PartialOrdering
@@ -128,9 +120,12 @@ seqPO POGT POGT = POGT -- idempotent
seqPO _ _ = POAny
-- | Partial ordering forms a monoid under sequencing.
+instance Semigroup PartialOrdering where
+ (<>) = seqPO
+
instance Monoid PartialOrdering where
mempty = POEQ
- mappend = seqPO
+ mappend = (<>)
-- | Embed 'Ordering'.
fromOrdering :: Ordering -> PartialOrdering
@@ -291,161 +286,3 @@ instance PartialOrd PartialOrdering where
comparable POGT POGE = POLT
-- anything horizontal is not comparable
comparable _ _ = POAny
-
--- * Properties
-
-instance Arbitrary PartialOrdering where
- arbitrary = arbitraryBoundedEnum
-
--- | We test our properties on integer sets ordered by inclusion.
-
-newtype ISet = ISet { iset :: Inclusion (Set Int) }
- deriving (Eq, Ord, PartialOrd, Show)
-
-instance Arbitrary ISet where
- arbitrary = ISet . Inclusion . Set.fromList <$> listOf (choose (0, 8))
-
--- | Any two elements are 'related' in the way 'comparable' computes.
-prop_comparable_related :: ISet -> ISet -> Bool
-prop_comparable_related (ISet a) (ISet b) =
- related a o b where o = comparable a b
-
--- | @flip comparable a b == oppPO (comparable a b)@
-prop_oppPO :: ISet -> ISet -> Bool
-prop_oppPO (ISet a) (ISet b) =
- comparable a b == oppPO (comparable b a)
-
--- | Auxiliary function: lists to sets = sorted duplicate-free lists.
-sortUniq :: [Ordering] -> [Ordering]
-sortUniq = Set.toAscList . Set.fromList
-
--- | 'leqPO' is inclusion of the associated 'Ordering' sets.
-prop_leqPO_sound :: PartialOrdering -> PartialOrdering -> Bool
-prop_leqPO_sound p q =
- (p `leqPO` q) == null (toOrderings p \\ toOrderings q)
-
--- | 'orPO' amounts to the union of the associated 'Ordering' sets.
--- Except that 'orPO POLT POGT == POAny' which should also include 'POEQ'.
-prop_orPO_sound :: PartialOrdering -> PartialOrdering -> Bool
-prop_orPO_sound p q =
- (p `orPO` q) == fromOrderings (toOrderings p ++ toOrderings q)
-
--- | 'orPO' is associative.
-prop_associative_orPO :: PartialOrdering -> PartialOrdering ->
- PartialOrdering -> Bool
-prop_associative_orPO = associative orPO
-
--- | 'orPO' is commutative.
-prop_commutative_orPO :: PartialOrdering -> PartialOrdering -> Bool
-prop_commutative_orPO = commutative orPO
-
--- | 'orPO' is idempotent.
-prop_idempotent_orPO :: PartialOrdering -> Bool
-prop_idempotent_orPO = idempotent orPO
-
--- | The dominant element wrt. 'orPO' is 'POAny'.
-prop_zero_orPO :: PartialOrdering -> Bool
-prop_zero_orPO = isZero POAny orPO
-
--- | Soundness of 'seqPO'.
---
--- As QuickCheck test, this property is inefficient, see 'prop_seqPO'.
-property_seqPO :: ISet -> PartialOrdering -> ISet -> PartialOrdering ->
- ISet -> Property
-property_seqPO (ISet a) o (ISet b) p (ISet c) =
- related a o b && related b p c ==> related a (seqPO o p) c
-
--- | A more efficient way of stating soundness of 'seqPO'.
-prop_seqPO :: ISet -> ISet -> ISet -> Bool
-prop_seqPO (ISet a) (ISet b) (ISet c) = related a o c
- where o = comparable a b `seqPO` comparable b c
-
--- | The unit of 'seqPO' is 'POEQ'.
-prop_identity_seqPO :: PartialOrdering -> Bool
-prop_identity_seqPO = identity POEQ seqPO
-
--- | The zero of 'seqPO' is 'POAny'.
-prop_zero_seqPO :: PartialOrdering -> Bool
-prop_zero_seqPO = isZero POAny seqPO
-
--- | 'seqPO' is associative.
-prop_associative_seqPO :: PartialOrdering -> PartialOrdering ->
- PartialOrdering -> Bool
-prop_associative_seqPO = associative seqPO
-
--- | 'seqPO' is also commutative.
-prop_commutative_seqPO :: PartialOrdering -> PartialOrdering -> Bool
-prop_commutative_seqPO = commutative seqPO
-
--- | 'seqPO' is idempotent.
-prop_idempotent_seqPO :: PartialOrdering -> Bool
-prop_idempotent_seqPO = idempotent seqPO
-
--- | 'seqPO' distributes over 'orPO'.
-prop_distributive_seqPO_orPO :: PartialOrdering -> PartialOrdering ->
- PartialOrdering -> Bool
-prop_distributive_seqPO_orPO = distributive seqPO orPO
-
--- | The result of 'toOrderings' is a sorted list without duplicates.
-prop_sorted_toOrderings :: PartialOrdering -> Bool
-prop_sorted_toOrderings p =
- sortUniq os == os where os = toOrderings p
-
--- | From 'Ordering' to 'PartialOrdering' and back is the identity.
-prop_toOrderings_after_fromOrdering :: Ordering -> Bool
-prop_toOrderings_after_fromOrdering o =
- toOrderings (fromOrdering o) == [o]
-
--- | From 'PartialOrdering' to 'Orderings' and back is the identity.
-prop_fromOrderings_after_toOrderings :: PartialOrdering -> Bool
-prop_fromOrderings_after_toOrderings p =
- fromOrderings (toOrderings p) == p
-
--- | From 'Orderings' to 'PartialOrdering' and back is the identity.
--- Except for @[LT,GT]@ which is a non-canonical representative of 'POAny'.
-prop_toOrderings_after_fromOrderings :: NonEmptyList Ordering -> Bool
-prop_toOrderings_after_fromOrderings (NonEmpty os) =
- Set.fromList os `Set.isSubsetOf`
- Set.fromList (toOrderings (fromOrderings os))
-
--- | Pairs are related iff both components are related.
-prop_related_pair :: ISet -> ISet -> ISet -> ISet -> PartialOrdering -> Bool
-prop_related_pair (ISet x1) (ISet x2) (ISet y1) (ISet y2) o =
- related (x1,x2) o (y1,y2) == (related x1 o y1 && related x2 o y2)
-
--- | Comparing 'PartialOrdering's amounts to compare their representation as
--- 'Ordering' sets.
-
-prop_comparable_PartialOrdering :: PartialOrdering -> PartialOrdering -> Bool
-
-prop_comparable_PartialOrdering p q =
- comparable p q == comparable (to p) (to q)
- where to = Inclusion . toOrderings
-
-------------------------------------------------------------------------
--- * All tests
-------------------------------------------------------------------------
-
--- Template Haskell hack to make the following $quickCheckAll work
--- under ghc-7.8.
-return [] -- KEEP!
-
--- | All tests as collected by 'quickCheckAll'.
---
--- Using 'quickCheckAll' is convenient and superior to the manual
--- enumeration of tests, since the name of the property is
--- added automatically.
-
-tests :: IO Bool
-tests = do
- putStrLn "Agda.Utils.PartialOrd"
- $quickCheckAll
-
--- tests' :: IO Bool
--- tests' = runTests "Agda.Utils.PartialOrd"
--- [ quickCheck' prop_comparable_related
--- , quickCheck' prop_oppPO
--- , quickCheck' prop_seqPO
--- , quickCheck' prop_assoc_seqPO
--- , quickCheck' prop_related_pair
--- ]
diff --git a/src/full/Agda/Utils/Permutation.hs b/src/full/Agda/Utils/Permutation.hs
index 87454ac..f87ce72 100644
--- a/src/full/Agda/Utils/Permutation.hs
+++ b/src/full/Agda/Utils/Permutation.hs
@@ -1,11 +1,5 @@
{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveDataTypeable #-}
-{-# LANGUAGE DeriveFoldable #-}
-{-# LANGUAGE DeriveFunctor #-}
-{-# LANGUAGE DeriveTraversable #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE TupleSections #-}
module Agda.Utils.Permutation where
@@ -22,8 +16,6 @@ import Data.Foldable (Foldable)
import Data.Traversable (Traversable)
import Data.Typeable (Typeable)
-import Test.QuickCheck
-
import Agda.Syntax.Position (KillRange(..))
import Agda.Utils.Functor
import Agda.Utils.List ((!!!))
@@ -256,17 +248,3 @@ instance DoDrop Permutation where
Perm (n + m) $ [0..m-1] ++ map (+ m) (List.drop k xs)
where m = -k
unDrop m = dropMore (-m) -- allow picking up more than dropped
-
-------------------------------------------------------------------------
--- * Test data generator
-------------------------------------------------------------------------
-
-instance Arbitrary Permutation where
- arbitrary = do
- is <- nub . map getNonNegative <$> arbitrary
- NonNegative n <- arbitrary
- return $ Perm (if null is then n else maximum is + n + 1) is
-
-------------------------------------------------------------------------
--- * Properties, see "Agda.Utils.Permutation.Tests".
-------------------------------------------------------------------------
diff --git a/src/full/Agda/Utils/Permutation/Tests.hs b/src/full/Agda/Utils/Permutation/Tests.hs
deleted file mode 100644
index 1bd4a59..0000000
--- a/src/full/Agda/Utils/Permutation/Tests.hs
+++ /dev/null
@@ -1,117 +0,0 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE DeriveDataTypeable #-}
-{-# LANGUAGE DeriveFoldable #-}
-{-# LANGUAGE DeriveFunctor #-}
-{-# LANGUAGE DeriveTraversable #-}
-{-# LANGUAGE TemplateHaskell #-}
-
-{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
-
-module Agda.Utils.Permutation.Tests (tests) where
-
-import Data.Functor
-import Data.List as List
-import Data.Maybe
-
-import Test.QuickCheck
-
-import Agda.Utils.List (downFrom)
-import Agda.Utils.Permutation
-
-------------------------------------------------------------------------
--- * Properties
-------------------------------------------------------------------------
-
-data ComposablePermutations = ComposablePermutations Permutation Permutation
- deriving (Eq, Show)
-
-instance Arbitrary ComposablePermutations where
- arbitrary = do
- p2@(Perm n is) <- arbitrary
- let m = length is
- p1 <- Perm m . filter (< m) . map getNonNegative <$> arbitrary
- return $ ComposablePermutations p1 p2
-
-type A = Int
-
--- | Extend a list by indefinitely many elements.
-withStream :: ([a] -> b) -- ^ Stream function.
- -> [a] -- ^ Initial segment.
- -> a -- ^ Default element, appended ad infinitum.
- -> b
-withStream k as a = k $ as ++ repeat a
-
--- | Apply a permutation to a list which might be too short.
--- Silently discard picks that go beyond the list's boundaries.
-permutePartial :: Permutation -> [a] -> [a]
-permutePartial perm xs =
- catMaybes $ permute perm $ map Just xs ++ repeat Nothing
- -- Note: we have to add @Nothing@s to make @permute@ total.
-
--- | @perm([0..n-1]) == perm@
-prop_permute_id_r :: Permutation -> Bool
-prop_permute_id_r perm@(Perm n picks) =
- permute perm [0..] == picks
-
--- | @idP(xs) == xs@
-prop_permute_id_l :: Int -> [A] -> A -> Bool
-prop_permute_id_l n = withStream $ \ xs ->
- permute (idP n) xs == take n xs
-
--- | @takeP n perm = perm . take n@
-prop_takeP :: Int -> Permutation -> [A] -> A -> Bool
-prop_takeP n perm = withStream $ \ xs ->
- permute (takeP n perm) xs == permutePartial perm (take n xs)
- -- Note: we have to add @Nothing@s to make @permute@ total.
-
--- | @(droppedP perm)(xs) = xs \\ perm(xs)@
-prop_droppedP :: Permutation -> [A] -> A -> Bool
-prop_droppedP perm@(Perm n _) = withStream $ \ xs -> let xs' = take n xs in
- sort (permute (droppedP perm) xs') == sort (xs' \\ permute perm xs')
-
--- | @(p1 ∘ p2)(xs) = p1(p2(xs))@
-prop_composeP :: ComposablePermutations -> [A] -> A -> Bool
-prop_composeP (ComposablePermutations p1 p2) = withStream $ \ xs ->
- permute (composeP p1 p2) xs == permutePartial p1 (permute p2 xs)
-
-prop_flipP :: Permutation -> Bool
-prop_flipP p = permPicks (flipP p) == permute p (downFrom $ permRange p)
-
--- | @p ∘ p⁻¹ ∘ p = p@
-prop_invertP_left :: Permutation -> Int -> [A] -> A -> Bool
-prop_invertP_left p err = withStream $ \ xs -> let ys = permute p xs in
- permute p (permute (invertP err p) ys) == ys
-
--- NOT QUITE RIGHT YET:
--- -- | @p⁻1 ∘ p ∘ p⁻¹ = p⁻¹@
--- prop_invertP_right :: Permutation -> Int -> [A] -> A -> Bool
--- prop_invertP_right p err = withStream $ \ xs ->
--- let pinv = invertP err p
--- ys = permute pinv xs
--- in permute pinv (permute p ys) == ys
-
--- | @reverseP p = reverse . p . reverse@
-prop_reverseP :: Permutation -> [A] -> A -> Bool
-prop_reverseP p@(Perm n _) = withStream $ \ xs0 -> let xs = take n xs0 in
- permute (reverseP p) xs == reverse (permute p (reverse xs))
-
--- | @permute p . inversePermute p = id@
-prop_inversePermute :: Permutation -> [Maybe A] -> Maybe A -> Bool
-prop_inversePermute p@(Perm _ is) = withStream $ \ xs0 ->
- let xs = take (length is) xs0
- ys = inversePermute p xs
- in permute p ys == xs
-
-prop_inversePermute_invertP :: Permutation -> Bool
-prop_inversePermute_invertP p =
- inversePermute p (id :: Int -> Int) == safePermute (invertP (-1) p) [(0::Int)..]
-
--- Template Haskell hack to make the following $quickCheckAll work
--- under ghc-7.8.
-return [] -- KEEP!
-
--- | All tests as collected by 'quickCheckAll'.
-tests :: IO Bool
-tests = do
- putStrLn "Agda.Utils.Permutation"
- $quickCheckAll
diff --git a/src/full/Agda/Utils/Pretty.hs b/src/full/Agda/Utils/Pretty.hs
index 4359cc1..ec84a48 100644
--- a/src/full/Agda/Utils/Pretty.hs
+++ b/src/full/Agda/Utils/Pretty.hs
@@ -1,5 +1,4 @@
{-# LANGUAGE CPP #-}
-{-# LANGUAGE FlexibleInstances #-}
{-| Pretty printing functions.
-}
@@ -77,3 +76,8 @@ align :: Int -> [(String, Doc)] -> Doc
align max rows =
vcat $ map (\(s, d) -> text s $$ nest (maxLen + 1) d) $ rows
where maxLen = maximum $ 0 : filter (< max) (map (length . fst) rows)
+
+-- | Handles strings with newlines properly (preserving indentation)
+multiLineText :: String -> Doc
+multiLineText = vcat . map text . lines
+
diff --git a/src/full/Agda/Utils/QuickCheck.hs b/src/full/Agda/Utils/QuickCheck.hs
deleted file mode 100644
index 137a43f..0000000
--- a/src/full/Agda/Utils/QuickCheck.hs
+++ /dev/null
@@ -1,16 +0,0 @@
-module Agda.Utils.QuickCheck
- ( module Test.QuickCheck
- , module Agda.Utils.QuickCheck
- ) where
-
-import Test.QuickCheck hiding ((===))
-
-isSuccess :: Result -> Bool
-isSuccess Success{} = True
-isSuccess _ = False
-
-quickCheck' :: Testable prop => prop -> IO Bool
-quickCheck' p = fmap isSuccess $ quickCheckResult p
-
-quickCheckWith' :: Testable prop => Args -> prop -> IO Bool
-quickCheckWith' args p = fmap isSuccess $ quickCheckWithResult args p
diff --git a/src/full/Agda/Utils/Singleton.hs b/src/full/Agda/Utils/Singleton.hs
index 8a9b9d9..ce8d235 100644
--- a/src/full/Agda/Utils/Singleton.hs
+++ b/src/full/Agda/Utils/Singleton.hs
@@ -1,7 +1,4 @@
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-- {-# LANGUAGE TypeFamilies #-}
-- | Constructing singleton collections.
diff --git a/src/full/Agda/Utils/Suffix.hs b/src/full/Agda/Utils/Suffix.hs
index 935d3d4..c27e8ea 100644
--- a/src/full/Agda/Utils/Suffix.hs
+++ b/src/full/Agda/Utils/Suffix.hs
@@ -1,5 +1,4 @@
{-# LANGUAGE CPP #-}
-{-# LANGUAGE PatternGuards #-}
module Agda.Utils.Suffix where
diff --git a/src/full/Agda/Utils/TestHelpers.hs b/src/full/Agda/Utils/TestHelpers.hs
deleted file mode 100644
index 9be85ee..0000000
--- a/src/full/Agda/Utils/TestHelpers.hs
+++ /dev/null
@@ -1,169 +0,0 @@
--- | Some functions and generators suitable for writing QuickCheck
--- properties.
-
-module Agda.Utils.TestHelpers
- ( -- * Algebraic properties
- associative
- , commutative
- , idempotent
- , isZero
- , identity
- , leftDistributive
- , rightDistributive
- , distributive
- -- * Generators
- , natural
- , positive
- , maybeGen
- , maybeCoGen
- , listOfElements
- , elementsUnlessEmpty
- , two
- , three
- -- * Test driver.
- , runTests
- )
- where
-
-import Control.Monad
-import Data.Functor
-import Test.QuickCheck
-
-------------------------------------------------------------------------
--- Algebraic properties
-
--- | Is the operator associative?
-
-associative :: Eq a
- => (a -> a -> a)
- -> a -> a -> a -> Bool
-associative (+) = \x y z ->
- x + (y + z) == (x + y) + z
-
--- | Is the operator commutative?
-
-commutative :: Eq a
- => (a -> a -> a)
- -> a -> a -> Bool
-commutative (+) = \x y ->
- x + y == y + x
-
--- | Is the operator idempotent?
-
-idempotent :: Eq a
- => (a -> a -> a)
- -> a -> Bool
-idempotent (/\) = \ x ->
- (x /\ x) == x
-
--- | Is the element a zero for the operator?
-
-isZero :: Eq a
- => a -> (a -> a -> a)
- -> a -> Bool
-isZero zer (*) = \x ->
- (zer * x == zer)
- &&
- (x * zer == zer)
-
--- | Is the element a unit for the operator?
-
-identity :: Eq a
- => a -> (a -> a -> a)
- -> a -> Bool
-identity one (*) = \x ->
- (one * x == x)
- &&
- (x * one == x)
-
--- | Does the first operator distribute (from the left) over the
--- second one?
-
-leftDistributive
- :: Eq a
- => (a -> a -> a) -> (a -> a -> a)
- -> a -> a -> a -> Bool
-leftDistributive (*) (+) = \x y z ->
- x * (y + z) == (x * y) + (x * z)
-
--- | Does the first operator distribute (from the right) over the
--- second one?
-
-rightDistributive
- :: Eq a
- => (a -> a -> a) -> (a -> a -> a)
- -> a -> a -> a -> Bool
-rightDistributive (*) (+) = \x y z ->
- (x + y) * z == (x * z) + (y * z)
-
--- | Does the first operator distribute over the second one?
-
-distributive
- :: Eq a
- => (a -> a -> a) -> (a -> a -> a)
- -> a -> a -> a -> Bool
-distributive (*) (+) = \ x y z ->
- leftDistributive (*) (+) x y z &&
- rightDistributive (*) (+) x y z
-
-------------------------------------------------------------------------
--- Generators
-
--- | Generates natural numbers.
-
-natural :: (Integral i) => Gen i
-natural = fromInteger . abs <$> arbitrary
-
--- | Generates positive numbers.
-
-positive :: (Integral i) => Gen i
-positive = succ <$> natural
-
--- | Generates a list of elements picked from a given list.
-listOfElements :: [a] -> Gen [a]
-listOfElements [] = return []
-listOfElements xs = listOf $ elements xs
-
--- | If the given list is non-empty, then an element from the list is
--- generated, and otherwise an arbitrary element is generated.
-
-elementsUnlessEmpty :: Arbitrary a => [a] -> Gen a
-elementsUnlessEmpty [] = arbitrary
-elementsUnlessEmpty xs = elements xs
-
--- | Generates values of 'Maybe' type, using the given generator to
--- generate the contents of the 'Just' constructor.
-
-maybeGen :: Gen a -> Gen (Maybe a)
-maybeGen gen = frequency [ (1, return Nothing)
- , (9, Just <$> gen)
- ]
-
--- | 'Coarbitrary' \"generator\" for 'Maybe'.
-
-maybeCoGen :: (a -> Gen b -> Gen b) -> (Maybe a -> Gen b -> Gen b)
-maybeCoGen f Nothing = variant 0
-maybeCoGen f (Just x) = variant 1 . f x
-
--- | Generates two elements.
-
-two :: Gen a -> Gen (a, a)
-two gen = liftM2 (,) gen gen
-
--- | Generates three elements.
-
-three :: Gen a -> Gen (a, a, a)
-three gen = liftM3 (,,) gen gen gen
-
-------------------------------------------------------------------------
--- Test driver
-
--- | Runs the tests, and returns 'True' if all tests were successful.
-
-runTests :: String -- ^ A label for the tests. Used for
- -- informational purposes.
- -> [IO Bool]
- -> IO Bool
-runTests name tests = do
- putStrLn name
- and <$> sequence tests
diff --git a/src/full/Agda/Utils/Trie.hs b/src/full/Agda/Utils/Trie.hs
index 66f7851..350a15a 100644
--- a/src/full/Agda/Utils/Trie.hs
+++ b/src/full/Agda/Utils/Trie.hs
@@ -1,9 +1,6 @@
{-# LANGUAGE CPP #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-{-# LANGUAGE PatternGuards #-}
-{-# LANGUAGE TemplateHaskell #-}
-{-# LANGUAGE TupleSections #-}
-- | Strict tries (based on "Data.Map.Strict" and "Agda.Utils.Maybe.Strict").
@@ -12,8 +9,7 @@ module Agda.Utils.Trie
, empty, singleton, everyPrefix, insert, insertWith, union, unionWith
, adjust, delete
, toList, toAscList
- , lookup, member, lookupPath
- , tests
+ , lookup, member, lookupPath, lookupTrie
) where
import Prelude hiding (null, lookup)
@@ -21,13 +17,11 @@ import qualified Prelude
import Data.Function
import Data.Functor
-import Data.List (nubBy, sortBy, isPrefixOf, inits)
+import Data.Foldable (Foldable)
import qualified Data.Maybe as Lazy
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
-import Test.QuickCheck
-
import qualified Agda.Utils.Maybe.Strict as Strict
import Agda.Utils.Null
@@ -35,7 +29,7 @@ import Agda.Utils.Null
--
-- With the strict 'Maybe' type, 'Trie' is also strict in 'v'.
data Trie k v = Trie !(Strict.Maybe v) !(Map k (Trie k v))
- deriving (Show, Eq)
+ deriving (Show, Eq, Functor, Foldable)
-- | Empty trie.
instance Null (Trie k v) where
@@ -127,64 +121,8 @@ lookupPath xs (Trie v cs) = case xs of
x : xs -> Strict.maybeToList v ++
maybe [] (lookupPath xs) (Map.lookup x cs)
--- Tests ------------------------------------------------------------------
-
-newtype Key = Key Int
- deriving (Eq, Ord)
-
-newtype Val = Val Int
- deriving (Eq)
-
-newtype Model = Model [([Key], Val)]
- deriving (Eq, Show)
-
-instance Show Key where
- show (Key x) = show x
-
-instance Show Val where
- show (Val x) = show x
-
-instance Arbitrary Key where
- arbitrary = elements $ map Key [1..2]
- shrink (Key x) = Key <$> shrink x
-
-instance Arbitrary Val where
- arbitrary = elements $ map Val [1..3]
- shrink (Val x) = Val <$> shrink x
-
-instance Arbitrary Model where
- arbitrary = Model <$> arbitrary
- shrink (Model xs) = Model <$> shrink xs
-
-modelToTrie :: Model -> Trie Key Val
-modelToTrie (Model xs) = foldr (uncurry insert) empty xs
-
-prop_lookup :: [Key] -> Model -> Bool
-prop_lookup ks m@(Model ksvs) =
- lookup ks (modelToTrie m) == Prelude.lookup ks ksvs
-
-modelPath :: [Key] -> Model -> [Val]
-modelPath ks (Model xs) =
- map snd
- $ sortBy (compare `on` length . fst)
- $ nubBy ((==) `on` fst)
- $ filter (flip isPrefixOf ks . fst) xs
-
-prop_path :: [Key] -> Model -> Property
-prop_path ks m =
- collect (length $ modelPath ks m) $
- lookupPath ks (modelToTrie m) == modelPath ks m
-
-prop_everyPrefix :: [Integer] -> Integer -> Bool
-prop_everyPrefix ks v =
- everyPrefix ks v ==
- foldr union empty [ singleton ks' v | ks' <- inits ks ]
-
-return []
-
--- | All tests.
+-- | Get the subtrie rooted at the given key.
+lookupTrie :: Ord k => [k] -> Trie k v -> Trie k v
+lookupTrie [] t = t
+lookupTrie (k : ks) (Trie _ cs) = maybe empty (lookupTrie ks) (Map.lookup k cs)
-tests :: IO Bool
-tests = do
- putStrLn "Agda.Utils.Trie"
- $quickCheckAll
diff --git a/src/full/Agda/Utils/Tuple.hs b/src/full/Agda/Utils/Tuple.hs
index f69f998..f5dfe31 100644
--- a/src/full/Agda/Utils/Tuple.hs
+++ b/src/full/Agda/Utils/Tuple.hs
@@ -1,8 +1,4 @@
-{-# LANGUAGE DeriveFunctor #-}
-{-# LANGUAGE DeriveFoldable #-}
-{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-{-# LANGUAGE TupleSections #-}
module Agda.Utils.Tuple where
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" []