cdff1db · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #1659 from edwinb/partial-eval

cdff1dbEdwin Brady12 years ago

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"

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+50−18

@@ -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))

@@ -1059,12 +1075,14 @@ addStatics :: Name -> Term -> PTerm -> Idris ()

1059addStatics n tm ptm =

1075addStatics n tm ptm =

1060 do let (statics, dynamics) = initStatics tm ptm

1076 do let (statics, dynamics) = initStatics tm ptm

1061 ist <- getIState

1077 ist <- getIState

1078+ let paramnames

1062− let paramnames = case lookupCtxtExact n (idris_fninfo ist) of

1079+ = nub $ case lookupCtxtExact n (idris_fninfo ist) of

1063− Just p -> getNamesFrom 0 (fn_params p) tm

1080+ Just p -> getNamesFrom 0 (fn_params p) tm ++

1064− _ -> []

1081+ concatMap (getParamNames ist) (map snd statics)

1082+ _ -> concatMap (getParamNames ist) (map snd statics)

1065

1083

1066 let stnames = nub $ concatMap freeArgNames (map snd statics)

1084 let stnames = nub $ concatMap freeArgNames (map snd statics)

1067− let dnames = nub $ concatMap freeArgNames (map snd dynamics)

1085+ let dnames = (nub $ concatMap freeArgNames (map snd dynamics))

1068 \\ paramnames

1086 \\ paramnames

1069 -- also get the arguments which are 'uniquely inferrable' from

1087 -- also get the arguments which are 'uniquely inferrable' from

1070 -- statics (see sec 4.2 of "Scrapping Your Inefficient Engine")

1088 -- statics (see sec 4.2 of "Scrapping Your Inefficient Engine")

@@ -1074,8 +1092,10 @@ addStatics n tm ptm =

1074 let stpos = staticList statics' tm

1092 let stpos = staticList statics' tm

1075 i <- getIState

1093 i <- getIState

1076 when (not (null statics)) $

1094 when (not (null statics)) $

1077− logLvl 3 $ "Statics for " ++ show n ++ " " ++ show tm ++ " "

1095+ logLvl 3 $ "Statics for " ++ show n ++ " " ++ show tm ++ "\n"

1096+ ++ showTmImpls ptm ++ "\n"

1078− ++ show statics' ++ "\n" ++ show dynamics

1097+ ++ show statics ++ "\n" ++ show dynamics

1098+ ++ "\n" ++ show paramnames

1079 ++ "\n" ++ show stpos

1099 ++ "\n" ++ show stpos

1080 putIState $ i { idris_statics = addDef n stpos (idris_statics i) }

1100 putIState $ i { idris_statics = addDef n stpos (idris_statics i) }

1081 addIBC (IBCStatic n)

1101 addIBC (IBCStatic n)

@@ -1091,6 +1111,18 @@ addStatics n tm ptm =

1091 else (static, dynamic)

1111 else (static, dynamic)

1092 initStatics t pt = ([], [])

1112 initStatics t pt = ([], [])

1093

1113

1114+ getParamNames ist tm | (P _ n _ , args) <- unApply tm

1115+ = case lookupCtxtExact n (idris_datatypes ist) of

1116+ Just ti -> getNamePos 0 (param_pos ti) args

1117+ Nothing -> []

1118+ where getNamePos i ps [] = []

1119+ getNamePos i ps (P _ n _ : as)

1120+ | i `elem` ps = n : getNamePos (i + 1) ps as

1121+ getNamePos i ps (_ : as) = getNamePos (i + 1) ps as

1122+ getParamNames ist (Bind t (Pi (P _ n _) _) sc)

1123+ = n : getParamNames ist sc

1124+ getParamNames ist _ = []

1125+

1094 getNamesFrom i ps (Bind n (Pi _ _) sc)

1126 getNamesFrom i ps (Bind n (Pi _ _) sc)

1095 | i `elem` ps = n : getNamesFrom (i + 1) ps sc

1127 | i `elem` ps = n : getNamesFrom (i + 1) ps sc

1096 | otherwise = getNamesFrom (i + 1) ps sc

1128 | otherwise = getNamesFrom (i + 1) ps sc

src/Idris/AbsSyntaxTree.hs+12−5

@@ -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)

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

