git.iko.soy/Idris-dev
on ffd5e72 help sign in
Idris-dev/src/Typecheck.hs
178 lines 7.2 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 (normalise ctxt env x) ++ " and " ++
22 showEnv env (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")
30check :: Context -> Env -> Raw -> TC (Term, Type)
31check ctxt env (Var n)
32 | Just (i, ty) <- lookupTyEnv n env = return (P Bound n ty, ty)
33 | Just (P nt n' ty) <- lookupP n ctxt = return (P nt n' ty, ty)
34 | otherwise = do fail $ "No such variable " ++ show n
35check ctxt env (RApp f a)
36 = do (fv, fty) <- check ctxt env f
37 (av, aty) <- check ctxt env a
38 let fty' = normalise ctxt env fty
39-- trace (showEnv env fty ++ " ===> " ++ showEnv env fty') $
40 case fty' of
41 Bind x (Pi s) t ->
42 do converts ctxt env s aty
43 return (App fv av,
44 normalise ctxt env (Bind x (Let aty av) t))
45 t -> fail "Can't apply a non-function type"
46check ctxt env (RSet i) = return (Set i, Set i) -- LATER: (i+1))
47check ctxt env (RBind n b sc)
48 = do b' <- checkBinder b
49 (scv, sct) <- check ctxt ((n, b'):env) sc
50 discharge n b' (pToV n scv) (pToV n sct)
51 where checkBinder (Lam t)
52 = do (tv, tt) <- check ctxt env t
53 let tv' = normalise ctxt env tv
54 let tt' = normalise ctxt env tt
55 isSet ctxt env tt'
56 return (Lam tv')
57 checkBinder (Pi t)
58 = do (tv, tt) <- check ctxt env t
59 let tv' = normalise ctxt env tv
60 let tt' = normalise ctxt env tt
61 isSet ctxt env tt'
62 return (Pi tv')
63 checkBinder (Let t v)
64 = do (tv, tt) <- check ctxt env t
65 (vv, vt) <- check ctxt env v
66 let tv' = normalise ctxt env tv
67 let tt' = normalise ctxt env tt
68 converts ctxt env tv vt
69 isSet ctxt env tt'
70 return (Let tv' vv)
71 checkBinder (NLet t v)
72 = do (tv, tt) <- check ctxt env t
73 (vv, vt) <- check ctxt env v
74 let tv' = normalise ctxt env tv
75 let tt' = normalise ctxt env tt
76 converts ctxt env tv vt
77 isSet ctxt env tt'
78 return (NLet tv' vv)
79 checkBinder (Hole t)
80 = do (tv, tt) <- check ctxt env t
81 let tv' = normalise ctxt env tv
82 let tt' = normalise ctxt env tt
83 isSet ctxt env tt'
84 return (Hole tv')
85 checkBinder (Guess t v)
86 = do (tv, tt) <- check ctxt env t
87 (vv, vt) <- check ctxt env v
88 let tv' = normalise ctxt env tv
89 let tt' = normalise ctxt env tt
90 converts ctxt env tv vt
91 isSet ctxt env tt'
92 return (Guess tv' vv)
93 checkBinder (PVar t)
94 = do (tv, tt) <- check ctxt env t
95 let tv' = normalise ctxt env tv
96 let tt' = normalise ctxt env tt
97 isSet ctxt env tt'
98 return (PVar tv')
100 discharge n (Lam t) scv sct
101 = return (Bind n (Lam t) scv, Bind n (Pi t) sct)
102 discharge n (Pi t) scv sct
103 = return (Bind n (Pi t) scv, sct)
104 discharge n (Let t v) scv sct
105 = return (Bind n (Let t v) scv, Bind n (Let t v) sct)
106 discharge n (NLet t v) scv sct
107 = return (Bind n (NLet t v) scv, Bind n (Let t v) sct)
108 discharge n (Hole t) scv sct
109 = do -- A hole can't appear in the type of its scope
110 checkNotHoley 0 sct
111 return (Bind n (Hole t) scv, sct)
112 discharge n (Guess t v) scv sct
113 = do -- A hole can't appear in the type of its scope
114 checkNotHoley 0 sct
115 return (Bind n (Guess t v) scv, sct)
116 discharge n (PVar t) scv sct
117 = return (Bind n (PVar t) scv, sct)
119 checkNotHoley i (V v)
120 | v == i = fail "You can't put a hole where a hole don't belong"
121 checkNotHoley i (App f a) = do checkNotHoley i f
122 checkNotHoley i a
123 checkNotHoley i (Bind n b sc) = checkNotHoley (i+1) sc
124 checkNotHoley _ _ = return ()
126pToV :: Eq n => n -> TT n -> TT n
127pToV n = pToV' 0 where
128 pToV' i (P _ x _) | n == x = V i
129 pToV' i (Bind x b sc)
130 | n == x = Bind x (fmap (pToV' i) b) sc
131 | otherwise = Bind x (fmap (pToV' i) b) (pToV' (i+1) sc)
132 pToV' i (App f a) = App (pToV' i f) (pToV' i a)
133 pToV' i t = t
135vToP :: TT n -> TT n
136vToP = vToP' [] where
137 vToP' env (V i) = let (n, b) = (env !! i) in
138 P Bound n (binderTy b)
139 vToP' env (Bind n b sc) = let b' = fmap (vToP' env) b in
140 Bind n b' (vToP' ((n, b'):env) sc)
141 vToP' env (App f a) = App (vToP' env f) (vToP' env a)
142 vToP' env t = t
144instantiate :: TT n -> TT n -> TT n
145instantiate e = subst 0 where
146 subst i (V x) | i == x = e
147 subst i (Bind x b sc) = Bind x (fmap (subst i) b) (subst (i+1) sc)
148 subst i (App f a) = App (subst i f) (subst i a)
149 subst i t = t
151finalise :: Eq n => TT n -> TT n
152finalise (Bind x b sc) = Bind x (fmap finalise b) (pToV x (finalise sc))
153finalise (App f a) = App (finalise f) (finalise a)
154finalise t = t
156checkProgram :: Context -> RProgram -> TC Context
157checkProgram ctxt [] = return ctxt
158checkProgram ctxt ((n, RConst t) : xs)
159 = do (t', tt') <- trace (show n) $ check ctxt [] t
160 isSet ctxt [] tt'
161 checkProgram (addConstant n t' ctxt) xs
162checkProgram ctxt ((n, RFunction (RawFun ty val)) : xs)
163 = do (ty', tyt') <- trace (show n) $ check ctxt [] ty
164 (val', valt') <- check ctxt [] val
165 isSet ctxt [] tyt'
166 converts ctxt [] ty' valt'
167 checkProgram (addToCtxt n val' ty' ctxt) xs
168checkProgram ctxt ((n, RData (RDatatype _ ty cons)) : xs)
169 = do (ty', tyt') <- trace (show n) $ check ctxt [] ty
170 isSet ctxt [] tyt'
171 -- add the tycon temporarily so we can check constructors
172 let ctxt' = addDatatype (Data n ty' []) ctxt
173 cons' <- mapM (checkCon ctxt') cons
174 checkProgram (addDatatype (Data n ty' cons') ctxt) xs
175 where checkCon ctxt (n, cty) = do (cty', ctyt') <- check ctxt [] cty
176 return (n, cty')