{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveLift #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE Trustworthy #-}

{- HLINT ignore "Unused LANGUAGE pragma" -}

-- |
-- Module      :   Grisette.Core.Data.FileLocation
-- Copyright   :   (c) Sirui Lu 2021-2023
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.Core.Data.FileLocation
  ( -- * Symbolic constant generation with location
    FileLocation (..),
    nameWithLoc,
    slocsym,
    ilocsym,
  )
where

import Control.DeepSeq (NFData)
import Data.Hashable (Hashable)
import qualified Data.Text as T
import Debug.Trace.LocationTH (__LOCATION__)
import GHC.Generics (Generic)
import Grisette.Core.Data.Class.GenSym (FreshIdent, nameWithInfo)
import Grisette.Core.Data.Class.Solvable
  ( Solvable (iinfosym, sinfosym),
  )
import Language.Haskell.TH.Syntax (Lift, unsafeTExpCoerce)
import Language.Haskell.TH.Syntax.Compat (SpliceQ, liftSplice)

-- $setup
-- >>> import Grisette.Core
-- >>> import Grisette.IR.SymPrim
-- >>> :set -XTemplateHaskell

-- File location type.
data FileLocation = FileLocation {FileLocation -> String
locPath :: String, FileLocation -> Int
locLineno :: Int, FileLocation -> (Int, Int)
locSpan :: (Int, Int)}
  deriving (FileLocation -> FileLocation -> Bool
(FileLocation -> FileLocation -> Bool)
-> (FileLocation -> FileLocation -> Bool) -> Eq FileLocation
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: FileLocation -> FileLocation -> Bool
== :: FileLocation -> FileLocation -> Bool
$c/= :: FileLocation -> FileLocation -> Bool
/= :: FileLocation -> FileLocation -> Bool
Eq, Eq FileLocation
Eq FileLocation =>
(FileLocation -> FileLocation -> Ordering)
-> (FileLocation -> FileLocation -> Bool)
-> (FileLocation -> FileLocation -> Bool)
-> (FileLocation -> FileLocation -> Bool)
-> (FileLocation -> FileLocation -> Bool)
-> (FileLocation -> FileLocation -> FileLocation)
-> (FileLocation -> FileLocation -> FileLocation)
-> Ord FileLocation
FileLocation -> FileLocation -> Bool
FileLocation -> FileLocation -> Ordering
FileLocation -> FileLocation -> FileLocation
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 :: FileLocation -> FileLocation -> Ordering
compare :: FileLocation -> FileLocation -> Ordering
$c< :: FileLocation -> FileLocation -> Bool
< :: FileLocation -> FileLocation -> Bool
$c<= :: FileLocation -> FileLocation -> Bool
<= :: FileLocation -> FileLocation -> Bool
$c> :: FileLocation -> FileLocation -> Bool
> :: FileLocation -> FileLocation -> Bool
$c>= :: FileLocation -> FileLocation -> Bool
>= :: FileLocation -> FileLocation -> Bool
$cmax :: FileLocation -> FileLocation -> FileLocation
max :: FileLocation -> FileLocation -> FileLocation
$cmin :: FileLocation -> FileLocation -> FileLocation
min :: FileLocation -> FileLocation -> FileLocation
Ord, (forall x. FileLocation -> Rep FileLocation x)
-> (forall x. Rep FileLocation x -> FileLocation)
-> Generic FileLocation
forall x. Rep FileLocation x -> FileLocation
forall x. FileLocation -> Rep FileLocation x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. FileLocation -> Rep FileLocation x
from :: forall x. FileLocation -> Rep FileLocation x
$cto :: forall x. Rep FileLocation x -> FileLocation
to :: forall x. Rep FileLocation x -> FileLocation
Generic, (forall (m :: * -> *). Quote m => FileLocation -> m Exp)
-> (forall (m :: * -> *).
    Quote m =>
    FileLocation -> Code m FileLocation)
-> Lift FileLocation
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => FileLocation -> m Exp
forall (m :: * -> *).
Quote m =>
FileLocation -> Code m FileLocation
$clift :: forall (m :: * -> *). Quote m => FileLocation -> m Exp
lift :: forall (m :: * -> *). Quote m => FileLocation -> m Exp
$cliftTyped :: forall (m :: * -> *).
Quote m =>
FileLocation -> Code m FileLocation
liftTyped :: forall (m :: * -> *).
Quote m =>
FileLocation -> Code m FileLocation
Lift, FileLocation -> ()
(FileLocation -> ()) -> NFData FileLocation
forall a. (a -> ()) -> NFData a
$crnf :: FileLocation -> ()
rnf :: FileLocation -> ()
NFData, Eq FileLocation
Eq FileLocation =>
(Int -> FileLocation -> Int)
-> (FileLocation -> Int) -> Hashable FileLocation
Int -> FileLocation -> Int
FileLocation -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
$chashWithSalt :: Int -> FileLocation -> Int
hashWithSalt :: Int -> FileLocation -> Int
$chash :: FileLocation -> Int
hash :: FileLocation -> Int
Hashable)

instance Show FileLocation where
  show :: FileLocation -> String
show (FileLocation String
p Int
l (Int
s1, Int
s2)) = String
p String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
":" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
l String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
":" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
s1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"-" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
s2

parseFileLocation :: String -> FileLocation
parseFileLocation :: String -> FileLocation
parseFileLocation String
str =
  let r :: String
r = ShowS
forall a. [a] -> [a]
reverse String
str
      (String
s2, String
r1) = (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
break (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'-') String
r
      (String
s1, String
r2) = (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
break (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
':') (String -> (String, String)) -> String -> (String, String)
forall a b. (a -> b) -> a -> b
$ ShowS
forall a. HasCallStack => [a] -> [a]
tail String
r1
      (String
l, String
p) = (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
break (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
':') (String -> (String, String)) -> String -> (String, String)
forall a b. (a -> b) -> a -> b
$ ShowS
forall a. HasCallStack => [a] -> [a]
tail String
r2
   in String -> Int -> (Int, Int) -> FileLocation
FileLocation (ShowS
forall a. [a] -> [a]
reverse ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ ShowS
forall a. HasCallStack => [a] -> [a]
tail String
p) (String -> Int
forall a. Read a => String -> a
read (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ ShowS
forall a. [a] -> [a]
reverse String
l) (String -> Int
forall a. Read a => String -> a
read (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ ShowS
forall a. [a] -> [a]
reverse String
s1, String -> Int
forall a. Read a => String -> a
read (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ ShowS
forall a. [a] -> [a]
reverse String
s2)

-- | Identifier with the current location as extra information.
--
-- >>> $$(nameWithLoc "a") -- a sample result could be "a:<interactive>:18:4-18"
-- a:<interactive>:...
--
-- The uniqueness is ensured for the call to 'nameWithLoc' at different location.
nameWithLoc :: T.Text -> SpliceQ FreshIdent
nameWithLoc :: Text -> SpliceQ FreshIdent
nameWithLoc Text
s = [||Text -> a -> FreshIdent
forall a.
(Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) =>
Text -> a -> FreshIdent
nameWithInfo Text
s (String -> FileLocation
parseFileLocation $$(Q (TExp String) -> Splice Q String
forall a (m :: * -> *). m (TExp a) -> Splice m a
liftSplice (Q (TExp String) -> Splice Q String)
-> Q (TExp String) -> Splice Q String
forall a b. (a -> b) -> a -> b
$ Q Exp -> Q (TExp String)
forall a (m :: * -> *). Quote m => m Exp -> m (TExp a)
unsafeTExpCoerce Q Exp
__LOCATION__))||]

-- | Generate simply-named symbolic variables. The file location will be
-- attached to the identifier.
--
-- >>> $$(slocsym "a") :: SymBool
-- a:<interactive>:...
--
-- Calling 'slocsymb' with the same name at different location will always
-- generate different symbolic constants. Calling 'slocsymb' at the same
-- location for multiple times will generate the same symbolic constants.
--
-- >>> ($$(slocsym "a") :: SymBool) == $$(slocsym "a")
-- False
-- >>> let f _ = $$(slocsym "a") :: SymBool
-- >>> f () == f ()
-- True
slocsym :: (Solvable c s) => T.Text -> SpliceQ s
slocsym :: forall c s. Solvable c s => Text -> SpliceQ s
slocsym Text
nm = [||Text -> a -> t
forall a.
(Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) =>
Text -> a -> t
forall c t a.
(Solvable c t, Typeable a, Ord a, Lift a, NFData a, Show a,
 Hashable a) =>
Text -> a -> t
sinfosym Text
nm (String -> FileLocation
parseFileLocation $$(Q (TExp String) -> Splice Q String
forall a (m :: * -> *). m (TExp a) -> Splice m a
liftSplice (Q (TExp String) -> Splice Q String)
-> Q (TExp String) -> Splice Q String
forall a b. (a -> b) -> a -> b
$ Q Exp -> Q (TExp String)
forall a (m :: * -> *). Quote m => m Exp -> m (TExp a)
unsafeTExpCoerce Q Exp
__LOCATION__))||]

-- | Generate indexed symbolic variables. The file location will be attached to identifier.
--
-- >>> $$(ilocsym "a" 1) :: SymBool
-- a@1:<interactive>:...
--
-- Calling 'ilocsymb' with the same name and index at different location will
-- always generate different symbolic constants. Calling 'slocsymb' at the same
-- location for multiple times will generate the same symbolic constants.
ilocsym :: (Solvable c s) => T.Text -> Int -> SpliceQ s
ilocsym :: forall c s. Solvable c s => Text -> Int -> SpliceQ s
ilocsym Text
nm Int
idx = [||Text -> Int -> a -> t
forall a.
(Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) =>
Text -> Int -> a -> t
forall c t a.
(Solvable c t, Typeable a, Ord a, Lift a, NFData a, Show a,
 Hashable a) =>
Text -> Int -> a -> t
iinfosym Text
nm Int
idx (String -> FileLocation
parseFileLocation $$(Q (TExp String) -> Splice Q String
forall a (m :: * -> *). m (TExp a) -> Splice m a
liftSplice (Q (TExp String) -> Splice Q String)
-> Q (TExp String) -> Splice Q String
forall a b. (a -> b) -> a -> b
$ Q Exp -> Q (TExp String)
forall a (m :: * -> *). Quote m => m Exp -> m (TExp a)
unsafeTExpCoerce Q Exp
__LOCATION__))||]