[ #20 ] Initial work

src/full/OwO/Syntax/Abstract.hs

@@ -1,4 +1,5 @@
 {-# LANGUAGE CPP                   #-}
+{-# LANGUAGE DeriveFunctor         #-}
 {-# LANGUAGE DuplicateRecordFields #-}
 {-# LANGUAGE MultiWayIf            #-}
 {-# LANGUAGE TypeOperators         #-}
@@ -31,7 +32,7 @@ module OwO.Syntax.Abstract
   , AstDeclaration
   -- Declarations
 
-  , ULevel(..)
+  , ULevel'(..)
   ) where
 
 import           Control.Applicative
@@ -49,7 +50,7 @@ import qualified OwO.Util.StrictMaybe as Strict
 data AstTerm' c
   = AstLiteral Loc LiteralInfo
   -- ^ Constants, same as in Psi
-  | AstTypeLit c ULevel
+  | AstTypeLit c (ULevel' (AstTerm' c))
   -- ^ Type literal
   | AstApp (AstTerm' c) (AstTerm' c)
   -- ^ Application
@@ -112,14 +113,26 @@ data AstDeclaration' t c
   -- ^ Functions with types but no implementations
   deriving (Eq, Ord, Show)
 
-data ULevel
+data ULevel' c
   = ULevelLit Int
   -- ^ Like Type0, Type1
-  | ULevelVar String Int
-  -- ^ Level variables. Should be already computed.
+  | ULevelVar c
+  -- ^ Level variables
   | ULevelMax
   -- ^ TypeInf, TypeOmega
-  deriving (Eq, Ord, Show)
+  deriving (Eq, Functor, Ord, Show)
+
+instance Enum (ULevel' c) where
+  succ (ULevelLit i) = ULevelLit $ succ i
+  succ ULevelMax = ULevelMax
+  succ _ = error __TODO__
+  pred (ULevelLit i) = ULevelLit $ pred i
+  pred ULevelMax = ULevelMax
+  pred _ = error __TODO__
+  toEnum = ULevelLit
+  fromEnum (ULevelLit i) = i
+  fromEnum ULevelMax = -1
+  fromEnum _ = -2
 
 type AstDeclaration = AstDeclaration' AstTerm' Name
 type AstTerm        = AstTerm' Name

src/full/OwO/TypeChecking.hs

@@ -18,6 +18,7 @@ import           Control.Monad.State
 import           Data.Functor             ((<&>))
 import           Data.Maybe               (catMaybes)
 
+import           OwO.Syntax.Abstract
 import           OwO.Syntax.Concrete
     ( LiteralInfo
     , PsiFile (..)
@@ -37,6 +38,33 @@ import           OwO.TypeChecking.Reduce
 literalType :: LiteralInfo -> Type
 literalType _ = Var __TODO__
 
+-- | Check if some @AstTerm@ is a type-correct term of type @Type@
+checkExpr :: TCM m => AstTerm -> Type -> m Term
+checkExpr term ty = case term of
+  AstTypeLit name level -> do
+    typeLevel <- case ty of
+      TType l -> pure l
+      _       -> throwError $ TypeMismatch "Type mismatch"
+    termLevel <- case level of
+      ULevelLit i -> pure $ ULevelLit i
+      ULevelVar v -> ULevelVar <$> checkInfer v
+      ULevelMax   -> pure ULevelMax
+    case typeLevel of
+      ULevelLit _ | succ termLevel == typeLevel -> pure $ TType termLevel
+      ULevelVar var -> pure __TODO__
+      ULevelMax     -> pure $ TType termLevel
+  _ -> throwError __TODO__
+
+-- | Infer the type of an @AstTerm@
+checkInfer :: TCM m => AstTerm -> m Term
+checkInfer = \case
+  AstTypeLit name level -> case level of
+    ULevelLit lit -> pure . TType $ ULevelLit lit
+    ULevelVar var -> TType . ULevelVar <$> checkInfer var
+    ULevelMax     -> pure $ TType ULevelMax
+  AstLocalRef name index -> pure $ Var index
+  _ -> pure __TODO__
+
 typeCheckFile :: TCM m => PsiFile -> m ()
 typeCheckFile file = do
   let decls       = declarations file

src/full/OwO/TypeChecking/Core.hs

@@ -1,5 +1,4 @@
 {-# LANGUAGE CPP                   #-}
-{-# LANGUAGE DeriveFunctor         #-}
 {-# LANGUAGE DuplicateRecordFields #-}
 
 -- | Core language
@@ -12,6 +11,7 @@ module OwO.TypeChecking.Core
   , Type
   , typeUniverseOfLevel
   , typeUniverseOfLevel'
+  , typeOfLevel
   , definitionType
 
   , Definition(..)
@@ -39,10 +39,10 @@ data Term' i
   | Bind i !(BinderInfo (Term' i)) (Term' i)
   -- ^ Name binding
 -}
-  | TType ULevel
+  | TType (ULevel' (Term' i))
   -- ^ Type of Type, including type omega
   | Const LiteralInfo
-  deriving (Eq, Functor, Ord, Show)
+  deriving (Eq, Ord, Show)
 
 -- TODO
 
@@ -75,4 +75,7 @@ typeUniverseOfLevel :: Int -> Definition
 typeUniverseOfLevel = uncurry SimpleDefinition . typeUniverseOfLevel'
 
 typeUniverseOfLevel' :: Int -> (Term, Type)
-typeUniverseOfLevel' i = (TType . ULevelLit $ succ i, TType $ ULevelLit i)
+typeUniverseOfLevel' i = (typeOfLevel $ succ i, typeOfLevel i)
+
+typeOfLevel :: Int -> Term
+typeOfLevel = TType . ULevelLit

src/full/OwO/TypeChecking/Monad.hs

@@ -51,6 +51,7 @@ data TCEnv = TypeCheckingEnv
 -- | TypeChecking Error
 data TCError
   = DesugarErr DesugarError
+  | TypeMismatch String
   | OtherErr String
   deriving (Eq, Show)