0f3e4e3 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Apply forcing optimisation on LHS

0f3e4e3Edwin Brady10 years ago

src/Idris/ASTUtils.hs+4−1

compare with master

unifiedsplit

@@ -41,7 +41,7 @@ module Idris.ASTUtils(

41 Field(), cg_usedpos, ctxt_lookup, fgetState, fmodifyState

42 , fputState, idris_fixities, ist_callgraph, ist_optimisation

43 , known_interfaces, known_terms, opt_detaggable, opt_inaccessible

44− , opts_idrisCmdline, repl_definitions

44+ , opt_forceable, opts_idrisCmdline, repl_definitions

45 ) where

47import Idris.AbsSyntaxTree

@@ -111,6 +111,7 @@ ist_optimisation n =

111 maybe_default Optimise

112 { inaccessible = []

113 , detaggable = False

114+ , forceable = []

114 }

115 }

115 . ctxt_lookup n

116 . ctxt_lookup n

116 . Field idris_optimisation (\v ist -> ist{ idris_optimisation = v })

117 . Field idris_optimisation (\v ist -> ist{ idris_optimisation = v })

@@ -122,6 +123,8 @@ opt_inaccessible = Field inaccessible (\v opt -> opt{ inaccessible = v })

122opt_detaggable :: Field OptInfo Bool

123opt_detaggable :: Field OptInfo Bool

123opt_detaggable = Field detaggable (\v opt -> opt{ detaggable = v })

124opt_detaggable = Field detaggable (\v opt -> opt{ detaggable = v })

124

125

126+opt_forceable :: Field OptInfo [Int]

127+opt_forceable = Field forceable (\v opt -> opt{ forceable = v })

125

128

126-- | callgraph record for the given (exact) name

129-- | callgraph record for the given (exact) name

127ist_callgraph :: Name -> Field IState CGInfo

130ist_callgraph :: Name -> Field IState CGInfo

src/Idris/AbsSyntaxTree.hs+2−1

@@ -1440,6 +1440,7 @@ deriving instance Binary FnInfo

1440data OptInfo = Optimise {

1441 inaccessible :: [(Int,Name)] -- includes names for error reporting

1442 , detaggable :: Bool

1443+ , forceable :: [Int] -- argument positions which are forced by other values

1443 } deriving (Show, Generic)

1444 } deriving (Show, Generic)

