{-# 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 = HashMap Symbol (HashMap Symbol (RISig LocSpecType))
-> DEnv Symbol LocSpecType
forall x ty. HashMap x (HashMap Symbol (RISig ty)) -> DEnv x ty
DEnv (HashMap Symbol (HashMap Symbol (RISig LocSpecType))
 -> DEnv Symbol LocSpecType)
-> ([RInstance LocSpecType]
    -> HashMap Symbol (HashMap Symbol (RISig LocSpecType)))
-> [RInstance LocSpecType]
-> DEnv Symbol LocSpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Symbol, HashMap Symbol (RISig LocSpecType))]
-> HashMap Symbol (HashMap Symbol (RISig LocSpecType))
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList ([(Symbol, HashMap Symbol (RISig LocSpecType))]
 -> HashMap Symbol (HashMap Symbol (RISig LocSpecType)))
-> ([RInstance LocSpecType]
    -> [(Symbol, HashMap Symbol (RISig LocSpecType))])
-> [RInstance LocSpecType]
-> HashMap Symbol (HashMap Symbol (RISig LocSpecType))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (RInstance LocSpecType
 -> (Symbol, HashMap Symbol (RISig LocSpecType)))
-> [RInstance LocSpecType]
-> [(Symbol, HashMap Symbol (RISig LocSpecType))]
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, [(Symbol, RISig LocSpecType)] -> HashMap Symbol (RISig LocSpecType)
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList ((LocSymbol -> Symbol)
-> (LocSymbol, RISig LocSpecType) -> (Symbol, RISig LocSpecType)
forall a c b. (a -> c) -> (a, b) -> (c, b)
mapFst LocSymbol -> Symbol
forall a. Located a -> a
val ((LocSymbol, RISig LocSpecType) -> (Symbol, RISig LocSpecType))
-> [(LocSymbol, RISig LocSpecType)]
-> [(Symbol, RISig LocSpecType)]
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
  = [Char] -> Symbol -> Symbol
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
_msg (Symbol -> Symbol) -> Symbol -> Symbol
forall a b. (a -> b) -> a -> b
$ [Char] -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol ([Char]
"$f" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Symbol -> [Char]
F.symbolString (LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
t) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (LocSpecType -> [Char]) -> [LocSpecType] -> [Char]
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 (SpecType -> [Char])
-> (LocSpecType -> SpecType) -> LocSpecType -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecType -> SpecType
dropUniv (SpecType -> SpecType)
-> (LocSpecType -> SpecType) -> LocSpecType -> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LocSpecType -> SpecType
forall a. Located a -> a
val
    sp :: SrcSpan
sp     = LocSymbol -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan LocSymbol
t
    _msg :: [Char]
_msg   = [Char]
"MAKE-DICTIONARY " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Symbol, [LocSpecType]) -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp (LocSymbol -> Symbol
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 (Symbol -> [Char]) -> (RTyCon -> Symbol) -> RTyCon -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Symbol
GM.dropModuleNamesCorrect (Symbol -> Symbol) -> (RTyCon -> Symbol) -> RTyCon -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyCon -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (TyCon -> Symbol) -> (RTyCon -> TyCon) -> RTyCon -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTyCon -> TyCon
rtc_tc (RTyCon -> [Char]) -> RTyCon -> [Char]
forall a b. (a -> b) -> a -> b
$ RTyCon
c
makeDicTypeName SrcSpan
_ (RVar (RTV TyVar
a) UReft Reft
_) = Name -> [Char]
forall a. Show a => a -> [Char]
show (TyVar -> Name
forall a. NamedThing a => a -> Name
Ghc.getName TyVar
a)
makeDicTypeName SrcSpan
sp SpecType
t               = Maybe SrcSpan -> [Char] -> [Char]
forall a. Maybe SrcSpan -> [Char] -> a
panic (SrcSpan -> Maybe SrcSpan
forall a. a -> Maybe a
Just SrcSpan
sp) ([Char]
"makeDicTypeName: called with invalid type " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SpecType -> [Char]
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') = SpecType
-> ([(RTVar RTyVar (RType RTyCon RTyVar ()), UReft Reft)],
    [PVar (RType RTyCon RTyVar ())], SpecType)
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 = HashMap TyVar (HashMap Symbol (RISig t)) -> DEnv TyVar t
forall x ty. HashMap x (HashMap Symbol (RISig ty)) -> DEnv x ty
DEnv (HashMap TyVar (HashMap Symbol (RISig t)) -> DEnv TyVar t)
-> ([(TyVar, HashMap Symbol (RISig t))]
    -> HashMap TyVar (HashMap Symbol (RISig t)))
-> [(TyVar, HashMap Symbol (RISig t))]
-> DEnv TyVar t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(TyVar, HashMap Symbol (RISig t))]
-> HashMap TyVar (HashMap Symbol (RISig t))
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) = HashMap v (HashMap Symbol (RISig b)) -> DEnv v b
forall x ty. HashMap x (HashMap Symbol (RISig ty)) -> DEnv x ty
DEnv ((HashMap Symbol (RISig a) -> HashMap Symbol (RISig b))
-> HashMap v (HashMap Symbol (RISig a))
-> HashMap v (HashMap Symbol (RISig b))
forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
M.map ((RISig a -> RISig b)
-> HashMap Symbol (RISig a) -> HashMap Symbol (RISig b)
forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
M.map ((a -> b) -> RISig a -> RISig b
forall a b. (a -> b) -> RISig a -> RISig b
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 = (v1 -> v2) -> HashMap k v1 -> HashMap k v2
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 = HashMap x (HashMap Symbol (RISig ty)) -> DEnv x ty
forall x ty. HashMap x (HashMap Symbol (RISig ty)) -> DEnv x ty
DEnv (HashMap x (HashMap Symbol (RISig ty)) -> DEnv x ty)
-> HashMap x (HashMap Symbol (RISig ty)) -> DEnv x ty
forall a b. (a -> b) -> a -> b
$ x
-> HashMap Symbol (RISig ty)
-> HashMap x (HashMap Symbol (RISig ty))
-> HashMap x (HashMap Symbol (RISig ty))
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     = k
-> HashMap k (HashMap Symbol (RISig t))
-> Maybe (HashMap Symbol (RISig t))
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
_    = Maybe a
forall a. Maybe a
Nothing
dhasinfo (Just HashMap Symbol a
xts) a1
x = Symbol -> HashMap Symbol a -> Maybe a
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 (a1 -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol a1
x)