TypeSubst.hs 3.45 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
{- |
    Module      :  $Header$
    Description :  Type substitution
    Copyright   :  (c) 2003 Wolfgang Lux
    License     :  OtherLicense

    Maintainer  :  bjp@informatik.uni-kiel.de
    Stability   :  experimental
    Portability :  portable

   This module implements substitutions on types.
-}

module Base.TypeSubst
  ( module Base.TypeSubst, idSubst, singleSubst, bindSubst, compose
  ) where

Björn Peemöller 's avatar
Björn Peemöller committed
18
19
import Data.List   (nub)
import Data.Maybe  (fromJust)
20
21
22
23
24

import Base.Subst
import Base.TopEnv
import Base.Types

Björn Peemöller 's avatar
Björn Peemöller committed
25
import Env.Value   (ValueInfo (..))
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47

type TypeSubst = Subst Int Type

class SubstType a where
  subst :: TypeSubst -> a -> a

bindVar :: Int -> Type -> TypeSubst -> TypeSubst
bindVar tv ty = compose (bindSubst tv ty idSubst)

substVar :: TypeSubst -> Int -> Type
substVar = substVar' TypeVariable subst

instance SubstType Type where
  subst sigma (TypeConstructor tc tys) =
    TypeConstructor tc (map (subst sigma) tys)
  subst sigma (TypeVariable        tv) = substVar sigma tv
  subst sigma (TypeConstrained tys tv) = case substVar sigma tv of
    TypeVariable tv' -> TypeConstrained tys tv'
    ty -> ty
  subst sigma (TypeArrow      ty1 ty2) =
    TypeArrow (subst sigma ty1) (subst sigma ty2)
  subst _     ts@(TypeSkolem        _) = ts
48
49
50
51
52
  subst sigma (TypeRecord       fs rv) = case rv of
    Nothing -> TypeRecord fs' Nothing
    Just r' -> case substVar sigma r' of
      TypeVariable tv -> TypeRecord fs' (Just tv)
      ty              -> ty
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
   where fs' = map (\ (l,ty) -> (l, subst sigma ty)) fs

instance SubstType TypeScheme where
  subst sigma (ForAll n ty) =
    ForAll n (subst (foldr unbindSubst sigma [0..n-1]) ty)

instance SubstType ExistTypeScheme where
  subst sigma (ForAllExist n n' ty) =
    ForAllExist n n' (subst (foldr unbindSubst sigma [0..n+n'-1]) ty)

instance SubstType ValueInfo where
  subst _     dc@(DataConstructor  _ _ _) = dc
  subst _     nc@(NewtypeConstructor _ _) = nc
  subst theta (Value              v a ty) = Value v a (subst theta ty)
  subst theta (Label              l r ty) = Label l r (subst theta ty)

instance SubstType a => SubstType (TopEnv a) where
  subst = fmap . subst

-- The function 'expandAliasType' expands all occurrences of a
-- type synonym in a type. After the expansion we have to reassign the
-- type indices for all type variables. Otherwise, expanding a type
-- synonym like type Pair' a b = (b,a) could break the invariant
-- that the universally quantified type variables are assigned indices in
-- the order of their occurrence. This is handled by the function
-- 'normalize'.

expandAliasType :: [Type] -> Type -> Type
expandAliasType tys (TypeConstructor tc tys') =
  TypeConstructor tc (map (expandAliasType tys) tys')
83
expandAliasType tys (TypeVariable          n)
84
85
86
87
88
89
  | n >= 0    = tys !! n
  | otherwise = TypeVariable n
expandAliasType _   (TypeConstrained   tys n) = TypeConstrained tys n
expandAliasType tys (TypeArrow       ty1 ty2) =
  TypeArrow (expandAliasType tys ty1) (expandAliasType tys ty2)
expandAliasType _   tsk@(TypeSkolem        _) = tsk
90
91
92
93
expandAliasType tys (TypeRecord        fs rv) = case rv of
  Nothing -> TypeRecord fs' Nothing
  Just r' -> let (TypeVariable tv) = expandAliasType tys $ TypeVariable r'
             in  TypeRecord fs' (Just tv)
94
95
96
97
98
99
 where fs' = map (\ (l, ty) -> (l, expandAliasType tys ty)) fs

normalize :: Type -> Type
normalize ty = expandAliasType [TypeVariable (occur tv) | tv <- [0 ..]] ty
  where tvs = zip (nub (filter (>= 0) (typeVars ty))) [0 ..]
        occur tv = fromJust (lookup tv tvs)