589bb4b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Ctor erasure fixed.

589bb4bMatus Tejiscak13 years ago

src/IRTS/Compiler.hs+15−2

compare with master

unifiedsplit

@@ -21,6 +21,8 @@ import Idris.AbsSyntax

21import Idris.Erasure

22import Idris.Error

24+import Debug.Trace

25+

24import Idris.Core.TT

26import Idris.Core.TT

25import Idris.Core.Evaluate

27import Idris.Core.Evaluate

26import Idris.Core.CaseTree

28import Idris.Core.CaseTree

@@ -50,7 +52,8 @@ compile codegen f tm

51 -- TODO: DEBUG-ONLY, remove

53 -- TODO: DEBUG-ONLY, remove

52 ctx <- tt_ctxt <$> getIState

54 ctx <- tt_ctxt <$> getIState

55+ ci <- idris_classes <$> getIState

53− let depMap = buildDepMap ctx used

56+ let depMap = buildDepMap ci ctx used

54 let printItem (cond, deps) = show (S.toList cond) ++ " -> " ++ show (S.toList deps)

57 let printItem (cond, deps) = show (S.toList cond) ++ " -> " ++ show (S.toList deps)

55 -- iLOG $ "USAGE ANALYSIS:\n" ++ unlines (map printItem . M.toList $ depMap)

58 -- iLOG $ "USAGE ANALYSIS:\n" ++ unlines (map printItem . M.toList $ depMap)

@@ -127,7 +130,7 @@ storeUsage n args = do

127 cg <- idris_callgraph <$> getIState

130 cg <- idris_callgraph <$> getIState

128 case lookupCtxt n cg of

131 case lookupCtxt n cg of

129 [x] -> addToCG n x{ usedpos = IS.toList args }

132 [x] -> addToCG n x{ usedpos = IS.toList args }

130− _ -> return ()

133+ _ -> addToCG n (CGInfo [] [] [] [] (IS.toList args)) -- data ctors

131

134

132irMain :: TT Name -> Idris LDecl

135irMain :: TT Name -> Idris LDecl

133irMain tm = do i <- ir tm

136irMain tm = do i <- ir tm

@@ -252,6 +255,16 @@ instance ToIR (TT Name) where

252 e' <- ir' env e

255 e' <- ir' env e

