From ae4c8ca48b93b0063bcc66aeee43a1243426e8ed Mon Sep 17 00:00:00 2001 From: Pepe Iborra Date: Sun, 20 May 2007 11:21:41 +0000 Subject: [PATCH] Clean up & comments --- compiler/ghci/RtClosureInspect.hs | 239 +++++++++++++++++-------------------- 1 file changed, 109 insertions(+), 130 deletions(-) diff --git a/compiler/ghci/RtClosureInspect.hs b/compiler/ghci/RtClosureInspect.hs index 3ca0b0b..2d49ad7 100644 --- a/compiler/ghci/RtClosureInspect.hs +++ b/compiler/ghci/RtClosureInspect.hs @@ -376,9 +376,27 @@ 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 @@ -393,88 +411,11 @@ runTR hsc_env c = do 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) @@ -482,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) @@ -553,11 +500,10 @@ 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 --- Strict application of f at index i -appArr f (Array _ _ ptrs#) (I# i#) = case indexArray# ptrs# i# of - (# e #) -> f e + -- Fast, breadth-first version of obtainTerm that deals only with type reconstruction + cvReconstructType :: HscEnv -> Bool -> Maybe Type -> HValue -> IO Type cvReconstructType hsc_env force mb_ty hval = runTR hsc_env $ do tv <- liftM mkTyVarTy (newVar argTypeKind) @@ -602,6 +548,84 @@ cvReconstructType hsc_env force mb_ty hval = runTR hsc_env $ do otherwise -> return [] +-- 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. + + 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" + + +------------------------------------------------------------------------------------ + isMonomorphic ty | (tvs, ty') <- splitForAllTys ty = null tvs && (isEmptyVarSet . tyVarsOfType) ty' @@ -612,6 +636,10 @@ mapMif_ pred f (x:xx) = (if pred x then f x else return x) : mapMif_ pred f xx unlessM condM acc = condM >>= \c -> unless c acc +-- Strict application of f at index i +appArr f (Array _ _ ptrs#) (I# i#) = case indexArray# ptrs# i# of + (# e #) -> f e + zonkTerm :: Term -> TcM Term zonkTerm = foldTerm idTermFoldM { fTerm = \ty dc v tt -> sequence tt >>= \tt -> @@ -625,53 +653,4 @@ zonkTerm = foldTerm idTermFoldM { -- 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 - -data Opaque = forall a. Opaque a - -And we have a term built as: - -t = Opaque (map Just [[1,1],[2,2]]) - -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) - -seq _1 () - -t - O ( (_3::b) : (_4::[b]) ) - -seq _3 () - -t - O ( (Just (_5::c)) : (_4::[b]) ) -At this point, we know that b = (Maybe c) - -seq _5 () - -t - O ( (Just ((_6::d) : (_7::[d]) )) : (_4::[b]) ) - -At this point, we know that c = [d] - -seq _6 () - -t - O ( (Just (1 : (_7::[d]) )) : (_4::[b]) ) - -At this point, we know that d = Integer - -The fully reconstructed expressions, with propagation, would be: - -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]]) ) - - -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 --} -- 1.7.10.4