{-# LANGUAGE DeriveDataTypeable        #-}
{-# LANGUAGE DeriveGeneric             #-}
{-# LANGUAGE FlexibleInstances         #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE ScopedTypeVariables       #-}

module Language.Fixpoint.Types.Spans (

  -- * Concrete Location Type
    SourcePos
  , SrcSpan (..)

  -- * Located Values
  , Loc (..)
  , Located (..)

  -- * Constructing spans
  , dummySpan
  , panicSpan
  , locAt
  , dummyLoc
  , dummyPos
  , atLoc
  , toSourcePos

  -- * Destructing spans
  , sourcePosElts
  , srcLine 
  ) where

-- import           Control.Exception
import           Control.DeepSeq
-- import qualified Control.Monad.Error           as E
import           Data.Serialize                (Serialize (..))
import           Data.Generics                 (Data)
import           Data.Hashable
import           Data.Typeable
import           Data.String
import qualified Data.Binary                   as B
import           GHC.Generics                  (Generic)
import           Language.Fixpoint.Types.PrettyPrint
-- import           Language.Fixpoint.Misc
import           Text.Parsec.Pos
import           Text.PrettyPrint.HughesPJ
import           Text.Printf
-- import           Debug.Trace


-----------------------------------------------------------------------
-- | Located Values ---------------------------------------------------
-----------------------------------------------------------------------

class Loc a where
  srcSpan :: a -> SrcSpan

-----------------------------------------------------------------------
-- | Retrofitting instances to SourcePos ------------------------------
-----------------------------------------------------------------------

instance NFData SourcePos where
  rnf :: SourcePos -> ()
rnf = (SourceName, Line, Line) -> ()
forall a. NFData a => a -> ()
rnf ((SourceName, Line, Line) -> ())
-> (SourcePos -> (SourceName, Line, Line)) -> SourcePos -> ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourcePos -> (SourceName, Line, Line)
ofSourcePos

instance B.Binary SourcePos where
  put :: SourcePos -> Put
put = (SourceName, Line, Line) -> Put
forall t. Binary t => t -> Put
B.put ((SourceName, Line, Line) -> Put)
-> (SourcePos -> (SourceName, Line, Line)) -> SourcePos -> Put
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourcePos -> (SourceName, Line, Line)
ofSourcePos
  get :: Get SourcePos
get = (SourceName, Line, Line) -> SourcePos
toSourcePos ((SourceName, Line, Line) -> SourcePos)
-> Get (SourceName, Line, Line) -> Get SourcePos
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get (SourceName, Line, Line)
forall t. Binary t => Get t
B.get

instance Serialize SourcePos where
  put :: Putter SourcePos
put = Putter (SourceName, Line, Line)
forall t. Serialize t => Putter t
put Putter (SourceName, Line, Line)
-> (SourcePos -> (SourceName, Line, Line)) -> Putter SourcePos
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourcePos -> (SourceName, Line, Line)
ofSourcePos
  get :: Get SourcePos
get = (SourceName, Line, Line) -> SourcePos
toSourcePos ((SourceName, Line, Line) -> SourcePos)
-> Get (SourceName, Line, Line) -> Get SourcePos
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get (SourceName, Line, Line)
forall t. Serialize t => Get t
get

instance PPrint SourcePos where
  pprintTidy :: Tidy -> SourcePos -> Doc
pprintTidy Tidy
_ = SourceName -> Doc
text (SourceName -> Doc)
-> (SourcePos -> SourceName) -> SourcePos -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourcePos -> SourceName
forall a. Show a => a -> SourceName
show

instance Hashable SourcePos where
  hashWithSalt :: Line -> SourcePos -> Line
hashWithSalt Line
i   = Line -> (SourceName, Line, Line) -> Line
forall a. Hashable a => Line -> a -> Line
hashWithSalt Line
i ((SourceName, Line, Line) -> Line)
-> (SourcePos -> (SourceName, Line, Line)) -> SourcePos -> Line
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourcePos -> (SourceName, Line, Line)
sourcePosElts

ofSourcePos :: SourcePos -> (SourceName, Line, Column)
ofSourcePos :: SourcePos -> (SourceName, Line, Line)
ofSourcePos SourcePos
p = (SourceName
f, Line
l, Line
c)
  where
   f :: SourceName
f = SourcePos -> SourceName
sourceName   SourcePos
p
   l :: Line
l = SourcePos -> Line
sourceLine   SourcePos
p
   c :: Line
c = SourcePos -> Line
sourceColumn SourcePos
p

toSourcePos :: (SourceName, Line, Column) -> SourcePos
toSourcePos :: (SourceName, Line, Line) -> SourcePos
toSourcePos (SourceName
f, Line
l, Line
c) = SourceName -> Line -> Line -> SourcePos
newPos SourceName
f Line
l Line
c

sourcePosElts :: SourcePos -> (SourceName, Line, Column)
sourcePosElts :: SourcePos -> (SourceName, Line, Line)
sourcePosElts SourcePos
s = (SourceName
src, Line
line, Line
col)
  where
    src :: SourceName
src         = SourcePos -> SourceName
sourceName   SourcePos
s
    line :: Line
line        = SourcePos -> Line
sourceLine   SourcePos
s
    col :: Line
col         = SourcePos -> Line
sourceColumn SourcePos
s

instance Fixpoint SourcePos where
  toFix :: SourcePos -> Doc
toFix = SourceName -> Doc
text (SourceName -> Doc)
-> (SourcePos -> SourceName) -> SourcePos -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourcePos -> SourceName
forall a. Show a => a -> SourceName
show


data Located a = Loc { Located a -> SourcePos
loc  :: !SourcePos -- ^ Start Position
                     , Located a -> SourcePos
locE :: !SourcePos -- ^ End Position
                     , Located a -> a
val  :: !a
                     } deriving (Typeable (Located a)
DataType
Constr
Typeable (Located a)
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Located a -> c (Located a))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Located a))
-> (Located a -> Constr)
-> (Located a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (Located a)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (Located a)))
-> ((forall b. Data b => b -> b) -> Located a -> Located a)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Located a -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Located a -> r)
-> (forall u. (forall d. Data d => d -> u) -> Located a -> [u])
-> (forall u.
    Line -> (forall d. Data d => d -> u) -> Located a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Located a -> m (Located a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Located a -> m (Located a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Located a -> m (Located a))
-> Data (Located a)
Located a -> DataType
Located a -> Constr
(forall d. Data d => c (t d)) -> Maybe (c (Located a))
(forall b. Data b => b -> b) -> Located a -> Located a
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Located a -> c (Located a)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Located a)
forall a. Data a => Typeable (Located a)
forall a. Data a => Located a -> DataType
forall a. Data a => Located a -> Constr
forall a.
Data a =>
(forall b. Data b => b -> b) -> Located a -> Located a
forall a u.
Data a =>
Line -> (forall d. Data d => d -> u) -> Located a -> u
forall a u.
Data a =>
(forall d. Data d => d -> u) -> Located a -> [u]
forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Located a -> r
forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Located a -> r
forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Located a -> m (Located a)
forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Located a -> m (Located a)
forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Located a)
forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Located a -> c (Located a)
forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Located a))
forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Located a))
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Line -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Line -> (forall d. Data d => d -> u) -> Located a -> u
forall u. (forall d. Data d => d -> u) -> Located a -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Located a -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Located a -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Located a -> m (Located a)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Located a -> m (Located a)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Located a)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Located a -> c (Located a)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Located a))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Located a))
$cLoc :: Constr
$tLocated :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Located a -> m (Located a)
$cgmapMo :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Located a -> m (Located a)
gmapMp :: (forall d. Data d => d -> m d) -> Located a -> m (Located a)
$cgmapMp :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Located a -> m (Located a)
gmapM :: (forall d. Data d => d -> m d) -> Located a -> m (Located a)
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Located a -> m (Located a)
gmapQi :: Line -> (forall d. Data d => d -> u) -> Located a -> u
$cgmapQi :: forall a u.
Data a =>
Line -> (forall d. Data d => d -> u) -> Located a -> u
gmapQ :: (forall d. Data d => d -> u) -> Located a -> [u]
$cgmapQ :: forall a u.
Data a =>
(forall d. Data d => d -> u) -> Located a -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Located a -> r
$cgmapQr :: forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Located a -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Located a -> r
$cgmapQl :: forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Located a -> r
gmapT :: (forall b. Data b => b -> b) -> Located a -> Located a
$cgmapT :: forall a.
Data a =>
(forall b. Data b => b -> b) -> Located a -> Located a
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Located a))
$cdataCast2 :: forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Located a))
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (Located a))
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Located a))
dataTypeOf :: Located a -> DataType
$cdataTypeOf :: forall a. Data a => Located a -> DataType
toConstr :: Located a -> Constr
$ctoConstr :: forall a. Data a => Located a -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Located a)
$cgunfold :: forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Located a)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Located a -> c (Located a)
$cgfoldl :: forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Located a -> c (Located a)
$cp1Data :: forall a. Data a => Typeable (Located a)
Data, Typeable, (forall x. Located a -> Rep (Located a) x)
-> (forall x. Rep (Located a) x -> Located a)
-> Generic (Located a)
forall x. Rep (Located a) x -> Located a
forall x. Located a -> Rep (Located a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Located a) x -> Located a
forall a x. Located a -> Rep (Located a) x
$cto :: forall a x. Rep (Located a) x -> Located a
$cfrom :: forall a x. Located a -> Rep (Located a) x
Generic)