@@ -485,7 +492,7 @@ deriving instance NFData Plicity

485impl = Imp [] Dynamic False

492impl = Imp [] Dynamic False

486expl = Exp [] Dynamic False

493expl = Exp [] Dynamic False

487expl_param = Exp [] Dynamic True

494expl_param = Exp [] Dynamic True

488−constraint = Constraint [] Dynamic

495+constraint = Constraint [] Static

489tacimpl t = TacImp [] Dynamic t

496tacimpl t = TacImp [] Dynamic t

490

497

491data FnOpt = Inlinable -- always evaluate when simplifying

498data FnOpt = Inlinable -- always evaluate when simplifying

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/Class.hs+1−1

@@ -220,7 +220,7 @@ elabClass info syn_in doc fc constraints tn ps pDocs ds

220

221 insertConstraint c (PPi p@(Imp _ _ _) n ty sc)

222 = PPi p n ty (insertConstraint c sc)

223− insertConstraint c sc = PPi (constraint) -- { pstatic = Static })

223+ insertConstraint c sc = PPi (constraint { pstatic = Static })

224 (sMN 0 "class") c sc

225

226 -- make arguments explicit and don't bind class parameters

src/Idris/Elab/Clause.hs+42−25

@@ -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)

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

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

@@ -74,9 +76,11 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

74 let atys = map snd (getArgTys fty)

76 let atys = map snd (getArgTys fty)

75 cs_elab <- mapM (elabClause info opts)

77 cs_elab <- mapM (elabClause info opts)

76 (zip [0..] cs)

78 (zip [0..] cs)

79+ -- pats_raw is the version we'll work with at compile time:

80+ -- no simplification or PE

77 let (pats_in, cs_full) = unzip cs_elab

81 let (pats_in, cs_full) = unzip cs_elab

78−

82+ let pats_raw = map (simple_lhs (tt_ctxt ist)) pats_in

79− logLvl 3 $ "Elaborated patterns:\n" ++ show pats_in

83+ logLvl 3 $ "Elaborated patterns:\n" ++ show pats_raw

81 solveDeferred n

85 solveDeferred n

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

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

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

95 -- RHS

99 -- RHS

96 pe_tm <- doPartialEval ist tpats

100 pe_tm <- doPartialEval ist tpats

101+ let pats_pe = if petrans

97− let pats = map (simple_lhs (tt_ctxt ist)) pe_tm

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

103+ else pats_raw

104

99 let tcase = opt_typecase (idris_options ist)

105 let tcase = opt_typecase (idris_options ist)

100

106

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

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

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

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

103 -- for partially evaluated definitions

109 -- for partially evaluated definitions

110+ newrules <- if petrans

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

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

105− Left _ -> return []

112+ Left _ -> return []

106− Right (l, r) -> elabPE info fc n r) pats

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

114+ else return []

107

115

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

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

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

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

110 -- used in place of the general one

118 -- used in place of the general one

111 ist <- getIState

119 ist <- getIState

112− let pats_transformed = transformPats ist pats

120+ let pats_transformed = if petrans

121+ then transformPats ist pats_pe

122+ else pats_pe

113

123

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

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

115 --

125 --

@@ -118,11 +128,13 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

118 -- addCaseDef builds case trees from <pdef> and <pdef'>

128 -- addCaseDef builds case trees from <pdef> and <pdef'>

119

129

120 -- pdef is the compile-time pattern definition.

130 -- pdef is the compile-time pattern definition.

121− -- This will get further optimised for run-time, and, separately,

122− -- further inlined to help with totality checking.

131+ -- This will get further inlined to help with totality checking.

123− let pdef = map debind pats_transformed

132+ let pdef = map debind pats_raw

133+ -- pdef_pe is the one which will get further optimised

134+ -- for run-time, and, partially evaluated

135+ let pdef_pe = map debind pats_transformed

124

136

125− logLvl 5 $ "Initial typechecked patterns:\n" ++ show pats

137+ logLvl 5 $ "Initial typechecked patterns:\n" ++ show pats_raw

126 logLvl 5 $ "Initial typechecked pattern def:\n" ++ show pdef

138 logLvl 5 $ "Initial typechecked pattern def:\n" ++ show pdef

127

139

128 -- NOTE: Need to store original definition so that proofs which

