cb90bf8 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #4685 from ziman/generalised-nat-hack

cb90bf8Niklas Larsson8 years ago

CHANGELOG.md+6

compare with master

unifiedsplit

@@ -10,6 +10,12 @@

10 interfaces (i.e. types for names declared `export` and definitions of names

11 declared `public export`) are unchanged.

13+## Miscellaneous updates

14++ Compiler flag `--optimise-nat-like-types` enables compilation

15+ of `Nat`-like type families to big integers. A type family

16+ is `Nat`-like if, after erasure, it has two constructors,

17+ one nullary, the other one with exactly one recursive field.

18+

13# New in 1.3.1

19# New in 1.3.1

15## Tool updates

21## Tool updates

man/idris.1+4

@@ -99,6 +99,10 @@ should not necessarily be seen as production ready nor for industrial use.

99 e.g. corei7 or cortex-m3.

100 --color,--colour Force coloured output

101 --nocolor,--nocolour Disable coloured output

102+ --optimise-nat-like-types,--optimize-nat-like-types

103+ Compile Nat-like types to big ints

104+ --no-optimise-nat-like-types,--no-optimize-nat-like-types

105+ Do not compile Nat-like types to big ints

102 --consolewidth WIDTH Select console width: auto, infinite, nat

106 --consolewidth WIDTH Select console width: auto, infinite, nat

103 --highlight Emit source code highlighting

107 --highlight Emit source code highlighting

104 --no-tactic-deprecation-warnings

108 --no-tactic-deprecation-warnings

src/IRTS/Compiler.hs+131−14

@@ -5,7 +5,8 @@ Description : Coordinates the compilation process.

5License : BSD3

6Maintainer : The Idris Community.

7-}

