6bcf43a · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #1625 from edwinb/partial-eval

6bcf43aEdwin Brady12 years ago

src/Idris/Core/Evaluate.hs+8−3

compare with master

unifiedsplit

@@ -89,12 +89,17 @@ normaliseTrace tr ctxt env t

89 = evalState (do val <- eval tr ctxt [] (map finalEntry env) (finalise t) []

90 quote 0 val) initEval

92+-- Return a specialised name, and an updated list of reductions available,

93+-- so that the caller can tell how much specialisation was achieved.

92−specialise :: Context -> Env -> [(Name, Int)] -> TT Name -> TT Name

94+specialise :: Context -> Env -> [(Name, Int)] -> TT Name ->

95+ (TT Name, [(Name, Int)])

93specialise ctxt env limits t

96specialise ctxt env limits t

97+ = let (tm, st) =

94− = evalState (do val <- eval False ctxt []

98+ runState (do val <- eval False ctxt []

95 (map finalEntry env) (finalise t)

99 (map finalEntry env) (finalise t)

96 [Spec]

100 [Spec]

97− quote 0 val) (initEval { limited = limits })

101+ quote 0 val) (initEval { limited = limits }) in

102+ (tm, limited st)

103

99-- | Like normalise, but we only reduce functions that are marked as okay to

104-- | Like normalise, but we only reduce functions that are marked as okay to

100-- inline (and probably shouldn't reduce lets?)

105-- inline (and probably shouldn't reduce lets?)

src/Idris/Core/ProofState.hs+2−2

@@ -651,7 +651,7 @@ casetac tm induction ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do

651 mapM_ addConsHole (reverse consargs')

652 let res' = forget $ res

653 (scv, sct) <- lift $ check ctxt env res'

654− let scv' = specialise ctxt env [] scv

654+ let (scv', _) = specialise ctxt env [] scv

655 return scv'

656 [] -> fail $ tactt ++ " needs " ++ tacstr ++ " for " ++ show tnm

657 xs -> fail $ "Multiple definitions found when searching for " ++ tacstr ++ "of " ++ show tnm

@@ -705,7 +705,7 @@ hnf_compute ctxt env t = return t

705-- reduce let bindings only

706simplify :: RunTactic

707simplify ctxt env (Bind x (Hole ty) sc) =

708− do return $ Bind x (Hole (specialise ctxt env [] ty)) sc

708+ do return $ Bind x (Hole (fst (specialise ctxt env [] ty))) sc

709simplify ctxt env t = return t

710

711check_in :: Raw -> RunTactic

src/Idris/Elab/Clause.hs+60−56

@@ -90,22 +90,23 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

90 Nothing -> transformPats ist pats_in

91 _ -> pats_in

93+ -- If the definition is specialisable, this reduces the

94+ -- RHS

95+ pe_tm <- doPartialEval ist tpats

93− let pats = map (simple_lhs (tt_ctxt ist)) $

96+ let pats = map (simple_lhs (tt_ctxt ist)) pe_tm

94− doPartialEval ist tpats

96− -- logLvl 3 (showSep "\n" (map (\ (l,r) ->

97− -- show l ++ " = " ++

98− -- show r) pats))

99 let tcase = opt_typecase (idris_options ist)

98 let tcase = opt_typecase (idris_options ist)

100

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

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

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

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

103 -- for partially evaluated definitions

102 -- for partially evaluated definitions

104− mapM_ (\ e -> case e of

103+ newrules <- mapM (\ e -> case e of

105− Left _ -> return ()

104+ Left _ -> return []

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

105+ Right (l, r) -> elabPE info fc n r) pats

107

106

108− -- Redo transforms with the newly generated transformations

107+ -- Redo transforms with the newly generated transformations, so

108+ -- that the specialised application we've just made gets

109+ -- used in place of the general one

109 ist <- getIState

110 ist <- getIState

110 let pats_transformed = transformPats ist pats

111 let pats_transformed = transformPats ist pats

111

112

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

134 numArgs <- tclift $ sameLength pdef

135 numArgs <- tclift $ sameLength pdef

135

136

136 case specNames opts of

137 case specNames opts of

138+ Just _ ->

137− Just _ -> logLvl 1 $ "Partially evaluated:\n" ++ show pats

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

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

138 _ -> return ()

141 _ -> return ()

139

142

140 erInfo <- getErasureInfo <$> getIState

143 erInfo <- getErasureInfo <$> getIState

@@ -257,22 +260,12 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

257

260

258 getLHS (_, l, _) = l

261 getLHS (_, l, _) = l

259

262

260− simple_lhs ctxt (Right (x, y)) = Right (normalise ctxt [] x,

263+ simple_lhs ctxt (Right (x, y)) = Right (normalise ctxt [] x, y)

261− force (normalisePats ctxt [] y))

262 simple_lhs ctxt t = t

264 simple_lhs ctxt t = t

263

265

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

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

265 (rt_simplify ctxt [] y)))

267 (rt_simplify ctxt [] y)))

266

268

267− -- this is so pattern types are in the right form for erasure

268− normalisePats ctxt env (Bind n (PVar t) sc)

269− = let t' = normalise ctxt env t in

270− Bind n (PVar t') (normalisePats ctxt ((n, PVar t') : env) sc)

