#include <strings.ncc>

---------------
-- builtins ---
---------------

defn putChar    :  char -> prop -- builtin
   | putCharImp = [A] putChar A

-- for sequencing io actions
fixity left 1 ,
defn io : prop
   | do = io
   | ,  = io -> prop -> io 

defn run : io -> prop
   | runDo = run do
   | runSeq = run (Av , Bv) <- run Av
                            <- Bv

defn readLine    : (string -> io) -> prop -- builtin 
   | readLineImp = [Foo : string -> io] [A : string] readLine Foo <- run (Foo A)


----------------
--- printing ---
----------------

defn putStr : string -> prop
   | putStr_Nil = putStr nil
   | putStr_Cons = putStr (cons V L)
                   <- putChar V
                   <- putStr L