instance Loc (Located a) where
  srcSpan :: Located a -> SrcSpan
srcSpan (Loc SourcePos
l SourcePos
l' a
_) = SourcePos -> SourcePos -> SrcSpan
SS SourcePos
l SourcePos
l'


instance (NFData a) => NFData (Located a)

instance Fixpoint a => Fixpoint (Located a) where
  toFix :: Located a -> Doc
toFix = a -> Doc
forall a. Fixpoint a => a -> Doc
toFix (a -> Doc) -> (Located a -> a) -> Located a -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located a -> a
forall a. Located a -> a
val

instance Functor Located where
  fmap :: (a -> b) -> Located a -> Located b
fmap a -> b
f (Loc SourcePos
l SourcePos
l' a
x) =  SourcePos -> SourcePos -> b -> Located b
forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l SourcePos
l' (a -> b
f a
x)

instance Foldable Located where
  foldMap :: (a -> m) -> Located a -> m
foldMap a -> m
f (Loc SourcePos
_ SourcePos
_ a
x) = a -> m
f a
x

instance Traversable Located where
  traverse :: (a -> f b) -> Located a -> f (Located b)
traverse a -> f b
f (Loc SourcePos
l SourcePos
l' a
x) = SourcePos -> SourcePos -> b -> Located b
forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l SourcePos
l' (b -> Located b) -> f b -> f (Located b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f b
f a
x

