8e6b636 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Optimisation options

--partial-eval and --no-partial eval (former is the default) -O[0-3] now set packages of optimisation options (although the only one currently existing is partial-eval, which is set at levels >=2) Default -O2

commit8e6b6368a0aad86fd13ea1767fccfebb3f061a30 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 18 Oct 2014, 19:40 (12 years ago) parent03f6913

7 files changed+67−27

compare with master

unifiedsplit

src/IRTS/CodegenCommon.hs−1 src/IRTS/Compiler.hs+1−2 src/Idris/AbsSyntax.hs+28−12 src/Idris/AbsSyntaxTree.hs+11−4 src/Idris/CmdOptions.hs+3−1 src/Idris/Elab/Clause.hs+13−5 src/Idris/REPL.hs+11−2

src/IRTS/CodegenCommon.hs−1

@@ -25,7 +25,6 @@ data CodegenInfo = CodegenInfo { outputFile :: String,

2525 outputType :: OutputType,

2626 targetTriple :: String,

2727 targetCPU :: String,

28− optimisation :: Word,

2928 includes :: [FilePath],

3029 importDirs :: [FilePath],

3130 compileObjs :: [String],

src/IRTS/Compiler.hs+1−2

@@ -89,11 +89,10 @@ compile codegen f tm

8989 Just f -> runIO $ writeFile f (dumpDefuns defuns)

9090 triple <- Idris.AbsSyntax.targetTriple

9191 cpu <- Idris.AbsSyntax.targetCPU

92− optimise <- optLevel

9392 iLOG "Building output"

9493

9594 case checked of

96− OK c -> do return $ CodegenInfo f outty triple cpu optimise

95+ OK c -> do return $ CodegenInfo f outty triple cpu

9796 hdrs impdirs objs libs flags

9897 NONE c (toAlist defuns)

9998 tagged

src/Idris/AbsSyntax.hs+28−12

@@ -608,13 +608,39 @@ logLevel = do i <- getIState

608608setErrContext :: Bool -> Idris ()

609609setErrContext t = do i <- getIState

610610 let opts = idris_options i

611− let opt' = opts { opt_errContext = t }

612− putIState $ i { idris_options = opt' }

611+ let opts' = opts { opt_errContext = t }

612+ putIState $ i { idris_options = opts' }

613613

614614errContext :: Idris Bool

615615errContext = do i <- getIState

616616 return (opt_errContext (idris_options i))

617617

618+getOptimise :: Idris [Optimisation]

619+getOptimise = do i <- getIState

620+ return (opt_optimise (idris_options i))

621+

622+setOptimise :: [Optimisation] -> Idris ()

623+setOptimise newopts = do i <- getIState

624+ let opts = idris_options i

625+ let opts' = opts { opt_optimise = newopts }

626+ putIState $ i { idris_options = opts' }

627+

628+addOptimise :: Optimisation -> Idris ()

629+addOptimise opt = do opts <- getOptimise

630+ setOptimise (nub (opt : opts))

631+

632+removeOptimise :: Optimisation -> Idris ()

633+removeOptimise opt = do opts <- getOptimise

634+ setOptimise ((nub opts) \\ [opt])

635+

636+-- Set appropriate optimisation set for the given level. We only have

637+-- one optimisation that is configurable at the moment, however!

638+setOptLevel :: Int -> Idris ()

639+setOptLevel n | n <= 0 = setOptimise []

640+setOptLevel 1 = setOptimise []

641+setOptLevel 2 = setOptimise [PETransform]

642+setOptLevel n | n >= 3 = setOptimise [PETransform]

643+

618644useREPL :: Idris Bool

619645useREPL = do i <- getIState

620646 return (opt_repl (idris_options i))

@@ -708,16 +734,6 @@ targetCPU :: Idris String

708734targetCPU = do i <- getIState

709735 return (opt_cpu (idris_options i))

710736

711−setOptLevel :: Word -> Idris ()

712−setOptLevel t = do i <- getIState

713− let opts = idris_options i

714− opt' = opts { opt_optLevel = t }

715− putIState $ i { idris_options = opt' }

716−

717−optLevel :: Idris Word

718−optLevel = do i <- getIState

719− return (opt_optLevel (idris_options i))

720−

721737verbose :: Idris Bool

722738verbose = do i <- getIState

723739 return (opt_verbose (idris_options i))

src/Idris/AbsSyntaxTree.hs+11−4

@@ -75,11 +75,11 @@ data IOption = IOption { opt_logLevel :: Int,

7575 opt_importdirs :: [FilePath],

7676 opt_triple :: String,

7777 opt_cpu :: String,

78− opt_optLevel :: Word,

7978 opt_cmdline :: [Opt], -- remember whole command line

8079 opt_origerr :: Bool,

8180 opt_autoSolve :: Bool, -- ^ automatically apply "solve" tactic in prover

82− opt_autoImport :: [FilePath] -- ^ e.g. Builtins+Prelude

81+ opt_autoImport :: [FilePath], -- ^ e.g. Builtins+Prelude

82+ opt_optimise :: [Optimisation]

8383 }

8484 deriving (Show, Eq)

8585

@@ -99,17 +99,22 @@ defaultOpts = IOption { opt_logLevel = 0

9999 , opt_importdirs = []

100100 , opt_triple = ""

101101 , opt_cpu = ""

102− , opt_optLevel = 2

103102 , opt_cmdline = []

104103 , opt_origerr = False

105104 , opt_autoSolve = True

106105 , opt_autoImport = []

106+ , opt_optimise = defaultOptimise

107107 }

108108

109109data PPOption = PPOption {

110110 ppopt_impl :: Bool -- ^^ whether to show implicits

111111} deriving (Show)

112112

113+data Optimisation = PETransform -- partial eval and associated transforms

114+ deriving (Show, Eq)

115+

116+defaultOptimise = [PETransform]

117+

113118-- | Pretty printing options with default verbosity.

114119defaultPPOption :: PPOption

115120defaultPPOption = PPOption { ppopt_impl = False }

@@ -416,7 +421,9 @@ data Opt = Filename String

416421 | EvalExpr String

417422 | TargetTriple String

418423 | TargetCPU String

419− | OptLevel Word

424+ | OptLevel Int

425+ | AddOpt Optimisation

426+ | RemoveOpt Optimisation

420427 | Client String

421428 | ShowOrigErr

422429 | AutoWidth -- ^ Automatically adjust terminal width

src/Idris/CmdOptions.hs+3−1

@@ -80,7 +80,7 @@ parseFlags = many $

8080 <|> flag' NoBuiltins (long "nobuiltins")

8181 <|> flag' NoREPL (long "check" <> help "Typecheck only, don't start the REPL")

8282 <|> (Output <$> strOption (short 'o' <> long "output" <> metavar "FILE" <> help "Specify output file"))

83− <|> flag' TypeCase (long "typecase")

83+-- <|> flag' TypeCase (long "typecase")

8484 <|> flag' TypeInType (long "typeintype")

8585 <|> flag' DefaultTotal (long "total" <> help "Require functions to be total by default")

8686 <|> flag' DefaultPartial (long "partial")

@@ -121,6 +121,8 @@ parseFlags = many $

121121 <|> flag' (OptLevel 2) (long "O2")

122122 <|> flag' (OptLevel 1) (long "O1")

123123 <|> flag' (OptLevel 0) (long "O0")

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

125+ <|> flag' (RemoveOpt PETransform) (long "no-partial-eval")

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

125127 <|> (TargetTriple <$> strOption (long "target" <> metavar "TRIPLE" <> help "Select target triple (for llvm codegen)"))

126128 <|> (TargetCPU <$> strOption (long "cpu" <> metavar "CPU" <> help "Select target CPU e.g. corei7 or cortex-m3 (for LLVM codegen)"))

src/Idris/Elab/Clause.hs+13−5

@@ -59,6 +59,8 @@ elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()

5959elabClauses info fc opts n_in cs = let n = liftname info n_in in

6060 do ctxt <- getContext

6161 ist <- getIState

62+ optimise <- getOptimise

63+ let petrans = PETransform `elem` optimise

6264 inacc <- map fst <$> fgetState (opt_inaccessible . ist_optimisation n)

6365

6466 -- Check n actually exists, with no definition yet

@@ -96,22 +98,28 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

9698 -- If the definition is specialisable, this reduces the

9799 -- RHS

98100 pe_tm <- doPartialEval ist tpats

99− let pats_pe = map (simple_lhs (tt_ctxt ist)) pe_tm

101+ let pats_pe = if petrans

102+ then map (simple_lhs (tt_ctxt ist)) pe_tm

103+ else pats_raw

100104

101105 let tcase = opt_typecase (idris_options ist)

102106

103107 -- Look for 'static' names and generate new specialised

104108 -- definitions for them, as well as generating rewrite rules

105109 -- for partially evaluated definitions

106− newrules <- mapM (\ e -> case e of

107− Left _ -> return []

108− Right (l, r) -> elabPE info fc n r) pats_pe

110+ newrules <- if petrans

111+ then mapM (\ e -> case e of

112+ Left _ -> return []

113+ Right (l, r) -> elabPE info fc n r) pats_pe

114+ else return []

109115

110116 -- Redo transforms with the newly generated transformations, so

111117 -- that the specialised application we've just made gets

112118 -- used in place of the general one

113119 ist <- getIState

114− let pats_transformed = transformPats ist pats_pe

120+ let pats_transformed = if petrans

121+ then transformPats ist pats_pe

122+ else pats_pe

115123

116124 -- Summary of what's about to happen: Definitions go:

117125 --

src/Idris/REPL.hs+11−2

@@ -1441,15 +1441,19 @@ idrisMain opts =

14411441 let importdirs = opt getImportDir opts

14421442 let bcs = opt getBC opts

14431443 let pkgdirs = opt getPkgDir opts

1444− let optimize = case opt getOptLevel opts of

1444+ -- Set default optimisations

1445+ let optimise = case opt getOptLevel opts of

14451446 [] -> 2

14461447 xs -> last xs

1448+ setOptLevel optimise

14471449 let outty = case opt getOutputTy opts of

14481450 [] -> Executable

14491451 xs -> last xs

14501452 let cgn = case opt getCodegen opts of

14511453 [] -> Via "c"

14521454 xs -> last xs

1455+ -- Now set/unset specifically chosen optimisations

1456+ sequence_ (opt getOptimisation opts)

14531457 script <- case opt getExecScript opts of

14541458 [] -> return Nothing

14551459 x:y:xs -> do iputStrLn "More than one interpreter expression found."

@@ -1701,10 +1705,15 @@ getCPU :: Opt -> Maybe String

17011705getCPU (TargetCPU x) = Just x

17021706getCPU _ = Nothing

17031707

1704−getOptLevel :: Opt -> Maybe Word

1708+getOptLevel :: Opt -> Maybe Int

17051709getOptLevel (OptLevel x) = Just x

17061710getOptLevel _ = Nothing

17071711

1712+getOptimisation :: Opt -> Maybe (Idris ())

1713+getOptimisation (AddOpt p) = Just $ addOptimise p

1714+getOptimisation (RemoveOpt p) = Just $ removeOptimise p

1715+getOptimisation _ = Nothing

1716+

17081717getColour :: Opt -> Maybe Bool

17091718getColour (ColourREPL b) = Just b

17101719getColour _ = Nothing