* interp/property.lisp: "not" is prefix operator with "not " for

	rendering.
	* interp/i-output.boot ($allClassicOps): Include not.
	* algebra/boolean.spad.pamphlet (PropositionalFormula): Rework.

4 files changed, 65 insertions, 118 deletions

diff --git a/src/ChangeLog b/src/ChangeLog
index e4cb67f4..2b01db03 100644
--- a/src/ChangeLog
+++ b/src/ChangeLog
@@ -1,3 +1,10 @@
+2009-05-11  Gabriel Dos Reis  <gdr@cs.tamu.edu>
+
+	* interp/property.lisp: "not" is prefix operator with "not " for
+	rendering.
+	* interp/i-output.boot ($allClassicOps): Include not.
+	* algebra/boolean.spad.pamphlet (PropositionalFormula): Rework.
+
 2009-05-10  Gabriel Dos Reis  <gdr@cs.tamu.edu>
 
 	* boot/translator.boot: Don't load imported modules when
diff --git a/src/algebra/boolean.spad.pamphlet b/src/algebra/boolean.spad.pamphlet
index fd48f80c..7c30999b 100644
--- a/src/algebra/boolean.spad.pamphlet
+++ b/src/algebra/boolean.spad.pamphlet
@@ -39,74 +39,48 @@ PropositionalLogic(): Category == SetCategory with
 )abbrev domain PROPFRML PropositionalFormula
 ++ Author: Gabriel Dos Reis
 ++ Date Created: Januray 14, 2008
-++ Date Last Modified: January 16, 2008
+++ Date Last Modified: May 11, 2009
 ++ Description: This domain implements propositional formula build
 ++ over a term domain, that itself belongs to PropositionalLogic
-PropositionalFormula(T: PropositionalLogic): PropositionalLogic with
-    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? p returns true when `p' really is a term
-    term: % -> T
-      ++ term p extracts the term value from `p'; otherwise errors.
-   
-    variable?: % -> Boolean
-      ++ variables? p returns true when `p' really is a variable.
-    variable: % -> Symbol
-      ++ variable p extracts the variable name from `p'; otherwise errors.
-
-    not?: % -> Boolean
-      ++ not? p is true when `p' is a logical negation
-    notOperand: % -> %
-      ++ notOperand returns the operand to the logical `not' operator; 
-      ++ otherwise errors.
-
-    and?: % -> Boolean
-      ++ and? p is true when `p' is a logical conjunction.
-    andOperands: % -> Pair(%, %)
-      ++ andOperands p extracts the operands of the logical conjunction;
-      ++ otherwise errors.
-
-    or?: % -> Boolean
-      ++ or? p is true when `p' is a logical disjunction.
-    orOperands: % -> Pair(%,%)
-      ++ orOperands p extracts the operands to the logical disjunction;
-      ++ otherwise errors.
-
-    implies?: % -> Boolean
-      ++ implies? p is true when `p' is a logical implication.
-    impliesOperands: % -> Pair(%,%)
-      ++ impliesOperands p extracts the operands to the logical
-      ++ implication; otherwise errors.
-
-    equiv?: % -> Boolean
-      ++ equiv? p is true when `p' is a logical equivalence.
-    equivOperands: % -> Pair(%,%)
-      ++ equivOperands p extracts the operands to the logical equivalence;
-      ++ otherwise errors.
+PropositionalFormula(T: SetCategory): Public == Private where
+  Public == Join(PropositionalLogic, CoercibleFrom T) with
+    isTerm : % -> Maybe T
+      ++ \spad{isTerm f} returns a value \spad{v} such that
+      ++ \spad{v case T} holds if the formula \spad{f} is a term.
+
+    isNot : % -> Maybe %
+      ++ \spad{isNot f} returns a value \spad{v} such that
+      ++ \spad{v case %} holds if the formula \spad{f} is a negation.
+
+    isAnd : % -> Maybe Pair(%,%)
+      ++ \spad{isAnd f} returns a value \spad{v} such that 
+      ++ \spad{v case Pair(%,%)} holds if the formula \spad{f}
+      ++ is a conjunction formula.
+
+    isOr : % -> Maybe Pair(%,%)
+      ++ \spad{isOr f} returns a value \spad{v} such that 
+      ++ \spad{v case Pair(%,%)} holds if the formula \spad{f}
+      ++ is a disjunction formula.
+
+    isImplies : % -> Maybe Pair(%,%)
+      ++ \spad{isImplies f} returns a value \spad{v} such that 
+      ++ \spad{v case Pair(%,%)} holds if the formula \spad{f}
+      ++ is an implication formula.
+
+    isEquiv : % -> Maybe Pair(%,%)
+      ++ \spad{isEquiv f} returns a value \spad{v} such that 
+      ++ \spad{v case Pair(%,%)} holds if the formula \spad{f}
+      ++ is an equivalence formula.
 
