{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FlexibleContexts     #-}
{-# LANGUAGE TupleSections        #-}
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           Var
import           Name                                      (getName)
import qualified Language.Fixpoint.Types as F
import           Language.Haskell.Liquid.Types.PrettyPrint ()
import qualified Language.Haskell.Liquid.GHC.Misc       as GM 
import qualified Language.Haskell.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
  = String -> Symbol -> Symbol
forall a. PPrint a => String -> a -> a
F.notracepp String
_msg (Symbol -> Symbol) -> Symbol -> Symbol
forall a b. (a -> b) -> a -> b
$ String -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (String
"$f" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Symbol -> String
F.symbolString (LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
t) String -> String -> String
forall a. [a] -> [a] -> [a]
++ (LocSpecType -> String) -> [LocSpecType] -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap LocSpecType -> String
mkName [LocSpecType]
ts)
  where
    mkName :: LocSpecType -> String
mkName = SrcSpan -> SpecType -> String
makeDicTypeName SrcSpan
sp (SpecType -> String)
-> (LocSpecType -> SpecType) -> LocSpecType -> String
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 :: String
_msg   = String
"MAKE-DICTIONARY " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Symbol, [LocSpecType]) -> String
forall a. PPrint a => a -> String
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 -> String
makeDicTypeName SrcSpan
_ (RFun Symbol
_ SpecType
_ SpecType
_ RReft
_)   = String
"(->)"
makeDicTypeName SrcSpan
_ (RApp RTyCon
c [SpecType]
_ [RTProp RTyCon RTyVar RReft]
_ RReft
_)   = Symbol -> String
F.symbolString (Symbol -> String) -> (RTyCon -> Symbol) -> RTyCon -> String
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 -> String) -> RTyCon -> String
forall a b. (a -> b) -> a -> b
$ RTyCon
c
makeDicTypeName SrcSpan
_ (RVar (RTV TyVar
a) RReft
_) = Name -> String
forall a. Show a => a -> String
show (TyVar -> Name
forall a. NamedThing a => a -> Name
getName TyVar
a)      
makeDicTypeName SrcSpan
sp SpecType
t               = Maybe SrcSpan -> String -> String
forall a. Maybe SrcSpan -> String -> a
panic (SrcSpan -> Maybe SrcSpan
forall a. a -> Maybe a
Just SrcSpan
sp) (String
"makeDicTypeName: called with invalid type " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SpecType -> String
forall a. Show a => a -> String
show SpecType
t)

dropUniv :: SpecType -> SpecType 
dropUniv :: SpecType -> SpecType
dropUniv SpecType
t = SpecType
t' where ([(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)]
_,[PVar (RType RTyCon RTyVar ())]
_,SpecType
t') = SpecType
-> ([(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)],
    [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 :: [(Var, M.HashMap F.Symbol (RISig t))] -> DEnv Var t
dfromList :: [(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 :: (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 (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 :: 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 :: (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 :: 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 :: 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 :: 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)