140 -- NOTE: Need to store original definition so that proofs which

@@ -137,13 +149,13 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

137

149

138 case specNames opts of

150 case specNames opts of

139 Just _ ->

151 Just _ ->

140− do logLvl 2 $ "Partially evaluated:\n" ++ show pats

152+ do logLvl 2 $ "Partially evaluated:\n" ++ show pats_pe

141 logLvl 2 $ "Transformed:\n" ++ show pats_transformed

153 logLvl 2 $ "Transformed:\n" ++ show pats_transformed

142 _ -> return ()

154 _ -> return ()

143

155

144 erInfo <- getErasureInfo <$> getIState

156 erInfo <- getErasureInfo <$> getIState

145 tree@(CaseDef scargs sc _) <- tclift $

157 tree@(CaseDef scargs sc _) <- tclift $

146− simpleCase tcase False reflect CompileTime fc inacc atys pdef erInfo

158+ simpleCase tcase False reflect CompileTime fc inacc atys pdef erInfo

147 cov <- coverage

159 cov <- coverage

148 pmissing <-

160 pmissing <-

149 if cov && not (hasDefault cs)

161 if cov && not (hasDefault cs)

@@ -164,8 +176,9 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

164 else return []

176 else return []

165 let pcover = null pmissing

177 let pcover = null pmissing

166

178

167− -- pdef' is the version that gets compiled for run-time

179+ -- pdef' is the version that gets compiled for run-time,

180+ -- so we start from the partially evaluated version

168− pdef_in' <- applyOpts pdef

181+ pdef_in' <- applyOpts pdef_pe

169 let pdef' = map (simple_rt (tt_ctxt ist)) pdef_in'

182 let pdef' = map (simple_rt (tt_ctxt ist)) pdef_in'

170

183

171 logLvl 5 $ "After data structure transformations:\n" ++ show pdef'

184 logLvl 5 $ "After data structure transformations:\n" ++ show pdef'

@@ -197,7 +210,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

197 ctxt <- getContext

210 ctxt <- getContext

198 ist <- getIState

211 ist <- getIState

199 let opt = idris_optimisation ist

212 let opt = idris_optimisation ist

200− putIState (ist { idris_patdefs = addDef n (force pdef, force pmissing)

213+ putIState (ist { idris_patdefs = addDef n (force pdef_pe, force pmissing)

201 (idris_patdefs ist) })

214 (idris_patdefs ist) })

202 let caseInfo = CaseInfo (inlinable opts) (dictionary opts)

215 let caseInfo = CaseInfo (inlinable opts) (dictionary opts)

203 case lookupTy n ctxt of

216 case lookupTy n ctxt of

@@ -207,8 +220,11 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

207 (AssertTotal `elem` opts)

220 (AssertTotal `elem` opts)

208 atys

221 atys

209 inacc

222 inacc

210− pats

223+ pats_pe

224+ pdef

225+ pdef -- compile time

211− pdef pdef pdef_inl pdef' ty)

226+ pdef_inl -- inlined

227+ pdef' ty)

212 addIBC (IBCDef n)

228 addIBC (IBCDef n)

213 setTotality n tot

229 setTotality n tot

214 when (not reflect) $ do totcheck (fc, n)

230 when (not reflect) $ do totcheck (fc, n)

@@ -320,7 +336,8 @@ elabPE info fc caller r =

320 let cgns' = filter (/= n) cgns

336 let cgns' = filter (/= n) cgns

321 let opts = [Specialise (map (\x -> (x, Nothing)) cgns' ++

337 let opts = [Specialise (map (\x -> (x, Nothing)) cgns' ++

322 (n, Just 65536) :

338 (n, Just 65536) :

339+ mapMaybe (specName (pe_simple specdecl))

323− mapMaybe specName (snd specapp))]

340+ (snd specapp))]

324 logLvl 3 $ "Specialising application: " ++ show specapp

341 logLvl 3 $ "Specialising application: " ++ show specapp

325 ++ " in " ++ show caller ++

342 ++ " in " ++ show caller ++

326 " with " ++ show opts

343 " with " ++ show opts

@@ -347,14 +364,14 @@ elabPE info fc caller r =

347 -- if it doesn't work, just don't specialise. Could happen for lots

