X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Fghci%2FRtClosureInspect.hs;h=2cbdbe82f4517cdc54dcd7111862fe0923f07717;hb=955789f4fdc14d77063703d9d174353e6d9425a2;hp=0bcc7b2906713904cc0e9a7ce7aaa8f227c300ec;hpb=ecdc15ea7813c43a4d84b7c6554a13c06f210a7e;p=ghc-hetmet.git diff --git a/compiler/ghci/RtClosureInspect.hs b/compiler/ghci/RtClosureInspect.hs index 0bcc7b2..2cbdbe8 100644 --- a/compiler/ghci/RtClosureInspect.hs +++ b/compiler/ghci/RtClosureInspect.hs @@ -23,8 +23,9 @@ module RtClosureInspect( isPointed, isFullyEvaluatedTerm, mapTermType, - termTyVars + termTyVars, -- unsafeDeepSeq, + cvReconstructType ) where #include "HsVersions.h" @@ -375,105 +376,46 @@ repPrim t = rep where | t == tVarPrimTyCon = "" | otherwise = showSDoc (char '<' <> ppr t <> char '>') where build ww = unsafePerformIO $ withArray ww (peek . castPtr) + ----------------------------------- -- Type Reconstruction ----------------------------------- +{- +Type Reconstruction is type inference done on heap closures. +The algorithm walks the heap generating a set of equations, which +are solved with syntactic unification. +A type reconstruction equation looks like: + + = + +The full equation set is generated by traversing all the subterms, starting +from a given term. + +The only difficult part is that newtypes are only found in the lhs of equations. +Right hand sides are missing them. We can either (a) drop them from the lhs, or +(b) reconstruct them in the rhs when possible. + +The function congruenceNewtypes takes a shot at (b) +-} -- The Type Reconstruction monad type TR a = TcM a -runTR :: HscEnv -> TR Term -> IO Term +runTR :: HscEnv -> TR a -> IO a runTR hsc_env c = do mb_term <- initTcPrintErrors hsc_env iNTERACTIVE c case mb_term of Nothing -> panic "Can't unify" - Just term -> return term + Just x -> return x trIO :: IO a -> TR a trIO = liftTcM . ioToTcRn -addConstraint :: TcType -> TcType -> TR () -addConstraint t1 t2 = congruenceNewtypes t1 t2 >>= uncurry unifyType - -{- - A parallel fold over two Type values, - compensating for missing newtypes on both sides. - This is necessary because newtypes are not present - in runtime, but since sometimes there is evidence - available we do our best to reconstruct them. - Evidence can come from DataCon signatures or - from compile-time type inference. - I am using the words congruence and rewriting - because what we are doing here is an approximation - of unification modulo a set of equations, which would - come from newtype definitions. These should be the - equality coercions seen in System Fc. Rewriting - is performed, taking those equations as rules, - before launching unification. - - It doesn't make sense to rewrite everywhere, - or we would end up with all newtypes. So we rewrite - only in presence of evidence. - The lhs comes from the heap structure of ptrs,nptrs. - The rhs comes from a DataCon type signature. - Rewriting in the rhs is restricted to the result type. - - Note that it is very tricky to make this 'rewriting' - work with the unification implemented by TcM, where - substitutions are 'inlined'. The order in which - constraints are unified is vital for this (or I am - using TcM wrongly). --} -congruenceNewtypes :: TcType -> TcType -> TcM (TcType,TcType) -congruenceNewtypes = go True - where - go rewriteRHS lhs rhs - -- TyVar lhs inductive case - | Just tv <- getTyVar_maybe lhs - = recoverM (return (lhs,rhs)) $ do - Indirect ty_v <- readMetaTyVar tv - (lhs', rhs') <- go rewriteRHS ty_v rhs - writeMutVar (metaTvRef tv) (Indirect lhs') - return (lhs, rhs') - -- TyVar rhs inductive case - | Just tv <- getTyVar_maybe rhs - = recoverM (return (lhs,rhs)) $ do - Indirect ty_v <- readMetaTyVar tv - (lhs', rhs') <- go rewriteRHS lhs ty_v - writeMutVar (metaTvRef tv) (Indirect rhs') - return (lhs', rhs) --- FunTy inductive case - | Just (l1,l2) <- splitFunTy_maybe lhs - , Just (r1,r2) <- splitFunTy_maybe rhs - = do (l2',r2') <- go True l2 r2 - (l1',r1') <- go False l1 r1 - return (mkFunTy l1' l2', mkFunTy r1' r2') --- TyconApp Inductive case; this is the interesting bit. - | Just (tycon_l, args_l) <- splitNewTyConApp_maybe lhs - , Just (tycon_r, args_r) <- splitNewTyConApp_maybe rhs = do - - let (tycon_l',args_l') = if isNewTyCon tycon_r && not(isNewTyCon tycon_l) - then (tycon_r, rewrite tycon_r lhs) - else (tycon_l, args_l) - (tycon_r',args_r') = if rewriteRHS && isNewTyCon tycon_l && not(isNewTyCon tycon_r) - then (tycon_l, rewrite tycon_l rhs) - else (tycon_r, args_r) - (args_l'', args_r'') <- unzip `liftM` zipWithM (go rewriteRHS) args_l' args_r' - return (mkTyConApp tycon_l' args_l'', mkTyConApp tycon_r' args_r'') - - | otherwise = return (lhs,rhs) - - where rewrite newtyped_tc lame_tipe - | (tvs, tipe) <- newTyConRep newtyped_tc - = case tcUnifyTys (const BindMe) [tipe] [lame_tipe] of - Just subst -> substTys subst (map mkTyVarTy tvs) - otherwise -> panic "congruenceNewtypes: Can't unify a newtype" +liftTcM = id newVar :: Kind -> TR TcTyVar newVar = liftTcM . newFlexiTyVar -liftTcM = id - -- | Returns the instantiated type scheme ty', and the substitution sigma -- such that sigma(ty') = ty instScheme :: Type -> TR (TcType, TvSubst) @@ -481,6 +423,12 @@ instScheme ty | (tvs, rho) <- tcSplitForAllTys ty = liftTcM$ do (tvs',theta,ty') <- tcInstType (mapM tcInstTyVar) ty return (ty', zipTopTvSubst tvs' (mkTyVarTys tvs)) +addConstraint :: TcType -> TcType -> TR () +addConstraint t1 t2 = congruenceNewtypes t1 t2 >>= uncurry unifyType + + + +-- Type & Term reconstruction cvObtainTerm :: HscEnv -> Bool -> Maybe Type -> HValue -> IO Term cvObtainTerm hsc_env force mb_ty hval = runTR hsc_env $ do tv <- liftM mkTyVarTy (newVar argTypeKind) @@ -534,12 +482,6 @@ cvObtainTerm hsc_env force mb_ty hval = runTR hsc_env $ do otherwise -> return (Suspension (tipe clos) (Just tv) a Nothing) --- Access the array of pointers and recurse down. Needs to be done with --- care of no introducing a thunk! or go will fail to do its job - appArr f arr (I# i#) = case arr of - (Array _ _ ptrs#) -> case indexArray# ptrs# i# of - (# e #) -> f e - matchSubTypes dc ty | Just (_,ty_args) <- splitTyConApp_maybe (repType ty) , null (dataConExTyVars dc) --TODO Handle the case of extra existential tyvars @@ -558,69 +500,157 @@ cvObtainTerm hsc_env force mb_ty hval = runTR hsc_env $ do , ptext SLIT("reOrderTerms") $$ (ppr pointed $$ ppr unpointed)) head unpointed : reOrderTerms pointed (tail unpointed) tys -isMonomorphic ty | isForAllTy ty = False -isMonomorphic ty = (isEmptyVarSet . tyVarsOfType) ty - -zonkTerm :: Term -> TcM Term -zonkTerm = foldTerm idTermFoldM { - fTerm = \ty dc v tt -> sequence tt >>= \tt -> - zonkTcType ty >>= \ty' -> - return (Term ty' dc v tt) - ,fSuspension = \ct ty v b -> fmapMMaybe zonkTcType ty >>= \ty -> - return (Suspension ct ty v b)} - --- Is this defined elsewhere? --- Generalize the type: find all free tyvars and wrap in the appropiate ForAll. -sigmaType ty = mkForAllTys (varSetElems$ tyVarsOfType (dropForAlls ty)) ty -{- -Example of Type Reconstruction --------------------------------- -Suppose we have an existential type such as +-- Fast, breadth-first version of obtainTerm that deals only with type reconstruction -data Opaque = forall a. Opaque a - -And we have a term built as: - -t = Opaque (map Just [[1,1],[2,2]]) +cvReconstructType :: HscEnv -> Bool -> Maybe Type -> HValue -> IO Type +cvReconstructType hsc_env force mb_ty hval = runTR hsc_env $ do + tv <- liftM mkTyVarTy (newVar argTypeKind) + case mb_ty of + Nothing -> search (isMonomorphic `fmap` zonkTcType tv) (++) [(tv, hval)] >> + zonkTcType tv -- TODO untested! + Just ty | isMonomorphic ty -> return ty + Just ty -> do + (ty',rev_subst) <- instScheme (sigmaType ty) + addConstraint tv ty' + search (isMonomorphic `fmap` zonkTcType tv) (++) [(tv, hval)] + substTy rev_subst `fmap` zonkTcType tv + where +-- search :: m Bool -> ([a] -> [a] -> [a]) -> [a] -> m () + search stop combine [] = return () + search stop combine ((t,a):jj) = (jj `combine`) `fmap` go t a >>= + unlessM stop . search stop combine + + -- returns unification tasks, since we are going to want a breadth-first search + go :: Type -> HValue -> TR [(Type, HValue)] + go tv a = do + clos <- trIO $ getClosureData a + case tipe clos of + Indirection _ -> go tv $! (ptrs clos ! 0) + Constr -> do + m_dc <- trIO$ tcRnRecoverDataCon hsc_env (infoPtr clos) + case m_dc of + Nothing -> panic "Can't find the DataCon for a term" + Just dc -> do + let extra_args = length(dataConRepArgTys dc) - length(dataConOrigArgTys dc) + subTtypes <- mapMif (not . isMonomorphic) + (\t -> mkTyVarTy `fmap` newVar (typeKind t)) + (dataConRepArgTys dc) + -- It is vital for newtype reconstruction that the unification step is done + -- right here, _before_ the subterms are RTTI reconstructed. + let myType = mkFunTys subTtypes tv + fst `fmap` instScheme(dataConRepType dc) >>= addConstraint myType + return $map (\(I# i#,t) -> case ptrs clos of + (Array _ _ ptrs#) -> case indexArray# ptrs# i# of + (# e #) -> (t,e)) + (drop extra_args $ zip [0..] subTtypes) + otherwise -> return [] -The type of t as far as the typechecker goes is t :: Opaque -If we seq the head of t, we obtain: -t - O (_1::a) +-- Dealing with newtypes +{- + A parallel fold over two Type values, + compensating for missing newtypes on both sides. + This is necessary because newtypes are not present + in runtime, but since sometimes there is evidence + available we do our best to reconstruct them. + Evidence can come from DataCon signatures or + from compile-time type inference. + I am using the words congruence and rewriting + because what we are doing here is an approximation + of unification modulo a set of equations, which would + come from newtype definitions. These should be the + equality coercions seen in System Fc. Rewriting + is performed, taking those equations as rules, + before launching unification. -seq _1 () + It doesn't make sense to rewrite everywhere, + or we would end up with all newtypes. So we rewrite + only in presence of evidence. + The lhs comes from the heap structure of ptrs,nptrs. + The rhs comes from a DataCon type signature. + Rewriting in the rhs is restricted to the result type. -t - O ( (_3::b) : (_4::[b]) ) + Note that it is very tricky to make this 'rewriting' + work with the unification implemented by TcM, where + substitutions are 'inlined'. The order in which + constraints are unified is vital for this (or I am + using TcM wrongly). +-} +congruenceNewtypes :: TcType -> TcType -> TcM (TcType,TcType) +congruenceNewtypes = go True + where + go rewriteRHS lhs rhs + -- TyVar lhs inductive case + | Just tv <- getTyVar_maybe lhs + = recoverM (return (lhs,rhs)) $ do + Indirect ty_v <- readMetaTyVar tv + (lhs', rhs') <- go rewriteRHS ty_v rhs + writeMutVar (metaTvRef tv) (Indirect lhs') + return (lhs, rhs') + -- TyVar rhs inductive case + | Just tv <- getTyVar_maybe rhs + = recoverM (return (lhs,rhs)) $ do + Indirect ty_v <- readMetaTyVar tv + (lhs', rhs') <- go rewriteRHS lhs ty_v + writeMutVar (metaTvRef tv) (Indirect rhs') + return (lhs', rhs) +-- FunTy inductive case + | Just (l1,l2) <- splitFunTy_maybe lhs + , Just (r1,r2) <- splitFunTy_maybe rhs + = do (l2',r2') <- go True l2 r2 + (l1',r1') <- go False l1 r1 + return (mkFunTy l1' l2', mkFunTy r1' r2') +-- TyconApp Inductive case; this is the interesting bit. + | Just (tycon_l, args_l) <- splitNewTyConApp_maybe lhs + , Just (tycon_r, args_r) <- splitNewTyConApp_maybe rhs = do -seq _3 () + let (tycon_l',args_l') = if isNewTyCon tycon_r && not(isNewTyCon tycon_l) + then (tycon_r, rewrite tycon_r lhs) + else (tycon_l, args_l) + (tycon_r',args_r') = if rewriteRHS && isNewTyCon tycon_l && not(isNewTyCon tycon_r) + then (tycon_l, rewrite tycon_l rhs) + else (tycon_r, args_r) + (args_l'', args_r'') <- unzip `liftM` zipWithM (go rewriteRHS) args_l' args_r' + return (mkTyConApp tycon_l' args_l'', mkTyConApp tycon_r' args_r'') -t - O ( (Just (_5::c)) : (_4::[b]) ) + | otherwise = return (lhs,rhs) -At this point, we know that b = (Maybe c) + where rewrite newtyped_tc lame_tipe + | (tvs, tipe) <- newTyConRep newtyped_tc + = case tcUnifyTys (const BindMe) [tipe] [lame_tipe] of + Just subst -> substTys subst (map mkTyVarTy tvs) + otherwise -> panic "congruenceNewtypes: Can't unify a newtype" -seq _5 () -t - O ( (Just ((_6::d) : (_7::[d]) )) : (_4::[b]) ) +------------------------------------------------------------------------------------ -At this point, we know that c = [d] +isMonomorphic ty | (tvs, ty') <- splitForAllTys ty + = null tvs && (isEmptyVarSet . tyVarsOfType) ty' -seq _6 () +mapMif :: Monad m => (a -> Bool) -> (a -> m a) -> [a] -> m [a] +mapMif pred f xx = sequence $ mapMif_ pred f xx +mapMif_ pred f [] = [] +mapMif_ pred f (x:xx) = (if pred x then f x else return x) : mapMif_ pred f xx -t - O ( (Just (1 : (_7::[d]) )) : (_4::[b]) ) +unlessM condM acc = condM >>= \c -> unless c acc -At this point, we know that d = Integer +-- Strict application of f at index i +appArr f (Array _ _ ptrs#) (I# i#) = case indexArray# ptrs# i# of + (# e #) -> f e -The fully reconstructed expressions, with propagation, would be: +zonkTerm :: Term -> TcM Term +zonkTerm = foldTerm idTermFoldM { + fTerm = \ty dc v tt -> sequence tt >>= \tt -> + zonkTcType ty >>= \ty' -> + return (Term ty' dc v tt) + ,fSuspension = \ct ty v b -> fmapMMaybe zonkTcType ty >>= \ty -> + return (Suspension ct ty v b)} -t - O ( (Just (_5::c)) : (_4::[Maybe c]) ) -t - O ( (Just ((_6::d) : (_7::[d]) )) : (_4::[Maybe [d]]) ) -t - O ( (Just (1 : (_7::[Integer]) )) : (_4::[Maybe [Integer]]) ) +-- Is this defined elsewhere? +-- Generalize the type: find all free tyvars and wrap in the appropiate ForAll. +sigmaType ty = mkForAllTys (varSetElems$ tyVarsOfType (dropForAlls ty)) ty -For reference, the type of the thing inside the opaque is -map Just [[1,1],[2,2]] :: [Maybe [Integer]] -NOTE: (Num t) contexts have been manually replaced by Integer for clarity --}