Added unifying-related items to CompState, and changed all the uses of ST to IO in the TypeUnification module
As part of this patch I also had to provide a Data instance for TypeExp (to allow CompState to still be an instance of Data). Using IORefs is easier than STRef RealWorld, and puts everything in terms of IO (which is already in PassM) rather than ST (which would require more lifting).
This commit is contained in:
parent
e6162877af
commit
f8b7e8f8cb
|
@ -34,6 +34,7 @@ import qualified AST as A
|
||||||
import Errors (Die, dieP, ErrorReport, Warn, warnP)
|
import Errors (Die, dieP, ErrorReport, Warn, warnP)
|
||||||
import Metadata
|
import Metadata
|
||||||
import OrdAST ()
|
import OrdAST ()
|
||||||
|
import TypeUnification
|
||||||
|
|
||||||
-- | Modes that Tock can run in.
|
-- | Modes that Tock can run in.
|
||||||
data CompMode = ModeFlowGraph | ModeParse | ModeCompile | ModePostC | ModeFull
|
data CompMode = ModeFlowGraph | ModeParse | ModeCompile | ModePostC | ModeFull
|
||||||
|
@ -57,6 +58,23 @@ data PreprocDef =
|
||||||
-- | An item that has been pulled up.
|
-- | An item that has been pulled up.
|
||||||
type PulledItem = (Meta, Either A.Specification A.Process) -- Either Spec or ProcThen
|
type PulledItem = (Meta, Either A.Specification A.Process) -- Either Spec or ProcThen
|
||||||
|
|
||||||
|
-- | An index to identify an item involved in the type unification.
|
||||||
|
newtype UnifyIndex = UnifyIndex (Meta, Either Int A.Name)
|
||||||
|
deriving (Typeable, Data)
|
||||||
|
|
||||||
|
instance Show UnifyIndex where
|
||||||
|
show (UnifyIndex (m,u)) = show m ++ ": " ++ either (const "<anon>") show u
|
||||||
|
|
||||||
|
instance Eq UnifyIndex where
|
||||||
|
(UnifyIndex (_,u)) == (UnifyIndex (_,u')) = u == u'
|
||||||
|
|
||||||
|
instance Ord UnifyIndex where
|
||||||
|
compare (UnifyIndex (_,u)) (UnifyIndex (_,u'))
|
||||||
|
= compare u u'
|
||||||
|
|
||||||
|
-- | An entry in the map corresponding to a UnifyIndex
|
||||||
|
type UnifyValue = TypeExp A.Type
|
||||||
|
|
||||||
-- | State necessary for compilation.
|
-- | State necessary for compilation.
|
||||||
data CompState = CompState {
|
data CompState = CompState {
|
||||||
-- This structure needs to be printable with pshow.
|
-- This structure needs to be printable with pshow.
|
||||||
|
@ -92,7 +110,9 @@ data CompState = CompState {
|
||||||
csFunctionReturns :: Map String [A.Type],
|
csFunctionReturns :: Map String [A.Type],
|
||||||
csPulledItems :: [[PulledItem]],
|
csPulledItems :: [[PulledItem]],
|
||||||
csAdditionalArgs :: Map String [A.Actual],
|
csAdditionalArgs :: Map String [A.Actual],
|
||||||
csParProcs :: Set A.Name
|
csParProcs :: Set A.Name,
|
||||||
|
csUnifyLookup :: Map UnifyIndex UnifyValue,
|
||||||
|
csUnifyPairs :: [(UnifyValue, UnifyValue)]
|
||||||
}
|
}
|
||||||
deriving (Data, Typeable)
|
deriving (Data, Typeable)
|
||||||
|
|
||||||
|
@ -122,7 +142,9 @@ emptyState = CompState {
|
||||||
csFunctionReturns = Map.empty,
|
csFunctionReturns = Map.empty,
|
||||||
csPulledItems = [],
|
csPulledItems = [],
|
||||||
csAdditionalArgs = Map.empty,
|
csAdditionalArgs = Map.empty,
|
||||||
csParProcs = Set.empty
|
csParProcs = Set.empty,
|
||||||
|
csUnifyLookup = Map.empty,
|
||||||
|
csUnifyPairs = []
|
||||||
}
|
}
|
||||||
|
|
||||||
-- | Class of monads which keep a CompState.
|
-- | Class of monads which keep a CompState.
|
||||||
|
|
|
@ -19,11 +19,10 @@ 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.ST
|
|
||||||
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.STRef
|
import Data.IORef
|
||||||
|
|
||||||
import qualified AST as A
|
import qualified AST as A
|
||||||
import Utils
|
import Utils
|
||||||
|
@ -41,95 +40,106 @@ foldCon con _ = Left "foldCon: too many arguments given"
|
||||||
-- Pearl (2001)", citeseer: http://citeseer.ist.psu.edu/451401.html
|
-- Pearl (2001)", citeseer: http://citeseer.ist.psu.edu/451401.html
|
||||||
-- This in turn was taken from Luca Cardelli's "Basic Polymorphic Type Checking"
|
-- This in turn was taken from Luca Cardelli's "Basic Polymorphic Type Checking"
|
||||||
|
|
||||||
unifyRainTypes :: forall k. (Ord k, Show k) => Map.Map k A.Type -> [(k, k)] -> Either String
|
unifyRainTypes :: forall k. (Ord k, Show k) => (Map.Map k (TypeExp A.Type)) -> [(k, k)] -> IO
|
||||||
(Map.Map k A.Type)
|
(Either String (Map.Map k A.Type))
|
||||||
unifyRainTypes m prs
|
unifyRainTypes m' prs
|
||||||
= runST $ do m' <- mapToST m
|
= do outs <- mapM (\(x,y) -> unifyType (lookupStartType x m') (lookupStartType y m')) prs
|
||||||
outs <- mapM (\(x,y) -> unifyType (lookupStartType x m') (lookupStartType y
|
|
||||||
m')) prs
|
|
||||||
case mapMaybe (either Just (const Nothing)) outs of
|
case mapMaybe (either Just (const Nothing)) outs of
|
||||||
(err:_) -> return $ Left err
|
(err:_) -> return $ Left err
|
||||||
[] -> stToMap m'
|
[] -> stToMap m'
|
||||||
where
|
where
|
||||||
lookupStartType :: k -> Map.Map k (TypeExp s A.Type) -> TypeExp
|
lookupStartType :: k -> Map.Map k (TypeExp A.Type) -> TypeExp A.Type
|
||||||
s A.Type
|
|
||||||
lookupStartType s m = case Map.lookup s m of
|
lookupStartType s m = case Map.lookup s m of
|
||||||
Just x -> x
|
Just x -> x
|
||||||
Nothing -> error $ "Could not find type for variable in map before unification: "
|
Nothing -> error $ "Could not find type for variable in map before unification: "
|
||||||
++ show s
|
++ show s
|
||||||
|
|
||||||
mapToST :: Map.Map k A.Type -> ST s (Map.Map k (TypeExp s A.Type))
|
stToMap :: Map.Map k (TypeExp A.Type) -> IO (Either String (Map.Map k A.Type))
|
||||||
mapToST = mapMapM typeToTypeExp
|
|
||||||
|
|
||||||
stToMap :: Map.Map k (TypeExp s A.Type) -> ST s (Either String (Map.Map k A.Type))
|
|
||||||
stToMap m = do m' <- mapMapWithKeyM (\k v -> prune v >>= read k) m
|
stToMap m = do m' <- mapMapWithKeyM (\k v -> prune v >>= read k) m
|
||||||
let (mapOfErrs, mapOfRes) = Map.mapEitherWithKey (const id) m'
|
let (mapOfErrs, mapOfRes) = Map.mapEitherWithKey (const id) m'
|
||||||
case Map.elems mapOfErrs of
|
case Map.elems mapOfErrs of
|
||||||
(e:_) -> return $ Left e
|
(e:_) -> return $ Left e
|
||||||
[] -> return $ Right mapOfRes
|
[] -> return $ Right mapOfRes
|
||||||
where
|
where
|
||||||
read :: k -> TypeExp s A.Type -> ST s (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) = readSTRef 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, "
|
||||||
++ "ambigious type remains for: " ++ show k
|
++ "ambigious type remains for: " ++ show k
|
||||||
Just t' -> read k t'
|
Just t' -> read k t'
|
||||||
read k (NumLit v) = readSTRef v >>= \x -> case x of
|
read k (NumLit v) = readIORef v >>= \x -> case x of
|
||||||
Left _ -> return $ Left $ "Type error in unification, "
|
Left _ -> return $ Left $ "Type error in unification, "
|
||||||
++ "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
|
||||||
|
|
||||||
ttte :: Data b => b -> A.Type -> ST s (TypeExp s A.Type)
|
type Ptr a = IORef (Maybe (TypeExp a))
|
||||||
ttte c t = typeToTypeExp t >>= \t' -> return $ OperType (toConstr c) [t']
|
|
||||||
|
|
||||||
-- Transforms the given type into a typeexp, such that the only inner types
|
data TypeExp a
|
||||||
-- left will be the primitive types (integer types, float types, bool, time). Arrays
|
= MutVar (Ptr a)
|
||||||
-- (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 -> ST s (TypeExp s A.Type)
|
|
||||||
typeToTypeExp x@(A.List t) = ttte x t
|
|
||||||
typeToTypeExp (A.Chan A.DirInput _ t) = ttte "?" t
|
|
||||||
typeToTypeExp (A.Chan A.DirOutput _ t) = ttte "!" t
|
|
||||||
typeToTypeExp (A.Chan A.DirUnknown _ t) = ttte "channel" t
|
|
||||||
typeToTypeExp (A.Mobile t) = ttte "MOBILE" t
|
|
||||||
typeToTypeExp (A.Infer) = do r <- newSTRef Nothing
|
|
||||||
return $ MutVar r
|
|
||||||
typeToTypeExp (A.InferNum n) = do r <- newSTRef $ Left [n]
|
|
||||||
return $ NumLit r
|
|
||||||
typeToTypeExp t = return $ OperType (toConstr t) []
|
|
||||||
|
|
||||||
type Ptr s a = STRef s (Maybe (TypeExp s a))
|
|
||||||
|
|
||||||
data TypeExp s a
|
|
||||||
= MutVar (Ptr s 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 (STRef s (Either [Integer] A.Type))
|
| NumLit (IORef (Either [Integer] A.Type))
|
||||||
| OperType Constr [ TypeExp s a ]
|
| OperType Constr [ TypeExp a ]
|
||||||
|
deriving (Typeable)
|
||||||
|
|
||||||
|
-- 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
|
||||||
|
|
||||||
-- For debugging:
|
-- For debugging:
|
||||||
instance Show (TypeExp s a) where
|
instance Show (TypeExp a) where
|
||||||
show (MutVar {}) = "MutVar"
|
show (MutVar {}) = "MutVar"
|
||||||
show (GenVar {}) = "GenVar"
|
show (GenVar {}) = "GenVar"
|
||||||
show (NumLit {}) = "NumLit"
|
show (NumLit {}) = "NumLit"
|
||||||
show (OperType _ ts) = "OperType " ++ show ts
|
show (OperType _ ts) = "OperType " ++ show ts
|
||||||
|
|
||||||
prune :: TypeExp s a -> ST s (TypeExp s a)
|
prune :: TypeExp a -> IO (TypeExp a)
|
||||||
prune t =
|
prune t =
|
||||||
case t of
|
case t of
|
||||||
MutVar r ->
|
MutVar r ->
|
||||||
do m <- readSTRef r
|
do m <- readIORef r
|
||||||
case m of
|
case m of
|
||||||
Nothing -> return t
|
Nothing -> return t
|
||||||
Just t2 ->
|
Just t2 ->
|
||||||
do t' <- prune t2
|
do t' <- prune t2
|
||||||
writeSTRef r (Just t')
|
writeIORef r (Just t')
|
||||||
return t'
|
return t'
|
||||||
_ -> return t
|
_ -> return t
|
||||||
|
|
||||||
occursInType :: Ptr s a -> TypeExp s a -> ST s Bool
|
occursInType :: 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
|
||||||
|
@ -139,7 +149,7 @@ occursInType r t =
|
||||||
do bs <- mapM (occursInType r) ts
|
do bs <- mapM (occursInType r) ts
|
||||||
return (or bs)
|
return (or bs)
|
||||||
|
|
||||||
unifyType :: TypeExp s a -> TypeExp s a -> ST s (Either String ())
|
unifyType :: TypeExp a -> TypeExp a -> IO (Either String ())
|
||||||
unifyType te1 te2
|
unifyType te1 te2
|
||||||
= do t1' <- prune te1
|
= do t1' <- prune te1
|
||||||
t2' <- prune te2
|
t2' <- prune te2
|
||||||
|
@ -147,12 +157,12 @@ unifyType te1 te2
|
||||||
(MutVar r1, MutVar r2) ->
|
(MutVar r1, MutVar r2) ->
|
||||||
if r1 == r2
|
if r1 == r2
|
||||||
then return $ Right ()
|
then return $ Right ()
|
||||||
else liftM Right $ writeSTRef r1 (Just t2')
|
else liftM Right $ writeIORef r1 (Just t2')
|
||||||
(MutVar r1, _) ->
|
(MutVar r1, _) ->
|
||||||
do b <- occursInType r1 t2'
|
do b <- occursInType r1 t2'
|
||||||
if b
|
if b
|
||||||
then return $ Left "occurs in"
|
then return $ Left "occurs in"
|
||||||
else liftM Right $ writeSTRef r1 (Just t2')
|
else liftM Right $ writeIORef r1 (Just t2')
|
||||||
(_,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 "different genvars"
|
if n == m then return $ Right () else return $ Left "different genvars"
|
||||||
|
@ -161,26 +171,26 @@ unifyType te1 te2
|
||||||
then unifyArgs ts1 ts2
|
then unifyArgs ts1 ts2
|
||||||
else return $ Left "different constructors"
|
else return $ Left "different constructors"
|
||||||
(NumLit vns1, NumLit vns2) ->
|
(NumLit vns1, NumLit vns2) ->
|
||||||
do nst1 <- readSTRef vns1
|
do nst1 <- readIORef vns1
|
||||||
nst2 <- readSTRef vns2
|
nst2 <- readIORef vns2
|
||||||
case (nst1, nst2) of
|
case (nst1, nst2) of
|
||||||
(Right t1, Right t2) ->
|
(Right t1, Right t2) ->
|
||||||
if t1 /= t2
|
if t1 /= t2
|
||||||
then return $ Left "Numeric literals bound to different types"
|
then return $ Left "Numeric literals bound to different types"
|
||||||
else return $ Right ()
|
else return $ Right ()
|
||||||
(Left ns1, Left ns2) ->
|
(Left ns1, Left ns2) ->
|
||||||
do writeSTRef vns1 $ Left (ns1 ++ ns2)
|
do writeIORef vns1 $ Left (ns1 ++ ns2)
|
||||||
writeSTRef vns2 $ Left (ns1 ++ ns2)
|
writeIORef vns2 $ Left (ns1 ++ ns2)
|
||||||
return $ Right ()
|
return $ Right ()
|
||||||
(Right {}, Left {}) -> unifyType t2' t1'
|
(Right {}, Left {}) -> unifyType t2' t1'
|
||||||
(Left ns1, Right t2) ->
|
(Left ns1, Right t2) ->
|
||||||
if all (willFit t2) ns1
|
if all (willFit t2) ns1
|
||||||
then do writeSTRef vns1 (Right t2)
|
then do writeIORef vns1 (Right t2)
|
||||||
return $ Right ()
|
return $ Right ()
|
||||||
else return $ Left "Numeric literals will not fit in concrete type"
|
else return $ Left "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 ts2) ->
|
||||||
do nst1 <- readSTRef 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 == fromConstr n1
|
||||||
|
@ -190,7 +200,7 @@ unifyType te1 te2
|
||||||
Left ns ->
|
Left ns ->
|
||||||
if null ts2
|
if null ts2
|
||||||
then if all (willFit $ fromConstr n1) ns
|
then if all (willFit $ fromConstr n1) ns
|
||||||
then do writeSTRef vns1 $ Right (fromConstr n1)
|
then do writeIORef vns1 $ Right (fromConstr n1)
|
||||||
return $ Right ()
|
return $ Right ()
|
||||||
else return $ Left "Numeric literals will not fit in concrete type"
|
else return $ Left "Numeric literals will not fit in concrete type"
|
||||||
else return $ Left $ "Numeric literal cannot be unified"
|
else return $ Left $ "Numeric literal cannot be unified"
|
||||||
|
@ -202,7 +212,7 @@ unifyType te1 te2
|
||||||
unifyArgs [] [] = return $ Right ()
|
unifyArgs [] [] = return $ Right ()
|
||||||
unifyArgs _ _ = return $ Left "different lengths"
|
unifyArgs _ _ = return $ Left "different lengths"
|
||||||
|
|
||||||
instantiate :: [TypeExp s a] -> TypeExp s a -> TypeExp s a
|
instantiate :: [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 xs -> OperType nm (map (instantiate ts) xs)
|
||||||
|
|
Loading…
Reference in New Issue
Block a user