fixed type checker and the current transformations

haskell/src/ADTypes/Base.hs

@@ -109,7 +109,9 @@ inferType ctx tymap (Or t1 t2 _) = do
   checkType ctx tymap t1 Bool
   checkType ctx tymap t2 Bool
   return Bool
-inferType ctx _ (Var name _) = lookupVar ctx name
+inferType ctx tymap (Var name _) = do
+  ty <- lookupVar ctx name
+  matchTypeVar tymap ty
 inferType ctx tymap (Let name t body _) = do
   tyt <- inferType ctx tymap t
   inferType (Bind ctx name tyt) tymap body
@@ -159,14 +161,9 @@ checkType ctx tymap (Match m cases _) ty = do
     let casechecks = map (\c -> do
           tys <- liftMaybe (M.lookup (labelOfCase c) cotrs) "Could not find constructor" :: Infer [Type]
           if length (bindingsOfCase c) == length tys
-          then
-            if not (null (bindingsOfCase c))
-            then do
-              let bindchecks = map (\(b, bty) ->
-                    checkType (Bind ctx b bty) tymap (termOfCase c) ty
-                    ) $ zip (bindingsOfCase c) tys
-              foldl (>>) (return ()) bindchecks
-            else checkType ctx tymap (termOfCase c) ty
+          then do
+              let ctx' = foldl (\r (b, bty) -> Bind r b bty) ctx (zip (bindingsOfCase c) tys)
+              checkType ctx' tymap (termOfCase c) ty
           else fail "number of bindings does not match number of args of constructor"
           ) cases
     foldl (>>) (return ()) casechecks

haskell/src/ADTypes/ContinueAfterFail.hs

@@ -131,7 +131,6 @@ lookupCotr (Bind c x ty) y = case ty of
     else lookupCotr c y
   _ -> lookupCotr c y
 
-
 inferType :: Ctx -> TypeMap -> Term -> Infer Type
 inferType _ _ (Zero _) = return Nat
 inferType ctx tymap (Succ t _) = do
@@ -158,7 +157,9 @@ inferType ctx tymap (Or t1 t2 _) = do
   checkType ctx tymap t1 Bool
   checkType ctx tymap t2 Bool
   return Bool
-inferType ctx _ (Var name _) = lookupVar ctx name
+inferType ctx tymap (Var name _) = do
+  ty <- lookupVar ctx name
+  matchTypeVar tymap ty
 inferType ctx tymap (Let name t body _) = do
   tyt <- inferType ctx tymap t
   inferType (Bind ctx name tyt) tymap body
@@ -182,10 +183,10 @@ inferType ctx tymap (Cotr n ts p) = do
   if length ts == length tys
   then do
     -- check types accordingly to definition
-    let subchecks = map (\(t, ty) -> do
+    let subchecks = zipWith (\t ty -> do
           ty' <- matchTypeVar tymap ty
           checkType ctx tymap t ty'
-          ) (zip ts tys) -- basically a map over the [(Term, Type)] and apply check ctx
+          ) ts tys -- basically a map over the [(Term, Type)] and apply check ctx
     foldl (>>) (return ()) subchecks
     return adty
   else fail ["Expected number of arguments violated for " ++ show (Cotr n ts p)]
@@ -208,14 +209,9 @@ checkType ctx tymap (Match m cases _) ty = do
     let casechecks = map (\c -> do
           tys <- liftMaybe (M.lookup (labelOfCase c) cotrs) "Could not find constructor" :: Infer [Type]
           if length (bindingsOfCase c) == length tys
-          then
-            if not (null (bindingsOfCase c))
-            then do
-              let bindchecks = map (\(b, bty) ->
-                    checkType (Bind ctx b bty) tymap (termOfCase c) ty
-                    ) $ zip (bindingsOfCase c) tys
-              foldl (>>) (return ()) bindchecks
-            else checkType ctx tymap (termOfCase c) ty
+          then do
+              let ctx' = foldl (\r (b, bty) -> Bind r b bty) ctx (zip (bindingsOfCase c) tys)
+              checkType ctx' tymap (termOfCase c) ty
           else fail ["number of bindings does not match number of args of constructor"]
           ) cases
     foldl (>>) (return ()) casechecks

haskell/src/ADTypes/EliminateTypeArgumentOfCheck.hs

@@ -133,7 +133,6 @@ lookupCotr (Bind c x ty) y = case ty of
     else lookupCotr c y
   _ -> lookupCotr c y
 
-
 inferType :: Ctx -> TypeMap -> Term -> Infer Type
 inferType _ _ (Zero _) = return Nat
 inferType ctx tymap (Succ t _) = do
@@ -160,7 +159,9 @@ inferType ctx tymap (Or t1 t2 _) = do
   checkType ctx tymap t1
   checkType ctx tymap t2
   return Bool
