e09ef82 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Improve PE for class constraints and HOFs

e09ef82Edwin Brady12 years ago

CHANGELOG+11−4

compare with master

unifiedsplit

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

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

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

21* 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

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

23+ HTML highlighting

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

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

25+ 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.

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.

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

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)

27New in 0.9.14:

34New in 0.9.14:

28--------------

35--------------

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

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

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

174

175

176−deduct :: Name -> Eval ()

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

177+fnCount inc n

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

178+ = do ES ls num <- get

178 case lookup n ls of

179 case lookup n ls of

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

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

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

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

181 _ -> return ()

182 _ -> return ()

182

183

184+deduct = fnCount 1

185+reinstate = fnCount (-1)

186+

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

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

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

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

185

189

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

386 | length ns <= length args

390 | length ns <= length args

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

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

388 let rest = drop (length ns) args

392 let rest = drop (length ns) args

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

393+ when spec $ deduct n

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

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

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

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

392 return (t, rest)

399 return (t, rest)

393 | otherwise = return (Nothing, args)

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

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

292elabPE info fc caller r =

293 do ist <- getIState

294− let sa = getSpecApps ist [] r

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

295 rules <- mapM mkSpecialised sa

296 return $ concat rules

297 where

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

322 (n, Just 65536) :

323 mapMaybe specName (snd specapp))]

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

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

325− ++ " with " ++ show opts

326+ " with " ++ show opts

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

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

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

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

328 ++ "\n" ++ show opts

329 ++ "\n" ++ show opts

src/Idris/PartialEval.hs+35−24

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

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

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

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

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

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

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.

37partial_eval :: Context ->

40partial_eval :: Context ->

38 [(Name, Maybe Int)] ->

41 [(Name, Maybe Int)] ->

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

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

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

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

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

45 peClause (Right (lhs, rhs))

48 peClause (Right (lhs, rhs))

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

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

47− do -- checkProgress ns reductions

50+ do checkProgress ns reductions

48 return (Right (lhs, rhs'))

51 return (Right (lhs, rhs'))

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

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

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

53 checkProgress ns [] = return ()

56 checkProgress ns [] = return ()

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

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

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

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

57 | otherwise = checkProgress ns rs

60 | otherwise = checkProgress ns rs

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

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

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

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

154 where dynVar ap = case unApply ap of

157 where dynVar ap = case unApply ap of

155 (_, args) -> dynArgs ns args

158 (_, args) -> dynArgs ns args

156− dynArgs [] [] = True

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

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

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

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

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

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

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

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

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

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

169 mkClause (oldlhs, oldrhs)

172 mkClause (oldlhs, oldrhs)

170 = let (_, as) = unApply oldlhs

173 = let (_, as) = unApply oldlhs

171− lhs = PApp emptyFC (PRef emptyFC newname)

172− (mkLHSargs [] ns as)

174+ lhsargs = mkLHSargs [] ns as

173− rhs = mkRHS as oldrhs in

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

176+ rhs = PApp emptyFC (PRef emptyFC sname)

177+ (mkRHSargs ns lhsargs) in

174 (lhs, rhs)

178 (lhs, rhs)

175

179

176 mkLHSargs _ [] [] = []

180 mkLHSargs _ [] [] = []

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

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

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

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

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

181 = mkLHSargs sub ns as

185 = mkLHSargs sub ns as

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

187+ = mkLHSargs sub ns as

182 -- statics get dropped in any case

188 -- statics get dropped in any case

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

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

184 = mkLHSargs (extend a t sub) ns as

190 = mkLHSargs (extend a t sub) ns as

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

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

186 = mkLHSargs (extend a t sub) ns as

192 = mkLHSargs (extend a t sub) ns as

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

187

194

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

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

189 extend _ _ sub = sub

196 extend _ _ sub = sub

190

197

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

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

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

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

193− delab ist (substNames amap oldrhs)

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

194−

201+ mkRHSargs _ _ = []

202+

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

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

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

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

197 mkSubst _ = Nothing

205 mkSubst _ = Nothing

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

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

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

249 ss' = buildApp env ss is as ns in

257 ss' = buildApp env ss is as ns in

250 (s' : ss')

258 (s' : ss')

251−

259+

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

261+ -- it will become a specialised application

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

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

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

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

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

254− case (lookupCtxt n (idris_statics ist),

265+ case (lookupCtxt n (idris_statics ist),

255− lookupCtxt n (idris_implicits ist)) of

266+ lookupCtxt n (idris_implicits ist)) of

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

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

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

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

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

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

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

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

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

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

261−-- _ -> []

272+-- _ -> []

262− else []

273+ else []

263− _ -> []

274+ _ -> []

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

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

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

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

266 ga env t = []

277 ga env t = []