git.iko.soy/Idris-dev
on master help sign in
unique_hole needs to check whole context
f31caf5Edwin Brady
src/Core/Elaborate.hs+8−1
compare with master
unifiedsplit
@@ -120,7 +120,8 @@ get_instances = do ES p _ _ <- get
120unique_hole :: Name -> Elab Name
120unique_hole :: Name -> Elab Name
121unique_hole n = do ES p _ _ <- get
121unique_hole n = do ES p _ _ <- get
122 let bs = bound_in (pterm p) ++ bound_in (ptype p)
122 let bs = bound_in (pterm p) ++ bound_in (ptype p)
123− return (uniqueName n (holes p ++ bs))
123+ n' <- uniqueNameCtxt (context p) n (holes p ++ bs)
124+ return n'
124 where
125 where
125 bound_in (Bind n b sc) = n : bi b ++ bound_in sc
126 bound_in (Bind n b sc) = n : bi b ++ bound_in sc
126 where
127 where
@@ -130,6 +131,12 @@ unique_hole n = do ES p _ _ <- get
130 bound_in (App f a) = bound_in f ++ bound_in a
131 bound_in (App f a) = bound_in f ++ bound_in a
131 bound_in _ = []
132 bound_in _ = []
132
133
134+uniqueNameCtxt :: Context -> Name -> [Name] -> Elab Name
135+uniqueNameCtxt ctxt n hs
136+ | n `elem` hs = return $ uniqueName (nextName n) hs
137+ | Just _ <- lookupCtxt n ctxt = return $ uniqueName (nextName n) hs
138+ | otherwise = return n
139+
133elog :: String -> Elab ()
140elog :: String -> Elab ()
134elog str = do ES p logs prev <- get
141elog str = do ES p logs prev <- get
135 put (ES p (logs ++ str ++ "\n") prev)
142 put (ES p (logs ++ str ++ "\n") prev)