diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/ChangeLog | 12 | ||||
| -rw-r--r-- | src/algebra/Makefile.in | 6 | ||||
| -rw-r--r-- | src/algebra/Makefile.pamphlet | 6 | ||||
| -rw-r--r-- | src/algebra/boolean.spad.pamphlet | 153 | ||||
| -rw-r--r-- | src/algebra/data.spad.pamphlet | 5 | ||||
| -rw-r--r-- | src/interp/sys-macros.lisp | 7 |
6 files changed, 134 insertions, 55 deletions
diff --git a/src/ChangeLog b/src/ChangeLog index 7c0491fc..ef3796f0 100644 --- a/src/ChangeLog +++ b/src/ChangeLog @@ -1,5 +1,17 @@ 2008-09-20 Gabriel Dos Reis <gdr@cs.tamu.edu> + * interp/sys-macros.lisp (|byteEqual|): New. + * algebra/boolean.spad.pamphlet (PropositionalLogic): Extend + SetCategory. + (PropositionalFormula): Now unconditional exports coercion to + OutputForm. Adjust implementation. + (KleeneTrivalentLogic): New. + * algebra/data.spad.pamphlet (Byte): Tidy. + * algebra/Makefile.pamphlet (axiom_algebra_layer_0): Move PROPLOG + to layer 1. + +2008-09-20 Gabriel Dos Reis <gdr@cs.tamu.edu> + * include/cfuns.h (oa_dirname): Declare. * lib/cfuns-c.c (openaxiom_is_path_separator): New. (oa_dirname): Define. diff --git a/src/algebra/Makefile.in b/src/algebra/Makefile.in index 0da21709..4dab8997 100644 --- a/src/algebra/Makefile.in +++ b/src/algebra/Makefile.in @@ -358,7 +358,7 @@ axiom_algebra_layer_0 = \ AHYP ATTREG CFCAT ELTAB KOERCE KONVERT \ MSYSCMD OM OMCONN OMDEV OUT \ PRIMCAT PRINT PTRANFN SPFCAT TYPE UTYPE \ - PROPLOG PROPERTY BASTYPE BASTYPE- CATEGORY LMODULE \ + PROPERTY BASTYPE BASTYPE- CATEGORY LMODULE \ RMODULE FINITE STEP SGROUP SGROUP- ABELSG \ ABELSG- ORDSET ORDSET- FNCAT FILECAT SEXCAT \ MKBCFUNC MKRECORD MKUCFUNC DROPT1 PLOT1 ITFUN2 \ @@ -376,7 +376,7 @@ axiom_algebra_layer_1 = \ PATAB PPCURVE PSCURVE REAL RESLATC RETRACT \ RETRACT- SEGCAT BINDING SYNTAX BMODULE LOGIC \ LOGIC- EVALAB EVALAB- FEVALAB FEVALAB- BYTE \ - OSGROUP MAYBE DATABUF + OSGROUP MAYBE DATABUF PROPLOG axiom_algebra_layer_1_nrlibs = \ $(addsuffix .NRLIB/code.$(FASLEXT),$(axiom_algebra_layer_1)) @@ -387,7 +387,7 @@ axiom_algebra_layer_1_objects = \ axiom_algebra_layer_2 = \ ELTAGG ELTAGG- FMC FMFUN FORTFN FVC \ CTORCALL FVFUN INTRET IXAGG IXAGG- SEGXCAT \ - CONTOUR LIST3 MKFUNC OASGP + CONTOUR LIST3 MKFUNC OASGP KTVLOGIC axiom_algebra_layer_2_nrlibs = \ $(addsuffix .NRLIB/code.$(FASLEXT),$(axiom_algebra_layer_2)) diff --git a/src/algebra/Makefile.pamphlet b/src/algebra/Makefile.pamphlet index 3c489670..d34998bd 100644 --- a/src/algebra/Makefile.pamphlet +++ b/src/algebra/Makefile.pamphlet @@ -187,7 +187,7 @@ axiom_algebra_layer_0 = \ AHYP ATTREG CFCAT ELTAB KOERCE KONVERT \ MSYSCMD OM OMCONN OMDEV OUT \ PRIMCAT PRINT PTRANFN SPFCAT TYPE UTYPE \ - PROPLOG PROPERTY BASTYPE BASTYPE- CATEGORY LMODULE \ + PROPERTY BASTYPE BASTYPE- CATEGORY LMODULE \ RMODULE FINITE STEP SGROUP SGROUP- ABELSG \ ABELSG- ORDSET ORDSET- FNCAT FILECAT SEXCAT \ MKBCFUNC MKRECORD MKUCFUNC DROPT1 PLOT1 ITFUN2 \ @@ -219,7 +219,7 @@ axiom_algebra_layer_1 = \ PATAB PPCURVE PSCURVE REAL RESLATC RETRACT \ RETRACT- SEGCAT BINDING SYNTAX BMODULE LOGIC \ LOGIC- EVALAB EVALAB- FEVALAB FEVALAB- BYTE \ - OSGROUP MAYBE DATABUF + OSGROUP MAYBE DATABUF PROPLOG axiom_algebra_layer_1_nrlibs = \ $(addsuffix .NRLIB/code.$(FASLEXT),$(axiom_algebra_layer_1)) @@ -237,7 +237,7 @@ axiom_algebra_layer_1_objects = \ axiom_algebra_layer_2 = \ ELTAGG ELTAGG- FMC FMFUN FORTFN FVC \ CTORCALL FVFUN INTRET IXAGG IXAGG- SEGXCAT \ - CONTOUR LIST3 MKFUNC OASGP + CONTOUR LIST3 MKFUNC OASGP KTVLOGIC axiom_algebra_layer_2_nrlibs = \ $(addsuffix .NRLIB/code.$(FASLEXT),$(axiom_algebra_layer_2)) diff --git a/src/algebra/boolean.spad.pamphlet b/src/algebra/boolean.spad.pamphlet index ab33ba62..b9cb64cb 100644 --- a/src/algebra/boolean.spad.pamphlet +++ b/src/algebra/boolean.spad.pamphlet @@ -17,10 +17,10 @@ )abbrev category PROPLOG PropositionalLogic ++ Author: Gabriel Dos Reis ++ Date Created: Januray 14, 2008 -++ Date Last Modified: January 14, 2008 +++ Date Last Modified: September 20, 2008 ++ Description: This category declares the connectives of ++ Propositional Logic. -PropositionalLogic(): Category == with +PropositionalLogic(): Category == SetCategory with "not": % -> % ++ not p returns the logical negation of `p'. "and": (%, %) -> % @@ -43,7 +43,6 @@ PropositionalLogic(): Category == with ++ Description: This domain implements propositional formula build ++ over a term domain, that itself belongs to PropositionalLogic PropositionalFormula(T: PropositionalLogic): PropositionalLogic with - if T has CoercibleTo OutputForm then CoercibleTo OutputForm coerce: T -> % ++ coerce(t) turns the term `t' into a propositional formula coerce: Symbol -> % @@ -236,47 +235,46 @@ PropositionalFormula(T: PropositionalLogic): PropositionalLogic with -- Term -- implies(Formula, Formula) -- equiv(Formula, Formula) - if T has CoercibleTo OutputForm then - formula: % -> OutputForm - coerce(p: %): OutputForm == - formula p - - primaryFormula(p: %): OutputForm == - term? p => term(p)::OutputForm - variable? p => variable(p)::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 - paren(formula p)$OutputForm - - notFormula(p: %): OutputForm == - not? p => - elt(outputForm '_not, [notFormula((rep p).unForm)])$OutputForm - primaryFormula p - - andFormula(p: %): OutputForm == - and? p => - 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 == - or? p => - 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 == - -- Note: this should be equivFormula, but see the explanation above. - orFormula p + formula: % -> OutputForm + coerce(p: %): OutputForm == + formula p + + primaryFormula(p: %): OutputForm == + term? p => term(p)::OutputForm + variable? p => variable(p)::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 + paren(formula p)$OutputForm + + notFormula(p: %): OutputForm == + not? p => + elt(outputForm '_not, [notFormula((rep p).unForm)])$OutputForm + primaryFormula p + + andFormula(p: %): OutputForm == + and? p => + 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 == + or? p => + 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 == + -- Note: this should be equivFormula, but see the explanation above. + orFormula p @ @@ -501,9 +499,70 @@ Bits(): Exports == Implementation where bits(n,b) == new(n,b) @ + + +\section{Kleene's Three-Valued Logic} +<<domain KTVLOGIC KleeneTrivalentLogic>>= +)abbrev domain KTVLOGIC KleeneTrivalentLogic +++ Author: Gabriel Dos Reis +++ Date Created: September 20, 2008 +++ Date Last Modified: September 20, 2008 +++ Description: +++ This domain implements Kleene's 3-valued propositional logic. +KleeneTrivalentLogic(): Public == Private where + Public == PropositionalLogic with + false: % + unknown: % + true: % + _case: (%,[| false |]) -> Boolean + _case: (%,[| unknown |]) -> Boolean + _case: (%,[| true |]) -> Boolean + Private == add + Rep == Byte -- We need only 3 bits, in fact. + false == per(0::NonNegativeInteger::Byte) + unknown == per(1::NonNegativeInteger::Byte) + true == per(2::Byte) + x = y == rep x = rep y + x case true == x = true + x case false == x = false + x case unknown == x = unknown + not x == + x case false => true + x case unknown => unknown + false + x and y == + x case false => false + x case unknown => + y case false => false + unknown + y + x or y == + x case false => y + x case true => x + y case true => y + unknown + implies(x,y) == + x case false => true + x case true => y + y case true => true + unknown + equiv(x,y) == + x case unknown => x + x case true => y + not y + coerce(x: %): OutputForm == + x case true => outputForm 'true + x case false => outputForm 'false + outputForm 'unknown +@ + + \section{License} + <<license>>= ---Copyright (c) 1991-2002, The Numerical ALgorithms Group Ltd. +--Copyright (c) 1991-2002, The Numerical Algorithms Group Ltd. +--All rights reserved. +--Copyright (C) 2007-2008, Gabriel Dos Reis. --All rights reserved. -- --Redistribution and use in source and binary forms, with or without @@ -518,7 +577,7 @@ Bits(): Exports == Implementation where -- the documentation and/or other materials provided with the -- distribution. -- --- - Neither the name of The Numerical ALgorithms Group Ltd. nor the +-- - Neither the name of The Numerical Algorithms Group Ltd. nor the -- names of its contributors may be used to endorse or promote products -- derived from this software without specific prior written permission. -- @@ -544,6 +603,8 @@ Bits(): Exports == Implementation where <<domain BITS Bits>> <<category PROPLOG PropositionalLogic>> <<domain PROPFRML PropositionalFormula>> +<<domain KTVLOGIC KleeneTrivalentLogic>> + @ \eject \begin{thebibliography}{99} diff --git a/src/algebra/data.spad.pamphlet b/src/algebra/data.spad.pamphlet index 9640d7ad..e3262ef5 100644 --- a/src/algebra/data.spad.pamphlet +++ b/src/algebra/data.spad.pamphlet @@ -36,7 +36,7 @@ Byte(): Public == Private where Private ==> add byte(x: NonNegativeInteger): % == - byteGreaterEqual(x,256$Lisp)$Lisp => + not (x < 256$Lisp) => userError "integer value cannot be represented by a byte" x : % @@ -48,6 +48,9 @@ Byte(): Public == Private where coerce(x: %): OutputForm == x::NonNegativeInteger::OutputForm + + x = y == + byteEqual(x,y)$Lisp x < y == byteLessThan(x,y)$Lisp diff --git a/src/interp/sys-macros.lisp b/src/interp/sys-macros.lisp index cd389841..c53dac73 100644 --- a/src/interp/sys-macros.lisp +++ b/src/interp/sys-macros.lisp @@ -62,11 +62,14 @@ ;; -*- Byte -*- ;; +(defmacro |byteEqual| (|x| |y|) + `(EQL (the |%Byte| ,|x|) (the |%Byte| ,|y|))) + (defmacro |byteLessThan| (|x| |y|) - `(< (the fixnum ,|x|) (the fixnum ,|y|))) + `(< (the |%Byte| ,|x|) (the |%Byte| ,|y|))) (defmacro |byteGreaterEqual| (|x| |y|) - `(>= (the fixnum ,|x|) (the fixnum ,|y|))) + `(>= (the |%Byte| ,|x|) (the |%Byte| ,|y|))) ;; ;; -*- BigFloat Constructors -*- |