Move retypes check into the SpecType checker, and update the pass list.
This completes the occam typechecker.
This commit is contained in:
Adam Sampson
parent
ef329e3ed0
commit
b36068b815
|
|
@ -17,15 +17,13 @@ with this program. If not, see <http://www.gnu.org/licenses/>.
|
|||
-}
|
||||
|
||||
-- | The occam-specific frontend passes.
|
||||
module OccamPasses (occamPasses, foldConstants, checkConstants,
|
||||
checkRetypes) where
|
||||
module OccamPasses (occamPasses, foldConstants, checkConstants) where
|
||||
|
||||
import Control.Monad.State
|
||||
import Data.Generics
|
||||
|
||||
import qualified AST as A
|
||||
import CompState
|
||||
import Errors
|
||||
import EvalConstants
|
||||
import EvalLiterals
|
||||
import Metadata
|
||||
|
|
@ -49,16 +47,11 @@ occamPasses = makePassesDep' ((== FrontendOccam) . csFrontend)
|
|||
[Prop.constantsChecked])
|
||||
, ("Check types", checkTypes,
|
||||
[],
|
||||
[Prop.expressionTypesChecked, Prop.processTypesChecked])
|
||||
, ("Check retyping", checkRetypes,
|
||||
[],
|
||||
[Prop.retypesChecked])
|
||||
[Prop.expressionTypesChecked, Prop.processTypesChecked,
|
||||
Prop.functionTypesChecked, Prop.retypesChecked])
|
||||
, ("Dummy occam pass", dummyOccamPass,
|
||||
[],
|
||||
Prop.agg_namesDone ++ [Prop.expressionTypesChecked,
|
||||
Prop.inferredTypesRecorded, Prop.mainTagged,
|
||||
Prop.processTypesChecked,
|
||||
Prop.functionTypesChecked])
|
||||
Prop.agg_namesDone ++ [Prop.inferredTypesRecorded, Prop.mainTagged])
|
||||
]
|
||||
|
||||
-- | Fixed the types of array constructors according to the replicator count
|
||||
|
|
@ -93,7 +86,6 @@ foldConstants = applyDepthM2 doExpression doSpecification
|
|||
return s
|
||||
doSpecification s = return s
|
||||
|
||||
|
||||
-- | Check that things that must be constant are.
|
||||
checkConstants :: Data t => t -> PassM t
|
||||
checkConstants = applyDepthM2 doDimension doOption
|
||||
|
|
@ -115,49 +107,6 @@ checkConstants = applyDepthM2 doDimension doOption
|
|||
return o
|
||||
doOption o = return o
|
||||
|
||||
-- | Check that retyping is safe.
|
||||
checkRetypes :: Data t => t -> PassM t
|
||||
checkRetypes = applyDepthM doSpecType
|
||||
where
|
||||
doSpecType :: A.SpecType -> PassM A.SpecType
|
||||
doSpecType st@(A.Retypes m _ t v)
|
||||
= do fromT <- typeOfVariable v
|
||||
checkRetypes m fromT t
|
||||
return st
|
||||
doSpecType st@(A.RetypesExpr m _ t e)
|
||||
= do fromT <- typeOfExpression e
|
||||
checkRetypes m fromT t
|
||||
return st
|
||||
doSpecType st = return st
|
||||
|
||||
checkRetypes :: Meta -> A.Type -> A.Type -> PassM ()
|
||||
checkRetypes m fromT toT
|
||||
= do (fromBI, fromN) <- evalBytesInType fromT
|
||||
(toBI, toN) <- evalBytesInType toT
|
||||
case (fromBI, toBI, fromN, toN) of
|
||||
(_, BIManyFree, _, _) ->
|
||||
dieP m "Multiple free dimensions in retype destination type"
|
||||
(BIJust _, BIJust _, Just a, Just b) ->
|
||||
when (a /= b) $
|
||||
dieP m "Sizes do not match in retype"
|
||||
(BIJust _, BIOneFree _ _, Just a, Just b) ->
|
||||
when (not ((b <= a) && (a `mod` b == 0))) $
|
||||
dieP m "Sizes do not match in retype"
|
||||
(BIOneFree _ _, BIJust _, Just a, Just b) ->
|
||||
when (not ((a <= b) && (b `mod` a == 0))) $
|
||||
dieP m "Sizes do not match in retype"
|
||||
-- Otherwise we must do a runtime check.
|
||||
_ -> return ()
|
||||
|
||||
evalBytesInType :: A.Type -> PassM (BytesInResult, Maybe Int)
|
||||
evalBytesInType t
|
||||
= do bi <- bytesInType t
|
||||
n <- case bi of
|
||||
BIJust e -> maybeEvalIntExpression e
|
||||
BIOneFree e _ -> maybeEvalIntExpression e
|
||||
_ -> return Nothing
|
||||
return (bi, n)
|
||||
|
||||
-- | A dummy pass for things that haven't been separated out into passes yet.
|
||||
dummyOccamPass :: Data t => t -> PassM t
|
||||
dummyOccamPass = return
|
||||
|
|
|
|||
|
|
@ -154,64 +154,8 @@ testCheckConstants = TestList
|
|||
var = exprVariable "var"
|
||||
skip = A.Skip m
|
||||
|
||||
-- | Test 'OccamPasses.checkRetypes'.
|
||||
testCheckRetypes :: Test
|
||||
testCheckRetypes = TestList
|
||||
[
|
||||
-- Definitely OK at compile time
|
||||
testOK 0 $ retypesV A.Int intV
|
||||
, testOK 1 $ retypesE A.Int intE
|
||||
, testOK 2 $ retypesV A.Byte byteV
|
||||
, testOK 3 $ retypesE A.Byte byteE
|
||||
, testOK 4 $ retypesV known1 intV
|
||||
, testOK 5 $ retypesV known2 intV
|
||||
, testOK 6 $ retypesV both intV
|
||||
, testOK 7 $ retypesV unknown1 intV
|
||||
|
||||
-- Definitely wrong at compile time
|
||||
, testFail 100 $ retypesV A.Byte intV
|
||||
, testFail 101 $ retypesV A.Int byteV
|
||||
, testFail 102 $ retypesV unknown2 intV
|
||||
, testFail 103 $ retypesV unknown2 intsV
|
||||
, testFail 104 $ retypesV A.Byte intsV
|
||||
|
||||
-- Can't tell; need a runtime check
|
||||
, testOK 200 $ retypesV unknown1 intsV
|
||||
, testOK 201 $ retypesV A.Int intsV
|
||||
, testOK 202 $ retypesV known2 intsV
|
||||
, testOK 203 $ retypesV unknown1 bytesV
|
||||
]
|
||||
where
|
||||
testOK :: (Show a, Data a) => Int -> a -> Test
|
||||
testOK n orig
|
||||
= TestCase $ testPass ("testCheckRetypes" ++ show n)
|
||||
orig (OccamPasses.checkRetypes orig)
|
||||
startState
|
||||
|
||||
testFail :: (Show a, Data a) => Int -> a -> Test
|
||||
testFail n orig
|
||||
= TestCase $ testPassShouldFail ("testCheckRetypes" ++ show n)
|
||||
(OccamPasses.checkRetypes orig)
|
||||
startState
|
||||
|
||||
retypesV = A.Retypes m A.ValAbbrev
|
||||
retypesE = A.RetypesExpr m A.ValAbbrev
|
||||
|
||||
intV = variable "someInt"
|
||||
intE = intLiteral 42
|
||||
byteV = variable "someByte"
|
||||
byteE = byteLiteral 42
|
||||
intsV = variable "someInts"
|
||||
bytesV = variable "someBytes"
|
||||
known1 = A.Array [dimension 4] A.Byte
|
||||
known2 = A.Array [dimension 2, dimension 2] A.Byte
|
||||
both = A.Array [dimension 2, A.UnknownDimension] A.Byte
|
||||
unknown1 = A.Array [A.UnknownDimension] A.Int
|
||||
unknown2 = A.Array [A.UnknownDimension, A.UnknownDimension] A.Int
|
||||
|
||||
tests :: Test
|
||||
tests = TestLabel "OccamPassesTest" $ TestList
|
||||
[ testFoldConstants
|
||||
, testCheckConstants
|
||||
, testCheckRetypes
|
||||
]
|
||||
|
|
|
|||
|
|
@ -26,6 +26,7 @@ import Data.List
|
|||
import qualified AST as A
|
||||
import CompState
|
||||
import Errors
|
||||
import EvalConstants
|
||||
import EvalLiterals
|
||||
import Intrinsics
|
||||
import Metadata
|
||||
|
|
@ -505,6 +506,40 @@ checkStructured doInner (A.Only _ i)
|
|||
checkStructured doInner (A.Several _ ss)
|
||||
= mapM_ (checkStructured doInner) ss
|
||||
|
||||
--}}}
|
||||
--{{{ retyping checks
|
||||
|
||||
-- | Check that one type can be retyped to another.
|
||||
checkRetypes :: Meta -> A.Type -> A.Type -> PassM ()
|
||||
checkRetypes m fromT toT
|
||||
= do (fromBI, fromN) <- evalBytesInType fromT
|
||||
(toBI, toN) <- evalBytesInType toT
|
||||
case (fromBI, toBI, fromN, toN) of
|
||||
(_, BIManyFree, _, _) ->
|
||||
dieP m "Multiple free dimensions in retype destination type"
|
||||
(BIJust _, BIJust _, Just a, Just b) ->
|
||||
when (a /= b) $
|
||||
dieP m "Sizes do not match in retype"
|
||||
(BIJust _, BIOneFree _ _, Just a, Just b) ->
|
||||
when (not ((b <= a) && (a `mod` b == 0))) $
|
||||
dieP m "Sizes do not match in retype"
|
||||
(BIOneFree _ _, BIJust _, Just a, Just b) ->
|
||||
when (not ((a <= b) && (b `mod` a == 0))) $
|
||||
dieP m "Sizes do not match in retype"
|
||||
-- Otherwise we must do a runtime check.
|
||||
_ -> return ()
|
||||
|
||||
-- | Evaluate 'BytesIn' for a type.
|
||||
-- If the size isn't known at compile type, return 'Nothing'.
|
||||
evalBytesInType :: A.Type -> PassM (BytesInResult, Maybe Int)
|
||||
evalBytesInType t
|
||||
= do bi <- bytesInType t
|
||||
n <- case bi of
|
||||
BIJust e -> maybeEvalIntExpression e
|
||||
BIOneFree e _ -> maybeEvalIntExpression e
|
||||
_ -> return Nothing
|
||||
return (bi, n)
|
||||
|
||||
--}}}
|
||||
|
||||
-- | Check the AST for type consistency.
|
||||
|
|
@ -601,6 +636,7 @@ checkSpecTypes = checkDepthM doSpecType
|
|||
where
|
||||
doSpecType :: A.SpecType -> PassM ()
|
||||
doSpecType (A.Place _ e) = checkExpressionInt e
|
||||
doSpecType (A.Declaration _ _) = ok
|
||||
doSpecType (A.Is m am t v)
|
||||
= do tv <- typeOfVariable v
|
||||
checkType (findMeta v) t tv
|
||||
|
|
@ -662,13 +698,16 @@ checkSpecTypes = checkDepthM doSpecType
|
|||
doFunctionBody rs (Left s) = checkStructured (checkExpressionList rs) s
|
||||
-- FIXME: Need to know the name of the function to do this
|
||||
doFunctionBody rs (Right p) = dieP m "Cannot check function process body"
|
||||
-- FIXME: Retypes/RetypesExpr is checked elsewhere
|
||||
doSpecType _ = ok
|
||||
doSpecType (A.Retypes m _ t v)
|
||||
= do fromT <- typeOfVariable v
|
||||
checkRetypes m fromT t
|
||||
doSpecType (A.RetypesExpr m _ t e)
|
||||
= do fromT <- typeOfExpression e
|
||||
checkRetypes m fromT t
|
||||
|
||||
unexpectedAM :: Meta -> PassM ()
|
||||
unexpectedAM m = dieP m "Unexpected abbreviation mode"
|
||||
|
||||
|
||||
--}}}
|
||||
--{{{ checkProcesses
|
||||
|
||||
|
|
|
|||
|
|
@ -376,12 +376,15 @@ testOccamTypes = TestList
|
|||
--}}}
|
||||
--{{{ specifications
|
||||
|
||||
-- Place
|
||||
, testOK 2000 $ A.Place m intE
|
||||
, testFail 2001 $ A.Place m twoIntsE
|
||||
|
||||
-- Declaration
|
||||
, testOK 2010 $ A.Declaration m A.Int
|
||||
, testOK 2011 $ A.Declaration m twoIntsT
|
||||
|
||||
-- Is
|
||||
, testOK 2020 $ A.Is m A.Abbrev A.Int intV
|
||||
, testFail 2021 $ A.Is m A.ValAbbrev A.Int intV
|
||||
, testFail 2022 $ A.Is m A.Original A.Int intV
|
||||
|
|
@ -391,11 +394,13 @@ testOccamTypes = TestList
|
|||
, testOK 2026 $ A.Is m A.Abbrev (A.Timer A.OccamTimer) tim
|
||||
, testFail 2027 $ A.Is m A.ValAbbrev (A.Timer A.OccamTimer) tim
|
||||
|
||||
-- IsExpr
|
||||
, testOK 2030 $ A.IsExpr m A.ValAbbrev A.Int intE
|
||||
, testFail 2031 $ A.IsExpr m A.Abbrev A.Int intE
|
||||
, testFail 2032 $ A.IsExpr m A.Original A.Int intE
|
||||
, testFail 2033 $ A.IsExpr m A.ValAbbrev A.Real32 intE
|
||||
|
||||
-- IsChannelArray
|
||||
, testOK 2040 $ A.IsChannelArray m chansIntT [intC, intC]
|
||||
, testOK 2041 $ A.IsChannelArray m uchansIntT [intC, intC]
|
||||
, testOK 2042 $ A.IsChannelArray m uchansIntT []
|
||||
|
|
@ -404,12 +409,14 @@ testOccamTypes = TestList
|
|||
, testFail 2045 $ A.IsChannelArray m chansIntT [intC, intC, intC]
|
||||
, testFail 2046 $ A.IsChannelArray m chansIntT [intV, intV]
|
||||
|
||||
-- DataType
|
||||
, testOK 2050 $ A.DataType m A.Int
|
||||
, testOK 2051 $ A.DataType m twoIntsT
|
||||
, testOK 2052 $ A.DataType m myTwoIntsT
|
||||
, testFail 2053 $ A.DataType m chanIntT
|
||||
, testFail 2054 $ A.DataType m $ A.Timer A.OccamTimer
|
||||
|
||||
-- RecordType
|
||||
, testOK 2060 $ A.RecordType m True []
|
||||
, testOK 2061 $ A.RecordType m False []
|
||||
, testOK 2062 $ A.RecordType m False [ (simpleName "x", A.Int)
|
||||
|
|
@ -422,6 +429,7 @@ testOccamTypes = TestList
|
|||
, (simpleName "x", A.Real32)
|
||||
]
|
||||
|
||||
-- Protocol
|
||||
, testOK 2070 $ A.Protocol m [A.Int]
|
||||
, testOK 2071 $ A.Protocol m [A.Int, A.Real32, twoIntsT]
|
||||
, testOK 2072 $ A.Protocol m [A.Mobile A.Int]
|
||||
|
|
@ -440,6 +448,7 @@ testOccamTypes = TestList
|
|||
, (simpleName "one", [A.Real32])
|
||||
]
|
||||
|
||||
-- Proc
|
||||
, testOK 2090 $ A.Proc m A.PlainSpec [] skip
|
||||
, testOK 2091 $ A.Proc m A.InlineSpec [] skip
|
||||
, testOK 2092 $ A.Proc m A.PlainSpec
|
||||
|
|
@ -453,6 +462,7 @@ testOccamTypes = TestList
|
|||
]
|
||||
skip
|
||||
|
||||
-- Function
|
||||
, testOK 2100 $ A.Function m A.PlainSpec [A.Int] [] returnOne
|
||||
, testOK 2110 $ A.Function m A.InlineSpec [A.Int] [] returnOne
|
||||
, testFail 2120 $ A.Function m A.PlainSpec [] [] returnNone
|
||||
|
|
@ -471,6 +481,32 @@ testOccamTypes = TestList
|
|||
, testFail 2160 $ A.Function m A.PlainSpec [A.Int] [] returnNone
|
||||
, testFail 2170 $ A.Function m A.PlainSpec [A.Int] [] returnTwo
|
||||
|
||||
--}}}
|
||||
--{{{ retyping
|
||||
|
||||
-- Definitely OK at compile time
|
||||
, testOK 3000 $ retypesV A.Int intV
|
||||
, testOK 3001 $ retypesE A.Int intE
|
||||
, testOK 3002 $ retypesV A.Byte byteV
|
||||
, testOK 3003 $ retypesE A.Byte byteE
|
||||
, testOK 3004 $ retypesV known1 intV
|
||||
, testOK 3005 $ retypesV known2 intV
|
||||
, testOK 3006 $ retypesV both intV
|
||||
, testOK 3007 $ retypesV unknown1 intV
|
||||
|
||||
-- Definitely wrong at compile time
|
||||
, testFail 3100 $ retypesV A.Byte intV
|
||||
, testFail 3101 $ retypesV A.Int byteV
|
||||
, testFail 3102 $ retypesV unknown2 intV
|
||||
, testFail 3103 $ retypesV unknown2 intsV
|
||||
, testFail 3104 $ retypesV A.Byte intsV
|
||||
|
||||
-- Can't tell; need a runtime check
|
||||
, testOK 3200 $ retypesV unknown1 intsV
|
||||
, testOK 3201 $ retypesV A.Int intsV
|
||||
, testOK 3202 $ retypesV known2 intsV
|
||||
, testOK 3203 $ retypesV unknown1 bytesV
|
||||
|
||||
--}}}
|
||||
]
|
||||
where
|
||||
|
|
@ -569,6 +605,14 @@ testOccamTypes = TestList
|
|||
returnOne = Left $ A.Only m $ A.ExpressionList m [intE]
|
||||
returnTwo = Left $ A.Only m $ A.ExpressionList m [intE, intE]
|
||||
|
||||
retypesV = A.Retypes m A.ValAbbrev
|
||||
retypesE = A.RetypesExpr m A.ValAbbrev
|
||||
known1 = A.Array [dimension 4] A.Byte
|
||||
known2 = A.Array [dimension 2, dimension 2] A.Byte
|
||||
both = A.Array [dimension 2, A.UnknownDimension] A.Byte
|
||||
unknown1 = A.Array [A.UnknownDimension] A.Int
|
||||
unknown2 = A.Array [A.UnknownDimension, A.UnknownDimension] A.Int
|
||||
|
||||
--}}}
|
||||
|
||||
tests :: Test
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user