\documentclass{article} \usepackage{open-axiom} \title{src/algebra boolean.spad} \author{Stephen M. Watt, Michael Monagan, Gabriel Dos~Reis} \begin{document} \maketitle \begin{abstract} \end{abstract} \tableofcontents \eject \section{domain REF Reference} <>= )abbrev domain REF Reference ++ Author: Stephen M. Watt ++ Date Created: ++ Date Last Changed: October 11, 2011 ++ Basic Operations: deref, ref, setref, = ++ Related Constructors: ++ Keywords: reference ++ Description: \spadtype{Reference} is for making a changeable instance ++ of something. Reference(S:Type): SetCategory with ref : S -> % ++ \spad{ref(s)} creates a reference to the object \spad{s}. deref : % -> S ++ \spad{deref(r)} returns the object referenced by \spad{r} setref: (%, S) -> S ++ setref(r,s) reset the reference \spad{r} to refer to \spad{s} = : (%, %) -> Boolean ++ \spad{a=b} tests if \spad{a} and \spad{b} are equal. == add Rep == Record(value: S) import %peq: (%,%) -> Boolean from Foreign Builtin p = q == %peq(p,q) ref v == per [v] deref p == rep(p).value setref(p, v) == rep(p).value := v coerce p == obj := S has CoercibleTo OutputForm => rep(p).value::OutputForm '?::OutputForm prefix('ref::OutputForm, [obj]) @ \section{domain BOOLEAN Boolean} <>= )abbrev domain BOOLEAN Boolean ++ Author: Stephen M. Watt ++ Date Created: ++ Date Last Changed: May 27, 2009 ++ 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(OrderedFinite, PropositionalLogic, ConvertibleTo InputForm) with 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. == add import %false: % from Foreign Builtin import %true: % from Foreign Builtin import %peq: (%,%) -> Boolean from Foreign Builtin import %and: (%,%) -> % from Foreign Builtin import %or: (%,%) -> % from Foreign Builtin import %not: % -> % from Foreign Builtin true == %true false == %false not b == %not b ~b == %not b a and b == %and(a,b) a /\ b == %and(a,b) a or b == %or(a,b) a \/ b == %or(a,b) xor(a, b) == (a => %not b; b) nor(a, b) == (a => %false; %not b) nand(a, b) == (a => %not b; %true) a = b == %peq(a,b) implies(a, b) == (a => b; %true) equiv(a,b) == %peq(a, b) a < b == (b => %not a; %false) size() == 2 index i == even?(i::Integer) => %false %true lookup a == a => 1 2 random() == zero? random(2)$Integer => %false %true convert(x:%):InputForm == x => 'true 'false coerce(x:%):OutputForm == x => 'true 'false @ \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() == add import %2bool: NonNegativeInteger -> Boolean from Foreign Builtin import %2bit: Boolean -> NonNegativeInteger from Foreign Builtin import %bitveccopy: % -> % from Foreign Builtin import %bitveclength: % -> NonNegativeInteger from Foreign Builtin import %bitvecref: (%,Integer) -> NonNegativeInteger from Foreign Builtin import %bitveceq: (%,%) -> Boolean from Foreign Builtin import %bitvecnot: % -> % from Foreign Builtin import %bitvecand: (%,%) -> % from Foreign Builtin import %bitvecor: (%,%) -> % from Foreign Builtin import %bitvecxor: (%,%) -> % from Foreign Builtin import %bitvector: (NonNegativeInteger,NonNegativeInteger) -> % from Foreign Builtin minIndex u == mn -- range check index of `i' into `v'. range(v: %, i: Integer): Integer == 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) == %bitvector(n, %2bit(b)$Foreign(Builtin)) empty() == %bitvector(0,0) copy v == %bitveccopy v #v == %bitveclength v v = u == %bitveceq(v,u) u < v == -- lexicographic nu := #u nv := #v for i in 0.. repeat i >= nu => return or/[%bitvecref(v,j) = 1 for j in i..nv-1] i >= nv => return false %bitvecref(u,i) < %bitvecref(v,i) => return true %bitvecref(u,i) > %bitvecref(v,i) => return false u and v == (#v=#u => %bitvecand(v,u); map("and",v,u)) u or v == (#v=#u => %bitvecor(v,u); map("or", v,u)) xor(v,u) == (#v=#u => %bitvecxor(v,u); map("xor",v,u)) setelt(v:%, i:Integer, f:Boolean) == %2bool %store(%bitvecref(v,range(v,i-mn)),%2bit f)$Foreign(Builtin) elt(v:%, i:Integer) == %2bool %bitvecref(v,range(v,i-mn)) ~v == %bitvecnot v u /\ v == (#v=#u => %bitvecand(v,u); map("and",v,u)) u \/ v == (#v=#u => %bitvecor(v,u); 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. --Copyright (C) 2007-2012, Gabriel Dos Reis. --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}