module Language.Haskell.Liquid.Synthesize.Env where 

import           Language.Fixpoint.Types
import           Language.Haskell.Liquid.Constraint.Types
import           Language.Haskell.Liquid.Types
import           Language.Haskell.Liquid.Synthesize.Monad
import qualified Data.HashMap.Strict           as M
import qualified Data.HashSet                  as S
import           DataCon
import           TyCon
import           Var
import           Data.List 

initSSEnv :: SpecType -> CGInfo -> SSEnv -> (SSEnv, [Var])
initSSEnv :: SpecType -> CGInfo -> SSEnv -> (SSEnv, [Var])
initSSEnv SpecType
rt CGInfo
info SSEnv
senv = (SSEnv -> SSEnv -> SSEnv
forall k v.
(Eq k, Hashable k) =>
HashMap k v -> HashMap k v -> HashMap k v
M.union SSEnv
senv ([(Symbol, (SpecType, Var))] -> SSEnv
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(Symbol, (SpecType, Var))]
foralls), [Var]
vs)
  where foralls :: [(Symbol, (SpecType, Var))]
foralls = ((Symbol, (SpecType, Var)) -> Bool)
-> [(Symbol, (SpecType, Var))] -> [(Symbol, (SpecType, Var))]
forall a. (a -> Bool) -> [a] -> [a]
filter (Symbol, (SpecType, Var)) -> Bool
forall a a. (a, (a, Var)) -> Bool
iNeedIt ((Var, Located SpecType) -> (Symbol, (SpecType, Var))
forall b a. Symbolic b => (b, Located a) -> (Symbol, (a, b))
mkElem ((Var, Located SpecType) -> (Symbol, (SpecType, Var)))
-> [(Var, Located SpecType)] -> [(Symbol, (SpecType, Var))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Var, Located SpecType)]
prims)
        vs :: [Var]
vs = ((Symbol, (SpecType, Var)) -> Var)
-> [(Symbol, (SpecType, Var))] -> [Var]
forall a b. (a -> b) -> [a] -> [b]
map ((SpecType, Var) -> Var
forall a b. (a, b) -> b
snd ((SpecType, Var) -> Var)
-> ((Symbol, (SpecType, Var)) -> (SpecType, Var))
-> (Symbol, (SpecType, Var))
-> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, (SpecType, Var)) -> (SpecType, Var)
forall a b. (a, b) -> b
snd) [(Symbol, (SpecType, Var))]
foralls
        dataCons :: [DataCon]
dataCons = SpecType -> [DataCon]
typeToCons SpecType
rt 
        mkElem :: (b, Located a) -> (Symbol, (a, b))
mkElem (b
v, Located a
lt) = (b -> Symbol
forall a. Symbolic a => a -> Symbol
symbol b
v, (Located a -> a
forall a. Located a -> a
val Located a
lt, b
v))
        prims :: [(Var, Located SpecType)]
prims = GhcSpecData -> [(Var, Located SpecType)]
gsCtors (GhcSpecData -> [(Var, Located SpecType)])
-> GhcSpecData -> [(Var, Located SpecType)]
forall a b. (a -> b) -> a -> b
$ TargetSpec -> GhcSpecData
gsData (TargetSpec -> GhcSpecData) -> TargetSpec -> GhcSpecData
forall a b. (a -> b) -> a -> b
$ TargetInfo -> TargetSpec
giSpec (TargetInfo -> TargetSpec) -> TargetInfo -> TargetSpec
forall a b. (a -> b) -> a -> b
$ CGInfo -> TargetInfo
ghcI CGInfo
info
        iNeedIt :: (a, (a, Var)) -> Bool
iNeedIt (a
_, (a
_, Var
v)) = Var
v Var -> [Var] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (DataCon -> Var
dataConWorkId (DataCon -> Var) -> [DataCon] -> [Var]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DataCon]
dataCons)

-- | For algebraic datatypes: Find (in the refinement type) 
--   all the datatypes that are used and 
--   get their constructors.
tpToCons :: SpecType -> [DataCon] 
tpToCons :: SpecType -> [DataCon]
tpToCons (RAllT RTVU RTyCon RTyVar
_a SpecType
t RReft
_x)  
  = SpecType -> [DataCon]
tpToCons SpecType
t 
tpToCons (RApp RTyCon
c [SpecType]
args [RTProp RTyCon RTyVar RReft]
_ RReft
_r) 
  = TyCon -> [DataCon]
tyConDataCons (RTyCon -> TyCon
rtc_tc RTyCon
c) [DataCon] -> [DataCon] -> [DataCon]
forall a. [a] -> [a] -> [a]
++ (SpecType -> [DataCon]) -> [SpecType] -> [DataCon]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap SpecType -> [DataCon]
tpToCons [SpecType]
args
tpToCons (RFun Symbol
_sym SpecType
rt0 SpecType
rt1 RReft
_reft)
  = SpecType -> [DataCon]
tpToCons SpecType
rt0 [DataCon] -> [DataCon] -> [DataCon]
forall a. [a] -> [a] -> [a]
++ SpecType -> [DataCon]
tpToCons SpecType
rt1
tpToCons RVar{} 
  = []
tpToCons (RAllP PVU RTyCon RTyVar
_ SpecType
t)
  = SpecType -> [DataCon]
tpToCons SpecType
t
tpToCons (RRTy [(Symbol, SpecType)]
_ RReft
_ Oblig
_ SpecType
t)
  = SpecType -> [DataCon]
tpToCons SpecType
t
tpToCons SpecType
_ 
  = []

typeToCons :: SpecType -> [DataCon]
typeToCons :: SpecType -> [DataCon]
typeToCons SpecType
rt = HashSet DataCon -> [DataCon]
forall a. HashSet a -> [a]
S.toList (HashSet DataCon -> [DataCon]) -> HashSet DataCon -> [DataCon]
forall a b. (a -> b) -> a -> b
$ [DataCon] -> HashSet DataCon
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList (SpecType -> [DataCon]
tpToCons SpecType
rt)

rmMeasures :: [Symbol] -> [(Symbol, SpecType)] -> [(Symbol, SpecType)]
rmMeasures :: [Symbol] -> [(Symbol, SpecType)] -> [(Symbol, SpecType)]
rmMeasures [Symbol]
meas = ((Symbol, SpecType) -> Bool)
-> [(Symbol, SpecType)] -> [(Symbol, SpecType)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Symbol
s,SpecType
_) -> case (Symbol -> Bool) -> [Symbol] -> Maybe Symbol
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
s) [Symbol]
meas of  Maybe Symbol
Nothing -> Bool
True
                                                              Just Symbol
_  -> Bool
False)