bb76c6c · Idris-dev · git.iko.soy

idris.cabal+2−1

@@ -73,7 +73,8 @@ Executable idris

7373 Pkg.Package, Pkg.PParser,

7474

7575 IRTS.Lang, IRTS.LParser, IRTS.Bytecode, IRTS.Simplified,

76− IRTS.CodegenC, IRTS.Defunctionalise, IRTS.Compiler,

76+ IRTS.CodegenC, IRTS.Defunctionalise, IRTS.Inliner,

77+ IRTS.Compiler,

7778

7879 Paths_idris

7980

src/Core/CaseTree.hs+21−6

@@ -31,10 +31,19 @@ type CaseTree = SC

3131type Clause = ([Pat], (Term, Term))

3232type CS = ([Term], Int)

3333

34+instance TermSize SC where

35+ termsize (Case n as) = termsize as

36+ termsize (STerm t) = termsize t

37+ termsize _ = 1

38+

39+instance TermSize CaseAlt where

40+ termsize (ConCase _ _ _ s) = termsize s

41+ termsize (ConstCase _ s) = termsize s

42+ termsize (DefaultCase s) = termsize s

43+

3444-- simple terms can be inlined trivially - good for primitives in particular

3545small :: SC -> Bool

36−-- small (STerm t) = True

37−small _ = False

46+small t = termsize t < 150

3847

3948namesUsed :: SC -> [Name]

4049namesUsed sc = nub $ nu' [] sc where