271− normalisePats ctxt env (Bind n (PVTy t) sc)

272− = let t' = normalise ctxt env t in

273− Bind n (PVTy t') (normalisePats ctxt ((n, PVar t') : env) sc)

274− normalisePats ctxt env t = t

275−

276 specNames [] = Nothing

269 specNames [] = Nothing

277 specNames (Specialise ns : _) = Just ns

270 specNames (Specialise ns : _) = Just ns

278 specNames (_ : xs) = specNames xs

271 specNames (_ : xs) = specNames xs

@@ -287,15 +280,19 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

287 -- Partially evaluate, if the definition is marked as specialisable

280 -- Partially evaluate, if the definition is marked as specialisable

288 doPartialEval ist pats =

281 doPartialEval ist pats =

289 case specNames opts of

282 case specNames opts of

290− Nothing -> pats

283+ Nothing -> return pats

291− Just ns -> partial_eval (tt_ctxt ist) ns pats

284+ Just ns -> case partial_eval (tt_ctxt ist) ns pats of

292−

285+ Just t -> return t

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

287+

293−-- | Find 'static' applications in a term and partially evaluate them

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

289+-- Return any new transformation rules

294−elabPE :: ElabInfo -> FC -> Name -> Term -> Idris ()

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

295elabPE info fc caller r =

291elabPE info fc caller r =

296 do ist <- getIState

292 do ist <- getIState

297 let sa = getSpecApps ist [] r

293 let sa = getSpecApps ist [] r

298− mapM_ (mkSpecialised ist) sa

294+ rules <- mapM mkSpecialised sa

295+ return $ concat rules

299 where

296 where

300 -- Make a specialised version of the application, and

297 -- Make a specialised version of the application, and

301 -- add a PTerm level transformation rule, which is basically the

298 -- add a PTerm level transformation rule, which is basically the

@@ -305,41 +302,48 @@ elabPE info fc caller r =

305

302

306 -- Transformation rules are applied after every PClause elaboration

303 -- Transformation rules are applied after every PClause elaboration

307

304

305+ mkSpecialised :: (Name, [(PEArgType, Term)]) -> Idris [(Term, Term)]

308− mkSpecialised ist specapp_in = do

306+ mkSpecialised specapp_in = do

307+ ist <- getIState

309 let (specTy, specapp) = getSpecTy ist specapp_in

308 let (specTy, specapp) = getSpecTy ist specapp_in

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

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

311− let undef = case lookupDef newnm (tt_ctxt ist) of

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

312− [] -> True

311+ Nothing -> True

313 _ -> False

312 _ -> False

314− logLvl 3 $ show (newnm, map (concreteArg ist) (snd specapp))

313+ logLvl 5 $ show (newnm, undef, map (concreteArg ist) (snd specapp))

315 idrisCatch

314 idrisCatch

316− (when (undef && all (concreteArg ist) (snd specapp)) $ do

315+ (if (undef && all (concreteArg ist) (snd specapp)) then do

317− cgns <- getAllNames n

316+ cgns <- getAllNames n

317+ let cgns' = filter (/= n) cgns

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

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

319+ (n, Just 65536) :

319− mapMaybe specName (snd specapp))]

320+ mapMaybe specName (snd specapp))]

320− logLvl 3 $ "Specialising application: " ++ show specapp

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

321− ++ " with " ++ show opts

322+ ++ " with " ++ show opts

322− logLvl 3 $ "New name: " ++ show newnm

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

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

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

324− ++ "\n" ++ show opts

325+ ++ "\n" ++ show opts

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

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

326−-- showSep "\n"

327+ -- showSep "\n"

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

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

328− (showTmImpls lhs ++ " = " ++

329+ (showTmImpls lhs ++ " = " ++

329− showTmImpls rhs) -- pats)

330+ showTmImpls rhs) -- pats)

330−

331+

331− logLvl 2 $ show n ++ " transformation rule: " ++

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

332− show rhs ++ " ==> " ++ show lhs

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

333−

334+

334− elabType info defaultSyntax emptyDocstring [] fc opts newnm specTy

335+ elabType info defaultSyntax emptyDocstring [] fc opts newnm specTy

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

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

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

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

337− elabTransform info fc False rhs lhs

338+ trans <- elabTransform info fc False rhs lhs

338− elabClauses info fc opts newnm def)

