28ecd81 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Erase unused arguments when compiling

commit28ecd81d562b957f6c69eaac162151bdf6aaa0aa authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 20 Oct 2012, 17:10 (14 years ago) parentb2f8c4c

7 files changed+31−6

compare with master

unifiedsplit

src/Core/Elaborate.hs+2−1 src/Core/ProofState.hs+3−1 src/IRTS/Compiler.hs+13−1 src/IRTS/Defunctionalise.hs+1 src/IRTS/Lang.hs+2−1 src/Idris/ElabTerm.hs+9−1 src/Idris/UnusedArgs.hs+1−1

src/Core/Elaborate.hs+2−1

@@ -317,8 +317,9 @@ apply fn imps =

317317 -- HMMM: Actually, if we get it wrong, the typechecker will complain!

318318 -- so do nothing

319319 ptm <- get_term

320+ hs <- get_holes

320321 ES (p, a) s prev <- get

321− let dont = nub $ dontunify p ++

322+ let dont = nub $ head hs : dontunify p ++

322323 if null imps then [] -- do all we can

323324 else

324325 map fst (filter (not.snd) (zip args (map fst imps)))

src/Core/ProofState.hs+3−1

@@ -266,6 +266,7 @@ focus n ctxt env t = do action (\ps -> let hs = holes ps in

266266 if n `elem` hs

267267 then ps { holes = n : (hs \\ [n]) }

268268 else ps)

269+ ps <- get

269270 return t

270271

271272movelast :: Name -> RunTactic

@@ -357,7 +358,8 @@ solve ctxt env (Bind x (Guess ty val) sc)

357358 instances = instances ps \\ [x] })

358359 return $ {- Bind x (Let ty val) sc -} instantiate val (pToV x sc)

359360 | otherwise = lift $ tfail $ IncompleteTerm val

360−solve _ _ h = fail $ "Not a guess " ++ show h

361+solve _ _ h = do ps <- get

362+ fail $ "Not a guess " ++ show h ++ "\n" ++ show (holes ps, pterm ps)

361363

362364introTy :: Raw -> Maybe Name -> RunTactic

363365introTy ty mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

src/IRTS/Compiler.hs+13−1

@@ -120,6 +120,7 @@ class ToIR a where

120120build :: (Name, Def) -> Idris (Name, LDecl)

121121build (n, d)

122122 = do i <- getIState

123+ traceUnused n

123124 case lookup n (idris_scprims i) of

124125 Just (ar, op) ->

125126 let args = map (\x -> MN x "op") [0..] in

@@ -169,10 +170,20 @@ instance ToIR (TT Name) where

169170 return t' -- TODO

170171 | (P (DCon t a) n _, args) <- unApply tm

171172 = irCon env t a n args

173+ | (P _ n _, args) <- unApply tm

174+ = do i <- get

175+ let unused = case lookupCtxt Nothing n (idris_callgraph i) of

176+ [CGInfo _ _ _ unusedpos] -> unusedpos

177+ _ -> []

178+ args' <- mapM (ir' env) args

179+ return (LApp False (LV (Glob n)) (mkUnused unused 0 args'))

172180 | (f, args) <- unApply tm

173181 = do f' <- ir' env f

174182 args' <- mapM (ir' env) args

175183 return (LApp False f' args')

184+ where mkUnused u i [] = []

185+ mkUnused u i (x : xs) | i `elem` u = LNothing : mkUnused u (i + 1) xs

186+ | otherwise = x : mkUnused u (i + 1) xs

176187 ir' env (P _ n _) = return $ LV (Glob n)

177188 ir' env (V i) | i < length env = return $ LV (Glob (env!!i))

178189 | otherwise = error $ "IR fail " ++ show i ++ " " ++ show tm

@@ -184,10 +195,11 @@ instance ToIR (TT Name) where

184195 = do sc' <- ir' (n : env) sc

185196 v' <- ir' env v

186197 return $ LLet n v' sc'

187− ir' env (Bind _ _ _) = return $ LConst (I 424242)

198+ ir' env (Bind _ _ _) = return $ LNothing

188199 ir' env (Proj t i) = do t' <- ir' env t

189200 return $ LProj t' i

190201 ir' env (Constant c) = return $ LConst c

202+ ir' env (Set _) = return $ LNothing

191203 ir' env _ = return $ LError "Impossible"

192204

193205 irCon env t arity n args

src/IRTS/Defunctionalise.hs+1

@@ -189,6 +189,7 @@ instance Show DExp where

189189 = "foreign " ++ n ++ "(" ++ showSep ", " (map (show' env) (map snd args)) ++ ")"

190190 show' env (DOp f args) = show f ++ "(" ++ showSep ", " (map (show' env) args) ++ ")"

191191 show' env (DError str) = "error " ++ show str

192+ show' env DNothing = "____"

192193

193194 showAlt env (DConCase _ n args e)

194195 = show n ++ "(" ++ showSep ", " (map show args) ++ ") => "

src/IRTS/Lang.hs+2−1

@@ -143,7 +143,7 @@ lift env (LForeign l t s args) = do args' <- mapM (liftF env) args

143143lift env (LOp f args) = do args' <- mapM (lift env) args

144144 return (LOp f args')

145145lift env (LError str) = return $ LError str

146−

146+lift env LNothing = return $ LNothing

147147

148148-- Return variables in list which are used in the expression

149149

@@ -189,6 +189,7 @@ instance Show LExp where

189189 = "foreign " ++ n ++ "(" ++ showSep ", " (map (show' env) (map snd args)) ++ ")"

190190 show' env (LOp f args) = show f ++ "(" ++ showSep ", " (map (show' env) args) ++ ")"

191191 show' env (LError str) = "error " ++ show str

192+ show' env LNothing = "____"

192193

193194 showAlt env (LConCase _ n args e)

194195 = show n ++ "(" ++ showSep ", " (map show args) ++ ") => "

src/Idris/ElabTerm.hs+9−1

@@ -174,12 +174,20 @@ elab ist info pattern tcgen fn tm

174174 elab' ina@(_, a) (PLam n Placeholder sc)

175175 = do attack; intro (Just n); elabE (True, a) sc; solve

176176 elab' ina@(_, a) (PLam n ty sc)

177− = do tyn <- unique_hole (MN 0 "lamty")

177+ = do hsin <- get_holes

178+ ptmin <- get_term

179+ tyn <- unique_hole (MN 0 "lamty")

178180 claim tyn RSet

179181 attack

182+ ptm <- get_term

183+ hs <- get_holes

184+ -- trace ("BEFORE:\n" ++ show hsin ++ "\n" ++ show ptmin ++

185+ -- "\nNOW:\n" ++ show hs ++ "\n" ++ show ptm) $

180186 introTy (Var tyn) (Just n)

181187 -- end_unify

182188 focus tyn

189+ ptm <- get_term

190+ hs <- get_holes

183191 elabE (True, a) ty

184192 elabE (True, a) sc

185193 solve

src/Idris/UnusedArgs.hs+1−1

@@ -49,7 +49,7 @@ used path g j

4949 used ((g,j):path) g' j') garg

5050 -- used on any route from here, or not used recursively

5151 return (null recused || or recused)

52− _ -> return False -- clearly...

52+ _ -> return True -- no definition, assume used

5353

5454getFargpos :: [(Name, [[Name]])] -> (Name, Int) -> [(Name, Int, (Name, Int))]

5555getFargpos calls (n, i) = concatMap (getCallArgpos n i) calls