b3bf956 · Idris-dev · git.iko.soy

src/Core/Evaluate.hs+1−1

compare with master

unifiedsplit

@@ -151,7 +151,7 @@ usable True n ns

151 case lookup n ls of

152 Just 0 -> return (False, ns)

153 Just i -> return (True, ns)

154− _ -> return (True, ns)

154+ _ -> return (False, ns)

155usable False n ns

156 = case lookup n ns of

157 Just 0 -> return (False, ns)

src/IRTS/Compiler.hs−8

@@ -110,14 +110,6 @@ irMain :: TT Name -> Idris LDecl

110irMain tm = do i <- ir tm

111 return $ LFun [] (MN 0 "runMain") [] (LForce i)

112

113−allNames :: [Name] -> Name -> Idris [Name]

114−allNames ns n | n `elem` ns = return []

115−allNames ns n = do i <- getIState

116− case lookupCtxtExact n (idris_callgraph i) of

117− [ns'] -> do more <- mapM (allNames (n:ns)) (map fst (calls ns'))

118− return (nub (n : concat more))

119− _ -> return [n]

120−

121mkDecls :: Term -> [Name] -> Idris [(Name, LDecl)]

113mkDecls :: Term -> [Name] -> Idris [(Name, LDecl)]

122mkDecls t used

114mkDecls t used

123 = do i <- getIState

115 = do i <- getIState

src/Idris/AbsSyntax.hs+12

@@ -141,6 +141,18 @@ addToCG n cg

141 = do i <- getIState

142 putIState $ i { idris_callgraph = addDef n cg (idris_callgraph i) }

143

144+-- Trace all the names in a call graph starting at the given name

145+getAllNames :: Name -> Idris [Name]

146+getAllNames n = allNames [] n

147+

148+allNames :: [Name] -> Name -> Idris [Name]

149+allNames ns n | n `elem` ns = return []

150+allNames ns n = do i <- getIState

151+ case lookupCtxtExact n (idris_callgraph i) of

152+ [ns'] -> do more <- mapM (allNames (n:ns)) (map fst (calls ns'))

153+ return (nub (n : concat more))

154+ _ -> return [n]

155+

144addCoercion :: Name -> Idris ()

156addCoercion :: Name -> Idris ()

145addCoercion n = do i <- getIState

157addCoercion n = do i <- getIState

146 putIState $ i { idris_coercions = nub $ n : idris_coercions i }

158 putIState $ i { idris_coercions = nub $ n : idris_coercions i }

src/Idris/ElabDecls.hs+3−2

@@ -803,8 +803,9 @@ elabPE info fc caller r =

803 logLvl 5 $ show (newnm, map (concreteArg ist) (snd specapp))

804 idrisCatch

805 (when (undef && all (concreteArg ist) (snd specapp)) $ do

806+ cgns <- getAllNames n

806− let opts = [Specialise ((n, Nothing) :

807+ let opts = [Specialise (map (\x -> (x, Nothing)) cgns ++

807− (mapMaybe specName (snd specapp)))]

808+ mapMaybe specName (snd specapp))]

808 logLvl 3 $ "Specialising application: " ++ show specapp

809 logLvl 3 $ "Specialising application: " ++ show specapp

809 logLvl 2 $ "New name: " ++ show newnm

810 logLvl 2 $ "New name: " ++ show newnm

810 iLOG $ "PE definition type : " ++ (show specTy)

811 iLOG $ "PE definition type : " ++ (show specTy)