{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FlexibleContexts     #-}
module Language.Haskell.Liquid.Types.Dictionaries (
    makeDictionaries
  , makeDictionary
  , dfromList
  , dmapty
  , dmap
  , dinsert
  , dlookup
  , dhasinfo
  , fromRISig
  ) where

import           Data.Hashable
-- import           Data.Maybe (catMaybes)

import           Prelude                                   hiding (error)
import qualified Language.Fixpoint.Types as F
import           Language.Haskell.Liquid.Types.PrettyPrint ()
import qualified Language.Haskell.Liquid.GHC.Misc       as GM
import qualified Liquid.GHC.API        as Ghc
import           Language.Haskell.Liquid.Types.Types
-- import           Language.Haskell.Liquid.Types.Visitors (freeVars)
import           Language.Haskell.Liquid.Types.RefType ()
import           Language.Fixpoint.Misc                (mapFst)
import qualified Data.HashMap.Strict                       as M





makeDictionaries :: [RInstance LocSpecType] -> DEnv F.Symbol LocSpecType
makeDictionaries :: [RInstance LocSpecType] -> DEnv Symbol LocSpecType
makeDictionaries = forall x ty. HashMap x (HashMap Symbol (RISig ty)) -> DEnv x ty
DEnv forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map RInstance LocSpecType
-> (Symbol, HashMap Symbol (RISig LocSpecType))
makeDictionary


makeDictionary :: RInstance LocSpecType -> (F.Symbol, M.HashMap F.Symbol (RISig LocSpecType))
makeDictionary :: RInstance LocSpecType
-> (Symbol, HashMap Symbol (RISig LocSpecType))
makeDictionary (RI BTyCon
c [LocSpecType]
ts [(LocSymbol, RISig LocSpecType)]
xts) = (LocSymbol -> [LocSpecType] -> Symbol
makeDictionaryName (BTyCon -> LocSymbol
btc_tc BTyCon
c) [LocSpecType]
ts, forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList (forall a c b. (a -> c) -> (a, b) -> (c, b)
mapFst forall a. Located a -> a
val forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(LocSymbol, RISig LocSpecType)]
xts))

makeDictionaryName :: LocSymbol -> [LocSpecType] -> F.Symbol
makeDictionaryName :: LocSymbol -> [LocSpecType] -> Symbol
makeDictionaryName LocSymbol
t [LocSpecType]
ts
  = forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
_msg forall a b. (a -> b) -> a -> b
$ forall a. Symbolic a => a -> Symbol
F.symbol ([Char]
"$f" forall a. [a] -> [a] -> [a]
++ Symbol -> [Char]
F.symbolString (forall a. Located a -> a
val LocSymbol
t) forall a. [a] -> [a] -> [a]
++ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap LocSpecType -> [Char]
mkName [LocSpecType]
ts)
  where
    mkName :: LocSpecType -> [Char]
mkName = SrcSpan -> SpecType -> [Char]
makeDicTypeName SrcSpan
sp forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecType -> SpecType
dropUniv forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Located a -> a
val
    sp :: SrcSpan
sp     = forall a. Loc a => a -> SrcSpan
GM.fSrcSpan LocSymbol
t
    _msg :: [Char]
_msg   = [Char]
"MAKE-DICTIONARY " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp (forall a. Located a -> a
val LocSymbol
t, [LocSpecType]
ts)

-- | @makeDicTypeName@ DOES NOT use show/symbol in the @RVar@ case 
--   as those functions add the unique-suffix which then breaks the 
--   class resolution.

makeDicTypeName :: Ghc.SrcSpan -> SpecType -> String
makeDicTypeName :: SrcSpan -> SpecType -> [Char]
makeDicTypeName SrcSpan
_ RFun{}           = [Char]
"(->)"
makeDicTypeName SrcSpan
_ (RApp RTyCon
c [SpecType]
_ [RTProp RTyCon RTyVar (UReft Reft)]
_ UReft Reft
_)   = Symbol -> [Char]
F.symbolString forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Symbol
GM.dropModuleNamesCorrect forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Symbolic a => a -> Symbol
F.symbol forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTyCon -> TyCon
rtc_tc forall a b. (a -> b) -> a -> b
$ RTyCon
c
makeDicTypeName SrcSpan
_ (RVar (RTV TyVar
a) UReft Reft
_) = forall a. Show a => a -> [Char]
show (forall a. NamedThing a => a -> Name
Ghc.getName TyVar
a)
makeDicTypeName SrcSpan
sp SpecType
t               = forall a. Maybe SrcSpan -> [Char] -> a
panic (forall a. a -> Maybe a
Just SrcSpan
sp) ([Char]
"makeDicTypeName: called with invalid type " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show SpecType
t)

