Changed the conditionals type-checking to use type unification rather than the old system
This commit is contained in:
parent
f8b7e8f8cb
commit
63a28d0044
|
@ -45,6 +45,9 @@ rainPasses = makePassesDep' ((== FrontendRain) . csFrontend)
|
||||||
uniquifyAndResolveVars, [Prop.noInt], namesDone)
|
uniquifyAndResolveVars, [Prop.noInt], namesDone)
|
||||||
|
|
||||||
,("Fold all constant expressions", constantFoldPass, [Prop.noInt] ++ namesDone, [Prop.constantsFolded, Prop.constantsChecked])
|
,("Fold all constant expressions", constantFoldPass, [Prop.noInt] ++ namesDone, [Prop.constantsFolded, Prop.constantsChecked])
|
||||||
|
,("Type Checking", performTypeUnification, [Prop.noInt] ++ namesDone,
|
||||||
|
typesDone)
|
||||||
|
|
||||||
,("Annotate integer literal types", annotateIntLiteralTypes, [Prop.noInt] ++ namesDone, [Prop.intLiteralsInBounds])
|
,("Annotate integer literal types", annotateIntLiteralTypes, [Prop.noInt] ++ namesDone, [Prop.intLiteralsInBounds])
|
||||||
,("Annotate list literal and range types", annotateListLiteralTypes,
|
,("Annotate list literal and range types", annotateListLiteralTypes,
|
||||||
namesDone ++ [Prop.noInt, Prop.intLiteralsInBounds], [Prop.listsGivenType])
|
namesDone ++ [Prop.noInt, Prop.intLiteralsInBounds], [Prop.listsGivenType])
|
||||||
|
@ -54,7 +57,7 @@ rainPasses = makePassesDep' ((== FrontendRain) . csFrontend)
|
||||||
|
|
||||||
,("Check types in expressions",checkExpressionTypes, namesDone ++ [Prop.noInt, Prop.constantsFolded, Prop.intLiteralsInBounds, Prop.inferredTypesRecorded], [Prop.expressionTypesChecked])
|
,("Check types in expressions",checkExpressionTypes, namesDone ++ [Prop.noInt, Prop.constantsFolded, Prop.intLiteralsInBounds, Prop.inferredTypesRecorded], [Prop.expressionTypesChecked])
|
||||||
,("Check types in assignments", checkAssignmentTypes, typesDone ++ [Prop.expressionTypesChecked], [Prop.processTypesChecked])
|
,("Check types in assignments", checkAssignmentTypes, typesDone ++ [Prop.expressionTypesChecked], [Prop.processTypesChecked])
|
||||||
,("Check types in if/while conditions",checkConditionalTypes, typesDone ++ [Prop.expressionTypesChecked], [Prop.processTypesChecked])
|
-- ,("Check types in if/while conditions",checkConditionalTypes, typesDone ++ [Prop.expressionTypesChecked], [Prop.processTypesChecked])
|
||||||
,("Check types in input/output",checkCommTypes, typesDone ++ [Prop.expressionTypesChecked], [Prop.processTypesChecked])
|
,("Check types in input/output",checkCommTypes, typesDone ++ [Prop.expressionTypesChecked], [Prop.processTypesChecked])
|
||||||
,("Check parameters in process calls", matchParamPass, typesDone, [Prop.processTypesChecked,
|
,("Check parameters in process calls", matchParamPass, typesDone, [Prop.processTypesChecked,
|
||||||
Prop.functionTypesChecked])
|
Prop.functionTypesChecked])
|
||||||
|
|
|
@ -20,6 +20,9 @@ module RainTypes where
|
||||||
|
|
||||||
import Control.Monad.State
|
import Control.Monad.State
|
||||||
import Data.Generics
|
import Data.Generics
|
||||||
|
import qualified Data.Map as Map
|
||||||
|
import Data.Maybe
|
||||||
|
import Data.IORef
|
||||||
|
|
||||||
import qualified AST as A
|
import qualified AST as A
|
||||||
import CompState
|
import CompState
|
||||||
|
@ -30,7 +33,66 @@ import Pass
|
||||||
import ShowCode
|
import ShowCode
|
||||||
import Traversal
|
import Traversal
|
||||||
import Types
|
import Types
|
||||||
|
import TypeUnification
|
||||||
|
import Utils
|
||||||
|
|
||||||
|
lookupMapElseMutVar :: UnifyIndex -> PassM (TypeExp A.Type)
|
||||||
|
lookupMapElseMutVar k
|
||||||
|
= do st <- get
|
||||||
|
let m = csUnifyLookup st
|
||||||
|
case Map.lookup k m of
|
||||||
|
Just v -> return v
|
||||||
|
Nothing -> do r <- liftIO $ newIORef Nothing
|
||||||
|
let v = MutVar r
|
||||||
|
m' = Map.insert k v m
|
||||||
|
put st {csUnifyLookup = m'}
|
||||||
|
return v
|
||||||
|
|
||||||
|
ttte :: Data b => b -> A.Type -> PassM (TypeExp A.Type)
|
||||||
|
ttte c t = typeToTypeExp t >>= \t' -> return $ OperType (toConstr c) [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 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.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
|
||||||
|
st <- get
|
||||||
|
let mp = csUnifyLookup st
|
||||||
|
put st {csUnifyLookup = Map.insert (UnifyIndex (m,Left id)) v mp}
|
||||||
|
return v
|
||||||
|
typeToTypeExp t = return $ OperType (toConstr t) []
|
||||||
|
|
||||||
|
markUnify :: (Typed a, Typed b) => a -> b -> PassM ()
|
||||||
|
markUnify x y
|
||||||
|
= do tx <- astTypeOf x
|
||||||
|
ty <- astTypeOf y
|
||||||
|
tex <- typeToTypeExp tx
|
||||||
|
tey <- typeToTypeExp ty
|
||||||
|
modify $ \st -> st {csUnifyPairs = (tex,tey) : csUnifyPairs st}
|
||||||
|
|
||||||
|
|
||||||
|
performTypeUnification :: Data t => t -> PassM t
|
||||||
|
performTypeUnification x
|
||||||
|
-- First, we markup all the types in the tree:
|
||||||
|
= do x' <- markConditionalTypes x --TODO markup everything else
|
||||||
|
-- Then, we do the unification:
|
||||||
|
prs <- get >>* csUnifyPairs
|
||||||
|
res <- liftIO $ mapM (uncurry unifyType) prs
|
||||||
|
mapM (dieP emptyMeta) (fst $ splitEither res)
|
||||||
|
return x'
|
||||||
|
|
||||||
-- | A pass that records inferred types. Currently the only place where types are inferred is in seqeach\/pareach loops.
|
-- | A pass that records inferred types. Currently the only place where types are inferred is in seqeach\/pareach loops.
|
||||||
recordInfNameTypes :: Data t => t -> PassM t
|
recordInfNameTypes :: Data t => t -> PassM t
|
||||||
|
@ -319,23 +381,17 @@ checkAssignmentTypes = applyDepthM checkAssignment
|
||||||
checkAssignment st = return st
|
checkAssignment st = return st
|
||||||
|
|
||||||
-- | Checks the types in if and while conditionals
|
-- | Checks the types in if and while conditionals
|
||||||
checkConditionalTypes :: Data t => t -> PassM t
|
markConditionalTypes :: Data t => t -> PassM t
|
||||||
checkConditionalTypes = applyDepthM2 checkWhile checkIf
|
markConditionalTypes = checkDepthM2 checkWhile checkIf
|
||||||
where
|
where
|
||||||
checkWhile :: A.Process -> PassM A.Process
|
checkWhile :: Check A.Process
|
||||||
checkWhile w@(A.While m exp _)
|
checkWhile w@(A.While m exp _)
|
||||||
= do t <- astTypeOf exp
|
= markUnify exp A.Bool
|
||||||
if (t == A.Bool)
|
checkWhile _ = return ()
|
||||||
then return w
|
|
||||||
else dieP m "Expression in while conditional must be of boolean type"
|
|
||||||
checkWhile p = return p
|
|
||||||
|
|
||||||
checkIf :: A.Choice -> PassM A.Choice
|
checkIf :: Check A.Choice
|
||||||
checkIf c@(A.Choice m exp _)
|
checkIf c@(A.Choice m exp _)
|
||||||
= do t <- astTypeOf exp
|
= markUnify exp A.Bool
|
||||||
if (t == A.Bool)
|
|
||||||
then return c
|
|
||||||
else dieP m "Expression in if conditional must be of boolean type"
|
|
||||||
|
|
||||||
-- | Checks the types in inputs and outputs, including inputs in alts
|
-- | Checks the types in inputs and outputs, including inputs in alts
|
||||||
checkCommTypes :: Data t => t -> PassM t
|
checkCommTypes :: Data t => t -> PassM t
|
||||||
|
|
|
@ -359,11 +359,11 @@ checkExpressionTest = TestList
|
||||||
[
|
[
|
||||||
TestCase $ testPass ("checkExpressionTest/if " ++ show n)
|
TestCase $ testPass ("checkExpressionTest/if " ++ show n)
|
||||||
(mIf $ mOnlyC $ tag3 A.Choice DontCare (buildExprPattern exp) (tag1 A.Skip DontCare))
|
(mIf $ mOnlyC $ tag3 A.Choice DontCare (buildExprPattern exp) (tag1 A.Skip DontCare))
|
||||||
(checkConditionalTypes $ A.If m $ A.Only m $ A.Choice m (buildExpr src) (A.Skip m))
|
(performTypeUnification $ A.If m $ A.Only m $ A.Choice m (buildExpr src) (A.Skip m))
|
||||||
state
|
state
|
||||||
,TestCase $ testPass ("checkExpressionTest/while " ++ show n)
|
,TestCase $ testPass ("checkExpressionTest/while " ++ show n)
|
||||||
(mWhile (buildExprPattern exp) (tag1 A.Skip DontCare))
|
(mWhile (buildExprPattern exp) (tag1 A.Skip DontCare))
|
||||||
(checkConditionalTypes $ A.While m (buildExpr src) (A.Skip m))
|
(performTypeUnification $ A.While m (buildExpr src) (A.Skip m))
|
||||||
state
|
state
|
||||||
]
|
]
|
||||||
|
|
||||||
|
@ -371,10 +371,10 @@ checkExpressionTest = TestList
|
||||||
failWhileIf n src = TestList
|
failWhileIf n src = TestList
|
||||||
[
|
[
|
||||||
TestCase $ testPassShouldFail ("checkExpressionTest/if " ++ show n)
|
TestCase $ testPassShouldFail ("checkExpressionTest/if " ++ show n)
|
||||||
(checkConditionalTypes $ A.If m $ A.Only m $ A.Choice m (buildExpr src) (A.Skip m))
|
(performTypeUnification $ A.If m $ A.Only m $ A.Choice m (buildExpr src) (A.Skip m))
|
||||||
state
|
state
|
||||||
,TestCase $ testPassShouldFail ("checkExpressionTest/while " ++ show n)
|
,TestCase $ testPassShouldFail ("checkExpressionTest/while " ++ show n)
|
||||||
(checkConditionalTypes $ A.While m (buildExpr src) (A.Skip m))
|
(performTypeUnification $ A.While m (buildExpr src) (A.Skip m))
|
||||||
state
|
state
|
||||||
]
|
]
|
||||||
|
|
||||||
|
@ -482,7 +482,7 @@ checkExpressionTest = TestList
|
||||||
markRainTest
|
markRainTest
|
||||||
|
|
||||||
testUnify :: Test
|
testUnify :: Test
|
||||||
testUnify = TestList
|
testUnify = TestList [] {-
|
||||||
[pass [] [] []
|
[pass [] [] []
|
||||||
,pass' [("a",A.Int)] []
|
,pass' [("a",A.Int)] []
|
||||||
,pass' [("a",A.Int)] [("a","a")]
|
,pass' [("a",A.Int)] [("a","a")]
|
||||||
|
@ -499,7 +499,8 @@ testUnify = TestList
|
||||||
pass :: [(String, A.Type)] -> [(String, String)] -> [(String, A.Type)]
|
pass :: [(String, A.Type)] -> [(String, String)] -> [(String, A.Type)]
|
||||||
-> Test
|
-> Test
|
||||||
pass im u om = TestCase $ assertEqual "testUnify" (Right $ Map.fromList om)
|
pass im u om = TestCase $ assertEqual "testUnify" (Right $ Map.fromList om)
|
||||||
$ unifyRainTypes (Map.fromList im) u
|
=<< unifyRainTypes (Map.fromList $ map transformPair
|
||||||
|
id im) u
|
||||||
|
|
||||||
fail :: [(String, A.Type)] -> [(String, String)] -> Test
|
fail :: [(String, A.Type)] -> [(String, String)] -> Test
|
||||||
fail im u = TestCase $ case unifyRainTypes (Map.fromList im) u of
|
fail im u = TestCase $ case unifyRainTypes (Map.fromList im) u of
|
||||||
|
@ -513,7 +514,7 @@ testUnify = TestList
|
||||||
pass2 xs ys = pass (zip names xs) (allPairs names) (zip names ys)
|
pass2 xs ys = pass (zip names xs) (allPairs names) (zip names ys)
|
||||||
where
|
where
|
||||||
names = take (min (length xs) (length ys)) $ map (:[]) ['a'..]
|
names = take (min (length xs) (length ys)) $ map (:[]) ['a'..]
|
||||||
|
-}
|
||||||
tests :: Test
|
tests :: Test
|
||||||
tests = TestLabel "RainTypesTest" $ TestList
|
tests = TestLabel "RainTypesTest" $ TestList
|
||||||
[
|
[
|
||||||
|
|
Loading…
Reference in New Issue
Block a user