3971cb9 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

More partial evaluation improvements

3971cb9Edwin Brady12 years ago

src/Idris/Elab/Clause.hs+19−11

compare with master

unifiedsplit

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

149

150 case specNames opts of

151 Just _ ->

152− do logLvl 2 $ "Partially evaluated:\n" ++ show pats_pe

152+ do logLvl 3 $ "Partially evaluated:\n" ++ show pats_pe

153− logLvl 2 $ "Transformed:\n" ++ show pats_transformed

154 _ -> return ()

153 _ -> return ()

154+ logLvl 3 $ "Transformed:\n" ++ show pats_transformed

155

156 erInfo <- getErasureInfo <$> getIState

157 tree@(CaseDef scargs sc _) <- tclift $

@@ -333,8 +333,14 @@ elabPE info fc caller r =

333 idrisCatch

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

335 cgns <- getAllNames n

336+ -- on the RHS of the new definition, we should reduce

337+ -- everything that's not itself static (because we'll

338+ -- want to be a PE version of those next)

336− let cgns' = filter (/= n) cgns

339+ let cgns' = filter (\x -> x /= n &&

340+ notStatic ist x) cgns

341+ let opts = [Specialise ((if pe_simple specdecl

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

342+ then map (\x -> (x, Nothing)) cgns'

343+ else []) ++

338 (n, Just 65536) :

344 (n, Just 65536) :

339 mapMaybe (specName (pe_simple specdecl))

345 mapMaybe (specName (pe_simple specdecl))

340 (snd specapp))]

346 (snd specapp))]

@@ -347,7 +353,7 @@ elabPE info fc caller r =

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

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

348 showSep "\n"

354 showSep "\n"

349 (map (\ (lhs, rhs) ->

355 (map (\ (lhs, rhs) ->

350− (showTmImpls lhs ++ " = " ++

356+ (show lhs ++ " = " ++

351 showTmImpls rhs)) (pe_clauses specdecl))

357 showTmImpls rhs)) (pe_clauses specdecl))

352

358

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

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

@@ -373,6 +379,10 @@ elabPE info fc caller r =

373 | (P Ref n _, _) <- unApply tm = Just (n, Just (if simpl then 1 else 0))

379 | (P Ref n _, _) <- unApply tm = Just (n, Just (if simpl then 1 else 0))

374 specName simpl _ = Nothing

380 specName simpl _ = Nothing

375

381

382+ notStatic ist n = case lookupCtxtExact n (idris_statics ist) of

383+ Just s -> not (or s)

384+ _ -> True

385+

376 concreteArg ist (ImplicitS, tm) = concreteTm ist tm

386 concreteArg ist (ImplicitS, tm) = concreteTm ist tm

377 concreteArg ist (ExplicitS, tm) = concreteTm ist tm

387 concreteArg ist (ExplicitS, tm) = concreteTm ist tm

378 concreteArg ist _ = True

388 concreteArg ist _ = True

@@ -554,6 +564,8 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

554

564

555 let lhs_tm = orderPats (getInferTerm lhs')

565 let lhs_tm = orderPats (getInferTerm lhs')

556 let lhs_ty = getInferType lhs'

566 let lhs_ty = getInferType lhs'

567+ let static_names = getStaticNames i lhs_tm

568+

557 logLvl 3 ("Elaborated: " ++ show lhs_tm)

569 logLvl 3 ("Elaborated: " ++ show lhs_tm)

558 logLvl 3 ("Elaborated type: " ++ show lhs_ty)

570 logLvl 3 ("Elaborated type: " ++ show lhs_ty)

559 logLvl 5 ("Injective: " ++ show fname ++ " " ++ show inj)

571 logLvl 5 ("Injective: " ++ show fname ++ " " ++ show inj)

@@ -596,7 +608,8 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

596 let newargs = filter (\(n,_) -> n `notElem` uniqargs) newargs_all

608 let newargs = filter (\(n,_) -> n `notElem` uniqargs) newargs_all

597

609

598 let winfo = pinfo info newargs defs windex

610 let winfo = pinfo info newargs defs windex

611+ let wb = map (mkStatic static_names) $

599− let wb = map (expandParamsD False ist decorate newargs defs) whereblock

612+ map (expandParamsD False ist decorate newargs defs) whereblock

600

613

601 -- Split the where block into declarations with a type, and those

614 -- Split the where block into declarations with a type, and those

602 -- without

615 -- without

@@ -875,11 +888,6 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

875 getImps (Bind n (Pi _ _) t) = pexp Placeholder : getImps t

888 getImps (Bind n (Pi _ _) t) = pexp Placeholder : getImps t

876 getImps _ = []

889 getImps _ = []

877

890

878− getStatics ns (Bind n (Pi _ _) t)

879− | n `elem` ns = True : getStatics ns t

880− | otherwise = False : getStatics ns t

881− getStatics _ _ = []

882−

883 mkAuxC wname lhs ns ns' (PClauses fc o n cs)

891 mkAuxC wname lhs ns ns' (PClauses fc o n cs)

884 | True = do cs' <- mapM (mkAux wname lhs ns ns') cs

892 | True = do cs' <- mapM (mkAux wname lhs ns ns') cs

