466a2e7 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #1654 from edwinb/partial-eval

466a2e7Edwin 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/AbsSyntax.hs+13−1

@@ -1058,10 +1058,17 @@ getPriority i tm = 1 -- pri tm

1058addStatics :: Name -> Term -> PTerm -> Idris ()

1059addStatics n tm ptm =

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

1061+ ist <- getIState

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

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

1064+ _ -> []

1065+

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

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

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

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

1068+ \\ paramnames

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

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

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

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

1071+ -- or parameters to the type of a static

1065 let statics' = nub $ map fst statics ++

1072 let statics' = nub $ map fst statics ++

1066 filter (\x -> not (elem x dnames)) stnames

1073 filter (\x -> not (elem x dnames)) stnames

1067 let stpos = staticList statics' tm

1074 let stpos = staticList statics' tm

@@ -1084,8 +1091,13 @@ addStatics n tm ptm =

1084 else (static, dynamic)

1091 else (static, dynamic)

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

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

1086

1093

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

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

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

1097+ getNamesFrom i ps sc = []

1098+

1087 freeArgNames (Bind n (Pi ty _) sc)

1099 freeArgNames (Bind n (Pi ty _) sc)

1088− = nub $ freeArgNames ty

1100+ = nub $ freeNames ty ++ freeNames sc -- treat '->' as fn here

1089 freeArgNames tm = let (_, args) = unApply tm in

1101 freeArgNames tm = let (_, args) = unApply tm in

1090 concatMap freeNames args

1102 concatMap freeNames args

1091

1103

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+14−9

@@ -16,7 +16,7 @@ import Idris.Inliner

16import Idris.PartialEval

17import Idris.Transforms

18import Idris.DeepSeq

19−import Idris.Output (iputStrLn, pshow, iWarn)

19+import Idris.Output (iputStrLn, pshow, iWarn, iRenderResult)

20import IRTS.Lang

22import Idris.Elab.Type

@@ -31,6 +31,7 @@ import Idris.Core.Typecheck

31import Idris.Core.CaseTree

33import Idris.Docstrings

34+import Util.Pretty hiding ((<$>))

35import Prelude hiding (id, (.))

36import Prelude hiding (id, (.))

36import Control.Category

37import Control.Category

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

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

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

291elabPE info fc caller r =

292elabPE info fc caller r =

292 do ist <- getIState

293 do ist <- getIState

293− let sa = getSpecApps ist [] r

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

294 rules <- mapM mkSpecialised sa

295 rules <- mapM mkSpecialised sa

295 return $ concat rules

296 return $ concat rules

296 where

297 where

@@ -306,7 +307,9 @@ elabPE info fc caller r =

306 mkSpecialised specapp_in = do

307 mkSpecialised specapp_in = do

307 ist <- getIState

308 ist <- getIState

308 let (specTy, specapp) = getSpecTy ist specapp_in

309 let (specTy, specapp) = getSpecTy ist specapp_in

309− let (n, newnm, (lhs, rhs)) = getSpecClause ist specapp

310+ let (n, newnm, specdecl) = getSpecClause ist specapp

311+ let lhs = pe_app specdecl

312+ let rhs = pe_def specdecl

310 let undef = case lookupDefExact newnm (tt_ctxt ist) of

313 let undef = case lookupDefExact newnm (tt_ctxt ist) of

311 Nothing -> True

314 Nothing -> True

312 _ -> False

315 _ -> False

@@ -319,22 +322,24 @@ elabPE info fc caller r =

319 (n, Just 65536) :

322 (n, Just 65536) :

320 mapMaybe specName (snd specapp))]

323 mapMaybe specName (snd specapp))]

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

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

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

322− ++ " with " ++ show opts

326+ " with " ++ show opts

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

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

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

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

325 ++ "\n" ++ show opts

329 ++ "\n" ++ show opts

326 logLvl 3 $ "PE definition " ++ show newnm ++ ":\n" ++

330 logLvl 3 $ "PE definition " ++ show newnm ++ ":\n" ++

327− -- showSep "\n"

331+ showSep "\n"

