Commit 701797c3 authored by TomSchrijvers's avatar TomSchrijvers
Browse files

type family normalisation

parent 289ee3d0
......@@ -31,7 +31,17 @@ module Coercion (
unsafeCoercionTyCon, symCoercionTyCon,
transCoercionTyCon, leftCoercionTyCon,
rightCoercionTyCon, instCoercionTyCon -- needed by TysWiredIn
rightCoercionTyCon, instCoercionTyCon, -- needed by TysWiredIn
-- CoercionI
CoercionI(..),
isIdentityCoercion,
mkSymCoI, mkTransCoI,
mkTyConAppCoI, mkAppTyCoI, mkFunTyCoI,
mkNoteTyCoI, mkForAllTyCoI,
fromCoI,
mkClassPPredCoI, mkIParamPredCoI, mkEqPredCoI,
) where
#include "HsVersions.h"
......@@ -39,6 +49,7 @@ module Coercion (
import TypeRep
import Type
import TyCon
import Class
import Var
import Name
import OccName
......@@ -421,3 +432,92 @@ splitNewTypeRepCo_maybe (TyConApp tc tys)
co_con = maybe (pprPanic "splitNewTypeRepCo_maybe" (ppr tc)) id (newTyConCo_maybe tc)
splitNewTypeRepCo_maybe other = Nothing
\end{code}
--------------------------------------
-- CoercionI smart constructors
-- lifted smart constructors of ordinary coercions
\begin{code}
-- CoercionI is either
-- (a) proper coercion
-- (b) the identity coercion
data CoercionI = IdCo | ACo Coercion
isIdentityCoercion :: CoercionI -> Bool
isIdentityCoercion IdCo = True
isIdentityCoercion _ = False
mkSymCoI :: CoercionI -> CoercionI
mkSymCoI IdCo = IdCo
mkSymCoI (ACo co) = ACo $ mkCoercion symCoercionTyCon [co]
-- the smart constructor
-- is too smart with tyvars
mkTransCoI :: CoercionI -> CoercionI -> CoercionI
mkTransCoI IdCo aco = aco
mkTransCoI aco IdCo = aco
mkTransCoI (ACo co1) (ACo co2) = ACo $ mkTransCoercion co1 co2
mkTyConAppCoI :: TyCon -> [Type] -> [CoercionI] -> CoercionI
mkTyConAppCoI tyCon tys cois =
let (anyAcon,co_args) = f tys cois
in if anyAcon
then ACo (TyConApp tyCon co_args)
else IdCo
where
f [] [] = (False,[])
f (x:xs) (y:ys) =
let (b,cos) = f xs ys
in case y of
IdCo -> (b,x:cos)
ACo co -> (True,co:cos)
mkAppTyCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
mkAppTyCoI ty1 IdCo ty2 IdCo = IdCo
mkAppTyCoI ty1 coi1 ty2 coi2 =
ACo $ AppTy (fromCoI coi1 ty1) (fromCoI coi2 ty2)
mkFunTyCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
mkFunTyCoI ty1 IdCo ty2 IdCo = IdCo
mkFunTyCoI ty1 coi1 ty2 coi2 =
ACo $ FunTy (fromCoI coi1 ty1) (fromCoI coi2 ty2)
mkNoteTyCoI :: TyNote -> CoercionI -> CoercionI
mkNoteTyCoI _ IdCo = IdCo
mkNoteTyCoI note (ACo co) = ACo $ NoteTy note co
mkForAllTyCoI :: TyVar -> CoercionI -> CoercionI
mkForAllTyCoI _ IdCo = IdCo
mkForAllTyCoI tv (ACo co) = ACo $ ForAllTy tv co
fromCoI IdCo ty = ty
fromCoI (ACo co) ty = co
mkClassPPredCoI :: Class -> [Type] -> [CoercionI] -> CoercionI
mkClassPPredCoI cls tys cois =
let (anyAcon,co_args) = f tys cois
in if anyAcon
then ACo $ PredTy $ ClassP cls co_args
else IdCo
where
f [] [] = (False,[])
f (x:xs) (y:ys) =
let (b,cos) = f xs ys
in case y of
IdCo -> (b,x:cos)
ACo co -> (True,co:cos)
mkIParamPredCoI :: (IPName Name) -> CoercionI -> CoercionI
mkIParamPredCoI ipn IdCo = IdCo
mkIParamPredCoI ipn (ACo co) = ACo $ PredTy $ IParam ipn co
mkEqPredCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
mkEqPredCoI _ IdCo _ IdCo = IdCo
mkEqPredCoI ty1 IdCo _ (ACo co2) = ACo $ PredTy $ EqPred ty1 co2
mkEqPredCoI ty1 (ACo co1) ty2 coi2 = ACo $ PredTy $ EqPred co1 (fromCoI coi2 ty2)
\end{code}
......@@ -14,7 +14,10 @@ module FamInstEnv (
extendFamInstEnv, extendFamInstEnvList,
famInstEnvElts, familyInstances,
lookupFamInstEnv, lookupFamInstEnvUnify
lookupFamInstEnv, lookupFamInstEnvUnify,
-- Normalisation
toplevelNormaliseFamInst
) where
#include "HsVersions.h"
......@@ -24,7 +27,9 @@ import Unify
import TcGadt
import TcType
import Type
import TypeRep
import TyCon
import Coercion
import VarSet
import Var
import Name
......@@ -32,6 +37,8 @@ import OccName
import SrcLoc
import UniqFM
import Outputable
import Maybes
import Util
import Maybe
\end{code}
......@@ -310,3 +317,99 @@ lookupFamInstEnvUnify (pkg_ie, home_ie) fam tys
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}
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment