git.iko.soy/Idris-dev
on ccd64c7 help sign in
Idris-dev/src/Typecheck.hs
140 lines 5.2 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
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 Show
15-- at some point, this instance should also carry type checking options
16-- (e.g. Set:Set)
18instance Monad TC where
19 return = OK
20 x >>= k = case x of
21 OK v -> k v
22 Error e -> Error e
23 fail = Error
25instance MonadPlus TC where
26 mzero = Error "Unknown error"
27 (OK x) `mplus` _ = OK x
28 _ `mplus` (OK y) = OK y
29 err `mplus` _ = err
31converts :: Context -> Env -> Term -> Term -> TC ()
32converts ctxt env x y = if (normalise ctxt env (bindEnv env x) ==
33 normalise ctxt env (bindEnv env y))
34 then return ()
35 else fail ("Can't convert between " ++
36 show x ++ " and " ++ show y)
38isSet :: Term -> TC ()
39isSet (Set _) = return ()
40isSet tm = fail (show tm ++ " is not a Set")
42check :: Context -> Env -> Raw -> TC (Term, Type)
43check ctxt env (Var n)
44 | Just (i, ty) <- lookupTyEnv n env = return (V i, ty)
45 | Just (P nt n' ty) <- lookupP n ctxt = return (P nt n' ty, ty)
46 | otherwise = do fail $ "No such variable " ++ show n
47check ctxt env (RApp f a)
48 = do (fv, fty) <- check ctxt env f
49 (av, aty) <- check ctxt env a
50 let fty' = normalise ctxt env fty
51 case fty' of
52 Bind x (Pi s) t ->
53 do converts ctxt env s aty
54 return (App fv fty av,
55 normalise ctxt env (Bind x (Let av aty) t))
56 t -> fail "Can't apply a non-function type"
57check ctxt env (RSet i) = return (Set i, Set (i+1))
58check ctxt env (RBind n b sc)
59 = do b' <- checkBinder b
60 (scv, sct) <- check ctxt ((n, b'):env) sc
61 discharge n b' scv sct
62 where checkBinder (Lam t)
63 = do (tv, tt) <- check ctxt env t
64 let tv' = normalise ctxt env tv
65 let tt' = normalise ctxt env tt
66 isSet tt'
67 return (Lam tv')
68 checkBinder (Pi t)
69 = do (tv, tt) <- check ctxt env t
70 let tv' = normalise ctxt env tv
71 let tt' = normalise ctxt env tt
72 isSet tt'
73 return (Pi tv')
74 checkBinder (Let 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 tt'
81 return (Let 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 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 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 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 (Hole t) scv sct
110 = do -- A hole can't appear in the type of its scope
111 checkNotHoley 0 sct
112 return (Bind n (Hole t) scv, sct)
113 discharge n (Guess t v) scv sct
114 = do -- A hole can't appear in the type of its scope
115 checkNotHoley 0 sct
116 return (Bind n (Guess t v) scv, sct)
117 discharge n (PVar t) scv sct
118 = return (Bind n (PVar t) scv, sct)
120 checkNotHoley i (V v)
121 | v == i = fail "You can't put a hole where a hole don't belong"
122 checkNotHoley i (App f t a) = do checkNotHoley i f
123 checkNotHoley i t
124 checkNotHoley i a
125 checkNotHoley i (Bind n b sc) = checkNotHoley (i+1) sc
126 checkNotHoley _ _ = return ()
128checkProgram :: Context -> RProgram -> TC Context
129checkProgram ctxt [] = return ctxt
130checkProgram ctxt ((n, RConst t):xs)
131 = do (t', tt') <- trace (show n) $ check ctxt [] t
132 isSet tt'
133 checkProgram ((n, Constant Ref t' (hoas [] t')):ctxt) xs
134checkProgram ctxt ((n, RFunction (RawFun ty val)):xs)
135 = do (ty', tyt') <- trace (show n) $ check ctxt [] ty
136 (val', valt') <- check ctxt [] val
137 isSet tyt'
138 converts ctxt [] ty' valt'
139 checkProgram ((n, Function (Fun ty' (hoas [] ty')
140 val' (hoas [] val'))):ctxt) xs