content: {-# LANGUAGE DeriveDataTypeable        #-}
  {-# LANGUAGE DeriveGeneric             #-}
  {-# LANGUAGE FlexibleInstances         #-}
  {-# LANGUAGE NoMonomorphismRestriction #-}
  {-# LANGUAGE ScopedTypeVariables       #-}
  
  {-# OPTIONS_GHC -Wno-orphans           #-}
  {-# LANGUAGE DeriveAnyClass #-}
  
  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           Data.Aeson
  -- 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, ToJSON, FromJSON)
  
  instance ToJSON SourcePos where
  instance FromJSON SourcePos where
  
  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)
  
  
  instance ToJSON Pos where 
  
  instance FromJSON Pos where
  
  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, ToJSON, FromJSON)
  
  instance NFData SrcSpan
  instance S.Store SrcSpan
  instance Serialize SrcSpan
  instance B.Binary 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
  