-inferType ctx _ (Var name _) = lookupVar ctx name
+inferType ctx tymap (Var name _) = do
+  ty <- lookupVar ctx name
+  matchTypeVar tymap ty
 inferType ctx tymap (Let name t body _) = do
   tyt <- inferType ctx tymap t
   inferType (Bind ctx name tyt) tymap body
@@ -179,14 +180,15 @@ inferType ctx tymap (LetData n adty t _) =
 inferType ctx tymap (Cotr n ts p) = do
   -- TODO find better solution
   -- PROBLEM we need to find the binding that contains the constructor
+
   (adty, tys) <- lookupCotr tymap n
   if length ts == length tys
   then do
     -- check types accordingly to definition
-    let subchecks = map (\(t, ty) -> do
+    let subchecks = zipWith (\t ty -> do
           ty' <- matchTypeVar tymap ty
           checkType ctx tymap t
-          ) (zip ts tys) -- basically a map over the [(Term, Type)] and apply check ctx
+          ) ts tys -- basically a map over the [(Term, Type)] and apply check ctx
     foldl (>>) (return ()) subchecks
     return adty
   else fail ["Expected number of arguments violated for " ++ show (Cotr n ts p)]
@@ -212,14 +214,9 @@ checkType ctx tymap p@(Match m cases _) = do
     let casechecks = map (\c -> do
           tys <- liftMaybe (M.lookup (labelOfCase c) cotrs) "Could not find constructor" :: Infer [Type]
           if length (bindingsOfCase c) == length tys
-          then
-            if not (null (bindingsOfCase c))
-            then do
-              let bindchecks = map (\(b, bty) ->
-                    checkType (Bind ctx b bty) tymap (termOfCase c)
-                    ) $ zip (bindingsOfCase c) tys
-              foldl (>>) (return ()) bindchecks
-            else checkType ctx tymap (termOfCase c)
+          then do
+              let ctx' = foldl (\r (b, bty) -> Bind r b bty) ctx (zip (bindingsOfCase c) tys)
+              checkType ctx' tymap (termOfCase c)
           else fail ["number of bindings does not match number of args of constructor"]
           ) cases
     foldl (>>) (return ()) casechecks
@@ -270,9 +267,22 @@ requiredType ctx tymap term = case parent term of
     (_, cotrs) <- matchADT mty' (show m)
     if length cases == length cotrs
     then do
-      -- throw away ctx extension if bindingsOfCase c != null
-      -- let x = find (\c -> term == termOfCase c) cases
-      let (Bind ctx' _ _) = ctx
-      requiredType ctx' tymap p
-    else fail ["cases do not match number of constructors of" ++ show m]
+      let maybeCase = find (\c -> termOfCase c == term) cases
+      case maybeCase of
+        Just c -> do
+          tys <- liftMaybe (M.lookup (labelOfCase c) cotrs) "Could not find constructor" :: Infer [Type]
+          let ctx' = foldl (\r (b, bty) -> let (Bind r' _ _) = r in r') ctx (zip (bindingsOfCase c) tys)
+          ty <- requiredType ctx' tymap p
+          return ty
+        Nothing -> fail ["could not find corresponding case"]
+      -- let casechecks = map (\c -> do
+      --       tys <- liftMaybe (M.lookup (labelOfCase c) cotrs) "Could not find constructor" :: Infer [Type]
+      --       if length (bindingsOfCase c) == length tys
+      --       then do
+      --           let ctx' = foldl (\r (b, bty) -> Bind r b bty) ctx (zip (bindingsOfCase c) tys)
+      --           checkType ctx' tymap (termOfCase c)
+      --       else fail ["number of bindings does not match number of args of constructor"]
+      --       ) cases
+      -- foldl (>>) (return ()) casechecks
+    else fail [""]
   _ -> fail ["Could not determine required type"]

haskell/src/ADTypes/ErrorList.hs

@@ -82,7 +82,6 @@ lookupCotr (Bind c x ty) y = case ty of
     else lookupCotr c y
   _ -> lookupCotr c y
 
-
 inferType :: Ctx -> TypeMap -> Term -> Infer Type
 inferType _ _ (Zero _) = return Nat
 inferType ctx tymap (Succ t _) = do
@@ -109,7 +108,9 @@ inferType ctx tymap (Or t1 t2 _) = do
   checkType ctx tymap t1 Bool
   checkType ctx tymap t2 Bool
   return Bool
-inferType ctx _ (Var name _) = lookupVar ctx name
+inferType ctx tymap (Var name _) = do
+  ty <- lookupVar ctx name
+  matchTypeVar tymap ty
 inferType ctx tymap (Let name t body _) = do
   tyt <- inferType ctx tymap t
   inferType (Bind ctx name tyt) tymap body
