liquidhaskell-0.2.0.0: src/Language/Haskell/Liquid/RefType.hs
{-# LANGUAGE IncoherentInstances #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternGuards #-}
-- | Refinement Types. Mostly mirroring the GHC Type definition, but with
-- room for refinements of various sorts.
-- TODO: Desperately needs re-organization.
module Language.Haskell.Liquid.RefType (
-- * Functions for lifting Reft-values to Spec-values
uTop, uReft, uRType, uRType', uRTypeGen, uPVar
-- * Applying a solution to a SpecType
, applySolution
-- * Functions for decreasing arguments
, isDecreasing, makeDecrType
, makeLexRefa
-- * Functions for manipulating `Predicate`s
, pdVar
, findPVar
, freeTyVars, tyClasses, tyConName
-- TODO: categorize these!
, ofType, ofPredTree, toType
, rTyVar, rVar, rApp, rEx
, addTyConInfo
-- , expandRApp
, appRTyCon
, typeSort, typeUniqueSymbol
, strengthen
, generalize, normalizePds
, subts, subvPredicate, subvUReft
, subsTyVar_meet, subsTyVars_meet, subsTyVar_nomeet, subsTyVars_nomeet
, dataConSymbol, dataConMsReft, dataConReft
, literalFRefType, literalFReft, literalConst
, classBinds
-- * Manipulating Refinements in RTypes
, rTypeSortedReft
, rTypeSort
, shiftVV
, mkDataConIdsTy
, mkTyConInfo
) where
import WwLib
import FamInstEnv (emptyFamInstEnv)
import Var
import Literal
import GHC hiding (Located)
import DataCon
import PrelInfo (isNumericClass)
import qualified TyCon as TC
import TypeRep hiding (maybeParen, pprArrowChain)
import Type (mkClassPred, splitFunTys, expandTypeSynonyms, isPredTy, substTyWith, classifyPredType, PredTree(..), isClassPred)
import TysWiredIn (listTyCon, intDataCon, trueDataCon, falseDataCon)
import qualified Data.Text as T
import Data.Interned
import Data.Monoid hiding ((<>))
import Data.Maybe (fromMaybe, isJust)
import Data.Hashable
import Data.Aeson
import qualified Data.HashMap.Strict as M
import qualified Data.HashSet as S
import qualified Data.List as L
import Data.Function (on)
import Control.Applicative hiding (empty)
import Control.DeepSeq
import Control.Monad (liftM, liftM2, liftM3, void)
import Control.Exception (Exception (..))
import qualified Data.Foldable as Fold
import Text.Printf
import Text.PrettyPrint.HughesPJ
import Text.Parsec.Pos (SourcePos)
import Language.Haskell.Liquid.PrettyPrint
import qualified Language.Fixpoint.Types as F
import Language.Fixpoint.Types hiding (shiftVV, Predicate)
import Language.Haskell.Liquid.Types hiding (R, DataConP (..), sort)
import Language.Haskell.Liquid.World
import Language.Haskell.Liquid.Misc
import Language.Fixpoint.Misc
import Language.Haskell.Liquid.GhcMisc (pprDoc, sDocDoc, typeUniqueString, tracePpr, tvId, getDataConVarUnique, showSDoc, showPpr, showSDocDump)
import Language.Fixpoint.Names (dropModuleNames, symSepName, funConName, listConName, tupConName)
import Data.List (sort, isSuffixOf, foldl')
pdVar v = Pr [uPVar v]
findPVar :: [PVar (RType p c tv ())] -> UsedPVar -> PVar (RType p c tv ())
findPVar ps p
= PV name ty v (zipWith (\(_, _, e) (t, s, _) -> (t, s, e)) (pargs p) args)
where PV name ty v args = fromMaybe (msg p) $ L.find ((== pname p) . pname) ps
msg p = errorstar $ "RefType.findPVar" ++ showpp p ++ "not found"
-- | Various functions for converting vanilla `Reft` to `Spec`
uRType :: RType p c tv a -> RType p c tv (UReft a)
uRType = fmap uTop
uRType' :: RType p c tv (UReft a) -> RType p c tv a
uRType' = fmap ur_reft
uRTypeGen :: Reftable b => RType p c tv a -> RType p c tv b
uRTypeGen = fmap $ const mempty
uPVar :: PVar t -> UsedPVar
uPVar = void -- fmap (const ())
uReft :: (Symbol, [Refa]) -> UReft Reft
uReft = uTop . Reft
uTop :: r -> UReft r
uTop r = U r mempty mempty
--------------------------------------------------------------------
-------------- (Class) Predicates for Valid Refinement Types -------
--------------------------------------------------------------------
-- Monoid Instances ---------------------------------------------------------
instance ( SubsTy tv (RType p c tv ()) (RType p c tv ())
, SubsTy tv (RType p c tv ()) c
, RefTypable p c tv ()
, RefTypable p c tv r
, PPrint (RType p c tv r)
)
=> Monoid (RType p c tv r) where
mempty = errorstar "mempty: RType"
mappend = strengthenRefType
-- MOVE TO TYPES
instance ( SubsTy tv (RType p c tv ()) (RType p c tv ())
, SubsTy tv (RType p c tv ()) c
, Reftable r
, RefTypable p c tv ()
, RefTypable p c tv (UReft r))
=> Monoid (Ref (RType p c tv ()) r (RType p c tv (UReft r))) where
mempty = errorstar "mempty: RType 2"
mappend _ _ = errorstar "mappend: RType 2"
instance ( Monoid r, Reftable r, RefTypable a b c r, RefTypable a b c ()) => Monoid (RTProp a b c r) where
mempty = errorstar "mempty: RTProp"
mappend (RPropP s1 r1) (RPropP s2 r2)
| isTauto r1 = RPropP s2 r2
| isTauto r2 = RPropP s1 r1
| otherwise = RPropP (s1 ++ s2) $ r1 `meet` r2
mappend (RProp s1 t1) (RProp s2 t2)
| isTrivial t1 = RProp s2 t2
| isTrivial t2 = RProp s1 t1
| otherwise = RProp (s1 ++ s2) $ t1 `strengthenRefType` t2
instance (Reftable r, RefTypable p c tv r, RefTypable p c tv ()) => Reftable (RTProp p c tv r) where
isTauto (RPropP _ r) = isTauto r
isTauto (RProp _ t) = isTrivial t
top (RProp xs t) = RProp xs $ mapReft top t
ppTy (RPropP _ r) d = ppTy r d
ppTy (RProp _ _) _ = errorstar "RefType: Reftable ppTy in RProp"
toReft = errorstar "RefType: Reftable toReft"
params = errorstar "RefType: Reftable params for Ref"
bot = errorstar "RefType: Reftable bot for Ref"
----------------------------------------------------------------------------
-- | Subable Instances -----------------------------------------------------
----------------------------------------------------------------------------
instance Subable (RRProp Reft) where
syms (RPropP ss r) = (fst <$> ss) ++ syms r
syms (RProp ss t) = (fst <$> ss) ++ syms t
syms _ = error "TODO:EFFECTS"
subst su (RPropP ss r) = RPropP (mapSnd (subst su) <$> ss) $ subst su r
subst su (RProp ss r) = RProp (mapSnd (subst su) <$> ss) $ subst su r
subst _ _ = error "TODO:EFFECTS"
substf f (RPropP ss r) = RPropP (mapSnd (substf f) <$> ss) $ substf f r
substf f (RProp ss r) = RProp (mapSnd (substf f) <$> ss) $ substf f r
substa f (RPropP ss r) = RPropP (mapSnd (substa f) <$> ss) $ substa f r
substa f (RProp ss r) = RProp (mapSnd (substa f) <$> ss) $ substa f r
substa f _ = error "TODO:EFFECTS"
-------------------------------------------------------------------------------
-- | Reftable Instances -------------------------------------------------------
-------------------------------------------------------------------------------
instance (PPrint r, Reftable r) => Reftable (RType Class RTyCon RTyVar r) where
isTauto = isTrivial
ppTy = errorstar "ppTy RProp Reftable"
toReft = errorstar "toReft on RType"
params = errorstar "params on RType"
bot = errorstar "bot on RType"
-------------------------------------------------------------------------------
-- | TyConable Instances -------------------------------------------------------
-------------------------------------------------------------------------------
-- MOVE TO TYPES
instance TyConable RTyCon where
isFun = isFunTyCon . rtc_tc
isList = (listTyCon ==) . rtc_tc
isTuple = TC.isTupleTyCon . rtc_tc
ppTycon = toFix
-- MOVE TO TYPES
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
-------------------------------------------------------------------------------
-- | RefTypable Instances -----------------------------------------------------
-------------------------------------------------------------------------------
-- MOVE TO TYPES
instance Fixpoint String where
toFix = text
-- MOVE TO TYPES
instance Fixpoint Class where
toFix = text . showPpr
-- MOVE TO TYPES
instance (Eq p, PPrint p, TyConable c, Reftable r, PPrint r) => RefTypable p c Symbol r where
ppCls = ppClassSymbol
ppRType = ppr_rtype ppEnv
-- MOVE TO TYPES
instance (Reftable r, PPrint r) => RefTypable Class RTyCon RTyVar r where
ppCls = ppClassClassPred
ppRType = ppr_rtype ppEnv
-- MOVE TO TYPES
class FreeVar a v where
freeVars :: a -> [v]
-- MOVE TO TYPES
instance FreeVar RTyCon RTyVar where
freeVars = (RTV <$>) . tyConTyVars . rtc_tc
-- MOVE TO TYPES
instance FreeVar LocSymbol Symbol where
freeVars _ = []
ppClassSymbol c _ = pprint c <+> text "..."
ppClassClassPred c ts = sDocDoc $ pprClassPred c (toType <$> ts)
-- Eq Instances ------------------------------------------------------
-- MOVE TO TYPES
instance (RefTypable p c tv ()) => Eq (RType p c tv ()) where
(==) = eqRSort M.empty
eqRSort m (RAllP _ t) (RAllP _ t')
= eqRSort m t t'
eqRSort m (RAllS _ t) (RAllS _ t')
= eqRSort m t t'
eqRSort m (RAllP _ t) t'
= eqRSort m t t'
eqRSort m (RAllT a t) (RAllT a' t')
| a == a'
= eqRSort m t t'
| otherwise
= eqRSort (M.insert a' a m) t t'
eqRSort m (RFun _ t1 t2 _) (RFun _ t1' t2' _)
= eqRSort m t1 t1' && eqRSort m t2 t2'
eqRSort m (RAppTy t1 t2 _) (RAppTy t1' t2' _)
= eqRSort m t1 t1' && eqRSort m t2 t2'
eqRSort m (RApp c ts _ _) (RApp c' ts' _ _)
= c == c' && length ts == length ts' && and (zipWith (eqRSort m) ts ts')
eqRSort m (RCls c ts) (RCls c' ts')
= c == c' && length ts == length ts' && and (zipWith (eqRSort m) ts ts')
eqRSort m (RVar a _) (RVar a' _)
= a == M.lookupDefault a' a' m
eqRSort _ (RHole _) _
= True
eqRSort _ _ (RHole _)
= True
eqRSort _ _ _
= False
--------------------------------------------------------------------
-- | Wrappers for GHC Type Elements --------------------------------
--------------------------------------------------------------------
instance Eq Predicate where
(==) = eqpd
eqpd (Pr vs) (Pr ws)
= and $ (length vs' == length ws') : [v == w | (v, w) <- zip vs' ws']
where vs' = sort vs
ws' = sort ws
instance Eq RTyVar where
RTV α == RTV α' = tvId α == tvId α'
instance Ord RTyVar where
compare (RTV α) (RTV α') = compare (tvId α) (tvId α')
instance Hashable RTyVar where
hashWithSalt i (RTV α) = hashWithSalt i α
instance Ord RTyCon where
compare x y = compare (rtc_tc x) (rtc_tc y)
instance Eq RTyCon where
x == y = rtc_tc x == rtc_tc y
instance Hashable RTyCon where
hashWithSalt i = hashWithSalt i . rtc_tc
--------------------------------------------------------------------
---------------------- Helper Functions ----------------------------
--------------------------------------------------------------------
rVar = (`RVar` mempty) . RTV
rTyVar = RTV
normalizePds t = addPds ps t'
where (t', ps) = nlzP [] t
rPred = RAllP
rEx xts t = foldr (\(x, tx) t -> REx x tx t) t xts
rApp c = RApp (RTyCon c [] (mkTyConInfo c [] [] Nothing))
addPds ps (RAllT v t) = RAllT v $ addPds ps t
addPds ps t = foldl' (flip rPred) t ps
nlzP ps t@(RVar _ _ )
= (t, ps)
nlzP ps (RFun b t1 t2 r)
= (RFun b t1' t2' r, ps ++ ps1 ++ ps2)
where (t1', ps1) = nlzP [] t1
(t2', ps2) = nlzP [] t2
nlzP ps (RAppTy t1 t2 r)
= (RAppTy t1' t2' r, ps ++ ps1 ++ ps2)
where (t1', ps1) = nlzP [] t1
(t2', ps2) = nlzP [] t2
nlzP ps (RAllT v t )
= (RAllT v t', ps ++ ps')
where (t', ps') = nlzP [] t
nlzP ps t@(RApp _ _ _ _)
= (t, ps)
nlzP ps (RAllS _ t)
= (t, ps)
nlzP ps t@(RCls _ _)
= (t, ps)
nlzP ps (RAllP p t)
= (t', [p] ++ ps ++ ps')
where (t', ps') = nlzP [] t
nlzP ps t@(ROth _)
= (t, ps)
nlzP ps t@(REx _ _ _)
= (t, ps)
nlzP ps t@(RRTy _ _ _ t')
= (t, ps ++ ps')
where ps' = snd $ nlzP [] t'
nlzP ps t@(RAllE _ _ _)
= (t, ps)
nlzP _ t
= errorstar $ "RefType.nlzP: cannot handle " ++ show t
-- NEWISH: with unifying type variables: causes big problems with TUPLES?
--strengthenRefType t1 t2 = maybe (errorstar msg) (strengthenRefType_ t1) (unifyShape t1 t2)
-- where msg = printf "strengthen on differently shaped reftypes \nt1 = %s [shape = %s]\nt2 = %s [shape = %s]"
-- (render t1) (render (toRSort t1)) (render t2) (render (toRSort t2))
-- OLD: without unifying type variables, but checking α-equivalence
strengthenRefType t1 t2
| eqt t1 t2
= strengthenRefType_ t1 t2
| otherwise
= errorstar msg
where
eqt t1 t2 = {- render -} toRSort t1 == {- render -} toRSort t2
msg = printf "strengthen on differently shaped reftypes \nt1 = %s [shape = %s]\nt2 = %s [shape = %s]"
(showpp t1) (showpp (toRSort t1)) (showpp t2) (showpp (toRSort t2))
unifyShape :: ( RefTypable p c tv r
, FreeVar c tv
, RefTypable p c tv ()
, SubsTy tv (RType p c tv ()) (RType p c tv ())
, SubsTy tv (RType p c tv ()) c)
=> RType p c tv r -> RType p c tv r -> Maybe (RType p c tv r)
unifyShape (RAllT a1 t1) (RAllT a2 t2)
| a1 == a2 = RAllT a1 <$> unifyShape t1 t2
| otherwise = RAllT a1 <$> unifyShape t1 (sub a2 a1 t2)
where sub a b = let bt = RVar b mempty in subsTyVar_meet (a, toRSort bt, bt)
unifyShape t1 t2
| eqt t1 t2 = Just t1
| otherwise = Nothing
where eqt t1 t2 = showpp (toRSort t1) == showpp (toRSort t2)
-- strengthenRefType_ :: RefTypable p c tv r =>RType p c tv r -> RType p c tv r -> RType p c tv r
strengthenRefType_ (RAllT a1 t1) (RAllT _ t2)
= RAllT a1 $ strengthenRefType_ t1 t2
strengthenRefType_ (RAllP p1 t1) (RAllP _ t2)
= RAllP p1 $ strengthenRefType_ t1 t2
strengthenRefType_ (RAllS s t1) t2
= RAllS s $ strengthenRefType_ t1 t2
strengthenRefType_ t1 (RAllS s t2)
= RAllS s $ strengthenRefType_ t1 t2
strengthenRefType_ (RAppTy t1 t1' r1) (RAppTy t2 t2' r2)
= RAppTy t t' (r1 `meet` r2)
where t = strengthenRefType_ t1 t2
t' = strengthenRefType_ t1' t2'
strengthenRefType_ (RFun x1 t1 t1' r1) (RFun x2 t2 t2' r2)
= RFun x1 t t' (r1 `meet` r2)
where t = strengthenRefType_ t1 t2
t' = strengthenRefType_ t1' $ subst1 t2' (x2, EVar x1)
strengthenRefType_ (RApp tid t1s rs1 r1) (RApp _ t2s rs2 r2)
= RApp tid ts rs (r1 `meet` r2)
where ts = zipWith strengthenRefType_ t1s t2s
rs = {- tracePpr msg $ -} meets rs1 rs2
msg = "strengthenRefType_: RApp rs1 = " ++ showpp rs1 ++ " rs2 = " ++ showpp rs2
strengthenRefType_ (RVar v1 r1) (RVar _ r2)
= RVar v1 ({- tracePpr msg $ -} r1 `meet` r2)
where msg = "strengthenRefType_: RVAR r1 = " ++ showpp r1 ++ " r2 = " ++ showpp r2
strengthenRefType_ t1 _
= t1
meets [] rs = rs
meets rs [] = rs
meets rs rs'
| length rs == length rs' = zipWith meet rs rs'
| otherwise = errorstar "meets: unbalanced rs"
strengthen :: Reftable r => RType p c tv r -> r -> RType p c tv r
strengthen (RApp c ts rs r) r' = RApp c ts rs (r `meet` r')
strengthen (RVar a r) r' = RVar a (r `meet` r')
strengthen (RFun b t1 t2 r) r' = RFun b t1 t2 (r `meet` r')
strengthen (RAppTy t1 t2 r) r' = RAppTy t1 t2 (r `meet` r')
strengthen t _ = t
-------------------------------------------------------------------------
addTyConInfo :: (PPrint r, Reftable r)
=> (M.HashMap TyCon FTycon)
-> (M.HashMap TyCon RTyCon)
-> RRType r
-> RRType r
-------------------------------------------------------------------------
addTyConInfo tce tyi = mapBot (expandRApp tce tyi)
-------------------------------------------------------------------------
expandRApp :: (PPrint r, Reftable r)
=> (M.HashMap TyCon FTycon)
-> (M.HashMap TyCon RTyCon)
-> RRType r
-> RRType r
-------------------------------------------------------------------------
expandRApp tce tyi t@(RApp {}) = RApp rc' ts rs' r
where
RApp rc ts rs r = t
rc' = appRTyCon tce tyi rc ts
pvs = rTyConPVs rc'
rs' = applyNonNull rs0 (rtPropPV rc pvs) rs
rs0 = rtPropTop <$> pvs
expandRApp _ _ t = t
rtPropTop pv = case ptype pv of
PVProp t -> RProp xts $ ofRSort t
PVHProp -> RProp xts $ mempty
where
xts = pvArgs pv
rtPropPV rc = safeZipWith msg mkRTProp
where
msg = "appRefts: " ++ showFix rc
mkRTProp pv (RPropP ss r)
= RProp ss $ (ofRSort $ pvType pv) `strengthen` r
mkRTProp pv (RProp ss t)
| length (pargs pv) == length ss
= RProp ss t
| otherwise
= RProp (pvArgs pv) t
mkRTProp pv (RHProp ss w)
| length (pargs pv) == length ss
= RHProp ss w
| otherwise
= RHProp (pvArgs pv) w
pvArgs pv = [(s, t) | (t, s, _) <- pargs pv]
appRTyCon tce tyi rc ts = RTyCon c ps' (rtc_info rc'')
where
c = rtc_tc rc
ps' = subts (zip (RTV <$> αs) ts') <$> rTyConPVs rc'
ts' = if null ts then rVar <$> βs else toRSort <$> ts
rc' = M.lookupDefault rc c tyi
αs = TC.tyConTyVars $ rtc_tc rc'
βs = TC.tyConTyVars c
rc'' = if isNumeric tce rc' then addNumSizeFun rc' else rc'
isNumeric tce c
= fromMaybe (symbolFTycon . dummyLoc $ tyConName (rtc_tc c))
(M.lookup (rtc_tc c) tce) == intFTyCon
addNumSizeFun c
= c {rtc_info = (rtc_info c) {sizeFunction = Just EVar} }
generalize :: (RefTypable c p tv r) => RType c p tv r -> RType c p tv r
generalize t = mkUnivs (freeTyVars t) [] [] t
freeTyVars (RAllP _ t) = freeTyVars t
freeTyVars (RAllS _ t) = freeTyVars t
freeTyVars (RAllT α t) = freeTyVars t L.\\ [α]
freeTyVars (RFun _ t t' _) = freeTyVars t `L.union` freeTyVars t'
freeTyVars (RApp _ ts _ _) = L.nub $ concatMap freeTyVars ts
freeTyVars (RCls _ ts) = []
freeTyVars (RVar α _) = [α]
freeTyVars (RAllE _ _ t) = freeTyVars t
freeTyVars (REx _ _ t) = freeTyVars t
freeTyVars (RExprArg _) = []
freeTyVars (RAppTy t t' _) = freeTyVars t `L.union` freeTyVars t'
freeTyVars (RHole r) = []
freeTyVars t = errorstar ("RefType.freeTyVars cannot handle" ++ show t)
tyClasses (RAllP _ t) = tyClasses t
tyClasses (RAllS _ t) = tyClasses t
tyClasses (RAllT α t) = tyClasses t
tyClasses (RAllE _ _ t) = tyClasses t
tyClasses (REx _ _ t) = tyClasses t
tyClasses (RFun _ t t' _) = tyClasses t ++ tyClasses t'
tyClasses (RAppTy t t' _) = tyClasses t ++ tyClasses t'
tyClasses (RApp _ ts _ _) = concatMap tyClasses ts
tyClasses (RCls c ts) = (c, ts) : concatMap tyClasses ts
tyClasses (RVar α _) = []
tyClasses (RRTy _ _ _ t) = tyClasses t
tyClasses (RHole r) = []
tyClasses t = errorstar ("RefType.tyClasses cannot handle" ++ show t)
--getTyClasses = everything (++) ([] `mkQ` f)
-- where f ((RCls c ts) :: SpecType) = [(c, ts)]
-- f _ = []
----------------------------------------------------------------
---------------------- Strictness ------------------------------
----------------------------------------------------------------
instance (NFData a, NFData b, NFData t) => NFData (Ref t a b) where
rnf (RPropP s a) = rnf s `seq` rnf a
rnf (RProp s b) = rnf s `seq` rnf b
instance (NFData a, NFData b, NFData c, NFData e) => NFData (RType a b c e) where
rnf (RVar α r) = rnf α `seq` rnf r
rnf (RAllT α t) = rnf α `seq` rnf t
rnf (RAllP π t) = rnf π `seq` rnf t
rnf (RAllS s t) = rnf s `seq` rnf t
rnf (RFun x t t' r) = rnf x `seq` rnf t `seq` rnf t' `seq` rnf r
rnf (RApp _ ts rs r) = rnf ts `seq` rnf rs `seq` rnf r
rnf (RCls c ts) = c `seq` rnf ts
rnf (RAllE x t t') = rnf x `seq` rnf t `seq` rnf t'
rnf (REx x t t') = rnf x `seq` rnf t `seq` rnf t'
rnf (ROth s) = rnf s
rnf (RExprArg e) = rnf e
rnf (RAppTy t t' r) = rnf t `seq` rnf t' `seq` rnf r
rnf (RRTy _ r o t) = rnf r `seq` rnf t
rnf (RHole r) = rnf r
----------------------------------------------------------------
------------------ Printing Refinement Types -------------------
----------------------------------------------------------------
instance Show RTyVar where
show = showpp
instance PPrint (UReft r) => Show (UReft r) where
show = showpp
-- instance (Fixpoint a, Fixpoint b, Fixpoint c) => Fixpoint (a, b, c) where
-- toFix (a, b, c) = hsep ([toFix a ,toFix b, toFix c])
instance (RefTypable p c tv r) => PPrint (RType p c tv r) where
pprint = ppRType TopPrec
instance PPrint (RType p c tv r) => Show (RType p c tv r) where
show = showpp
instance PPrint (RTProp p c tv r) => Show (RTProp p c tv r) where
show = showpp
instance Fixpoint RTyCon where
toFix (RTyCon c _ _) = text $ showPpr c -- <+> text "\n<<" <+> hsep (map toFix ts) <+> text ">>\n"
instance PPrint RTyCon where
pprint = toFix
instance Show RTyCon where
show = showpp
instance PPrint REnv where
pprint (REnv m) = pprint m
------------------------------------------------------------------------------------------
-- TODO: Rewrite subsTyvars with Traversable
------------------------------------------------------------------------------------------
subsTyVars_meet = subsTyVars True
subsTyVars_nomeet = subsTyVars False
subsTyVar_nomeet = subsTyVar False
subsTyVar_meet = subsTyVar True
subsTyVars meet ats t = foldl' (flip (subsTyVar meet)) t ats
subsTyVar meet = subsFree meet S.empty
--subsFree :: ( Ord tv
-- , SubsTy tv ty c
-- , SubsTy tv ty r
-- , SubsTy tv ty (PVar (RType p c tv ()))
-- , RefTypable p c tv r)
-- => Bool
-- -> S.Set tv
-- -> (tv, ty, RType p c tv r)
-- -> RType p c tv r
-- -> RType p c tv r
subsFree m s z@(α, τ,_) (RAllS l t)
= RAllS l (subsFree m s z t)
subsFree m s z@(α, τ,_) (RAllP π t)
= RAllP (subt (α, τ) π) (subsFree m s z t)
subsFree m s z (RAllT α t)
= RAllT α $ subsFree m (α `S.insert` s) z t
subsFree m s z@(_, _, _) (RFun x t t' r)
= RFun x (subsFree m s z t) (subsFree m s z t') r
subsFree m s z@(α, τ, _) (RApp c ts rs r)
= RApp (subt z' c) (subsFree m s z <$> ts) (subsFreeRef m s z <$> rs) r
where z' = (α, τ) -- UNIFY: why instantiating INSIDE parameters?
subsFree m s z (RCls c ts)
= RCls c (subsFree m s z <$> ts)
subsFree meet s (α', _, t') t@(RVar α r)
| α == α' && not (α `S.member` s)
= if meet then t' `strengthen` r else t'
| otherwise
= t
subsFree m s z (RAllE x t t')
= RAllE x (subsFree m s z t) (subsFree m s z t')
subsFree m s z (REx x t t')
= REx x (subsFree m s z t) (subsFree m s z t')
subsFree m s z@(_, _, _) (RAppTy t t' r)
= subsFreeRAppTy m s (subsFree m s z t) (subsFree m s z t') r
subsFree _ _ _ t@(RExprArg _)
= t
subsFree m s z (RRTy e r o t)
= RRTy (mapSnd (subsFree m s z) <$> e) r o (subsFree m s z t)
subsFree _ _ _ t@(ROth _)
= t
subsFree _ _ _ t@(RHole r)
= t
-- subsFree _ _ _ t
-- = errorstar $ "subsFree fails on: " ++ showFix t
subsFrees m s zs t = foldl' (flip(subsFree m s)) t zs
-- GHC INVARIANT: RApp is Type Application to something other than TYCon
subsFreeRAppTy m s (RApp c ts rs r) t' r'
= mkRApp m s c (ts ++ [t']) rs r r'
subsFreeRAppTy m s t t' r'
= RAppTy t t' r'
mkRApp m s c ts rs r r'
| isFun c, [t1, t2] <- ts
= RFun dummySymbol t1 t2 $ refAppTyToFun r'
| otherwise
= subsFrees m s zs $ RApp c ts rs $ r `meet` r' -- (refAppTyToApp r')
where
zs = [(tv, toRSort t, t) | (tv, t) <- zip (freeVars c) ts]
refAppTyToFun r
| isTauto r = r
| otherwise = errorstar "RefType.refAppTyToFun"
subsFreeRef m s (α', τ', t') (RProp ss t)
= RProp (mapSnd (subt (α', τ')) <$> ss) $ subsFree m s (α', τ', fmap top t') t
subsFreeRef _ _ (α', τ', _) (RPropP ss r)
= RPropP (mapSnd (subt (α', τ')) <$> ss) $ {- subt (α', τ') -} r
-------------------------------------------------------------------
------------------- Type Substitutions ----------------------------
-------------------------------------------------------------------
subts = flip (foldr subt)
instance SubsTy tv ty () where
subt _ = id
instance SubsTy tv ty Reft where
subt _ = id
instance (SubsTy tv ty ty) => SubsTy tv ty (PVKind ty) where
subt su (PVProp t) = PVProp (subt su t)
subt su PVHProp = PVHProp
instance (SubsTy tv ty ty) => SubsTy tv ty (PVar ty) where
subt su (PV n t v xts) = PV n (subt su t) v [(subt su t, x, y) | (t,x,y) <- xts]
instance SubsTy RTyVar RSort RTyCon where
subt z c = RTyCon tc ps' i
where
tc = rtc_tc c
ps' = subt z <$> rTyConPVs c
i = rtc_info c
-- NOTE: This DOES NOT substitute at the binders
instance SubsTy RTyVar RSort PrType where
subt (α, τ) = subsTyVar_meet (α, τ, ofRSort τ)
instance SubsTy RTyVar RSort SpecType where
subt (α, τ) = subsTyVar_meet (α, τ, ofRSort τ)
instance SubsTy RTyVar RTyVar SpecType where
subt (α, a) = subt (α, RVar a () :: RSort)
instance SubsTy RTyVar RSort RSort where
subt (α, τ) = subsTyVar_meet (α, τ, ofRSort τ)
-- Here the "String" is a Bare-TyCon. TODO: wrap in newtype
instance SubsTy Symbol BSort LocSymbol where
subt _ t = t
instance SubsTy Symbol BSort BSort where
subt (α, τ) = subsTyVar_meet (α, τ, ofRSort τ)
instance (SubsTy tv ty (UReft r), SubsTy tv ty (RType p c tv ())) => SubsTy tv ty (RTProp p c tv (UReft r)) where
subt m (RPropP ss p) = RPropP ((mapSnd (subt m)) <$> ss) $ subt m p
subt m (RProp ss t) = RProp ((mapSnd (subt m)) <$> ss) $ fmap (subt m) t
subvUReft :: (UsedPVar -> UsedPVar) -> UReft Reft -> UReft Reft
subvUReft f (U r p s) = U r (subvPredicate f p) s
subvPredicate :: (UsedPVar -> UsedPVar) -> Predicate -> Predicate
subvPredicate f (Pr pvs) = Pr (f <$> pvs)
---------------------------------------------------------------
-- ofType, ofType_ :: Reftable r => Type -> RRType r
ofType = ofType_ . expandTypeSynonyms
ofType_ (TyVarTy α)
= rVar α
ofType_ (FunTy τ τ')
= rFun dummySymbol (ofType_ τ) (ofType_ τ')
ofType_ (ForAllTy α τ)
= RAllT (rTyVar α) $ ofType_ τ
ofType_ τ
| Just t <- ofPredTree (classifyPredType τ)
= t
ofType_ (TyConApp c τs)
| Just (αs, τ) <- TC.synTyConDefn_maybe c
= ofType_ $ substTyWith αs τs τ
| otherwise
= rApp c (ofType_ <$> τs) [] mempty
ofType_ (AppTy t1 t2)
= RAppTy (ofType_ t1) (ofType t2) mempty
-- ofType_ τ
-- = errorstar ("ofType cannot handle: " ++ showPpr τ)
ofPredTree (ClassPred c τs)
= Just $ RCls c (ofType_ <$> τs)
ofPredTree _
= Nothing
----------------------------------------------------------------
------------------- Converting to Fixpoint ---------------------
----------------------------------------------------------------
instance Expression Var where
expr = eVar
pprShort = symbolString . dropModuleNames . symbol
dataConSymbol :: DataCon -> Symbol
dataConSymbol = symbol . dataConWorkId
-- TODO: turn this into a map lookup?
dataConReft :: DataCon -> [Symbol] -> Reft
dataConReft c []
| c == trueDataCon
= Reft (vv_, [RConc $ eProp vv_])
| c == falseDataCon
= Reft (vv_, [RConc $ PNot $ eProp vv_])
dataConReft c [x]
| c == intDataCon
= Reft (vv_, [RConc (PAtom Eq (EVar vv_) (EVar x))])
dataConReft c _
| not $ isBaseDataCon c
= mempty
dataConReft c xs
= Reft (vv_, [RConc (PAtom Eq (EVar vv_) dcValue)])
where dcValue | null xs && null (dataConUnivTyVars c)
= EVar $ dataConSymbol c
| otherwise
= EApp (dummyLoc $ dataConSymbol c) (EVar <$> xs)
isBaseDataCon c = and $ isBaseTy <$> dataConOrigArgTys c ++ dataConRepArgTys c
isBaseTy (TyVarTy _) = True
isBaseTy (AppTy t1 t2) = False
isBaseTy (TyConApp _ ts) = and $ isBaseTy <$> ts
isBaseTy (FunTy _ _) = False
isBaseTy (ForAllTy _ _) = False
vv_ = vv Nothing
dataConMsReft ty ys = subst su (rTypeReft (ignoreOblig $ ty_res trep))
where trep = toRTypeRep ty
xs = ty_binds trep
ts = ty_args trep
su = mkSubst $ [(x, EVar y) | ((x, _), y) <- zip (zip xs ts) ys]
---------------------------------------------------------------
---------------------- Embedding RefTypes ---------------------
---------------------------------------------------------------
-- TODO: remove toType, generalize typeSort
toType :: (Reftable r, PPrint r) => RRType r -> Type
toType (RFun _ t t' _)
= FunTy (toType t) (toType t')
toType (RAllT (RTV α) t)
= ForAllTy α (toType t)
toType (RAllP _ t)
= toType t
toType (RAllS _ t)
= toType t
toType (RVar (RTV α) _)
= TyVarTy α
toType (RApp (RTyCon {rtc_tc = c}) ts _ _)
= TyConApp c (toType <$> ts)
toType (RCls c ts)
= mkClassPred c (toType <$> ts)
toType (RAllE _ _ t)
= toType t
toType (REx _ _ t)
= toType t
toType (RAppTy t t' _)
= AppTy (toType t) (toType t')
toType t@(RExprArg _)
= errorstar $ "RefType.toType cannot handle 1: " ++ show t
toType t@(ROth _)
= errorstar $ "RefType.toType cannot handle 2: " ++ show t
toType (RRTy _ _ _ t)
= toType t
toType t
= errorstar $ "RefType.toType cannot handle: " ++ show t
---------------------------------------------------------------
----------------------- Typing Literals -----------------------
---------------------------------------------------------------
-- makeRTypeBase :: Type -> Reft -> RefType
makeRTypeBase (TyVarTy α) x
= RVar (rTyVar α) x
makeRTypeBase (TyConApp c _) x
= rApp c [] [] x
makeRTypeBase _ _
= error "RefType : makeRTypeBase"
literalFRefType tce l
= makeRTypeBase (literalType l) (literalFReft tce l)
literalFReft tce = maybe mempty exprReft . snd . literalConst tce
-- exprReft . snd . literalConst tce
-- | `literalConst` returns `Nothing` for unhandled lits because
-- otherwise string-literals show up as global int-constants
-- which blow up qualifier instantiation.
literalConst tce l = (sort, mkLit l)
where
sort = typeSort tce $ literalType l
mkLit (MachInt n) = mkI n
mkLit (MachInt64 n) = mkI n
mkLit (MachWord n) = mkI n
mkLit (MachWord64 n) = mkI n
mkLit (MachFloat n) = mkR n
mkLit (MachDouble n) = mkR n
mkLit (LitInteger n _) = mkI n
mkLit _ = Nothing -- ELit sym sort
mkI = Just . ECon . I
mkR = Just . ECon . R . fromRational
---------------------------------------------------------------
---------------- Annotations and Solutions --------------------
---------------------------------------------------------------
rTypeSortedReft :: (PPrint r, Reftable r) => TCEmb TyCon -> RRType r -> SortedReft
rTypeSortedReft emb t = RR (rTypeSort emb t) (rTypeReft t)
rTypeSort :: (PPrint r, Reftable r) => TCEmb TyCon -> RRType r -> Sort
rTypeSort tce = typeSort tce . toType
-------------------------------------------------------------------------------
applySolution :: (Functor f) => FixSolution -> f SpecType -> f SpecType
-------------------------------------------------------------------------------
applySolution = fmap . fmap . mapReft . map . appSolRefa
where
appSolRefa _ ra@(RConc _) = ra
-- appSolRefa _ p@(RPvar _) = p
appSolRefa s (RKvar k su) = RConc $ subst su $ M.lookupDefault PTop k s
mapReft f (U (Reft (x, zs)) p s) = U (Reft (x, squishRefas $ f zs)) p s
-------------------------------------------------------------------------------
shiftVV :: SpecType -> Symbol -> SpecType
-------------------------------------------------------------------------------
shiftVV t@(RApp _ ts _ r) vv'
= t { rt_args = subst1 ts (rTypeValueVar t, EVar vv') }
{ rt_reft = (`F.shiftVV` vv') <$> r }
shiftVV t@(RFun _ _ _ r) vv'
= t { rt_reft = (`F.shiftVV` vv') <$> r }
shiftVV t@(RAppTy _ _ r) vv'
= t { rt_reft = (`F.shiftVV` vv') <$> r }
shiftVV t@(RVar _ r) vv'
= t { rt_reft = (`F.shiftVV` vv') <$> r }
shiftVV t _
= t -- errorstar $ "shiftVV: cannot handle " ++ showpp t
------------------------------------------------------------------------
---------------- Auxiliary Stuff Used Elsewhere ------------------------
------------------------------------------------------------------------
-- MOVE TO TYPES
instance (Show tv, Show ty) => Show (RTAlias tv ty) where
show (RTA n as xs t p) = printf "type %s %s %s = %s -- defined at %s" (symbolString n)
(L.intercalate " " (show <$> as))
(L.intercalate " " (show <$> xs))
(show t) (show p)
----------------------------------------------------------------
------------ From Old Fixpoint ---------------------------------
----------------------------------------------------------------
typeUniqueSymbol :: Type -> Symbol
typeUniqueSymbol = symbol . typeUniqueString
typeSort :: TCEmb TyCon -> Type -> Sort
typeSort tce τ@(ForAllTy _ _)
= typeSortForAll tce τ
typeSort tce t@(FunTy τ1 τ2)
= typeSortFun tce t
typeSort tce (TyConApp c τs)
= fApp (Left $ tyConFTyCon tce c) (typeSort tce <$> τs)
typeSort tce (AppTy t1 t2)
= fApp (Right $ typeSort tce t1) [typeSort tce t2]
typeSort _ τ
= FObj $ typeUniqueSymbol τ
tyConFTyCon tce c = fromMaybe (symbolFTycon $ dummyLoc $ tyConName c) (M.lookup c tce)
typeSortForAll tce τ
= genSort $ typeSort tce tbody
where genSort (FFunc _ t) = FFunc n (sortSubst su <$> t)
genSort t = FFunc n [sortSubst su t]
(as, tbody) = splitForAllTys τ
su = M.fromList $ zip sas (FVar <$> [0..])
sas = (typeUniqueSymbol . TyVarTy) <$> as
n = length as
-- sortSubst su t@(FObj x) = fromMaybe t (M.lookup x su)
-- sortSubst su (FFunc n ts) = FFunc n (sortSubst su <$> ts)
-- sortSubst su (FApp c ts) = FApp c (sortSubst su <$> ts)
-- sortSubst _ t = t
tyConName c
| listTyCon == c = listConName
| TC.isTupleTyCon c = tupConName
| otherwise = symbol c
typeSortFun tce t -- τ1 τ2
= FFunc 0 sos
where sos = typeSort tce <$> τs
τs = grabArgs [] t
grabArgs τs (FunTy τ1 τ2 )
| not $ isClassPred τ1 = grabArgs (τ1:τs) τ2
| otherwise = grabArgs τs τ2
grabArgs τs τ = reverse (τ:τs)
mkDataConIdsTy (dc, t) = [expandProductType id t | id <- dataConImplicitIds dc]
expandProductType x t
| ofType (varType x) == toRSort t = (x, t)
| otherwise = (x, t')
where t' = fromRTypeRep $ trep {ty_binds = xs', ty_args = ts'}
τs = fst $ splitFunTys $ toType t
trep = toRTypeRep t
(xs', ts') = unzip $ concatMap mkProductTy $ zip3 τs (ty_binds trep) (ty_args trep)
mkProductTy (τ, x, t) = maybe [(x, t)] f $ deepSplitProductType_maybe menv τ
where f = ((<$>) ((,) dummySymbol . ofType)) . third4
menv = (emptyFamInstEnv, emptyFamInstEnv)
-- Move to misc
forth4 (_, _, _, x) = x
-----------------------------------------------------------------------------------------
-- | Binders generated by class predicates, typically for constraining tyvars (e.g. FNum)
-----------------------------------------------------------------------------------------
classBinds (RCls c ts)
| isNumericClass c = [(rTyVarSymbol a, trueSortedReft FNum) | (RVar a _) <- ts]
classBinds _ = []
rTyVarSymbol (RTV α) = typeUniqueSymbol $ TyVarTy α
-----------------------------------------------------------------------------------------
--------------------------- Termination Predicates --------------------------------------
-----------------------------------------------------------------------------------------
isDecreasing (RApp c _ _ _)
= isJust (sizeFunction (rtc_info c))
isDecreasing _
= False
makeDecrType = mkDType [] []
mkDType xvs acc [(v, (x, t@(RApp c _ _ _)))]
= (x, ) $ t `strengthen` tr
where tr = uTop $ Reft (vv, [RConc $ pOr (r:acc)])
r = cmpLexRef xvs (v', vv, f)
v' = symbol v
Just f = sizeFunction $ rtc_info c
vv = "vvRec"
mkDType xvs acc ((v, (x, t@(RApp c _ _ _))):vxts)
= mkDType ((v', x, f):xvs) (r:acc) vxts
where r = cmpLexRef xvs (v', x, f)
v' = symbol v
Just f = sizeFunction $ rtc_info c
cmpLexRef vxs (v, x, g)
= pAnd $ (PAtom Lt (g x) (g v)) : (PAtom Ge (g x) zero)
: [PAtom Eq (f y) (f z) | (y, z, f) <- vxs]
++ [PAtom Ge (f y) zero | (y, _, f) <- vxs]
where zero = ECon $ I 0
makeLexRefa es' es = uTop $ Reft (vv, [RConc $ PIff (PBexp $ EVar vv) $ pOr rs])
where rs = makeLexReft [] [] es es'
vv = "vvRec"
makeLexReft old acc [] []
= acc
makeLexReft old acc (e:es) (e':es')
= makeLexReft ((e,e'):old) (r:acc) es es'
where
r = pAnd $ (PAtom Lt e' e)
: (PAtom Ge e' zero)
: [PAtom Eq o' o | (o,o') <- old]
++ [PAtom Ge o' zero | (o,o') <- old]
zero = ECon $ I 0
-------------------------------------------------------------------------------
mkTyConInfo :: TyCon -> [Int] -> [Int] -> (Maybe (Symbol -> Expr)) -> TyConInfo
mkTyConInfo c = TyConInfo pos neg
where pos = neutral ++ [i | (i, b) <- varsigns, b, i /= dindex]
neg = neutral ++ [i | (i, b) <- varsigns, not b, i /= dindex]
varsigns = L.nub $ concatMap goDCon $ TC.tyConDataCons c
initmap = zip (showPpr <$> tyvars) [0..n]
mkmap vs = zip (showPpr <$> vs) (repeat dindex) ++ initmap
goDCon dc = concatMap (go (mkmap (DataCon.dataConExTyVars dc)) True)
(DataCon.dataConOrigArgTys dc)
go m pos (ForAllTy v t) = go ((showPpr v, dindex):m) pos t
go m pos (TyVarTy v) = [(varLookup (showPpr v) m, pos)]
go m pos (AppTy t1 t2) = go m pos t1 ++ go m pos t2
go m pos (TyConApp _ ts) = concatMap (go m pos) ts
go m pos (FunTy t1 t2) = go m (not pos) t1 ++ go m pos t2
varLookup v m = fromMaybe (errmsg v) $ L.lookup v m
tyvars = TC.tyConTyVars c
n = (TC.tyConArity c) - 1
errmsg v = error $ "GhcMisc.getTyConInfo: var not found" ++ showPpr v
dindex = -1
neutral = [0..n] L.\\ (fst <$> varsigns)