fmrisc.Semantics
Class Checking

java.lang.Object
  fmrisc.Semantics.Checking

public final class Checking
extends java.lang.Object

type checking routines

Constructor Summary

Checking()

Method Summary

static Type	canonical(Type type) Returns canonical version of type (equality of two types implies the equality of the canonical version of the types).
static Type	canonicalTcc(Type type) Returns canonical version of type (equality of two types implies the equality of the canonical version of the types).
static TypeExpression	clearSubtypes(Type type, Expression exp) return version of type where subtypes and subranges (including NAT) are replaced by their base types; the corresponding constraints are returned as a formula which a corresponding expression exp has to fulfill
static Type	getBooleanType() Get canonical type BOOLEAN
static Type	getIntType() Get canonical type INT
static Type	getNatType() Get canonical type NAT
static java.util.Collection	getReferencedSymbols() get collection of referenced symbols
static boolean	hasType(Expression exp, Type etype, Type type, boolean tcc) returns true iff expr of type etype matches type.
static void	init() Initialize checking state
static boolean	isBoolean(Type type) checks if type equals BOOLEAN
static boolean	isInt(Type type) checks if type equals INT
static boolean	isNat(Type type) checks if type equals NAT
static java.lang.Integer	parseInt(java.lang.String digits) get number from digit representation
static Type	process(Expression value) type check value
static void	resetReferencedSymbols() reset collection of referenced symbols
static void	setStrongerTypes(boolean stronger) signals whether stronger type discipline is to be preserved
static void	setWeakerTypes(boolean weaker) signals whether weaker type discipline is to be preserved
static void	simplifyNames(TypedIdentifier[] vars, Environment env, Expression exp) Simplify names of local variables to their base names if no name capture can occur.
static Type	subType(Type type0, Type type1) return greatest subtype of type0 and type1 (null, if none exists) does not generate tccs.

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

Checking

public Checking()

Method Detail

init

public static void init()

Initialize checking state

setStrongerTypes

public static void setStrongerTypes(boolean stronger)

signals whether stronger type discipline is to be preserved

Parameters:

stronger - is true iff stronger type discipline is to be preserved

setWeakerTypes

public static void setWeakerTypes(boolean weaker)

signals whether weaker type discipline is to be preserved

Parameters:

weaker - is true iff weaker type discipline is to be preserved

getBooleanType

public static Type getBooleanType()

Get canonical type BOOLEAN

getIntType

public static Type getIntType()

Get canonical type INT

getNatType

public static Type getNatType()

Get canonical type NAT

isBoolean

public static boolean isBoolean(Type type)

checks if type equals BOOLEAN

Parameters:

type -

Returns:

true iff type equals BOOLEAN

isInt

public static boolean isInt(Type type)

checks if type equals INT

Parameters:

type -

Returns:

true iff type equals INT

isNat

public static boolean isNat(Type type)

checks if type equals NAT

Parameters:

type -

Returns:

true iff type equals NAT

getReferencedSymbols

public static java.util.Collection getReferencedSymbols()

get collection of referenced symbols

resetReferencedSymbols

public static void resetReferencedSymbols()

reset collection of referenced symbols

canonical

public static Type canonical(Type type)

Returns canonical version of type (equality of two types implies the equality of the canonical version of the types). No type-checking conditions are generated.

Parameters:

type - the type

Returns:

the canonical version of the type (null, if an error occured)

canonicalTcc

public static Type canonicalTcc(Type type)

Returns canonical version of type (equality of two types implies the equality of the canonical version of the types). Type-checking conditions may be generaed.

Parameters:

type - the type

Returns:

the canonical version of the type (null, if an error occured)

parseInt

public static java.lang.Integer parseInt(java.lang.String digits)

get number from digit representation

Parameters:

digits - the representation of the number as a decimal digit sequence

Returns:

the number or null if conversion not possible

process

public static Type process(Expression value)

type check value

Parameters:

value - the value to be type checked

Returns:

the type of the value or null if typechecking encountered error

hasType

public static boolean hasType(Expression exp,
                              Type etype,
                              Type type,
                              boolean tcc)

returns true iff expr of type etype matches type. may add as a side effect a type checking condition to the global context. the following general rules succeed without generating TCCs: exp: T matches T exp: SUBTYPE(p:T->BOOL) matches T the following general rule succeeds by generating a TCC: exp: T matches SUBTYPE(T) if p(exp) the following structural rules do not generate TCCs: exp: A->B matches A0->B0, if A0 matches A and B matches B0 exp: ARRAY A OF B matches ARRAY A0 OF B0, if A0 matches A and B matches B0 the following structural rules *may* generate TCCs: exp: [T,...] matches [T0,...], if exp.0: T matches T0, ... exp: [#f:T,...#] matches [#f:T0,...], if exp.f: T matches T0, ... as for arithmetic, the relationship is as follows: [a..b] < INT < REAL NAT < INT REAL0 < REAL (REAL0, i.e. REAL without 0, is only internally used to denote the second argument type of the / operator and thus trigger a TCC) the corresponding conversions from left to right succeed without generating TCCs; conversions are applied transitively. as for the conversion from right to left, we have: exp: REAL matches INT if (EXISTS (x:INT): x=exp) // we switch this rule off in order to not confuse CVCL exp: INT matches [a..b] if a <= exp && exp <= b exp: INT matches NAT if 0 <= exp exp: REAL matches REAL0 if exp /= 0 as for subranges of INT, we have exp: NAT matches [a..b] if (a <= 0 || a <= exp) && (exp <= b) exp: [a..b] matches NAT if 0 <= a || 0 <= exp exp: [a..b] matches [c..d] if (c <= a || c <= exp) && (b <= d || exp <= d) if rules are applied transitively, the conditions are appropriately conjoined, e.g. exp: REAL -> SUBTYPE(p:[a..b]->BOOL) generates the TCC (EXISTS (x:INT): x=exp) && a <= exp && exp <= b && p(exp)

Parameters:

exp - the expression (may be null if tcc is false)

etype - its type

type - the type which expr:etype is expected to match

tcc - true iff a tcc may be generated

Returns:

true iff the matching succeeds

subType

public static Type subType(Type type0,
                           Type type1)

return greatest subtype of type0 and type1 (null, if none exists) does not generate tccs.

Parameters:

type0 - a type

type1 - a type

Returns:

the subtype of type0 and type1 (or null, if none exists)

clearSubtypes

public static TypeExpression clearSubtypes(Type type,
                                           Expression exp)

return version of type where subtypes and subranges (including NAT) are replaced by their base types; the corresponding constraints are returned as a formula which a corresponding expression exp has to fulfill

Parameters:

type - the type to be cleared

exp - an expression of this type

Returns:

a pair of cleared type and formula (may be null if no condition generated) or null (if cleared type is identical to given type)

simplifyNames

public static void simplifyNames(TypedIdentifier[] vars,
                                 Environment env,
                                 Expression exp)

Simplify names of local variables to their base names if no name capture can occur.

Parameters:

vars - local variables

env - the environment in which the local variables are introduced.

exp - the expression within which the variables are referenced.