aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/ChangeLog7
-rw-r--r--src/algebra/boolean.spad.pamphlet170
-rw-r--r--src/interp/i-output.boot4
-rw-r--r--src/interp/property.lisp2
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)))