60a441b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix bug in compilation of optimised Nats

commit60a441b721ef0eb09178c293434dc721e20849a3 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 14 Sep 2013, 23:00 (13 years ago) parentc254c61

2 files changed+9−5

unifiedsplit

src/Core/CaseTree.hs+4

@@ -501,6 +501,10 @@ prune proj (Case n alts)

501501 [] -> ImpossibleCase

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

503503 else Case n as

504+ -- Bit of a hack here! The default case will always be 0, make sure

505+ -- it gets caught first.

506+ [s@(SucCase _ _), DefaultCase dc]

507+ -> Case n [ConstCase (BI 0) dc, s]

504508 as -> Case n as

505509 where pruneAlt (ConCase cn i ns sc) = ConCase cn i ns (prune proj sc)

506510 pruneAlt (FnCase cn ns sc) = FnCase cn ns (prune proj sc)

src/IRTS/Compiler.hs+5−5

@@ -352,10 +352,10 @@ instance ToIR SC where

352352

353353 ir' (STerm t) = ir t

354354 ir' (UnmatchedCase str) = return $ LError str

355− ir' (ProjCase tm alts) = do alts' <- mapM (mkIRAlt tm) alts

356− tm' <- ir tm

355+ ir' (ProjCase tm alts) = do tm' <- ir tm

356+ alts' <- mapM (mkIRAlt tm') alts

357357 return $ LCase tm' alts'

358− ir' (Case n alts) = do alts' <- mapM (mkIRAlt (P Bound n Erased)) alts

358+ ir' (Case n alts) = do alts' <- mapM (mkIRAlt (LV (Glob n))) alts

359359 return $ LCase (LV (Glob n)) alts'

360360 ir' ImpossibleCase = return LNothing

361361

@@ -379,10 +379,10 @@ instance ToIR SC where

379379 | matchableTy x

380380 = do rhs' <- ir rhs

381381 return $ LDefaultCase rhs'

382− mkIRAlt (P _ orig _) (SucCase n rhs)

382+ mkIRAlt tm (SucCase n rhs)

383383 = do rhs' <- ir rhs

384384 return $ LDefaultCase (LLet n (LOp (LMinus (ATInt ITBig))

385− [LV (Glob orig),

385+ [tm,

386386 LConst (BI 1)]) rhs')

387387-- return $ LSucCase n rhs'

388388 mkIRAlt _ (ConstCase c rhs)