git.iko.soy/Idris-dev
on 86e32fb help sign in
Idris-dev/src/Core/Unify.hs
526 lines 23 kB history raw
1{-# LANGUAGE PatternGuards #-}
3module Core.Unify(match_unify, unify, Fails) where
5import Core.TT
6import Core.Evaluate
8import Control.Monad
9import Control.Monad.State
10import Data.List
11import Debug.Trace
13-- Unification is applied inside the theorem prover. We're looking for holes
14-- which can be filled in, by matching one term's normal form against another.
15-- Returns a list of hole names paired with the term which solves them, and
16-- a list of things which need to be injective.
18-- terms which need to be injective, with the things we're trying to unify
19-- at the time
21type Injs = [(TT Name, TT Name, TT Name)]
22type Fails = [(TT Name, TT Name, Env, Err)]
24data UInfo = UI Int Fails
25 deriving Show
27data UResult a = UOK a
28 | UPartOK a
29 | UFail Err
31-- Solve metavariables by matching terms against each other
32-- Not really unification, of course!
34match_unify :: Context -> Env -> TT Name -> TT Name -> [Name] -> [Name] ->
35 TC [(Name, TT Name)]
36match_unify ctxt env topx topy dont holes =
37 case runStateT (un [] topx topy) (UI 0 []) of
38 OK (v, UI _ []) -> return (filter notTrivial v)
39 res ->
40 let topxn = normalise ctxt env topx
41 topyn = normalise ctxt env topy in
42 case runStateT (un [] topxn topyn)
43 (UI 0 []) of
44 OK (v, UI _ fails) ->
45 return (filter notTrivial v)
46 Error e ->
47 -- just normalise the term we're matching against
48 case runStateT (un [] topxn topy)
49 (UI 0 []) of
50 OK (v, UI _ fails) ->
51 return (filter notTrivial v)
52 _ -> tfail e
53 where
54 un names (P _ x _) tm
55 | holeIn env x || x `elem` holes
56 = do sc 1; checkCycle names (x, tm)
57 un names tm (P _ y _)
58 | holeIn env y || y `elem` holes
59 = do sc 1; checkCycle names (y, tm)
60 un bnames (V i) (P _ x _)
61 | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []
62 un bnames (P _ x _) (V i)
63 | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []
64 un bnames (Bind x bx sx) (Bind y by sy)
65 = do h1 <- uB bnames bx by
66 h2 <- un ((x, y) : bnames) sx sy
67 combine bnames h1 h2
68 un names (App fx ax) (App fy ay)
69 = do hf <- un names fx fy
70 ha <- un names ax ay
71 combine names hf ha
72 un names x y
73 | OK True <- convEq' ctxt x y = do sc 1; return []
74 | otherwise = do UI s f <- get
75 let r = recoverable x y
76 let err = CantUnify r
77 topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s
78 if (not r) then lift $ tfail err
79 else do put (UI s ((x, y, env, err) : f))
80 lift $ tfail err
83 uB bnames (Let tx vx) (Let ty vy) = do h1 <- un bnames tx ty
84 h2 <- un bnames vx vy
85 combine bnames h1 h2
86 uB bnames (Lam tx) (Lam ty) = un bnames tx ty
87 uB bnames (Pi tx) (Pi ty) = un bnames tx ty
88 uB bnames x y = do UI s f <- get
89 let r = recoverable (binderTy x) (binderTy y)
90 let err = CantUnify r topx topy
91 (CantUnify r (binderTy x) (binderTy y) (Msg "") [] s)
92 (errEnv env) s
93 put (UI s ((binderTy x, binderTy y, env, err) : f))
94 return []
96 -- TODO: there's an annoying amount of repetition between this and the
97 -- main unification function. Consider lifting it out.
99 sc i = do UI s f <- get
100 put (UI (s+i) f)
102 unifyFail x y = do UI s f <- get
103 let r = recoverable x y
104 let err = CantUnify r
105 topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s
106 put (UI s ((x, y, env, err) : f))
107 lift $ tfail err
108 combine bnames as [] = return as
109 combine bnames as ((n, t) : bs)
110 = case lookup n as of
111 Nothing -> combine bnames (as ++ [(n,t)]) bs
112 Just t' -> do ns <- un bnames t t'
113 -- make sure there's n mapping from n in ns
114 let ns' = filter (\ (x, _) -> x/=n) ns
115 sc 1
116 combine bnames as (ns' ++ bs)
118 checkCycle ns p@(x, P _ _ _) = return [p]
119 checkCycle ns (x, tm)
120 | not (x `elem` freeNames tm) = checkScope ns (x, tm)
121 | otherwise = lift $ tfail (InfiniteUnify x tm (errEnv env))
123 checkScope ns (x, tm) =
124 case boundVs (envPos x 0 env) tm of
125 [] -> return [(x, tm)]
126 (i:_) -> lift $ tfail (UnifyScope x (fst (ns!!i))
127 (inst ns tm) (errEnv env))
128 where inst [] tm = tm
129 inst ((n, _) : ns) tm = inst ns (substV (P Bound n Erased) tm)
131notTrivial (x, P _ x' _) = x /= x'
132notTrivial _ = True
134expandLets env (x, tm) = (x, doSubst (reverse env) tm)
135 where
136 doSubst [] tm = tm
137 doSubst ((n, Let v t) : env) tm
138 = doSubst env (subst n v tm)
139 doSubst (_ : env) tm
140 = doSubst env tm
143unify :: Context -> Env -> TT Name -> TT Name -> [Name] -> [Name] ->
144 TC ([(Name, TT Name)], Fails)
145unify ctxt env topx topy dont holes =
146-- trace ("Unifying " ++ show (topx, topy)) $
147 -- don't bother if topx and topy are different at the head
148 case runStateT (un False [] topx topy) (UI 0 []) of
149 OK (v, UI _ []) -> return (filter notTrivial v,
150 [])
151 res ->
152 let topxn = normalise ctxt env topx
153 topyn = normalise ctxt env topy in
154-- trace ("Unifying " ++ show (topx, topy) ++ "\n\n==>\n" ++ show (topxn, topyn) ++ "\n\n" ++ show res ++ "\n\n") $
155 case runStateT (un False [] topxn topyn)
156 (UI 0 []) of
157 OK (v, UI _ fails) ->
158 return (filter notTrivial v, reverse fails)
159-- Error e@(CantUnify False _ _ _ _ _) -> tfail e
160 Error e -> tfail e
161 where
162 headDiff (P (DCon _ _) x _) (P (DCon _ _) y _) = x /= y
163 headDiff (P (TCon _ _) x _) (P (TCon _ _) y _) = x /= y
164 headDiff _ _ = False
166 injective (P (DCon _ _) _ _) = True
167 injective (P (TCon _ _) _ _) = True
168-- injective (App f (P _ _ _)) = injective f
169-- injective (App f (Constant _)) = injective f
170 injective (App f a) = injective f -- && injective a
171 injective _ = False
173 notP (P _ _ _) = False
174 notP _ = True
176 sc i = do UI s f <- get
177 put (UI (s+i) f)
179 errors = do UI s f <- get
180 return (not (null f))
182 uplus u1 u2 = do UI s f <- get
183 r <- u1
184 UI s f' <- get
185 if (length f == length f')
186 then return r
187 else do put (UI s f); u2
189 un :: Bool -> [(Name, Name)] -> TT Name -> TT Name ->
190 StateT UInfo
191 TC [(Name, TT Name)]
192 un = un'
193-- un fn names x y
194-- = let (xf, _) = unApply x
195-- (yf, _) = unApply y in
196-- if headDiff xf yf then unifyFail x y else
197-- uplus (un' fn names x y)
198-- (un' fn names (hnf ctxt env x) (hnf ctxt env y))
200 un' :: Bool -> [(Name, Name)] -> TT Name -> TT Name ->
201 StateT UInfo
202 TC [(Name, TT Name)]
203 un' fn names x y | x == y = return [] -- shortcut
204 un' fn names topx@(P (DCon _ _) x _) topy@(P (DCon _ _) y _)
205 | x /= y = unifyFail topx topy
206 un' fn names topx@(P (TCon _ _) x _) topy@(P (TCon _ _) y _)
207 | x /= y = unifyFail topx topy
208 un' fn names topx@(P (DCon _ _) x _) topy@(P (TCon _ _) y _)
209 = unifyFail topx topy
210 un' fn names topx@(P (TCon _ _) x _) topy@(P (DCon _ _) y _)
211 = unifyFail topx topy
212 un' fn names topx@(Constant _) topy@(P (TCon _ _) y _)
213 = unifyFail topx topy
214 un' fn names topx@(P (TCon _ _) x _) topy@(Constant _)
215 = unifyFail topx topy
216 un' fn bnames tx@(P _ x _) ty@(P _ y _)
217 | (x,y) `elem` bnames || x == y = do sc 1; return []
218 | injective tx && not (holeIn env y || y `elem` holes)
219 = unifyTmpFail tx ty
220 | injective ty && not (holeIn env x || x `elem` holes)
221 = unifyTmpFail tx ty
222 un' fn bnames xtm@(P _ x _) tm
223 | holeIn env x || x `elem` holes
224 = do UI s f <- get
225 -- injectivity check
226 if (notP tm && fn)
227-- trace (show (x, tm, normalise ctxt env tm)) $
228-- put (UI s ((tm, topx, topy) : i) f)
229 then unifyTmpFail xtm tm
230 else do sc 1
231 checkCycle bnames (x, tm)
232 | not (injective xtm) && injective tm = unifyFail xtm tm
233 un' fn bnames tm ytm@(P _ y _)
234 | holeIn env y || y `elem` holes
235 = do UI s f <- get
236 -- injectivity check
237 if (notP tm && fn)
238-- trace (show (y, tm, normalise ctxt env tm)) $
239-- put (UI s ((tm, topx, topy) : i) f)
240 then unifyTmpFail tm ytm
241 else do sc 1
242 checkCycle bnames (y, tm)
243 | not (injective ytm) && injective tm = unifyFail ytm tm
244 un' fn bnames (V i) (P _ x _)
245 | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []
246 un' fn bnames (P _ x _) (V i)
247 | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []
249 un' fn bnames appx@(App _ _) appy@(App _ _)
250 = unApp fn bnames appx appy
251-- = uplus (unApp fn bnames appx appy)
252-- (unifyTmpFail appx appy) -- take the whole lot
254 un' fn bnames x (Bind n (Lam t) (App y (P Bound n' _)))
255 | n == n' = un' False bnames x y
256 un' fn bnames (Bind n (Lam t) (App x (P Bound n' _))) y
257 | n == n' = un' False bnames x y
258 un' fn bnames x (Bind n (Lam t) (App y (V 0)))
259 = un' False bnames x y
260 un' fn bnames (Bind n (Lam t) (App x (V 0))) y
261 = un' False bnames x y
262-- un' fn bnames (Bind x (PVar _) sx) (Bind y (PVar _) sy)
263-- = un' False ((x,y):bnames) sx sy
264-- un' fn bnames (Bind x (PVTy _) sx) (Bind y (PVTy _) sy)
265-- = un' False ((x,y):bnames) sx sy
267 -- f D unifies with t -> D. This is dubious, but it helps with type
268 -- class resolution for type classes over functions.
270 un' fn bnames (App f x) (Bind n (Pi t) y)
271 | noOccurrence n y && x == y
272 = un' False bnames f (Bind (MN 0 "uv") (Lam (TType (UVar 0)))
273 (Bind n (Pi t) (V 1)))
275 un' fn bnames (Bind x bx sx) (Bind y by sy)
276 = do h1 <- uB bnames bx by
277 h2 <- un' False ((x,y):bnames) sx sy
278 combine bnames h1 h2
279 un' fn bnames x y
280 | OK True <- convEq' ctxt x y = do sc 1; return []
281 | otherwise = do UI s f <- get
282 let r = recoverable x y
283 let err = CantUnify r
284 topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s
285 if (not r) then lift $ tfail err
286 else do put (UI s ((x, y, env, err) : f))
287 return [] -- lift $ tfail err
289 unApp fn bnames appx@(App fx ax) appy@(App fy ay)
290 | (injective fx && injective fy)
291 || (injective fx && rigid appx && metavarApp appy)
292 || (injective fy && rigid appy && metavarApp appx)
293 || (injective fx && metavarApp fy && ax == ay)
294 || (injective fy && metavarApp fx && ax == ay)
295 = do let (headx, _) = unApply fx
296 let (heady, _) = unApply fy
297 -- fail quickly if the heads are disjoint
298 checkHeads headx heady
299-- if True then -- (injective fx || injective fy || fx == fy) then
300-- if (injective fx && metavarApp appy) ||
301-- (injective fy && metavarApp appx) ||
302-- (injective fx && injective fy) || fx == fy
303 uplus
304 (do hf <- un' True bnames fx fy
305 let ax' = hnormalise hf ctxt env (substNames hf ax)
306 let ay' = hnormalise hf ctxt env (substNames hf ay)
307 ha <- un' False bnames ax' ay'
308 sc 1
309 combine bnames hf ha)
310 (do ha <- un' False bnames ax ay
311 let fx' = hnormalise ha ctxt env (substNames ha fx)
312 let fy' = hnormalise ha ctxt env (substNames ha fy)
313 hf <- un' False bnames fx' fy'
314 sc 1
315 combine bnames hf ha)
316 | otherwise = -- trace (show (appx, appy, injective fx, metavarApp appy, sameArgStruct appx appy)) $
317 do let (headx, argsx) = unApply appx
318 let (heady, argsy) = unApply appy
319 -- traceWhen (headx == heady) (show (appx, appy)) $
320 uplus (
321 if (length argsx == length argsy &&
322 ((headx == heady && inenv headx) || (argsx == argsy) ||
323 (and (zipWith sameStruct (headx:argsx) (heady:argsy)))))
324 then
325-- (notFn headx && notFn heady))) then
326 do uf <- un' True bnames headx heady
327 failed <- errors
328 if (not failed) then unArgs uf argsx argsy
329 else return []
330 else -- trace ("TMPFAIL " ++ show (appx, appy, injective appx, injective appy)) $
331 unifyTmpFail appx appy)
332 (unifyTmpFail appx appy) -- whole application fails
333 where hnormalise [] _ _ t = t
334 hnormalise ns ctxt env t = normalise ctxt env t
335 checkHeads (P (DCon _ _) x _) (P (DCon _ _) y _)
336 | x /= y = unifyFail appx appy
337 checkHeads (P (TCon _ _) x _) (P (TCon _ _) y _)
338 | x /= y = unifyFail appx appy
339 checkHeads (P (DCon _ _) x _) (P (TCon _ _) y _)
340 = unifyFail appx appy
341 checkHeads (P (TCon _ _) x _) (P (DCon _ _) y _)
342 = unifyFail appx appy
343 checkHeads _ _ = return []
345 unArgs as [] [] = return as
346 unArgs as (x : xs) (y : ys)
347 = do let x' = hnormalise as ctxt env (substNames as x)
348 let y' = hnormalise as ctxt env (substNames as y)
349 as' <- un' False bnames x' y'
350 vs <- combine bnames as as'
351 unArgs vs xs ys
353 metavarApp tm = let (f, args) = unApply tm in
354 metavar f &&
355 all (\x -> metavarApp x) args
356 && nub args == args
357 metavarArgs tm = let (f, args) = unApply tm in
358 all (\x -> metavar x || inenv x) args
359 && nub args == args
360 metavarApp' tm = let (f, args) = unApply tm in
361 all (\x -> pat x || metavar x) (f : args)
362 && nub args == args
364 sameArgStruct appx appy
365 = let (_, ax) = unApply appx
366 (_, ay) = unApply appy in
367 length ax == length ay &&
368 and (zipWith sameStruct ax ay)
370 sameStruct fapp@(App f x) gapp@(App g y)
371 = let (f',a') = unApply fapp
372 (g',b') = unApply gapp in
373 (f' == g' && length a' == length b' &&
374 (injective f' || injective g'))
375 || (sameStruct f g && sameStruct x y)
376 sameStruct (P _ x _) (P _ y _) = True
377 sameStruct (V i) (V j) = i == j
378 sameStruct (Constant x) (Constant y) = True
379 sameStruct (P _ _ _) (Constant y) = True
380 sameStruct (Constant x) (P _ _ _) = True
381 sameStruct (Bind n t sc) (P _ _ _) = True
382 sameStruct (P _ _ _) (Bind n t sc) = True
383 sameStruct (Bind n t sc) (Bind n' t' sc') = sameStruct sc sc'
384 sameStruct _ _ = False
386 rigid (P (DCon _ _) _ _) = True
387 rigid (P (TCon _ _) _ _) = True
388 rigid t@(P Ref _ _) = inenv t
389 rigid (Constant _) = True
390 rigid (App f a) = rigid f && rigid a
391 rigid t = not (metavar t)
393 metavar t = case t of
394 P _ x _ -> (x `elem` holes || holeIn env x) &&
395 not (x `elem` dont)
396 _ -> False
397 pat t = case t of
398 P _ x _ -> x `elem` holes || patIn env x
399 _ -> False
400 inenv t = case t of
401 P _ x _ -> x `elem` (map fst env)
402 _ -> False
404 notFn t = injective t || metavar t || inenv t
407 unifyTmpFail x y
408 = do UI s f <- get
409 let r = recoverable x y
410 let err = CantUnify r
411 topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s
412 put (UI s ((topx, topy, env, err) : f))
413 return []
415 -- shortcut failure, if we *know* nothing can fix it
416 unifyFail x y = do UI s f <- get
417 let r = recoverable x y
418 let err = CantUnify r
419 topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s
420 put (UI s ((topx, topy, env, err) : f))
421 lift $ tfail err
424 uB bnames (Let tx vx) (Let ty vy)
425 = do h1 <- un' False bnames tx ty
426 h2 <- un' False bnames vx vy
427 sc 1
428 combine bnames h1 h2
429 uB bnames (Guess tx vx) (Guess ty vy)
430 = do h1 <- un' False bnames tx ty
431 h2 <- un' False bnames vx vy
432 sc 1
433 combine bnames h1 h2
434 uB bnames (Lam tx) (Lam ty) = do sc 1; un' False bnames tx ty
435 uB bnames (Pi tx) (Pi ty) = do sc 1; un' False bnames tx ty
436 uB bnames (Hole tx) (Hole ty) = un' False bnames tx ty
437 uB bnames (PVar tx) (PVar ty) = un' False bnames tx ty
438 uB bnames x y = do UI s f <- get
439 let r = recoverable (binderTy x) (binderTy y)
440 let err = CantUnify r topx topy
441 (CantUnify r (binderTy x) (binderTy y) (Msg "") [] s)
442 (errEnv env) s
443 put (UI s ((binderTy x, binderTy y, env, err) : f))
444 return [] -- lift $ tfail err
446 checkCycle ns p@(x, P _ _ _) = return [p]
447 checkCycle ns (x, tm)
448 | not (x `elem` freeNames tm) = checkScope ns (x, tm)
449 | otherwise = lift $ tfail (InfiniteUnify x tm (errEnv env))
451 checkScope ns (x, tm) =
452 case boundVs (envPos x 0 env) tm of
453 [] -> return [(x, tm)]
454 (i:_) -> lift $ tfail (UnifyScope x (fst (ns!!i))
455 (inst ns tm) (errEnv env))
456 where inst [] tm = tm
457 inst ((n, _) : ns) tm = inst ns (substV (P Bound n Erased) tm)
459 combineArgs bnames args = ca [] args where
460 ca acc [] = return acc
461 ca acc (x : xs) = do x' <- combine bnames acc x
462 ca x' xs
464 combine bnames as [] = return as
465 combine bnames as ((n, t) : bs)
466 = case lookup n as of
467 Nothing -> combine bnames (as ++ [(n,t)]) bs
468 Just t' -> do ns <- un' False bnames t t'
469 -- make sure there's n mapping from n in ns
470 let ns' = filter (\ (x, _) -> x/=n) ns
471 sc 1
472 combine bnames as (ns' ++ bs)
474boundVs :: Int -> Term -> [Int]
475boundVs i (V j) | j <= i = []
476 | otherwise = [j]
477boundVs i (Bind n b sc) = boundVs (i + 1) sc
478boundVs i (App f x) = let fs = boundVs i f
479 xs = boundVs i x in
480 nub (fs ++ xs)
481boundVs i _ = []
483envPos x i [] = 0
484envPos x i ((y, _) : ys) | x == y = i
485 | otherwise = envPos x (i + 1) ys
488-- If there are any clashes of constructors, deem it unrecoverable, otherwise some
489-- more work may help.
490-- FIXME: Depending on how overloading gets used, this may cause problems. Better
491-- rethink overloading properly...
493recoverable (P (DCon _ _) x _) (P (DCon _ _) y _)
494 | x == y = True
495 | otherwise = False
496recoverable (P (TCon _ _) x _) (P (TCon _ _) y _)
497 | x == y = True
498 | otherwise = False
499recoverable (Constant _) (P (DCon _ _) y _) = False
500recoverable (P (DCon _ _) x _) (Constant _) = False
501recoverable (Constant _) (P (TCon _ _) y _) = False
502recoverable (P (TCon _ _) x _) (Constant _) = False
503recoverable (P (DCon _ _) x _) (P (TCon _ _) y _) = False
504recoverable (P (TCon _ _) x _) (P (DCon _ _) y _) = False
505recoverable p@(Constant _) (App f a) = recoverable p f
506recoverable (App f a) p@(Constant _) = recoverable f p
507recoverable p@(P _ n _) (App f a) = recoverable p f
508-- recoverable (App f a) p@(P _ _ _) = recoverable f p
509recoverable (App f a) (App f' a')
510 = recoverable f f' -- && recoverable a a'
511recoverable _ _ = True
513errEnv = map (\(x, b) -> (x, binderTy b))
515holeIn :: Env -> Name -> Bool
516holeIn env n = case lookup n env of
517 Just (Hole _) -> True
518 Just (Guess _ _) -> True
519 _ -> False
521patIn :: Env -> Name -> Bool
522patIn env n = case lookup n env of
523 Just (PVar _) -> True
524 Just (PVTy _) -> True
525 _ -> False