The basic functionality is implemented in _generate_constraints_from_to which can use naive exploration or path expressions (from Tarjan's algorithm) depending on the solver's configuration. This basic functionality is used to generate constraints in two ways. _generate_type_scheme which roughly corresponds to the use of transducer in procedure in Algorithm F.1 and _generate_primitive_constraints which corresponds to the use of transducer in Solve (Algorithm F.2).
For the first use _generate_type_scheme, I have recovered some functionality to create type vars to capture recursive types, which allows us to get good types even in the case of recursive types with no primitive leafs such as test test_recursive_no_primitive. This is something that I think we do differently from the paper, which seems to imply generating these type variables from the path expressions. The problem is that if you try to do that for an example such as test_recursive_no_primitive, you will not get any path expression.
The new type var creation for recursive types tries to introduce the minimum number of type vars (although it is not guaranteed) and does not break cycles that do not represent recursive types.
Finally, I have adapted the "instantiate" functionality to use both type schemes and sketches. Type schemes can give us constraints that relate procedure arguments among each other, constraints on primitive types, constraints describing recursive types. Sketches can give us capability information "Var alpha.l" constraints. The existentially quantified variables (anonymous variables) in type schemes need to be instantiated with fresh variable names to avoid collisions.
Apart from the reworking of constraint generation, this MR has two additional changes:
The nodes of interesting variables in the constraint graph are now annotated with a L (left) or R (right) marker, as described in Definition D.2 of the appendix. This prevents the graph from "admitting derivations that represent non-elementary proofs" (see Note 1 in section D.1). As a result, the set of final constraints that we get is smaller (less redundant).
The data structure for regular expressions have been adapted to make U and . (dot) n-ary operands, which allows for some additional simplifications of path expressions, I.e. A U (B U A) = A U B U A = A U B
The MR also adds a bunch of tests that illustrate the need and the changes of this MR.
This MR reworks the constraint generation.
The basic functionality is implemented in
_generate_constraints_from_towhich can use naive exploration or path expressions (from Tarjan's algorithm) depending on the solver's configuration. This basic functionality is used to generate constraints in two ways._generate_type_schemewhich roughly corresponds to the use of transducer in procedure in Algorithm F.1 and_generate_primitive_constraintswhich corresponds to the use of transducer in Solve (Algorithm F.2).For the first use
_generate_type_scheme, I have recovered some functionality to create type vars to capture recursive types, which allows us to get good types even in the case of recursive types with no primitive leafs such as testtest_recursive_no_primitive. This is something that I think we do differently from the paper, which seems to imply generating these type variables from the path expressions. The problem is that if you try to do that for an example such astest_recursive_no_primitive, you will not get any path expression. The new type var creation for recursive types tries to introduce the minimum number of type vars (although it is not guaranteed) and does not break cycles that do not represent recursive types.Finally, I have adapted the "instantiate" functionality to use both type schemes and sketches. Type schemes can give us constraints that relate procedure arguments among each other, constraints on primitive types, constraints describing recursive types. Sketches can give us capability information "Var alpha.l" constraints. The existentially quantified variables (anonymous variables) in type schemes need to be instantiated with fresh variable names to avoid collisions.
Apart from the reworking of constraint generation, this MR has two additional changes:
The nodes of interesting variables in the constraint graph are now annotated with a
L(left) orR(right) marker, as described in Definition D.2 of the appendix. This prevents the graph from "admitting derivations that represent non-elementary proofs" (see Note 1 in section D.1). As a result, the set of final constraints that we get is smaller (less redundant).The data structure for regular expressions have been adapted to make U and . (dot) n-ary operands, which allows for some additional simplifications of path expressions, I.e.
A U (B U A) = A U B U A = A U BThe MR also adds a bunch of tests that illustrate the need and the changes of this MR.