339+ elabClauses info fc opts newnm def

340+ return [trans]

341+ else return [])

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

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

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

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

341 -- lifted out).

344 -- lifted out).

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

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

346+ return [])

343

347

344 specName (ImplicitS, tm)

348 specName (ImplicitS, tm)

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

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

@@ -370,7 +374,7 @@ elabPE info fc caller r =

370

374

371 -- get the clause of a specialised application

375 -- get the clause of a specialised application

372 getSpecClause ist (n, args)

376 getSpecClause ist (n, args)

373− = let newnm = sUN ("PE_"++ show (nsroot n) ++ "_" ++

377+ = let newnm = sUN ("PE_" ++ show (nsroot n) ++ "_" ++

374 qhash 0 (showSep "_" (map showArg args))) in

378 qhash 0 (showSep "_" (map showArg args))) in

375 -- UN (show n ++ show (map snd args)) in

379 -- UN (show n ++ show (map snd args)) in

376 (n, newnm, mkPE_TermDecl ist newnm n args)

380 (n, newnm, mkPE_TermDecl ist newnm n args)

src/Idris/Elab/Transform.hs+2−1

@@ -48,7 +48,7 @@ import Data.List.Split (splitOn)

49import Util.Pretty(pretty, text)

51−elabTransform :: ElabInfo -> FC -> Bool -> PTerm -> PTerm -> Idris ()

51+elabTransform :: ElabInfo -> FC -> Bool -> PTerm -> PTerm -> Idris (Term, Term)

52elabTransform info fc safe lhs_in@(PApp _ (PRef _ tf) _) rhs_in

53 = do ctxt <- getContext

54 i <- getIState

@@ -88,6 +88,7 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ tf) _) rhs_in

88 (P _ tfname _, _) -> do addTrans tfname (clhs_tm, crhs_tm)

89 addIBC (IBCTrans tf (clhs_tm, crhs_tm))

90 _ -> ierror (At fc (Msg "Invalid transformation rule (must be function application)"))

91+ return (clhs_tm, crhs_tm)

92 where

93 where

93 depat (Bind n (PVar t) sc) = depat (instantiate (P Bound n t) sc)

94 depat (Bind n (PVar t) sc) = depat (instantiate (P Bound n t) sc)

src/Idris/ElabDecls.hs+2−1

@@ -254,6 +254,7 @@ elabDecl' what info (PProvider syn fc provWhat n)

254 = do iLOG $ "Elaborating type provider " ++ show n

255 elabProvider info syn fc provWhat n

256elabDecl' what info (PTransform fc safety old new)

257− = elabTransform info fc safety old new

257+ = do elabTransform info fc safety old new

258+ return ()

258elabDecl' _ _ _ = return () -- skipped this time

259elabDecl' _ _ _ = return () -- skipped this time

259

260

src/Idris/Interactive.hs+1−1

@@ -188,7 +188,7 @@ doProofSearch fn updatefile rec l n hints (Just depth)

188 pprintPTerm defaultPPOption [] [] (idris_infixes i)

189 (stripNS

190 (dropCtxt envlen

191− (delab i (specialise ctxt [] [(mn, 1)] tm)))))

191+ (delab i (fst (specialise ctxt [] [(mn, 1)] tm))))))

192 (\e -> return ("?" ++ show n))

193 if updatefile then

194 do let fb = fn ++ "~"

src/Idris/PartialEval.hs+17−6

@@ -13,20 +13,31 @@ import Control.Monad.State

13import Debug.Trace

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

16+-- 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

18+-- reduction limits must have reduced at least once.

16−partial_eval :: Context -> [(Name, Maybe Int)] ->

19+partial_eval :: Context ->

20+ [(Name, Maybe Int)] ->

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

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

18− [Either Term (Term, Term)]

22+ Maybe [Either Term (Term, Term)]

19−partial_eval ctxt ns tms = map peClause tms where

23+partial_eval ctxt ns tms = mapM peClause tms where

20 -- If the term is not a clause, it is simply kept as is

24 -- If the term is not a clause, it is simply kept as is

21− peClause (Left t) = Left t

25+ peClause (Left t) = Just $ Left t

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

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

23 peClause (Right (lhs, rhs))

27 peClause (Right (lhs, rhs))

24− = let rhs' = specialise ctxt [] (map toLimit ns) rhs in

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

29+ do checkProgress ns reductions

