Added Meta tags all over the place in the type unification to give better error messages
This commit is contained in:
Neil Brown
parent
6afea19ee6
commit
4429dfc051
|
|
@ -44,44 +44,45 @@ lookupMapElseMutVar k
|
|||
case Map.lookup k m of
|
||||
Just v -> return v
|
||||
Nothing -> do r <- liftIO $ newIORef Nothing
|
||||
let v = MutVar r
|
||||
let UnifyIndex (mt,_) = k
|
||||
v = MutVar mt r
|
||||
m' = Map.insert k v m
|
||||
put st {csUnifyLookup = m'}
|
||||
return v
|
||||
|
||||
ttte :: String -> (A.Type -> A.Type) -> A.Type -> PassM (TypeExp A.Type)
|
||||
ttte c f t = typeToTypeExp t >>= \t' -> return $ OperType c (\[x] -> f x) [t']
|
||||
ttte :: Meta -> String -> (A.Type -> A.Type) -> A.Type -> PassM (TypeExp A.Type)
|
||||
ttte m c f t = typeToTypeExp m t >>= \t' -> return $ OperType m c (\[x] -> f x) [t']
|
||||
|
||||
-- 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
|
||||
-- (which would require unification of dimensions and such) are not supported,
|
||||
-- neither are records.
|
||||
-- User data types should not be present in the input.
|
||||
typeToTypeExp :: A.Type -> PassM (TypeExp A.Type)
|
||||
typeToTypeExp (A.List t) = ttte "[]" A.List t
|
||||
typeToTypeExp (A.Chan A.DirInput at t) = ttte "?" (A.Chan A.DirInput at) t
|
||||
typeToTypeExp (A.Chan A.DirOutput at t) = ttte "!" (A.Chan A.DirOutput at) t
|
||||
typeToTypeExp (A.Chan A.DirUnknown at t) = ttte "channel" (A.Chan A.DirUnknown at) t
|
||||
typeToTypeExp (A.Mobile t) = ttte "MOBILE" A.Mobile t
|
||||
typeToTypeExp (A.UnknownVarType en)
|
||||
typeToTypeExp :: Meta -> A.Type -> PassM (TypeExp A.Type)
|
||||
typeToTypeExp m (A.List t) = ttte m "[]" A.List t
|
||||
typeToTypeExp m (A.Chan A.DirInput at t) = ttte m "?" (A.Chan A.DirInput at) t
|
||||
typeToTypeExp m (A.Chan A.DirOutput at t) = ttte m "!" (A.Chan A.DirOutput at) t
|
||||
typeToTypeExp m (A.Chan A.DirUnknown at t) = ttte m "channel" (A.Chan A.DirUnknown at) t
|
||||
typeToTypeExp m (A.Mobile t) = ttte m "MOBILE" A.Mobile t
|
||||
typeToTypeExp _ (A.UnknownVarType en)
|
||||
= case en of
|
||||
Left n -> lookupMapElseMutVar (UnifyIndex (A.nameMeta n, Right n))
|
||||
Right (m, i) -> lookupMapElseMutVar (UnifyIndex (m, Left i))
|
||||
typeToTypeExp (A.UnknownNumLitType m id n)
|
||||
= do r <- liftIO . newIORef $ Left [n]
|
||||
let v = NumLit r
|
||||
typeToTypeExp _ (A.UnknownNumLitType m id n)
|
||||
= do r <- liftIO . newIORef $ Left [(m,n)]
|
||||
let v = NumLit m r
|
||||
st <- get
|
||||
let mp = csUnifyLookup st
|
||||
put st {csUnifyLookup = Map.insert (UnifyIndex (m,Left id)) v mp}
|
||||
return v
|
||||
typeToTypeExp t = return $ OperType (show t) (const t) []
|
||||
typeToTypeExp m t = return $ OperType m (show t) (const t) []
|
||||
|
||||
markUnify :: (Typed a, Typed b) => a -> b -> PassM ()
|
||||
markUnify :: (Typed a, Typed b, Data a, Data b) => a -> b -> PassM ()
|
||||
markUnify x y
|
||||
= do tx <- astTypeOf x
|
||||
ty <- astTypeOf y
|
||||
tex <- typeToTypeExp tx
|
||||
tey <- typeToTypeExp ty
|
||||
tex <- typeToTypeExp (findMeta x) tx
|
||||
tey <- typeToTypeExp (findMeta y) ty
|
||||
modify $ \st -> st {csUnifyPairs = (tex,tey) : csUnifyPairs st}
|
||||
|
||||
|
||||
|
|
@ -101,11 +102,10 @@ performTypeUnification x
|
|||
$ x
|
||||
-- Then, we do the unification:
|
||||
prs <- get >>* csUnifyPairs
|
||||
res <- liftIO $ mapM (uncurry unifyType) prs
|
||||
mapM (diePC emptyMeta) (fst $ splitEither res)
|
||||
mapM_ (uncurry unifyType) prs
|
||||
-- Now put the types back in a map, and replace them through the tree:
|
||||
l <- get >>* csUnifyLookup
|
||||
ts <- mapMapWithKeyM (\(UnifyIndex(m,_)) v -> fromTypeExp m v) l
|
||||
ts <- mapMapM (\v -> fromTypeExp v) l
|
||||
get >>= substituteUnknownTypes ts >>= put
|
||||
substituteUnknownTypes ts x'
|
||||
where
|
||||
|
|
@ -116,7 +116,7 @@ performTypeUnification x
|
|||
shift' (rawName, d) = do mt <- typeOfSpec (A.ndType d)
|
||||
case mt of
|
||||
Nothing -> return Nothing
|
||||
Just t -> do te <- typeToTypeExp t
|
||||
Just t -> do te <- typeToTypeExp (A.ndMeta d) t
|
||||
return $ Just (UnifyIndex (A.ndMeta d, Right name), te)
|
||||
where
|
||||
name = A.Name {A.nameName = rawName, A.nameMeta = A.ndMeta d, A.nameType
|
||||
|
|
|
|||
|
|
@ -45,13 +45,11 @@ foldCon con es = case splitEither es of
|
|||
-- Pearl (2001)", citeseer: http://citeseer.ist.psu.edu/451401.html
|
||||
-- This in turn was taken from Luca Cardelli's "Basic Polymorphic Type Checking"
|
||||
|
||||
unifyRainTypes :: forall k. (Ord k, Show k) => (Map.Map k (TypeExp A.Type)) -> [(k, k)] -> IO
|
||||
(Either (PassM String) (Map.Map k A.Type))
|
||||
unifyRainTypes :: forall k. (Ord k, Show k) => (Map.Map k (TypeExp A.Type)) -> [(k, k)] ->
|
||||
PassM (Map.Map k A.Type)
|
||||
unifyRainTypes m' prs
|
||||
= do outs <- mapM (\(x,y) -> unifyType (lookupStartType x m') (lookupStartType y m')) prs
|
||||
case mapMaybe (either Just (const Nothing)) outs of
|
||||
(err:_) -> return $ Left err
|
||||
[] -> stToMap m'
|
||||
= do mapM_ (\(x,y) -> unifyType (lookupStartType x m') (lookupStartType y m')) prs
|
||||
stToMap m'
|
||||
where
|
||||
lookupStartType :: k -> Map.Map k (TypeExp A.Type) -> TypeExp A.Type
|
||||
lookupStartType s m = case Map.lookup s m of
|
||||
|
|
@ -59,53 +57,56 @@ unifyRainTypes m' prs
|
|||
Nothing -> error $ "Could not find type for variable in map before unification: "
|
||||
++ show s
|
||||
|
||||
stToMap :: Map.Map k (TypeExp A.Type) -> IO (Either (PassM String) (Map.Map k A.Type))
|
||||
stToMap m = do m' <- mapMapWithKeyM (\k v -> prune v >>= read k) m
|
||||
stToMap :: Map.Map k (TypeExp A.Type) -> PassM (Map.Map k A.Type)
|
||||
stToMap m = do m' <- liftIO $ mapMapWithKeyM (\k v -> prune v >>= read k) m
|
||||
let (mapOfErrs, mapOfRes) = Map.mapEitherWithKey (const id) m'
|
||||
case Map.elems mapOfErrs of
|
||||
(e:_) -> return $ Left $ return e
|
||||
[] -> return $ Right mapOfRes
|
||||
((m,e):_) -> dieP m e
|
||||
[] -> return mapOfRes
|
||||
where
|
||||
read :: k -> TypeExp A.Type -> IO (Either String A.Type)
|
||||
read k (OperType _ con vals) = do vals' <- mapM (read k) vals
|
||||
return $ foldCon con vals'
|
||||
read k (MutVar v) = readIORef v >>= \t -> case t of
|
||||
Nothing -> return $ Left $ "Type error in unification, "
|
||||
++ "ambigious type remains for: " ++ show k
|
||||
read :: k -> TypeExp A.Type -> IO (Either (Meta, String) A.Type)
|
||||
read k (OperType m _ con vals)
|
||||
= do vals' <- mapM (read k) vals
|
||||
case foldCon con (map (either (Left . snd) Right) vals') of
|
||||
Left e -> return $ Left (m, e)
|
||||
Right x -> return $ Right x
|
||||
read k (MutVar m v) = readIORef v >>= \t -> case t of
|
||||
Nothing -> return $ Left (m, "Type error in unification, "
|
||||
++ "ambigious type remains for: " ++ show k)
|
||||
Just t' -> read k t'
|
||||
read k (NumLit v) = readIORef v >>= \x -> case x of
|
||||
Left _ -> return $ Left $ "Type error in unification, "
|
||||
++ "ambigious type remains for numeric literal: " ++ show k
|
||||
read k (NumLit m v) = readIORef v >>= \x -> case x of
|
||||
Left _ -> return $ Left (m, "Type error in unification, "
|
||||
++ "ambigious type remains for numeric literal: " ++ show k)
|
||||
Right t -> return $ Right t
|
||||
|
||||
fromTypeExp :: Meta -> TypeExp A.Type -> PassM A.Type
|
||||
fromTypeExp m x = fromTypeExp' =<< (liftIO $ prune x)
|
||||
fromTypeExp :: TypeExp A.Type -> PassM A.Type
|
||||
fromTypeExp 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
|
||||
fromTypeExp' (MutVar m _) = dieP m "Unresolved type"
|
||||
fromTypeExp' (GenVar m _) = dieP m "Template vars not yet supported"
|
||||
fromTypeExp' (NumLit m 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
|
||||
fromTypeExp' (OperType _ _ f ts) = mapM fromTypeExp ts >>* f
|
||||
|
||||
-- For debugging:
|
||||
showInErr :: TypeExp A.Type -> PassM String
|
||||
showInErr (MutVar {}) = return "MutVar"
|
||||
showInErr (GenVar {}) = return "GenVar"
|
||||
showInErr (NumLit {}) = return "NumLit"
|
||||
showInErr t@(OperType {}) = showCode =<< fromTypeExp undefined t
|
||||
showInErr t@(OperType {}) = showCode =<< fromTypeExp t
|
||||
|
||||
giveErr :: String -> TypeExp A.Type -> TypeExp A.Type -> Either (PassM String) a
|
||||
giveErr msg tx ty
|
||||
= Left $ do x <- showInErr tx
|
||||
giveErr :: Meta -> String -> TypeExp A.Type -> TypeExp A.Type -> PassM a
|
||||
giveErr m msg tx ty
|
||||
= do x <- showInErr tx
|
||||
y <- showInErr ty
|
||||
return $ msg ++ x ++ " and " ++ y
|
||||
dieP m $ msg ++ x ++ " and " ++ y
|
||||
|
||||
prune :: Typeable a => TypeExp a -> IO (TypeExp a)
|
||||
prune t =
|
||||
case t of
|
||||
MutVar r ->
|
||||
MutVar _ r ->
|
||||
do m <- readIORef r
|
||||
case m of
|
||||
Nothing -> return t
|
||||
|
|
@ -119,80 +120,75 @@ occursInType :: Typeable a => Ptr a -> TypeExp a -> IO Bool
|
|||
occursInType r t =
|
||||
do t' <- prune t
|
||||
case t' of
|
||||
MutVar r2 -> return $ r == r2
|
||||
GenVar n -> return False
|
||||
OperType _ _ ts -> mapM (occursInType r) ts >>* or
|
||||
MutVar _ r2 -> return $ r == r2
|
||||
GenVar _ n -> return False
|
||||
OperType _ _ _ ts -> mapM (occursInType r) ts >>* or
|
||||
|
||||
unifyType :: TypeExp A.Type -> TypeExp A.Type -> IO (Either (PassM String) ())
|
||||
unifyType :: TypeExp A.Type -> TypeExp A.Type -> PassM ()
|
||||
unifyType te1 te2
|
||||
= do t1' <- prune te1
|
||||
t2' <- prune te2
|
||||
= do t1' <- liftIO $ prune te1
|
||||
t2' <- liftIO $ prune te2
|
||||
case (t1',t2') of
|
||||
(MutVar r1, MutVar r2) ->
|
||||
(MutVar _ r1, MutVar _ r2) ->
|
||||
if r1 == r2
|
||||
then return $ Right ()
|
||||
else liftM Right $ writeIORef r1 (Just t2')
|
||||
(MutVar r1, _) ->
|
||||
do b <- occursInType r1 t2'
|
||||
then return ()
|
||||
else liftIO $ writeIORef r1 (Just t2')
|
||||
(MutVar m r1, _) ->
|
||||
do b <- liftIO $ occursInType r1 t2'
|
||||
if b
|
||||
then return $ Left $ return "occurs in"
|
||||
else liftM Right $ writeIORef r1 (Just t2')
|
||||
(_,MutVar _) -> unifyType t2' t1'
|
||||
(GenVar n,GenVar m) ->
|
||||
if n == m then return $ Right () else return $ Left $ return "different genvars"
|
||||
(OperType n1 _ ts1,OperType n2 _ ts2) ->
|
||||
then dieP m "Infinitely recursive type formed"
|
||||
else liftIO $ writeIORef r1 (Just t2')
|
||||
(_,MutVar {}) -> unifyType t2' t1'
|
||||
(GenVar m x,GenVar _ y) ->
|
||||
if x == y then return () else dieP m $ "different template variables"
|
||||
++ " cannot be assumed to be equal"
|
||||
(OperType m1 n1 _ ts1,OperType m2 n2 _ ts2) ->
|
||||
if n1 == n2
|
||||
then unifyArgs ts1 ts2
|
||||
else return $ giveErr "Different constructors: " t1' t2'
|
||||
(NumLit vns1, NumLit vns2) ->
|
||||
do nst1 <- readIORef vns1
|
||||
nst2 <- readIORef vns2
|
||||
else giveErr m1 "Type cannot be matched: " t1' t2'
|
||||
(NumLit m1 vns1, NumLit m2 vns2) ->
|
||||
do nst1 <- liftIO $ readIORef vns1
|
||||
nst2 <- liftIO $ readIORef vns2
|
||||
case (nst1, nst2) of
|
||||
(Right t1, Right t2) ->
|
||||
if t1 /= t2
|
||||
then return $ Left $ return "Numeric literals bound to different types"
|
||||
else return $ Right ()
|
||||
then dieP m1 "Numeric literals bound to different types"
|
||||
else return ()
|
||||
(Left ns1, Left ns2) ->
|
||||
do writeIORef vns1 $ Left (ns1 ++ ns2)
|
||||
writeIORef vns2 $ Left (ns2 ++ ns1)
|
||||
return $ Right ()
|
||||
do liftIO $ writeIORef vns1 $ Left (ns1 ++ ns2)
|
||||
liftIO $ writeIORef vns2 $ Left (ns2 ++ ns1)
|
||||
(Right {}, Left {}) -> unifyType t2' t1'
|
||||
(Left ns1, Right t2) ->
|
||||
if all (willFit t2) ns1
|
||||
then do writeIORef vns1 (Right t2)
|
||||
return $ Right ()
|
||||
else return $ Left $ return "Numeric literals will not fit in concrete type"
|
||||
if all (willFit t2) (map snd ns1)
|
||||
then liftIO $ writeIORef vns1 (Right t2)
|
||||
else dieP m1 "Numeric literals will not fit in concrete type"
|
||||
(OperType {}, NumLit {}) -> unifyType t2' t1'
|
||||
(NumLit vns1, OperType n1 f ts2) ->
|
||||
do nst1 <- readIORef vns1
|
||||
(NumLit m1 vns1, OperType m2 n2 f ts2) ->
|
||||
do nst1 <- liftIO $ readIORef vns1
|
||||
case nst1 of
|
||||
Right t ->
|
||||
if null ts2 && t == f []
|
||||
then return $ Right ()
|
||||
else return $ Left $ return $ "numeric literal cannot be unified"
|
||||
then return ()
|
||||
else dieP m1 $ "numeric literal cannot be unified"
|
||||
++ " with two different types"
|
||||
Left ns ->
|
||||
if null ts2
|
||||
then if all (willFit $ f []) ns
|
||||
then do writeIORef vns1 $ Right (f [])
|
||||
return $ Right ()
|
||||
else return $ Left $ return "Numeric literals will not fit in concrete type"
|
||||
else return $ Left $ return $ "Numeric literal cannot be unified"
|
||||
then if all (willFit $ f []) (map snd ns)
|
||||
then liftIO $ writeIORef vns1 $ Right (f [])
|
||||
else dieP m1 "Numeric literals will not fit in concrete type"
|
||||
else dieP m1 $ "Numeric literal cannot be unified"
|
||||
++ " with non-numeric type"
|
||||
(_,_) -> return $ Left $ return "different types"
|
||||
(t,_) -> dieP (findMeta t) "different types"
|
||||
where
|
||||
unifyArgs (x:xs) (y:ys) = do r <- unifyType x y
|
||||
case r of
|
||||
Left _ -> return r
|
||||
Right _ -> unifyArgs xs ys
|
||||
unifyArgs [] [] = return $ Right ()
|
||||
unifyArgs _ _ = return $ Left $ return "different lengths"
|
||||
unifyArgs (x:xs) (y:ys) = unifyType x y >> unifyArgs xs ys
|
||||
unifyArgs [] [] = return ()
|
||||
unifyArgs xs ys = dieP (findMeta (xs,ys)) "different lengths"
|
||||
|
||||
instantiate :: Typeable a => [TypeExp a] -> TypeExp a -> TypeExp a
|
||||
instantiate ts x = case x of
|
||||
MutVar _ -> x
|
||||
OperType nm f xs -> OperType nm f (map (instantiate ts) xs)
|
||||
GenVar n -> ts !! n
|
||||
MutVar _ _ -> x
|
||||
OperType m nm f xs -> OperType m nm f (map (instantiate ts) xs)
|
||||
GenVar _ n -> ts !! n
|
||||
|
||||
willFit :: A.Type -> Integer -> Bool
|
||||
willFit t n = case bounds t of
|
||||
|
|
|
|||
|
|
@ -22,13 +22,14 @@ import Data.Generics
|
|||
import Data.IORef
|
||||
|
||||
import qualified AST as A
|
||||
import Metadata
|
||||
|
||||
type Ptr a = IORef (Maybe (TypeExp a))
|
||||
|
||||
data Typeable a => TypeExp a
|
||||
= MutVar (Ptr a)
|
||||
| GenVar Int
|
||||
= MutVar Meta (Ptr a)
|
||||
| GenVar Meta Int
|
||||
-- Either a list of integers that must fit, or a concrete type
|
||||
| NumLit (IORef (Either [Integer] A.Type))
|
||||
| OperType String ([A.Type] -> A.Type) [ TypeExp a ]
|
||||
| NumLit Meta (IORef (Either [(Meta, Integer)] A.Type))
|
||||
| OperType Meta String ([A.Type] -> A.Type) [ TypeExp a ]
|
||||
deriving (Typeable, Data)
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user