253 return (LCase x' [LConCase 0 (sNS (sUN "False") ["Bool","Prelude"]) [] e',

256 return (LCase x' [LConCase 0 (sNS (sUN "False") ["Bool","Prelude"]) [] e',

254 LConCase 1 (sNS (sUN "True") ["Bool","Prelude"]) [] t'])

257 LConCase 1 (sNS (sUN "True") ["Bool","Prelude"]) [] t'])

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

259+ = do

260+ cg <- idris_callgraph <$> getIState

261+ iLOG $ "DCTOR-LEAD " ++ show n ++ " -- " ++ show (lookupCtxt n cg)

262+ case lookupCtxtExact n cg of

263+ Just (CGInfo _ _ _ _ usedpos)

264+ | ("DCTOR", n, usedpos) `traceShow` True

265+ -> irCon env t a n [if i `elem` usedpos then a else Erased | (i,a) <- zip [0..] args]

266+ Nothing -> irCon env t a n args

267+

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

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

256 = irCon env t a n args

269 = irCon env t a n args

257 | (P (TCon t a) n _, args) <- unApply tm

270 | (P (TCon t a) n _, args) <- unApply tm

src/IRTS/Simplified.hs+1

@@ -123,6 +123,7 @@ checkDefs ctxt [] = return []

123checkDefs ctxt (con@(n, DConstructor _ _ _) : xs)

124 = do xs' <- checkDefs ctxt xs

125 return xs'

126+checkDefs ctxt ((n, DFun n' args exp) : xs) | ("CHECK DEF", n, n', args, exp) `traceShow` False = undefined

126checkDefs ctxt ((n, DFun n' args exp) : xs)

127checkDefs ctxt ((n, DFun n' args exp) : xs)

127 = do let sexp = evalState (simplify True exp) (ctxt, 0)

128 = do let sexp = evalState (simplify True exp) (ctxt, 0)

128 (exp', locs) <- runStateT (scopecheck ctxt (zip args [0..]) sexp) (length args)

129 (exp', locs) <- runStateT (scopecheck ctxt (zip args [0..]) sexp) (length args)

src/Idris/Core/CaseTree.hs+1−1

@@ -583,7 +583,7 @@ prune proj (Case n alts)

583 | delay == txt "Delay"

584 -> if proj then mkForce n arg sc

585 else Case n as

586− as@[ConCase cn i args sc] -> if proj then mkProj n 0 args sc

586+ as@[ConCase cn i args sc] -> if proj && False then mkProj n 0 args sc

587 else Case n as

588 as@[SucCase cn sc] -> if proj then mkProj n (-1) [cn] sc

589 else Case n as

src/Idris/Core/TT.hs+3−3

@@ -324,11 +324,11 @@ instance Pretty [Name] OutputAnnotation where

324 pretty = encloseSep empty empty comma . map pretty

325

326instance Show Name where

327− show (UN n) = str n

327+ show (UN n) = "UN:" ++ show (str n)

328− show (NS n s) = showSep "." (map T.unpack (reverse s)) ++ "." ++ show n

328+ show (NS n s) = "NS." ++ showSep "." (map T.unpack (reverse s)) ++ "." ++ show n

329 show (MN _ u) | u == txt "underscore" = "_"

330 show (MN i s) = "{" ++ str s ++ show i ++ "}"

331− show (SN s) = show s

331+ show (SN s) = "SN." ++ show s

332 show NErased = "_"

333

334instance Show SpecialName where

src/Idris/Erasure.hs+20−5

@@ -11,6 +11,7 @@ import Idris.Core.TT

11import Idris.Core.Evaluate

13import Debug.Trace

14+import System.IO.Unsafe

15import Control.Arrow

16import Control.Arrow

16import Control.Applicative

17import Control.Applicative

@@ -72,8 +73,8 @@ forwardChain deps

73-- Build the dependency graph,

74-- Build the dependency graph,

74-- starting the depth-first search from a list of Names.

75-- starting the depth-first search from a list of Names.

75−buildDepMap :: Context -> [Name] -> Deps

76+buildDepMap :: Ctxt ClassInfo -> Context -> [Name] -> Deps

76−buildDepMap ctx ns = addPostulates $ dfs S.empty M.empty ns

77+buildDepMap ci ctx ns = addPostulates $ dfs S.empty M.empty ns

77 where

78 where

78 -- mark the result of Main.main as used with the empty assumption

79 -- mark the result of Main.main as used with the empty assumption

79 addPostulates :: Deps -> Deps

80 addPostulates :: Deps -> Deps

@@ -160,6 +161,13 @@ buildDepMap ctx ns = addPostulates $ dfs S.empty M.empty ns

160 etaExpand (n : ns) t = etaExpand ns (App t (P Ref n Erased))

161 etaExpand (n : ns) t = etaExpand ns (App t (P Ref n Erased))

161

162

162 getDepsSC :: Name -> [Name] -> Vars -> SC -> Deps

163 getDepsSC :: Name -> [Name] -> Vars -> SC -> Deps

164+ getDepsSC fn es vs (STerm t)

165+ | show fn == "SN.I-Char instance of NS.Prelude.Classes.UN:\"Ord\""

166+ , ("ORDINST", fn, t) `traceShow` True

167+ , "===" `traceShow` True

168+ , unsafePerformIO (mapM_ print . M.toList $ getDepsTerm vs [] (S.singleton (fn, Result)) (etaExpand es t)) `traceShow` True

169+ , "===" `traceShow` False

170+ = undefined

163 getDepsSC fn es vs ImpossibleCase = M.empty

171 getDepsSC fn es vs ImpossibleCase = M.empty

164 getDepsSC fn es vs (UnmatchedCase msg) = M.empty

172 getDepsSC fn es vs (UnmatchedCase msg) = M.empty

165 getDepsSC fn es vs (ProjCase t alt) = error "ProjCase not supported"

173 getDepsSC fn es vs (ProjCase t alt) = error "ProjCase not supported"

@@ -171,6 +179,8 @@ buildDepMap ctx ns = addPostulates $ dfs S.empty M.empty ns

171 = M.insertWith S.union (S.singleton (fn, Result)) casedVar -- add this dep to all deps

179 = M.insertWith S.union (S.singleton (fn, Result)) casedVar -- add this dep to all deps

172 $ unionMap (getDepsAlt fn es vs casedVar) alts -- coming from the whole subtree

180 $ unionMap (getDepsAlt fn es vs casedVar) alts -- coming from the whole subtree

173 where

181 where

182+ -- TODO: use effect instead of casedVar to mark the ctor tag

183+ -- effect = S.insert (typeName, Result) casedVar -- mark the tag of the type name as used

174 casedVar = fromMaybe (error $ "nonpatvar in case: " ++ show n) (M.lookup n vs)

184 casedVar = fromMaybe (error $ "nonpatvar in case: " ++ show n) (M.lookup n vs)

175

185

176 getDepsAlt :: Name -> [Name] -> Vars -> Var -> CaseAlt -> Deps

186 getDepsAlt :: Name -> [Name] -> Vars -> Var -> CaseAlt -> Deps

@@ -245,7 +255,13 @@ buildDepMap ctx ns = addPostulates $ dfs S.empty M.empty ns

245

255

246 -- TODO: figure out what to do with methods

256 -- TODO: figure out what to do with methods

247 -- the following code marks them as completely used

257 -- the following code marks them as completely used

258+ Proj (P Ref n@(SN (InstanceN className parms)) _) i

259+ | [CI ctorName ms ds dscs ps is] <- lookupCtxt className ci

260+ -> S.fromList [(ctorName, Arg i), (n, Result)]

248− Proj t i -> getDepsTerm vs bs cd t `M.union` unconditionalDeps args

261+ `ins` unconditionalDeps args

262+

263+ Proj t i

264+ -> error $ "cannot analyse projection !" ++ show i ++ " of " ++ show t

249

265

250 _ -> error $ "cannot analyse application of " ++ show fun ++ " to " ++ show args

266 _ -> error $ "cannot analyse application of " ++ show fun ++ " to " ++ show args

251 where

267 where

@@ -255,8 +271,7 @@ buildDepMap ctx ns = addPostulates $ dfs S.empty M.empty ns

255 unconditionalDeps args = unionMap (getDepsTerm vs bs cd) args

271 unconditionalDeps args = unionMap (getDepsTerm vs bs cd) args

256

272

257 -- projections (= methods)

273 -- projections (= methods)

258− getDepsTerm vs bs cd (Proj t i) | ("PROJ", t, S.toList cd) `traceShow` False = undefined

274+ getDepsTerm vs bs cd (Proj t i) = getDepsTerm vs bs cd t -- TODO?

259− getDepsTerm vs bs cd (Proj t i) = getDepsTerm vs bs cd t

260

275

261 -- the easy cases

276 -- the easy cases

262 getDepsTerm vs bs cd (Constant _) = M.empty

277 getDepsTerm vs bs cd (Constant _) = M.empty