git.iko.soy/Idris-dev
on 66ff954 help sign in
Idris-dev/src/Core/Unify.hs
356 lines 16 kB history raw
1{-# LANGUAGE PatternGuards #-}
3module Core.Unify(unify, Fails) where
5import Core.TT
6import Core.Evaluate
8import Control.Monad
9import Control.Monad.State
10import Debug.Trace
12-- Unification is applied inside the theorem prover. We're looking for holes
13-- which can be filled in, by matching one term's normal form against another.
14-- Returns a list of hole names paired with the term which solves them, and
15-- a list of things which need to be injective.
17-- terms which need to be injective, with the things we're trying to unify
18-- at the time
20type Injs = [(TT Name, TT Name, TT Name)]
21type Fails = [(TT Name, TT Name, Env, Err)]
23data UInfo = UI Int Fails
24 deriving Show
26data UResult a = UOK a
27 | UPartOK a
28 | UFail Err
30unify :: Context -> Env -> TT Name -> TT Name -> [Name] -> [Name] ->
31 TC ([(Name, TT Name)], Fails)
32unify ctxt env topx topy dont holes =
33-- trace ("Unifying " ++ show (topx, topy)) $
34 -- don't bother if topx and topy are different at the head
35 case runStateT (un False [] topx topy) (UI 0 []) of
36 OK (v, UI _ []) -> return (filter notTrivial v, [])
37 res ->
38 let topxn = normalise ctxt env topx
39 topyn = normalise ctxt env topy in
40-- trace ("Unifying " ++ show (topx, topy) ++ "\n\n==>\n" ++ show (topxn, topyn) ++ "\n\n" ++ show res ++ "\n\n") $
41 case runStateT (un False [] topxn topyn)
42 (UI 0 []) of
43 OK (v, UI _ fails) ->
44 return (filter notTrivial v, reverse fails)
45-- Error e@(CantUnify False _ _ _ _ _) -> tfail e
46 Error e -> tfail e
47 where
48 notTrivial (x, P _ x' _) = x /= x'
49 notTrivial _ = True
51 headDiff (P (DCon _ _) x _) (P (DCon _ _) y _) = x /= y
52 headDiff (P (TCon _ _) x _) (P (TCon _ _) y _) = x /= y
53 headDiff _ _ = False
55 injective (P (DCon _ _) _ _) = True
56 injective (P (TCon _ _) _ _) = True
57 injective (App f (P _ _ _)) = injective f
58 injective (App f (Constant _)) = injective f
59 injective (App f a) = injective f -- && injective a
60 injective _ = False
62 notP (P _ _ _) = False
63 notP _ = True
65 sc i = do UI s f <- get
66 put (UI (s+i) f)
68 uplus u1 u2 = do UI s f <- get
69 r <- u1
70 UI s f' <- get
71 if (length f == length f')
72 then return r
73 else do put (UI s f); u2
75 un :: Bool -> [(Name, Name)] -> TT Name -> TT Name ->
76 StateT UInfo
77 TC [(Name, TT Name)]
78 un = un'
79-- un fn names x y
80-- = let (xf, _) = unApply x
81-- (yf, _) = unApply y in
82-- if headDiff xf yf then unifyFail x y else
83-- uplus (un' fn names x y)
84-- (un' fn names (hnf ctxt env x) (hnf ctxt env y))
86 un' :: Bool -> [(Name, Name)] -> TT Name -> TT Name ->
87 StateT UInfo
88 TC [(Name, TT Name)]
89 un' fn names x y | x == y = return [] -- shortcut
90 un' fn names topx@(P (DCon _ _) x _) topy@(P (DCon _ _) y _)
91 | x /= y = unifyFail topx topy
92 un' fn names topx@(P (TCon _ _) x _) topy@(P (TCon _ _) y _)
93 | x /= y = unifyFail topx topy
94 un' fn names topx@(P (DCon _ _) x _) topy@(P (TCon _ _) y _)
95 = unifyFail topx topy
96 un' fn names topx@(P (TCon _ _) x _) topy@(P (DCon _ _) y _)
97 = unifyFail topx topy
98 un' fn names topx@(Constant _) topy@(P (TCon _ _) y _)
99 = unifyFail topx topy
100 un' fn names topx@(P (TCon _ _) x _) topy@(Constant _)
101 = unifyFail topx topy
102 un' fn bnames tx@(P _ x _) ty@(P _ y _)
103 | (x,y) `elem` bnames || x == y = do sc 1; return []
104 | injective tx && not (holeIn env y || y `elem` holes)
105 = unifyTmpFail tx ty
106 | injective ty && not (holeIn env x || x `elem` holes)
107 = unifyTmpFail tx ty
108 un' fn bnames xtm@(P _ x _) tm
109 | holeIn env x || x `elem` holes
110 = do UI s f <- get
111 -- injectivity check
112 if (notP tm && fn)
113-- trace (show (x, tm, normalise ctxt env tm)) $
114-- put (UI s ((tm, topx, topy) : i) f)
115 then unifyTmpFail xtm tm
116 else do sc 1
117 checkCycle (x, tm)
118 | not (injective xtm) && injective tm = unifyFail xtm tm
119 un' fn bnames tm ytm@(P _ y _)
120 | holeIn env y || y `elem` holes
121 = do UI s f <- get
122 -- injectivity check
123 if (notP tm && fn)
124-- trace (show (y, tm, normalise ctxt env tm)) $
125-- put (UI s ((tm, topx, topy) : i) f)
126 then unifyTmpFail tm ytm
127 else do sc 1
128 checkCycle (y, tm)
129 | not (injective ytm) && injective tm = unifyFail ytm tm
130 un' fn bnames (V i) (P _ x _)
131 | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []
132 un' fn bnames (P _ x _) (V i)
133 | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []
135 un' fn bnames appx@(App fx ax) appy@(App fy ay)
136 | (injective fx && sameArgStruct appx appy && metavarApp appy)
137 || (injective fy && sameArgStruct appx appy && metavarApp appx)
138 || (injective fx && injective fy)
139 = do let (headx, _) = unApply fx
140 let (heady, _) = unApply fy
141 -- fail quickly if the heads are disjoint
142 checkHeads headx heady
143-- if True then -- (injective fx || injective fy || fx == fy) then
144-- if (injective fx && metavarApp appy) ||
145-- (injective fy && metavarApp appx) ||
146-- (injective fx && injective fy) || fx == fy
147 uplus
148 (do hf <- un' True bnames fx fy
149 let ax' = hnormalise hf ctxt env (substNames hf ax)
150 let ay' = hnormalise hf ctxt env (substNames hf ay)
151 ha <- un' False bnames ax' ay'
152 sc 1
153 combine bnames hf ha)
154 (do ha <- un' False bnames ax ay
155 let fx' = hnormalise ha ctxt env (substNames ha fx)
156 let fy' = hnormalise ha ctxt env (substNames ha fy)
157 hf <- un' False bnames fx' fy'
158 sc 1
159 combine bnames hf ha)
160 | otherwise =
161 do let (headx, argsx) = unApply appx
162 let (heady, argsy) = unApply appy
163 -- traceWhen (headx == heady) (show (appx, appy)) $
164 if (length argsx == length argsy &&
165 ((headx == heady && inenv headx) || (argsx == argsy) ||
166 (and (zipWith sameStruct (headx:argsx) (heady:argsy)))))
167 then
168-- (notFn headx && notFn heady))) then
169 do uf <- un' True bnames headx heady
170 unArgs uf argsx argsy
171 else -- trace ("TMPFAIL " ++ show (appx, appy, injective appx, injective appy)) $
172 unifyTmpFail appx appy
173 where hnormalise [] _ _ t = t
174 hnormalise ns ctxt env t = normalise ctxt env t
175 checkHeads (P (DCon _ _) x _) (P (DCon _ _) y _)
176 | x /= y = unifyFail appx appy
177 checkHeads (P (TCon _ _) x _) (P (TCon _ _) y _)
178 | x /= y = unifyFail appx appy
179 checkHeads (P (DCon _ _) x _) (P (TCon _ _) y _)
180 = unifyFail appx appy
181 checkHeads (P (TCon _ _) x _) (P (DCon _ _) y _)
182 = unifyFail appx appy
183 checkHeads _ _ = return []
185 unArgs as [] [] = return as
186 unArgs as (x : xs) (y : ys)
187 = do let x' = hnormalise as ctxt env (substNames as x)
188 let y' = hnormalise as ctxt env (substNames as y)
189 as' <- un' False bnames x' y'
190 vs <- combine bnames as as'
191 unArgs vs xs ys
193 metavarApp tm = let (f, args) = unApply tm in
194 all (\x -> metavar x || inenv x) (f : args)
195 metavarArgs tm = let (f, args) = unApply tm in
196 all (\x -> metavar x || inenv x) args
197 metavarApp' tm = let (f, args) = unApply tm in
198 all (\x -> pat x || metavar x) (f : args)
200 sameArgStruct appx appy = let (_, ax) = unApply appx
201 (_, ay) = unApply appy in
202 and (zipWith sameStruct ax ay)
204 sameStruct fapp@(App f x) gapp@(App g y)
205 = let (f',a') = unApply fapp
206 (g',b') = unApply gapp in
207 (f' == g' && length a' == length b' &&
208 (injective f' || injective g'))
209 || (sameStruct f g && sameStruct x y)
210 sameStruct (P _ x _) (P _ y _) = True
211 sameStruct (V i) (V j) = i == j
212 sameStruct (Constant x) (Constant y) = True
213 sameStruct (P _ _ _) (Constant y) = True
214 sameStruct (Constant x) (P _ _ _) = True
215 sameStruct (Bind n t sc) (P _ _ _) = True
216 sameStruct (P _ _ _) (Bind n t sc) = True
217 sameStruct (Bind n t sc) (Bind n' t' sc') = sameStruct sc sc'
218 sameStruct _ _ = False
220 metavar t = case t of
221 P _ x _ -> (x `elem` holes || holeIn env x) &&
222 not (x `elem` dont)
223 _ -> False
224 pat t = case t of
225 P _ x _ -> x `elem` holes || patIn env x
226 _ -> False
227 inenv t = case t of
228 P _ x _ -> x `elem` (map fst env)
229 _ -> False
231 notFn t = injective t || metavar t || inenv t
233 un' fn bnames x (Bind n (Lam t) (App y (P Bound n' _)))
234 | n == n' = un' False bnames x y
235 un' fn bnames (Bind n (Lam t) (App x (P Bound n' _))) y
236 | n == n' = un' False bnames x y
237 un' fn bnames x (Bind n (Lam t) (App y (V 0)))
238 = un' False bnames x y
239 un' fn bnames (Bind n (Lam t) (App x (V 0))) y
240 = un' False bnames x y
241-- un' fn bnames (Bind x (PVar _) sx) (Bind y (PVar _) sy)
242-- = un' False ((x,y):bnames) sx sy
243-- un' fn bnames (Bind x (PVTy _) sx) (Bind y (PVTy _) sy)
244-- = un' False ((x,y):bnames) sx sy
245 un' fn bnames (Bind x bx sx) (Bind y by sy)
246 = do h1 <- uB bnames bx by
247 h2 <- un' False ((x,y):bnames) sx sy
248 combine bnames h1 h2
249 un' fn bnames x y
250 | OK True <- convEq' ctxt x y = do sc 1; return []
251 | otherwise = do UI s f <- get
252 let r = recoverable x y
253 let err = CantUnify r
254 topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s
255 if (not r) then lift $ tfail err
256 else do put (UI s ((x, y, env, err) : f))
257 return [] -- lift $ tfail err
259 unifyTmpFail x y
260 = do UI s f <- get
261 let r = recoverable x y
262 let err = CantUnify r
263 topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s
264 put (UI s ((x, y, env, err) : f))
265 return []
267 -- shortcut failure, if we *know* nothing can fix it
268 unifyFail x y = do UI s f <- get
269 let r = recoverable x y
270 let err = CantUnify r
271 topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s
272 put (UI s ((x, y, env, err) : f))
273 lift $ tfail err
276 uB bnames (Let tx vx) (Let ty vy)
277 = do h1 <- un' False bnames tx ty
278 h2 <- un' False bnames ty vy
279 sc 1
280 combine bnames h1 h2
281 uB bnames (Guess tx vx) (Guess ty vy)
282 = do h1 <- un' False bnames tx ty
283 h2 <- un' False bnames ty vy
284 sc 1
285 combine bnames h1 h2
286 uB bnames (Lam tx) (Lam ty) = do sc 1; un' False bnames tx ty
287 uB bnames (Pi tx) (Pi ty) = do sc 1; un' False bnames tx ty
288 uB bnames (Hole tx) (Hole ty) = un' False bnames tx ty
289 uB bnames (PVar tx) (PVar ty) = un' False bnames tx ty
290 uB bnames x y = do UI s f <- get
291 let r = recoverable (binderTy x) (binderTy y)
292 let err = CantUnify r topx topy
293 (CantUnify r (binderTy x) (binderTy y) (Msg "") [] s)
294 (errEnv env) s
295 put (UI s ((binderTy x, binderTy y, env, err) : f))
296 return [] -- lift $ tfail err
298 checkCycle p@(x, P _ _ _) = return [p]
299 checkCycle (x, tm)
300 | not (x `elem` freeNames tm) = return [(x, tm)]
301 | otherwise = lift $ tfail (InfiniteUnify x tm (errEnv env))
303 combineArgs bnames args = ca [] args where
304 ca acc [] = return acc
305 ca acc (x : xs) = do x' <- combine bnames acc x
306 ca x' xs
308 combine bnames as [] = return as
309 combine bnames as ((n, t) : bs)
310 = case lookup n as of
311 Nothing -> combine bnames (as ++ [(n,t)]) bs
312 Just t' -> do ns <- un' False bnames t t'
313 -- make sure there's n mapping from n in ns
314 let ns' = filter (\ (x, _) -> x/=n) ns
315 sc 1
316 combine bnames as (ns' ++ bs)
318 -- If there are any clashes of constructors, deem it unrecoverable, otherwise some
319 -- more work may help.
320 -- FIXME: Depending on how overloading gets used, this may cause problems. Better
321 -- rethink overloading properly...
323 recoverable (P (DCon _ _) x _) (P (DCon _ _) y _)
324 | x == y = True
325 | otherwise = False
326 recoverable (P (TCon _ _) x _) (P (TCon _ _) y _)
327 | x == y = True
328 | otherwise = False
329 recoverable (Constant _) (P (DCon _ _) y _) = False
330 recoverable (P (DCon _ _) x _) (Constant _) = False
331 recoverable (Constant _) (P (TCon _ _) y _) = False
332 recoverable (P (TCon _ _) x _) (Constant _) = False
333 recoverable (P (DCon _ _) x _) (P (TCon _ _) y _) = False
334 recoverable (P (TCon _ _) x _) (P (DCon _ _) y _) = False
335 recoverable p@(Constant _) (App f a) = recoverable p f
336 recoverable (App f a) p@(Constant _) = recoverable f p
337 recoverable p@(P _ n _) (App f a) = recoverable p f
338-- recoverable (App f a) p@(P _ _ _) = recoverable f p
339 recoverable (App f a) (App f' a')
340 = recoverable f f' -- && recoverable a a'
341 recoverable _ _ = True
343errEnv = map (\(x, b) -> (x, binderTy b))
345holeIn :: Env -> Name -> Bool
346holeIn env n = case lookup n env of
347 Just (Hole _) -> True
348 Just (Guess _ _) -> True
349 _ -> False
351patIn :: Env -> Name -> Bool
352patIn env n = case lookup n env of
353 Just (PVar _) -> True
354 Just (PVTy _) -> True
355 _ -> False