instance Show a => Show (Located a) where
  show :: Located a -> SourceName
show (Loc SourcePos
l SourcePos
l' a
x)
    | SourcePos
l SourcePos -> SourcePos -> Bool
forall a. Eq a => a -> a -> Bool
== SourcePos
l' Bool -> Bool -> Bool
&& SourcePos
l SourcePos -> SourcePos -> Bool
forall a. Eq a => a -> a -> Bool
== SourceName -> SourcePos
dummyPos SourceName
"Fixpoint.Types.dummyLoc" = a -> SourceName
forall a. Show a => a -> SourceName
show a
x SourceName -> ShowS
forall a. [a] -> [a] -> [a]
++ SourceName
" (dummyLoc)"
    | Bool
otherwise  = a -> SourceName
forall a. Show a => a -> SourceName
show a
x SourceName -> ShowS
forall a. [a] -> [a] -> [a]
++ SourceName
" defined from: " SourceName -> ShowS
forall a. [a] -> [a] -> [a]
++ SourcePos -> SourceName
forall a. Show a => a -> SourceName
show SourcePos
l SourceName -> ShowS
forall a. [a] -> [a] -> [a]
++ SourceName
" to: " SourceName -> ShowS
forall a. [a] -> [a] -> [a]
++ SourcePos -> SourceName
forall a. Show a => a -> SourceName
show SourcePos
l'

instance PPrint a => PPrint (Located a) where
  pprintTidy :: Tidy -> Located a -> Doc
