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

git.iko.soy/Idris-dev

Ctor erasure fixed.

commit589bb4bcf486acf3a4a92ac4011b4c22adf5036f authorMatus Tejiscak <ziman@functor.sk> dateWed 5 Feb 2014, 20:14 (13 years ago) parent238569e

5 files changed+40−11

compare with master

unifiedsplit

src/IRTS/Compiler.hs+15−2 src/IRTS/Simplified.hs+1 src/Idris/Core/CaseTree.hs+1−1 src/Idris/Core/TT.hs+3−3 src/Idris/Erasure.hs+20−5

src/IRTS/Compiler.hs+15−2

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

2121import Idris.Erasure

2222import Idris.Error

2323

24+import Debug.Trace

25+

2426import Idris.Core.TT

2527import Idris.Core.Evaluate

2628import Idris.Core.CaseTree

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

5052

5153 -- TODO: DEBUG-ONLY, remove

5254 ctx <- tt_ctxt <$> getIState

53− let depMap = buildDepMap ctx used

55+ ci <- idris_classes <$> getIState

56+ let depMap = buildDepMap ci ctx used

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

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

5659

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

127130 cg <- idris_callgraph <$> getIState

128131 case lookupCtxt n cg of

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

130− _ -> return ()

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

131134

132135irMain :: TT Name -> Idris LDecl

133136irMain tm = do i <- ir tm

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

252255 e' <- ir' env e

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

254257 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+

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

256269 = irCon env t a n args

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

src/IRTS/Simplified.hs+1

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

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

124124 = do xs' <- checkDefs ctxt xs

125125 return xs'

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

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

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

128129 (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)

583583 | delay == txt "Delay"

584584 -> if proj then mkForce n arg sc

585585 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

587587 else Case n as

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

589589 else Case n as

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

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

324324 pretty = encloseSep empty empty comma . map pretty

325325

326326instance Show Name where

327− show (UN n) = str n

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

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

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

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

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

331− show (SN s) = show s

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

332332 show NErased = "_"

333333

334334instance Show SpecialName where

src/Idris/Erasure.hs+20−5

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

1111import Idris.Core.Evaluate

1212

1313import Debug.Trace

14+import System.IO.Unsafe

1415

1516import Control.Arrow

1617import Control.Applicative

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

7273

7374-- Build the dependency graph,

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

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

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

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

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

7778 where

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

7980 addPostulates :: Deps -> Deps

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

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

161162

162163 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

163171 getDepsSC fn es vs ImpossibleCase = M.empty

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

165173 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

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

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

173181 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

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

175185

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

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

245255

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

247257 -- the following code marks them as completely used

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

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)]

261+ `ins` unconditionalDeps args

262+

263+ Proj t i

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

249265

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

251267 where

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

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

256272

257273 -- projections (= methods)

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

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

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

260275

261276 -- the easy cases

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