git.iko.soy/Idris-dev
on master help sign in
Remove unused code in Evaluator
dd12ac4Edwin Brady
src/Core/Evaluate.hs+56−206
compare with master
unifiedsplit
@@ -42,22 +42,14 @@ data Value = VP NameType Name Value
42 | VBind Bool Name (Binder Value) (Value -> Eval Value)
42 | VBind Bool Name (Binder Value) (Value -> Eval Value)
43 -- For frozen let bindings when simplifying
43 -- For frozen let bindings when simplifying
44 | VBLet Int Name Value Value Value
44 | VBLet Int Name Value Value Value
45− | VApp Value Value
45+ | VApp Value (Value, -- inarg
46+ Value) -- not inarg
46 | VType UExp
47 | VType UExp
47 | VErased
48 | VErased
48 | VConstant Const
49 | VConstant Const
49-- | VLazy Env [Value] Term
50-- | VLazy Env [Value] Term
50 | VTmp Int
51 | VTmp Int
51
52
52−data HNF = HP NameType Name (TT Name)
53− | HV Int
54− | HBind Name (Binder HNF) (HNF -> Eval HNF)
55− | HApp HNF [HNF] [TT Name]
56− | HType UExp
57− | HConstant Const
58− | HTmp Int
59− deriving Show
60−
61instance Show Value where
53instance Show Value where
62 show x = show $ evalState (quote 100 x) initEval
54 show x = show $ evalState (quote 100 x) initEval
63
55
@@ -169,19 +161,22 @@ eval :: Bool -> Context -> [(Name, Int)] -> Env -> TT Name ->
169 [EvalOpt] -> Eval Value
161 [EvalOpt] -> Eval Value
170eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
162eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
171 spec = Spec `elem` opts
163 spec = Spec `elem` opts
172− simpl = Simplify True `elem` opts
164+ simpl = Simplify True `elem` opts
173 atRepl = AtREPL `elem` opts
165 atRepl = AtREPL `elem` opts
174 hnf = HNF `elem` opts
166 hnf = HNF `elem` opts
175
167
176 -- returns 'True' if the function should block
168 -- returns 'True' if the function should block
177 -- normal evaluation should return false
169 -- normal evaluation should return false
178− blockSimplify (CaseInfo inl dict) n stk
170+ blockSimplify (CaseInfo inl dict) inarg n stk
179 = (Simplify False `elem` opts && (not (inl || dict) || elem n stk))
171 = (Simplify False `elem` opts && (not (inl || dict) || elem n stk))
180− || (Simplify True `elem` opts && (not inl || elem n stk))
172+ || (Simplify True `elem` opts &&
173+ (not (inl || (dict && False)) || elem n stk))
174+
175+ ev = ev' False
181
176
182− ev ntimes stk top env (P _ n ty)
177+ ev' inarg ntimes stk top env (P _ n ty)
183 | Just (Let t v) <- lookup n genv = ev ntimes stk top env v
178 | Just (Let t v) <- lookup n genv = ev ntimes stk top env v
184− ev ntimes_in stk top env (P Ref n ty)
179+ ev' inarg ntimes_in stk top env (P Ref n ty)
185 | not top && hnf = liftM (VP Ref n) (ev ntimes stk top env ty)
180 | not top && hnf = liftM (VP Ref n) (ev ntimes stk top env ty)
186 | otherwise
181 | otherwise
187 = do (u, ntimes) <- usable simpl spec n ntimes_in
182 = do (u, ntimes) <- usable simpl spec n ntimes_in
@@ -194,7 +189,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
194 return $ VP nt n vty
189 return $ VP nt n vty
195 [(CaseOp ci _ _ _ [] tree _ _, acc)]
190 [(CaseOp ci _ _ _ [] tree _ _, acc)]
196 | acc == Public || simpl -> -- unoptimised version
191 | acc == Public || simpl -> -- unoptimised version
197− if blockSimplify ci n stk
192+ if blockSimplify ci inarg n stk
198 then liftM (VP Ref n) (ev ntimes stk top env ty)
193 then liftM (VP Ref n) (ev ntimes stk top env ty)
199 else do c <- evCase ntimes n (n:stk) top env [] [] tree
194 else do c <- evCase ntimes n (n:stk) top env [] [] tree
200 case c of
195 case c of
@@ -202,12 +197,12 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
202 (Just v, _) -> return v
197 (Just v, _) -> return v
203 _ -> liftM (VP Ref n) (ev ntimes stk top env ty)
198 _ -> liftM (VP Ref n) (ev ntimes stk top env ty)
204 else liftM (VP Ref n) (ev ntimes stk top env ty)
199 else liftM (VP Ref n) (ev ntimes stk top env ty)
205− ev ntimes stk top env (P nt n ty)
200+ ev' inarg ntimes stk top env (P nt n ty)
206 = liftM (VP nt n) (ev ntimes stk top env ty)
201 = liftM (VP nt n) (ev ntimes stk top env ty)
207− ev ntimes stk top env (V i)
202+ ev' inarg ntimes stk top env (V i)
208 | i < length env && i >= 0 = return $ env !! i
203 | i < length env && i >= 0 = return $ env !! i
209 | otherwise = return $ VV i
204 | otherwise = return $ VV i
210− ev ntimes stk top env (Bind n (Let t v) sc)
205+ ev' inarg ntimes stk top env (Bind n (Let t v) sc)
211 | not simpl -- - || vinstances 0 sc < 2
206 | not simpl -- - || vinstances 0 sc < 2
212 = do v' <- ev ntimes stk top env v --(finalise v)
207 = do v' <- ev ntimes stk top env v --(finalise v)
213 sc' <- ev ntimes stk top (v' : env) sc
208 sc' <- ev ntimes stk top (v' : env) sc
@@ -222,12 +217,12 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
222 put (hs { nexthole = vd + 1 })
217 put (hs { nexthole = vd + 1 })
223 sc' <- ev ntimes stk top (VP Bound (MN vd "vlet") VErased : env) sc
218 sc' <- ev ntimes stk top (VP Bound (MN vd "vlet") VErased : env) sc
224 return $ VBLet vd n t' v' sc'
219 return $ VBLet vd n t' v' sc'
225− ev ntimes stk top env (Bind n (NLet t v) sc)
220+ ev' inarg ntimes stk top env (Bind n (NLet t v) sc)
226 = do t' <- ev ntimes stk top env (finalise t)
221 = do t' <- ev ntimes stk top env (finalise t)
227 v' <- ev ntimes stk top env (finalise v)
222 v' <- ev ntimes stk top env (finalise v)
228 sc' <- ev ntimes stk top (v' : env) sc
223 sc' <- ev ntimes stk top (v' : env) sc
229 return $ VBind True n (Let t' v') (\x -> return sc')
224 return $ VBind True n (Let t' v') (\x -> return sc')
230− ev ntimes stk top env (Bind n b sc)
225+ ev' inarg ntimes stk top env (Bind n b sc)
231 = do b' <- vbind env b
226 = do b' <- vbind env b
232 return $ VBind (not simpl || vinstances 0 sc < 2)
227 return $ VBind (not simpl || vinstances 0 sc < 2)
233 n b' (\x -> ev ntimes stk False (x:env) sc)
228 n b' (\x -> ev ntimes stk False (x:env) sc)
@@ -237,28 +232,25 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
237 stk top env (finalise tm)) t
232 stk top env (finalise tm)) t
238 | otherwise
233 | otherwise
239 = fmapMB (\tm -> ev ntimes stk top env (finalise tm)) t
234 = fmapMB (\tm -> ev ntimes stk top env (finalise tm)) t
240−-- ev ntimes stk top env (App (App (P _ laz _) _) a)
241−-- | laz == UN "lazy"
242−-- = trace (showEnvDbg genv a) $ ev ntimes stk top env a
243− ev ntimes stk top env (App f a)
235+ ev' inarg ntimes stk top env (App f a)
244 = do f' <- ev ntimes stk False env f
236 = do f' <- ev ntimes stk False env f
237+ a' <- ev' False ntimes stk False env a
245− a' <- ev ntimes stk False env a
238+ aArg' <- ev' True ntimes stk False env a
246− evApply ntimes stk top env [a'] f'
239+ evApply inarg ntimes stk top env [(aArg', a')] f'
247− ev ntimes stk top env (Constant c) = return $ VConstant c
240+ ev' inarg ntimes stk top env (Constant c) = return $ VConstant c
248− ev ntimes stk top env Erased = return VErased
241+ ev' inarg ntimes stk top env Erased = return VErased
249− ev ntimes stk top env (TType i) = return $ VType i
242+ ev' inarg ntimes stk top env (TType i) = return $ VType i
250
243
251− evApply ntimes stk top env args (VApp f a) =
244+ evApply inarg ntimes stk top env args (VApp f a)
252− evApply ntimes stk top env (a:args) f
245+ = evApply inarg ntimes stk top env (a:args) f
253− evApply ntimes stk top env args f = apply ntimes stk top env f args
246+ evApply inarg ntimes stk top env args f
247+ = apply inarg ntimes stk top env f args
254
248
255− apply ntimes stk top env (VBind True n (Lam t) sc) (a:as)
249+ apply inarg ntimes stk top env (VBind True n (Lam t) sc) ((_,a):as)
256 = do a' <- sc a
250 = do a' <- sc a
257− app <- apply ntimes stk top env a' as
251+ app <- apply inarg ntimes stk top env a' as
258 wknV (-1) app
252 wknV (-1) app
259−-- apply ntimes stk False env f args
260−-- | spec = specApply ntimes stk env f args
261− apply ntimes_in stk top env f@(VP Ref n ty) args
253+ apply inarg ntimes_in stk top env f@(VP Ref n ty) args
262 | not top && hnf = case args of
254 | not top && hnf = case args of
263 [] -> return f
255 [] -> return f
264 _ -> return $ unload env f args
256 _ -> return $ unload env f args
@@ -269,17 +261,17 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
269 case val of
261 case val of
270 [(CaseOp ci _ _ _ ns tree _ _, acc)]
262 [(CaseOp ci _ _ _ ns tree _ _, acc)]
271 | acc == Public -> -- unoptimised version
263 | acc == Public -> -- unoptimised version
272− if blockSimplify ci n stk
264+ if blockSimplify ci inarg n stk
273 then return $ unload env (VP Ref n ty) args
265 then return $ unload env (VP Ref n ty) args
274 else do c <- evCase ntimes n (n:stk) top env ns args tree
266 else do c <- evCase ntimes n (n:stk) top env ns args tree
275 case c of
267 case c of
276 (Nothing, _) -> return $ unload env (VP Ref n ty) args
268 (Nothing, _) -> return $ unload env (VP Ref n ty) args
277− (Just v, rest) -> evApply ntimes stk top env rest v
269+ (Just v, rest) -> evApply inarg ntimes stk top env rest v
278 [(Operator _ i op, _)] ->
270 [(Operator _ i op, _)] ->
279 if (i <= length args)
271 if (i <= length args)
280− then case op (take i args) of
272+ then case op (map snd (take i args)) of
281 Nothing -> return $ unload env (VP Ref n ty) args
273 Nothing -> return $ unload env (VP Ref n ty) args
282− Just v -> evApply ntimes stk top env (drop i args) v
274+ Just v -> evApply inarg ntimes stk top env (drop i args) v
283 else return $ unload env (VP Ref n ty) args
275 else return $ unload env (VP Ref n ty) args
284 _ -> case args of
276 _ -> case args of
285 [] -> return f
277 [] -> return f
@@ -287,8 +279,8 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
287 else case args of
279 else case args of
288 (a : as) -> return $ unload env f (a:as)
280 (a : as) -> return $ unload env f (a:as)
289 [] -> return f
281 [] -> return f
290− apply ntimes stk top env f (a:as) = return $ unload env f (a:as)
282+ apply inarg ntimes stk top env f (a:as) = return $ unload env f (a:as)
291− apply ntimes stk top env f [] = return f
283+ apply inarg ntimes stk top env f [] = return f
292
284
293-- specApply stk env f@(VP Ref n ty) args
285-- specApply stk env f@(VP Ref n ty) args
294-- = case lookupCtxt n statics of
286-- = case lookupCtxt n statics of
@@ -299,6 +291,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
299-- _ -> return $ unload env f args
291-- _ -> return $ unload env f args
300-- specApply stk env f args = return $ unload env f args
292-- specApply stk env f args = return $ unload env f args
301
293
294+ unload :: [Value] -> Value -> [(Value, Value)] -> Value
302 unload env f [] = f
295 unload env f [] = f
303 unload env f (a:as) = unload env (VApp f a) as
296 unload env f (a:as) = unload env (VApp f a) as
304
297
@@ -307,8 +300,10 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
307 = do let args' = take (length ns) args
300 = do let args' = take (length ns) args
308 let rest = drop (length ns) args
301 let rest = drop (length ns) args
309 when spec $ deduct n -- successful, so deduct usages
302 when spec $ deduct n -- successful, so deduct usages
303+ tInArg <- evTree ntimes stk top env
304+ (zipWith (\n (t, _) -> (n, t)) ns args') tree
310− t <- evTree ntimes stk top env
305+ t<- evTree ntimes stk top env
311− (zipWith (\n t -> (n, t)) ns args') tree
306+ (zipWith (\n (_, t) -> (n, t)) ns args') tree
312 return (t, rest)
307 return (t, rest)
313 | otherwise = return (Nothing, args)
308 | otherwise = return (Nothing, args)
314
309
@@ -322,7 +317,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
322 return $ Just etm'
317 return $ Just etm'
323 evTree ntimes stk top env amap (Case n alts)
318 evTree ntimes stk top env amap (Case n alts)
324 = case lookup n amap of
319 = case lookup n amap of
325− Just v -> do c <- chooseAlt env v (getValArgs v) alts amap
320+ Just v -> do c <- chooseAlt env v (getValInArgs v) alts amap
326 case c of
321 case c of
327 Just (altmap, sc) -> evTree ntimes stk top env altmap sc
322 Just (altmap, sc) -> evTree ntimes stk top env altmap sc
328 _ -> do c' <- chooseAlt' ntimes stk env v (getValArgs v) alts amap
323 _ -> do c' <- chooseAlt' ntimes stk env v (getValArgs v) alts amap
@@ -337,10 +332,12 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
337 conHeaded t = False
332 conHeaded t = False
338
333
339 chooseAlt' ntimes stk env _ (f, args) alts amap
334 chooseAlt' ntimes stk env _ (f, args) alts amap
340− = do f' <- apply ntimes stk True env f args
335+ = do f' <- apply False ntimes stk True env f args
341− chooseAlt env f' (getValArgs f') alts amap
336+ chooseAlt env f' (getValInArgs f')
337+ alts amap
342
338
343− chooseAlt :: [Value] -> Value -> (Value, [Value]) -> [CaseAlt] -> [(Name, Value)] ->
339+ chooseAlt :: [Value] -> Value -> (Value, [Value]) -> [CaseAlt] ->
340+ [(Name, Value)] ->
344 Eval (Maybe ([(Name, Value)], SC))
341 Eval (Maybe ([(Name, Value)], SC))
345 chooseAlt env _ (VP (DCon i a) _ _, args) alts amap
342 chooseAlt env _ (VP (DCon i a) _ _, args) alts amap
346 | Just (ns, sc) <- findTag i alts = return $ Just (updateAmap (zip ns args) amap, sc)
343 | Just (ns, sc) <- findTag i alts = return $ Just (updateAmap (zip ns args) amap, sc)
@@ -394,6 +391,9 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
394 | tag == (fromEnum ity + 1) * 1000 + count = Just v
391 | tag == (fromEnum ity + 1) * 1000 + count = Just v
395 findConst c (_ : xs) = findConst c xs
392 findConst c (_ : xs) = findConst c xs
396
393
394+ getValInArgs tm = case getValArgs tm of
395+ (f, as) -> (f, map snd as)
396+
397 getValArgs tm = getValArgs' tm []
397 getValArgs tm = getValArgs' tm []
398 getValArgs' (VApp f a) as = getValArgs' f (a:as)
398 getValArgs' (VApp f a) as = getValArgs' f (a:as)
399 getValArgs' f as = (f, as)
399 getValArgs' f as = (f, as)
@@ -427,173 +427,23 @@ instance Quote Value where
427 v' <- quote i v
427 v' <- quote i v
428 let sc'' = pToV (MN vd "vlet") (addBinder sc')
428 let sc'' = pToV (MN vd "vlet") (addBinder sc')
429 return (Bind n (Let t' v') sc'')
429 return (Bind n (Let t' v') sc'')
430− quote i (VApp f a) = liftM2 App (quote i f) (quote i a)
430+ quote i (VApp f (_,a)) = liftM2 App (quote i f) (quote i a)
431 quote i (VType u) = return $ TType u
431 quote i (VType u) = return $ TType u
432 quote i VErased = return $ Erased
432 quote i VErased = return $ Erased
433 quote i (VConstant c) = return $ Constant c
433 quote i (VConstant c) = return $ Constant c
434 quote i (VTmp x) = return $ V (i - x - 1)
434 quote i (VTmp x) = return $ V (i - x - 1)
435
435
436−instance Quote HNF where
437− quote i (HP nt n t) = return (P nt n t)
438− quote i (HV x) = return $ V x
439− quote i (HBind n b sc) = do sc' <- sc (HTmp i)
440− b' <- quoteB b
441− liftM (Bind n b') (quote (i+1) sc')
442− where quoteB t = fmapMB (quote i) t
443− quote i (HApp f env as) = do f' <- quote i f
444− as' <- mapM (iEnv env) as
445− return $ mkApp f' as'
446− where iEnv [] a = return a
447− iEnv (x:xs) a = do x' <- quote i x
448− iEnv xs (weakenTm (-1) (instantiate x' a))
449− quote i (HType u) = return $ TType u
450− quote i (HConstant c) = return $ Constant c
451− quote i (HTmp x) = return $ V (i - x - 1)
452−
453wknV :: Int -> Value -> Eval Value
436wknV :: Int -> Value -> Eval Value
454wknV i (VV x) = return $ VV (x + i)
437wknV i (VV x) = return $ VV (x + i)
455wknV i (VBind red n b sc) = do b' <- fmapMB (wknV i) b
438wknV i (VBind red n b sc) = do b' <- fmapMB (wknV i) b
456 return $ VBind red n b' (\x -> do x' <- sc x
439 return $ VBind red n b' (\x -> do x' <- sc x
457 wknV i x')
440 wknV i x')
458−wknV i (VApp f a) = liftM2 VApp (wknV i f) (wknV i a)
441+wknV i (VApp f (a,b)) = do a' <- wknV i a
442+ b' <- wknV i b
443+ f' <- wknV i f
444+ return $ VApp f' (a',b')
459wknV i t = return t
445wknV i t = return t
460
446
461−wknH :: Int -> HNF -> Eval HNF
462−wknH i (HV x) = return $ HV (x + i)
463−wknH i (HBind n b sc) = do b' <- fmapMB (wknH i) b
464− return $ HBind n b' (\x -> do x' <- sc x
465− wknH i x')
466−wknH i (HApp f env as) = liftM3 HApp (wknH i f) (return env)
467− (return as)
468−wknH i t = return t
469−
470−-- HEAD NORMAL FORM ---------------------------------------------------------
471−
472−eval_hnf :: Context -> Ctxt [Bool] -> Env -> TT Name -> Eval HNF
473−eval_hnf ctxt statics genv tm = ev [] tm where
474− ev :: [HNF] -> TT Name -> Eval HNF
475− ev env (P _ n ty)
476− | Just (Let t v) <- lookup n genv = ev env v
477− ev env (P Ref n ty) = case lookupDef n ctxt of
478− [Function _ t] -> ev env t
479− [TyDecl nt ty] -> return $ HP nt n ty
480− [CaseOp _ _ _ _ [] tree _ _] ->
481− do c <- evCase env [] [] tree
482− case c of
483− (Nothing, _, _) -> return $ HP Ref n ty
484− (Just v, _, _) -> return v
485− _ -> return $ HP Ref n ty
486− ev env (P nt n ty) = return $ HP nt n ty
487− ev env (V i) | i < length env = return $ env !! i
488− | otherwise = return $ HV i
489− ev env (Bind n (Let t v) sc)
490− = do v' <- ev env (finalise v)
491− sc' <- ev (v' : env) sc
492− wknH (-1) sc'
493− ev env (Bind n b sc)
494− = do b' <- hbind env b
495− return $ HBind n b' (\x -> ev (x : env) sc)
496− where hbind env t = fmapMB (\tm -> ev env (finalise tm)) t
497− ev env (App f a) = evApply env [a] f
498− ev env (Constant c) = return $ HConstant c
499− ev env (TType i) = return $ HType i
500−
501− evApply env args (App f a) = evApply env (a : args) f
502− evApply env args f = do f' <- ev env f
503− apply env f' args
504−
505− apply env (HBind n (Lam t) sc) (a:as) = do a' <- ev env a
506− sc' <- sc a'
507− app <- apply env sc' as
508− wknH (-1) app
509− apply env (HP Ref n ty) args
510− | [CaseOp _ _ _ _ ns tree _ _] <- lookupDef n ctxt
511− = do c <- evCase env ns args tree
512− case c of
513− (Nothing, _, env') -> return $ unload env' (HP Ref n ty) args
514− (Just v, rest, env') -> do v' <- quote 0 v
515− apply env' v rest
516−-- | Just (Operator _ i op) <- lookupDef n ctxt
517−-- = if (i <= length args)
518−-- then case op (take i args) of
519−-- Nothing -> return $ unload env (HP Ref n ty) args
520−-- Just v -> evApply env (drop i args) v
521−-- else return $ unload env (HP Ref n ty) args
522− apply env f (a:as) = return $ unload env f (a:as)
523− apply env f [] = return f
524−
525− unload env f [] = f
526− unload env f as = HApp f env as
527−
528− evCase env ns args tree
529− | length ns <= length args
530− = do let args' = take (length ns) args
531− let rest = drop (length ns) args
532− (t, env') <- evTree env (zipWith (\n t -> (n, t)) ns args') tree
533− return (t, rest, env')
534− | otherwise = return (Nothing, args, env)
535−
536− evTree :: [HNF] -> [(Name, TT Name)] -> SC -> Eval (Maybe HNF, [HNF])
537− evTree env amap (UnmatchedCase str) = return (Nothing, env)
538− evTree env amap (STerm tm)
539− = do let etm = pToVs (map fst amap) tm
540− amap' <- mapM (ev env) (map snd amap)
541− envw <- mapM (wknH (length amap)) env
542− let env' = amap' ++ envw
543− etm' <- trace (show etm) $ ev env' etm
544− etmq <- quote 0 etm'
545− trace ("Ev: " ++ show (etm, etmq)) $ return $ (Just etm', env')
546− evTree env amap (Case n alts)
547− = case lookup n amap of
548− Just v -> do v' <- ev env v
549− case chooseAlt v' (getValArgs v') alts amap of
550− Just (altmap, sc) -> evTree env altmap sc
551− _ -> return (Nothing, env)
552−
553− chooseAlt :: HNF -> (HNF, [HNF], [TT Name]) ->
554− [CaseAlt] -> [(Name, TT Name)] ->
555− Maybe ([(Name, TT Name)], SC)
556− chooseAlt _ (HP (DCon i a) _ _, env, args) alts amap
557− | Just (ns, sc) <- findTag i alts = Just (updateAmap (zip ns args) amap, sc)
558− | Just v <- findDefault alts = Just (amap, v)
559− chooseAlt _ (HP (TCon i a) _ _, env, args) alts amap
560− | Just (ns, sc) <- findTag i alts = Just (updateAmap (zip ns args) amap, sc)
561− | Just v <- findDefault alts = Just (amap, v)
562− chooseAlt _ (HConstant c, env, []) alts amap
563− | Just v <- findConst c alts = Just (amap, v)
564− | Just v <- findDefault alts = Just (amap, v)
565− chooseAlt _ _ _ _ = Nothing
566−
567− -- Replace old variable names in the map with new matches
568− -- (This is possibly unnecessary since we make unique names and don't
569− -- allow repeated variables...?)
570− updateAmap newm amap
571− = newm ++ filter (\ (x, _) -> not (elem x (map fst newm))) amap
572− findTag i [] = Nothing
573− findTag i (ConCase n j ns sc : xs) | i == j = Just (ns, sc)
574− findTag i (_ : xs) = findTag i xs
575−
576− findDefault [] = Nothing
577− findDefault (DefaultCase sc : xs) = Just sc
578− findDefault (_ : xs) = findDefault xs
579−
580− findConst c [] = Nothing
581− findConst c (ConstCase c' v : xs) | c == c' = Just v
582− findConst (AType (ATInt ITNative)) (ConCase n 1 [] v : xs) = Just v
583− findConst (AType ATFloat) (ConCase n 2 [] v : xs) = Just v
584− findConst (AType (ATInt ITChar)) (ConCase n 3 [] v : xs) = Just v
585− findConst StrType (ConCase n 4 [] v : xs) = Just v
586− findConst PtrType (ConCase n 5 [] v : xs) = Just v
587− findConst (AType (ATInt ITBig)) (ConCase n 6 [] v : xs) = Just v
588− findConst (AType (ATInt (ITFixed ity))) (ConCase n tag [] v : xs)
589− | tag == 7 + fromEnum ity = Just v
590− findConst (AType (ATInt (ITVec ity count))) (ConCase n tag [] v : xs)
591− | tag == (fromEnum ity + 1) * 1000 + count = Just v
592− findConst c (_ : xs) = findConst c xs
593−
594− getValArgs (HApp t env args) = (t, env, args)
595− getValArgs t = (t, [], [])
596−
597convEq' ctxt x y = evalStateT (convEq ctxt x y) (0, [])
447convEq' ctxt x y = evalStateT (convEq ctxt x y) (0, [])
598
448
599convEq :: Context -> TT Name -> TT Name -> StateT UCs TC Bool
449convEq :: Context -> TT Name -> TT Name -> StateT UCs TC Bool
@@ -821,7 +671,7 @@ addCasedef n ci@(CaseInfo alwaysInline tcdict)
821 ctxt' = case (simpleCase tcase covering reflect CompileTime (FC "" 0) ps,
671 ctxt' = case (simpleCase tcase covering reflect CompileTime (FC "" 0) ps,
822 simpleCase tcase covering reflect RunTime (FC "" 0) psrt) of
672 simpleCase tcase covering reflect RunTime (FC "" 0) psrt) of
823 (OK (CaseDef args sc _), OK (CaseDef args' sc' _)) ->
673 (OK (CaseDef args sc _), OK (CaseDef args' sc' _)) ->
824− let inl = alwaysInline || tcdict
674+ let inl = alwaysInline -- || tcdict
825 inlc = (inl || small n args sc') && (not asserted)
675 inlc = (inl || small n args sc') && (not asserted)
826 inlr = inl || small n args sc' in
676 inlr = inl || small n args sc' in
827 addDef n (CaseOp (ci { case_inlinable = inlc })
677 addDef n (CaseOp (ci { case_inlinable = inlc })
src/Idris/ElabDecls.hs+16−4
@@ -253,11 +253,13 @@ elabPrims = do mapM_ (elabDecl EAll toplevel)
253 }
253 }
254
254
255 p_synEq [t,_,x,y]
255 p_synEq [t,_,x,y]
256− | x == y = Just (VApp (VApp vnJust VErased)
256+ | x == y = Just (vApp (vApp vnJust VErased)
257− (VApp (VApp vnRefl t) x))
257+ (vApp (vApp vnRefl t) x))
258− | otherwise = Just (VApp vnNothing VErased)
258+ | otherwise = Just (vApp vnNothing VErased)
259 p_synEq args = Nothing
259 p_synEq args = Nothing
260
260
261+ vApp f a = VApp f (a, a)
262+
261 nMaybe = P (TCon 0 2) (NS (UN "Maybe") ["Maybe", "Prelude"]) Erased
263 nMaybe = P (TCon 0 2) (NS (UN "Maybe") ["Maybe", "Prelude"]) Erased
262 vnJust = VP (DCon 1 2) (NS (UN "Just") ["Maybe", "Prelude"]) VErased
264 vnJust = VP (DCon 1 2) (NS (UN "Just") ["Maybe", "Prelude"]) VErased
263 vnNothing = VP (DCon 0 1) (NS (UN "Nothing") ["Maybe", "Prelude"]) VErased
265 vnNothing = VP (DCon 0 1) (NS (UN "Nothing") ["Maybe", "Prelude"]) VErased
@@ -553,10 +555,17 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
553 -- show l ++ " = " ++
555 -- show l ++ " = " ++
554 -- show r) pats))
556 -- show r) pats))
555 let tcase = opt_typecase (idris_options ist)
557 let tcase = opt_typecase (idris_options ist)
558+
559+ -- pdef is the compile-time pattern definition with basic
560+ -- simplifications applied.
561+ -- This will get further optimised for run-time, and, separately,
562+ -- further inlined to help with totality checking.
556 let pdef = map debind $ map (simpl (tt_ctxt ist)) pats
563 let pdef = map debind $ map (simpl (tt_ctxt ist)) pats
557
564
558 numArgs <- tclift $ sameLength pdef
565 numArgs <- tclift $ sameLength pdef
559
566
567+ -- patterns after collapsing optimisation applied
568+ -- (i.e. check if the function should do nothing at run time)
560 optpats <- if doNothing
569 optpats <- if doNothing
561 then return $ [Right (mkApp (P Bound n Erased)
570 then return $ [Right (mkApp (P Bound n Erased)
562 (take numArgs (repeat Erased)), Erased)]
571 (take numArgs (repeat Erased)), Erased)]
@@ -592,6 +601,8 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
592 let pcover = null pmissing
601 let pcover = null pmissing
593 logLvl 2 $ "Optimising patterns"
602 logLvl 2 $ "Optimising patterns"
594 logLvl 5 $ show optpdef
603 logLvl 5 $ show optpdef
604+
605+ -- pdef' is the version that gets compiled for run-time
595 pdef' <- applyOpts optpdef
606 pdef' <- applyOpts optpdef
596 logLvl 2 $ "Optimised patterns"
607 logLvl 2 $ "Optimised patterns"
597 logLvl 5 $ show pdef'
608 logLvl 5 $ show pdef'
@@ -672,7 +683,8 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
672
683
673 getLHS (_, l, _) = l
684 getLHS (_, l, _) = l
674
685
675− simpl ctxt (Right (x, y)) = Right (normalise ctxt [] x, y)
686+ simpl ctxt (Right (x, y)) = Right (normalise ctxt [] x, y)
687+-- Core.Evaluate.simplify ctxt True [] y)
676 simpl ctxt t = t
688 simpl ctxt t = t
677
689
678 specNames [] = Nothing
690 specNames [] = Nothing