@@ -14,16 +14,19 @@ import Debug.Trace
1414
1515-- terms which need to be injective, with the things we're trying to unify
1616-- at the time
17−type UInfo = [(TT Name, TT Name, TT Name)]
17+
18+type Injs = [(TT Name, TT Name, TT Name)]
19+
20+data UInfo = UI Int Injs
1821
1922unify :: Context -> Env -> TT Name -> TT Name -> TC ([(Name, TT Name)],
20− UInfo)
23+ Injs)
2124unify ctxt env topx topy
2225 = case runStateT
2326 (un' False [] (normalise ctxt env topx) (normalise ctxt env topy))
24− [] of
25− OK (v, inj) -> return (filter notTrivial v, inj)
26− Error e -> tfail $ CantUnify topx topy e
27+ (UI 0 []) of
28+ OK (v, (UI _ inj)) -> return (filter notTrivial v, inj)
29+ Error e -> tfail $ CantUnify topx topy e 0
2730 where
2831 notTrivial (x, P _ x' _) = x /= x'
2932 notTrivial _ = True
@@ -36,34 +39,41 @@ unify ctxt env topx topy
3639 notP (P _ _ _) = False
3740 notP _ = True
3841
42+ sc i = do UI s x <- get
43+ put (UI (s+i) x)
44+
3945 un' :: Bool -> [(Name, Name)] -> TT Name -> TT Name ->
4046 StateT UInfo
4147 TC [(Name, TT Name)]
4248 un' fn bnames (P Bound x _) (P Bound y _)
43− | (x,y) `elem` bnames = return []
49+ | (x,y) `elem` bnames = do sc 1; return []
4450 un' fn bnames (P Bound x _) tm
45− | holeIn env x = do i <- get
46− when (notP tm && fn) $ put ((tm, topx, topy) : i)
51+ | holeIn env x = do UI s i <- get
52+ when (notP tm && fn) $ put (UI s ((tm, topx, topy) : i))
53+ sc 1
4754 return [(x, tm)]
4855 un' fn bnames tm (P Bound y _)
49− | holeIn env y = do i <- get
50− when (notP tm && fn) $ put ((tm, topx, topy) : i)
56+ | holeIn env y = do UI s i <- get
57+ when (notP tm && fn) $ put (UI s ((tm, topx, topy) : i))
58+ sc 1
5159 return [(y, tm)]
5260 un' fn bnames (V i) (P Bound x _)
53− | fst (bnames!!i) == x || snd (bnames!!i) == x = return []
61+ | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []
5462 un' fn bnames (P Bound x _) (V i)
55− | fst (bnames!!i) == x || snd (bnames!!i) == x = return []
63+ | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []
5664
5765 un' fn bnames (App fx ax) (App fy ay)
5866 = mplus (do hf <- un' True bnames fx fy
5967 let ax' = normalise ctxt env (substNames hf ax)
6068 let ay' = normalise ctxt env (substNames hf ay)
6169 ha <- un' False bnames ax' ay'
70+ sc 1
6271 combine bnames hf ha)
6372 (do ha <- un' False bnames ax ay
6473 let fx' = normalise ctxt env (substNames ha fx)
6574 let fy' = normalise ctxt env (substNames ha fy)
6675 hf <- un' False bnames fx' fy'
76+ sc 1
6777 combine bnames hf ha)
6878
6979 un' fn bnames x (Bind n (Lam t) (App y (P Bound n' _)))
@@ -75,29 +85,33 @@ unify ctxt env topx topy
7585 h2 <- un' False ((x,y):bnames) sx sy
7686 combine bnames h1 h2
7787 un' fn bnames x y
78− | x == y = return []
79− | otherwise = fail $ "Can't unify " ++ show x ++ " and " ++ show y
80− ++ " " ++ show bnames ++ " " ++ show env
88+ | x == y = do sc 1; return []
89+ | otherwise = do UI s _ <- get
90+ lift $ tfail (CantUnify x y (Msg "") s)
8191
8292 uB bnames (Let tx vx) (Let ty vy)
8393 = do h1 <- un' False bnames tx ty
8494 h2 <- un' False bnames ty vy
95+ sc 1
8596 combine bnames h1 h2
8697 uB bnames (Guess tx vx) (Guess ty vy)
8798 = do h1 <- un' False bnames tx ty
8899 h2 <- un' False bnames ty vy
100+ sc 1
89101 combine bnames h1 h2
90− uB bnames (Lam tx) (Lam ty) = un' False bnames tx ty
91− uB bnames (Pi tx) (Pi ty) = un' False bnames tx ty
102+ uB bnames (Lam tx) (Lam ty) = do sc 1; un' False bnames tx ty
103+ uB bnames (Pi tx) (Pi ty) = do sc 1; un' False bnames tx ty
92104 uB bnames (Hole tx) (Hole ty) = un' False bnames tx ty
93105 uB bnames (PVar tx) (PVar ty) = un' False bnames tx ty
94− uB bnames _ _ = fail "Can't unify"
106+ uB bnames x y = do UI s _ <- get
107+ lift $ tfail (CantUnify (binderTy x) (binderTy y) (Msg "") s)
95108
96109 combine bnames as [] = return as
97110 combine bnames as ((n, t) : bs)
98111 = case lookup n as of
99112 Nothing -> combine bnames (as ++ [(n,t)]) bs
100113 Just t' -> do un' False bnames t t'
114+ sc 1
101115 combine bnames as bs
102116
103117holeIn :: Env -> Name -> Bool