[ #7 ] Add type

src/full/OwO/Syntax/Abstract.hs

@@ -191,8 +191,8 @@ type DataPragmas = [DataPragma]
 -- | Top-level declarations
 --   TODOs: PsiCodata, PsiPattern, PsiCopattern
 data PsiDeclaration' t c
-  = PsiFixity PsiFixityInfo [c]
-  -- ^ infix, infixl, infixr
+  = PsiFixity PsiFixityInfo Int [c]
+  -- ^ (infix, infixl, infixr), priority, symbols
   | PsiType c FnPragmas (t c)
   -- ^ Type signature
   | PsiSubmodule QModuleName [PsiDeclaration' t c]

src/full/OwO/TypeChecking.hs

@@ -18,9 +18,11 @@ typeCheck :: TCEnv -> PsiTerm -> Either TCErr Term
 typeCheck env term = return __TODO__
 
 typeCheckFile :: TCState -> PsiFile -> TCM ()
-typeCheckFile state file@(PsiFile _ moduleName decls) = do
-  let typeSignatures = catMaybes $ decls <&> \case
-        PsiType name pragmas t -> Just (name, pragmas, t)
+typeCheckFile state file = do
+  let decls      = declarations file
+  let moduleName = topLevelModuleName file
+  let signatures = catMaybes $ decls <&> \case
+        PsiType name pragmas t -> Just (name, (pragmas, t))
         _ -> Nothing
   -- TODO:
   --  Look for definitions, give warnings about unimplemented definitions

src/full/OwO/TypeChecking/Core.hs

@@ -9,9 +9,13 @@ module OwO.TypeChecking.Core
   , ULevel(..)
   , BinderInfo(..)
   , ConstInfo(..)
+
   , Term'(..)
   , Term
   , Type
+  , typeUniverseOfLevel
+  , typeUniverseModule
+
   , Definition(..)
   ) where
 
@@ -92,3 +96,11 @@ data Definition
   = SimpleDefinition !Type !Term
   -- ^ No type signature, just an expression with (optional) type specified
   deriving (Eq, Generic, Ord, Show)
+
+-- | Built-in definition: Type0, Type1, etc
+typeUniverseOfLevel :: Int -> Definition
+typeUniverseOfLevel i = SimpleDefinition (TType $ ULevelLit $ succ i) (TType $ ULevelLit i)
+
+-- | Module name for type universes. Like a placeholder
+typeUniverseModule :: QModuleName
+typeUniverseModule = QModuleName ["OwO", "Primitive"]