module Language.Haskell.Liquid.Bare.Misc (
makeSymbols
, joinVar
, mkVarExpr
, MapTyVarST(..)
, initMapSt
, runMapTyVars
, mapTyVars
, symbolRTyVar
, simpleSymbolVar
, hasBoolResult
) where
import Prelude hiding (error)
import TysWiredIn
import Name
import Id
import Type
import TypeRep
import Var
import Control.Monad.Except (throwError)
import Control.Monad.State
import Data.Maybe (isNothing)
import qualified Data.List as L
import Language.Fixpoint.Misc (sortNub)
import Language.Fixpoint.Types (Symbol, Expr(..), Reft(..), Reftable(..), mkEApp, emptySEnv, memberSEnv, symbol, syms, toReft)
import Language.Haskell.Liquid.GHC.Misc
import Language.Haskell.Liquid.Types.RefType
import Language.Haskell.Liquid.Types
import Language.Haskell.Liquid.Misc (sortDiff)
import Language.Haskell.Liquid.Bare.Env
makeSymbols f vs xs' xts yts ivs
= do svs <- gets varEnv
return $ L.nub ([ (x,v') | (x,v) <- svs, x `elem` xs, let (v',_,_) = joinVar vs (v,x,x)]
++ [ (symbol v, v) | v <- vs, f v, isDataConId v, hasBasicArgs $ varType v ])
where
xs = sortNub $ zs ++ zs' ++ zs''
zs = concatMap freeSymbols (snd <$> xts) `sortDiff` xs'
zs' = concatMap freeSymbols (snd <$> yts) `sortDiff` xs'
zs'' = concatMap freeSymbols ivs `sortDiff` xs'
hasBasicArgs (ForAllTy _ t) = hasBasicArgs t
hasBasicArgs (FunTy tx t) = isBaseTy tx && hasBasicArgs t
hasBasicArgs _ = True
freeSymbols ty = sortNub $ concat $ efoldReft (\_ _ -> []) (const ()) f (const id) emptySEnv [] (val ty)
where
f γ _ r xs = let Reft (v, _) = toReft r in
[ x | x <- syms r, x /= v, not (x `memberSEnv` γ)] : xs
data MapTyVarST = MTVST { vmap :: [(Var, RTyVar)]
, errmsg :: Error
}
initMapSt = MTVST []
runMapTyVars :: StateT MapTyVarST (Either Error) () -> MapTyVarST -> Either Error MapTyVarST
runMapTyVars = execStateT
mapTyVars :: (PPrint r, Reftable r) => Type -> RRType r -> StateT MapTyVarST (Either Error) ()
mapTyVars τ (RAllT _ t)
= mapTyVars τ t
mapTyVars (ForAllTy _ τ) t
= mapTyVars τ t
mapTyVars (FunTy τ τ') (RFun _ t t' _)
= mapTyVars τ t >> mapTyVars τ' t'
mapTyVars (TyConApp _ τs) (RApp _ ts _ _)
= zipWithM_ mapTyVars τs ts
mapTyVars (TyVarTy α) (RVar a _)
= do s <- get
s' <- mapTyRVar α a s
put s'
mapTyVars τ (RAllP _ t)
= mapTyVars τ t
mapTyVars τ (RAllS _ t)
= mapTyVars τ t
mapTyVars τ (RAllE _ _ t)
= mapTyVars τ t
mapTyVars τ (RRTy _ _ _ t)
= mapTyVars τ t
mapTyVars τ (REx _ _ t)
= mapTyVars τ t
mapTyVars _ (RExprArg _)
= return ()
mapTyVars (AppTy τ τ') (RAppTy t t' _)
= do mapTyVars τ t
mapTyVars τ' t'
mapTyVars _ (RHole _)
= return ()
mapTyVars _ _
= throwError =<< errmsg <$> get
mapTyRVar α a s@(MTVST αas err)
= case lookup α αas of
Just a' | a == a' -> return s
| otherwise -> throwError err
Nothing -> return $ MTVST ((α,a):αas) err
mkVarExpr v
| isFunVar v = mkEApp (varFunSymbol v) []
| otherwise = EVar (symbol v)
varFunSymbol = dummyLoc . symbol . idDataCon
isFunVar v = isDataConId v && not (null αs) && isNothing tf
where
(αs, t) = splitForAllTys $ varType v
tf = splitFunTy_maybe t
joinVar :: [Var] -> (Var, s, t) -> (Var, s, t)
joinVar vs (v,s,t) = case L.find ((== showPpr v) . showPpr) vs of
Just v' -> (v',s,t)
Nothing -> (v,s,t)
simpleSymbolVar :: Var -> Symbol
simpleSymbolVar = dropModuleNames . symbol . showPpr . getName
hasBoolResult (ForAllTy _ t) = hasBoolResult t
hasBoolResult (FunTy _ t) | eqType boolTy t = True
hasBoolResult (FunTy _ t) = hasBoolResult t
hasBoolResult _ = False