-  == add
-    FORMULA ==> Union(base: T, var: Symbol, unForm: %,
+  Private == add
+    FORMULA ==> Union(base: T, unForm: %,
                   binForm: Record(op: Symbol, lhs: %, rhs: %))
 
-    per(f: FORMULA): % ==
-      f pretend %
-
-    rep(p: %): FORMULA ==
-      p pretend FORMULA
+    Rep == FORMULA
 
     coerce(t: T): % ==
       per [t]$FORMULA
 
-    coerce(s: Symbol): % ==
-      per [s]$FORMULA
-
     not p ==
       per [p]$FORMULA
 
@@ -125,14 +99,6 @@ PropositionalFormula(T: PropositionalLogic): PropositionalLogic with
     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 ==
@@ -144,54 +110,29 @@ PropositionalFormula(T: PropositionalLogic): PropositionalLogic with
       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)
+    isTerm f ==
+      rep f case base => just rep(f).base
+      nothing
 
-    orOperands p ==
-      or? p => binaryOperands p
-      userError "formula is not a disjunction formula"
+    isNot f ==
+      rep f case unForm => just rep(f).unForm
+      nothing
 
-    implies? p ==
-      isBinaryNode?(p, 'implies)
+    isAnd f ==
+      isBinaryNode?(f,'_and) => just binaryOperands f
+      nothing
 
-    impliesOperands p ==
-      implies? p => binaryOperands p
-      userError "formula is not an implication formula"
+    isOr f ==
+      isBinaryNode?(f,'_or) => just binaryOperands f
+      nothing
 
-    equiv? p ==
-      isBinaryNode?(p,'equiv)
+    isImplies f ==
+      isBinaryNode?(f, 'implies) => just binaryOperands f
+      nothing
 
-    equivOperands p ==
-      equiv? p =>  binaryOperands p
-      userError "formula is not an equivalence equivalence"
+    isEquiv f ==
+      isBinaryNode?(f,'equiv) => just binaryOperands f
+      nothing
 
     -- Unparsing grammar.
     --
@@ -240,8 +181,7 @@ PropositionalFormula(T: PropositionalLogic): PropositionalLogic with
       formula p
 
     primaryFormula(p: %): OutputForm ==
-      term? p => term(p)::OutputForm
-      variable? p => variable(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 =>
@@ -250,12 +190,12 @@ PropositionalFormula(T: PropositionalLogic): PropositionalLogic with
       paren(formula p)$OutputForm
 
     notFormula(p: %): OutputForm ==
-      not? p =>
+      isNot p case % =>
 	elt(outputForm '_not, [notFormula((rep p).unForm)])$OutputForm
       primaryFormula p
 
     andFormula(p: %): OutputForm ==
-      and? p =>
+      isAnd p case Pair(%,%) =>
 	p' := (rep p).binForm
 	-- ??? idealy, we should be using `and$OutputForm' but
 	-- ??? a bug in the compiler currently prevents that.
@@ -264,7 +204,7 @@ PropositionalFormula(T: PropositionalLogic): PropositionalLogic with
       notFormula p
 
     orFormula(p: %): OutputForm ==
-      or? p =>
+      isOr p case Pair(%,%) =>
 	p' := (rep p).binForm
 	-- ??? idealy, we should be using `or$OutputForm' but
 	-- ??? a bug in the compiler currently prevents that.
diff --git a/src/interp/i-output.boot b/src/interp/i-output.boot
index 41dacca2..ca24779d 100644
--- a/src/interp/i-output.boot
+++ b/src/interp/i-output.boot
@@ -2592,10 +2592,10 @@ maPrin u ==
 --% Rendering of InputForm
 
 $allClassicOps == 
-  ["~","#","**","^","*","/","rem","quo","+","-","@","::", "pretend"]
+  ["~","#","not","**","^","*","/","rem","quo","+","-","@","::", "pretend"]
 
 isUnaryPrefix op ==
-  op in '(_~ _# _-)
+  op in '(_~ _# _- _not)
 
 primaryForm2String x ==
   x = nil => '""
diff --git a/src/interp/property.lisp b/src/interp/property.lisp
index 62e93bf3..1a8a2323 100644
--- a/src/interp/property.lisp
+++ b/src/interp/property.lisp
@@ -112,7 +112,7 @@
 (REPEAT (IN X '(
   (= "=")
   (|:| ":")
-  (|not| "^ ")
+  (|not| "not ")
   (\| " \| ")
   (SEGMENT "..")  ;" 0.. is represented by (SEGMENT 0)"
  )) (MAKEPROP (CAR X) 'PREFIXOP (CADR X)))