Comparing of types that is indifferent to changes in names of type va…

…riables (things like: TVar X1).

interpreter/Lucretia/TypeChecker/Main.hs

@@ -191,23 +191,23 @@ findType env (EIf eIf eThen eElse) = do
   return $ mergeTypes tThen tElse
 
 findType env (EFunc (Func xParams tFunc eBody)) = do
-  let TFunc expectedConstraintsBefore tParams tBody expectedConstraintsAfter = tFunc
+  let TFunc expectedConstraintsBefore tParams expectedU expectedConstraintsAfter = tFunc
   (length xParams == length tParams) `orFail` "Number of arguments and number of their types doesn't match"
   let params = zip xParams tParams
   let extendedEnv = foldl (\envAccumulator (eXi, tXi) -> Map.insert eXi tXi envAccumulator) env params
   constraintsBeforeBody <- getConstraints
 
   putConstraints expectedConstraintsBefore
   u <- findTypeCleanConstraints extendedEnv eBody
-  (tBody == u) `orFail` ("Expected type: " ++ show tBody ++ " is different than actual type: " ++ show u)
   actualConstraintsAfter <- getConstraints
-  (expectedConstraintsAfter == actualConstraintsAfter) `orFail` ("Constraints after type-checking method body: " ++ showConstraints actualConstraintsAfter ++ " are not the same as declared in the signature: " ++ showConstraints expectedConstraintsAfter ++ ".")
+  --(expectedU, expectedConstraintsAfter) `areIsomorphic` (u, actualConstraintsAfter)
+  (TypeIso expectedU expectedConstraintsAfter == TypeIso u actualConstraintsAfter) `orFail` ("Type and associated constraints after type-checking method body: " ++ show u ++ ", " ++ showConstraints actualConstraintsAfter ++ " are not the same as declared in the signature: " ++ show expectedU ++ ", " ++ showConstraints expectedConstraintsAfter ++ ".")
   --TODO maybe this:
   --(actualConstraintsAfter `areAtLeastThatStrongAs` expectedConstraintsAfter) `orFail` ("Returned value should match at least all the constraints that are declared in the signature of function " ++ funcName ++ ".")
 
   putConstraints constraintsBeforeBody
 