25− Right (lhs, rhs')

30+ return (Right (lhs, rhs'))

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

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

28 toLimit (n, Just l) = (n, l)

33 toLimit (n, Just l) = (n, l)

35+ checkProgress ns [] = return ()

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

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

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

39+ | otherwise = checkProgress ns rs

40+

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

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

31-- a pair of the specialised type and the types of expected arguments.

42-- a pair of the specialised type and the types of expected arguments.

32specType :: [(PEArgType, Term)] -> Type -> (Type, [(PEArgType, Term)])

43specType :: [(PEArgType, Term)] -> Type -> (Type, [(PEArgType, Term)])

src/Idris/Transforms.hs+37−13

@@ -1,6 +1,9 @@

1{-# LANGUAGE PatternGuards #-}

3−module Idris.Transforms(transformPats, applyTransRules) where

3+module Idris.Transforms(transformPats,

4+ transformPatsWith,

5+ applyTransRulesWith,

6+ applyTransRules) where

5import Idris.AbsSyntax

8import Idris.AbsSyntax

6import Idris.Core.CaseTree

9import Idris.Core.CaseTree

@@ -16,19 +19,40 @@ transformPats ist ps = map tClause ps where

16 = let rhs' = applyTransRules ist rhs in

19 = let rhs' = applyTransRules ist rhs in

17 Right (lhs, rhs')

20 Right (lhs, rhs')

22+transformPatsWith :: [(Term, Term)] -> [Either Term (Term, Term)] ->

23+ [Either Term (Term, Term)]

24+transformPatsWith rs ps = map tClause ps where

25+ tClause (Left t) = Left t -- not a clause, leave it alone

26+ tClause (Right (lhs, rhs)) -- apply transforms on RHS

27+ = let rhs' = applyTransRulesWith rs rhs in

28+ Right (lhs, rhs')

29+

30+-- Work on explicitly named terms, so we don't have to manipulate

31+-- de Bruijn indices

19applyTransRules :: IState -> Term -> Term

32applyTransRules :: IState -> Term -> Term

20−applyTransRules ist tm = applyAll (idris_transforms ist) tm

33+applyTransRules ist tm = finalise $ applyAll [] (idris_transforms ist) (vToP tm)

34+

35+-- Work on explicitly named terms, so we don't have to manipulate

36+-- de Bruijn indices

37+applyTransRulesWith :: [(Term, Term)] -> Term -> Term

38+applyTransRulesWith rules tm

39+ = finalise $ applyAll rules emptyContext (vToP tm)

22−applyAll :: Ctxt [(Term, Term)] -> Term -> Term

41+applyAll :: [(Term, Term)] -> Ctxt [(Term, Term)] -> Term -> Term

23−applyAll ts ap@(App f a)

42+applyAll extra ts ap@(App f a)

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

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

25− = case lookupCtxtExact fn ts of

44+ = let rules = case lookupCtxtExact fn ts of

45+ Just r -> extra ++ r

46+ Nothing -> extra in

47+ case rules of

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

26− Just rules -> case applyFnRules rules ap of

49+ rs -> case applyFnRules rs ap of

27 Just tm' -> tm'

50 Just tm' -> tm'

28− _ -> App (applyAll ts f) (applyAll ts a)

51+ _ -> App (applyAll extra ts f)

29− Nothing -> App (applyAll ts f) (applyAll ts a)

52+ (applyAll extra ts a)

30−applyAll ts (Bind n b sc) = Bind n (fmap (applyAll ts) b) (applyAll ts sc)

53+applyAll extra ts (Bind n b sc) = Bind n (fmap (applyAll extra ts) b)

54+ (applyAll extra ts sc)

31−applyAll ts t = t

55+applyAll extra ts t = t

33applyFnRules :: [(Term, Term)] -> Term -> Maybe Term

57applyFnRules :: [(Term, Term)] -> Term -> Maybe Term

34applyFnRules [] tm = Nothing

58applyFnRules [] tm = Nothing

@@ -40,12 +64,12 @@ applyRule (lhs, rhs) tm

40 | Just ms <- matchTerm lhs tm

64 | Just ms <- matchTerm lhs tm

41-- = trace ("SUCCESS " ++ show ms ++ "\n FROM\n" ++ show lhs ++

65-- = trace ("SUCCESS " ++ show ms ++ "\n FROM\n" ++ show lhs ++

42-- "\n" ++ show rhs

66-- "\n" ++ show rhs

43−-- ++ "\n" ++ show tm) $

67+-- ++ "\n" ++ show tm ++ " GIVES\n" ++ show (depat ms rhs)) $

44− = Just $ depat ms rhs

68+ = Just $ depat ms rhs

45 | otherwise = Nothing

69 | otherwise = Nothing

46 where depat ms (Bind n (PVar t) sc)

70 where depat ms (Bind n (PVar t) sc)

47 = case lookup n ms of

71 = case lookup n ms of

48− Just tm -> depat ms (instantiate tm sc)

72+ Just tm -> depat ms (subst n tm sc)

49 _ -> depat ms sc -- no occurrence? Shouldn't happen

73 _ -> depat ms sc -- no occurrence? Shouldn't happen

50 depat ms tm = tm

74 depat ms tm = tm