diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/ChangeLog | 7 | ||||
| -rw-r--r-- | src/algebra/boolean.spad.pamphlet | 170 | ||||
| -rw-r--r-- | src/interp/i-output.boot | 4 | ||||
| -rw-r--r-- | src/interp/property.lisp | 2 |
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))) |