From af1e28db0602c229f4b85d117075f964a196d33a Mon Sep 17 00:00:00 2001
From: Marvin Borner
Date: Sun, 16 Oct 2022 16:07:40 +0200
Subject: Started typing

not like i've been typing for a long time lol
---
 src/Typer.hs | 45 +++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 45 insertions(+)
 create mode 100644 src/Typer.hs

(limited to 'src/Typer.hs')

diff --git a/src/Typer.hs b/src/Typer.hs
new file mode 100644
index 0000000..0de01dd
--- /dev/null
+++ b/src/Typer.hs
@@ -0,0 +1,45 @@
+module Typer
+  ( typeCheck
+  ) where
+
+import           Helper
+
+-- removes ys from start of xs
+dropList :: (Eq a) => [a] -> [a] -> [a]
+dropList [] _  = []
+dropList xs [] = xs
+dropList e@(x : xs) (y : ys) | x == y    = dropList xs ys
+                             | otherwise = e
+
+typeMatches :: Type -> Type -> Bool
+typeMatches AnyType _       = True
+typeMatches _       AnyType = True
+typeMatches a       b       = a == b
+
+typeApply :: Type -> Type -> Type
+typeApply (FunctionType ts1) (FunctionType ts2) =
+  FunctionType $ dropList ts1 ts2
+typeApply AnyType _       = AnyType
+typeApply _       AnyType = AnyType
+typeApply a       b       = error "invalid"
+
+typeImply :: Expression -> Type
+typeImply (Bruijn      _        ) = AnyType
+typeImply (Abstraction e        ) = typeImply e
+typeImply (Application     e1 e2) = typeApply (typeImply e1) (typeImply e2)
+typeImply (TypedExpression t  _ ) = t
+typeImply _                       = error "invalid"
+
+typeCheck :: Expression -> Type -> Failable Expression
+typeCheck e@(Bruijn   _) _ = Right e
+typeCheck e@(Function _) _ = error "invalid"
+typeCheck e@(Abstraction e') (FunctionType (t : ts)) =
+  typeCheck e' (FunctionType ts) >>= pure (Right e)
+typeCheck e@(Abstraction _) _ = Right e
+typeCheck e@(Application e1 e2) t
+  | typeMatches (typeImply e) t = Right e
+  | otherwise = Left $ TypeError [(typeImply e1), (typeImply e2), t]
+typeCheck e@(MixfixChain _) _ = Right e
+typeCheck e@(Prefix _ _   ) _ = Right e
+typeCheck (TypedExpression t' e) t | typeMatches t' t = Right e
+                                   | otherwise        = Left $ TypeError [t', t]
-- 
cgit v1.2.3