git.iko.soy/Idris-dev
on master help sign in
Fix naming problem in unification
1fe537fEdwin Brady
src/Idris/Core/Unify.hs+25−5
compare with master
unifiedsplit
@@ -35,22 +35,24 @@ match_unify :: Context -> Env -> TT Name -> TT Name -> [Name] -> [Name] ->
35 TC [(Name, TT Name)]
35 TC [(Name, TT Name)]
36match_unify ctxt env topx topy dont holes =
36match_unify ctxt env topx topy dont holes =
37 case runStateT (un [] topx topy) (UI 0 []) of
37 case runStateT (un [] topx topy) (UI 0 []) of
38− OK (v, UI _ []) -> return (trimSolutions v)
38+ OK (v, UI _ []) -> return (map (renameBinders env) (trimSolutions v))
39 res ->
39 res ->
40 let topxn = normalise ctxt env topx
40 let topxn = normalise ctxt env topx
41 topyn = normalise ctxt env topy in
41 topyn = normalise ctxt env topy in
42 case runStateT (un [] topxn topyn)
42 case runStateT (un [] topxn topyn)
43 (UI 0 []) of
43 (UI 0 []) of
44 OK (v, UI _ fails) ->
44 OK (v, UI _ fails) ->
45− return (trimSolutions v)
45+ return (map (renameBinders env) (trimSolutions v))
46 Error e ->
46 Error e ->
47 -- just normalise the term we're matching against
47 -- just normalise the term we're matching against
48 case runStateT (un [] topxn topy)
48 case runStateT (un [] topxn topy)
49 (UI 0 []) of
49 (UI 0 []) of
50 OK (v, UI _ fails) ->
50 OK (v, UI _ fails) ->
51− return (trimSolutions v)
51+ return (map (renameBinders env) (trimSolutions v))
52 _ -> tfail e
52 _ -> tfail e
53 where
53 where
54+
55+
54 un names (P _ x _) tm
56 un names (P _ x _) tm
55 | holeIn env x || x `elem` holes
57 | holeIn env x || x `elem` holes
56 = do sc 1; checkCycle names (x, tm)
58 = do sc 1; checkCycle names (x, tm)
@@ -127,6 +129,23 @@ match_unify ctxt env topx topy dont holes =
127 (inst ns tm) (errEnv env))
129 (inst ns tm) (errEnv env))
128 where inst [] tm = tm
130 where inst [] tm = tm
129 inst ((n, _) : ns) tm = inst ns (substV (P Bound n Erased) tm)
131 inst ((n, _) : ns) tm = inst ns (substV (P Bound n Erased) tm)
132+
133+renameBinders :: Env -> (Name, TT Name) -> (Name, TT Name)
134+renameBinders env (x, tm) = (x, uniqueBinders tm)
135+ where
136+ uniqueBinders (Bind n b sc)
137+ | n `elem` map fst env
138+ = let n' = uniqueName n (map fst env) in
139+ Bind n' (fmap uniqueBinders b)
140+ (uniqueBinders (rename n n' sc))
141+ | otherwise = Bind n (fmap uniqueBinders b) (uniqueBinders sc)
142+ uniqueBinders (App f a) = App (uniqueBinders f) (uniqueBinders a)
143+ uniqueBinders t = t
144+
145+ rename n n' (P nt x ty) | n == x = P nt n' ty
146+ rename n n' (Bind x b sc) = Bind x (fmap (rename n n') b) (rename n n' sc)
147+ rename n n' (App f a) = App (rename n n' f) (rename n n' a)
148+ rename n n' t = t
130
149
131trimSolutions ns = dropPairs ns
150trimSolutions ns = dropPairs ns
132 where dropPairs [] = []
151 where dropPairs [] = []
@@ -154,7 +173,7 @@ unify ctxt env topx topy dont holes =
154-- trace ("Unifying " ++ show (topx, topy)) $
173-- trace ("Unifying " ++ show (topx, topy)) $
155 -- don't bother if topx and topy are different at the head
174 -- don't bother if topx and topy are different at the head
156 case runStateT (un False [] topx topy) (UI 0 []) of
175 case runStateT (un False [] topx topy) (UI 0 []) of
157− OK (v, UI _ []) -> return (trimSolutions v,
176+ OK (v, UI _ []) -> return (map (renameBinders env) (trimSolutions v),
158 [])
177 [])
159 res ->
178 res ->
160 let topxn = normalise ctxt env topx
179 let topxn = normalise ctxt env topx
@@ -163,7 +182,8 @@ unify ctxt env topx topy dont holes =
163 case runStateT (un False [] topxn topyn)
182 case runStateT (un False [] topxn topyn)
164 (UI 0 []) of
183 (UI 0 []) of
165 OK (v, UI _ fails) ->
184 OK (v, UI _ fails) ->
166− return (trimSolutions v, reverse fails)
185+ return (map (renameBinders env) (trimSolutions v),
186+ reverse fails)
167-- Error e@(CantUnify False _ _ _ _ _) -> tfail e
187-- Error e@(CantUnify False _ _ _ _ _) -> tfail e
168 Error e -> tfail e
188 Error e -> tfail e
169 where
189 where
src/Idris/ElabDecls.hs+2−2
@@ -1332,7 +1332,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
1332 return (tm, ds, is))
1332 return (tm, ds, is))
1333 logLvl 5 "DONE CHECK"
1333 logLvl 5 "DONE CHECK"
1334 logLvl 2 $ "---> " ++ show rhs'
1334 logLvl 2 $ "---> " ++ show rhs'
1335− when (not (null defer)) $ iLOG $ "DEFERRED " ++ show defer
1335+ when (not (null defer)) $ iLOG $ "DEFERRED " ++ show (map fst defer)
1336 def' <- checkDef fc defer
1336 def' <- checkDef fc defer
1337 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'
1337 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'
1338 addDeferred def''
1338 addDeferred def''
@@ -2126,7 +2126,7 @@ elabDecl' _ _ _ = return () -- skipped this time
2126
2126
2127elabCaseBlock info opts d@(PClauses f o n ps)
2127elabCaseBlock info opts d@(PClauses f o n ps)
2128 = do addIBC (IBCDef n)
2128 = do addIBC (IBCDef n)
2129− logLvl 6 $ "CASE BLOCK: " ++ show (n, d)
2129+ logLvl 5 $ "CASE BLOCK: " ++ show (n, d)
2130 let opts' = nub (o ++ opts)
2130 let opts' = nub (o ++ opts)
2131 -- propagate totality assertion to the new definitions
2131 -- propagate totality assertion to the new definitions
2132 when (AssertTotal `elem` opts) $ setFlags n [AssertTotal]
2132 when (AssertTotal `elem` opts) $ setFlags n [AssertTotal]