364 -- if it doesn't work, just don't specialise. Could happen for lots

348 -- of valid reasons (e.g. local variables in scope which can't be

365 -- of valid reasons (e.g. local variables in scope which can't be

349 -- lifted out).

366 -- lifted out).

350− (\e -> do logLvl 4 $ "Couldn't specialise: " ++ (pshow ist e)

367+ (\e -> do logLvl 3 $ "Couldn't specialise: " ++ (pshow ist e)

351 return [])

368 return [])

352

369

353− specName (ImplicitS, tm)

370+ specName simpl (ImplicitS, tm)

354− | (P Ref n _, _) <- unApply tm = Just (n, Just 1)

371+ | (P Ref n _, _) <- unApply tm = Just (n, Just (if simpl then 1 else 0))

355− specName (ExplicitS, tm)

372+ specName simpl (ExplicitS, tm)

356− | (P Ref n _, _) <- unApply tm = Just (n, Just 1)

373+ | (P Ref n _, _) <- unApply tm = Just (n, Just (if simpl then 1 else 0))

357− specName _ = Nothing

374+ specName simpl _ = Nothing

358

375

359 concreteArg ist (ImplicitS, tm) = concreteTm ist tm

376 concreteArg ist (ImplicitS, tm) = concreteTm ist tm

360 concreteArg ist (ExplicitS, tm) = concreteTm ist tm

377 concreteArg ist (ExplicitS, tm) = concreteTm ist tm

src/Idris/PartialEval.hs+8−5

@@ -2,7 +2,7 @@

3module Idris.PartialEval(partial_eval, getSpecApps, specType,

4 mkPE_TyDecl, mkPE_TermDecl, PEArgType(..),

5− pe_app, pe_def, pe_clauses) where

5+ pe_app, pe_def, pe_clauses, pe_simple) where

7import Idris.AbsSyntax

8import Idris.Delaborate

@@ -25,9 +25,12 @@ data PEArgType = ImplicitS -- ^ Implicit static argument

25-- | A partially evaluated function. pe_app captures the lhs of the

26-- new definition, pe_def captures the rhs, and pe_clauses is the

27-- specialised implementation.

28+-- pe_simple is set if the result is always reducible, because in such a

29+-- case we'll also need to reduce the static argument

28data PEDecl = PEDecl { pe_app :: PTerm, -- new application

30data PEDecl = PEDecl { pe_app :: PTerm, -- new application

29 pe_def :: PTerm, -- old application

31 pe_def :: PTerm, -- old application

30− pe_clauses :: [(PTerm, PTerm)] -- clauses of new application

32+ pe_clauses :: [(PTerm, PTerm)], -- clauses of new application

33+ pe_simple :: Bool -- if just one reducible clause

31 }

34 }

33-- | Partially evaluates given terms under the given context.

36-- | Partially evaluates given terms under the given context.

@@ -153,7 +156,7 @@ mkNewPats :: IState ->

153-- definition isn't going to block on any of the dynamic arguments

156-- definition isn't going to block on any of the dynamic arguments

154-- in this case

157-- in this case

155mkNewPats ist d ns newname sname lhs rhs | all dynVar (map fst d)

158mkNewPats ist d ns newname sname lhs rhs | all dynVar (map fst d)

156− = PEDecl lhs rhs [(lhs, rhs)]

159+ = PEDecl lhs rhs [(lhs, rhs)] True

157 where dynVar ap = case unApply ap of

160 where dynVar ap = case unApply ap of

158 (_, args) -> dynArgs ns args

161 (_, args) -> dynArgs ns args

159 dynArgs _ [] = True -- can definitely reduce from here

162 dynArgs _ [] = True -- can definitely reduce from here

@@ -166,7 +169,7 @@ mkNewPats ist d ns newname sname lhs rhs | all dynVar (map fst d)

166 dynArgs (_ : ns) (P _ _ _ : as) = dynArgs ns as

169 dynArgs (_ : ns) (P _ _ _ : as) = dynArgs ns as

167 dynArgs _ _ = False -- and now we'll get stuck

170 dynArgs _ _ = False -- and now we'll get stuck

168mkNewPats ist d ns newname sname lhs rhs =

171mkNewPats ist d ns newname sname lhs rhs =

