diff options
| -rwxr-xr-x | configure | 18 | ||||
| -rw-r--r-- | configure.ac | 2 | ||||
| -rw-r--r-- | configure.ac.pamphlet | 2 | ||||
| -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 |
8 files changed, 113 insertions, 83 deletions
@@ -1,6 +1,6 @@ #! /bin/sh # Guess values for system-dependent variables and create Makefiles. -# Generated by GNU Autoconf 2.63 for OpenAxiom 1.4.0-2010-02-17. +# Generated by GNU Autoconf 2.63 for OpenAxiom 1.4.0-2010-02-20. # # Report bugs to <open-axiom-bugs@lists.sf.net>. # @@ -745,8 +745,8 @@ SHELL=${CONFIG_SHELL-/bin/sh} # Identity of this package. PACKAGE_NAME='OpenAxiom' PACKAGE_TARNAME='openaxiom' -PACKAGE_VERSION='1.4.0-2010-02-17' -PACKAGE_STRING='OpenAxiom 1.4.0-2010-02-17' +PACKAGE_VERSION='1.4.0-2010-02-20' +PACKAGE_STRING='OpenAxiom 1.4.0-2010-02-20' PACKAGE_BUGREPORT='open-axiom-bugs@lists.sf.net' ac_unique_file="src/Makefile.pamphlet" @@ -1511,7 +1511,7 @@ if test "$ac_init_help" = "long"; then # Omit some internal or obsolete options to make the list less imposing. # This message is too long to be a string in the A/UX 3.1 sh. cat <<_ACEOF -\`configure' configures OpenAxiom 1.4.0-2010-02-17 to adapt to many kinds of systems. +\`configure' configures OpenAxiom 1.4.0-2010-02-20 to adapt to many kinds of systems. Usage: $0 [OPTION]... [VAR=VALUE]... @@ -1581,7 +1581,7 @@ fi if test -n "$ac_init_help"; then case $ac_init_help in - short | recursive ) echo "Configuration of OpenAxiom 1.4.0-2010-02-17:";; + short | recursive ) echo "Configuration of OpenAxiom 1.4.0-2010-02-20:";; esac cat <<\_ACEOF @@ -1688,7 +1688,7 @@ fi test -n "$ac_init_help" && exit $ac_status if $ac_init_version; then cat <<\_ACEOF -OpenAxiom configure 1.4.0-2010-02-17 +OpenAxiom configure 1.4.0-2010-02-20 generated by GNU Autoconf 2.63 Copyright (C) 1992, 1993, 1994, 1995, 1996, 1998, 1999, 2000, 2001, @@ -1702,7 +1702,7 @@ cat >config.log <<_ACEOF This file contains any messages produced by compilers while running configure, to aid debugging if configure makes a mistake. -It was created by OpenAxiom $as_me 1.4.0-2010-02-17, which was +It was created by OpenAxiom $as_me 1.4.0-2010-02-20, which was generated by GNU Autoconf 2.63. Invocation command line was $ $0 $@ @@ -21165,7 +21165,7 @@ exec 6>&1 # report actual input values of CONFIG_FILES etc. instead of their # values after options handling. ac_log=" -This file was extended by OpenAxiom $as_me 1.4.0-2010-02-17, which was +This file was extended by OpenAxiom $as_me 1.4.0-2010-02-20, which was generated by GNU Autoconf 2.63. Invocation command line was CONFIG_FILES = $CONFIG_FILES @@ -21228,7 +21228,7 @@ Report bugs to <bug-autoconf@gnu.org>." _ACEOF cat >>$CONFIG_STATUS <<_ACEOF || ac_write_fail=1 ac_cs_version="\\ -OpenAxiom config.status 1.4.0-2010-02-17 +OpenAxiom config.status 1.4.0-2010-02-20 configured by $0, generated by GNU Autoconf 2.63, with options \\"`$as_echo "$ac_configure_args" | sed 's/^ //; s/[\\""\`\$]/\\\\&/g'`\\" diff --git a/configure.ac b/configure.ac index 335b69aa..30fd65fc 100644 --- a/configure.ac +++ b/configure.ac @@ -1,6 +1,6 @@ sinclude(config/open-axiom.m4) sinclude(config/aclocal.m4) -AC_INIT([OpenAxiom], [1.4.0-2010-02-17], +AC_INIT([OpenAxiom], [1.4.0-2010-02-20], [open-axiom-bugs@lists.sf.net]) AC_CONFIG_AUX_DIR(config) diff --git a/configure.ac.pamphlet b/configure.ac.pamphlet index 3ff4a27a..b07464dc 100644 --- a/configure.ac.pamphlet +++ b/configure.ac.pamphlet @@ -1200,7 +1200,7 @@ information: <<Autoconf init>>= sinclude(config/open-axiom.m4) sinclude(config/aclocal.m4) -AC_INIT([OpenAxiom], [1.4.0-2010-02-17], +AC_INIT([OpenAxiom], [1.4.0-2010-02-20], [open-axiom-bugs@lists.sf.net]) @ 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() |