[commit: ghc] supercompiler: Preliminary thoughts about renaming via MSG, invertRenaming (170cee5)

Repository : ssh://darcs.haskell.org//srv/darcs/ghc

On branch  : supercompiler

http://hackage.haskell.org/trac/ghc/changeset/170cee5a92f97563c5a7fb722fa1c530b7f9d623

>---------------------------------------------------------------

commit 170cee5a92f97563c5a7fb722fa1c530b7f9d623
Author: Max Bolingbroke <[email protected]>
Date:   Thu Apr 19 23:30:02 2012 +0100

    Preliminary thoughts about renaming via MSG, invertRenaming

>---------------------------------------------------------------

 .../supercompile/Supercompile/Core/Renaming.hs     |   32 ++++++++++++++++---
 compiler/supercompile/Supercompile/Drive/MSG.hs    |   33 +++++++++++++++++++-
 compiler/supercompile/Supercompile/Utilities.hs    |    3 ++
 3 files changed, 62 insertions(+), 6 deletions(-)

diff --git a/compiler/supercompile/Supercompile/Core/Renaming.hs b/compiler/supercompile/Supercompile/Core/Renaming.hs
index 863f92a..1d1b369 100644
--- a/compiler/supercompile/Supercompile/Core/Renaming.hs
+++ b/compiler/supercompile/Supercompile/Core/Renaming.hs
@@ -4,6 +4,7 @@ module Supercompile.Core.Renaming (
     -- | Renamings
     Renaming, emptyRenaming,
     mkInScopeIdentityRenaming, mkIdentityRenaming, mkTyVarRenaming,
+    invertRenaming,
     InScopeSet, emptyInScopeSet, mkInScopeSet,
     
     -- | Extending the renaming
@@ -38,10 +39,15 @@ import Supercompile.Utilities
 
 import CoreSubst
 import OptCoercion (optCoercion)
-import Coercion    (CvSubst(..), CvSubstEnv, isCoVar, mkCoVarCo)
+import Coercion    (CvSubst(..), CvSubstEnv, isCoVar, mkCoVarCo, getCoVar_maybe)
 import qualified CoreSyn as CoreSyn (CoreExpr, Expr(Var))
-import Type        (mkTyVarTy)
-import Var         (Id, TyVar, CoVar, isTyVar)
+import Type        (mkTyVarTy, getTyVar_maybe)
+import Id          (mkSysLocal)
+import Var         (Id, TyVar, CoVar, isTyVar, mkTyVar, varType)
+import OccName     (occNameFS)
+import Name        (getOccName, mkSysTvName)
+import FastString  (FastString)
+import UniqFM      (ufmToList)
 import VarEnv
 
 
@@ -133,12 +139,28 @@ mkInScopeIdentityRenaming = mkIdentityRenaming . getInScopeVars
 mkTyVarRenaming :: [(TyVar, Type)] -> Renaming
 mkTyVarRenaming aas = (emptyVarEnv, mkVarEnv aas, emptyVarEnv)
 
+invertRenaming :: Renaming -> Maybe Renaming
+invertRenaming (id_subst, tv_subst, co_subst)
+  = liftM3 (,,) (traverse coreSynToVar_maybe id_subst >>= invertVarEnv (\fs uniq -> varToCoreSyn . mkSysLocal fs uniq))
+                (traverse getTyVar_maybe     tv_subst >>= invertVarEnv (\fs uniq -> mkTyVarTy    . mkTyVar (mkSysTvName uniq fs)))
+                (traverse getCoVar_maybe     co_subst >>= invertVarEnv (\fs uniq -> mkCoVarCo    . mkSysLocal fs uniq))
+  where
+    -- FIXME: this inversion relies on something of a hack because the domain of the mapping is not stored (only its Unique)
+    invertVarEnv :: (FastString -> Unique -> Type -> a)
+                 -> VarEnv Var -> Maybe (VarEnv a)
+    invertVarEnv mk env
+      | distinct (varEnvElts env) = Just (mkVarEnv [(x, mk (occNameFS (getOccName x)) u (varType x)) | (u, x) <- ufmToList env])
+      | otherwise                 = Nothing
+
 varToCoreSyn :: Var -> CoreSyn.CoreExpr
 varToCoreSyn = CoreSyn.Var
 
+coreSynToVar_maybe :: CoreSyn.CoreExpr -> Maybe Var
+coreSynToVar_maybe (CoreSyn.Var x') = Just x'
+coreSynToVar_maybe _                = Nothing
+
 coreSynToVar :: CoreSyn.CoreExpr -> Var
-coreSynToVar (CoreSyn.Var x') = x'
-coreSynToVar e                = panic "renameId" (ppr e)
+coreSynToVar = fromMaybe (panic "renameId" empty) . coreSynToVar_maybe
 
 insertIdRenaming :: Renaming -> Id -> Out Id -> Renaming
 insertIdRenaming (id_subst, tv_subst, co_subst) x x'
diff --git a/compiler/supercompile/Supercompile/Drive/MSG.hs b/compiler/supercompile/Supercompile/Drive/MSG.hs
index 7eb436b..23dfeb9 100644
--- a/compiler/supercompile/Supercompile/Drive/MSG.hs
+++ b/compiler/supercompile/Supercompile/Drive/MSG.hs
@@ -267,6 +267,37 @@ data MSGMode = MM {
 
 type MSGResult = ((Deeds, Heap, Renaming, Stack), (Heap, Stack, Anned QA), (Deeds, Heap, Renaming, Stack))
 
+-- Note [Renaming via MSG]
+-- ~~~~~~~~~~~~~~~~~~~~~~~
+--
+-- If s1 can be renamed/instantiated to s2, then taking the MSG of the two should yield:
+--  1. On the left:
+--    a) An empty stack
+--    b) A heap containing only lambdaBounds
+--    c) A Renaming that maps TyVar->TyVar and CoVar->CoVar, and which is invertible
+--       (we can't accept [x |-> z, y |-> z] because the right part of the MSG might
+--        instantiate x and y to two different things)
+--  2. On the right:
+--    a) An empty stack, or one which is an allowed instantiation
+--    b) A heap containing only lambdaBounds, or one which is an allowed instantiation
+--    c) A Renaming. We can always allow TyVar->Type and CoVar->Coercion mappings because
+--       they are not computationally relevant. We could optionally forbid non-invertible
+--       renamings like [x |-> z, y |-> z] because it means that two variables are shared
+--       here which weren't in the original term. However, this is likely not important in practice.
+--
+-- If s1 and s2 match to give type generalisation info, we expect this from the MSG:
+--  1. On the left:
+--    a) An empty stack
+--    b) A heap containing only lambdaBounds
+--  2. On the right:
+--    a) An empty stack
+--    b) A heap containing only lambdaBounds
+--
+-- The form of the Renaming is unimportant (as long as we don't care about whether 2 variables
+-- are shared or not) because we are always happy to generalise away Type/Coercion info, and
+-- we're going to satisfy the demand for the States on both sides by driving the (instantiable)
+-- common State.
+
 msg :: {- MSGMode -- ^ How to match
     -> -} State   -- ^ Tieback semantics
     -> State   -- ^ This semantics
