From 55a446812d4406c21bc7f03f3a80a32e9608c6f6 Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Tue, 25 Dec 2018 01:26:46 +0800
Subject: [PATCH] [ #20 ] I don't know what to do

---
 src/full/OwO/TypeChecking.hs      | 22 +++++++++++++---------
 src/full/OwO/TypeChecking/Core.hs |  4 ++++
 2 files changed, 17 insertions(+), 9 deletions(-)

diff --git a/src/full/OwO/TypeChecking.hs b/src/full/OwO/TypeChecking.hs
index 51c8977..87decb6 100644
--- a/src/full/OwO/TypeChecking.hs
+++ b/src/full/OwO/TypeChecking.hs
@@ -1,13 +1,11 @@
-{-# LANGUAGE CPP             #-}
-{-# LANGUAGE LambdaCase      #-}
-{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE CPP        #-}
+{-# LANGUAGE LambdaCase #-}
 
 module OwO.TypeChecking where
 
 import           Control.Applicative     (Alternative (..))
 import           Data.Functor            ((<&>))
 import           Data.Maybe              (catMaybes)
-import           Each
 
 import           OwO.Syntax.Abstract
 import           OwO.TypeChecking.Core
@@ -17,15 +15,21 @@ import           OwO.TypeChecking.Reduce
 
 #include <impossible.h>
 
-typeCheck :: TCEnv -> PsiTerm -> Either TCErr Term
-typeCheck env (PsiConstant _ info) = Right $ Constant info
+constType :: ConstInfo -> Type
+constType = __TODO__
+
+typeCheck :: TCEnv -> PsiTerm -> Either TCErr (Type, Term)
+typeCheck env (PsiConstant _ info) = Right (constType info, Constant info)
 typeCheck env (PsiLambda binder term) = return __TODO__
-typeCheck env (PsiApplication func term) = $(each [|
-  App (~! typeCheck env func) (~! typeCheck env term) |] )
+typeCheck env (PsiApplication func term) = do
+  (f, ft) <- typeCheck env func
+  (x, xt) <- typeCheck env term
+  -- TODO: check the relationship
+  return (__TODO__, App f x)
 typeCheck env (PsiReference name) =
   case contextual <|> builtin of
     Nothing  -> Left  $ UnresolvedReferenceErr name
-    Just def -> Right $ Ref FunctionName name def
+    Just def -> Right (definitionType def, Ref FunctionName name def)
   where
     txt = textOfName name
     builtin = builtinDefinition txt
diff --git a/src/full/OwO/TypeChecking/Core.hs b/src/full/OwO/TypeChecking/Core.hs
index 788679c..219a10c 100644
--- a/src/full/OwO/TypeChecking/Core.hs
+++ b/src/full/OwO/TypeChecking/Core.hs
@@ -20,6 +20,7 @@ module OwO.TypeChecking.Core
 
   , builtinDefinition
   , builtinDefinition'
+  , definitionType
 
   , Definition(..)
   ) where
@@ -97,6 +98,9 @@ data Definition
   -- ^ No type signature, just an expression with (optional) type specified
   deriving (Eq, Generic, Ord, Show)
 
+definitionType :: Definition -> Type
+definitionType (SimpleDefinition t _) = t
+
 -- | Built-in definition: Type0, Type1, etc
 typeUniverseOfLevel :: Int -> Definition
 typeUniverseOfLevel = uncurry SimpleDefinition . typeUniverseOfLevel'