{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE NoMonomorphismRestriction #-} {-# LANGUAGE TypeSynonymInstances #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE TupleSections #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE ParallelListComp #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ViewPatterns #-} -- | 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 ) where import ConLike import GHC hiding (lookupName, Located) import Text.PrettyPrint.HughesPJ hiding (first, (<>)) import Var import Name (getSrcSpan, isInternalName) import NameSet import Id (isConLikeId) import CoreSyn hiding (Expr) import PrelNames import PrelInfo (wiredInThings) import Type (expandTypeSynonyms, splitFunTy_maybe) import DataCon (dataConWorkId, dataConStupidTheta) import TyCon (SynTyConRhs(SynonymTyCon)) import HscMain import TysWiredIn import BasicTypes (TupleSort (..), Arity) import TcRnDriver (tcRnLookupRdrName) import RdrName (setRdrNameSpace) import OccName (tcName) import Data.Char (isLower, isUpper) import Text.Printf -- import Data.Maybe (listToMaybe, fromMaybe, mapMaybe, catMaybes, isNothing, fromJust) import Control.Monad.State (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.Bifunctor import Data.Generics.Aliases (mkT) import Data.Generics.Schemes (everywhere) -- import Data.Data hiding (TyCon, tyConName) -- import Data.Function (on) import qualified Data.Text as T import Text.Parsec.Pos import Language.Fixpoint.Misc import Language.Fixpoint.Names (prims, hpropConName, propConName, takeModuleNames, dropModuleNames, isPrefixOfSym, dropSym, lengthSym, headSym, stripParensSym, takeWhileSym) import Language.Fixpoint.Types hiding (Def, Predicate, R) import Language.Fixpoint.Sort (checkSortFull, checkSortedReftFull, checkSorted) 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.Errors import Language.Haskell.Liquid.PredType hiding (unify) import qualified Language.Haskell.Liquid.Measure as Ms import Data.Maybe import qualified Data.List as L import qualified Data.HashSet as S import qualified Data.HashMap.Strict as M import TypeRep import Debug.Trace (trace) ------------------------------------------------------------------ ---------- Top Level Output -------------------------------------- ------------------------------------------------------------------ makeGhcSpec :: Config -> ModName -> [CoreBind] -> [Var] -> [Var] -> NameSet -> HscEnv -> [(ModName,Ms.BareSpec)] -> IO GhcSpec makeGhcSpec cfg name cbs vars defVars exports env specs = throwOr (throwOr return . checkGhcSpec specs . postProcess cbs) =<< execBare act initEnv where act = makeGhcSpec' cfg vars defVars exports specs throwOr = either Ex.throw initEnv = BE name mempty mempty mempty env postProcess :: [CoreBind] -> GhcSpec -> GhcSpec postProcess cbs sp@(SP {..}) = sp { tySigs = sigs, texprs = ts } -- HEREHEREHEREHERE (addTyConInfo stuff) where (sigs, ts) = replaceLocalBinds tcEmbeds tyconEnv tySigs texprs (ghcSpecEnv sp) cbs ------------------------------------------------------------------------------------------------ makeGhcSpec' :: Config -> [Var] -> [Var] -> NameSet -> [(ModName, Ms.BareSpec)] -> BareM GhcSpec ------------------------------------------------------------------------------------------------ makeGhcSpec' cfg vars defVars exports specs = do name <- gets modName _ <- makeRTEnv specs (tycons, datacons, dcSelectors, tyi) <- makeGhcSpecCHOP1 specs modify $ \be -> be { tcEnv = tyi } (cls, mts) <- second mconcat . unzip . mconcat <$> mapM (makeClasses cfg vars) specs (invs, ialias, embs, sigs, asms) <- makeGhcSpecCHOP2 cfg vars defVars specs name cls mts (measures, cms', ms', cs', xs') <- makeGhcSpecCHOP3 cfg vars specs dcSelectors datacons cls embs syms <- makeSymbols (vars ++ map fst cs') xs' (sigs ++ asms ++ cs') ms' (invs ++ (snd <$> ialias)) let su = mkSubst [ (x, mkVarExpr v) | (x, v) <- syms] return (emptySpec cfg) >>= makeGhcSpec0 cfg defVars exports name >>= makeGhcSpec1 vars embs tyi exports name sigs asms cs' ms' cms' su >>= makeGhcSpec2 invs ialias measures su >>= makeGhcSpec3 datacons tycons embs syms >>= makeGhcSpec4 defVars specs name su emptySpec :: Config -> GhcSpec emptySpec cfg = SP [] [] [] [] [] [] [] [] [] mempty [] [] [] [] mempty mempty cfg mempty [] mempty makeGhcSpec0 cfg defVars exports name sp = do targetVars <- makeTargetVars name defVars $ binders cfg return $ sp { config = cfg , exports = exports , tgtVars = targetVars } makeGhcSpec1 vars embs tyi exports name sigs asms cs' ms' cms' su sp = return $ sp { tySigs = makePluggedSigs name embs tyi exports $ tx sigs , asmSigs = renameTyVars <$> tx asms , ctors = tx cs' , meas = tx $ ms' ++ varMeasures vars ++ cms' } where tx = fmap . mapSnd . subst $ su makeGhcSpec2 invs ialias measures su sp = return $ sp { invariants = subst su invs , ialiases = subst su ialias , measures = subst su <$> M.elems $ Ms.measMap measures } makeGhcSpec3 datacons tycons embs syms sp = do tcEnv <- gets tcEnv return $ sp { tyconEnv = tcEnv , dconsP = datacons , tconsP = tycons , tcEmbeds = embs , freeSyms = [(symbol v, v) | (_, v) <- syms] } makeGhcSpec4 defVars specs name su sp = do decr' <- mconcat <$> mapM (makeHints defVars) specs texprs' <- mconcat <$> mapM (makeTExpr defVars) specs lazies <- mkThing makeLazy lvars' <- mkThing makeLVar quals <- mconcat <$> mapM makeQualifiers specs return $ sp { qualifiers = subst su quals , decr = decr' , texprs = texprs' , lvars = lvars' , lazy = lazies } where mkThing mk = S.fromList . mconcat <$> sequence [ mk defVars (m, s) | (m, s) <- specs, m == name ] makeGhcSpecCHOP1 specs = do (tcs, dcs) <- mconcat <$> mapM makeConTypes specs let tycons = tcs ++ wiredTyCons let datacons = mapSnd val <$> (concat dcs ++ wiredDataCons) let dcSelectors = concat $ map makeMeasureSelectors (concat dcs) let tyi = makeTyConInfo tycons return $ (tycons, datacons, dcSelectors, tyi) makeGhcSpecCHOP2 cfg vars defVars specs name cls mts = do sigs' <- mconcat <$> mapM (makeAssertSpec name cfg vars defVars) specs asms' <- mconcat <$> mapM (makeAssumeSpec name cfg vars defVars) specs invs <- mconcat <$> mapM makeInvariants specs ialias <- mconcat <$> mapM makeIAliases specs embs <- mconcat <$> mapM makeTyConEmbeds specs let dms = makeDefaultMethods vars mts tyi <- gets tcEnv let sigs = [ (x, txRefSort tyi embs . txExpToBind <$> t) | (m, x, t) <- sigs' ++ mts ++ dms ] let asms = [ (x, txRefSort tyi embs . txExpToBind <$> t) | (m, x, t) <- asms' ] return (invs, ialias, embs, sigs, asms) makeGhcSpecCHOP3 cfg vars specs dcSelectors datacons cls embs = do measures' <- mconcat <$> mapM makeMeasureSpec specs tyi <- gets tcEnv let measures = measures' `mappend` Ms.mkMSpec' dcSelectors let (cs, ms) = makeMeasureSpec' measures let cms = makeClassMeasureSpec measures let cms' = [ (x, Loc l $ cSort t) | (Loc l x, t) <- cms ] let ms' = [ (x, Loc l t) | (Loc l x, t) <- ms, isNothing $ lookup x cms' ] let cs' = [ (v, Loc (getSourcePos v) (txRefSort tyi embs t)) | (v, t) <- meetDataConSpec cs (datacons ++ cls)] let xs' = val . fst <$> ms return (measures, cms', ms', cs', xs') makeMeasureSelectors :: (DataCon, Located DataConP) -> [Measure SpecType DataCon] makeMeasureSelectors (dc, (Loc loc (DataConP _ vs _ _ _ xts r))) = go <$> zip (reverse xts) [1..] where go ((x,t), i) = makeMeasureSelector (Loc loc x) (dty t) dc n i dty t = foldr RAllT (RFun dummySymbol r (fmap mempty t) mempty) vs n = length xts makePluggedSigs name embs tcEnv exports sigs = [ (x, plugHoles embs tcEnv x r τ t) | (x, t) <- sigs , let τ = expandTypeSynonyms $ varType x , let r = maybeTrue x name exports ] makeMeasureSelector x s dc n i = M {name = x, sort = s, eqns = [eqn]} where eqn = Def x dc (mkx <$> [1 .. n]) (E (EVar $ mkx i)) mkx j = symbol ("xx" ++ show j) --- Refinement Type Aliases makeRTEnv specs = do forM_ rts $ \(mod, rta) -> setRTAlias (rtName rta) $ Left (mod, rta) forM_ pts $ \(mod, pta) -> setRPAlias (rtName pta) $ Left (mod, pta) makeRPAliases pts makeRTAliases rts where rts = (concat [(m,) <$> Ms.aliases s | (m, s) <- specs]) pts = (concat [(m,) <$> Ms.paliases s | (m, s) <- specs]) makeRTAliases xts = mapM_ expBody xts where expBody (mod,xt) = inModule mod $ do let l = rtPos xt body <- withVArgs l (rtVArgs xt) $ expandRTAlias l $ rtBody xt setRTAlias (rtName xt) $ Right $ mapRTAVars symbolRTyVar $ xt { rtBody = body } makeRPAliases xts = mapM_ expBody xts where expBody (mod, xt) = inModule mod $ do let l = rtPos xt env <- gets $ predAliases . rtEnv body <- withVArgs l (rtVArgs xt) $ expandRPAliasE l $ rtBody xt setRPAlias (rtName xt) $ Right $ xt { rtBody = body } -- | Using the Alias Environment to Expand Definitions expandRTAliasMeasure m = do eqns <- sequence $ expandRTAliasDef <$> (eqns m) return $ m { sort = generalize (sort m) , eqns = eqns } expandRTAliasDef :: Def LocSymbol -> BareM (Def LocSymbol) expandRTAliasDef d = do env <- gets rtEnv body <- expandRTAliasBody (loc $ measure d) env $ body d return $ d { body = body } expandRTAliasBody :: SourcePos -> RTEnv -> Body -> BareM Body expandRTAliasBody l env (P p) = P <$> expPAlias l p expandRTAliasBody l env (R x p) = R x <$> expPAlias l p expandRTAliasBody l _ (E e) = E <$> resolve l e expPAlias :: SourcePos -> Pred -> BareM Pred expPAlias l = expandPAlias l [] expandRTAlias :: SourcePos -> BareType -> BareM SpecType expandRTAlias l bt = expType =<< expReft bt where expReft = mapReftM (txPredReft expPred) expType = expandAlias l [] expPred = expandPAlias l [] txPredReft :: (Pred -> BareM Pred) -> RReft -> BareM RReft txPredReft f (U r p l) = (\r -> U r p l) <$> 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 l = expandPAlias l [] expandAlias :: SourcePos -> [Symbol] -> BareType -> BareM SpecType expandAlias l = go where go s t@(RApp (Loc _ c) _ _ _) | c `elem` s = Ex.throw $ errOther $ text $ "Cyclic Reftype Alias Definition: " ++ show (c:s) | otherwise = lookupExpandRTApp l s t go s (RVar a r) = RVar (symbolRTyVar a) <$> resolve l 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' <*> resolve l r 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 (symbolRTyVar a) <$> go s t go s (RAllP a t) = RAllP <$> ofBPVar a <*> go s t go s (RAllS l t) = RAllS l <$> 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 _ (RHole r) = RHole <$> resolve l r lookupExpandRTApp l s (RApp lc@(Loc _ c) ts rs r) = do env <- gets (typeAliases.rtEnv) case M.lookup c env of Just (Left (mod,rtb)) -> do st <- inModule mod $ withVArgs l (rtVArgs rtb) $ expandAlias l (c:s) $ rtBody rtb let rts = mapRTAVars symbolRTyVar $ rtb { rtBody = st } setRTAlias c $ Right rts r' <- resolve l r expandRTApp l s rts ts r' Just (Right rts) -> do r' <- resolve l r withVArgs l (rtVArgs rts) $ expandRTApp l s rts ts r' Nothing | isList c && length ts == 1 -> do tyi <- tcEnv <$> get r' <- resolve l r liftM2 (bareTCApp tyi r' listTyCon) (mapM (go s) rs) (mapM (expandAlias l s) ts) | isTuple c -> do tyi <- tcEnv <$> get r' <- resolve l r let tc = tupleTyCon BoxedTuple (length ts) liftM2 (bareTCApp tyi r' tc) (mapM (go s) rs) (mapM (expandAlias l s) ts) | otherwise -> do tyi <- tcEnv <$> get r' <- resolve l r liftM3 (bareTCApp tyi r') (lookupGhcTyCon lc) (mapM (go s) rs) (mapM (expandAlias l s) ts) where go s (RPropP ss r) = RPropP <$> mapM ofSyms ss <*> resolve l r go s (RProp ss t) = RProp <$> mapM ofSyms ss <*> expandAlias l s t go _ (RHProp _ _) = errorstar "TODO:EFFECTS:lookupExpandRTApp" expandRTApp :: SourcePos -> [Symbol] -> RTAlias RTyVar SpecType -> [BareType] -> RReft -> BareM SpecType expandRTApp l s rta args r | length args == (length αs) + (length εs) = do args' <- mapM (expandAlias l 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 msg) where su = mkSubst $ zip (symbol <$> ε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_ msg = "Malformed type alias application at " ++ show l ++ "\n\t" ++ show (rtName rta) ++ " defined at " ++ show (rtPos rta) ++ "\n\texpects " ++ show (length αs + length εs) ++ " arguments but it is given " ++ show (length args) -- | 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 (symbol x) exprArg _ (RApp x [] [] _) = EVar (symbol x) exprArg msg (RApp f ts [] _) = EApp (symbol <$> f) (exprArg msg <$> ts) exprArg msg (RAppTy (RVar f _) t _) = EApp (dummyLoc $ symbol f) [exprArg msg t] exprArg msg z = errorstar $ printf "Unexpected expression parameter: %s in %s" (show z) msg expandPAlias :: SourcePos -> [Symbol] -> Pred -> BareM Pred expandPAlias l = go where go s p@(PBexp (EApp f@(Loc l' f') es)) | f' `elem` s = errorstar $ "Cyclic Predicate Alias Definition: " ++ show (f':s) | otherwise = do env <- gets (predAliases.rtEnv) case M.lookup f' env of Just (Left (mod,rp)) -> do body <- inModule mod $ withVArgs l' (rtVArgs rp) $ expandPAlias l' (f':s) $ rtBody rp let rp' = rp { rtBody = body } setRPAlias f' $ Right $ rp' expandRPApp l (f':s) rp' <$> resolve l es Just (Right rp) -> withVArgs l (rtVArgs rp) (expandRPApp l (f':s) rp <$> resolve l es) Nothing -> fmap PBexp (EApp <$> resolve l f <*> resolve l 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 l p expandRPApp l s rp es = let su = mkSubst $ safeZipWithError msg (rtVArgs rp) es msg = "Malformed alias application at " ++ show l ++ "\n\t" ++ show (rtName rp) ++ " defined at " ++ show (rtPos rp) ++ "\n\texpects " ++ show (length $ rtVArgs rp) ++ " arguments but it is given " ++ show (length es) -- msg = "expandRPApp: " ++ show (EApp (dummyLoc $ symbol $ rtName rp) es) in subst su $ rtBody rp makeQualifiers (mod,spec) = inModule mod mkQuals where mkQuals = -- resolve dummyPos $ Ms.qualifiers spec mapM (\q -> resolve (q_pos q) q) $ Ms.qualifiers spec makeClasses cfg vs (mod, spec) = inModule mod $ mapM mkClass $ Ms.classes spec where --FIXME: cleanup this code unClass = snd . bkClass . fourth4 . bkUniv mkClass (RClass c ss as ms) = do let l = loc c tc <- lookupGhcTyCon c ss' <- mapM (mkSpecType l) ss let (dc:_) = tyConDataCons tc let αs = map symbolRTyVar as let as' = [rVar $ symbolTyVar a | a <- as ] let ms' = [ (s, rFun "" (RCls c (flip RVar mempty <$> as)) t) | (s, t) <- ms] vts <- makeSpec cfg vs ms' let sts = [(val s, unClass $ val t) | (s, _) <- ms | (_, _, t) <- vts] let t = RCls (fromJust $ tyConClass_maybe tc) as' let dcp = DataConP l αs [] [] ss' (reverse sts) t return ((dc,dcp),vts) makeHints vs (_, spec) = varSymbols id "Hint" vs $ Ms.decr spec makeLVar vs (_, spec) = fmap fst <$> (varSymbols id "LazyVar" vs $ [(v, ()) | v <- Ms.lvars spec]) makeLazy vs (_, spec) = fmap fst <$> (varSymbols id "Lazy" vs $ [(v, ()) | v <- S.toList $ Ms.lazy spec]) makeTExpr vs (_, spec) = varSymbols id "TermExpr" vs $ Ms.termexprs spec varSymbols :: ([Var] -> [Var]) -> Symbol -> [Var] -> [(LocSymbol, a)] -> BareM [(Var, a)] varSymbols f n vs = concatMapM go where lvs = M.map L.sort $ group [(sym v, locVar v) | v <- vs] sym = dropModuleNames . symbol . showPpr locVar v = (getSourcePos v, v) go (s, ns) = case M.lookup (val s) lvs of Just lvs -> return ((, ns) <$> varsAfter f s lvs) Nothing -> ((:[]).(,ns)) <$> lookupGhcVar s msg s = printf "%s: %s for Undefined Var %s" (symbolString n) (show (loc s)) (show (val s)) varsAfter f s lvs | eqList (fst <$> lvs) = f (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 -- EFFECTS: TODO is this the SAME as addTyConInfo? No. `txRefSort` -- (1) adds the _real_ sorts to RProp, -- (2) gathers _extra_ RProp at turnst them into refinements, -- e.g. tests/pos/multi-pred-app-00.hs txRefSort tyi tce = mapBot (addSymSort tce tyi) addSymSort tce tyi t@(RApp rc@(RTyCon c _ _) ts rs r) = RApp rc ts (zipWith addSymSortRef pvs rargs) r' where rc' = appRTyCon tce tyi rc ts pvs = rTyConPVs rc' rs' = zipWith addSymSortRef pvs rargs (rargs, rrest) = splitAt (length pvs) rs r' = L.foldl' go r rrest go r (RPropP _ r') = r' `meet` r go _ (RHProp _ _ ) = errorstar "TODO:EFFECTS:addSymSort" go r _ = errorstar "YUCKER" -- r addSymSort _ _ t = t addSymSortRef _ (RHProp _ _) = errorstar "TODO:EFFECTS:addSymSortRef" addSymSortRef p r | isPropPV p = addSymSortRef' p r | otherwise = errorstar "addSymSortRef: malformed ref application" addSymSortRef' p (RProp s (RVar v r)) | isDummy v = RProp xs t where t = ofRSort (pvType p) `strengthen` r xs = spliceArgs "addSymSortRef 1" s p addSymSortRef' p (RProp s t) = RProp xs t where xs = spliceArgs "addSymSortRef 2" s p -- EFFECTS: why can't we replace the next two equations with (breaks many tests) -- -- EFFECTS: addSymSortRef' (PV _ (PVProp t) _ ptxs) (RPropP s r@(U _ (Pr [up]) _)) -- EFFECTS: = RProp xts $ (ofRSort t) `strengthen` r -- EFFECTS: where -- EFFECTS: xts = safeZip "addRefSortMono" xs ts -- EFFECTS: xs = snd3 <$> pargs up -- EFFECTS: ts = fst3 <$> ptxs -- -- EFFECTS: addSymSortRef' (PV _ (PVProp t) _ _) (RPropP s r) -- EFFECTS: = RProp s $ (ofRSort t) `strengthen` r addSymSortRef' p (RPropP s r@(U _ (Pr [up]) _)) = RPropP xts r where xts = safeZip "addRefSortMono" xs ts xs = snd3 <$> pargs up ts = fst3 <$> pargs p addSymSortRef' p (RPropP s r) = RPropP s r addSymSortRef' _ _ = errorstar "TODO:EFFECTS:addSymSortRef'" spliceArgs msg s p = safeZip msg (fst <$> s) (fst3 <$> pargs p) varMeasures vars = [ (symbol 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)) = (x, Loc l $ mkUnivs (rTyVar <$> αs) [] [] t') where t' = subts su $ mkUnivs [] ps ls tbody su = [(y, rTyVar x) | (x, y) <- tyvsmap] tyvsmap = vmap $ execState (mapTyVars τbody tbody) initvmap initvmap = initMapSt err (αs, τbody) = splitForAllTys $ expandTypeSynonyms $ varType x (as, ps, ls, tbody) = bkUniv t err = errTypeMismatch x lt data MapTyVarST = MTVST { vmap :: [(Var, RTyVar)] , errmsg :: Error } initMapSt = MTVST [] mapTyVars :: (PPrint r, Reftable r) => Type -> RRType r -> State MapTyVarST () mapTyVars τ (RAllT a t) = mapTyVars τ t mapTyVars (ForAllTy α τ) t = 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 τ (RAllS _ 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 τ (RHole _) = return () mapTyVars τ t = Ex.throw =<< errmsg <$> get mapTyRVar α a s@(MTVST αas err) = case lookup α αas of Just a' | a == a' -> s | otherwise -> Ex.throw err Nothing -> MTVST ((α,a):αas) err mkVarExpr v | isFunVar v = EApp (varFunSymbol v) [] | otherwise = EVar (symbol v) varFunSymbol = dummyLoc . dataConSymbol . idDataCon isFunVar v = isDataConWorkId v && not (null αs) && isNothing tf where (αs, t) = splitForAllTys $ varType v tf = splitFunTy_maybe t -- 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, ls1, _), (α2s, [], ls2, t2')) -> meet t1 (mkUnivs α2s π1s (ls1 ++ ls2) t2') ((α1s, [], ls1, t1'), (_, π2s, ls2, _)) -> meet (mkUnivs α1s π2s (ls1 ++ ls2) 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 Error (StateT BareEnv IO)) a type Warn = String type TCEnv = M.HashMap TyCon RTyCon data BareEnv = BE { modName :: !ModName , tcEnv :: !TCEnv , 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 l vs act = do old <- gets rtEnv mapM (mkExprAlias l . symbol . showpp) vs res <- act modify $ \be -> be { rtEnv = old } return res addSym x = modify $ \be -> be { varEnv = (varEnv be) `L.union` [x] } mkExprAlias l v = setRTAlias v (Right (RTA v [] [] (RExprArg (EVar $ symbol v)) l)) 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 (Either Error a) ------------------------------------------------------------------ execBare act benv = do z <- evalStateT (runErrorT (runWriterT act)) benv case z of Left s -> return $ Left s Right (x, ws) -> do forM_ ws $ putStrLn . ("WARNING: " ++) return $ Right x ------------------------------------------------------------------ -- | API: Bare Refinement Types ---------------------------------- ------------------------------------------------------------------ makeMeasureSpec :: (ModName, Ms.Spec BareType LocSymbol) -> BareM (Ms.MSpec SpecType DataCon) makeMeasureSpec (mod,spec) = inModule mod mkSpec where mkSpec = mkMeasureDCon =<< mkMeasureSort =<< m m = Ms.mkMSpec <$> (mapM expandRTAliasMeasure $ Ms.measures spec) <*> return (Ms.cmeasures spec) <*> (mapM expandRTAliasMeasure $ Ms.imeasures spec) makeMeasureSpec' = mapFst (mapSnd uRType <$>) . Ms.dataConTypes . first (mapReft ur_reft) makeClassMeasureSpec (Ms.MSpec {..}) = tx <$> M.elems cmeasMap where tx (M n s _) = (n, CM n (mapReft ur_reft s) -- [(t,m) | (IM n' t m) <- imeas, n == n'] ) makeTargetVars :: ModName -> [Var] -> [String] -> BareM [Var] makeTargetVars name vs ss = do env <- gets hscEnv ns <- liftIO $ concatMapM (lookupName env name . dummyLoc . prefix) ss return $ filter ((`elem` ns) . varName) vs where prefix s = qualifySymbol (symbol name) (symbol s) makeAssertSpec cmod cfg vs lvs (mod,spec) | cmod == mod = makeLocalSpec cfg cmod vs lvs (Ms.sigs spec ++ Ms.localSigs spec) | otherwise = inModule mod $ makeSpec cfg vs $ Ms.sigs spec makeAssumeSpec cmod cfg vs lvs (mod,spec) | cmod == mod = makeLocalSpec cfg cmod vs lvs $ Ms.asmSigs spec | otherwise = inModule mod $ makeSpec cfg vs $ Ms.asmSigs spec makeDefaultMethods :: [Var] -> [(ModName,Var,Located SpecType)] -> [(ModName,Var,Located SpecType)] makeDefaultMethods defVs sigs = [ (m,dmv,t) | dmv <- defVs , let dm = symbol $ showPpr dmv , "$dm" `isPrefixOfSym` (dropModuleNames dm) , let mod = takeModuleNames dm , let method = qualifySymbol mod $ dropSym 3 (dropModuleNames dm) , let mb = L.find ((method `isPrefixOfSym`) . symbol . snd3) sigs , isJust mb , let Just (m,_,t) = mb ] makeLocalSpec :: Config -> ModName -> [Var] -> [Var] -> [(LocSymbol, BareType)] -> BareM [(ModName, Var, Located SpecType)] makeLocalSpec cfg mod vs lvs xbs = do env <- get vbs1 <- fmap expand3 <$> varSymbols fchoose "Var" lvs (dupSnd <$> xbs1) unless (noCheckUnknown cfg) $ checkDefAsserts env vbs1 xbs1 vts1 <- map (addFst3 mod) <$> mapM mkVarSpec vbs1 vts2 <- makeSpec cfg vs xbs2 return $ vts1 ++ vts2 where (xbs1, xbs2) = L.partition (modElem mod . fst) xbs dupSnd (x, y) = (dropMod x, (x, y)) expand3 (x, (y, w)) = (x, y, w) dropMod = fmap (dropModuleNames . symbol) fchoose ls = maybe ls (:[]) $ L.find (`elem` vs) ls modElem n x = (takeModuleNames $ val x) == (symbol n) makeSpec :: Config -> [Var] -> [(LocSymbol, BareType)] -> BareM [(ModName, Var, Located SpecType)] makeSpec cfg vs xbs = do vbs <- map (joinVar vs) <$> lookupIds xbs env@(BE { modName = mod}) <- get unless (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 = mapM lookup where lookup (s, t) = (,s,t) <$> lookupGhcVar s 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 = mapM_ (warn . berrUnknownVar) moduleName = symbol $ modName env isTarget = isPrefixOfSym moduleName . stripParensSym . val . fst warn x = tell [x] mkVarSpec :: (Var, LocSymbol, BareType) -> BareM (Var, Located SpecType) mkVarSpec (v, Loc l _, b) = tx <$> mkSpecType l b where tx = (v,) . Loc l . generalize plugHoles tce tyi x f t (Loc l st) = Loc l $ mkArrow αs ps' (ls1 ++ ls2) cs' $ go rt' st''' where (αs, _, ls1, rt) = bkUniv (ofType t :: SpecType) (cs, rt') = bkClass rt (_, ps, ls2, st') = bkUniv st (_, st'') = bkClass st' cs' = [(dummySymbol, RCls c t) | (c,t) <- cs] tyvsmap = vmap $ execState (mapTyVars (toType rt') st'') initvmap initvmap = initMapSt $ ErrMismatch (sourcePosSrcSpan l) (pprint x) t st su = [(y, rTyVar x) | (x, y) <- tyvsmap] st''' = subts su st'' ps' = fmap (subts su') <$> ps su' = [(y, RVar (rTyVar x) ()) | (x, y) <- tyvsmap] :: [(RTyVar, RSort)] go t (RHole r) = (addHoles t') { rt_reft = f r } where t' = everywhere (mkT $ addRefs tce tyi) t addHoles = fmap (const $ f $ uReft ("v", [hole])) go (RVar _ _) v@(RVar _ _) = v go (RFun _ i o _) (RFun x i' o' r) = RFun x (go i i') (go o o') r go (RAllT _ t) (RAllT a t') = RAllT a $ go t t' go t (RAllE b a t') = RAllE b a $ go t t' go t (REx b x t') = REx b x $ go t t' go (RAppTy t1 t2 _) (RAppTy t1' t2' r) = RAppTy (go t1 t1') (go t2 t2') r go (RApp _ t _ _) (RApp c t' p r) = RApp c (zipWith go t t') p r go (RCls _ t) (RCls c t') = RCls c $ zipWith go t t' go t st = Ex.throw err where err = errOther $ text msg msg = printf "plugHoles: unhandled case!\nt = %s\nst = %s\n" (showpp t) (showpp st) addRefs :: TCEmb TyCon -> M.HashMap TyCon RTyCon -> SpecType -> SpecType addRefs tce tyi (RApp c ts _ r) = RApp c' ts ps r where RApp c' _ ps _ = addTyConInfo tce tyi (RApp c ts [] r) ps' = safeZip "addRefHoles" ps (rTyConPVs c') addRefs _ _ t = t showTopLevelVars vs = forM vs $ \v -> when (isExportedId v) $ donePhase Loud ("Exported: " ++ showPpr v) ---------------------------------------------------------------------- makeTyConEmbeds (mod, spec) = inModule mod $ makeTyConEmbeds' $ Ms.embeds spec makeTyConEmbeds' :: TCEmb (Located Symbol) -> BareM (TCEmb TyCon) makeTyConEmbeds' z = M.fromList <$> mapM tx (M.toList z) where tx (c, y) = (, y) <$> lookupGhcTyCon c makeIAliases (mod, spec) = inModule mod $ makeIAliases' $ Ms.ialiases spec makeIAliases' :: [(Located BareType, Located BareType)] -> BareM [(Located SpecType, Located SpecType)] makeIAliases' ts = mapM mkIA ts where mkIA (t1, t2) = liftM2 (,) (mkI t1) (mkI t2) mkI (Loc l t) = (Loc l) . generalize <$> mkSpecType l t 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 l t mkSpecType l t = mkSpecType' l (ty_preds $ toRTypeRep t) t mkSpecType' :: SourcePos -> [PVar BSort] -> BareType -> BareM SpecType mkSpecType' l πs = expandRTAlias l . txParams subvUReft (uPVar <$> πs) -- WTF does this function do? makeSymbols vs xs' xts yts ivs = do svs <- gets varEnv return [ (x,v') | (x,v) <- svs, x `elem` xs, let (v',_,_) = joinVar vs (v,x,x)] where xs = sortNub $ zs ++ zs' ++ zs'' zs = concatMap freeSymbols (snd <$> xts) `sortDiff` xs' zs' = concatMap freeSymbols (snd <$> yts) `sortDiff` xs' zs'' = concatMap freeSymbols ivs `sortDiff` xs' freeSymbols ty = sortNub $ concat $ efoldReft (\_ _ -> []) (\ _ -> ()) f (\_ -> id) 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 Symbolic a => GhcLookup a where lookupName :: HscEnv -> ModName -> a -> IO [Name] srcSpan :: a -> SrcSpan instance GhcLookup (Located Symbol) where lookupName e m = symbolLookup e m . val srcSpan = sourcePosSrcSpan . loc instance GhcLookup Name where lookupName _ _ = return . (:[]) srcSpan = nameSrcSpan -- lookupGhcThing :: (GhcLookup a) => String -> (TyThing -> Maybe b) -> a -> BareM b lookupGhcThing name f x = do zs <- lookupGhcThing' name f x case zs of Just x' -> return x' Nothing -> throwError $ ErrGhc (srcSpan x) (text msg) where msg = "Not in scope: " ++ name ++ " `" ++ symbolString (symbol x) ++ "'" -- lookupGhcThing' :: (GhcLookup a) => String -> (TyThing -> Maybe b) -> a -> BareM (Maybe b) lookupGhcThing' _ f x = do (BE mod _ _ _ env) <- get ns <- liftIO $ lookupName env mod x mts <- liftIO $ mapM (fmap (join . fmap f) . hscTcRcLookupName env) ns case catMaybes mts of [] -> return Nothing (t:_) -> return $ Just t symbolLookup :: HscEnv -> ModName -> Symbol -> IO [Name] symbolLookup env mod k | k `M.member` wiredIn = return $ maybeToList $ M.lookup k wiredIn | otherwise = symbolLookupEnv env mod k symbolLookupEnv env mod s | isSrcImport mod = do let modName = getModName mod L _ rn <- hscParseIdentifier env $ symbolString s res <- lookupRdrName env modName rn -- 'hscParseIdentifier' defaults constructors to 'DataCon's, but we also -- need to get the 'TyCon's for declarations like @data Foo = Foo Int@. res' <- lookupRdrName env modName (setRdrNameSpace rn tcName) return $ catMaybes [res, res'] | otherwise = do L _ rn <- hscParseIdentifier env $ symbolString s (_, lookupres) <- tcRnLookupRdrName env rn case lookupres of Just ns -> return ns _ -> return [] -- | 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 'Name's to 'Var's and prefer pulling 'Var's from it. lookupGhcVar :: GhcLookup a => a -> BareM Var lookupGhcVar x = do env <- gets varEnv case L.lookup (symbol x) env of Nothing -> lookupGhcThing "variable" fv x Just v -> return v where fv (AnId x) = Just x fv (AConLike (RealDataCon x)) = Just $ dataConWorkId x fv _ = Nothing lookupGhcTyCon :: GhcLookup a => a -> BareM TyCon lookupGhcTyCon s = (lookupGhcThing "type constructor or class" ftc s) `catchError` (tryPropTyCon s) where ftc (ATyCon x) = Just x ftc _ = Nothing tryPropTyCon s e | sx == propConName = return propTyCon | sx == hpropConName = return hpropTyCon | otherwise = throwError e where sx = symbol s lookupGhcClass = lookupGhcThing "class" ftc where ftc (ATyCon x) = tyConClass_maybe x ftc _ = Nothing lookupGhcDataCon dc = case isTupleDC $ val dc of Just n -> return $ tupleCon BoxedTuple n Nothing -> lookupGhcDataCon' dc isTupleDC zs | "(," `isPrefixOfSym` zs = Just $ lengthSym zs - 1 | otherwise = Nothing lookupGhcDataCon' = lookupGhcThing "data constructor" fdc where fdc (AConLike (RealDataCon x)) = Just x fdc _ = Nothing wiredIn :: M.HashMap Symbol Name wiredIn = M.fromList $ special ++ wiredIns where wiredIns = [ (symbol n, n) | thing <- wiredInThings, let n = getName thing ] special = [ ("GHC.Integer.smallInteger", smallIntegerName) , ("GHC.Num.fromInteger" , fromIntegerName ) ] class Resolvable a where resolve :: SourcePos -> a -> BareM a instance Resolvable a => Resolvable [a] where resolve = mapM . resolve instance Resolvable Qualifier where resolve _ (Q n ps b l) = Q n <$> mapM (secondM (resolve l)) ps <*> resolve l b <*> return l instance Resolvable Pred where resolve l (PAnd ps) = PAnd <$> resolve l ps resolve l (POr ps) = POr <$> resolve l ps resolve l (PNot p) = PNot <$> resolve l p resolve l (PImp p q) = PImp <$> resolve l p <*> resolve l q resolve l (PIff p q) = PIff <$> resolve l p <*> resolve l q resolve l (PBexp b) = PBexp <$> resolve l b resolve l (PAtom r e1 e2) = PAtom r <$> resolve l e1 <*> resolve l e2 resolve l (PAll vs p) = PAll <$> mapM (secondM (resolve l)) vs <*> resolve l p resolve _ p = return p instance Resolvable Expr where resolve l (EVar s) = EVar <$> resolve l s resolve l (EApp s es) = EApp <$> resolve l s <*> resolve l es resolve l (EBin o e1 e2) = EBin o <$> resolve l e1 <*> resolve l e2 resolve l (EIte p e1 e2) = EIte <$> resolve l p <*> resolve l e1 <*> resolve l e2 resolve l (ECst x s) = ECst <$> resolve l x <*> resolve l s resolve l x = return x instance Resolvable LocSymbol where resolve _ ls@(Loc l s) | s `elem` prims = return ls | otherwise = do env <- gets (typeAliases . rtEnv) case M.lookup s env of Nothing | isCon s -> do v <- lookupGhcVar $ Loc l s let qs = symbol v addSym (qs,v) return $ Loc l qs _ -> return ls isCon c | Just (c,cs) <- T.uncons $ symbolText c = isUpper c | otherwise = False instance Resolvable Symbol where resolve l x = fmap val $ resolve l $ Loc l x 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 l (FFunc i ss) = FFunc i <$> resolve l ss resolve _ (FApp tc ss) | tcs' `elem` prims = FApp tc <$> ss' | otherwise = FApp <$> (symbolFTycon.Loc l.symbol <$> lookupGhcTyCon tcs) <*> ss' where tcs@(Loc l tcs') = fTyconSymbol tc ss' = resolve l ss instance Resolvable (UReft Reft) where resolve l (U r p s) = U <$> resolve l r <*> resolve l p <*> return s instance Resolvable Reft where resolve l (Reft (s, ras)) = Reft . (s,) <$> mapM resolveRefa ras where resolveRefa (RConc p) = RConc <$> resolve l p resolveRefa kv = return kv instance Resolvable Predicate where resolve l (Pr pvs) = Pr <$> resolve l pvs instance (Resolvable t) => Resolvable (PVar t) where resolve l (PV n t v as) = PV n t v <$> mapM (third3M (resolve l)) as instance Resolvable () where resolve l = return -------------------------------------------------------------------- ------ Predicate Types for WiredIns -------------------------------- -------------------------------------------------------------------- maxArity :: Arity maxArity = 7 wiredTyCons = fst wiredTyDataCons wiredDataCons = snd wiredTyDataCons wiredTyDataCons :: ([(TyCon, TyConP)] , [(DataCon, Located DataConP)]) wiredTyDataCons = (concat tcs, mapSnd dummyLoc <$> concat dcs) where (tcs, dcs) = unzip l l = [listTyDataCons] ++ map tupleTyDataCons [2..maxArity] listTyDataCons :: ([(TyCon, TyConP)] , [(DataCon, DataConP)]) listTyDataCons = ( [(c, TyConP [(RTV tyv)] [p] [] [0] [] (Just fsize))] , [(nilDataCon, DataConP l0 [(RTV tyv)] [p] [] [] [] lt) , (consDataCon, DataConP l0 [(RTV tyv)] [p] [] [] cargs lt)]) where l0 = dummyPos "LH.Bare.listTyDataCons" c = listTyCon [tyv] = tyConTyVars c t = rVar tyv :: RSort fld = "fldList" x = "xListSelector" xs = "xsListSelector" p = PV "p" (PVProp t) (vv Nothing) [(t, fld, EVar fld)] px = pdVarReft $ PV "p" (PVProp t) (vv Nothing) [(t, fld, EVar x)] lt = rApp c [xt] [RPropP [] $ pdVarReft p] mempty xt = rVar tyv xst = rApp c [RVar (RTV tyv) px] [RPropP [] $ pdVarReft p] mempty cargs = [(xs, xst), (x, xt)] fsize = \x -> EApp (dummyLoc "len") [EVar x] tupleTyDataCons :: Int -> ([(TyCon, TyConP)] , [(DataCon, DataConP)]) tupleTyDataCons n = ( [(c, TyConP (RTV <$> tyvs) ps [] [0..(n-2)] [] Nothing)] , [(dc, DataConP l0 (RTV <$> tyvs) ps [] [] cargs lt)]) where l0 = dummyPos "LH.Bare.tupleTyDataCons" c = tupleTyCon BoxedTuple n dc = tupleCon BoxedTuple n tyvs@(tv:tvs) = tyConTyVars c (ta:ts) = (rVar <$> tyvs) :: [RSort] flds = mks "fld_Tuple" fld = "fld_Tuple" x1:xs = mks ("x_Tuple" ++ show n) 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) (RPropP [] . pdVarReft <$> ups) mempty 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 -> symbol (x++ show i)) <$> [1..n] mks_ x = (\i -> symbol (x++ show i)) <$> [2..n] pdVarReft = (\p -> U mempty p mempty) . pdVar mkps ns (t:ts) ((f,x):fxs) = reverse $ mkps_ 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 (PVProp t) (vv Nothing) args a = (t, f, x) mkps_ _ _ _ _ _ = error "Bare : mkps_" ------------------------------------------------------------------------ -- | Transforming Raw Strings using GHC Env ---------------------------- ------------------------------------------------------------------------ ofBareType :: (PPrint r, Reftable r) => BRType r -> BareM (RRType r) ------------------------------------------------------------------------ ofBareType (RVar a r) = return $ RVar (symbolRTyVar a) r ofBareType (RFun x t1 t2 _) = liftM2 (rFun x) (ofBareType t1) (ofBareType t2) ofBareType t@(RAppTy t1 t2 r) = liftM3 RAppTy (ofBareType t1) (ofBareType t2) (return r) 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 (symbolRTyVar a)) (ofBareType t) ofBareType (RAllP π t) = liftM2 RAllP (ofBPVar π) (ofBareType t) ofBareType (RAllS s t) = liftM (RAllS s) (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 (RHole r) = return $ RHole r ofBareType t = errorstar $ "Bare : ofBareType cannot handle " ++ show t ofRef (RProp ss t) = RProp <$> mapM ofSyms ss <*> ofBareType t ofRef (RPropP ss r) = (`RPropP` r) <$> mapM ofSyms ss ofRef (RHProp _ _) = errorstar "TODO:EFFECTS:ofRef" ofSyms (x, t) = liftM ((,) x) (ofBareType t) tyApp (RApp c ts rs r) ts' rs' r' = RApp c (ts ++ ts') (rs ++ rs') (r `meet` r') tyApp t [] [] r = t `strengthen` r bareTCApp _ r c rs ts | Just (SynonymTyCon rhs) <- synTyConRhs_maybe c = tyApp (subsTyVars_meet su $ ofType rhs) (drop nts ts) rs r where tvs = tyConTyVars c su = zipWith (\a t -> (rTyVar a, toRSort t, t)) tvs ts nts = length tvs -- TODO expandTypeSynonyms here to bareTCApp _ r c rs ts | isFamilyTyCon c && isTrivial t = expandRTypeSynonyms $ t `strengthen` r where t = rApp c ts rs mempty bareTCApp _ r c rs ts = rApp c ts rs r expandRTypeSynonyms = ofType . expandTypeSynonyms . toType symbolRTyVar = rTyVar . stringTyVar . symbolString -- stringTyVarTy = TyVarTy . stringTyVar mkMeasureDCon :: Ms.MSpec t LocSymbol -> BareM (Ms.MSpec t DataCon) mkMeasureDCon m = (forM (measureCtors m) $ \n -> (val n,) <$> lookupGhcDataCon n) >>= (return . mkMeasureDCon_ m) mkMeasureDCon_ :: Ms.MSpec t LocSymbol -> [(Symbol, DataCon)] -> Ms.MSpec t DataCon mkMeasureDCon_ m ndcs = m' {Ms.ctorMap = cm'} where m' = fmap (tx.val) m cm' = hashMapMapKeys (tx' . tx) $ Ms.ctorMap m' tx = mlookup (M.fromList ndcs) tx' = dataConSymbol measureCtors :: Ms.MSpec t LocSymbol -> [LocSymbol] measureCtors = sortNub . fmap 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 c mm cm im) = Ms.MSpec c <$> forM mm tx <*> forM cm tx <*> forM im tx where tx m = liftM (\s' -> m {sort = s'}) (ofBareType (sort m)) ----------------------------------------------------------------------- -- | LH Primitive TyCons ---------------------------------------------- ----------------------------------------------------------------------- propTyCon, hpropTyCon :: TyCon propTyCon = symbolTyCon 'w' 24 propConName hpropTyCon = symbolTyCon 'w' 24 hpropConName ----------------------------------------------------------------------- ---------------- Bare Predicate: DataCon Definitions ------------------ ----------------------------------------------------------------------- makeConTypes (name,spec) = inModule name $ makeConTypes' $ Ms.dataDecls spec makeConTypes' :: [DataDecl] -> BareM ([(TyCon, TyConP)], [[(DataCon, Located DataConP)]]) makeConTypes' dcs = unzip <$> mapM ofBDataDecl dcs ofBDataDecl :: DataDecl -> BareM ((TyCon, TyConP), [(DataCon, Located DataConP)]) ofBDataDecl (D tc as ps ls cts pos sfun) = do πs <- mapM ofBPVar ps tc' <- lookupGhcTyCon tc cts' <- mapM (ofBDataCon lc tc' αs ps ls πs) cts let tys = [t | (_, dcp) <- cts', (_, t) <- tyArgs dcp] let initmap = zip (uPVar <$> πs) [0..] let varInfo = concatMap (getPsSig initmap True) tys let neutral = [0 .. (length πs)] L.\\ (fst <$> varInfo) let cov = neutral ++ [i | (i, b)<- varInfo, b, i >=0] let contr = neutral ++ [i | (i, b)<- varInfo, not b, i >=0] return ((tc', TyConP αs πs ls cov contr sfun), (mapSnd (Loc lc) <$> cts')) where αs = RTV . symbolTyVar <$> as lc = loc tc 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 (RPropP _ r) = addps m pos r getPsSigPs m pos (RProp _ t) = getPsSig m pos t getPsSigPs _ _ (RHProp _ _) = errorstar "TODO:EFFECTS:getPsSigPs" 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 . symbolTyVar) (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 v txys) = do t' <- forM t f txys' <- mapM (\(t, x, y) -> liftM (, x, y) (f t)) txys return $ PV x t' v txys' -- TODO:EFFECTS:ofBDataCon ofBDataCon l tc αs ps ls πs (c, xts) = do c' <- lookupGhcDataCon c ts' <- mapM (mkSpecType' l ps) ts let cs = map ofType (dataConStupidTheta c') let t0 = rApp tc rs (RPropP [] . pdVarReft <$> πs) mempty return $ (c', DataConP l αs πs ls cs (reverse (zip xs ts')) t0) where (xs, ts) = unzip xts rs = [rVar α | RTV α <- α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 . ty_preds . toRTypeRep -- rtypePredBinds t = everything (++) ([] `mkQ` grab) t -- where grab ((RAllP pv _) :: BRType RPVar RPredicate) = [pv] -- grab _ = [] ---------------------------------------------------------------------------------------------- ----- Checking GhcSpec ----------------------------------------------------------------------- ---------------------------------------------------------------------------------------------- checkGhcSpec :: [(ModName, Ms.BareSpec)] -> GhcSpec -> Either [Error] GhcSpec checkGhcSpec specs sp = applyNonNull (Right sp) Left errors where errors = mapMaybe (checkBind "constructor" emb tcEnv env) (dcons sp) ++ mapMaybe (checkBind "measure" emb tcEnv env) (measSpec sp) ++ mapMaybe (checkInv emb tcEnv env) (invariants sp) ++ (checkIAl emb tcEnv env) (ialiases sp) ++ checkMeasures emb env ms ++ mapMaybe checkMismatch sigs ++ checkDuplicate (tySigs sp) ++ checkDuplicate (asmSigs sp) ++ checkDupIntersect (tySigs sp) (asmSigs sp) ++ checkRTAliases "Type Alias" env tAliases ++ checkRTAliases "Pred Alias" env pAliases -- ++ checkDuplicateRTAlias "Predicate Alias" pAliases -- ++ checkRTAliasSyms "Predicate Alias" (concat [Ms.paliases sp | (_, sp) <- specs]) tAliases = concat [Ms.aliases sp | (_, sp) <- specs] pAliases = concat [Ms.paliases sp | (_, sp) <- specs] dcons spec = [ (v, Loc l dc) | (v, dc) <- dataConSpec (dconsP spec), let l = getSourcePos v ] emb = tcEmbeds sp env = ghcSpecEnv sp tcEnv = tyconEnv sp ms = measures sp measSpec sp = [(x, uRType <$> t) | (x, t) <- meas sp] sigs = tySigs sp ++ asmSigs sp type ReplaceM = ReaderT ( M.HashMap Symbol Symbol , SEnv SortedReft , TCEmb TyCon , M.HashMap TyCon RTyCon ) (State ( M.HashMap Var (Located SpecType) , M.HashMap Var [Expr] )) replaceLocalBinds :: TCEmb TyCon -> M.HashMap TyCon RTyCon -> [(Var, Located SpecType)] -> [(Var, [Expr])] -> SEnv SortedReft -> CoreProgram -> ([(Var, Located SpecType)], [(Var, [Expr])]) replaceLocalBinds emb tyi sigs texprs senv cbs = (M.toList s, M.toList t) where (s,t) = execState (runReaderT (mapM_ (`traverseBinds` return ()) cbs) (M.empty, senv, emb, tyi)) (M.fromList sigs, M.fromList texprs) traverseExprs (Let b e) = traverseBinds b (traverseExprs e) traverseExprs (Lam _ e) = traverseExprs e traverseExprs (App x y) = traverseExprs x >> traverseExprs y traverseExprs (Case e _ _ as) = traverseExprs e >> mapM_ (traverseExprs . thd3) as traverseExprs (Cast e _) = traverseExprs e traverseExprs (Tick _ e) = traverseExprs e traverseExprs _ = return () traverseBinds b k = do (env', fenv', emb, tyi) <- ask let env = L.foldl' (\m v -> M.insert (takeWhileSym (/='#') $ symbol v) (symbol v) m) env' vs fenv = L.foldl' (\m v -> insertSEnv (symbol v) (rTypeSortedReft emb (ofType $ varType v :: RSort)) m) fenv' vs withReaderT (const (env,fenv,emb,tyi)) $ do mapM_ replaceLocalBindsOne vs mapM_ traverseExprs es k where vs = bindersOf b es = rhssOfBind b replaceLocalBindsOne :: Var -> ReplaceM () replaceLocalBindsOne v = do mt <- gets (M.lookup v . fst) case mt of Nothing -> return () Just (Loc l (toRTypeRep -> t@(RTypeRep {..}))) -> do (env',fenv,emb,tyi) <- ask let f m k = M.lookupDefault k k m let (env,args) = L.mapAccumL (\e (v,t) -> (M.insert v v e, substa (f e) t)) env' (zip ty_binds ty_args) let res = substa (f env) ty_res let t' = fromRTypeRep $ t { ty_args = args, ty_res = res } let msg = ErrTySpec (sourcePosSrcSpan l) (pprint v) t' case checkTy msg emb tyi fenv t' of Just err -> Ex.throw err Nothing -> modify (first $ M.insert v (Loc l t')) mes <- gets (M.lookup v . snd) case mes of Nothing -> return () Just es -> do let es' = substa (f env) es case checkExpr "termination" emb fenv (v, Loc l t', es') of Just err -> Ex.throw err Nothing -> modify (second $ M.insert v es') checkInv :: TCEmb TyCon -> TCEnv -> SEnv SortedReft -> Located SpecType -> Maybe Error checkInv emb tcEnv env t = checkTy err emb tcEnv env (val t) where err = ErrInvt (sourcePosSrcSpan $ loc t) (val t) checkIAl :: TCEmb TyCon -> TCEnv -> SEnv SortedReft -> [(Located SpecType, Located SpecType)] -> [Error] checkIAl emb tcEnv env ials = catMaybes $ concatMap (checkIAlOne emb tcEnv env) ials checkIAlOne emb tcEnv env (t1, t2) = checkEq : (tcheck <$> [t1, t2]) where tcheck t = checkTy (err t) emb tcEnv env (val t) err t = ErrIAl (sourcePosSrcSpan $ loc t) (val t) t1' :: RSort t1' = toRSort $ val t1 t2' :: RSort t2' = toRSort $ val t2 checkEq = if (t1' == t2') then Nothing else Just errmis errmis = ErrIAlMis (sourcePosSrcSpan $ loc t1) (val t1) (val t2) emsg emsg = pprint t1 <+> text "does not match with" <+> pprint t2 checkRTAliases msg env as = err1s -- ++ err2s where err1s = checkDuplicateRTAlias msg as err2s = concatMap (checkRTAliasWF env) as checkRTAliasWF env a = {- trace ("checkRTAliasWF: " ++ rtName a) $ -} mkErr <$> filter (not . ok) aSyms where aSyms = {- traceShow ("RTAWF: " ++ aName) $ -} syms $ rtBody a ok x = memberSEnv x env || x `elem` params params = symbol <$> rtVArgs a mkErr = ErrUnbound sp . pprint sp = sourcePosSrcSpan (rtPos a) aName = rtName a checkBind :: (PPrint v) => String -> TCEmb TyCon -> TCEnv -> SEnv SortedReft -> (v, Located SpecType) -> Maybe Error checkBind s emb tcEnv env (v, Loc l t) = checkTy msg emb tcEnv env' t where msg = ErrTySpec (sourcePosSrcSpan l) (text s <+> pprint v) t env' = foldl (\e (x, s) -> insertSEnv x (RR s mempty) e) env wiredSortedSyms checkExpr :: (Eq v, PPrint v) => String -> TCEmb TyCon -> SEnv SortedReft -> (v, Located SpecType, [Expr])-> Maybe Error checkExpr s emb env (v, Loc l t, es) = mkErr <$> go es where mkErr = ErrTySpec (sourcePosSrcSpan l) (text s <+> pprint v) t go = foldl (\err e -> err <|> checkSorted env' e) Nothing env' = foldl (\e (x, s) -> insertSEnv x s e) env'' wiredSortedSyms env'' = mapSEnv sr_sort $ foldl (\e (x,s) -> insertSEnv x s e) env xss xss = mapSnd rSort <$> (uncurry zip $ dropThd3 $ bkArrowDeep t) rSort = rTypeSortedReft emb msg = "Bare.checkExpr " ++ showpp v ++ " not found\n" ++ "\t Try give a haskell type signature to the recursive function" checkTy :: (Doc -> Error) -> TCEmb TyCon -> TCEnv -> SEnv SortedReft -> SpecType -> Maybe Error checkTy mkE emb tcEnv env t = mkE <$> checkRType emb env (txRefSort tcEnv emb t) checkDupIntersect :: [(Var, Located SpecType)] -> [(Var, Located SpecType)] -> [Error] checkDupIntersect xts mxts = concatMap mkWrn dups where mkWrn (x, t) = pprWrn x (sourcePosSrcSpan $ loc t) dups = L.intersectBy (\x y -> (fst x == fst y)) mxts xts pprWrn v l = trace ("WARNING: Assume Overwrites Specifications for "++ show v ++ " : " ++ showPpr l) [] 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 ] checkDuplicateRTAlias :: String -> [RTAlias s a] -> [Error] checkDuplicateRTAlias s tas = mkErr <$> dups where mkErr xs@(x:_) = ErrDupAlias (sourcePosSrcSpan $ rtPos x) (text s) (pprint $ rtName x) (sourcePosSrcSpan . rtPos <$> xs) dups = [z | z@(_:_:_) <- L.groupBy (\x y -> rtName x == rtName y) tas] 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] ++ [(symbol v, rSort t) | (v, Loc _ t) <- ctors sp] ++ [(x, vSort v) | (x, v) <- freeSyms sp, isConLikeId v] rSort = rTypeSortedReft emb vSort = rSort . varRSort varRSort :: Var -> RSort varRSort = ofType . varType errTypeMismatch :: Var -> Located SpecType -> Error errTypeMismatch x t = ErrMismatch (sourcePosSrcSpan $ loc t) (pprint x) (varType x) (val t) ------------------------------------------------------------------------------------------------ -- | @checkRType@ determines 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 insertPEnv env Nothing t where cb c ts = classBinds (RCls c ts) f env me r err = err <|> checkReft env emb me r insertPEnv p γ = insertsSEnv γ (mapSnd (rTypeSortedReft emb) <$> pbinds p) pbinds p = (pname p, pvarRType p :: RSort) : [(x, t) | (t, x, _) <- pargs p] checkReft :: (PPrint r, Reftable r) => SEnv SortedReft -> TCEmb TyCon -> Maybe (RRType r) -> r -> Maybe Doc checkReft env emb Nothing _ = Nothing -- TODO:RPropP/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 env' = foldl (\e (x, s) -> insertSEnv x (RR s mempty) e) env wiredSortedSyms -- 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) --------------------------------------------------------------------------------------------------- -- | @checkMeasures@ determines if a measure definition is wellformed ----------------------------- --------------------------------------------------------------------------------------------------- checkMeasures :: M.HashMap TyCon FTycon -> SEnv SortedReft -> [Measure SpecType DataCon] -> [Error] --------------------------------------------------------------------------------------------------- checkMeasures emb env = concatMap (checkMeasure emb env) checkMeasure :: M.HashMap TyCon FTycon -> SEnv SortedReft -> Measure SpecType DataCon -> [Error] checkMeasure emb γ (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 (Def s c bs body) = checkMBody' emb sort γ' body where γ' = L.foldl' (\γ (x, t) -> insertSEnv x t γ) γ xts xts = zip bs $ rTypeSortedReft emb . subsTyVars_meet su <$> ty_args trep trep = toRTypeRep ct su = checkMBodyUnify (ty_res trep) (head $ snd3 $ bkArrowDeep sort) ct = ofType $ dataConUserType c :: SpecType checkMBodyUnify = go where go (RVar tv _) t = [(tv, toRSort t, t)] go t@(RApp {}) t'@(RApp {}) = concat $ zipWith go (rt_args t) (rt_args t') go _ _ = [] checkMBody' emb sort γ body = case body of E e -> checkSortFull γ (rTypeSort emb sort') e P p -> checkSortFull γ psort p R s p -> checkSortFull (insertSEnv s sty γ) psort p where psort = FApp propFTyCon [] sty = rTypeSortedReft emb sort' sort' = fromRTypeRep $ trep' { ty_vars = [], ty_preds = [], ty_labels = [] , ty_binds = tail $ ty_binds trep' , ty_args = tail $ ty_args trep' } trep' = toRTypeRep sort ------------------------------------------------------------------------------- -- | 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 <- ty_preds $ toRTypeRep 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 (RAllS s t) = liftM (RAllS s) (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 :: SpecProp -> State ExSt SpecProp expToBindReft (RProp s t) = RProp s <$> expToBindT t expToBindReft (RPropP s r) = RPropP s <$> expToBindRef r expToBindReft (RHProp _ _) = errorstar "TODO:EFFECTS:expToBindReft" 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) l) = mapM expToBind p >>= return . (\p -> U r p l). 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 -> RSort -> State ExSt Expr expToBindExpr e@(EVar s) _ | isLower $ headSym $ symbol s = 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 $ symbol $ "ex#" ++ show n maybeTrue :: NamedThing a => a -> ModName -> NameSet -> RReft -> RReft maybeTrue x target exports r | isInternalName name || inTarget && notExported = r | otherwise = killHoles r where inTarget = moduleName (nameModule name) == getModName target name = getName x notExported = not $ getName x `elemNameSet` exports killHoles r@(U (Reft (v,rs)) _ _) = r { ur_reft = Reft (v, filter (not . isHole) rs) } ------------------------------------------------------------------------------------- -- | Tasteful Error Messages -------------------------------------------------------- ------------------------------------------------------------------------------------- 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)