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

src/IRTS/CodegenCommon.hs−1

compare with master

unifiedsplit

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

25 outputType :: OutputType,

26 targetTriple :: String,

27 targetCPU :: String,

28− optimisation :: Word,

29 includes :: [FilePath],

28 includes :: [FilePath],

30 importDirs :: [FilePath],

29 importDirs :: [FilePath],

31 compileObjs :: [String],

30 compileObjs :: [String],

src/IRTS/Compiler.hs+1−2

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

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

90 triple <- Idris.AbsSyntax.targetTriple

91 cpu <- Idris.AbsSyntax.targetCPU

92− optimise <- optLevel

93 iLOG "Building output"

92 iLOG "Building output"

94

93

95 case checked of

94 case checked of

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

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

97 hdrs impdirs objs libs flags

96 hdrs impdirs objs libs flags

98 NONE c (toAlist defuns)

97 NONE c (toAlist defuns)

99 tagged

98 tagged

src/Idris/AbsSyntax.hs+28−12

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

608setErrContext :: Bool -> Idris ()

609setErrContext t = do i <- getIState

610 let opts = idris_options i

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

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

612− putIState $ i { idris_options = opt' }

612+ putIState $ i { idris_options = opts' }

613

614errContext :: Idris Bool

615errContext = do i <- getIState

616 return (opt_errContext (idris_options i))

617

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+

618useREPL :: Idris Bool

644useREPL :: Idris Bool

619useREPL = do i <- getIState

645useREPL = do i <- getIState

620 return (opt_repl (idris_options i))

646 return (opt_repl (idris_options i))

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

708targetCPU = do i <- getIState

734targetCPU = do i <- getIState

709 return (opt_cpu (idris_options i))

735 return (opt_cpu (idris_options i))

710

736

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−

721verbose :: Idris Bool

737verbose :: Idris Bool

722verbose = do i <- getIState

738verbose = do i <- getIState

723 return (opt_verbose (idris_options i))

739 return (opt_verbose (idris_options i))

src/Idris/AbsSyntaxTree.hs+11−4

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

75 opt_importdirs :: [FilePath],

76 opt_triple :: String,

77 opt_cpu :: String,

78− opt_optLevel :: Word,

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

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

80 opt_origerr :: Bool,

79 opt_origerr :: Bool,

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

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

83 }

84 deriving (Show, Eq)

85

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

99 , opt_importdirs = []

100 , opt_triple = ""

101 , opt_cpu = ""

102− , opt_optLevel = 2

103 , opt_cmdline = []

102 , opt_cmdline = []

104 , opt_origerr = False

103 , opt_origerr = False

105 , opt_autoSolve = True

104 , opt_autoSolve = True

106 , opt_autoImport = []

105 , opt_autoImport = []

106+ , opt_optimise = defaultOptimise

107 }

108

109data PPOption = PPOption {

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

111} deriving (Show)

112

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

114+ deriving (Show, Eq)

115+

116+defaultOptimise = [PETransform]

117+

113-- | Pretty printing options with default verbosity.

118-- | Pretty printing options with default verbosity.

114defaultPPOption :: PPOption

119defaultPPOption :: PPOption

115defaultPPOption = PPOption { ppopt_impl = False }

120defaultPPOption = PPOption { ppopt_impl = False }

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

416 | EvalExpr String

421 | EvalExpr String

417 | TargetTriple String

422 | TargetTriple String

418 | TargetCPU String

423 | TargetCPU String

419− | OptLevel Word

424+ | OptLevel Int

425+ | AddOpt Optimisation

426+ | RemoveOpt Optimisation

420 | Client String

427 | Client String

421 | ShowOrigErr

428 | ShowOrigErr

422 | AutoWidth -- ^ Automatically adjust terminal width

429 | AutoWidth -- ^ Automatically adjust terminal width

src/Idris/CmdOptions.hs+3−1

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

60 do ctxt <- getContext

61 ist <- getIState

62+ optimise <- getOptimise

63+ let petrans = PETransform `elem` optimise

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

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

63

65

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

66 -- 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

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

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

97 -- RHS

99 -- RHS

98 pe_tm <- doPartialEval ist tpats

100 pe_tm <- doPartialEval ist tpats

101+ let pats_pe = if petrans

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

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

103+ else pats_raw

100

104

101 let tcase = opt_typecase (idris_options ist)

105 let tcase = opt_typecase (idris_options ist)

102

106

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

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

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

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

105 -- for partially evaluated definitions

109 -- for partially evaluated definitions

110+ newrules <- if petrans

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

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

107− Left _ -> return []

112+ Left _ -> return []

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

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

114+ else return []

109

115

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

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

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

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

112 -- used in place of the general one

118 -- used in place of the general one

113 ist <- getIState

119 ist <- getIState

120+ let pats_transformed = if petrans

114− let pats_transformed = transformPats ist pats_pe

121+ then transformPats ist pats_pe

122+ else pats_pe

115

123

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

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

117 --

125 --

src/Idris/REPL.hs+11−2

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

1441 let importdirs = opt getImportDir opts

1442 let bcs = opt getBC opts

1443 let pkgdirs = opt getPkgDir opts

1444+ -- Set default optimisations

1444− let optimize = case opt getOptLevel opts of

1445+ let optimise = case opt getOptLevel opts of

1445 [] -> 2

1446 [] -> 2

1446 xs -> last xs

1447 xs -> last xs

1448+ setOptLevel optimise

1447 let outty = case opt getOutputTy opts of

1449 let outty = case opt getOutputTy opts of

1448 [] -> Executable

1450 [] -> Executable

1449 xs -> last xs

1451 xs -> last xs

1450 let cgn = case opt getCodegen opts of

1452 let cgn = case opt getCodegen opts of

1451 [] -> Via "c"

1453 [] -> Via "c"

1452 xs -> last xs

1454 xs -> last xs

1455+ -- Now set/unset specifically chosen optimisations

1456+ sequence_ (opt getOptimisation opts)

1453 script <- case opt getExecScript opts of

1457 script <- case opt getExecScript opts of

1454 [] -> return Nothing

1458 [] -> return Nothing

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

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

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

1701getCPU (TargetCPU x) = Just x

1705getCPU (TargetCPU x) = Just x

1702getCPU _ = Nothing

1706getCPU _ = Nothing

1703

1707

1704−getOptLevel :: Opt -> Maybe Word

1708+getOptLevel :: Opt -> Maybe Int

1705getOptLevel (OptLevel x) = Just x

1709getOptLevel (OptLevel x) = Just x

1706getOptLevel _ = Nothing

1710getOptLevel _ = Nothing

1707

1711

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

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

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

1715+getOptimisation _ = Nothing

1716+

1708getColour :: Opt -> Maybe Bool

1717getColour :: Opt -> Maybe Bool

1709getColour (ColourREPL b) = Just b

1718getColour (ColourREPL b) = Just b

1710getColour _ = Nothing

1719getColour _ = Nothing