git.iko.soy/Idris-dev
on 875eecc help sign in
Idris-dev/src/Core/Unify.hs
236 lines 10 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 Injs Fails
24 deriving Show
26unify :: Context -> Env -> TT Name -> TT Name -> TC ([(Name, TT Name)],
27 Injs, Fails)
28unify ctxt env topx topy =
29-- trace ("Unifying " ++ show (topx, topy)) $
30 -- don't bother if topx and topy are different at the head
31 case runStateT (un False [] topx topy) (UI 0 [] []) of
32 OK (v, UI _ inj []) -> return (filter notTrivial v, inj, [])
33-- Error e@(CantUnify False _ _ _ _ _) -> tfail e
34 res ->
35 let topxn = normalise ctxt env topx
36 topyn = normalise ctxt env topy in
37-- trace ("Unifying " ++ show (topx, topy) ++ "\n\n==>\n" ++ show (topxn, topyn) ++ "\n\n" ++ show res ++ "\n\n") $
38 case runStateT (un False [] topxn topyn)
39 (UI 0 [] []) of
40 OK (v, UI _ inj fails) ->
41 return (filter notTrivial v, inj, reverse fails)
42 Error e -> tfail e
43 where
44 notTrivial (x, P _ x' _) = x /= x'
45 notTrivial _ = True
47 headDiff (P (DCon _ _) x _) (P (DCon _ _) y _) = x /= y
48 headDiff (P (TCon _ _) x _) (P (TCon _ _) y _) = x /= y
49 headDiff _ _ = False
51 injective (P (DCon _ _) _ _) = True
52 injective (P (TCon _ _) _ _) = True
53 injective (App f a) = injective f
54 injective _ = False
56 notP (P _ _ _) = False
57 notP _ = True
59 sc i = do UI s x f <- get
60 put (UI (s+i) x f)
62 uplus u1 u2 = do UI s i f <- get
63 r <- u1
64 UI s _ f' <- get
65 if (length f == length f')
66 then return r
67 else do put (UI s i f); u2
69 un :: Bool -> [(Name, Name)] -> TT Name -> TT Name ->
70 StateT UInfo
71 TC [(Name, TT Name)]
72 un fn names x y
73 = let (xf, _) = unApply x
74 (yf, _) = unApply y in
75 if headDiff xf yf then unifyFail x y else
76 uplus (un' fn names x y)
77 (un' fn names (hnf ctxt env x) (hnf ctxt env y))
79 un' :: Bool -> [(Name, Name)] -> TT Name -> TT Name ->
80 StateT UInfo
81 TC [(Name, TT Name)]
82 un' fn names x y | x == y = return [] -- shortcut
83 un' fn names topx@(P (DCon _ _) x _) topy@(P (DCon _ _) y _)
84 | x /= y = unifyFail topx topy
85 un' fn names topx@(P (TCon _ _) x _) topy@(P (TCon _ _) y _)
86 | x /= y = unifyFail topx topy
87 un' fn names topx@(P (DCon _ _) x _) topy@(P (TCon _ _) y _)
88 = unifyFail topx topy
89 un' fn names topx@(P (TCon _ _) x _) topy@(P (DCon _ _) y _)
90 = unifyFail topx topy
91 un' fn bnames (P Bound x _) (P Bound y _)
92 | (x,y) `elem` bnames = do sc 1; return []
93 un' fn bnames (P Bound x _) tm
94 | holeIn env x = do UI s i f <- get
95 -- injectivity check
96 when (notP tm && fn) $
97-- trace (show (x, tm, normalise ctxt env tm)) $
98 put (UI s ((tm, topx, topy) : i) f)
99 sc 1
100 checkCycle (x, tm)
101 un' fn bnames tm (P Bound y _)
102 | holeIn env y = do UI s i f <- get
103 -- injectivity check
104 when (notP tm && fn) $
105-- trace (show (y, tm, normalise ctxt env tm)) $
106 put (UI s ((tm, topx, topy) : i) f)
107 sc 1
108 checkCycle (y, tm)
109 un' fn bnames (V i) (P Bound x _)
110 | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []
111 un' fn bnames (P Bound x _) (V i)
112 | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []
114 un' fn bnames appx@(App fx ax) appy@(App fy ay)
115 = do let (headx, _) = unApply fx
116 let (heady, _) = unApply fy
117 checkHeads headx heady
118 uplus -- do the second one if the first adds any errors
119 (do hf <- un' True bnames fx fy
120 let ax' = hnormalise hf ctxt env (substNames hf ax)
121 let ay' = hnormalise hf ctxt env (substNames hf ay)
122 ha <- un False bnames ax' ay'
123 sc 1
124 combine bnames hf ha)
125 (do ha <- un False bnames ax ay
126 let fx' = hnormalise ha ctxt env (substNames ha fx)
127 let fy' = hnormalise ha ctxt env (substNames ha fy)
128 hf <- un' False bnames fx' fy'
129 sc 1
130 combine bnames hf ha)
131 where hnormalise [] _ _ t = t
132 hnormalise ns ctxt env t = hnf ctxt env t
133 checkHeads (P (DCon _ _) x _) (P (DCon _ _) y _)
134 | x /= y = unifyFail appx appy
135 checkHeads (P (TCon _ _) x _) (P (TCon _ _) y _)
136 | x /= y = unifyFail appx appy
137 checkHeads (P (DCon _ _) x _) (P (TCon _ _) y _)
138 = unifyFail appx appy
139 checkHeads (P (TCon _ _) x _) (P (DCon _ _) y _)
140 = unifyFail appx appy
141 checkHeads _ _ = return []
143 un' fn bnames x (Bind n (Lam t) (App y (P Bound n' _)))
144 | n == n' = un' False bnames x y
145 un' fn bnames (Bind n (Lam t) (App x (P Bound n' _))) y
146 | n == n' = un' False bnames x y
147-- un' fn bnames (Bind x (PVar _) sx) (Bind y (PVar _) sy)
148-- = un' False ((x,y):bnames) sx sy
149-- un' fn bnames (Bind x (PVTy _) sx) (Bind y (PVTy _) sy)
150-- = un' False ((x,y):bnames) sx sy
151 un' fn bnames (Bind x bx sx) (Bind y by sy)
152 = do h1 <- uB bnames bx by
153 h2 <- un' False ((x,y):bnames) sx sy
154 combine bnames h1 h2
155 un' fn bnames x y
156 | OK True <- convEq' ctxt x y = do sc 1; return []
157 | otherwise = do UI s i f <- get
158 let r = recoverable x y
159 let err = CantUnify r
160 topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s
161 if (not r) then lift $ tfail err
162 else do put (UI s i ((x, y, env, err) : f))
163 return [] -- lift $ tfail err
165 -- shortcut failure, if we *know* nothing can fix it
166 unifyFail x y = do UI s i f <- get
167 let r = recoverable x y
168 let err = CantUnify r
169 topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s
170 put (UI s i ((x, y, env, err) : f))
171 lift $ tfail err
174 uB bnames (Let tx vx) (Let ty vy)
175 = do h1 <- un' False bnames tx ty
176 h2 <- un' False bnames ty vy
177 sc 1
178 combine bnames h1 h2
179 uB bnames (Guess tx vx) (Guess ty vy)
180 = do h1 <- un' False bnames tx ty
181 h2 <- un' False bnames ty vy
182 sc 1
183 combine bnames h1 h2
184 uB bnames (Lam tx) (Lam ty) = do sc 1; un' False bnames tx ty
185 uB bnames (Pi tx) (Pi ty) = do sc 1; un' False bnames tx ty
186 uB bnames (Hole tx) (Hole ty) = un' False bnames tx ty
187 uB bnames (PVar tx) (PVar ty) = un' False bnames tx ty
188 uB bnames x y = do UI s i f <- get
189 let r = recoverable (binderTy x) (binderTy y)
190 let err = CantUnify r topx topy
191 (CantUnify r (binderTy x) (binderTy y) (Msg "") [] s)
192 (errEnv env) s
193 put (UI s i ((binderTy x, binderTy y, env, err) : f))
194 return [] -- lift $ tfail err
196 checkCycle p@(x, P _ _ _) = return [p]
197 checkCycle (x, tm)
198 | not (x `elem` freeNames tm) = return [(x, tm)]
199 | otherwise = lift $ tfail (InfiniteUnify x tm (errEnv env))
201 combine bnames as [] = return as
202 combine bnames as ((n, t) : bs)
203 = case lookup n as of
204 Nothing -> combine bnames (as ++ [(n,t)]) bs
205 Just t' -> do ns <- un' False bnames t t'
206 -- make sure there's n mapping from n in ns
207 let ns' = filter (\ (x, _) -> x/=n) ns
208 sc 1
209 combine bnames as (ns' ++ bs)
211 -- If there are any clashes of constructors, deem it unrecoverable, otherwise some
212 -- more work may help.
213 -- FIXME: Depending on how overloading gets used, this may cause problems. Better
214 -- rethink overloading properly...
216 recoverable (P (DCon _ _) x _) (P (DCon _ _) y _)
217 | x == y = True
218 | otherwise = False
219 recoverable (P (TCon _ _) x _) (P (TCon _ _) y _)
220 | x == y = True
221 | otherwise = False
222 recoverable (P (DCon _ _) x _) (P (TCon _ _) y _) = False
223 recoverable (P (TCon _ _) x _) (P (DCon _ _) y _) = False
224 recoverable p@(P _ n _) (App f a) = recoverable p f
225-- recoverable (App f a) p@(P _ _ _) = recoverable f p
226 recoverable (App f a) (App f' a')
227 = recoverable f f' -- && recoverable a a'
228 recoverable _ _ = True
230errEnv = map (\(x, b) -> (x, binderTy b))
232holeIn :: Env -> Name -> Bool
233holeIn env n = case lookup n env of
234 Just (Hole _) -> True
235 _ -> False