Fix SF/1849734

	* interp/i-spec1.boot (upand): Don't insist on having operands of
	type Boolean.
	(upor): Likewise.
	* algebra/mkrecord.spad.pamphlet (Pair): New domain constructor.
	* algebra/exposed.lsp.pamphlet: Expose Pair, PropositionalLogic,
	PropositionalFormula. 
	* algebra/boolean.spad.pamphlet (PropositionalFormula): New domain
	constructor. 
	* algebra/Makefile.pamphlet (axiom_algebra_layer_4): Include
	PAIR.o. 
	(axiom_algebra_layer_19): Include PROPFRML.o
	* share/algebra: Update databases.
	* testsuite/interpreter/1849734.input: New.

5 files changed, 296 insertions, 10 deletions

diff --git a/src/algebra/Makefile.in b/src/algebra/Makefile.in
index 7fe8dd8f..4a806873 100644
--- a/src/algebra/Makefile.in
+++ b/src/algebra/Makefile.in
@@ -391,7 +391,7 @@ axiom_algebra_layer_1 = \
   PATAB.o    PLOT1.o    PPCURVE.o  PSCURVE.o  \
   REAL.o     RESLATC.o  RETRACT.o  RETRACT-.o \
   SEGBIND2.o SEGCAT.o   STREAM1.o  STREAM2.o  \
-  STREAM3.o
+  STREAM3.o  
 
 axiom_algebra_layer_1_nrlibs = \
 	$(axiom_algebra_layer_1:.$(OBJEXT)=.NRLIB/code.$(OBJEXT))
@@ -433,7 +433,7 @@ axiom_algebra_layer_4 = \
   REPDB.o    RFDIST.o   RIDIST.o   RMODULE.o  \
   SEXCAT.o   SGROUP.o   SGROUP-.o  SPACEC.o   \
   SPLNODE.o  STEP.o     SUCH.o     TEX1.o     \
-  UDVO.o     YSTREAM.o
+  UDVO.o     YSTREAM.o  PAIR.o
 
 axiom_algebra_layer_4_nrlibs = \
 	$(axiom_algebra_layer_4:.$(OBJEXT)=.NRLIB/code.$(OBJEXT))
@@ -453,7 +453,7 @@ axiom_algebra_layer_5 = \
   ODVAR.o    OPQUERY.o  ORDFIN.o   ORDMON.o   \
   PATMATCH.o PERMCAT.o  PDRING.o   PDRING-.o  \
   SDVAR.o    SUP2.o     TRIGCAT.o  TRIGCAT-.o \
-  ULS2.o     UP2.o
+  ULS2.o     UP2.o      
 
 axiom_algebra_layer_5_nrlibs = \
 	$(axiom_algebra_layer_5:.$(OBJEXT)=.NRLIB/code.$(OBJEXT))
@@ -732,7 +732,7 @@ axiom_algebra_layer_19 = \
   SET.o      SPECOUT.o  SQMATRIX.o SWITCH.o  \
   SYMS.o     SYMTAB.o   SYSSOLP.o  UTSCAT.o  \
   UTSCAT-.o  VARIABLE.o WFFINTBS.o SPADPRSR.o \
-  PARSER.o
+  PARSER.o   PROPFRML.o
 
 axiom_algebra_layer_19_nrlibs = \
 	$(axiom_algebra_layer_19:.$(OBJEXT)=.NRLIB/code.$(OBJEXT))
diff --git a/src/algebra/Makefile.pamphlet b/src/algebra/Makefile.pamphlet
index 70a3f05c..2e8dc2be 100644
--- a/src/algebra/Makefile.pamphlet
+++ b/src/algebra/Makefile.pamphlet
@@ -233,7 +233,7 @@ axiom_algebra_layer_1 = \
   PATAB.o    PLOT1.o    PPCURVE.o  PSCURVE.o  \
   REAL.o     RESLATC.o  RETRACT.o  RETRACT-.o \
   SEGBIND2.o SEGCAT.o   STREAM1.o  STREAM2.o  \
