@@ -8,11 +8,14 @@ import Idris.Core.TT
88import Idris.Core.CaseTree
99import Idris.Core.Evaluate
1010
11+import Debug.Trace
12+
1113-- A stack entry consists of a term and the environment it is to be
1214-- evaluated in (i.e. it's a thunk)
1315type StackEntry = (Term, WEnv)
1416data WEnv = WEnv Int -- number of free variables
1517 [(Term, WEnv)]
18+ deriving Show
1619
1720type Stack = [StackEntry]
1821
@@ -73,12 +76,102 @@ do_whnf ctxt env tm = eval env [] tm
7376 TCon t a -> WTCon t a n (ty, env)
7477 _ -> WPRef n (ty, env)
7578 in
76− unload wp stk
79+ case lookupDefExact n ctxt of
80+ Just (CaseOp ci _ _ _ _ cd) ->
81+ let (ns, tree) = cases_compiletime cd in
82+ case evalCase env ns tree stk of
83+ Just w -> w
84+ Nothing -> unload wp stk
85+ Just (Operator _ i op) ->
86+ if i <= length stk
87+ then case runOp op (take i stk) of
88+ Nothing -> unload wp stk
89+ -- Given that we can't apply constants
90+ -- to things, and runOp only does
91+ -- constants for now, this should
92+ -- never happen...
93+ Just v -> unload v (drop i stk)
94+ else unload wp stk
95+ _ -> unload wp stk
7796
7897 unload :: WHNF -> Stack -> WHNF
7998 unload f [] = f
8099 unload f (a : as) = unload (WApp f a) as
81100
101+ runOp :: ([Value] -> Maybe Value) -> Stack -> Maybe WHNF
102+ runOp op stk = do vals <- mapM toValue stk
103+ case op vals of
104+ Just (VConstant c) -> Just (WConstant c)
105+ _ -> Nothing
106+
107+ toValue :: (Term, WEnv) -> Maybe Value
108+ toValue (tm, tenv) = case eval tenv [] tm of
109+ WConstant c -> Just (VConstant c)
110+ _ -> Nothing
111+
112+ evalCase :: WEnv -> [Name] -> SC -> Stack -> Maybe WHNF
113+ evalCase wenv@(WEnv d env) ns tree args
114+ | length ns > length args = Nothing
115+ | otherwise = let args' = take (length ns) args
116+ rest = drop (length ns) args in
117+ do (tm, amap) <- evalTree wenv (zip ns args') tree
118+ let wtm = pToVs (map fst amap) tm
119+ Just $ eval (WEnv d (map snd amap)) rest wtm
120+
121+ evalTree :: WEnv -> [(Name, (Term, WEnv))] -> SC ->
122+ Maybe (Term, [(Name, (Term, WEnv))])
123+ evalTree env amap (STerm tm) = Just (tm, amap)
124+ evalTree env amap (Case _ n alts)
125+ = case lookup n amap of
126+ Just (tm, tenv) -> findAlt env amap
127+ (deconstruct (eval tenv [] tm) []) alts
128+ _ -> Nothing
129+ evalTree _ _ _ = Nothing
130+
131+ deconstruct :: WHNF -> Stack -> (WHNF, Stack)
132+ deconstruct (WApp f arg) stk = deconstruct f (arg : stk)
133+ deconstruct t stk = (t, stk)
134+
135+ findAlt :: WEnv -> [(Name, (Term, WEnv))] -> (WHNF, Stack) ->
136+ [CaseAlt] ->
137+ Maybe (Term, [(Name, (Term, WEnv))])
138+ findAlt env amap (WDCon tag _ _ _ _, args) alts
139+ | Just (ns, sc) <- findTag tag alts
140+ = let amap' = updateAmap (zip ns args) amap in
141+ evalTree env amap' sc
142+ | Just sc <- findDefault alts
143+ = evalTree env amap sc
144+ findAlt env amap (WConstant c, []) alts
145+ | Just sc <- findConst c alts
146+ = evalTree env amap sc
147+ | Just sc <- findDefault alts
148+ = evalTree env amap sc
149+ findAlt _ _ _ _ = Nothing
150+
151+ findTag :: Int -> [CaseAlt] -> Maybe ([Name], SC)
152+ findTag i [] = Nothing
153+ findTag i (ConCase n j ns sc : xs) | i == j = Just (ns, sc)
154+ findTag i (_ : xs) = findTag i xs
155+
156+ findDefault :: [CaseAlt] -> Maybe SC
157+ findDefault [] = Nothing
158+ findDefault (DefaultCase sc : xs) = Just sc
159+ findDefault (_ : xs) = findDefault xs
160+
161+ findConst c [] = Nothing
162+ findConst c (ConstCase c' v : xs) | c == c' = Just v
163+ findConst (AType (ATInt ITNative)) (ConCase n 1 [] v : xs) = Just v
164+ findConst (AType ATFloat) (ConCase n 2 [] v : xs) = Just v
165+ findConst (AType (ATInt ITChar)) (ConCase n 3 [] v : xs) = Just v
166+ findConst StrType (ConCase n 4 [] v : xs) = Just v
167+ findConst (AType (ATInt ITBig)) (ConCase n 6 [] v : xs) = Just v
168+ findConst (AType (ATInt (ITFixed ity))) (ConCase n tag [] v : xs)
169+ | tag == 7 + fromEnum ity = Just v
170+ findConst c (_ : xs) = findConst c xs
171+
172+ updateAmap newm amap
173+ = newm ++ filter (\ (x, _) -> not (elem x (map fst newm))) amap
174+
82175quote :: WHNF -> Term
83176quote (WDCon t a u n (ty, env)) = P (DCon t a u) n (quoteEnv env ty)
84177quote (WTCon t a n (ty, env)) = P (TCon t a) n (quoteEnv env ty)