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