Changed TypeExp to stop using Data.Generics (which was getting awkward)
Instead of storing the Constr, which was messy, we now store a String (to allow comparison of constructor types during unification) and a function to reform the type at the end of the type checking.
This commit is contained in:
parent
abbca5f235
commit
1115364d47
|
@ -49,8 +49,8 @@ lookupMapElseMutVar k
|
||||||
put st {csUnifyLookup = m'}
|
put st {csUnifyLookup = m'}
|
||||||
return v
|
return v
|
||||||
|
|
||||||
ttte :: Data b => b -> A.Type -> PassM (TypeExp A.Type)
|
ttte :: String -> (A.Type -> A.Type) -> A.Type -> PassM (TypeExp A.Type)
|
||||||
ttte c t = typeToTypeExp t >>= \t' -> return $ OperType (toConstr c) [t']
|
ttte c f t = typeToTypeExp t >>= \t' -> return $ OperType c (\[x] -> f x) [t']
|
||||||
|
|
||||||
-- Transforms the given type into a typeexp, such that the only inner types
|
-- Transforms the given type into a typeexp, such that the only inner types
|
||||||
-- left will be the primitive types (integer types, float types, bool, time). Arrays
|
-- left will be the primitive types (integer types, float types, bool, time). Arrays
|
||||||
|
@ -58,11 +58,11 @@ ttte c t = typeToTypeExp t >>= \t' -> return $ OperType (toConstr c) [t']
|
||||||
-- neither are records.
|
-- neither are records.
|
||||||
-- User data types should not be present in the input.
|
-- User data types should not be present in the input.
|
||||||
typeToTypeExp :: A.Type -> PassM (TypeExp A.Type)
|
typeToTypeExp :: A.Type -> PassM (TypeExp A.Type)
|
||||||
typeToTypeExp x@(A.List t) = ttte x t
|
typeToTypeExp (A.List t) = ttte "[]" A.List t
|
||||||
typeToTypeExp (A.Chan A.DirInput _ t) = ttte "?" t
|
typeToTypeExp (A.Chan A.DirInput at t) = ttte "?" (A.Chan A.DirInput at) t
|
||||||
typeToTypeExp (A.Chan A.DirOutput _ t) = ttte "!" t
|
typeToTypeExp (A.Chan A.DirOutput at t) = ttte "!" (A.Chan A.DirOutput at) t
|
||||||
typeToTypeExp (A.Chan A.DirUnknown _ t) = ttte "channel" t
|
typeToTypeExp (A.Chan A.DirUnknown at t) = ttte "channel" (A.Chan A.DirUnknown at) t
|
||||||
typeToTypeExp (A.Mobile t) = ttte "MOBILE" t
|
typeToTypeExp (A.Mobile t) = ttte "MOBILE" A.Mobile t
|
||||||
typeToTypeExp (A.UnknownVarType en)
|
typeToTypeExp (A.UnknownVarType en)
|
||||||
= case en of
|
= case en of
|
||||||
Left n -> lookupMapElseMutVar (UnifyIndex (A.nameMeta n, Right n))
|
Left n -> lookupMapElseMutVar (UnifyIndex (A.nameMeta n, Right n))
|
||||||
|
@ -74,7 +74,7 @@ typeToTypeExp (A.UnknownNumLitType m id n)
|
||||||
let mp = csUnifyLookup st
|
let mp = csUnifyLookup st
|
||||||
put st {csUnifyLookup = Map.insert (UnifyIndex (m,Left id)) v mp}
|
put st {csUnifyLookup = Map.insert (UnifyIndex (m,Left id)) v mp}
|
||||||
return v
|
return v
|
||||||
typeToTypeExp t = return $ OperType (toConstr t) []
|
typeToTypeExp t = return $ OperType (show t) (const t) []
|
||||||
|
|
||||||
markUnify :: (Typed a, Typed b) => a -> b -> PassM ()
|
markUnify :: (Typed a, Typed b) => a -> b -> PassM ()
|
||||||
markUnify x y
|
markUnify x y
|
||||||
|
|
|
@ -19,23 +19,25 @@ with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||||
module TypeUnification where
|
module TypeUnification where
|
||||||
|
|
||||||
import Control.Monad
|
import Control.Monad
|
||||||
|
import Control.Monad.State
|
||||||
|
import Control.Monad.Trans
|
||||||
import Data.Generics
|
import Data.Generics
|
||||||
import qualified Data.Map as Map
|
import qualified Data.Map as Map
|
||||||
import Data.Maybe
|
import Data.Maybe
|
||||||
import Data.IORef
|
import Data.IORef
|
||||||
|
|
||||||
import qualified AST as A
|
import qualified AST as A
|
||||||
|
import Errors
|
||||||
|
import Metadata
|
||||||
import Pass
|
import Pass
|
||||||
import ShowCode
|
import ShowCode
|
||||||
import UnifyType
|
import UnifyType
|
||||||
import Utils
|
import Utils
|
||||||
|
|
||||||
foldCon :: Constr -> [Either String A.Type] -> Either String A.Type
|
foldCon :: ([A.Type] -> A.Type) -> [Either String A.Type] -> Either String A.Type
|
||||||
foldCon con [] = Right $ fromConstr con
|
foldCon con es = case splitEither es of
|
||||||
foldCon con [Left e] = Left e
|
([],ts) -> Right $ con ts
|
||||||
foldCon con [Right t] = Right $ fromConstrB (fromJust $ cast t) con
|
((e:_),_) -> Left e
|
||||||
foldCon con _ = Left "foldCon: too many arguments given"
|
|
||||||
|
|
||||||
|
|
||||||
-- Much of the code in this module is taken from or based on Tim Sheard's Haskell
|
-- Much of the code in this module is taken from or based on Tim Sheard's Haskell
|
||||||
-- listing of a simple type unification algorithm at the beginning of his
|
-- listing of a simple type unification algorithm at the beginning of his
|
||||||
|
@ -65,7 +67,7 @@ unifyRainTypes m' prs
|
||||||
[] -> return $ Right mapOfRes
|
[] -> return $ Right mapOfRes
|
||||||
where
|
where
|
||||||
read :: k -> TypeExp A.Type -> IO (Either String A.Type)
|
read :: k -> TypeExp A.Type -> IO (Either String A.Type)
|
||||||
read k (OperType con vals) = do vals' <- mapM (read k) vals
|
read k (OperType _ con vals) = do vals' <- mapM (read k) vals
|
||||||
return $ foldCon con vals'
|
return $ foldCon con vals'
|
||||||
read k (MutVar v) = readIORef v >>= \t -> case t of
|
read k (MutVar v) = readIORef v >>= \t -> case t of
|
||||||
Nothing -> return $ Left $ "Type error in unification, "
|
Nothing -> return $ Left $ "Type error in unification, "
|
||||||
|
@ -76,16 +78,23 @@ unifyRainTypes m' prs
|
||||||
++ "ambigious type remains for numeric literal: " ++ show k
|
++ "ambigious type remains for numeric literal: " ++ show k
|
||||||
Right t -> return $ Right t
|
Right t -> return $ Right t
|
||||||
|
|
||||||
|
fromTypeExp :: Meta -> TypeExp A.Type -> PassM A.Type
|
||||||
|
fromTypeExp m x = fromTypeExp' =<< (liftIO $ prune x)
|
||||||
|
where
|
||||||
|
fromTypeExp' :: TypeExp A.Type -> PassM A.Type
|
||||||
|
fromTypeExp' (MutVar {}) = dieP m "Unresolved type"
|
||||||
|
fromTypeExp' (GenVar {}) = dieP m "Template vars not yet supported"
|
||||||
|
fromTypeExp' (NumLit v) = liftIO (readIORef v) >>= \x -> case x of
|
||||||
|
Left (n:_) -> dieP m $ "Ambigiously typed numeric literal: " ++ show n
|
||||||
|
Right t -> return t
|
||||||
|
fromTypeExp' (OperType _ f ts) = mapM (fromTypeExp m) ts >>* f
|
||||||
|
|
||||||
-- For debugging:
|
-- For debugging:
|
||||||
showInErr :: TypeExp A.Type -> PassM String
|
showInErr :: TypeExp A.Type -> PassM String
|
||||||
showInErr (MutVar {}) = return "MutVar"
|
showInErr (MutVar {}) = return "MutVar"
|
||||||
showInErr (GenVar {}) = return "GenVar"
|
showInErr (GenVar {}) = return "GenVar"
|
||||||
showInErr (NumLit {}) = return "NumLit"
|
showInErr (NumLit {}) = return "NumLit"
|
||||||
showInErr (OperType c ts) = showCode $ case length ts of
|
showInErr t@(OperType {}) = showCode =<< fromTypeExp undefined t
|
||||||
0 -> fromConstr c :: A.Type
|
|
||||||
1 -> (fromConstr c :: A.Type -> A.Type)
|
|
||||||
(A.UserDataType $ A.Name {A.nameName = "a"})
|
|
||||||
:: A.Type
|
|
||||||
|
|
||||||
giveErr :: String -> TypeExp A.Type -> TypeExp A.Type -> Either (PassM String) a
|
giveErr :: String -> TypeExp A.Type -> TypeExp A.Type -> Either (PassM String) a
|
||||||
giveErr msg tx ty
|
giveErr msg tx ty
|
||||||
|
@ -93,7 +102,7 @@ giveErr msg tx ty
|
||||||
y <- showInErr ty
|
y <- showInErr ty
|
||||||
return $ msg ++ x ++ " and " ++ y
|
return $ msg ++ x ++ " and " ++ y
|
||||||
|
|
||||||
prune :: TypeExp a -> IO (TypeExp a)
|
prune :: Typeable a => TypeExp a -> IO (TypeExp a)
|
||||||
prune t =
|
prune t =
|
||||||
case t of
|
case t of
|
||||||
MutVar r ->
|
MutVar r ->
|
||||||
|
@ -106,15 +115,13 @@ prune t =
|
||||||
return t'
|
return t'
|
||||||
_ -> return t
|
_ -> return t
|
||||||
|
|
||||||
occursInType :: Ptr a -> TypeExp a -> IO Bool
|
occursInType :: Typeable a => Ptr a -> TypeExp a -> IO Bool
|
||||||
occursInType r t =
|
occursInType r t =
|
||||||
do t' <- prune t
|
do t' <- prune t
|
||||||
case t' of
|
case t' of
|
||||||
MutVar r2 -> return $ r == r2
|
MutVar r2 -> return $ r == r2
|
||||||
GenVar n -> return False
|
GenVar n -> return False
|
||||||
OperType nm ts ->
|
OperType _ _ ts -> mapM (occursInType r) ts >>* or
|
||||||
do bs <- mapM (occursInType r) ts
|
|
||||||
return (or bs)
|
|
||||||
|
|
||||||
unifyType :: TypeExp A.Type -> TypeExp A.Type -> IO (Either (PassM String) ())
|
unifyType :: TypeExp A.Type -> TypeExp A.Type -> IO (Either (PassM String) ())
|
||||||
unifyType te1 te2
|
unifyType te1 te2
|
||||||
|
@ -133,7 +140,7 @@ unifyType te1 te2
|
||||||
(_,MutVar _) -> unifyType t2' t1'
|
(_,MutVar _) -> unifyType t2' t1'
|
||||||
(GenVar n,GenVar m) ->
|
(GenVar n,GenVar m) ->
|
||||||
if n == m then return $ Right () else return $ Left $ return "different genvars"
|
if n == m then return $ Right () else return $ Left $ return "different genvars"
|
||||||
(OperType n1 ts1,OperType n2 ts2) ->
|
(OperType n1 _ ts1,OperType n2 _ ts2) ->
|
||||||
if n1 == n2
|
if n1 == n2
|
||||||
then unifyArgs ts1 ts2
|
then unifyArgs ts1 ts2
|
||||||
else return $ giveErr "Different constructors: " t1' t2'
|
else return $ giveErr "Different constructors: " t1' t2'
|
||||||
|
@ -147,7 +154,7 @@ unifyType te1 te2
|
||||||
else return $ Right ()
|
else return $ Right ()
|
||||||
(Left ns1, Left ns2) ->
|
(Left ns1, Left ns2) ->
|
||||||
do writeIORef vns1 $ Left (ns1 ++ ns2)
|
do writeIORef vns1 $ Left (ns1 ++ ns2)
|
||||||
writeIORef vns2 $ Left (ns1 ++ ns2)
|
writeIORef vns2 $ Left (ns2 ++ ns1)
|
||||||
return $ Right ()
|
return $ Right ()
|
||||||
(Right {}, Left {}) -> unifyType t2' t1'
|
(Right {}, Left {}) -> unifyType t2' t1'
|
||||||
(Left ns1, Right t2) ->
|
(Left ns1, Right t2) ->
|
||||||
|
@ -156,18 +163,18 @@ unifyType te1 te2
|
||||||
return $ Right ()
|
return $ Right ()
|
||||||
else return $ Left $ return "Numeric literals will not fit in concrete type"
|
else return $ Left $ return "Numeric literals will not fit in concrete type"
|
||||||
(OperType {}, NumLit {}) -> unifyType t2' t1'
|
(OperType {}, NumLit {}) -> unifyType t2' t1'
|
||||||
(NumLit vns1, OperType n1 ts2) ->
|
(NumLit vns1, OperType n1 f ts2) ->
|
||||||
do nst1 <- readIORef vns1
|
do nst1 <- readIORef vns1
|
||||||
case nst1 of
|
case nst1 of
|
||||||
Right t ->
|
Right t ->
|
||||||
if null ts2 && t == fromConstr n1
|
if null ts2 && t == f []
|
||||||
then return $ Right ()
|
then return $ Right ()
|
||||||
else return $ Left $ return $ "numeric literal cannot be unified"
|
else return $ Left $ return $ "numeric literal cannot be unified"
|
||||||
++ " with two different types"
|
++ " with two different types"
|
||||||
Left ns ->
|
Left ns ->
|
||||||
if null ts2
|
if null ts2
|
||||||
then if all (willFit $ fromConstr n1) ns
|
then if all (willFit $ f []) ns
|
||||||
then do writeIORef vns1 $ Right (fromConstr n1)
|
then do writeIORef vns1 $ Right (f [])
|
||||||
return $ Right ()
|
return $ Right ()
|
||||||
else return $ Left $ return "Numeric literals will not fit in concrete type"
|
else return $ Left $ return "Numeric literals will not fit in concrete type"
|
||||||
else return $ Left $ return $ "Numeric literal cannot be unified"
|
else return $ Left $ return $ "Numeric literal cannot be unified"
|
||||||
|
@ -181,10 +188,10 @@ unifyType te1 te2
|
||||||
unifyArgs [] [] = return $ Right ()
|
unifyArgs [] [] = return $ Right ()
|
||||||
unifyArgs _ _ = return $ Left $ return "different lengths"
|
unifyArgs _ _ = return $ Left $ return "different lengths"
|
||||||
|
|
||||||
instantiate :: [TypeExp a] -> TypeExp a -> TypeExp a
|
instantiate :: Typeable a => [TypeExp a] -> TypeExp a -> TypeExp a
|
||||||
instantiate ts x = case x of
|
instantiate ts x = case x of
|
||||||
MutVar _ -> x
|
MutVar _ -> x
|
||||||
OperType nm xs -> OperType nm (map (instantiate ts) xs)
|
OperType nm f xs -> OperType nm f (map (instantiate ts) xs)
|
||||||
GenVar n -> ts !! n
|
GenVar n -> ts !! n
|
||||||
|
|
||||||
willFit :: A.Type -> Integer -> Bool
|
willFit :: A.Type -> Integer -> Bool
|
||||||
|
|
|
@ -25,46 +25,10 @@ import qualified AST as A
|
||||||
|
|
||||||
type Ptr a = IORef (Maybe (TypeExp a))
|
type Ptr a = IORef (Maybe (TypeExp a))
|
||||||
|
|
||||||
data TypeExp a
|
data Typeable a => TypeExp a
|
||||||
= MutVar (Ptr a)
|
= MutVar (Ptr a)
|
||||||
| GenVar Int
|
| GenVar Int
|
||||||
-- Either a list of integers that must fit, or a concrete type
|
-- Either a list of integers that must fit, or a concrete type
|
||||||
| NumLit (IORef (Either [Integer] A.Type))
|
| NumLit (IORef (Either [Integer] A.Type))
|
||||||
| OperType Constr [ TypeExp a ]
|
| OperType String ([A.Type] -> A.Type) [ TypeExp a ]
|
||||||
deriving (Typeable)
|
deriving (Typeable, Data)
|
||||||
|
|
||||||
-- Because Constr is not a member of Data, we must provide our own Data instance
|
|
||||||
-- here:
|
|
||||||
|
|
||||||
_typeExp_MutVarConstr, _typeExp_GenVarConstr, _typeExp_NumLitConstr,
|
|
||||||
_typeExp_OperTypeConstr :: Constr
|
|
||||||
_typeExp_DataType :: DataType
|
|
||||||
|
|
||||||
_typeExp_MutVarConstr = mkConstr _typeExp_DataType "MutVar" [] Prefix
|
|
||||||
_typeExp_GenVarConstr = mkConstr _typeExp_DataType "GenVar" [] Prefix
|
|
||||||
_typeExp_NumLitConstr = mkConstr _typeExp_DataType "NumLit" [] Prefix
|
|
||||||
_typeExp_OperTypeConstr = mkConstr _typeExp_DataType "OperType" [] Prefix
|
|
||||||
_typeExp_DataType = mkDataType "TypeUnification.TypeExp"
|
|
||||||
[ _typeExp_MutVarConstr
|
|
||||||
, _typeExp_GenVarConstr
|
|
||||||
, _typeExp_NumLitConstr
|
|
||||||
, _typeExp_OperTypeConstr
|
|
||||||
]
|
|
||||||
|
|
||||||
instance Data a => Data (TypeExp a) where
|
|
||||||
gfoldl f z (MutVar x) = z MutVar `f` x
|
|
||||||
gfoldl f z (GenVar x) = z GenVar `f` x
|
|
||||||
gfoldl f z (NumLit x) = z NumLit `f` x
|
|
||||||
-- We leave the Constr item untouched, as it is not of type Data:
|
|
||||||
gfoldl f z (OperType x y) = z (OperType x) `f` y
|
|
||||||
toConstr (MutVar {}) = _typeExp_MutVarConstr
|
|
||||||
toConstr (GenVar {}) = _typeExp_GenVarConstr
|
|
||||||
toConstr (NumLit {}) = _typeExp_NumLitConstr
|
|
||||||
toConstr (OperType {}) = _typeExp_OperTypeConstr
|
|
||||||
gunfold k z c = case constrIndex c of
|
|
||||||
1 -> (k) (z MutVar)
|
|
||||||
2 -> (k) (z GenVar)
|
|
||||||
3 -> (k) (z NumLit)
|
|
||||||
4 -> error "gunfold typeExp OperType"
|
|
||||||
_ -> error "gunfold typeExp"
|
|
||||||
dataTypeOf _ = _typeExp_DataType
|
|
||||||
|
|
Loading…
Reference in New Issue
Block a user