* algebra/catdef.spad.pamphlet (Finite) [random]: Provide default

	implementation. 
	* algebra/boolean.spad.pamphlet (KleeneTrivalentLogic): Now
	satisfy Finite.  Use Maybe Boolean as representation.

2 files changed, 38 insertions, 16 deletions

diff --git a/src/algebra/boolean.spad.pamphlet b/src/algebra/boolean.spad.pamphlet
index e3c6ab7f..dcdf0562 100644
--- a/src/algebra/boolean.spad.pamphlet
+++ b/src/algebra/boolean.spad.pamphlet
@@ -611,11 +611,11 @@ Bits(): Exports == Implementation where
 )abbrev domain KTVLOGIC KleeneTrivalentLogic
 ++ Author: Gabriel Dos Reis
 ++ Date Created: September 20, 2008
-++ Date Last Modified: May 27, 2009
+++ Date Last Modified: January 14, 2012
 ++ Description: 
 ++   This domain implements Kleene's 3-valued propositional logic.
 KleeneTrivalentLogic(): Public == Private where
-  Public == PropositionalLogic with
+  Public == Join(PropositionalLogic,Finite) with
     unknown: %     ++ the indefinite `unknown' 
     case: (%,[| false |]) -> Boolean
       ++ x case false holds if the value of `x' is `false'
@@ -623,54 +623,69 @@ KleeneTrivalentLogic(): Public == Private where
       ++ x case unknown holds if the value of `x' is `unknown'
     case: (%,[| true |]) -> Boolean
       ++ s case true holds if the value of `x' is `true'.
-  Private == add
-    Rep == Byte    -- We need only 3 bits, in fact.
-    false == per(0::Byte)
-    unknown == per(1::Byte)
-    true == per(2::Byte)
+  Private == Maybe Boolean add
+    false == per just(false@Boolean)
+    unknown == per nothing
+    true == per just(true@Boolean)
     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
+      case rep x is
+        y@Boolean => y::OutputForm
+        otherwise => outputForm 'unknown
+
+    size() == 3
+
+    index n ==
+      n > 3 => error "index: argument out of bound"
+      n = 1 => false
+      n = 2 => unknown
+      true
+
+    lookup x ==
+      x = false => 1
+      x = unknown => 2
+      3
 @
 
-
-
-
 \section{License}
 
 <<license>>=
 --Copyright (c) 1991-2002, The Numerical Algorithms Group Ltd.
 --All rights reserved.
---Copyright (C) 2007-2010, Gabriel Dos Reis.
+--Copyright (C) 2007-2012, Gabriel Dos Reis.
 --All rights reserved.
 --
 --Redistribution and use in source and binary forms, with or without
diff --git a/src/algebra/catdef.spad.pamphlet b/src/algebra/catdef.spad.pamphlet
index e546bb01..6fae2576 100644
--- a/src/algebra/catdef.spad.pamphlet
+++ b/src/algebra/catdef.spad.pamphlet
@@ -915,7 +915,6 @@ Field(): Category == Join(EuclideanDomain,UniqueFactorizationDomain,
 ++   \spad{index(lookup(s)) = s}
 
 Finite(): Category == SetCategory with
-    --operations
       size: () ->  NonNegativeInteger
         ++ size() returns the number of elements in the set.
       index: PositiveInteger -> %
@@ -928,7 +927,15 @@ Finite(): Category == SetCategory with
         ++ \spad{x = index lookup x}.
       random: () -> %
         ++ random() returns a random element from the set.
-
+  add
+      --FIXME: Tthe only purpose of this local function is to bring
+      --FIXME: the compiler to admission that the successor of a
+      --FIXME: nonnegative integer has positive value.
+      --FIXME: Take it out when the its logic is sufficiently advanced.
+      succ(x: NonNegativeInteger): PositiveInteger ==
+        (1 + x) : PositiveInteger
+      random() ==
+        index succ random(size())$NonNegativeInteger
 @
 \section{category FLINEXP FullyLinearlyExplicitRingOver}
 <<category FLINEXP FullyLinearlyExplicitRingOver>>=