module Language.Haskell.Liquid.Types (
Config (..)
, GhcInfo (..)
, GhcSpec (..)
, TargetVars (..)
, Located (..)
, dummyLoc
, LocSymbol
, LocText
, dummyName, isDummy
, RTyCon (RTyCon, rtc_tc, rtc_info)
, TyConInfo(..)
, rTyConPVs
, rTyConPropVs
, isClassRTyCon
, RType (..), Ref(..), RTProp (..)
, 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, pToRef, pApp
, isBase
, isFunTy
, isTrivial
, efoldReft, foldReft
, mapReft, mapReftM
, mapBot, mapBind
, Oblig(..)
, ignoreOblig
, addTermCond
, addInvCond
, AnnInfo (..)
, Annot (..)
, Output (..)
, hole, isHole, hasHole
, ofRSort, toRSort
, rTypeValueVar
, rTypeReft
, stripRTypeBase
, PPrint (..)
, showpp
, PPEnv (..)
, Tidy (..)
, ppEnv
, ppEnvShort
, ModName (..), ModType (..)
, isSrcImport, isSpecImport
, getModName, getModString
, RTEnv (..)
, RTBareOrSpec
, mapRT, mapRP, mapRE
, Result (..)
, Error
, TError (..)
, EMsg (..)
, ErrorResult
, errSpan
, errOther
, Cinfo (..)
, Measure (..)
, CMeasure (..)
, Def (..)
, Body (..)
, RClass (..)
, KVKind (..)
, KVProf
, emptyKVProf
, updKVProf
, mapRTAVars
, insertsSEnv
, Stratum(..), Strata
, isSVar
, getStrata
, makeDivType, makeFinType
)
where
import FastString (fsLit)
import SrcLoc (noSrcSpan, mkGeneralSrcSpan, SrcSpan)
import TyCon
import DataCon
import Name (getName)
import NameSet
import Module (moduleNameFS)
import Class (classTyCon)
import TypeRep hiding (maybeParen, pprArrowChain)
import Var
import Unique
import Literal
import Text.Printf
import GHC (Class, HscEnv, ModuleName, Name, moduleNameString)
import GHC.Generics
import Language.Haskell.Liquid.GhcMisc
import PrelInfo (isNumericClass)
import TysWiredIn (listTyCon)
import Control.Arrow (second)
import Control.Monad (liftM, liftM2, liftM3)
import qualified Control.Monad.Error as Ex
import Control.DeepSeq
import Control.Applicative ((<$>), (<*>))
import Data.Typeable (Typeable)
import Data.Generics (Data)
import Data.Monoid hiding ((<>))
import qualified Data.Foldable as F
import Data.Hashable
import qualified Data.HashMap.Strict as M
import qualified Data.HashSet as S
import Data.Function (on)
import Data.Maybe (maybeToList, fromMaybe)
import Data.Traversable hiding (mapM)
import Data.List (isSuffixOf, nub, union, unionBy)
import Data.Text (Text)
import qualified Data.Text as T
import Data.Aeson hiding (Result)
import Text.Parsec.Pos (SourcePos, newPos, sourceName, sourceLine, sourceColumn)
import Text.Parsec.Error (ParseError)
import Text.PrettyPrint.HughesPJ
import Language.Fixpoint.Config hiding (Config)
import Language.Fixpoint.Misc
import Language.Fixpoint.Types hiding (Predicate, Def, R)
import Language.Fixpoint.Names (symSepName, isSuffixOfSym, singletonSym, funConName, listConName, tupConName)
import CoreSyn (CoreBind)
import Language.Haskell.Liquid.GhcMisc (isFractionalClass)
import System.FilePath ((</>), isAbsolute, takeDirectory)
import Data.Default
data Config = Config {
files :: [FilePath]
, idirs :: [FilePath]
, diffcheck :: Bool
, real :: Bool
, fullcheck :: Bool
, binders :: [String]
, noCheckUnknown :: Bool
, notermination :: Bool
, nowarnings :: Bool
, trustinternals :: Bool
, nocaseexpand :: Bool
, strata :: Bool
, notruetypes :: Bool
, totality :: Bool
, noPrune :: Bool
, maxParams :: Int
, smtsolver :: SMTSolver
, shortNames :: Bool
, shortErrors :: Bool
, ghcOptions :: [String]
, cFiles :: [String]
} deriving (Data, Typeable, Show, Eq)
data Tidy = Lossy | Full deriving (Eq, Ord)
class PPrint a where
pprint :: a -> Doc
pprintTidy :: Tidy -> a -> Doc
pprintTidy _ = pprint
showpp :: (PPrint a) => a -> String
showpp = render . pprint
showEMsg :: (PPrint a) => a -> EMsg
showEMsg = EMsg . showpp
instance PPrint a => PPrint (Maybe a) where
pprint = maybe (text "Nothing") ((text "Just" <+>) . pprint)
instance PPrint a => PPrint [a] where
pprint = brackets . intersperse comma . map pprint
instance (PPrint a, PPrint b) => PPrint (a,b) where
pprint (x, y) = pprint x <+> text ":" <+> pprint y
data PPEnv
= PP { ppPs :: Bool
, ppTyVar :: Bool
, ppSs :: Bool
, ppShort :: Bool
}
ppEnv = ppEnvPrintPreds
ppEnvCurrent = PP False False False False
ppEnvPrintPreds = PP True False False False
ppEnvShort pp = pp { ppShort = True }
data GhcInfo = GI {
env :: !HscEnv
, cbs :: ![CoreBind]
, derVars :: ![Var]
, impVars :: ![Var]
, defVars :: ![Var]
, useVars :: ![Var]
, hqFiles :: ![FilePath]
, imports :: ![String]
, includes :: ![FilePath]
, spec :: !GhcSpec
}
data GhcSpec = SP {
tySigs :: ![(Var, Located SpecType)]
, asmSigs :: ![(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)
, config :: !Config
, exports :: !NameSet
, measures :: [Measure SpecType DataCon]
, tyconEnv :: M.HashMap TyCon RTyCon
}
data TyConP = TyConP { freeTyVarsTy :: ![RTyVar]
, freePredTy :: ![PVar RSort]
, freeLabelTy :: ![Symbol]
, covPs :: ![Int]
, contravPs :: ![Int]
, sizeFun :: !(Maybe (Symbol -> Expr))
} deriving (Data, Typeable)
data DataConP = DataConP { dc_loc :: !SourcePos
, freeTyVars :: ![RTyVar]
, freePred :: ![PVar RSort]
, freeLabels :: ![Symbol]
, tyConsts :: ![SpecType]
, tyArgs :: ![(Symbol, SpecType)]
, tyRes :: !SpecType
} deriving (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)
pvType p = case ptype p of
PVProp t -> t
PVHProp -> errorstar "pvType on HProp-PVar"
data PVKind t
= PVProp t | PVHProp
deriving (Generic, Data, Typeable, F.Foldable, Traversable, Show)
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 Functor PVKind where
fmap f (PVProp t) = PVProp (f t)
fmap f (PVHProp) = PVHProp
instance Functor PVar where
fmap f (PV x t v txys) = PV x (f <$> t) v (mapFst3 f <$> txys)
instance (NFData a) => NFData (PVKind a) where
rnf (PVProp t) = rnf t
rnf (PVHProp) = ()
instance (NFData a) => NFData (PVar a) where
rnf (PV n t v txys) = rnf n `seq` rnf v `seq` rnf t `seq` rnf txys
instance Hashable (PVar a) where
hashWithSalt i (PV n _ _ xys) = hashWithSalt i n
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 = U mempty mempty mempty
mappend (U x y z) (U x' y' z') = U (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) where
rnf (U r p s) = rnf r `seq` rnf p `seq` rnf s
instance NFData Strata where
rnf _ = ()
instance NFData PrType where
rnf _ = ()
instance NFData RTyVar where
rnf _ = ()
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)
isClassRTyCon = isClassTyCon . rtc_tc
rTyConInfo = rtc_info
rTyConTc = rtc_tc
rTyConPVs = rtc_pvars
rTyConPropVs = filter isPropPV . rtc_pvars
isPropPV = isProp . ptype
isProp (PVProp _) = True
isProp _ = False
defaultTyConInfo = TyConInfo [] [] [] [] Nothing
instance Default TyConInfo where
def = defaultTyConInfo
data TyConInfo = TyConInfo
{ covariantTyArgs :: ![Int]
, contravariantTyArgs :: ![Int]
, covariantPsArgs :: ![Int]
, contravariantPsArgs :: ![Int]
, sizeFunction :: !(Maybe (Symbol -> Expr))
} deriving (Generic, Data, Typeable)
data RType p c tv r
= RVar {
rt_var :: !tv
, rt_reft :: !r
}
| RFun {
rt_bind :: !Symbol
, rt_in :: !(RType p c tv r)
, rt_out :: !(RType p c tv r)
, rt_reft :: !r
}
| RAllT {
rt_tvbind :: !tv
, rt_ty :: !(RType p c tv r)
}
| RAllP {
rt_pvbind :: !(PVar (RType p c tv ()))
, rt_ty :: !(RType p c tv r)
}
| RAllS {
rt_sbind :: !(Symbol)
, rt_ty :: !(RType p c tv r)
}
| RApp {
rt_tycon :: !c
, rt_args :: ![RType p c tv r]
, rt_pargs :: ![RTProp p c tv r]
, rt_reft :: !r
}
| RAllE {
rt_bind :: !Symbol
, rt_allarg :: !(RType p c tv r)
, rt_ty :: !(RType p c tv r)
}
| REx {
rt_bind :: !Symbol
, rt_exarg :: !(RType p c tv r)
, rt_ty :: !(RType p c tv r)
}
| RExprArg Expr
| RAppTy{
rt_arg :: !(RType p c tv r)
, rt_res :: !(RType p c tv r)
, rt_reft :: !r
}
| RRTy {
rt_env :: ![(Symbol, RType p c tv r)]
, rt_ref :: !r
, rt_obl :: !Oblig
, rt_ty :: !(RType p c tv r)
}
| ROth !Symbol
| RHole r
deriving (Generic, Data, Typeable)
data Oblig
= OTerm
| OInv
deriving (Generic, Data, Typeable)
ignoreOblig (RRTy _ _ _ t) = t
ignoreOblig t = t
instance Show Oblig where
show OTerm = "termination-condition"
show OInv = "invariant-obligation"
instance PPrint Oblig where
pprint = text . show
data Ref Ï„ r t
= RPropP {
rf_args :: [(Symbol, Ï„)]
, rf_reft :: r
}
| RProp {
rf_args :: [(Symbol, Ï„)]
, rf_body :: t
}
| RHProp {
rf_args :: [(Symbol, Ï„)]
, rf_heap :: World t
}
deriving (Generic, Data, Typeable)
type RTProp p c tv r = Ref (RType p c tv ()) r (RType p 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
= U { ur_reft :: !r, ur_pred :: !Predicate, ur_strata :: !Strata }
deriving (Generic, Data, Typeable)
type BRType = RType LocSymbol LocSymbol Symbol
type RRType = RType Class 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 r (RRType r)
data Stratum = SVar Symbol | SDiv | SWhnf | SFin
deriving (Generic, Data, Typeable, Eq)
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
isNumCls :: c -> Bool
isFracCls :: c -> Bool
isClass = const False
isNumCls = const False
isFracCls = const False
class ( TyConable c
, Eq p, Eq c, Eq tv
, Hashable tv
, Reftable r
, PPrint r
) => RefTypable p c tv r
where
ppCls :: p -> [RType p c tv r] -> Doc
ppRType :: Prec -> RType p c tv r -> Doc
instance TyConable RTyCon where
isFun = isFunTyCon . rtc_tc
isList = (listTyCon ==) . rtc_tc
isTuple = TyCon.isTupleTyCon . rtc_tc
isClass = isClassRTyCon
ppTycon = toFix
isNumCls c = maybe False isNumericClass (tyConClass_maybe $ rtc_tc c)
isFracCls c = maybe False isFractionalClass (tyConClass_maybe $ rtc_tc c)
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 PPrint RTyCon where
pprint = toFix
instance Show RTyCon where
show = showpp
data DataDecl = D { tycName :: LocSymbol
, tycTyVars :: [Symbol]
, tycPVars :: [PVar BSort]
, tycTyLabs :: [Symbol]
, tycDCons :: [(LocSymbol, [(Symbol, BareType)])]
, tycSrcPos :: !SourcePos
, tycSFun :: (Maybe (Symbol -> Expr))
}
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
}
mapRTAVars f rt = rt { rtTArgs = f <$> rtTArgs rt
, rtVArgs = f <$> rtVArgs rt
}
data RTypeRep p c tv r
= RTypeRep { ty_vars :: [tv]
, ty_preds :: [PVar (RType p c tv ())]
, ty_labels :: [Symbol]
, ty_binds :: [Symbol]
, ty_args :: [RType p c tv r]
, ty_res :: (RType p c tv r)
}
fromRTypeRep rep
= mkArrow (ty_vars rep) (ty_preds rep) (ty_labels rep) (zip (ty_binds rep) (ty_args rep)) (ty_res rep)
toRTypeRep :: RType p c tv r -> RTypeRep p c tv r
toRTypeRep t = RTypeRep αs πs ls xs ts t''
where
(αs, πs, ls, t') = bkUniv t
(xs, ts, t'') = bkArrow t'
mkArrow αs πs ls xts = mkUnivs αs πs ls . mkArrs xts
where
mkArrs xts t = foldr (uncurry rFun) t xts
bkArrowDeep (RAllT _ t) = bkArrowDeep t
bkArrowDeep (RAllP _ t) = bkArrowDeep t
bkArrowDeep (RAllS _ t) = bkArrowDeep t
bkArrowDeep (RFun x t t' _) = let (xs, ts, t'') = bkArrowDeep t' in (x:xs, t:ts, t'')
bkArrowDeep t = ([], [], t)
bkArrow (RFun x t t' _) = let (xs, ts, t'') = bkArrow t' in (x:xs, t:ts, t'')
bkArrow t = ([], [], t)
safeBkArrow (RAllT _ _) = errorstar "safeBkArrow on RAllT"
safeBkArrow (RAllP _ _) = errorstar "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 t t1 a t2 -> ([a], [PVar (RType t t1 a ())], [Symbol], RType t 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 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
addTermCond = addObligation OTerm
addInvCond :: SpecType -> RReft -> SpecType
addInvCond t r'
| null rv
= 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 = [RConc $ PIff (PBexp $ EVar v) $ subst1 r su | RConc r <- rv]
Reft(v, rv) = ur_reft r'
addObligation :: Oblig -> SpecType -> RReft -> SpecType
addObligation o t r = mkArrow αs πs ls xts $ RRTy [] r o t2
where (αs, πs, ls, t1) = bkUniv t
(xs, ts, t2) = bkArrow t1
xts = zip xs ts
instance Subable Stratum where
syms (SVar s) = [s]
syms _ = []
subst su (SVar s) = SVar $ subst su s
subst su s = s
substf f (SVar s) = SVar $ substf f s
substf f s = s
substa f (SVar s) = SVar $ substa f s
substa f s = s
instance Subable Strata where
syms s = concatMap syms s
subst su = (subst su <$>)
substf f = (substf f <$>)
substa f = (substa f <$>)
instance Reftable Strata where
isTauto [] = True
isTauto _ = False
ppTy s = error "ppTy on Strata"
toReft s = mempty
params s = [l | SVar l <- s]
bot s = []
top s = []
instance (PPrint r, Reftable r) => Reftable (UReft r) where
isTauto = isTauto_ureft
ppTy = ppTy_ureft
toReft (U r ps _) = toReft r `meet` toReft ps
params (U r _ _) = params r
bot (U r _ s) = U (bot r) (Pr []) (bot s)
top (U r p s) = U (top r) (top p) (top s)
isTauto_ureft u = isTauto (ur_reft u) && isTauto (ur_pred u) && (isTauto $ ur_strata u)
isTauto_ureft' u = isTauto (ur_reft u) && isTauto (ur_pred u)
ppTy_ureft u@(U r p s) d
| isTauto_ureft u = d
| isTauto_ureft' u = d <> ppr_str s
| otherwise = ppr_reft r (ppTy p d) s
ppr_reft r d s = braces (toFix 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 (U r p s) = syms r ++ syms p
subst s (U r z l) = U (subst s r) (subst s z) (subst s l)
substf f (U r z l) = U (substf f r) (substf f z) (substf f l)
substa f (U r z l) = U (substa f r) (substa f z) (substa f l)
instance (Reftable r, RefTypable p c tv r) => Subable (RTProp p c tv r) where
syms (RPropP ss r) = (fst <$> ss) ++ syms r
syms (RProp ss r) = (fst <$> ss) ++ syms r
subst su (RPropP ss r) = RPropP ss (subst su r)
subst su (RProp ss t) = RProp ss (subst su <$> t)
substf f (RPropP ss r) = RPropP ss (substf f r)
substf f (RProp ss t) = RProp ss (substf f <$> t)
substa f (RPropP ss r) = RPropP ss (substa f r)
substa f (RProp ss t) = RProp ss (substa f <$> t)
instance (Subable r, RefTypable p c tv r) => Subable (RType p 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 _) = errorstar "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, pToRef <$> ps)
toReft _ = mempty
params = errorstar "TODO: instance of params for Predicate"
pToRef p = RConc $ pApp (pname p) $ (EVar $ parg p) : (thd3 <$> pargs p)
pApp :: Symbol -> [Expr] -> Pred
pApp p es = PBexp $ EApp (dummyLoc $ pappSym $ length es) (EVar p:es)
pappSym n = symbol $ "papp" ++ show n
isTrivial t = foldReft (\r b -> isTauto r && b) True t
instance Functor UReft where
fmap f (U r p s) = U (f r) p s
instance Functor (RType a b c) where
fmap = mapReft
mapReft :: (r1 -> r2) -> RType p c tv r1 -> RType p c tv r2
mapReft f = emapReft (\_ -> f) []
emapReft :: ([Symbol] -> r1 -> r2) -> [Symbol] -> RType p c tv r1 -> RType p 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 _ _ (ROth s) = ROth s
emapReft f γ (RHole r) = RHole (f γ r)
emapRef :: ([Symbol] -> t -> s) -> [Symbol] -> RTProp p c tv t -> RTProp p c tv s
emapRef f γ (RPropP s r) = RPropP s $ f γ r
emapRef f γ (RProp s t) = RProp s $ emapReft f γ t
isBase (RAllP _ t) = isBase t
isBase (RVar _ _) = True
isBase (RApp _ ts _ _) = all isBase ts
isBase (RFun _ t1 t2 _) = isBase t1 && isBase t2
isBase (RAppTy t1 t2 _) = isBase t1 && isBase t2
isBase (RRTy _ _ _ 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 _ t1 t2 _) = True
isFunTy _ = False
mapReftM :: (Monad m) => (r1 -> m r2) -> RType p c tv r1 -> m (RType p 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 _ (ROth s) = return $ ROth s
mapReftM f (RHole r) = liftM RHole (f r)
mapRefM :: (Monad m) => (t -> m s) -> (RTProp p c tv t) -> m (RTProp p c tv s)
mapRefM f (RPropP s r) = liftM (RPropP s) (f r)
mapRefM f (RProp s t) = liftM (RProp s) (mapReftM f t)
foldReft f = efoldReft (\_ _ -> []) (\_ -> ()) (\_ _ -> f) (\_ γ -> γ) 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 s 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 (ROth _) = z
go γ z me@(RRTy e r o t) = f γ (Just me) r (go γ z 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 (RPropP ss 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
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 t' = f t'
mapBotRef _ (RPropP s r) = RPropP s $ 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 _ (ROth s) = ROth s
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 (RPropP s r) = RPropP (mapFst f <$> s) r
mapBindRef f (RProp s t) = RProp (mapFst f <$> s) $ mapBind f t
ofRSort :: Reftable r => RType p c tv () -> RType p c tv r
ofRSort = fmap mempty
toRSort :: RType p c tv r -> RType p c tv ()
toRSort = stripQuantifiers . mapBind (const dummySymbol) . fmap (const ())
stripQuantifiers (RAllT α t) = RAllT α (stripQuantifiers t)
stripQuantifiers (RAllP _ t) = stripQuantifiers t
stripQuantifiers (RAllS _ t) = stripQuantifiers t
stripQuantifiers (RAllE _ _ t) = stripQuantifiers t
stripQuantifiers (REx _ _ t) = stripQuantifiers t
stripQuantifiers (RFun x t t' r) = RFun x (stripQuantifiers t) (stripQuantifiers t') r
stripQuantifiers (RAppTy t t' r) = RAppTy (stripQuantifiers t) (stripQuantifiers t') r
stripQuantifiers (RApp c ts rs r) = RApp c (stripQuantifiers <$> ts) (stripQuantifiersRef <$> rs) r
stripQuantifiers t = t
stripQuantifiersRef (RProp s t) = RProp s $ stripQuantifiers t
stripQuantifiersRef r = r
insertsSEnv = foldr (\(x, t) γ -> insertSEnv x t γ)
rTypeValueVar :: (Reftable r) => RType p c tv r -> Symbol
rTypeValueVar t = vv where Reft (vv,_) = rTypeReft t
rTypeReft :: (Reftable r) => RType p 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 f t = t
makeLType :: Stratum -> SpecType -> SpecType
makeLType l t = fromRTypeRep trep{ty_res = mapRBase f $ ty_res trep}
where trep = toRTypeRep t
f (U r p s) = U 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
pprint = text . show
instance PPrint Strata where
pprint [] = empty
pprint ss = hsep (pprint <$> nub ss)
instance PPrint SourcePos where
pprint = text . show
instance PPrint () where
pprint = text . show
instance PPrint String where
pprint = text
instance PPrint Text where
pprint = text . T.unpack
instance PPrint a => PPrint (Located a) where
pprint = pprint . val
instance PPrint Int where
pprint = toFix
instance PPrint Integer where
pprint = toFix
instance PPrint Constant where
pprint = toFix
instance PPrint Brel where
pprint Eq = text "=="
pprint Ne = text "/="
pprint r = toFix r
instance PPrint Bop where
pprint = toFix
instance PPrint Sort where
pprint = toFix
instance PPrint Symbol where
pprint = pprint . symbolText
instance PPrint Expr where
pprint (EApp f es) = intersperse empty $ (pprint f) : (pprint <$> es)
pprint (ECon c) = pprint c
pprint (EVar s) = pprint s
pprint (ELit s _) = pprint s
pprint (EBin o e1 e2) = pprint e1 <+> pprint o <+> pprint e2
pprint (EIte p e1 e2) = text "if" <+> parens (pprint p) <+> text "then" <+> pprint e1 <+> text "else" <+> pprint e2
pprint (ECst e so) = parens $ pprint e <+> text " : " <+> pprint so
pprint (EBot) = text "_|_"
pprint (ESym s) = pprint s
instance PPrint SymConst where
pprint (SL s) = text $ T.unpack s
instance PPrint Pred where
pprint PTop = text "???"
pprint PTrue = trueD
pprint PFalse = falseD
pprint (PBexp e) = pprint e
pprint (PNot p) = text "not" <+> parens (pprint p)
pprint (PImp p1 p2) = pprint p1 <+> text "=>" <+> pprint p2
pprint (PIff p1 p2) = (pprint p1) <+> text "<=>" <+> (pprint p2)
pprint (PAnd ps) = pprintBin trueD andD ps
pprint (POr ps) = pprintBin falseD orD ps
pprint (PAtom r e1 e2) = pprint e1 <+> pprint r <+> pprint e2
pprint (PAll xts p) = text "forall" <+> toFix xts <+> text "." <+> pprint p
trueD = text "true"
falseD = text "false"
andD = text " &&"
orD = text " ||"
pprintBin b _ [] = b
pprintBin _ o xs = intersperse o $ pprint <$> xs
instance PPrint a => PPrint (PVar a) where
pprint (PV s _ _ xts) = pprint s <+> hsep (pprint <$> dargs xts)
where
dargs = map thd3 . takeWhile (\(_, x, y) -> EVar x /= y)
instance PPrint Predicate where
pprint (Pr []) = text "True"
pprint (Pr pvs) = hsep $ punctuate (text "&") (map pprint pvs)
instance PPrint Refa where
pprint (RConc p) = pprint p
pprint k = toFix k
instance PPrint Reft where
pprint r@(Reft (_,ras))
| isTauto r = text "true"
| otherwise = pprintBin trueD andD $ flattenRefas ras
instance PPrint SortedReft where
pprint (RR so (Reft (v, ras)))
= braces
$ (pprint v) <+> (text ":") <+> (toFix so) <+> (text "|") <+> pprint ras
newtype REnv = REnv (M.HashMap Symbol SpecType)
type ErrorResult = FixResult Error
newtype EMsg = EMsg String deriving (Generic, Data, Typeable)
instance PPrint EMsg where
pprint (EMsg s) = text s
type Error = TError SpecType
data TError t =
ErrSubType { pos :: !SrcSpan
, msg :: !Doc
, ctx :: !(M.HashMap Symbol t)
, tact :: !t
, texp :: !t
}
| ErrAssType { pos :: !SrcSpan
, obl :: !Oblig
, msg :: !Doc
, ref :: !RReft
}
| ErrParse { pos :: !SrcSpan
, msg :: !Doc
, err :: !ParseError
}
| ErrTySpec { pos :: !SrcSpan
, var :: !Doc
, typ :: !t
, msg :: !Doc
}
| ErrDupAlias { pos :: !SrcSpan
, var :: !Doc
, kind :: !Doc
, locs :: ![SrcSpan]
}
| ErrDupSpecs { pos :: !SrcSpan
, var :: !Doc
, locs:: ![SrcSpan]
}
| ErrInvt { pos :: !SrcSpan
, inv :: !t
, msg :: !Doc
}
| ErrIAl { pos :: !SrcSpan
, inv :: !t
, msg :: !Doc
}
| ErrIAlMis { pos :: !SrcSpan
, t1 :: !t
, t2 :: !t
, msg :: !Doc
}
| ErrMeas { pos :: !SrcSpan
, ms :: !Symbol
, msg :: !Doc
}
| ErrHMeas { pos :: !SrcSpan
, ms :: !Symbol
, msg :: !Doc
}
| ErrUnbound { pos :: !SrcSpan
, var :: !Doc
}
| ErrGhc { pos :: !SrcSpan
, msg :: !Doc
}
| ErrMismatch { pos :: !SrcSpan
, var :: !Doc
, hs :: !Type
, texp :: !t
}
| ErrAliasApp { pos :: !SrcSpan
, nargs :: !Int
, dname :: !Doc
, dpos :: !SrcSpan
, dargs :: !Int
}
| ErrSaved { pos :: !SrcSpan
, msg :: !Doc
}
| ErrTermin { bind :: ![Var]
, pos :: !SrcSpan
, msg :: !Doc
}
| ErrOther { pos :: !SrcSpan
, msg :: !Doc
}
deriving (Typeable, Functor)
instance Eq Error where
e1 == e2 = pos e1 == pos e2
instance Ord Error where
e1 <= e2 = pos e1 <= pos e2
instance Ex.Error Error where
strMsg = errOther . pprint
errSpan :: TError a -> SrcSpan
errSpan = pos
errOther :: Doc -> Error
errOther = ErrOther noSrcSpan
data Cinfo = Ci { ci_loc :: !SrcSpan
, ci_err :: !(Maybe Error)
}
deriving (Eq, Ord)
instance NFData Cinfo
class Result a where
result :: a -> FixResult Error
instance Result [Error] where
result es = Crash es ""
instance Result Error where
result (ErrOther _ d) = UnknownError $ render d
result e = result [e]
instance Result (FixResult Cinfo) where
result = fmap cinfoError
data ModName = ModName !ModType !ModuleName deriving (Eq,Ord)
instance Show ModName where
show = getModString
instance Symbolic ModName where
symbol (ModName t 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
type RTBareOrSpec = Either (ModName, (RTAlias Symbol BareType))
(RTAlias RTyVar SpecType)
type RTPredAlias = Either (ModName, RTAlias Symbol Pred)
(RTAlias Symbol Pred)
type RTExprAlias = Either (ModName, RTAlias Symbol Expr)
(RTAlias Symbol Expr)
data RTEnv = RTE { typeAliases :: M.HashMap Symbol RTBareOrSpec
, predAliases :: M.HashMap Symbol RTPredAlias
, exprAliases :: M.HashMap Symbol RTExprAlias
}
instance Monoid RTEnv where
(RTE ta1 pa1 ea1) `mappend` (RTE ta2 pa2 ea2)
= RTE (ta1 `M.union` ta2) (pa1 `M.union` pa2) (ea1 `M.union` ea2)
mempty = RTE M.empty M.empty M.empty
mapRT f e = e { typeAliases = f $ typeAliases e }
mapRP f e = e { predAliases = f $ predAliases e }
mapRE f e = e { exprAliases = f $ exprAliases e }
cinfoError (Ci _ (Just e)) = e
cinfoError (Ci l _) = errOther $ text $ "Cinfo:" ++ showPpr l
data Measure ty ctor = M {
name :: LocSymbol
, sort :: ty
, eqns :: [Def ctor]
} deriving (Data, Typeable)
data CMeasure ty
= CM { cName :: LocSymbol
, cSort :: ty
}
data Def ctor
= Def {
measure :: LocSymbol
, ctor :: ctor
, binds :: [Symbol]
, body :: Body
} deriving (Show, Data, Typeable)
deriving instance (Eq ctor) => Eq (Def ctor)
data Body
= E Expr
| P Pred
| R Symbol Pred
deriving (Show, Eq, Data, Typeable)
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 ctor) where
syms (Def _ _ _ bd) = syms bd
substa f (Def m c b bd) = Def m c b $ substa f bd
substf f (Def m c b bd) = Def m c b $ substf f bd
subst su (Def m c b bd) = Def m c 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)
instance Functor RClass where
fmap f (RClass n ss tvs ms) = RClass n (fmap f ss) tvs (fmap (second f) ms)
newtype AnnInfo a = AI (M.HashMap SrcSpan [(Maybe Text, a)]) deriving (Generic)
data Annot t = AnnUse t
| AnnDef t
| AnnRDf t
| AnnLoc SrcSpan
instance Monoid (AnnInfo a) where
mempty = AI M.empty
mappend (AI m1) (AI m2) = AI $ M.unionWith (++) m1 m2
instance Functor AnnInfo where
fmap f (AI m) = AI (fmap (fmap (\(x, y) -> (x, f y)) ) m)
instance NFData a => NFData (AnnInfo a) where
rnf (AI x) = ()
instance NFData (Annot a) where
rnf (AnnDef x) = ()
rnf (AnnRDf x) = ()
rnf (AnnUse x) = ()
rnf (AnnLoc x) = ()
data Output a = O { o_vars :: Maybe [String]
, o_errors :: ! [Error]
, o_types :: !(AnnInfo a)
, o_templs :: !(AnnInfo a)
, o_bots :: ![SrcSpan]
, o_result :: FixResult Error
} deriving (Generic)
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 where
hashWithSalt i = hashWithSalt i. fromEnum
newtype KVProf = KVP (M.HashMap KVKind Int)
emptyKVProf :: KVProf
emptyKVProf = KVP M.empty
updKVProf :: KVKind -> [Symbol] -> KVProf -> KVProf
updKVProf k kvs (KVP m) = KVP $ M.insert k (kn + length kvs) m
where
kn = M.lookupDefault 0 k m
instance NFData KVKind where
rnf z = z `seq` ()
instance PPrint KVKind where
pprint = text . show
instance PPrint KVProf where
pprint (KVP m) = pprint $ M.toList m
instance NFData KVProf where
rnf (KVP m) = rnf m `seq` ()
hole = RKvar "HOLE" mempty
isHole (RKvar ("HOLE") _) = True
isHole _ = False
hasHole (toReft -> (Reft (_, rs))) = any isHole rs
instance Symbolic DataCon where
symbol = symbol . dataConWorkId
instance Symbolic Var where
symbol = varSymbol
varSymbol :: Var -> Symbol
varSymbol v
| us `isSuffixOfSym` vs = vs
| otherwise = vs `mappend` singletonSym symSepName `mappend` us
where us = symbol $ showPpr $ getDataConVarUnique v
vs = symbol $ getName v
instance PPrint DataCon where
pprint = text . showPpr
instance Show DataCon where
show = showpp