169− PEDecl lhs rhs (map mkClause d)

172+ PEDecl lhs rhs (map mkClause d) False

170 where

173 where

171 mkClause :: (Term, Term) -> (PTerm, PTerm)

174 mkClause :: (Term, Term) -> (PTerm, PTerm)

172 mkClause (oldlhs, oldrhs)

175 mkClause (oldlhs, oldrhs)

@@ -215,7 +218,7 @@ mkPE_TermDecl ist newname sname ns

215 rhs = eraseImps $ delab ist (mkApp (P Ref sname Erased) (map snd ns))

218 rhs = eraseImps $ delab ist (mkApp (P Ref sname Erased) (map snd ns))

216 patdef = lookupCtxtExact sname (idris_patdefs ist)

219 patdef = lookupCtxtExact sname (idris_patdefs ist)

217 newpats = case patdef of

220 newpats = case patdef of

218− Nothing -> PEDecl lhs rhs [(lhs, rhs)]

221+ Nothing -> PEDecl lhs rhs [(lhs, rhs)] True

219 Just d -> mkNewPats ist (getPats d) ns

222 Just d -> mkNewPats ist (getPats d) ns

220 newname sname lhs rhs in

223 newname sname lhs rhs in

221 newpats where

224 newpats where

src/Idris/REPL.hs+11−2

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

1453 let importdirs = opt getImportDir opts

1454 let bcs = opt getBC opts

1455 let pkgdirs = opt getPkgDir opts

1456+ -- Set default optimisations

1456− let optimize = case opt getOptLevel opts of

1457+ let optimise = case opt getOptLevel opts of

1457 [] -> 2

1458 [] -> 2

1458 xs -> last xs

1459 xs -> last xs

1460+ setOptLevel optimise

1459 let outty = case opt getOutputTy opts of

1461 let outty = case opt getOutputTy opts of

1460 [] -> Executable

1462 [] -> Executable

1461 xs -> last xs

1463 xs -> last xs

1462 let cgn = case opt getCodegen opts of

1464 let cgn = case opt getCodegen opts of

1463 [] -> Via "c"

1465 [] -> Via "c"

1464 xs -> last xs

1466 xs -> last xs

1467+ -- Now set/unset specifically chosen optimisations

1468+ sequence_ (opt getOptimisation opts)

1465 script <- case opt getExecScript opts of

1469 script <- case opt getExecScript opts of

1466 [] -> return Nothing

1470 [] -> return Nothing

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

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

@@ -1713,10 +1717,15 @@ getCPU :: Opt -> Maybe String

1713getCPU (TargetCPU x) = Just x

1717getCPU (TargetCPU x) = Just x

1714getCPU _ = Nothing

1718getCPU _ = Nothing

1715

1719

1716−getOptLevel :: Opt -> Maybe Word

1720+getOptLevel :: Opt -> Maybe Int

1717getOptLevel (OptLevel x) = Just x

1721getOptLevel (OptLevel x) = Just x

1718getOptLevel _ = Nothing

1722getOptLevel _ = Nothing

1719

1723

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

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

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

1727+getOptimisation _ = Nothing

1728+

1720getColour :: Opt -> Maybe Bool

1729getColour :: Opt -> Maybe Bool

1721getColour (ColourREPL b) = Just b

1730getColour (ColourREPL b) = Just b

1722getColour _ = Nothing

1731getColour _ = Nothing

src/Idris/Transforms.hs+4−3

@@ -43,10 +43,11 @@ applyAll extra ts ap@(App f a)

43 | (P _ fn ty, args) <- unApply ap

44 = let rules = case lookupCtxtExact fn ts of

45 Just r -> extra ++ r

46− Nothing -> extra in

46+ Nothing -> extra

47+ ap' = App (applyAll extra ts f) (applyAll extra ts a) in

47 case rules of

48 case rules of

48− [] -> App (applyAll extra ts f) (applyAll extra ts a)

49+ [] -> ap'

49− rs -> case applyFnRules rs ap of

50+ rs -> case applyFnRules rs ap' of

50 Just tm' -> tm'

51 Just tm' -> tm'

51 _ -> App (applyAll extra ts f)

52 _ -> App (applyAll extra ts f)

52 (applyAll extra ts a)

53 (applyAll extra ts a)