Facet is an opaque pair of pointer to vtable and pointer to data. Every facet declares number of supported functions that are delegated to data object. The vtable is immutable tuple of pointer to functions that take data object as argument. There are operations to define vtables (deffacetimpl) and operation to make facet from vtable and data pointer (make-facet). Below is an example of how it could be done.
This can allow avoiding raw pointers for such situations and should help with proofs.
Constantine
; define closable facet (deffacet Closable (defun (close)))
; define IOChannel facet (deffacet IOChannel (extends Closable) ; facet extends closable facet (deffun (seek pos:int)) ;seek operation (deffun (read buffer:(vector uint8)):int) ; read operation (deffun (write buffer:(vector uint8)):int)) ; write operation
; Example of default facet
(defstruct NullStream (pos:int))
; define facet implemeantions
(deffun (seek stream:NullStream pos) (set! stream.pos pos))
(deffun (read stream:NullStream buffer:(vector uint8)):int 0) ; read operation
(deffun (write stream:NullStream buffer:(vector uint8)):int) (lenght buffer)) ; write operation
(deffun (close stream:NullStream pos) -1); ignore close
; define default facet implementation that maps functions by name
(deffacetimpl NullChannel ; name of facet implemenation
IOChannel ; name of facet definition
NullStream ; name of facet data type )
(defstruct SameCharStream (pos:int char:uint8)) ; define facet implemeantions (deffun (seek stream:NullStream pos) (set! stream.pos pos)) (deffun (read buffer:(vector uint8)):int 0) ; read operation (deffun (write buffer:(vector uint8)):int) (lenght buffer))
; define facet with explicit implementation
(deffacetimpl SameCharChannel ; name of facet implemenation
IOChannel ; name of facet definition
(data SameCharStream) ; name of facet data structures
(deffun (seek pos) (set! data.pos pos))
(deffun (read buffer:(vector uint8)):int 0 (memset buffer data.char) ) ; read operation
(deffun (write buffer:(vector uint8)):int) (lenght buffer))
(deffun (close) -1)) ; ignore close
(define DefaultZeroData : ZeroStream (pos 0) (char 0) ) ; data for zero stream
(define DefaultNullData : NullStream (pos 0) ; data for null stream
; the function that returs either null or zero facet
(deffun (get-default-stream isZero) : IOChannel
(cond
((isZero) (make-facet ZeroChannel DefaultZeroData))
(else (make-facet NullChannel DefaultNullData))))
(deffun (test) (define c (get-default-stream #t) ) ; get channel (define b (unboxed (vector uint8 4)) ; create buffer (read c b)) ; read zeros into buffer
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
