From 5810cb6f263679851a135691a7ee483fda959472 Mon Sep 17 00:00:00 2001 From: dos-reis Date: Fri, 9 Jan 2009 16:11:08 +0000 Subject: * algebra/data.spad.pamphlet (Byte): Satisfy OrderedFinite. (SystemInteger, SystemNonNegativeInteger, Int8, Int16, Int32, UInt8, UInt 16, UInt32): New. * algebra/Makefile.pamphlet (axiom_algebra_layer_7): Include INT8, INT16, INT32, UINT8, UINT16, UINT32. --- src/algebra/data.spad.pamphlet | 153 +++++++++++++++++++++++++++++++++++++++-- 1 file changed, 149 insertions(+), 4 deletions(-) (limited to 'src/algebra/data.spad.pamphlet') diff --git a/src/algebra/data.spad.pamphlet b/src/algebra/data.spad.pamphlet index a46ab663..d52ee479 100644 --- a/src/algebra/data.spad.pamphlet +++ b/src/algebra/data.spad.pamphlet @@ -19,13 +19,13 @@ import OutputForm )abbrev domain BYTE Byte ++ Author: Gabriel Dos Reis ++ Date Created: April 19, 2008 -++ Date Last Updated: October 5, 2008 +++ Date Last Updated: January 6, 2009 ++ Basic Operations: byte, bitand, bitor, bitxor ++ Related Constructor: NonNegativeInteger ++ Description: ++ Byte is the datatype of 8-bit sized unsigned integer values. Byte(): Public == Private where - Public == Join(OrderedSet, HomotopicTo Character) with + Public == Join(OrderedFinite, HomotopicTo Character) with byte: NonNegativeInteger -> % ++ byte(x) injects the unsigned integer value `v' into ++ the Byte algebra. `v' must be non-negative and less than 256. @@ -36,14 +36,149 @@ Byte(): Public == Private where sample: () -> % ++ sample() returns a sample datum of type Byte. Private == SubDomain(NonNegativeInteger, #1 < 256) add - byte(x: NonNegativeInteger): % == x::% + byte(x: NonNegativeInteger): % == per x sample() = 0$Lisp - coerce(c: Character) == ord(c)::% + coerce(c: Character) == per ord c coerce(x: %): Character == char rep x x = y == byteEqual(x,y)$Lisp x < y == byteLessThan(x,y)$Lisp + min() == per 0 + max() == per 255 bitand(x,y) == bitand(x,y)$Lisp bitior(x,y) == bitior(x,y)$Lisp + +@ + + +\section{Sized System Integer datatypes} + +<>= +)abbrev domain SYSINT SystemInteger +++ Author: Gabriel Dos Reis +++ Date Created: December 26, 2008 +++ Date Last Modified: December 27, 2008 +++ Description: +++ This domain implements sized (signed) integer datatypes parameterized +++ by the precision (or width) of the underlying representation. +++ The intent is that they map directly to the hosting hardware +++ natural integer datatypes. Consequently, natural values for +++ N are: 8, 16, 32, 64, etc. These datatypes are mostly useful +++ for system programming tasks, i.e. interfacting with the hosting +++ operating system, reading/writing external binary format files. +SystemInteger(N: PositiveInteger): Public == Private where + Public == OrderedFinite + Private == SubDomain(Integer, length #1 <= N) add + min == per(-shift(1,N-1)) + max == per(shift(1,N-1)-1) + size() == (rep max - rep min + 1)::NonNegativeInteger + index i == per (i + rep min - 1) + lookup x == (rep x - rep min + 1)::PositiveInteger + random() == per(random()$Integer rem rep max) + +@ + +<>= +)abbrev domain INT8 Int8 +++ Author: Gabriel Dos Reis +++ Date Created: January 6, 2009 +++ Date Last Modified: January 6, 2009 +++ Description: +++ This domain is a datatype for (signed) integer values +++ of precision 8 bits. +Int8() == SystemInteger 8 + +@ + +<>= +)abbrev domain INT16 Int16 +++ Author: Gabriel Dos Reis +++ Date Created: January 6, 2009 +++ Date Last Modified: January 6, 2009 +++ Description: +++ This domain is a datatype for (signed) integer values +++ of precision 16 bits. +Int16() == SystemInteger 16 + +@ + +<>= +)abbrev domain INT32 Int32 +++ Author: Gabriel Dos Reis +++ Date Created: January 6, 2009 +++ Date Last Modified: January 6, 2009 +++ Description: +++ This domain is a datatype for (signed) integer values +++ of precision 32 bits. +Int32() == SystemInteger 32 + +@ + + +<>= +)abbrev domain SYSNNI SystemNonNegativeInteger +++ Author: Gabriel Dos Reis +++ Date Created: December 26, 2008 +++ Date Last Modified: December 27, 2008 +++ Description: +++ This domain implements sized (unsigned) integer datatypes +++ parameterized by the precision (or width) of the underlying +++ representation. The intent is that they map directly to the +++ hosting hardware natural integer datatypes. Consequently, +++ natural values for N are: 8, 16, 32, 64, etc. These datatypes +++ are mostly useful for system programming tasks, i.e. interfacting +++ with the hosting operating system, reading/writing external +++ binary format files. +SystemNonNegativeInteger(N: PositiveInteger): Public == Private where + Public == OrderedFinite with + bitand: (%,%) -> % + ++ bitand(x,y) returns the bitwise `and' of `x' and `y'. + bitior: (%,%) -> % + ++ bitor(x,y) returns the bitwise `inclusive or' of `x' and `y'. + sample: () -> % + ++ sample() returns a sample datum of type Byte. + Private == SubDomain(NonNegativeInteger, length #1 <= N) add + min == per 0 + max == per((shift(1,N)-1)::NonNegativeInteger) + sample() == min + bitand(x,y) == BOOLE(BOOLE_-AND$Lisp,x,y)$Lisp + bitior(x,y) == BOOLE(BOOLE_-IOR$Lisp,x,y)$Lisp + +@ + +<>= +)abbrev domain UINT8 UInt8 +++ Author: Gabriel Dos Reis +++ Date Created: January 6, 2009 +++ Date Last Modified: January 6, 2009 +++ Description: +++ This domain is a datatype for (unsigned) integer values +++ of precision 8 bits. +UInt8() == SystemNonNegativeInteger 8 + +@ + +<>= +)abbrev domain UINT16 UInt16 +++ Author: Gabriel Dos Reis +++ Date Created: January 6, 2009 +++ Date Last Modified: January 6, 2009 +++ Description: +++ This domain is a datatype for (unsigned) integer values +++ of precision 16 bits. +UInt16() == SystemNonNegativeInteger 16 + +@ + +<>= +)abbrev domain UINT32 UInt32 +++ Author: Gabriel Dos Reis +++ Date Created: January 6, 2009 +++ Date Last Modified: January 6, 2009 +++ Description: +++ This domain is a datatype for (unsigned) integer values +++ of precision 32 bits. +UInt32() == SystemNonNegativeInteger 32 + @ @@ -225,6 +360,16 @@ DataArray(N: PositiveInteger, T: SetCategory): Public == Private where <> <> +<> +<> +<> +<> + +<> +<> +<> +<> + @ \end{document} -- cgit v1.2.3