885 return $ PClauses fc o wname cs'

893 return $ PClauses fc o wname cs'

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

@@ -223,7 +223,7 @@ elabInstance info syn what fc cs n ps t expn ds = do

223

224 mkTyDecl (n, op, t, _) = PTy emptyDocstring [] syn fc op n t

225

226− conbind (ty : ns) x = PPi (constraint { pstatic = Dynamic })

226+ conbind (ty : ns) x = PPi (constraint) -- { pstatic = Dynamic })

227 (sMN 0 "class") ty (conbind ns x)

228 conbind [] x = x

229

src/Idris/Elab/Utils.hs+17

@@ -251,5 +251,22 @@ getStaticNames ist tm

251 getStatics _ _ = []

252getStaticNames _ _ = []

253

254+getStatics :: [Name] -> Term -> [Bool]

255+getStatics ns (Bind n (Pi _ _) t)

256+ | n `elem` ns = True : getStatics ns t

257+ | otherwise = False : getStatics ns t

258+getStatics _ _ = []

259+

260+mkStatic :: [Name] -> PDecl -> PDecl

261+mkStatic ns (PTy doc argdocs syn fc o n ty)

262+ = PTy doc argdocs syn fc o n (mkStaticTy ns ty)

263+mkStatic ns t = t

264+

265+mkStaticTy :: [Name] -> PTerm -> PTerm

266+mkStaticTy ns (PPi p n ty sc)

267+ | n `elem` ns = PPi (p { pstatic = Static }) n ty (mkStaticTy ns sc)

268+ | otherwise = PPi p n ty (mkStaticTy ns sc)

269+mkStaticTy ns t = t

270+

254

271

255

272

src/Idris/PartialEval.hs+36−9

@@ -11,6 +11,7 @@ import Idris.Core.TT

11import Idris.Core.Evaluate

13import Control.Monad.State

14+import Control.Applicative

14import Data.Maybe

15import Data.Maybe

15import Debug.Trace

16import Debug.Trace

@@ -44,13 +45,25 @@ partial_eval :: Context ->

44 [(Name, Maybe Int)] ->

45 [(Name, Maybe Int)] ->

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

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

46 Maybe [Either Term (Term, Term)]

47 Maybe [Either Term (Term, Term)]

47−partial_eval ctxt ns tms = mapM peClause tms where

48+partial_eval ctxt ns_in tms = mapM peClause tms where

49+ ns = squash ns_in

50+ squash ((n, Just x) : ns)

51+ | Just (Just y) <- lookup n ns

52+ = squash ((n, Just (x + y)) : drop n ns)

53+ | otherwise = (n, Just x) : squash ns

54+ squash (n : ns) = n : squash ns

55+ squash [] = []

56+

57+ drop n ((m, _) : ns) | n == m = ns

58+ drop n (x : ns) = x : drop n ns

59+ drop n [] = []

60+

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

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

49 peClause (Left t) = Just $ Left t

62 peClause (Left t) = Just $ Left t

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

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

51 peClause (Right (lhs, rhs))

64 peClause (Right (lhs, rhs))

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

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

53− do checkProgress ns reductions

66+ do when (length tms == 1) $ checkProgress ns reductions

