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

1 files changed, 107 insertions, 46 deletions

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}