328− -- (map (\ (lhs, rhs) ->

332+ (map (\ (lhs, rhs) ->

329 (showTmImpls lhs ++ " = " ++

333 (showTmImpls lhs ++ " = " ++

330− showTmImpls rhs) -- pats)

334+ showTmImpls rhs)) (pe_clauses specdecl))

331

335

332 logLvl 2 $ show n ++ " transformation rule: " ++

336 logLvl 2 $ show n ++ " transformation rule: " ++

333 show rhs ++ " ==> " ++ show lhs

337 show rhs ++ " ==> " ++ show lhs

334

338

335 elabType info defaultSyntax emptyDocstring [] fc opts newnm specTy

339 elabType info defaultSyntax emptyDocstring [] fc opts newnm specTy

336− let def = -- map (\ (lhs, rhs) ->

340+ let def = map (\(lhs, rhs) ->

337− [PClause fc newnm lhs [] rhs []] --) pats

341+ PClause fc newnm lhs [] rhs [])

342+ (pe_clauses specdecl)

338 trans <- elabTransform info fc False rhs lhs

343 trans <- elabTransform info fc False rhs lhs

339 elabClauses info fc opts newnm def

344 elabClauses info fc opts newnm def

340 return [trans]

345 return [trans]

src/Idris/ElabTerm.hs+5−3

@@ -499,9 +499,11 @@ elab ist info emode opts fn tm

499 _ -> lift $ tfail (NoSuchVariable fn)

500 ns <- match_apply (Var fn') (map (\x -> (x,0)) imps)

501 solve

502+ -- This isn't a sound way of checking for Typecase - we need a

503+ -- better way!

502− elab' (_, _, inty, qq) (PApp fc (PRef _ f) args')

504+-- elab' (_, _, inty, qq) (PApp fc (PRef _ f) args')

503− | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty && not qq

505+-- | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty && not qq

504− = lift $ tfail (Msg "Typecase is not allowed")

506+-- = lift $ tfail (Msg "Typecase is not allowed")

505 -- if f is local, just do a simple_app

507 -- if f is local, just do a simple_app

506 elab' (ina, g, inty, qq) tm@(PApp fc (PRef _ f) args)

508 elab' (ina, g, inty, qq) tm@(PApp fc (PRef _ f) args)

507 = do env <- get_env

509 = do env <- get_env

src/Idris/PartialEval.hs+120−28

@@ -1,7 +1,8 @@

1{-# LANGUAGE PatternGuards #-}

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

4− mkPE_TyDecl, mkPE_TermDecl, PEArgType(..)) where

4+ mkPE_TyDecl, mkPE_TermDecl, PEArgType(..),

5+ pe_app, pe_def, pe_clauses) where

6import Idris.AbsSyntax

7import Idris.AbsSyntax

7import Idris.Delaborate

8import Idris.Delaborate

@@ -10,12 +11,32 @@ import Idris.Core.TT

10import Idris.Core.Evaluate

11import Idris.Core.Evaluate

12import Control.Monad.State

13import Control.Monad.State

14+import Data.Maybe

13import Debug.Trace

15import Debug.Trace

17+-- | Data type representing binding-time annotations for partial evaluation of arguments

18+data PEArgType = ImplicitS -- ^ Implicit static argument

19+ | ImplicitD -- ^ Implicit dynamic argument

20+ | ExplicitS -- ^ Explicit static argument

21+ | ExplicitD -- ^ Explicit dynamic argument

22+ | UnifiedD -- ^ Erasable dynamic argument (found under unification)

23+ deriving (Eq, Show)

24+

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+data PEDecl = PEDecl { pe_app :: PTerm, -- new application

29+ pe_def :: PTerm, -- old application

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

31+ }

32+

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

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

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

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

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

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

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

18−-- 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.

19partial_eval :: Context ->

40partial_eval :: Context ->

20 [(Name, Maybe Int)] ->

41 [(Name, Maybe Int)] ->

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

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

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

35 checkProgress ns [] = return ()

56 checkProgress ns [] = return ()

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

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

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

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

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

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

39 | otherwise = checkProgress ns rs

60 | otherwise = checkProgress ns rs

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

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

@@ -118,13 +139,89 @@ concreteClass ist v

118 _ -> False

139 _ -> False

119 | otherwise = False

140 | otherwise = False

120

141

142+mkNewPats :: IState ->

143+ [(Term, Term)] -> -- definition to specialise

144+ [(PEArgType, Term)] -> -- arguments to specialise with

145+ Name -> -- New name

146+ Name -> -- Specialised function name

147+ PTerm -> -- Default lhs

148+ PTerm -> -- Default rhs

149+ PEDecl

150+-- If all of the dynamic positions on the lhs are variables (rather than

151+-- patterns or constants) then we can just make a simple definition

152+-- directly applying the specialised function, since we know the

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

154+-- in this case

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

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

