liquidhaskell-0.1: Language/Haskell/Liquid/Bare.hs
{-# LANGUAGE MultiParamTypeClasses, NoMonomorphismRestriction, TypeSynonymInstances, FlexibleInstances, TupleSections, ScopedTypeVariables #-}
-- | This module contains the functions that convert /from/ descriptions of
-- symbols, names and types (over freshly parsed /bare/ Strings),
-- /to/ representations connected to GHC vars, names, and types.
-- The actual /representations/ of bare and real (refinement) types are all
-- in `RefType` -- they are different instances of `RType`
module Language.Haskell.Liquid.Bare (
GhcSpec (..)
, makeGhcSpec
-- , varSpecType
) where
import GHC hiding (lookupName, Located)
import Text.PrettyPrint.HughesPJ hiding (first)
import Var
import Name (getSrcSpan)
import Id (isConLikeId)
import PrelNames
import PrelInfo (wiredInThings)
import Type (expandTypeSynonyms, splitFunTy_maybe)
import DataCon (dataConImplicitIds, dataConWorkId)
import TyCon (tyConArity)
import HscMain
import TysWiredIn
import BasicTypes (TupleSort (..), Arity)
import TcRnDriver (tcRnLookupRdrName, tcRnLookupName)
import RdrName (setRdrNameSpace)
import OccName (tcName)
import Data.Char (isLower, isUpper)
import Text.Printf
import Data.Maybe (listToMaybe, fromMaybe, mapMaybe, catMaybes, isNothing)
import Control.Monad.State (put, get, gets, modify, State, evalState, evalStateT, execState, StateT)
import Data.Traversable (forM)
import Control.Applicative ((<$>), (<*>), (<|>))
import Control.Monad.Reader hiding (forM)
import Control.Monad.Error hiding (Error, forM)
import Control.Monad.Writer hiding (forM)
import qualified Control.Exception as Ex
-- import Data.Data hiding (TyCon, tyConName)
import Data.Bifunctor
import Data.Function (on)
import Language.Fixpoint.Misc
import Language.Fixpoint.Names (propConName, takeModuleNames, dropModuleNames)
import Language.Fixpoint.Types hiding (Predicate)
import Language.Fixpoint.Sort (checkSortedReftFull)
import Language.Haskell.Liquid.GhcMisc hiding (L)
import Language.Haskell.Liquid.Misc
import Language.Haskell.Liquid.Types
import Language.Haskell.Liquid.RefType
import Language.Haskell.Liquid.PredType hiding (unify)
import qualified Language.Haskell.Liquid.Measure as Ms
import qualified Data.List as L
import qualified Data.HashSet as S
import qualified Data.HashMap.Strict as M
import TypeRep
------------------------------------------------------------------
---------- Top Level Output --------------------------------------
------------------------------------------------------------------
makeGhcSpec :: Config -> ModName -> [Var] -> [Var] -> HscEnv
-> [(ModName,Ms.Spec BareType Symbol)]
-> IO GhcSpec
makeGhcSpec cfg name vars defVars env specs
= either Ex.throw return . checkGhcSpec =<< execBare (makeGhcSpec' cfg vars defVars specs) initEnv
where initEnv = BE name mempty mempty mempty env
checkMeasures emb env ms = concatMap (checkMeasure emb env) ms
checkMeasure :: M.HashMap TyCon FTycon-> SEnv SortedReft -> Ms.Measure SpecType DataCon -> [Error]
checkMeasure emb γ (Ms.M name@(Loc src n) sort body)
= [txerror e | Just e <- checkMBody γ emb name sort <$> body]
where
txerror = ErrMeas (sourcePosSrcSpan src) n
checkMBody γ emb name sort (Ms.Def s c bs body) = go γ' body
where
γ' = foldl (\γ (x, t) -> insertSEnv x t γ) γ xts
xts = zip bs $ rTypeSortedReft emb . subsTyVars_meet su <$> ts
ct = ofType $ dataConUserType c :: SpecType
su = unify tr (head $ snd3 $ bkArrowDeep sort)
(_, ts, tr) = bkArrow $ thd3 $ bkUniv ct
unify (RVar tv _) t = [(tv, toRSort t, t)]
unify (RApp _ ts _ _) (RApp _ ts' _ _) = concat $ zipWith unify ts ts'
unify _ _ = []
go γ (Ms.E e) = checkSortedReftFull γ e
go γ (Ms.P p) = checkSortedReftFull γ p
go γ (Ms.R s p) = checkSortedReftFull (insertSEnv s sty γ) p
sty = rTypeSortedReft emb (thd3 $ bkArrowDeep sort)
makeGhcSpec' :: Config -> [Var] -> [Var]
-> [(ModName,Ms.Spec BareType Symbol)]
-> BareM (GhcSpec, [Ms.Measure SpecType DataCon])
makeGhcSpec' cfg vars defVars specs
= do name <- gets modName
makeRTEnv (concat [map (mod,) $ Ms.aliases sp | (mod,sp) <- specs])
(concat [map (mod,) $ Ms.paliases sp | (mod,sp) <- specs])
(tcs, dcs) <- mconcat <$> mapM makeConTypes specs
let (tcs', dcs') = wiredTyDataCons
let tycons = tcs ++ tcs'
let datacons = concat dcs ++ dcs'
modify $ \be -> be { tcEnv = makeTyConInfo tycons }
measures <- mconcat <$> mapM makeMeasureSpec specs
let (cs, ms) = makeMeasureSpec' measures
sigs' <- mconcat <$> mapM (makeAssumeSpec cfg vars) specs
invs <- mconcat <$> mapM makeInvariants specs
embs <- mconcat <$> mapM makeTyConEmbeds specs
targetVars <- makeTargetVars name defVars $ binders cfg
lazies <- mconcat <$> mapM makeLazies specs
tcEnv <- gets tcEnv
let sigs = [ (x, (txRefSort tcEnv embs . txExpToBind) <$> t)
| (m, x, t) <- sigs' ]
let cs' = mapSnd (Loc dummyPos) <$> meetDataConSpec cs datacons
let ms' = [ (x, Loc l t) | (Loc l x, t) <- ms ] -- first val <$> ms
syms <- makeSymbols (vars ++ map fst cs') (map fst ms) (sigs ++ cs') ms'
let su = mkSubst [ (x, mkVarExpr v) | (x, v) <- syms]
let tx = subsFreeSymbols su
let txq = subsFreeSymbolsQual su
let syms' = [(varSymbol v, v) | (_, v) <- syms]
let decr' = mconcat $ map (makeHints defVars) specs
let lvars' = S.fromList $ mconcat $ [ makeLVars defVars (mod,spec)
| (mod,spec) <- specs
, mod == name
]
quals <- mconcat <$> mapM makeQualifiers specs
return $ (SP { tySigs = renameTyVars <$> tx sigs
, ctor = tx cs'
, meas = tx (ms' ++ varMeasures vars)
, invariants = invs
, dconsP = datacons
, tconsP = tycons
, freeSyms = syms'
, tcEmbeds = embs
, qualifiers = txq quals
, decr = decr'
, lvars = lvars'
, lazy = lazies
, tgtVars = targetVars
, config = cfg
}
, subst su <$> M.elems $ Ms.measMap measures)
--- Refinement Type Aliases
makeRTEnv rts pts = do initRTEnv
makeRPAliases pts
makeRTAliases rts
where initRTEnv = do forM_ rts $ \(mod,rta) -> setRTAlias (rtName rta) $ Left (mod,rta)
forM_ pts $ \(mod,pta) -> setRPAlias (rtName pta) $ Left (mod,pta)
makeRTAliases xts = mapM_ expBody xts
where expBody (mod,xt) = inModule mod $ do
body <- withVArgs (rtVArgs xt) $ expandRTAlias $ rtBody xt
setRTAlias (rtName xt)
$ Right $ mapRTAVars stringRTyVar $ xt { rtBody = body }
makeRPAliases xts = mapM_ expBody xts
where expBody (mod,xt) = inModule mod $ do
env <- gets $ predAliases . rtEnv
body <- withVArgs (rtVArgs xt) $ expandRPAliasE $ rtBody xt
setRPAlias (rtName xt) $ Right $ xt { rtBody = body }
-- | Using the Alias Environment to Expand Definitions
expandRTAliasMeasure m
= do eqns <- sequence $ expandRTAliasDef <$> (Ms.eqns m)
return $ m { Ms.sort = generalize (Ms.sort m)
, Ms.eqns = eqns }
expandRTAliasDef :: Ms.Def Symbol -> BareM (Ms.Def Symbol)
expandRTAliasDef d
= do env <- gets rtEnv
body <- expandRTAliasBody env $ Ms.body d
return $ d { Ms.body = body }
expandRTAliasBody :: RTEnv -> Ms.Body -> BareM Ms.Body
expandRTAliasBody env (Ms.P p) = Ms.P <$> (expPAlias p)
expandRTAliasBody env (Ms.R x p) = Ms.R x <$> (expPAlias p)
expandRTAliasBody _ (Ms.E e) = Ms.E <$> resolve e
expPAlias :: Pred -> BareM Pred
expPAlias = expandPAlias []
expandRTAlias :: BareType -> BareM SpecType
expandRTAlias bt = expType =<< expReft bt
where
expReft = mapReftM (txPredReft expPred)
expType = expandAlias []
expPred = expandPAlias []
txPredReft :: (Pred -> BareM Pred) -> RReft -> BareM RReft
txPredReft f (U r p) = (`U` p) <$> txPredReft' f r
where
txPredReft' f (Reft (v, ras)) = Reft . (v,) <$> mapM (txPredRefa f) ras
txPredRefa f (RConc p) = RConc <$> f p
txPredRefa _ z = return z
-- | Using the Alias Environment to Expand Definitions
expandRPAliasE = expandPAlias []
expandRTAliasE = expandAlias []
expandAlias s = go s
where
go s (RApp c ts rs r)
| c `elem` s = errorstar $ "Cyclic Reftype Alias Definition: " ++ show (c:s)
| otherwise = do
env <- gets (typeAliases.rtEnv)
case M.lookup c env of
Just (Left (mod,rtb)) -> do
st <- inModule mod $ withVArgs (rtVArgs rtb) $ expandAlias (c:s) $ rtBody rtb
let rts = mapRTAVars stringRTyVar $ rtb { rtBody = st }
setRTAlias c $ Right rts
r' <- resolve r
expandRTApp s rts ts r'
Just (Right rts) -> do
r' <- resolve r
withVArgs (rtVArgs rts) $ expandRTApp s rts ts r'
Nothing | isList c && length ts == 1 -> do
tyi <- tcEnv <$> get
r' <- resolve r
liftM2 (bareTCApp tyi r' listTyCon) (mapM (go' s) rs) (mapM (go s) ts)
| isTuple c -> do
tyi <- tcEnv <$> get
r' <- resolve r
let tc = tupleTyCon BoxedTuple (length ts)
liftM2 (bareTCApp tyi r' tc) (mapM (go' s) rs) (mapM (go s) ts)
| otherwise -> do
tyi <- tcEnv <$> get
r' <- resolve r
liftM3 (bareTCApp tyi r') (lookupGhcTyCon c) (mapM (go' s) rs) (mapM (go s) ts)
go s (RVar a r) = RVar (stringRTyVar a) <$> resolve r
go s (RFun x t t' r) = rFun x <$> go s t <*> go s t'
go s (RAppTy t t' r) = rAppTy <$> go s t <*> go s t'
go s (RAllE x t1 t2) = liftM2 (RAllE x) (go s t1) (go s t2)
go s (REx x t1 t2) = liftM2 (REx x) (go s t1) (go s t2)
go s (RAllT a t) = RAllT (stringRTyVar a) <$> go s t
go s (RAllP a t) = RAllP <$> ofBPVar a <*> go s t
go s (RCls c ts) = RCls <$> lookupGhcClass c <*> (mapM (go s) ts)
go _ (ROth s) = return $ ROth s
go _ (RExprArg e) = return $ RExprArg e
go' s (RMono ss r) = RMono <$> mapM ofSyms ss <*> resolve r
go' s (RPoly ss t) = RPoly <$> mapM ofSyms ss <*> go s t
expandRTApp s rta args r
| length args == (length αs) + (length εs)
= do args' <- mapM (expandAlias s) args
let ts = take (length αs) args'
αts = zipWith (\α t -> (α, toRSort t, t)) αs ts
return $ subst su . (`strengthen` r) . subsTyVars_meet αts $ rtBody rta
| otherwise
= errortext $ (text "Malformed Type-Alias Application" $+$ text msg)
where
su = mkSubst $ zip (stringSymbol . showpp <$> εs) es
αs = rtTArgs rta
εs = rtVArgs rta
msg = rtName rta ++ " " ++ join (map showpp args)
es_ = drop (length αs) args
es = map (exprArg msg) es_
-- | exprArg converts a tyVar to an exprVar because parser cannot tell
-- HORRIBLE HACK To allow treating upperCase X as value variables X
-- e.g. type Matrix a Row Col = List (List a Row) Col
exprArg _ (RExprArg e)
= e
exprArg _ (RVar x _)
= EVar (stringSymbol $ showpp x)
exprArg _ (RApp x [] [] _)
= EVar (stringSymbol $ showpp x)
exprArg msg (RApp f ts [] _)
= EApp (stringSymbol $ showpp f) (exprArg msg <$> ts)
exprArg msg (RAppTy (RVar f _) t _)
= EApp (stringSymbol $ showpp f) [exprArg msg t]
exprArg msg z
= errorstar $ printf "Unexpected expression parameter: %s in %s" (show z) msg
expandPAlias :: [Symbol] -> Pred -> BareM Pred
expandPAlias s = go s
where
go s p@(PBexp (EApp f es))
| f `elem` s = errorstar $ "Cyclic Predicate Alias Definition: " ++ show (f:s)
| otherwise = do
env <- gets (predAliases.rtEnv)
case M.lookup (symbolString f) env of
Just (Left (mod,rp)) -> do
body <- inModule mod $ withVArgs (rtVArgs rp) $ expandPAlias (f:s) $ rtBody rp
let rp' = rp { rtBody = body }
setRPAlias (show f) $ Right $ rp'
expandRPApp (f:s) rp' <$> mapM resolve es
Just (Right rp) ->
withVArgs (rtVArgs rp) (expandRPApp (f:s) rp <$> mapM resolve es)
Nothing -> fmap PBexp (EApp <$> resolve f <*> mapM resolve es)
go s (PAnd ps) = PAnd <$> (mapM (go s) ps)
go s (POr ps) = POr <$> (mapM (go s) ps)
go s (PNot p) = PNot <$> (go s p)
go s (PImp p q) = PImp <$> (go s p) <*> (go s q)
go s (PIff p q) = PIff <$> (go s p) <*> (go s q)
go s (PAll xts p) = PAll xts <$> (go s p)
go _ p = resolve p
expandRPApp s rp es
= let su = mkSubst $ safeZip msg (rtVArgs rp) es
msg = "expandRPApp: " ++ show (EApp (symbol $ rtName rp) es)
in subst su $ rtBody rp
makeQualifiers (mod,spec) = inModule mod mkQuals
where
mkQuals = mapM resolve $ Ms.qualifiers spec
makeHints vs (_,spec) = makeHints' vs $ Ms.decr spec
makeLVars vs (_,spec) = fst <$> (makeHints' vs $ [(v, ()) | v <- Ms.lvars spec])
makeHints' :: [Var] -> [(LocSymbol, a)] -> [(Var, a)]
makeHints' vs = concatMap go
where lvs = M.map L.sort $ group [(varSymbol v, locVar v) | v <- vs]
varSymbol = stringSymbol . dropModuleNames . showPpr
locVar v = (getSourcePos v, v)
go (s, ns) = case M.lookup (val s) lvs of
Just lvs -> (, ns) <$> varsAfter s lvs
Nothing -> errorstar $ msg s
msg s = printf "%s: Hint for Undefined Var %s"
(show (loc s)) (show (val s))
varsAfter s lvs
| eqList (fst <$> lvs)
= snd <$> lvs
| otherwise
= map snd $ takeEqLoc $ dropLeLoc lvs
where takeEqLoc xs@((l, _):_) = L.takeWhile ((l==) . fst) xs
takeEqLoc [] = []
dropLeLoc = L.dropWhile ((loc s >) . fst)
eqList [] = True
eqList (x:xs) = all (==x) xs
txRefSort env embs = mapBot (addSymSort embs env)
addSymSort embs tcenv (RApp rc@(RTyCon c _ _) ts rs r)
= RApp rc ts (addSymSortRef <$> zip ps rs) r
where ps = rTyConPs $ appRTyCon embs tcenv rc ts
addSymSort _ _ t
= t
addSymSortRef (p, RPoly s (RVar v r)) | isDummy v
= RPoly (safeZip "addRefSortPoly" (fst <$> s) (fst3 <$> pargs p)) t
where t = ofRSort (ptype p) `strengthen` r
addSymSortRef (p, RPoly s t)
= RPoly (safeZip "addRefSortPoly" (fst <$> s) (fst3 <$> pargs p)) t
addSymSortRef (p, RMono s r@(U _ (Pr [up])))
= RMono (safeZip "addRefSortMono" (snd3 <$> pargs up) (fst3 <$> pargs p)) r
addSymSortRef (p, RMono s t)
= RMono s t
varMeasures vars = [ (varSymbol v, varSpecType v)
| v <- vars
, isDataConWorkId v
, isSimpleType $ varType v
]
varSpecType v = Loc (getSourcePos v) (ofType $ varType v)
isSimpleType t = null tvs && isNothing (splitFunTy_maybe tb)
where (tvs, tb) = splitForAllTys t
-------------------------------------------------------------------------------
-- Renaming Type Variables in Haskell Signatures ------------------------------
-------------------------------------------------------------------------------
-- This throws an exception if there is a mismatch
-- renameTyVars :: (Var, SpecType) -> (Var, SpecType)
renameTyVars (x, lt@(Loc l t))
| length as == length αs = (x, Loc l $ mkUnivs (rTyVar <$> αs) [] t')
| otherwise = Ex.throw $ err
where
t' = subts su (mkUnivs [] ps tbody)
su = [(y, rTyVar x) | (x, y) <- tyvsmap]
tyvsmap = vmap $ execState (mapTyVars τbody tbody) initvmap
initvmap = initMapSt αs as err
(αs, τbody) = splitForAllTys $ expandTypeSynonyms $ varType x
(as, ps, tbody) = bkUniv t
err = errTypeMismatch x lt
data MapTyVarST = MTVST { τvars :: S.HashSet Var
, tvars :: S.HashSet RTyVar
, vmap :: [(Var, RTyVar)]
, errmsg :: Error
}
initMapSt α a = MTVST (S.fromList α) (S.fromList a) []
mapTyVars :: (PPrint r, Reftable r) => Type -> RRType r -> State MapTyVarST ()
mapTyVars τ (RAllT a t)
= do modify $ \s -> s{ tvars = S.delete a (tvars s) }
mapTyVars τ t
mapTyVars (ForAllTy α τ) t
= do modify $ \s -> s{ τvars = S.delete α (τvars s) }
mapTyVars τ t
mapTyVars (FunTy τ τ') (RFun _ t t' _)
= mapTyVars τ t >> mapTyVars τ' t'
mapTyVars (TyConApp _ τs) (RApp _ ts _ _)
= zipWithM_ mapTyVars τs ts
mapTyVars (TyVarTy α) (RVar a _)
= modify $ \s -> mapTyRVar α a s
mapTyVars τ (RAllP _ t)
= mapTyVars τ t
mapTyVars τ (RCls _ ts)
= return ()
mapTyVars τ (RAllE _ _ t)
= mapTyVars τ t
mapTyVars τ (REx _ _ t)
= mapTyVars τ t
mapTyVars τ (RExprArg _)
= return ()
mapTyVars (AppTy τ τ') (RAppTy t t' _)
= do mapTyVars τ t
mapTyVars τ' t'
mapTyVars τ t
= Ex.throw =<< errmsg <$> get
-- errorstar $ "Bare.mapTyVars : " ++ err
mapTyRVar α a s@(MTVST αs as αas err)
| (α `S.member` αs) && (a `S.member` as)
= MTVST (S.delete α αs) (S.delete a as) ((α, a):αas) err
| (not (α `S.member` αs)) && (not (a `S.member` as))
= s
| otherwise
= Ex.throw err -- errorstar err
mkVarExpr v
| isDataConWorkId v && not (null tvs) && isNothing tfun
= EApp (dataConSymbol (idDataCon v)) []
| otherwise
= EVar $ varSymbol v
where t = varType v
(tvs, tbase) = splitForAllTys t
tfun = splitFunTy_maybe tbase
subsFreeSymbols su = tx
where
tx = fmap $ mapSnd $ subst su
subsFreeSymbolsQual su = tx
where
tx = fmap $ mapBody $ subst su
mapBody f (Q n p b) = Q n p (f b)
-- meetDataConSpec :: [(Var, SpecType)] -> [(DataCon, DataConP)] -> [(Var, SpecType)]
meetDataConSpec xts dcs = M.toList $ L.foldl' upd dcm xts
where
dcm = M.fromList $ dataConSpec dcs
upd dcm (x, t) = M.insert x (maybe t (meetPad t) (M.lookup x dcm)) dcm
strengthen (x,t) = (x, maybe t (meetPad t) (M.lookup x dcm))
-- dataConSpec :: [(DataCon, DataConP)] -> [(Var, SpecType)]
dataConSpec :: [(DataCon, DataConP)]-> [(Var, (RType Class RTyCon RTyVar RReft))]
dataConSpec dcs = concatMap mkDataConIdsTy [(dc, dataConPSpecType dc t) | (dc, t) <- dcs]
meetPad t1 t2 = -- traceShow ("meetPad: " ++ msg) $
case (bkUniv t1, bkUniv t2) of
((_, π1s, _), (α2s, [], t2')) -> meet t1 (mkUnivs α2s π1s t2')
((α1s, [], t1'), (_, π2s, _)) -> meet (mkUnivs α1s π2s t1') t2
_ -> errorstar $ "meetPad: " ++ msg
where msg = "\nt1 = " ++ showpp t1 ++ "\nt2 = " ++ showpp t2
------------------------------------------------------------------
---------- Error-Reader-IO For Bare Transformation ---------------
------------------------------------------------------------------
type BareM a = WriterT [Warn] (ErrorT String (StateT BareEnv IO)) a
type Warn = String
data BareEnv = BE { modName :: !ModName
, tcEnv :: !(M.HashMap TyCon RTyCon)
, rtEnv :: !RTEnv
, varEnv :: ![(Symbol,Var)]
, hscEnv :: HscEnv }
setModule m b = b { modName = m }
inModule m act = do
old <- gets modName
modify $ setModule m
res <- act
modify $ setModule old
return res
withVArgs vs act = do
old <- gets rtEnv
mapM (mkExprAlias . showpp) vs
res <- act
modify $ \be -> be { rtEnv = old }
return res
addSym x = modify $ \be -> be { varEnv = (varEnv be) `L.union` [x] }
mkExprAlias v
= setRTAlias v (Right (RTA v [] [] (RExprArg (EVar $ symbol v)) dummyPos))
setRTAlias s a =
modify $ \b -> b { rtEnv = mapRT (M.insert s a) $ rtEnv b }
setRPAlias s a =
modify $ \b -> b { rtEnv = mapRP (M.insert s a) $ rtEnv b }
execBare :: BareM a -> BareEnv -> IO a
execBare act benv =
do z <- evalStateT (runErrorT (runWriterT act)) benv
case z of
Left s -> errorstar $ "execBare:\n " ++ s
Right (x, ws) -> do forM_ ws $ putStrLn . ("WARNING: " ++)
return x
wrapErr msg f x = yesStack
where
noStack = f x
yesStack = noStack `catchError` \e -> throwError $ str e
str e = printf "Bare Error %s: \nThrows Exception: %s\n" msg e
------------------------------------------------------------------
------------------- API: Bare Refinement Types -------------------
------------------------------------------------------------------
makeMeasureSpec (mod,spec) = inModule mod mkSpec
where
mkSpec = mkMeasureDCon =<< wrapErr "mkMeasureSort" mkMeasureSort =<< m
m = Ms.mkMSpec <$> (mapM expandRTAliasMeasure $ Ms.measures spec)
makeMeasureSpec' = mapFst (mapSnd uRType <$>) . Ms.dataConTypes . first (mapReft ur_reft)
makeTargetVars :: ModName -> [Var] -> [String] -> BareM [Var]
makeTargetVars name vs ss = do
env <- gets hscEnv
ns <- liftIO $ catMaybes <$> mapM (lookupName env name) (map prefix ss)
return $ filter ((`elem` ns) . varName) vs
where
prefix s = getModString name ++ "." ++ s
makeAssumeSpec cfg vs (mod,spec)
= inModule mod $ makeAssumeSpec' cfg vs $ Ms.sigs spec
makeAssumeSpec' :: Config -> [Var] -> [(LocSymbol, BareType)]
-> BareM [(ModName, Var, Located SpecType)]
makeAssumeSpec' cfg vs xbs
= do vbs <- map (joinVar vs) <$> lookupIds xbs
env@(BE { modName = mod}) <- get
when (not $ noCheckUnknown cfg) $
checkDefAsserts env vbs xbs
map (addFst3 mod) <$> mapM mkVarSpec vbs
-- the Vars we lookup in GHC don't always have the same tyvars as the Vars
-- we're given, so return the original var when possible.
-- see tests/pos/ResolvePred.hs for an example
joinVar vs (v,s,t) = case L.find ((== showPpr v) . showPpr) vs of
Just v' -> (v',s,t)
Nothing -> (v,s,t)
lookupIds xs = mapM lookup xs
where
lookup (s, t) = (,s,t) <$> lookupGhcVar (ss s)
ss = symbolString . symbol
checkDefAsserts :: BareEnv -> [(Var, LocSymbol, BareType)] -> [(LocSymbol, BareType)] -> BareM ()
checkDefAsserts env vbs xbs = applyNonNull (return ()) grumble undefSigs
where
undefSigs = [x | (x, _) <- assertSigs, not (x `S.member` definedSigs)]
assertSigs = filter isTarget xbs
definedSigs = S.fromList $ snd3 <$> vbs
grumble xs = mapM_ (warn . berrUnknownVar) xs -- [berrUnknownVar (loc x) (val x) | x <- xs]
moduleName = getModString $ modName env
isTarget = L.isPrefixOf moduleName . symbolStringRaw . val . fst
symbolStringRaw = stripParens . symbolString
-- grumble = {- throwError -} warn . render . vcat . fmap errorMsg
-- errorMsg = (text "Specification for unknown variable:" <+>) . locatedSymbolText
warn x = tell [x]
mkVarSpec :: (Var, LocSymbol, BareType) -> BareM (Var, Located SpecType)
mkVarSpec (v, Loc l _, b) = ((v, ) . (Loc l) . generalize) <$> mkSpecType msg b
where
msg = berrVarSpec l v b
showTopLevelVars vs =
forM vs $ \v ->
if isExportedId v
then donePhase Loud ("Exported: " ++ showPpr v)
else return ()
----------------------------------------------------------------------
makeTyConEmbeds (mod,spec)
= inModule mod $ makeTyConEmbeds' $ Ms.embeds spec
makeTyConEmbeds' :: TCEmb (Located String) -> BareM (TCEmb TyCon)
makeTyConEmbeds' z = M.fromList <$> mapM tx (M.toList z)
where
tx (c, y) = (, y) <$> lookupGhcTyCon' c -- wrapErr () (lookupGhcTyCon (val c))
lookupGhcTyCon' c = wrapErr msg lookupGhcTyCon (val c)
where
msg :: String = berrUnknownTyCon c
makeLazies (mod,spec)
= inModule mod $ makeLazies' $ Ms.lazy spec
makeLazies' :: S.HashSet Symbol -> BareM (S.HashSet Var)
makeLazies' s = S.fromList <$> (fmap fst3 <$> lookupIds xxs)
where xs = S.toList s
xxs = zip xs xs
makeInvariants (mod,spec)
= inModule mod $ makeInvariants' $ Ms.invariants spec
makeInvariants' :: [Located BareType] -> BareM [Located SpecType]
makeInvariants' ts = mapM mkI ts
where
mkI (Loc l t) = (Loc l) . generalize <$> mkSpecType (berrInvariant l t) t
mkSpecType msg t = mkSpecType' msg (snd3 $ bkUniv t) t
mkSpecType' :: String -> [PVar BSort] -> BareType -> BareM SpecType
mkSpecType' msg πs = expandRTAlias . txParams subvUReft (uPVar <$> πs)
makeSymbols vs xs' xts yts = mkxvs
where
xs'' = val <$> xs'
zs = (concatMap freeSymbols ((snd <$> xts))) `sortDiff` xs''
zs' = (concatMap freeSymbols ((snd <$> yts))) `sortDiff` xs''
xs = sortNub $ zs ++ zs'
mkxvs = do
svs <- gets varEnv
return [(x,v') | (x,v) <- svs, x `elem` xs, let (v',_,_) = joinVar vs (v,x,x)]
freeSymbols ty = sortNub $ concat $ efoldReft (\_ _ -> []) (\ _ -> ()) f emptySEnv [] (val ty)
where
f γ _ r xs = let Reft (v, _) = toReft r in
[ x | x <- syms r, x /= v, not (x `memberSEnv` γ)] : xs
-----------------------------------------------------------------
------ Querying GHC for Id, Type, Class, Con etc. ---------------
-----------------------------------------------------------------
class GhcLookup a where
lookupName :: HscEnv -> ModName -> a -> IO (Maybe Name)
candidates :: a -> [a]
pp :: a -> String
instance GhcLookup String where
lookupName = stringLookup
candidates x = [x]
pp x = x
instance GhcLookup Name where
lookupName _ _ = return . Just
candidates x = [x]
pp = showPpr
lookupGhcThing :: (GhcLookup a) => String -> (TyThing -> Maybe b) -> a -> BareM b
lookupGhcThing name f x
= do zs <- catMaybes <$> mapM (lookupGhcThing' name f) (candidates x)
case zs of
x:_ -> return x
_ -> throwError $ "lookupGhcThing unknown " ++ name ++ " : " ++ (pp x)
lookupGhcThing' :: (GhcLookup a) => String -> (TyThing -> Maybe b) -> a -> BareM (Maybe b)
lookupGhcThing' _ f x
= do (BE mod _ _ _ env) <- get
z <- liftIO $ lookupName env mod x
case z of
Nothing -> return Nothing
Just n -> liftIO $ liftM (join . (f <$>) . snd) (tcRnLookupName env n)
stringLookup :: HscEnv -> ModName -> String -> IO (Maybe Name)
stringLookup env mod k
| k `M.member` wiredIn
= return $ M.lookup k wiredIn
| otherwise
= stringLookupEnv env mod k
stringLookupEnv env mod s
| isSrcImport mod
= do let modName = getModName mod
L _ rn <- hscParseIdentifier env s
res <- lookupRdrName env modName rn
case res of
Just _ -> return res
Nothing -> lookupRdrName env modName (setRdrNameSpace rn tcName)
| otherwise
= do L _ rn <- hscParseIdentifier env s
(_, lookupres) <- tcRnLookupRdrName env rn
case lookupres of
Just (n:_) -> return (Just n)
_ -> return Nothing
lookupGhcVar :: GhcLookup a => a -> BareM Var
lookupGhcVar x
-- It's possible that we have already resolved the Name we are
-- looking for, but have had to turn it back into a String, e.g. to
-- be used in an Expr, as in {v:Ordering | v = EQ}. In this case,
-- the fully-qualified Name (GHC.Types.EQ) will likely not be in
-- scope, so we store our own mapping of fully-qualified Names to
-- Vars and prefer pulling Vars from it.
= do env <- gets varEnv
case L.lookup (symbol $ pp x) env of
Nothing -> lookupGhcThing "Var" fv x
Just v -> return v
where
fv (AnId x) = Just x
fv (ADataCon x) = Just $ dataConWorkId x
fv _ = Nothing
lookupGhcTyCon :: GhcLookup a => a -> BareM TyCon
lookupGhcTyCon s = (lookupGhcThing "TyCon" ftc s) `catchError` (tryPropTyCon s)
where
ftc (ATyCon x) = Just x
ftc (ADataCon x) = Just $ dataConTyCon x
ftc _ = Nothing
tryPropTyCon s e
| pp s == propConName = return propTyCon
| otherwise = throwError e
lookupGhcClass = lookupGhcThing "Class" ftc
where
ftc (ATyCon x) = tyConClass_maybe x
ftc _ = Nothing
lookupGhcDataCon dc = case isTupleDC dc of
Just n -> return $ tupleCon BoxedTuple n
Nothing -> lookupGhcDataCon' dc
isTupleDC zs@('(':',':_) = Just $ length zs - 1
isTupleDC _ = Nothing
lookupGhcDataCon' = lookupGhcThing "DataCon" fdc
where
fdc (ADataCon x) = Just x
fdc _ = Nothing
wiredIn :: M.HashMap String Name
wiredIn = M.fromList $ {- tracePpr "wiredIn: " $ -} special ++ wiredIns
where wiredIns = [ (showPpr n, n) | thing <- wiredInThings, let n = getName thing ]
special = [ ("GHC.Integer.smallInteger", smallIntegerName)
, ("GHC.Num.fromInteger" , fromIntegerName ) ]
fixpointPrims = ["Pred", "Prop", "List", "Set_Set", "Set_sng", "Set_cup", "Set_cap"
,"Set_dif", "Set_emp", "Set_mem", "Set_sub", "VV"]
class Resolvable a where
resolve :: a -> BareM a
instance Resolvable Qualifier where
resolve (Q n ps b) = Q n <$> mapM (secondM resolve) ps <*> resolve b
instance Resolvable Pred where
resolve (PAnd ps) = PAnd <$> mapM resolve ps
resolve (POr ps) = POr <$> mapM resolve ps
resolve (PNot p) = PNot <$> resolve p
resolve (PImp p q) = PImp <$> resolve p <*> resolve q
resolve (PIff p q) = PIff <$> resolve p <*> resolve q
resolve (PBexp b) = PBexp <$> resolve b
resolve (PAtom r e1 e2) = PAtom r <$> resolve e1 <*> resolve e2
resolve (PAll vs p) = PAll <$> mapM (secondM resolve) vs
<*> resolve p
resolve p = return p
instance Resolvable Expr where
resolve (EVar s) = EVar <$> resolve s
resolve (EApp s es) = EApp <$> resolve s <*> es'
where es' = mapM resolve es
resolve (EBin o e1 e2) = EBin o <$> resolve e1 <*> resolve e2
resolve (EIte p e1 e2) = EIte <$> resolve p <*> resolve e1 <*> resolve e2
resolve (ECst x s) = ECst <$> resolve x <*> resolve s
resolve x = return x
instance Resolvable Symbol where
resolve (S s)
| s `elem` fixpointPrims = return (S s)
| otherwise = do env <- gets (typeAliases.rtEnv)
case M.lookup s env of
Nothing | isCon s
-> do v <- lookupGhcVar s
let qs = symbol $ showPpr v
addSym (qs,v)
return qs
_ -> return (S s)
instance Resolvable Sort where
resolve FInt = return FInt
resolve FNum = return FNum
resolve s@(FObj _) = return s --FObj . S <$> lookupName env m s
resolve s@(FVar _) = return s
resolve (FFunc i ss) = FFunc i <$> mapM resolve ss
resolve (FApp tc ss)
| tcs `elem` fixpointPrims = FApp tc <$> ss'
| otherwise = FApp <$> (stringFTycon.showPpr <$> lookupGhcTyCon tcs)
<*> ss'
where tcs = fTyconString tc
ss' = mapM resolve ss
instance Resolvable (UReft Reft) where
resolve (U r p) = U <$> resolve r <*> resolve p
instance Resolvable Reft where
resolve (Reft (s, ras)) = Reft . (s,) <$> mapM resolveRefa ras
where
resolveRefa (RConc p) = RConc <$> resolve p
resolveRefa kv = return kv
instance Resolvable Predicate where
resolve (Pr pvs) = Pr <$> mapM resolve pvs
instance (Resolvable t) => Resolvable (PVar t) where
resolve (PV n t as) = PV n t <$> mapM (third3M resolve) as
instance Resolvable () where
resolve () = return ()
isCon (c:cs) = isUpper c
isCon [] = False
--------------------------------------------------------------------
------ Predicate Types for WiredIns --------------------------------
--------------------------------------------------------------------
maxArity :: Arity
maxArity = 7
wiredTyDataCons :: ([(TyCon, TyConP)] , [(DataCon, DataConP)])
wiredTyDataCons = (concat tcs, concat dcs)
where
(tcs, dcs) = unzip l
l = [listTyDataCons] ++ map tupleTyDataCons [1..maxArity]
listTyDataCons :: ([(TyCon, TyConP)] , [(DataCon, DataConP)])
listTyDataCons = ( [(c, TyConP [(RTV tyv)] [p] [0] [] (Just fsize))]
, [(nilDataCon , DataConP [(RTV tyv)] [p] [] lt)
, (consDataCon, DataConP [(RTV tyv)] [p] cargs lt)])
where c = listTyCon
[tyv] = tyConTyVars c
t = {- TyVarTy -} rVar tyv :: RSort
fld = stringSymbol "fld"
x = stringSymbol "x"
xs = stringSymbol "xs"
p = PV (stringSymbol "p") t [(t, fld, EVar fld)]
px = (pdVarReft $ PV (stringSymbol "p") t [(t, fld, EVar x)])
lt = rApp c [xt] [RMono [] $ pdVarReft p] top
xt = rVar tyv
xst = rApp c [RVar (RTV tyv) px] [RMono [] $ pdVarReft p] top
cargs = [(xs, xst), (x, xt)]
fsize = \x -> EApp (S "len") [EVar x]
tupleTyDataCons :: Int -> ([(TyCon, TyConP)] , [(DataCon, DataConP)])
tupleTyDataCons n = ( [(c, TyConP (RTV <$> tyvs) ps [0..(n-2)] [] Nothing)]
, [(dc, DataConP (RTV <$> tyvs) ps cargs lt)])
where c = tupleTyCon BoxedTuple n
dc = tupleCon BoxedTuple n
tyvs@(tv:tvs) = tyConTyVars c
(ta:ts) = (rVar <$> tyvs) :: [RSort]
flds = mks "fld"
fld = stringSymbol "fld"
x1:xs = mks "x"
-- y = stringSymbol "y"
ps = mkps pnames (ta:ts) ((fld, EVar fld):(zip flds (EVar <$>flds)))
ups = uPVar <$> ps
pxs = mkps pnames (ta:ts) ((fld, EVar x1):(zip flds (EVar <$> xs)))
lt = rApp c (rVar <$> tyvs) (RMono [] . pdVarReft <$> ups) top
xts = zipWith (\v p -> RVar (RTV v) (pdVarReft p)) tvs pxs
cargs = reverse $ (x1, rVar tv) : (zip xs xts)
pnames = mks_ "p"
mks x = (\i -> stringSymbol (x++ show i)) <$> [1..n]
mks_ x = (\i -> (x++ show i)) <$> [2..n]
pdVarReft = U top . pdVar
mkps ns (t:ts) ((f,x):fxs) = reverse $ mkps_ (stringSymbol <$> ns) ts fxs [(t, f, x)] []
mkps _ _ _ = error "Bare : mkps"
mkps_ [] _ _ _ ps = ps
mkps_ (n:ns) (t:ts) ((f, x):xs) args ps
= mkps_ ns ts xs (a:args) (p:ps)
where p = PV n t args
a = (t, f, x)
mkps_ _ _ _ _ _ = error "Bare : mkps_"
------------------------------------------------------------------------
----------------- Transforming Raw Strings using GHC Env ---------------
------------------------------------------------------------------------
-- makeRTyConPs :: Reftable r => String -> M.HashMap TyCon RTyCon -> [RPVar] -> RRType r -> RRType r
-- makeRTyConPs msg tyi πs t@(RApp c ts rs r)
-- | null $ rTyConPs c
-- = expandRApp tyi t
-- | otherwise
-- = RApp c {rTyConPs = findπ πs <$> rTyConPs c} ts rs r
-- -- need type application????
-- where findπ πs π = findWithDefaultL (== π) πs (emsg π)
-- emsg π = errorstar $ "Bare: out of scope predicate " ++ msg ++ " " ++ show π
-- -- throwError $ "Bare: out of scope predicate" ++ show π
--
--
-- makeRTyConPs _ _ _ t = t
ofBareType' :: (PPrint r, Reftable r) => String -> BRType r -> BareM (RRType r)
ofBareType' msg = wrapErr msg ofBareType
ofBareType :: (PPrint r, Reftable r) => BRType r -> BareM (RRType r)
ofBareType (RVar a r)
= return $ RVar (stringRTyVar a) r
ofBareType (RFun x t1 t2 _)
= liftM2 (rFun x) (ofBareType t1) (ofBareType t2)
ofBareType (RAppTy t1 t2 _)
= liftM2 rAppTy (ofBareType t1) (ofBareType t2)
ofBareType (RAllE x t1 t2)
= liftM2 (RAllE x) (ofBareType t1) (ofBareType t2)
ofBareType (REx x t1 t2)
= liftM2 (REx x) (ofBareType t1) (ofBareType t2)
ofBareType (RAllT a t)
= liftM (RAllT (stringRTyVar a)) (ofBareType t)
ofBareType (RAllP π t)
= liftM2 RAllP (ofBPVar π) (ofBareType t)
ofBareType (RApp tc ts@[_] rs r)
| isList tc
= do tyi <- tcEnv <$> get
liftM2 (bareTCApp tyi r listTyCon) (mapM ofRef rs) (mapM ofBareType ts)
ofBareType (RApp tc ts rs r)
| isTuple tc
= do tyi <- tcEnv <$> get
liftM2 (bareTCApp tyi r c) (mapM ofRef rs) (mapM ofBareType ts)
where c = tupleTyCon BoxedTuple (length ts)
ofBareType (RApp tc ts rs r)
= do tyi <- tcEnv <$> get
liftM3 (bareTCApp tyi r) (lookupGhcTyCon tc) (mapM ofRef rs) (mapM ofBareType ts)
ofBareType (RCls c ts)
= liftM2 RCls (lookupGhcClass c) (mapM ofBareType ts)
ofBareType (ROth s)
= return $ ROth s
ofBareType t
= errorstar $ "Bare : ofBareType cannot handle " ++ show t
ofRef (RPoly ss t)
= liftM2 RPoly (mapM ofSyms ss) (ofBareType t)
ofRef (RMono ss r)
= liftM (`RMono` r) (mapM ofSyms ss)
ofSyms (x, t)
= liftM ((,) x) (ofBareType t)
-- TODO: move back to RefType
bareTCApp _ r c rs ts | length ts == tyConArity c
= if isTrivial t0 then t' else t
where t0 = rApp c ts rs top
t = rApp c ts rs r
t' = (expandRTypeSynonyms t0) `strengthen` r
-- otherwise create an error
-- create the error later to get better message
bareTCApp _ _ c rs ts = rApp c ts rs top
expandRTypeSynonyms = ofType . expandTypeSynonyms . toType
stringRTyVar = rTyVar . stringTyVar
-- stringTyVarTy = TyVarTy . stringTyVar
mkMeasureDCon :: Ms.MSpec t Symbol -> BareM (Ms.MSpec t DataCon)
mkMeasureDCon m = (forM (measureCtors m) $ \n -> (n,) <$> lookupGhcDataCon n)
>>= (return . mkMeasureDCon_ m)
mkMeasureDCon_ :: Ms.MSpec t Symbol -> [(String, DataCon)] -> Ms.MSpec t DataCon
mkMeasureDCon_ m ndcs = m' {Ms.ctorMap = cm'}
where
m' = fmap tx m
cm' = hashMapMapKeys (tx' . tx) $ Ms.ctorMap m'
tx = mlookup (M.fromList ndcs) . symbolString
tx' = dataConSymbol
measureCtors :: Ms.MSpec t Symbol -> [String]
measureCtors = sortNub . fmap (symbolString . Ms.ctor) . concat . M.elems . Ms.ctorMap
-- mkMeasureSort :: (PVarable pv, Reftable r) => Ms.MSpec (BRType pv r) bndr-> BareM (Ms.MSpec (RRType pv r) bndr)
mkMeasureSort (Ms.MSpec cm mm)
= liftM (Ms.MSpec cm) $ forM mm $ \m -> do
liftM (\s' -> m {Ms.sort = s'}) (ofBareType' (msg m) (Ms.sort m))
where
msg m = berrMeasure (loc $ Ms.name m) (Ms.name m) (Ms.sort m)
-----------------------------------------------------------------------
----------------------- Prop TyCon Definition -------------------------
-----------------------------------------------------------------------
propTyCon = stringTyCon 'w' 24 propConName
-- propMeasure = (stringSymbolRaw propConName, FFunc
-----------------------------------------------------------------------
---------------- Bare Predicate: DataCon Definitions ------------------
-----------------------------------------------------------------------
makeConTypes (name,spec) = inModule name $ makeConTypes' $ Ms.dataDecls spec
makeConTypes' :: [DataDecl] -> BareM ([(TyCon, TyConP)], [[(DataCon, DataConP)]])
makeConTypes' dcs = unzip <$> mapM ofBDataDecl dcs
ofBDataDecl :: DataDecl -> BareM ((TyCon, TyConP), [(DataCon, DataConP)])
ofBDataDecl (D tc as ps cts pos sfun)
= do πs <- mapM ofBPVar ps
tc' <- lookupGhcTyCon tc
cts' <- mapM (ofBDataCon (berrDataDecl pos tc πs) tc' αs ps πs) cts
let tys = [t | (_, dcp) <- cts', (_, t) <- tyArgs dcp]
let initmap = zip (uPVar <$> πs) [0..]
let varInfo = concatMap (getPsSig initmap True) tys
let cov = [i | (i, b)<- varInfo, b, i >=0]
let contr = [i | (i, b)<- varInfo, not b, i >=0]
return ((tc', TyConP αs πs cov contr sfun), cts')
where αs = fmap (RTV . stringTyVar) as
-- cpts = fmap (second (fmap (second (mapReft ur_pred)))) cts
getPsSig m pos (RAllT _ t)
= getPsSig m pos t
getPsSig m pos (RApp _ ts rs r)
= addps m pos r ++ concatMap (getPsSig m pos) ts
++ concatMap (getPsSigPs m pos) rs
getPsSig m pos (RVar _ r)
= addps m pos r
getPsSig m pos (RAppTy t1 t2 r)
= addps m pos r ++ getPsSig m pos t1 ++ getPsSig m pos t2
getPsSig m pos (RFun _ t1 t2 r)
= addps m pos r ++ getPsSig m pos t2 ++ getPsSig m (not pos) t1
getPsSigPs m pos (RMono _ r) = addps m pos r
getPsSigPs m pos (RPoly _ t) = getPsSig m pos t
addps m pos (U _ ps) = (flip (,)) pos . f <$> pvars ps
where f = fromMaybe (error "Bare.addPs: notfound") . (`L.lookup` m) . uPVar
-- ofBPreds = fmap (fmap stringTyVarTy)
dataDeclTyConP d
= do let αs = fmap (RTV . stringTyVar) (tycTyVars d) -- as
πs <- mapM ofBPVar (tycPVars d) -- ps
tc' <- lookupGhcTyCon (tycName d) -- tc
return $ (tc', TyConP αs πs)
-- ofBPreds = fmap (fmap stringTyVarTy)
ofBPVar :: PVar BSort -> BareM (PVar RSort)
ofBPVar = mapM_pvar ofBareType
mapM_pvar :: (Monad m) => (a -> m b) -> PVar a -> m (PVar b)
mapM_pvar f (PV x t txys)
= do t' <- f t
txys' <- mapM (\(t, x, y) -> liftM (, x, y) (f t)) txys
return $ PV x t' txys'
ofBDataCon msg tc αs ps πs (c, xts)
= do c' <- wrapErr msg lookupGhcDataCon c
ts' <- mapM (mkSpecType' msg ps) ts
let t0 = rApp tc rs (RMono [] . pdVarReft <$> πs) top
return $ (c', DataConP αs πs (reverse (zip xs' ts')) t0)
where
(xs, ts) = unzip xts
xs' = map stringSymbol xs
rs = [rVar α | RTV α <- αs] -- [RVar α pdTrue | α <- αs]
-----------------------------------------------------------------------
---------------- Bare Predicate: RefTypes -----------------------------
-----------------------------------------------------------------------
txParams f πs t = mapReft (f (txPvar (predMap πs t))) t
txPvar :: M.HashMap Symbol UsedPVar -> UsedPVar -> UsedPVar
txPvar m π = π { pargs = args' }
where args' | not (null (pargs π)) = zipWith (\(_,x ,_) (t,_,y) -> (t, x, y)) (pargs π') (pargs π)
| otherwise = pargs π'
π' = fromMaybe (errorstar err) $ M.lookup (pname π) m
err = "Bare.replaceParams Unbound Predicate Variable: " ++ show π
predMap πs t = Ex.assert (M.size xπm == length xπs) xπm
where xπm = M.fromList xπs
xπs = [(pname π, π) | π <- πs ++ rtypePredBinds t]
rtypePredBinds = map uPVar . snd3 . bkUniv
-- rtypePredBinds t = everything (++) ([] `mkQ` grab) t
-- where grab ((RAllP pv _) :: BRType RPVar RPredicate) = [pv]
-- grab _ = []
----------------------------------------------------------------------------------------------
----- Checking GhcSpec -----------------------------------------------------------------------
----------------------------------------------------------------------------------------------
checkGhcSpec :: (GhcSpec, [Ms.Measure SpecType DataCon]) -> Either [Error] GhcSpec
checkGhcSpec (sp, ms) = applyNonNull (Right sp) Left errors
where
errors = mapMaybe (checkBind "variable" emb env) (tySigs sp)
++ mapMaybe (checkBind "constructor" emb env) (dcons sp)
++ mapMaybe (checkBind "measure" emb env) (measSpec sp)
++ mapMaybe (checkInv emb env) (invariants sp)
++ checkMeasures emb env ms
++ mapMaybe checkMismatch (tySigs sp)
++ checkDuplicate (tySigs sp)
dcons spec = mapSnd (Loc dummyPos) <$> dataConSpec (dconsP spec)
emb = tcEmbeds sp
env = ghcSpecEnv sp
measSpec sp = [(x, uRType <$> t) | (x, t) <- meas sp]
-- specError = errorstar
-- . render
-- . vcat
-- . punctuate (text "\n----\n")
-- . (text "Alas, errors found in specification..." :)
checkInv :: TCEmb TyCon -> SEnv SortedReft -> Located SpecType -> Maybe Error
checkInv emb env t = checkTy err emb env (val t)
where
err = ErrInvt (sourcePosSrcSpan $ loc t) (val t)
checkBind :: (PPrint v) => String -> TCEmb TyCon -> SEnv SortedReft -> (v, Located SpecType) -> Maybe Error
checkBind s emb env (v, Loc l t) = checkTy msg emb env t
where
msg = ErrTySpec (sourcePosSrcSpan l) (text s <+> pprint v) t
checkTy :: (Doc -> Error) -> TCEmb TyCon -> SEnv SortedReft -> SpecType -> Maybe Error
checkTy mkE emb env t = mkE <$> checkRType emb env t
checkDuplicate :: [(Var, Located SpecType)] -> [Error]
checkDuplicate xts = mkErr <$> dups
where
mkErr (x, ts) = ErrDupSpecs (getSrcSpan x) (pprint x) (sourcePosSrcSpan . loc <$> ts)
dups = [z | z@(x, t1:t2:_) <- M.toList $ group xts ]
checkMismatch :: (Var, Located SpecType) -> Maybe Error
checkMismatch (x, t) = if ok then Nothing else Just err
where
ok = tyCompat x (val t)
err = errTypeMismatch x t
tyCompat x t = lhs == rhs
where
lhs :: RSort = toRSort t
rhs :: RSort = ofType $ varType x
msg = printf "tyCompat: l = %s r = %s" (showpp lhs) (showpp rhs)
ghcSpecEnv sp = fromListSEnv binds
where
emb = tcEmbeds sp
binds = [(x, rSort t) | (x, Loc _ t) <- meas sp]
++ [(varSymbol v, rSort t) | (v, Loc _ t) <- ctor sp]
++ [(x , vSort v) | (x, v) <- freeSyms sp, isConLikeId v]
rSort = rTypeSortedReft emb
vSort = rSort . varRType
varRType :: Var -> RRType ()
varRType = ofType . varType
errTypeMismatch :: Var -> Located SpecType -> Error
errTypeMismatch x t = ErrMismatch (sourcePosSrcSpan $ loc t) (pprint x) (varType x) (val t)
-------------------------------------------------------------------------------------
-- | This function checks if a type is malformed in a given environment -------------
-------------------------------------------------------------------------------------
-------------------------------------------------------------------------------------
checkRType :: (PPrint r, Reftable r) => TCEmb TyCon -> SEnv SortedReft -> RRType r -> Maybe Doc
-------------------------------------------------------------------------------------
checkRType emb env t = efoldReft cb (rTypeSortedReft emb) f env Nothing t
where
cb c ts = classBinds (RCls c ts)
f env me r err = err <|> checkReft env emb me r
checkReft :: (PPrint r, Reftable r) => SEnv SortedReft -> TCEmb TyCon -> Maybe (RRType r) -> r -> Maybe Doc
checkReft env emb Nothing _ = Nothing -- RMono / Ref case, not sure how to check these yet.
checkReft env emb (Just t) _ = (dr $+$) <$> checkSortedReftFull env r
where
r = rTypeSortedReft emb t
dr = text "Sort Error in Refinement:" <+> pprint r
-- DONT DELETE the below till we've added pred-checking as well
-- checkReft env emb (Just t) _ = checkSortedReft env xs (rTypeSortedReft emb t)
-- where xs = fromMaybe [] $ params <$> stripRTypeBase t
-- checkSig env (x, t)
-- = case filter (not . (`S.member` env)) (freeSymbols t) of
-- [] -> True
-- ys -> errorstar (msg ys)
-- where
-- msg ys = printf "Unkown free symbols: %s in specification for %s \n%s\n" (showpp ys) (showpp x) (showpp t)
-------------------------------------------------------------------------------
------------------ Replace Predicate Arguments With Existentials -------------
-------------------------------------------------------------------------------
data ExSt = ExSt { fresh :: Int
, emap :: M.HashMap Symbol (RSort, Expr)
, pmap :: M.HashMap Symbol RPVar
}
-- | Niki: please write more documentation for this, maybe an example?
-- I can't really tell whats going on... (RJ)
txExpToBind :: SpecType -> SpecType
txExpToBind t = evalState (expToBindT t) (ExSt 0 M.empty πs)
where πs = M.fromList [(pname p, p) | p <- snd3 $ bkUniv t ]
expToBindT :: SpecType -> State ExSt SpecType
expToBindT (RVar v r)
= expToBindRef r >>= addExists . RVar v
expToBindT (RFun x t1 t2 r)
= do t1' <- expToBindT t1
t2' <- expToBindT t2
expToBindRef r >>= addExists . RFun x t1' t2'
expToBindT (RAllT a t)
= liftM (RAllT a) (expToBindT t)
expToBindT (RAllP p t)
= liftM (RAllP p) (expToBindT t)
expToBindT (RApp c ts rs r)
= do ts' <- mapM expToBindT ts
rs' <- mapM expToBindReft rs
expToBindRef r >>= addExists . RApp c ts' rs'
expToBindT (RCls c ts)
= liftM (RCls c) (mapM expToBindT ts)
expToBindT (RAppTy t1 t2 r)
= do t1' <- expToBindT t1
t2' <- expToBindT t2
expToBindRef r >>= addExists . RAppTy t1' t2'
expToBindT t
= return t
expToBindReft :: Ref RSort RReft (SpecType) -> State ExSt (Ref RSort RReft SpecType)
expToBindReft (RPoly s t) = liftM (RPoly s) (expToBindT t)
expToBindReft (RMono s r) = liftM (RMono s) (expToBindRef r)
getBinds :: State ExSt (M.HashMap Symbol (RSort, Expr))
getBinds
= do bds <- emap <$> get
modify $ \st -> st{emap = M.empty}
return bds
addExists t = liftM (M.foldlWithKey' addExist t) getBinds
addExist t x (tx, e) = RAllE x t' t
where t' = (ofRSort tx) `strengthen` uTop r
r = Reft (vv Nothing, [RConc (PAtom Eq (EVar (vv Nothing)) e)])
expToBindRef :: UReft r -> State ExSt (UReft r)
expToBindRef (U r (Pr p))
= mapM expToBind p >>= return . U r . Pr
expToBind :: UsedPVar -> State ExSt UsedPVar
expToBind p
= do Just π <- liftM (M.lookup (pname p)) (pmap <$> get)
let pargs0 = zip (pargs p) (fst3 <$> pargs π)
pargs' <- mapM expToBindParg pargs0
return $ p{pargs = pargs'}
expToBindParg :: (((), Symbol, Expr), RSort) -> State ExSt ((), Symbol, Expr)
expToBindParg ((t, s, e), s') = liftM ((,,) t s) (expToBindExpr e s')
expToBindExpr :: Expr -> RRType () -> State ExSt Expr
expToBindExpr e@(EVar (S (c:_))) _ | isLower c
= return e
expToBindExpr e t
= do s <- freshSymbol
modify $ \st -> st{emap = M.insert s (t, e) (emap st)}
return $ EVar s
freshSymbol :: State ExSt Symbol
freshSymbol
= do n <- fresh <$> get
modify $ \s -> s{fresh = n+1}
return $ S $ "ex#" ++ show n
-------------------------------------------------------------------------------------
-- | Tasteful Error Messages --------------------------------------------------------
-------------------------------------------------------------------------------------
berrDataDecl l c πs = printf "[%s]\nCannot convert data type %s with πs = %s"
(showpp l) (showpp c) (showpp πs)
berrVarSpec l v b = printf "[%s]\nCannot convert\n %s :: %s"
(showpp l) (showpp v) (showpp b)
berrInvariant l i = printf "[%s]\nCannot convert invariant\n %s"
(showpp l) (showpp i)
berrMeasure l x t = printf "[%s]\nCannot convert measure %s :: %s"
(showpp l) (showpp x) (showpp t)
-- berrUnknownVar x = printf "[%s]\nSpecification for unknown Variable : %s"
-- (showpp $ loc x) (showpp $ val x)
--
-- berrUnknownTyCon x = printf "[%s]\nSpecification for unknown TyCon : %s"
-- (showpp $ loc x) (showpp $ val x)
berrUnknownTyCon = berrUnknown "TyCon"
berrUnknownVar = berrUnknown "Variable"
berrUnknown :: (PPrint a) => String -> Located a -> String
berrUnknown thing x = printf "[%s]\nSpecification for unknown %s : %s"
thing (showpp $ loc x) (showpp $ val x)
-- berrUnknownTyCon z = printf "Specification for unknown variable: %s defined at: %s"
-- (showpp $ symbolString $ val z) (showpp $ loc z)