liquidhaskell-0.8.10.7: src/Language/Haskell/Liquid/Constraint/Generate.hs
{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE ImplicitParams #-}
-- | This module defines the representation of Subtyping and WF Constraints,
-- and the code for syntax-directed constraint generation.
module Language.Haskell.Liquid.Constraint.Generate ( generateConstraints, generateConstraintsWithEnv, caseEnv, consE ) where
#if !MIN_VERSION_base(4,14,0)
import Control.Monad.Fail
#endif
import Prelude hiding (error)
import GHC.Stack
import Language.Haskell.Liquid.GHC.API as Ghc hiding ( panic
, checkErr
, (<+>)
, text
, vcat
)
import Language.Haskell.Liquid.GHC.TypeRep ()
import Text.PrettyPrint.HughesPJ hiding ((<>))
import Control.Monad.State
import Data.Maybe (fromMaybe, catMaybes, isJust)
import qualified Data.HashMap.Strict as M
import qualified Data.HashSet as S
import qualified Data.List as L
import qualified Data.Foldable as F
import qualified Data.Traversable as T
import qualified Data.Functor.Identity
import Language.Fixpoint.Misc
import Language.Fixpoint.Types.Visitor
import qualified Language.Fixpoint.Types as F
import qualified Language.Fixpoint.Types.Visitor as F
import Language.Haskell.Liquid.Constraint.Fresh
import Language.Haskell.Liquid.Constraint.Init
import Language.Haskell.Liquid.Constraint.Env
import Language.Haskell.Liquid.Constraint.Monad
import Language.Haskell.Liquid.Constraint.Split
import Language.Haskell.Liquid.Types.Dictionaries
import Language.Haskell.Liquid.GHC.Play (isHoleVar)
import qualified Language.Haskell.Liquid.GHC.Resugar as Rs
import qualified Language.Haskell.Liquid.GHC.SpanStack as Sp
import qualified Language.Haskell.Liquid.GHC.Misc as GM -- ( isInternal, collectArguments, tickSrcSpan, showPpr )
import Language.Haskell.Liquid.Misc
import Language.Haskell.Liquid.Constraint.Types
import Language.Haskell.Liquid.Constraint.Constraint
import Language.Haskell.Liquid.Transforms.Rec
import Language.Haskell.Liquid.Transforms.CoreToLogic (weakenResult)
import Language.Haskell.Liquid.Bare.DataType (makeDataConChecker)
import Language.Haskell.Liquid.Types hiding (binds, Loc, loc, Def)
--------------------------------------------------------------------------------
-- | Constraint Generation: Toplevel -------------------------------------------
--------------------------------------------------------------------------------
generateConstraints :: TargetInfo -> CGInfo
--------------------------------------------------------------------------------
generateConstraints info = {-# SCC "ConsGen" #-} execState act $ initCGI cfg info
where
act = do { γ <- initEnv info; consAct γ cfg info }
cfg = getConfig info
generateConstraintsWithEnv :: TargetInfo -> CGInfo -> CGEnv -> CGInfo
--------------------------------------------------------------------------------
generateConstraintsWithEnv info cgi γ = {-# SCC "ConsGenEnv" #-} execState act cgi
where
act = consAct γ cfg info
cfg = getConfig info
consAct :: CGEnv -> Config -> TargetInfo -> CG ()
consAct γ cfg info = do
let sSpc = gsSig . giSpec $ info
let gSrc = giSrc info
when (gradual cfg) (mapM_ (addW . WfC γ . val . snd) (gsTySigs sSpc ++ gsAsmSigs sSpc))
foldM_ (consCBTop cfg info) γ (giCbs gSrc)
mapM_ (consClass γ) (gsMethods $ gsSig $ giSpec info)
hcs <- gets hsCs
hws <- gets hsWfs
fcs <- concat <$> mapM (splitC (typeclass (getConfig info))) hcs
fws <- concat <$> mapM splitW hws
modify $ \st -> st { fEnv = feEnv (fenv γ)
, cgLits = litEnv γ
, cgConsts = cgConsts st `mappend` constEnv γ
, fixCs = fcs
, fixWfs = fws }
--------------------------------------------------------------------------------
-- | Ensure that the instance type is a subtype of the class type --------------
--------------------------------------------------------------------------------
consClass :: CGEnv -> (Var, MethodType LocSpecType) -> CG ()
consClass γ (x,mt)
| Just ti <- tyInstance mt
, Just tc <- tyClass mt
= addC (SubC (γ `setLocation` Sp.Span (GM.fSrcSpan (F.loc ti))) (val ti) (val tc)) ("cconsClass for " ++ GM.showPpr x)
consClass _ _
= return ()
--------------------------------------------------------------------------------
-- | TERMINATION TYPE ----------------------------------------------------------
--------------------------------------------------------------------------------
makeDecrIndex :: (Var, Template SpecType, [Var]) -> CG [Int]
makeDecrIndex (x, Assumed t, args)
= do dindex <- makeDecrIndexTy x t args
case dindex of
Left _ -> return []
Right i -> return i
makeDecrIndex (x, Asserted t, args)
= do dindex <- makeDecrIndexTy x t args
case dindex of
Left msg -> addWarning msg >> return []
Right i -> return i
makeDecrIndex _ = return []
makeDecrIndexTy :: Var -> SpecType -> [Var] -> CG (Either (TError t) [Int])
makeDecrIndexTy x t args
= do spDecr <- specDecr <$> get
autosz <- autoSize <$> get
hint <- checkHint' autosz (L.lookup x spDecr)
case dindex autosz of
Nothing -> return $ Left msg
Just i -> return $ Right $ fromMaybe [i] hint
where
ts = ty_args trep
tvs = zip ts args
checkHint' = \autosz -> checkHint x ts (isDecreasing autosz cenv)
dindex = \autosz -> L.findIndex (p autosz) tvs
p autosz (t, v) = isDecreasing autosz cenv t && not (isIdTRecBound v)
msg = ErrTermin (getSrcSpan x) [F.pprint x] (text "No decreasing parameter")
cenv = makeNumEnv ts
trep = toRTypeRep $ unOCons t
recType :: F.Symbolic a
=> S.HashSet TyCon
-> (([a], [Int]), (t, [Int], SpecType))
-> SpecType
recType _ ((_, []), (_, [], t))
= t
recType autoenv ((vs, indexc), (_, index, t))
= makeRecType autoenv t v dxt index
where v = (vs !!) <$> indexc
dxt = (xts !!) <$> index
xts = zip (ty_binds trep) (ty_args trep)
trep = toRTypeRep $ unOCons t
checkIndex :: (NamedThing t, PPrint t, PPrint a)
=> (t, [a], Template (RType c tv r), [Int])
-> CG [Maybe (RType c tv r)]
checkIndex (x, vs, t, index)
= do mapM_ (safeLogIndex msg1 vs) index
mapM (safeLogIndex msg2 ts) index
where
loc = getSrcSpan x
ts = ty_args $ toRTypeRep $ unOCons $ unTemplate t
msg1 = ErrTermin loc [xd] ("No decreasing" <+> F.pprint index <-> "-th argument on" <+> xd <+> "with" <+> (F.pprint vs))
msg2 = ErrTermin loc [xd] "No decreasing parameter"
xd = F.pprint x
makeRecType :: (Enum a1, Eq a1, Num a1, F.Symbolic a)
=> S.HashSet TyCon
-> SpecType
-> [a]
-> [(F.Symbol, SpecType)]
-> [a1]
-> SpecType
makeRecType autoenv t vs dxs is
= mergecondition t $ fromRTypeRep $ trep {ty_binds = xs', ty_args = ts'}
where
(xs', ts') = unzip $ replaceN (last is) (safeFromLeft "makeRecType" $ makeDecrType autoenv vdxs) xts
vdxs = zip vs dxs
xts = zip (ty_binds trep) (ty_args trep)
trep = toRTypeRep $ unOCons t
unOCons :: RType c tv r -> RType c tv r
unOCons (RAllT v t r) = RAllT v (unOCons t) r
unOCons (RAllP p t) = RAllP p $ unOCons t
unOCons (RFun x i tx t r) = RFun x i (unOCons tx) (unOCons t) r
unOCons (RRTy _ _ OCons t) = unOCons t
unOCons t = t
mergecondition :: RType c tv r -> RType c tv r -> RType c tv r
mergecondition (RAllT _ t1 _) (RAllT v t2 r2) = RAllT v (mergecondition t1 t2) r2
mergecondition (RAllP _ t1) (RAllP p t2) = RAllP p (mergecondition t1 t2)
mergecondition (RRTy xts r OCons t1) t2 = RRTy xts r OCons (mergecondition t1 t2)
mergecondition (RFun _ _ t11 t12 _) (RFun x2 i t21 t22 r2) = RFun x2 i (mergecondition t11 t21) (mergecondition t12 t22) r2
mergecondition _ t = t
safeLogIndex :: Error -> [a] -> Int -> CG (Maybe a)
safeLogIndex err ls n
| n >= length ls = addWarning err >> return Nothing
| otherwise = return $ Just $ ls !! n
checkHint :: (NamedThing a, PPrint a, PPrint a1)
=> a -> [a1] -> (a1 -> Bool) -> Maybe [Int] -> CG (Maybe [Int])
checkHint _ _ _ Nothing
= return Nothing
checkHint x _ _ (Just ns) | L.sort ns /= ns
= addWarning (ErrTermin loc [dx] (text "The hints should be increasing")) >> return Nothing
where
loc = getSrcSpan x
dx = F.pprint x
checkHint x ts f (Just ns)
= (mapM (checkValidHint x ts f) ns) >>= (return . Just . catMaybes)
checkValidHint :: (NamedThing a, PPrint a, PPrint a1)
=> a -> [a1] -> (a1 -> Bool) -> Int -> CG (Maybe Int)
checkValidHint x ts f n
| n < 0 || n >= length ts = addWarning err >> return Nothing
| f (ts L.!! n) = return $ Just n
| otherwise = addWarning err >> return Nothing
where
err = ErrTermin loc [xd] (vcat [ "Invalid Hint" <+> F.pprint (n+1) <+> "for" <+> xd
, "in"
, F.pprint ts ])
loc = getSrcSpan x
xd = F.pprint x
--------------------------------------------------------------------------------
consCBLet :: CGEnv -> CoreBind -> CG CGEnv
--------------------------------------------------------------------------------
consCBLet γ cb = do
oldtcheck <- tcheck <$> get
isStr <- doTermCheck (getConfig γ) cb
-- TODO: yuck.
modify $ \s -> s { tcheck = oldtcheck && isStr }
γ' <- consCB (oldtcheck && isStr) isStr γ cb
modify $ \s -> s{tcheck = oldtcheck}
return γ'
--------------------------------------------------------------------------------
-- | Constraint Generation: Corebind -------------------------------------------
--------------------------------------------------------------------------------
consCBTop :: Config -> TargetInfo -> CGEnv -> CoreBind -> CG CGEnv
--------------------------------------------------------------------------------
consCBTop cfg info γ cb
| all (trustVar cfg info) xs
= foldM addB γ xs
where
xs = bindersOf cb
tt = trueTy (typeclass cfg) . varType
addB γ x = tt x >>= (\t -> γ += ("derived", F.symbol x, t))
consCBTop _ _ γ cb
= do oldtcheck <- tcheck <$> get
-- lazyVars <- specLazy <$> get
isStr <- doTermCheck (getConfig γ) cb
modify $ \s -> s { tcheck = oldtcheck && isStr}
-- remove invariants that came from the cb definition
let (γ', i) = removeInvariant γ cb --- DIFF
γ'' <- consCB (oldtcheck && isStr) isStr (γ'{cgVar = topBind cb}) cb
modify $ \s -> s { tcheck = oldtcheck}
return $ restoreInvariant γ'' i --- DIFF
where
topBind (NonRec v _) = Just v
topBind (Rec [(v,_)]) = Just v
topBind _ = Nothing
trustVar :: Config -> TargetInfo -> Var -> Bool
trustVar cfg info x = not (checkDerived cfg) && derivedVar (giSrc info) x
derivedVar :: TargetSrc -> Var -> Bool
derivedVar src x = S.member x (giDerVars src)
doTermCheck :: Config -> Bind Var -> CG Bool
doTermCheck cfg bind = do
lazyVs <- specLazy <$> get
termVs <- specTmVars <$> get
let skip = any (\x -> S.member x lazyVs || nocheck x) xs
let chk = not (structuralTerm cfg) || any (\x -> S.member x termVs) xs
return $ chk && not skip
where
nocheck = if typeclass cfg then GM.isEmbeddedDictVar else GM.isInternal
xs = bindersOf bind
-- nonStructTerm && not skip
-- RJ: AAAAAAARGHHH!!!!!! THIS CODE IS HORRIBLE!!!!!!!!!
consCBSizedTys :: CGEnv -> [(Var, CoreExpr)] -> CG CGEnv
consCBSizedTys γ xes
= do xets <- forM xes $ \(x, e) -> liftM (x, e,) (varTemplate γ (x, Just e))
autoenv <- autoSize <$> get
ts <- mapM (T.mapM refreshArgs) $ (thd3 <$> xets)
let vs = zipWith collectArgs ts es
is <- mapM makeDecrIndex (zip3 xs ts vs) >>= checkSameLens
let xeets = (\vis -> [(vis, x) | x <- zip3 xs is $ map unTemplate ts]) <$> (zip vs is)
(L.transpose <$> mapM checkIndex (zip4 xs vs ts is)) >>= checkEqTypes
let rts = (recType autoenv <$>) <$> xeets
let xts = zip xs ts
γ' <- foldM extender γ xts
let γs = zipWith makeRecInvariants [γ' `setTRec` zip xs rts' | rts' <- rts] (filter (not . noMakeRec) <$> vs)
let xets' = zip3 xs es ts
mapM_ (uncurry $ consBind True) (zip γs xets')
return γ'
where
noMakeRec = if allowTC then GM.isEmbeddedDictVar else GM.isPredVar
allowTC = typeclass (getConfig γ)
(xs, es) = unzip xes
dxs = F.pprint <$> xs
collectArgs = GM.collectArguments . length . ty_binds . toRTypeRep . unOCons . unTemplate
checkEqTypes :: [[Maybe SpecType]] -> CG [[SpecType]]
checkEqTypes x = mapM (checkAll err1 toRSort) (catMaybes <$> x)
checkSameLens = checkAll err2 length
err1 = ErrTermin loc dxs $ text "The decreasing parameters should be of same type"
err2 = ErrTermin loc dxs $ text "All Recursive functions should have the same number of decreasing parameters"
loc = getSrcSpan (head xs)
checkAll _ _ [] = return []
checkAll err f (x:xs)
| all (==(f x)) (f <$> xs) = return (x:xs)
| otherwise = addWarning err >> return []
consCBWithExprs :: CGEnv -> [(Var, CoreExpr)] -> CG CGEnv
consCBWithExprs γ xes
= do xets <- forM xes $ \(x, e) -> liftM (x, e,) (varTemplate γ (x, Just e))
texprs <- termExprs <$> get
let xtes = catMaybes $ (`lookup` texprs) <$> xs
let ts = safeFromAsserted err . thd3 <$> xets
ts' <- mapM refreshArgs ts
let xts = zip xs (Asserted <$> ts')
γ' <- foldM extender γ xts
let γs = makeTermEnvs γ' xtes xes ts ts'
let xets' = zip3 xs es (Asserted <$> ts')
mapM_ (uncurry $ consBind True) (zip γs xets')
return γ'
where (xs, es) = unzip xes
lookup k m | Just x <- M.lookup k m = Just (k, x)
| otherwise = Nothing
err = "Constant: consCBWithExprs"
makeTermEnvs :: CGEnv -> [(Var, [F.Located F.Expr])] -> [(Var, CoreExpr)]
-> [SpecType] -> [SpecType]
-> [CGEnv]
makeTermEnvs γ xtes xes ts ts' = setTRec γ . zip xs <$> rts
where
vs = zipWith collectArgs ts es
ys = (fst5 . bkArrowDeep) <$> ts
ys' = (fst5 . bkArrowDeep) <$> ts'
sus' = zipWith mkSub ys ys'
sus = zipWith mkSub ys ((F.symbol <$>) <$> vs)
ess = (\x -> (safeFromJust (err x) $ (x `L.lookup` xtes))) <$> xs
tes = zipWith (\su es -> F.subst su <$> es) sus ess
tes' = zipWith (\su es -> F.subst su <$> es) sus' ess
rss = zipWith makeLexRefa tes' <$> (repeat <$> tes)
rts = zipWith (addObligation OTerm) ts' <$> rss
(xs, es) = unzip xes
mkSub ys ys' = F.mkSubst [(x, F.EVar y) | (x, y) <- zip ys ys']
collectArgs = GM.collectArguments . length . ty_binds . toRTypeRep
err x = "Constant: makeTermEnvs: no terminating expression for " ++ GM.showPpr x
addObligation :: Oblig -> SpecType -> RReft -> SpecType
addObligation o t r = mkArrow αs πs yts xts $ RRTy [] r o t2
where
(αs, πs, t1) = bkUniv t
((xs',is',ts',rs'),(xs, is, ts, rs), t2) = bkArrow t1
xts = zip4 xs is ts rs
yts = zip4 xs' is' ts' rs'
--------------------------------------------------------------------------------
consCB :: Bool -> Bool -> CGEnv -> CoreBind -> CG CGEnv
--------------------------------------------------------------------------------
-- do termination checking
consCB True _ γ (Rec xes)
= do texprs <- termExprs <$> get
modify $ \i -> i { recCount = recCount i + length xes }
let xxes = catMaybes $ (`lookup` texprs) <$> xs
if null xxes
then consCBSizedTys γ xes
else check xxes <$> consCBWithExprs γ xes
where
xs = fst (unzip xes)
check ys r | length ys == length xs = r
| otherwise = panic (Just loc) $ msg
msg = "Termination expressions must be provided for all mutually recursive binders"
loc = getSrcSpan (head xs)
lookup k m = (k,) <$> M.lookup k m
-- don't do termination checking, but some strata checks?
consCB _ False γ (Rec xes)
= do xets <- forM xes $ \(x, e) -> (x, e,) <$> varTemplate γ (x, Just e)
modify $ \i -> i { recCount = recCount i + length xes }
let xts = [(x, to) | (x, _, to) <- xets]
γ' <- foldM extender (γ `setRecs` (fst <$> xts)) xts
mapM_ (consBind True γ') xets
return γ'
-- don't do termination checking, and don't do any strata checks either?
consCB _ _ γ (Rec xes)
= do xets <- forM xes $ \(x, e) -> liftM (x, e,) (varTemplate γ (x, Just e))
modify $ \i -> i { recCount = recCount i + length xes }
let xts = [(x, to) | (x, _, to) <- xets]
γ' <- foldM extender (γ `setRecs` (fst <$> xts)) xts
mapM_ (consBind True γ') xets
return γ'
-- | NV: Dictionaries are not checked, because
-- | class methods' preconditions are not satisfied
consCB _ _ γ (NonRec x _) | isDictionary x
= do t <- trueTy (typeclass (getConfig γ)) (varType x)
extender γ (x, Assumed t)
where
isDictionary = isJust . dlookup (denv γ)
consCB _ _ γ (NonRec x _ ) | isHoleVar x && typedHoles (getConfig γ)
= return γ
consCB _ _ γ (NonRec x def)
| Just (w, τ) <- grepDictionary def
, Just d <- dlookup (denv γ) w
= do t <- mapM (trueTy (typeclass (getConfig γ))) τ
mapM addW (WfC γ <$> t)
let xts = dmap (fmap (f t)) d
let γ' = γ { denv = dinsert (denv γ) x xts }
t <- trueTy (typeclass (getConfig γ)) (varType x)
extender γ' (x, Assumed t)
where
f [t'] (RAllT α te _) = subsTyVar_meet' (ty_var_value α, t') te
f (t':ts) (RAllT α te _) = f ts $ subsTyVar_meet' (ty_var_value α, t') te
f _ _ = impossible Nothing "consCB on Dictionary: this should not happen"
consCB _ _ γ (NonRec x e)
= do to <- varTemplate γ (x, Nothing)
to' <- consBind False γ (x, e, to) >>= (addPostTemplate γ)
extender γ (x, makeSingleton γ (simplify e) <$> to')
grepDictionary :: CoreExpr -> Maybe (Var, [Type])
grepDictionary = go []
where
go ts (App (Var w) (Type t)) = Just (w, reverse (t:ts))
go ts (App e (Type t)) = go (t:ts) e
go ts (App e (Var _)) = go ts e
go ts (Let _ e) = go ts e
go _ _ = Nothing
--------------------------------------------------------------------------------
consBind :: Bool -> CGEnv -> (Var, CoreExpr, Template SpecType) -> CG (Template SpecType)
--------------------------------------------------------------------------------
consBind _ _ (x, _, Assumed t)
| RecSelId {} <- idDetails x -- don't check record selectors with assumed specs
= return $ F.notracepp ("TYPE FOR SELECTOR " ++ show x) $ Assumed t
consBind isRec γ (x, e, Asserted spect)
= do let γ' = γ `setBind` x
(_,πs,_) = bkUniv spect
γπ <- foldM addPToEnv γ' πs
-- take implcits out of the function's SpecType and into the env
let tyr = toRTypeRep spect
let spect' = fromRTypeRep (tyr { ty_ebinds = [], ty_einfo = [], ty_eargs = [], ty_erefts = [] })
γπ <- foldM (+=) γπ $ (\(y,t)->("implicitError",y,t)) <$> zip (ty_ebinds tyr) (ty_eargs tyr)
cconsE γπ e (weakenResult (typeclass (getConfig γ)) x spect')
when (F.symbol x `elemHEnv` holes γ) $
-- have to add the wf constraint here for HOLEs so we have the proper env
addW $ WfC γπ $ fmap killSubst spect
addIdA x (defAnn isRec spect)
return $ Asserted spect
consBind isRec γ (x, e, Internal spect)
= do let γ' = γ `setBind` x
(_,πs,_) = bkUniv spect
γπ <- foldM addPToEnv γ' πs
let γπ' = γπ {cerr = Just $ ErrHMeas (getLocation γπ) (pprint x) (text explanation)}
cconsE γπ' e spect
when (F.symbol x `elemHEnv` holes γ) $
-- have to add the wf constraint here for HOLEs so we have the proper env
addW $ WfC γπ $ fmap killSubst spect
addIdA x (defAnn isRec spect)
return $ Internal spect
where
explanation = "Cannot give singleton type to the function definition."
consBind isRec γ (x, e, Assumed spect)
= do let γ' = γ `setBind` x
γπ <- foldM addPToEnv γ' πs
cconsE γπ e =<< true (typeclass (getConfig γ)) spect
addIdA x (defAnn isRec spect)
return $ Asserted spect
where πs = ty_preds $ toRTypeRep spect
consBind isRec γ (x, e, Unknown)
= do t' <- consE (γ `setBind` x) e
t <- topSpecType x t'
addIdA x (defAnn isRec t)
when (isExportedId x) (addKuts x t)
return $ Asserted t
killSubst :: RReft -> RReft
killSubst = fmap killSubstReft
killSubstReft :: F.Reft -> F.Reft
killSubstReft = trans kv () ()
where
kv = defaultVisitor { txExpr = ks }
ks _ (F.PKVar k _) = F.PKVar k mempty
ks _ p = p
defAnn :: Bool -> t -> Annot t
defAnn True = AnnRDf
defAnn False = AnnDef
addPToEnv :: CGEnv
-> PVar RSort -> CG CGEnv
addPToEnv γ π
= do γπ <- γ += ("addSpec1", pname π, pvarRType π)
foldM (+=) γπ [("addSpec2", x, ofRSort t) | (t, x, _) <- pargs π]
extender :: F.Symbolic a => CGEnv -> (a, Template SpecType) -> CG CGEnv
extender γ (x, Asserted t)
= case lookupREnv (F.symbol x) (assms γ) of
Just t' -> γ += ("extender", F.symbol x, t')
_ -> γ += ("extender", F.symbol x, t)
extender γ (x, Assumed t)
= γ += ("extender", F.symbol x, t)
extender γ _
= return γ
data Template a
= Asserted a
| Assumed a
| Internal a
| Unknown
deriving (Functor, F.Foldable, T.Traversable)
deriving instance (Show a) => (Show (Template a))
instance PPrint a => PPrint (Template a) where
pprintTidy k (Asserted t) = "Asserted" <+> pprintTidy k t
pprintTidy k (Assumed t) = "Assumed" <+> pprintTidy k t
pprintTidy k (Internal t) = "Internal" <+> pprintTidy k t
pprintTidy _ Unknown = "Unknown"
unTemplate :: Template t -> t
unTemplate (Asserted t) = t
unTemplate (Assumed t) = t
unTemplate (Internal t) = t
unTemplate _ = panic Nothing "Constraint.Generate.unTemplate called on `Unknown`"
addPostTemplate :: CGEnv
-> Template SpecType
-> CG (Template SpecType)
addPostTemplate γ (Asserted t) = Asserted <$> addPost γ t
addPostTemplate γ (Assumed t) = Assumed <$> addPost γ t
addPostTemplate γ (Internal t) = Internal <$> addPost γ t
addPostTemplate _ Unknown = return Unknown
safeFromAsserted :: [Char] -> Template t -> t
safeFromAsserted _ (Asserted t) = t
safeFromAsserted msg _ = panic Nothing $ "safeFromAsserted:" ++ msg
-- | @varTemplate@ is only called with a `Just e` argument when the `e`
-- corresponds to the body of a @Rec@ binder.
varTemplate :: CGEnv -> (Var, Maybe CoreExpr) -> CG (Template SpecType)
varTemplate γ (x, eo) = varTemplate' γ (x, eo) >>= mapM (topSpecType x)
-- | @lazVarTemplate@ is like `varTemplate` but for binders that are *not*
-- termination checked and hence, the top-level refinement / KVar is
-- stripped out. e.g. see tests/neg/T743.hs
-- varTemplate :: CGEnv -> (Var, Maybe CoreExpr) -> CG (Template SpecType)
-- lazyVarTemplate γ (x, eo) = dbg <$> (topRTypeBase <$>) <$> varTemplate' γ (x, eo)
-- where
-- dbg = traceShow ("LAZYVAR-TEMPLATE: " ++ show x)
varTemplate' :: CGEnv -> (Var, Maybe CoreExpr) -> CG (Template SpecType)
varTemplate' γ (x, eo)
= case (eo, lookupREnv (F.symbol x) (grtys γ), lookupREnv (F.symbol x) (assms γ), lookupREnv (F.symbol x) (intys γ)) of
(_, Just t, _, _) -> Asserted <$> refreshArgsTop (x, t)
(_, _, _, Just t) -> Internal <$> refreshArgsTop (x, t)
(_, _, Just t, _) -> Assumed <$> refreshArgsTop (x, t)
(Just e, _, _, _) -> do t <- freshTy_expr (typeclass (getConfig γ)) (RecBindE x) e (exprType e)
addW (WfC γ t)
Asserted <$> refreshArgsTop (x, t)
(_, _, _, _) -> return Unknown
-- | @topSpecType@ strips out the top-level refinement of "derived var"
topSpecType :: Var -> SpecType -> CG SpecType
topSpecType x t = do
info <- ghcI <$> get
return $ if derivedVar (giSrc info) x then topRTypeBase t else t
--------------------------------------------------------------------------------
-- | Bidirectional Constraint Generation: CHECKING -----------------------------
--------------------------------------------------------------------------------
cconsE :: CGEnv -> CoreExpr -> SpecType -> CG ()
--------------------------------------------------------------------------------
cconsE g e t = do
-- NOTE: tracing goes here
-- traceM $ printf "cconsE:\n expr = %s\n exprType = %s\n lqType = %s\n" (showPpr e) (showPpr (exprType e)) (showpp t)
cconsE' g e t
--------------------------------------------------------------------------------
cconsE' :: CGEnv -> CoreExpr -> SpecType -> CG ()
--------------------------------------------------------------------------------
cconsE' γ e t
| Just (Rs.PatSelfBind _x e') <- Rs.lift e
= cconsE' γ e' t
| Just (Rs.PatSelfRecBind x e') <- Rs.lift e
= let γ' = γ { grtys = insertREnv (F.symbol x) t (grtys γ)}
in void $ consCBLet γ' (Rec [(x, e')])
cconsE' γ e@(Let b@(NonRec x _) ee) t
= do sp <- specLVars <$> get
if (x `S.member` sp)
then cconsLazyLet γ e t
else do γ' <- consCBLet γ b
cconsE γ' ee t
cconsE' γ e (RAllP p t)
= cconsE γ' e t''
where
t' = replacePredsWithRefs su <$> t
su = (uPVar p, pVartoRConc p)
(css, t'') = splitConstraints (typeclass (getConfig γ)) t'
γ' = L.foldl' addConstraints γ css
cconsE' γ (Let b e) t
= do γ' <- consCBLet γ b
cconsE γ' e t
cconsE' γ (Case e x _ cases) t
= do γ' <- consCBLet γ (NonRec x e)
forM_ cases $ cconsCase γ' x t nonDefAlts
where
nonDefAlts = [a | (a, _, _) <- cases, a /= DEFAULT]
_msg = "cconsE' #nonDefAlts = " ++ show (length (nonDefAlts))
cconsE' γ (Lam α e) (RAllT α' t r) | isTyVar α
= do γ' <- updateEnvironment γ α
addForAllConstraint γ' α e (RAllT α' t r)
cconsE γ' e $ subsTyVar_meet' (ty_var_value α', rVar α) t
cconsE' γ (Lam x e) (RFun y i ty t r)
| not (isTyVar x)
= do γ' <- γ += ("cconsE", x', ty)
cconsE γ' e t'
addFunctionConstraint γ x e (RFun x' i ty t' r')
addIdA x (AnnDef ty)
where
x' = F.symbol x
t' = t `F.subst1` (y, F.EVar x')
r' = r `F.subst1` (y, F.EVar x')
cconsE' γ (Tick tt e) t
= cconsE (γ `setLocation` (Sp.Tick tt)) e t
cconsE' γ (Cast e co) t
-- See Note [Type classes with a single method]
| Just f <- isClassConCo co
= cconsE γ (f e) t
cconsE' γ e@(Cast e' c) t
= do t' <- castTy γ (exprType e) e' c
addC (SubC γ (F.notracepp ("Casted Type for " ++ GM.showPpr e ++ "\n init type " ++ showpp t) t') t) ("cconsE Cast: " ++ GM.showPpr e)
cconsE' γ (Var x) t | isHoleVar x && typedHoles (getConfig γ)
= addHole x t γ
cconsE' γ e t
= do te <- consE γ e
te' <- instantiatePreds γ e te >>= addPost γ
addC (SubC γ te' t) ("cconsE: " ++ "\n t = " ++ showpp t ++ "\n te = " ++ showpp te ++ GM.showPpr e)
lambdaSingleton :: CGEnv -> F.TCEmb TyCon -> Var -> CoreExpr -> UReft F.Reft
lambdaSingleton γ tce x e
| higherOrderFlag γ, Just e' <- lamExpr γ e
= uTop $ F.exprReft $ F.ELam (F.symbol x, sx) e'
where
sx = typeSort tce $ Ghc.expandTypeSynonyms $ varType x
lambdaSingleton _ _ _ _
= mempty
addForAllConstraint :: CGEnv -> Var -> CoreExpr -> SpecType -> CG ()
addForAllConstraint γ _ _ (RAllT a t r)
| F.isTauto r
= return ()
| otherwise
= do t' <- true (typeclass (getConfig γ)) t
let truet = RAllT a $ unRAllP t'
addC (SubC γ (truet mempty) $ truet r) "forall constraint true"
where unRAllP (RAllT a t r) = RAllT a (unRAllP t) r
unRAllP (RAllP _ t) = unRAllP t
unRAllP t = t
addForAllConstraint γ _ _ _
= impossible (Just $ getLocation γ) "addFunctionConstraint: called on non function argument"
addFunctionConstraint :: CGEnv -> Var -> CoreExpr -> SpecType -> CG ()
addFunctionConstraint γ x e (RFun y i ty t r)
= do ty' <- true (typeclass (getConfig γ)) ty
t' <- true (typeclass (getConfig γ)) t
let truet = RFun y i ty' t'
case (lamExpr γ e, higherOrderFlag γ) of
(Just e', True) -> do tce <- tyConEmbed <$> get
let sx = typeSort tce $ varType x
let ref = uTop $ F.exprReft $ F.ELam (F.symbol x, sx) e'
addC (SubC γ (truet ref) $ truet r) "function constraint singleton"
_ -> addC (SubC γ (truet mempty) $ truet r) "function constraint true"
addFunctionConstraint γ _ _ _
= impossible (Just $ getLocation γ) "addFunctionConstraint: called on non function argument"
splitConstraints :: TyConable c
=> Bool -> RType c tv r -> ([[(F.Symbol, RType c tv r)]], RType c tv r)
splitConstraints allowTC (RRTy cs _ OCons t)
= let (css, t') = splitConstraints allowTC t in (cs:css, t')
splitConstraints allowTC (RFun x i tx@(RApp c _ _ _) t r) | isErasable c
= let (css, t') = splitConstraints allowTC t in (css, RFun x i tx t' r)
where isErasable = if allowTC then isEmbeddedDict else isClass
splitConstraints _ t
= ([], t)
-------------------------------------------------------------------
-- | @instantiateGhosts@ peels away implicit argument binders,
-- instantiates them with fresh variables, and adds those variables
-- to the context as @ebind@s TODO: the second half
-------------------------------------------------------------------
instantiateGhosts :: CGEnv
-> SpecType
-> CG (Bool, CGEnv, SpecType)
instantiateGhosts γ t | not (null yts)
= do ys' <- mapM (const fresh) ys
γ' <- foldM addEEnv γ (zip ys' ts)
let su = F.mkSubst $ zip ys (F.EVar <$> ys')
return (True, γ', F.subst su te')
where (yts, te') = bkImplicit t
(ys, ts) = unzip yts
instantiateGhosts γ t = return (False, γ, t)
bkImplicit :: RType c tv r
-> ( [(F.Symbol, RType c tv r)]
, RType c tv r)
bkImplicit (RImpF x _ tx t _) = ((x,tx):acc, t')
where (acc,t') = bkImplicit t
bkImplicit t = ([],t)
-------------------------------------------------------------------
-- | @instantiatePreds@ peels away the universally quantified @PVars@
-- of a @RType@, generates fresh @Ref@ for them and substitutes them
-- in the body.
-------------------------------------------------------------------
instantiatePreds :: CGEnv
-> CoreExpr
-> SpecType
-> CG SpecType
instantiatePreds γ e (RAllP π t)
= do r <- freshPredRef γ e π
instantiatePreds γ e $ replacePreds "consE" t [(π, r)]
instantiatePreds _ _ t0
= return t0
-------------------------------------------------------------------
cconsLazyLet :: CGEnv
-> CoreExpr
-> SpecType
-> CG ()
cconsLazyLet γ (Let (NonRec x ex) e) t
= do tx <- trueTy (typeclass (getConfig γ)) (varType x)
γ' <- (γ, "Let NonRec") +++= (x', ex, tx)
cconsE γ' e t
where
x' = F.symbol x
cconsLazyLet _ _ _
= panic Nothing "Constraint.Generate.cconsLazyLet called on invalid inputs"
--------------------------------------------------------------------------------
-- | Bidirectional Constraint Generation: SYNTHESIS ----------------------------
--------------------------------------------------------------------------------
consE :: CGEnv -> CoreExpr -> CG SpecType
--------------------------------------------------------------------------------
consE γ e
| patternFlag γ
, Just p <- Rs.lift e
= consPattern γ (F.notracepp "CONSE-PATTERN: " p) (exprType e)
-- NV CHECK 3 (unVar and does this hack even needed?)
-- NV (below) is a hack to type polymorphic axiomatized functions
-- no need to check this code with flag, the axioms environment with
-- is empty if there is no axiomatization.
-- [NOTE: PLE-OPT] We *disable* refined instantiation for
-- reflected functions inside proofs.
consE γ (Var x)
= do t <- varRefType γ x
addLocA (Just x) (getLocation γ) (varAnn γ x t)
return t
consE _ (Lit c)
= refreshVV $ uRType $ literalFRefType c
consE γ e'@(App e a@(Type τ))
= do RAllT α te _ <- checkAll ("Non-all TyApp with expr", e) γ <$> consE γ e
t <- if not (nopolyinfer (getConfig γ)) && isPos α && isGenericVar (ty_var_value α) te
then freshTy_type (typeclass (getConfig γ)) TypeInstE e τ
else trueTy (typeclass (getConfig γ)) τ
addW $ WfC γ t
t' <- refreshVV t
tt0 <- instantiatePreds γ e' (subsTyVar_meet' (ty_var_value α, t') te)
let tt = makeSingleton γ (simplify e') $ subsTyReft γ (ty_var_value α) τ tt0
case rTVarToBind α of
Just (x, _) -> return $ maybe (checkUnbound γ e' x tt a) (F.subst1 tt . (x,)) (argType τ)
Nothing -> return tt
where
isPos α = not (extensionality (getConfig γ)) || rtv_is_pol (ty_var_info α)
consE γ e'@(App e a) | Just aDict <- getExprDict γ a
= case dhasinfo (dlookup (denv γ) aDict) (getExprFun γ e) of
Just riSig -> return $ fromRISig riSig
_ -> do
([], πs, te) <- bkUniv <$> consE γ e
te' <- instantiatePreds γ e' $ foldr RAllP te πs
(γ', te''') <- dropExists γ te'
te'' <- dropConstraints γ te'''
updateLocA {- πs -} (exprLoc e) te''
let RFun x _ tx t _ = checkFun ("Non-fun App with caller ", e') γ te''
cconsE γ' a tx
addPost γ' $ maybe (checkUnbound γ' e' x t a) (F.subst1 t . (x,)) (argExpr γ a)
consE γ e'@(App e a)
= do ([], πs, te) <- bkUniv <$> consE γ ({- GM.tracePpr ("APP-EXPR: " ++ GM.showPpr (exprType e)) -} e)
te' <- instantiatePreds γ e' $ foldr RAllP te πs
(γ', te''') <- dropExists γ te'
te'' <- dropConstraints γ te'''
updateLocA (exprLoc e) te''
(hasGhost, γ'', te''') <- instantiateGhosts γ' te''
let RFun x _ tx t _ = checkFun ("Non-fun App with caller ", e') γ te'''
cconsE γ'' a tx
tout <- makeSingleton γ'' (simplify e') <$> (addPost γ'' $ maybe (checkUnbound γ'' e' x t a) (F.subst1 t . (x,)) (argExpr γ $ simplify a))
if hasGhost
then do
tk <- freshTy_type (typeclass (getConfig γ)) ImplictE e' $ exprType e'
addW $ WfC γ tk
addC (SubC γ'' tout tk) ""
return tk
else return tout
consE γ (Lam α e) | isTyVar α
= do γ' <- updateEnvironment γ α
t' <- consE γ' e
return $ RAllT (makeRTVar $ rTyVar α) t' mempty
consE γ e@(Lam x e1)
= do tx <- freshTy_type (typeclass (getConfig γ)) LamE (Var x) τx
γ' <- γ += ("consE", F.symbol x, tx)
t1 <- consE γ' e1
addIdA x $ AnnDef tx
addW $ WfC γ tx
tce <- tyConEmbed <$> get
return $ RFun (F.symbol x) (mkRFInfo $ getConfig γ) tx t1 $ lambdaSingleton γ tce x e1
where
FunTy { ft_arg = τx } = exprType e
consE γ e@(Let _ _)
= cconsFreshE LetE γ e
consE γ e@(Case _ _ _ [_])
| Just p@(Rs.PatProject {}) <- Rs.lift e
= consPattern γ p (exprType e)
consE γ e@(Case _ _ _ cs)
= cconsFreshE (caseKVKind cs) γ e
consE γ (Tick tt e)
= do t <- consE (setLocation γ (Sp.Tick tt)) e
addLocA Nothing (GM.tickSrcSpan tt) (AnnUse t)
return t
-- See Note [Type classes with a single method]
consE γ (Cast e co)
| Just f <- isClassConCo co
= consE γ (f e)
consE γ e@(Cast e' c)
= castTy γ (exprType e) e' c
consE γ e@(Coercion _)
= trueTy (typeclass (getConfig γ)) $ exprType e
consE _ e@(Type t)
= panic Nothing $ "consE cannot handle type " ++ GM.showPpr (e, t)
caseKVKind ::[Alt Var] -> KVKind
caseKVKind [(DataAlt _, _, Var _)] = ProjectE
caseKVKind cs = CaseE (length cs)
updateEnvironment :: CGEnv -> TyVar -> CG CGEnv
updateEnvironment γ a
| isValKind (tyVarKind a)
= γ += ("varType", F.symbol $ varName a, kindToRType $ tyVarKind a)
| otherwise
= return γ
getExprFun :: CGEnv -> CoreExpr -> Var
getExprFun γ e = go e
where
go (App x (Type _)) = go x
go (Var x) = x
go _ = panic (Just (getLocation γ)) msg
msg = "getFunName on \t" ++ GM.showPpr e
-- | `exprDict e` returns the dictionary `Var` inside the expression `e`
getExprDict :: CGEnv -> CoreExpr -> Maybe Var
getExprDict γ = go
where
go (Var x) = case dlookup (denv γ) x of {Just _ -> Just x; Nothing -> Nothing}
go (Tick _ e) = go e
go (App a (Type _)) = go a
go (Let _ e) = go e
go _ = Nothing
--------------------------------------------------------------------------------
-- | With GADTs and reflection, refinements can contain type variables,
-- as 'coercions' (see ucsd-progsys/#1424). At application sites, we
-- must also substitute those from the refinements (not just the types).
-- https://github.com/ucsd-progsys/liquidhaskell/issues/1424
--
-- see: tests/ple/{pos,neg}/T1424.hs
--
--------------------------------------------------------------------------------
subsTyReft :: CGEnv -> RTyVar -> Type -> SpecType -> SpecType
subsTyReft γ a t = mapExprReft (\_ -> F.applyCoSub coSub)
where
coSub = M.fromList [(F.symbol a, typeSort (emb γ) t)]
--------------------------------------------------------------------------------
-- | Type Synthesis for Special @Pattern@s -------------------------------------
--------------------------------------------------------------------------------
consPattern :: CGEnv -> Rs.Pattern -> Type -> CG SpecType
{- [NOTE] special type rule for monadic-bind application
G |- e1 ~> m tx G, x:tx |- e2 ~> m t
-----------------------------------------
G |- (e1 >>= \x -> e2) ~> m t
-}
consPattern γ (Rs.PatBind e1 x e2 _ _ _ _ _) _ = do
tx <- checkMonad (msg, e1) γ <$> consE γ e1
γ' <- γ += ("consPattern", F.symbol x, tx)
addIdA x (AnnDef tx)
mt <- consE γ' e2
return mt
where
msg = "This expression has a refined monadic type; run with --no-pattern-inline: "
{- [NOTE] special type rule for monadic-return
G |- e ~> et
------------------------
G |- return e ~ m et
-}
consPattern γ (Rs.PatReturn e m _ _ _) t = do
et <- F.notracepp "Cons-Pattern-Ret" <$> consE γ e
mt <- trueTy (typeclass (getConfig γ)) m
tt <- trueTy (typeclass (getConfig γ)) t
return (mkRAppTy mt et tt) -- /// {- $ RAppTy mt et mempty -}
{- [NOTE] special type rule for field projection, is
t = G(x) ti = Proj(t, i)
-----------------------------------------
G |- case x of C [y1...yn] -> yi : ti
-}
consPattern γ (Rs.PatProject xe _ τ c ys i) _ = do
let yi = ys !! i
t <- (addW . WfC γ) <<= freshTy_type (typeclass (getConfig γ)) ProjectE (Var yi) τ
γ' <- caseEnv γ xe [] (DataAlt c) ys (Just [i])
ti <- {- γ' ??= yi -} varRefType γ' yi
addC (SubC γ' ti t) "consPattern:project"
return t
consPattern γ (Rs.PatSelfBind _ e) _ =
consE γ e
consPattern γ p@(Rs.PatSelfRecBind {}) _ =
cconsFreshE LetE γ (Rs.lower p)
mkRAppTy :: SpecType -> SpecType -> SpecType -> SpecType
mkRAppTy mt et (RAppTy _ _ _) = RAppTy mt et mempty
mkRAppTy _ et (RApp c [_] [] _) = RApp c [et] [] mempty
mkRAppTy _ _ _ = panic Nothing $ "Unexpected return-pattern"
checkMonad :: (Outputable a) => (String, a) -> CGEnv -> SpecType -> SpecType
checkMonad x g = go . unRRTy
where
go (RApp _ ts [] _)
| length ts > 0 = last ts
go (RAppTy _ t _) = t
go t = checkErr x g t
unRRTy :: SpecType -> SpecType
unRRTy (RRTy _ _ _ t) = unRRTy t
unRRTy t = t
--------------------------------------------------------------------------------
castTy :: CGEnv -> Type -> CoreExpr -> Coercion -> CG SpecType
castTy' :: CGEnv -> Type -> CoreExpr -> CG SpecType
--------------------------------------------------------------------------------
castTy γ t e (AxiomInstCo ca _ _)
= fromMaybe <$> castTy' γ t e <*> lookupNewType (coAxiomTyCon ca)
castTy γ t e (SymCo (AxiomInstCo ca _ _))
= do mtc <- lookupNewType (coAxiomTyCon ca)
case mtc of
Just tc -> cconsE γ e tc
Nothing -> return ()
castTy' γ t e
castTy γ t e _
= castTy' γ t e
castTy' γ τ (Var x)
= do t <- trueTy (typeclass (getConfig γ)) τ
-- tx <- varRefType γ x -- NV HERE: the refinements of the var x do not get into the
-- -- environment. Check
let ce = if typeclass (getConfig γ) && (noADT (getConfig γ)) then F.expr x
else eCoerc (typeSort (emb γ) $ Ghc.expandTypeSynonyms $ varType x)
(typeSort (emb γ) τ)
$ F.expr x
return ((t `strengthen` (uTop $ F.uexprReft $ ce)) {- `F.meet` tx -})
where eCoerc s t e
| s == t = e
| otherwise = F.ECoerc s t e
castTy' γ t (Tick _ e)
= castTy' γ t e
castTy' _ _ e
= panic Nothing $ "castTy cannot handle expr " ++ GM.showPpr e
{-
showCoercion :: Coercion -> String
showCoercion (AxiomInstCo co1 co2 co3)
= "AxiomInstCo " ++ showPpr co1 ++ "\t\t " ++ showPpr co2 ++ "\t\t" ++ showPpr co3 ++ "\n\n" ++
"COAxiom Tycon = " ++ showPpr (coAxiomTyCon co1) ++ "\nBRANCHES\n" ++ concatMap showBranch bs
where
bs = fromBranchList $ co_ax_branches co1
showBranch ab = "\nCoAxiom \nLHS = " ++ showPpr (coAxBranchLHS ab) ++
"\nRHS = " ++ showPpr (coAxBranchRHS ab)
showCoercion (SymCo c)
= "Symc :: " ++ showCoercion c
showCoercion c
= "Coercion " ++ showPpr c
-}
isClassConCo :: Coercion -> Maybe (Expr Var -> Expr Var)
-- See Note [Type classes with a single method]
isClassConCo co
| Pair t1 t2 <- coercionKind co
, isClassPred t2
, (tc,ts) <- splitTyConApp t2
, [dc] <- tyConDataCons tc
, [tm] <- map irrelevantMult (Ghc.dataConOrigArgTys dc)
-- tcMatchTy because we have to instantiate the class tyvars
, Just _ <- ruleMatchTyX (mkUniqSet $ tyConTyVars tc) (mkRnEnv2 emptyInScopeSet) emptyTvSubstEnv tm t1
= Just (\e -> mkCoreConApps dc $ map Type ts ++ [e])
| otherwise
= Nothing
where
ruleMatchTyX =ruleMatchTyKiX -- TODO: is this correct?
----------------------------------------------------------------------
-- Note [Type classes with a single method]
----------------------------------------------------------------------
-- GHC 7.10 encodes type classes with a single method as newtypes and
-- `cast`s between the method and class type instead of applying the
-- class constructor. Just rewrite the core to what we're used to
-- seeing..
--
-- specifically, we want to rewrite
--
-- e `cast` ((a -> b) ~ C)
--
-- to
--
-- D:C e
--
-- but only when
--
-- D:C :: (a -> b) -> C
--------------------------------------------------------------------------------
-- | @consFreshE@ is used to *synthesize* types with a **fresh template**.
-- e.g. at joins, recursive binders, polymorphic instantiations etc. It is
-- the "portal" that connects `consE` (synthesis) and `cconsE` (checking)
--------------------------------------------------------------------------------
cconsFreshE :: KVKind -> CGEnv -> CoreExpr -> CG SpecType
cconsFreshE kvkind γ e = do
t <- freshTy_type (typeclass (getConfig γ)) kvkind e $ exprType e
addW $ WfC γ t
cconsE γ e t
return t
--------------------------------------------------------------------------------
checkUnbound :: (Show a, Show a2, F.Subable a)
=> CGEnv -> CoreExpr -> F.Symbol -> a -> a2 -> a
checkUnbound γ e x t a
| x `notElem` (F.syms t) = t
| otherwise = panic (Just $ getLocation γ) msg
where
msg = unlines [ "checkUnbound: " ++ show x ++ " is elem of syms of " ++ show t
, "In", GM.showPpr e, "Arg = " , show a ]
dropExists :: CGEnv -> SpecType -> CG (CGEnv, SpecType)
dropExists γ (REx x tx t) = (, t) <$> γ += ("dropExists", x, tx)
dropExists γ t = return (γ, t)
dropConstraints :: CGEnv -> SpecType -> CG SpecType
dropConstraints γ (RFun x i tx@(RApp c _ _ _) t r) | isErasable c
= (flip (RFun x i tx)) r <$> dropConstraints γ t
where
isErasable = if typeclass (getConfig γ) then isEmbeddedDict else isClass
dropConstraints γ (RRTy cts _ OCons t)
= do γ' <- foldM (\γ (x, t) -> γ `addSEnv` ("splitS", x,t)) γ xts
addC (SubC γ' t1 t2) "dropConstraints"
dropConstraints γ t
where
(xts, t1, t2) = envToSub cts
dropConstraints _ t = return t
-------------------------------------------------------------------------------------
cconsCase :: CGEnv -> Var -> SpecType -> [AltCon] -> (AltCon, [Var], CoreExpr) -> CG ()
-------------------------------------------------------------------------------------
cconsCase γ x t acs (ac, ys, ce)
= do cγ <- caseEnv γ x acs ac ys mempty
cconsE cγ ce t
{-
case x :: List b of
Emp -> e
Emp :: tdc forall a. {v: List a | cons v === 0}
x :: xt List b
ys == binders []
-}
-------------------------------------------------------------------------------------
caseEnv :: CGEnv -> Var -> [AltCon] -> AltCon -> [Var] -> Maybe [Int] -> CG CGEnv
-------------------------------------------------------------------------------------
caseEnv γ x _ (DataAlt c) ys pIs = do
let (x' : ys') = F.symbol <$> (x:ys)
xt0 <- checkTyCon ("checkTycon cconsCase", x) γ <$> γ ??= x
let xt = shiftVV xt0 x'
tdc <- (γ ??= (dataConWorkId c) >>= refreshVV)
let (rtd,yts',_) = unfoldR tdc xt ys
yts <- projectTypes (typeclass (getConfig γ)) pIs yts'
let ys'' = F.symbol <$> filter (not . if allowTC then GM.isEmbeddedDictVar else GM.isEvVar) ys
let r1 = dataConReft c ys''
let r2 = dataConMsReft rtd ys''
let xt = (xt0 `F.meet` rtd) `strengthen` (uTop (r1 `F.meet` r2))
let cbs = safeZip "cconsCase" (x':ys') (xt0 : yts)
cγ' <- addBinders γ x' cbs
addBinders cγ' x' [(x', xt)]
where allowTC = typeclass (getConfig γ)
caseEnv γ x acs a _ _ = do
let x' = F.symbol x
xt' <- (`strengthen` uTop (altReft γ acs a)) <$> (γ ??= x)
cγ <- addBinders γ x' [(x', xt')]
return cγ
--------------------------------------------------------------------------------
-- | `projectTypes` masks (i.e. true's out) all types EXCEPT those
-- at given indices; it is used to simplify the environment used
-- when projecting out fields of single-ctor datatypes.
--------------------------------------------------------------------------------
projectTypes :: Bool -> Maybe [Int] -> [SpecType] -> CG [SpecType]
projectTypes _ Nothing ts = return ts
projectTypes allowTC (Just is) ts = mapM (projT is) (zip [0..] ts)
where
projT is (j, t)
| j `elem` is = return t
| otherwise = true allowTC t
altReft :: CGEnv -> [AltCon] -> AltCon -> F.Reft
altReft _ _ (LitAlt l) = literalFReft l
altReft γ acs DEFAULT = mconcat ([notLiteralReft l | LitAlt l <- acs] ++ [notDataConReft d | DataAlt d <- acs])
where
notLiteralReft = maybe mempty F.notExprReft . snd . literalConst (emb γ)
notDataConReft d | exactDC (getConfig γ)
= F.Reft (F.vv_, F.PNot (F.EApp (F.EVar $ makeDataConChecker d) (F.EVar F.vv_)))
| otherwise = mempty
altReft _ _ _ = panic Nothing "Constraint : altReft"
unfoldR :: SpecType -> SpecType -> [Var] -> (SpecType, [SpecType], SpecType)
unfoldR td (RApp _ ts rs _) ys = (t3, tvys ++ yts, ignoreOblig rt)
where
tbody = instantiatePvs (instantiateTys td ts) (reverse rs)
-- TODO: if we ever want to support applying implicits explicitly, will need to rejigger
((_,_,_,_),(ys0,_,yts',_), rt) = safeBkArrow (F.notracepp msg $ instantiateTys tbody tvs')
msg = "INST-TY: " ++ F.showpp (td, ts, tbody, ys, tvs')
yts'' = zipWith F.subst sus (yts'++[rt])
(t3,yts) = (last yts'', init yts'')
sus = F.mkSubst <$> (L.inits [(x, F.EVar y) | (x, y) <- zip ys0 ys'])
(αs, ys') = mapSnd (F.symbol <$>) $ L.partition isTyVar ys
tvs' :: [SpecType]
tvs' = rVar <$> αs
tvys = ofType . varType <$> αs
unfoldR _ _ _ = panic Nothing "Constraint.hs : unfoldR"
instantiateTys :: SpecType -> [SpecType] -> SpecType
instantiateTys = L.foldl' go
where
go (RAllT α tbody _) t = subsTyVar_meet' (ty_var_value α, t) tbody
go _ _ = panic Nothing "Constraint.instantiateTy"
instantiatePvs :: SpecType -> [SpecProp] -> SpecType
instantiatePvs = L.foldl' go
where
go (RAllP p tbody) r = replacePreds "instantiatePv" tbody [(p, r)]
go t _ = errorP "" ("Constraint.instantiatePvs: t = " ++ showpp t)
checkTyCon :: (Outputable a) => (String, a) -> CGEnv -> SpecType -> SpecType
checkTyCon _ _ t@(RApp _ _ _ _) = t
checkTyCon x g t = checkErr x g t
checkFun :: (Outputable a) => (String, a) -> CGEnv -> SpecType -> SpecType
checkFun _ _ t@(RFun _ _ _ _ _) = t
checkFun x g t = checkErr x g t
checkAll :: (Outputable a) => (String, a) -> CGEnv -> SpecType -> SpecType
checkAll _ _ t@(RAllT _ _ _) = t
checkAll x g t = checkErr x g t
checkErr :: (Outputable a) => (String, a) -> CGEnv -> SpecType -> SpecType
checkErr (msg, e) γ t = panic (Just sp) $ msg ++ GM.showPpr e ++ ", type: " ++ showpp t
where
sp = getLocation γ
varAnn :: CGEnv -> Var -> t -> Annot t
varAnn γ x t
| x `S.member` recs γ = AnnLoc (getSrcSpan x)
| otherwise = AnnUse t
-----------------------------------------------------------------------
-- | Helpers: Creating Fresh Refinement -------------------------------
-----------------------------------------------------------------------
freshPredRef :: CGEnv -> CoreExpr -> PVar RSort -> CG SpecProp
freshPredRef γ e (PV _ (PVProp τ) _ as)
= do t <- freshTy_type (typeclass (getConfig γ)) PredInstE e (toType False τ)
args <- mapM (\_ -> fresh) as
let targs = [(x, s) | (x, (s, y, z)) <- zip args as, (F.EVar y) == z ]
γ' <- foldM (+=) γ [("freshPredRef", x, ofRSort τ) | (x, τ) <- targs]
addW $ WfC γ' t
return $ RProp targs t
freshPredRef _ _ (PV _ PVHProp _ _)
= todo Nothing "EFFECTS:freshPredRef"
--------------------------------------------------------------------------------
-- | Helpers: Creating Refinement Types For Various Things ---------------------
--------------------------------------------------------------------------------
argType :: Type -> Maybe F.Expr
argType (LitTy (NumTyLit i))
= mkI i
argType (LitTy (StrTyLit s))
= mkS $ bytesFS s
argType (TyVarTy x)
= Just $ F.EVar $ F.symbol $ varName x
argType t
| F.symbol (GM.showPpr t) == anyTypeSymbol
= Just $ F.EVar anyTypeSymbol
argType _
= Nothing
argExpr :: CGEnv -> CoreExpr -> Maybe F.Expr
argExpr _ (Var v) = Just $ F.eVar v
argExpr γ (Lit c) = snd $ literalConst (emb γ) c
argExpr γ (Tick _ e) = argExpr γ e
argExpr γ (App e (Type _)) = argExpr γ e
argExpr _ _ = Nothing
-- NIKI TODO: merge arg/lam/fun-Expr
lamExpr :: CGEnv -> CoreExpr -> Maybe F.Expr
lamExpr _ (Var v) = Just $ F.eVar v
lamExpr γ (Lit c) = snd $ literalConst (emb γ) c
lamExpr γ (Tick _ e) = lamExpr γ e
lamExpr γ (App e (Type _)) = lamExpr γ e
lamExpr γ (App e1 e2) = case (lamExpr γ e1, lamExpr γ e2) of
(Just p1, Just p2) | not ((if allowTC then GM.isEmbeddedDictExpr else GM.isPredExpr) e2) -- (isClassPred $ exprType e2)
-> Just $ F.EApp p1 p2
(Just p1, Just _ ) -> Just p1
_ -> Nothing
where allowTC = typeclass (getConfig γ)
lamExpr γ (Let (NonRec x ex) e) = case (lamExpr γ ex, lamExpr γ e) of
(Just px, Just p) -> Just (p `F.subst1` (F.symbol x, px))
_ -> Nothing
lamExpr γ (Lam x e) = case lamExpr γ e of
Just p -> Just $ F.ELam (F.symbol x, typeSort (emb γ) $ Ghc.expandTypeSynonyms $ varType x) p
_ -> Nothing
lamExpr _ _ = Nothing
--------------------------------------------------------------------------------
(??=) :: (?callStack :: CallStack) => CGEnv -> Var -> CG SpecType
--------------------------------------------------------------------------------
γ ??= x = case M.lookup x' (lcb γ) of
Just e -> consE (γ -= x') e
Nothing -> refreshTy tx
where
x' = F.symbol x
tx = fromMaybe tt (γ ?= x')
tt = ofType $ varType x
--------------------------------------------------------------------------------
varRefType :: (?callStack :: CallStack) => CGEnv -> Var -> CG SpecType
--------------------------------------------------------------------------------
varRefType γ x = do
xt <- varRefType' γ x <$> (γ ??= x)
return xt -- F.tracepp (printf "varRefType x = [%s]" (showpp x))
varRefType' :: CGEnv -> Var -> SpecType -> SpecType
varRefType' γ x t'
| Just tys <- trec γ, Just tr <- M.lookup x' tys
= strengthen tr xr
| otherwise
= strengthen t' xr
where
xr = singletonReft x
x' = F.symbol x
strengthen
| higherOrderFlag γ
= strengthenMeet
| otherwise
= strengthenTop
-- | create singleton types for function application
makeSingleton :: CGEnv -> CoreExpr -> SpecType -> SpecType
makeSingleton γ e t
| higherOrderFlag γ, App f x <- simplify e
= case (funExpr γ f, argForAllExpr x) of
(Just f', Just x')
| not (if (typeclass (getConfig γ)) then GM.isEmbeddedDictExpr x else GM.isPredExpr x) -- (isClassPred $ exprType x)
-> strengthenMeet t (uTop $ F.exprReft (F.EApp f' x'))
(Just f', Just _)
-> strengthenMeet t (uTop $ F.exprReft f')
_ -> t
| rankNTypes (getConfig γ)
= case argExpr γ (simplify e) of
Just e' -> strengthenMeet t $ (uTop $ F.exprReft e')
_ -> t
| otherwise
= t
where
argForAllExpr (Var x)
| rankNTypes (getConfig γ)
, Just e <- M.lookup x (forallcb γ)
= Just e
argForAllExpr e
= argExpr γ e
funExpr :: CGEnv -> CoreExpr -> Maybe F.Expr
funExpr _ (Var v)
= Just $ F.EVar (F.symbol v)
funExpr γ (App e1 e2)
= case (funExpr γ e1, argExpr γ e2) of
(Just e1', Just e2') | not (if typeclass (getConfig γ) then GM.isEmbeddedDictExpr e2 else GM.isPredExpr e2) -- (isClassPred $ exprType e2)
-> Just (F.EApp e1' e2')
(Just e1', Just _)
-> Just e1'
_ -> Nothing
funExpr _ _
= Nothing
simplify :: CoreExpr -> CoreExpr
simplify (Tick _ e) = simplify e
simplify (App e (Type _)) = simplify e
simplify (App e1 e2) = App (simplify e1) (simplify e2)
simplify (Lam x e) | isTyVar x = simplify e
simplify e = e
singletonReft :: (F.Symbolic a) => a -> UReft F.Reft
singletonReft = uTop . F.symbolReft . F.symbol
-- | RJ: `nomeet` replaces `strengthenS` for `strengthen` in the definition
-- of `varRefType`. Why does `tests/neg/strata.hs` fail EVEN if I just replace
-- the `otherwise` case? The fq file holds no answers, both are sat.
strengthenTop :: (PPrint r, F.Reftable r) => RType c tv r -> r -> RType c tv r
strengthenTop (RApp c ts rs r) r' = RApp c ts rs $ F.meet r r'
strengthenTop (RVar a r) r' = RVar a $ F.meet r r'
strengthenTop (RFun b i t1 t2 r) r'= RFun b i t1 t2 $ F.meet r r'
strengthenTop (RAppTy t1 t2 r) r' = RAppTy t1 t2 $ F.meet r r'
strengthenTop (RAllT a t r) r' = RAllT a t $ F.meet r r'
strengthenTop t _ = t
-- TODO: this is almost identical to RT.strengthen! merge them!
strengthenMeet :: (PPrint r, F.Reftable r) => RType c tv r -> r -> RType c tv r
strengthenMeet (RApp c ts rs r) r' = RApp c ts rs (r `F.meet` r')
strengthenMeet (RVar a r) r' = RVar a (r `F.meet` r')
strengthenMeet (RFun b i t1 t2 r) r'= RFun b i t1 t2 (r `F.meet` r')
strengthenMeet (RAppTy t1 t2 r) r' = RAppTy t1 t2 (r `F.meet` r')
strengthenMeet (RAllT a t r) r' = RAllT a (strengthenMeet t r') (r `F.meet` r')
strengthenMeet t _ = t
-- topMeet :: (PPrint r, F.Reftable r) => r -> r -> r
-- topMeet r r' = r `F.meet` r'
--------------------------------------------------------------------------------
-- | Cleaner Signatures For Rec-bindings ---------------------------------------
--------------------------------------------------------------------------------
exprLoc :: CoreExpr -> Maybe SrcSpan
exprLoc (Tick tt _) = Just $ GM.tickSrcSpan tt
exprLoc (App e a) | isType a = exprLoc e
exprLoc _ = Nothing
isType :: Expr CoreBndr -> Bool
isType (Type _) = True
isType a = eqType (exprType a) predType
-- | @isGenericVar@ determines whether the @RTyVar@ has no class constraints
isGenericVar :: RTyVar -> SpecType -> Bool
isGenericVar α t = all (\(c, α') -> (α'/=α) || isGenericClass c ) (classConstrs t)
where
classConstrs t = [(c, ty_var_value α')
| (c, ts) <- tyClasses t
, t' <- ts
, α' <- freeTyVars t']
isGenericClass c = className c `elem` [ordClassName, eqClassName] -- , functorClassName, monadClassName]
-- instance MonadFail CG where
-- fail msg = panic Nothing msg
instance MonadFail Data.Functor.Identity.Identity where
fail msg = panic Nothing msg