aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authordos-reis <gdr@axiomatics.org>2008-09-21 03:35:55 +0000
committerdos-reis <gdr@axiomatics.org>2008-09-21 03:35:55 +0000
commitfd8c12056474ecab97015eff9cdadd4bd77b5fd5 (patch)
tree9e6106481e73d5cd1b78e7653e8414d585ef76ab /src
parentfde9260a842114ae27a99f7de23c9a46b79eccf4 (diff)
downloadopen-axiom-fd8c12056474ecab97015eff9cdadd4bd77b5fd5.tar.gz
* interp/sys-macros.lisp (|byteEqual|): New.
* algebra/boolean.spad.pamphlet (PropositionalLogic): Extend SetCategory. (PropositionalFormula): Now unconditional exports coercion to OutputForm. Adjust implementation. (KleeneTrivalentLogic): New. * algebra/data.spad.pamphlet (Byte): Tidy. * algebra/Makefile.pamphlet (axiom_algebra_layer_0): Move PROPLOG to layer 1.
Diffstat (limited to 'src')
-rw-r--r--src/ChangeLog12
-rw-r--r--src/algebra/Makefile.in6
-rw-r--r--src/algebra/Makefile.pamphlet6
-rw-r--r--src/algebra/boolean.spad.pamphlet153
-rw-r--r--src/algebra/data.spad.pamphlet5
-rw-r--r--src/interp/sys-macros.lisp7
6 files changed, 134 insertions, 55 deletions
diff --git a/src/ChangeLog b/src/ChangeLog
index 7c0491fc..ef3796f0 100644
--- a/src/ChangeLog
+++ b/src/ChangeLog
@@ -1,5 +1,17 @@
2008-09-20 Gabriel Dos Reis <gdr@cs.tamu.edu>
+ * interp/sys-macros.lisp (|byteEqual|): New.
+ * algebra/boolean.spad.pamphlet (PropositionalLogic): Extend
+ SetCategory.
+ (PropositionalFormula): Now unconditional exports coercion to
+ OutputForm. Adjust implementation.
+ (KleeneTrivalentLogic): New.
+ * algebra/data.spad.pamphlet (Byte): Tidy.
+ * algebra/Makefile.pamphlet (axiom_algebra_layer_0): Move PROPLOG
+ to layer 1.
+
+2008-09-20 Gabriel Dos Reis <gdr@cs.tamu.edu>
+
* include/cfuns.h (oa_dirname): Declare.
* lib/cfuns-c.c (openaxiom_is_path_separator): New.
(oa_dirname): Define.
diff --git a/src/algebra/Makefile.in b/src/algebra/Makefile.in
index 0da21709..4dab8997 100644
--- a/src/algebra/Makefile.in
+++ b/src/algebra/Makefile.in
@@ -358,7 +358,7 @@ axiom_algebra_layer_0 = \
AHYP ATTREG CFCAT ELTAB KOERCE KONVERT \
MSYSCMD OM OMCONN OMDEV OUT \
PRIMCAT PRINT PTRANFN SPFCAT TYPE UTYPE \
- PROPLOG PROPERTY BASTYPE BASTYPE- CATEGORY LMODULE \
+ PROPERTY BASTYPE BASTYPE- CATEGORY LMODULE \
RMODULE FINITE STEP SGROUP SGROUP- ABELSG \
ABELSG- ORDSET ORDSET- FNCAT FILECAT SEXCAT \
MKBCFUNC MKRECORD MKUCFUNC DROPT1 PLOT1 ITFUN2 \
@@ -376,7 +376,7 @@ axiom_algebra_layer_1 = \
PATAB PPCURVE PSCURVE REAL RESLATC RETRACT \
RETRACT- SEGCAT BINDING SYNTAX BMODULE LOGIC \
LOGIC- EVALAB EVALAB- FEVALAB FEVALAB- BYTE \
- OSGROUP MAYBE DATABUF
+ OSGROUP MAYBE DATABUF PROPLOG
axiom_algebra_layer_1_nrlibs = \
$(addsuffix .NRLIB/code.$(FASLEXT),$(axiom_algebra_layer_1))
@@ -387,7 +387,7 @@ axiom_algebra_layer_1_objects = \
axiom_algebra_layer_2 = \
ELTAGG ELTAGG- FMC FMFUN FORTFN FVC \
CTORCALL FVFUN INTRET IXAGG IXAGG- SEGXCAT \
- CONTOUR LIST3 MKFUNC OASGP
+ CONTOUR LIST3 MKFUNC OASGP KTVLOGIC
axiom_algebra_layer_2_nrlibs = \
$(addsuffix .NRLIB/code.$(FASLEXT),$(axiom_algebra_layer_2))
diff --git a/src/algebra/Makefile.pamphlet b/src/algebra/Makefile.pamphlet
index 3c489670..d34998bd 100644
--- a/src/algebra/Makefile.pamphlet
+++ b/src/algebra/Makefile.pamphlet
@@ -187,7 +187,7 @@ axiom_algebra_layer_0 = \
AHYP ATTREG CFCAT ELTAB KOERCE KONVERT \
MSYSCMD OM OMCONN OMDEV OUT \
PRIMCAT PRINT PTRANFN SPFCAT TYPE UTYPE \
- PROPLOG PROPERTY BASTYPE BASTYPE- CATEGORY LMODULE \
+ PROPERTY BASTYPE BASTYPE- CATEGORY LMODULE \
RMODULE FINITE STEP SGROUP SGROUP- ABELSG \
ABELSG- ORDSET ORDSET- FNCAT FILECAT SEXCAT \
MKBCFUNC MKRECORD MKUCFUNC DROPT1 PLOT1 ITFUN2 \
@@ -219,7 +219,7 @@ axiom_algebra_layer_1 = \
PATAB PPCURVE PSCURVE REAL RESLATC RETRACT \
RETRACT- SEGCAT BINDING SYNTAX BMODULE LOGIC \
LOGIC- EVALAB EVALAB- FEVALAB FEVALAB- BYTE \
- OSGROUP MAYBE DATABUF
+ OSGROUP MAYBE DATABUF PROPLOG
axiom_algebra_layer_1_nrlibs = \
$(addsuffix .NRLIB/code.$(FASLEXT),$(axiom_algebra_layer_1))
@@ -237,7 +237,7 @@ axiom_algebra_layer_1_objects = \
axiom_algebra_layer_2 = \
ELTAGG ELTAGG- FMC FMFUN FORTFN FVC \
CTORCALL FVFUN INTRET IXAGG IXAGG- SEGXCAT \
- CONTOUR LIST3 MKFUNC OASGP
+ CONTOUR LIST3 MKFUNC OASGP KTVLOGIC
axiom_algebra_layer_2_nrlibs = \
$(addsuffix .NRLIB/code.$(FASLEXT),$(axiom_algebra_layer_2))
diff --git a/src/algebra/boolean.spad.pamphlet b/src/algebra/boolean.spad.pamphlet
index ab33ba62..b9cb64cb 100644
--- a/src/algebra/boolean.spad.pamphlet
+++ b/src/algebra/boolean.spad.pamphlet
@@ -17,10 +17,10 @@
)abbrev category PROPLOG PropositionalLogic
++ Author: Gabriel Dos Reis
++ Date Created: Januray 14, 2008
-++ Date Last Modified: January 14, 2008
+++ Date Last Modified: September 20, 2008
++ Description: This category declares the connectives of
++ Propositional Logic.
-PropositionalLogic(): Category == with
+PropositionalLogic(): Category == SetCategory with
"not": % -> %
++ not p returns the logical negation of `p'.
"and": (%, %) -> %
@@ -43,7 +43,6 @@ PropositionalLogic(): Category == with
++ Description: This domain implements propositional formula build
++ over a term domain, that itself belongs to PropositionalLogic
PropositionalFormula(T: PropositionalLogic): PropositionalLogic with
- if T has CoercibleTo OutputForm then CoercibleTo OutputForm
coerce: T -> %
++ coerce(t) turns the term `t' into a propositional formula
coerce: Symbol -> %
@@ -236,47 +235,46 @@ PropositionalFormula(T: PropositionalLogic): PropositionalLogic with
-- Term
-- implies(Formula, Formula)
-- equiv(Formula, Formula)
- if T has CoercibleTo OutputForm then
- formula: % -> OutputForm
- coerce(p: %): OutputForm ==
- formula p
-
- primaryFormula(p: %): OutputForm ==
- term? p => term(p)::OutputForm
- variable? p => variable(p)::OutputForm
- if rep p case binForm then
- p' := (rep p).binForm
- p'.op = 'implies or p'.op = 'equiv =>
- return elt(outputForm p'.op,
- [formula p'.lhs, formula p'.rhs])$OutputForm
- paren(formula p)$OutputForm
-
- notFormula(p: %): OutputForm ==
- not? p =>
- elt(outputForm '_not, [notFormula((rep p).unForm)])$OutputForm
- primaryFormula p
-
- andFormula(p: %): OutputForm ==
- and? p =>
- p' := (rep p).binForm
- -- ??? idealy, we should be using `and$OutputForm' but
- -- ??? a bug in the compiler currently prevents that.
- infix(outputForm '_and, notFormula p'.lhs,
- andFormula p'.rhs)$OutputForm
- notFormula p
-
- orFormula(p: %): OutputForm ==
- or? p =>
- p' := (rep p).binForm
- -- ??? idealy, we should be using `or$OutputForm' but
- -- ??? a bug in the compiler currently prevents that.
- infix(outputForm '_or, andFormula p'.lhs,
- orFormula p'.rhs)$OutputForm
- andFormula p
-
- formula p ==
- -- Note: this should be equivFormula, but see the explanation above.
- orFormula p
+ formula: % -> OutputForm
+ coerce(p: %): OutputForm ==
+ formula p
+
+ primaryFormula(p: %): OutputForm ==
+ term? p => term(p)::OutputForm
+ variable? p => variable(p)::OutputForm
+ if rep p case binForm then
+ p' := (rep p).binForm
+ p'.op = 'implies or p'.op = 'equiv =>
+ return elt(outputForm p'.op,
+ [formula p'.lhs, formula p'.rhs])$OutputForm
+ paren(formula p)$OutputForm
+
+ notFormula(p: %): OutputForm ==
+ not? p =>
+ elt(outputForm '_not, [notFormula((rep p).unForm)])$OutputForm
+ primaryFormula p
+
+ andFormula(p: %): OutputForm ==
+ and? p =>
+ p' := (rep p).binForm
+ -- ??? idealy, we should be using `and$OutputForm' but
+ -- ??? a bug in the compiler currently prevents that.
+ infix(outputForm '_and, notFormula p'.lhs,
+ andFormula p'.rhs)$OutputForm
+ notFormula p
+
+ orFormula(p: %): OutputForm ==
+ or? p =>
+ p' := (rep p).binForm
+ -- ??? idealy, we should be using `or$OutputForm' but
+ -- ??? a bug in the compiler currently prevents that.
+ infix(outputForm '_or, andFormula p'.lhs,
+ orFormula p'.rhs)$OutputForm
+ andFormula p
+
+ formula p ==
+ -- Note: this should be equivFormula, but see the explanation above.
+ orFormula p
@
@@ -501,9 +499,70 @@ Bits(): Exports == Implementation where
bits(n,b) == new(n,b)
@
+
+
+\section{Kleene's Three-Valued Logic}
+<<domain KTVLOGIC KleeneTrivalentLogic>>=
+)abbrev domain KTVLOGIC KleeneTrivalentLogic
+++ Author: Gabriel Dos Reis
+++ Date Created: September 20, 2008
+++ Date Last Modified: September 20, 2008
+++ Description:
+++ This domain implements Kleene's 3-valued propositional logic.
+KleeneTrivalentLogic(): Public == Private where
+ Public == PropositionalLogic with
+ false: %
+ unknown: %
+ true: %
+ _case: (%,[| false |]) -> Boolean
+ _case: (%,[| unknown |]) -> Boolean
+ _case: (%,[| true |]) -> Boolean
+ Private == add
+ Rep == Byte -- We need only 3 bits, in fact.
+ false == per(0::NonNegativeInteger::Byte)
+ unknown == per(1::NonNegativeInteger::Byte)
+ true == per(2::Byte)
+ x = y == rep x = rep y
+ x case true == x = true
+ x case false == x = false
+ x case unknown == x = unknown
+ not x ==
+ x case false => true
+ x case unknown => unknown
+ false
+ x and y ==
+ x case false => false
+ x case unknown =>
+ y case false => false
+ unknown
+ y
+ x or y ==
+ x case false => y
+ x case true => x
+ y case true => y
+ unknown
+ implies(x,y) ==
+ x case false => true
+ x case true => y
+ y case true => true
+ unknown
+ equiv(x,y) ==
+ x case unknown => x
+ x case true => y
+ not y
+ coerce(x: %): OutputForm ==
+ x case true => outputForm 'true
+ x case false => outputForm 'false
+ outputForm 'unknown
+@
+
+
\section{License}
+
<<license>>=
---Copyright (c) 1991-2002, The Numerical ALgorithms Group Ltd.
+--Copyright (c) 1991-2002, The Numerical Algorithms Group Ltd.
+--All rights reserved.
+--Copyright (C) 2007-2008, Gabriel Dos Reis.
--All rights reserved.
--
--Redistribution and use in source and binary forms, with or without
@@ -518,7 +577,7 @@ Bits(): Exports == Implementation where
-- the documentation and/or other materials provided with the
-- distribution.
--
--- - Neither the name of The Numerical ALgorithms Group Ltd. nor the
+-- - 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.
--
@@ -544,6 +603,8 @@ Bits(): Exports == Implementation where
<<domain BITS Bits>>
<<category PROPLOG PropositionalLogic>>
<<domain PROPFRML PropositionalFormula>>
+<<domain KTVLOGIC KleeneTrivalentLogic>>
+
@
\eject
\begin{thebibliography}{99}
diff --git a/src/algebra/data.spad.pamphlet b/src/algebra/data.spad.pamphlet
index 9640d7ad..e3262ef5 100644
--- a/src/algebra/data.spad.pamphlet
+++ b/src/algebra/data.spad.pamphlet
@@ -36,7 +36,7 @@ Byte(): Public == Private where
Private ==> add
byte(x: NonNegativeInteger): % ==
- byteGreaterEqual(x,256$Lisp)$Lisp =>
+ not (x < 256$Lisp) =>
userError "integer value cannot be represented by a byte"
x : %
@@ -48,6 +48,9 @@ Byte(): Public == Private where
coerce(x: %): OutputForm ==
x::NonNegativeInteger::OutputForm
+
+ x = y ==
+ byteEqual(x,y)$Lisp
x < y ==
byteLessThan(x,y)$Lisp
diff --git a/src/interp/sys-macros.lisp b/src/interp/sys-macros.lisp
index cd389841..c53dac73 100644
--- a/src/interp/sys-macros.lisp
+++ b/src/interp/sys-macros.lisp
@@ -62,11 +62,14 @@
;; -*- Byte -*-
;;
+(defmacro |byteEqual| (|x| |y|)
+ `(EQL (the |%Byte| ,|x|) (the |%Byte| ,|y|)))
+
(defmacro |byteLessThan| (|x| |y|)
- `(< (the fixnum ,|x|) (the fixnum ,|y|)))
+ `(< (the |%Byte| ,|x|) (the |%Byte| ,|y|)))
(defmacro |byteGreaterEqual| (|x| |y|)
- `(>= (the fixnum ,|x|) (the fixnum ,|y|)))
+ `(>= (the |%Byte| ,|x|) (the |%Byte| ,|y|)))
;;
;; -*- BigFloat Constructors -*-