thautwarm
Handling I/O
Hey, I'm wondering is it possible to run programs with I/O (like reading user input)
file (check.idr)
module Main
import QB.FFI
main : IO ()
main = do line <- getLine
putStr $ line
when running idris check.idr -p quick-backend I get an error
Type checking ./check.idr
check.idr:6:19-25:
|
6 | main = do line <- getLine
| ~~~~~~~
When checking right hand side of main with expected type
IO ()
When checking an application of function Prelude.Monad.>>=:
Type mismatch between
IO String (Type of getLine)
and
IO' (MkFFI QuickTypes ForeignName String) a (Expected type)
Specifically:
Type mismatch between
C_Types
and
QuickTypes
As I understand QuickTypes/some underlying implementation just does not provide currently any kind of input handling, so how much effort is to add that? Any hints / general overview of the implementation process for this feature is appreciated.
Hi, Idris-dev they implemented backend polymorphic standard libraries:
putStr and getLine is for C backend, but putStr' and getLine' are backend polymorphic.
module Main
import QB.FFI
main : IO ()
main = do line <- getLine'
putStr' line
Suppose you're using Python backend(similar modifications for Julia, Ruby, etc.), remember to add these methods to rts.py:
def op_read_str(f):
return input()
def op_str_eq(a, b):
return a == b
def op_str_rev(a):
return a[::-1]
def op_str_head(a):
return a[0]
def op_str_cons(a, b):
return a + b
def op_str_tail(a):
if not a:
raise IndexError
return a[1:]
and things work well:
> python examples\io_.py
aaa
aaa
Further, QuickBackend is actually designed for easier FFI, and we can just use a foreign function:
module Main
import QB.FFI
main : IO ()
main = do line <- callff0 "py_get_line"
callff1 "py_print" line
which requires implementing RTS.py_get_line() and RTS.py_print(line).
You can also make C backend functions work, by removing import QB.FFI.
module Main
main : IO ()
main = do line <- getLine
putStr $ line