* algebra/boolean.spad.pamphlet (PropositionalFormula):

	Reimplement in terms of kernels.
	* algebra/Makefile.pamphlet ($(OUT)/KERNEL.$(FASLEXT)): New
	dependence rule.
	($(OUT)PROPFRML.$(FASLEXT)): Likewise.
	(axiom_algebra_layer_19): Move PROPFRML to...
	(axiom_algebra_layer_6): ...here.

4 files changed, 92 insertions, 72 deletions

diff --git a/src/algebra/Makefile.in b/src/algebra/Makefile.in
index 9c0bb482..fc58968f 100644
--- a/src/algebra/Makefile.in
+++ b/src/algebra/Makefile.in
@@ -478,6 +478,9 @@ axiom_algebra_layer_4_nrlibs = \
 axiom_algebra_layer_4_objects = \
 	$(addprefix $(OUT)/, \
 	   $(addsuffix .$(FASLEXT),$(axiom_algebra_layer_4)))
+
+$(OUT)/KERNEL.$(FASLEXT): $(OUT)/KERNEL2.$(FASLEXT)
+
 axiom_algebra_layer_5 = \
            CHARNZ            DVARCAT  DVARCAT- ELEMFUN  \
   ELEMFUN- ESTOOLS2 FCOMP    FPATMAB  IDPAM    IDPO     \
@@ -495,9 +498,10 @@ axiom_algebra_layer_5_objects = \
 	   $(addsuffix .$(FASLEXT),$(axiom_algebra_layer_5)))
 
 $(OUT)/CHARPOL.$(FASLEXT): $(OUT)/SETCAT-.$(FASLEXT)
+$(OUT)PROPFRML.$(FASLEXT): $(OUT)/KERNEL.$(FASLEXT)
 
 axiom_algebra_layer_6 = \
-                   AUTOMOR  CARTEN2 CHARPOL  COMPLEX2 \
+  PROPFRML         AUTOMOR  CARTEN2 CHARPOL  COMPLEX2 \
   DIFEXT  DIFEXT-  ES1      ES2     GRMOD    GRMOD-   \
   HYPCAT  HYPCAT-           MODRING NASRING  NASRING- \
   SORTPAK ZMOD                                        \
@@ -693,7 +697,7 @@ axiom_algebra_layer_14 = \
   TWOFACT  UNIFACT  UP       UPCDEN   \
   UPDECOMP UPDIVP   UPMP     UPOLYC2  \
   UPXSCAT  UPSQFREE VIEWDEF  VIEW2D   \
-  VOID     WEIER    WP       \
+           WEIER    WP       \
  EQTBL  GSTBL   HASHTBL \
   INTABL  INTFTBL  STBL    STRTBL\
   TABLE     FST SYMS     SYMTAB \
@@ -787,7 +791,7 @@ axiom_algebra_layer_19 = \
   SET      SPECOUT  SQMATRIX SWITCH  \
                     SYSSOLP  UTSCAT  \
   UTSCAT-  VARIABLE WFFINTBS SPADPRSR \
-  PARSER   PROPFRML TSETCAT  TSETCAT-
+  PARSER            TSETCAT  TSETCAT-
 
 axiom_algebra_layer_19_nrlibs = \
 	$(addsuffix .NRLIB/code.$(FASLEXT),$(axiom_algebra_layer_19))
diff --git a/src/algebra/Makefile.pamphlet b/src/algebra/Makefile.pamphlet
index 63e3bd9f..b9ea75d0 100644
--- a/src/algebra/Makefile.pamphlet
+++ b/src/algebra/Makefile.pamphlet
@@ -457,6 +457,9 @@ axiom_algebra_layer_4_objects = \
 \subsection{Layer 5}
 
 <<layer5>>=
+
+$(OUT)/KERNEL.$(FASLEXT): $(OUT)/KERNEL2.$(FASLEXT)
+
 axiom_algebra_layer_5 = \
            CHARNZ            DVARCAT  DVARCAT- ELEMFUN  \
   ELEMFUN- ESTOOLS2 FCOMP    FPATMAB  IDPAM    IDPO     \
@@ -479,9 +482,10 @@ axiom_algebra_layer_5_objects = \
 <<layer6>>=
 
 $(OUT)/CHARPOL.$(FASLEXT): $(OUT)/SETCAT-.$(FASLEXT)