157+ where dynVar ap = case unApply ap of

158+ (_, args) -> dynArgs ns args

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

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

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

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

163+ -- if Dynamic, it had better be a variable or we'll need to

164+ -- do some more work

165+ dynArgs (_ : ns) (V _ : as) = dynArgs ns as

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

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

168+mkNewPats ist d ns newname sname lhs rhs =

169+ PEDecl lhs rhs (map mkClause d)

170+ where

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

172+ mkClause (oldlhs, oldrhs)

173+ = let (_, as) = unApply oldlhs

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

178+ (lhs, rhs)

179+

180+ mkLHSargs _ [] [] = []

181+ -- dynamics don't appear if they're implicit

182+ mkLHSargs sub ((ExplicitD, t) : ns) (a : as)

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

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

185+ = mkLHSargs sub ns as

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

187+ = mkLHSargs sub ns as

188+ -- statics get dropped in any case

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

190+ = mkLHSargs (extend a t sub) ns as

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

192+ = mkLHSargs (extend a t sub) ns as

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

194+

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

196+ extend _ _ sub = sub

197+

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+

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

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

205+ mkSubst _ = Nothing

206+

121−-- | Creates a new clause for a specialised function application

207+-- | Creates a new declaration for a specialised function application.

208+-- Simple version at the moment: just create a version which is a direct

209+-- application of the function to be specialised.

210+-- More complex version to do: specialise the definition clause by clause

122mkPE_TermDecl :: IState -> Name -> Name ->

211mkPE_TermDecl :: IState -> Name -> Name ->

123− [(PEArgType, Term)] -> (PTerm, PTerm)

212+ [(PEArgType, Term)] -> PEDecl

124mkPE_TermDecl ist newname sname ns

213mkPE_TermDecl ist newname sname ns

125 = let lhs = PApp emptyFC (PRef emptyFC newname) (map pexp (mkp ns))

214 = let lhs = PApp emptyFC (PRef emptyFC newname) (map pexp (mkp ns))

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

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

216+ patdef = lookupCtxtExact sname (idris_patdefs ist)

217+ newpats = case patdef of

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

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

220+ newname sname lhs rhs in

127− (lhs, rhs) where

221+ newpats where

222+

223+ getPats (ps, _) = map (\(_, lhs, rhs) -> (lhs, rhs)) ps

224+

128 mkp [] = []

225 mkp [] = []

129 mkp ((ExplicitD, tm) : tms) = delab ist tm : mkp tms

226 mkp ((ExplicitD, tm) : tms) = delab ist tm : mkp tms

130 mkp (_ : tms) = mkp tms

227 mkp (_ : tms) = mkp tms

@@ -137,14 +234,6 @@ mkPE_TermDecl ist newname sname ns

137 deImpArg a@(PImp _ _ _ _ _) = a { getTm = Placeholder }

234 deImpArg a@(PImp _ _ _ _ _) = a { getTm = Placeholder }

138 deImpArg a = a

235 deImpArg a = a

139

236

140−-- | Data type representing binding-time annotations for partial evaluation of arguments

141−data PEArgType = ImplicitS -- ^ Implicit static argument

142− | ImplicitD -- ^ Implicit dynamic argument

143− | ExplicitS -- ^ Explicit static argument

144− | ExplicitD -- ^ Explicit dynamic argument

145− | UnifiedD -- ^ Erasable dynamic argument (found under unification)

146− deriving (Eq, Show)

147−

148-- | Get specialised applications for a given function

237-- | Get specialised applications for a given function

149getSpecApps :: IState -> [Name] -> Term ->

238getSpecApps :: IState -> [Name] -> Term ->

150 [(Name, [(PEArgType, Term)])]

239 [(Name, [(PEArgType, Term)])]

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

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

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

168 ss' = buildApp env ss is as ns in

257 ss' = buildApp env ss is as ns in

169 (s' : ss')

258 (s' : ss')

170−

259+

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

261+ -- it will become a specialised application

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

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

172− ga env f ++ ga env a ++

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

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

173− case (lookupCtxt n (idris_statics ist),

265+ case (lookupCtxt n (idris_statics ist),

174− lookupCtxt n (idris_implicits ist)) of

266+ lookupCtxt n (idris_implicits ist)) of

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

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

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

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

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

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

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

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

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

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

180−-- _ -> []

272+-- _ -> []

181− else []

273+ else []

182− _ -> []

274+ _ -> []

183 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

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

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

185 ga env t = []

277 ga env t = []