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

src/Core/Elaborate.hs+2−1

compare with master

unifiedsplit

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

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

318 -- so do nothing

319 ptm <- get_term

320+ hs <- get_holes

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

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

321− let dont = nub $ dontunify p ++

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

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

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

323 else

324 else

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

325 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

266 if n `elem` hs

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

268 else ps)

269+ ps <- get

269 return t

270 return t

270

271

271movelast :: Name -> RunTactic

272movelast :: Name -> RunTactic

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

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

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

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

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

359 | otherwise = lift $ tfail $ IncompleteTerm val

360 | otherwise = lift $ tfail $ IncompleteTerm val

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

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

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

361

363

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

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

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

365introTy 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

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

121build (n, d)

122 = do i <- getIState

123+ traceUnused n

123 case lookup n (idris_scprims i) of

124 case lookup n (idris_scprims i) of

124 Just (ar, op) ->

125 Just (ar, op) ->

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

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

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

169 return t' -- TODO

170 return t' -- TODO

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

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

171 = irCon env t a n args

172 = 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'))

172 | (f, args) <- unApply tm

180 | (f, args) <- unApply tm

173 = do f' <- ir' env f

181 = do f' <- ir' env f

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

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

175 return (LApp False f' args')

183 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

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

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

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

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

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

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

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

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

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

185 v' <- ir' env v

196 v' <- ir' env v

186 return $ LLet n v' sc'

197 return $ LLet n v' sc'

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

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

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

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

189 return $ LProj t' i

200 return $ LProj t' i

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

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

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

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

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

192

204

193 irCon env t arity n args

205 irCon env t arity n args

src/IRTS/Defunctionalise.hs+1

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

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

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

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

192+ show' env DNothing = "____"

192

193

193 showAlt env (DConCase _ n args e)

194 showAlt env (DConCase _ n args e)

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

195 = 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

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

144 return (LOp f args')

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

146−

146+lift env LNothing = return $ LNothing

147

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

149

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

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

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

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

192+ show' env LNothing = "____"

192

193

193 showAlt env (LConCase _ n args e)

194 showAlt env (LConCase _ n args e)

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

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

src/Idris/ElabTerm.hs+9−1

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

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

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

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

177+ = do hsin <- get_holes

178+ ptmin <- get_term

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

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

178 claim tyn RSet

180 claim tyn RSet

179 attack

181 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) $

180 introTy (Var tyn) (Just n)

186 introTy (Var tyn) (Just n)

181 -- end_unify

187 -- end_unify

182 focus tyn

188 focus tyn

189+ ptm <- get_term

190+ hs <- get_holes

183 elabE (True, a) ty

191 elabE (True, a) ty

184 elabE (True, a) sc

192 elabE (True, a) sc

185 solve

193 solve

src/Idris/UnusedArgs.hs+1−1

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

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

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

51 return (null recused || or recused)

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

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

53

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

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