Refactor implementation of suggestNames in Generalize.hs

agda/src/full/Agda/TypeChecking/Generalize.hs

Lines 375 to 387 in 01f12f0

    
           let suggestNames i [] = return () 
        
               suggestNames i (m : ms) = do 
        
                 -- #4291: Override existing meta name suggestion. If we solved the parent with a new 
        
                 --        meta use the parent name for that, otherwise suffix with a number. 
        
                 let suf | null ms && i == 1, 
        
                           MetaV{} <- instBody inst = "" 
        
                         | otherwise                = "." ++ show i 
        
                 setMetaNameSuggestion m (parentName ++ suf) 
        
                 suggestNames (i + 1) ms 
        
           unless (null metas) $ 
        
             reportSDoc "tc.generalize" 40 $ hcat ["Inherited metas from ", prettyTCM x, ":"] <?> prettyList_ (map prettyTCM metas) 
        
                                       -- Don't suggest names for explicitly named generalizable metas 
        
           Set.fromList metas <$ suggestNames 1 (filter (`Map.notMember` nameMap) metas)

Rather than a for-loop with manual recursion, this can be written with the usual zip [1..] trick and a mapM.
The case for exactly one meta is special and should be treated outside of the loop, rather than checking at every iteration.

Code original in a6db224.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

	let suggestNames i [] = return ()
	suggestNames i (m : ms) = do
	-- #4291: Override existing meta name suggestion. If we solved the parent with a new
	-- meta use the parent name for that, otherwise suffix with a number.
	let suf \| null ms && i == 1,
	MetaV{} <- instBody inst = ""
	\| otherwise = "." ++ show i
	setMetaNameSuggestion m (parentName ++ suf)
	suggestNames (i + 1) ms
	unless (null metas) $
	reportSDoc "tc.generalize" 40 $ hcat ["Inherited metas from ", prettyTCM x, ":"] <?> prettyList_ (map prettyTCM metas)
	-- Don't suggest names for explicitly named generalizable metas
	Set.fromList metas <$ suggestNames 1 (filter (`Map.notMember` nameMap) metas)

Description

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions