\documentclass{article} \usepackage{axiom} \begin{document} \title{\$SPAD/src/algebra boolean.spad} \author{Stephen M. Watt, Michael Monagan} \maketitle \begin{abstract} \end{abstract} \eject \tableofcontents \eject \section{domain REF Reference} <>= )abbrev domain REF Reference ++ Author: Stephen M. Watt ++ Date Created: ++ Change History: ++ Basic Operations: deref, elt, ref, setelt, setref, = ++ Related Constructors: ++ Keywords: reference ++ Description: \spadtype{Reference} is for making a changeable instance ++ of something. Reference(S:Type): Type with ref : S -> % ++ ref(n) creates a pointer (reference) to the object n. elt : % -> S ++ elt(n) returns the object n. setelt: (%, S) -> S ++ setelt(n,m) changes the value of the object n to m. -- alternates for when bugs don't allow the above deref : % -> S ++ deref(n) is equivalent to \spad{elt(n)}. setref: (%, S) -> S ++ setref(n,m) same as \spad{setelt(n,m)}. _= : (%, %) -> Boolean ++ a=b tests if \spad{a} and b are equal. if S has SetCategory then SetCategory == add Rep := Record(value: S) p = q == EQ(p, q)$Lisp ref v == [v] elt p == p.value setelt(p, v) == p.value := v deref p == p.value setref(p, v) == p.value := v if S has SetCategory then coerce p == prefix(message("ref"@String), [p.value::OutputForm]) @ \section{REF.lsp BOOTSTRAP} {\bf REF} depends on a chain of files. We need to break this cycle to build the algebra. So we keep a cached copy of the translated {\bf REF} category which we can write into the {\bf MID} directory. We compile the lisp code and copy the {\bf REF.o} file to the {\bf OUT} directory. This is eventually forcibly replaced by a recompiled version. Note that this code is not included in the generated catdef.spad file. <>= (|/VERSIONCHECK| 2) (PUT (QUOTE |REF;=;2$B;1|) (QUOTE |SPADreplace|) (QUOTE EQ)) (DEFUN |REF;=;2$B;1| (|p| |q| |$|) (EQ |p| |q|)) (PUT (QUOTE |REF;ref;S$;2|) (QUOTE |SPADreplace|) (QUOTE LIST)) (DEFUN |REF;ref;S$;2| (|v| |$|) (LIST |v|)) (PUT (QUOTE |REF;elt;$S;3|) (QUOTE |SPADreplace|) (QUOTE QCAR)) (DEFUN |REF;elt;$S;3| (|p| |$|) (QCAR |p|)) (DEFUN |REF;setelt;$2S;4| (|p| |v| |$|) (PROGN (RPLACA |p| |v|) (QCAR |p|))) (PUT (QUOTE |REF;deref;$S;5|) (QUOTE |SPADreplace|) (QUOTE QCAR)) (DEFUN |REF;deref;$S;5| (|p| |$|) (QCAR |p|)) (DEFUN |REF;setref;$2S;6| (|p| |v| |$|) (PROGN (RPLACA |p| |v|) (QCAR |p|))) (DEFUN |REF;coerce;$Of;7| (|p| |$|) (SPADCALL (SPADCALL "ref" (QREFELT |$| 17)) (LIST (SPADCALL (QCAR |p|) (QREFELT |$| 18))) (QREFELT |$| 20))) (DEFUN |Reference| (#1=#:G82336) (PROG NIL (RETURN (PROG (#2=#:G82337) (RETURN (COND ((LETT #2# (|lassocShiftWithFunction| (LIST (|devaluate| #1#)) (HGET |$ConstructorCache| (QUOTE |Reference|)) (QUOTE |domainEqualList|)) |Reference|) (|CDRwithIncrement| #2#)) ((QUOTE T) (|UNWIND-PROTECT| (PROG1 (|Reference;| #1#) (LETT #2# T |Reference|)) (COND ((NOT #2#) (HREM |$ConstructorCache| (QUOTE |Reference|)))))))))))) (DEFUN |Reference;| (|#1|) (PROG (|DV$1| |dv$| |$| |pv$|) (RETURN (PROGN (LETT |DV$1| (|devaluate| |#1|) . #1=(|Reference|)) (LETT |dv$| (LIST (QUOTE |Reference|) |DV$1|) . #1#) (LETT |$| (GETREFV 23) . #1#) (QSETREFV |$| 0 |dv$|) (QSETREFV |$| 3 (LETT |pv$| (|buildPredVector| 0 0 (LIST (|HasCategory| |#1| (QUOTE (|SetCategory|))))) . #1#)) (|haddProp| |$ConstructorCache| (QUOTE |Reference|) (LIST |DV$1|) (CONS 1 |$|)) (|stuffDomainSlots| |$|) (QSETREFV |$| 6 |#1|) (QSETREFV |$| 7 (|Record| (|:| |value| |#1|))) (COND ((|testBitVector| |pv$| 1) (QSETREFV |$| 21 (CONS (|dispatchFunction| |REF;coerce;$Of;7|) |$|)))) |$|)))) (MAKEPROP (QUOTE |Reference|) (QUOTE |infovec|) (LIST (QUOTE #(NIL NIL NIL NIL NIL NIL (|local| |#1|) (QUOTE |Rep|) (|Boolean|) |REF;=;2$B;1| |REF;ref;S$;2| |REF;elt;$S;3| |REF;setelt;$2S;4| |REF;deref;$S;5| |REF;setref;$2S;6| (|String|) (|OutputForm|) (0 . |message|) (5 . |coerce|) (|List| |$|) (10 . |prefix|) (16 . |coerce|) (|SingleInteger|))) (QUOTE #(|~=| 21 |setref| 27 |setelt| 33 |ref| 39 |latex| 44 |hash| 49 |elt| 54 |deref| 59 |coerce| 64 |=| 69)) (QUOTE NIL) (CONS (|makeByteWordVec2| 1 (QUOTE (1 0 1 1))) (CONS (QUOTE #(|SetCategory&| NIL |BasicType&| NIL)) (CONS (QUOTE #((|SetCategory|) (|Type|) (|BasicType|) (|CoercibleTo| 16))) (|makeByteWordVec2| 22 (QUOTE (1 16 0 15 17 1 6 16 0 18 2 16 0 0 19 20 1 0 16 0 21 2 1 8 0 0 1 2 0 6 0 6 14 2 0 6 0 6 12 1 0 0 6 10 1 1 15 0 1 1 1 22 0 1 1 0 6 0 11 1 0 6 0 13 1 1 16 0 21 2 0 8 0 0 9)))))) (QUOTE |lookupComplete|))) @ \section{category LOGIC Logic} <>= )abbrev category LOGIC Logic ++ Author: ++ Date Created: ++ Change History: ++ Basic Operations: ~, /\, \/ ++ Related Constructors: ++ Keywords: boolean ++ Description: ++ `Logic' provides the basic operations for lattices, ++ e.g., boolean algebra. Logic: Category == BasicType with _~: % -> % ++ ~(x) returns the logical complement of x. _/_\: (%, %) -> % ++ \spadignore { /\ }returns the logical `meet', e.g. `and'. _\_/: (%, %) -> % ++ \spadignore{ \/ } returns the logical `join', e.g. `or'. add _\_/(x: %,y: %) == _~( _/_\(_~(x), _~(y))) @ \section{domain BOOLEAN Boolean} <>= )abbrev domain BOOLEAN Boolean ++ Author: Stephen M. Watt ++ Date Created: ++ Change History: ++ Basic Operations: true, false, not, and, or, xor, nand, nor, implies, ^ ++ Related Constructors: ++ Keywords: boolean ++ Description: \spadtype{Boolean} is the elementary logic with 2 values: ++ true and false Boolean(): Join(OrderedSet, Finite, Logic, ConvertibleTo InputForm) with true : constant -> % ++ true is a logical constant. false : constant -> % ++ false is a logical constant. _^ : % -> % ++ ^ n returns the negation of n. _not : % -> % ++ not n returns the negation of n. _and : (%, %) -> % ++ a and b returns the logical {\em and} of Boolean \spad{a} and b. _or : (%, %) -> % ++ a or b returns the logical inclusive {\em or} ++ of Boolean \spad{a} and b. xor : (%, %) -> % ++ xor(a,b) returns the logical exclusive {\em or} ++ of Boolean \spad{a} and b. nand : (%, %) -> % ++ nand(a,b) returns the logical negation of \spad{a} and b. nor : (%, %) -> % ++ nor(a,b) returns the logical negation of \spad{a} or b. implies: (%, %) -> % ++ implies(a,b) returns the logical implication ++ of Boolean \spad{a} and b. test: % -> Boolean ++ test(b) returns b and is provided for compatibility with the new compiler. == add nt: % -> % test a == a pretend Boolean nt b == (b pretend Boolean => false; true) true == EQ(2,2)$Lisp --well, 1 is rather special false == NIL$Lisp sample() == true not b == (test b => false; true) _^ b == (test b => false; true) _~ b == (test b => false; true) _and(a, b) == (test a => b; false) _/_\(a, b) == (test a => b; false) _or(a, b) == (test a => true; b) _\_/(a, b) == (test a => true; b) xor(a, b) == (test a => nt b; b) nor(a, b) == (test a => false; nt b) nand(a, b) == (test a => nt b; true) a = b == BooleanEquality(a, b)$Lisp implies(a, b) == (test a => b; true) a < b == (test b => not(test a);false) size() == 2 index i == even?(i::Integer) => false true lookup a == a pretend Boolean => 1 2 random() == even?(random()$Integer) => false true convert(x:%):InputForm == x pretend Boolean => convert("true"::Symbol) convert("false"::Symbol) coerce(x:%):OutputForm == x pretend Boolean => message "true" message "false" @ \section{BOOLEAN.lsp} {\bf BOOLEAN} depends on {\bf ORDSET} which depends on {\bf SETCAT} which depends on {\bf BASTYPE} which depends on {\bf BOOLEAN}. We need to break this cycle to build the algebra. So we keep a cached copy of the translated BOOLEAN domain which we can write into the {\bf MID} directory. We compile the lisp code and copy the {\bf BOOLEAN.o} file to the {\bf OUT} directory. This is eventually forcibly replaced by a recompiled version. <>= (|/VERSIONCHECK| 2) (PUT (QUOTE |BOOLEAN;test;2$;1|) (QUOTE |SPADreplace|) (QUOTE (XLAM (|a|) |a|))) (DEFUN |BOOLEAN;test;2$;1| (|a| |$|) |a|) (DEFUN |BOOLEAN;nt| (|b| |$|) (COND (|b| (QUOTE NIL)) ((QUOTE T) (QUOTE T)))) (PUT (QUOTE |BOOLEAN;true;$;3|) (QUOTE |SPADreplace|) (QUOTE (XLAM NIL (QUOTE T)))) (DEFUN |BOOLEAN;true;$;3| (|$|) (QUOTE T)) (PUT (QUOTE |BOOLEAN;false;$;4|) (QUOTE |SPADreplace|) (QUOTE (XLAM NIL NIL))) (DEFUN |BOOLEAN;false;$;4| (|$|) NIL) (DEFUN |BOOLEAN;not;2$;5| (|b| |$|) (COND (|b| (QUOTE NIL)) ((QUOTE T) (QUOTE T)))) (DEFUN |BOOLEAN;^;2$;6| (|b| |$|) (COND (|b| (QUOTE NIL)) ((QUOTE T) (QUOTE T)))) (DEFUN |BOOLEAN;~;2$;7| (|b| |$|) (COND (|b| (QUOTE NIL)) ((QUOTE T) (QUOTE T)))) (DEFUN |BOOLEAN;and;3$;8| (|a| |b| |$|) (COND (|a| |b|) ((QUOTE T) (QUOTE NIL)))) (DEFUN |BOOLEAN;/\\;3$;9| (|a| |b| |$|) (COND (|a| |b|) ((QUOTE T) (QUOTE NIL)))) (DEFUN |BOOLEAN;or;3$;10| (|a| |b| |$|) (COND (|a| (QUOTE T)) ((QUOTE T) |b|))) (DEFUN |BOOLEAN;\\/;3$;11| (|a| |b| |$|) (COND (|a| (QUOTE T)) ((QUOTE T) |b|))) (DEFUN |BOOLEAN;xor;3$;12| (|a| |b| |$|) (COND (|a| (|BOOLEAN;nt| |b| |$|)) ((QUOTE T) |b|))) (DEFUN |BOOLEAN;nor;3$;13| (|a| |b| |$|) (COND (|a| (QUOTE NIL)) ((QUOTE T) (|BOOLEAN;nt| |b| |$|)))) (DEFUN |BOOLEAN;nand;3$;14| (|a| |b| |$|) (COND (|a| (|BOOLEAN;nt| |b| |$|)) ((QUOTE T) (QUOTE T)))) (PUT (QUOTE |BOOLEAN;=;3$;15|) (QUOTE |SPADreplace|) (QUOTE |BooleanEquality|)) (DEFUN |BOOLEAN;=;3$;15| (|a| |b| |$|) (|BooleanEquality| |a| |b|)) (DEFUN |BOOLEAN;implies;3$;16| (|a| |b| |$|) (COND (|a| |b|) ((QUOTE T) (QUOTE T)))) (DEFUN |BOOLEAN;<;3$;17| (|a| |b| |$|) (COND (|b| (COND (|a| (QUOTE NIL)) ((QUOTE T) (QUOTE T)))) ((QUOTE T) (QUOTE NIL)))) (PUT (QUOTE |BOOLEAN;size;Nni;18|) (QUOTE |SPADreplace|) (QUOTE (XLAM NIL 2))) (DEFUN |BOOLEAN;size;Nni;18| (|$|) 2) (DEFUN |BOOLEAN;index;Pi$;19| (|i| |$|) (COND ((SPADCALL |i| (QREFELT |$| 26)) (QUOTE NIL)) ((QUOTE T) (QUOTE T)))) (DEFUN |BOOLEAN;lookup;$Pi;20| (|a| |$|) (COND (|a| 1) ((QUOTE T) 2))) (DEFUN |BOOLEAN;random;$;21| (|$|) (COND ((SPADCALL (|random|) (QREFELT |$| 26)) (QUOTE NIL)) ((QUOTE T) (QUOTE T)))) (DEFUN |BOOLEAN;convert;$If;22| (|x| |$|) (COND (|x| (SPADCALL (SPADCALL "true" (QREFELT |$| 33)) (QREFELT |$| 35))) ((QUOTE T) (SPADCALL (SPADCALL "false" (QREFELT |$| 33)) (QREFELT |$| 35))))) (DEFUN |BOOLEAN;coerce;$Of;23| (|x| |$|) (COND (|x| (SPADCALL "true" (QREFELT |$| 38))) ((QUOTE T) (SPADCALL "false" (QREFELT |$| 38))))) (DEFUN |Boolean| NIL (PROG NIL (RETURN (PROG (#1=#:G82461) (RETURN (COND ((LETT #1# (HGET |$ConstructorCache| (QUOTE |Boolean|)) |Boolean|) (|CDRwithIncrement| (CDAR #1#))) ((QUOTE T) (|UNWIND-PROTECT| (PROG1 (CDDAR (HPUT |$ConstructorCache| (QUOTE |Boolean|) (LIST (CONS NIL (CONS 1 (|Boolean;|)))))) (LETT #1# T |Boolean|)) (COND ((NOT #1#) (HREM |$ConstructorCache| (QUOTE |Boolean|)))))))))))) (DEFUN |Boolean;| NIL (PROG (|dv$| |$| |pv$|) (RETURN (PROGN (LETT |dv$| (QUOTE (|Boolean|)) . #1=(|Boolean|)) (LETT |$| (GETREFV 41) . #1#) (QSETREFV |$| 0 |dv$|) (QSETREFV |$| 3 (LETT |pv$| (|buildPredVector| 0 0 NIL) . #1#)) (|haddProp| |$ConstructorCache| (QUOTE |Boolean|) NIL (CONS 1 |$|)) (|stuffDomainSlots| |$|) |$|)))) (MAKEPROP (QUOTE |Boolean|) (QUOTE |infovec|) (LIST (QUOTE #(NIL NIL NIL NIL NIL NIL (|Boolean|) |BOOLEAN;test;2$;1| (CONS IDENTITY (FUNCALL (|dispatchFunction| |BOOLEAN;true;$;3|) |$|)) (CONS IDENTITY (FUNCALL (|dispatchFunction| |BOOLEAN;false;$;4|) |$|)) |BOOLEAN;not;2$;5| |BOOLEAN;^;2$;6| |BOOLEAN;~;2$;7| |BOOLEAN;and;3$;8| |BOOLEAN;/\\;3$;9| |BOOLEAN;or;3$;10| |BOOLEAN;\\/;3$;11| |BOOLEAN;xor;3$;12| |BOOLEAN;nor;3$;13| |BOOLEAN;nand;3$;14| |BOOLEAN;=;3$;15| |BOOLEAN;implies;3$;16| |BOOLEAN;<;3$;17| (|NonNegativeInteger|) |BOOLEAN;size;Nni;18| (|Integer|) (0 . |even?|) (|PositiveInteger|) |BOOLEAN;index;Pi$;19| |BOOLEAN;lookup;$Pi;20| |BOOLEAN;random;$;21| (|String|) (|Symbol|) (5 . |coerce|) (|InputForm|) (10 . |convert|) |BOOLEAN;convert;$If;22| (|OutputForm|) (15 . |message|) |BOOLEAN;coerce;$Of;23| (|SingleInteger|))) (QUOTE #(|~=| 20 |~| 26 |xor| 31 |true| 37 |test| 41 |size| 46 |random| 50 |or| 54 |not| 60 |nor| 65 |nand| 71 |min| 77 |max| 83 |lookup| 89 |latex| 94 |index| 99 |implies| 104 |hash| 110 |false| 115 |convert| 119 |coerce| 124 |and| 129 |^| 135 |\\/| 140 |>=| 146 |>| 152 |=| 158 |<=| 164 |<| 170 |/\\| 176)) (QUOTE NIL) (CONS (|makeByteWordVec2| 1 (QUOTE (0 0 0 0 0 0 0))) (CONS (QUOTE #(|OrderedSet&| NIL |Logic&| |SetCategory&| NIL |BasicType&| NIL)) (CONS (QUOTE #((|OrderedSet|) (|Finite|) (|Logic|) (|SetCategory|) (|ConvertibleTo| 34) (|BasicType|) (|CoercibleTo| 37))) (|makeByteWordVec2| 40 (QUOTE (1 25 6 0 26 1 32 0 31 33 1 34 0 32 35 1 37 0 31 38 2 0 6 0 0 1 1 0 0 0 12 2 0 0 0 0 17 0 0 0 8 1 0 6 0 7 0 0 23 24 0 0 0 30 2 0 0 0 0 15 1 0 0 0 10 2 0 0 0 0 18 2 0 0 0 0 19 2 0 0 0 0 1 2 0 0 0 0 1 1 0 27 0 29 1 0 31 0 1 1 0 0 27 28 2 0 0 0 0 21 1 0 40 0 1 0 0 0 9 1 0 34 0 36 1 0 37 0 39 2 0 0 0 0 13 1 0 0 0 11 2 0 0 0 0 16 2 0 6 0 0 1 2 0 6 0 0 1 2 0 6 0 0 20 2 0 6 0 0 1 2 0 6 0 0 22 2 0 0 0 0 14)))))) (QUOTE |lookupComplete|))) (MAKEPROP (QUOTE |Boolean|) (QUOTE NILADIC) T) @ \section{domain IBITS IndexedBits} <>= )abbrev domain IBITS IndexedBits ++ Author: Stephen Watt and Michael Monagan ++ Date Created: ++ July 86 ++ Change History: ++ Oct 87 ++ Basic Operations: range ++ Related Constructors: ++ Keywords: indexed bits ++ Description: \spadtype{IndexedBits} is a domain to compactly represent ++ large quantities of Boolean data. IndexedBits(mn:Integer): BitAggregate() with -- temporaries until parser gets better Not: % -> % ++ Not(n) returns the bit-by-bit logical {\em Not} of n. Or : (%, %) -> % ++ Or(n,m) returns the bit-by-bit logical {\em Or} of ++ n and m. And: (%, %) -> % ++ And(n,m) returns the bit-by-bit logical {\em And} of ++ n and m. == add range: (%, Integer) -> Integer --++ range(j,i) returnes the range i of the boolean j. minIndex u == mn range(v, i) == i >= 0 and i < #v => i error "Index out of range" coerce(v):OutputForm == t:Character := char "1" f:Character := char "0" s := new(#v, space()$Character)$String for i in minIndex(s)..maxIndex(s) for j in mn.. repeat s.i := if v.j then t else f s::OutputForm new(n, b) == BVEC_-MAKE_-FULL(n,TRUTH_-TO_-BIT(b)$Lisp)$Lisp empty() == BVEC_-MAKE_-FULL(0,0)$Lisp copy v == BVEC_-COPY(v)$Lisp #v == BVEC_-SIZE(v)$Lisp v = u == BVEC_-EQUAL(v, u)$Lisp v < u == BVEC_-GREATER(u, v)$Lisp _and(u, v) == (#v=#u => BVEC_-AND(v,u)$Lisp; map("and",v,u)) _or(u, v) == (#v=#u => BVEC_-OR(v, u)$Lisp; map("or", v,u)) xor(v,u) == (#v=#u => BVEC_-XOR(v,u)$Lisp; map("xor",v,u)) setelt(v:%, i:Integer, f:Boolean) == BVEC_-SETELT(v, range(v, i-mn), TRUTH_-TO_-BIT(f)$Lisp)$Lisp elt(v:%, i:Integer) == BIT_-TO_-TRUTH(BVEC_-ELT(v, range(v, i-mn))$Lisp)$Lisp Not v == BVEC_-NOT(v)$Lisp And(u, v) == (#v=#u => BVEC_-AND(v,u)$Lisp; map("and",v,u)) Or(u, v) == (#v=#u => BVEC_-OR(v, u)$Lisp; map("or", v,u)) @ \section{domain BITS Bits} <>= )abbrev domain BITS Bits ++ Author: Stephen M. Watt ++ Date Created: ++ Change History: ++ Basic Operations: And, Not, Or ++ Related Constructors: ++ Keywords: bits ++ Description: \spadtype{Bits} provides logical functions for Indexed Bits. Bits(): Exports == Implementation where Exports == BitAggregate() with bits: (NonNegativeInteger, Boolean) -> % ++ bits(n,b) creates bits with n values of b Implementation == IndexedBits(1) add bits(n,b) == new(n,b) @ \section{License} <>= --Copyright (c) 1991-2002, The Numerical ALgorithms Group Ltd. --All rights reserved. -- --Redistribution and use in source and binary forms, with or without --modification, are permitted provided that the following conditions are --met: -- -- - Redistributions of source code must retain the above copyright -- notice, this list of conditions and the following disclaimer. -- -- - Redistributions in binary form must reproduce the above copyright -- notice, this list of conditions and the following disclaimer in -- the documentation and/or other materials provided with the -- distribution. -- -- - Neither the name of The Numerical ALgorithms Group Ltd. nor the -- names of its contributors may be used to endorse or promote products -- derived from this software without specific prior written permission. -- --THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS --IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED --TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A --PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER --OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, --EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, --PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR --PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF --LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING --NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS --SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. @ <<*>>= <> <> <> <> <> <> @ \eject \begin{thebibliography}{99} \bibitem{1} nothing \end{thebibliography} \end{document}