@@ -121,6 +130,7 @@ toPat tc tms = evalState (mapM (\x -> toPat' x []) tms) []

121130

122131data Partition = Cons [Clause]

123132 | Vars [Clause]

133+ deriving Show

124134

125135isVarPat (PV _ : ps , _) = True

126136isVarPat (PAny : ps , _) = True

@@ -145,7 +155,8 @@ match [] (([], ret) : xs) err

145155 = do (ts, v) <- get

146156 put (ts ++ (map (fst.snd) xs), v)

147157 return $ STerm (snd ret) -- run out of arguments

148−match vs cs err = do cs <- mixture vs (partition cs) err

158+match vs cs err = do let ps = partition cs

159+ cs <- mixture vs ps err

149160 return cs

150161

151162mixture :: [Name] -> [Partition] -> SC -> State CS SC

@@ -188,19 +199,23 @@ caseGroups (v:vs) gs err = do g <- altGroups gs

188199

189200argsToAlt :: [([Pat], Clause)] -> State CS ([Name], [Clause])

190201argsToAlt [] = return ([], [])

191−argsToAlt rs@((r, m) : _)

202+argsToAlt rs@((r, m) : rest)

192203 = do newArgs <- getNewVars r

193204 return (newArgs, addRs rs)

194205 where

195206 getNewVars [] = return []

196− getNewVars ((PV n) : ns) = do nsv <- getNewVars ns

197− return (n : nsv)

207+ getNewVars ((PV n) : ns) = do v <- getVar

208+ nsv <- getNewVars ns

209+ return (v : nsv)

198210 getNewVars (_ : ns) = do v <- getVar

199211 nsv <- getNewVars ns

200212 return (v : nsv)

201213 addRs [] = []

202214 addRs ((r, (ps, res)) : rs) = ((r++ps, res) : addRs rs)

203215

216+ uniq i (UN n) = MN i n

217+ uniq i n = n

218+

204219getVar :: State CS Name

205220getVar = do (t, v) <- get; put (t, v+1); return (MN v "e")

206221

src/Core/Evaluate.hs+19−14

@@ -109,7 +109,7 @@ specialise ctxt env limits t

109109

110110simplify :: Context -> Env -> TT Name -> TT Name

111111simplify ctxt env t

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

112+ = evalState (do val <- eval False ctxt threshold [(UN "lazy", 0)]

113113 (map finalEntry env) (finalise t) [Simplify]

114114 quote 0 val) initEval

115115

@@ -133,12 +133,13 @@ unbindEnv :: EnvTT n -> TT n -> TT n

133133unbindEnv [] tm = tm

134134unbindEnv (_:bs) (Bind n b sc) = unbindEnv bs sc

135135

136−usable :: Name -> [(Name, Int)] -> (Bool, [(Name, Int)])

137−usable n [] = (True, [])

138−usable n ns = case lookup n ns of

139− Just 0 -> (False, ns)

140− Just i -> (True, (n, abs (i-1)) : filter (\ (n', _) -> n/=n') ns)

141− _ -> (True, (n, 100) : filter (\ (n', _) -> n/=n') ns)

136+usable :: Bool -> Name -> [(Name, Int)] -> (Bool, [(Name, Int)])

137+usable s n [] = (True, [])

138+usable s n ns = case lookup n ns of

139+ Just 0 -> (False, ns)

140+ Just i -> (True, (n, abs (i-1)) : filter (\ (n', _) -> n/=n') ns)

141+ _ -> if s then (True, (n, 0) : filter (\ (n', _) -> n/=n') ns)

142+ else (True, (n, 100) : filter (\ (n', _) -> n/=n') ns)

142143

143144reduction :: Eval ()

144145reduction = do ES ns s <- get

@@ -158,7 +159,7 @@ eval traceon ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where

158159 | Just (Let t v) <- lookup n genv = do when (not atRepl) $ step maxred

159160 ev ntimes stk top env v

160161 ev ntimes_in stk top env (P Ref n ty)

161− | (True, ntimes) <- usable n ntimes_in

162+ | (True, ntimes) <- usable simpl n ntimes_in

162163 = do let val = lookupDefAcc Nothing n atRepl ctxt

163164 when (not atRepl) $ step maxred

164165 case val of

@@ -178,10 +179,17 @@ eval traceon ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where

178179 ev ntimes stk top env (V i) | i < length env = return $ env !! i

179180 | otherwise = return $ VV i

180181 ev ntimes stk top env (Bind n (Let t v) sc)

182+ | not simpl || vinstances 0 sc < 2

181183 = do v' <- ev ntimes stk top env v --(finalise v)

182184 when (not atRepl) $ step maxred

183185 sc' <- ev ntimes stk top (v' : env) sc

184186 wknV (-1) sc'

187+ | otherwise

188+ = do t' <- ev ntimes stk top env t

189+ v' <- ev ntimes stk top env v --(finalise v)

190+ when (not atRepl) $ step maxred

191+ sc' <- ev ntimes stk top (v' : env) sc

192+ return $ VBind n (Let t' v') (\x -> return sc')

185193 ev ntimes stk top env (Bind n (NLet t v) sc)

186194 = do t' <- ev ntimes stk top env (finalise t)

187195 v' <- ev ntimes stk top env (finalise v)

@@ -219,7 +227,7 @@ eval traceon ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where

219227-- apply ntimes stk False env f args

220228-- | spec = specApply ntimes stk env f args

221229 apply ntimes_in stk top env f@(VP Ref n ty) args

222− | (True, ntimes) <- usable n ntimes_in

230+ | (True, ntimes) <- usable simpl n ntimes_in

223231 = traceWhen traceon (show stk) $

224232 do let val = lookupDefAcc Nothing n atRepl ctxt

225233 case val of

@@ -683,16 +691,13 @@ addCasedef :: Name -> Bool -> Bool -> Bool ->

683691 Type -> Context -> Context

684692addCasedef n alwaysInline tcase covering ps psrt ty uctxt

685693 = let ctxt = definitions uctxt

686− ps' = ps -- simpl ps in

687− ctxt' = case (simpleCase tcase covering (FC "" 0) ps',

694+ ctxt' = case (simpleCase tcase covering (FC "" 0) ps,

688695 simpleCase tcase covering (FC "" 0) psrt) of

689696 (OK (CaseDef args sc _), OK (CaseDef args' sc' _)) ->

690− let inl = alwaysInline in

697+ let inl = alwaysInline || small sc' in

691698 addDef n (CaseOp inl ty ps args sc args' sc',

692699 Public, Unchecked) ctxt in

693700 uctxt { definitions = ctxt' }

694− where simpl [] = []

695− simpl ((l,r) : xs) = (l, simplify uctxt [] r) : simpl xs

696701

697702addOperator :: Name -> Type -> Int -> ([Value] -> Maybe Value) -> Context -> Context

698703addOperator n ty a op uctxt

src/Core/TT.hs+23

@@ -417,6 +417,20 @@ data TT n = P NameType n (TT n) -- embed type

417417deriving instance Binary TT

418418!-}

419419

420+class TermSize a where

421+ termsize :: a -> Int

422+

423+instance TermSize a => TermSize [a] where

424+ termsize [] = 0

425+ termsize (x : xs) = termsize x + termsize xs

426+

427+instance TermSize (TT a) where

428+ termsize (P _ _ _) = 1

429+ termsize (V _) = 1

430+ termsize (Bind n (Let t v) sc) = termsize v + termsize sc

431+ termsize (App f a) = termsize f + termsize a

432+ termsize _ = 1

433+

420434instance Sized a => Sized (TT a) where

421435 size (P name n trm) = 1 + size name + size n + size trm

422436 size (V v) = 1

@@ -459,6 +473,15 @@ isInjective (Bind _ (Pi _) sc) = True

459473isInjective (App f a) = isInjective f

460474isInjective _ = False

461475

476+-- Count the number of instances of a de Bruijn index in a term

477+vinstances :: Int -> TT n -> Int

478+vinstances i (V x) | i == x = 1

479+vinstances i (App f a) = vinstances i f + vinstances i a

480+vinstances i (Bind x b sc) = instancesB b + vinstances (i + 1) sc

481+ where instancesB (Let t v) = vinstances i v

482+ instancesB _ = 0

483+vinstances i t = 0

484+

462485instantiate :: TT n -> TT n -> TT n

463486instantiate e = subst 0 where

464487 subst i (V x) | i == x = e

src/IRTS/Compiler.hs+24−15

@@ -7,6 +7,7 @@ import IRTS.Defunctionalise

77import IRTS.Simplified

88import IRTS.CodegenC

99import IRTS.CodegenJava

10+import IRTS.Inliner

1011

1112import Idris.AbsSyntax

1213import Core.TT

@@ -36,7 +37,13 @@ compile target f tm

3637 -- iputStrLn $ showSep "\n" (map show defs)

3738 let (nexttag, tagged) = addTags 65536 (liftAll defs)

3839 let ctxtIn = addAlist tagged emptyContext

39− let defuns = defunctionalise nexttag ctxtIn

40+ iLOG "Defunctionalising"

41+ let defuns_in = defunctionalise nexttag ctxtIn

42+ logLvl 5 $ show defuns_in

43+ iLOG "Inlining"

44+ let defuns = inline defuns_in

45+ logLvl 5 $ show defuns

46+

4047 -- iputStrLn $ showSep "\n" (map show (toAlist defuns))

4148 let checked = checkDefs defuns (toAlist defuns)

4249 case checked of

@@ -108,7 +115,7 @@ instance ToIR (TT Name) where

108115 ir tm = ir' [] tm where

109116 ir' env tm@(App f a)

110117 | (P _ (UN "mkForeign") _, args) <- unApply tm

111− = doForeign args

118+ = doForeign env args

112119 | (P _ (UN "unsafePerformIO") _, [_, arg]) <- unApply tm

113120 = ir' env arg

114121 | (P _ (UN "lazy") _, [_, arg]) <- unApply tm

@@ -138,10 +145,12 @@ instance ToIR (TT Name) where

138145 args' <- mapM (ir' env) args

139146 return (LApp False f' args')

140147 ir' env (P _ n _) = return $ LV (Glob n)

141− ir' env (V i) = return $ LV (Glob (env!!i))

148+ ir' env (V i) | i < length env = return $ LV (Glob (env!!i))

149+ | otherwise = error $ "IR fail " ++ show i ++ " " ++ show tm

142150 ir' env (Bind n (Lam _) sc)

143− = do sc' <- ir' (n : env) sc

144− return $ LLam [n] sc'

151+ = do let n' = uniqueName n env

152+ sc' <- ir' (n' : env) sc

153+ return $ LLam [n'] sc'

145154 ir' env (Bind n (Let _ v) sc)

146155 = do sc' <- ir' (n : env) sc

147156 v' <- ir' env v

@@ -163,16 +172,16 @@ instance ToIR (TT Name) where

163172 buildApp env e xs = do xs' <- mapM (ir' env) xs

164173 return $ LApp False e xs'

165174

166−doForeign :: [TT Name] -> Idris LExp

167−doForeign (_ : fgn : args)

168− | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn

169− = let tys = getFTypes fgnArgTys

170− rty = mkIty' ret in

171− do args' <- mapM ir args

172− -- wrap it in a prim__IO

173− -- return $ con_ 0 @@ impossible @@

174− return $ LLazyExp $ LForeign LANG_C rty fgnName (zip tys args')

175− | otherwise = fail "Badly formed foreign function call"

175+ doForeign :: [Name] -> [TT Name] -> Idris LExp

176+ doForeign env (_ : fgn : args)

177+ | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn

178+ = let tys = getFTypes fgnArgTys

179+ rty = mkIty' ret in

180+ do args' <- mapM (ir' env) args

181+ -- wrap it in a prim__IO

182+ -- return $ con_ 0 @@ impossible @@

183+ return $ LLazyExp $ LForeign LANG_C rty fgnName (zip tys args')

184+ | otherwise = fail "Badly formed foreign function call"

176185

177186getFTypes :: TT Name -> [FType]

178187getFTypes tm = case unApply tm of

src/IRTS/Defunctionalise.hs+48−3

@@ -1,4 +1,5 @@

1−module IRTS.Defunctionalise where

1+module IRTS.Defunctionalise(module IRTS.Defunctionalise,

2+ module IRTS.Lang) where

23

34import IRTS.Lang

45import Core.TT

@@ -137,7 +138,7 @@ mkApplyCase fname n ar

137138

138139mkEval :: [(Name, Int, EvalApply DAlt)] -> (Name, DDecl)

139140mkEval xs = (MN 0 "EVAL", DFun (MN 0 "EVAL") [MN 0 "arg"]

140− (DCase (DV (Glob (MN 0 "arg")))

141+ (mkBigCase (MN 0 "EVAL") 256 (DV (Glob (MN 0 "arg")))

141142 (mapMaybe evalCase xs ++

142143 [DDefaultCase (DV (Glob (MN 0 "arg")))])))

143144 where

@@ -146,13 +147,15 @@ mkEval xs = (MN 0 "EVAL", DFun (MN 0 "EVAL") [MN 0 "arg"]

146147

147148mkApply :: [(Name, Int, EvalApply DAlt)] -> (Name, DDecl)

148149mkApply xs = (MN 0 "APPLY", DFun (MN 0 "APPLY") [MN 0 "fn", MN 0 "arg"]

149− (DCase (DApp False (MN 0 "EVAL")

150+ (mkBigCase (MN 0 "APPLY")

151+ 256 (DApp False (MN 0 "EVAL")

150152 [DV (Glob (MN 0 "fn"))])

151153 (mapMaybe applyCase xs)))

152154 where

153155 applyCase (n, t, ApplyCase x) = Just x

154156 applyCase _ = Nothing

155157

158+

156159declare :: Int -> [(Name, Int, EvalApply DAlt)] -> [(Name, DDecl)]

157160declare t xs = dec' t xs [] where

158161 dec' t [] acc = reverse acc

@@ -189,3 +192,45 @@ instance Show DExp where

189192 ++ show' env e

190193 showAlt env (DConstCase c e) = show c ++ " => " ++ show' env e

191194 showAlt env (DDefaultCase e) = "_ => " ++ show' env e

195+

196+-- Divide up a large case expression so that each has a maximum of

197+-- 'max' branches

198+

199+mkBigCase cn max arg branches

200+ | length branches <= max = DCase arg branches

201+ | otherwise = -- DCase arg branches -- until I think of something...

202+ -- divide the branches into groups of at most max (by tag),

203+ -- generate a new case and shrink, recursively

204+ let bs = sortBy tagOrd branches

205+ (all, def) = case (last bs) of

206+ DDefaultCase t -> (init all, Just (DDefaultCase t))

207+ _ -> (all, Nothing)

208+ bss = groupsOf max all

209+ cs = map mkCase bss in

210+ DCase arg branches

211+

212+ where mkCase bs = DCase arg bs

213+

214+ tagOrd (DConCase t _ _ _) (DConCase t' _ _ _) = compare t t'

215+ tagOrd (DConstCase c _) (DConstCase c' _) = compare c c'

216+ tagOrd (DDefaultCase _) (DDefaultCase _) = EQ

217+ tagOrd (DConCase _ _ _ _) (DDefaultCase _) = LT

218+ tagOrd (DConCase _ _ _ _) (DConstCase _ _) = LT

219+ tagOrd (DConstCase _ _) (DDefaultCase _) = LT

220+ tagOrd (DDefaultCase _) (DConCase _ _ _ _) = GT

221+ tagOrd (DConstCase _ _) (DConCase _ _ _ _) = GT

222+ tagOrd (DDefaultCase _) (DConstCase _ _) = GT

223+

224+

225+groupsOf :: Int -> [DAlt] -> [[DAlt]]

226+groupsOf x [] = []

227+groupsOf x xs = let (batch, rest) = span (tagLT (x + tagHead xs)) xs in

228+ batch : groupsOf x rest

229+ where tagHead (DConstCase (I i) _ : _) = i

230+ tagHead (DConCase t _ _ _ : _) = t

231+ tagHead (DDefaultCase _ : _) = -1 -- must be the end

232+

233+ tagLT i (DConstCase (I j) _) = i < j

234+ tagLT i (DConCase j _ _ _) = i < j

235+ tagLT i (DDefaultCase _) = False

236+

src/IRTS/Inliner.hsnew file+9

@@ -0,0 +1,9 @@

1+module IRTS.Inliner where

2+

3+import Core.TT

4+

5+import IRTS.Defunctionalise

6+

7+inline :: DDefs -> DDefs

8+inline xs = xs

9+

src/IRTS/Lang.hs+1−1

@@ -52,7 +52,7 @@ data LAlt = LConCase Int Name [Name] LExp

5252 | LDefaultCase LExp

5353 deriving (Show, Eq)

5454

55−data LDecl = LFun Name [Name] LExp -- name, arg names, definition

55+data LDecl = LFun Name [Name] LExp -- name, arg names, definition, inlinable

5656 | LConstructor Name Int Int -- constructor name, tag, arity

5757 deriving (Show, Eq)

5858

src/IRTS/Simplified.hs−1

@@ -1,6 +1,5 @@

11module IRTS.Simplified where

22

3−import IRTS.Lang

43import IRTS.Defunctionalise

54import Core.TT

65import Data.Maybe

src/Idris/REPL.hs+1−1

@@ -226,7 +226,7 @@ process fn (Search t) = iputStrLn "Not implemented"

226226process fn (Spec t) = do (tm, ty) <- elabVal toplevel False t

227227 ctxt <- getContext

228228 ist <- get

229− let tm' = specialise ctxt [] [] {- (idris_statics ist) -} tm

229+ let tm' = simplify ctxt [] {- (idris_statics ist) -} tm

230230 iputStrLn (show (delab ist tm'))

231231

232232process fn (RmProof n')