dropUniv :: SpecType -> SpecType
dropUniv :: SpecType -> SpecType
dropUniv SpecType
t = SpecType
t' where ([(RTVar RTyVar (RType RTyCon RTyVar ()), UReft Reft)]
_,[PVar (RType RTyCon RTyVar ())]
_,SpecType
t') = forall tv c r.
RType tv c r
-> ([(RTVar c (RType tv c ()), r)], [PVar (RType tv c ())],
    RType tv c r)
bkUniv SpecType
t

--------------------------------------------------------------------------------
-- | Dictionary Environment ----------------------------------------------------
--------------------------------------------------------------------------------

dfromList :: [(Ghc.Var, M.HashMap F.Symbol (RISig t))] -> DEnv Ghc.Var t
dfromList :: forall t. [(TyVar, HashMap Symbol (RISig t))] -> DEnv TyVar t
dfromList = forall x ty. HashMap x (HashMap Symbol (RISig ty)) -> DEnv x ty
DEnv forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList

dmapty :: (a -> b) -> DEnv v a -> DEnv v b
dmapty :: forall a b v. (a -> b) -> DEnv v a -> DEnv v b
dmapty a -> b
f (DEnv HashMap v (HashMap Symbol (RISig a))
e) = forall x ty. HashMap x (HashMap Symbol (RISig ty)) -> DEnv x ty
DEnv (forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
M.map (forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
M.map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f)) HashMap v (HashMap Symbol (RISig a))
e)

-- REBARE: mapRISig :: (a -> b) -> RISig a -> RISig b
-- REBARE: mapRISig f (RIAssumed t) = RIAssumed (f t)
-- REBARE: mapRISig f (RISig     t) = RISig     (f t)

fromRISig :: RISig a -> a
fromRISig :: forall a. RISig a -> a
fromRISig (RIAssumed a
t) = a
t
fromRISig (RISig     a
t) = a
t

dmap :: (v1 -> v2) -> M.HashMap k v1 -> M.HashMap k v2
dmap :: forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
dmap v1 -> v2
f HashMap k v1
xts = forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
M.map v1 -> v2
f HashMap k v1
xts

dinsert :: (Eq x, Hashable x)
        => DEnv x ty -> x -> M.HashMap F.Symbol (RISig ty) -> DEnv x ty
dinsert :: forall x ty.
(Eq x, Hashable x) =>
DEnv x ty -> x -> HashMap Symbol (RISig ty) -> DEnv x ty
dinsert (DEnv HashMap x (HashMap Symbol (RISig ty))
denv) x
x HashMap Symbol (RISig ty)
xts = forall x ty. HashMap x (HashMap Symbol (RISig ty)) -> DEnv x ty
DEnv forall a b. (a -> b) -> a -> b
$ forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert x
x HashMap Symbol (RISig ty)
xts HashMap x (HashMap Symbol (RISig ty))
denv

dlookup :: (Eq k, Hashable k)
        => DEnv k t -> k -> Maybe (M.HashMap F.Symbol (RISig t))
dlookup :: forall k t.
(Eq k, Hashable k) =>
DEnv k t -> k -> Maybe (HashMap Symbol (RISig t))
dlookup (DEnv HashMap k (HashMap Symbol (RISig t))
denv) k
x     = forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup k
x HashMap k (HashMap Symbol (RISig t))
denv


dhasinfo :: (F.Symbolic a1, Show a) => Maybe (M.HashMap F.Symbol a) -> a1 -> Maybe a
dhasinfo :: forall a1 a.
(Symbolic a1, Show a) =>
Maybe (HashMap Symbol a) -> a1 -> Maybe a
dhasinfo Maybe (HashMap Symbol a)
Nothing a1
_    = forall a. Maybe a
Nothing
dhasinfo (Just HashMap Symbol a
xts) a1
x = forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Symbol
x' HashMap Symbol a
xts
  where
     x' :: Symbol
x'               = Symbol -> Symbol
GM.dropModuleNamesCorrect (forall a. Symbolic a => a -> Symbol
F.symbol a1
x)