pprintTidy Tidy
k (Loc SourcePos
_ SourcePos
_ a
x) = Tidy -> a -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k a
x

instance Eq a => Eq (Located a) where
  (Loc SourcePos
_ SourcePos
_ a
x) == :: Located a -> Located a -> Bool
== (Loc SourcePos
_ SourcePos
_ a
y) = a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y

instance Ord a => Ord (Located a) where
  compare :: Located a -> Located a -> Ordering
compare Located a
x Located a
y = a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Located a -> a
forall a. Located a -> a
val Located a
x) (Located a -> a
forall a. Located a -> a
val Located a
y)

instance (B.Binary a) => B.Binary (Located a)

instance Hashable a => Hashable (Located a) where
  hashWithSalt :: Line -> Located a -> Line
hashWithSalt Line
i = Line -> a -> Line
forall a. Hashable a => Line -> a -> Line
hashWithSalt Line
i (a -> Line) -> (Located a -> a) -> Located a -> Line
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located a -> a
forall a. Located a -> a
val

instance (IsString a) => IsString (Located a) where
  fromString :: SourceName -> Located a
fromString = a -> Located a
forall a. a -> Located a
dummyLoc (a -> Located a) -> (SourceName -> a) -> SourceName -> Located a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourceName -> a
forall a. IsString a => SourceName -> a
fromString

srcLine :: (Loc a) => a -> Int 
srcLine :: a -> Line
srcLine = SourcePos -> Line
sourceLine (SourcePos -> Line) -> (a -> SourcePos) -> a -> Line
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SrcSpan -> SourcePos
sp_start (SrcSpan -> SourcePos) -> (a -> SrcSpan) -> a -> SourcePos
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> SrcSpan
forall a. Loc a => a -> SrcSpan
srcSpan 

-----------------------------------------------------------------------
-- | A Reusable SrcSpan Type ------------------------------------------
-----------------------------------------------------------------------

