projects / ghc-hetmet.git / blobdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | inline | side by side
White-space only
[ghc-hetmet.git] / compiler / types / FamInstEnv.lhs
diff --git a/compiler/types/FamInstEnv.lhs b/compiler/types/FamInstEnv.lhs
index 9b49f5c..d1a3445 100644 (file)
--- a/compiler/types/FamInstEnv.lhs
+++ b/compiler/types/FamInstEnv.lhs
@@ -6,13 +6,18 @@ FamInstEnv: Type checked family instance declarations
 
 \begin{code}
 module FamInstEnv (
 
 \begin{code}
 module FamInstEnv (
-       FamInst(..), famInstTyCon, pprFamInst, pprFamInstHdr, pprFamInsts, 
+       FamInst(..), famInstTyCon, famInstTyVars, 
+       pprFamInst, pprFamInstHdr, pprFamInsts, 
        famInstHead, mkLocalFamInst, mkImportedFamInst,
 
        famInstHead, mkLocalFamInst, mkImportedFamInst,
 
-       FamInstEnv, emptyFamInstEnv, extendFamInstEnv, extendFamInstEnvList, 
+       FamInstEnvs, FamInstEnv, emptyFamInstEnv, 
+       extendFamInstEnv, extendFamInstEnvList, 
        famInstEnvElts, familyInstances,
 
        famInstEnvElts, familyInstances,
 
-       lookupFamInstEnv, lookupFamInstEnvUnify
+       lookupFamInstEnv, lookupFamInstEnvUnify,
+       
+       -- Normalisation
+       toplevelNormaliseFamInst
     ) where
 
 #include "HsVersions.h"
     ) where
 
 #include "HsVersions.h"
@@ -22,7 +27,9 @@ import Unify
 import TcGadt
 import TcType
 import Type
 import TcGadt
 import TcType
 import Type
+import TypeRep
 import TyCon
 import TyCon
+import Coercion
 import VarSet
 import Var
 import Name
 import VarSet
 import Var
 import Name
@@ -30,9 +37,10 @@ import OccName
 import SrcLoc
 import UniqFM
 import Outputable
 import SrcLoc
 import UniqFM
 import Outputable
+import Maybes
+import Util
 
 import Maybe
 
 import Maybe
-import Monad
 \end{code}
 
 
 \end{code}
 
 
@@ -45,13 +53,19 @@ import Monad
 \begin{code}
 data FamInst 
   = FamInst { fi_fam   :: Name         -- Family name
 \begin{code}
 data FamInst 
   = FamInst { fi_fam   :: Name         -- Family name
+               -- INVARIANT: fi_fam = case tyConFamInst_maybe fi_tycon of
+               --                         Just (tc, tys) -> tc
 
                -- Used for "rough matching"; same idea as for class instances
            , fi_tcs   :: [Maybe Name]  -- Top of type args
 
                -- Used for "rough matching"; same idea as for class instances
            , fi_tcs   :: [Maybe Name]  -- Top of type args
+               -- INVARIANT: fi_tcs = roughMatchTcs fi_tys
 
                -- Used for "proper matching"; ditto
            , fi_tvs   :: TyVarSet      -- Template tyvars for full match
            , fi_tys   :: [Type]        -- Full arg types
 
                -- Used for "proper matching"; ditto
            , fi_tvs   :: TyVarSet      -- Template tyvars for full match
            , fi_tys   :: [Type]        -- Full arg types
+               -- INVARIANT: fi_tvs = tyConTyVars fi_tycon
+               --            fi_tys = case tyConFamInst_maybe fi_tycon of
+               --                         Just (_, tys) -> tys
 
            , fi_tycon :: TyCon         -- Representation tycon
            }
 
            , fi_tycon :: TyCon         -- Representation tycon
            }
@@ -60,6 +74,8 @@ data FamInst
 --
 famInstTyCon :: FamInst -> TyCon
 famInstTyCon = fi_tycon
 --
 famInstTyCon :: FamInst -> TyCon
 famInstTyCon = fi_tycon
+
+famInstTyVars = fi_tvs
 \end{code}
 
 \begin{code}
 \end{code}
 
 \begin{code}
