git.iko.soy/Idris-dev
on fd6898e help sign in
Idris-dev/src/Idris/Core/Unify.hs
776 lines 35 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.Maybe
12import Data.List
13import Debug.Trace
15-- Unification is applied inside the theorem prover. We're looking for holes
16-- which can be filled in, by matching one term's normal form against another.
17-- Returns a list of hole names paired with the term which solves them, and
18-- a list of things which need to be injective.
20-- terms which need to be injective, with the things we're trying to unify
21-- at the time
23data FailAt = Match | Unify
24 deriving (Show, Eq)
26data FailContext = FailContext { fail_sourceloc :: FC,
27 fail_fn :: Name,
28 fail_param :: Name
29 }
30 deriving (Eq, Show)
32type Injs = [(TT Name, TT Name, TT Name)]
33type Fails = [(TT Name, TT Name, -- unification error
34 Bool, -- ready to retry yet
35 Env, Err, [FailContext], FailAt)]
37unrecoverable :: Fails -> Bool
38unrecoverable = any bad
39 where bad (_,_,_,_, err, _, _) = unrec err
41 unrec (CantUnify r _ _ _ _ _) = not r
42 unrec (At _ e) = unrec e
43 unrec (Elaborating _ _ _ e) = unrec e
44 unrec (ElaboratingArg _ _ _ e) = unrec e
45 unrec _ = False
47data UInfo = UI Int Fails
48 deriving Show
50data UResult a = UOK a
51 | UPartOK a
52 | UFail Err
54-- | Smart constructor for unification errors that takes into account the FailContext
55cantUnify :: [FailContext] -> Bool -> (t, Maybe Provenance) -> (t, Maybe Provenance) -> (Err' t) -> [(Name, t)] -> Int -> Err' t
56cantUnify [] r t1 t2 e ctxt i = CantUnify r t1 t2 e ctxt i
57cantUnify (FailContext fc f x : prev) r t1 t2 e ctxt i =
58 At fc (ElaboratingArg f x
59 (map (\(FailContext _ f' x') -> (f', x')) prev)
60 (CantUnify r t1 t2 e ctxt i))
62-- Solve metavariables by matching terms against each other
63-- Not really unification, of course!
65match_unify :: Context -> Env ->
66 (TT Name, Maybe Provenance) ->
67 (TT Name, Maybe Provenance) -> [Name] -> [Name] -> [FailContext] ->
68 TC [(Name, TT Name)]
69match_unify ctxt env (topx, xfrom) (topy, yfrom) inj holes from =
70 case runStateT (un [] (renameBindersTm env topx)
71 (renameBindersTm env topy)) (UI 0 []) of
72 OK (v, UI _ []) ->
73 do v' <- trimSolutions (topx, xfrom) (topy, yfrom) from env v
74 return (map (renameBinders env) v')
75 res ->
76 let topxn = renameBindersTm env (normalise ctxt env topx)
77 topyn = renameBindersTm env (normalise ctxt env topy) in
78 case runStateT (un [] topxn topyn)
79 (UI 0 []) of
80 OK (v, UI _ fails) ->
81 do v' <- trimSolutions (topx, xfrom) (topy, yfrom) from env v
82 return (map (renameBinders env) v')
83 Error e ->
84 -- just normalise the term we're matching against
85 case runStateT (un [] topxn topy)
86 (UI 0 []) of
87 OK (v, UI _ fails) ->
88 do v' <- trimSolutions (topx, xfrom) (topy, yfrom) from env v
89 return (map (renameBinders env) v')
90 _ -> tfail e
91 where
92 un :: [((Name, Name), TT Name)] -> TT Name -> TT Name ->
93 StateT UInfo
94 TC [(Name, TT Name)]
96 un names tx@(P _ x _) tm
97 | tx /= tm && holeIn env x || x `elem` holes
98 = do sc 1; checkCycle names (x, tm)
99 un names tm ty@(P _ y _)
100 | ty /= tm && holeIn env y || y `elem` holes
101 = do sc 1; checkCycle names (y, tm)
102 un bnames (V i) (P _ x _)
103 | length bnames > i,
104 fst (fst (bnames!!i)) == x ||
105 snd (fst (bnames!!i)) == x = do sc 1; return []
106 un bnames (P _ x _) (V i)
107 | length bnames > i,
108 fst (fst (bnames!!i)) == x ||
109 snd (fst (bnames!!i)) == x = do sc 1; return []
110 un bnames (Bind x bx sx) (Bind y by sy) | notHole bx && notHole by
111 = do h1 <- uB bnames bx by
112 h2 <- un (((x, y), binderTy bx) : bnames) sx sy
113 combine bnames h1 h2
114 un names (App _ fx ax) (App _ fy ay)
115 = do hf <- un names fx fy
116 ha <- un names ax ay
117 combine names hf ha
118 un names x y
119 | OK True <- convEq' ctxt holes x y = do sc 1; return []
120 | otherwise = do UI s f <- get
121 let r = recoverable (normalise ctxt env x)
122 (normalise ctxt env y)
123 let err = cantUnify from r
124 (topx, xfrom) (topy, yfrom) (CantUnify r (x, Nothing) (y, Nothing) (Msg "") (errEnv env) s) (errEnv env) s
125 if (not r) then lift $ tfail err
126 else do put (UI s ((x, y, True, env, err, from, Match) : f))
127 lift $ tfail err
130 uB bnames (Let tx vx) (Let ty vy) = do h1 <- un bnames tx ty
131 h2 <- un bnames vx vy
132 combine bnames h1 h2
133 uB bnames (Lam tx) (Lam ty) = un bnames tx ty
134 uB bnames (Pi i tx _) (Pi i' ty _) = un bnames tx ty
135 uB bnames x y = do UI s f <- get
136 let r = recoverable (normalise ctxt env (binderTy x))
137 (normalise ctxt env (binderTy y))
138 let err = cantUnify from r (topx, xfrom) (topy, yfrom)
139 (CantUnify r (binderTy x, Nothing)
140 (binderTy y, Nothing) (Msg "") (errEnv env) s)
141 (errEnv env) s
142 put (UI s ((binderTy x, binderTy y,
143 False,
144 env, err, from, Match) : f))
145 return []
147 notHole (Hole _) = False
148 notHole _ = True
150 -- TODO: there's an annoying amount of repetition between this and the
151 -- main unification function. Consider lifting it out.
152 -- Issue #1721 on the issue tracker: https://github.com/idris-lang/Idris-dev/issues/1721
154 sc i = do UI s f <- get
155 put (UI (s+i) f)
157 unifyFail x y = do UI s f <- get
158 let r = recoverable (normalise ctxt env x)
159 (normalise ctxt env y)
160 let err = cantUnify from r
161 (topx, xfrom) (topy, yfrom)
162 (CantUnify r (x, Nothing) (y, Nothing) (Msg "") (errEnv env) s) (errEnv env) s
163 put (UI s ((x, y, True, env, err, from, Match) : f))
164 lift $ tfail err
165 combine bnames as [] = return as
166 combine bnames as ((n, t) : bs)
167 = case lookup n as of
168 Nothing -> combine bnames (as ++ [(n,t)]) bs
169 Just t' -> do ns <- un bnames t t'
170 let ns' = filter (\ (x, _) -> x/=n) ns
171 sc 1
172 combine bnames as (ns' ++ bs)
174-- substN n tm (var, sol) = (var, subst n tm sol)
176 checkCycle ns p@(x, P _ x' _) | x == x' = return []
177 checkCycle ns p@(x, P _ _ _) = return [p]
178 checkCycle ns (x, tm)
179 | not (x `elem` freeNames tm) = checkScope ns (x, tm)
180 | otherwise = lift $ tfail (InfiniteUnify x tm (errEnv env))
182 checkScope ns (x, tm) =
183-- case boundVs (envPos x 0 env) tm of
184-- [] -> return [(x, tm)]
185-- (i:_) -> lift $ tfail (UnifyScope x (fst (fst (ns!!i)))
186-- (inst ns tm) (errEnv env))
187 let v = highV (-1) tm in
188 if v >= length ns
189 then lift $ tfail (Msg "SCOPE ERROR")
190 else return [(x, bind v ns tm)]
191 where inst [] tm = tm
192 inst ((n, _) : ns) tm = inst ns (substV (P Bound n Erased) tm)
194 bind i ns tm
195 | i < 0 = tm
196 | otherwise = let ((x,y),ty) = ns!!i in
197 App MaybeHoles (Bind y (Lam ty) (bind (i-1) ns tm))
198 (P Bound x ty)
200renameBinders env (x, t) = (x, renameBindersTm env t)
202renameBindersTm :: Env -> TT Name -> TT Name
203renameBindersTm env tm = uniqueBinders (map fst env) tm
204 where
205 uniqueBinders env (Bind n b sc)
206 | n `elem` env
207 = let n' = uniqueName n env in
208 explicitHole $ Bind n' (fmap (uniqueBinders env) b)
209 (uniqueBinders (n':env) (rename n n' sc))
210 | otherwise = Bind n (fmap (uniqueBinders (n:env)) b)
211 (uniqueBinders (n:env) sc)
212 uniqueBinders env (App s f a) = App s (uniqueBinders env f) (uniqueBinders env a)
213 uniqueBinders env t = t
215 rename n n' (P nt x ty) | n == x = P nt n' ty
216 rename n n' (Bind x b sc) = Bind x (fmap (rename n n') b) (rename n n' sc)
217 rename n n' (App s f a) = App s (rename n n' f) (rename n n' a)
218 rename n n' t = t
220 explicitHole (Bind n (Hole ty) sc)
221 = Bind n (Hole ty) (instantiate (P Bound n ty) sc)
222 explicitHole t = t
224trimSolutions (topx, xfrom) (topy, yfrom) from env topns = followSols [] (dropPairs topns)
225 where dropPairs [] = []
226 dropPairs (n@(x, P _ x' _) : ns)
227 | x == x' = dropPairs ns
228 | otherwise
229 = n : dropPairs
230 (filter (\t -> case t of
231 (n, P _ n' _) -> not (n == x' && n' == x)
232 _ -> True) ns)
233 dropPairs (n : ns) = n : dropPairs ns
235 followSols vs [] = return []
236 followSols vs ((n, P _ t _) : ns)
237 | Just t' <- lookup t ns
238 = do vs' <- case t' of
239 P _ tn _ ->
240 if (n, tn) `elem` vs then -- cycle
241 tfail (cantUnify from False (topx, xfrom) (topy, yfrom)
242 (Msg "") (errEnv env) 0)
243 else return ((n, tn) : vs)
244 _ -> return vs
245 followSols vs' ((n, t') : ns)
246 followSols vs (n : ns) = do ns' <- followSols vs ns
247 return $ n : ns'
249expandLets env (x, tm) = (x, doSubst (reverse env) tm)
250 where
251 doSubst [] tm = tm
252 doSubst ((n, Let v t) : env) tm
253 = doSubst env (subst n v tm)
254 doSubst (_ : env) tm
255 = doSubst env tm
257hasv :: TT Name -> Bool
258hasv (V x) = True
259hasv (App _ f a) = hasv f || hasv a
260hasv (Bind x b sc) = hasv (binderTy b) || hasv sc
261hasv _ = False
263unify :: Context -> Env ->
264 (TT Name, Maybe Provenance) ->
265 (TT Name, Maybe Provenance) ->
266 [Name] -> [Name] -> [Name] -> [FailContext] ->
267 TC ([(Name, TT Name)], Fails)
268unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =
269-- traceWhen (hasv topx || hasv topy)
270-- ("Unifying " ++ show topx ++ "\nAND\n" ++ show topy ++ "\n") $
271 -- don't bother if topx and topy are different at the head
272 case runStateT (un False [] (renameBindersTm env topx)
273 (renameBindersTm env topy)) (UI 0 []) of
274 OK (v, UI _ []) -> do v' <- trimSolutions (topx, xfrom) (topy, yfrom) from env v
275 return (map (renameBinders env) v', [])
276 res ->
277 let topxn = renameBindersTm env (normalise ctxt env topx)
278 topyn = renameBindersTm env (normalise ctxt env topy) in
279-- trace ("Unifying " ++ show (topx, topy) ++ "\n\n==>\n" ++ show (topxn, topyn) ++ "\n\n") $
280 case runStateT (un False [] topxn topyn)
281 (UI 0 []) of
282 OK (v, UI _ fails) ->
283 do v' <- trimSolutions (topx, xfrom) (topy, yfrom) from env v
284-- trace ("OK " ++ show (topxn, topyn, v, holes)) $
285 return (map (renameBinders env) v', reverse fails)
286-- Error e@(CantUnify False _ _ _ _ _) -> tfail e
287 Error e -> tfail e
288 where
289 headDiff (P (DCon _ _ _) x _) (P (DCon _ _ _) y _) = x /= y
290 headDiff (P (TCon _ _) x _) (P (TCon _ _) y _) = x /= y
291 headDiff _ _ = False
293 injective (P (DCon _ _ _) _ _) = True
294 injective (P (TCon _ _) _ _) = True
295 injective (App _ f a) = injective f -- && injective a
296 injective _ = False
298-- injectiveVar (P _ (MN _ _) _) = True -- TMP HACK
299 injectiveVar (P _ n _) = n `elem` inj
300 injectiveVar (App _ f a) = injectiveVar f -- && injective a
301 injectiveVar _ = False
303 injectiveApp x = injective x || injectiveVar x
305 notP (P _ _ _) = False
306 notP _ = True
308 sc i = do UI s f <- get
309 put (UI (s+i) f)
311 errors :: StateT UInfo TC Bool
312 errors = do UI s f <- get
313 return (not (null f))
315 uplus u1 u2 = do UI s f <- get
316 r <- u1
317 UI s f' <- get
318 if (length f == length f')
319 then return r
320 else do put (UI s f); u2
322 un :: Bool -> [((Name, Name), TT Name)] -> TT Name -> TT Name ->
323 StateT UInfo
324 TC [(Name, TT Name)]
325 un = un' env
326-- un fn names x y
327-- = let (xf, _) = unApply x
328-- (yf, _) = unApply y in
329-- if headDiff xf yf then unifyFail x y else
330-- uplus (un' fn names x y)
331-- (un' fn names (hnf ctxt env x) (hnf ctxt env y))
333 un' :: Env -> Bool -> [((Name, Name), TT Name)] -> TT Name -> TT Name ->
334 StateT UInfo
335 TC [(Name, TT Name)]
336 un' env fn names x y | x == y = return [] -- shortcut
337 un' env fn names topx@(P (DCon _ _ _) x _) topy@(P (DCon _ _ _) y _)
338 | x /= y = unifyFail topx topy
339 un' env fn names topx@(P (TCon _ _) x _) topy@(P (TCon _ _) y _)
340 | x /= y = unifyFail topx topy
341 un' env fn names topx@(P (DCon _ _ _) x _) topy@(P (TCon _ _) y _)
342 = unifyFail topx topy
343 un' env fn names topx@(P (TCon _ _) x _) topy@(P (DCon _ _ _) y _)
344 = unifyFail topx topy
345 un' env fn names topx@(Constant _) topy@(P (TCon _ _) y _)
346 = unifyFail topx topy
347 un' env fn names topx@(P (TCon _ _) x _) topy@(Constant _)
348 = unifyFail topx topy
349 un' env fn bnames tx@(P _ x _) ty@(P _ y _)
350 | (x,y) `elem` map fst bnames || x == y = do sc 1; return []
351 | injective tx && not (holeIn env y || y `elem` holes)
352 = unifyTmpFail tx ty
353 | injective ty && not (holeIn env x || x `elem` holes)
354 = unifyTmpFail tx ty
355 -- pick the one bound earliest if both are holes
356 | tx /= ty && (holeIn env x || x `elem` holes)
357 && (holeIn env y || y `elem` holes)
358 = case compare (envPos 0 x env) (envPos 0 y env) of
359 LT -> do sc 1; checkCycle bnames (x, ty)
360 _ -> do sc 1; checkCycle bnames (y, tx)
361 where envPos i n ((n',_):env) | n == n' = i
362 envPos i n (_:env) = envPos (i+1) n env
363 envPos _ _ _ = 100000
364 un' env fn bnames xtm@(P _ x _) tm
365 | pureTerm tm, holeIn env x || x `elem` holes
366 = do UI s f <- get
367 -- injectivity check
368 x <- checkCycle bnames (x, tm)
369 if (notP tm && fn)
370-- trace (show (x, tm, normalise ctxt env tm)) $
371-- put (UI s ((tm, topx, topy) : i) f)
372 then unifyTmpFail xtm tm
373 else do sc 1
374 return x
375 | pureTerm tm, not (injective xtm) && injective tm
376 = do checkCycle bnames (x, tm)
377 unifyTmpFail xtm tm
378 un' env fn bnames tm ytm@(P _ y _)
379 | pureTerm tm, holeIn env y || y `elem` holes
380 = do UI s f <- get
381 -- injectivity check
382 x <- checkCycle bnames (y, tm)
383 if (notP tm && fn)
384-- trace (show (y, tm, normalise ctxt env tm)) $
385-- put (UI s ((tm, topx, topy) : i) f)
386 then unifyTmpFail tm ytm
387 else do sc 1
388 return x
389 | pureTerm tm, not (injective ytm) && injective tm
390 = do checkCycle bnames (y, tm)
391 unifyTmpFail tm ytm
392 un' env fn bnames (V i) (P _ x _)
393 | length bnames > i,
394 fst ((map fst bnames)!!i) == x ||
395 snd ((map fst bnames)!!i) == x = do sc 1; return []
396 un' env fn bnames (P _ x _) (V i)
397 | length bnames > i,
398 fst ((map fst bnames)!!i) == x ||
399 snd ((map fst bnames)!!i) == x = do sc 1; return []
401 un' env fn names topx@(Bind n (Hole t) sc) y = unifyTmpFail topx y
402 un' env fn names x topy@(Bind n (Hole t) sc) = unifyTmpFail x topy
404-- Pattern unification rule
405 un' env fn bnames tm app@(App _ _ _)
406 | (P _ mv _, args) <- unApply app,
407 holeIn env mv || mv `elem` holes,
408 all rigid args,
409 containsOnly (mapMaybe getname args) (mapMaybe getV args) tm
410 -- && TODO: tm does not refer to any variables other than those
411 -- in 'args'
412 = -- trace ("PATTERN RULE SOLVE: " ++ show (mv, tm, env, bindLams args (substEnv env tm))) $
413 checkCycle bnames (mv, eta [] $ bindLams args (substEnv env tm))
414 where rigid (V i) = True
415 rigid (P _ t _) = t `elem` map fst env &&
416 not (holeIn env t || t `elem` holes)
417 rigid _ = False
419 getV (V i) = Just i
420 getV _ = Nothing
422 getname (P _ n _) = Just n
423 getname _ = Nothing
425 containsOnly args vs (V i) = i `elem` vs
426 containsOnly args vs (P Bound n ty)
427 = n `elem` args && containsOnly args vs ty
428 containsOnly args vs (P _ n ty)
429 = not (holeIn env n || n `elem` holes)
430 && containsOnly args vs ty
431 containsOnly args vs (App _ f a)
432 = containsOnly args vs f && containsOnly args vs a
433 containsOnly args vs (Bind _ b sc)
434 = containsOnly args vs (binderTy b) &&
435 containsOnly args (0 : map (+1) vs) sc
436 containsOnly args vs _ = True
438 bindLams [] tm = tm
439 bindLams (a : as) tm = bindLam a (bindLams as tm)
441 bindLam (V i) tm = Bind (fst (env !! i))
442 (Lam (binderTy (snd (env !! i))))
443 tm
444 bindLam (P _ n ty) tm = Bind n (Lam ty) tm
445 bindLam _ tm = error "Can't happen [non rigid bindLam]"
447 substEnv [] tm = tm
448 substEnv ((n, t) : env) tm
449 = substEnv env (substV (P Bound n (binderTy t)) tm)
451 -- remove any unnecessary lambdas (helps with type class
452 -- resolution later).
453 eta ks (Bind n (Lam ty) sc) = eta ((n, ty) : ks) sc
454 eta ks t = rebind ks t
456 rebind ((n, ty) : ks) (App _ f (P _ n' _))
457 | n == n' = eta ks f
458 rebind ((n, ty) : ks) t = rebind ks (Bind n (Lam ty) t)
459 rebind _ t = t
461 un' env fn bnames appx@(App _ _ _) appy@(App _ _ _)
462 = unApp env fn bnames appx appy
463-- = uplus (unApp fn bnames appx appy)
464-- (unifyTmpFail appx appy) -- take the whole lot
466 un' env fn bnames x (Bind n (Lam t) (App _ y (P Bound n' _)))
467 | n == n' = un' env False bnames x y
468 un' env fn bnames (Bind n (Lam t) (App _ x (P Bound n' _))) y
469 | n == n' = un' env False bnames x y
470 un' env fn bnames x (Bind n (Lam t) (App _ y (V 0)))
471 = un' env False bnames x y
472 un' env fn bnames (Bind n (Lam t) (App _ x (V 0))) y
473 = un' env False bnames x y
474-- un' env fn bnames (Bind x (PVar _) sx) (Bind y (PVar _) sy)
475-- = un' env False ((x,y):bnames) sx sy
476-- un' env fn bnames (Bind x (PVTy _) sx) (Bind y (PVTy _) sy)
477-- = un' env False ((x,y):bnames) sx sy
479 -- f D unifies with t -> D. This is dubious, but it helps with type
480 -- class resolution for type classes over functions.
482 un' env fn bnames (App _ f x) (Bind n (Pi i t k) y)
483 | noOccurrence n y && injectiveApp f
484 = do ux <- un' env False bnames x y
485 uf <- un' env False bnames f (Bind (sMN 0 "uv") (Lam (TType (UVar 0)))
486 (Bind n (Pi i t k) (V 1)))
487 combine env bnames ux uf
489 un' env fn bnames (Bind n (Pi i t k) y) (App _ f x)
490 | noOccurrence n y && injectiveApp f
491 = do ux <- un' env False bnames y x
492 uf <- un' env False bnames (Bind (sMN 0 "uv") (Lam (TType (UVar 0)))
493 (Bind n (Pi i t k) (V 1))) f
494 combine env bnames ux uf
496 un' env fn bnames (Bind x bx sx) (Bind y by sy)
497 | sameBinder bx by
498 = do h1 <- uB env bnames bx by
499 h2 <- un' ((x, bx) : env) False (((x,y),binderTy bx):bnames) sx sy
500 combine env bnames h1 h2
501 where sameBinder (Lam _) (Lam _) = True
502 sameBinder (Pi i _ _) (Pi i' _ _) = True
503 sameBinder _ _ = False -- never unify holes/guesses/etc
504 un' env fn bnames x y
505 | OK True <- convEq' ctxt holes x y = do sc 1; return []
506 | isUniverse x && isUniverse y = do sc 1; return []
507 | otherwise = do UI s f <- get
508 let r = recoverable (normalise ctxt env x)
509 (normalise ctxt env y)
510 let err = cantUnify from r
511 (topx, xfrom) (topy, yfrom) (CantUnify r (x, Nothing) (y, Nothing) (Msg "") (errEnv env) s) (errEnv env) s
512 if (not r) then lift $ tfail err
513 else do put (UI s ((x, y, True, env, err, from, Unify) : f))
514 return [] -- lift $ tfail err
516 unApp env fn bnames appx@(App _ fx ax) appy@(App _ fy ay)
517 -- shortcut for the common case where we just want to check the
518 -- arguments are correct
519 | (injectiveApp fx && fx == fy)
520 = un' env False bnames ax ay
521 | (injectiveApp fx && injectiveApp fy)
522 || (injectiveApp fx && metavarApp fy && ax == ay)
523 || (injectiveApp fy && metavarApp fx && ax == ay)
524 = do let (headx, _) = unApply fx
525 let (heady, _) = unApply fy
526 -- fail quickly if the heads are disjoint
527 checkHeads headx heady
528 uplus
529 (do hf <- un' env True bnames fx fy
530 let ax' = hnormalise hf ctxt env (substNames hf ax)
531 let ay' = hnormalise hf ctxt env (substNames hf ay)
532 ha <- un' env False bnames ax' ay'
533 sc 1
534 combine env bnames hf ha)
535 (do ha <- un' env False bnames ax ay
536 let fx' = hnormalise ha ctxt env (substNames ha fx)
537 let fy' = hnormalise ha ctxt env (substNames ha fy)
538 hf <- un' env False bnames fx' fy'
539 sc 1
540 combine env bnames hf ha)
541 | otherwise = unifyTmpFail appx appy
542 where hnormalise [] _ _ t = t
543 hnormalise ns ctxt env t = normalise ctxt env t
544 checkHeads (P (DCon _ _ _) x _) (P (DCon _ _ _) y _)
545 | x /= y = unifyFail appx appy
546 checkHeads (P (TCon _ _) x _) (P (TCon _ _) y _)
547 | x /= y = unifyFail appx appy
548 checkHeads (P (DCon _ _ _) x _) (P (TCon _ _) y _)
549 = unifyFail appx appy
550 checkHeads (P (TCon _ _) x _) (P (DCon _ _ _) y _)
551 = unifyFail appx appy
552 checkHeads _ _ = return []
554 unArgs as [] [] = return as
555 unArgs as (x : xs) (y : ys)
556 = do let x' = hnormalise as ctxt env (substNames as x)
557 let y' = hnormalise as ctxt env (substNames as y)
558 as' <- un' env False bnames x' y'
559 vs <- combine env bnames as as'
560 unArgs vs xs ys
562 numArgs tm = let (f, args) = unApply tm in length args
564 metavarApp tm = let (f, args) = unApply tm in
565 (metavar f &&
566 all (\x -> metavarApp x) args
567 && nub args == args) ||
568 globmetavar tm
569 metavarArgs tm = let (f, args) = unApply tm in
570 all (\x -> metavar x || inenv x) args
571 && nub args == args
572 metavarApp' tm = let (f, args) = unApply tm in
573 all (\x -> pat x || metavar x) (f : args)
574 && nub args == args
576 rigid (P (DCon _ _ _) _ _) = True
577 rigid (P (TCon _ _) _ _) = True
578 rigid t@(P Ref _ _) = inenv t || globmetavar t
579 rigid (Constant _) = True
580 rigid (App _ f a) = rigid f && rigid a
581 rigid t = not (metavar t) || globmetavar t
583 globmetavar t = case unApply t of
584 (P _ x _, _) ->
585 case lookupDef x ctxt of
586 [TyDecl _ _] -> True
587 _ -> False
588 _ -> False
590 metavar t = case t of
591 P _ x _ -> (x `notElem` usersupp &&
592 (x `elem` holes || holeIn env x))
593 || globmetavar t
594 _ -> False
595 pat t = case t of
596 P _ x _ -> x `elem` holes || patIn env x
597 _ -> False
598 inenv t = case t of
599 P _ x _ -> x `elem` (map fst env)
600 _ -> False
602 notFn t = injective t || metavar t || inenv t
605 unifyTmpFail :: Term -> Term -> StateT UInfo TC [(Name, TT Name)]
606 unifyTmpFail x y
607 = do UI s f <- get
608 let r = recoverable (normalise ctxt env x) (normalise ctxt env y)
609 let err = cantUnify from r
610 (topx, xfrom) (topy, yfrom)
611 (CantUnify r (x, Nothing) (y, Nothing) (Msg "") (errEnv env) s) (errEnv env) s
612 put (UI s ((topx, topy, True, env, err, from, Unify) : f))
613 return []
615 -- shortcut failure, if we *know* nothing can fix it
616 unifyFail x y = do UI s f <- get
617 let r = recoverable (normalise ctxt env x) (normalise ctxt env y)
618 let err = cantUnify from r
619 (topx, xfrom) (topy, yfrom)
620 (CantUnify r (x, Nothing) (y, Nothing) (Msg "") (errEnv env) s) (errEnv env) s
621 put (UI s ((topx, topy, True, env, err, from, Unify) : f))
622 lift $ tfail err
625 uB env bnames (Let tx vx) (Let ty vy)
626 = do h1 <- un' env False bnames tx ty
627 h2 <- un' env False bnames vx vy
628 sc 1
629 combine env bnames h1 h2
630 uB env bnames (Guess tx vx) (Guess ty vy)
631 = do h1 <- un' env False bnames tx ty
632 h2 <- un' env False bnames vx vy
633 sc 1
634 combine env bnames h1 h2
635 uB env bnames (Lam tx) (Lam ty) = do sc 1; un' env False bnames tx ty
636 uB env bnames (Pi _ tx _) (Pi _ ty _) = do sc 1; un' env False bnames tx ty
637 uB env bnames (Hole tx) (Hole ty) = un' env False bnames tx ty
638 uB env bnames (PVar tx) (PVar ty) = un' env False bnames tx ty
639 uB env bnames x y
640 = do UI s f <- get
641 let r = recoverable (normalise ctxt env (binderTy x))
642 (normalise ctxt env (binderTy y))
643 let err = cantUnify from r (topx, xfrom) (topy, yfrom)
644 (CantUnify r (binderTy x, Nothing) (binderTy y, Nothing) (Msg "") (errEnv env) s)
645 (errEnv env) s
646 put (UI s ((binderTy x, binderTy y,
647 False,
648 env, err, from, Unify) : f))
649 return [] -- lift $ tfail err
651 checkCycle ns p@(x, P _ _ _) = return [p]
652 checkCycle ns (x, tm)
653 | not (x `elem` freeNames tm) = checkScope ns (x, tm)
654 | otherwise = lift $ tfail (InfiniteUnify x tm (errEnv env))
656 checkScope ns (x, tm) | pureTerm tm =
657-- case boundVs (envPos x 0 env) tm of
658-- [] -> return [(x, tm)]
659-- (i:_) -> lift $ tfail (UnifyScope x (fst (fst (ns!!i)))
660-- (inst ns tm) (errEnv env))
661 let v = highV (-1) tm in
662 if v >= length ns
663 then lift $ tfail (Msg "SCOPE ERROR")
664 else return [(x, bind v ns tm)]
665 where inst [] tm = tm
666 inst (((n, _), _) : ns) tm = inst ns (substV (P Bound n Erased) tm)
667 checkScope ns (x, tm) = lift $ tfail (Msg "HOLE ERROR")
669 bind i ns tm
670 | i < 0 = tm
671 | otherwise = let ((x,y),ty) = ns!!i in
672 App MaybeHoles (Bind y (Lam ty) (bind (i-1) ns tm))
673 (P Bound x ty)
675 combine env bnames as [] = return as
676 combine env bnames as ((n, t) : bs)
677 = case lookup n as of
678 Nothing -> combine env bnames (as ++ [(n,t)]) bs
679 Just t' -> do ns <- un' env False bnames t t'
680 -- make sure there's n mapping from n in ns
681 let ns' = filter (\ (x, _) -> x/=n) ns
682 sc 1
683 combine env bnames as (ns' ++ bs)
685boundVs :: Int -> Term -> [Int]
686boundVs i (V j) | j < i = []
687 | otherwise = [j]
688boundVs i (Bind n b sc) = boundVs (i + 1) sc
689boundVs i (App _ f x) = let fs = boundVs i f
690 xs = boundVs i x in
691 nub (fs ++ xs)
692boundVs i _ = []
694highV :: Int -> Term -> Int
695highV i (V j) | j > i = j
696 | otherwise = i
697highV i (Bind n b sc) = maximum [i, highV i (binderTy b), (highV i sc - 1)]
698highV i (App _ f x) = max (highV i f) (highV i x)
699highV i _ = i
701envPos x i [] = 0
702envPos x i ((y, _) : ys) | x == y = i
703 | otherwise = envPos x (i + 1) ys
706-- If there are any clashes of constructors, deem it unrecoverable, otherwise some
707-- more work may help.
708-- FIXME: Depending on how overloading gets used, this may cause problems. Better
709-- rethink overloading properly...
710-- ASSUMPTION: inputs are in normal form
711--
712-- Issue #1722 on the issue tracker https://github.com/idris-lang/Idris-dev/issues/1722
713--
714recoverable t@(App _ _ _) _
715 | (P _ (UN l) _, _) <- unApply t, l == txt "Lazy'" = False
716recoverable _ t@(App _ _ _)
717 | (P _ (UN l) _, _) <- unApply t, l == txt "Lazy'" = False
718recoverable (P (DCon _ _ _) x _) (P (DCon _ _ _) y _) = x == y
719recoverable (P (TCon _ _) x _) (P (TCon _ _) y _) = x == y
720recoverable (TType _) (P (DCon _ _ _) y _) = False
721recoverable (UType _) (P (DCon _ _ _) y _) = False
722recoverable (Constant _) (P (DCon _ _ _) y _) = False
723recoverable (Constant x) (Constant y) = x == y
724recoverable (P (DCon _ _ _) x _) (TType _) = False
725recoverable (P (DCon _ _ _) x _) (UType _) = False
726recoverable (P (DCon _ _ _) x _) (Constant _) = False
727recoverable (TType _) (P (TCon _ _) y _) = False
728recoverable (UType _) (P (TCon _ _) y _) = False
729recoverable (Constant _) (P (TCon _ _) y _) = False
730recoverable (P (TCon _ _) x _) (TType _) = False
731recoverable (P (TCon _ _) x _) (UType _) = False
732recoverable (P (TCon _ _) x _) (Constant _) = False
733recoverable (P (DCon _ _ _) x _) (P (TCon _ _) y _) = False
734recoverable (P (TCon _ _) x _) (P (DCon _ _ _) y _) = False
735recoverable p@(TType _) (App _ f a) = recoverable p f
736recoverable p@(UType _) (App _ f a) = recoverable p f
737recoverable p@(Constant _) (App _ f a) = recoverable p f
738recoverable (App _ f a) p@(TType _) = recoverable f p
739recoverable (App _ f a) p@(UType _) = recoverable f p
740recoverable (App _ f a) p@(Constant _) = recoverable f p
741recoverable p@(P _ n _) (App _ f a) = recoverable p f
742recoverable (App _ f a) p@(P _ _ _) = recoverable f p
743recoverable (App _ f a) (App _ f' a')
744 | f == f' = recoverable a a'
745recoverable (App _ f a) (App _ f' a')
746 = recoverable f f' -- && recoverable a a'
747recoverable f (Bind _ (Pi _ _ _) sc)
748 | (P (DCon _ _ _) _ _, _) <- unApply f = False
749 | (P (TCon _ _) _ _, _) <- unApply f = False
750 | (Constant _) <- f = False
751 | TType _ <- f = False
752 | UType _ <- f = False
753recoverable (Bind _ (Pi _ _ _) sc) f
754 | (P (DCon _ _ _) _ _, _) <- unApply f = False
755 | (P (TCon _ _) _ _, _) <- unApply f = False
756 | (Constant _) <- f = False
757 | TType _ <- f = False
758 | UType _ <- f = False
759recoverable (Bind _ (Lam _) sc) f = recoverable sc f
760recoverable f (Bind _ (Lam _) sc) = recoverable f sc
761recoverable x y = True
763errEnv :: [(a, Binder b)] -> [(a, b)]
764errEnv = map (\(x, b) -> (x, binderTy b))
766holeIn :: Env -> Name -> Bool
767holeIn env n = case lookup n env of
768 Just (Hole _) -> True
769 Just (Guess _ _) -> True
770 _ -> False
772patIn :: Env -> Name -> Bool
773patIn env n = case lookup n env of
774 Just (PVar _) -> True
775 Just (PVTy _) -> True
776 _ -> False