git.iko.soy/Idris-dev
on 54e4e41 help sign in
Idris-dev/src/Idris/Core/Unify.hs
743 lines 33 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, -- unification error
33 Bool, -- ready to retry yet
34 Env, Err, [FailContext], FailAt)]
36unrecoverable :: Fails -> Bool
37unrecoverable = any bad
38 where bad (_,_,_,_, err, _, _) = unrec err
40 unrec (CantUnify r _ _ _ _ _) = not r
41 unrec (At _ e) = unrec e
42 unrec (Elaborating _ _ e) = unrec e
43 unrec (ElaboratingArg _ _ _ e) = unrec e
44 unrec _ = False
46data UInfo = UI Int Fails
47 deriving Show
49data UResult a = UOK a
50 | UPartOK a
51 | UFail Err
53-- | Smart constructor for unification errors that takes into account the FailContext
54cantUnify :: [FailContext] -> Bool -> (t, Maybe Provenance) -> (t, Maybe Provenance) -> (Err' t) -> [(Name, t)] -> Int -> Err' t
55cantUnify [] r t1 t2 e ctxt i = CantUnify r t1 t2 e ctxt i
56cantUnify (FailContext fc f x : prev) r t1 t2 e ctxt i =
57 At fc (ElaboratingArg f x
58 (map (\(FailContext _ f' x') -> (f', x')) prev)
59 (CantUnify r t1 t2 e ctxt i))
61-- Solve metavariables by matching terms against each other
62-- Not really unification, of course!
64match_unify :: Context -> Env ->
65 (TT Name, Maybe Provenance) ->
66 (TT Name, Maybe Provenance) -> [Name] -> [Name] -> [FailContext] ->
67 TC [(Name, TT Name)]
68match_unify ctxt env (topx, xfrom) (topy, yfrom) inj holes from =
69 case runStateT (un [] (renameBindersTm env topx)
70 (renameBindersTm env topy)) (UI 0 []) of
71 OK (v, UI _ []) ->
72 do v' <- trimSolutions (topx, xfrom) (topy, yfrom) from env v
73 return (map (renameBinders env) v')
74 res ->
75 let topxn = renameBindersTm env (normalise ctxt env topx)
76 topyn = renameBindersTm env (normalise ctxt env topy) in
77 case runStateT (un [] topxn topyn)
78 (UI 0 []) of
79 OK (v, UI _ fails) ->
80 do v' <- trimSolutions (topx, xfrom) (topy, yfrom) from env v
81 return (map (renameBinders env) v')
82 Error e ->
83 -- just normalise the term we're matching against
84 case runStateT (un [] topxn topy)
85 (UI 0 []) of
86 OK (v, UI _ fails) ->
87 do v' <- trimSolutions (topx, xfrom) (topy, yfrom) from env v
88 return (map (renameBinders env) v')
89 _ -> tfail e
90 where
91 un :: [((Name, Name), TT Name)] -> TT Name -> TT Name ->
92 StateT UInfo
93 TC [(Name, TT Name)]
95 -- This rule is highly dubious... it certainly produces a valid answer
96 -- but it scares me. However, matching is never guaranteed to give a unique
97 -- answer, merely a valid one, so perhaps we're okay.
98 -- In other words: it may vanish without warning some day :)
99 un names x tm@(App _ (P _ f (Bind fn (Pi _ t _) sc)) a)
100 | (P (TCon _ _) _ _, _) <- unApply x,
101 holeIn env f || f `elem` holes
102 = let n' = uniqueName (sMN 0 "mv") (map fst env) in
103 checkCycle names (f, Bind n' (Lam t) x)
104 un names tm@(App _ (P _ f (Bind fn (Pi _ t _) sc)) a) x
105 | (P (TCon _ _) _ _, _) <- unApply x,
106 holeIn env f || f `elem` holes
107 = let n' = uniqueName fn (map fst env) in
108 checkCycle names (f, Bind n' (Lam t) x)
109 un names x tm@(App _ (P _ f (Bind fn (Pi _ t _) sc)) a)
110 | (P (DCon _ _ _) _ _, _) <- unApply x,
111 holeIn env f || f `elem` holes
112 = let n' = uniqueName (sMN 0 "mv") (map fst env) in
113 checkCycle names (f, Bind n' (Lam t) x)
114 un names tm@(App _ (P _ f (Bind fn (Pi _ t _) sc)) a) x
115 | (P (DCon _ _ _) _ _, _) <- unApply x,
116 holeIn env f || f `elem` holes
117 = let n' = uniqueName fn (map fst env) in
118 checkCycle names (f, Bind n' (Lam t) x)
120 un names tx@(P _ x _) tm
121 | tx /= tm && holeIn env x || x `elem` holes
122 = do sc 1; checkCycle names (x, tm)
123 un names tm ty@(P _ y _)
124 | ty /= tm && holeIn env y || y `elem` holes
125 = do sc 1; checkCycle names (y, tm)
126 un bnames (V i) (P _ x _)
127 | length bnames > i,
128 fst (fst (bnames!!i)) == x ||
129 snd (fst (bnames!!i)) == x = do sc 1; return []
130 un bnames (P _ x _) (V i)
131 | length bnames > i,
132 fst (fst (bnames!!i)) == x ||
133 snd (fst (bnames!!i)) == x = do sc 1; return []
134 un bnames (Bind x bx sx) (Bind y by sy) | notHole bx && notHole by
135 = do h1 <- uB bnames bx by
136 h2 <- un (((x, y), binderTy bx) : bnames) sx sy
137 combine bnames h1 h2
138 un names (App _ fx ax) (App _ fy ay)
139 = do hf <- un names fx fy
140 ha <- un names ax ay
141 combine names hf ha
142 un names x y
143 | OK True <- convEq' ctxt holes x y = do sc 1; return []
144 | otherwise = do UI s f <- get
145 let r = recoverable (normalise ctxt env x)
146 (normalise ctxt env y)
147 let err = cantUnify from r
148 (topx, xfrom) (topy, yfrom) (CantUnify r (x, Nothing) (y, Nothing) (Msg "") (errEnv env) s) (errEnv env) s
149 if (not r) then lift $ tfail err
150 else do put (UI s ((x, y, True, env, err, from, Match) : f))
151 lift $ tfail err
154 uB bnames (Let tx vx) (Let ty vy) = do h1 <- un bnames tx ty
155 h2 <- un bnames vx vy
156 combine bnames h1 h2
157 uB bnames (Lam tx) (Lam ty) = un bnames tx ty
158 uB bnames (Pi i tx _) (Pi i' ty _) = un bnames tx ty
159 uB bnames x y = do UI s f <- get
160 let r = recoverable (normalise ctxt env (binderTy x))
161 (normalise ctxt env (binderTy y))
162 let err = cantUnify from r (topx, xfrom) (topy, yfrom)
163 (CantUnify r (binderTy x, Nothing)
164 (binderTy y, Nothing) (Msg "") (errEnv env) s)
165 (errEnv env) s
166 put (UI s ((binderTy x, binderTy y,
167 False,
168 env, err, from, Match) : f))
169 return []
171 notHole (Hole _) = False
172 notHole _ = True
174 -- TODO: there's an annoying amount of repetition between this and the
175 -- main unification function. Consider lifting it out.
176 -- Issue #1721 on the issue tracker: https://github.com/idris-lang/Idris-dev/issues/1721
178 sc i = do UI s f <- get
179 put (UI (s+i) f)
181 unifyFail x y = do UI s f <- get
182 let r = recoverable (normalise ctxt env x)
183 (normalise ctxt env y)
184 let err = cantUnify from r
185 (topx, xfrom) (topy, yfrom)
186 (CantUnify r (x, Nothing) (y, Nothing) (Msg "") (errEnv env) s) (errEnv env) s
187 put (UI s ((x, y, True, env, err, from, Match) : f))
188 lift $ tfail err
189 combine bnames as [] = return as
190 combine bnames as ((n, t) : bs)
191 = case lookup n as of
192 Nothing -> combine bnames (as ++ [(n,t)]) bs
193 Just t' -> do ns <- un bnames t t'
194 let ns' = filter (\ (x, _) -> x/=n) ns
195 sc 1
196 combine bnames as (ns' ++ bs)
198-- substN n tm (var, sol) = (var, subst n tm sol)
200 checkCycle ns p@(x, P _ x' _) | x == x' = return []
201 checkCycle ns p@(x, P _ _ _) = return [p]
202 checkCycle ns (x, tm)
203 | not (x `elem` freeNames tm) = checkScope ns (x, tm)
204 | otherwise = lift $ tfail (InfiniteUnify x tm (errEnv env))
206 checkScope ns (x, tm) =
207-- case boundVs (envPos x 0 env) tm of
208-- [] -> return [(x, tm)]
209-- (i:_) -> lift $ tfail (UnifyScope x (fst (fst (ns!!i)))
210-- (inst ns tm) (errEnv env))
211 let v = highV (-1) tm in
212 if v >= length ns
213 then lift $ tfail (Msg "SCOPE ERROR")
214 else return [(x, bind v ns tm)]
215 where inst [] tm = tm
216 inst ((n, _) : ns) tm = inst ns (substV (P Bound n Erased) tm)
218 bind i ns tm
219 | i < 0 = tm
220 | otherwise = let ((x,y),ty) = ns!!i in
221 App MaybeHoles (Bind y (Lam ty) (bind (i-1) ns tm))
222 (P Bound x ty)
224renameBinders env (x, t) = (x, renameBindersTm env t)
226renameBindersTm :: Env -> TT Name -> TT Name
227renameBindersTm env tm = uniqueBinders (map fst env) tm
228 where
229 uniqueBinders env (Bind n b sc)
230 | n `elem` env
231 = let n' = uniqueName n env in
232 explicitHole $ Bind n' (fmap (uniqueBinders env) b)
233 (uniqueBinders (n':env) (rename n n' sc))
234 | otherwise = Bind n (fmap (uniqueBinders (n:env)) b)
235 (uniqueBinders (n:env) sc)
236 uniqueBinders env (App s f a) = App s (uniqueBinders env f) (uniqueBinders env a)
237 uniqueBinders env t = t
239 rename n n' (P nt x ty) | n == x = P nt n' ty
240 rename n n' (Bind x b sc) = Bind x (fmap (rename n n') b) (rename n n' sc)
241 rename n n' (App s f a) = App s (rename n n' f) (rename n n' a)
242 rename n n' t = t
244 explicitHole (Bind n (Hole ty) sc)
245 = Bind n (Hole ty) (instantiate (P Bound n ty) sc)
246 explicitHole t = t
248trimSolutions (topx, xfrom) (topy, yfrom) from env topns = followSols [] (dropPairs topns)
249 where dropPairs [] = []
250 dropPairs (n@(x, P _ x' _) : ns)
251 | x == x' = dropPairs ns
252 | otherwise
253 = n : dropPairs
254 (filter (\t -> case t of
255 (n, P _ n' _) -> not (n == x' && n' == x)
256 _ -> True) ns)
257 dropPairs (n : ns) = n : dropPairs ns
259 followSols vs [] = return []
260 followSols vs ((n, P _ t _) : ns)
261 | Just t' <- lookup t ns
262 = do vs' <- case t' of
263 P _ tn _ ->
264 if (n, tn) `elem` vs then -- cycle
265 tfail (cantUnify from False (topx, xfrom) (topy, yfrom)
266 (Msg "") (errEnv env) 0)
267 else return ((n, tn) : vs)
268 _ -> return vs
269 followSols vs' ((n, t') : ns)
270 followSols vs (n : ns) = do ns' <- followSols vs ns
271 return $ n : ns'
273expandLets env (x, tm) = (x, doSubst (reverse env) tm)
274 where
275 doSubst [] tm = tm
276 doSubst ((n, Let v t) : env) tm
277 = doSubst env (subst n v tm)
278 doSubst (_ : env) tm
279 = doSubst env tm
281hasv :: TT Name -> Bool
282hasv (V x) = True
283hasv (App _ f a) = hasv f || hasv a
284hasv (Bind x b sc) = hasv (binderTy b) || hasv sc
285hasv _ = False
287unify :: Context -> Env ->
288 (TT Name, Maybe Provenance) ->
289 (TT Name, Maybe Provenance) ->
290 [Name] -> [Name] -> [Name] -> [FailContext] ->
291 TC ([(Name, TT Name)], Fails)
292unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =
293-- traceWhen (hasv topx || hasv topy)
294-- ("Unifying " ++ show topx ++ "\nAND\n" ++ show topy ++ "\n") $
295 -- don't bother if topx and topy are different at the head
296 case runStateT (un False [] (renameBindersTm env topx)
297 (renameBindersTm env topy)) (UI 0 []) of
298 OK (v, UI _ []) -> do v' <- trimSolutions (topx, xfrom) (topy, yfrom) from env v
299 return (map (renameBinders env) v', [])
300 res ->
301 let topxn = renameBindersTm env (normalise ctxt env topx)
302 topyn = renameBindersTm env (normalise ctxt env topy) in
303-- trace ("Unifying " ++ show (topx, topy) ++ "\n\n==>\n" ++ show (topxn, topyn) ++ "\n\n") $
304 case runStateT (un False [] topxn topyn)
305 (UI 0 []) of
306 OK (v, UI _ fails) ->
307 do v' <- trimSolutions (topx, xfrom) (topy, yfrom) from env v
308-- trace ("OK " ++ show (topxn, topyn, v, holes)) $
309 return (map (renameBinders env) v', reverse fails)
310-- Error e@(CantUnify False _ _ _ _ _) -> tfail e
311 Error e -> tfail e
312 where
313 headDiff (P (DCon _ _ _) x _) (P (DCon _ _ _) y _) = x /= y
314 headDiff (P (TCon _ _) x _) (P (TCon _ _) y _) = x /= y
315 headDiff _ _ = False
317 injective (P (DCon _ _ _) _ _) = True
318 injective (P (TCon _ _) _ _) = True
319 injective (App _ f a) = injective f -- && injective a
320 injective _ = False
322-- injectiveVar (P _ (MN _ _) _) = True -- TMP HACK
323 injectiveVar (P _ n _) = n `elem` inj
324 injectiveVar (App _ f a) = injectiveVar f -- && injective a
325 injectiveVar _ = False
327 injectiveApp x = injective x || injectiveVar x
329 notP (P _ _ _) = False
330 notP _ = True
332 sc i = do UI s f <- get
333 put (UI (s+i) f)
335 errors :: StateT UInfo TC Bool
336 errors = do UI s f <- get
337 return (not (null f))
339 uplus u1 u2 = do UI s f <- get
340 r <- u1
341 UI s f' <- get
342 if (length f == length f')
343 then return r
344 else do put (UI s f); u2
346 un :: Bool -> [((Name, Name), TT Name)] -> TT Name -> TT Name ->
347 StateT UInfo
348 TC [(Name, TT Name)]
349 un = un'
350-- un fn names x y
351-- = let (xf, _) = unApply x
352-- (yf, _) = unApply y in
353-- if headDiff xf yf then unifyFail x y else
354-- uplus (un' fn names x y)
355-- (un' fn names (hnf ctxt env x) (hnf ctxt env y))
357 un' :: Bool -> [((Name, Name), TT Name)] -> TT Name -> TT Name ->
358 StateT UInfo
359 TC [(Name, TT Name)]
360 un' fn names x y | x == y = return [] -- shortcut
361 un' fn names topx@(P (DCon _ _ _) x _) topy@(P (DCon _ _ _) y _)
362 | x /= y = unifyFail topx topy
363 un' fn names topx@(P (TCon _ _) x _) topy@(P (TCon _ _) y _)
364 | x /= y = unifyFail topx topy
365 un' fn names topx@(P (DCon _ _ _) x _) topy@(P (TCon _ _) y _)
366 = unifyFail topx topy
367 un' fn names topx@(P (TCon _ _) x _) topy@(P (DCon _ _ _) y _)
368 = unifyFail topx topy
369 un' fn names topx@(Constant _) topy@(P (TCon _ _) y _)
370 = unifyFail topx topy
371 un' fn names topx@(P (TCon _ _) x _) topy@(Constant _)
372 = unifyFail topx topy
373 un' fn bnames tx@(P _ x _) ty@(P _ y _)
374 | (x,y) `elem` map fst bnames || x == y = do sc 1; return []
375 | injective tx && not (holeIn env y || y `elem` holes)
376 = unifyTmpFail tx ty
377 | injective ty && not (holeIn env x || x `elem` holes)
378 = unifyTmpFail tx ty
379 -- pick the one bound earliest if both are holes
380 | tx /= ty && (holeIn env x || x `elem` holes)
381 && (holeIn env y || y `elem` holes)
382 = case compare (envPos 0 x env) (envPos 0 y env) of
383 LT -> do sc 1; checkCycle bnames (x, ty)
384 _ -> do sc 1; checkCycle bnames (y, tx)
385 where envPos i n ((n',_):env) | n == n' = i
386 envPos i n (_:env) = envPos (i+1) n env
387 envPos _ _ _ = 100000
388 un' fn bnames xtm@(P _ x _) tm
389 | pureTerm tm, holeIn env x || x `elem` holes
390 = do UI s f <- get
391 -- injectivity check
392 x <- checkCycle bnames (x, tm)
393 if (notP tm && fn)
394-- trace (show (x, tm, normalise ctxt env tm)) $
395-- put (UI s ((tm, topx, topy) : i) f)
396 then unifyTmpFail xtm tm
397 else do sc 1
398 return x
399 | pureTerm tm, not (injective xtm) && injective tm
400 = do checkCycle bnames (x, tm)
401 unifyTmpFail xtm tm
402 un' fn bnames tm ytm@(P _ y _)
403 | pureTerm tm, holeIn env y || y `elem` holes
404 = do UI s f <- get
405 -- injectivity check
406 x <- checkCycle bnames (y, tm)
407 if (notP tm && fn)
408-- trace (show (y, tm, normalise ctxt env tm)) $
409-- put (UI s ((tm, topx, topy) : i) f)
410 then unifyTmpFail tm ytm
411 else do sc 1
412 return x
413 | pureTerm tm, not (injective ytm) && injective tm
414 = do checkCycle bnames (y, tm)
415 unifyTmpFail tm ytm
416 un' fn bnames (V i) (P _ x _)
417 | length bnames > i,
418 fst ((map fst bnames)!!i) == x ||
419 snd ((map fst bnames)!!i) == x = do sc 1; return []
420 un' fn bnames (P _ x _) (V i)
421 | length bnames > i,
422 fst ((map fst bnames)!!i) == x ||
423 snd ((map fst bnames)!!i) == x = do sc 1; return []
425 un' fn names topx@(Bind n (Hole t) sc) y = unifyTmpFail topx y
426 un' fn names x topy@(Bind n (Hole t) sc) = unifyTmpFail x topy
428 un' fn bnames appx@(App _ _ _) appy@(App _ _ _)
429 = unApp fn bnames appx appy
430-- = uplus (unApp fn bnames appx appy)
431-- (unifyTmpFail appx appy) -- take the whole lot
433 un' fn bnames x (Bind n (Lam t) (App _ y (P Bound n' _)))
434 | n == n' = un' False bnames x y
435 un' fn bnames (Bind n (Lam t) (App _ x (P Bound n' _))) y
436 | n == n' = un' False bnames x y
437 un' fn bnames x (Bind n (Lam t) (App _ y (V 0)))
438 = un' False bnames x y
439 un' fn bnames (Bind n (Lam t) (App _ x (V 0))) y
440 = un' False bnames x y
441-- un' fn bnames (Bind x (PVar _) sx) (Bind y (PVar _) sy)
442-- = un' False ((x,y):bnames) sx sy
443-- un' fn bnames (Bind x (PVTy _) sx) (Bind y (PVTy _) sy)
444-- = un' False ((x,y):bnames) sx sy
446 -- f D unifies with t -> D. This is dubious, but it helps with type
447 -- class resolution for type classes over functions.
449 un' fn bnames (App _ f x) (Bind n (Pi i t k) y)
450 | noOccurrence n y && injectiveApp f
451 = do ux <- un' False bnames x y
452 uf <- un' False bnames f (Bind (sMN 0 "uv") (Lam (TType (UVar 0)))
453 (Bind n (Pi i t k) (V 1)))
454 combine bnames ux uf
456 un' fn bnames (Bind n (Pi i t k) y) (App _ f x)
457 | noOccurrence n y && injectiveApp f
458 = do ux <- un' False bnames y x
459 uf <- un' False bnames (Bind (sMN 0 "uv") (Lam (TType (UVar 0)))
460 (Bind n (Pi i t k) (V 1))) f
461 combine bnames ux uf
463 un' fn bnames (Bind x bx sx) (Bind y by sy)
464 | sameBinder bx by
465 = do h1 <- uB bnames bx by
466 h2 <- un' False (((x,y),binderTy bx):bnames) sx sy
467 combine bnames h1 h2
468 where sameBinder (Lam _) (Lam _) = True
469 sameBinder (Pi i _ _) (Pi i' _ _) = True
470 sameBinder _ _ = False -- never unify holes/guesses/etc
471 un' fn bnames x y
472 | OK True <- convEq' ctxt holes x y = do sc 1; return []
473 | isUniverse x && isUniverse y = do sc 1; return []
474 | otherwise = do UI s f <- get
475 let r = recoverable (normalise ctxt env x)
476 (normalise ctxt env y)
477 let err = cantUnify from r
478 (topx, xfrom) (topy, yfrom) (CantUnify r (x, Nothing) (y, Nothing) (Msg "") (errEnv env) s) (errEnv env) s
479 if (not r) then lift $ tfail err
480 else do put (UI s ((x, y, True, env, err, from, Unify) : f))
481 return [] -- lift $ tfail err
483 unApp fn bnames appx@(App _ fx ax) appy@(App _ fy ay)
484 -- shortcut for the common case where we just want to check the
485 -- arguments are correct
486 | (injectiveApp fx && fx == fy)
487 = un' False bnames ax ay
488 | (injectiveApp fx && injectiveApp fy)
489 || (injectiveApp fx && metavarApp fy && ax == ay)
490 || (injectiveApp fy && metavarApp fx && ax == ay)
491 = do let (headx, _) = unApply fx
492 let (heady, _) = unApply fy
493 -- fail quickly if the heads are disjoint
494 checkHeads headx heady
495 uplus
496 (do hf <- un' True bnames fx fy
497 let ax' = hnormalise hf ctxt env (substNames hf ax)
498 let ay' = hnormalise hf ctxt env (substNames hf ay)
499 ha <- un' False bnames ax' ay'
500 sc 1
501 combine bnames hf ha)
502 (do ha <- un' False bnames ax ay
503 let fx' = hnormalise ha ctxt env (substNames ha fx)
504 let fy' = hnormalise ha ctxt env (substNames ha fy)
505 hf <- un' False bnames fx' fy'
506 sc 1
507 combine bnames hf ha)
508 | otherwise = unifyTmpFail appx appy
509 where hnormalise [] _ _ t = t
510 hnormalise ns ctxt env t = normalise ctxt env t
511 checkHeads (P (DCon _ _ _) x _) (P (DCon _ _ _) y _)
512 | x /= y = unifyFail appx appy
513 checkHeads (P (TCon _ _) x _) (P (TCon _ _) y _)
514 | x /= y = unifyFail appx appy
515 checkHeads (P (DCon _ _ _) x _) (P (TCon _ _) y _)
516 = unifyFail appx appy
517 checkHeads (P (TCon _ _) x _) (P (DCon _ _ _) y _)
518 = unifyFail appx appy
519 checkHeads _ _ = return []
521 unArgs as [] [] = return as
522 unArgs as (x : xs) (y : ys)
523 = do let x' = hnormalise as ctxt env (substNames as x)
524 let y' = hnormalise as ctxt env (substNames as y)
525 as' <- un' False bnames x' y'
526 vs <- combine bnames as as'
527 unArgs vs xs ys
529 numArgs tm = let (f, args) = unApply tm in length args
531 metavarApp tm = let (f, args) = unApply tm in
532 (metavar f &&
533 all (\x -> metavarApp x) args
534 && nub args == args) ||
535 globmetavar tm
536 metavarArgs tm = let (f, args) = unApply tm in
537 all (\x -> metavar x || inenv x) args
538 && nub args == args
539 metavarApp' tm = let (f, args) = unApply tm in
540 all (\x -> pat x || metavar x) (f : args)
541 && nub args == args
543 rigid (P (DCon _ _ _) _ _) = True
544 rigid (P (TCon _ _) _ _) = True
545 rigid t@(P Ref _ _) = inenv t || globmetavar t
546 rigid (Constant _) = True
547 rigid (App _ f a) = rigid f && rigid a
548 rigid t = not (metavar t) || globmetavar t
550 globmetavar t = case unApply t of
551 (P _ x _, _) ->
552 case lookupDef x ctxt of
553 [TyDecl _ _] -> True
554 _ -> False
555 _ -> False
557 metavar t = case t of
558 P _ x _ -> (x `notElem` usersupp &&
559 (x `elem` holes || holeIn env x))
560 || globmetavar t
561 _ -> False
562 pat t = case t of
563 P _ x _ -> x `elem` holes || patIn env x
564 _ -> False
565 inenv t = case t of
566 P _ x _ -> x `elem` (map fst env)
567 _ -> False
569 notFn t = injective t || metavar t || inenv t
572 unifyTmpFail :: Term -> Term -> StateT UInfo TC [(Name, TT Name)]
573 unifyTmpFail x y
574 = do UI s f <- get
575 let r = recoverable (normalise ctxt env x) (normalise ctxt env y)
576 let err = cantUnify from r
577 (topx, xfrom) (topy, yfrom)
578 (CantUnify r (x, Nothing) (y, Nothing) (Msg "") (errEnv env) s) (errEnv env) s
579 put (UI s ((topx, topy, True, env, err, from, Unify) : f))
580 return []
582 -- shortcut failure, if we *know* nothing can fix it
583 unifyFail x y = do UI s f <- get
584 let r = recoverable (normalise ctxt env x) (normalise ctxt env y)
585 let err = cantUnify from r
586 (topx, xfrom) (topy, yfrom)
587 (CantUnify r (x, Nothing) (y, Nothing) (Msg "") (errEnv env) s) (errEnv env) s
588 put (UI s ((topx, topy, True, env, err, from, Unify) : f))
589 lift $ tfail err
592 uB bnames (Let tx vx) (Let ty vy)
593 = do h1 <- un' False bnames tx ty
594 h2 <- un' False bnames vx vy
595 sc 1
596 combine bnames h1 h2
597 uB bnames (Guess tx vx) (Guess ty vy)
598 = do h1 <- un' False bnames tx ty
599 h2 <- un' False bnames vx vy
600 sc 1
601 combine bnames h1 h2
602 uB bnames (Lam tx) (Lam ty) = do sc 1; un' False bnames tx ty
603 uB bnames (Pi _ tx _) (Pi _ ty _) = do sc 1; un' False bnames tx ty
604 uB bnames (Hole tx) (Hole ty) = un' False bnames tx ty
605 uB bnames (PVar tx) (PVar ty) = un' False bnames tx ty
606 uB bnames x y = do UI s f <- get
607 let r = recoverable (normalise ctxt env (binderTy x))
608 (normalise ctxt env (binderTy y))
609 let err = cantUnify from r (topx, xfrom) (topy, yfrom)
610 (CantUnify r (binderTy x, Nothing) (binderTy y, Nothing) (Msg "") (errEnv env) s)
611 (errEnv env) s
612 put (UI s ((binderTy x, binderTy y,
613 False,
614 env, err, from, Unify) : f))
615 return [] -- lift $ tfail err
617 checkCycle ns p@(x, P _ _ _) = return [p]
618 checkCycle ns (x, tm)
619 | not (x `elem` freeNames tm) = checkScope ns (x, tm)
620 | otherwise = lift $ tfail (InfiniteUnify x tm (errEnv env))
622 checkScope ns (x, tm) | pureTerm tm =
623-- case boundVs (envPos x 0 env) tm of
624-- [] -> return [(x, tm)]
625-- (i:_) -> lift $ tfail (UnifyScope x (fst (fst (ns!!i)))
626-- (inst ns tm) (errEnv env))
627 let v = highV (-1) tm in
628 if v >= length ns
629 then lift $ tfail (Msg "SCOPE ERROR")
630 else return [(x, bind v ns tm)]
631 where inst [] tm = tm
632 inst (((n, _), _) : ns) tm = inst ns (substV (P Bound n Erased) tm)
633 checkScope ns (x, tm) = lift $ tfail (Msg "HOLE ERROR")
635 bind i ns tm
636 | i < 0 = tm
637 | otherwise = let ((x,y),ty) = ns!!i in
638 App MaybeHoles (Bind y (Lam ty) (bind (i-1) ns tm))
639 (P Bound x ty)
641 combineArgs bnames args = ca [] args where
642 ca acc [] = return acc
643 ca acc (x : xs) = do x' <- combine bnames acc x
644 ca x' xs
646 combine bnames as [] = return as
647 combine bnames as ((n, t) : bs)
648 = case lookup n as of
649 Nothing -> combine bnames (as ++ [(n,t)]) bs
650 Just t' -> do ns <- un' False bnames t t'
651 -- make sure there's n mapping from n in ns
652 let ns' = filter (\ (x, _) -> x/=n) ns
653 sc 1
654 combine bnames as (ns' ++ bs)
656boundVs :: Int -> Term -> [Int]
657boundVs i (V j) | j < i = []
658 | otherwise = [j]
659boundVs i (Bind n b sc) = boundVs (i + 1) sc
660boundVs i (App _ f x) = let fs = boundVs i f
661 xs = boundVs i x in
662 nub (fs ++ xs)
663boundVs i _ = []
665highV :: Int -> Term -> Int
666highV i (V j) | j > i = j
667 | otherwise = i
668highV i (Bind n b sc) = maximum [i, highV i (binderTy b), (highV i sc - 1)]
669highV i (App _ f x) = max (highV i f) (highV i x)
670highV i _ = i
672envPos x i [] = 0
673envPos x i ((y, _) : ys) | x == y = i
674 | otherwise = envPos x (i + 1) ys
677-- If there are any clashes of constructors, deem it unrecoverable, otherwise some
678-- more work may help.
679-- FIXME: Depending on how overloading gets used, this may cause problems. Better
680-- rethink overloading properly...
681-- ASSUMPTION: inputs are in normal form
682--
683-- Issue #1722 on the issue tracker https://github.com/idris-lang/Idris-dev/issues/1722
684--
685recoverable t@(App _ _ _) _
686 | (P _ (UN l) _, _) <- unApply t, l == txt "Lazy'" = False
687recoverable _ t@(App _ _ _)
688 | (P _ (UN l) _, _) <- unApply t, l == txt "Lazy'" = False
689recoverable (P (DCon _ _ _) x _) (P (DCon _ _ _) y _) = x == y
690recoverable (P (TCon _ _) x _) (P (TCon _ _) y _) = x == y
691recoverable (TType _) (P (DCon _ _ _) y _) = False
692recoverable (UType _) (P (DCon _ _ _) y _) = False
693recoverable (Constant _) (P (DCon _ _ _) y _) = False
694recoverable (Constant x) (Constant y) = x == y
695recoverable (P (DCon _ _ _) x _) (TType _) = False
696recoverable (P (DCon _ _ _) x _) (UType _) = False
697recoverable (P (DCon _ _ _) x _) (Constant _) = False
698recoverable (TType _) (P (TCon _ _) y _) = False
699recoverable (UType _) (P (TCon _ _) y _) = False
700recoverable (Constant _) (P (TCon _ _) y _) = False
701recoverable (P (TCon _ _) x _) (TType _) = False
702recoverable (P (TCon _ _) x _) (UType _) = False
703recoverable (P (TCon _ _) x _) (Constant _) = False
704recoverable (P (DCon _ _ _) x _) (P (TCon _ _) y _) = False
705recoverable (P (TCon _ _) x _) (P (DCon _ _ _) y _) = False
706recoverable p@(TType _) (App _ f a) = recoverable p f
707recoverable p@(UType _) (App _ f a) = recoverable p f
708recoverable p@(Constant _) (App _ f a) = recoverable p f
709recoverable (App _ f a) p@(TType _) = recoverable f p
710recoverable (App _ f a) p@(UType _) = recoverable f p
711recoverable (App _ f a) p@(Constant _) = recoverable f p
712recoverable p@(P _ n _) (App _ f a) = recoverable p f
713recoverable (App _ f a) p@(P _ _ _) = recoverable f p
714recoverable (App _ f a) (App _ f' a')
715 | f == f' = recoverable a a'
716recoverable (App _ f a) (App _ f' a')
717 = recoverable f f' -- && recoverable a a'
718recoverable f (Bind _ (Pi _ _ _) sc)
719 | (P (DCon _ _ _) _ _, _) <- unApply f = False
720 | (P (TCon _ _) _ _, _) <- unApply f = False
721 | (Constant _) <- f = False
722recoverable (Bind _ (Pi _ _ _) sc) f
723 | (P (DCon _ _ _) _ _, _) <- unApply f = False
724 | (P (TCon _ _) _ _, _) <- unApply f = False
725 | (Constant _) <- f = False
726recoverable (Bind _ (Lam _) sc) f = recoverable sc f
727recoverable f (Bind _ (Lam _) sc) = recoverable f sc
728recoverable x y = True
730errEnv :: [(a, Binder b)] -> [(a, b)]
731errEnv = map (\(x, b) -> (x, binderTy b))
733holeIn :: Env -> Name -> Bool
734holeIn env n = case lookup n env of
735 Just (Hole _) -> True
736 Just (Guess _ _) -> True
737 _ -> False
739patIn :: Env -> Name -> Bool
740patIn env n = case lookup n env of
741 Just (PVar _) -> True
742 Just (PVTy _) -> True
743 _ -> False