data SrcSpan = SS { SrcSpan -> SourcePos
sp_start :: !SourcePos
                  , SrcSpan -> SourcePos
sp_stop  :: !SourcePos}
                 deriving (SrcSpan -> SrcSpan -> Bool
(SrcSpan -> SrcSpan -> Bool)
-> (SrcSpan -> SrcSpan -> Bool) -> Eq SrcSpan
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SrcSpan -> SrcSpan -> Bool
$c/= :: SrcSpan -> SrcSpan -> Bool
== :: SrcSpan -> SrcSpan -> Bool
$c== :: SrcSpan -> SrcSpan -> Bool
Eq, Eq SrcSpan
Eq SrcSpan
-> (SrcSpan -> SrcSpan -> Ordering)
-> (SrcSpan -> SrcSpan -> Bool)
-> (SrcSpan -> SrcSpan -> Bool)
-> (SrcSpan -> SrcSpan -> Bool)
-> (SrcSpan -> SrcSpan -> Bool)
-> (SrcSpan -> SrcSpan -> SrcSpan)
-> (SrcSpan -> SrcSpan -> SrcSpan)
-> Ord SrcSpan
SrcSpan -> SrcSpan -> Bool
SrcSpan -> SrcSpan -> Ordering
SrcSpan -> SrcSpan -> SrcSpan
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: SrcSpan -> SrcSpan -> SrcSpan
$cmin :: SrcSpan -> SrcSpan -> SrcSpan
max :: SrcSpan -> SrcSpan -> SrcSpan
$cmax :: SrcSpan -> SrcSpan -> SrcSpan
>= :: SrcSpan -> SrcSpan -> Bool
$c>= :: SrcSpan -> SrcSpan -> Bool
> :: SrcSpan -> SrcSpan -> Bool
$c> :: SrcSpan -> SrcSpan -> Bool
<= :: SrcSpan -> SrcSpan -> Bool
$c<= :: SrcSpan -> SrcSpan -> Bool
< :: SrcSpan -> SrcSpan -> Bool
$c< :: SrcSpan -> SrcSpan -> Bool
compare :: SrcSpan -> SrcSpan -> Ordering
$ccompare :: SrcSpan -> SrcSpan -> Ordering
$cp1Ord :: Eq SrcSpan
Ord, Line -> SrcSpan -> ShowS
[SrcSpan] -> ShowS
SrcSpan -> SourceName
(Line -> SrcSpan -> ShowS)
-> (SrcSpan -> SourceName) -> ([SrcSpan] -> ShowS) -> Show SrcSpan
forall a.
(Line -> a -> ShowS)
-> (a -> SourceName) -> ([a] -> ShowS) -> Show a
showList :: [SrcSpan] -> ShowS
$cshowList :: [SrcSpan] -> ShowS
show :: SrcSpan -> SourceName
$cshow :: SrcSpan -> SourceName
showsPrec :: Line -> SrcSpan -> ShowS
$cshowsPrec :: Line -> SrcSpan -> ShowS
Show, Typeable SrcSpan
DataType
Constr
Typeable SrcSpan
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> SrcSpan -> c SrcSpan)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c SrcSpan)
-> (SrcSpan -> Constr)
-> (SrcSpan -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c SrcSpan))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SrcSpan))
-> ((forall b. Data b => b -> b) -> SrcSpan -> SrcSpan)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> SrcSpan -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> SrcSpan -> r)
-> (forall u. (forall d. Data d => d -> u) -> SrcSpan -> [u])
-> (forall u. Line -> (forall d. Data d => d -> u) -> SrcSpan -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> SrcSpan -> m SrcSpan)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> SrcSpan -> m SrcSpan)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> SrcSpan -> m SrcSpan)
-> Data SrcSpan
SrcSpan -> DataType
SrcSpan -> Constr
(forall b. Data b => b -> b) -> SrcSpan -> SrcSpan
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SrcSpan -> c SrcSpan
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SrcSpan
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Line -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Line -> (forall d. Data d => d -> u) -> SrcSpan -> u
forall u. (forall d. Data d => d -> u) -> SrcSpan -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SrcSpan -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SrcSpan -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SrcSpan -> m SrcSpan
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SrcSpan -> m SrcSpan
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SrcSpan
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SrcSpan -> c SrcSpan
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SrcSpan)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SrcSpan)
$cSS :: Constr
$tSrcSpan :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> SrcSpan -> m SrcSpan
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SrcSpan -> m SrcSpan
gmapMp :: (forall d. Data d => d -> m d) -> SrcSpan -> m SrcSpan
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SrcSpan -> m SrcSpan
gmapM :: (forall d. Data d => d -> m d) -> SrcSpan -> m SrcSpan
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SrcSpan -> m SrcSpan
gmapQi :: Line -> (forall d. Data d => d -> u) -> SrcSpan -> u
$cgmapQi :: forall u. Line -> (forall d. Data d => d -> u) -> SrcSpan -> u
gmapQ :: (forall d. Data d => d -> u) -> SrcSpan -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> SrcSpan -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SrcSpan -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SrcSpan -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SrcSpan -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SrcSpan -> r
gmapT :: (forall b. Data b => b -> b) -> SrcSpan -> SrcSpan
$cgmapT :: (forall b. Data b => b -> b) -> SrcSpan -> SrcSpan
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SrcSpan)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SrcSpan)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c SrcSpan)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SrcSpan)
dataTypeOf :: SrcSpan -> DataType
$cdataTypeOf :: SrcSpan -> DataType
toConstr :: SrcSpan -> Constr
$ctoConstr :: SrcSpan -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SrcSpan
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SrcSpan
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SrcSpan -> c SrcSpan
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SrcSpan -> c SrcSpan
$cp1Data :: Typeable SrcSpan
Data, Typeable, (forall x. SrcSpan -> Rep SrcSpan x)
-> (forall x. Rep SrcSpan x -> SrcSpan) -> Generic SrcSpan
forall x. Rep SrcSpan x -> SrcSpan
forall x. SrcSpan -> Rep SrcSpan x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep SrcSpan x -> SrcSpan
$cfrom :: forall x. SrcSpan -> Rep SrcSpan x
Generic)

instance Serialize SrcSpan

instance PPrint SrcSpan where
  pprintTidy :: Tidy -> SrcSpan -> Doc
pprintTidy Tidy
_ = SrcSpan -> Doc
ppSrcSpan

