git.iko.soy/Idris-dev
on f553076 help sign in
Idris-dev/src/Core/Unify.hs
439 lines 19 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 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
30-- Solve metavariables by matching terms against each other
31-- Not really unification, of course!
33match_unify :: Context -> Env -> TT Name -> TT Name -> [Name] -> [Name] ->
34 TC [(Name, TT Name)]
35match_unify ctxt env topx topy dont holes =
36-- trace ("Matching " ++ show (topx, topy)) $
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 -> tfail e
47 where
48 un names (P _ x _) tm
49 | holeIn env x || x `elem` holes
50 = do sc 1; checkCycle (x, tm)
51 un names tm (P _ y _)
52 | holeIn env y || y `elem` holes
53 = do sc 1; checkCycle (y, tm)
54 un bnames (V i) (P _ x _)
55 | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []
56 un bnames (P _ x _) (V i)
57 | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []
58 un names (App fx ax) (App fy ay)
59 = do hf <- un names fx fy
60 ha <- un names ax ay
61 combine names hf ha
62 un names x y
63 | OK True <- convEq' ctxt x y = do sc 1; return []
64 | otherwise = do UI s f <- get
65 let r = recoverable x y
66 let err = CantUnify r
67 topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s
68 if (not r) then lift $ tfail err
69 else do put (UI s ((x, y, env, err) : f))
70 lift $ tfail err
73 -- TODO: there's an annoying amount of repetition between this and the
74 -- main unification function. Consider lifting it out.
76 sc i = do UI s f <- get
77 put (UI (s+i) f)
79 unifyFail x y = do UI s f <- get
80 let r = recoverable x y
81 let err = CantUnify r
82 topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s
83 put (UI s ((x, y, env, err) : f))
84 lift $ tfail err
85 combine bnames as [] = return as
86 combine bnames as ((n, t) : bs)
87 = case lookup n as of
88 Nothing -> combine bnames (as ++ [(n,t)]) bs
89 Just t' -> do ns <- un bnames t t'
90 -- make sure there's n mapping from n in ns
91 let ns' = filter (\ (x, _) -> x/=n) ns
92 sc 1
93 combine bnames as (ns' ++ bs)
95 checkCycle p@(x, P _ _ _) = return [p]
96 checkCycle (x, tm)
97 | not (x `elem` freeNames tm) = return [(x, tm)]
98 | otherwise = lift $ tfail (InfiniteUnify x tm (errEnv env))
100notTrivial (x, P _ x' _) = x /= x'
101notTrivial _ = True
104unify :: Context -> Env -> TT Name -> TT Name -> [Name] -> [Name] ->
105 TC ([(Name, TT Name)], Fails)
106unify ctxt env topx topy dont holes =
107-- trace ("Unifying " ++ show (topx, topy)) $
108 -- don't bother if topx and topy are different at the head
109 case runStateT (un False [] topx topy) (UI 0 []) of
110 OK (v, UI _ []) -> return (filter notTrivial v, [])
111 res ->
112 let topxn = normalise ctxt env topx
113 topyn = normalise ctxt env topy in
114-- trace ("Unifying " ++ show (topx, topy) ++ "\n\n==>\n" ++ show (topxn, topyn) ++ "\n\n" ++ show res ++ "\n\n") $
115 case runStateT (un False [] topxn topyn)
116 (UI 0 []) of
117 OK (v, UI _ fails) ->
118 return (filter notTrivial v, reverse fails)
119-- Error e@(CantUnify False _ _ _ _ _) -> tfail e
120 Error e -> tfail e
121 where
122 headDiff (P (DCon _ _) x _) (P (DCon _ _) y _) = x /= y
123 headDiff (P (TCon _ _) x _) (P (TCon _ _) y _) = x /= y
124 headDiff _ _ = False
126 injective (P (DCon _ _) _ _) = True
127 injective (P (TCon _ _) _ _) = True
128-- injective (App f (P _ _ _)) = injective f
129-- injective (App f (Constant _)) = injective f
130 injective (App f a) = injective f -- && injective a
131 injective _ = False
133 notP (P _ _ _) = False
134 notP _ = True
136 sc i = do UI s f <- get
137 put (UI (s+i) f)
139 uplus u1 u2 = do UI s f <- get
140 r <- u1
141 UI s f' <- get
142 if (length f == length f')
143 then return r
144 else do put (UI s f); u2
146 un :: Bool -> [(Name, Name)] -> TT Name -> TT Name ->
147 StateT UInfo
148 TC [(Name, TT Name)]
149 un = un'
150-- un fn names x y
151-- = let (xf, _) = unApply x
152-- (yf, _) = unApply y in
153-- if headDiff xf yf then unifyFail x y else
154-- uplus (un' fn names x y)
155-- (un' fn names (hnf ctxt env x) (hnf ctxt env y))
157 un' :: Bool -> [(Name, Name)] -> TT Name -> TT Name ->
158 StateT UInfo
159 TC [(Name, TT Name)]
160 un' fn names x y | x == y = return [] -- shortcut
161 un' fn names topx@(P (DCon _ _) x _) topy@(P (DCon _ _) y _)
162 | x /= y = unifyFail topx topy
163 un' fn names topx@(P (TCon _ _) x _) topy@(P (TCon _ _) y _)
164 | x /= y = unifyFail topx topy
165 un' fn names topx@(P (DCon _ _) x _) topy@(P (TCon _ _) y _)
166 = unifyFail topx topy
167 un' fn names topx@(P (TCon _ _) x _) topy@(P (DCon _ _) y _)
168 = unifyFail topx topy
169 un' fn names topx@(Constant _) topy@(P (TCon _ _) y _)
170 = unifyFail topx topy
171 un' fn names topx@(P (TCon _ _) x _) topy@(Constant _)
172 = unifyFail topx topy
173 un' fn bnames tx@(P _ x _) ty@(P _ y _)
174 | (x,y) `elem` bnames || x == y = do sc 1; return []
175 | injective tx && not (holeIn env y || y `elem` holes)
176 = unifyTmpFail tx ty
177 | injective ty && not (holeIn env x || x `elem` holes)
178 = unifyTmpFail tx ty
179 un' fn bnames xtm@(P _ x _) tm
180 | holeIn env x || x `elem` holes
181 = do UI s f <- get
182 -- injectivity check
183 if (notP tm && fn)
184-- trace (show (x, tm, normalise ctxt env tm)) $
185-- put (UI s ((tm, topx, topy) : i) f)
186 then unifyTmpFail xtm tm
187 else do sc 1
188 checkCycle (x, tm)
189 | not (injective xtm) && injective tm = unifyFail xtm tm
190 un' fn bnames tm ytm@(P _ y _)
191 | holeIn env y || y `elem` holes
192 = do UI s f <- get
193 -- injectivity check
194 if (notP tm && fn)
195-- trace (show (y, tm, normalise ctxt env tm)) $
196-- put (UI s ((tm, topx, topy) : i) f)
197 then unifyTmpFail tm ytm
198 else do sc 1
199 checkCycle (y, tm)
200 | not (injective ytm) && injective tm = unifyFail ytm tm
201 un' fn bnames (V i) (P _ x _)
202 | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []
203 un' fn bnames (P _ x _) (V i)
204 | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []
206 un' fn bnames appx@(App fx ax) appy@(App fy ay)
207 | (injective fx && injective fy)
208 || (injective fx && rigid appx && metavarApp appy)
209 || (injective fy && rigid appy && metavarApp appx)
210 || (injective fx && metavarApp fy && ax == ay)
211 || (injective fy && metavarApp fx && ax == ay)
212 = do let (headx, _) = unApply fx
213 let (heady, _) = unApply fy
214 -- fail quickly if the heads are disjoint
215 checkHeads headx heady
216-- if True then -- (injective fx || injective fy || fx == fy) then
217-- if (injective fx && metavarApp appy) ||
218-- (injective fy && metavarApp appx) ||
219-- (injective fx && injective fy) || fx == fy
220 uplus
221 (do hf <- un' True bnames fx fy
222 let ax' = hnormalise hf ctxt env (substNames hf ax)
223 let ay' = hnormalise hf ctxt env (substNames hf ay)
224 ha <- un' False bnames ax' ay'
225 sc 1
226 combine bnames hf ha)
227 (do ha <- un' False bnames ax ay
228 let fx' = hnormalise ha ctxt env (substNames ha fx)
229 let fy' = hnormalise ha ctxt env (substNames ha fy)
230 hf <- un' False bnames fx' fy'
231 sc 1
232 combine bnames hf ha)
233 | otherwise = -- trace (show (appx, appy, injective fx, metavarApp appy, sameArgStruct appx appy)) $
234 do let (headx, argsx) = unApply appx
235 let (heady, argsy) = unApply appy
236 -- traceWhen (headx == heady) (show (appx, appy)) $
237 if (length argsx == length argsy &&
238 ((headx == heady && inenv headx) || (argsx == argsy) ||
239 (and (zipWith sameStruct (headx:argsx) (heady:argsy)))))
240 then
241-- (notFn headx && notFn heady))) then
242 do uf <- un' True bnames headx heady
243 unArgs uf argsx argsy
244 else -- trace ("TMPFAIL " ++ show (appx, appy, injective appx, injective appy)) $
245 unifyTmpFail appx appy
246 where hnormalise [] _ _ t = t
247 hnormalise ns ctxt env t = normalise ctxt env t
248 checkHeads (P (DCon _ _) x _) (P (DCon _ _) y _)
249 | x /= y = unifyFail appx appy
250 checkHeads (P (TCon _ _) x _) (P (TCon _ _) y _)
251 | x /= y = unifyFail appx appy
252 checkHeads (P (DCon _ _) x _) (P (TCon _ _) y _)
253 = unifyFail appx appy
254 checkHeads (P (TCon _ _) x _) (P (DCon _ _) y _)
255 = unifyFail appx appy
256 checkHeads _ _ = return []
258 unArgs as [] [] = return as
259 unArgs as (x : xs) (y : ys)
260 = do let x' = hnormalise as ctxt env (substNames as x)
261 let y' = hnormalise as ctxt env (substNames as y)
262 as' <- un' False bnames x' y'
263 vs <- combine bnames as as'
264 unArgs vs xs ys
266 metavarApp tm = let (f, args) = unApply tm in
267 all (\x -> metavar x) (f : args)
268 metavarArgs tm = let (f, args) = unApply tm in
269 all (\x -> metavar x || inenv x) args
270 metavarApp' tm = let (f, args) = unApply tm in
271 all (\x -> pat x || metavar x) (f : args)
273 sameArgStruct appx appy
274 = let (_, ax) = unApply appx
275 (_, ay) = unApply appy in
276 length ax == length ay &&
277 and (zipWith sameStruct ax ay)
279 sameStruct fapp@(App f x) gapp@(App g y)
280 = let (f',a') = unApply fapp
281 (g',b') = unApply gapp in
282 (f' == g' && length a' == length b' &&
283 (injective f' || injective g'))
284 || (sameStruct f g && sameStruct x y)
285 sameStruct (P _ x _) (P _ y _) = True
286 sameStruct (V i) (V j) = i == j
287 sameStruct (Constant x) (Constant y) = True
288 sameStruct (P _ _ _) (Constant y) = True
289 sameStruct (Constant x) (P _ _ _) = True
290 sameStruct (Bind n t sc) (P _ _ _) = True
291 sameStruct (P _ _ _) (Bind n t sc) = True
292 sameStruct (Bind n t sc) (Bind n' t' sc') = sameStruct sc sc'
293 sameStruct _ _ = False
295 rigid (P (DCon _ _) _ _) = True
296 rigid (P (TCon _ _) _ _) = True
297 rigid t@(P Ref _ _) = inenv t
298 rigid (Constant _) = True
299 rigid (App f a) = rigid f && rigid a
300 rigid t = not (metavar t)
302 metavar t = case t of
303 P _ x _ -> (x `elem` holes || holeIn env x) &&
304 not (x `elem` dont)
305 _ -> False
306 pat t = case t of
307 P _ x _ -> x `elem` holes || patIn env x
308 _ -> False
309 inenv t = case t of
310 P _ x _ -> x `elem` (map fst env)
311 _ -> False
313 notFn t = injective t || metavar t || inenv t
315 un' fn bnames x (Bind n (Lam t) (App y (P Bound n' _)))
316 | n == n' = un' False bnames x y
317 un' fn bnames (Bind n (Lam t) (App x (P Bound n' _))) y
318 | n == n' = un' False bnames x y
319 un' fn bnames x (Bind n (Lam t) (App y (V 0)))
320 = un' False bnames x y
321 un' fn bnames (Bind n (Lam t) (App x (V 0))) y
322 = un' False bnames x y
323-- un' fn bnames (Bind x (PVar _) sx) (Bind y (PVar _) sy)
324-- = un' False ((x,y):bnames) sx sy
325-- un' fn bnames (Bind x (PVTy _) sx) (Bind y (PVTy _) sy)
326-- = un' False ((x,y):bnames) sx sy
327 un' fn bnames (Bind x bx sx) (Bind y by sy)
328 = do h1 <- uB bnames bx by
329 h2 <- un' False ((x,y):bnames) sx sy
330 combine bnames h1 h2
331 un' fn bnames x y
332 | OK True <- convEq' ctxt x y = do sc 1; return []
333 | otherwise = do UI s f <- get
334 let r = recoverable x y
335 let err = CantUnify r
336 topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s
337 if (not r) then lift $ tfail err
338 else do put (UI s ((x, y, env, err) : f))
339 return [] -- lift $ tfail err
341 unifyTmpFail x y
342 = do UI s f <- get
343 let r = recoverable x y
344 let err = CantUnify r
345 topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s
346 put (UI s ((x, y, env, err) : f))
347 return []
349 -- shortcut failure, if we *know* nothing can fix it
350 unifyFail x y = do UI s f <- get
351 let r = recoverable x y
352 let err = CantUnify r
353 topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s
354 put (UI s ((x, y, env, err) : f))
355 lift $ tfail err
358 uB bnames (Let tx vx) (Let ty vy)
359 = do h1 <- un' False bnames tx ty
360 h2 <- un' False bnames ty vy
361 sc 1
362 combine bnames h1 h2
363 uB bnames (Guess tx vx) (Guess ty vy)
364 = do h1 <- un' False bnames tx ty
365 h2 <- un' False bnames ty vy
366 sc 1
367 combine bnames h1 h2
368 uB bnames (Lam tx) (Lam ty) = do sc 1; un' False bnames tx ty
369 uB bnames (Pi tx) (Pi ty) = do sc 1; un' False bnames tx ty
370 uB bnames (Hole tx) (Hole ty) = un' False bnames tx ty
371 uB bnames (PVar tx) (PVar ty) = un' False bnames tx ty
372 uB bnames x y = do UI s f <- get
373 let r = recoverable (binderTy x) (binderTy y)
374 let err = CantUnify r topx topy
375 (CantUnify r (binderTy x) (binderTy y) (Msg "") [] s)
376 (errEnv env) s
377 put (UI s ((binderTy x, binderTy y, env, err) : f))
378 return [] -- lift $ tfail err
380 checkCycle p@(x, P _ _ _) = return [p]
381 checkCycle (x, tm)
382 | not (x `elem` freeNames tm) = return [(x, tm)]
383 | otherwise = lift $ tfail (InfiniteUnify x tm (errEnv env))
386 combineArgs bnames args = ca [] args where
387 ca acc [] = return acc
388 ca acc (x : xs) = do x' <- combine bnames acc x
389 ca x' xs
391 combine bnames as [] = return as
392 combine bnames as ((n, t) : bs)
393 = case lookup n as of
394 Nothing -> combine bnames (as ++ [(n,t)]) bs
395 Just t' -> do ns <- un' False bnames t t'
396 -- make sure there's n mapping from n in ns
397 let ns' = filter (\ (x, _) -> x/=n) ns
398 sc 1
399 combine bnames as (ns' ++ bs)
401-- If there are any clashes of constructors, deem it unrecoverable, otherwise some
402-- more work may help.
403-- FIXME: Depending on how overloading gets used, this may cause problems. Better
404-- rethink overloading properly...
406recoverable (P (DCon _ _) x _) (P (DCon _ _) y _)
407 | x == y = True
408 | otherwise = False
409recoverable (P (TCon _ _) x _) (P (TCon _ _) y _)
410 | x == y = True
411 | otherwise = False
412recoverable (Constant _) (P (DCon _ _) y _) = False
413recoverable (P (DCon _ _) x _) (Constant _) = False
414recoverable (Constant _) (P (TCon _ _) y _) = False
415recoverable (P (TCon _ _) x _) (Constant _) = False
416recoverable (P (DCon _ _) x _) (P (TCon _ _) y _) = False
417recoverable (P (TCon _ _) x _) (P (DCon _ _) y _) = False
418recoverable p@(Constant _) (App f a) = recoverable p f
419recoverable (App f a) p@(Constant _) = recoverable f p
420recoverable p@(P _ n _) (App f a) = recoverable p f
421-- recoverable (App f a) p@(P _ _ _) = recoverable f p
422recoverable (App f a) (App f' a')
423 = recoverable f f' -- && recoverable a a'
424recoverable _ _ = True
426errEnv = map (\(x, b) -> (x, binderTy b))
428holeIn :: Env -> Name -> Bool
429holeIn env n = case lookup n env of
430 Just (Hole _) -> True
431 Just (Guess _ _) -> True
432 _ -> False
434patIn :: Env -> Name -> Bool
435patIn env n = case lookup n env of
436 Just (PVar _) -> True
437 Just (PVTy _) -> True
438 _ -> False