module Language.Haskell.Liquid.Types (
Config (..)
, HasConfig (..)
, hasOpt
, GhcInfo (..)
, GhcSpec (..)
, TargetVars (..)
, Located (..)
, dummyLoc
, LocSymbol
, LocText
, dummyName, isDummy
, RTyCon (RTyCon, rtc_tc, rtc_info)
, TyConInfo(..), defaultTyConInfo
, rTyConPVs
, rTyConPropVs
, isClassRTyCon, isClassType, isEqType
, RType (..), Ref(..), RTProp, rPropP
, RTyVar (..)
, RTAlias (..)
, HSeg (..)
, World (..)
, TyConable (..)
, RefTypable (..)
, SubsTy (..)
, PVar (PV, pname, parg, ptype, pargs), isPropPV, pvType
, PVKind (..)
, Predicate (..)
, UReft(..)
, DataDecl (..)
, DataConP (..)
, TyConP (..)
, RRType, BRType, RRProp
, BSort, BPVar
, BareType, PrType
, SpecType, SpecProp
, RSort
, UsedPVar, RPVar, RReft
, REnv (..)
, RTypeRep(..), fromRTypeRep, toRTypeRep
, mkArrow, bkArrowDeep, bkArrow, safeBkArrow
, mkUnivs, bkUniv, bkClass
, rFun, rCls, rRCls
, pvars, pappSym, pApp
, isBase
, isFunTy
, isTrivial
, efoldReft, foldReft, foldReft'
, mapReft, mapReftM
, mapBot, mapBind
, Oblig(..)
, ignoreOblig
, addInvCond
, AnnInfo (..)
, Annot (..)
, Output (..)
, hole, isHole, hasHole
, ofRSort, toRSort
, rTypeValueVar
, rTypeReft
, stripRTypeBase
, PPrint (..), pprint
, showpp
, PPEnv (..)
, ppEnv
, ppEnvShort
, ModName (..), ModType (..)
, isSrcImport, isSpecImport
, getModName, getModString
, RTEnv (..)
, mapRT, mapRE
, module Language.Haskell.Liquid.Types.Errors
, Error
, ErrorResult
, Cinfo (..)
, Measure (..)
, CMeasure (..)
, Def (..)
, Body (..)
, MSpec (..)
, RClass (..)
, KVKind (..)
, KVProf
, emptyKVProf
, updKVProf
, mapRTAVars
, insertsSEnv
, Stratum(..), Strata
, isSVar
, getStrata
, makeDivType, makeFinType
, LogicMap(..), toLogicMap, eAppWithMap, LMap(..)
, RDEnv, DEnv(..), RInstance(..)
, UReftable(..)
, liquidBegin, liquidEnd
, Axiom(..), HAxiom, LAxiom
)
where
import Prelude hiding (error)
import SrcLoc (SrcSpan)
import TyCon
import DataCon
import NameSet
import Module (moduleNameFS)
import TypeRep hiding (maybeParen, pprArrowChain)
import Var
import GHC (HscEnv, ModuleName, moduleNameString)
import GHC.Generics
import Class
import CoreSyn (CoreBind, CoreExpr)
import PrelInfo (isNumericClass)
import Type (getClassPredTys_maybe)
import TysPrim (eqPrimTyCon)
import TysWiredIn (listTyCon)
import Control.Monad (liftM, liftM2, liftM3, liftM4)
import Control.DeepSeq
import Data.Bifunctor
import Data.Bifunctor.TH
import Data.Typeable (Typeable)
import Data.Generics (Data)
import qualified Data.Foldable as F
import Data.Hashable
import qualified Data.HashMap.Strict as M
import qualified Data.HashSet as S
import Data.Maybe (fromMaybe, mapMaybe)
import Data.List (nub)
import Data.Text (Text)
import qualified Data.Text as T
import Text.PrettyPrint.HughesPJ hiding (first)
import Text.Printf
import Language.Fixpoint.Misc
import Language.Fixpoint.Types hiding (Error, SrcSpan, Result, Predicate, R)
import Language.Haskell.Liquid.GHC.Misc
import Language.Haskell.Liquid.Types.Variance
import Language.Haskell.Liquid.Types.Errors
import Language.Haskell.Liquid.Misc
import Language.Haskell.Liquid.UX.Config
import Data.Default
data PPEnv
= PP { ppPs :: Bool
, ppTyVar :: Bool
, ppSs :: Bool
, ppShort :: Bool
}
ppEnv = ppEnvCurrent
ppEnvCurrent = PP False False False False
_ppEnvPrintPreds = PP False False False False
ppEnvShort pp = pp { ppShort = True }
data GhcInfo = GI {
target :: !FilePath
, env :: !HscEnv
, cbs :: ![CoreBind]
, derVars :: ![Var]
, impVars :: ![Var]
, defVars :: ![Var]
, useVars :: ![Var]
, hqFiles :: ![FilePath]
, imports :: ![String]
, includes :: ![FilePath]
, spec :: !GhcSpec
}
instance HasConfig GhcInfo where
getConfig = getConfig . spec
data GhcSpec = SP {
tySigs :: ![(Var, Located SpecType)]
, asmSigs :: ![(Var, Located SpecType)]
, inSigs :: ![(Var, Located SpecType)]
, ctors :: ![(Var, Located SpecType)]
, meas :: ![(Symbol, Located SpecType)]
, invariants :: ![Located SpecType]
, ialiases :: ![(Located SpecType, Located SpecType)]
, dconsP :: ![(DataCon, DataConP)]
, tconsP :: ![(TyCon, TyConP)]
, freeSyms :: ![(Symbol, Var)]
, tcEmbeds :: TCEmb TyCon
, qualifiers :: ![Qualifier]
, tgtVars :: ![Var]
, decr :: ![(Var, [Int])]
, texprs :: ![(Var, [Expr])]
, lvars :: !(S.HashSet Var)
, lazy :: !(S.HashSet Var)
, autosize :: !(S.HashSet TyCon)
, config :: !Config
, exports :: !NameSet
, measures :: [Measure SpecType DataCon]
, tyconEnv :: M.HashMap TyCon RTyCon
, dicts :: DEnv Var SpecType
, axioms :: [HAxiom]
, logicMap :: LogicMap
, proofType :: Maybe Type
}
instance HasConfig GhcSpec where
getConfig = config
data LogicMap = LM { logic_map :: M.HashMap Symbol LMap
, axiom_map :: M.HashMap Var Symbol
} deriving (Show)
instance Monoid LogicMap where
mempty = LM M.empty M.empty
mappend (LM x1 x2) (LM y1 y2) = LM (M.union x1 y1) (M.union x2 y2)
data LMap = LMap { lvar :: Symbol
, largs :: [Symbol]
, lexpr :: Expr
}
instance Show LMap where
show (LMap x xs e) = show x ++ " " ++ show xs ++ "\t|->\t" ++ show e
toLogicMap ls = mempty {logic_map = M.fromList $ map toLMap ls}
where
toLMap (x, xs, e) = (x, LMap {lvar = x, largs = xs, lexpr = e})
eAppWithMap lmap f es def
| Just (LMap _ xs e) <- M.lookup (val f) (logic_map lmap), length xs == length es
= subst (mkSubst $ zip xs es) e
| Just (LMap _ xs e) <- M.lookup (val f) (logic_map lmap), isApp e
= subst (mkSubst $ zip xs es) $ dropApp e (length xs length es)
| otherwise
= def
dropApp e i | i <= 0 = e
dropApp (EApp e _) i = dropApp e (i1)
dropApp _ _ = errorstar "impossible"
isApp (EApp (EVar _) (EVar _)) = True
isApp (EApp e (EVar _)) = isApp e
isApp _ = False
data TyConP = TyConP { freeTyVarsTy :: ![RTyVar]
, freePredTy :: ![PVar RSort]
, freeLabelTy :: ![Symbol]
, varianceTs :: !VarianceInfo
, variancePs :: !VarianceInfo
, sizeFun :: !(Maybe (Symbol -> Expr))
} deriving (Generic, Data, Typeable)
data DataConP = DataConP { dc_loc :: !SourcePos
, freeTyVars :: ![RTyVar]
, freePred :: ![PVar RSort]
, freeLabels :: ![Symbol]
, tyConsts :: ![SpecType]
, tyArgs :: ![(Symbol, SpecType)]
, tyRes :: !SpecType
, dc_locE :: !SourcePos
} deriving (Generic, Data, Typeable)
data TargetVars = AllVars | Only ![Var]
data PVar t = PV
{ pname :: !Symbol
, ptype :: !(PVKind t)
, parg :: !Symbol
, pargs :: ![(t, Symbol, Expr)]
} deriving (Generic, Data, Typeable, Show, Functor)
instance Eq (PVar t) where
pv == pv' = pname pv == pname pv'
instance Ord (PVar t) where
compare (PV n _ _ _) (PV n' _ _ _) = compare n n'
instance NFData t => NFData (PVar t)
instance Hashable (PVar a) where
hashWithSalt i (PV n _ _ _) = hashWithSalt i n
pvType :: PVar t -> t
pvType p = case ptype p of
PVProp t -> t
PVHProp -> panic Nothing "pvType on HProp-PVar"
data PVKind t
= PVProp t
| PVHProp
deriving (Generic, Data, Typeable, Functor, F.Foldable, Traversable, Show)
instance NFData a => NFData (PVKind a)
type UsedPVar = PVar ()
newtype Predicate = Pr [UsedPVar] deriving (Generic, Data, Typeable)
instance NFData Predicate where
rnf _ = ()
instance Monoid Predicate where
mempty = pdTrue
mappend p p' = pdAnd [p, p']
instance (Monoid a) => Monoid (UReft a) where
mempty = MkUReft mempty mempty mempty
mappend (MkUReft x y z) (MkUReft x' y' z') = MkUReft (mappend x x') (mappend y y') (mappend z z')
pdTrue = Pr []
pdAnd ps = Pr (nub $ concatMap pvars ps)
pvars (Pr pvs) = pvs
instance Subable UsedPVar where
syms pv = [ y | (_, x, EVar y) <- pargs pv, x /= y ]
subst s pv = pv { pargs = mapThd3 (subst s) <$> pargs pv }
substf f pv = pv { pargs = mapThd3 (substf f) <$> pargs pv }
substa f pv = pv { pargs = mapThd3 (substa f) <$> pargs pv }
instance Subable Predicate where
syms (Pr pvs) = concatMap syms pvs
subst s (Pr pvs) = Pr (subst s <$> pvs)
substf f (Pr pvs) = Pr (substf f <$> pvs)
substa f (Pr pvs) = Pr (substa f <$> pvs)
instance Subable Qualifier where
syms = syms . q_body
subst = mapQualBody . subst
substf = mapQualBody . substf
substa = mapQualBody . substa
mapQualBody f q = q { q_body = f (q_body q) }
instance NFData r => NFData (UReft r)
instance NFData RTyVar
newtype RTyVar = RTV TyVar deriving (Generic, Data, Typeable)
instance Symbolic RTyVar where
symbol (RTV tv) = symbol . T.pack . showPpr $ tv
data RTyCon = RTyCon
{ rtc_tc :: TyCon
, rtc_pvars :: ![RPVar]
, rtc_info :: !TyConInfo
}
deriving (Generic, Data, Typeable)
instance NFData RTyCon
isClassRTyCon = isClassTyCon . rtc_tc
rTyConPVs = rtc_pvars
rTyConPropVs = filter isPropPV . rtc_pvars
isPropPV = isProp . ptype
isEqType (RApp c _ _ _) = isEqual c
isEqType _ = False
isClassType (RApp c _ _ _) = isClass c
isClassType _ = False
isProp (PVProp _) = True
isProp _ = False
defaultTyConInfo = TyConInfo [] [] Nothing
instance Default TyConInfo where
def = defaultTyConInfo
data TyConInfo = TyConInfo
{ varianceTyArgs :: !VarianceInfo
, variancePsArgs :: !VarianceInfo
, sizeFunction :: !(Maybe (Symbol -> Expr))
} deriving (Generic, Data, Typeable)
instance NFData TyConInfo
instance Show TyConInfo where
show (TyConInfo x y _) = show x ++ "\n" ++ show y
data RType c tv r
= RVar {
rt_var :: !tv
, rt_reft :: !r
}
| RFun {
rt_bind :: !Symbol
, rt_in :: !(RType c tv r)
, rt_out :: !(RType c tv r)
, rt_reft :: !r
}
| RAllT {
rt_tvbind :: !tv
, rt_ty :: !(RType c tv r)
}
| RAllP {
rt_pvbind :: !(PVar (RType c tv ()))
, rt_ty :: !(RType c tv r)
}
| RAllS {
rt_sbind :: !(Symbol)
, rt_ty :: !(RType c tv r)
}
| RApp {
rt_tycon :: !c
, rt_args :: ![RType c tv r]
, rt_pargs :: ![RTProp c tv r]
, rt_reft :: !r
}
| RAllE {
rt_bind :: !Symbol
, rt_allarg :: !(RType c tv r)
, rt_ty :: !(RType c tv r)
}
| REx {
rt_bind :: !Symbol
, rt_exarg :: !(RType c tv r)
, rt_ty :: !(RType c tv r)
}
| RExprArg (Located Expr)
| RAppTy{
rt_arg :: !(RType c tv r)
, rt_res :: !(RType c tv r)
, rt_reft :: !r
}
| RRTy {
rt_env :: ![(Symbol, RType c tv r)]
, rt_ref :: !r
, rt_obl :: !Oblig
, rt_ty :: !(RType c tv r)
}
| RHole r
deriving (Generic, Data, Typeable, Functor)
instance (NFData c, NFData tv, NFData r) => NFData (RType c tv r)
ignoreOblig (RRTy _ _ _ t) = t
ignoreOblig t = t
data Ref τ t = RProp
{ rf_args :: [(Symbol, τ)]
, rf_body :: t
} deriving (Generic, Data, Typeable, Functor)
instance (NFData τ, NFData t) => NFData (Ref τ t)
rPropP τ r = RProp τ (RHole r)
type RTProp c tv r = Ref (RType c tv ()) (RType c tv r)
newtype World t = World [HSeg t]
deriving (Generic, Data, Typeable)
data HSeg t = HBind {hs_addr :: !Symbol, hs_val :: t}
| HVar UsedPVar
deriving (Generic, Data, Typeable)
data UReft r
= MkUReft { ur_reft :: !r
, ur_pred :: !Predicate
, ur_strata :: !Strata
}
deriving (Generic, Data, Typeable, Functor)
type BRType = RType LocSymbol Symbol
type RRType = RType RTyCon RTyVar
type BSort = BRType ()
type RSort = RRType ()
type BPVar = PVar BSort
type RPVar = PVar RSort
type RReft = UReft Reft
type PrType = RRType Predicate
type BareType = BRType RReft
type SpecType = RRType RReft
type SpecProp = RRProp RReft
type RRProp r = Ref RSort (RRType r)
data Stratum = SVar Symbol | SDiv | SWhnf | SFin
deriving (Generic, Data, Typeable, Eq)
instance NFData Stratum
type Strata = [Stratum]
isSVar (SVar _) = True
isSVar _ = False
instance Monoid Strata where
mempty = []
mappend s1 s2 = nub $ s1 ++ s2
class SubsTy tv ty a where
subt :: (tv, ty) -> a -> a
class (Eq c) => TyConable c where
isFun :: c -> Bool
isList :: c -> Bool
isTuple :: c -> Bool
ppTycon :: c -> Doc
isClass :: c -> Bool
isEqual :: c -> Bool
isNumCls :: c -> Bool
isFracCls :: c -> Bool
isClass = const False
isEqual = const False
isNumCls = const False
isFracCls = const False
class ( TyConable c
, Eq c, Eq tv
, Hashable tv
, Reftable r
, PPrint r
) => RefTypable c tv r
where
ppRType :: Prec -> RType c tv r -> Doc
instance TyConable RTyCon where
isFun = isFunTyCon . rtc_tc
isList = (listTyCon ==) . rtc_tc
isTuple = TyCon.isTupleTyCon . rtc_tc
isClass = isClassRTyCon
isEqual = (eqPrimTyCon ==) . rtc_tc
ppTycon = toFix
isNumCls c = maybe False (isClassOrSubClass isNumericClass)
(tyConClass_maybe $ rtc_tc c)
isFracCls c = maybe False (isClassOrSubClass isFractionalClass)
(tyConClass_maybe $ rtc_tc c)
isClassOrSubClass p cls
= p cls || any (isClassOrSubClass p . fst)
(mapMaybe getClassPredTys_maybe (classSCTheta cls))
instance TyConable Symbol where
isFun s = funConName == s
isList s = listConName == s
isTuple s = tupConName == s
ppTycon = text . symbolString
instance TyConable LocSymbol where
isFun = isFun . val
isList = isList . val
isTuple = isTuple . val
ppTycon = ppTycon . val
instance Eq RTyCon where
x == y = rtc_tc x == rtc_tc y
instance Fixpoint RTyCon where
toFix (RTyCon c _ _) = text $ showPpr c
instance Fixpoint Cinfo where
toFix = text . showPpr . ci_loc
instance PPrint RTyCon where
pprintTidy _ = text . showPpr . rtc_tc
instance Show RTyCon where
show = showpp
data RInstance t = RI
{ riclass :: LocSymbol
, ritype :: t
, risigs :: [(LocSymbol, t)]
} deriving Functor
newtype DEnv x ty = DEnv (M.HashMap x (M.HashMap Symbol ty)) deriving (Monoid)
type RDEnv = DEnv Var SpecType
data Axiom b s e = Axiom { aname :: (Var, Maybe DataCon)
, abinds :: [b]
, atypes :: [s]
, alhs :: e
, arhs :: e
}
type HAxiom = Axiom Var Type CoreExpr
type LAxiom = Axiom Symbol Sort Expr
instance Show (Axiom Var Type CoreExpr) where
show (Axiom (n, c) bs _ts lhs rhs) = "Axiom : " ++
"\nFun Name: " ++ (showPpr n) ++
"\nData Con: " ++ (showPpr c) ++
"\nArguments:" ++ (showPpr bs) ++
"\nLHS :" ++ (showPpr lhs) ++
"\nRHS :" ++ (showPpr rhs)
data DataDecl = D { tycName :: LocSymbol
, tycTyVars :: [Symbol]
, tycPVars :: [PVar BSort]
, tycTyLabs :: [Symbol]
, tycDCons :: [(LocSymbol, [(Symbol, BareType)])]
, tycSrcPos :: !SourcePos
, tycSFun :: (Maybe (Symbol -> Expr))
}
instance Eq DataDecl where
d1 == d2 = tycName d1 == tycName d2
instance Ord DataDecl where
compare d1 d2 = compare (tycName d1) (tycName d2)
instance Show DataDecl where
show dd = printf "DataDecl: data = %s, tyvars = %s"
(show $ tycName dd)
(show $ tycTyVars dd)
data RTAlias tv ty
= RTA { rtName :: Symbol
, rtTArgs :: [tv]
, rtVArgs :: [tv]
, rtBody :: ty
, rtPos :: SourcePos
, rtPosE :: SourcePos
}
mapRTAVars f rt = rt { rtTArgs = f <$> rtTArgs rt
, rtVArgs = f <$> rtVArgs rt
}
data RTypeRep c tv r
= RTypeRep { ty_vars :: [tv]
, ty_preds :: [PVar (RType c tv ())]
, ty_labels :: [Symbol]
, ty_binds :: [Symbol]
, ty_refts :: [r]
, ty_args :: [RType c tv r]
, ty_res :: (RType c tv r)
}
fromRTypeRep (RTypeRep {..})
= mkArrow ty_vars ty_preds ty_labels arrs ty_res
where
arrs = safeZip3WithError ("fromRTypeRep: " ++ show (length ty_binds, length ty_args, length ty_refts)) ty_binds ty_args ty_refts
toRTypeRep :: RType c tv r -> RTypeRep c tv r
toRTypeRep t = RTypeRep αs πs ls xs rs ts t''
where
(αs, πs, ls, t') = bkUniv t
(xs, ts, rs, t'') = bkArrow t'
mkArrow αs πs ls xts = mkUnivs αs πs ls . mkArrs xts
where
mkArrs xts t = foldr (\(b,t1,r) t2 -> RFun b t1 t2 r) t xts
bkArrowDeep (RAllT _ t) = bkArrowDeep t
bkArrowDeep (RAllP _ t) = bkArrowDeep t
bkArrowDeep (RAllS _ t) = bkArrowDeep t
bkArrowDeep (RFun x t t' r) = let (xs, ts, rs, t'') = bkArrowDeep t' in (x:xs, t:ts, r:rs, t'')
bkArrowDeep t = ([], [], [], t)
bkArrow (RFun x t t' r) = let (xs, ts, rs, t'') = bkArrow t' in (x:xs, t:ts, r:rs, t'')
bkArrow t = ([], [], [], t)
safeBkArrow (RAllT _ _) = panic Nothing "safeBkArrow on RAllT"
safeBkArrow (RAllP _ _) = panic Nothing "safeBkArrow on RAllP"
safeBkArrow (RAllS _ t) = safeBkArrow t
safeBkArrow t = bkArrow t
mkUnivs αs πs ls t = foldr RAllT (foldr RAllP (foldr RAllS t ls) πs) αs
bkUniv :: RType t1 a t2 -> ([a], [PVar (RType t1 a ())], [Symbol], RType t1 a t2)
bkUniv (RAllT α t) = let (αs, πs, ls, t') = bkUniv t in (α:αs, πs, ls, t')
bkUniv (RAllP π t) = let (αs, πs, ls, t') = bkUniv t in (αs, π:πs, ls, t')
bkUniv (RAllS s t) = let (αs, πs, ss, t') = bkUniv t in (αs, πs, s:ss, t')
bkUniv t = ([], [], [], t)
bkClass (RFun _ (RApp c t _ _) t' _)
| isClass c
= let (cs, t'') = bkClass t' in ((c, t):cs, t'')
bkClass (RRTy e r o t)
= let (cs, t') = bkClass t in (cs, RRTy e r o t')
bkClass t
= ([], t)
rFun b t t' = RFun b t t' mempty
rCls c ts = RApp (RTyCon c [] defaultTyConInfo) ts [] mempty
rRCls rc ts = RApp rc ts [] mempty
addInvCond :: SpecType -> RReft -> SpecType
addInvCond t r'
| isTauto $ ur_reft r'
= t
| otherwise
= fromRTypeRep $ trep {ty_res = RRTy [(x', tbd)] r OInv tbd}
where
trep = toRTypeRep t
tbd = ty_res trep
r = r' {ur_reft = Reft (v, rx)}
su = (v, EVar x')
x' = "xInv"
rx = PIff (EVar v) $ subst1 rv su
Reft(v, rv) = ur_reft r'
instance Subable Stratum where
syms (SVar s) = [s]
syms _ = []
subst su (SVar s) = SVar $ subst su s
subst _ s = s
substf f (SVar s) = SVar $ substf f s
substf _ s = s
substa f (SVar s) = SVar $ substa f s
substa _ s = s
instance Reftable Strata where
isTauto [] = True
isTauto _ = False
ppTy _ = panic Nothing "ppTy on Strata"
toReft _ = mempty
params s = [l | SVar l <- s]
bot _ = []
top _ = []
ofReft = todo Nothing "TODO: Strata.ofReft"
class Reftable r => UReftable r where
ofUReft :: UReft Reft -> r
ofUReft (MkUReft r _ _) = ofReft r
instance UReftable (UReft Reft) where
ofUReft r = r
instance UReftable () where
ofUReft _ = mempty
instance (PPrint r, Reftable r) => Reftable (UReft r) where
isTauto = isTauto_ureft
ppTy = ppTy_ureft
toReft (MkUReft r ps _) = toReft r `meet` toReft ps
params (MkUReft r _ _) = params r
bot (MkUReft r _ s) = MkUReft (bot r) (Pr []) (bot s)
top (MkUReft r p s) = MkUReft (top r) (top p) s
ofReft r = MkUReft (ofReft r) mempty mempty
isTauto_ureft u = isTauto (ur_reft u) && isTauto (ur_pred u)
ppTy_ureft u@(MkUReft r p s) d
| isTauto_ureft u = d
| otherwise = ppr_reft r (ppTy p d) s
ppr_reft r d s = braces (pprint v <+> colon <+> d <> ppr_str s <+> text "|" <+> pprint r')
where
r'@(Reft (v, _)) = toReft r
ppr_str [] = empty
ppr_str s = text "^" <> pprint s
instance Subable r => Subable (UReft r) where
syms (MkUReft r p _) = syms r ++ syms p
subst s (MkUReft r z l) = MkUReft (subst s r) (subst s z) (subst s l)
substf f (MkUReft r z l) = MkUReft (substf f r) (substf f z) (substf f l)
substa f (MkUReft r z l) = MkUReft (substa f r) (substa f z) (substa f l)
instance (Reftable r, RefTypable c tv r) => Subable (RTProp c tv r) where
syms (RProp ss r) = (fst <$> ss) ++ syms r
subst su (RProp ss (RHole r)) = RProp ss (RHole (subst su r))
subst su (RProp ss t) = RProp ss (subst su <$> t)
substf f (RProp ss (RHole r)) = RProp ss (RHole (substf f r))
substf f (RProp ss t) = RProp ss (substf f <$> t)
substa f (RProp ss (RHole r)) = RProp ss (RHole (substa f r))
substa f (RProp ss t) = RProp ss (substa f <$> t)
instance (Subable r, RefTypable c tv r) => Subable (RType c tv r) where
syms = foldReft (\_ r acc -> syms r ++ acc) []
substa f = mapReft (substa f)
substf f = emapReft (substf . substfExcept f) []
subst su = emapReft (subst . substExcept su) []
subst1 t su = emapReft (\xs r -> subst1Except xs r su) [] t
instance Reftable Predicate where
isTauto (Pr ps) = null ps
bot (Pr _) = panic Nothing "No BOT instance for Predicate"
ppTy r d | isTauto r = d
| not (ppPs ppEnv) = d
| otherwise = d <> (angleBrackets $ pprint r)
toReft (Pr ps@(p:_)) = Reft (parg p, pAnd $ pToRef <$> ps)
toReft _ = mempty
params = todo Nothing "TODO: instance of params for Predicate"
ofReft = todo Nothing "TODO: Predicate.ofReft"
pToRef p = pApp (pname p) $ (EVar $ parg p) : (thd3 <$> pargs p)
pApp :: Symbol -> [Expr] -> Expr
pApp p es = mkEApp (dummyLoc $ pappSym $ length es) (EVar p:es)
pappSym n = symbol $ "papp" ++ show n
isTrivial t = foldReft (\_ r b -> isTauto r && b) True t
mapReft :: (r1 -> r2) -> RType c tv r1 -> RType c tv r2
mapReft f = emapReft (\_ -> f) []
emapReft :: ([Symbol] -> r1 -> r2) -> [Symbol] -> RType c tv r1 -> RType c tv r2
emapReft f γ (RVar α r) = RVar α (f γ r)
emapReft f γ (RAllT α t) = RAllT α (emapReft f γ t)
emapReft f γ (RAllP π t) = RAllP π (emapReft f γ t)
emapReft f γ (RAllS p t) = RAllS p (emapReft f γ t)
emapReft f γ (RFun x t t' r) = RFun x (emapReft f γ t) (emapReft f (x:γ) t') (f γ r)
emapReft f γ (RApp c ts rs r) = RApp c (emapReft f γ <$> ts) (emapRef f γ <$> rs) (f γ r)
emapReft f γ (RAllE z t t') = RAllE z (emapReft f γ t) (emapReft f γ t')
emapReft f γ (REx z t t') = REx z (emapReft f γ t) (emapReft f γ t')
emapReft _ _ (RExprArg e) = RExprArg e
emapReft f γ (RAppTy t t' r) = RAppTy (emapReft f γ t) (emapReft f γ t') (f γ r)
emapReft f γ (RRTy e r o t) = RRTy (mapSnd (emapReft f γ) <$> e) (f γ r) o (emapReft f γ t)
emapReft f γ (RHole r) = RHole (f γ r)
emapRef :: ([Symbol] -> t -> s) -> [Symbol] -> RTProp c tv t -> RTProp c tv s
emapRef f γ (RProp s (RHole r)) = RProp s $ RHole (f γ r)
emapRef f γ (RProp s t) = RProp s $ emapReft f γ t
isBase (RAllT _ t) = isBase t
isBase (RAllP _ t) = isBase t
isBase (RVar _ _) = True
isBase (RApp _ ts _ _) = all isBase ts
isBase (RFun _ _ _ _) = False
isBase (RAppTy t1 t2 _) = isBase t1 && isBase t2
isBase (RRTy _ _ _ t) = isBase t
isBase (RAllE _ _ t) = isBase t
isBase _ = False
isFunTy (RAllE _ _ t) = isFunTy t
isFunTy (RAllS _ t) = isFunTy t
isFunTy (RAllT _ t) = isFunTy t
isFunTy (RAllP _ t) = isFunTy t
isFunTy (RFun _ _ _ _) = True
isFunTy _ = False
mapReftM :: (Monad m) => (r1 -> m r2) -> RType c tv r1 -> m (RType c tv r2)
mapReftM f (RVar α r) = liftM (RVar α) (f r)
mapReftM f (RAllT α t) = liftM (RAllT α) (mapReftM f t)
mapReftM f (RAllP π t) = liftM (RAllP π) (mapReftM f t)
mapReftM f (RAllS s t) = liftM (RAllS s) (mapReftM f t)
mapReftM f (RFun x t t' r) = liftM3 (RFun x) (mapReftM f t) (mapReftM f t') (f r)
mapReftM f (RApp c ts rs r) = liftM3 (RApp c) (mapM (mapReftM f) ts) (mapM (mapRefM f) rs) (f r)
mapReftM f (RAllE z t t') = liftM2 (RAllE z) (mapReftM f t) (mapReftM f t')
mapReftM f (REx z t t') = liftM2 (REx z) (mapReftM f t) (mapReftM f t')
mapReftM _ (RExprArg e) = return $ RExprArg e
mapReftM f (RAppTy t t' r) = liftM3 RAppTy (mapReftM f t) (mapReftM f t') (f r)
mapReftM f (RHole r) = liftM RHole (f r)
mapReftM f (RRTy xts r o t) = liftM4 RRTy (mapM (mapSndM (mapReftM f)) xts) (f r) (return o) (mapReftM f t)
mapRefM :: (Monad m) => (t -> m s) -> (RTProp c tv t) -> m (RTProp c tv s)
mapRefM f (RProp s t) = liftM (RProp s) (mapReftM f t)
foldReft :: (Reftable r, TyConable c) => (SEnv (RType c tv r) -> r -> a -> a) -> a -> RType c tv r -> a
foldReft f = foldReft' id (\γ _ -> f γ)
foldReft' :: (Reftable r, TyConable c)
=> (RType c tv r -> b)
-> (SEnv b -> Maybe (RType c tv r) -> r -> a -> a)
-> a -> RType c tv r -> a
foldReft' g f = efoldReft (\_ _ -> []) g (\γ t r z -> f γ t r z) (\_ γ -> γ) emptySEnv
efoldReft cb g f fp = go
where
go γ z me@(RVar _ r) = f γ (Just me) r z
go γ z (RAllT _ t) = go γ z t
go γ z (RAllP p t) = go (fp p γ) z t
go γ z (RAllS _ t) = go γ z t
go γ z me@(RFun _ (RApp c ts _ _) t' r)
| isClass c = f γ (Just me) r (go (insertsSEnv γ (cb c ts)) (go' γ z ts) t')
go γ z me@(RFun x t t' r) = f γ (Just me) r (go (insertSEnv x (g t) γ) (go γ z t) t')
go γ z me@(RApp _ ts rs r) = f γ (Just me) r (ho' γ (go' (insertSEnv (rTypeValueVar me) (g me) γ) z ts) rs)
go γ z (RAllE x t t') = go (insertSEnv x (g t) γ) (go γ z t) t'
go γ z (REx x t t') = go (insertSEnv x (g t) γ) (go γ z t) t'
go γ z me@(RRTy [] r _ t) = f γ (Just me) r (go γ z t)
go γ z me@(RRTy xts r _ t) = f γ (Just me) r (go γ (go γ z (envtoType xts)) t)
go γ z me@(RAppTy t t' r) = f γ (Just me) r (go γ (go γ z t) t')
go _ z (RExprArg _) = z
go γ z me@(RHole r) = f γ (Just me) r z
ho γ z (RProp ss (RHole r)) = f (insertsSEnv γ (mapSnd (g . ofRSort) <$> ss)) Nothing r z
ho γ z (RProp ss t) = go (insertsSEnv γ ((mapSnd (g . ofRSort)) <$> ss)) z t
go' γ z ts = foldr (flip $ go γ) z ts
ho' γ z rs = foldr (flip $ ho γ) z rs
envtoType xts = foldr (\(x,t1) t2 -> rFun x t1 t2) (snd $ last xts) (init xts)
mapBot f (RAllT α t) = RAllT α (mapBot f t)
mapBot f (RAllP π t) = RAllP π (mapBot f t)
mapBot f (RAllS s t) = RAllS s (mapBot f t)
mapBot f (RFun x t t' r) = RFun x (mapBot f t) (mapBot f t') r
mapBot f (RAppTy t t' r) = RAppTy (mapBot f t) (mapBot f t') r
mapBot f (RApp c ts rs r) = f $ RApp c (mapBot f <$> ts) (mapBotRef f <$> rs) r
mapBot f (REx b t1 t2) = REx b (mapBot f t1) (mapBot f t2)
mapBot f (RAllE b t1 t2) = RAllE b (mapBot f t1) (mapBot f t2)
mapBot f (RRTy e r o t) = RRTy (mapSnd (mapBot f) <$> e) r o (mapBot f t)
mapBot f t' = f t'
mapBotRef _ (RProp s (RHole r)) = RProp s $ RHole r
mapBotRef f (RProp s t) = RProp s $ mapBot f t
mapBind f (RAllT α t) = RAllT α (mapBind f t)
mapBind f (RAllP π t) = RAllP π (mapBind f t)
mapBind f (RAllS s t) = RAllS s (mapBind f t)
mapBind f (RFun b t1 t2 r) = RFun (f b) (mapBind f t1) (mapBind f t2) r
mapBind f (RApp c ts rs r) = RApp c (mapBind f <$> ts) (mapBindRef f <$> rs) r
mapBind f (RAllE b t1 t2) = RAllE (f b) (mapBind f t1) (mapBind f t2)
mapBind f (REx b t1 t2) = REx (f b) (mapBind f t1) (mapBind f t2)
mapBind _ (RVar α r) = RVar α r
mapBind _ (RHole r) = RHole r
mapBind f (RRTy e r o t) = RRTy e r o (mapBind f t)
mapBind _ (RExprArg e) = RExprArg e
mapBind f (RAppTy t t' r) = RAppTy (mapBind f t) (mapBind f t') r
mapBindRef f (RProp s (RHole r)) = RProp (mapFst f <$> s) (RHole r)
mapBindRef f (RProp s t) = RProp (mapFst f <$> s) $ mapBind f t
ofRSort :: Reftable r => RType c tv () -> RType c tv r
ofRSort = fmap mempty
toRSort :: RType c tv r -> RType c tv ()
toRSort = stripAnnotations . mapBind (const dummySymbol) . fmap (const ())
stripAnnotations (RAllT α t) = RAllT α (stripAnnotations t)
stripAnnotations (RAllP _ t) = stripAnnotations t
stripAnnotations (RAllS _ t) = stripAnnotations t
stripAnnotations (RAllE _ _ t) = stripAnnotations t
stripAnnotations (REx _ _ t) = stripAnnotations t
stripAnnotations (RFun x t t' r) = RFun x (stripAnnotations t) (stripAnnotations t') r
stripAnnotations (RAppTy t t' r) = RAppTy (stripAnnotations t) (stripAnnotations t') r
stripAnnotations (RApp c ts rs r) = RApp c (stripAnnotations <$> ts) (stripAnnotationsRef <$> rs) r
stripAnnotations (RRTy _ _ _ t) = stripAnnotations t
stripAnnotations t = t
stripAnnotationsRef (RProp s (RHole r)) = RProp s (RHole r)
stripAnnotationsRef (RProp s t) = RProp s $ stripAnnotations t
insertsSEnv = foldr (\(x, t) γ -> insertSEnv x t γ)
rTypeValueVar :: (Reftable r) => RType c tv r -> Symbol
rTypeValueVar t = vv where Reft (vv,_) = rTypeReft t
rTypeReft :: (Reftable r) => RType c tv r -> Reft
rTypeReft = fromMaybe trueReft . fmap toReft . stripRTypeBase
stripRTypeBase (RApp _ _ _ x)
= Just x
stripRTypeBase (RVar _ x)
= Just x
stripRTypeBase (RFun _ _ _ x)
= Just x
stripRTypeBase (RAppTy _ _ x)
= Just x
stripRTypeBase _
= Nothing
mapRBase f (RApp c ts rs r) = RApp c ts rs $ f r
mapRBase f (RVar a r) = RVar a $ f r
mapRBase f (RFun x t1 t2 r) = RFun x t1 t2 $ f r
mapRBase f (RAppTy t1 t2 r) = RAppTy t1 t2 $ f r
mapRBase _ t = t
makeLType :: Stratum -> SpecType -> SpecType
makeLType l t = fromRTypeRep trep{ty_res = mapRBase f $ ty_res trep}
where trep = toRTypeRep t
f (MkUReft r p _) = MkUReft r p [l]
makeDivType = makeLType SDiv
makeFinType = makeLType SFin
getStrata = maybe [] ur_strata . stripRTypeBase
instance Show Stratum where
show SFin = "Fin"
show SDiv = "Div"
show SWhnf = "Whnf"
show (SVar s) = show s
instance PPrint Stratum where
pprintTidy _ = text . show
instance PPrint Strata where
pprintTidy _ [] = empty
pprintTidy k ss = hsep (pprintTidy k <$> nub ss)
instance PPrint (PVar a) where
pprintTidy _ = ppr_pvar
ppr_pvar :: PVar a -> Doc
ppr_pvar (PV s _ _ xts) = pprint s <+> hsep (pprint <$> dargs xts)
where
dargs = map thd3 . takeWhile (\(_, x, y) -> EVar x /= y)
instance PPrint Predicate where
pprintTidy _ (Pr []) = text "True"
pprintTidy k (Pr pvs) = hsep $ punctuate (text "&") (map (pprintTidy k) pvs)
data REnv = REnv
{ reGlobal :: M.HashMap Symbol SpecType
, reLocal :: M.HashMap Symbol SpecType
}
instance NFData REnv where
rnf (REnv {}) = ()
type ErrorResult = FixResult UserError
type Error = TError SpecType
instance NFData a => NFData (TError a)
data Cinfo = Ci { ci_loc :: !SrcSpan
, ci_err :: !(Maybe Error)
}
deriving (Eq, Ord, Generic)
instance NFData Cinfo
data ModName = ModName !ModType !ModuleName deriving (Eq,Ord)
instance Show ModName where
show = getModString
instance Symbolic ModName where
symbol (ModName _ m) = symbol m
instance Symbolic ModuleName where
symbol = symbol . moduleNameFS
data ModType = Target | SrcImport | SpecImport deriving (Eq,Ord)
isSrcImport (ModName SrcImport _) = True
isSrcImport _ = False
isSpecImport (ModName SpecImport _) = True
isSpecImport _ = False
getModName (ModName _ m) = m
getModString = moduleNameString . getModName
data RTEnv = RTE { typeAliases :: M.HashMap Symbol (RTAlias RTyVar SpecType)
, exprAliases :: M.HashMap Symbol (RTAlias Symbol Expr)
}
instance Monoid RTEnv where
(RTE ta1 ea1) `mappend` (RTE ta2 ea2)
= RTE (ta1 `M.union` ta2) (ea1 `M.union` ea2)
mempty = RTE M.empty M.empty
mapRT f e = e { typeAliases = f $ typeAliases e }
mapRE f e = e { exprAliases = f $ exprAliases e }
data Body
= E Expr
| P Expr
| R Symbol Expr
deriving (Show, Data, Typeable, Generic, Eq)
data Def ty ctor = Def
{ measure :: LocSymbol
, dparams :: [(Symbol, ty)]
, ctor :: ctor
, dsort :: Maybe ty
, binds :: [(Symbol, Maybe ty)]
, body :: Body
} deriving (Show, Data, Typeable, Generic, Eq, Functor)
data Measure ty ctor = M
{ name :: LocSymbol
, sort :: ty
, eqns :: [Def ty ctor]
} deriving (Data, Typeable, Generic, Functor)
deriveBifunctor ''Def
deriveBifunctor ''Measure
data CMeasure ty = CM
{ cName :: LocSymbol
, cSort :: ty
} deriving (Data, Typeable, Generic, Functor)
instance PPrint Body where
pprintTidy k (E e) = pprintTidy k e
pprintTidy k (P p) = pprintTidy k p
pprintTidy k (R v p) = braces (pprintTidy k v <+> text "|" <+> pprintTidy k p)
instance PPrint a => PPrint (Def t a) where
pprintTidy k (Def m p c _ bs body) = pprintTidy k m <+> pprintTidy k (fst <$> p) <+> cbsd <> text " = " <> pprintTidy k body
where cbsd = parens (pprintTidy k c <> hsep (pprintTidy k `fmap` (fst <$> bs)))
instance (PPrint t, PPrint a) => PPrint (Measure t a) where
pprintTidy k (M n s eqs) = pprintTidy k n <> text " :: " <> pprintTidy k s
$$ vcat (pprintTidy k `fmap` eqs)
instance PPrint (Measure t a) => Show (Measure t a) where
show = showpp
instance PPrint t => PPrint (CMeasure t) where
pprintTidy k (CM n s) = pprintTidy k n <> text " :: " <> pprintTidy k s
instance PPrint (CMeasure t) => Show (CMeasure t) where
show = showpp
instance Subable (Measure ty ctor) where
syms (M _ _ es) = concatMap syms es
substa f (M n s es) = M n s $ substa f <$> es
substf f (M n s es) = M n s $ substf f <$> es
subst su (M n s es) = M n s $ subst su <$> es
instance Subable (Def ty ctor) where
syms (Def _ sp _ _ sb bd) = (fst <$> sp) ++ (fst <$> sb) ++ syms bd
substa f (Def m p c t b bd) = Def m p c t b $ substa f bd
substf f (Def m p c t b bd) = Def m p c t b $ substf f bd
subst su (Def m p c t b bd) = Def m p c t b $ subst su bd
instance Subable Body where
syms (E e) = syms e
syms (P e) = syms e
syms (R s e) = s:syms e
substa f (E e) = E $ substa f e
substa f (P e) = P $ substa f e
substa f (R s e) = R s $ substa f e
substf f (E e) = E $ substf f e
substf f (P e) = P $ substf f e
substf f (R s e) = R s $ substf f e
subst su (E e) = E $ subst su e
subst su (P e) = P $ subst su e
subst su (R s e) = R s $ subst su e
data RClass ty
= RClass { rcName :: LocSymbol
, rcSupers :: [ty]
, rcTyVars :: [Symbol]
, rcMethods :: [(LocSymbol,ty)]
} deriving (Show, Functor)
newtype AnnInfo a = AI (M.HashMap SrcSpan [(Maybe Text, a)])
deriving (Data, Typeable, Generic, Functor)
data Annot t
= AnnUse t
| AnnDef t
| AnnRDf t
| AnnLoc SrcSpan
deriving (Data, Typeable, Generic, Functor)
instance Monoid (AnnInfo a) where
mempty = AI M.empty
mappend (AI m1) (AI m2) = AI $ M.unionWith (++) m1 m2
instance NFData a => NFData (AnnInfo a)
instance NFData a => NFData (Annot a)
data Output a = O
{ o_vars :: Maybe [String]
, o_errors :: ![UserError]
, o_types :: !(AnnInfo a)
, o_templs :: !(AnnInfo a)
, o_bots :: ![SrcSpan]
, o_result :: ErrorResult
} deriving (Typeable, Generic, Functor)
emptyOutput = O Nothing [] mempty mempty [] mempty
instance Monoid (Output a) where
mempty = emptyOutput
mappend o1 o2 = O { o_vars = sortNub <$> mappend (o_vars o1) (o_vars o2)
, o_errors = sortNub $ mappend (o_errors o1) (o_errors o2)
, o_types = mappend (o_types o1) (o_types o2)
, o_templs = mappend (o_templs o1) (o_templs o2)
, o_bots = sortNub $ mappend (o_bots o1) (o_bots o2)
, o_result = mappend (o_result o1) (o_result o2)
}
data KVKind
= RecBindE
| NonRecBindE
| TypeInstE
| PredInstE
| LamE
| CaseE
| LetE
deriving (Generic, Eq, Ord, Show, Enum, Data, Typeable)
instance Hashable KVKind
newtype KVProf = KVP (M.HashMap KVKind Int) deriving (Generic)
emptyKVProf :: KVProf
emptyKVProf = KVP M.empty
updKVProf :: KVKind -> Kuts -> KVProf -> KVProf
updKVProf k kvs (KVP m) = KVP $ M.insert k (kn + n) m
where
kn = M.lookupDefault 0 k m
n = S.size $ ksVars kvs
instance NFData KVKind
instance PPrint KVKind where
pprintTidy _ = text . show
instance PPrint KVProf where
pprintTidy k (KVP m) = pprintTidy k $ M.toList m
instance NFData KVProf
hole :: Expr
hole = PKVar "HOLE" mempty
isHole :: Expr -> Bool
isHole (PKVar ("HOLE") _) = True
isHole _ = False
hasHole :: Reftable r => r -> Bool
hasHole = any isHole . conjuncts . reftPred . toReft
instance Symbolic DataCon where
symbol = symbol . dataConWorkId
instance PPrint DataCon where
pprintTidy _ = text . showPpr
instance Show DataCon where
show = showpp
liquidBegin :: String
liquidBegin = ['{', '-', '@']
liquidEnd :: String
liquidEnd = ['@', '-', '}']
data MSpec ty ctor = MSpec
{ ctorMap :: M.HashMap Symbol [Def ty ctor]
, measMap :: M.HashMap LocSymbol (Measure ty ctor)
, cmeasMap :: M.HashMap LocSymbol (Measure ty ())
, imeas :: ![Measure ty ctor]
} deriving (Data, Typeable, Generic, Functor)
instance Bifunctor MSpec where
first f (MSpec c m cm im) = MSpec (fmap (fmap (first f)) c)
(fmap (first f) m)
(fmap (first f) cm)
(fmap (first f) im)
second = fmap
instance (PPrint t, PPrint a) => PPrint (MSpec t a) where
pprintTidy k = vcat . fmap (pprintTidy k) . fmap snd . M.toList . measMap
instance (Show ty, Show ctor, PPrint ctor, PPrint ty) => Show (MSpec ty ctor) where
show (MSpec ct m cm im)
= "\nMSpec:\n" ++
"\nctorMap:\t " ++ show ct ++
"\nmeasMap:\t " ++ show m ++
"\ncmeasMap:\t " ++ show cm ++
"\nimeas:\t " ++ show im ++
"\n"
instance Eq ctor => Monoid (MSpec ty ctor) where
mempty = MSpec M.empty M.empty M.empty []
(MSpec c1 m1 cm1 im1) `mappend` (MSpec c2 m2 cm2 im2)
| null dups
= MSpec (M.unionWith (++) c1 c2) (m1 `M.union` m2)
(cm1 `M.union` cm2) (im1 ++ im2)
| otherwise
= panic Nothing $ err (head dups)
where dups = [(k1, k2) | k1 <- M.keys m1 , k2 <- M.keys m2, val k1 == val k2]
err (k1, k2) = printf "\nDuplicate Measure Definitions for %s\n%s" (showpp k1) (showpp $ map loc [k1, k2])
instance PPrint RTyVar where
pprintTidy _k (RTV α)
| ppTyVar ppEnv = ppr_tyvar α
| otherwise = ppr_tyvar_short α
ppr_tyvar = text . tvId
ppr_tyvar_short = text . showPpr
instance (PPrint r, Reftable r, PPrint t, PPrint (RType c tv r)) => PPrint (Ref t (RType c tv r)) where
pprintTidy k (RProp ss s) = ppRefArgs (fst <$> ss) <+> pprintTidy k s
ppRefArgs :: [Symbol] -> Doc
ppRefArgs [] = empty
ppRefArgs ss = text "\\" <> hsep (ppRefSym <$> ss ++ [vv Nothing]) <+> text "->"
ppRefSym "" = text "_"
ppRefSym s = pprint s