files

cfamily.State.file

def State.file {L : Constructs} (s : State L) (name : String) : Option (List Nat)

The bytes of a file, if it exists.

cfamily.State.contents

def State.contents {L : Constructs} (s : State L) (name : String) : List Nat

The bytes of a file (none if it does not exist).

cfamily.State.withFile

def State.withFile {L : Constructs} (s : State L) (name : String) (bytes : List Nat) : State L

The state with a file’s bytes replaced (or the file made).

cfamily.Stream.replace

def Stream.replace (k : Nat) (x : Stream) (xs : List Stream) : List Stream

The k-th of a list replaced.

cfamily.State.stream

def State.stream {L : Constructs} (s : State L) (k : Nat) : Option Stream

The stream the program opened with the number (3 on), if any.

cfamily.State.withStream

def State.withStream {L : Constructs} (s : State L) (k : Nat) (x : Stream) : State L

The state with the stream with the number replaced.

cfamily.OpenMode

data OpenMode

How a mode opens a file: for reading, for writing from the start, for writing at the end; none for a mode the model does not have.

cfamily.OpenMode.ofText

def OpenMode.ofText (text : List Nat) : Option OpenMode

The mode written as fopen takes it (a trailing b is the same).

cfamily.Stream.openFile

def Stream.openFile {L : Constructs} (n : NodeId) (s : State L) (name : String) (written : List Nat) : Evaluated L (State L * Pointer)

fopen: the new stream’s pointer and the state, or NULL when a file to read does not exist.

cfamily.Stream.opened

def Stream.opened {L : Constructs} (n : NodeId) (s : State L) (k : Nat) : Evaluated L Stream

The stream a pointer is, if it is one the program opened and still open; else why it cannot be used.

cfamily.Stream.number

def Stream.number {L : Constructs} (n : NodeId) (p : Pointer) : Evaluated L Nat

The number of the stream a pointer is: NULL is undefined, a pointer that is not a stream an invalid argument.

cfamily.Stream.closeFile

def Stream.closeFile {L : Constructs} (n : NodeId) (s : State L) (p : Pointer) : Evaluated L (State L)

fclose: the stream closed (the standard ones stay as they are).

cfamily.Stream.write

def Stream.write {L : Constructs} (n : NodeId) (s : State L) (p : Pointer) (bytes : List Nat) : Evaluated L (State L)

Output to a stream: stdout and stderr are the console’s; a file opened for writing gets the bytes at its end.

cfamily.Stream.input

def Stream.input {L : Constructs} (n : NodeId) (s : State L) (p : Pointer) : Evaluated L (List Nat)

The input left on a stream: stdin’s is the console’s; a file opened for reading has its bytes after what was read.

cfamily.Stream.consume

def Stream.consume {L : Constructs} (s : State L) (p : Pointer) (count : Nat) (reachedEnd : Bool) : State L

The state after count bytes of a stream’s input were read (the stream checked by Stream.input); reading at the end marks it.

cfamily.Stream.atEnd

def Stream.atEnd {L : Constructs} (n : NodeId) (s : State L) (p : Pointer) : Evaluated L Bool

feof: whether reading a stream reached its end.