module Language.Haskell.Liquid.Constraint.Types where
import CoreSyn
import SrcLoc
import qualified TyCon as TC
import qualified DataCon as DC
import Text.PrettyPrint.HughesPJ hiding (first)
import qualified Data.HashMap.Strict as M
import qualified Data.HashSet as S
import qualified Data.List as L
import Control.Applicative ((<$>))
import Data.Monoid (mconcat)
import Data.Maybe (catMaybes)
import Var
import Language.Haskell.Liquid.Types
import Language.Haskell.Liquid.Strata
import Language.Haskell.Liquid.Misc (fourth4)
import Language.Haskell.Liquid.RefType (shiftVV)
import Language.Haskell.Liquid.PredType (wiredSortedSyms)
import qualified Language.Fixpoint.Types as F
import Language.Fixpoint.Misc
import qualified Language.Haskell.Liquid.CTags as Tg
data CGEnv
= CGE { loc :: !SrcSpan
, renv :: !REnv
, syenv :: !(F.SEnv Var)
, denv :: !RDEnv
, fenv :: !FEnv
, recs :: !(S.HashSet Var)
, invs :: !RTyConInv
, ial :: !RTyConIAl
, grtys :: !REnv
, assms :: !REnv
, emb :: F.TCEmb TC.TyCon
, tgEnv :: !Tg.TagEnv
, tgKey :: !(Maybe Tg.TagKey)
, trec :: !(Maybe (M.HashMap F.Symbol SpecType))
, lcb :: !(M.HashMap F.Symbol CoreExpr)
, holes :: !HEnv
, lcs :: !LConstraint
}
data LConstraint = LC [[(F.Symbol, SpecType)]]
instance PPrint CGEnv where
pprint = pprint . renv
instance Show CGEnv where
show = showpp
data SubC = SubC { senv :: !CGEnv
, lhs :: !SpecType
, rhs :: !SpecType
}
| SubR { senv :: !CGEnv
, oblig :: !Oblig
, ref :: !RReft
}
data WfC = WfC !CGEnv !SpecType
type FixSubC = F.SubC Cinfo
type FixWfC = F.WfC Cinfo
instance PPrint SubC where
pprint c = pprint (senv c)
$+$ ((text " |- ") <+> ( (pprint (lhs c))
$+$ text "<:"
$+$ (pprint (rhs c))))
instance PPrint WfC where
pprint (WfC w r) = pprint w <> text " |- " <> pprint r
instance SubStratum SubC where
subS su (SubC γ t1 t2) = SubC γ (subS su t1) (subS su t2)
subS _ c = c
data CGInfo = CGInfo { hsCs :: ![SubC]
, hsWfs :: ![WfC]
, sCs :: ![SubC]
, fixCs :: ![FixSubC]
, isBind :: ![Bool]
, fixWfs :: ![FixWfC]
, freshIndex :: !Integer
, binds :: !F.BindEnv
, annotMap :: !(AnnInfo (Annot SpecType))
, tyConInfo :: !(M.HashMap TC.TyCon RTyCon)
, specDecr :: ![(Var, [Int])]
, termExprs :: !(M.HashMap Var [F.Expr])
, specLVars :: !(S.HashSet Var)
, specLazy :: !(S.HashSet Var)
, tyConEmbed :: !(F.TCEmb TC.TyCon)
, kuts :: !(F.Kuts)
, lits :: ![(F.Symbol, F.Sort)]
, tcheck :: !Bool
, scheck :: !Bool
, trustghc :: !Bool
, pruneRefs :: !Bool
, logErrors :: ![TError SpecType]
, kvProf :: !KVProf
, recCount :: !Int
}
instance PPrint CGInfo where
pprint cgi = ppr_CGInfo cgi
ppr_CGInfo _cgi
= (text "*********** Constraint Information ***********")
newtype HEnv = HEnv (S.HashSet F.Symbol)
fromListHEnv = HEnv . S.fromList
elemHEnv x (HEnv s) = x `S.member` s
type RTyConInv = M.HashMap RTyCon [SpecType]
type RTyConIAl = M.HashMap RTyCon [SpecType]
mkRTyConInv :: [F.Located SpecType] -> RTyConInv
mkRTyConInv ts = group [ (c, t) | t@(RApp c _ _ _) <- strip <$> ts]
where
strip = fourth4 . bkUniv . val
mkRTyConIAl = mkRTyConInv . fmap snd
addRTyConInv :: RTyConInv -> SpecType -> SpecType
addRTyConInv m t@(RApp c _ _ _)
= case M.lookup c m of
Nothing -> t
Just ts -> L.foldl' conjoinInvariant' t ts
addRTyConInv _ t
= t
addRInv :: RTyConInv -> (Var, SpecType) -> (Var, SpecType)
addRInv m (x, t)
| x `elem` ids , (RApp c _ _ _) <- res t, Just invs <- M.lookup c m
= (x, addInvCond t (mconcat $ catMaybes (stripRTypeBase <$> invs)))
| otherwise
= (x, t)
where
ids = [id | tc <- M.keys m
, dc <- TC.tyConDataCons $ rtc_tc tc
, id <- DC.dataConImplicitIds dc]
res = ty_res . toRTypeRep
conjoinInvariant' t1 t2
= conjoinInvariantShift t1 t2
conjoinInvariantShift t1 t2
= conjoinInvariant t1 (shiftVV t2 (rTypeValueVar t1))
conjoinInvariant (RApp c ts rs r) (RApp ic its _ ir)
| (c == ic && length ts == length its)
= RApp c (zipWith conjoinInvariantShift ts its) rs (r `F.meet` ir)
conjoinInvariant t@(RApp _ _ _ r) (RVar _ ir)
= t { rt_reft = r `F.meet` ir }
conjoinInvariant t@(RVar _ r) (RVar _ ir)
= t { rt_reft = r `F.meet` ir }
conjoinInvariant t _
= t
grapBindsWithType tx γ
= fst <$> toListREnv (filterREnv ((== toRSort tx) . toRSort) (renv γ))
toListREnv (REnv env) = M.toList env
filterREnv f (REnv env) = REnv $ M.filter f env
fromListREnv = REnv . M.fromList
deleteREnv x (REnv env) = REnv (M.delete x env)
insertREnv x y (REnv env) = REnv (M.insert x y env)
lookupREnv x (REnv env) = M.lookup x env
memberREnv x (REnv env) = M.member x env
data FEnv = FE { fe_binds :: !F.IBindEnv
, fe_env :: !(F.SEnv F.Sort)
}
insertFEnv (FE benv env) ((x, t), i)
= FE (F.insertsIBindEnv [i] benv) (F.insertSEnv x t env)
insertsFEnv = L.foldl' insertFEnv
initFEnv init = FE F.emptyIBindEnv $ F.fromListSEnv (wiredSortedSyms ++ init)