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
, beginningOfFile
, tests
) where
import Data.Generics (Typeable, Data)
import Data.List
import Data.Function
import Data.Set (Set, (\\))
import qualified Data.Set as Set
import Data.Int
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 :: !Int32
, posLine :: !Int32
, posCol :: !Int32
}
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 -> Int32
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 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 (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 | genericLength s > iLength i = __IMPOSSIBLE__
| otherwise = i { iEnd = movePosByString (iStart i) s }
dropI :: String -> Interval -> Interval
dropI s i | genericLength 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
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 -> Set Int32
iPositions i = Set.fromList [posPos (iStart i) .. posPos (iEnd i)]
rPositions :: Range -> 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 i = iLength i >= 0
prop_startPos = positionInvariant . startPos
prop_noRange = rangeInvariant noRange
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 []) = 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)
prop_beginningOfFile r = rangeInvariant (beginningOfFile 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_beginningOfFile
, quickCheck' prop_intervalInSameFileAs
]