liquid-fixpoint-0.8.10.7: src/Language/Fixpoint/Types/Spans.hs
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Language.Fixpoint.Types.Spans (
-- * Concrete Location Type
SourcePos(..)
, SourceName
, SrcSpan (..)
, Pos
, predPos
, safePos
, safeSourcePos
, succPos
, unPos
, mkPos
-- * Located Values
, Loc (..)
, Located (..)
-- * Constructing spans
, dummySpan
, panicSpan
, locAt
, dummyLoc
, dummyPos
, atLoc
, toSourcePos
, ofSourcePos
-- * 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.Store as S
import GHC.Generics (Generic)
import Language.Fixpoint.Types.PrettyPrint
-- import Language.Fixpoint.Misc
import Text.Megaparsec.Pos
import Text.PrettyPrint.HughesPJ
import Text.Printf
import Data.Functor.Contravariant (Contravariant(contramap))
import qualified Data.Binary as B
-- import Debug.Trace
-----------------------------------------------------------------------
-- | Located Values ---------------------------------------------------
-----------------------------------------------------------------------
class Loc a where
srcSpan :: a -> SrcSpan
-----------------------------------------------------------------------
-- Additional (orphan) instances for megaparsec's Pos type ------------
-----------------------------------------------------------------------
instance S.Store Pos where
poke = S.poke . unPos
peek = mkPos <$> S.peek
size = contramap unPos S.size
instance Serialize Pos where
put = put . unPos
get = mkPos <$> get
instance Hashable Pos where
hashWithSalt i = hashWithSalt i . unPos
instance PrintfArg Pos where
formatArg = formatArg . unPos
parseFormat = parseFormat . unPos
-- | Computes, safely, the predecessor of a 'Pos' value, stopping at 1.
predPos :: Pos -> Pos
predPos pos =
mkPos $
case unPos pos of
1 -> 1
atLeastTwo -> atLeastTwo - 1
-- | Computes the successor of a 'Pos' value.
succPos :: Pos -> Pos
succPos pos =
mkPos $ unPos pos + 1
-- | Create, safely, as position. If a non-positive number is given,
-- we use 1.
--
safePos :: Int -> Pos
safePos i
| i <= 0 = mkPos 1
| otherwise = mkPos i
-- | Create a source position from integers, using 1 in case of
-- non-positive numbers.
safeSourcePos :: FilePath -> Int -> Int -> SourcePos
safeSourcePos file line col =
SourcePos file (safePos line) (safePos col)
-----------------------------------------------------------------------
-- | Retrofitting instances to SourcePos ------------------------------
-----------------------------------------------------------------------
instance S.Store SourcePos where
-- poke = S.poke . ofSourcePos
-- peek = toSourcePos <$> S.peek
instance Serialize SourcePos where
put = put . ofSourcePos
get = toSourcePos <$> get
instance PPrint SourcePos where
pprintTidy _ = ppSourcePos
instance Hashable SourcePos where
hashWithSalt i = hashWithSalt i . sourcePosElts
-- | This is a compatibility type synonym for megaparsec vs. parsec.
type SourceName = FilePath
-- | This is a compatibility type synonym for megaparsec vs. parsec.
type Line = Pos
-- | This is a compatibility type synonym for megaparsec vs. parsec.
type Column = Pos
ofSourcePos :: SourcePos -> (SourceName, Line, Column)
ofSourcePos p = (f, l, c)
where
f = sourceName p
l = sourceLine p
c = sourceColumn p
toSourcePos :: (SourceName, Line, Column) -> SourcePos
toSourcePos (f, l, c) = SourcePos f l c
sourcePosElts :: SourcePos -> (SourceName, Line, Column)
sourcePosElts = ofSourcePos
ppSourcePos :: SourcePos -> Doc
ppSourcePos z = text (printf "%s:%d:%d" f l c)
where
(f,l,c) = sourcePosElts $ z
instance Fixpoint SourcePos where
toFix = text . show
data Located a = Loc { loc :: !SourcePos -- ^ Start Position
, locE :: !SourcePos -- ^ End Position
, val :: !a
} deriving (Data, Typeable, Generic)
instance Loc (Located a) where
srcSpan (Loc l l' _) = SS l l'
instance (NFData a) => NFData (Located a)
instance Fixpoint a => Fixpoint (Located a) where
toFix = toFix . val
instance Functor Located where
fmap f (Loc l l' x) = Loc l l' (f x)
instance Foldable Located where
foldMap f (Loc _ _ x) = f x
instance Traversable Located where
traverse f (Loc l l' x) = Loc l l' <$> f x
instance Show a => Show (Located a) where
show (Loc l l' x)
| l == l' && l == dummyPos "Fixpoint.Types.dummyLoc" = show x ++ " (dummyLoc)"
| otherwise = show x ++ " defined at: " ++ render (ppSrcSpan (SS l l'))
instance PPrint a => PPrint (Located a) where
pprintTidy k (Loc _ _ x) = pprintTidy k x
instance Eq a => Eq (Located a) where
(Loc _ _ x) == (Loc _ _ y) = x == y
instance Ord a => Ord (Located a) where
compare x y = compare (val x) (val y)
instance (S.Store a) => S.Store (Located a)
instance Hashable a => Hashable (Located a) where
hashWithSalt i = hashWithSalt i . val
instance (IsString a) => IsString (Located a) where
fromString = dummyLoc . fromString
-- | We need the Binary instances for LH's spec serialization
instance B.Binary Pos where
put = B.put . unPos
get = mkPos <$> B.get
instance B.Binary SourcePos
instance (B.Binary a) => B.Binary (Located a)
srcLine :: (Loc a) => a -> Pos
srcLine = sourceLine . sp_start . srcSpan
-----------------------------------------------------------------------
-- | A Reusable SrcSpan Type ------------------------------------------
-----------------------------------------------------------------------
data SrcSpan = SS { sp_start :: !SourcePos
, sp_stop :: !SourcePos}
deriving (Eq, Ord, Show, Data, Typeable, Generic)
instance Serialize SrcSpan
instance PPrint SrcSpan where
pprintTidy _ = 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 z = text (printf "%s:%d:%d-%d:%d" f l c l' c')
-- 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
instance Hashable SrcSpan where
hashWithSalt i z = hashWithSalt i (sp_start z, sp_stop z)
instance Loc SrcSpan where
srcSpan x = x
instance Loc () where
srcSpan _ = dummySpan
instance Loc SourcePos where
srcSpan l = SS l l
dummySpan :: SrcSpan
dummySpan = panicSpan ""
panicSpan :: String -> SrcSpan
panicSpan s = SS l l
where l = initialPos s
-- atLoc :: Located a -> b -> Located b
-- atLoc (Loc l l' _) = Loc l l'
atLoc :: (Loc l) => l -> b -> Located b
atLoc z x = Loc l l' x
where
SS l l' = srcSpan z
locAt :: String -> a -> Located a
locAt s = Loc l l
where
l = dummyPos s
dummyLoc :: a -> Located a
dummyLoc = Loc l l
where
l = dummyPos "Fixpoint.Types.dummyLoc"
dummyPos :: FilePath -> SourcePos
dummyPos = initialPos