+$(OUT)PROPFRML.$(FASLEXT): $(OUT)/KERNEL.$(FASLEXT)
 
 axiom_algebra_layer_6 = \
-                   AUTOMOR  CARTEN2 CHARPOL  COMPLEX2 \
+  PROPFRML         AUTOMOR  CARTEN2 CHARPOL  COMPLEX2 \
   DIFEXT  DIFEXT-  ES1      ES2     GRMOD    GRMOD-   \
   HYPCAT  HYPCAT-           MODRING NASRING  NASRING- \
   SORTPAK ZMOD                                        \
@@ -839,7 +843,7 @@ axiom_algebra_layer_19 = \
   SET      SPECOUT  SQMATRIX SWITCH  \
                     SYSSOLP  UTSCAT  \
   UTSCAT-  VARIABLE WFFINTBS SPADPRSR \
-  PARSER   PROPFRML TSETCAT  TSETCAT-
+  PARSER            TSETCAT  TSETCAT-
 
 axiom_algebra_layer_19_nrlibs = \
 	$(addsuffix .NRLIB/code.$(FASLEXT),$(axiom_algebra_layer_19))
diff --git a/src/algebra/boolean.spad.pamphlet b/src/algebra/boolean.spad.pamphlet
index 08c39765..032655ee 100644
--- a/src/algebra/boolean.spad.pamphlet
+++ b/src/algebra/boolean.spad.pamphlet
@@ -77,65 +77,77 @@ PropositionalFormula(T: SetCategory): Public == Private where
       ++ is an equivalence formula.
 
   Private == add
-    FORMULA ==> Union(base: T, unForm: %,
-                  binForm: Record(op: Symbol, lhs: %, rhs: %))
-
-    Rep == FORMULA
-
-    coerce(t: T): % ==
-      per [t]$FORMULA
+    Rep == Union(T, Kernel %)
+    import Kernel %
+    import BasicOperator
+    import List %
+
+    -- Local names for proposition logical operators
+    macro NOT == '%not
+    macro AND == '%and
+    macro OR == '%OR
+    macro IMP == '%implies
+    macro EQV == '%equiv
+
+    -- Return the nesting level of a formula
+    level(f: %): NonNegativeInteger ==
+      f' := rep f
+      f' case T => 0
+      height f'
+
+    -- A term is a formula
+    coerce(t: T): % == 
+      per t
 
     not p ==
-      per [p]$FORMULA
-
-    binaryForm(o: Symbol, l: %, r: %): % ==
-      per [[o, l, r]$Record(op: Symbol, lhs: %, rhs: %)]$FORMULA
+      per kernel(operator(NOT, 1::Arity), [p], 1 + level p)
 
     p and q ==
