mirror of
https://github.com/AdaCore/alt-ergo.git
synced 2026-02-12 12:39:26 -08:00
b26bcaabb7
* Do not erase type constraints in `Ty.fresh`
The purpose of the function `Ty.fresh` is to replace all the type
variables occurring in its input type by fresh type variables. This
function is only used by the legacy typechecker in order to simulate
local typechecking contexts. We have to perform this substitution before
unifying types because the unification function [Ty.unify] used by the
legacy frontend is destructive.
The variant `Tvar` of `Ty.t` is a node used in a kind of union-find that
store type constraints. It is important to preserve these constraints in
`Ty.fresh`. So we have to generate a fresh type variable only if `Tvar`
is the representative of its own class in the implicit union-find, that
is if the `value` is field is `None`. Otherwise, we have to call
recursively `Ty.fresh` on `value`.
Notice that this patch proceed a little bit differently. We use the
function `Ty.shorten` that performs two tasks:
1. Path compressing of the implicit union-find. This task is performed
in place.
2. Return a type whose `Tvar` subterms that are not roots in the union-find
have been replaced by a concrete type or a free type variable.
So in particular `Ty.shorten t` does not contain subterms of the form
`Ty.Tvar { value = Some _; _ }` (but `t` can still contain such
subterms after calling the function).