ExprLib

DATE : 7 August 2001
AUTHOR : underdarkPrime
ADDRESS : underdarkPrime@yahoo.com

Index


  1. freshenTyVars
  2. getSubs_TofreshenTyVars
  3. inventNewVarName
  4. tiInfer

Provide utilities to work on 'expression' (value of type ExprDD.Expr).

inventNewVarName

inventNewVarName : int -> string

inventNewVarName i



Converts i to a string representing a variable name. Each (non-negative) integer i will be translated to a unique name. This used on places where fresh variable names need to be generated.

freshenTyVars

freshenTyVars : int -> TypeDD.Type -> (int * TypeDD.Type)

freshenTyVars i ty



Renames all type variables occuring in ty with new names, using i as the base counter to generate new names. It also returns the next free integer (to be used to generate the next fresh type variable).

getSubs_TofreshenTyVars

getSubs_TofreshenTyVars : int -> TypeDD.Type -> (int * (string * TypeDD.Type) list)

getSubs_TofreshenTyVars i ty



Same as freshenTyVars above, but instead of producing a new type it produces the type substitution that refreshes the type variables in ty.

tiInfer

tiInfer : (string * TypeDD.Type) list -> ExprDD.Expr -> (ExprDD.Expr * TypeDD.Type)

tiInfer sc expr



A static context is a list that associates an identifier or a literal with its type. This is typically extracted from exConst.sml, plus information extracted from the variable declaration section of the target programming language.

Given a static context sc, the function tiInfer will infer the type of expr, and will also produce a new expression in which all identifiers and literals have been correctly typed.

Type inference goes in a number of phases. It is easier to explain it by example. Let say we have an expression:

(x=y) /\ (!x: hd x = t : hd t = u) ==> (x=1)
The parser will buid an Expr tree, in which all identifiers have the type a. Given this tree, tiInfer works as follows:
  1. It consults the static context. Identifiers appearing in the static context will be typed accordingly. However, the type variables are renamed to be fresh. So the two hd's above will have different types, e.g. [e]->e and [g]->g. Notice that they should indeed have different type. So had we type them equal, say [e]->e, type unification will later fail.

  2. Each identifier which do not occur in the static context is given the type a', in which a' is fresh. Note that the x in x=y and in x=1 should get the same initial type variable. Whereas the x in the quantification should get a different type variable (because of the bounding).

    So, after the above two steps, the expression has the following typing (we will not write down the type of ALL identifiers in the expression):

    ((x:a)=(y:b)) 
    
    (/\:c->c->bool) 
    
    (!(x:d): (hd:[e]->e) (x:d) = (t:f) : (hd:[g]->g) (t:f) = (u:h)) 
    
    (==>:i->i->bool) 
    
    ((x:a)=1)
    
    
    The above two steps are carried out by the help function tyPhaseOne.

  3. We recursively unify the types in the resulting expression. This is done by the function tiInfer0. The funtion returns a unifier (type substitution) and the infered type.
  4. The resulting unifier is applied by to the original expression to correctly type all indentifiers in the expression. This is done by the function tySpec. After this we get the correct type:
    ((x:int)=(y:int)) 
    
    (/\:bool->bool->bool) 
    
    (!(x:[[h]]): (hd:[[h]]->[h]) (x:[[h]]) = (t:[h]) : (hd:[h]->h) (t:[h]) = (u:h)) 
    
    (==>:bool->bool->bool) 
    
    ((x:int)=1)
    
    
  5. Finally, the resulting typing is also refreshed with base 0, and get this:
    ((x:int)=(y:int)) 
    
    (/\:bool->bool->bool) 
    
    (!(x:[[a]]): (hd:[[a]]->[a]) (x:[[a]]) = (t:[a]) : (hd:[a]->a) (t:[a]) = (u:a)) 
    
    (==>:bool->bool->bool) 
    
    ((x:int)=1)
    
    

Generated by mosmldoc --underdarkPrime