e09ef82 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Improve PE for class constraints and HOFs

Reinstate and improve check for progress in PE (which is necessary in mutually defined functions in particular) and change RHS of more complex PE definitions to call the specialised function, rather than rewriting the RHS directly, so that progress can be detected more easily (and so that more reduction can happen where possible)

commite09ef821dced0153e322f2e16a97bd571079eee3 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 18 Oct 2014, 00:31 (12 years ago) parent02de034

4 files changed+60−34

compare with master

unifiedsplit

CHANGELOG+11−4 src/Idris/Core/Evaluate.hs+11−4 src/Idris/Elab/Clause.hs+3−2 src/Idris/PartialEval.hs+35−24

CHANGELOG+11−4

@@ -19,10 +19,17 @@ New in 0.9.15:

1919* The Java and LLVM backends have been factored out for separate maintenance. Now, the

2020 compiler distribution only ships with the C and JavaScript backends.

2121* New REPL command :printdef displays the internal definition of a name

22−* New REPL command :pprint pretty-prints a definition or term with LaTeX or HTML highlighting

23−* Naming of data and type constructors is made consistent across the standard library (see #1516)

24−* Terms in `code blocks` inside of documentation strings are now parsed and type checked. If this succeeds, they are rendered in full color in documentation lookups, and with semantic highlighting for IDEs.

25−* Fenced code blocks in docs defined with the "example" attribute are rendered as code examples.

22+* New REPL command :pprint pretty-prints a definition or term with LaTeX or

23+ HTML highlighting

24+* Naming of data and type constructors is made consistent across the standard

25+ library (see #1516)

26+* Terms in `code blocks` inside of documentation strings are now parsed and

27+ type checked. If this succeeds, they are rendered in full color in

28+ documentation lookups, and with semantic highlighting for IDEs.

29+* Fenced code blocks in docs defined with the "example" attribute are rendered

30+ as code examples.

31+* EXPERIMENTAL support for partial evaluation (Scrapping your Inefficient

32+ Engine style)

2633

2734New in 0.9.14:

2835--------------

src/Idris/Core/Evaluate.hs+11−4

@@ -173,13 +173,17 @@ usable False n ns

173173 _ -> return $ (True, (n, 100) : filter (\ (n', _) -> n/=n') ns)

174174

175175

176−deduct :: Name -> Eval ()

177−deduct n = do ES ls num <- get

176+fnCount :: Int -> Name -> Eval ()

177+fnCount inc n

178+ = do ES ls num <- get

178179 case lookup n ls of

179− Just i -> do put $ ES ((n, (i-1)) :

180+ Just i -> do put $ ES ((n, (i - inc)) :

180181 filter (\ (n', _) -> n/=n') ls) num

181182 _ -> return ()

182183

184+deduct = fnCount 1

185+reinstate = fnCount (-1)

186+

183187-- | Evaluate in a context of locally named things (i.e. not de Bruijn indexed,

184188-- such as we might have during construction of a proof)

185189

@@ -386,8 +390,11 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

386390 | length ns <= length args

387391 = do let args' = take (length ns) args

388392 let rest = drop (length ns) args

389− when spec $ deduct n -- successful, so deduct usages

393+ when spec $ deduct n

390394 t <- evTree ntimes stk top env (zip ns args') tree

395+ when spec $ case t of

396+ Nothing -> reinstate n -- Blocked, count n again

397+ Just _ -> return ()

391398-- (zipWith (\n , t) -> (n, t)) ns args') tree

392399 return (t, rest)

393400 | otherwise = return (Nothing, args)

src/Idris/Elab/Clause.hs+3−2

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

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

292292elabPE info fc caller r =

293293 do ist <- getIState

294− let sa = getSpecApps ist [] r

294+ let sa = filter (\ap -> fst ap /= caller) $ getSpecApps ist [] r

295295 rules <- mapM mkSpecialised sa

296296 return $ concat rules

297297 where

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

322322 (n, Just 65536) :

323323 mapMaybe specName (snd specapp))]

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

325− ++ " with " ++ show opts

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

326+ " with " ++ show opts

326327 logLvl 3 $ "New name: " ++ show newnm

327328 logLvl 3 $ "PE definition type : " ++ (show specTy)

328329 ++ "\n" ++ show opts

src/Idris/PartialEval.hs+35−24

@@ -33,7 +33,10 @@ data PEDecl = PEDecl { pe_app :: PTerm, -- new application

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

3434-- It is an error if partial evaluation fails to make any progress.

3535-- Making progress is defined as: all of the names given with explicit

36−-- reduction limits must have reduced at least once.

36+-- reduction limits (in practice, the function being specialised)

37+-- must have reduced at least once.

38+-- If we don't do this, we might end up making an infinite function after

39+-- applying the transformation.

3740partial_eval :: Context ->

3841 [(Name, Maybe Int)] ->

3942 [Either Term (Term, Term)] ->

@@ -44,7 +47,7 @@ partial_eval ctxt ns tms = mapM peClause tms where

4447 -- If the term is a clause, specialise the right hand side

4548 peClause (Right (lhs, rhs))

4649 = let (rhs', reductions) = specialise ctxt [] (map toLimit ns) rhs in

47− do -- checkProgress ns reductions

50+ do checkProgress ns reductions

4851 return (Right (lhs, rhs'))

4952

5053 toLimit (n, Nothing) = (n, 65536) -- somewhat arbitrary reduction limit

@@ -53,7 +56,7 @@ partial_eval ctxt ns tms = mapM peClause tms where

5356 checkProgress ns [] = return ()

5457 checkProgress ns ((n, r) : rs)

5558 | Just (Just start) <- lookup n ns

56− = if r < start then checkProgress ns rs else Nothing

59+ = if start <= 1 || r < start then checkProgress ns rs else Nothing

5760 | otherwise = checkProgress ns rs

5861

5962-- | Specialises the type of a partially evaluated TT function returning

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

153156 = PEDecl lhs rhs [(lhs, rhs)]

154157 where dynVar ap = case unApply ap of

155158 (_, args) -> dynArgs ns args

156− dynArgs [] [] = True

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

157160 -- if Static, doesn't matter what the argument is

158161 dynArgs ((ImplicitS, _) : ns) (a : as) = dynArgs ns as

159162 dynArgs ((ExplicitS, _) : ns) (a : as) = dynArgs ns as

@@ -168,9 +171,10 @@ mkNewPats ist d ns newname sname lhs rhs =

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

169172 mkClause (oldlhs, oldrhs)

170173 = let (_, as) = unApply oldlhs

171− lhs = PApp emptyFC (PRef emptyFC newname)

172− (mkLHSargs [] ns as)

173− rhs = mkRHS as oldrhs in

174+ lhsargs = mkLHSargs [] ns as

175+ lhs = PApp emptyFC (PRef emptyFC newname) lhsargs

176+ rhs = PApp emptyFC (PRef emptyFC sname)

177+ (mkRHSargs ns lhsargs) in

174178 (lhs, rhs)

175179

176180 mkLHSargs _ [] [] = []

@@ -179,19 +183,23 @@ mkNewPats ist d ns newname sname lhs rhs =

179183 = pexp (delab ist (substNames sub a)) : mkLHSargs sub ns as

180184 mkLHSargs sub ((ImplicitD, _) : ns) (a : as)

181185 = mkLHSargs sub ns as

186+ mkLHSargs sub ((UnifiedD, _) : ns) (a : as)

187+ = mkLHSargs sub ns as

182188 -- statics get dropped in any case

183189 mkLHSargs sub ((ImplicitS, t) : ns) (a : as)

184190 = mkLHSargs (extend a t sub) ns as

185191 mkLHSargs sub ((ExplicitS, t) : ns) (a : as)

186192 = mkLHSargs (extend a t sub) ns as

193+ mkLHSargs sub _ [] = [] -- no more LHS

187194

188195 extend (P _ n _) t sub = (n, t) : sub

189196 extend _ _ sub = sub

190197

191− mkRHS :: [Term] -> Term -> PTerm

192− mkRHS as oldrhs = let amap = mapMaybe mkSubst (zip as (map snd ns)) in

193− delab ist (substNames amap oldrhs)

194−

198+ mkRHSargs ((ExplicitS, t) : ns) as = pexp (delab ist t) : mkRHSargs ns as

199+ mkRHSargs ((ExplicitD, t) : ns) (a : as) = a : mkRHSargs ns as

200+ mkRHSargs (_ : ns) as = mkRHSargs ns as

201+ mkRHSargs _ _ = []

202+

195203 mkSubst :: (Term, Term) -> Maybe (Name, Term)

196204 mkSubst (P _ n _, t) = Just (n, t)

197205 mkSubst _ = Nothing

@@ -248,19 +256,22 @@ getSpecApps ist env tm = ga env (explicitNames tm) where

248256 = let s' = staticArg env s i a n

249257 ss' = buildApp env ss is as ns in

250258 (s' : ss')

251−

252− ga env tm@(App f a) | (P _ n _, args) <- unApply tm =

253− ga env f ++ ga env a ++

254− case (lookupCtxt n (idris_statics ist),

255− lookupCtxt n (idris_implicits ist)) of

256− ([statics], [imps]) ->

257− if (length statics == length args && or statics) then

258−-- trace (show (n, statics, imps, args)) $

259− case buildApp env statics imps args [0..] of

260− args -> [(n, args)]

261−-- _ -> []

262− else []

263− _ -> []

259+

260+ -- if we have a *defined* function that has static arguments,

261+ -- it will become a specialised application

262+ ga env tm@(App f a) | (P _ n _, args) <- unApply tm,

263+ n `notElem` map fst (idris_metavars ist) =

264+ ga env f ++ ga env a ++

265+ case (lookupCtxt n (idris_statics ist),

266+ lookupCtxt n (idris_implicits ist)) of

267+ ([statics], [imps]) ->

268+ if (length statics == length args && or statics) then

269+-- trace (show (n, statics, imps, args)) $

270+ case buildApp env statics imps args [0..] of

271+ args -> [(n, args)]

272+-- _ -> []

273+ else []

274+ _ -> []

264275 ga env (Bind n (Let t v) sc) = ga env v ++ ga (n : env) sc

265276 ga env (Bind n t sc) = ga (n : env) sc

266277 ga env t = []