The real abstract domain
type evalt = Notype
| Vvar of string
| Intero
| Mkarrow of evalt * evalt
type eval = evalt * (evalt * evalt) list
the second component of an abstract value (the constraint) represents a set of term equalities (equations)
each abstract operation
combines the constraints in the arguments and updates the result with new constraints
checks the resulting constraint for satisfiability and transforms it to solved form (by means of unification)
applies the constraint in solved form (substitution) to the type
returns the pair (type,constraint)
the partial order on eval and the corresponding lub and glb operations are obtained by lifting the definitions for evalt
Previous slide
Next slide
Back to first slide
View graphic version