diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/ChangeLog | 10 | ||||
| -rw-r--r-- | src/algebra/Makefile.in | 10 | ||||
| -rw-r--r-- | src/algebra/Makefile.pamphlet | 8 | ||||
| -rw-r--r-- | src/algebra/boolean.spad.pamphlet | 136 | ||||
| -rw-r--r-- | src/algebra/kl.spad.pamphlet | 10 |
5 files changed, 102 insertions, 72 deletions
diff --git a/src/ChangeLog b/src/ChangeLog index 1e4d8f24..74841751 100644 --- a/src/ChangeLog +++ b/src/ChangeLog @@ -1,3 +1,13 @@ +2010-02-20 Gabriel Dos Reis <gdr@cs.tamu.edu> + + * 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. + 2010-02-17 Gabriel Dos Reis <gdr@cs.tamu.edu> * interp/sys-constants.boot ($SystemInlinableConstructorNames): 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() |