-  STREAM3.o
+  STREAM3.o  
 
 axiom_algebra_layer_1_nrlibs = \
 	$(axiom_algebra_layer_1:.$(OBJEXT)=.NRLIB/code.$(OBJEXT))
@@ -308,7 +308,7 @@ axiom_algebra_layer_4 = \
   REPDB.o    RFDIST.o   RIDIST.o   RMODULE.o  \
   SEXCAT.o   SGROUP.o   SGROUP-.o  SPACEC.o   \
   SPLNODE.o  STEP.o     SUCH.o     TEX1.o     \
-  UDVO.o     YSTREAM.o
+  UDVO.o     YSTREAM.o  PAIR.o
 
 axiom_algebra_layer_4_nrlibs = \
 	$(axiom_algebra_layer_4:.$(OBJEXT)=.NRLIB/code.$(OBJEXT))
@@ -339,7 +339,7 @@ axiom_algebra_layer_5 = \
   ODVAR.o    OPQUERY.o  ORDFIN.o   ORDMON.o   \
   PATMATCH.o PERMCAT.o  PDRING.o   PDRING-.o  \
   SDVAR.o    SUP2.o     TRIGCAT.o  TRIGCAT-.o \
-  ULS2.o     UP2.o
+  ULS2.o     UP2.o      
 
 axiom_algebra_layer_5_nrlibs = \
 	$(axiom_algebra_layer_5:.$(OBJEXT)=.NRLIB/code.$(OBJEXT))
@@ -997,7 +997,7 @@ axiom_algebra_layer_19 = \
   SET.o      SPECOUT.o  SQMATRIX.o SWITCH.o  \
   SYMS.o     SYMTAB.o   SYSSOLP.o  UTSCAT.o  \
   UTSCAT-.o  VARIABLE.o WFFINTBS.o SPADPRSR.o \
-  PARSER.o
+  PARSER.o   PROPFRML.o
 
 axiom_algebra_layer_19_nrlibs = \
 	$(axiom_algebra_layer_19:.$(OBJEXT)=.NRLIB/code.$(OBJEXT))
diff --git a/src/algebra/boolean.spad.pamphlet b/src/algebra/boolean.spad.pamphlet
index 85b2c056..4fe76ef3 100644
--- a/src/algebra/boolean.spad.pamphlet
+++ b/src/algebra/boolean.spad.pamphlet
@@ -1,4 +1,4 @@
-\documentclass{article}
+documentclass{article}
 \usepackage{axiom}
 
 \title{src/algebra boolean.spad}
@@ -33,6 +33,233 @@ PropositionalLogic(): Category == with
     ++ equiv(p,q) returns the logical equivalence of `p', `q'.
 @
 
