git.iko.soy/Idris-dev
on d615021 help sign in
Idris-dev/src/Typecheck.hs
143 lines 5.2 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor #-}
3module Typecheck where
5import Control.Monad.State
6import Debug.Trace
8import Core
9import Evaluate
11data TC a = OK a
12 | Error String -- TMP! Make this an informative data structure
13 deriving (Eq, Functor)
15instance Show a => Show (TC a) where
16 show (OK x) = show x
17 show (Error str) = "Error: " ++ str
19-- at some point, this instance should also carry type checking options
20-- (e.g. Set:Set)
22instance Monad TC where
23 return = OK
24 x >>= k = case x of
25 OK v -> k v
26 Error e -> Error e
27 fail = Error
29instance MonadPlus TC where
30 mzero = Error "Unknown error"
31 (OK x) `mplus` _ = OK x
32 _ `mplus` (OK y) = OK y
33 err `mplus` _ = err
35converts :: Context -> Env -> Term -> Term -> TC ()
36converts ctxt env x y = if (normalise ctxt env (bindEnv env x) ==
37 normalise ctxt env (bindEnv env y))
38 then return ()
39 else fail ("Can't convert between " ++
40 show x ++ " and " ++ show y)
42isSet :: Term -> TC ()
43isSet (Set _) = return ()
44isSet tm = fail (show tm ++ " is not a Set")
46check :: Context -> Env -> Raw -> TC (Term, Type)
47check ctxt env (Var n)
48 | Just (i, ty) <- lookupTyEnv n env = return (V i, ty)
49 | Just (P nt n' ty) <- lookupP n ctxt = return (P nt n' ty, ty)
50 | otherwise = do fail $ "No such variable " ++ show n
51check ctxt env (RApp f a)
52 = do (fv, fty) <- check ctxt env f
53 (av, aty) <- check ctxt env a
54 let fty' = normalise ctxt env fty
55 case fty' of
56 Bind x (Pi s) t ->
57 do converts ctxt env s aty
58 return (App fv av,
59 normalise ctxt env (Bind x (Let aty av) t))
60 t -> fail "Can't apply a non-function type"
61check ctxt env (RSet i) = return (Set i, Set (i+1))
62check ctxt env (RBind n b sc)
63 = do b' <- checkBinder b
64 (scv, sct) <- check ctxt ((n, b'):env) sc
65 discharge n b' scv sct
66 where checkBinder (Lam t)
67 = do (tv, tt) <- check ctxt env t
68 let tv' = normalise ctxt env tv
69 let tt' = normalise ctxt env tt
70 isSet tt'
71 return (Lam tv')
72 checkBinder (Pi t)
73 = do (tv, tt) <- check ctxt env t
74 let tv' = normalise ctxt env tv
75 let tt' = normalise ctxt env tt
76 isSet tt'
77 return (Pi tv')
78 checkBinder (Let t v)
79 = do (tv, tt) <- check ctxt env t
80 (vv, vt) <- check ctxt env v
81 let tv' = normalise ctxt env tv
82 let tt' = normalise ctxt env tt
83 converts ctxt env tv vt
84 isSet tt'
85 return (Let tv' vv)
86 checkBinder (Hole t)
87 = do (tv, tt) <- check ctxt env t
88 let tv' = normalise ctxt env tv
89 let tt' = normalise ctxt env tt
90 isSet tt'
91 return (Hole tv')
92 checkBinder (Guess t v)
93 = do (tv, tt) <- check ctxt env t
94 (vv, vt) <- check ctxt env v
95 let tv' = normalise ctxt env tv
96 let tt' = normalise ctxt env tt
97 converts ctxt env tv vt
98 isSet tt'
99 return (Guess tv' vv)
100 checkBinder (PVar t)
101 = do (tv, tt) <- check ctxt env t
102 let tv' = normalise ctxt env tv
103 let tt' = normalise ctxt env tt
104 isSet tt'
105 return (PVar tv')
107 discharge n (Lam t) scv sct
108 = return (Bind n (Lam t) scv, Bind n (Pi t) sct)
109 discharge n (Pi t) scv sct
110 = return (Bind n (Pi t) scv, sct)
111 discharge n (Let t v) scv sct
112 = return (Bind n (Let t v) scv, Bind n (Let t v) sct)
113 discharge n (Hole t) scv sct
114 = do -- A hole can't appear in the type of its scope
115 checkNotHoley 0 sct
116 return (Bind n (Hole t) scv, sct)
117 discharge n (Guess t v) scv sct
118 = do -- A hole can't appear in the type of its scope
119 checkNotHoley 0 sct
120 return (Bind n (Guess t v) scv, sct)
121 discharge n (PVar t) scv sct
122 = return (Bind n (PVar t) scv, sct)
124 checkNotHoley i (V v)
125 | v == i = fail "You can't put a hole where a hole don't belong"
126 checkNotHoley i (App f a) = do checkNotHoley i f
127 checkNotHoley i a
128 checkNotHoley i (Bind n b sc) = checkNotHoley (i+1) sc
129 checkNotHoley _ _ = return ()
131checkProgram :: Context -> RProgram -> TC Context
132checkProgram ctxt [] = return ctxt
133checkProgram ctxt ((n, RConst t):xs)
134 = do (t', tt') <- trace (show n) $ check ctxt [] t
135 isSet tt'
136 checkProgram (addConstant n t' ctxt) xs
137checkProgram ctxt ((n, RFunction (RawFun ty val)):xs)
138 = do (ty', tyt') <- trace (show n) $ check ctxt [] ty
139 (val', valt') <- check ctxt [] val
140 isSet tyt'
141 converts ctxt [] ty' valt'
142 checkProgram (addToCtxt n val' ty' ctxt) xs