#if __GLASGOW_HASKELL__ <= 708
#endif
module Agda.Syntax.Position
(
Position
, PositionWithoutFile
, Position'(..)
, SrcFile
, positionInvariant
, startPos
, movePos
, movePosByString
, backupPos
, Interval
, IntervalWithoutFile
, Interval'(..)
, intervalInvariant
, posToInterval
, takeI
, dropI
, Range
, Range'
, rangeInvariant
, consecutiveAndSeparated
, intervalsToRange
, rangeIntervals
, rangeFile
, rightMargin
, noRange
, posToRange, posToRange'
, rStart, rStart'
, rEnd, rEnd'
, rangeToInterval
, continuous
, continuousPerLine
, PrintRange(..)
, HasRange(..)
, SetRange(..)
, KillRange(..)
, KillRangeT
, killRangeMap
, 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 hiding (empty)
import Control.Monad
import Data.Foldable (Foldable)
import qualified Data.Foldable as Fold
import Data.Function
import Data.Int
import Data.List hiding (null)
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Traversable (Traversable)
import Data.Typeable (Typeable)
import Data.Sequence (Seq)
import qualified Data.Sequence as Seq
import Data.Void
import GHC.Generics (Generic)
import Test.QuickCheck.All
import Agda.Utils.FileName hiding (tests)
import Agda.Utils.List hiding (tests)
import qualified Agda.Utils.Maybe.Strict as Strict
import Agda.Utils.Null
import Agda.Utils.Pretty
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, Generic)
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 = Strict.Maybe AbsolutePath
type Position = Position' SrcFile
type PositionWithoutFile = Position' ()
data Interval' a = Interval { iStart, iEnd :: !(Position' a) }
deriving (Typeable, Eq, Ord, Functor, Foldable, Traversable, Generic)
type Interval = Interval' SrcFile
type IntervalWithoutFile = Interval' ()
intervalInvariant :: Ord a => Interval' a -> Bool
intervalInvariant i =
all positionInvariant [iStart i, iEnd i]
&&
iStart i <= iEnd i
&&
srcFile (iStart i) == srcFile (iEnd i)
setIntervalFile :: a -> Interval' b -> Interval' a
setIntervalFile f (Interval p1 p2) =
Interval (p1 { srcFile = f }) (p2 { srcFile = f })
posToInterval ::
a -> PositionWithoutFile -> PositionWithoutFile -> Interval' a
posToInterval f p1 p2 = setIntervalFile f $
if p1 < p2
then Interval p1 p2
else Interval p2 p1
iLength :: Interval' a -> Int32
iLength i = posPos (iEnd i) posPos (iStart i)
data Range' a
= NoRange
| Range !a (Seq IntervalWithoutFile)
deriving
(Typeable, Eq, Ord, Functor, Foldable, Traversable, Generic)
type Range = Range' SrcFile
instance Null (Range' a) where
null NoRange = True
null Range{} = False
empty = NoRange
rangeIntervals :: Range' a -> [IntervalWithoutFile]
rangeIntervals NoRange = []
rangeIntervals (Range _ is) = Fold.toList is
intervalsToRange :: a -> [IntervalWithoutFile] -> Range' a
intervalsToRange _ [] = NoRange
intervalsToRange f is = Range f (Seq.fromList is)
consecutiveAndSeparated :: Ord a => [Interval' a] -> Bool
consecutiveAndSeparated is =
all intervalInvariant is
&&
allEqual (map (srcFile . iStart) is)
&&
(null is
||
and (zipWith (<) (map iEnd (init is))
(map iStart (tail is))))
rangeInvariant :: Ord a => Range' a -> Bool
rangeInvariant r =
consecutiveAndSeparated (rangeIntervals r)
&&
case r of
Range _ is -> not (null is)
NoRange -> True
rangeFile :: Range -> SrcFile
rangeFile NoRange = Strict.Nothing
rangeFile (Range f _) = f
rightMargin :: Range -> Range
rightMargin r@NoRange = r
rightMargin r@(Range f is) = case Seq.viewr is of
Seq.EmptyR -> __IMPOSSIBLE__
_ Seq.:> i -> intervalToRange f (i { iStart = iEnd i })
newtype PrintRange a = PrintRange a
deriving (Eq, Ord, HasRange, SetRange, KillRange)
class HasRange t where
getRange :: t -> Range
instance HasRange Interval where
getRange i =
intervalToRange (srcFile (iStart i))
(setIntervalFile () i)
instance HasRange Range where
getRange = id
instance HasRange Bool where
getRange _ = noRange
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
instance (HasRange a, HasRange b) => HasRange (Either a b) where
getRange = either getRange getRange
class HasRange t => SetRange t where
setRange :: Range -> t -> t
instance SetRange Range where
setRange = const
instance SetRange a => SetRange [a] where
setRange r = fmap $ setRange r
class KillRange a where
killRange :: KillRangeT a
type KillRangeT a = a -> a
killRangeMap :: (KillRange k, KillRange v) => KillRangeT (Map k v)
killRangeMap = Map.mapKeysMonotonic killRange . Map.map killRange
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 Void where
killRange = id
instance KillRange () where
killRange = id
instance KillRange Bool where
killRange = id
instance KillRange Int where
killRange = id
instance KillRange Integer where
killRange = id
#if __GLASGOW_HASKELL__ >= 710
instance KillRange a => KillRange [a] where
#else
instance KillRange a => KillRange [a] where
#endif
killRange = map killRange
#if __GLASGOW_HASKELL__ >= 710
instance KillRange String where
#else
instance KillRange String where
#endif
killRange = id
#if __GLASGOW_HASKELL__ >= 710
instance KillRange a => KillRange (Map k a) where
#else
instance KillRange a => KillRange (Map k a) where
#endif
killRange = fmap killRange
#if __GLASGOW_HASKELL__ >= 710
instance (Ord a, KillRange a) => KillRange (Set a) where
#else
instance (Ord a, KillRange a) => KillRange (Set a) where
#endif
killRange = Set.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 b, KillRange c, KillRange d) =>
KillRange (a, b, c, d) where
killRange (x, y, z, u) = killRange4 (,,,) x y z u
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' (Strict.Maybe a)) where
show (Pn (Strict.Just f) _ l c) = show f ++ ":" ++
show l ++ "," ++ show c
show (Pn Strict.Nothing _ l c) = show l ++ "," ++ show c
instance Show PositionWithoutFile where
show p = show (p { srcFile = Strict.Nothing } :: Position)
instance Show IntervalWithoutFile where
show (Interval s e) = start ++ "-" ++ end
where
sl = posLine s
el = posLine e
sc = posCol s
ec = posCol e
start :: String
start = show sl ++ "," ++ show sc
end :: String
end | sl == el = show ec
| otherwise = show el ++ "," ++ show ec
instance Show a => Show (Interval' (Strict.Maybe a)) where
show i@(Interval s _) = file ++ show (setIntervalFile () i)
where
file :: String
file = case srcFile s of
Strict.Nothing -> ""
Strict.Just f -> show f ++ ":"
instance Show a => Show (Range' (Strict.Maybe a)) where
show r = case rangeToIntervalWithFile r of
Nothing -> ""
Just i -> show i
instance Show a => Show (Range' (Maybe a)) where
show = show . fmap Strict.toStrict
instance Pretty a => Pretty (Position' (Strict.Maybe a)) where
pretty (Pn Strict.Nothing _ l c) = pretty l <> pretty "," <> pretty c
pretty (Pn (Strict.Just f) _ l c) =
pretty f <> pretty ":" <> pretty l <> pretty "," <> pretty c
instance Pretty PositionWithoutFile where
pretty p = pretty (p { srcFile = Strict.Nothing } :: Position)
instance Pretty IntervalWithoutFile where
pretty (Interval s e) = start <> pretty "-" <> end
where
sl = posLine s
el = posLine e
sc = posCol s
ec = posCol e
start :: Doc
start = pretty sl <> comma <> pretty sc
end :: Doc
| sl == el = pretty ec
| otherwise = pretty el <> comma <> pretty ec
instance Pretty a => Pretty (Interval' (Strict.Maybe a)) where
pretty i@(Interval s _) = file <> pretty (setIntervalFile () i)
where
file :: Doc
file = case srcFile s of
Strict.Nothing -> empty
Strict.Just f -> pretty f <> colon
instance Pretty a => Pretty (Range' (Strict.Maybe a)) where
pretty r = case rangeToIntervalWithFile r of
Nothing -> empty
Just i -> pretty i
instance (Pretty a, HasRange a) => Pretty (PrintRange a) where
pretty (PrintRange a) = pretty a <+> parens (text "at" <+> pretty (getRange a))
startPos' :: a -> Position' a
startPos' f = Pn
{ srcFile = f
, posPos = 1
, posLine = 1
, posCol = 1
}
startPos :: Maybe AbsolutePath -> Position
startPos = startPos' . Strict.toStrict
noRange :: Range' a
noRange = NoRange
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' ::
a -> PositionWithoutFile -> PositionWithoutFile -> Range' a
posToRange' f p1 p2 = intervalToRange f (posToInterval () p1 p2)
posToRange :: Position' a -> Position' a -> Range' a
posToRange p1 p2 =
posToRange' (srcFile p1) (p1 { srcFile = () }) (p2 { srcFile = () })
intervalToRange :: a -> IntervalWithoutFile -> Range' a
intervalToRange f i = Range f (Seq.singleton i)
rangeToIntervalWithFile :: Range' a -> Maybe (Interval' a)
rangeToIntervalWithFile NoRange = Nothing
rangeToIntervalWithFile (Range f is) = case (Seq.viewl is, Seq.viewr is) of
(head Seq.:< _, _ Seq.:> last) -> Just $ setIntervalFile f $
Interval { iStart = iStart head
, iEnd = iEnd last
}
_ -> __IMPOSSIBLE__
rangeToInterval :: Range' a -> Maybe IntervalWithoutFile
rangeToInterval NoRange = Nothing
rangeToInterval (Range _ is) = case (Seq.viewl is, Seq.viewr is) of
(head Seq.:< _, _ Seq.:> last) -> Just $
Interval { iStart = iStart head
, iEnd = iEnd last
}
_ -> __IMPOSSIBLE__
continuous :: Range' a -> Range' a
continuous NoRange = NoRange
continuous r@(Range f _) = case rangeToInterval r of
Nothing -> __IMPOSSIBLE__
Just i -> intervalToRange f i
continuousPerLine :: Ord a => Range' a -> Range' a
continuousPerLine r@NoRange = r
continuousPerLine r@(Range f _) =
Range f (Seq.unfoldr step (rangeIntervals r))
where
step [] = Nothing
step [i] = Just (i, [])
step (i : is@(j : js))
| sameLine = step (fuseIntervals i j : js)
| otherwise = Just (i, is)
where
sameLine = posLine (iEnd i) == posLine (iStart j)
rStart' :: Range' a -> Maybe PositionWithoutFile
rStart' r = iStart <$> rangeToInterval r
rStart :: Range' a -> Maybe (Position' a)
rStart NoRange = Nothing
rStart r@(Range f _) = (\p -> p { srcFile = f }) <$> rStart' r
rEnd' :: Range' a -> Maybe PositionWithoutFile
rEnd' r = iEnd <$> rangeToInterval r
rEnd :: Range' a -> Maybe (Position' a)
rEnd NoRange = Nothing
rEnd r@(Range f _) = (\p -> p { srcFile = f }) <$> rEnd' r
fuseIntervals :: Ord a => Interval' a -> Interval' a -> Interval' a
fuseIntervals x y = Interval { iStart = head ss, iEnd = last es }
where
ss = sort [iStart x, iStart y]
es = sort [iEnd x, iEnd y]
fuseRanges :: (Ord a) => Range' a -> Range' a -> Range' a
fuseRanges NoRange is2 = is2
fuseRanges is1 NoRange = is1
fuseRanges (Range f is1) (Range _ is2) = Range f (fuse is1 is2)
where
fuse is1 is2 = case (Seq.viewl is1, Seq.viewr is1,
Seq.viewl is2, Seq.viewr is2) of
(Seq.EmptyL, _, _, _) -> is2
(_, _, Seq.EmptyL, _) -> is1
(s1 Seq.:< r1, l1 Seq.:> e1, s2 Seq.:< r2, l2 Seq.:> e2)
| iEnd e1 < iStart s2 -> is1 Seq.>< is2
| iEnd e2 < iStart s1 -> is2 Seq.>< is1
| iEnd e1 == iStart s2 -> mergeTouching l1 e1 s2 r2
| iEnd e2 == iStart s1 -> mergeTouching l2 e2 s1 r1
| iEnd s1 < iStart s2 -> outputLeftPrefix s1 r1 s2 is2
| iEnd s2 < iStart s1 -> outputLeftPrefix s2 r2 s1 is1
| iEnd s1 < iEnd s2 -> fuseSome s1 r1 s2 r2
| otherwise -> fuseSome s2 r2 s1 r1
_ -> __IMPOSSIBLE__
mergeTouching l e s r = l Seq.>< i Seq.<| r
where
i = Interval { iStart = iStart e, iEnd = iEnd s }
outputLeftPrefix s1 r1 s2 is2 = s1 Seq.<| r1' Seq.>< fuse r1'' is2
where
(r1', r1'') = Seq.spanl (\s -> iEnd s < iStart s2) r1
fuseSome s1 r1 s2 r2 = fuse r1' (fuseIntervals s1 s2 Seq.<| r2)
where
r1' = Seq.dropWhileL (\s -> iEnd s <= iEnd s2) r1
fuseRange :: (HasRange u, HasRange t) => u -> t -> Range
fuseRange x y = fuseRanges (getRange x) (getRange y)
beginningOf :: Range -> Range
beginningOf NoRange = NoRange
beginningOf r@(Range f _) = case rStart' r of
Nothing -> __IMPOSSIBLE__
Just pos -> posToRange' f pos pos
beginningOfFile :: Range -> Range
beginningOfFile NoRange = NoRange
beginningOfFile (Range f _) = posToRange' f p p
where p = startPos' ()
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 r = Set.unions (map iPositions $ rangeIntervals r)
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' :: Bool
prop_startPos' = positionInvariant (startPos' ())
prop_startPos :: Maybe AbsolutePath -> Bool
prop_startPos = positionInvariant . startPos
prop_noRange :: Bool
prop_noRange = rangeInvariant (noRange :: Range)
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_posToRange' ::
Integer -> PositionWithoutFile -> PositionWithoutFile -> Bool
prop_posToRange' f p1 p2 =
rangeInvariant (posToRange' f p1 p2)
prop_posToRange :: Position' Integer -> Position' Integer -> Bool
prop_posToRange p1 p2 =
rangeInvariant (posToRange p1 (p2 { srcFile = srcFile p1 }))
prop_intervalToRange :: Integer -> IntervalWithoutFile -> Bool
prop_intervalToRange f i = rangeInvariant (intervalToRange f i)
rangeToIntervalPropertyTemplate ::
Ord a =>
(Range' Integer -> Maybe (Interval' a)) ->
Range' Integer -> Bool
rangeToIntervalPropertyTemplate r2i r = case r2i r of
Nothing -> r == noRange
Just i ->
r /= noRange
&&
intervalInvariant i
&&
iPositions i == makeInterval (rPositions r)
prop_rangeToIntervalWithFile :: Range' Integer -> Bool
prop_rangeToIntervalWithFile =
rangeToIntervalPropertyTemplate rangeToIntervalWithFile
prop_rangeToInterval :: Range' Integer -> Bool
prop_rangeToInterval =
rangeToIntervalPropertyTemplate rangeToInterval
prop_continuous :: Range -> Bool
prop_continuous r =
rangeInvariant cr &&
rPositions cr == makeInterval (rPositions r)
where cr = continuous r
prop_continuousPerLine :: Range -> Bool
prop_continuousPerLine r =
rangeInvariant r'
&&
distinct lineNumbers
&&
rangeFile r' == rangeFile r
where
r' = continuousPerLine r
lineNumbers = concatMap lines (rangeIntervals r')
where
lines i | s == e = [s]
| otherwise = [s, e]
where
s = posLine (iStart i)
e = posLine (iEnd i)
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 -> Property
prop_fuseRanges r1 =
forAll (rangeInSameFileAs r1) $ \r2 ->
let r = fuseRanges r1 r2 in
rangeInvariant r
&&
rPositions r == Set.union (rPositions r1) (rPositions 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 })
intervalInSameFileAs ::
(Arbitrary a, Ord a) => Interval' a -> Gen (Interval' a)
intervalInSameFileAs i =
setIntervalFile (srcFile $ iStart i) <$>
(arbitrary :: Gen IntervalWithoutFile)
prop_intervalInSameFileAs :: Interval' Integer -> Property
prop_intervalInSameFileAs i =
forAll (intervalInSameFileAs i) $ \i' ->
intervalInvariant i' &&
srcFile (iStart i) == srcFile (iStart i')
rangeInSameFileAs :: (Arbitrary a, Ord a) => Range' a -> Gen (Range' a)
rangeInSameFileAs NoRange = arbitrary
rangeInSameFileAs (Range f is) = do
Range _f is <- arbitrary `suchThat` (not . null)
return $ Range (f `asTypeOf` _f) is
prop_rangeInSameFileAs :: Range' Integer -> Property
prop_rangeInSameFileAs r =
forAll (rangeInSameFileAs r) $ \r' ->
rangeInvariant r'
&&
case (r, r') of
(NoRange, _) -> True
(Range f _, Range f' _) -> f == f'
(Range _ _, NoRange) -> False
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 = do
f <- arbitrary
intervalsToRange f . fuse . sort <$> arbitrary
where
fuse (i1 : i2 : is)
| iEnd i1 >= iStart i2 = fuse (fuseIntervals i1 i2 : is)
| otherwise = i1 : fuse (i2 : is)
fuse is = is
instance CoArbitrary a => CoArbitrary (Position' a)
instance CoArbitrary a => CoArbitrary (Interval' a)
instance CoArbitrary a => CoArbitrary (Range' a)
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 Strict.Just
instance Show (Interval' Integer) where show = show . fmap Strict.Just
instance Show (Range' Integer) where show = show . fmap Strict.Just
return []
tests :: IO Bool
tests = do
putStrLn "Agda.Syntax.Position"
$quickCheckAll