Added support to a couple of functions for the IsClaimed SpecType

This commit is contained in:
Neil Brown 2009-03-23 18:56:48 +00:00
parent 41805aaacf
commit 04108613d9
2 changed files with 20 additions and 0 deletions

View File

@ -99,6 +99,20 @@ typeOfSpec' st
A.IsExpr a b t c -> return $ Just (t, \t' -> A.IsExpr a b t' c)
A.IsChannelArray a t b
-> return $ Just (t, \t' -> A.IsChannelArray a t' b)
A.IsClaimed m v
-> do t <- typeOfVariable v
let t' = case t of
A.Chan attr innerT -> Just $ A.Chan (attr
{ A.caWritingShared = A.Unshared
, A.caReadingShared = A.Unshared
}) innerT
A.ChanEnd A.DirInput _ innerT
-> Just $ A.ChanEnd A.DirInput A.Unshared innerT
A.ChanEnd A.DirOutput _ innerT
-> Just $ A.ChanEnd A.DirOutput A.Unshared innerT
A.ChanDataType dir _ innerT -> Just $ A.ChanDataType dir A.Unshared innerT
_ -> Nothing
return $ fmap (\x -> (x, error "typeOfSpec'")) t'
A.Retypes a b t c -> return $ Just (t, \t' -> A.Retypes a b t' c)
A.RetypesExpr a b t c
-> return $ Just (t, \t' -> A.RetypesExpr a b t' c)

View File

@ -1331,6 +1331,12 @@ checkSpecTypes = checkDepthM doSpecType
checkType (findMeta e) t te
checkValAM m am
checkAbbrev m A.ValAbbrev am
doSpecType (A.IsClaimed m v)
= do t <- astTypeOf v
case t of
A.ChanEnd _ A.Shared _ -> return ()
A.ChanDataType _ A.Shared _ -> return ()
_ -> dieP m "Expected shared channel end in claim"
doSpecType (A.IsChannelArray m rawT cs)
= do t <- resolveUserType m rawT
let isChan (A.Chan {}) = True