Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

Add support for subtypes.

  • Loading branch information...
commit 5b9ea8cd66851f8062bf955ba497ae302deff8ff 1 parent 93f5e42
@tomgr authored
View
2  src/CSPM/DataStructures/Syntax.hs
@@ -450,6 +450,8 @@ data Decl id =
| Channel [id] (Maybe (AnExp id))
-- | A datatype declaration, e.g. @datatype T = Clause1 | Clause2@.
| DataType id [AnDataTypeClause id]
+ -- | A subtype declaration, e.g. @subtype T = Clause1 | Clause2@.
+ | SubType id [AnDataTypeClause id]
-- | A nametype declaration, e.g. @nametype T2 = T.T@.
| NameType id (AnExp id)
deriving (Eq, Show)
View
1  src/CSPM/Desugar.hs
@@ -39,6 +39,7 @@ instance Desugarable (Decl Name) where
desugar (Transparent ns) = Transparent ns
desugar (Channel ns me) = Channel ns (desugar me)
desugar (DataType n cs) = DataType n (desugar cs)
+ desugar (SubType n cs) = SubType n (desugar cs)
desugar (NameType n e) = NameType n (desugar e)
instance Desugarable (Assertion Name) where
View
17 src/CSPM/Evaluator/DeclBind.hs
@@ -141,12 +141,27 @@ bindDecl (an@(An _ _ (DataType n cs))) =
vs <- mapM mkSet [nc | DataTypeClause nc _ <- map unAnnotate cs]
return $ VSet (unions vs)
in return $ (n, computeSetOfValues):(map mkDataTypeClause (map unAnnotate cs))
+bindDecl (an@(An _ _ (SubType n cs))) =
+ let
+ computeSetOfValues =
+ let
+ mkSet (DataTypeClause nc me) = do
+ VTuple [_, _, VList fields] <- lookupVar nc
+ fs <- case me of
+ Just e -> eval e >>= evalTypeExprToList
+ Nothing -> return []
+ let preFieldCount = length fs
+ return $ cartesianProduct CartDot $ fromList
+ [VDataType nc] : fs ++ map (\(VSet vs) -> vs) (drop preFieldCount fields)
+ in do
+ vs <- mapM (mkSet . unAnnotate) cs
+ return $ VSet (unions vs)
+ in return $ [(n, computeSetOfValues)]
bindDecl (an@(An _ _ (NameType n e))) = return $
[(n, do
v <- eval e
sets <- evalTypeExprToList v
return $ VSet $ cartesianProduct CartDot sets)]
-
bindDecl (an@(An _ _ (Assert _))) = return []
bindDecl (an@(An _ _ (External ns))) = return []
bindDecl (an@(An _ _ (Transparent ns))) = return []
View
1  src/CSPM/Parser/Lexer.x
@@ -147,6 +147,7 @@ tokens :-
<0>"channel"/$notid { soakTok TChannel }
<0>"assert"/$notid { soakTok' TAssert }
<0>"datatype"/$notid { soakTok TDataType }
+ <0>"subtype"/$notid { soakTok TSubType }
<0>"external"/$notid { soakTok TExternal }
<0>"transparent"/$notid { soakTok TTransparent }
<0>"nametype"/$notid { soakTok TNameType }
View
621 src/CSPM/Parser/Parser.hs
318 additions, 303 deletions not shown
View
4 src/CSPM/Parser/Parser.ppy
@@ -16,11 +16,11 @@ import Data.Char
import CSPM.DataStructures.Literals
import CSPM.DataStructures.Names
import CSPM.DataStructures.Syntax
-import CSPM.DataStructures.Tokens
import CSPM.DataStructures.Types hiding (TDot)
import CSPM.Parser.Exceptions
import CSPM.Parser.Lexer
import CSPM.Parser.Monad
+import CSPM.Parser.Tokens
import Util.Annotated
}
@@ -73,6 +73,7 @@ import Util.Annotated
"@" { L _ TLambdaDot }
"channel" { L _ TChannel }
"datatype" { L _ TDataType }
+ "subtype" { L _ TSubType }
"external" { L _ TExternal }
"transparent" { L _ TTransparent }
"nametype" { L _ TNameType }
@@ -207,6 +208,7 @@ DeclA :: { PDecl }
| "channel" NameCommaList1 { AN2L (Channel (map unLoc $2) Nothing) }
| "channel" NameCommaList1 ":" CExp { AN2 (Channel (map unLoc $2) (Just $4)) }
| "datatype" Name "=" DataTypeClauseList1 { AN2L (DataType (unLoc $2) $4) }
+ | "subtype" Name "=" DataTypeClauseList1 { AN2L (SubType (unLoc $2) $4) }
| "external" NameCommaList1 { AN2L (External (map unLoc $2)) }
| "transparent" NameCommaList1 { AN2L (Transparent (map unLoc $2)) }
| "assert" "anot" Assertion { AN (Assert (ASNot $3)) }
View
2  src/CSPM/Parser/Tokens.hs
@@ -50,6 +50,7 @@ data Token =
| TAssert
| TAssertNot
| TDataType
+ | TSubType
| TExternal
| TTransparent
| TNameType
@@ -149,6 +150,7 @@ instance PrettyPrintable Token where
prettyPrint TAssert = text "assert"
prettyPrint TAssertNot = text "not"
prettyPrint TDataType = text "datatype"
+ prettyPrint TSubType = text "subtype"
prettyPrint TExternal = text "external"
prettyPrint TTransparent = text "transparent"
prettyPrint TNameType = text "nametype"
View
3  src/CSPM/PrettyPrinter.hs
@@ -45,6 +45,9 @@ instance PrettyPrintable id => PrettyPrintable (Decl id) where
prettyPrint (DataType n dtcs) =
text "datatype" <+> prettyPrint n <+> text "="
<+> fsep (punctuate (text "|") (map prettyPrint dtcs))
+ prettyPrint (SubType n dtcs) =
+ text "subtype" <+> prettyPrint n <+> text "="
+ <+> fsep (punctuate (text "|") (map prettyPrint dtcs))
prettyPrint (NameType n e) =
text "nametype" <+> prettyPrint n <+> text "=" <+> prettyPrint e
prettyPrint (Assert a) =
View
12 src/CSPM/Renamer.hs
@@ -185,6 +185,9 @@ renameDeclarations topLevel ds prog = do
DataType rn _ -> do
n <- nameMaker (loc pd) rn
setName rn n
+ SubType rn _ -> do
+ n <- nameMaker (loc pd) rn
+ setName rn n
External ns ->
mapM_ (\ rn@(UnQual ocn) -> do
case externalFunctionForOccName ocn of
@@ -224,6 +227,14 @@ renameDeclarations topLevel ds prog = do
e' <- rename e
return $ DataTypeClause n' e') cs
return $ DataType n cs'
+ SubType rn cs -> do
+ n <- renameVarRHS rn
+ cs' <- mapM (\ pc -> addScope $ reAnnotate pc $ case unAnnotate pc of
+ DataTypeClause rn e -> do
+ n' <- renameVarRHS rn
+ e' <- rename e
+ return $ DataTypeClause n' e') cs
+ return $ SubType n cs'
External rns -> do
ns <- mapM renameVarRHS rns
return $ External ns
@@ -544,6 +555,7 @@ instance FreeVars (Decl UnRenamedName) where
freeVars (Channel ns _) = return ns
freeVars (DataType n cs) =
return $ n:[n' | DataTypeClause n' _ <- map unAnnotate cs]
+ freeVars (SubType n _) = return [n]
freeVars (FunBind n _) = return [n]
freeVars (NameType n _) = return [n]
freeVars (PatBind p _) = freeVars p
View
1  src/CSPM/TypeChecker/Compressor.hs
@@ -121,6 +121,7 @@ instance Compressable (Decl a) where
mcompress (Transparent ns) = return (Transparent ns)
mcompress (Channel ns me) = return (Channel ns) $$ mcompress me
mcompress (DataType n cs) = return (DataType n) $$ mcompress cs
+ mcompress (SubType n cs) = return (SubType n) $$ mcompress cs
mcompress (NameType n e) = return (NameType n) $$ mcompress e
instance Compressable (Assertion a) where
View
19 src/CSPM/TypeChecker/Decl.hs
@@ -180,6 +180,8 @@ instance TypeCheckable (Decl Name) [(Name, Type)] where
hang (text "In a pattern binding:") tabWidth (prettyPrint p)
errorContext (DataType n cs) = Just $
text "In the declaration of:" <+> prettyPrint n
+ errorContext (SubType n cs) = Just $
+ text "In the declaration of:" <+> prettyPrint n
errorContext (NameType n e) = Just $
text "In the declaration of:" <+> prettyPrint n
errorContext (Channel ns es) = Just $
@@ -235,6 +237,23 @@ instance TypeCheckable (Decl Name) [(Name, Type)] where
ForAll [] t' <- getType n
unify t' t) ns
return $ [(n, t) | n <- ns]
+ typeCheck' (SubType n clauses) = do
+ -- Get the type fromthe first clause
+ parentType <- freshTypeVar
+ mapM_ (\ clause -> do
+ let nclause = case unAnnotate clause of
+ DataTypeClause x _ -> x
+ (_, tsFields) <- typeCheck clause
+ ForAll [] typeCon <- getType nclause
+ (actFields, dataType) <- dotableToDotList typeCon
+ -- Check that the datatype is the correct subtype.
+ unify parentType dataType
+ -- Check that the fields are compatible with the expected fields.
+ zipWithM unify actFields tsFields
+ ) clauses
+ ForAll [] t <- getType n
+ t' <- unify t (TSet parentType)
+ return [(n, TSet parentType)]
typeCheck' (DataType n clauses) = do
nts <- mapM (\ clause -> do
let
View
6 src/CSPM/TypeChecker/Dependencies.hs
@@ -24,6 +24,7 @@ namesBoundByDecl = namesBoundByDecl' . unAnnotate
namesBoundByDecl' (FunBind n ms) = return [n]
namesBoundByDecl' (PatBind p ms) = freeVars p
namesBoundByDecl' (Channel ns es) = return ns
+namesBoundByDecl' (SubType n dcs) = return [n]
namesBoundByDecl' (DataType n dcs) =
let
namesBoundByDtClause (DataTypeClause n _) = [n]
@@ -199,6 +200,11 @@ instance Dependencies (Decl Name) where
return $ depsp++depse
dependencies' (Channel ns es) = dependencies es
dependencies' (DataType n cs) = dependencies [cs]
+ dependencies' (SubType n cs) =
+ concatMapM (\ (DataTypeClause n e) -> do
+ ds <- dependencies e
+ return $ n:ds
+ ) (map unAnnotate cs)
dependencies' (NameType n e) = dependencies' e
dependencies' (External ns) = return []
dependencies' (Transparent ns) = return []
View
2  src/CSPM/TypeChecker/Monad.hs
@@ -275,7 +275,7 @@ getSymbolInformation n = do
-- If we don't do this the error is deferred until later
case Env.maybeLookup env n of
Just symb -> return symb
- Nothing -> panic "Name not found after renaming."
+ Nothing -> panic $ "Name "++show n++" not found after renaming."
-- | Get the type of 'n' and throw an exception if it doesn't exist.
getType :: Name -> TypeCheckMonad TypeScheme
View
5 src/CSPM/TypeChecker/Unification.hs
@@ -1,6 +1,6 @@
module CSPM.TypeChecker.Unification (
generaliseGroup, instantiate, unify, unifyAll, evaluateDots,
- typeToDotList,
+ typeToDotList, dotableToDotList,
) where
import Control.Monad
@@ -152,6 +152,9 @@ typeToDotList t = compress t >>= \ t ->
return (t:ts1++ts2)
_ -> return [t]
+dotableToDotList :: Type -> TypeCheckMonad ([Type], Type)
+dotableToDotList t = compress t >>= return . reduceDotable
+
-- | Takes a 'TDotable' and returns a tuple consisting of:
-- the arguments that it takes and the ultimate return type. Note
-- that due to the way that TDotables are introduced the return type
View
10 tests/evaluator/should_pass/subtypes.csp
@@ -0,0 +1,10 @@
+datatype X = A | B.{0}
+datatype Y = C.{0..100} | D.Bool
+
+subtype X' = A
+subtype Y' = C | D.{false}
+subtype Z = C | D
+
+test1 = X' == {A}
+test2 = Y' == union({C.x | x <- {0..100}}, {D.false})
+test3 = Z == Y
View
4 tests/typechecker/should_fail/subtypes_1.csp
@@ -0,0 +1,4 @@
+datatype X = A | B.{0}
+datatype Y = C.Int | D.Bool
+
+subtype X' = A | C.{0}
View
3  tests/typechecker/should_fail/subtypes_2.csp
@@ -0,0 +1,3 @@
+datatype X = A | B.{0}
+
+subtype X' = B.0
View
5 tests/typechecker/should_pass/subtypes.csp
@@ -0,0 +1,5 @@
+datatype X = A | B.{0}
+datatype Y = C.Int | D.Bool
+
+subtype X' = A
+subtype Y' = C | D.{false}
Please sign in to comment.
Something went wrong with that request. Please try again.