+\section{domain PROPFRML PropositionalFormula}
+<<domain PROPFRML PropositionalFormula>>=
+)set mess autoload on
+)abbrev domain PROPFRML PropositionalFormula
+++ Author: Gabriel Dos Reis
+++ Date Created: Januray 14, 2008
+++ Date Last Modified: January 16, 2008
+++ 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 -> %
+      ++ coerce(t) turns the term `t' into a propositional variable.
+--    variables: % -> Set Symbol
+      ++ variables(p) returns the set of propositional variables
+      ++ appearing in the proposition `p'.
+
+    term?: % -> Boolean
+    term: % -> T
+   
+    variable?: % -> Boolean
+    variable: % -> Symbol
+
+    not?: % -> Boolean
+    notOperand: % -> %
+
+    and?: % -> Boolean
+    andOperands: % -> Pair(%, %)
+
+    or?: % -> Boolean
+    orOperands: % -> Pair(%,%)
+
+    implies?: % -> Boolean
+    impliesOperands: % -> Pair(%,%)
+
+    equiv?: % -> Boolean
+    equivOperands: % -> Pair(%,%)
+
+  == add
+    FORMULA ==> Union(base: T, var: Symbol, unForm: %,
+                  binForm: Record(op: Symbol, lhs: %, rhs: %))
+
+    per(f: FORMULA): % ==
+      f pretend %
+
+    rep(p: %): FORMULA ==
+      p pretend FORMULA
+
+    coerce(t: T): % ==
+      per [t]$FORMULA
+
+    coerce(s: Symbol): % ==
+      per [s]$FORMULA
+
+    not p ==
+      per [p]$FORMULA
+
+    binaryForm(o: Symbol, l: %, r: %): % ==
+      per [[o, l, r]$Record(op: Symbol, lhs: %, rhs: %)]$FORMULA
+
+    p and q ==
+      binaryForm('_and, p, q)
+
+    p or q ==
+      binaryForm('_or, p, q)
+
+    implies(p,q) ==
+      binaryForm('implies, p, q)
+
+    equiv(p,q) ==
+      binaryForm('equiv, p, q)
+
+--     variables p ==
+--       p' := rep p
+--       p' case base => empty()$Set(Symbol)
+--       p' case var => { p'.var }
+--       p' case unForm => variables(p'.unForm)
+--       p'' := p'.binForm
+--       union(variables(p''.lhs), variables(p''.rhs))$Set(Symbol)
+
+    -- 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(%,%)
+
+    term? p ==
+      rep p case base
+
+    term p ==
+      term? p => (rep p).base
+      userError "formula is not a term"
+
+    variable? p ==
+      rep p case var
+
+    variable p ==
+      variable? p => (rep p).var
+      userError "formula is not a variable"
+
+    not? p ==
+      rep p case unForm
+
+    notOperand p ==
+      not? p => (rep p).unForm
+      userError "formula is not a logical negation"
+
+    and? p ==
+      isBinaryNode?(p,'_and)
+
+    andOperands p ==
+      and? p => binaryOperands p
+      userError "formula is not a conjunction formula"
+
+    or? p ==
+      isBinaryNode?(p,'_or)
+
+    orOperands p ==
+      or? p => binaryOperands p
+      userError "formula is not a disjunction formula"
+
+    implies? p ==
+      isBinaryNode?(p, 'implies)
+
+    impliesOperands p ==
+      implies? p => binaryOperands p
+      userError "formula is not an implication formula"
+
+    equiv? p ==
+      isBinaryNode?(p,'equiv)
+
+    equivOperands p ==
+      equiv? p =>  binaryOperands p
+      userError "formula is not an equivalence equivalence"
+
+    -- Unparsing grammar.
+    --
+    -- Ideally, the following syntax would the external form
+    -- Formula:
+    --   EquivFormula
+    --
+    -- EquivFormula:
+    --   ImpliesFormula
+    --   ImpliesFormula <=> EquivFormula
+    --
+    -- ImpliesFormula:
+    --   OrFormula
+    --   OrFormula => ImpliesFormula
+    --
+    -- OrFormula:
+    --   AndFormula
+    --   AndFormula or OrFormula 
+    -- 
+    -- AndFormula
+    --   NotFormula
+    --   NotFormula and AndFormula
+    --
+    -- NotFormula:
+    --   PrimaryFormula
+    --   not NotFormula
+    --
+    -- PrimaryFormula:
+    --   Term
+    --   ( Formula )
+    --
+    -- Note: Since the token '=>' already means a construct different
+    --       from what we would like to have as a notation for
+    --       propositional logic, we will output the formula `p => q'
+    --       as implies(p,q), which looks like a function call.
+    --       Similarly, we do not have the token `<=>' for logical
+    --       equivalence; so we unparser `p <=> q' as equiv(p,q).
+    --
+    --       So, we modify the nonterminal PrimaryFormula to read
+    --       PrimaryFormula:
+    --         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
+
+@
 
 \section{domain REF Reference}
 <<domain REF Reference>>=
@@ -503,6 +730,7 @@ Bits(): Exports == Implementation where
 <<domain IBITS IndexedBits>>
 <<domain BITS Bits>>
 <<category PROPLOG PropositionalLogic>>
+<<domain PROPFRML PropositionalFormula>>
 @
 \eject
 \begin{thebibliography}{99}
diff --git a/src/algebra/exposed.lsp.pamphlet b/src/algebra/exposed.lsp.pamphlet
index 94b05ddb..be4f8464 100644
--- a/src/algebra/exposed.lsp.pamphlet
+++ b/src/algebra/exposed.lsp.pamphlet
@@ -254,6 +254,7 @@
   (|OrthogonalPolynomialFunctions| . ORTHPOL)
   (|OutputPackage| . OUT)
   (|PadeApproximantPackage| . PADEPAC)
+  (|Pair| . PAIR)
   (|Palette| . PALETTE)
   (|PartialFraction| . PFR)
   (|PatternFunctions2| . PATTERN2)
@@ -289,6 +290,7 @@
   (|PrimeField| . PF)
   (|PrimitiveArrayFunctions2| . PRIMARR2)
   (|PrintPackage| . PRINT)
+  (|PropositionalFormula| . PROPFRML)
   (|QuadraticForm| . QFORM)
   (|QuasiComponentPackage| . QCMPACK)
   (|Quaternion| . QUAT)
@@ -663,6 +665,7 @@
   (|PrimitiveFunctionCategory| . PRIMCAT)
   (|PrincipalIdealDomain| . PID)
   (|PriorityQueueAggregate| . PRQAGG)
+  (|PropositionalLogic| . PROPLOG)
   (|QuaternionCategory| . QUATCAT)
   (|QueueAggregate| . QUAGG)
   (|QuotientFieldCategory| . QFCAT)
diff --git a/src/algebra/mkrecord.spad.pamphlet b/src/algebra/mkrecord.spad.pamphlet
index 2fe15855..0087800c 100644
--- a/src/algebra/mkrecord.spad.pamphlet
+++ b/src/algebra/mkrecord.spad.pamphlet
@@ -25,10 +25,64 @@ MakeRecord(S: Type, T: Type): public == private where
       [s,t]$Record(part1: S, part2: T)
 
 @
+
+\section{domain PAIR Pair}
+<<domain PAIR Pair>>=
+)abbrev domain PAIR Pair
+++ Author: Gabriel Dos Reis
+++ Date Created: January 16, 2008
+++ Date Last Modified: January 16, 2008
+++ Description:  This domain provides a very simple representation
+++ of the notion of `pair of objects'.  It does not try to achieve
+++ all possible imaginable things.
+Pair(S: Type, T: Type): Public == Private where
+  Public ==> Type with
+
+    if S has CoercibleTo OutputForm and T has CoercibleTo OutputForm then
+      CoercibleTo OutputForm
+
+    if S has SetCategory and T has SetCategory then SetCategory
+
+    pair: (S,T) -> %
+      ++ pair(s,t) returns a pair object composed of `s' and `t'.
+    construct: (S,T) -> %
+      ++ construct(s,t) is same as pair(s,t), with syntactic sugar.
+    first: % -> S
+      ++ first(p) extracts the first component of `p'.
+    second: % -> T
+      ++ second(p) extracts the second components of `p'.
+
+  Private ==> add
+    Rep := Record(fst: S, snd: T)
+
+    pair(s,t) ==
+      [s,t]$Rep
+
+    construct(s,t) ==
+      pair(s,t)
+
+    first x ==
+      x.fst
+
+    second x ==
+      x.snd
+
+    if S has CoercibleTo OutputForm and T has CoercibleTo OutputForm then
+      coerce x ==
+        paren([first(x)::OutputForm, second(x)::OutputForm])$OutputForm
+
+    if S has SetCategory and T has SetCategory then
+      x = y ==
+        first(x) = first(y) and second(x) = second(y)
+@
+
+
 \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
 --modification, are permitted provided that the following conditions are
@@ -62,6 +116,7 @@ MakeRecord(S: Type, T: Type): public == private where
 <<license>>
 
 <<package MKRECORD MakeRecord>>
+<<domain PAIR Pair>>
 @
 \eject
 \begin{thebibliography}{99}