path: root/src/algebra/boolean.spad.pamphlet

\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}
<<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}
<<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}
<<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}
<<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}

<<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.
@
<<*>>=
<<license>>

<<domain BOOLEAN Boolean>>

<<domain IBITS IndexedBits>>
<<domain BITS Bits>>
<<domain REF Reference>>

@
\eject
\begin{thebibliography}{99}
\bibitem{1} nothing
\end{thebibliography}
\end{document}