{-# LANGUAGE CPP, DeriveDataTypeable #-}

{-| Position information for syntax. Crucial for giving good error messages.
-}

module Agda.Syntax.Position
  ( -- * Positions
    Position(..)
  , positionInvariant
  , startPos
  , movePos
  , movePosByString
  , backupPos

    -- * Intervals
  , Interval(..)
  , intervalInvariant
  , takeI
  , dropI

    -- * Ranges
  , Range(..)
  , rangeInvariant
  , noRange
  , posToRange
  , rStart
  , rEnd
  , rangeToInterval
  , continuous
  , continuousPerLine
  , HasRange(..)
  , SetRange(..)
  , KillRange(..)
  , killRange1, killRange2, killRange3, killRange4, killRange5, killRange6, killRange7
  , withRangeOf
  , fuseRange
  , fuseRanges
  , beginningOf

    -- * Tests
  , 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

{--------------------------------------------------------------------------
    Types and classes
 --------------------------------------------------------------------------}

-- | Represents a point in the input (file, position, line, col).
-- Positions and line and column numbers start from 1.
--
-- If two positions have the same 'srcFile' and 'posPos' components,
-- then the final two components should be the same as well, but since
-- this can be hard to enforce the program should not rely too much on
-- the last two components; they are mainly there to improve error
-- messages for the user.
--
-- Note the invariant which positions have to satisfy: 'positionInvariant'.
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

-- | An interval. The @iEnd@ position is not included in the interval.
--
-- Note the invariant which intervals have to satisfy: 'intervalInvariant'.
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

-- | The length of an interval, assuming that the start and end
-- positions are in the same file.
iLength :: Interval -> Int
iLength i = posPos (iEnd i) - posPos (iStart i)

-- | A range is a list of intervals. The intervals should be
-- consecutive and separated.
--
-- Note the invariant which ranges have to satisfy: 'rangeInvariant'.
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))

-- | Things that have a range are instances of this class.
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

-- | If it is also possible to set the range, this is the class.
--
--   Instances should satisfy @'getRange' ('setRange' r x) == r@.
class HasRange t => SetRange t where
  setRange :: Range -> t -> t

instance SetRange Range where
  setRange = const

-- | Killing the range of an object sets all range information to 'noRange'.
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

{--------------------------------------------------------------------------
    Pretty printing
 --------------------------------------------------------------------------}

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

{--------------------------------------------------------------------------
    Functions on postitions and ranges
 --------------------------------------------------------------------------}

-- | The first position in a file: position 1, line 1, column 1.
startPos :: Maybe AbsolutePath -> Position
startPos f = Pn { srcFile = f, posPos = 1, posLine = 1, posCol = 1 }

-- | Ranges between two unknown positions
noRange :: Range
noRange = Range []

-- | Advance the position by one character.
--   A newline character (@'\n'@) moves the position to the first
--   character in the next line. Any other character moves the
--   position to the next column.
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)

-- | Advance the position by a string.
--
--   > movePosByString = foldl' movePos
movePosByString :: Position -> String -> Position
movePosByString = foldl' movePos

-- | Backup the position by one character.
--
-- Precondition: The character must not be @'\n'@.
backupPos :: Position -> Position
backupPos (Pn f p l c) = Pn f (p - 1) l (c - 1)

-- | Extracts the interval corresponding to the given string, assuming
-- that the string starts at the beginning of the given interval.
--
-- Precondition: The string must not be too long for the interval.
takeI :: String -> Interval -> Interval
takeI s i | length s > iLength i = __IMPOSSIBLE__
          | otherwise = i { iEnd = movePosByString (iStart i) s }

-- | Removes the interval corresponding to the given string from the
-- given interval, assuming that the string starts at the beginning of
-- the interval.
--
-- Precondition: The string must not be too long for the interval.
dropI :: String -> Interval -> Interval
dropI s i | length s > iLength i = __IMPOSSIBLE__
          | otherwise = i { iStart = movePosByString (iStart i) s }

-- | Converts two positions to a range.
posToRange :: Position -> Position -> Range
posToRange p1 p2 | p1 < p2   = Range [Interval p1 p2]
                 | otherwise = Range [Interval p2 p1]

-- | Converts a range to an interval, if possible.
rangeToInterval :: Range -> Maybe Interval
rangeToInterval (Range [])   = Nothing
rangeToInterval (Range is)   = Just $ Interval { iStart = iStart (head is)
                                               , iEnd   = iEnd   (last is)
                                               }

-- | Returns the shortest continuous range containing the given one.
continuous :: Range -> Range
continuous r = case rangeToInterval r of
  Nothing -> Range []
  Just i  -> Range [i]

-- | Removes gaps between intervals on the same line.
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)

-- | The initial position in the range, if any.
rStart :: Range -> Maybe Position
rStart r = iStart <$> rangeToInterval r

-- | The position after the final position in the range, if any.
rEnd :: Range -> Maybe Position
rEnd r = iEnd <$> rangeToInterval r

-- | Finds the least interval which covers the arguments.
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]

-- | Finds a range which covers the arguments.
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 r@ is an empty range (a single, empty interval)
-- positioned at the beginning of @r@. If @r@ does not have a
-- beginning, then 'noRange' is returned.
beginningOf :: Range -> Range
beginningOf r = case rStart r of
  Just pos -> Range [Interval { iStart = pos, iEnd = pos }]
  Nothing  -> noRange

-- | @x `withRangeOf` y@ sets the range of @x@ to the range of @y@.
withRangeOf :: (SetRange t, HasRange u) => t -> u -> t
x `withRangeOf` y = setRange (getRange y) x

------------------------------------------------------------------------
-- Test suite

-- | The positions corresponding to the interval, /including/ the
-- end-point. This function assumes that the two end points belong to
-- the same file. Note that the 'Arbitrary' instance for 'Position's
-- uses a single, hard-wired file name.
iPositions :: Interval -> Set Int
iPositions i = Set.fromList [posPos (iStart i) .. posPos (iEnd i)]

-- | The positions corresponding to the range, including the
-- end-points. All ranges are assumed to belong to a single file.
rPositions :: Range -> Set Int
rPositions (Range is) = Set.unions (map iPositions is)

-- | Constructs the least interval containing all the elements in the
-- set.
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 })

-- | Sets the 'srcFile' components of the interval.

setFile :: Maybe AbsolutePath -> Interval -> Interval
setFile f (Interval p1 p2) =
  Interval (p1 { srcFile = f }) (p2 { srcFile = f })

-- | Generates an interval located in the same file as the given
-- interval.

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

-- | Test suite.
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
  ]