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