-- ppSrcSpan_short z = parens
--                   $ text (printf "file %s: (%d, %d) - (%d, %d)" (takeFileName f) l c l' c')
--   where
--     (f,l ,c )     = sourcePosElts $ sp_start z
--     (_,l',c')     = sourcePosElts $ sp_stop  z

ppSrcSpan :: SrcSpan -> Doc
ppSrcSpan :: SrcSpan -> Doc
ppSrcSpan SrcSpan
z       = SourceName -> Doc
text (SourceName
-> SourceName -> Line -> Line -> Line -> Line -> SourceName
forall r. PrintfType r => SourceName -> r
printf SourceName
"%s:%d:%d-%d:%d" SourceName
f Line
l Line
c Line
l' Line
c')
                -- parens $ text (printf "file %s: (%d, %d) - (%d, %d)" (takeFileName f) l c l' c')
  where
    (SourceName
f,Line
l ,Line
c )     = SourcePos -> (SourceName, Line, Line)
sourcePosElts (SourcePos -> (SourceName, Line, Line))
-> SourcePos -> (SourceName, Line, Line)
forall a b. (a -> b) -> a -> b
$ SrcSpan -> SourcePos
sp_start SrcSpan
z
    (SourceName
_,Line
l',Line
c')     = SourcePos -> (SourceName, Line, Line)
sourcePosElts (SourcePos -> (SourceName, Line, Line))
-> SourcePos -> (SourceName, Line, Line)
forall a b. (a -> b) -> a -> b
$ SrcSpan -> SourcePos
sp_stop  SrcSpan
z


instance Hashable SrcSpan where
  hashWithSalt :: Line -> SrcSpan -> Line
hashWithSalt Line
i SrcSpan
z = Line -> (SourcePos, SourcePos) -> Line
forall a. Hashable a => Line -> a -> Line
hashWithSalt Line
i (SrcSpan -> SourcePos
sp_start SrcSpan
z, SrcSpan -> SourcePos
sp_stop SrcSpan
z)

instance Loc SrcSpan where 
  srcSpan :: SrcSpan -> SrcSpan
srcSpan SrcSpan
x = SrcSpan
x 

instance Loc () where
  srcSpan :: () -> SrcSpan
srcSpan ()
_ = SrcSpan
dummySpan

instance Loc SourcePos where 
  srcSpan :: SourcePos -> SrcSpan
srcSpan SourcePos
l = SourcePos -> SourcePos -> SrcSpan
SS SourcePos
l SourcePos
l

dummySpan :: SrcSpan
dummySpan :: SrcSpan
dummySpan = SourceName -> SrcSpan
panicSpan SourceName
""

panicSpan :: String -> SrcSpan
panicSpan :: SourceName -> SrcSpan
panicSpan SourceName
s = SourcePos -> SourcePos -> SrcSpan
SS SourcePos
l SourcePos
l
  where l :: SourcePos
l = SourceName -> SourcePos
initialPos SourceName
s

-- atLoc :: Located a -> b -> Located b
-- atLoc (Loc l l' _) = Loc l l'

atLoc :: (Loc l) => l -> b -> Located b
atLoc :: l -> b -> Located b
atLoc l
z b
x   = SourcePos -> SourcePos -> b -> Located b
forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l SourcePos
l' b
x
  where
    SS SourcePos
l SourcePos
l' = l -> SrcSpan
forall a. Loc a => a -> SrcSpan
srcSpan l
z


locAt :: String -> a -> Located a
locAt :: SourceName -> a -> Located a
locAt SourceName
s  = SourcePos -> SourcePos -> a -> Located a
forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l SourcePos
l
  where
    l :: SourcePos
l    = SourceName -> SourcePos
dummyPos SourceName
s

dummyLoc :: a -> Located a
dummyLoc :: a -> Located a
dummyLoc = SourcePos -> SourcePos -> a -> Located a
forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l SourcePos
l
  where
    l :: SourcePos
l    = SourceName -> SourcePos
dummyPos SourceName
"Fixpoint.Types.dummyLoc"

dummyPos   :: String -> SourcePos
dummyPos :: SourceName -> SourcePos
dummyPos SourceName
s = SourceName -> Line -> Line -> SourcePos
newPos SourceName
s Line
0 Line
0