@@ -60,6 +60,7 @@ data ExecVal = EP NameType Name ExecVal
60 | EBind Name (Binder ExecVal) (ExecVal -> Exec ExecVal)
60 | EBind Name (Binder ExecVal) (ExecVal -> Exec ExecVal)
61 | EApp ExecVal ExecVal
61 | EApp ExecVal ExecVal
62 | EType UExp
62 | EType UExp
64 | EConstant Const
65 | EConstant Const
65 | forall a. EPtr (Ptr a)
66 | forall a. EPtr (Ptr a)
@@ -72,6 +73,7 @@ instance Show ExecVal where
72 show (EBind n b body) = "EBind " ++ show b ++ " <<fn>>"
73 show (EBind n b body) = "EBind " ++ show b ++ " <<fn>>"
73 show (EApp e1 e2) = show e1 ++ " (" ++ show e2 ++ ")"
74 show (EApp e1 e2) = show e1 ++ " (" ++ show e2 ++ ")"
74 show (EType _) = "Type"
75 show (EType _) = "Type"
76+ show (EUType _) = "UType"
75 show EErased = "[__]"
77 show EErased = "[__]"
76 show (EConstant c) = show c
78 show (EConstant c) = show c
77 show (EPtr p) = "<<ptr " ++ show p ++ ">>"
79 show (EPtr p) = "<<ptr " ++ show p ++ ">>"
@@ -102,6 +104,7 @@ toTT (EApp e1 e2) = do e1' <- toTT e1
102 e2' <- toTT e2
104 e2' <- toTT e2
103 return $ App e1' e2'
105 return $ App e1' e2'
104toTT (EType u) = return $ TType u
106toTT (EType u) = return $ TType u
107+toTT (EUType u) = return $ UType u
105toTT EErased = return Erased
108toTT EErased = return Erased
106toTT (EConstant c) = return (Constant c)
109toTT (EConstant c) = return (Constant c)
107toTT (EThunk ctxt env tm) = do env' <- mapM toBinder env
110toTT (EThunk ctxt env tm) = do env' <- mapM toBinder env
@@ -205,6 +208,7 @@ doExec env ctxt (Proj tm i) = let (x, xs) = unApply tm in
205doExec env ctxt Erased = return EErased
208doExec env ctxt Erased = return EErased
206doExec env ctxt Impossible = fail "Tried to execute an impossible case"
209doExec env ctxt Impossible = fail "Tried to execute an impossible case"
207doExec env ctxt (TType u) = return (EType u)
210doExec env ctxt (TType u) = return (EType u)
211+doExec env ctxt (UType u) = return (EUType u)
209execApp :: ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
213execApp :: ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
210execApp env ctxt v [] = return v -- no args is just a constant! can result from function calls
214execApp env ctxt v [] = return v -- no args is just a constant! can result from function calls
@@ -404,7 +408,7 @@ force = sUN "Force"
404-- | Look up primitive operations in the global table and transform them into ExecVal functions
408-- | Look up primitive operations in the global table and transform them into ExecVal functions
405getOp :: Name -> [ExecVal] -> Maybe (Exec ExecVal)
409getOp :: Name -> [ExecVal] -> Maybe (Exec ExecVal)
406getOp fn [_, _, x] | fn == pbm = Just (return x)
410getOp fn [_, _, x] | fn == pbm = Just (return x)
407−getOp fn [EP _ fn' _]
411+getOp fn [EP _ fn' _]
408 | fn == prs && fn' == pstd =
412 | fn == prs && fn' == pstd =
409 Just $ do line <- execIO getLine
413 Just $ do line <- execIO getLine
410 return (EConstant (Str line))
414 return (EConstant (Str line))
@@ -548,7 +552,7 @@ foreignFromTT t = case (unApplyV t) of
548 _ -> trace ("failed to construct ffun") Nothing
552 _ -> trace ("failed to construct ffun") Nothing
550getFTy :: ExecVal -> Maybe FType
554getFTy :: ExecVal -> Maybe FType
551−getFTy (EApp (EP _ (UN fi) _) (EP _ (UN intTy) _))
555+getFTy (EApp (EP _ (UN fi) _) (EP _ (UN intTy) _))
552 | fi == txt "FIntT" =
556 | fi == txt "FIntT" =
553 case str intTy of
557 case str intTy of
554 "ITNative" -> Just (FArith (ATInt ITNative))
558 "ITNative" -> Just (FArith (ATInt ITNative))