Module UtyExprs implements data types for untyped expressions that are used to store parse trees of program expressions and specifications. Given a declaration of the used variables, the module provides also functions to convert these untyped constructs to corresponding typed constructs according to the type rules of the Quartz language.
Type  Description 


UtyExpr is the data type for untyped expressions that are generated by the parser. The following remarks should help to understand the meaning of the operators and their arguments:


a type for untyped substitutions 
Function or value  Description 
MacroDefs is a map that stores macro definitions of a Quartz file. It maps the name of the macro function to a pair (xL,tau) where xL is the list of formal arguments and tau the righthand side of the macro definition. For example, the macro definition "max(a,b) = ((a>b)?a:b)" maps the name "max" to the pair ([a,b],((a>b)?a:b)). This global variable must be assigned before calling any of the typechecking functions! 

SubstUty rho utye replaces the variables in utye as specified in the substitution rho. Note that the substitution must be clean, i.e., substituted expressions must not have free variables that are substituted like [(x,y),(y,z)] which should be rather [(x,z),(y,z)]


Typechecking of LhsExpr: Given a declaration d and an untyped expression utye, Uty2LhsExpr d utye computes a tuple (ty,e,asrt,orcL) where ty is a Quartz type, e is the lefthand side expression obtained by typing utye according to the declarations d, asrt is a list of assertions that assure the absence of runtime errors for evaluating e, and orcL is a declaration list of oracle variables that have been introduced to replace anyexpressions. The function also evaluates constant expressions and unrolls generic expressions. It computes the least general type, and where necessary, types of subexpressions are adapted to supertypes to derive a type at all. The function might fail with an InternalException holding messages why the typing failed, which may also be the case if e is not writable. 

Typechecking of LhsExpr: Uty2ReadableLhsExpr performs the same computations as Uty2LhsExpr, but additionally checks that e is also readable (it fails if that is not the case). 

Typechecking of RhsExpr: Given a declaration d and an untyped expression utye, Uty2RhsExpr d utye computes a triple (ty,e,asrt,orcL) where ty is a Quartz type, e is the (righthand side) expression obtained by typing utye according to the declarations d, asrt is a list of assertions that assure the absence of runtime errors for evaluating e, and orcL is a declaration list of oracle variables that have been introduced to remove anyexpressions. Uty2LhsExpr also checks that e is readable and fails if that is not the case. 

Typechecking Specifications: Given a declaration d and an untyped expression utye, Uty2Spec decls utye computes a tuple (phi,asrL,orcL) where phi is a specification obtained by typing utye according to the declarations, asrL is a list of assertions that assure the absence of runtime errors for evaluating phi, and orcL is a declaration list of the oracle variables that have been introduced by removing anyexpressions. 


UtyFrVars computes the set of free variables of a given untyped expression.
