blob: 0de01dd21844324163dedbd0976b060f3e0f059a (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
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]
|
