Anubis / Anubis

 *Project*                                  Anubis
   
 *Title*                           A simple notion of stream.
   
 *Copyright*                     Copyright (c) Alain Prouté 2005. 


 *Author*       Alain Prouté

   
 *Overview*  
   
   A 'stream'  is an object  (in the sens of  OOP) from which  bytes may be read,  or into
   which bytes may be written.  We have defined the opaque type:

public type Stream:...

   in a  'implementation independant' way.   This means that  the actual source  or target
   behind  a   stream  may  be  a   file,  a  network  connection,   a  character  string,
   etc... Whatever it is, the stream is used the same way by the tools provided here.
   
   Different streams  may have different  capabilities. For example,  a stream may  not be
   writable. A  tool returns the capabilities  of the stream. If  you use a  function on a
   stream not having the corresponding capability, the function has just no effect. 
   
   
   *** Creating a stream. 
   
   As said above, a stream may be  created from various sources.  We provide below several
   functions for creating streams:
   
public define Stream      make_stream(RAddr(Int8)     file). 
public define Stream      make_stream(WAddr(Int8)     file). 
public define Stream      make_stream(RWAddr(Int8)    file).
public define Stream      make_stream(String          s).    
   
   
   
   
   *** Getting the capabilities. 
   
public type StreamCapability:
   readable,
   writable,
   seekable.
   
public define List(StreamCapability)   get_capabilities(Stream s). 
   
   
   
   
   *** Reading from a stream. 
   
public define Maybe(Int8)     read_byte        (Stream s). 
public define Maybe(String)   read_line        (Stream s).
public define One             skip_blanks      (Stream s).
public define Maybe(String)   read_symbol      (Stream s).   
public define Maybe(String)   read_integer     (Stream s). 
public define List($T)        read_several     (Stream s, Stream -> Maybe($T) read_one).  
public define Maybe(List($T)) read_list        (Stream s, Stream -> Maybe($T) read_one). 
   
   
   'read_byte' reads the next byte
   
   'read_line' reads from the current position to  end of current line. The end of line is
      any of:     LF
                  CR LF
                  CR
   
   'skip_blanks' skips blank  characters until the next non blank  character (which is not
      read)
   
   'read_symbol' reads  a symbol, skiping leading blanks  if necessary. A symbol  is a non
      empty concatenation of letters from 'a' to 'z', 'A' to 'Z', '0' to '9' and '_'. 
   
   'read_integer' is like 'read_symbol' but accepts only the characters '0' to '9'. 
   
   'read_several' applies 'read_one' repeatedly until it returns 'failure'. 'read_several'
      returns the list of all the entities read by 'read_one' (in their natural order). 
   
   'read_list'  expects an  opening parenthese,  then applies  'read_one'  repeatedly, and
      expects a closing parenthese. It returns the list of entities read by 'read_one'. 

   
   You may also unput an arbitrary number of bytes in the stream:
   
public define One        unput_byte      (Int8 c, Stream s).   
   
   If   the  bytes   unput  are   not  those   read  from   the  stream   the   result  is
   unpredictable. Unputing a '\n' may induce a wrong column count. 

   
   
   *** Informations about the current state of the stream. 
   
public define Int32           current_offset   (Stream s).
public define Int32           current_line     (Stream s).
public define Int32           current_column   (Stream s). 
          
   'current_offset' returns the number of bytes read so far.
   
   'current_line'   returns the number of '\n' read so_far.
   
   'current_column' returns the number of bytes read since the last '\n' (or the beginning
       of the input).
   

   
   *** Writting into a stream. 
   
public define Maybe(One)    write_byte       (Stream  s, Int8  byte). 
public define Maybe(One)    write_string     (Stream  s, String t).    
   
   
   
   
   --- That's all for the public part ! --------------------------------------------------

   
   
   
   
public type Stream:
   stream(One -> Maybe(Int8)       rb,       // read a byte
          Int8 -> Maybe(One)       wb,       // write a byte
          Int8 -> One              ub,       // unput a byte
          One -> Int32             of,       // offset
          One -> Int32             ln,       // line
          One -> Int32             cl).      // column
   
         

define One -> Maybe(Int8)
   make_rb   // making the 'rb' function 
     (
       RAddr(Int8)       file,
       Var(List(Int8))   v, 
       Var(Int32)        o, 
       Var(Int32)        l,
       Var(Int32)        c
     ) =
   (One u) |-> if *v is 
      {
        [ ] then if *file is 
          {
            failure then failure, 
            success(byte) then o <- *o+1;      //increment the offset counter
                               (if byte = '\n' then (l <- *l+1; c <- 0) 
                                               //and if it is a new line increment the line counter
                                               else c <- *c+1);
                               success(byte)   
          }, 
        [h . t] then v <- t; 
                     o <- *o+1; 
                     (if h = '\n' then (l <- *l+1; c <- 0)
                                  else c <- *c+1); 
                     success(h)
     }. 
   

   