-  return tFunc
+  return tFunc --TODO: test eFuncWithUnnecessaryConstraints, tFunc { constraintsAfter = cleanConstraints (Map.fromList [("_", expectedU)] (constraintsAfter tFunc) }
 
 findType env (ECall eFunc eParams) = do
   let funcName = findName env eFunc

interpreter/Lucretia/TypeChecker/Test.hs

@@ -27,7 +27,7 @@ outputTypeTestsData = [
   (VARIABLE_NAME(eIfTOr), "Right (X1,[X1 < {a:int v bool}])"),
   (VARIABLE_NAME(eIfTFieldUndefined), "Right (X1,[X1 < {a:undefined v int, b:undefined v bool}])"),
   (VARIABLE_NAME(eFunc), "Right (([] bool int -> bool []),[])"),
-  (VARIABLE_NAME(eFuncWrongReturnType), "Left \"Expected type: int is different than actual type: bool\""),
+  (VARIABLE_NAME(eFuncWrongReturnType), "Left \"Type and associated constraints after type-checking method body: bool, [] are not the same as declared in the signature: int, [].\""),
   (VARIABLE_NAME(eFuncWithConstraints), "Right (([] bool int -> X1 [X1 < {a:int}]),[])"),
   (VARIABLE_NAME(eFuncWrongNumberOfArguments), "Left \"Number of arguments and number of their types doesn't match\""),
   --maybe this should be ok:
@@ -36,7 +36,15 @@ outputTypeTestsData = [
   (VARIABLE_NAME(eLetDefiningRecordInsideButNotReturningIt), "Right (bool,[])"),
   (VARIABLE_NAME(eFuncDefiningNestedRecordInsideAndReturningIt), "Right (([] bool int -> X3 [X1 < {a:int}, X3 < {c:X1}]),[])"),
   (VARIABLE_NAME(eLetDefiningNestedRecordInsideAndReturningIt), "Right (X3,[X1 < {a:int}, X3 < {c:X1}])"),
+  (VARIABLE_NAME(eFuncDefiningNestedRecordInsideAndReturningItHavingDifferentlyNamedConstraintVariables), "Right (([] bool int -> C [A < {a:int}, C < {c:A}]),[])"),
+  (VARIABLE_NAME(eFuncWithUnnecessaryConstraints), "Right (([] bool int -> X1 [X1 < {a:int}]),[])"),
+  (VARIABLE_NAME(eFuncDefiningNestedRecordInsideAndHavingMismatchingConstraintSignature1), "Left \"Type and associated constraints after type-checking method body: X3, [X1 < {a:int}, X3 < {c:X1}] are not the same as declared in the signature: C, [C < {c:int}].\""),
+
+  --TODO test catching error
+  (VARIABLE_NAME(eFuncDefiningNestedRecordInsideAndHavingWrongConstraintSignature), ""),
   (VARIABLE_NAME(eCall), "Right (X1,[X1 < {a:int}])"),
+  (VARIABLE_NAME(eLetReturningCyclicNestedRecord), "Right (X3,[X1 < {a:X3}, X3 < {c:X1}])"),
+  (VARIABLE_NAME(eFuncReturningCyclicNestedRecord), ""),
   (VARIABLE_NAME(eCallLet), "Right (X1,[X1 < {a:int}])")
   ]
 
@@ -141,6 +149,25 @@ eFuncDefiningNestedRecordInsideAndReturningIt =
     eLetDefiningNestedRecordInsideAndReturningIt
   )
 
+eLetReturningCyclicNestedRecord :: Exp
+eLetReturningCyclicNestedRecord =
+  ELet "x" ENew $
+  ELet "y" ENew $
+  ELet "z" ENew $
+  ELet "_" (ESet "x" "a" $ EVar "z") $
+  ELet "_" (ESet "y" "b" $ EInt 7) $
+  ELet "_" (ESet "z" "c" $ EVar "x") $
+    EVar "z"
+
+eFuncReturningCyclicNestedRecord :: Exp
+eFuncReturningCyclicNestedRecord =
+  EFunc (Func 
+    ["x1", "x2"]
+    (TFunc (Map.empty) [TBool, TInt] (TVar "X3") (Map.fromList [("X1", oneFieldTRec "a" (TVar "X3")), ("X3", oneFieldTRec "c" (TVar "X1"))])) $
+    eLetReturningCyclicNestedRecord
+  )
+
+
 eLetDefiningNestedRecordInsideAndReturningIt :: Exp
 eLetDefiningNestedRecordInsideAndReturningIt =
   ELet "x" ENew $
@@ -151,6 +178,38 @@ eLetDefiningNestedRecordInsideAndReturningIt =
   ELet "_" (ESet "z" "c" $ EVar "x") $
     EVar "z"
 
+eFuncDefiningNestedRecordInsideAndReturningItHavingDifferentlyNamedConstraintVariables :: Exp
+eFuncDefiningNestedRecordInsideAndReturningItHavingDifferentlyNamedConstraintVariables =
+  EFunc (Func 
+    ["x1", "x2"]
+    (TFunc (Map.empty) [TBool, TInt] (TVar "C") (Map.fromList [("A", oneFieldTRec "a" TInt), ("C", oneFieldTRec "c" (TVar "A"))])) $
+    eLetDefiningNestedRecordInsideAndReturningIt
+  )
+
+eFuncDefiningNestedRecordInsideAndHavingMismatchingConstraintSignature1 :: Exp
+eFuncDefiningNestedRecordInsideAndHavingMismatchingConstraintSignature1 =
+  EFunc (Func 
+    ["x1", "x2"]
+    (TFunc (Map.empty) [TBool, TInt] (TVar "C") (Map.fromList [("C", oneFieldTRec "c" TInt)])) $
+    eLetDefiningNestedRecordInsideAndReturningIt
+  )
+
+eFuncWithUnnecessaryConstraints :: Exp
+eFuncWithUnnecessaryConstraints =
+  EFunc (Func 
+    ["x1", "x2"]
+    (TFunc (Map.fromList []) [TBool, TInt] (TVar "X1") (Map.fromList [("X1", oneFieldTRec "a" TInt), ("X2", oneFieldTRec "b" TBool)]))
+    eRecordWithOneField
+  )
+
+eFuncDefiningNestedRecordInsideAndHavingWrongConstraintSignature :: Exp
+eFuncDefiningNestedRecordInsideAndHavingWrongConstraintSignature =
+  EFunc (Func 
+    ["x1", "x2"]
+    (TFunc (Map.empty) [TBool, TInt] (TVar "C") (Map.fromList [("A", oneFieldTRec "a" TInt)])) $
+    eLetDefiningNestedRecordInsideAndReturningIt
+  )
+
 eFuncDefiningRecordInsideButNotReturningIt :: Exp
 eFuncDefiningRecordInsideButNotReturningIt =
   EFunc (Func 

interpreter/Lucretia/TypeChecker/Types.hs

@@ -56,3 +56,38 @@ instance Show Type where
 
 oneFieldTRec :: Name -> Type -> RecType
 oneFieldTRec a t = Map.fromList [(a,t)]
+
+
+data TypeIso = TypeIso Type Constraints
+data MapNameTypeIso = MapNameTypeIso Env Constraints
+data NameIso = NameIso Name Constraints
+data RecTypeIso = RecTypeIso RecType Constraints
+
+instance Eq MapNameTypeIso where
+  MapNameTypeIso e1 cs1 == MapNameTypeIso e2 cs2 = (toTypeIso e1 cs1) == (toTypeIso e2 cs2)
+    where
+    toTypeIso e cs = Map.map (\t -> TypeIso t cs) e
+
+--Why *Iso types? To avoid rewriting the contents of "instance Eq (Map * *)".
+
+--TODO introduce state: visited nodes, to avoid non-termination
+--Problem with introducing state: how to have a state that is transferred between nodes compared in the code of "instance Eq (Map * *)" without rewriting this code.
+  -- 1. solution (unclean): use global state / global variables
+  -- 2. solution (not really answering above question): rewrite "instance Eq (Map * *)" using fold / State monad
+
+instance Eq TypeIso where
+  TypeIso (TVar n1) cs1 == TypeIso (TVar n2) cs2 = 
+    NameIso n1 cs1 == NameIso n2 cs2
+  TypeIso t1 _ == TypeIso t2 _ = 
+    t1 == t2
+
+instance Eq NameIso where
+  NameIso n1 cs1 == NameIso n2 cs2 = RecTypeIso (cs1 `findOrFail` n1) cs1 == RecTypeIso (cs2 `findOrFail` n2) cs2
+    where
+    cs `findOrFail` n = case Map.lookup n cs of
+			  Just result -> result
+			  Nothing     -> error $ "Cannot find type variable named: " ++ n1 ++ " in constraints: " ++ showConstraints cs ++ "."
+
+instance Eq RecTypeIso where
+  RecTypeIso r1 cs1 == RecTypeIso r2 cs2 = MapNameTypeIso r1 cs1 == MapNameTypeIso r2 cs2
+