git.iko.soy/Idris-dev
on 7afa310 help sign in
Idris-dev/src/Idris/Core/Unify.hs
682 lines 30 kB history raw
1{-# LANGUAGE PatternGuards #-}
3module Idris.Core.Unify(match_unify, unify, Fails, FailContext(..), FailAt(..),
4 unrecoverable) where
6import Idris.Core.TT
7import Idris.Core.Evaluate
9import Control.Monad
10import Control.Monad.State.Strict
11import Data.List
12import Debug.Trace
14-- Unification is applied inside the theorem prover. We're looking for holes
15-- which can be filled in, by matching one term's normal form against another.
16-- Returns a list of hole names paired with the term which solves them, and
17-- a list of things which need to be injective.
19-- terms which need to be injective, with the things we're trying to unify
20-- at the time
22data FailAt = Match | Unify
23 deriving (Show, Eq)
25data FailContext = FailContext { fail_sourceloc :: FC,
26 fail_fn :: Name,
27 fail_param :: Name
28 }
29 deriving (Eq, Show)
31type Injs = [(TT Name, TT Name, TT Name)]
32type Fails = [(TT Name, TT Name, Env, Err, [FailContext], FailAt)]
34unrecoverable :: Fails -> Bool
35unrecoverable = any bad
36 where bad (_,_,_, err, _, _) = unrec err
38 unrec (CantUnify r _ _ _ _ _) = not r
39 unrec (At _ e) = unrec e
40 unrec (Elaborating _ _ e) = unrec e
41 unrec (ElaboratingArg _ _ _ e) = unrec e
42 unrec _ = False
44data UInfo = UI Int Fails
45 deriving Show
47data UResult a = UOK a
48 | UPartOK a
49 | UFail Err
51-- | Smart constructor for unification errors that takes into account the FailContext
52cantUnify :: [FailContext] -> Bool -> t -> t -> (Err' t) -> [(Name, t)] -> Int -> Err' t
53cantUnify [] r t1 t2 e ctxt i = CantUnify r t1 t2 e ctxt i
54cantUnify (FailContext fc f x : prev) r t1 t2 e ctxt i =
55 At fc (ElaboratingArg f x
56 (map (\(FailContext _ f' x') -> (f', x')) prev)
57 (CantUnify r t1 t2 e ctxt i))
59-- Solve metavariables by matching terms against each other
60-- Not really unification, of course!
62match_unify :: Context -> Env -> TT Name -> TT Name -> [Name] -> [Name] -> [FailContext] ->
63 TC [(Name, TT Name)]
64match_unify ctxt env topx topy inj holes from =
65 case runStateT (un [] (renameBindersTm env topx)
66 (renameBindersTm env topy)) (UI 0 []) of
67 OK (v, UI _ []) -> return (map (renameBinders env) (trimSolutions v))
68 res ->
69 let topxn = renameBindersTm env (normalise ctxt env topx)
70 topyn = renameBindersTm env (normalise ctxt env topy) in
71 case runStateT (un [] topxn topyn)
72 (UI 0 []) of
73 OK (v, UI _ fails) ->
74 return (map (renameBinders env) (trimSolutions v))
75 Error e ->
76 -- just normalise the term we're matching against
77 case runStateT (un [] topxn topy)
78 (UI 0 []) of
79 OK (v, UI _ fails) ->
80 return (map (renameBinders env) (trimSolutions v))
81 _ -> tfail e
82 where
83 -- This rule is highly dubious... it certainly produces a valid answer
84 -- but it scares me. However, matching is never guaranteed to give a unique
85 -- answer, merely a valid one, so perhaps we're okay.
86 -- In other words: it may vanish without warning some day :)
87 un :: [((Name, Name), TT Name)] -> TT Name -> TT Name ->
88 StateT UInfo
89 TC [(Name, TT Name)]
91 un names x tm@(App (P _ f (Bind fn (Pi t _) sc)) a)
92 | (P (DCon _ _ _) _ _, _) <- unApply x,
93 holeIn env f || f `elem` holes
94 = let n' = uniqueName (sMN 0 "mv") (map fst env) in
95 checkCycle names (f, Bind n' (Lam t) x)
96 un names tm@(App (P _ f (Bind fn (Pi t _) sc)) a) x
97 | (P (DCon _ _ _) _ _, _) <- unApply x,
98 holeIn env f || f `elem` holes
99 = let n' = uniqueName fn (map fst env) in
100 checkCycle names (f, Bind n' (Lam t) x)
102 un names tx@(P _ x _) tm
103 | tx /= tm && holeIn env x || x `elem` holes
104 = do sc 1; checkCycle names (x, tm)
105 un names tm ty@(P _ y _)
106 | ty /= tm && holeIn env y || y `elem` holes
107 = do sc 1; checkCycle names (y, tm)
108 un bnames (V i) (P _ x _)
109 | length bnames > i,
110 fst (fst (bnames!!i)) == x ||
111 snd (fst (bnames!!i)) == x = do sc 1; return []
112 un bnames (P _ x _) (V i)
113 | length bnames > i,
114 fst (fst (bnames!!i)) == x ||
115 snd (fst (bnames!!i)) == x = do sc 1; return []
116 un bnames (Bind x bx sx) (Bind y by sy) | notHole bx && notHole by
117 = do h1 <- uB bnames bx by
118 h2 <- un (((x, y), binderTy bx) : bnames) sx sy
119 combine bnames h1 h2
120 un names (App fx ax) (App fy ay)
121 = do hf <- un names fx fy
122 ha <- un names ax ay
123 combine names hf ha
124 un names x y
125 | OK True <- convEq' ctxt holes x y = do sc 1; return []
126 | otherwise = do UI s f <- get
127 let r = recoverable (normalise ctxt env x)
128 (normalise ctxt env y)
129 let err = cantUnify from r
130 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s
131 if (not r) then lift $ tfail err
132 else do put (UI s ((x, y, env, err, from, Match) : f))
133 lift $ tfail err
136 uB bnames (Let tx vx) (Let ty vy) = do h1 <- un bnames tx ty
137 h2 <- un bnames vx vy
138 combine bnames h1 h2
139 uB bnames (Lam tx) (Lam ty) = un bnames tx ty
140 uB bnames (Pi tx _) (Pi ty _) = un bnames tx ty
141 uB bnames x y = do UI s f <- get
142 let r = recoverable (normalise ctxt env (binderTy x))
143 (normalise ctxt env (binderTy y))
144 let err = cantUnify from r topx topy
145 (CantUnify r (binderTy x) (binderTy y) (Msg "") (errEnv env) s)
146 (errEnv env) s
147 put (UI s ((binderTy x, binderTy y, env, err, from, Match) : f))
148 return []
150 notHole (Hole _) = False
151 notHole _ = True
153 -- TODO: there's an annoying amount of repetition between this and the
154 -- main unification function. Consider lifting it out.
156 sc i = do UI s f <- get
157 put (UI (s+i) f)
159 unifyFail x y = do UI s f <- get
160 let r = recoverable (normalise ctxt env x)
161 (normalise ctxt env y)
162 let err = cantUnify from r
163 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s
164 put (UI s ((x, y, env, err, from, Match) : f))
165 lift $ tfail err
166 combine bnames as [] = return as
167 combine bnames as ((n, t) : bs)
168 = case lookup n as of
169 Nothing -> combine bnames (as ++ [(n,t)]) bs
170 Just t' -> do ns <- un bnames t t'
171 let ns' = filter (\ (x, _) -> x/=n) ns
172 sc 1
173 combine bnames as (ns' ++ bs)
175-- substN n tm (var, sol) = (var, subst n tm sol)
177 checkCycle ns p@(x, P _ x' _) | x == x' = return []
178 checkCycle ns p@(x, P _ _ _) = return [p]
179 checkCycle ns (x, tm)
180 | not (x `elem` freeNames tm) = checkScope ns (x, tm)
181 | otherwise = lift $ tfail (InfiniteUnify x tm (errEnv env))
183 checkScope ns (x, tm) =
184-- case boundVs (envPos x 0 env) tm of
185-- [] -> return [(x, tm)]
186-- (i:_) -> lift $ tfail (UnifyScope x (fst (fst (ns!!i)))
187-- (inst ns tm) (errEnv env))
188 let v = highV (-1) tm in
189 if v >= length ns
190 then lift $ tfail (Msg "SCOPE ERROR")
191 else return [(x, bind v ns tm)]
192 where inst [] tm = tm
193 inst ((n, _) : ns) tm = inst ns (substV (P Bound n Erased) tm)
195 bind i ns tm
196 | i < 0 = tm
197 | otherwise = let ((x,y),ty) = ns!!i in
198 App (Bind y (Lam ty) (bind (i-1) ns tm))
199 (P Bound x ty)
201renameBinders env (x, t) = (x, renameBindersTm env t)
203renameBindersTm :: Env -> TT Name -> TT Name
204renameBindersTm env tm = uniqueBinders (map fst env) tm
205 where
206 uniqueBinders env (Bind n b sc)
207 | n `elem` env
208 = let n' = uniqueName n env in
209 explicitHole $ Bind n' (fmap (uniqueBinders env) b)
210 (uniqueBinders (n':env) (rename n n' sc))
211 | otherwise = Bind n (fmap (uniqueBinders (n:env)) b)
212 (uniqueBinders (n:env) sc)
213 uniqueBinders env (App f a) = App (uniqueBinders env f) (uniqueBinders env a)
214 uniqueBinders env t = t
216 rename n n' (P nt x ty) | n == x = P nt n' ty
217 rename n n' (Bind x b sc) = Bind x (fmap (rename n n') b) (rename n n' sc)
218 rename n n' (App f a) = App (rename n n' f) (rename n n' a)
219 rename n n' t = t
221 explicitHole (Bind n (Hole ty) sc)
222 = Bind n (Hole ty) (instantiate (P Bound n ty) sc)
223 explicitHole t = t
225trimSolutions ns = dropPairs ns
226 where dropPairs [] = []
227 dropPairs (n@(x, P _ x' _) : ns)
228 | x == x' = dropPairs ns
229 | otherwise
230 = n : dropPairs
231 (filter (\t -> case t of
232 (n, P _ n' _) -> not (n == x' && n' == x)
233 _ -> True) ns)
234 dropPairs (n : ns) = n : dropPairs ns
236expandLets env (x, tm) = (x, doSubst (reverse env) tm)
237 where
238 doSubst [] tm = tm
239 doSubst ((n, Let v t) : env) tm
240 = doSubst env (subst n v tm)
241 doSubst (_ : env) tm
242 = doSubst env tm
244hasv :: TT Name -> Bool
245hasv (V x) = True
246hasv (App f a) = hasv f || hasv a
247hasv (Bind x b sc) = hasv (binderTy b) || hasv sc
248hasv _ = False
250unify :: Context -> Env -> TT Name -> TT Name ->
251 [Name] -> [Name] -> [Name] -> [FailContext] ->
252 TC ([(Name, TT Name)], Fails)
253unify ctxt env topx topy inj holes usersupp from =
254-- traceWhen (hasv topx || hasv topy)
255-- ("Unifying " ++ show topx ++ "\nAND\n" ++ show topy ++ "\n") $
256 -- don't bother if topx and topy are different at the head
257 case runStateT (un False [] (renameBindersTm env topx)
258 (renameBindersTm env topy)) (UI 0 []) of
259 OK (v, UI _ []) -> return (map (renameBinders env) (trimSolutions v),
260 [])
261 res ->
262 let topxn = renameBindersTm env (normalise ctxt env topx)
263 topyn = renameBindersTm env (normalise ctxt env topy) in
264-- trace ("Unifying " ++ show (topx, topy) ++ "\n\n==>\n" ++ show (topxn, topyn) ++ "\n\n" ++ show res ++ "\n\n") $
265 case runStateT (un False [] topxn topyn)
266 (UI 0 []) of
267 OK (v, UI _ fails) ->
268 return (map (renameBinders env) (trimSolutions v),
269 reverse fails)
270-- Error e@(CantUnify False _ _ _ _ _) -> tfail e
271 Error e -> tfail e
272 where
273 headDiff (P (DCon _ _ _) x _) (P (DCon _ _ _) y _) = x /= y
274 headDiff (P (TCon _ _) x _) (P (TCon _ _) y _) = x /= y
275 headDiff _ _ = False
277 injective (P (DCon _ _ _) _ _) = True
278 injective (P (TCon _ _) _ _) = True
279-- injective (App f (P _ _ _)) = injective f
280-- injective (App f (Constant _)) = injective f
281 injective (App f a) = injective f -- && injective a
282 injective _ = False
284-- injectiveVar (P _ (MN _ _) _) = True -- TMP HACK
285 injectiveVar (P _ n _) = n `elem` inj
286 injectiveVar (App f a) = injectiveVar f -- && injective a
287 injectiveVar _ = False
289 injectiveApp x = injective x || injectiveVar x
291 notP (P _ _ _) = False
292 notP _ = True
294 sc i = do UI s f <- get
295 put (UI (s+i) f)
297 errors :: StateT UInfo TC Bool
298 errors = do UI s f <- get
299 return (not (null f))
301 uplus u1 u2 = do UI s f <- get
302 r <- u1
303 UI s f' <- get
304 if (length f == length f')
305 then return r
306 else do put (UI s f); u2
308 un :: Bool -> [((Name, Name), TT Name)] -> TT Name -> TT Name ->
309 StateT UInfo
310 TC [(Name, TT Name)]
311 un = un'
312-- un fn names x y
313-- = let (xf, _) = unApply x
314-- (yf, _) = unApply y in
315-- if headDiff xf yf then unifyFail x y else
316-- uplus (un' fn names x y)
317-- (un' fn names (hnf ctxt env x) (hnf ctxt env y))
319 un' :: Bool -> [((Name, Name), TT Name)] -> TT Name -> TT Name ->
320 StateT UInfo
321 TC [(Name, TT Name)]
322 un' fn names x y | x == y = return [] -- shortcut
323 un' fn names topx@(P (DCon _ _ _) x _) topy@(P (DCon _ _ _) y _)
324 | x /= y = unifyFail topx topy
325 un' fn names topx@(P (TCon _ _) x _) topy@(P (TCon _ _) y _)
326 | x /= y = unifyFail topx topy
327 un' fn names topx@(P (DCon _ _ _) x _) topy@(P (TCon _ _) y _)
328 = unifyFail topx topy
329 un' fn names topx@(P (TCon _ _) x _) topy@(P (DCon _ _ _) y _)
330 = unifyFail topx topy
331 un' fn names topx@(Constant _) topy@(P (TCon _ _) y _)
332 = unifyFail topx topy
333 un' fn names topx@(P (TCon _ _) x _) topy@(Constant _)
334 = unifyFail topx topy
335 un' fn bnames tx@(P _ x _) ty@(P _ y _)
336 | (x,y) `elem` map fst bnames || x == y = do sc 1; return []
337 | injective tx && not (holeIn env y || y `elem` holes)
338 = unifyTmpFail tx ty
339 | injective ty && not (holeIn env x || x `elem` holes)
340 = unifyTmpFail tx ty
341 -- pick the one bound earliest if both are holes
342 | tx /= ty && (holeIn env x || x `elem` holes)
343 && (holeIn env y || y `elem` holes)
344 = case compare (envPos 0 x env) (envPos 0 y env) of
345 LT -> do sc 1; checkCycle bnames (x, ty)
346 _ -> do sc 1; checkCycle bnames (y, tx)
347 where envPos i n ((n',_):env) | n == n' = i
348 envPos i n (_:env) = envPos (i+1) n env
349 envPos _ _ _ = 100000
350 un' fn bnames xtm@(P _ x _) tm
351 | pureTerm tm, holeIn env x || x `elem` holes
352 = do UI s f <- get
353 -- injectivity check
354 x <- checkCycle bnames (x, tm)
355 if (notP tm && fn)
356-- trace (show (x, tm, normalise ctxt env tm)) $
357-- put (UI s ((tm, topx, topy) : i) f)
358 then unifyTmpFail xtm tm
359 else do sc 1
360 return x
361 | pureTerm tm, not (injective xtm) && injective tm
362 = do checkCycle bnames (x, tm)
363 unifyTmpFail xtm tm
364 un' fn bnames tm ytm@(P _ y _)
365 | pureTerm tm, holeIn env y || y `elem` holes
366 = do UI s f <- get
367 -- injectivity check
368 x <- checkCycle bnames (y, tm)
369 if (notP tm && fn)
370-- trace (show (y, tm, normalise ctxt env tm)) $
371-- put (UI s ((tm, topx, topy) : i) f)
372 then unifyTmpFail tm ytm
373 else do sc 1
374 return x
375 | pureTerm tm, not (injective ytm) && injective tm
376 = do checkCycle bnames (y, tm)
377 unifyTmpFail tm ytm
378 un' fn bnames (V i) (P _ x _)
379 | length bnames > i,
380 fst ((map fst bnames)!!i) == x ||
381 snd ((map fst bnames)!!i) == x = do sc 1; return []
382 un' fn bnames (P _ x _) (V i)
383 | length bnames > i,
384 fst ((map fst bnames)!!i) == x ||
385 snd ((map fst bnames)!!i) == x = do sc 1; return []
387 un' fn names topx@(Bind n (Hole t) sc) y = unifyTmpFail topx y
388 un' fn names x topy@(Bind n (Hole t) sc) = unifyTmpFail x topy
390 un' fn bnames appx@(App _ _) appy@(App _ _)
391 = unApp fn bnames appx appy
392-- = uplus (unApp fn bnames appx appy)
393-- (unifyTmpFail appx appy) -- take the whole lot
395 un' fn bnames x (Bind n (Lam t) (App y (P Bound n' _)))
396 | n == n' = un' False bnames x y
397 un' fn bnames (Bind n (Lam t) (App x (P Bound n' _))) y
398 | n == n' = un' False bnames x y
399 un' fn bnames x (Bind n (Lam t) (App y (V 0)))
400 = un' False bnames x y
401 un' fn bnames (Bind n (Lam t) (App x (V 0))) y
402 = un' False bnames x y
403-- un' fn bnames (Bind x (PVar _) sx) (Bind y (PVar _) sy)
404-- = un' False ((x,y):bnames) sx sy
405-- un' fn bnames (Bind x (PVTy _) sx) (Bind y (PVTy _) sy)
406-- = un' False ((x,y):bnames) sx sy
408 -- f D unifies with t -> D. This is dubious, but it helps with type
409 -- class resolution for type classes over functions.
411 un' fn bnames (App f x) (Bind n (Pi t k) y)
412 | noOccurrence n y && injectiveApp f
413 = do ux <- un' False bnames x y
414 uf <- un' False bnames f (Bind (sMN 0 "uv") (Lam (TType (UVar 0)))
415 (Bind n (Pi t k) (V 1)))
416 combine bnames ux uf
418 un' fn bnames (Bind n (Pi t k) y) (App f x)
419 | noOccurrence n y && injectiveApp f
420 = do ux <- un' False bnames y x
421 uf <- un' False bnames (Bind (sMN 0 "uv") (Lam (TType (UVar 0)))
422 (Bind n (Pi t k) (V 1))) f
423 combine bnames ux uf
425 un' fn bnames (Bind x bx sx) (Bind y by sy)
426 | sameBinder bx by
427 = do h1 <- uB bnames bx by
428 h2 <- un' False (((x,y),binderTy bx):bnames) sx sy
429 combine bnames h1 h2
430 where sameBinder (Lam _) (Lam _) = True
431 sameBinder (Pi _ _) (Pi _ _) = True
432 sameBinder _ _ = False
433 un' fn bnames x y
434 | OK True <- convEq' ctxt holes x y = do sc 1; return []
435 | isUniverse x && isUniverse y = do sc 1; return []
436 | otherwise = do UI s f <- get
437 let r = recoverable (normalise ctxt env x)
438 (normalise ctxt env y)
439 let err = cantUnify from r
440 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s
441 if (not r) then lift $ tfail err
442 else do put (UI s ((x, y, env, err, from, Unify) : f))
443 return [] -- lift $ tfail err
445 unApp fn bnames appx@(App fx ax) appy@(App fy ay)
446 | (injectiveApp fx && injectiveApp fy)
447 || (injectiveApp fx && metavarApp fy && ax == ay)
448 || (injectiveApp fy && metavarApp fx && ax == ay)
449 = do let (headx, _) = unApply fx
450 let (heady, _) = unApply fy
451 -- fail quickly if the heads are disjoint
452 checkHeads headx heady
453 uplus
454 (do hf <- un' True bnames fx fy
455 let ax' = hnormalise hf ctxt env (substNames hf ax)
456 let ay' = hnormalise hf ctxt env (substNames hf ay)
457 ha <- un' False bnames ax' ay'
458 sc 1
459 combine bnames hf ha)
460 (do ha <- un' False bnames ax ay
461 let fx' = hnormalise ha ctxt env (substNames ha fx)
462 let fy' = hnormalise ha ctxt env (substNames ha fy)
463 hf <- un' False bnames fx' fy'
464 sc 1
465 combine bnames hf ha)
466 | otherwise = unifyTmpFail appx appy
467 where hnormalise [] _ _ t = t
468 hnormalise ns ctxt env t = normalise ctxt env t
469 checkHeads (P (DCon _ _ _) x _) (P (DCon _ _ _) y _)
470 | x /= y = unifyFail appx appy
471 checkHeads (P (TCon _ _) x _) (P (TCon _ _) y _)
472 | x /= y = unifyFail appx appy
473 checkHeads (P (DCon _ _ _) x _) (P (TCon _ _) y _)
474 = unifyFail appx appy
475 checkHeads (P (TCon _ _) x _) (P (DCon _ _ _) y _)
476 = unifyFail appx appy
477 checkHeads _ _ = return []
479 unArgs as [] [] = return as
480 unArgs as (x : xs) (y : ys)
481 = do let x' = hnormalise as ctxt env (substNames as x)
482 let y' = hnormalise as ctxt env (substNames as y)
483 as' <- un' False bnames x' y'
484 vs <- combine bnames as as'
485 unArgs vs xs ys
487 numArgs tm = let (f, args) = unApply tm in length args
489 metavarApp tm = let (f, args) = unApply tm in
490 (metavar f &&
491 all (\x -> metavarApp x) args
492 && nub args == args) ||
493 globmetavar tm
494 metavarArgs tm = let (f, args) = unApply tm in
495 all (\x -> metavar x || inenv x) args
496 && nub args == args
497 metavarApp' tm = let (f, args) = unApply tm in
498 all (\x -> pat x || metavar x) (f : args)
499 && nub args == args
501 rigid (P (DCon _ _ _) _ _) = True
502 rigid (P (TCon _ _) _ _) = True
503 rigid t@(P Ref _ _) = inenv t || globmetavar t
504 rigid (Constant _) = True
505 rigid (App f a) = rigid f && rigid a
506 rigid t = not (metavar t) || globmetavar t
508 globmetavar t = case unApply t of
509 (P _ x _, _) ->
510 case lookupDef x ctxt of
511 [TyDecl _ _] -> True
512 _ -> False
513 _ -> False
515 metavar t = case t of
516 P _ x _ -> (x `notElem` usersupp &&
517 (x `elem` holes || holeIn env x))
518 || globmetavar t
519 _ -> False
520 pat t = case t of
521 P _ x _ -> x `elem` holes || patIn env x
522 _ -> False
523 inenv t = case t of
524 P _ x _ -> x `elem` (map fst env)
525 _ -> False
527 notFn t = injective t || metavar t || inenv t
530 unifyTmpFail :: Term -> Term -> StateT UInfo TC [(Name, TT Name)]
531 unifyTmpFail x y
532 = do UI s f <- get
533 let r = recoverable (normalise ctxt env x) (normalise ctxt env y)
534 let err = cantUnify from r
535 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s
536 put (UI s ((topx, topy, env, err, from, Unify) : f))
537 return []
539 -- shortcut failure, if we *know* nothing can fix it
540 unifyFail x y = do UI s f <- get
541 let r = recoverable (normalise ctxt env x) (normalise ctxt env y)
542 let err = cantUnify from r
543 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s
544 put (UI s ((topx, topy, env, err, from, Unify) : f))
545 lift $ tfail err
548 uB bnames (Let tx vx) (Let ty vy)
549 = do h1 <- un' False bnames tx ty
550 h2 <- un' False bnames vx vy
551 sc 1
552 combine bnames h1 h2
553 uB bnames (Guess tx vx) (Guess ty vy)
554 = do h1 <- un' False bnames tx ty
555 h2 <- un' False bnames vx vy
556 sc 1
557 combine bnames h1 h2
558 uB bnames (Lam tx) (Lam ty) = do sc 1; un' False bnames tx ty
559 uB bnames (Pi tx _) (Pi ty _) = do sc 1; un' False bnames tx ty
560 uB bnames (Hole tx) (Hole ty) = un' False bnames tx ty
561 uB bnames (PVar tx) (PVar ty) = un' False bnames tx ty
562 uB bnames x y = do UI s f <- get
563 let r = recoverable (normalise ctxt env (binderTy x))
564 (normalise ctxt env (binderTy y))
565 let err = cantUnify from r topx topy
566 (CantUnify r (binderTy x) (binderTy y) (Msg "") (errEnv env) s)
567 (errEnv env) s
568 put (UI s ((binderTy x, binderTy y, env, err, from, Unify) : f))
569 return [] -- lift $ tfail err
571 checkCycle ns p@(x, P _ _ _) = return [p]
572 checkCycle ns (x, tm)
573 | not (x `elem` freeNames tm) = checkScope ns (x, tm)
574 | otherwise = lift $ tfail (InfiniteUnify x tm (errEnv env))
576 checkScope ns (x, tm) | pureTerm tm =
577-- case boundVs (envPos x 0 env) tm of
578-- [] -> return [(x, tm)]
579-- (i:_) -> lift $ tfail (UnifyScope x (fst (fst (ns!!i)))
580-- (inst ns tm) (errEnv env))
581 let v = highV (-1) tm in
582 if v >= length ns
583 then lift $ tfail (Msg "SCOPE ERROR")
584 else return [(x, bind v ns tm)]
585 where inst [] tm = tm
586 inst (((n, _), _) : ns) tm = inst ns (substV (P Bound n Erased) tm)
587 checkScope ns (x, tm) = lift $ tfail (Msg "HOLE ERROR")
589 bind i ns tm
590 | i < 0 = tm
591 | otherwise = let ((x,y),ty) = ns!!i in
592 App (Bind y (Lam ty) (bind (i-1) ns tm))
593 (P Bound x ty)
595 combineArgs bnames args = ca [] args where
596 ca acc [] = return acc
597 ca acc (x : xs) = do x' <- combine bnames acc x
598 ca x' xs
600 combine bnames as [] = return as
601 combine bnames as ((n, t) : bs)
602 = case lookup n as of
603 Nothing -> combine bnames (as ++ [(n,t)]) bs
604 Just t' -> do ns <- un' False bnames t t'
605 -- make sure there's n mapping from n in ns
606 let ns' = filter (\ (x, _) -> x/=n) ns
607 sc 1
608 combine bnames as (ns' ++ bs)
610boundVs :: Int -> Term -> [Int]
611boundVs i (V j) | j < i = []
612 | otherwise = [j]
613boundVs i (Bind n b sc) = boundVs (i + 1) sc
614boundVs i (App f x) = let fs = boundVs i f
615 xs = boundVs i x in
616 nub (fs ++ xs)
617boundVs i _ = []
619highV :: Int -> Term -> Int
620highV i (V j) | j > i = j
621 | otherwise = i
622highV i (Bind n b sc) = maximum [i, highV i (binderTy b), (highV i sc - 1)]
623highV i (App f x) = max (highV i f) (highV i x)
624highV i _ = i
626envPos x i [] = 0
627envPos x i ((y, _) : ys) | x == y = i
628 | otherwise = envPos x (i + 1) ys
631-- If there are any clashes of constructors, deem it unrecoverable, otherwise some
632-- more work may help.
633-- FIXME: Depending on how overloading gets used, this may cause problems. Better
634-- rethink overloading properly...
635-- ASSUMPTION: inputs are in normal form
637recoverable t@(App _ _) _
638 | (P _ (UN l) _, _) <- unApply t, l == txt "Lazy'" = False
639recoverable _ t@(App _ _)
640 | (P _ (UN l) _, _) <- unApply t, l == txt "Lazy'" = False
641recoverable (P (DCon _ _ _) x _) (P (DCon _ _ _) y _) = x == y
642recoverable (P (TCon _ _) x _) (P (TCon _ _) y _) = x == y
643recoverable (Constant _) (P (DCon _ _ _) y _) = False
644recoverable (Constant x) (Constant y) = x == y
645recoverable (P (DCon _ _ _) x _) (Constant _) = False
646recoverable (Constant _) (P (TCon _ _) y _) = False
647recoverable (P (TCon _ _) x _) (Constant _) = False
648recoverable (P (DCon _ _ _) x _) (P (TCon _ _) y _) = False
649recoverable (P (TCon _ _) x _) (P (DCon _ _ _) y _) = False
650recoverable p@(Constant _) (App f a) = recoverable p f
651recoverable (App f a) p@(Constant _) = recoverable f p
652recoverable p@(P _ n _) (App f a) = recoverable p f
653recoverable (App f a) p@(P _ _ _) = recoverable f p
654recoverable (App f a) (App f' a')
655 | f == f' = recoverable a a'
656recoverable (App f a) (App f' a')
657 = recoverable f f' -- && recoverable a a'
658recoverable f (Bind _ (Pi _ _) sc)
659 | (P (DCon _ _ _) _ _, _) <- unApply f = False
660 | (P (TCon _ _) _ _, _) <- unApply f = False
661recoverable (Bind _ (Pi _ _) sc) f
662 | (P (DCon _ _ _) _ _, _) <- unApply f = False
663 | (P (TCon _ _) _ _, _) <- unApply f = False
664recoverable (Bind _ (Lam _) sc) f = recoverable sc f
665recoverable f (Bind _ (Lam _) sc) = recoverable f sc
666recoverable x y = True
668errEnv :: [(a, Binder b)] -> [(a, b)]
669errEnv = map (\(x, b) -> (x, binderTy b))
671holeIn :: Env -> Name -> Bool
672holeIn env n = case lookup n env of
673 Just (Hole _) -> True
674 Just (Guess _ _) -> True
675 _ -> False
677patIn :: Env -> Name -> Bool
678patIn env n = case lookup n env of
679 Just (PVar _) -> True
680 Just (PVTy _) -> True
681 _ -> False