diff --git a/05.simpleExtensions/code/STLCExtensions.hs b/05.simpleExtensions/code/STLCExtensions.hs index d62d114..511c36c 100644 --- a/05.simpleExtensions/code/STLCExtensions.hs +++ b/05.simpleExtensions/code/STLCExtensions.hs @@ -19,6 +19,7 @@ Contributors: module STLCExtensions where import Prelude hiding (lookup) +import qualified Data.Map as Map type Id = String @@ -30,7 +31,15 @@ type RItem = (Label, Term) type TItem = (Term) -data Type = TBool +type SubRel = [(Type, Type)] + +-- | List of tuples representing subtype relations. +-- Subtype should be the first element, supertype should be the second. +sub_sup = [(TBool,TInt),(TInt,TNumber)] + +data Type = TTop + | TBool + | TNumber -- For subtyping transitivity purposes | TInt | TString | TUnit @@ -210,6 +219,34 @@ sure :: Maybe Type -> Type sure (Just x) = x sure Nothing = error "'Nothing' detected" +-- | Subtyping checker. Returns a Bool indicating if the first argument +-- is a subtype of the second. +(<:) :: Type -> Type -> Bool +_ <: TTop = True +(TArrow s1 s2) <: (TArrow t1 t2) = t1 <: s1 && s2 <: t2 +(TRecord s) <: (TRecord t) = isRecSubType s t +s <: t = if s == t then True else lookup_subtype s t sub_sup + +-- | Turn Records into maps and checks for: +-- Width, Permutation and Depth +-- Map.lookup takes care of Width and Permutation. +-- Depth is taken care by the subtyping 'typ2 <: typ'. +isRecSubType :: [(Label,Type)] -> [(Label,Type)] -> Bool +isRecSubType sub super = all sRcd super + where sRcd (label, typ) = case Map.lookup label (Map.fromList sub) of + Just typ2 -> typ2 <: typ + Nothing -> False + +-- | Lookup function for transitivity +lookup_subtype :: Type -> Type -> SubRel -> Bool +lookup_subtype sub sup [] = False +lookup_subtype sub sup ((v, t):tail) + | sub == v && sup == t = True + | sub == v && sup /= t = lookup_subtype t sup tail + | sub /= v && sup /= t = lookup_subtype sub sup tail + | sub /= v && sup == t = lookup_subtype sub sup tail + | otherwise = False + -- | A lookup function. It searches for a specific -- mapping involving an identifier and a type. lookup :: Id -> Gamma -> Maybe Type diff --git a/05.simpleExtensions/code/SubTypeTests.hs b/05.simpleExtensions/code/SubTypeTests.hs new file mode 100644 index 0000000..4b2533b --- /dev/null +++ b/05.simpleExtensions/code/SubTypeTests.hs @@ -0,0 +1,99 @@ +module SubTypeTests where + +import STLCExtensions +import Test.HUnit + +-- run the test suite: runTestTT testSuite +runTests = runTestTT testSuite + +testSuite = TestList [ + TestLabel "Record: r2 <: r" recc, + TestLabel "Record: r1 <: r3" rec1, + TestLabel "Record: r1 <: r2" rec2, + TestLabel "Record: RcdWidth - r2 <: r1" rec3, + TestLabel "Record: r1 <: r2" rec4, + TestLabel "Record: RcdPerm - r2 <: r2perm" rec5, + TestLabel "Record: RcdPerm - r2perm <: r2" rec6, + TestLabel "Record: RcdDepth - r4 <: r5" rec7, + TestLabel "Record: RcdDepth - r5 <: r4" rec8, + TestLabel "Record: Transitivity - recA <: recB, recB <: recC, recA <: recC" recTrans, + TestLabel "Record: Reflexivity" recRefl, + TestLabel "TBool <: TBool" reflTBool, + TestLabel "TInt <: TInt" reflTInt, + TestLabel "TString <: TString" reflTString, + TestLabel "arr <: arr" reflArr, + TestLabel "Arrow: arr1 <: arr" arrow1, + TestLabel "Arrow: arr2 <: arr" arrow2, + TestLabel "Arrow: arr3 <: arr " arrow3, + TestLabel "Transitivity with Primitive Types" trans + ] + +r = TRecord [("y", TString)] +r1 = TRecord [("x", TInt)] +r2 = TRecord [("x", TInt), ("y", TString)] +r2perm = TRecord [("y", TString), ("x", TInt)] +r3 = TRecord [("x", TTop)] +innerRecX = TRecord [("a", TInt), ("b", TInt)] +innerRecY = TRecord [("m", TInt), ("n", TInt)] +r4 = TRecord [("x", innerRecX), ("y", innerRecY)] +r5 = TRecord [("x", TRecord [("a", TInt)]), ("y", TRecord [("n", TInt)]) ] + +-- Transitivity on Records +recA = TRecord [("v1", TInt), ("v2", TString), ("v3", TBool)] +recB = TRecord [("v3", TBool), ("v2", TString)] +recC = TRecord [("v2", TString)] + +-- T3 <: T1 T2 <: T4 +-- ---------------------- +-- T1 -> T2 <: T3 -> T4 +arr = TArrow (TRecord [("x", TInt), ("y", TInt), ("z", TInt)]) (TRecord [("x", TInt), ("y", TInt)]) +arr1 = TArrow (TRecord [("x", TInt), ("y", TInt)]) (TRecord [("x", TInt), ("y", TInt), ("w", TBool)]) +arr2 = TArrow (TRecord [("y", TInt)]) (TRecord [("w", TBool)]) +arr3 = TArrow (TRecord [("w", TInt)]) (TRecord [("x", TInt), ("y", TInt)]) + +-- Test cases + +recc = TestCase $ assertEqual "{x: Int, y: String} should be subtype of {y: String}" True (r2 <: r) + +rec1 = TestCase $ assertEqual "{x: Top} should not be subtype of {x: Int}" True (r1 <: r3) + +rec2 = TestCase $ assertEqual "{x: Int} should be subtype of {x: Top}" False (r3 <: r1) + +rec3 = TestCase $ assertEqual "Record with at least all fields of super type should be a subtype" True (r2 <: r3) + +rec4 = TestCase $ assertEqual "Record that doesn't have all fields of super type should not be a subtype" False (r1 <: r2) + +rec5 = TestCase $ assertEqual "Order of fields should not matter in a subtype relation for records" True (r2 <: r2perm) + +rec6 = TestCase $ assertEqual "Order of fields should not matter in a subtype relation for records" True (r2perm <: r2) + +rec7 = TestCase $ assertEqual "Corresponding fields should keep a subtype relation" True (r4 <: r5) + +rec8 = TestCase $ assertEqual "Corresponding fields should keep a subtype relation" False (r5 <: r4) + +recTrans = TestCase $ do assertEqual "recA should be subtype of recB" True (recA <: recB) + assertEqual "recB should be subtype of recC" True (recB <: recC) + assertEqual "recA should be subtype of recC" True (recA <: recC) + +recRefl = TestCase $ do assertEqual "A record should be subtype/supertype of itself" True (recA <: recA) + assertEqual "A record should be subtype/supertype of itself" True (recB <: recB) + assertEqual "A record should be subtype/supertype of itself" True (recC <: recC) + assertEqual "A record should be subtype/supertype of itself" True (r <: r) + assertEqual "A record should be subtype/supertype of itself" True (r1 <: r1) + assertEqual "A record should be subtype/supertype of itself" True (r2 <: r2) + assertEqual "A record should be subtype/supertype of itself" True (r3 <: r3) + assertEqual "A record should be subtype/supertype of itself" True (r4 <: r4) + assertEqual "A record should be subtype/supertype of itself" True (r5 <: r5) + +reflTInt = TestCase $ assertEqual "TInt should be subtype of itself" True (TInt <: TInt) +reflTBool = TestCase $ assertEqual "TInt should be subtype of itself" True (TBool <: TBool) +reflTString = TestCase $ assertEqual "TInt should be subtype of itself" True (TString <: TString) + +reflArr = TestCase $ assertEqual "arr should be subtype of itself" True (arr <: arr) +arrow1 = TestCase $ assertEqual "Should be subtype" True (arr1 <: arr) +arrow2 = TestCase $ assertEqual "Should not be subtype" False (arr2 <: arr) +arrow3 = TestCase $ assertEqual "Should not be subtype" False (arr3 <: arr) + +trans = TestCase $ do assertEqual "TBool <: TInt should return true (sub_sup list of tuples)" True (TBool <: TInt) + assertEqual "TInt <: TNumber should return true (sub_sup list of tuples)" True (TInt <: TNumber) + assertEqual "TBool <: TNumber should return true (TRANSITIVITY)" True (TBool <: TNumber)