@@ -638,7 +669,7 @@ msgPureHeap {- mm -} rn2 msg_s init_h_l init_h_r (k_bvs_l, k_fvs_l) (k_bvs_r, k_
                    (Just Nothing, Just Nothing)
                      | x_l == x_r
                      -> return (rn_l, rn_r, msg_s, hb_r) -- Right biased
-                   (Nothing, Nothing)
+                   (Nothing, Nothing) -- FIXME: I should possibly be adding lambdaBound bindings for x_l and x_r to h_l and h_r respectively
                      -> return (insertIdRenaming rn_l x_common x_l, insertIdRenaming rn_r x_common x_r, msg_s, lambdaBound)
                    _ -> Left "msgPureHeap: non-unifiable heap bindings"
                  -- If they match, we need to make a common heap binding
diff --git a/compiler/supercompile/Supercompile/Utilities.hs b/compiler/supercompile/Supercompile/Utilities.hs
index 7fc59e5..9b5371a 100644
--- a/compiler/supercompile/Supercompile/Utilities.hs
+++ b/compiler/supercompile/Supercompile/Utilities.hs
@@ -500,6 +500,9 @@ runs f g (x:xs) = go (f x) [g x] xs
           | otherwise = (b, reverse pending) : go b' [g x] xs
           where b' = f x
 
+distinct :: Ord a => [a] -> Bool
+distinct xs = length xs /= S.size (S.fromList xs)
+
 
 -- | Orders elements of a map into dependency order insofar as that is possible.
 --