define Int8 -> One
   make_ub     // making the 'ub' function 
     (
       Var(List(Int8))   v, 
       Var(Int32)        o, 
       Var(Int32)        l,
       Var(Int32)        c
     ) =
   (Int8 byte) |-> v <- [byte . *v]; 
                   o <- *o-1;
                   (if byte = '\n' then (l <- *l-1; c <- 0)
                                   else c <- *c-1).

   
   
   
public define Stream
   make_stream
     (
       RAddr(Int8)    file
     ) =
   with v = var((List(Int8))[]),     // stack of unput bytes
        o = var((Int32)0),           // offset
        l = var((Int32)1),           // line
        c = var((Int32)0),           // column
   stream(
     make_rb(file,v,o,l,c), 
     (Int8 c) |-> failure, 
     make_ub(v,o,l,c), 
     (One u) |-> *o, 
     (One u) |-> *l,
     (One u) |-> *c
         ). 
   
public define Stream
   make_stream
     (
       RWAddr(Int8)    file
     ) =
   with v = var((List(Int8))[]),     // stack of unput bytes
        o = var((Int32)0),           // offset
        l = var((Int32)1),           // line
        c = var((Int32)0),           // column
   stream(
     make_rb(weaken(file),v,o,l,c), 
     (Int8 c) |-> file <- c, 
     make_ub(v,o,l,c), 
     (One u) |-> *o, 
     (One u) |-> *l,
     (One u) |-> *c
         ). 
   
public define Stream
   make_stream
     (
       WAddr(Int8)    file
     ) =
   stream(
     (One u) |-> failure,
     (Int8 c) |-> file <- c,
     (Int8 c) |-> unique, 
     (One u) |-> 0,
     (One u) |-> 0, 
     (One u) |-> 0
   ).
   
public define Stream
   make_stream
     (
       String s
     ) =
   with i = var((Int32)0), 
        l = var((Int32)1), 
        c = var((Int32)0), 
        b = var((List(Int8))[]), 
        d = var((List(String))[]),
        n = var((Int32)0), 
   stream(
          // reading the next byte:
          (One u) |-> if nth(*i,s) is 
                {
                  failure then failure, 
                  success(byte) then i <- *i+1; 
                                     (if byte = '\n' then (l <- *l+1; c <- 0)
                                                     else c <- *c+1);
                                     success(byte)
                },
   
          // writing a byte
          (Int8 c) |-> 
             b <- [c . *b];
             n <- *n + 1; 
             if *n >= 100
             then 
               (protect
                d <- [implode(reverse(*b)) . *d];
                b <- [];
                n <- 0;
                success(unique)
               )
             else success(unique), 
   
          // unputting a byte:
          (Int8 byte) |-> i <- *i-1;
                          (if byte = '\n' then (l <- *l-1; c <- 0)
                                          else c <- *c-1),
   
          // getting the offset:
          (One u) |-> *i,
   
          // getting the line:
          (One u) |-> *l,
    
          // getting the column
          (One u) |-> *c
         ). 
   
   
   

public define Int32      
   current_offset
     (
       Stream s
     ) =
   of(s)(unique).    
   
   
public define Int32
   current_line
     (
       Stream s
     ) =
   ln(s)(unique). 
   
public define Int32
   current_column
     (
       Stream s
     ) =
   cl(s)(unique). 
   
   
public define Maybe(Int8)
   read_byte
     (
       Stream s
     ) =
   rb(s)(unique). 
   
public define One
   unput_byte
     (
       Int8 c, 
       Stream s
     ) =
   ub(s)(c). 
   
   

   *Description*  'read_text_byte' transforms  a  function of  type  'One ->  Maybe(Int8)'
   reading bytes  in binary mode into  a function of the  same type reading  bytes in text
   mode. By convention all ends of lines are returned as '\n'. 
   
define One -> Maybe(Int8)
   read_text_byte
     (
       One -> Maybe(Int8) rbs,
       Int8 -> One        unput
     ) =
   (One u) |-> 
     if rbs(unique) is 
       {
         failure    then failure, 
         success(c) then 
           if c = '\r'
           then if rbs(unique) is 
             {
               failure     then success('\n'),
               success(d)  then 
                 if d = '\n'
                 then success('\n')
                 else unput(d); success('\n')
             }
           else success(c)
                /* actually: 
                if c = '\n'
                then success('\n')
                else success(c)
                */
       }.
   
   
   