8−{-# LANGUAGE CPP, FlexibleContexts, PatternGuards, TypeSynonymInstances #-}

8+{-# LANGUAGE CPP, FlexibleContexts, MultiWayIf, NamedFieldPuns, PatternGuards,

9+ TypeSynonymInstances #-}

10module IRTS.Compiler(compile, generate) where

11module IRTS.Compiler(compile, generate) where

@@ -34,6 +35,7 @@ import Control.Category

34import Control.Monad.State

35import Control.Monad.State

35import Data.List

36import Data.List

36import qualified Data.Map as M

37import qualified Data.Map as M

38+import Data.Maybe (maybe)

37import Data.Ord

39import Data.Ord

38import qualified Data.Set as S

40import qualified Data.Set as S

39import System.Directory

41import System.Directory

@@ -393,6 +395,16 @@ irTerm top vs env tm@(App _ f a) = do

393 EQ | isNewtype

395 EQ | isNewtype

394 -> irTerm top vs env (head argsPruned)

396 -> irTerm top vs env (head argsPruned)

395

397

398+ -- compile Nat-likes as bigints

399+ | Just LikeZ <- isLikeNat ist n

400+ -> irTerm top vs env $ Constant (BI 0)

401+

402+ -- compile Nat-likes as bigints

403+ | Just LikeS <- isLikeNat ist n

404+ -> irTerm top vs env $ mkApp

405+ (P Ref (sUN "prim__addBigInt") Erased)

406+ (Constant (BI 1) : argsPruned)

407+

396 | otherwise -- not newtype, plain data ctor

408 | otherwise -- not newtype, plain data ctor

397 -> buildApp (LV n) argsPruned

409 -> buildApp (LV n) argsPruned

398

410

@@ -405,6 +417,14 @@ irTerm top vs env tm@(App _ f a) = do

405 | isNewtype -- newtype but the value is not among args yet

417 | isNewtype -- newtype but the value is not among args yet

406 -> return . padLams $ \[vn] -> LApp False (LV n) [LV vn]

418 -> return . padLams $ \[vn] -> LApp False (LV n) [LV vn]

407

419

420+ -- compile Nat-likes as bigints

421+ -- it seems that prim applications needn't be saturated

422+ | Just LikeS <- isLikeNat ist n

423+ -> irTerm top vs env $

424+ App Complete

425+ (P Ref (sUN "prim__addBigInt") Erased)

426+ (Constant $ BI 1)

427+

408 -- not a newtype, just apply to a constructor

428 -- not a newtype, just apply to a constructor

409 | otherwise

429 | otherwise

410 -> padLams . applyToNames <$> buildApp (LV n) argsPruned

430 -> padLams . applyToNames <$> buildApp (LV n) argsPruned

@@ -501,6 +521,58 @@ irTerm top vs env (TType _) = return LNothing

501irTerm top vs env Erased = return LNothing

521irTerm top vs env Erased = return LNothing

502irTerm top vs env Impossible = return LNothing

522irTerm top vs env Impossible = return LNothing

503

523

524+data LikeNat = LikeZ | LikeS

525+

526+isLikeNat :: IState -> Name -> Maybe LikeNat

527+isLikeNat ist cn

528+ -- Nat itself is special-cased in Idris/DataOpts.hs,

529+ -- which will have already happened at this point.

530+

531+ -- If the optimisation is disabled then nothing looks like Nat.

532+ | GeneralisedNatHack `notElem` opt_optimise (idris_options ist)

533+ = Nothing

534+

535+ | Just cTy <- lookupTyExact cn $ tt_ctxt ist

536+ , (P TCon{} tyN _, _) <- unApply $ getRetTy cTy

537+ , Just (z, s) <- natLikeCtors tyN

538+ = if | cn == z -> Just LikeZ

539+ | cn == s -> Just LikeS

540+ | otherwise -> error $ "isLikeNat: constructor not found in its own family: " ++ show (cn, tyN)

541+

542+ | otherwise = Nothing

543+ where

544+ natLikeCtors :: Name -> Maybe (Name, Name)

545+ natLikeCtors tyN = case lookupCtxtExact tyN $ idris_datatypes ist of

546+ Just TI{con_names = [z, s]}

547+ | 0 <- getUsedCount z

548+ , looksLikeS s

549+ -> Just (z, s)

550+

551+ Just TI{con_names = [s, z]}

552+ | 0 <- getUsedCount z

553+ , looksLikeS s

554+ -> Just (z, s)

555+

556+ _ -> Nothing

557+

558+ getUsedCount :: Name -> Int

559+ getUsedCount n =

560+ maybe 0 (length . usedpos)

561+ $ lookupCtxtExact n

562+ $ idris_callgraph ist

563+

564+ looksLikeS :: Name -> Bool

565+ looksLikeS cn

566+ | Just [(i, _)] <- fmap usedpos $ lookupCtxtExact cn $ idris_callgraph ist

567+ , Just cTy <- lookupTyExact cn $ tt_ctxt ist

568+ , [recTy] <- [recTy | (j, (_n, recTy)) <- zip [0..] (getArgTys cTy), j == i]

569+ , (P TCon{} recTyN _, _) <- unApply recTy

570+ , (P TCon{} tyN _, _) <- unApply $ getRetTy cTy

571+ , recTyN == tyN

572+ = True

573+

574+ | otherwise = False

575+

504doForeign :: Vars -> [Name] -> [Term] -> Idris LExp

576doForeign :: Vars -> [Name] -> [Term] -> Idris LExp

505doForeign vs env (ret : fname : world : args)

577doForeign vs env (ret : fname : world : args)

506 = do args' <- mapM splitArg args

578 = do args' <- mapM splitArg args

@@ -616,18 +688,41 @@ irSC top vs (Case up n alts@[ConCase cn a ns sc, DefaultCase sc']) = do

616 detag <- fgetState (opt_detaggable . ist_optimisation cn)

688 detag <- fgetState (opt_detaggable . ist_optimisation cn)

617 if detag

689 if detag

618 then irSC top vs (Case up n [ConCase cn a ns sc])

690 then irSC top vs (Case up n [ConCase cn a ns sc])

691+ else do

692+ likeNat <- isLikeNat <$> getIState <*> pure cn

693+ case likeNat of

694+ -- the annoying case: LikeS is translated into a default case

695+ -- so we need to change the original DefaultCase to Z-case

696+ -- and reorder it before this one

697+ Just LikeS -> do

698+ zCase <- LConstCase (BI 0) <$> irSC top vs sc'

699+ sCase <- irAlt top vs (LV n) (ConCase cn a ns sc)

700+ return $ LCase up (LV n) [zCase, sCase]

701+

702+ -- the usual case

619− else LCase up (LV n) <$> mapM (irAlt top vs (LV n)) alts

703+ _ -> LCase up (LV n) <$> mapM (irAlt top vs (LV n)) alts

620−

704+

621−irSC top vs sc@(Case up n alts) = do

705+irSC top vs sc@(Case up n alts) = getIState >>= rhs

622− -- check that neither alternative needs the newtype optimisation,

623− -- see comment above

624− goneWrong <- or <$> mapM isDetaggable alts

625− when goneWrong

626− $ ifail ("irSC: non-trivial case-match on detaggable data: " ++ show sc)

627−

628− -- everything okay

629− LCase up (LV n) <$> mapM (irAlt top vs (LV n)) alts

630 where

706 where

707+ rhs ist

708+ | [ConCase cns as nss scs, ConCase cnz az nsz scz] <- alts

709+ , Just LikeS <- isLikeNat ist cns

710+ = do

711+ -- reorder to make the Z case come first

712+ zCase <- LConstCase (BI 0) <$> irSC top vs scz

713+ sCase <- irAlt top vs (LV n) (ConCase cns as nss scs)

714+ return $ LCase up (LV n) [zCase, sCase]

715+

716+ | otherwise = do

717+ -- check that neither alternative needs the newtype optimisation,

718+ -- see comment above

719+ goneWrong <- or <$> mapM isDetaggable alts

720+ when goneWrong

721+ $ ifail ("irSC: non-trivial case-match on detaggable data: " ++ show sc)

722+

723+ -- everything okay

724+ LCase up (LV n) <$> mapM (irAlt top vs (LV n)) alts

725+

631 isDetaggable (ConCase cn _ _ _) = fgetState $ opt_detaggable . ist_optimisation cn

726 isDetaggable (ConCase cn _ _ _) = fgetState $ opt_detaggable . ist_optimisation cn

632 isDetaggable _ = return False

727 isDetaggable _ = return False

633

728

@@ -636,10 +731,32 @@ irSC top vs ImpossibleCase = return LNothing

636irAlt :: Name -> Vars -> LExp -> CaseAlt -> Idris LAlt

731irAlt :: Name -> Vars -> LExp -> CaseAlt -> Idris LAlt

637

732

638-- this leaves out all unused arguments of the constructor

733-- this leaves out all unused arguments of the constructor

639−irAlt top vs _ (ConCase n t args sc) = do

734+irAlt top vs tm (ConCase n t args sc) = do

735+ likeNat <- isLikeNat <$> getIState <*> pure n

640 used <- map fst <$> fgetState (cg_usedpos . ist_callgraph n)

736 used <- map fst <$> fgetState (cg_usedpos . ist_callgraph n)

641 let usedArgs = [a | (i,a) <- zip [0..] args, i `elem` used]

737 let usedArgs = [a | (i,a) <- zip [0..] args, i `elem` used]

738+

739+ case likeNat of

740+ -- like S

741+ Just LikeS -> do

742+ sc' <- irSC top vs sc

743+ case usedArgs of

744+ [pv] -> return $ LDefaultCase $ LLet pv

745+ ( LOp

746+ (LMinus (ATInt ITBig))

747+ [ tm

748+ , LConst (BI 1)

749+ ]

750+ )

751+ sc'

752+

753+ _ -> ifail $ "irAlt/LikeS: multiple used args: " ++ show usedArgs

754+

755+ -- like Z

756+ Just LikeZ -> LConstCase (BI 0) <$> irSC top vs sc

757+

758+ -- not like Nat

642− LConCase (-1) n usedArgs <$> irSC top (methodVars `M.union` vs) sc

759+ Nothing -> LConCase (-1) n usedArgs <$> irSC top (methodVars `M.union` vs) sc

643 where

760 where

644 methodVars = case n of

761 methodVars = case n of

645 SN (ImplementationCtorN interfaceName)

762 SN (ImplementationCtorN interfaceName)

src/Idris/CmdOptions.hs+11

@@ -209,6 +209,17 @@ parseFlags = many $

209 <|> flag' (AddOpt PETransform) (long "partial-eval")

210 <|> flag' (RemoveOpt PETransform) (long "no-partial-eval" <> help "Switch off partial evaluation, mainly for debugging purposes")

211

212+ <|> flag' (AddOpt GeneralisedNatHack) (

213+ long "optimise-nat-like-types"

214+ <> long "optimize-nat-like-types"

215+ <> help "Enable compilation of Nat-like types to bigints"

216+ )

217+ <|> flag' (RemoveOpt GeneralisedNatHack) (

218+ long "no-optimise-nat-like-types"

219+ <> long "no-optimize-nat-like-types"

220+ <> help "Disable compilation of Nat-like types to bigints"

221+ )

222+

212 <|> OptLevel <$> option auto (short 'O' <> long "level")

223 <|> OptLevel <$> option auto (short 'O' <> long "level")

213

224

214 <|> TargetTriple <$> strOption (long "target" <> metavar "TRIPLE" <> help "If supported the codegen will target the named triple.")

225 <|> TargetTriple <$> strOption (long "target" <> metavar "TRIPLE" <> help "If supported the codegen will target the named triple.")

src/Idris/Options.hs+1−1

@@ -125,7 +125,7 @@ data HowMuchDocs = FullDocs | OverviewDocs

125

126data OutputFmt = HTMLOutput | LaTeXOutput

127

128−data Optimisation = PETransform -- ^ partial eval and associated transforms

128+data Optimisation = PETransform | GeneralisedNatHack -- ^ partial eval and associated transforms

129 deriving (Show, Eq, Generic)

130

131-- | Recognised logging categories for the Idris compiler.

test/pkg010/expected+6−3

21 [--codegen TARGET] | [--portable-codegen TARGET] | [--cg-opt ARG] |

23 [--O3] | [--O2] | [--O1] | [--O0] | [--partial-eval] |

24+ [--no-partial-eval] |

25+ [--optimise-nat-like-types|--optimize-nat-like-types] |

26+ [--no-optimise-nat-like-types|--no-optimize-nat-like-types] |

24− [--no-partial-eval] | [-O|--level ARG] | [--target TRIPLE] | [--cpu CPU]

26− [--highlight] | [--no-tactic-deprecation-warnings] |

29+ [--no-tactic-deprecation-warnings] |

27 [--allow-capitalized-pattern-variables]) [FILES] [-v|--version]

30 [--allow-capitalized-pattern-variables]) [FILES] [-v|--version]

28)

31)