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