define Maybe(String)
   read_line
     (
       One -> Maybe(Int8)    rtb,       // this function reads bytes in text mode
       List(Int8)            so_far
     ) =
   if rtb(unique) is 
     {
       failure     then if so_far is []
                        then failure 
                        else success(implode(reverse(so_far))), 
       success(c)  then 
         if c = '\n'
         then success(implode(reverse(so_far)))
         else read_line(rtb,[c . so_far])
     }. 
   
public define Maybe(String)
   read_line
     (
       Stream s
     ) =
   read_line(read_text_byte(rb(s),ub(s)),[]). 
   
   
public define One
   skip_blanks
     (
       Stream     s
     ) =
   if rb(s)(unique) is 
     {
       failure then unique, 
       success(c) then 
         if int8_to_int32(c) =< ' '
         then skip_blanks(s)
         else ub(s)(c)
     }. 
   
   
   
define Maybe(String)
   read_symbol
     (
       Stream         s,
       List(Int8)     so_far,
       Int8 -> Bool   is_acceptable_char
     ) =
   if rb(s)(unique) is 
     {
       failure then if so_far is 
         {
           [ ] then failure, 
           [_ . _] then success(implode(reverse(so_far)))
         },
       success(c) then 
         if is_acceptable_char(c)
         then read_symbol(s,[c . so_far],is_acceptable_char)
         else 
           ub(s)(c); 
           if so_far is 
             {
               [ ] then failure, 
               [_ . _] then success(implode(reverse(so_far)))
             }
     }.
   
   
define Bool
   is_symbol_char
     (
       Int8   c
     ) =
   with n = int8_to_int32(c), 
   if n = '_' then true else
   if ('a' =< n & n =< 'z') then true else
   if ('A' =< n & n =< 'Z') then true else
   ('0' =< n & n =< '9').
   
define Bool
   is_integer_char
     (
       Int8   c
     ) =
   with n = int8_to_int32(c), 
   '0' =< n & n =< '9'.
   
   
public define Maybe(String)
   read_symbol
     (
       Stream     s
     ) =
   skip_blanks(s);
   read_symbol(s,[],is_symbol_char).    
   
public define Maybe(String)
   read_integer
     (
       Stream     s
     ) =
   skip_blanks(s);
   read_symbol(s,[],is_integer_char).    
   
   
define List($T)
   read_several
     (
       Stream                   s, 
       Stream -> Maybe($T)      read_one,
       List($T)                 so_far
     ) =
   if read_one(s) is 
     {
       failure then reverse(so_far),
       success(u) then read_several(s,read_one,[u . so_far])
     }.
   
   
   
public define List($T)
   read_several
     (
       Stream                   s, 
       Stream -> Maybe($T)      read_one
     ) =
   read_several(s,read_one,[]).    
   
   
define List($T)
   read_list
     (
       Stream                   s, 
       Stream -> Maybe($T)      read_one,
       List($T)                 so_far
     ) =
   if read_one(s) is 
     {
       failure then 
         skip_blanks(s); 
         if rb(s)(unique) is 
           {
             failure then reverse(so_far),
             success(c) then
               if c = ')'
               then reverse(so_far)
               else (ub(s)(c); reverse(so_far))
           },
       success(u) then read_list(s,read_one,[u . so_far])
     }.
   
public define Maybe(List($T))   
   read_list
     (
       Stream                   s, 
       Stream -> Maybe($T)      read_one
     ) =
   skip_blanks(s); 
   if rb(s)(unique) is 
     {
       failure then failure, 
       success(c) then 
         if c = '('
         then success(read_list(s,read_one,[]))
         else ub(s)(c); failure
     }.
   
   
public define Maybe(One)
   write_byte
     (
       Stream  s, 
       Int8  byte
     ) =
   wb(s)(byte). 

   
   
define Maybe(One)    
   write_string     
     (
       Int8 -> Maybe(One)  wb, 
       String              t,
       Int32               i
     ) =    
   if nth(i,t) is 
     {
       failure then success(unique), 
       success(c) then 
         if wb(c) is 
           {
             failure then failure, 
             success(_) then write_string(wb,t,i+1)
           }
     }.
   
   
public define Maybe(One)    
   write_string
     (
       Stream      s, 
       String      t
     ) =    
   write_string(wb(s),t,0).