module Language.Haskell.Liquid.Constraint.Types
(
CG
, CGInfo (..)
, CGEnv (..)
, LConstraint (..)
, FEnv (..)
, initFEnv
, insertsFEnv
, HEnv
, fromListHEnv
, elemHEnv
, SubC (..)
, FixSubC
, WfC (..)
, FixWfC
, RTyConInv
, mkRTyConInv
, addRTyConInv
, addRInv
, RTyConIAl
, mkRTyConIAl
) where
import Prelude hiding (error)
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.DeepSeq
import Data.Maybe (catMaybes)
import Control.Monad.State
import Var
import Language.Haskell.Liquid.GHC.SpanStack
import Language.Haskell.Liquid.Types hiding (binds)
import Language.Haskell.Liquid.Types.Strata
import Language.Haskell.Liquid.Misc (fourth4)
import Language.Haskell.Liquid.Types.RefType (shiftVV)
import Language.Haskell.Liquid.WiredIn (wiredSortedSyms)
import qualified Language.Fixpoint.Types as F
import Language.Fixpoint.Misc
import qualified Language.Haskell.Liquid.UX.CTags as Tg
type CG = State CGInfo
data CGEnv
= CGE { cgLoc :: !SpanStack
, renv :: !REnv
, syenv :: !(F.SEnv Var)
, denv :: !RDEnv
, fenv :: !FEnv
, recs :: !(S.HashSet Var)
, invs :: !RTyConInv
, ial :: !RTyConIAl
, grtys :: !REnv
, assms :: !REnv
, intys :: !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
, aenv :: !(M.HashMap Var F.Symbol)
, cerr :: !(Maybe (TError SpecType))
}
data LConstraint = LC [[(F.Symbol, SpecType)]]
instance Monoid LConstraint where
mempty = LC []
mappend (LC cs1) (LC cs2) = LC (cs1 ++ cs2)
instance PPrint CGEnv where
pprintTidy k = pprintTidy k . 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
pprintTidy k c@(SubC {}) = pprintTidy k (senv c)
$+$ ("||-" <+> vcat [ pprintTidy k (lhs c)
, "<:"
, pprintTidy k (rhs c) ] )
pprintTidy k c@(SubR {}) = pprintTidy k (senv c)
$+$ ("||-" <+> vcat [ pprintTidy k (ref c)
, parens (pprintTidy k (oblig c))])
instance PPrint WfC where
pprintTidy k (WfC _ r) = "<...> |-" <+> pprintTidy k r
instance SubStratum SubC where
subS su (SubC γ t1 t2) = SubC γ (subS su t1) (subS su t2)
subS _ c = c
data CGInfo = CGInfo {
fEnv :: !(F.SEnv F.Sort)
, 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)
, autoSize :: !(S.HashSet TC.TyCon)
, tyConEmbed :: !(F.TCEmb TC.TyCon)
, kuts :: !F.Kuts
, lits :: ![(F.Symbol, F.Sort)]
, tcheck :: !Bool
, scheck :: !Bool
, trustghc :: !Bool
, pruneRefs :: !Bool
, logErrors :: ![Error]
, kvProf :: !KVProf
, recCount :: !Int
, bindSpans :: M.HashMap F.BindId SrcSpan
, allowHO :: !Bool
}
instance PPrint CGInfo where
pprintTidy _ cgi = pprCGInfo cgi
pprCGInfo _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' conjoinInvariantShift 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
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
data FEnv = FE { feBinds :: !F.IBindEnv
, feEnv :: !(F.SEnv F.Sort)
}
insertFEnv (FE benv env) ((x, t), i)
= FE (F.insertsIBindEnv [i] benv) (F.insertSEnv x t env)
insertsFEnv :: FEnv -> [((F.Symbol, F.Sort), F.BindId)] -> FEnv
insertsFEnv = L.foldl' insertFEnv
initFEnv xts = FE F.emptyIBindEnv $ F.fromListSEnv (wiredSortedSyms ++ xts)
instance NFData CGEnv where
rnf (CGE x1 _ x3 _ x5 x6 x7 x8 x9 _ _ _ x10 _ _ _ _ _ _ _)
= x1 `seq` seq x3 `seq` rnf x5 `seq`
rnf x6 `seq` x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10
instance NFData FEnv where
rnf (FE x1 _) = rnf x1
instance NFData SubC where
rnf (SubC x1 x2 x3)
= rnf x1 `seq` rnf x2 `seq` rnf x3
rnf (SubR x1 _ x2)
= rnf x1 `seq` rnf x2
instance NFData WfC where
rnf (WfC x1 x2)
= rnf x1 `seq` rnf x2
instance NFData CGInfo where
rnf x = ( rnf (hsCs x)) `seq`
( rnf (hsWfs x)) `seq`
( rnf (fixCs x)) `seq`
( rnf (fixWfs x)) `seq`
( rnf (freshIndex x)) `seq`
( rnf (binds x)) `seq`
( rnf (annotMap x)) `seq`
( rnf (kuts x)) `seq`
( rnf (lits x)) `seq`
( rnf (kvProf x))