@@ -73,14 +89,13 @@ instance Outputable FamInst where
 pprFamInst :: FamInst -> SDoc
 pprFamInst famInst
   = hang (pprFamInstHdr famInst)
 pprFamInst :: FamInst -> SDoc
 pprFamInst famInst
   = hang (pprFamInstHdr famInst)
-       2 (ptext SLIT("--") <+> (pprDefnLoc (getSrcLoc famInst)))
+       2 (ptext SLIT("--") <+> (pprDefnLoc (getSrcSpan famInst)))
 
 pprFamInstHdr :: FamInst -> SDoc
 pprFamInstHdr (FamInst {fi_fam = fam, fi_tys = tys, fi_tycon = tycon})
   = pprTyConSort <+> pprHead
   where
 
 pprFamInstHdr :: FamInst -> SDoc
 pprFamInstHdr (FamInst {fi_fam = fam, fi_tys = tys, fi_tycon = tycon})
   = pprTyConSort <+> pprHead
   where
-    pprHead = parenSymOcc (getOccName fam) (ppr fam) <+> 
-             sep (map pprParendType tys)
+    pprHead = pprTypeApp (parenSymOcc (getOccName fam) (ppr fam)) tys
     pprTyConSort | isDataTyCon tycon = ptext SLIT("data instance")
                 | isNewTyCon  tycon = ptext SLIT("newtype instance")
                 | isSynTyCon  tycon = ptext SLIT("type instance")
     pprTyConSort | isDataTyCon tycon = ptext SLIT("data instance")
                 | isNewTyCon  tycon = ptext SLIT("newtype instance")
                 | isSynTyCon  tycon = ptext SLIT("type instance")
@@ -140,6 +155,9 @@ InstEnv maps a family name to the list of known instances for that family.
 \begin{code}
 type FamInstEnv = UniqFM FamilyInstEnv -- Maps a family to its instances
 
 \begin{code}
 type FamInstEnv = UniqFM FamilyInstEnv -- Maps a family to its instances
 
+type FamInstEnvs = (FamInstEnv, FamInstEnv)
+       -- External package inst-env, Home-package inst-env
+
 data FamilyInstEnv
   = FamIE [FamInst]    -- The instances for a particular family, in any order
          Bool          -- True <=> there is an instance of form T a b c
 data FamilyInstEnv
   = FamIE [FamInst]    -- The instances for a particular family, in any order
          Bool          -- True <=> there is an instance of form T a b c
@@ -174,7 +192,7 @@ extendFamInstEnv inst_env ins_item@(FamInst {fi_fam = cls_nm, fi_tcs = mb_tcs})
     add (FamIE items tyvar) _ = FamIE (ins_item:items)
                                      (ins_tyvar || tyvar)
     ins_tyvar = not (any isJust mb_tcs)
     add (FamIE items tyvar) _ = FamIE (ins_item:items)
                                      (ins_tyvar || tyvar)
     ins_tyvar = not (any isJust mb_tcs)
-\end{code}                   
+\end{code}
 
 %************************************************************************
 %*                                                                     *
 
 %************************************************************************
 %*                                                                     *
@@ -187,11 +205,24 @@ Multiple matches are only possible in case of type families (not data
 families), and then, it doesn't matter which match we choose (as the
 instances are guaranteed confluent).
 
 families), and then, it doesn't matter which match we choose (as the
 instances are guaranteed confluent).
 
+We return the matching family instances and the type instance at which it
+matches.  For example, if we lookup 'T [Int]' and have a family instance
+
+  data instance T [a] = ..
+
+desugared to
+
+  data :R42T a = ..
+  coe :Co:R42T a :: T [a] ~ :R42T a
+
+we return the matching instance '(FamInst{.., fi_tycon = :R42T}, Int)'.
+
 \begin{code}
 \begin{code}
-lookupFamInstEnv :: (FamInstEnv        -- External package inst-env
-                   ,FamInstEnv)        -- Home-package inst-env
+type FamInstMatch = (FamInst, [Type])           -- Matching type instance
+
+lookupFamInstEnv :: FamInstEnvs
                 -> TyCon -> [Type]             -- What we are looking for
                 -> TyCon -> [Type]             -- What we are looking for
