7a1b64d · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #1667 from edwinb/partial-eval

More partial evaluation improvements

commit7a1b64da6e15ddf91812368c764185a7dcadc144 authorEdwin Brady <edwin.brady@gmail.com> dateSun 19 Oct 2014, 22:55 (12 years ago) parentfde21b7 3971cb9

5 files changed+77−22

compare with master

unifiedsplit

src/Idris/Elab/Clause.hs+19−11 src/Idris/Elab/Instance.hs+1−1 src/Idris/Elab/Utils.hs+17 src/Idris/PartialEval.hs+36−9 src/Idris/Transforms.hs+4−1

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

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

149149

150150 case specNames opts of

151151 Just _ ->

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

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

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

154153 _ -> return ()

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

155155

156156 erInfo <- getErasureInfo <$> getIState

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

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

333333 idrisCatch

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

335335 cgns <- getAllNames n

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

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

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)

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

340+ notStatic ist x) cgns

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

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

343+ else []) ++

338344 (n, Just 65536) :

339345 mapMaybe (specName (pe_simple specdecl))

340346 (snd specapp))]

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

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

348354 showSep "\n"

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

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

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

351357 showTmImpls rhs)) (pe_clauses specdecl))

352358

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

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

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

374380 specName simpl _ = Nothing

375381

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

383+ Just s -> not (or s)

384+ _ -> True

385+

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

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

378388 concreteArg ist _ = True

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

554564

555565 let lhs_tm = orderPats (getInferTerm lhs')

556566 let lhs_ty = getInferType lhs'

567+ let static_names = getStaticNames i lhs_tm

568+

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

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

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

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

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

597609

598610 let winfo = pinfo info newargs defs windex

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

611+ let wb = map (mkStatic static_names) $

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

600613

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

602615 -- without

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

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

876889 getImps _ = []

877890

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

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

880− | otherwise = False : getStatics ns t

881− getStatics _ _ = []

882−

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

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

885893 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

223223

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

225225

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

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

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

228228 conbind [] x = x

229229

src/Idris/Elab/Utils.hs+17

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

251251 getStatics _ _ = []

252252getStaticNames _ _ = []

253253

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+

254271

255272

src/Idris/PartialEval.hs+36−9

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

1111import Idris.Core.Evaluate

1212

1313import Control.Monad.State

14+import Control.Applicative

1415import Data.Maybe

1516import Debug.Trace

1617

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

4445 [(Name, Maybe Int)] ->

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

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

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

4962 peClause (Left t) = Just $ Left t

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

5164 peClause (Right (lhs, rhs))

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

53− do checkProgress ns reductions

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

5467 return (Right (lhs, rhs'))

5568

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

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

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

104117 return t

105118

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.

107121-- 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.

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

109126mkPE_TyDecl ist args ty = mkty args ty

110127 where

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

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

114131 | concreteClass ist t = mkty xs sc

115132 | classConstraint ist t

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

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

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

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

118135

119136 mkty (_ : xs) t

120137 = mkty xs t

121138 mkty [] t = delab ist t

122139

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+

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

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

125152classConstraint ist v

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

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

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

267294 ga env f ++ ga env a ++

268− case (lookupCtxt n (idris_statics ist),

269− lookupCtxt n (idris_implicits ist)) of

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

295+ case (lookupCtxtExact n (idris_statics ist),

296+ lookupCtxtExact n (idris_implicits ist)) of

297+ (Just statics, Just imps) ->

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

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

273300 args -> [(n, args)]

src/Idris/Transforms.hs+4−1

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

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

4848 case rules of

4949 [] -> 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')

5154 Just tm' -> tm'

5255 _ -> App (applyAll extra ts f)

5356 (applyAll extra ts a)