1444{-!

1445{-!

1445deriving instance Binary OptInfo

1446deriving instance Binary OptInfo

@@ -2564,5 +2565,5 @@ usedNamesIn vars ist tm = nub $ ni 0 [] tm

2564getErasureInfo :: IState -> Name -> [Int]

2565getErasureInfo :: IState -> Name -> [Int]

2565getErasureInfo ist n =

2566getErasureInfo ist n =

2566 case lookupCtxtExact n (idris_optimisation ist) of

2567 case lookupCtxtExact n (idris_optimisation ist) of

2567− Just (Optimise inacc detagg) -> map fst inacc

2568+ Just (Optimise inacc detag force) -> map fst inacc

2568 Nothing -> []

2569 Nothing -> []

src/Idris/Core/CaseTree.hs+19−17

@@ -36,6 +36,7 @@ import Control.Monad.State

36import Data.List hiding (partition)

37import qualified Data.List (partition)

38import Data.Maybe

39+import qualified Data.Set as S

39import Debug.Trace

40import Debug.Trace

40import GHC.Generics (Generic)

41import GHC.Generics (Generic)

@@ -153,33 +154,34 @@ findCalls :: SC -> [Name] -> [(Name, [[Name]])]

153findCalls = findCalls' False

154findCalls = findCalls' False

154

155

155findCalls' :: Bool -> SC -> [Name] -> [(Name, [[Name]])]

156findCalls' :: Bool -> SC -> [Name] -> [(Name, [[Name]])]

156−findCalls' ignoreasserts sc topargs = nub $ nu' topargs sc where

157+findCalls' ignoreasserts sc topargs = S.toList $ nu' topargs sc where

157− nu' ps (Case _ n alts) = nub (concatMap (nua (n : ps)) alts)

158+ nu' ps (Case _ n alts) = S.unions $ map (nua (n : ps)) alts

158− nu' ps (ProjCase t alts) = nub $ nut ps t ++ concatMap (nua ps) alts

159+ nu' ps (ProjCase t alts) = S.unions $ nut ps t : map (nua ps) alts

159− nu' ps (STerm t) = nub $ nut ps t

160+ nu' ps (STerm t) = nut ps t

160− nu' ps _ = []

161+ nu' ps _ = S.empty

161−

162+

162− nua ps (ConCase n i args sc) = nub (nu' (ps ++ args) sc)

163+ nua ps (ConCase n i args sc) = nu' (ps ++ args) sc

163− nua ps (FnCase n args sc) = nub (nu' (ps ++ args) sc)

164+ nua ps (FnCase n args sc) = nu' (ps ++ args) sc

164 nua ps (ConstCase _ sc) = nu' ps sc

165 nua ps (ConstCase _ sc) = nu' ps sc

165 nua ps (SucCase _ sc) = nu' ps sc

166 nua ps (SucCase _ sc) = nu' ps sc

166 nua ps (DefaultCase sc) = nu' ps sc

167 nua ps (DefaultCase sc) = nu' ps sc

167

168

168− nut ps (P _ n _) | n `elem` ps = []

169+ nut ps (P _ n _) | n `elem` ps = S.empty

169− | otherwise = [(n, [])] -- tmp

170+ | otherwise = S.singleton (n, [])

170 nut ps fn@(App _ f a)

171 nut ps fn@(App _ f a)

171 | (P _ n _, args) <- unApply fn

172 | (P _ n _, args) <- unApply fn

172 = if ignoreasserts && n == sUN "assert_total"

173 = if ignoreasserts && n == sUN "assert_total"

173− then []

174+ then S.empty

174 else if n `elem` ps

175 else if n `elem` ps

175− then nut ps f ++ nut ps a

176+ then S.union (nut ps f) (nut ps a)

176− else [(n, map argNames args)] ++ concatMap (nut ps) args

177+ else S.insert (n, map argNames args)

178+ (S.unions $ map (nut ps) args)

177− | (P (TCon _ _) n _, _) <- unApply fn = []

179+ | (P (TCon _ _) n _, _) <- unApply fn = S.empty

178− | otherwise = nut ps f ++ nut ps a

180+ | otherwise = S.union (nut ps f) (nut ps a)

179− nut ps (Bind n (Let t v) sc) = nut ps v ++ nut (n:ps) sc

181+ nut ps (Bind n (Let t v) sc) = S.union (nut ps v) (nut (n:ps) sc)

180 nut ps (Proj t _) = nut ps t

182 nut ps (Proj t _) = nut ps t

181 nut ps (Bind n b sc) = nut (n:ps) sc

183 nut ps (Bind n b sc) = nut (n:ps) sc

182− nut ps _ = []

184+ nut ps _ = S.empty

183

185

184 argNames tm = let ns = directUse tm in

186 argNames tm = let ns = directUse tm in

185 filter (\x -> x `elem` ns) topargs

187 filter (\x -> x `elem` ns) topargs

src/Idris/Elab/Clause.hs+57−14

@@ -86,11 +86,16 @@ elabClauses info' fc opts n_in cs =

86 cs_elab <- mapM (elabClause info opts)

87 (zip [0..] cs)

88 ctxt <- getContext

89− -- pats_raw is the version we'll work with at compile time:

89+ -- pats_raw is the basic type checked version, no PE or forcing

90− -- no simplification or PE

90+ let optinfo = idris_optimisation ist

91 let (pats_in, cs_full) = unzip cs_elab

92 let pats_raw = map (simple_lhs ctxt) pats_in

93+ -- We'll apply forcing to the left hand side here, so that we don't

94+ -- do any unnecessary case splits

95+ let pats_forced = map (force_lhs optinfo) pats_raw

96+

93 logElab 3 $ "Elaborated patterns:\n" ++ show pats_raw

97 logElab 3 $ "Elaborated patterns:\n" ++ show pats_raw

98+ logElab 5 $ "Forced patterns:\n" ++ show pats_forced

95 solveDeferred fc n

100 solveDeferred fc n

101

@@ -109,9 +114,10 @@ elabClauses info' fc opts n_in cs =

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

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

110 -- RHS

115 -- RHS

111 pe_tm <- doPartialEval ist tpats

116 pe_tm <- doPartialEval ist tpats

117+

112 let pats_pe = if petrans

118 let pats_pe = if petrans

113− then map (simple_lhs ctxt) pe_tm

119+ then map (force_lhs optinfo . simple_lhs ctxt) pe_tm

114− else pats_raw

120+ else pats_forced

115

121

116 let tcase = opt_typecase (idris_options ist)

122 let tcase = opt_typecase (idris_options ist)

117

123

@@ -138,11 +144,19 @@ elabClauses info' fc opts n_in cs =

138

144

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

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

140

146

141− -- pdef is the compile-time pattern definition.

147+ -- pdef is the compile-time pattern definition, after forcing

142− -- This will get further inlined to help with totality checking.

148+ -- optimisation applied to LHS

149+ let pdef = map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) $

150+ map debind pats_forced

151+ -- pdef_cov is the pattern definition without forcing, which

152+ -- we feed to the coverage checker (we need to know what the

153+ -- programmer wrote before forcing erasure)

154+ let pdef_cov

143− let pdef = map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) $ map debind pats_raw

155+ = map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) $

156+ map debind pats_raw

144 -- pdef_pe is the one which will get further optimised

157 -- pdef_pe is the one which will get further optimised

158+ -- for run-time, with no forcing optimisation of the LHS because

145− -- for run-time, and, partially evaluated

159+ -- the affects erasure. Also, it's partially evaluated

146 let pdef_pe = map debind pats_transformed

160 let pdef_pe = map debind pats_transformed

147

161

148 logElab 5 $ "Initial typechecked patterns:\n" ++ show pats_raw

162 logElab 5 $ "Initial typechecked patterns:\n" ++ show pats_raw

@@ -171,12 +185,12 @@ elabClauses info' fc opts n_in cs =

171 pmissing <-

185 pmissing <-

172 if cov && not (hasDefault pats_raw)

186 if cov && not (hasDefault pats_raw)

173 then do -- Generate clauses from the given possible cases

187 then do -- Generate clauses from the given possible cases

174− missing <- genClauses fc n (map getLHS pdef) cs_full

188+ missing <- genClauses fc n (map getLHS pdef_cov) cs_full

175 -- missing <- genMissing n scargs sc

189 -- missing <- genMissing n scargs sc

176 missing' <- filterM (checkPossible info fc True n) missing

190 missing' <- filterM (checkPossible info fc True n) missing

177 -- Filter out the ones which match one of the

191 -- Filter out the ones which match one of the

178 -- given cases (including impossible ones)

192 -- given cases (including impossible ones)

179− let clhs = map getLHS pdef

193+ let clhs = map getLHS pdef_cov

180 logElab 2 $ "Must be unreachable:\n" ++

194 logElab 2 $ "Must be unreachable:\n" ++

181 showSep "\n" (map showTmImpls missing') ++

195 showSep "\n" (map showTmImpls missing') ++

182 "\nAgainst: " ++

196 "\nAgainst: " ++

@@ -228,6 +242,7 @@ elabClauses info' fc opts n_in cs =

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

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

229 (idris_patdefs ist) })

243 (idris_patdefs ist) })

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

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

