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

-- |
-- 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
import Data.Hashable
import Debug.Trace.LocationTH (__LOCATION__)
import GHC.Generics
import Grisette.Core.Data.Class.GenSym
import Grisette.Core.Data.Class.Solvable
import Language.Haskell.TH.Syntax
import Language.Haskell.TH.Syntax.Compat

-- $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
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: FileLocation -> FileLocation -> Bool
$c/= :: FileLocation -> FileLocation -> Bool
== :: FileLocation -> FileLocation -> Bool
$c== :: FileLocation -> FileLocation -> Bool
Eq, Eq 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
min :: FileLocation -> FileLocation -> FileLocation
$cmin :: FileLocation -> FileLocation -> FileLocation
max :: FileLocation -> FileLocation -> FileLocation
$cmax :: FileLocation -> FileLocation -> FileLocation
>= :: FileLocation -> FileLocation -> Bool
$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
compare :: FileLocation -> FileLocation -> Ordering
$ccompare :: FileLocation -> FileLocation -> Ordering
Ord, 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
$cto :: forall x. Rep FileLocation x -> FileLocation
$cfrom :: forall x. FileLocation -> Rep FileLocation x
Generic, 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
liftTyped :: forall (m :: * -> *).
Quote m =>
FileLocation -> Code m FileLocation
$cliftTyped :: forall (m :: * -> *).
Quote m =>
FileLocation -> Code m FileLocation
lift :: forall (m :: * -> *). Quote m => FileLocation -> m Exp
$clift :: forall (m :: * -> *). Quote m => FileLocation -> m Exp
Lift, FileLocation -> ()
forall a. (a -> ()) -> NFData a
rnf :: FileLocation -> ()
$crnf :: FileLocation -> ()
NFData, Eq FileLocation
Int -> FileLocation -> Int
FileLocation -> Int
forall a. Eq a -> (Int -> a -> Int) -> (a -> Int) -> Hashable a
hash :: FileLocation -> Int
$chash :: FileLocation -> Int
hashWithSalt :: Int -> FileLocation -> Int
$chashWithSalt :: Int -> FileLocation -> Int
Hashable)

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

parseFileLocation :: String -> FileLocation
parseFileLocation :: String -> FileLocation
parseFileLocation String
str =
  let r :: String
r = forall a. [a] -> [a]
reverse String
str
      (String
s2, String
r1) = forall a. (a -> Bool) -> [a] -> ([a], [a])
break (forall a. Eq a => a -> a -> Bool
== Char
'-') String
r
      (String
s1, String
r2) = forall a. (a -> Bool) -> [a] -> ([a], [a])
break (forall a. Eq a => a -> a -> Bool
== Char
':') forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
tail String
r1
      (String
l, String
p) = forall a. (a -> Bool) -> [a] -> ([a], [a])
break (forall a. Eq a => a -> a -> Bool
== Char
':') forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
tail String
r2
   in String -> Int -> (Int, Int) -> FileLocation
FileLocation (forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
tail String
p) (forall a. Read a => String -> a
read forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
reverse String
l) (forall a. Read a => String -> a
read forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
reverse String
s1, forall a. Read a => String -> a
read forall a b. (a -> b) -> a -> b
$ 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 :: String -> SpliceQ FreshIdent
nameWithLoc :: String -> SpliceQ FreshIdent
nameWithLoc String
s = [||nameWithInfo s (parseFileLocation $$(liftSplice $ unsafeTExpCoerce __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) => String -> SpliceQ s
slocsym :: forall c s. Solvable c s => String -> SpliceQ s
slocsym String
nm = [||sinfosym nm (parseFileLocation $$(liftSplice $ unsafeTExpCoerce __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) => String -> Int -> SpliceQ s
ilocsym :: forall c s. Solvable c s => String -> Int -> SpliceQ s
ilocsym String
nm Int
idx = [||iinfosym nm idx (parseFileLocation $$(liftSplice $ unsafeTExpCoerce __LOCATION__))||]