module Agda.Syntax.Position
(
Position(..)
, positionInvariant
, startPos
, movePos
, movePosByString
, backupPos
, Interval(..)
, intervalInvariant
, takeI
, dropI
, Range(..)
, rangeInvariant
, noRange
, posToRange
, rStart
, rEnd
, rangeToInterval
, continuous
, continuousPerLine
, HasRange(..)
, SetRange(..)
, KillRange(..)
, killRange1, killRange2, killRange3, killRange4, killRange5, killRange6, killRange7
, withRangeOf
, fuseRange
, fuseRanges
, beginningOf
, tests
) where
import Data.Generics (Data, Typeable)
import Data.List
import Data.Function
import Data.Set (Set, (\\))
import qualified Data.Set as Set
import Agda.Utils.QuickCheck
import Control.Applicative
import Control.Monad
import Agda.Utils.FileName hiding (tests)
import Agda.Utils.TestHelpers
#include "../undefined.h"
import Agda.Utils.Impossible
data Position = Pn { srcFile :: Maybe AbsolutePath
, posPos :: !Int
, posLine :: !Int
, posCol :: !Int
}
deriving (Typeable, Data)
positionInvariant :: Position -> Bool
positionInvariant p =
posPos p > 0 && posLine p > 0 && posCol p > 0
importantPart p = (srcFile p, posPos p)
instance Eq Position where
(==) = (==) `on` importantPart
instance Ord Position where
compare = compare `on` importantPart
data Interval = Interval { iStart, iEnd :: !Position }
deriving (Typeable, Data, Eq, Ord)
intervalInvariant :: Interval -> Bool
intervalInvariant i =
all positionInvariant [iStart i, iEnd i] &&
iStart i <= iEnd i
iLength :: Interval -> Int
iLength i = posPos (iEnd i) posPos (iStart i)
newtype Range = Range [Interval]
deriving (Typeable, Data, Eq, Ord)
rangeInvariant :: Range -> Bool
rangeInvariant (Range []) = True
rangeInvariant (Range is) =
all intervalInvariant is &&
and (zipWith (<) (map iEnd $ init is) (map iStart $ tail is))
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 (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 :: a -> a
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)
instance KillRange Range where
killRange _ = noRange
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 (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 Position where
show (Pn Nothing _ l c) = show l ++ "," ++ show c
show (Pn (Just f) _ l c) = filePath f ++ ":" ++ show l ++ "," ++ show c
instance Show Interval 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 -> filePath f ++ ":"
start = show sl ++ "," ++ show sc
end
| sl == el = show ec
| otherwise = show el ++ "," ++ show ec
instance Show Range where
show r = case rangeToInterval r of
Nothing -> ""
Just i -> show i
startPos :: Maybe AbsolutePath -> Position
startPos f = Pn { srcFile = f, posPos = 1, posLine = 1, posCol = 1 }
noRange :: Range
noRange = Range []
movePos :: Position -> Char -> Position
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 -> String -> Position
movePosByString = foldl' movePos
backupPos :: Position -> Position
backupPos (Pn f p l c) = Pn f (p 1) l (c 1)
takeI :: String -> Interval -> Interval
takeI s i | length s > iLength i = __IMPOSSIBLE__
| otherwise = i { iEnd = movePosByString (iStart i) s }
dropI :: String -> Interval -> Interval
dropI s i | length s > iLength i = __IMPOSSIBLE__
| otherwise = i { iStart = movePosByString (iStart i) s }
posToRange :: Position -> Position -> Range
posToRange p1 p2 | p1 < p2 = Range [Interval p1 p2]
| otherwise = Range [Interval p2 p1]
rangeToInterval :: Range -> Maybe Interval
rangeToInterval (Range []) = Nothing
rangeToInterval (Range is) = Just $ Interval { iStart = iStart (head is)
, iEnd = iEnd (last is)
}
continuous :: Range -> Range
continuous r = case rangeToInterval r of
Nothing -> Range []
Just i -> Range [i]
continuousPerLine :: Range -> Range
continuousPerLine (Range []) = Range []
continuousPerLine (Range (i:is)) = Range $ fuse i $ sortBy (compare `on` iStart) 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 -> Maybe Position
rStart r = iStart <$> rangeToInterval r
rEnd :: Range -> Maybe Position
rEnd r = iEnd <$> rangeToInterval r
fuseIntervals :: Interval -> Interval -> Interval
fuseIntervals x y = Interval { iStart = head ps, iEnd = last ps }
where ps = sort [iStart x, iStart y, iEnd x, iEnd y]
fuseRanges :: Range -> Range -> Range
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
Just pos -> Range [Interval { iStart = pos, iEnd = pos }]
Nothing -> noRange
withRangeOf :: (SetRange t, HasRange u) => t -> u -> t
x `withRangeOf` y = setRange (getRange y) x
iPositions :: Interval -> Set Int
iPositions i = Set.fromList [posPos (iStart i) .. posPos (iEnd i)]
rPositions :: Range -> Set Int
rPositions (Range is) = Set.unions (map iPositions is)
makeInterval :: Set Int -> Set Int
makeInterval s
| Set.null s = Set.empty
| otherwise = Set.fromList [Set.findMin s .. Set.findMax s]
prop_iLength i = iLength i >= 0
prop_startPos = positionInvariant . startPos
prop_noRange = rangeInvariant noRange
prop_takeI_dropI i =
forAll (choose (0, iLength i)) $ \n ->
let s = replicate n ' '
t = takeI s i
d = dropI s i
in
intervalInvariant t &&
intervalInvariant d &&
fuseIntervals t d == i
prop_rangeToInterval (Range []) = True
prop_rangeToInterval r =
intervalInvariant i &&
iPositions i == makeInterval (rPositions r)
where Just i = rangeToInterval r
prop_continuous r =
rangeInvariant cr &&
rPositions cr == makeInterval (rPositions r)
where cr = continuous r
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 r = rangeInvariant (beginningOf r)
instance Arbitrary Position where
arbitrary = do
srcFile <- arbitrary
NonZero (NonNegative 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 :: Maybe AbsolutePath -> Interval -> Interval
setFile f (Interval p1 p2) =
Interval (p1 { srcFile = f }) (p2 { srcFile = f })
intervalInSameFileAs i = setFile (srcFile $ iStart i) <$> arbitrary
prop_intervalInSameFileAs i =
forAll (intervalInSameFileAs i) $ \i' ->
intervalInvariant i' &&
srcFile (iStart i) == srcFile (iStart i')
instance Arbitrary Interval where
arbitrary = do
(p1, p2) <- liftM2 (,) arbitrary arbitrary
let [p1', p2'] = sort [p1, p2 { srcFile = srcFile p1 }]
return (Interval p1' p2')
instance Arbitrary Range 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
tests :: IO Bool
tests = runTests "Agda.Syntax.Position"
[ quickCheck' positionInvariant
, quickCheck' intervalInvariant
, quickCheck' rangeInvariant
, quickCheck' prop_iLength
, quickCheck' prop_startPos
, quickCheck' prop_noRange
, quickCheck' prop_takeI_dropI
, quickCheck' prop_rangeToInterval
, quickCheck' prop_continuous
, quickCheck' prop_fuseIntervals
, quickCheck' prop_fuseRanges
, quickCheck' prop_beginningOf
, quickCheck' prop_intervalInSameFileAs
]