-                -> [(TvSubst, FamInst)]        -- Successful matches
+                -> [FamInstMatch]              -- Successful matches
 lookupFamInstEnv (pkg_ie, home_ie) fam tys
   = home_matches ++ pkg_matches
   where
 lookupFamInstEnv (pkg_ie, home_ie) fam tys
   = home_matches ++ pkg_matches
   where
@@ -221,7 +252,7 @@ lookupFamInstEnv (pkg_ie, home_ie) fam tys
 
         -- Proper check
       | Just subst <- tcMatchTys tpl_tvs tpl_tys tys
 
         -- Proper check
       | Just subst <- tcMatchTys tpl_tvs tpl_tys tys
-      = (subst, item) : find rest
+      = (item, substTyVars subst (tyConTyVars tycon)) : find rest
 
         -- No match => try next
       | otherwise
 
         -- No match => try next
       | otherwise
@@ -240,7 +271,7 @@ indexed synonyms and we don't want to slow that down by needless unification.
 
 \begin{code}
 lookupFamInstEnvUnify :: (FamInstEnv, FamInstEnv) -> TyCon -> [Type]
 
 \begin{code}
 lookupFamInstEnvUnify :: (FamInstEnv, FamInstEnv) -> TyCon -> [Type]
-                     -> [(TvSubst, FamInst)]
+                     -> [(FamInstMatch)]
 lookupFamInstEnvUnify (pkg_ie, home_ie) fam tys
   = home_matches ++ pkg_matches
   where
 lookupFamInstEnvUnify (pkg_ie, home_ie) fam tys
   = home_matches ++ pkg_matches
   where
@@ -276,7 +307,9 @@ lookupFamInstEnvUnify (pkg_ie, home_ie) fam tys
                -- Unification will break badly if the variables overlap
                -- They shouldn't because we allocate separate uniques for them
         case tcUnifyTys bind_fn tpl_tys tys of
                -- Unification will break badly if the variables overlap
                -- They shouldn't because we allocate separate uniques for them
         case tcUnifyTys bind_fn tpl_tys tys of
-           Just subst -> (subst, item) : find rest
+           Just subst -> let rep_tys = substTyVars subst (tyConTyVars tycon)
+                          in
+                          (item, rep_tys) : find rest
            Nothing    -> find rest
 
 -- See explanation at @InstEnv.bind_fn@.
            Nothing    -> find rest
 
 -- See explanation at @InstEnv.bind_fn@.
@@ -284,3 +317,99 @@ lookupFamInstEnvUnify (pkg_ie, home_ie) fam tys
 bind_fn tv | isTcTyVar tv && isExistentialTyVar tv = Skolem
           | otherwise                             = BindMe
 \end{code}
 bind_fn tv | isTcTyVar tv && isExistentialTyVar tv = Skolem
           | otherwise                             = BindMe
 \end{code}
