git.iko.soy/Idris-dev
on master help sign in
Fix unary apps + ordering of case trees.
f0f566fMatus Tejiscak
src/IRTS/Compiler.hs+35−11
compare with master
unifiedsplit
@@ -400,8 +400,9 @@ irTerm top vs env tm@(App _ f a) = do
400
400
401 -- compile Nat-likes as bigints
401 -- compile Nat-likes as bigints
402 | Just LikeS <- isLikeNat ist n
402 | Just LikeS <- isLikeNat ist n
403− -> irTerm top vs env $
403+ -> irTerm top vs env $ mkApp
404− App Complete (P Ref (sUN "prim__addBigInt") Erased) (Constant $ BI 1)
404+ (P Ref (sUN "prim__addBigInt") Erased)
405+ (Constant (BI 1) : argsPruned)
405
406
406 | otherwise -- not newtype, plain data ctor
407 | otherwise -- not newtype, plain data ctor
407 -> buildApp (LV n) argsPruned
408 -> buildApp (LV n) argsPruned
@@ -674,17 +675,40 @@ irSC top vs (Case up n alts@[ConCase cn a ns sc, DefaultCase sc']) = do
674 detag <- fgetState (opt_detaggable . ist_optimisation cn)
675 detag <- fgetState (opt_detaggable . ist_optimisation cn)
675 if detag
676 if detag
676 then irSC top vs (Case up n [ConCase cn a ns sc])
677 then irSC top vs (Case up n [ConCase cn a ns sc])
678+ else do
679+ likeNat <- isLikeNat <$> getIState <*> pure cn
680+ case likeNat of
681+ -- the annoying case: LikeS is translated into a default case
682+ -- so we need to change the original DefaultCase to Z-case
683+ -- and reorder it before this one
684+ Just LikeS -> do
685+ zCase <- LConstCase (BI 0) <$> irSC top vs sc'
686+ sCase <- irAlt top vs (LV n) (ConCase cn a ns sc)
687+ return $ LCase up (LV n) [zCase, sCase]
688+
689+ -- the usual case
677− else LCase up (LV n) <$> mapM (irAlt top vs (LV n)) alts
690+ _ -> LCase up (LV n) <$> mapM (irAlt top vs (LV n)) alts
678
691
679irSC top vs sc@(Case up n alts) = do
692irSC top vs sc@(Case up n alts) = do
693+ ist <- getIState
694+
695+ if | [ConCase cns as nss scs, ConCase cnz az nsz scz] <- alts
696+ , Just LikeS <- isLikeNat ist cns
697+ -> do
698+ -- reorder to make the Z case come first
699+ zCase <- LConstCase (BI 0) <$> irSC top vs scz
700+ sCase <- irAlt top vs (LV n) (ConCase cns as nss scs)
701+ return $ LCase up (LV n) [zCase, sCase]
702+
703+ | otherwise -> do
680− -- check that neither alternative needs the newtype optimisation,
704+ -- check that neither alternative needs the newtype optimisation,
681− -- see comment above
705+ -- see comment above
682− goneWrong <- or <$> mapM isDetaggable alts
706+ goneWrong <- or <$> mapM isDetaggable alts
683− when goneWrong
707+ when goneWrong
684− $ ifail ("irSC: non-trivial case-match on detaggable data: " ++ show sc)
708+ $ ifail ("irSC: non-trivial case-match on detaggable data: " ++ show sc)
685−
709+
686− -- everything okay
710+ -- everything okay
687− LCase up (LV n) <$> mapM (irAlt top vs (LV n)) alts
711+ LCase up (LV n) <$> mapM (irAlt top vs (LV n)) alts
688 where
712 where
689 isDetaggable (ConCase cn _ _ _) = fgetState $ opt_detaggable . ist_optimisation cn
713 isDetaggable (ConCase cn _ _ _) = fgetState $ opt_detaggable . ist_optimisation cn
690 isDetaggable _ = return False
714 isDetaggable _ = return False