@@ -42,22 +42,14 @@ data Value = VP NameType Name Value
4242 | VBind Bool Name (Binder Value) (Value -> Eval Value)
4343 -- For frozen let bindings when simplifying
4444 | VBLet Int Name Value Value Value
45− | VApp Value Value
45+ | VApp Value (Value, -- inarg
46+ Value) -- not inarg
4647 | VType UExp
4748 | VErased
4849 | VConstant Const
4950-- | VLazy Env [Value] Term
5051 | VTmp Int
5152
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−
6153instance Show Value where
6254 show x = show $ evalState (quote 100 x) initEval
6355
@@ -169,19 +161,22 @@ eval :: Bool -> Context -> [(Name, Int)] -> Env -> TT Name ->
169161 [EvalOpt] -> Eval Value
170162eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
171163 spec = Spec `elem` opts
172− simpl = Simplify True `elem` opts
164+ simpl = Simplify True `elem` opts
173165 atRepl = AtREPL `elem` opts
174166 hnf = HNF `elem` opts
175167
176168 -- returns 'True' if the function should block
177169 -- normal evaluation should return false
178− blockSimplify (CaseInfo inl dict) n stk
170+ blockSimplify (CaseInfo inl dict) inarg n stk
179171 = (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
181176
182− ev ntimes stk top env (P _ n ty)
177+ ev' inarg ntimes stk top env (P _ n ty)
183178 | 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)
185180 | not top && hnf = liftM (VP Ref n) (ev ntimes stk top env ty)
186181 | otherwise
187182 = 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
194189 return $ VP nt n vty
195190 [(CaseOp ci _ _ _ [] tree _ _, acc)]
196191 | acc == Public || simpl -> -- unoptimised version
197− if blockSimplify ci n stk
192+ if blockSimplify ci inarg n stk
198193 then liftM (VP Ref n) (ev ntimes stk top env ty)
199194 else do c <- evCase ntimes n (n:stk) top env [] [] tree
200195 case c of
@@ -202,12 +197,12 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
202197 (Just v, _) -> return v
203198 _ -> liftM (VP Ref n) (ev ntimes stk top env ty)
204199 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)
206201 = 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)
208203 | i < length env && i >= 0 = return $ env !! i
209204 | 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)
211206 | not simpl -- - || vinstances 0 sc < 2
212207 = do v' <- ev ntimes stk top env v --(finalise v)
213208 sc' <- ev ntimes stk top (v' : env) sc
@@ -222,12 +217,12 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
222217 put (hs { nexthole = vd + 1 })
223218 sc' <- ev ntimes stk top (VP Bound (MN vd "vlet") VErased : env) sc
224219 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)
226221 = do t' <- ev ntimes stk top env (finalise t)
227222 v' <- ev ntimes stk top env (finalise v)
228223 sc' <- ev ntimes stk top (v' : env) sc
229224 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)
231226 = do b' <- vbind env b
232227 return $ VBind (not simpl || vinstances 0 sc < 2)
233228 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
237232 stk top env (finalise tm)) t
238233 | otherwise
239234 = 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)
244236 = do f' <- ev ntimes stk False env f
245− a' <- ev ntimes stk False env a
246− evApply ntimes stk top env [a'] f'
247− ev ntimes stk top env (Constant c) = return $ VConstant c
248− ev ntimes stk top env Erased = return VErased
249− ev ntimes stk top env (TType i) = return $ VType i
237+ a' <- ev' False ntimes stk False env a
238+ aArg' <- ev' True ntimes stk False env a
239+ evApply inarg ntimes stk top env [(aArg', a')] f'
240+ ev' inarg ntimes stk top env (Constant c) = return $ VConstant c
241+ ev' inarg ntimes stk top env Erased = return VErased
242+ ev' inarg ntimes stk top env (TType i) = return $ VType i
250243
251− evApply ntimes stk top env args (VApp f a) =
252− evApply ntimes stk top env (a:args) f
253− evApply ntimes stk top env args f = apply ntimes stk top env f args
244+ evApply inarg ntimes stk top env args (VApp f a)
245+ = evApply inarg ntimes stk top env (a:args) f
246+ evApply inarg ntimes stk top env args f
247+ = apply inarg ntimes stk top env f args
254248
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)
256250 = do a' <- sc a
257− app <- apply ntimes stk top env a' as
251+ app <- apply inarg ntimes stk top env a' as
258252 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
262254 | not top && hnf = case args of
263255 [] -> return f
264256 _ -> return $ unload env f args
@@ -269,17 +261,17 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
269261 case val of
270262 [(CaseOp ci _ _ _ ns tree _ _, acc)]
271263 | acc == Public -> -- unoptimised version
272− if blockSimplify ci n stk
264+ if blockSimplify ci inarg n stk
273265 then return $ unload env (VP Ref n ty) args
274266 else do c <- evCase ntimes n (n:stk) top env ns args tree
275267 case c of
276268 (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
278270 [(Operator _ i op, _)] ->
279271 if (i <= length args)
280− then case op (take i args) of
272+ then case op (map snd (take i args)) of
281273 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
283275 else return $ unload env (VP Ref n ty) args
284276 _ -> case args of
285277 [] -> return f
@@ -287,8 +279,8 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
287279 else case args of
288280 (a : as) -> return $ unload env f (a:as)
289281 [] -> return f
290− apply ntimes stk top env f (a:as) = return $ unload env f (a:as)
291− apply ntimes stk top env f [] = return f
282+ apply inarg ntimes stk top env f (a:as) = return $ unload env f (a:as)
283+ apply inarg ntimes stk top env f [] = return f
292284
293285-- specApply stk env f@(VP Ref n ty) args
294286-- = case lookupCtxt n statics of
@@ -299,6 +291,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
299291-- _ -> return $ unload env f args
300292-- specApply stk env f args = return $ unload env f args
301293
294+ unload :: [Value] -> Value -> [(Value, Value)] -> Value
302295 unload env f [] = f
303296 unload env f (a:as) = unload env (VApp f a) as
304297
@@ -307,8 +300,10 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
307300 = do let args' = take (length ns) args
308301 let rest = drop (length ns) args
309302 when spec $ deduct n -- successful, so deduct usages
310− t <- evTree ntimes stk top env
311− (zipWith (\n t -> (n, t)) ns args') tree
303+ tInArg <- evTree ntimes stk top env
304+ (zipWith (\n (t, _) -> (n, t)) ns args') tree
305+ t<- evTree ntimes stk top env
306+ (zipWith (\n (_, t) -> (n, t)) ns args') tree
312307 return (t, rest)
313308 | otherwise = return (Nothing, args)
314309
@@ -322,7 +317,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
322317 return $ Just etm'
323318 evTree ntimes stk top env amap (Case n alts)
324319 = 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
326321 case c of
327322 Just (altmap, sc) -> evTree ntimes stk top env altmap sc
328323 _ -> 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
337332 conHeaded t = False
338333
339334 chooseAlt' ntimes stk env _ (f, args) alts amap
340− = do f' <- apply ntimes stk True env f args
341− chooseAlt env f' (getValArgs f') alts amap
335+ = do f' <- apply False ntimes stk True env f args
336+ chooseAlt env f' (getValInArgs f')
337+ alts amap
342338
343− chooseAlt :: [Value] -> Value -> (Value, [Value]) -> [CaseAlt] -> [(Name, Value)] ->
339+ chooseAlt :: [Value] -> Value -> (Value, [Value]) -> [CaseAlt] ->
340+ [(Name, Value)] ->
344341 Eval (Maybe ([(Name, Value)], SC))
345342 chooseAlt env _ (VP (DCon i a) _ _, args) alts amap
346343 | 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
394391 | tag == (fromEnum ity + 1) * 1000 + count = Just v
395392 findConst c (_ : xs) = findConst c xs
396393
394+ getValInArgs tm = case getValArgs tm of
395+ (f, as) -> (f, map snd as)
396+
397397 getValArgs tm = getValArgs' tm []
398398 getValArgs' (VApp f a) as = getValArgs' f (a:as)
399399 getValArgs' f as = (f, as)
@@ -427,173 +427,23 @@ instance Quote Value where
427427 v' <- quote i v
428428 let sc'' = pToV (MN vd "vlet") (addBinder sc')
429429 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)
431431 quote i (VType u) = return $ TType u
432432 quote i VErased = return $ Erased
433433 quote i (VConstant c) = return $ Constant c
434434 quote i (VTmp x) = return $ V (i - x - 1)
435435
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−
453436wknV :: Int -> Value -> Eval Value
454437wknV i (VV x) = return $ VV (x + i)
455438wknV i (VBind red n b sc) = do b' <- fmapMB (wknV i) b
456439 return $ VBind red n b' (\x -> do x' <- sc x
457440 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')
459445wknV i t = return t
460446
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−
597447convEq' ctxt x y = evalStateT (convEq ctxt x y) (0, [])
598448
599449convEq :: Context -> TT Name -> TT Name -> StateT UCs TC Bool
@@ -821,7 +671,7 @@ addCasedef n ci@(CaseInfo alwaysInline tcdict)
821671 ctxt' = case (simpleCase tcase covering reflect CompileTime (FC "" 0) ps,
822672 simpleCase tcase covering reflect RunTime (FC "" 0) psrt) of
823673 (OK (CaseDef args sc _), OK (CaseDef args' sc' _)) ->
824− let inl = alwaysInline || tcdict
674+ let inl = alwaysInline -- || tcdict
825675 inlc = (inl || small n args sc') && (not asserted)
826676 inlr = inl || small n args sc' in
827677 addDef n (CaseOp (ci { case_inlinable = inlc })