* 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.

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 -*-