exit ~rectypes roots
updates the current state by popping a frame off the current constraint context. It is invoked when the left-hand side of a CLet
constraint is exited.
exit
examines the young fragment of the unification graph, that is, the part of the unification graph that has been created or affected since the most recent call to enter
. The following actions are taken.
First, if rectypes
is false
, then an occurs check is performed: that is, if there is a cycle in the young fragment, then an exception of the form Cycle v
is raised, where the vertex v
participates in the cycle.
Second, every young unification variable is inspected so as to determine whether its logical binding site can be hoisted up to a strictly older frame or must remain part of the most recent frame. In the latter case, the variable is generalizable. A list vs
of the generalizable variables is constructed. If a rigid variable is found to be non-generalizable, then VariableScopeEscape
is raised.
Third, for each variable root
provided by the user in the list roots
, a scheme is constructed. The body of this scheme is the variable root
. Its quantifiers are the structureless generalizable variables that are reachable from this root. They form a subset of vs
. A list of schemes schemes
, in correspondence with the list roots
, is constructed.
It may be the case that some variables in the list vs
appear in none of the quantifier lists of the constructed schemes. These variables are generalizable and unreachable from the roots. They are logically unconstrained.
The pair (vs, schemes)
is returned.