#if __GLASGOW_HASKELL__ <= 700
#endif
module Agda.Syntax.Position
(
Position
, Position'(..)
, positionInvariant
, startPos
, movePos
, movePosByString
, backupPos
, Interval
, Interval'(..)
, intervalInvariant
, takeI
, dropI
, Range
, Range'(..)
, rangeInvariant
, rightMargin
, noRange
, posToRange
, rStart
, rEnd
, rangeToInterval
, continuous
, continuousPerLine
, HasRange(..)
, SetRange(..)
, KillRange(..)
, KillRangeT
, killRange1, killRange2, killRange3, killRange4, killRange5, killRange6, killRange7
, killRange8, killRange9, killRange10, killRange11, killRange12, killRange13, killRange14
, killRange15, killRange16, killRange17, killRange18, killRange19
, withRangeOf
, fuseRange
, fuseRanges
, beginningOf
, beginningOfFile
, tests
) where
import Prelude hiding (null)
import Control.Applicative
import Control.Monad
import Data.Foldable (Foldable)
import Data.Function
import Data.Int
import Data.List hiding (null)
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Traversable (Traversable)
import Data.Typeable (Typeable)
import Test.QuickCheck.All
import Agda.Utils.FileName hiding (tests)
import Agda.Utils.Maybe
import Agda.Utils.Null
import Agda.Utils.Pretty ( (<>), Pretty(pretty) )
import Agda.Utils.TestHelpers
import Agda.Utils.QuickCheck
#include "undefined.h"
import Agda.Utils.Impossible
data Position' a = Pn
{ srcFile :: a
, posPos :: !Int32
, posLine :: !Int32
, posCol :: !Int32
}
deriving (Typeable, Functor, Foldable, Traversable)
positionInvariant :: Position' a -> Bool
positionInvariant p =
posPos p > 0 && posLine p > 0 && posCol p > 0
importantPart :: Position' a -> (a, Int32)
importantPart p = (srcFile p, posPos p)
instance Eq a => Eq (Position' a) where
(==) = (==) `on` importantPart
instance Ord a => Ord (Position' a) where
compare = compare `on` importantPart
type SrcFile = Maybe AbsolutePath
type Position = Position' SrcFile
data Interval' a = Interval { iStart, iEnd :: !(Position' a) }
deriving (Typeable, Eq, Ord, Functor, Foldable, Traversable)
type Interval = Interval' SrcFile
intervalInvariant :: Ord a => Interval' a -> Bool
intervalInvariant i =
all positionInvariant [iStart i, iEnd i] &&
iStart i <= iEnd i
iLength :: Interval' a -> Int32
iLength i = posPos (iEnd i) posPos (iStart i)
newtype Range' a = Range [Interval' a]
deriving (Typeable, Eq, Ord, Functor, Foldable, Traversable, Null)
type Range = Range' SrcFile
rangeInvariant :: Range -> Bool
rangeInvariant (Range []) = True
rangeInvariant (Range is) =
all intervalInvariant is &&
and (zipWith (<) (map iEnd $ init is) (map iStart $ tail is))
rightMargin :: Range -> Range
rightMargin r@(Range is) =
if null is then r else
let i = last is in Range [ i { iStart = iEnd i } ]
class HasRange t where
getRange :: t -> Range
instance HasRange Interval where
getRange i = Range [i]
instance HasRange Range where
getRange = id
instance HasRange a => HasRange [a] where
getRange = foldr fuseRange noRange
instance (HasRange a, HasRange b) => HasRange (a,b) where
getRange = uncurry fuseRange
instance (HasRange a, HasRange b, HasRange c) => HasRange (a,b,c) where
getRange (x,y,z) = getRange (x,(y,z))
instance (HasRange a, HasRange b, HasRange c, HasRange d) => HasRange (a,b,c,d) where
getRange (x,y,z,w) = getRange (x,(y,(z,w)))
instance (HasRange a, HasRange b, HasRange c, HasRange d, HasRange e) => HasRange (a,b,c,d,e) where
getRange (x,y,z,w,v) = getRange (x,(y,(z,(w,v))))
instance (HasRange a, HasRange b, HasRange c, HasRange d, HasRange e, HasRange f) => HasRange (a,b,c,d,e,f) where
getRange (x,y,z,w,v,u) = getRange (x,(y,(z,(w,(v,u)))))
instance (HasRange a, HasRange b, HasRange c, HasRange d, HasRange e, HasRange f, HasRange g) => HasRange (a,b,c,d,e,f,g) where
getRange (x,y,z,w,v,u,t) = getRange (x,(y,(z,(w,(v,(u,t))))))
instance HasRange a => HasRange (Maybe a) where
getRange Nothing = noRange
getRange (Just a) = getRange a
class HasRange t => SetRange t where
setRange :: Range -> t -> t
instance SetRange Range where
setRange = const
class KillRange a where
killRange :: KillRangeT a
type KillRangeT a = a -> a
killRange1 :: KillRange a => (a -> b) -> a -> b
killRange2 :: (KillRange a, KillRange b) => (a -> b -> c) -> a -> b -> c
killRange3 :: (KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange4 :: (KillRange a, KillRange b, KillRange c, KillRange d) =>
(a -> b -> c -> d -> e) -> a -> b -> c -> d -> e
killRange5 :: ( KillRange a, KillRange b, KillRange c, KillRange d
, KillRange e ) =>
(a -> b -> c -> d -> e -> f) -> a -> b -> c -> d -> e -> f
killRange6 :: ( KillRange a, KillRange b, KillRange c, KillRange d
, KillRange e, KillRange f ) =>
(a -> b -> c -> d -> e -> f -> g) -> a -> b -> c -> d -> e -> f -> g
killRange7 :: ( KillRange a, KillRange b, KillRange c, KillRange d
, KillRange e, KillRange f, KillRange g ) =>
(a -> b -> c -> d -> e -> f -> g -> h) -> a -> b -> c -> d -> e -> f -> g -> h
killRange8 :: ( KillRange a, KillRange b, KillRange c, KillRange d
, KillRange e, KillRange f, KillRange g, KillRange h ) =>
(a -> b -> c -> d -> e -> f -> g -> h -> i) ->
a -> b -> c -> d -> e -> f -> g -> h -> i
killRange9 :: ( KillRange a, KillRange b, KillRange c, KillRange d
, KillRange e, KillRange f, KillRange g, KillRange h
, KillRange i ) =>
(a -> b -> c -> d -> e -> f -> g -> h -> i -> j) ->
a -> b -> c -> d -> e -> f -> g -> h -> i -> j
killRange10 :: ( KillRange a, KillRange b, KillRange c, KillRange d
, KillRange e, KillRange f, KillRange g, KillRange h
, KillRange i, KillRange j ) =>
(a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k) ->
a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k
killRange11 :: ( KillRange a, KillRange b, KillRange c, KillRange d
, KillRange e, KillRange f, KillRange g, KillRange h
, KillRange i, KillRange j, KillRange k ) =>
(a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l) ->
a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l
killRange12 :: ( KillRange a, KillRange b, KillRange c, KillRange d
, KillRange e, KillRange f, KillRange g, KillRange h
, KillRange i, KillRange j, KillRange k, KillRange l ) =>
(a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m) ->
a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m
killRange13 :: ( KillRange a, KillRange b, KillRange c, KillRange d
, KillRange e, KillRange f, KillRange g, KillRange h
, KillRange i, KillRange j, KillRange k, KillRange l
, KillRange m ) =>
(a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n) ->
a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n
killRange14 :: ( KillRange a, KillRange b, KillRange c, KillRange d
, KillRange e, KillRange f, KillRange g, KillRange h
, KillRange i, KillRange j, KillRange k, KillRange l
, KillRange m, KillRange n ) =>
(a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o) ->
a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o
killRange15 :: ( KillRange a, KillRange b, KillRange c, KillRange d
, KillRange e, KillRange f, KillRange g, KillRange h
, KillRange i, KillRange j, KillRange k, KillRange l
, KillRange m, KillRange n, KillRange o ) =>
(a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p) ->
a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p
killRange16 :: ( KillRange a, KillRange b, KillRange c, KillRange d
, KillRange e, KillRange f, KillRange g, KillRange h
, KillRange i, KillRange j, KillRange k, KillRange l
, KillRange m, KillRange n, KillRange o, KillRange p ) =>
(a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> q) ->
a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> q
killRange17 :: ( KillRange a, KillRange b, KillRange c, KillRange d
, KillRange e, KillRange f, KillRange g, KillRange h
, KillRange i, KillRange j, KillRange k, KillRange l
, KillRange m, KillRange n, KillRange o, KillRange p
, KillRange q ) =>
(a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> q -> r) ->
a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> q -> r
killRange18 :: ( KillRange a, KillRange b, KillRange c, KillRange d
, KillRange e, KillRange f, KillRange g, KillRange h
, KillRange i, KillRange j, KillRange k, KillRange l
, KillRange m, KillRange n, KillRange o, KillRange p
, KillRange q, KillRange r ) =>
(a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> q -> r -> s) ->
a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> q -> r -> s
killRange19 :: ( KillRange a, KillRange b, KillRange c, KillRange d
, KillRange e, KillRange f, KillRange g, KillRange h
, KillRange i, KillRange j, KillRange k, KillRange l
, KillRange m, KillRange n, KillRange o, KillRange p
, KillRange q, KillRange r, KillRange s ) =>
(a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> q -> r -> s -> t) ->
a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> q -> r -> s -> t
killRange1 f a = f (killRange a)
killRange2 f a = killRange1 (f $ killRange a)
killRange3 f a = killRange2 (f $ killRange a)
killRange4 f a = killRange3 (f $ killRange a)
killRange5 f a = killRange4 (f $ killRange a)
killRange6 f a = killRange5 (f $ killRange a)
killRange7 f a = killRange6 (f $ killRange a)
killRange8 f a = killRange7 (f $ killRange a)
killRange9 f a = killRange8 (f $ killRange a)
killRange10 f a = killRange9 (f $ killRange a)
killRange11 f a = killRange10 (f $ killRange a)
killRange12 f a = killRange11 (f $ killRange a)
killRange13 f a = killRange12 (f $ killRange a)
killRange14 f a = killRange13 (f $ killRange a)
killRange15 f a = killRange14 (f $ killRange a)
killRange16 f a = killRange15 (f $ killRange a)
killRange17 f a = killRange16 (f $ killRange a)
killRange18 f a = killRange17 (f $ killRange a)
killRange19 f a = killRange18 (f $ killRange a)
instance KillRange Range where
killRange _ = noRange
instance KillRange () where
killRange = id
instance KillRange Bool where
killRange = id
instance KillRange Int where
killRange = id
instance KillRange a => KillRange [a] where
killRange = map killRange
instance (KillRange a, KillRange b) => KillRange (a, b) where
killRange (x, y) = (killRange x, killRange y)
instance (KillRange a, KillRange b, KillRange c) =>
KillRange (a, b, c) where
killRange (x, y, z) = killRange3 (,,) x y z
instance KillRange a => KillRange (Maybe a) where
killRange = fmap killRange
instance (KillRange a, KillRange b) => KillRange (Either a b) where
killRange (Left x) = Left $ killRange x
killRange (Right x) = Right $ killRange x
instance Show a => Show (Position' (Maybe a)) where
show (Pn Nothing _ l c) = show l ++ "," ++ show c
show (Pn (Just f) _ l c) = show f ++ ":" ++ show l ++ "," ++ show c
instance Show a => Show (Interval' (Maybe a)) where
show (Interval s e) = file ++ start ++ "-" ++ end
where
f = srcFile s
sl = posLine s
el = posLine e
sc = posCol s
ec = posCol e
file = case f of
Nothing -> ""
Just f -> show f ++ ":"
start = show sl ++ "," ++ show sc
end
| sl == el = show ec
| otherwise = show el ++ "," ++ show ec
instance Show a => Show (Range' (Maybe a)) where
show r = case rangeToInterval r of
Nothing -> ""
Just i -> show i
instance Pretty a => Pretty (Position' (Maybe a)) where
pretty (Pn Nothing _ l c) = pretty l <> pretty "," <> pretty c
pretty (Pn (Just f) _ l c) =
pretty f <> pretty ":" <> pretty l <> pretty "," <> pretty c
startPos :: Maybe AbsolutePath -> Position
startPos f = Pn { srcFile = f, posPos = 1, posLine = 1, posCol = 1 }
noRange :: Range' a
noRange = Range []
movePos :: Position' a -> Char -> Position' a
movePos (Pn f p l c) '\n' = Pn f (p + 1) (l + 1) 1
movePos (Pn f p l c) _ = Pn f (p + 1) l (c + 1)
movePosByString :: Position' a -> String -> Position' a
movePosByString = foldl' movePos
backupPos :: Position' a -> Position' a
backupPos (Pn f p l c) = Pn f (p 1) l (c 1)
takeI :: String -> Interval' a -> Interval' a
takeI s i | genericLength s > iLength i = __IMPOSSIBLE__
| otherwise = i { iEnd = movePosByString (iStart i) s }
dropI :: String -> Interval' a -> Interval' a
dropI s i | genericLength s > iLength i = __IMPOSSIBLE__
| otherwise = i { iStart = movePosByString (iStart i) s }
posToRange :: Ord a => Position' a -> Position' a -> Range' a
posToRange p1 p2 | p1 < p2 = Range [Interval p1 p2]
| otherwise = Range [Interval p2 p1]
rangeToInterval :: Range' a -> Maybe (Interval' a)
rangeToInterval (Range []) = Nothing
rangeToInterval (Range is) = Just $ Interval { iStart = iStart (head is)
, iEnd = iEnd (last is)
}
continuous :: Range' a -> Range' a
continuous r = case rangeToInterval r of
Nothing -> Range []
Just i -> Range [i]
continuousPerLine :: Ord a => Range' a -> Range' a
continuousPerLine (Range []) = Range []
continuousPerLine (Range (i:is)) = Range $ fuse i is
where
fuse i [] = [i]
fuse i (j:is)
| sameLine i j = fuse (fuseIntervals i j) is
| otherwise = i : fuse j is
sameLine i j = posLine (iEnd i) == posLine (iStart j)
rStart :: Range' a -> Maybe (Position' a)
rStart r = iStart <$> rangeToInterval r
rEnd :: Range' a -> Maybe (Position' a)
rEnd r = iEnd <$> rangeToInterval r
fuseIntervals :: Ord a => Interval' a -> Interval' a -> Interval' a
fuseIntervals x y = Interval { iStart = head ps, iEnd = last ps }
where ps = sort [iStart x, iStart y, iEnd x, iEnd y]
fuseRanges :: (Ord a) => Range' a -> Range' a -> Range' a
fuseRanges (Range is) (Range js) = Range (helper is js)
where
helper [] js = js
helper is [] = is
helper (i:is) (j:js)
| iEnd i < iStart j = i : helper is (j:js)
| iEnd j < iStart i = j : helper (i:is) js
| iEnd i < iEnd j = helper is (fuseIntervals i j : js)
| otherwise = helper (fuseIntervals i j : is) js
fuseRange :: (HasRange u, HasRange t) => u -> t -> Range
fuseRange x y = fuseRanges (getRange x) (getRange y)
beginningOf :: Range -> Range
beginningOf r = case rStart r of
Nothing -> noRange
Just pos -> posToRange pos pos
beginningOfFile :: Range -> Range
beginningOfFile r = case rStart r of
Nothing -> noRange
Just (Pn { srcFile = f }) -> posToRange p p
where p = startPos f
withRangeOf :: (SetRange t, HasRange u) => t -> u -> t
x `withRangeOf` y = setRange (getRange y) x
iPositions :: Interval' a -> Set Int32
iPositions i = Set.fromList [posPos (iStart i) .. posPos (iEnd i)]
rPositions :: Range' a -> Set Int32
rPositions (Range is) = Set.unions (map iPositions is)
makeInterval :: Set Int32 -> Set Int32
makeInterval s
| Set.null s = Set.empty
| otherwise = Set.fromList [Set.findMin s .. Set.findMax s]
prop_iLength :: Interval' Integer -> Bool
prop_iLength i = iLength i >= 0
prop_startPos :: Maybe AbsolutePath -> Bool
prop_startPos = positionInvariant . startPos
prop_noRange :: Bool
prop_noRange = rangeInvariant noRange
prop_takeI_dropI :: Interval' Integer -> Property
prop_takeI_dropI i =
forAll (choose (0, toInteger $ iLength i)) $ \n ->
let s = genericReplicate n ' '
t = takeI s i
d = dropI s i
in
intervalInvariant t &&
intervalInvariant d &&
fuseIntervals t d == i
prop_rangeToInterval :: Range' Integer -> Bool
prop_rangeToInterval (Range []) = True
prop_rangeToInterval r =
intervalInvariant i &&
iPositions i == makeInterval (rPositions r)
where Just i = rangeToInterval r
prop_continuous :: Range -> Bool
prop_continuous r =
rangeInvariant cr &&
rPositions cr == makeInterval (rPositions r)
where cr = continuous r
prop_fuseIntervals :: Interval' Integer -> Property
prop_fuseIntervals i1 =
forAll (intervalInSameFileAs i1) $ \i2 ->
let i = fuseIntervals i1 i2 in
intervalInvariant i &&
iPositions i ==
makeInterval (Set.union (iPositions i1) (iPositions i2))
prop_fuseRanges :: Range -> Range -> Bool
prop_fuseRanges r1 r2 =
rangeInvariant r &&
rPositions r == Set.union (rPositions r1) (rPositions r2)
where r = fuseRanges r1 r2
prop_beginningOf :: Range -> Bool
prop_beginningOf r = rangeInvariant (beginningOf r)
prop_beginningOfFile :: Range -> Bool
prop_beginningOfFile r = rangeInvariant (beginningOfFile r)
instance Arbitrary a => Arbitrary (Position' a) where
arbitrary = do
srcFile <- arbitrary
Positive pos' <- arbitrary
let pos = fromInteger pos'
line = pred pos `div` 10 + 1
col = pred pos `mod` 10 + 1
return (Pn {srcFile = srcFile, posPos = pos,
posLine = line, posCol = col })
setFile :: a -> Interval' a -> Interval' a
setFile f (Interval p1 p2) =
Interval (p1 { srcFile = f }) (p2 { srcFile = f })
intervalInSameFileAs :: Interval' Integer -> Gen (Interval' Integer)
intervalInSameFileAs i = setFile (srcFile $ iStart i) <$> arbitrary
prop_intervalInSameFileAs :: Interval' Integer -> Property
prop_intervalInSameFileAs i =
forAll (intervalInSameFileAs i) $ \i' ->
intervalInvariant i' &&
srcFile (iStart i) == srcFile (iStart i')
instance (Arbitrary a, Ord a) => Arbitrary (Interval' a) where
arbitrary = do
(p1, p2 :: Position' a) <- liftM2 (,) arbitrary arbitrary
let [p1', p2'] = sort [p1, p2 { srcFile = srcFile p1 }]
return (Interval p1' p2')
instance (Ord a, Arbitrary a) => Arbitrary (Range' a) where
arbitrary = Range . fuse . sort . fixFiles <$> arbitrary
where
fixFiles [] = []
fixFiles (i : is) = i : map (setFile $ srcFile $ iStart i) is
fuse (i1 : i2 : is)
| iEnd i1 >= iStart i2 = fuse (fuseIntervals i1 i2 : is)
| otherwise = i1 : fuse (i2 : is)
fuse is = is
prop_positionInvariant :: Position' Integer -> Bool
prop_positionInvariant = positionInvariant
prop_intervalInvariant :: Interval' Integer -> Bool
prop_intervalInvariant = intervalInvariant
prop_rangeInvariant :: Range -> Bool
prop_rangeInvariant = rangeInvariant
instance Show (Position' Integer) where show = show . fmap Just
instance Show (Interval' Integer) where show = show . fmap Just
instance Show (Range' Integer) where show = show . fmap Just
return []
tests :: IO Bool
tests = do
putStrLn "Agda.Syntax.Position"
$quickCheckAll