245+

231 case lookupTyExact n ctxt of

246 case lookupTyExact n ctxt of

232 Just ty ->

247 Just ty ->

233 do ctxt' <- do ctxt <- getContext

248 do ctxt' <- do ctxt <- getContext

@@ -238,7 +253,7 @@ elabClauses info' fc opts n_in cs =

238 (AssertTotal `elem` opts)

253 (AssertTotal `elem` opts)

239 atys

254 atys

240 inacc

255 inacc

241− pats_pe

256+ pats_forced

242 pdef

257 pdef

243 pdef' ty

258 pdef' ty

244 ctxt

259 ctxt

@@ -329,9 +344,13 @@ elabClauses info' fc opts n_in cs =

329

344

330 -- Simplify the left hand side of a definition, to remove any lets

345 -- Simplify the left hand side of a definition, to remove any lets

331 -- that may have arisen during elaboration

346 -- that may have arisen during elaboration

347+ simple_lhs ctxt (Right (x, y))

332− simple_lhs ctxt (Right (x, y)) = Right (Idris.Core.Evaluate.simplify ctxt [] x, y)

348+ = Right (Idris.Core.Evaluate.simplify ctxt [] x, y)

333 simple_lhs ctxt t = t

349 simple_lhs ctxt t = t

334

350

