diff options
Diffstat (limited to 'src/algebra')
| -rw-r--r-- | src/algebra/Makefile.in | 12 | ||||
| -rw-r--r-- | src/algebra/Makefile.pamphlet | 12 | ||||
| -rw-r--r-- | src/algebra/data.spad.pamphlet | 45 | ||||
| -rw-r--r-- | src/algebra/java.spad.pamphlet | 225 |
4 files changed, 259 insertions, 35 deletions
diff --git a/src/algebra/Makefile.in b/src/algebra/Makefile.in index 8577be6d..e2293479 100644 --- a/src/algebra/Makefile.in +++ b/src/algebra/Makefile.in @@ -537,6 +537,8 @@ $(OUT)/KTVLOGIC.$(FASLEXT): $(OUT)/PROPLOG.$(FASLEXT) $(OUT)/BYTE.$(FASLEXT) $(OUT)/PROPFUN1.$(FASLEXT): $(OUT)/PROPFRML.$(FASLEXT) $(OUT)/PROPFUN2.$(FASLEXT): $(OUT)/PROPFRML.$(FASLEXT) $(OUT)/DIFEXT.$(FASLEXT): $(OUT)/DSEXT.$(FASLEXT) +$(OUT)/BYTE.$(FASLEXT): $(OUT)/LOGIC.$(FASLEXT) +$(OUT)/SYSNNI.$(FASLEXT): $(OUT)/LOGIC.$(FASLEXT) $(OUT)/ORDFIN.$(FASLEXT) axiom_algebra_layer_6 = \ PROPFRML PROPFUN1 AUTOMOR CARTEN2 CHARPOL COMPLEX2 \ @@ -797,7 +799,7 @@ axiom_algebra_layer_15 = \ FRAMALG FRAMALG- MDAGG ODPOL \ PLOT RMCAT2 ROIRC SDPOL \ ULS ULSCONS TUBETOOL UPXSCCA \ - UPXSCCA- JAVACODE POLY BYTEBUF OVERSET \ + UPXSCCA- JVMBCODE POLY BYTEBUF OVERSET \ ULSCCAT ULSCCAT- UTS UTSCAT UTSCAT- axiom_algebra_layer_15_nrlibs = \ @@ -994,7 +996,8 @@ axiom_algebra_layer_user = \ ASP20 ASP30 ASP31 ASP35 ASP41 ASP42 \ ASP74 ASP77 ASP80 ASP29 IRFORM COMPILER \ ITFORM ELABOR TALGOP YDIAGRAM LINELT DBASIS \ - LINFORM LINBASIS + LINFORM LINBASIS JVMOP JVMCFACC JVMFDACC JVMMDACC \ + JVMCSTTG axiom_algebra_layer_user_nrlibs = \ $(addsuffix .NRLIB/code.$(FASLEXT),$(axiom_algebra_layer_user)) @@ -1081,6 +1084,11 @@ $(OUT)/DBASIS.$(FASLEXT): $(OUT)/ORDFIN.$(FASLEXT) $(OUT)/KVTFROM.$(FASLEXT) $(OUT)/LINFORM.$(FASLEXT): $(OUT)/DBASIS.$(FASLEXT) \ $(OUT)/VSPACE.$(FASLEXT) $(OUT)/LINELT.$(FASLEXT) +$(OUT)/JVMOP.$(FASLEXT): $(OUT)/JVMBCODE.$(FASLEXT) +$(OUT)/JVMCFACC.$(FASLEXT): $(OUT)/LOGIC.$(FASLEXT) +$(OUT)/JVMFDACC.$(FASLEXT): $(OUT)/LOGIC.$(FASLEXT) +$(OUT)/JVMMDACC.$(FASLEXT): $(OUT)/LOGIC.$(FASLEXT) + .PHONY: all all-algebra mkdir-output-directory all: all-ax diff --git a/src/algebra/Makefile.pamphlet b/src/algebra/Makefile.pamphlet index 06f10433..24d15915 100644 --- a/src/algebra/Makefile.pamphlet +++ b/src/algebra/Makefile.pamphlet @@ -521,6 +521,8 @@ $(OUT)/KTVLOGIC.$(FASLEXT): $(OUT)/PROPLOG.$(FASLEXT) $(OUT)/BYTE.$(FASLEXT) $(OUT)/PROPFUN1.$(FASLEXT): $(OUT)/PROPFRML.$(FASLEXT) $(OUT)/PROPFUN2.$(FASLEXT): $(OUT)/PROPFRML.$(FASLEXT) $(OUT)/DIFEXT.$(FASLEXT): $(OUT)/DSEXT.$(FASLEXT) +$(OUT)/BYTE.$(FASLEXT): $(OUT)/LOGIC.$(FASLEXT) +$(OUT)/SYSNNI.$(FASLEXT): $(OUT)/LOGIC.$(FASLEXT) $(OUT)/ORDFIN.$(FASLEXT) axiom_algebra_layer_6 = \ PROPFRML PROPFUN1 AUTOMOR CARTEN2 CHARPOL COMPLEX2 \ @@ -829,7 +831,7 @@ axiom_algebra_layer_15 = \ FRAMALG FRAMALG- MDAGG ODPOL \ PLOT RMCAT2 ROIRC SDPOL \ ULS ULSCONS TUBETOOL UPXSCCA \ - UPXSCCA- JAVACODE POLY BYTEBUF OVERSET \ + UPXSCCA- JVMBCODE POLY BYTEBUF OVERSET \ ULSCCAT ULSCCAT- UTS UTSCAT UTSCAT- axiom_algebra_layer_15_nrlibs = \ @@ -1073,7 +1075,8 @@ axiom_algebra_layer_user = \ ASP20 ASP30 ASP31 ASP35 ASP41 ASP42 \ ASP74 ASP77 ASP80 ASP29 IRFORM COMPILER \ ITFORM ELABOR TALGOP YDIAGRAM LINELT DBASIS \ - LINFORM LINBASIS + LINFORM LINBASIS JVMOP JVMCFACC JVMFDACC JVMMDACC \ + JVMCSTTG axiom_algebra_layer_user_nrlibs = \ $(addsuffix .NRLIB/code.$(FASLEXT),$(axiom_algebra_layer_user)) @@ -1160,6 +1163,11 @@ $(OUT)/DBASIS.$(FASLEXT): $(OUT)/ORDFIN.$(FASLEXT) $(OUT)/KVTFROM.$(FASLEXT) $(OUT)/LINFORM.$(FASLEXT): $(OUT)/DBASIS.$(FASLEXT) \ $(OUT)/VSPACE.$(FASLEXT) $(OUT)/LINELT.$(FASLEXT) +$(OUT)/JVMOP.$(FASLEXT): $(OUT)/JVMBCODE.$(FASLEXT) +$(OUT)/JVMCFACC.$(FASLEXT): $(OUT)/LOGIC.$(FASLEXT) +$(OUT)/JVMFDACC.$(FASLEXT): $(OUT)/LOGIC.$(FASLEXT) +$(OUT)/JVMMDACC.$(FASLEXT): $(OUT)/LOGIC.$(FASLEXT) + @ \section{Broken Files} diff --git a/src/algebra/data.spad.pamphlet b/src/algebra/data.spad.pamphlet index 81f574cc..39576863 100644 --- a/src/algebra/data.spad.pamphlet +++ b/src/algebra/data.spad.pamphlet @@ -19,13 +19,13 @@ import OutputForm )abbrev domain BYTE Byte ++ Author: Gabriel Dos Reis ++ Date Created: April 19, 2008 -++ Date Last Updated: January 6, 2009 +++ Date Last Updated: July 18, 2010 ++ Basic Operations: byte, bitand, bitor, bitxor ++ Related Constructor: NonNegativeInteger ++ Description: ++ Byte is the datatype of 8-bit sized unsigned integer values. Byte(): Public == Private where - Public == Join(OrderedFinite, HomotopicTo Character) with + Public == Join(OrderedFinite, HomotopicTo Character,Logic) with byte: NonNegativeInteger -> % ++ byte(x) injects the unsigned integer value `v' into ++ the Byte algebra. `v' must be non-negative and less than 256. @@ -36,23 +36,35 @@ Byte(): Public == Private where sample: % ++ \spad{sample} gives a sample datum of type Byte. Private == SubDomain(NonNegativeInteger, #1 < 256) add + import %beq: (%,%) -> Boolean from Foreign Builtin + import %blt: (%,%) -> Boolean from Foreign Builtin + import %bgt: (%,%) -> Boolean from Foreign Builtin + import %ble: (%,%) -> Boolean from Foreign Builtin + import %bge: (%,%) -> Boolean from Foreign Builtin + import %bitand: (%,%) -> % from Foreign Builtin + import %bitior: (%,%) -> % from Foreign Builtin + import %bitnot: % -> % from Foreign Builtin + byte(x: NonNegativeInteger): % == per x sample = 0$Foreign(Builtin) coerce(c: Character) == per ord c coerce(x: %): Character == char rep x - x = y == byteEqual(x,y)$Foreign(Builtin) - x < y == byteLessThan(x,y)$Foreign(Builtin) - x > y == byteGreaterThan(x,y)$Foreign(Builtin) - x <= y == byteLessEqual(x,y)$Foreign(Builtin) - x >= y == byteGreaterEqual(x,y)$Foreign(Builtin) + x = y == %beq(x,y) + x < y == %blt(x,y) + x > y == %bgt(x,y) + x <= y == %ble(x,y) + x >= y == %bge(x,y) min() == per 0 max() == per 255 size() == 256 index n == byte((n - 1) pretend NonNegativeInteger) lookup x == (rep x + 1) pretend PositiveInteger random() == byte random(size())$NonNegativeInteger - bitand(x,y) == bitand(x,y)$Foreign(Builtin) - bitior(x,y) == bitior(x,y)$Foreign(Builtin) + bitand(x,y) == %bitand(x,y) + bitior(x,y) == %bitior(x,y) + x /\ y == bitand(x,y) + x \/ y == bitior(x,y) + ~ x == %bitnot x @ @@ -175,19 +187,26 @@ Int64() == SystemInteger 64 ++ with the hosting operating system, reading/writing external ++ binary format files. SystemNonNegativeInteger(N: PositiveInteger): Public == Private where - Public == OrderedFinite with + Public == Join(OrderedFinite,Logic) with bitand: (%,%) -> % ++ bitand(x,y) returns the bitwise `and' of `x' and `y'. bitior: (%,%) -> % - ++ bitor(x,y) returns the bitwise `inclusive or' of `x' and `y'. + ++ bitior(x,y) returns the bitwise `inclusive or' of `x' and `y'. sample: % ++ \spad{sample} gives a sample datum of type Byte. Private == SubDomain(NonNegativeInteger, length #1 <= N) add + import %bitand: (%,%) -> % from Foreign Builtin + import %bitior: (%,%) -> % from Foreign Builtin + import %bitnot: % -> % from Foreign Builtin + min == per 0 max == per((shift(1,N)-1)::NonNegativeInteger) sample == min - bitand(x,y) == BOOLE(BOOLE_-AND$Foreign(Builtin),x,y)$Foreign(Builtin) - bitior(x,y) == BOOLE(BOOLE_-IOR$Foreign(Builtin),x,y)$Foreign(Builtin) + bitand(x,y) == %bitand(x,y) + bitior(x,y) == %bitior(x,y) + x /\ y == bitand(x,y) + x \/ y == bitior(x,y) + ~ x == %bitnot x @ diff --git a/src/algebra/java.spad.pamphlet b/src/algebra/java.spad.pamphlet index fae7c311..d09d8607 100644 --- a/src/algebra/java.spad.pamphlet +++ b/src/algebra/java.spad.pamphlet @@ -11,16 +11,203 @@ \tableofcontents \eject -\section{The JavaBytecode domain} -<<domain JAVACODE JavaBytecode>>= -)abbrev domain JAVACODE JavaBytecode +\section{Class file access flags} + +<<domain JVMCFACC JVMClassFileAccess>>= +)abbrev domain JVMCFACC JVMClassFileAccess +++ Date Created: July 18, 2008 +++ Data Last Modified: July 18, 2010 +++ Description: JVM class file access bitmask and values. +JVMClassFileAccess(): Public == Private where + Public == Join(SetCategory,Logic) with + jvmPublic: % + ++ The class was declared public, therefore may be accessed + ++ from outside its package + jvmFinal: % + ++ The class was declared final; therefore no derived class allowed. + jvmSuper: % + ++ Instruct the JVM to treat base clss method invokation specially. + jvmInterface: % + ++ The class file represents an interface, not a class. + jvmAbstract: % + ++ The class was declared abstract; therefore object of this class + ++ may not be created. + Private == UInt16 add + jvmPublic == per(16r0001::Rep) + jvmFinal == per(16r0010::Rep) + jvmSuper == per(16r0020::Rep) + jvmInterface == per(16r0200::Rep) + jvmAbstract == per(16r0400::Rep) +@ + +\section{JVM field access flags} + +<<domain JVMFDACC JVMFieldAccess>>= +)abbrev domain JVMFDACC JVMFieldAccess +++ Date Created: July 18, 2008 +++ Data Last Modified: July 18, 2010 +++ Description: +++ JVM class field access bitmask and values. +JVMFieldAccess(): Public == Private where + Public == Join(SetCategory,Logic) with + jvmPublic: % + ++ The field was declared public; therefore mey accessed from + ++ outside its package. + jvmPrivate: % + ++ The field was declared private; threfore can be accessed only + ++ within the defining class. + jvmProtected: % + ++ The field was declared protected; therefore may be accessed + ++ withing derived classes. + jvmStatic: % + ++ The field was declared static. + jvmFinal: % + ++ The field was declared final; therefore may not be modified + ++ after initialization. + jvmVolatile: % + ++ The field was declared volatile. + jvmTransient: % + ++ The field was declared transient. + Private == UInt16 add + jvmPublic == per(16r0001::Rep) + jvmPrivate == per(16r0002::Rep) + jvmProtected == per(16r0004::Rep) + jvmStatic == per(16r0008::Rep) + jvmFinal == per(16r0010::Rep) + jvmVolatile == per(16r0040::Rep) + jvmTransient == per(16r0080::Rep) +@ + + +\section{JVM method access flags} + +<<domain JVMMDACC JVMMethodAccess>>= +)abbrev domain JVMMDACC JVMMethodAccess +)abbrev domain JVMFDACC JVMFieldAccess +++ Date Created: July 18, 2008 +++ Data Last Modified: July 18, 2010 +++ Description: +++ JVM class method access bitmask and values. +JVMMethodAccess(): Public == Private where + Public == Join(SetCategory,Logic) with + jvmPublic: % + ++ The method was declared public; therefore mey accessed from + ++ outside its package. + jvmPrivate: % + ++ The method was declared private; threfore can be accessed only + ++ within the defining class. + jvmProtected: % + ++ The method was declared protected; therefore may be accessed + ++ withing derived classes. + jvmStatic: % + ++ The method was declared static. + jvmFinal: % + ++ The method was declared final; therefore may not be overriden. + ++ in derived classes. + jvmSynchronized: % + ++ The method was declared synchronized. + jvmNative: % + ++ The method was declared native; therefore implemented in a language + ++ other than Java. + jvmAbstract: % + ++ The method was declared abstract; therefore no implementation + ++ is provided. + jvmStrict: % + ++ The method was declared fpstrict; therefore floating-point mode + ++ is FP-strict. + Private == UInt16 add + jvmPublic == per(16r0001::Rep) + jvmPrivate == per(16r0002::Rep) + jvmProtected == per(16r0004::Rep) + jvmStatic == per(16r0008::Rep) + jvmFinal == per(16r0010::Rep) + jvmSynchronized == per(16r0020::Rep) + jvmNative == per(16r0100::Rep) + jvmAbstract == per(16r0400::Rep) + jvmStrict == per(16r0800::Rep) + +@ + +\section{JVM constant pool tags} + +<<domain JVMCSTTG JVMConstantTag>>= +)abbrev domain JVMCSTTG JVMConstantTag +++ Date Created: July 18, 2008 +++ Data Last Modified: July 18, 2010 +++ Description: +++ JVM class file constant pool tags. +JVMConstantTag(): Public == Private where + Public == Join(SetCategory,CoercibleTo Byte) with + jvmUTF8ConstantTag: % + ++ The corresponding constant pool entry is sequence of bytes + ++ representing Java UTF8 string constant. + jvmIntegerConstantTag: % + ++ The corresponding constant pool entry is an integer constant info. + jvmFloatConstantTag: % + ++ The corresponding constant pool entry is a float constant info. + jvmLongConstantTag: % + ++ The corresponding constant pool entry is a long constant info. + jvmDoubleConstantTag: % + ++ The corresponding constant pool entry is a double constant info. + jvmClassConstantTag: % + ++ The corresponding constant pool entry represents a class or + ++ and interface. + jvmStringConstantTag: % + ++ The corresponding constant pool entry is a string constant info. + jvmFieldrefConstantTag: % + ++ The corresponding constant pool entry represents a class field info. + jvmMethodrefConstantTag: % + ++ The correspondong constant pool entry represents a class method info. + jvmInterfaceMethodConstantTag: % + ++ The correspondong constant pool entry represents an interface + ++ method info. + jvmNameAndTypeConstantTag: % + ++ The correspondong constant pool entry represents the name + ++ and type of a field or method info. + Private == Byte add + jvmUTF8ConstantTag == per byte 1 + jvmIntegerConstantTag == per byte 3 + jvmFloatConstantTag == per byte 4 + jvmLongConstantTag == per byte 5 + jvmDoubleConstantTag == per byte 6 + jvmClassConstantTag == per byte 7 + jvmStringConstantTag == per byte 8 + jvmFieldrefConstantTag == per byte 9 + jvmMethodrefConstantTag == per byte 10 + jvmInterfaceMethodConstantTag == per byte 11 + jvmNameAndTypeConstantTag == per byte 12 +@ + + +\section{The JVMBytecode domain} +<<domain JVMBCODE JVMBytecode>>= +)abbrev domain JVMBCODE JVMBytecode ++ Author: Gabriel Dos Reis ++ Date Created: May 08, 2008 -++ Description: This domain defines the datatype for the Java -++ Virtual Machine byte codes. -JavaBytecode(): Public == Private where - Public == Join(CoercibleTo OutputForm, HomotopicTo Byte) - Private == add +++ Data Last Modified: July 18, 2010 +++ Description: +++ This is the datatype for the JVM bytecodes. +JVMBytecode(): Public == Private where + Public == Join(SetCategory, HomotopicTo Byte) + Private == Byte add + coerce(b: Byte): % == + per b + + coerce(x: %): Byte == + rep x +@ + +\section{JVM Opcodes} + +<<domain JVMOP JVMOpcode>>= +)abbrev domain JVMOP JVMOpcode +++ Date Created: July 18, 2008 +++ Data Last Modified: July 18, 2010 +++ Description: +++ This is the datatype for the JVM opcodes. +JVMOpcode(): Public == Private where + Public == Join(SetCategory,HomotopicTo JVMBytecode,HomotopicTo Byte) + Private == JVMBytecode add -- mnemonics equivalent of bytecodes. mnemonics : PrimitiveArray Symbol := [['nop, 'aconst__null, 'iconst__m1, 'iconst__0, 'iconst__1, _ @@ -77,22 +264,17 @@ JavaBytecode(): Public == Private where 'unknownopcode49, 'unknownopcode50, _ 'impldep1, 'impldep2 ]]$PrimitiveArray(Symbol) - Rep == Byte - - coerce(x: Byte): % == - per x - - coerce(x: %): Byte == - rep x - + coerce(x: %): JVMBytecode == rep x + coerce(b: JVMBytecode): % == per b coerce(x: %): OutputForm == mnemonics.(x::Byte::Integer) :: OutputForm + @ \section{License} <<license>>= ---Copyright (C) 2007-2008, Gabriel Dos Reis. +--Copyright (C) 2007-2010, Gabriel Dos Reis. --All rights reserved. -- --Redistribution and use in source and binary forms, with or without @@ -126,7 +308,14 @@ JavaBytecode(): Public == Private where <<*>>= <<license>> -<<domain JAVACODE JavaBytecode>> + +<<domain JVMCFACC JVMClassFileAccess>> +<<domain JVMFDACC JVMFieldAccess>> +<<domain JVMMDACC JVMMethodAccess>> +<<domain JVMCSTTG JVMConstantTag>> +<<domain JVMBCODE JVMBytecode>> +<<domain JVMOP JVMOpcode>> + @ \end{document} |