54 return (Right (lhs, rhs'))

67 return (Right (lhs, rhs'))

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

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

@@ -103,23 +116,37 @@ specType args ty = let (t, args') = runState (unifyEq args ty) [] in

103 put (args ++ (zip xs (repeat (sUN "_"))))

116 put (args ++ (zip xs (repeat (sUN "_"))))

104 return t

117 return t

105

118

106−-- | Creates an Idris type declaration given current state and a specialised TT function application type.

119+-- | Creates an Idris type declaration given current state and a

120+-- specialised TT function application type.

107-- Can be used in combination with the output of 'specType'.

121-- Can be used in combination with the output of 'specType'.

122+--

123+-- This should: specialise any static argument position, then generalise

124+-- over any function applications in the result.

108mkPE_TyDecl :: IState -> [(PEArgType, Term)] -> Type -> PTerm

125mkPE_TyDecl :: IState -> [(PEArgType, Term)] -> Type -> PTerm

109mkPE_TyDecl ist args ty = mkty args ty

126mkPE_TyDecl ist args ty = mkty args ty

110 where

127 where

111 mkty ((ExplicitD, v) : xs) (Bind n (Pi t k) sc)

128 mkty ((ExplicitD, v) : xs) (Bind n (Pi t k) sc)

112− = PPi expl n (delab ist t) (mkty xs sc)

129+ = PPi expl n (delab ist (generaliseIn t)) (mkty xs sc)

113 mkty ((ImplicitD, v) : xs) (Bind n (Pi t k) sc)

130 mkty ((ImplicitD, v) : xs) (Bind n (Pi t k) sc)

114 | concreteClass ist t = mkty xs sc

131 | concreteClass ist t = mkty xs sc

115 | classConstraint ist t

132 | classConstraint ist t

116− = PPi constraint n (delab ist t) (mkty xs sc)

133+ = PPi constraint n (delab ist (generaliseIn t)) (mkty xs sc)

117− | otherwise = PPi impl n (delab ist t) (mkty xs sc)

134+ | otherwise = PPi impl n (delab ist (generaliseIn t)) (mkty xs sc)

118

135

119 mkty (_ : xs) t

136 mkty (_ : xs) t

120 = mkty xs t

137 = mkty xs t

121 mkty [] t = delab ist t

138 mkty [] t = delab ist t

122

139

140+ generaliseIn tm = evalState (gen tm) 0

141+

142+ gen tm | (P _ fn _, args) <- unApply tm,

143+ isFnName fn (tt_ctxt ist)

144+ = do nm <- get

145+ put (nm + 1)

146+ return (P Bound (sMN nm "spec") Erased)

147+ gen (App f a) = App <$> gen f <*> gen a

148+ gen tm = return tm

149+

123-- | Checks if a given argument is a type class constraint argument

150-- | Checks if a given argument is a type class constraint argument

124classConstraint :: Idris.AbsSyntax.IState -> TT Name -> Bool

151classConstraint :: Idris.AbsSyntax.IState -> TT Name -> Bool

125classConstraint ist v

152classConstraint ist v

@@ -265,9 +292,9 @@ getSpecApps ist env tm = ga env (explicitNames tm) where

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

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

266 n `notElem` map fst (idris_metavars ist) =

293 n `notElem` map fst (idris_metavars ist) =

267 ga env f ++ ga env a ++

294 ga env f ++ ga env a ++

268− case (lookupCtxt n (idris_statics ist),

295+ case (lookupCtxtExact n (idris_statics ist),

269− lookupCtxt n (idris_implicits ist)) of

296+ lookupCtxtExact n (idris_implicits ist)) of

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

297+ (Just statics, Just imps) ->

271 if (length statics == length args && or statics) then

298 if (length statics == length args && or statics) then

272 case buildApp env statics imps args [0..] of

299 case buildApp env statics imps args [0..] of

273 args -> [(n, args)]

300 args -> [(n, args)]

src/Idris/Transforms.hs+4−1

@@ -47,7 +47,10 @@ applyAll extra ts ap@(App f a)

47 ap' = App (applyAll extra ts f) (applyAll extra ts a) in

48 case rules of

49 [] -> ap'

50− rs -> case applyFnRules rs ap' of

50+ rs -> case applyFnRules rs ap of

51+ Just tm'@(App f' a') ->

52+ App (applyAll extra ts f')

53+ (applyAll extra ts a')

51 Just tm' -> tm'

54 Just tm' -> tm'

52 _ -> App (applyAll extra ts f)

55 _ -> App (applyAll extra ts f)

53 (applyAll extra ts a)

56 (applyAll extra ts a)