    -----------------------------------------------------------------------
    -- |
    -- Module           : What4.ProgramLoc
    -- Description      : Datatype for handling program locations
    -- Copyright        : (c) Galois, Inc 2014-2020
    -- License          : BSD3
    -- Maintainer       : Joe Hendrix <jhendrix@galois.com>
    -- Stability        : provisional
    --
    -- This module primarily defines the `Position` datatype for
    -- handling program location data.  A program location may refer
    -- either to a source file location (file name, line and column number),
    -- a binary file location (file name and byte offset) or be a dummy
    -- "internal" location assigned to generated program fragments.
    ------------------------------------------------------------------------
    {-# LANGUAGE CPP #-}
    {-# LANGUAGE DeriveFoldable #-}
    {-# LANGUAGE DeriveFunctor #-}
    {-# LANGUAGE DeriveTraversable #-}
    module What4.ProgramLoc
      ( Position(..)
      , sourcePos
      , startOfFile
      , ppNoFileName
      , Posd(..)
      , ProgramLoc
      , mkProgramLoc
      , initializationLoc
      , plFunction
      , plSourceLoc
        -- * Objects with a program location associated.
      , HasProgramLoc(..)
      ) where

    import           Control.DeepSeq
    import           Control.Lens
    import           Data.Text (Text)
    import qualified Data.Text as Text
    import           Data.Word
    import           Numeric (showHex)
    import qualified Prettyprinter as PP

    import           What4.FunctionName

    ------------------------------------------------------------------------
    -- Position

    data Position
         -- | A source position containing filename, line, and column.
       = SourcePos !Text !Int !Int
         -- | A binary position containing a filename and address in memory.
       | BinaryPos !Text !Word64
         -- | Some unstructured position information that doesn't fit into the other categories.
       | OtherPos !Text
         -- | Generated internally by the simulator, or otherwise unknown.
       | InternalPos
      deriving (Position -> Position -> Bool
    (Position -> Position -> Bool)
    -> (Position -> Position -> Bool) -> Eq Position
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: Position -> Position -> Bool
    == :: Position -> Position -> Bool
    $c/= :: Position -> Position -> Bool
    /= :: Position -> Position -> Bool
    Eq, Eq Position
    Eq Position =>
    (Position -> Position -> Ordering)
    -> (Position -> Position -> Bool)
    -> (Position -> Position -> Bool)
    -> (Position -> Position -> Bool)
    -> (Position -> Position -> Bool)
    -> (Position -> Position -> Position)
    -> (Position -> Position -> Position)
    -> Ord Position
    Position -> Position -> Bool
    Position -> Position -> Ordering
    Position -> Position -> Position
    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
    $ccompare :: Position -> Position -> Ordering
    compare :: Position -> Position -> Ordering
    $c< :: Position -> Position -> Bool
    < :: Position -> Position -> Bool
    $c<= :: Position -> Position -> Bool
    <= :: Position -> Position -> Bool
    $c> :: Position -> Position -> Bool
    > :: Position -> Position -> Bool
    $c>= :: Position -> Position -> Bool
    >= :: Position -> Position -> Bool
    $cmax :: Position -> Position -> Position
    max :: Position -> Position -> Position
    $cmin :: Position -> Position -> Position
    min :: Position -> Position -> Position
    Ord)

    instance Show Position where
      show :: Position -> String
    show Position
    p = Doc (ZonkAny 0) -> String
    forall a. Show a => a -> String
    show (Position -> Doc (ZonkAny 0)
    forall a ann. Pretty a => a -> Doc ann
    forall ann. Position -> Doc ann
    PP.pretty Position
    p)

    instance NFData Position where
      rnf :: Position -> ()
    rnf (SourcePos Text
    t Int
    l Int
    c) = (Text, Int, Int) -> ()
    forall a. NFData a => a -> ()
    rnf (Text
    t,Int
    l,Int
    c)
      rnf (BinaryPos Text
    t Word64
    a)   = (Text, Word64) -> ()
    forall a. NFData a => a -> ()
    rnf (Text
    t,Word64
    a)
      rnf (OtherPos Text
    t)      = Text -> ()
    forall a. NFData a => a -> ()
    rnf Text
    t
      rnf Position
    InternalPos       = ()

    sourcePos :: FilePath -> Int -> Int -> Position
    sourcePos :: String -> Int -> Int -> Position
    sourcePos String
    p Int
    l Int
    c = Text -> Int -> Int -> Position
    SourcePos (String -> Text
    Text.pack String
    p) Int
    l Int
    c

    startOfFile :: FilePath -> Position
    startOfFile :: String -> Position
    startOfFile String
    path = String -> Int -> Int -> Position
    sourcePos String
    path Int
    1 Int
    0

    instance PP.Pretty Position where
      pretty :: forall ann. Position -> Doc ann
    pretty (SourcePos Text
    path Int
    l Int
    c) =
        Text -> Doc ann
    forall ann. Text -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    PP.pretty Text
    path
          Doc ann -> Doc ann -> Doc ann
    forall a. Semigroup a => a -> a -> a
    PP.<> Doc ann
    forall ann. Doc ann
    PP.colon Doc ann -> Doc ann -> Doc ann
    forall a. Semigroup a => a -> a -> a
    PP.<> Int -> Doc ann
    forall ann. Int -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    PP.pretty Int
    l
          Doc ann -> Doc ann -> Doc ann
    forall a. Semigroup a => a -> a -> a
    PP.<> Doc ann
    forall ann. Doc ann
    PP.colon Doc ann -> Doc ann -> Doc ann
    forall a. Semigroup a => a -> a -> a
    PP.<> Int -> Doc ann
    forall ann. Int -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    PP.pretty Int
    c
      pretty (BinaryPos Text
    path Word64
    addr) =
        Text -> Doc ann
    forall ann. Text -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    PP.pretty Text
    path Doc ann -> Doc ann -> Doc ann
    forall a. Semigroup a => a -> a -> a
    PP.<> Doc ann
    forall ann. Doc ann
    PP.colon Doc ann -> Doc ann -> Doc ann
    forall a. Semigroup a => a -> a -> a
    PP.<>
          String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    PP.pretty String
    "0x" Doc ann -> Doc ann -> Doc ann
    forall a. Semigroup a => a -> a -> a
    PP.<> String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    PP.pretty (Word64 -> ShowS
    forall a. Integral a => a -> ShowS
    showHex Word64
    addr String
    "")
      pretty (OtherPos Text
    txt) = Text -> Doc ann
    forall ann. Text -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    PP.pretty Text
    txt
      pretty Position
    InternalPos = String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    PP.pretty String
    "internal"

    ppNoFileName :: Position -> PP.Doc ann
    ppNoFileName :: forall ann. Position -> Doc ann
    ppNoFileName (SourcePos Text
    _ Int
    l Int
    c) =
      Int -> Doc ann
    forall ann. Int -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    PP.pretty Int
    l Doc ann -> Doc ann -> Doc ann
    forall a. Semigroup a => a -> a -> a
    PP.<> Doc ann
    forall ann. Doc ann
    PP.colon Doc ann -> Doc ann -> Doc ann
    forall a. Semigroup a => a -> a -> a
    PP.<> Int -> Doc ann
    forall ann. Int -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    PP.pretty Int
    c
    ppNoFileName (BinaryPos Text
    _ Word64
    addr) =
      String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    PP.pretty (Word64 -> ShowS
    forall a. Integral a => a -> ShowS
    showHex Word64
    addr String
    "")
    ppNoFileName (OtherPos Text
    msg) =
      Text -> Doc ann
    forall ann. Text -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    PP.pretty Text
    msg
    ppNoFileName Position
    InternalPos = String -> Doc ann
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    PP.pretty String
    "internal"

    ------------------------------------------------------------------------
    -- Posd

    -- | A value with a source position associated.
    data Posd v = Posd { forall v. Posd v -> Position
    pos :: !Position
                       , forall v. Posd v -> v
    pos_val :: !v
                       }
      deriving ((forall a b. (a -> b) -> Posd a -> Posd b)
    -> (forall a b. a -> Posd b -> Posd a) -> Functor Posd
    forall a b. a -> Posd b -> Posd a
    forall a b. (a -> b) -> Posd a -> Posd b
    forall (f :: Type -> Type).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall a b. (a -> b) -> Posd a -> Posd b
    fmap :: forall a b. (a -> b) -> Posd a -> Posd b
    $c<$ :: forall a b. a -> Posd b -> Posd a
    <$ :: forall a b. a -> Posd b -> Posd a
    Functor, (forall m. Monoid m => Posd m -> m)
    -> (forall m a. Monoid m => (a -> m) -> Posd a -> m)
    -> (forall m a. Monoid m => (a -> m) -> Posd a -> m)
    -> (forall a b. (a -> b -> b) -> b -> Posd a -> b)
    -> (forall a b. (a -> b -> b) -> b -> Posd a -> b)
    -> (forall b a. (b -> a -> b) -> b -> Posd a -> b)
    -> (forall b a. (b -> a -> b) -> b -> Posd a -> b)
    -> (forall a. (a -> a -> a) -> Posd a -> a)
    -> (forall a. (a -> a -> a) -> Posd a -> a)
    -> (forall a. Posd a -> [a])
    -> (forall a. Posd a -> Bool)
    -> (forall a. Posd a -> Int)
    -> (forall a. Eq a => a -> Posd a -> Bool)
    -> (forall a. Ord a => Posd a -> a)
    -> (forall a. Ord a => Posd a -> a)
    -> (forall a. Num a => Posd a -> a)
    -> (forall a. Num a => Posd a -> a)
    -> Foldable Posd
    forall a. Eq a => a -> Posd a -> Bool
    forall a. Num a => Posd a -> a
    forall a. Ord a => Posd a -> a
    forall m. Monoid m => Posd m -> m
    forall a. Posd a -> Bool
    forall a. Posd a -> Int
    forall a. Posd a -> [a]
    forall a. (a -> a -> a) -> Posd a -> a
    forall m a. Monoid m => (a -> m) -> Posd a -> m
    forall b a. (b -> a -> b) -> b -> Posd a -> b
    forall a b. (a -> b -> b) -> b -> Posd a -> b
    forall (t :: Type -> Type).
    (forall m. Monoid m => t m -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. t a -> [a])
    -> (forall a. t a -> Bool)
    -> (forall a. t a -> Int)
    -> (forall a. Eq a => a -> t a -> Bool)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> Foldable t
    $cfold :: forall m. Monoid m => Posd m -> m
    fold :: forall m. Monoid m => Posd m -> m
    $cfoldMap :: forall m a. Monoid m => (a -> m) -> Posd a -> m
    foldMap :: forall m a. Monoid m => (a -> m) -> Posd a -> m
    $cfoldMap' :: forall m a. Monoid m => (a -> m) -> Posd a -> m
    foldMap' :: forall m a. Monoid m => (a -> m) -> Posd a -> m
    $cfoldr :: forall a b. (a -> b -> b) -> b -> Posd a -> b
    foldr :: forall a b. (a -> b -> b) -> b -> Posd a -> b
    $cfoldr' :: forall a b. (a -> b -> b) -> b -> Posd a -> b
    foldr' :: forall a b. (a -> b -> b) -> b -> Posd a -> b
    $cfoldl :: forall b a. (b -> a -> b) -> b -> Posd a -> b
    foldl :: forall b a. (b -> a -> b) -> b -> Posd a -> b
    $cfoldl' :: forall b a. (b -> a -> b) -> b -> Posd a -> b
    foldl' :: forall b a. (b -> a -> b) -> b -> Posd a -> b
    $cfoldr1 :: forall a. (a -> a -> a) -> Posd a -> a
    foldr1 :: forall a. (a -> a -> a) -> Posd a -> a
    $cfoldl1 :: forall a. (a -> a -> a) -> Posd a -> a
    foldl1 :: forall a. (a -> a -> a) -> Posd a -> a
    $ctoList :: forall a. Posd a -> [a]
    toList :: forall a. Posd a -> [a]
    $cnull :: forall a. Posd a -> Bool
    null :: forall a. Posd a -> Bool
    $clength :: forall a. Posd a -> Int
    length :: forall a. Posd a -> Int
    $celem :: forall a. Eq a => a -> Posd a -> Bool
    elem :: forall a. Eq a => a -> Posd a -> Bool
    $cmaximum :: forall a. Ord a => Posd a -> a
    maximum :: forall a. Ord a => Posd a -> a
    $cminimum :: forall a. Ord a => Posd a -> a
    minimum :: forall a. Ord a => Posd a -> a
    $csum :: forall a. Num a => Posd a -> a
    sum :: forall a. Num a => Posd a -> a
    $cproduct :: forall a. Num a => Posd a -> a
    product :: forall a. Num a => Posd a -> a
    Foldable, Functor Posd
    Foldable Posd
    (Functor Posd, Foldable Posd) =>
    (forall (f :: Type -> Type) a b.
     Applicative f =>
     (a -> f b) -> Posd a -> f (Posd b))
    -> (forall (f :: Type -> Type) a.
        Applicative f =>
        Posd (f a) -> f (Posd a))
    -> (forall (m :: Type -> Type) a b.
        Monad m =>
        (a -> m b) -> Posd a -> m (Posd b))
    -> (forall (m :: Type -> Type) a.
        Monad m =>
        Posd (m a) -> m (Posd a))
    -> Traversable Posd
    forall (t :: Type -> Type).
    (Functor t, Foldable t) =>
    (forall (f :: Type -> Type) a b.
     Applicative f =>
     (a -> f b) -> t a -> f (t b))
    -> (forall (f :: Type -> Type) a.
        Applicative f =>
        t (f a) -> f (t a))
    -> (forall (m :: Type -> Type) a b.
        Monad m =>
        (a -> m b) -> t a -> m (t b))
    -> (forall (m :: Type -> Type) a. Monad m => t (m a) -> m (t a))
    -> Traversable t
    forall (m :: Type -> Type) a. Monad m => Posd (m a) -> m (Posd a)
    forall (f :: Type -> Type) a.
    Applicative f =>
    Posd (f a) -> f (Posd a)
    forall (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> Posd a -> m (Posd b)
    forall (f :: Type -> Type) a b.
    Applicative f =>
    (a -> f b) -> Posd a -> f (Posd b)
    $ctraverse :: forall (f :: Type -> Type) a b.
    Applicative f =>
    (a -> f b) -> Posd a -> f (Posd b)
    traverse :: forall (f :: Type -> Type) a b.
    Applicative f =>
    (a -> f b) -> Posd a -> f (Posd b)
    $csequenceA :: forall (f :: Type -> Type) a.
    Applicative f =>
    Posd (f a) -> f (Posd a)
    sequenceA :: forall (f :: Type -> Type) a.
    Applicative f =>
    Posd (f a) -> f (Posd a)
    $cmapM :: forall (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> Posd a -> m (Posd b)
    mapM :: forall (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> Posd a -> m (Posd b)
    $csequence :: forall (m :: Type -> Type) a. Monad m => Posd (m a) -> m (Posd a)
    sequence :: forall (m :: Type -> Type) a. Monad m => Posd (m a) -> m (Posd a)
    Traversable, Int -> Posd v -> ShowS
    [Posd v] -> ShowS
    Posd v -> String
    (Int -> Posd v -> ShowS)
    -> (Posd v -> String) -> ([Posd v] -> ShowS) -> Show (Posd v)
    forall v. Show v => Int -> Posd v -> ShowS
    forall v. Show v => [Posd v] -> ShowS
    forall v. Show v => Posd v -> String
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: forall v. Show v => Int -> Posd v -> ShowS
    showsPrec :: Int -> Posd v -> ShowS
    $cshow :: forall v. Show v => Posd v -> String
    show :: Posd v -> String
    $cshowList :: forall v. Show v => [Posd v] -> ShowS
    showList :: [Posd v] -> ShowS
    Show, Posd v -> Posd v -> Bool
    (Posd v -> Posd v -> Bool)
    -> (Posd v -> Posd v -> Bool) -> Eq (Posd v)
    forall v. Eq v => Posd v -> Posd v -> Bool
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: forall v. Eq v => Posd v -> Posd v -> Bool
    == :: Posd v -> Posd v -> Bool
    $c/= :: forall v. Eq v => Posd v -> Posd v -> Bool
    /= :: Posd v -> Posd v -> Bool
    Eq)

    instance NFData v => NFData (Posd v) where
      rnf :: Posd v -> ()
    rnf Posd v
    p = (Position, v) -> ()
    forall a. NFData a => a -> ()
    rnf (Posd v -> Position
    forall v. Posd v -> Position
    pos Posd v
    p, Posd v -> v
    forall v. Posd v -> v
    pos_val Posd v
    p)

    ------------------------------------------------------------------------
    -- ProgramLoc

    -- | A very small type that contains a function and PC identifier.
    data ProgramLoc
       = ProgramLoc { ProgramLoc -> FunctionName
    plFunction :: {-# UNPACK #-} !FunctionName
                    , ProgramLoc -> Position
    plSourceLoc :: !Position
                    }
     deriving (Int -> ProgramLoc -> ShowS
    [ProgramLoc] -> ShowS
    ProgramLoc -> String
    (Int -> ProgramLoc -> ShowS)
    -> (ProgramLoc -> String)
    -> ([ProgramLoc] -> ShowS)
    -> Show ProgramLoc
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> ProgramLoc -> ShowS
    showsPrec :: Int -> ProgramLoc -> ShowS
    $cshow :: ProgramLoc -> String
    show :: ProgramLoc -> String
    $cshowList :: [ProgramLoc] -> ShowS
    showList :: [ProgramLoc] -> ShowS
    Show, ProgramLoc -> ProgramLoc -> Bool
    (ProgramLoc -> ProgramLoc -> Bool)
    -> (ProgramLoc -> ProgramLoc -> Bool) -> Eq ProgramLoc
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: ProgramLoc -> ProgramLoc -> Bool
    == :: ProgramLoc -> ProgramLoc -> Bool
    $c/= :: ProgramLoc -> ProgramLoc -> Bool
    /= :: ProgramLoc -> ProgramLoc -> Bool
    Eq, Eq ProgramLoc
    Eq ProgramLoc =>
    (ProgramLoc -> ProgramLoc -> Ordering)
    -> (ProgramLoc -> ProgramLoc -> Bool)
    -> (ProgramLoc -> ProgramLoc -> Bool)
    -> (ProgramLoc -> ProgramLoc -> Bool)
    -> (ProgramLoc -> ProgramLoc -> Bool)
    -> (ProgramLoc -> ProgramLoc -> ProgramLoc)
    -> (ProgramLoc -> ProgramLoc -> ProgramLoc)
    -> Ord ProgramLoc
    ProgramLoc -> ProgramLoc -> Bool
    ProgramLoc -> ProgramLoc -> Ordering
    ProgramLoc -> ProgramLoc -> ProgramLoc
    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
    $ccompare :: ProgramLoc -> ProgramLoc -> Ordering
    compare :: ProgramLoc -> ProgramLoc -> Ordering
    $c< :: ProgramLoc -> ProgramLoc -> Bool
    < :: ProgramLoc -> ProgramLoc -> Bool
    $c<= :: ProgramLoc -> ProgramLoc -> Bool
    <= :: ProgramLoc -> ProgramLoc -> Bool
    $c> :: ProgramLoc -> ProgramLoc -> Bool
    > :: ProgramLoc -> ProgramLoc -> Bool
    $c>= :: ProgramLoc -> ProgramLoc -> Bool
    >= :: ProgramLoc -> ProgramLoc -> Bool
    $cmax :: ProgramLoc -> ProgramLoc -> ProgramLoc
    max :: ProgramLoc -> ProgramLoc -> ProgramLoc
    $cmin :: ProgramLoc -> ProgramLoc -> ProgramLoc
    min :: ProgramLoc -> ProgramLoc -> ProgramLoc
    Ord)

    -- | Location for initialization code
    initializationLoc :: ProgramLoc
    initializationLoc :: ProgramLoc
    initializationLoc = FunctionName -> Position -> ProgramLoc
    ProgramLoc FunctionName
    startFunctionName (String -> Position
    startOfFile String
    "")

    -- | Make a program loc
    mkProgramLoc :: FunctionName
                 -> Position
                 -> ProgramLoc
    mkProgramLoc :: FunctionName -> Position -> ProgramLoc
    mkProgramLoc = FunctionName -> Position -> ProgramLoc
    ProgramLoc

    ------------------------------------------------------------------------
    -- HasProgramLoc

    class HasProgramLoc v where
      programLoc :: Lens' v ProgramLoc