351+ force_lhs opts (Right (x, y)) = Right (forceWith opts x, y)

352+ force_lhs opts t = t

353+

335 simple_rt ctxt (p, x, y) = (p, x, force (uniqueBinders p

354 simple_rt ctxt (p, x, y) = (p, x, force (uniqueBinders p

336 (rt_simplify ctxt [] y)))

355 (rt_simplify ctxt [] y)))

337

356

@@ -354,6 +373,28 @@ elabClauses info' fc opts n_in cs =

354 Just t -> return t

373 Just t -> return t

355 Nothing -> ierror (At fc (Msg "No specialisation achieved"))

374 Nothing -> ierror (At fc (Msg "No specialisation achieved"))

356

375

376+forceWith :: Ctxt OptInfo -> Term -> Term

377+forceWith opts lhs = -- trace (show lhs ++ "\n==>\n" ++ show (force lhs) ++ "\n----") $

378+ force lhs

379+ where

380+ -- If there's forced arguments, erase them

381+ force ap@(App _ _ _)

382+ | (fn@(P _ c _), args) <- unApply ap,

383+ Just copt <- lookupCtxtExact c opts

384+ = let args' = eraseArg 0 (forceable copt) args in

385+ mkApp fn (map force args')

386+ force (App t f a)

387+ = App t (force f) (force a)

388+ -- We might have pat bindings, so go under them

389+ force (Bind n b sc) = Bind n b (force sc)

390+ -- Everything else, leave it alone

391+ force t = t

392+

393+ eraseArg i fs (n : ns) | i `elem` fs = Erased : eraseArg (i + 1) fs ns

394+ | otherwise = n : eraseArg (i + 1) fs ns

395+ eraseArg i _ [] = []

396+

397+

357-- | Find 'static' applications in a term and partially evaluate them.

398-- | Find 'static' applications in a term and partially evaluate them.

358-- Return any new transformation rules

399-- Return any new transformation rules

359elabPE :: ElabInfo -> FC -> Name -> Term -> Idris [(Term, Term)]

400elabPE :: ElabInfo -> FC -> Name -> Term -> Idris [(Term, Term)]

@@ -667,7 +708,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

667 then recheckC_borrowing False (PEGenerated `notElem` opts)

708 then recheckC_borrowing False (PEGenerated `notElem` opts)

668 [] (constraintNS info) fc id [] lhs_tm

709 [] (constraintNS info) fc id [] lhs_tm

669 else return (lhs_tm, lhs_ty)

710 else return (lhs_tm, lhs_ty)

670− let clhs = Idris.Core.Evaluate.simplify ctxt [] clhs_c

711+ let clhs = normalise ctxt [] clhs_c

671 let borrowed = borrowedNames [] clhs

712 let borrowed = borrowedNames [] clhs

672

713

673 -- These are the names we're not allowed to use on the RHS, because

714 -- These are the names we're not allowed to use on the RHS, because

@@ -925,7 +966,9 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

925 let ret_ty = getRetTy (explicitNames (normalise ctxt [] lhs_ty))

966 let ret_ty = getRetTy (explicitNames (normalise ctxt [] lhs_ty))

926 let static_names = getStaticNames i lhs_tm

967 let static_names = getStaticNames i lhs_tm

927 logElab 5 (show lhs_tm ++ "\n" ++ show static_names)

968 logElab 5 (show lhs_tm ++ "\n" ++ show static_names)

928− (clhs, clhsty) <- recheckC (constraintNS info) fc id [] lhs_tm

969+ (clhs_c, clhsty) <- recheckC (constraintNS info) fc id [] lhs_tm

970+ let clhs = normalise ctxt [] clhs_c

971+

929 logElab 5 ("Checked " ++ show clhs)

972 logElab 5 ("Checked " ++ show clhs)

930 let bargs = getPBtys (explicitNames (normalise ctxt [] lhs_tm))

973 let bargs = getPBtys (explicitNames (normalise ctxt [] lhs_tm))

931 let wval = rhs_trans info $ addImplBound i (map fst bargs) wval_in

974 let wval = rhs_trans info $ addImplBound i (map fst bargs) wval_in

src/Idris/Elab/Data.hs+46

@@ -189,9 +189,13 @@ elabCon info syn tn codata expkind dkind (doc, argDocs, n, nfc, t_in, fc, forcen

189

190 -- Check that the constructor type is, in fact, a part of the family being defined

191 tyIs n cty'

192+ let force = if tn == sUN "Delayed"

193+ then [] -- TMP HACK! Totality checker needs this info

194+ else forceArgs ctxt cty'

192

195

193 logElab 5 $ show fc ++ ":Constructor " ++ show n ++ " elaborated : " ++ show t

196 logElab 5 $ show fc ++ ":Constructor " ++ show n ++ " elaborated : " ++ show t

194 logElab 5 $ "Inaccessible args: " ++ show inacc

197 logElab 5 $ "Inaccessible args: " ++ show inacc

198+ logElab 5 $ "Forceable args: " ++ show force

195 logElab 2 $ "---> " ++ show n ++ " : " ++ show cty

199 logElab 2 $ "---> " ++ show n ++ " : " ++ show cty

196

200

197 -- Add to the context (this is temporary, so that later constructors

201 -- Add to the context (this is temporary, so that later constructors

@@ -206,6 +210,7 @@ elabCon info syn tn codata expkind dkind (doc, argDocs, n, nfc, t_in, fc, forcen

206 addDocStr n doc' argDocs'

210 addDocStr n doc' argDocs'

207 addIBC (IBCDoc n)

211 addIBC (IBCDoc n)

208 fputState (opt_inaccessible . ist_optimisation n) inacc

212 fputState (opt_inaccessible . ist_optimisation n) inacc

213+ fputState (opt_forceable . ist_optimisation n) force

209 addIBC (IBCOpt n)

214 addIBC (IBCOpt n)

210 return (n, cty)

215 return (n, cty)

211 where

216 where

@@ -255,6 +260,47 @@ elabCon info syn tn codata expkind dkind (doc, argDocs, n, nfc, t_in, fc, forcen

255 = tclift $ tfail (At fc (UniqueKindError AllTypes n))

260 = tclift $ tfail (At fc (UniqueKindError AllTypes n))

256 checkUniqueKind _ _ = return ()

261 checkUniqueKind _ _ = return ()

257

262

263+forceArgs :: Context -> Type -> [Int]

264+forceArgs ctxt ty = forceFrom 0 ty

265+ where

266+ -- for each argument, substitute in MN pos "FF"

267+ -- then when we look at the return type, if we see MN pos name

268+ -- constructor guarded, then 'pos' is a forceable position

269+ forceFrom :: Int -> Type -> [Int]

270+ forceFrom i (Bind n (Pi _ _ _) sc)

271+ = forceFrom (i + 1) (substV (P Ref (sMN i "FF") Erased) sc)

272+ forceFrom i sc

273+ -- Go under the top level type application

274+ -- We risk affecting erasure of more complex indices, so we'll only

275+ -- mark something forced if *everything* which appears in an index

276+ -- is forceable

277+ -- (FIXME: Actually the real risk is if we erase something a programmer

278+ -- definitely wants, which is particularly the case with 'views'.

279+ -- So perhaps we need a way of marking that in the source?)

280+ | (P _ ty _, args) <- unApply sc

281+ = if null (concatMap (findNonForcePos True) args)

282+ then nub (concatMap findForcePos args)

283+ else []

284+ forceFrom i sc = []

285+

286+ findForcePos (P _ (MN i ff) _)

287+ | ff == txt "FF" = [i]

288+ -- Only look under constructors in applications

289+ findForcePos ap@(App _ f a)

290+ | (P _ con _, args) <- unApply ap,

291+ isDConName con ctxt

292+ = nub $ concatMap findForcePos args

293+ findForcePos _ = []

294+

295+ findNonForcePos fok (P _ (MN i ff) _)

296+ | ff == txt "FF" = if fok then [] else [i]

297+ -- Look under non-constructors in applications for things which can't

298+ -- be forced

299+ findNonForcePos fok ap@(App _ f a)

300+ | (P _ con _, args) <- unApply ap

301+ = nub $ concatMap (findNonForcePos (fok && isConName con ctxt)) args

302+ findNonForcePos _ _ = []

303+

258addParamConstraints :: FC -> [Int] -> Type -> [(Name, Type)] -> Idris ()

304addParamConstraints :: FC -> [Int] -> Type -> [(Name, Type)] -> Idris ()

259addParamConstraints fc ps cty cons

305addParamConstraints fc ps cty cons

260 = case getRetTy cty of

306 = case getRetTy cty of

src/Idris/Elab/Utils.hs+1−1

@@ -438,7 +438,7 @@ setDetaggable n = do

438 let opt = idris_optimisation ist

439 case lookupCtxt n opt of

440 [oi] -> putIState ist { idris_optimisation = addDef n oi { detaggable = True } opt }

441− _ -> putIState ist { idris_optimisation = addDef n (Optimise [] True) opt }

441+ _ -> putIState ist { idris_optimisation = addDef n (Optimise [] True []) opt }

442

443displayWarnings :: EState -> Idris ()

444displayWarnings est

src/Idris/Erasure.hs+1−1

@@ -134,7 +134,7 @@ performUsageAnalysis startNames = do

134

135 checkAccessibility :: Ctxt OptInfo -> (Name, IntMap (Set Reason)) -> Idris ()

136 checkAccessibility opt (n, reachable)

137− | Just (Optimise inaccessible dt) <- lookupCtxtExact n opt

137+ | Just (Optimise inaccessible dt force) <- lookupCtxtExact n opt

138 , eargs@(_:_) <- [fmt n (S.toList rs) | (i,n) <- inaccessible, rs <- maybeToList $ IM.lookup i reachable]

139 = warn $ show n ++ ": inaccessible arguments reachable:\n " ++ intercalate "\n " eargs

140

src/Idris/IBC.hs+5−3

@@ -47,7 +47,7 @@ import System.Directory

47import System.FilePath

49ibcVersion :: Word16

50−ibcVersion = 154

50+ibcVersion = 155

52-- | When IBC is being loaded - we'll load different things (and omit

53-- different structures/definitions) depending on which phase we're in.

@@ -2396,13 +2396,15 @@ instance Binary RecordInfo where

2396 return (RI x1 x2 x3)

2397

2398instance Binary OptInfo where

2399− put (Optimise x1 x2)

2399+ put (Optimise x1 x2 x3)

2400 = do put x1

2401 put x2

2402+ put x3

2402 get

2403 get

2403 = do x1 <- get

2404 = do x1 <- get

2404 x2 <- get

2405 x2 <- get

2406+ x3 <- get

2405− return (Optimise x1 x2)

2407+ return (Optimise x1 x2 x3)

2406

2408

2407instance Binary FnInfo where

2409instance Binary FnInfo where

2408 put (FnInfo x1)

2410 put (FnInfo x1)