@@ -29,7 +29,7 @@ import Foreign.Ptr
29import System.IO
29import System.IO
32−data Lazy = Delayed ExecEnv Context Term | Forced ExecVal
32+data Lazy = Delayed ExecEnv Context Term | Forced ExecVal deriving Show
34data ExecState = ExecState { exec_thunks :: M.Map Int Lazy -- ^ Thunks - the result of evaluating "lazy" or calling lazy funcs
34data ExecState = ExecState { exec_thunks :: M.Map Int Lazy -- ^ Thunks - the result of evaluating "lazy" or calling lazy funcs
35 , exec_next_thunk :: Int -- ^ Ensure thunk key uniqueness
35 , exec_next_thunk :: Int -- ^ Ensure thunk key uniqueness
@@ -81,7 +81,7 @@ toTT (EApp e1 e2) = do e1' <- toTT e1
81toTT (EType u) = return $ TType u
81toTT (EType u) = return $ TType u
82toTT EErased = return Erased
82toTT EErased = return Erased
83toTT (EConstant c) = return (Constant c)
83toTT (EConstant c) = return (Constant c)
84−toTT (EThunk _) = return Erased
84+toTT (EThunk i) = (force i) >>= toTT
85toTT (EHandle _) = return Erased
85toTT (EHandle _) = return Erased
87unApplyV :: ExecVal -> (ExecVal, [ExecVal])
87unApplyV :: ExecVal -> (ExecVal, [ExecVal])
@@ -144,6 +144,10 @@ tryForce :: ExecVal -> Exec ExecVal
144tryForce (EThunk i) = force i
144tryForce (EThunk i) = force i
145tryForce tm = return tm
145tryForce tm = return tm
147+debugThunks :: Exec ()
148+debugThunks = do st <- getExecState
149+ execIO $ putStrLn (take 4000 (show (exec_thunks st)))
147execute :: Term -> Idris Term
151execute :: Term -> Idris Term
148execute tm = do est <- initState
152execute tm = do est <- initState
149 ctxt <- getContext
153 ctxt <- getContext
@@ -266,10 +270,13 @@ execApp' env ctxt f@(EP _ n _) args =
266 [Function _ tm] -> fail "should already have been eval'd"
270 [Function _ tm] -> fail "should already have been eval'd"
267 [TyDecl nt ty] -> return $ mkEApp f args
271 [TyDecl nt ty] -> return $ mkEApp f args
268 [Operator tp arity op] ->
272 [Operator tp arity op] ->
273+ if length args >= arity
274+ then do args' <- mapM tryForce $ take arity args
269− case getOp n (take arity args) of
275+ case getOp n args' of
270− Just res -> do r <- res
276+ Just res -> do r <- res
271− execApp' env ctxt r (drop arity args)
277+ execApp' env ctxt r (drop arity args)
272− Nothing -> return (mkEApp f args)
278+ Nothing -> return (mkEApp f args)
279+ else return (mkEApp f args)
273 [CaseOp _ _ _ _ _ [] (STerm tm) _ _] -> -- nullary fun
280 [CaseOp _ _ _ _ _ [] (STerm tm) _ _] -> -- nullary fun
274 do rhs <- doExec env ctxt tm
281 do rhs <- doExec env ctxt tm
275 execApp' env ctxt rhs args
282 execApp' env ctxt rhs args
@@ -278,21 +285,52 @@ execApp' env ctxt f@(EP _ n _) args =
278 return $ fromMaybe (mkEApp f args) res
285 return $ fromMaybe (mkEApp f args) res
279 thing -> return $ mkEApp f args
286 thing -> return $ mkEApp f args
280 where getOp :: Name -> [ExecVal] -> Maybe (Exec ExecVal)
287 where getOp :: Name -> [ExecVal] -> Maybe (Exec ExecVal)
288+ getOp (UN "prim__addInt") [EConstant (I i1), EConstant (I i2)] =
290+ getOp (UN "prim__charToInt") [EConstant (Ch c)] =
291+ primRes I (fromEnum c)
281 getOp (UN "prim__concat") [EConstant (Str s1), EConstant (Str s2)] =
292 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)
283 getOp (UN "prim__eqInt") [EConstant (I i1), EConstant (I i2)] =
296 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))
285 getOp (UN "prim__ltInt") [EConstant (I i1), EConstant (I i2)] =
302 getOp (UN "prim__ltInt") [EConstant (I i1), EConstant (I i2)] =
286− Just . return . EConstant . I $ if i1 < i2 then 1 else 0
303+ primResBool (i1 < i2)
304+ getOp (UN "prim__mulBigInt") [EConstant (BI i1), EConstant (BI i2)] =
305+ primRes BI (i1 * i2)
287− getOp (UN "prim__subInt") [EConstant (I i1), EConstant (I i2)] =
306+ getOp (UN "prim__mulFloat") [EConstant (Fl i1), EConstant (Fl i2)] =
288− Just . return . EConstant . I $ i1 - i2
307+ primRes Fl (i1 * i2)
308+ getOp (UN "prim__mulInt") [EConstant (I i1), EConstant (I i2)] =
289 getOp (UN "prim__readString") [EP _ (UN "prim__stdin") _] =
310 getOp (UN "prim__readString") [EP _ (UN "prim__stdin") _] =
290 Just $ do line <- execIO getLine
311 Just $ do line <- execIO getLine
291 return (EConstant (Str line))
312 return (EConstant (Str line))
292 getOp (UN "prim__readString") [EHandle h] =
313 getOp (UN "prim__readString") [EHandle h] =
293 Just $ do contents <- execIO $ hGetLine h
314 Just $ do contents <- execIO $ hGetLine h
294 return (EConstant (Str contents))
315 return (EConstant (Str contents))
295− getOp _ _ = Nothing
316+ getOp (UN "prim__strCons") [EConstant (Ch c), EConstant (Str s)] =
318+ getOp (UN "prim__strHead") [EConstant (Str (c:s))] =
320+ getOp (UN "prim__strRev") [EConstant (Str s)] =
321+ primRes Str (reverse s)
322+ getOp (UN "prim__strTail") [EConstant (Str (c:s))] =
324+ getOp (UN "prim__subInt") [EConstant (I i1), EConstant (I i2)] =
326+ getOp n args = trace ("No prim " ++ show n ++ " for " ++ take 1000 (show args)) Nothing
328+ primRes :: (a -> Const) -> a -> Maybe (Exec ExecVal)
329+ primRes constr = Just . return . EConstant . constr
331+ primResBool :: Bool -> Maybe (Exec ExecVal)
332+ primResBool b = primRes I (if b then 1 else 0)
296execApp' env ctxt bnd@(EBind n b body) (arg:args) = do ret <- body arg
334execApp' env ctxt bnd@(EBind n b body) (arg:args) = do ret <- body arg
297 let (f', as) = unApplyV ret
335 let (f', as) = unApplyV ret
298 execApp' env ctxt f' (as ++ args)
336 execApp' env ctxt f' (as ++ args)
@@ -301,14 +339,18 @@ execApp' env ctxt (EThunk i) args = do f <- force i
301execApp' env ctxt f args = return (mkEApp f args)
339execApp' env ctxt f args = return (mkEApp f args)
304-- | Overall wrapper for case tree execution. If there are enough arguments, it takes them,
345-- | Overall wrapper for case tree execution. If there are enough arguments, it takes them,
305-- evaluates them, then begins the checks for matching cases.
346-- evaluates them, then begins the checks for matching cases.
306execCase :: ExecEnv -> Context -> [Name] -> SC -> [ExecVal] -> Exec (Maybe ExecVal)
347execCase :: ExecEnv -> Context -> [Name] -> SC -> [ExecVal] -> Exec (Maybe ExecVal)
307execCase env ctxt ns sc args =
348execCase env ctxt ns sc args =
308 let arity = length ns in
349 let arity = length ns in
309 if arity <= length args
350 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
353+-- trace ("Case exec in " ++ take 1000 (show amap) ++ "\nwith " ++ show sc++"\n") $ return ()
312 caseRes <- execCase' env ctxt amap sc
354 caseRes <- execCase' env ctxt amap sc
313 case caseRes of
355 case caseRes of
314 Just res -> Just <$> execApp' (map (\(n, tm) -> (n, Let EErased tm)) amap ++ env) ctxt res (drop arity args)
356 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
337chooseAlt tm (_:alts) = chooseAlt tm alts
379chooseAlt tm (_:alts) = chooseAlt tm alts
338chooseAlt _ [] = Nothing
380chooseAlt _ [] = Nothing
340data FTy = FInt | FFloat | FChar | FString | FPtr | FUnit deriving (Show, Read)
385data FTy = FInt | FFloat | FChar | FString | FPtr | FUnit deriving (Show, Read)
342idrisType :: FTy -> ExecVal
387idrisType :: FTy -> ExecVal