-      binaryForm('and, p, q)
+      per kernel(operator(AND, 2), [p, q], 1 + max(level p, level q))
 
     p or q ==
-      binaryForm('or, p, q)
+      per kernel(operator(OR, 2), [p, q], 1 + max(level p, level q))
 
     implies(p,q) ==
-      binaryForm('implies, p, q)
+      per kernel(operator(IMP, 2), [p, q], 1 + max(level p, level q))
 
     equiv(p,q) ==
-      binaryForm('equiv, p, q)
-
-    -- returns true if the proposition `p' is a formula of kind
-    -- indicated by `o'.
-    isBinaryNode?(p: %, o: Symbol): Boolean ==
-      p' := rep p
-      p' case binForm and p'.binForm.op = o
-
-    -- returns the operands of a binary formula node
-    binaryOperands(p: %): Pair(%,%) ==
-      p' := (rep p).binForm
-      pair(p'.lhs,p'.rhs)$Pair(%,%)
+      per kernel(operator(EQV, 2), [p, q], 1 + max(level p, level q))
 
     isTerm f ==
-      rep f case base => just rep(f).base
+      f' := rep f
+      f' case T => just(f'@T)
       nothing
 
     isNot f ==
-      rep f case unForm => just rep(f).unForm
+      f' := rep f
+      f' case Kernel(%) and is?(f', NOT) => just(first argument f')
       nothing
 
+    isBinaryOperator(f: Kernel %, op: Symbol): Maybe Pair(%, %) ==
+      not is?(f, op) => nothing
+      args := argument f
+      just pair(first args, second args)
+
     isAnd f ==
-      isBinaryNode?(f,'and) => just binaryOperands f
+      f' := rep f
+      f' case Kernel % => isBinaryOperator(f', AND)
       nothing
 
     isOr f ==
-      isBinaryNode?(f,'or) => just binaryOperands f
+      f' := rep f
+      f' case Kernel % => isBinaryOperator(f', OR)
       nothing
 
     isImplies f ==
-      isBinaryNode?(f, 'implies) => just binaryOperands f
+      f' := rep f
+      f' case Kernel % => isBinaryOperator(f', IMP)
       nothing
 
+
     isEquiv f ==
-      isBinaryNode?(f,'equiv) => just binaryOperands f
+      f' := rep f
+      f' case Kernel % => isBinaryOperator(f', EQV)
       nothing
 
     -- Unparsing grammar.
@@ -185,40 +197,40 @@ PropositionalFormula(T: SetCategory): Public == Private where
       formula p
 
     primaryFormula(p: %): OutputForm ==
-      (t := isTerm p) case T => t@T::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
+      p' := rep p
+      p' case T => p'@T::OutputForm
+      is?(p', IMP) or is?(p', EQV) =>
+        args := argument p'
+        elt(operator(p')::OutputForm, 
+		    [formula first args, formula second args])$OutputForm
       paren(formula p)$OutputForm
 
     notFormula(p: %): OutputForm ==
-      isNot p case % =>
-	elt(outputForm 'not, [notFormula((rep p).unForm)])$OutputForm
-      primaryFormula p
-
-    andFormula(p: %): OutputForm ==
-      isAnd p case Pair(%,%) =>
-	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 ==
-      isOr p case Pair(%,%) =>
-	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 ==
+      case isNot p is
+        f@% => elt(outputForm 'not, [formula f])$OutputForm
+        otherwise => primaryFormula p
+
+    andFormula(f: %): OutputForm ==
+      case isAnd f is
+	p@Pair(%,%) =>
+          -- ??? idealy, we should be using `and$OutputForm' but
+          -- ??? a bug in the compiler currently prevents that.
+          infix(outputForm 'and, notFormula first p,
+             andFormula second p)$OutputForm
+        otherwise => notFormula f
+
+    orFormula(f: %): OutputForm ==
+      case isOr f is
+        p@Pair(%,%) => 
+          -- ??? idealy, we should be using `or$OutputForm' but
+          -- ??? a bug in the compiler currently prevents that.
+          infix(outputForm 'or, andFormula first p, 
+             orFormula second p)$OutputForm
+        otherwise => andFormula f
+
+    formula f ==
       -- Note: this should be equivFormula, but see the explanation above.
-      orFormula p
+      orFormula f
 
 @
 
diff --git a/src/algebra/kl.spad.pamphlet b/src/algebra/kl.spad.pamphlet
index 28c7951f..d4211501 100644
--- a/src/algebra/kl.spad.pamphlet
+++ b/src/algebra/kl.spad.pamphlet
@@ -119,12 +119,12 @@ SortedCache(S:CachableSet): Exports == Implementation where
 ++ A kernel over a set S is an operator applied to a given list
 ++ of arguments from S.
 Kernel(S: SetCategory): Exports == Implementation where
-  O  ==> OutputForm
-  N  ==> NonNegativeInteger
-  OP ==> BasicOperator
+  macro O  == OutputForm
+  macro N  == NonNegativeInteger
+  macro OP == BasicOperator
 
 
-  Exports ==> Join(CachableSet, OrderedSet, Patternable S) with
+  Exports == Join(CachableSet, OrderedSet, Patternable S) with
     operator: % -> OP
       ++ operator(op(a1,...,an)) returns the operator op.
     argument: % -> List S
@@ -157,7 +157,7 @@ Kernel(S: SetCategory): Exports == Implementation where
     macro SPECIALINPUT == '%specialInput
     import SortedCache(%)
 
-    Rep == Record(op:OP, arg:List S, nest:N, posit:N)
+    Rep == Record(op: OP, arg: List S, nest: N, posit: N)
 
     clearCache()