1 files changed, 38 insertions, 26 deletions

diff --git a/src/TypeCheck.hs b/src/TypeCheck.hs
index 4c05c4b..1406a67 100644
--- a/src/TypeCheck.hs
+++ b/src/TypeCheck.hs
@@ -3,22 +3,37 @@
 {-# LANGUAGE DeriveFunctor #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE DeriveFoldable #-}
-module TypeCheck where
+module TypeCheck (typeCheck, typeInfer) where
 
 import Control.Monad
-import Control.Monad.Trans.Class
-import Control.Monad.Trans.State.Strict
-import Control.Monad.Trans.Writer.CPS
-import Data.Foldable (toList)
-import Data.Map.Strict (Map)
+-- import Control.Monad.Trans.Class
+-- import Control.Monad.Trans.State.Strict
+-- import Control.Monad.Trans.Writer.CPS
+-- import Data.Foldable (toList)
+-- import Data.Map.Strict (Map)
 import qualified Data.Map.Strict as Map
-import Numeric.Natural
+-- import Numeric.Natural
 
 import AST
 
 
+typeCheck :: Env -> Term -> Term -> Either String Term
+typeCheck env typ term =
+  runTM (check env term typ)
+  -- runTM (check env term typ) >>= \case
+  --   ([], term') -> return term'
+  --   (_, _) -> error "Don't know how to solve constraints yet"
+
+typeInfer :: Env -> Term -> Either String (OfType Term Term)
+typeInfer env term =
+  runTM (infer env term)
+  -- runTM (infer env term) >>= \case
+  --   ([], jud) -> return jud
+  --   (_, _) -> error "Don't know how to solve constraints yet"
+
+
 -- | type checking monad
-newtype TM a = TM (WriterT (Bag Constr) (StateT Natural (Either String)) a)
+newtype TM a = TM ({- WriterT (Bag Constr) (StateT Natural ( -} Either String {- )) -} a)
   deriving stock (Functor)
   deriving newtype (Applicative, Monad)
 
@@ -31,28 +46,23 @@ data Constr = VarEq Name Term
             | LevelLeq Term Term
   deriving (Show)
 
-type Subst = Map Name Term
-
-runTM :: TM a -> Either String ([Constr], a)
-runTM (TM m) = do
-  (res, cs) <- evalStateT (runWriterT m) 0
-  return (toList cs, res)
+runTM :: TM a -> Either String a
+runTM (TM m) = m
+  -- (res, cs) <- evalStateT (runWriterT m) 0
+  -- return (toList cs, res)
 
-genId :: TM Natural
-genId = TM (lift (state (\i -> (i, i + 1))))
+-- genId :: TM Natural
+-- genId = TM (lift (state (\i -> (i, i + 1))))
 
-genName :: TM Name
-genName = ("." ++) . show <$> genId
+-- genName :: TM Name
+-- genName = ("." ++) . show <$> genId
 
 throw :: String -> TM a
-throw err = TM (lift (lift (Left err)))
+-- throw err = TM (lift (lift (Left err)))
+throw err = TM (Left err)
 
-emit :: Constr -> TM ()
-emit c = TM (tell (BOne c))
-
-data OfType a b = a :| b
-  deriving stock (Show)
-infix 1 :|
+-- emit :: Constr -> TM ()
+-- emit c = TM (tell (BOne c))
 
 check :: Env -> Term -> Term -> TM Term
 check env topTerm typ = case topTerm of
@@ -151,8 +161,10 @@ infer env = \case
   TSigma x a b -> do
     inferW env a >>= \case
       a' :| TSet lvlA -> do
-        inferW env b >>= \case
+        inferW (Map.insert x a' env) b >>= \case
           b' :| TSet lvlB -> do
+            when (x `freeIn` lvlB) $
+              throw $ "Variable " ++ show x ++ " escapes Sigma"
             return (TSigma x a' b' :| TSet (TIMax lvlA lvlB))
           _ :| tb -> throw $ "RHS of a Sigma not of type Set i, but: " ++ show tb
       _ :| ta -> throw $ "LHS type of a Sigma not of type Set i, but: " ++ show ta