+
+--------------------------------------
+-- Normalisation 
+
+\begin{code}
+       -- get rid of TOPLEVEL type functions by rewriting them 
+       -- i.e. treating their equations as a TRS
+toplevelNormaliseFamInst :: FamInstEnvs ->
+                           Type ->
+                           (CoercionI,Type)
+toplevelNormaliseFamInst env ty
+       | Just ty' <- tcView ty = normaliseFamInst env ty'
+toplevelNormaliseFamInst env ty@(TyConApp tyCon tys)
+       | isOpenTyCon tyCon
+       = normaliseFamInst env ty
+toplevelNormaliseFamInst env ty
+       = (IdCo,ty)
+        
+
+       -- get rid of ALL type functions by rewriting them 
+       -- i.e. treating their equations as a TRS
+normaliseFamInst :: FamInstEnvs ->     -- environment with family instances
+                   Type ->             -- old type
+                   (CoercionI,Type)    -- (coercion,new type)
+normaliseFamInst env ty 
+       | Just ty' <- tcView ty = normaliseFamInst env ty' 
+normaliseFamInst env ty@(TyConApp tyCon tys) =
+       let (cois,ntys) = mapAndUnzip (normaliseFamInst env) tys
+           tycon_coi   = mkTyConAppCoI tyCon ntys cois
+           maybe_ty_co = lookupFamInst env tyCon ntys
+        in case maybe_ty_co of
+               -- a matching family instance exists
+               Just (ty',co) ->
+                       let first_coi      = mkTransCoI tycon_coi (ACo co)
+                           (rest_coi,nty) = normaliseFamInst env ty'
+                           fix_coi        = mkTransCoI first_coi rest_coi
+                       in (fix_coi,nty)
+               -- no matching family instance exists
+               -- we do not do anything
+               Nothing -> 
+                       (tycon_coi,TyConApp tyCon ntys)
+normaliseFamInst env ty@(AppTy ty1 ty2)        =
+       let (coi1,nty1) = normaliseFamInst env ty1
+           (coi2,nty2) = normaliseFamInst env ty2
+       in  (mkAppTyCoI nty1 coi1 nty2 coi2, AppTy nty1 nty2)
+normaliseFamInst env ty@(FunTy ty1 ty2)        =
+       let (coi1,nty1) = normaliseFamInst env ty1
+           (coi2,nty2) = normaliseFamInst env ty2
+       in  (mkFunTyCoI nty1 coi1 nty2 coi2, FunTy nty1 nty2)
+normaliseFamInst env ty@(ForAllTy tyvar ty1)   =
+       let (coi,nty1) = normaliseFamInst env ty1
+       in  (mkForAllTyCoI tyvar coi,ForAllTy tyvar nty1)
+normaliseFamInst env ty@(NoteTy note ty1)      =
+       let (coi,nty1) = normaliseFamInst env ty1
+       in  (mkNoteTyCoI note coi,NoteTy note nty1)
+normaliseFamInst env ty@(TyVarTy _) =
+       (IdCo,ty)
+normaliseFamInst env (PredTy predty) =
+       normaliseFamInstPred env predty 
+
+normaliseFamInstPred :: FamInstEnvs -> PredType -> (CoercionI,Type)
+normaliseFamInstPred env (ClassP cls tys) =
+       let (cois,tys') = mapAndUnzip (normaliseFamInst env) tys
+       in  (mkClassPPredCoI cls tys' cois, PredTy $ ClassP cls tys')
+normaliseFamInstPred env (IParam ipn ty) =
+       let (coi,ty') = normaliseFamInst env ty
+       in  (mkIParamPredCoI ipn coi, PredTy $ IParam ipn ty')
+normaliseFamInstPred env (EqPred ty1 ty2) =
+       let (coi1,ty1') = normaliseFamInst env ty1
+            (coi2,ty2') = normaliseFamInst env ty2
+       in  (mkEqPredCoI ty1' coi1 ty2' coi2, PredTy $ EqPred ty1' ty2')
+ 
+lookupFamInst :: FamInstEnvs -> TyCon -> [Type] -> Maybe (Type,Coercion)
+
+-- (lookupFamInst F tys) looks for a top-level instance
+--     co : forall a. F tys' = G a
+--   (The rhs is always of form G a; see Note [The FamInst structure]
+--     in FamInst.)
+-- where we can instantiate 'a' with t to make tys'[t/a] = tys
+-- Hence   (co t) : F tys ~ G t
+-- Then we return (Just (G t, co t))
+
+lookupFamInst env tycon tys 
+  | not (isOpenTyCon tycon)            -- Dead code; fix.
+  = Nothing
+  | otherwise
+  = case lookupFamInstEnv env tycon tys of
+          [(subst, fam_inst)] -> 
+            Just (mkTyConApp rep_tc substituted_vars, mkTyConApp coercion_tycon substituted_vars)
+               where   -- NB: invariant of lookupFamInstEnv is that (tyConTyVars rep_tc)
+                       --     is in the domain of the substitution
+                 rep_tc           = famInstTyCon fam_inst
+                 coercion_tycon   = expectJust "lookupFamInst" (tyConFamilyCoercion_maybe rep_tc)
+                 substituted_vars = substTyVars subst (tyConTyVars rep_tc)
+          other -> Nothing
+\end{code}
Glasgow Haskell Compiler with heterogeneous metaprogramming (generalized arrows and modal types)