@@ -29,7 +29,7 @@ import Foreign.Ptr
2929import System.IO
3030
3131
32−data Lazy = Delayed ExecEnv Context Term | Forced ExecVal
32+data Lazy = Delayed ExecEnv Context Term | Forced ExecVal deriving Show
3333
3434data ExecState = ExecState { exec_thunks :: M.Map Int Lazy -- ^ Thunks - the result of evaluating "lazy" or calling lazy funcs
3535 , exec_next_thunk :: Int -- ^ Ensure thunk key uniqueness
@@ -81,7 +81,7 @@ toTT (EApp e1 e2) = do e1' <- toTT e1
8181toTT (EType u) = return $ TType u
8282toTT EErased = return Erased
8383toTT (EConstant c) = return (Constant c)
84−toTT (EThunk _) = return Erased
84+toTT (EThunk i) = (force i) >>= toTT
8585toTT (EHandle _) = return Erased
8686
8787unApplyV :: ExecVal -> (ExecVal, [ExecVal])
@@ -144,6 +144,10 @@ tryForce :: ExecVal -> Exec ExecVal
144144tryForce (EThunk i) = force i
145145tryForce tm = return tm
146146
147+debugThunks :: Exec ()
148+debugThunks = do st <- getExecState
149+ execIO $ putStrLn (take 4000 (show (exec_thunks st)))
150+
147151execute :: Term -> Idris Term
148152execute tm = do est <- initState
149153 ctxt <- getContext
@@ -266,10 +270,13 @@ execApp' env ctxt f@(EP _ n _) args =
266270 [Function _ tm] -> fail "should already have been eval'd"
267271 [TyDecl nt ty] -> return $ mkEApp f args
268272 [Operator tp arity op] ->
269− case getOp n (take arity args) of
270− Just res -> do r <- res
271− execApp' env ctxt r (drop arity args)
272− Nothing -> return (mkEApp f args)
273+ if length args >= arity
274+ then do args' <- mapM tryForce $ take arity args
275+ case getOp n args' of
276+ Just res -> do r <- res
277+ execApp' env ctxt r (drop arity args)
278+ Nothing -> return (mkEApp f args)
279+ else return (mkEApp f args)
273280 [CaseOp _ _ _ _ _ [] (STerm tm) _ _] -> -- nullary fun
274281 do rhs <- doExec env ctxt tm
275282 execApp' env ctxt rhs args
@@ -278,21 +285,52 @@ execApp' env ctxt f@(EP _ n _) args =
278285 return $ fromMaybe (mkEApp f args) res
279286 thing -> return $ mkEApp f args
280287 where getOp :: Name -> [ExecVal] -> Maybe (Exec ExecVal)
288+ getOp (UN "prim__addInt") [EConstant (I i1), EConstant (I i2)] =
289+ primRes I (i1 + i2)
290+ getOp (UN "prim__charToInt") [EConstant (Ch c)] =
291+ primRes I (fromEnum c)
281292 getOp (UN "prim__concat") [EConstant (Str s1), EConstant (Str s2)] =
282− Just . return . EConstant . Str $ s1 ++ s2
293+ primRes Str (s1 ++ s2)
294+ getOp (UN "prim__eqChar") [EConstant (Ch c1), EConstant (Ch c2)] =
295+ primResBool (c1 == c2)
283296 getOp (UN "prim__eqInt") [EConstant (I i1), EConstant (I i2)] =
284− Just . return . EConstant . I $ if i1 == i2 then 1 else 0
297+ primResBool (i1 == i2)
298+ getOp (UN "prim__eqString") [EConstant (Str s1), EConstant (Str s2)] =
299+ primResBool (s1 == s2)
300+ getOp (UN "prim__intToFloat") [EConstant (I i)] =
301+ primRes Fl (fromRational (toRational i))
285302 getOp (UN "prim__ltInt") [EConstant (I i1), EConstant (I i2)] =
286− Just . return . EConstant . I $ if i1 < i2 then 1 else 0
287− getOp (UN "prim__subInt") [EConstant (I i1), EConstant (I i2)] =
288− Just . return . EConstant . I $ i1 - i2
303+ primResBool (i1 < i2)
304+ getOp (UN "prim__mulBigInt") [EConstant (BI i1), EConstant (BI i2)] =
305+ primRes BI (i1 * i2)
306+ getOp (UN "prim__mulFloat") [EConstant (Fl i1), EConstant (Fl i2)] =
307+ primRes Fl (i1 * i2)
308+ getOp (UN "prim__mulInt") [EConstant (I i1), EConstant (I i2)] =
309+ primRes I (i1 * i2)
289310 getOp (UN "prim__readString") [EP _ (UN "prim__stdin") _] =
290311 Just $ do line <- execIO getLine
291312 return (EConstant (Str line))
292313 getOp (UN "prim__readString") [EHandle h] =
293314 Just $ do contents <- execIO $ hGetLine h
294315 return (EConstant (Str contents))
295− getOp _ _ = Nothing
316+ getOp (UN "prim__strCons") [EConstant (Ch c), EConstant (Str s)] =
317+ primRes Str (c:s)
318+ getOp (UN "prim__strHead") [EConstant (Str (c:s))] =
319+ primRes Ch c
320+ getOp (UN "prim__strRev") [EConstant (Str s)] =
321+ primRes Str (reverse s)
322+ getOp (UN "prim__strTail") [EConstant (Str (c:s))] =
323+ primRes Str s
324+ getOp (UN "prim__subInt") [EConstant (I i1), EConstant (I i2)] =
325+ primRes I (i1 - i2)
326+ getOp n args = trace ("No prim " ++ show n ++ " for " ++ take 1000 (show args)) Nothing
327+
328+ primRes :: (a -> Const) -> a -> Maybe (Exec ExecVal)
329+ primRes constr = Just . return . EConstant . constr
330+
331+ primResBool :: Bool -> Maybe (Exec ExecVal)
332+ primResBool b = primRes I (if b then 1 else 0)
333+
296334execApp' env ctxt bnd@(EBind n b body) (arg:args) = do ret <- body arg
297335 let (f', as) = unApplyV ret
298336 execApp' env ctxt f' (as ++ args)
@@ -301,14 +339,18 @@ execApp' env ctxt (EThunk i) args = do f <- force i
301339execApp' env ctxt f args = return (mkEApp f args)
302340
303341
342+
343+
344+
304345-- | Overall wrapper for case tree execution. If there are enough arguments, it takes them,
305346-- evaluates them, then begins the checks for matching cases.
306347execCase :: ExecEnv -> Context -> [Name] -> SC -> [ExecVal] -> Exec (Maybe ExecVal)
307348execCase env ctxt ns sc args =
308349 let arity = length ns in
309350 if arity <= length args
310− then do -- args' <- mapM tryForce (take arity args)
311− let amap = zip ns args
351+ then do let amap = zip ns args
352+-- debugThunks
353+-- trace ("Case exec in " ++ take 1000 (show amap) ++ "\nwith " ++ show sc++"\n") $ return ()
312354 caseRes <- execCase' env ctxt amap sc
313355 case caseRes of
314356 Just res -> Just <$> execApp' (map (\(n, tm) -> (n, Let EErased tm)) amap ++ env) ctxt res (drop arity args)
@@ -337,6 +379,9 @@ chooseAlt tm (ConCase n i ns sc : alts) | ((EP _ cn _), args) <- unApplyV tm
337379chooseAlt tm (_:alts) = chooseAlt tm alts
338380chooseAlt _ [] = Nothing
339381
382+
383+
384+
340385data FTy = FInt | FFloat | FChar | FString | FPtr | FUnit deriving (Show, Read)
341386
342387idrisType :: FTy -> ExecVal