open-axiom repository from github
\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}