git.iko.soy/Idris-dev
on 76722bf help sign in
Idris-dev/src/Core/Unify.hs
512 lines 22 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-- trace ("Matching " ++ show (topx, topy)) $
38 case runStateT (un [] topx topy) (UI 0 []) of
39 OK (v, UI _ []) -> return (filter notTrivial v)
40 res ->
41 let topxn = normalise ctxt env topx
42 topyn = normalise ctxt env topy in
43 case runStateT (un [] topxn topyn)
44 (UI 0 []) of
45 OK (v, UI _ fails) ->
46 return (filter notTrivial v)
47 Error e -> tfail e
48 where
49 un names (P _ x _) tm
50 | holeIn env x || x `elem` holes
51 = do sc 1; checkCycle names (x, tm)
52 un names tm (P _ y _)
53 | holeIn env y || y `elem` holes
54 = do sc 1; checkCycle names (y, tm)
55 un bnames (V i) (P _ x _)
56 | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []
57 un bnames (P _ x _) (V i)
58 | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []
59 un bnames (Bind x bx sx) (Bind y by sy)
60 = do h1 <- uB bnames bx by
61 h2 <- un ((x, y) : bnames) sx sy
62 combine bnames h1 h2
63 un names (App fx ax) (App fy ay)
64 = do hf <- un names fx fy
65 ha <- un names ax ay
66 combine names hf ha
67 un names x y
68 | OK True <- convEq' ctxt x y = do sc 1; return []
69 | otherwise = do UI s f <- get
70 let r = recoverable x y
71 let err = CantUnify r
72 topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s
73 if (not r) then lift $ tfail err
74 else do put (UI s ((x, y, env, err) : f))
75 lift $ tfail err
78 uB bnames (Let tx vx) (Let ty vy) = do h1 <- un bnames tx ty
79 h2 <- un bnames vx vy
80 combine bnames h1 h2
81 uB bnames (Lam tx) (Lam ty) = un bnames tx ty
82 uB bnames (Pi tx) (Pi ty) = un bnames tx ty
83 uB bnames x y = do UI s f <- get
84 let r = recoverable (binderTy x) (binderTy y)
85 let err = CantUnify r topx topy
86 (CantUnify r (binderTy x) (binderTy y) (Msg "") [] s)
87 (errEnv env) s
88 put (UI s ((binderTy x, binderTy y, env, err) : f))
89 return []
91 -- TODO: there's an annoying amount of repetition between this and the
92 -- main unification function. Consider lifting it out.
94 sc i = do UI s f <- get
95 put (UI (s+i) f)
97 unifyFail x y = do UI s f <- get
98 let r = recoverable x y
99 let err = CantUnify r
100 topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s
101 put (UI s ((x, y, env, err) : f))
102 lift $ tfail err
103 combine bnames as [] = return as
104 combine bnames as ((n, t) : bs)
105 = case lookup n as of
106 Nothing -> combine bnames (as ++ [(n,t)]) bs
107 Just t' -> do ns <- un bnames t t'
108 -- make sure there's n mapping from n in ns
109 let ns' = filter (\ (x, _) -> x/=n) ns
110 sc 1
111 combine bnames as (ns' ++ bs)
113 checkCycle ns p@(x, P _ _ _) = return [p]
114 checkCycle ns (x, tm)
115 | not (x `elem` freeNames tm) = checkScope ns (x, tm)
116 | otherwise = lift $ tfail (InfiniteUnify x tm (errEnv env))
118 checkScope ns (x, tm) =
119 case boundVs (envPos x 0 env) tm of
120 [] -> return [(x, tm)]
121 (i:_) -> lift $ tfail (UnifyScope x (fst (ns!!i))
122 (inst ns tm) (errEnv env))
123 where inst [] tm = tm
124 inst ((n, _) : ns) tm = inst ns (substV (P Bound n Erased) tm)
126notTrivial (x, P _ x' _) = x /= x'
127notTrivial _ = True
129expandLets env (x, tm) = (x, doSubst (reverse env) tm)
130 where
131 doSubst [] tm = tm
132 doSubst ((n, Let v t) : env) tm
133 = doSubst env (subst n v tm)
134 doSubst (_ : env) tm
135 = doSubst env tm
138unify :: Context -> Env -> TT Name -> TT Name -> [Name] -> [Name] ->
139 TC ([(Name, TT Name)], Fails)
140unify ctxt env topx topy dont holes =
141-- trace ("Unifying " ++ show (topx, topy)) $
142 -- don't bother if topx and topy are different at the head
143 case runStateT (un False [] topx topy) (UI 0 []) of
144 OK (v, UI _ []) -> return (filter notTrivial v,
145 [])
146 res ->
147 let topxn = normalise ctxt env topx
148 topyn = normalise ctxt env topy in
149-- trace ("Unifying " ++ show (topx, topy) ++ "\n\n==>\n" ++ show (topxn, topyn) ++ "\n\n" ++ show res ++ "\n\n") $
150 case runStateT (un False [] topxn topyn)
151 (UI 0 []) of
152 OK (v, UI _ fails) ->
153 return (filter notTrivial v, reverse fails)
154-- Error e@(CantUnify False _ _ _ _ _) -> tfail e
155 Error e -> tfail e
156 where
157 headDiff (P (DCon _ _) x _) (P (DCon _ _) y _) = x /= y
158 headDiff (P (TCon _ _) x _) (P (TCon _ _) y _) = x /= y
159 headDiff _ _ = False
161 injective (P (DCon _ _) _ _) = True
162 injective (P (TCon _ _) _ _) = True
163-- injective (App f (P _ _ _)) = injective f
164-- injective (App f (Constant _)) = injective f
165 injective (App f a) = injective f -- && injective a
166 injective _ = False
168 notP (P _ _ _) = False
169 notP _ = True
171 sc i = do UI s f <- get
172 put (UI (s+i) f)
174 errors = do UI s f <- get
175 return (not (null f))
177 uplus u1 u2 = do UI s f <- get
178 r <- u1
179 UI s f' <- get
180 if (length f == length f')
181 then return r
182 else do put (UI s f); u2
184 un :: Bool -> [(Name, Name)] -> TT Name -> TT Name ->
185 StateT UInfo
186 TC [(Name, TT Name)]
187 un = un'
188-- un fn names x y
189-- = let (xf, _) = unApply x
190-- (yf, _) = unApply y in
191-- if headDiff xf yf then unifyFail x y else
192-- uplus (un' fn names x y)
193-- (un' fn names (hnf ctxt env x) (hnf ctxt env y))
195 un' :: Bool -> [(Name, Name)] -> TT Name -> TT Name ->
196 StateT UInfo
197 TC [(Name, TT Name)]
198 un' fn names x y | x == y = return [] -- shortcut
199 un' fn names topx@(P (DCon _ _) x _) topy@(P (DCon _ _) y _)
200 | x /= y = unifyFail topx topy
201 un' fn names topx@(P (TCon _ _) x _) topy@(P (TCon _ _) y _)
202 | x /= y = unifyFail topx topy
203 un' fn names topx@(P (DCon _ _) x _) topy@(P (TCon _ _) y _)
204 = unifyFail topx topy
205 un' fn names topx@(P (TCon _ _) x _) topy@(P (DCon _ _) y _)
206 = unifyFail topx topy
207 un' fn names topx@(Constant _) topy@(P (TCon _ _) y _)
208 = unifyFail topx topy
209 un' fn names topx@(P (TCon _ _) x _) topy@(Constant _)
210 = unifyFail topx topy
211 un' fn bnames tx@(P _ x _) ty@(P _ y _)
212 | (x,y) `elem` bnames || x == y = do sc 1; return []
213 | injective tx && not (holeIn env y || y `elem` holes)
214 = unifyTmpFail tx ty
215 | injective ty && not (holeIn env x || x `elem` holes)
216 = unifyTmpFail tx ty
217 un' fn bnames xtm@(P _ x _) tm
218 | holeIn env x || x `elem` holes
219 = do UI s f <- get
220 -- injectivity check
221 if (notP tm && fn)
222-- trace (show (x, tm, normalise ctxt env tm)) $
223-- put (UI s ((tm, topx, topy) : i) f)
224 then unifyTmpFail xtm tm
225 else do sc 1
226 checkCycle bnames (x, tm)
227 | not (injective xtm) && injective tm = unifyFail xtm tm
228 un' fn bnames tm ytm@(P _ y _)
229 | holeIn env y || y `elem` holes
230 = do UI s f <- get
231 -- injectivity check
232 if (notP tm && fn)
233-- trace (show (y, tm, normalise ctxt env tm)) $
234-- put (UI s ((tm, topx, topy) : i) f)
235 then unifyTmpFail tm ytm
236 else do sc 1
237 checkCycle bnames (y, tm)
238 | not (injective ytm) && injective tm = unifyFail ytm tm
239 un' fn bnames (V i) (P _ x _)
240 | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []
241 un' fn bnames (P _ x _) (V i)
242 | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []
244 un' fn bnames appx@(App _ _) appy@(App _ _)
245 = unApp fn bnames appx appy
246-- = uplus (unApp fn bnames appx appy)
247-- (unifyTmpFail appx appy) -- take the whole lot
249 un' fn bnames x (Bind n (Lam t) (App y (P Bound n' _)))
250 | n == n' = un' False bnames x y
251 un' fn bnames (Bind n (Lam t) (App x (P Bound n' _))) y
252 | n == n' = un' False bnames x y
253 un' fn bnames x (Bind n (Lam t) (App y (V 0)))
254 = un' False bnames x y
255 un' fn bnames (Bind n (Lam t) (App x (V 0))) y
256 = un' False bnames x y
257-- un' fn bnames (Bind x (PVar _) sx) (Bind y (PVar _) sy)
258-- = un' False ((x,y):bnames) sx sy
259-- un' fn bnames (Bind x (PVTy _) sx) (Bind y (PVTy _) sy)
260-- = un' False ((x,y):bnames) sx sy
261 un' fn bnames (Bind x bx sx) (Bind y by sy)
262 = do h1 <- uB bnames bx by
263 h2 <- un' False ((x,y):bnames) sx sy
264 combine bnames h1 h2
265 un' fn bnames x y
266 | OK True <- convEq' ctxt x y = do sc 1; return []
267 | otherwise = do UI s f <- get
268 let r = recoverable x y
269 let err = CantUnify r
270 topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s
271 if (not r) then lift $ tfail err
272 else do put (UI s ((x, y, env, err) : f))
273 return [] -- lift $ tfail err
275 unApp fn bnames appx@(App fx ax) appy@(App fy ay)
276 | (injective fx && injective fy)
277 || (injective fx && rigid appx && metavarApp appy)
278 || (injective fy && rigid appy && metavarApp appx)
279 || (injective fx && metavarApp fy && ax == ay)
280 || (injective fy && metavarApp fx && ax == ay)
281 = do let (headx, _) = unApply fx
282 let (heady, _) = unApply fy
283 -- fail quickly if the heads are disjoint
284 checkHeads headx heady
285-- if True then -- (injective fx || injective fy || fx == fy) then
286-- if (injective fx && metavarApp appy) ||
287-- (injective fy && metavarApp appx) ||
288-- (injective fx && injective fy) || fx == fy
289 uplus
290 (do hf <- un' True bnames fx fy
291 let ax' = hnormalise hf ctxt env (substNames hf ax)
292 let ay' = hnormalise hf ctxt env (substNames hf ay)
293 ha <- un' False bnames ax' ay'
294 sc 1
295 combine bnames hf ha)
296 (do ha <- un' False bnames ax ay
297 let fx' = hnormalise ha ctxt env (substNames ha fx)
298 let fy' = hnormalise ha ctxt env (substNames ha fy)
299 hf <- un' False bnames fx' fy'
300 sc 1
301 combine bnames hf ha)
302 | otherwise = -- trace (show (appx, appy, injective fx, metavarApp appy, sameArgStruct appx appy)) $
303 do let (headx, argsx) = unApply appx
304 let (heady, argsy) = unApply appy
305 -- traceWhen (headx == heady) (show (appx, appy)) $
306 uplus (
307 if (length argsx == length argsy &&
308 ((headx == heady && inenv headx) || (argsx == argsy) ||
309 (and (zipWith sameStruct (headx:argsx) (heady:argsy)))))
310 then
311-- (notFn headx && notFn heady))) then
312 do uf <- un' True bnames headx heady
313 failed <- errors
314 if (not failed) then unArgs uf argsx argsy
315 else return []
316 else -- trace ("TMPFAIL " ++ show (appx, appy, injective appx, injective appy)) $
317 unifyTmpFail appx appy)
318 (unifyTmpFail appx appy) -- whole application fails
319 where hnormalise [] _ _ t = t
320 hnormalise ns ctxt env t = normalise ctxt env t
321 checkHeads (P (DCon _ _) x _) (P (DCon _ _) y _)
322 | x /= y = unifyFail appx appy
323 checkHeads (P (TCon _ _) x _) (P (TCon _ _) y _)
324 | x /= y = unifyFail appx appy
325 checkHeads (P (DCon _ _) x _) (P (TCon _ _) y _)
326 = unifyFail appx appy
327 checkHeads (P (TCon _ _) x _) (P (DCon _ _) y _)
328 = unifyFail appx appy
329 checkHeads _ _ = return []
331 unArgs as [] [] = return as
332 unArgs as (x : xs) (y : ys)
333 = do let x' = hnormalise as ctxt env (substNames as x)
334 let y' = hnormalise as ctxt env (substNames as y)
335 as' <- un' False bnames x' y'
336 vs <- combine bnames as as'
337 unArgs vs xs ys
339 metavarApp tm = let (f, args) = unApply tm in
340 metavar f &&
341 all (\x -> metavarApp x) args
342 && nub args == args
343 metavarArgs tm = let (f, args) = unApply tm in
344 all (\x -> metavar x || inenv x) args
345 && nub args == args
346 metavarApp' tm = let (f, args) = unApply tm in
347 all (\x -> pat x || metavar x) (f : args)
348 && nub args == args
350 sameArgStruct appx appy
351 = let (_, ax) = unApply appx
352 (_, ay) = unApply appy in
353 length ax == length ay &&
354 and (zipWith sameStruct ax ay)
356 sameStruct fapp@(App f x) gapp@(App g y)
357 = let (f',a') = unApply fapp
358 (g',b') = unApply gapp in
359 (f' == g' && length a' == length b' &&
360 (injective f' || injective g'))
361 || (sameStruct f g && sameStruct x y)
362 sameStruct (P _ x _) (P _ y _) = True
363 sameStruct (V i) (V j) = i == j
364 sameStruct (Constant x) (Constant y) = True
365 sameStruct (P _ _ _) (Constant y) = True
366 sameStruct (Constant x) (P _ _ _) = True
367 sameStruct (Bind n t sc) (P _ _ _) = True
368 sameStruct (P _ _ _) (Bind n t sc) = True
369 sameStruct (Bind n t sc) (Bind n' t' sc') = sameStruct sc sc'
370 sameStruct _ _ = False
372 rigid (P (DCon _ _) _ _) = True
373 rigid (P (TCon _ _) _ _) = True
374 rigid t@(P Ref _ _) = inenv t
375 rigid (Constant _) = True
376 rigid (App f a) = rigid f && rigid a
377 rigid t = not (metavar t)
379 metavar t = case t of
380 P _ x _ -> (x `elem` holes || holeIn env x) &&
381 not (x `elem` dont)
382 _ -> False
383 pat t = case t of
384 P _ x _ -> x `elem` holes || patIn env x
385 _ -> False
386 inenv t = case t of
387 P _ x _ -> x `elem` (map fst env)
388 _ -> False
390 notFn t = injective t || metavar t || inenv t
393 unifyTmpFail x y
394 = do UI s f <- get
395 let r = recoverable x y
396 let err = CantUnify r
397 topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s
398 put (UI s ((topx, topy, env, err) : f))
399 return []
401 -- shortcut failure, if we *know* nothing can fix it
402 unifyFail x y = do UI s f <- get
403 let r = recoverable x y
404 let err = CantUnify r
405 topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s
406 put (UI s ((topx, topy, env, err) : f))
407 lift $ tfail err
410 uB bnames (Let tx vx) (Let ty vy)
411 = do h1 <- un' False bnames tx ty
412 h2 <- un' False bnames vx vy
413 sc 1
414 combine bnames h1 h2
415 uB bnames (Guess tx vx) (Guess ty vy)
416 = do h1 <- un' False bnames tx ty
417 h2 <- un' False bnames vx vy
418 sc 1
419 combine bnames h1 h2
420 uB bnames (Lam tx) (Lam ty) = do sc 1; un' False bnames tx ty
421 uB bnames (Pi tx) (Pi ty) = do sc 1; un' False bnames tx ty
422 uB bnames (Hole tx) (Hole ty) = un' False bnames tx ty
423 uB bnames (PVar tx) (PVar ty) = un' False bnames tx ty
424 uB bnames x y = do UI s f <- get
425 let r = recoverable (binderTy x) (binderTy y)
426 let err = CantUnify r topx topy
427 (CantUnify r (binderTy x) (binderTy y) (Msg "") [] s)
428 (errEnv env) s
429 put (UI s ((binderTy x, binderTy y, env, err) : f))
430 return [] -- lift $ tfail err
432 checkCycle ns p@(x, P _ _ _) = return [p]
433 checkCycle ns (x, tm)
434 | not (x `elem` freeNames tm) = checkScope ns (x, tm)
435 | otherwise = lift $ tfail (InfiniteUnify x tm (errEnv env))
437 checkScope ns (x, tm) =
438 case boundVs (envPos x 0 env) tm of
439 [] -> return [(x, tm)]
440 (i:_) -> lift $ tfail (UnifyScope x (fst (ns!!i))
441 (inst ns tm) (errEnv env))
442 where inst [] tm = tm
443 inst ((n, _) : ns) tm = inst ns (substV (P Bound n Erased) tm)
445 combineArgs bnames args = ca [] args where
446 ca acc [] = return acc
447 ca acc (x : xs) = do x' <- combine bnames acc x
448 ca x' xs
450 combine bnames as [] = return as
451 combine bnames as ((n, t) : bs)
452 = case lookup n as of
453 Nothing -> combine bnames (as ++ [(n,t)]) bs
454 Just t' -> do ns <- un' False bnames t t'
455 -- make sure there's n mapping from n in ns
456 let ns' = filter (\ (x, _) -> x/=n) ns
457 sc 1
458 combine bnames as (ns' ++ bs)
460boundVs :: Int -> Term -> [Int]
461boundVs i (V j) | j <= i = []
462 | otherwise = [j]
463boundVs i (Bind n b sc) = boundVs (i + 1) sc
464boundVs i (App f x) = let fs = boundVs i f
465 xs = boundVs i x in
466 nub (fs ++ xs)
467boundVs i _ = []
469envPos x i [] = 0
470envPos x i ((y, _) : ys) | x == y = i
471 | otherwise = envPos x (i + 1) ys
474-- If there are any clashes of constructors, deem it unrecoverable, otherwise some
475-- more work may help.
476-- FIXME: Depending on how overloading gets used, this may cause problems. Better
477-- rethink overloading properly...
479recoverable (P (DCon _ _) x _) (P (DCon _ _) y _)
480 | x == y = True
481 | otherwise = False
482recoverable (P (TCon _ _) x _) (P (TCon _ _) y _)
483 | x == y = True
484 | otherwise = False
485recoverable (Constant _) (P (DCon _ _) y _) = False
486recoverable (P (DCon _ _) x _) (Constant _) = False
487recoverable (Constant _) (P (TCon _ _) y _) = False
488recoverable (P (TCon _ _) x _) (Constant _) = False
489recoverable (P (DCon _ _) x _) (P (TCon _ _) y _) = False
490recoverable (P (TCon _ _) x _) (P (DCon _ _) y _) = False
491recoverable p@(Constant _) (App f a) = recoverable p f
492recoverable (App f a) p@(Constant _) = recoverable f p
493recoverable p@(P _ n _) (App f a) = recoverable p f
494-- recoverable (App f a) p@(P _ _ _) = recoverable f p
495recoverable (App f a) (App f' a')
496 = recoverable f f' -- && recoverable a a'
497recoverable _ _ = True
499errEnv = map (\(x, b) -> (x, binderTy b))
501holeIn :: Env -> Name -> Bool
502holeIn env n = case lookup n env of
503 Just (Hole _) -> True
504 Just (Guess _ _) -> True
505 _ -> False
507patIn :: Env -> Name -> Bool
508patIn env n = case lookup n env of
509 Just (PVar _) -> True
510 Just (PVTy _) -> True
511 _ -> False