git.iko.soy/Idris-dev
on de72eb9 help sign in
Idris-dev/src/Idris/Core/Unify.hs
560 lines 24 kB history raw
1{-# LANGUAGE PatternGuards #-}
3module Idris.Core.Unify(match_unify, unify, Fails) where
5import Idris.Core.TT
6import Idris.Core.Evaluate
8import Control.Monad
9import Control.Monad.State.Strict
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 (map (renameBinders env) (trimSolutions 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 (map (renameBinders env) (trimSolutions 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 (map (renameBinders env) (trimSolutions v))
52 _ -> tfail e
53 where
56 un names (P _ x _) tm
57 | holeIn env x || x `elem` holes
58 = do sc 1; checkCycle names (x, tm)
59 un names tm (P _ y _)
60 | holeIn env y || y `elem` holes
61 = do sc 1; checkCycle names (y, tm)
62 un bnames (V i) (P _ x _)
63 | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []
64 un bnames (P _ x _) (V i)
65 | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []
66 un bnames (Bind x bx sx) (Bind y by sy)
67 = do h1 <- uB bnames bx by
68 h2 <- un ((x, y) : bnames) sx sy
69 combine bnames h1 h2
70 un names (App fx ax) (App fy ay)
71 = do hf <- un names fx fy
72 ha <- un names ax ay
73 combine names hf ha
74 un names x y
75 | OK True <- convEq' ctxt x y = do sc 1; return []
76 | otherwise = do UI s f <- get
77 let r = recoverable x y
78 let err = CantUnify r
79 topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s
80 if (not r) then lift $ tfail err
81 else do put (UI s ((x, y, env, err) : f))
82 lift $ tfail err
85 uB bnames (Let tx vx) (Let ty vy) = do h1 <- un bnames tx ty
86 h2 <- un bnames vx vy
87 combine bnames h1 h2
88 uB bnames (Lam tx) (Lam ty) = un bnames tx ty
89 uB bnames (Pi tx) (Pi ty) = un bnames tx ty
90 uB bnames x y = do UI s f <- get
91 let r = recoverable (binderTy x) (binderTy y)
92 let err = CantUnify r topx topy
93 (CantUnify r (binderTy x) (binderTy y) (Msg "") [] s)
94 (errEnv env) s
95 put (UI s ((binderTy x, binderTy y, env, err) : f))
96 return []
98 -- TODO: there's an annoying amount of repetition between this and the
99 -- main unification function. Consider lifting it out.
101 sc i = do UI s f <- get
102 put (UI (s+i) f)
104 unifyFail x y = do UI s f <- get
105 let r = recoverable x y
106 let err = CantUnify r
107 topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s
108 put (UI s ((x, y, env, err) : f))
109 lift $ tfail err
110 combine bnames as [] = return as
111 combine bnames as ((n, t) : bs)
112 = case lookup n as of
113 Nothing -> combine bnames (as ++ [(n,t)]) bs
114 Just t' -> do ns <- un bnames t t'
115 -- make sure there's n mapping from n in ns
116 let ns' = filter (\ (x, _) -> x/=n) ns
117 sc 1
118 combine bnames as (ns' ++ bs)
120 checkCycle ns p@(x, P _ _ _) = return [p]
121 checkCycle ns (x, tm)
122 | not (x `elem` freeNames tm) = checkScope ns (x, tm)
123 | otherwise = lift $ tfail (InfiniteUnify x tm (errEnv env))
125 checkScope ns (x, tm) =
126 case boundVs (envPos x 0 env) tm of
127 [] -> return [(x, tm)]
128 (i:_) -> lift $ tfail (UnifyScope x (fst (ns!!i))
129 (inst ns tm) (errEnv env))
130 where inst [] tm = tm
131 inst ((n, _) : ns) tm = inst ns (substV (P Bound n Erased) tm)
133renameBinders :: Env -> (Name, TT Name) -> (Name, TT Name)
134renameBinders env (x, tm) = (x, uniqueBinders tm)
135 where
136 uniqueBinders (Bind n b sc)
137 | n `elem` map fst env
138 = let n' = uniqueName n (map fst env) in
139 Bind n' (fmap uniqueBinders b)
140 (uniqueBinders (rename n n' sc))
141 | otherwise = Bind n (fmap uniqueBinders b) (uniqueBinders sc)
142 uniqueBinders (App f a) = App (uniqueBinders f) (uniqueBinders a)
143 uniqueBinders t = t
145 rename n n' (P nt x ty) | n == x = P nt n' ty
146 rename n n' (Bind x b sc) = Bind x (fmap (rename n n') b) (rename n n' sc)
147 rename n n' (App f a) = App (rename n n' f) (rename n n' a)
148 rename n n' t = t
150trimSolutions ns = dropPairs ns
151 where dropPairs [] = []
152 dropPairs (n@(x, P _ x' _) : ns)
153 | x == x' = dropPairs ns
154 | otherwise
155 = n : dropPairs
156 (filter (\t -> case t of
157 (n, P _ n' _) -> not (n == x' && n' == x)
158 _ -> True) ns)
159 dropPairs (n : ns) = n : dropPairs ns
161expandLets env (x, tm) = (x, doSubst (reverse env) tm)
162 where
163 doSubst [] tm = tm
164 doSubst ((n, Let v t) : env) tm
165 = doSubst env (subst n v tm)
166 doSubst (_ : env) tm
167 = doSubst env tm
170unify :: Context -> Env -> TT Name -> TT Name -> [Name] -> [Name] ->
171 TC ([(Name, TT Name)], Fails)
172unify ctxt env topx topy dont holes =
173-- trace ("Unifying " ++ show (topx, topy)) $
174 -- don't bother if topx and topy are different at the head
175 case runStateT (un False [] topx topy) (UI 0 []) of
176 OK (v, UI _ []) -> return (map (renameBinders env) (trimSolutions v),
177 [])
178 res ->
179 let topxn = normalise ctxt env topx
180 topyn = normalise ctxt env topy in
181-- trace ("Unifying " ++ show (topx, topy) ++ "\n\n==>\n" ++ show (topxn, topyn) ++ "\n\n" ++ show res ++ "\n\n") $
182 case runStateT (un False [] topxn topyn)
183 (UI 0 []) of
184 OK (v, UI _ fails) ->
185 return (map (renameBinders env) (trimSolutions v),
186 reverse fails)
187-- Error e@(CantUnify False _ _ _ _ _) -> tfail e
188 Error e -> tfail e
189 where
190 headDiff (P (DCon _ _) x _) (P (DCon _ _) y _) = x /= y
191 headDiff (P (TCon _ _) x _) (P (TCon _ _) y _) = x /= y
192 headDiff _ _ = False
194 injective (P (DCon _ _) _ _) = True
195 injective (P (TCon _ _) _ _) = True
196-- injective (App f (P _ _ _)) = injective f
197-- injective (App f (Constant _)) = injective f
198 injective (App f a) = injective f -- && injective a
199 injective _ = False
201 notP (P _ _ _) = False
202 notP _ = True
204 sc i = do UI s f <- get
205 put (UI (s+i) f)
207 errors = do UI s f <- get
208 return (not (null f))
210 uplus u1 u2 = do UI s f <- get
211 r <- u1
212 UI s f' <- get
213 if (length f == length f')
214 then return r
215 else do put (UI s f); u2
217 un :: Bool -> [(Name, Name)] -> TT Name -> TT Name ->
218 StateT UInfo
219 TC [(Name, TT Name)]
220 un = un'
221-- un fn names x y
222-- = let (xf, _) = unApply x
223-- (yf, _) = unApply y in
224-- if headDiff xf yf then unifyFail x y else
225-- uplus (un' fn names x y)
226-- (un' fn names (hnf ctxt env x) (hnf ctxt env y))
228 un' :: Bool -> [(Name, Name)] -> TT Name -> TT Name ->
229 StateT UInfo
230 TC [(Name, TT Name)]
231 un' fn names x y | x == y = return [] -- shortcut
232 un' fn names topx@(P (DCon _ _) x _) topy@(P (DCon _ _) y _)
233 | x /= y = unifyFail topx topy
234 un' fn names topx@(P (TCon _ _) x _) topy@(P (TCon _ _) y _)
235 | x /= y = unifyFail topx topy
236 un' fn names topx@(P (DCon _ _) x _) topy@(P (TCon _ _) y _)
237 = unifyFail topx topy
238 un' fn names topx@(P (TCon _ _) x _) topy@(P (DCon _ _) y _)
239 = unifyFail topx topy
240 un' fn names topx@(Constant _) topy@(P (TCon _ _) y _)
241 = unifyFail topx topy
242 un' fn names topx@(P (TCon _ _) x _) topy@(Constant _)
243 = unifyFail topx topy
244 un' fn bnames tx@(P _ x _) ty@(P _ y _)
245 | (x,y) `elem` bnames || x == y = do sc 1; return []
246 | injective tx && not (holeIn env y || y `elem` holes)
247 = unifyTmpFail tx ty
248 | injective ty && not (holeIn env x || x `elem` holes)
249 = unifyTmpFail tx ty
250 un' fn bnames xtm@(P _ x _) tm
251 | holeIn env x || x `elem` holes
252 = do UI s f <- get
253 -- injectivity check
254 if (notP tm && fn)
255-- trace (show (x, tm, normalise ctxt env tm)) $
256-- put (UI s ((tm, topx, topy) : i) f)
257 then unifyTmpFail xtm tm
258 else do sc 1
259 checkCycle bnames (x, tm)
260 | not (injective xtm) && injective tm = unifyFail xtm tm
261 un' fn bnames tm ytm@(P _ y _)
262 | holeIn env y || y `elem` holes
263 = do UI s f <- get
264 -- injectivity check
265 if (notP tm && fn)
266-- trace (show (y, tm, normalise ctxt env tm)) $
267-- put (UI s ((tm, topx, topy) : i) f)
268 then unifyTmpFail tm ytm
269 else do sc 1
270 checkCycle bnames (y, tm)
271 | not (injective ytm) && injective tm = unifyFail ytm tm
272 un' fn bnames (V i) (P _ x _)
273 | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []
274 un' fn bnames (P _ x _) (V i)
275 | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []
277 un' fn bnames appx@(App _ _) appy@(App _ _)
278 = unApp fn bnames appx appy
279-- = uplus (unApp fn bnames appx appy)
280-- (unifyTmpFail appx appy) -- take the whole lot
282 un' fn bnames x (Bind n (Lam t) (App y (P Bound n' _)))
283 | n == n' = un' False bnames x y
284 un' fn bnames (Bind n (Lam t) (App x (P Bound n' _))) y
285 | n == n' = un' False bnames x y
286 un' fn bnames x (Bind n (Lam t) (App y (V 0)))
287 = un' False bnames x y
288 un' fn bnames (Bind n (Lam t) (App x (V 0))) y
289 = un' False bnames x y
290-- un' fn bnames (Bind x (PVar _) sx) (Bind y (PVar _) sy)
291-- = un' False ((x,y):bnames) sx sy
292-- un' fn bnames (Bind x (PVTy _) sx) (Bind y (PVTy _) sy)
293-- = un' False ((x,y):bnames) sx sy
295 -- f D unifies with t -> D. This is dubious, but it helps with type
296 -- class resolution for type classes over functions.
298 un' fn bnames (App f x) (Bind n (Pi t) y)
299 | noOccurrence n y && x == y
300 = un' False bnames f (Bind (sMN 0 "uv") (Lam (TType (UVar 0)))
301 (Bind n (Pi t) (V 1)))
303 un' fn bnames (Bind x bx sx) (Bind y by sy)
304 = do h1 <- uB bnames bx by
305 h2 <- un' False ((x,y):bnames) sx sy
306 combine bnames h1 h2
307 un' fn bnames x y
308 | OK True <- convEq' ctxt x y = do sc 1; return []
309 | otherwise = do UI s f <- get
310 let r = recoverable x y
311 let err = CantUnify r
312 topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s
313 if (not r) then lift $ tfail err
314 else do put (UI s ((x, y, env, err) : f))
315 return [] -- lift $ tfail err
317 unApp fn bnames appx@(App fx ax) appy@(App fy ay)
318 | (injective fx && injective fy)
319 || (injective fx && rigid appx && metavarApp appy)
320 || (injective fy && rigid appy && metavarApp appx)
321 || (injective fx && metavarApp fy && ax == ay)
322 || (injective fy && metavarApp fx && ax == ay)
323 = do let (headx, _) = unApply fx
324 let (heady, _) = unApply fy
325 -- fail quickly if the heads are disjoint
326 checkHeads headx heady
327-- if True then -- (injective fx || injective fy || fx == fy) then
328-- if (injective fx && metavarApp appy) ||
329-- (injective fy && metavarApp appx) ||
330-- (injective fx && injective fy) || fx == fy
331 uplus
332 (do hf <- un' True bnames fx fy
333 let ax' = hnormalise hf ctxt env (substNames hf ax)
334 let ay' = hnormalise hf ctxt env (substNames hf ay)
335 ha <- un' False bnames ax' ay'
336 sc 1
337 combine bnames hf ha)
338 (do ha <- un' False bnames ax ay
339 let fx' = hnormalise ha ctxt env (substNames ha fx)
340 let fy' = hnormalise ha ctxt env (substNames ha fy)
341 hf <- un' False bnames fx' fy'
342 sc 1
343 combine bnames hf ha)
344 | otherwise = -- trace (show (appx, appy, injective fx, metavarApp appy, sameArgStruct appx appy)) $
345 do let (headx, argsx) = unApply appx
346 let (heady, argsy) = unApply appy
347 -- traceWhen (headx == heady) (show (appx, appy)) $
348 uplus (
349 if (length argsx == length argsy &&
350 ((headx == heady && inenv headx) || (argsx == argsy) ||
351 (and (zipWith sameStruct (headx:argsx) (heady:argsy)))))
352 then
353-- (notFn headx && notFn heady))) then
354 do uf <- un' True bnames headx heady
355 failed <- errors
356 if (not failed) then unArgs uf argsx argsy
357 else return []
358 else -- trace ("TMPFAIL " ++ show (appx, appy, injective appx, injective appy)) $
359 unifyTmpFail appx appy)
360 (unifyTmpFail appx appy) -- whole application fails
361 where hnormalise [] _ _ t = t
362 hnormalise ns ctxt env t = normalise ctxt env t
363 checkHeads (P (DCon _ _) x _) (P (DCon _ _) y _)
364 | x /= y = unifyFail appx appy
365 checkHeads (P (TCon _ _) x _) (P (TCon _ _) y _)
366 | x /= y = unifyFail appx appy
367 checkHeads (P (DCon _ _) x _) (P (TCon _ _) y _)
368 = unifyFail appx appy
369 checkHeads (P (TCon _ _) x _) (P (DCon _ _) y _)
370 = unifyFail appx appy
371 checkHeads _ _ = return []
373 unArgs as [] [] = return as
374 unArgs as (x : xs) (y : ys)
375 = do let x' = hnormalise as ctxt env (substNames as x)
376 let y' = hnormalise as ctxt env (substNames as y)
377 as' <- un' False bnames x' y'
378 vs <- combine bnames as as'
379 unArgs vs xs ys
381 metavarApp tm = let (f, args) = unApply tm in
382 metavar f &&
383 all (\x -> metavarApp x) args
384 && nub args == args
385 metavarArgs tm = let (f, args) = unApply tm in
386 all (\x -> metavar x || inenv x) args
387 && nub args == args
388 metavarApp' tm = let (f, args) = unApply tm in
389 all (\x -> pat x || metavar x) (f : args)
390 && nub args == args
392 sameArgStruct appx appy
393 = let (_, ax) = unApply appx
394 (_, ay) = unApply appy in
395 length ax == length ay &&
396 and (zipWith sameStruct ax ay)
398 sameStruct fapp@(App f x) gapp@(App g y)
399 = let (f',a') = unApply fapp
400 (g',b') = unApply gapp in
401 (f' == g' && length a' == length b' &&
402 (injective f' || injective g'))
403 || (sameStruct f g && sameStruct x y)
404 sameStruct (P _ x _) (P _ y _) = True
405 sameStruct (V i) (V j) = i == j
406 sameStruct (Constant x) (Constant y) = True
407 sameStruct (P _ _ _) (Constant y) = True
408 sameStruct (Constant x) (P _ _ _) = True
409 sameStruct (Bind n t sc) (P _ _ _) = True
410 sameStruct (P _ _ _) (Bind n t sc) = True
411 sameStruct (Bind n t sc) (Bind n' t' sc') = sameStruct sc sc'
412 sameStruct _ _ = False
414 rigid (P (DCon _ _) _ _) = True
415 rigid (P (TCon _ _) _ _) = True
416 rigid t@(P Ref _ _) = inenv t
417 rigid (Constant _) = True
418 rigid (App f a) = rigid f && rigid a
419 rigid t = not (metavar t)
421 metavar t = case t of
422 P _ x _ -> (x `elem` holes || holeIn env x) &&
423 not (x `elem` dont)
424 _ -> False
425 pat t = case t of
426 P _ x _ -> x `elem` holes || patIn env x
427 _ -> False
428 inenv t = case t of
429 P _ x _ -> x `elem` (map fst env)
430 _ -> False
432 notFn t = injective t || metavar t || inenv t
435 unifyTmpFail x y
436 = do UI s f <- get
437 let r = recoverable x y
438 let err = CantUnify r
439 topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s
440 put (UI s ((topx, topy, env, err) : f))
441 return []
443 -- shortcut failure, if we *know* nothing can fix it
444 unifyFail x y = do UI s f <- get
445 let r = recoverable x y
446 let err = CantUnify r
447 topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s
448 put (UI s ((topx, topy, env, err) : f))
449 lift $ tfail err
452 uB bnames (Let tx vx) (Let ty vy)
453 = do h1 <- un' False bnames tx ty
454 h2 <- un' False bnames vx vy
455 sc 1
456 combine bnames h1 h2
457 uB bnames (Guess tx vx) (Guess ty vy)
458 = do h1 <- un' False bnames tx ty
459 h2 <- un' False bnames vx vy
460 sc 1
461 combine bnames h1 h2
462 uB bnames (Lam tx) (Lam ty) = do sc 1; un' False bnames tx ty
463 uB bnames (Pi tx) (Pi ty) = do sc 1; un' False bnames tx ty
464 uB bnames (Hole tx) (Hole ty) = un' False bnames tx ty
465 uB bnames (PVar tx) (PVar ty) = un' False bnames tx ty
466 uB bnames x y = do UI s f <- get
467 let r = recoverable (binderTy x) (binderTy y)
468 let err = CantUnify r topx topy
469 (CantUnify r (binderTy x) (binderTy y) (Msg "") [] s)
470 (errEnv env) s
471 put (UI s ((binderTy x, binderTy y, env, err) : f))
472 return [] -- lift $ tfail err
474 checkCycle ns p@(x, P _ _ _) = return [p]
475 checkCycle ns (x, tm)
476 | not (x `elem` freeNames tm) = checkScope ns (x, tm)
477 | otherwise = lift $ tfail (InfiniteUnify x tm (errEnv env))
479 checkScope ns (x, tm) =
480 case boundVs (envPos x 0 env) tm of
481 [] -> return [(x, tm)]
482 (i:_) -> lift $ tfail (UnifyScope x (fst (ns!!i))
483 (inst ns tm) (errEnv env))
484 where inst [] tm = tm
485 inst ((n, _) : ns) tm = inst ns (substV (P Bound n Erased) tm)
487 combineArgs bnames args = ca [] args where
488 ca acc [] = return acc
489 ca acc (x : xs) = do x' <- combine bnames acc x
490 ca x' xs
492 combine bnames as [] = return as
493 combine bnames as ((n, t) : bs)
494 = case lookup n as of
495 Nothing -> combine bnames (as ++ [(n,t)]) bs
496 Just t' -> do ns <- un' False bnames t t'
497 -- make sure there's n mapping from n in ns
498 let ns' = filter (\ (x, _) -> x/=n) ns
499 sc 1
500 combine bnames as (ns' ++ bs)
502boundVs :: Int -> Term -> [Int]
503boundVs i (V j) | j <= i = []
504 | otherwise = [j]
505boundVs i (Bind n b sc) = boundVs (i + 1) sc
506boundVs i (App f x) = let fs = boundVs i f
507 xs = boundVs i x in
508 nub (fs ++ xs)
509boundVs i _ = []
511envPos x i [] = 0
512envPos x i ((y, _) : ys) | x == y = i
513 | otherwise = envPos x (i + 1) ys
516-- If there are any clashes of constructors, deem it unrecoverable, otherwise some
517-- more work may help.
518-- FIXME: Depending on how overloading gets used, this may cause problems. Better
519-- rethink overloading properly...
521recoverable (P (DCon _ _) x _) (P (DCon _ _) y _)
522 | x == y = True
523 | otherwise = False
524recoverable (P (TCon _ _) x _) (P (TCon _ _) y _)
525 | x == y = True
526 | otherwise = False
527recoverable (Constant _) (P (DCon _ _) y _) = False
528recoverable (P (DCon _ _) x _) (Constant _) = False
529recoverable (Constant _) (P (TCon _ _) y _) = False
530recoverable (P (TCon _ _) x _) (Constant _) = False
531recoverable (P (DCon _ _) x _) (P (TCon _ _) y _) = False
532recoverable (P (TCon _ _) x _) (P (DCon _ _) y _) = False
533recoverable p@(Constant _) (App f a) = recoverable p f
534recoverable (App f a) p@(Constant _) = recoverable f p
535recoverable p@(P _ n _) (App f a) = recoverable p f
536-- recoverable (App f a) p@(P _ _ _) = recoverable f p
537recoverable (App f a) (App f' a')
538 = recoverable f f' -- && recoverable a a'
539recoverable f (Bind _ (Pi _) sc)
540 | (P (DCon _ _) _ _, _) <- unApply f = False
541 | (P (TCon _ _) _ _, _) <- unApply f = False
542recoverable (Bind _ (Pi _) sc) f
543 | (P (DCon _ _) _ _, _) <- unApply f = False
544 | (P (TCon _ _) _ _, _) <- unApply f = False
545recoverable _ _ = True
547errEnv = map (\(x, b) -> (x, binderTy b))
549holeIn :: Env -> Name -> Bool
550holeIn env n = case lookup n env of
551 Just (Hole _) -> True
552 Just (Guess _ _) -> True
553 _ -> False
555patIn :: Env -> Name -> Bool
556patIn env n = case lookup n env of
557 Just (PVar _) -> True
558 Just (PVTy _) -> True
559 _ -> False