Types and type environments for a quirk20 compiler. [Revision 0]
Qtype types
Tenv type environments
* * *
Qtype:
Signature:
Qtype.iVoidType: int
Qtype.iNullType: int
Qtype.iBoolType: int
Qtype.iCharType: int
Qtype.iStringType: int
Qtype.iIntType: int
Qtype.iDoubleType: int
Qtype.iTypeId: int
Qtype.iArrayType: int
Qtype.iFunType: int
Qtype.VOID: Qtype
Qtype.NULL: Qtype
Qtype.BOOLEAN: Qtype
Qtype.CHAR: Qtype
Qtype.STRING: Qtype
Qtype.INT: Qtype
Qtype.DOUBLE: Qtype
Qtype.toType: Ast -> Qtype
Qtype.kind: Qtype -> int
Qtype.equals: Qtype x Qtype -> boolean
Qtype.isSubtype: Qtype x Qtype -> boolean
Qtype.typeId_name: Qtype -> Qsymbol
Qtype.arrayType_elementType: Qtype -> Qtype
Qtype.funType_returnType: Qtype -> Qtype
Qtype.funType_arity: Qtype -> int
Qtype.funType_argumentType: Qtype x int -> Qtype
Qtype.write: Qtype ->
Specification:
iVoidType through iFunType are distinct non-negative integer constants.
VOID through DOUBLE represent the primitive types of quirk20.
toType translates an Ast to the corresponding Qtype.
kind(T) returns one of the integer constants iVoidType through iFunType.
equals(T1, T2) returns true iff T1 is equal to T2.
subtype(T1, T2) returns true iff T1 is a subtype of T2.
If kind(T) is iTypeId, then typeId_name(T) returns the name of the type
identifier T.
If kind(T) is iArrayType, then arrayType_elementType(T) returns the type
that T specifies for each array element.
If kind(T) is iFunType, then funType_returnType(T) returns the result
type, funType_arity(T) returns the number of arguments, and
funType_argumentType(T,i) returns the type of argument i (where the
first argument is argument 1).
write(T) writes a readable representation of T to standard output.
* * *
Tenv:
Signature:
Tenv.error: -> Tenv
Tenv.empty: -> Tenv
Tenv.extend: Tenv x Qsymbol x Qtype x boolean x boolean -> Tenv
Tenv.extendWithClass: Tenv x Qsymbol x Tenv x Tenv -> Tenv
Tenv.extendWithTenv: Tenv x Tenv -> Tenv
Tenv.lookupType: Tenv x Qsymbol -> Qtype
Tenv.lookupFinal: Tenv x Qsymbol -> boolean
Tenv.lookupGlobal: Tenv x Qsymbol -> boolean
Tenv.lookupStatic: Tenv x Qsymbol -> Tenv
Tenv.lookupDynamic: Tenv x Qsymbol -> Tenv
Tenv.length: Tenv -> int
Tenv.identifier: Tenv x int -> Qsymbol
Tenv.isError: Tenv -> boolean
Tenv.initial: -> Tenv
Algebraic specification:
extendWithTenv (tenv0, empty())
= tenv0
extendWithTenv (tenv0, extend (tenv1, I1, T, f, g))
= extend (extendWithTenv (tenv0, tenv1), I1, T, f, g)
lookupType (empty(), I1)
= VOID
lookupType (extend (tenv, I1, T, f, g), I1)
= T
lookupType (extend (tenv, I2, T, f, g), I1)
= lookupType (tenv, I1) if I1 != I2
lookupType (extendWithClass(tenv, R, tenv1, tenv2), I1)
= VOID
lookupFinal (empty(), I1)
= true
lookupFinal (extend (tenv, I1, T, f, g), I1)
= f
lookupFinal (extend (tenv, I2, T, f, g), I1)
= lookupFinal (tenv, I1) if I1 != I2
lookupFinal (extendWithClass (tenv, R, tenv1, tenv2), I1)
= true
lookupGlobal (empty(), I1)
= true
lookupGlobal (extend (tenv, I1, T, f, g), I1)
= g
lookupGlobal (extend (tenv, I2, T, f, g), I1)
= lookupGlobal (tenv, I1) if I1 != I2
lookupGlobal (extendWithClass (tenv, R, tenv1, tenv2), I1)
= true
lookupStatic (empty(), I1)
= error()
lookupStatic (extend (tenv, I1, T, f, g), I1)
= error()
lookupStatic (extend (tenv, I2, T, f, g), I1)
= lookupStatic (tenv, I1) if I1 != I2
lookupStatic (extendWithClass (tenv, R1, tenv1, tenv2), R1)
= tenv1
lookupStatic (extendWithClass (tenv, R2, tenv1, tenv2), R1)
= lookupStatic (tenv, I1) if R1 != R2
lookupDynamic (empty(), I1)
= error()
lookupDynamic (extend (tenv, I1, T, f, g), I1)
= error()
lookupDynamic (extend (tenv, I2, T, f, g), I1)
= lookupDynamic (tenv, I1) if I1 != I2
lookupDynamic (extendWithClass (tenv, R1, tenv1, tenv2), R1)
= tenv2
lookupDynamic (extendWithClass (tenv, R2, tenv1, tenv2), R1)
= lookupDynamic (tenv, I1) if R1 != R2
length (empty())
= 0
length (extend (tenv, I1, T, f, g))
= 1 + length (tenv)
length (extendWithClass (tenv, R, tenv1, tenv2))
= 0
identifier (extend (tenv, I1, T, f, g), 0)
= I1
identifier (extend (tenv, I1, T, f, g), n)
= identifier (tenv, n - 1) if n > 0
isError (error()) = true
isError (empty()) = false
isError (extend(_, _, _, _, _)) = false
isError (extendWithClass(_, _, _, _)) = false
Informal specification:
The basic constructors are error, empty, extend, and extendWithClass.
A Tenv returned by error() can be distinguish from those returned by
the other basic constructors by using the isError predicate. The
empty() Tenv binds no identifiers.
extend(tenv,I,T,f, g) returns an extension of tenv in which the
identifier I is bound to the type T, is final iff f, and is global
iff g.
extendWithClass(tenv,R,tenv1,tenv2) returns an extension of tenv in
which the class name R is bound to two type environments, one for its
static constants and methods (tenv1) and one for its dynamic fields
(tenv2).
lookupType(tenv,I) returns the type of I in tenv.
lookupFinal(tenv,I) tells whether I is final in tenv.
lookupGlobal(tenv,I) tells whether I is global in tenv.
lookupStatic(tenv,R) returns the static environment associated with
the class name R in tenv.
lookupDynamic(tenv,R) returns the dynamic environment associated with
the class name R in tenv.
length(tenv) returns the number of ordinary identifiers that are bound
within tenv. The identifier(_,_) operation provides a way to iterate
over the ordinary identifiers that are bound within a type environment.
An ordinary identifier I is bound within tenv iff there exists some
int i such that 0 <= i < length(tenv) and
identifier(tenv,i) returns I.
Note that there may exist more than one integer i that returns the same
identifier I.
The initial() operation returns a type environment that contains bindings
for the standard library of quirk20. This standard library is expected
to evolve rapidly during the development of a quirk20 compiler.