git.iko.soy/Idris-dev
on df5bf81 help sign in
Idris-dev/src/Core/Unify.hs
302 lines 13 kB history raw
1{-# LANGUAGE PatternGuards #-}
3module Core.Unify(unify, Fails) where
5import Core.TT
6import Core.Evaluate
8import Control.Monad
9import Control.Monad.State
10import Debug.Trace
12-- Unification is applied inside the theorem prover. We're looking for holes
13-- which can be filled in, by matching one term's normal form against another.
14-- Returns a list of hole names paired with the term which solves them, and
15-- a list of things which need to be injective.
17-- terms which need to be injective, with the things we're trying to unify
18-- at the time
20type Injs = [(TT Name, TT Name, TT Name)]
21type Fails = [(TT Name, TT Name, Env, Err)]
23data UInfo = UI Int Fails
24 deriving Show
26data UResult a = UOK a
27 | UPartOK a
28 | UFail Err
30unify :: Context -> Env -> TT Name -> TT Name -> [Name] -> [Name] ->
31 TC ([(Name, TT Name)], Fails)
32unify ctxt env topx topy injtc holes =
33-- trace ("Unifying " ++ show (topx, topy)) $
34 -- don't bother if topx and topy are different at the head
35 case runStateT (un False [] topx topy) (UI 0 []) of
36 OK (v, UI _ []) -> return (filter notTrivial v, [])
37 res ->
38 let topxn = normalise ctxt env topx
39 topyn = normalise ctxt env topy in
40-- trace ("Unifying " ++ show (topx, topy) ++ "\n\n==>\n" ++ show (topxn, topyn) ++ "\n\n" ++ show res ++ "\n\n") $
41 case runStateT (un False [] topxn topyn)
42 (UI 0 []) of
43 OK (v, UI _ fails) ->
44 return (filter notTrivial v, reverse fails)
45-- Error e@(CantUnify False _ _ _ _ _) -> tfail e
46 Error e -> tfail e
47 where
48 notTrivial (x, P _ x' _) = x /= x'
49 notTrivial _ = True
51 headDiff (P (DCon _ _) x _) (P (DCon _ _) y _) = x /= y
52 headDiff (P (TCon _ _) x _) (P (TCon _ _) y _) = x /= y
53 headDiff _ _ = False
55 injective (P (DCon _ _) _ _) = True
56 injective (P (TCon _ _) _ _) = True
57 injective (P _ n _) = n `elem` injtc
58 injective (App f a) = injective f
59 injective _ = False
61 notP (P _ _ _) = False
62 notP _ = True
64 sc i = do UI s f <- get
65 put (UI (s+i) f)
67 uplus u1 u2 = do UI s f <- get
68 r <- u1
69 UI s f' <- get
70 if (length f == length f')
71 then return r
72 else do put (UI s f); u2
74 un :: Bool -> [(Name, Name)] -> TT Name -> TT Name ->
75 StateT UInfo
76 TC [(Name, TT Name)]
77 un = un'
78-- un fn names x y
79-- = let (xf, _) = unApply x
80-- (yf, _) = unApply y in
81-- if headDiff xf yf then unifyFail x y else
82-- uplus (un' fn names x y)
83-- (un' fn names (hnf ctxt env x) (hnf ctxt env y))
85 un' :: Bool -> [(Name, Name)] -> TT Name -> TT Name ->
86 StateT UInfo
87 TC [(Name, TT Name)]
88 un' fn names x y | x == y = return [] -- shortcut
89 un' fn names topx@(P (DCon _ _) x _) topy@(P (DCon _ _) y _)
90 | x /= y = unifyFail topx topy
91 un' fn names topx@(P (TCon _ _) x _) topy@(P (TCon _ _) y _)
92 | x /= y = unifyFail topx topy
93 un' fn names topx@(P (DCon _ _) x _) topy@(P (TCon _ _) y _)
94 = unifyFail topx topy
95 un' fn names topx@(P (TCon _ _) x _) topy@(P (DCon _ _) y _)
96 = unifyFail topx topy
97 un' fn bnames tx@(P _ x _) ty@(P _ y _)
98 | (x,y) `elem` bnames || x == y = do sc 1; return []
99 | injective tx && not (holeIn env y || y `elem` holes)
100 = unifyFail tx ty
101 | injective ty && not (holeIn env x || x `elem` holes)
102 = unifyFail tx ty
103 un' fn bnames xtm@(P _ x _) tm
104 | holeIn env x || x `elem` holes
105 = do UI s f <- get
106 -- injectivity check
107 if (notP tm && fn)
108-- trace (show (x, tm, normalise ctxt env tm)) $
109-- put (UI s ((tm, topx, topy) : i) f)
110 then unifyTmpFail xtm tm
111 else do sc 1
112 checkCycle (x, tm)
113 | not (injective xtm) && injective tm = unifyFail xtm tm
114 un' fn bnames tm ytm@(P _ y _)
115 | holeIn env y || y `elem` holes
116 = do UI s f <- get
117 -- injectivity check
118 if (notP tm && fn)
119-- trace (show (y, tm, normalise ctxt env tm)) $
120-- put (UI s ((tm, topx, topy) : i) f)
121 then unifyTmpFail tm ytm
122 else do sc 1
123 checkCycle (y, tm)
124 | not (injective ytm) && injective tm = unifyFail ytm tm
125 un' fn bnames (V i) (P _ x _)
126 | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []
127 un' fn bnames (P _ x _) (V i)
128 | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []
130 un' fn bnames appx@(App fx ax) appy@(App fy ay)
131 | injective fx && metavarApp appy
132 || injective fy && metavarApp appx
133 || injective fx && injective fy
134 || fx == fy
135 = do let (headx, _) = unApply fx
136 let (heady, _) = unApply fy
137 -- fail quickly if the heads are disjoint
138 checkHeads headx heady
139-- if True then -- (injective fx || injective fy || fx == fy) then
140-- if (injective fx && metavarApp appy) ||
141-- (injective fy && metavarApp appx) ||
142-- (injective fx && injective fy) || fx == fy
143 uplus
144 (do hf <- un' True bnames fx fy
145 let ax' = hnormalise hf ctxt env (substNames hf ax)
146 let ay' = hnormalise hf ctxt env (substNames hf ay)
147 ha <- un' False bnames ax' ay'
148 sc 1
149 combine bnames hf ha)
150 (do ha <- un' False bnames ax ay
151 let fx' = hnormalise ha ctxt env (substNames ha fx)
152 let fy' = hnormalise ha ctxt env (substNames ha fy)
153 hf <- un' False bnames fx' fy'
154 sc 1
155 combine bnames hf ha)
156 | otherwise
157 = do let (headx, argsx) = unApply appx
158 let (heady, argsy) = unApply appy
159 if (length argsx == length argsy &&
160 ((headx == heady) || (argsx == argsy) ||
161 (notFn headx && notFn heady))) then
162 do uf <- un' True bnames headx heady
163 unArgs uf argsx argsy
164 else unifyTmpFail appx appy
165 where hnormalise [] _ _ t = t
166 hnormalise ns ctxt env t = hnf ctxt env t
167 checkHeads (P (DCon _ _) x _) (P (DCon _ _) y _)
168 | x /= y = unifyFail appx appy
169 checkHeads (P (TCon _ _) x _) (P (TCon _ _) y _)
170 | x /= y = unifyFail appx appy
171 checkHeads (P (DCon _ _) x _) (P (TCon _ _) y _)
172 = unifyFail appx appy
173 checkHeads (P (TCon _ _) x _) (P (DCon _ _) y _)
174 = unifyFail appx appy
175 checkHeads _ _ = return []
177 unArgs as [] [] = return as
178 unArgs as (x : xs) (y : ys)
179 = do let x' = hnormalise as ctxt env (substNames as x)
180 let y' = hnormalise as ctxt env (substNames as y)
181 as' <- un' False bnames x' y'
182 vs <- combine bnames as as'
183 unArgs vs xs ys
185 metavarApp tm = let (f, args) = unApply tm in
186 all (\x -> metavar x || notFn x) (f : args)
187 metavar t = case t of
188 P _ x _ -> x `elem` holes || holeIn env x
189 _ -> False
190 inenv t = case t of
191 P _ x _ -> x `elem` (map fst env)
192 _ -> False
194 notFn t = injective t || metavar t || inenv t
196 un' fn bnames x (Bind n (Lam t) (App y (P Bound n' _)))
197 | n == n' = un' False bnames x y
198 un' fn bnames (Bind n (Lam t) (App x (P Bound n' _))) y
199 | n == n' = un' False bnames x y
200-- un' fn bnames (Bind x (PVar _) sx) (Bind y (PVar _) sy)
201-- = un' False ((x,y):bnames) sx sy
202-- un' fn bnames (Bind x (PVTy _) sx) (Bind y (PVTy _) sy)
203-- = un' False ((x,y):bnames) sx sy
204 un' fn bnames (Bind x bx sx) (Bind y by sy)
205 = do h1 <- uB bnames bx by
206 h2 <- un' False ((x,y):bnames) sx sy
207 combine bnames h1 h2
208 un' fn bnames x y
209 | OK True <- convEq' ctxt x y = do sc 1; return []
210 | otherwise = do UI s f <- get
211 let r = recoverable x y
212 let err = CantUnify r
213 topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s
214 if (not r) then lift $ tfail err
215 else do put (UI s ((x, y, env, err) : f))
216 return [] -- lift $ tfail err
218 unifyTmpFail x y
219 = do UI s f <- get
220 let r = recoverable x y
221 let err = CantUnify r
222 topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s
223 put (UI s ((x, y, env, err) : f))
224 return []
226 -- shortcut failure, if we *know* nothing can fix it
227 unifyFail x y = do UI s f <- get
228 let r = recoverable x y
229 let err = CantUnify r
230 topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s
231 put (UI s ((x, y, env, err) : f))
232 lift $ tfail err
235 uB bnames (Let tx vx) (Let ty vy)
236 = do h1 <- un' False bnames tx ty
237 h2 <- un' False bnames ty vy
238 sc 1
239 combine bnames h1 h2
240 uB bnames (Guess tx vx) (Guess ty vy)
241 = do h1 <- un' False bnames tx ty
242 h2 <- un' False bnames ty vy
243 sc 1
244 combine bnames h1 h2
245 uB bnames (Lam tx) (Lam ty) = do sc 1; un' False bnames tx ty
246 uB bnames (Pi tx) (Pi ty) = do sc 1; un' False bnames tx ty
247 uB bnames (Hole tx) (Hole ty) = un' False bnames tx ty
248 uB bnames (PVar tx) (PVar ty) = un' False bnames tx ty
249 uB bnames x y = do UI s f <- get
250 let r = recoverable (binderTy x) (binderTy y)
251 let err = CantUnify r topx topy
252 (CantUnify r (binderTy x) (binderTy y) (Msg "") [] s)
253 (errEnv env) s
254 put (UI s ((binderTy x, binderTy y, env, err) : f))
255 return [] -- lift $ tfail err
257 checkCycle p@(x, P _ _ _) = return [p]
258 checkCycle (x, tm)
259 | not (x `elem` freeNames tm) = return [(x, tm)]
260 | otherwise = lift $ tfail (InfiniteUnify x tm (errEnv env))
262 combineArgs bnames args = ca [] args where
263 ca acc [] = return acc
264 ca acc (x : xs) = do x' <- combine bnames acc x
265 ca x' xs
267 combine bnames as [] = return as
268 combine bnames as ((n, t) : bs)
269 = case lookup n as of
270 Nothing -> combine bnames (as ++ [(n,t)]) bs
271 Just t' -> do ns <- un' False bnames t t'
272 -- make sure there's n mapping from n in ns
273 let ns' = filter (\ (x, _) -> x/=n) ns
274 sc 1
275 combine bnames as (ns' ++ bs)
277 -- If there are any clashes of constructors, deem it unrecoverable, otherwise some
278 -- more work may help.
279 -- FIXME: Depending on how overloading gets used, this may cause problems. Better
280 -- rethink overloading properly...
282 recoverable (P (DCon _ _) x _) (P (DCon _ _) y _)
283 | x == y = True
284 | otherwise = False
285 recoverable (P (TCon _ _) x _) (P (TCon _ _) y _)
286 | x == y = True
287 | otherwise = False
288 recoverable (P (DCon _ _) x _) (P (TCon _ _) y _) = False
289 recoverable (P (TCon _ _) x _) (P (DCon _ _) y _) = False
290 recoverable p@(P _ n _) (App f a) = recoverable p f
291-- recoverable (App f a) p@(P _ _ _) = recoverable f p
292 recoverable (App f a) (App f' a')
293 = recoverable f f' -- && recoverable a a'
294 recoverable _ _ = True
296errEnv = map (\(x, b) -> (x, binderTy b))
298holeIn :: Env -> Name -> Bool
299holeIn env n = case lookup n env of
300 Just (Hole _) -> True
301 _ -> False