git.iko.soy/Idris-dev
on aeb032a help sign in
Idris-dev/test/error007/error007.idr
29 lines 1.1 kB history raw
1module Main
3import CFFI
5string_from_c : Ptr -> IO String
6string_from_c str = foreign FFI_C "make_string_2" (Ptr -> IO String) str
8connection_information_struct : Composite
9connection_information_struct = STRUCT [I8, PTR, PTR, PTR, I32]
11send_page : (conn : Ptr) -> (text : String) -> (code : Int) -> IO Int
12send_page conn page code = pure (the Int 1)
14-- Error here was using the error from the 'do' block without 'Delay' applied,
15-- which ended up looking very strange... elaborator should take the first
16-- error (from the delayed block) when elaborating arguments which may or may
17-- not need a delay
18answer_to_connection : Ptr -> Ptr -> IO Int
19answer_to_connection conn conn_info = do
20 code_fld <- pure $ (connection_information_struct#4) conn_info
21 code <- peek I32 code_fld
22 answer_fld <- pure $ (connection_information_struct#1) conn_info
23 answer <- peek PTR answer_fld
24 if answer /= null then do
25 str <- string_from_c answer
26 send_page conn str code -- (prim__zextB32_Int code)
27 else do
28 send_page conn str (prim__zextB32_Int code)