git.iko.soy/Idris-dev
on master help sign in
Inline type class applications where possible to reduce overhead
10ea548Edwin Brady
src/Core/CaseTree.hs+1−1
compare with master
unifiedsplit
@@ -31,7 +31,7 @@ type CS = Int
31
31
32-- simple terms can be inlined trivially - good for primitives in particular
32-- simple terms can be inlined trivially - good for primitives in particular
33small :: SC -> Bool
33small :: SC -> Bool
34−small (STerm t) = True
34+-- small (STerm t) = True
35small _ = False
35small _ = False
36
36
37simpleCase :: Bool -> [(Term, Term)] -> CaseDef
37simpleCase :: Bool -> [(Term, Term)] -> CaseDef
src/Core/Evaluate.hs+56−54
@@ -109,105 +109,107 @@ unbindEnv (_:bs) (Bind n b sc) = unbindEnv bs sc
109-- such as we might have during construction of a proof)
109-- such as we might have during construction of a proof)
110
110
111eval :: Context -> Ctxt [Bool] -> Env -> TT Name -> [EvalOpt] -> Eval Value
111eval :: Context -> Ctxt [Bool] -> Env -> TT Name -> [EvalOpt] -> Eval Value
112−eval ctxt statics genv tm opts = ev True [] tm where
112+eval ctxt statics genv tm opts = ev [] True [] tm where
113 spec = Spec `elem` opts
113 spec = Spec `elem` opts
114 simpl = Simplify `elem` opts
114 simpl = Simplify `elem` opts
115 atRepl = AtREPL `elem` opts
115 atRepl = AtREPL `elem` opts
116
116
117− ev top env (P _ n ty)
117+ ev stk top env (P _ n ty)
118− | Just (Let t v) <- lookup n genv = ev top env v
118+ | Just (Let t v) <- lookup n genv = ev stk top env v
119− ev top env (P Ref n ty) = case lookupDefAcc Nothing n atRepl ctxt of
119+ ev stk top env (P Ref n ty) = case lookupDefAcc Nothing n atRepl ctxt of
120− [(Function _ tm, Public)] -> ev True env tm
120+ [(Function _ tm, Public)] ->
121+ ev (n:stk) True env tm
121− [(TyDecl nt ty, _)] -> do vty <- ev True env ty
122+ [(TyDecl nt ty, _)] -> do vty <- ev stk True env ty
122 return $ VP nt n vty
123 return $ VP nt n vty
123 [(CaseOp inl _ _ [] tree _ _, Public)] -> -- unoptimised version
124 [(CaseOp inl _ _ [] tree _ _, Public)] -> -- unoptimised version
124− if simpl && (not inl)
125+ if simpl && (not inl || elem n stk)
125− then liftM (VP Ref n) (ev top env ty)
126+ then liftM (VP Ref n) (ev stk top env ty)
126− else do c <- evCase top env [] [] tree
127+ else do c <- evCase (n:stk) top env [] [] tree
127 case c of
128 case c of
128− (Nothing, _) -> liftM (VP Ref n) (ev top env ty)
129+ (Nothing, _) -> liftM (VP Ref n) (ev stk top env ty)
129 (Just v, _) -> return v
130 (Just v, _) -> return v
130− _ -> liftM (VP Ref n) (ev top env ty)
131+ _ -> liftM (VP Ref n) (ev stk top env ty)
131− ev top env (P nt n ty) = liftM (VP nt n) (ev top env ty)
132+ ev stk top env (P nt n ty) = liftM (VP nt n) (ev stk top env ty)
132− ev top env (V i) | i < length env = return $ env !! i
133+ ev stk top env (V i) | i < length env = return $ env !! i
133 | otherwise = return $ VV i
134 | otherwise = return $ VV i
134− ev top env (Bind n (Let t v) sc)
135+ ev stk top env (Bind n (Let t v) sc)
135− = do v' <- ev top env v --(finalise v)
136+ = do v' <- ev stk top env v --(finalise v)
136− sc' <- ev top (v' : env) sc
137+ sc' <- ev stk top (v' : env) sc
137 wknV (-1) sc'
138 wknV (-1) sc'
138− ev top env (Bind n (NLet t v) sc)
139+ ev stk top env (Bind n (NLet t v) sc)
139− = do t' <- ev top env (finalise t)
140+ = do t' <- ev stk top env (finalise t)
140− v' <- ev top env (finalise v)
141+ v' <- ev stk top env (finalise v)
141− sc' <- ev top (v' : env) sc
142+ sc' <- ev stk top (v' : env) sc
142 return $ VBind n (Let t' v') (\x -> return sc')
143 return $ VBind n (Let t' v') (\x -> return sc')
143− ev top env (Bind n b sc)
144+ ev stk top env (Bind n b sc)
144 = do b' <- vbind env b
145 = do b' <- vbind env b
145− return $ VBind n b' (\x -> ev top (x:env) sc)
146+ return $ VBind n b' (\x -> ev stk top (x:env) sc)
146− where vbind env t = fmapMB (\tm -> ev top env (finalise tm)) t
147+ where vbind env t = fmapMB (\tm -> ev stk top env (finalise tm)) t
147− ev top env (App f a) = do f' <- ev top env f
148+ ev stk top env (App f a) = do f' <- ev stk top env f
148− a' <- ev False env a
149+ a' <- ev stk False env a
149− evApply top env [a'] f'
150+ evApply stk top env [a'] f'
150− ev top env (Constant c) = return $ VConstant c
151+ ev stk top env (Constant c) = return $ VConstant c
151− ev top env Erased = return VErased
152+ ev stk top env Erased = return VErased
152− ev top env (Set i) = return $ VSet i
153+ ev stk top env (Set i) = return $ VSet i
153
154
154− evApply top env args (VApp f a) =
155+ evApply stk top env args (VApp f a) =
155− evApply top env (a:args) f
156+ evApply stk top env (a:args) f
156− evApply top env args f = apply top env f args
157+ evApply stk top env args f = apply stk top env f args
157
158
158− apply top env (VBind n (Lam t) sc) (a:as)
159+ apply stk top env (VBind n (Lam t) sc) (a:as)
159 = do a' <- sc a
160 = do a' <- sc a
160− app <- apply top env a' as
161+ app <- apply stk top env a' as
161 wknV (-1) app
162 wknV (-1) app
162− apply False env f args
163+ apply stk False env f args
163 | spec = return $ unload env f args
164 | spec = return $ unload env f args
164− apply top env (VP Ref n ty) args
165+ apply stk top env (VP Ref n ty) args
165 | [(CaseOp inl _ _ ns tree _ _, Public)] <- lookupDefAcc Nothing n atRepl ctxt
166 | [(CaseOp inl _ _ ns tree _ _, Public)] <- lookupDefAcc Nothing n atRepl ctxt
166 = -- traceWhen (n == UN ["interp"]) (show (n, args)) $
167 = -- traceWhen (n == UN ["interp"]) (show (n, args)) $
168+ if simpl && (not inl || elem n stk)
167− if simpl && (not inl) then return $ unload env (VP Ref n ty) args
169+ then return $ unload env (VP Ref n ty) args
168− else do c <- evCase top env ns args tree
170+ else do c <- evCase (n:stk) top env ns args tree
169 case c of
171 case c of
170 (Nothing, _) -> return $ unload env (VP Ref n ty) args
172 (Nothing, _) -> return $ unload env (VP Ref n ty) args
171− (Just v, rest) -> evApply top env rest v
173+ (Just v, rest) -> evApply stk top env rest v
172 | [Operator _ i op] <- lookupDef Nothing n ctxt
174 | [Operator _ i op] <- lookupDef Nothing n ctxt
173 = if (i <= length args)
175 = if (i <= length args)
174 then case op (take i args) of
176 then case op (take i args) of
175 Nothing -> return $ unload env (VP Ref n ty) args
177 Nothing -> return $ unload env (VP Ref n ty) args
176− Just v -> evApply top env (drop i args) v
178+ Just v -> evApply stk top env (drop i args) v
177 else return $ unload env (VP Ref n ty) args
179 else return $ unload env (VP Ref n ty) args
178− apply top env f (a:as) = return $ unload env f (a:as)
180+ apply stk top env f (a:as) = return $ unload env f (a:as)
179− apply top env f [] = return f
181+ apply stk top env f [] = return f
180
182
181 unload env f [] = f
183 unload env f [] = f
182 unload env f (a:as) = unload env (VApp f a) as
184 unload env f (a:as) = unload env (VApp f a) as
183
185
184− evCase top env ns args tree
186+ evCase stk top env ns args tree
185 | length ns <= length args
187 | length ns <= length args
186 = do let args' = take (length ns) args
188 = do let args' = take (length ns) args
187 let rest = drop (length ns) args
189 let rest = drop (length ns) args
188− t <- evTree top env (zipWith (\n t -> (n, t)) ns args') tree
190+ t <- evTree stk top env (zipWith (\n t -> (n, t)) ns args') tree
189 return (t, rest)
191 return (t, rest)
190 | otherwise = return (Nothing, args)
192 | otherwise = return (Nothing, args)
191
193
192− evTree :: Bool -> [Value] -> [(Name, Value)] -> SC -> Eval (Maybe Value)
194+ evTree :: [Name] -> Bool -> [Value] -> [(Name, Value)] -> SC -> Eval (Maybe Value)
193− evTree top env amap (UnmatchedCase str) = return Nothing
195+ evTree stk top env amap (UnmatchedCase str) = return Nothing
194− evTree top env amap (STerm tm)
196+ evTree stk top env amap (STerm tm)
195 = do let etm = pToVs (map fst amap) tm
197 = do let etm = pToVs (map fst amap) tm
196− etm' <- ev top (map snd amap ++ env) etm
198+ etm' <- ev stk top (map snd amap ++ env) etm
197 return $ Just etm'
199 return $ Just etm'
198− evTree top env amap (Case n alts)
200+ evTree stk top env amap (Case n alts)
199 = case lookup n amap of
201 = case lookup n amap of
200 Just v -> do c <- chooseAlt env v (getValArgs v) alts amap
202 Just v -> do c <- chooseAlt env v (getValArgs v) alts amap
201 case c of
203 case c of
202− Just (altmap, sc) -> evTree top env altmap sc
204+ Just (altmap, sc) -> evTree stk top env altmap sc
203− _ -> do c' <- chooseAlt' env v (getValArgs v) alts amap
205+ _ -> do c' <- chooseAlt' stk env v (getValArgs v) alts amap
204 case c' of
206 case c' of
205− Just (altmap, sc) -> evTree top env altmap sc
207+ Just (altmap, sc) -> evTree stk top env altmap sc
206 _ -> return Nothing
208 _ -> return Nothing
207 _ -> return Nothing
209 _ -> return Nothing
208
210
209− chooseAlt' env _ (f, args) alts amap
211+ chooseAlt' stk env _ (f, args) alts amap
210− = do f' <- apply True env f args
212+ = do f' <- apply stk True env f args
211 chooseAlt env f' (getValArgs f') alts amap
213 chooseAlt env f' (getValArgs f') alts amap
212
214
213 chooseAlt :: [Value] -> Value -> (Value, [Value]) -> [CaseAlt] -> [(Name, Value)] ->
215 chooseAlt :: [Value] -> Value -> (Value, [Value]) -> [CaseAlt] -> [(Name, Value)] ->
src/Idris/ElabDecls.hs+3−1
@@ -106,7 +106,7 @@ elabClauses info fc opts n_in cs_in = let n = liftname info n_in in
106 show r) pats))
106 show r) pats))
107 ist <- get
107 ist <- get
108 let tcase = opt_typecase (idris_options ist)
108 let tcase = opt_typecase (idris_options ist)
109− let pdef = map debind pats
109+ let pdef = map debind (map (simpl (tt_ctxt ist)) pats)
110 pdef' <- applyOpts pdef
110 pdef' <- applyOpts pdef
111 let tree = simpleCase tcase pdef
111 let tree = simpleCase tcase pdef
112 let tree' = simpleCase tcase pdef'
112 let tree' = simpleCase tcase pdef'
@@ -126,6 +126,8 @@ elabClauses info fc opts n_in cs_in = let n = liftname info n_in in
126 depat (Bind n (PVar t) sc) = depat (instantiate (P Bound n t) sc)
126 depat (Bind n (PVar t) sc) = depat (instantiate (P Bound n t) sc)
127 depat x = x
127 depat x = x
128
128
129+ simpl ctxt (x, y) = (x, simplify ctxt [] y)
130+
129 sameLength ((x, _) : xs)
131 sameLength ((x, _) : xs)
130 = do l <- sameLength xs
132 = do l <- sameLength xs
131 let (f, as) = unApply x
133 let (f, as) = unApply x