git.iko.soy/Idris-dev
on ee3dbaa help sign in
Idris-dev/src/Typecheck.hs
181 lines 7.4 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor #-}
3module Typecheck where
5import Control.Monad.State
6import Debug.Trace
8import Core
9import Evaluate
11-- To check conversion, normalise each term wrt the current environment.
12-- Since we haven't converted everything to de Bruijn indices yet, we'll have to
13-- deal with alpha conversion - we do this by making each inner term de Bruijn
14-- indexed with 'finalise'
16converts :: Context -> Env -> Term -> Term -> TC ()
17converts ctxt env x y = if (finalise (normalise ctxt env x) ==
18 finalise (normalise ctxt env y))
19 then return ()
20 else fail ("Can't convert between " ++
21 showEnv env (finalise (normalise ctxt env x)) ++ " and " ++
22 showEnv env (finalise (normalise ctxt env y)))
24isSet :: Context -> Env -> Term -> TC ()
25isSet ctxt env tm = isSet' (normalise ctxt env tm)
26 where isSet' :: Term -> TC ()
27 isSet' (Set _) = return ()
28 isSet' tm = fail (showEnv env tm ++ " is not a Set")
30recheck :: Context -> Env -> Term -> TC (Term, Type)
31recheck ctxt env tm = check ctxt env (forget tm)
33check :: Context -> Env -> Raw -> TC (Term, Type)
34check ctxt env (Var n)
35 | Just (i, ty) <- lookupTyEnv n env = return (P Bound n ty, ty)
36 | Just (P nt n' ty) <- lookupP n ctxt = return (P nt n' ty, ty)
37 | otherwise = do fail $ "No such variable " ++ show n
38check ctxt env (RApp f a)
39 = do (fv, fty) <- check ctxt env f
40 (av, aty) <- check ctxt env a
41 let fty' = normalise ctxt env fty
42-- trace (showEnv env fty ++ " ===> " ++ showEnv env fty') $
43 case fty' of
44 Bind x (Pi s) t ->
45 do converts ctxt env s aty
46 return (App fv av,
47 normalise ctxt env (Bind x (Let aty av) t))
48 t -> fail "Can't apply a non-function type"
49check ctxt env (RSet i) = return (Set i, Set i) -- LATER: (i+1))
50check ctxt env (RBind n b sc)
51 = do b' <- checkBinder b
52 (scv, sct) <- check ctxt ((n, b'):env) sc
53 discharge n b' (pToV n scv) (pToV n sct)
54 where checkBinder (Lam t)
55 = do (tv, tt) <- check ctxt env t
56 let tv' = normalise ctxt env tv
57 let tt' = normalise ctxt env tt
58 isSet ctxt env tt'
59 return (Lam tv')
60 checkBinder (Pi t)
61 = do (tv, tt) <- check ctxt env t
62 let tv' = normalise ctxt env tv
63 let tt' = normalise ctxt env tt
64 isSet ctxt env tt'
65 return (Pi tv')
66 checkBinder (Let t v)
67 = do (tv, tt) <- check ctxt env t
68 (vv, vt) <- check ctxt env v
69 let tv' = normalise ctxt env tv
70 let tt' = normalise ctxt env tt
71 converts ctxt env tv vt
72 isSet ctxt env tt'
73 return (Let tv' vv)
74 checkBinder (NLet t v)
75 = do (tv, tt) <- check ctxt env t
76 (vv, vt) <- check ctxt env v
77 let tv' = normalise ctxt env tv
78 let tt' = normalise ctxt env tt
79 converts ctxt env tv vt
80 isSet ctxt env tt'
81 return (NLet tv' vv)
82 checkBinder (Hole t)
83 = do (tv, tt) <- check ctxt env t
84 let tv' = normalise ctxt env tv
85 let tt' = normalise ctxt env tt
86 isSet ctxt env tt'
87 return (Hole tv')
88 checkBinder (Guess t v)
89 = do (tv, tt) <- check ctxt env t
90 (vv, vt) <- check ctxt env v
91 let tv' = normalise ctxt env tv
92 let tt' = normalise ctxt env tt
93 converts ctxt env tv vt
94 isSet ctxt env tt'
95 return (Guess tv' vv)
96 checkBinder (PVar t)
97 = do (tv, tt) <- check ctxt env t
98 let tv' = normalise ctxt env tv
99 let tt' = normalise ctxt env tt
100 isSet ctxt env tt'
101 return (PVar tv')
103 discharge n (Lam t) scv sct
104 = return (Bind n (Lam t) scv, Bind n (Pi t) sct)
105 discharge n (Pi t) scv sct
106 = return (Bind n (Pi t) scv, sct)
107 discharge n (Let t v) scv sct
108 = return (Bind n (Let t v) scv, Bind n (Let t v) sct)
109 discharge n (NLet t v) scv sct
110 = return (Bind n (NLet t v) scv, Bind n (Let t v) sct)
111 discharge n (Hole t) scv sct
112 = do -- A hole can't appear in the type of its scope
113 checkNotHoley 0 sct
114 return (Bind n (Hole t) scv, sct)
115 discharge n (Guess t v) scv sct
116 = do -- A hole can't appear in the type of its scope
117 checkNotHoley 0 sct
118 return (Bind n (Guess t v) scv, sct)
119 discharge n (PVar t) scv sct
120 = return (Bind n (PVar t) scv, sct)
122 checkNotHoley i (V v)
123 | v == i = fail "You can't put a hole where a hole don't belong"
124 checkNotHoley i (App f a) = do checkNotHoley i f
125 checkNotHoley i a
126 checkNotHoley i (Bind n b sc) = checkNotHoley (i+1) sc
127 checkNotHoley _ _ = return ()
129pToV :: Eq n => n -> TT n -> TT n
130pToV n = pToV' 0 where
131 pToV' i (P _ x _) | n == x = V i
132 pToV' i (Bind x b sc)
133 | n == x = Bind x (fmap (pToV' i) b) sc
134 | otherwise = Bind x (fmap (pToV' i) b) (pToV' (i+1) sc)
135 pToV' i (App f a) = App (pToV' i f) (pToV' i a)
136 pToV' i t = t
138vToP :: TT n -> TT n
139vToP = vToP' [] where
140 vToP' env (V i) = let (n, b) = (env !! i) in
141 P Bound n (binderTy b)
142 vToP' env (Bind n b sc) = let b' = fmap (vToP' env) b in
143 Bind n b' (vToP' ((n, b'):env) sc)
144 vToP' env (App f a) = App (vToP' env f) (vToP' env a)
145 vToP' env t = t
147instantiate :: TT n -> TT n -> TT n
148instantiate e = subst 0 where
149 subst i (V x) | i == x = e
150 subst i (Bind x b sc) = Bind x (fmap (subst i) b) (subst (i+1) sc)
151 subst i (App f a) = App (subst i f) (subst i a)
152 subst i t = t
154finalise :: Eq n => TT n -> TT n
155finalise (Bind x b sc) = Bind x (fmap finalise b) (pToV x (finalise sc))
156finalise (App f a) = App (finalise f) (finalise a)
157finalise t = t
159checkProgram :: Context -> RProgram -> TC Context
160checkProgram ctxt [] = return ctxt
161checkProgram ctxt ((n, RConst t) : xs)
162 = do (t', tt') <- trace (show n) $ check ctxt [] t
163 isSet ctxt [] tt'
164 checkProgram (addConstant n t' ctxt) xs
165checkProgram ctxt ((n, RFunction (RawFun ty val)) : xs)
166 = do (ty', tyt') <- trace (show n) $ check ctxt [] ty
167 (val', valt') <- check ctxt [] val
168 isSet ctxt [] tyt'
169 converts ctxt [] ty' valt'
170 checkProgram (addToCtxt n val' ty' ctxt) xs
171checkProgram ctxt ((n, RData (RDatatype _ ty cons)) : xs)
172 = do (ty', tyt') <- trace (show n) $ check ctxt [] ty
173 isSet ctxt [] tyt'
174 -- add the tycon temporarily so we can check constructors
175 let ctxt' = addDatatype (Data n ty' []) ctxt
176 cons' <- mapM (checkCon ctxt') cons
177 checkProgram (addDatatype (Data n ty' cons') ctxt) xs
178 where checkCon ctxt (n, cty) = do (cty', ctyt') <- check ctxt [] cty
179 return (n, cty')