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

import           Data.Hashable

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.Visitors (freeVars)
import           Language.Haskell.Liquid.Types.RefType ()
import           Language.Haskell.Liquid.Types.Types
import qualified Data.HashMap.Strict                       as M


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

dfromList :: [(Ghc.Var, M.HashMap F.Symbol (RISig t))] -> DEnv Ghc.Var t
dfromList :: forall t. [(Var, HashMap Symbol (RISig t))] -> DEnv Var t
dfromList = HashMap Var (HashMap Symbol (RISig t)) -> DEnv Var t
forall x ty. HashMap x (HashMap Symbol (RISig ty)) -> DEnv x ty
DEnv (HashMap Var (HashMap Symbol (RISig t)) -> DEnv Var t)
-> ([(Var, HashMap Symbol (RISig t))]
    -> HashMap Var (HashMap Symbol (RISig t)))
-> [(Var, HashMap Symbol (RISig t))]
-> DEnv Var t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Var, HashMap Symbol (RISig t))]
-> HashMap Var (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)