@@ -159,14 +160,9 @@ checkType ctx tymap (Match m cases _) ty = do
     let casechecks = map (\c -> do
           tys <- liftMaybe (M.lookup (labelOfCase c) cotrs) "Could not find constructor" :: Infer [Type]
           if length (bindingsOfCase c) == length tys
-          then
-            if not (null (bindingsOfCase c))
-            then do
-              let bindchecks = map (\(b, bty) ->
-                    checkType (Bind ctx b bty) tymap (termOfCase c) ty
-                    ) $ zip (bindingsOfCase c) tys
-              foldl (>>) (return ()) bindchecks
-            else checkType ctx tymap (termOfCase c) ty
+          then do
+              let ctx' = foldl (\r (b, bty) -> Bind r b bty) ctx (zip (bindingsOfCase c) tys)
+              checkType ctx' tymap (termOfCase c) ty
           else fail "number of bindings does not match number of args of constructor"
           ) cases
     foldl (>>) (return ()) casechecks

haskell/test/ADTypes/SharedSpecs.hs

@@ -52,7 +52,7 @@ sharedSpec inferType = do
     it "should infer match with single binds" $ do
         let res = convert $ inferType tOkMatchTwo in res `shouldBe` B.Inferred boolADT
     it "should infer match with multiple binds" $ do
-        let res = convert $ inferType tOkMatchWithMultiplebinds in res `shouldBe` B.Inferred Nat
+        let res = convert $ inferType tOkMatchWithMultiplebinds in res `shouldBe` B.Inferred expADT
 
     it "should infer match for simple adt (bool)" $ do
         let res = convert $ inferType tOkMatchSingle in res `shouldBe` B.Inferred boolADT

haskell/test/ADTypes/TestCases.hs

@@ -26,7 +26,7 @@ tOkCotrSingleArg = root (letdata "Bool" (ADT "Bool" (fromList [("True", []), ("F
 tOkCotrTwoArg = root (letdata "Bool" (ADT "Bool" (fromList [("True", []), ("False", [])])) (letdata "Exp" (ADT "Exp" (fromList [("BoolExp", [TypeVar "Bool"]), ("AndExp", [TypeVar "Exp", TypeVar "Exp"]), ("NotExp", [TypeVar "Exp"])])) (cotr2 "AndExp" (cotr1 "BoolExp" (cotr0 "True")) (cotr1 "BoolExp" (cotr0 "False")))))
 tOkMatchSingle = root (letdata "Bool" (ADT "Bool" (fromList [("True", []), ("False", [])])) (anno boolADT (match2 (cotr0 "True") (case' "True" [] (cotr0 "False")) (case' "False" [] (cotr0 "True")))))
 tOkMatchTwo = root (letdata "Bool" (ADT "Bool" (fromList [("True", []), ("False", [])])) (anno boolADT (match2 (cotr0 "True") (case' "True" [] (cotr0 "False")) (case' "False" [] (cotr0 "True")))))
-tOkMatchWithMultiplebinds = root (letdata "Bool" (ADT "Bool" (fromList [("True", []), ("False", [])])) (letdata "Exp" (ADT "Exp" (fromList [("BoolExp", [TypeVar "Bool"]), ("AndExp", [TypeVar "Exp", TypeVar "Exp"]), ("NotExp", [TypeVar "Exp"])])) (anno Nat (match3 ((cotr2 "AndExp" (cotr1 "BoolExp" (cotr0 "True")) (cotr1 "BoolExp" (cotr0 "False")))) (case' "BoolExp" ["x"] zero) (case' "AndExp" ["x", "y"] (succ (succ zero))) (case' "NotExp" ["x"] (succ zero))))))
+tOkMatchWithMultiplebinds = root (letdata "Bool" (ADT "Bool" (fromList [("True", []), ("False", [])])) (letdata "Exp" (ADT "Exp" (fromList [("BoolExp", [TypeVar "Bool"]), ("AndExp", [TypeVar "Exp", TypeVar "Exp"]), ("NotExp", [TypeVar "Exp"])])) (anno expADT (match3 ((cotr2 "AndExp" (cotr1 "BoolExp" (cotr0 "True")) (cotr1 "BoolExp" (cotr0 "False")))) (case' "BoolExp" ["x"] (cotr1 "NotExp" (cotr1 "BoolExp" (var "x")))) (case' "AndExp" ["x", "y"] (cotr2 "AndExp" (var "y") (var "x"))) (case' "NotExp" ["x"] (var "x"))))))
 
 tFailArithmetic = root $ (add (succ $ succ zero) (mult (anno (Fun Nat Nat) (lam "f" (var "f"))) (succ $ succ $ succ $ succ zero)))
 tFailLambdaNoAnno = root $ (anno Nat (app (lam "b" (add (var "b") zero)) (succ $ succ zero)))