```
/**
* 15.12.2.7: Reduction of Constraints (the huge itemize in this section)
*
* @author Martin Bravenboer
*/
imports

strategies

/**
* Inference of type arguments begins with a set of initial constraints of the
* form A << F, A = F, or A >> F, where A is a type of an actual parameter, and F
* is a type of a formal parameter.
*
* These constraints are reduced to a set of simpler constraints of the forms T :> X,
* T = X or T <: X, where T is a type parameter of the method.
*
* The result of this method is a list of these simpler constraints.
*
* @param List of type variables
* @type Constraint -> List(Constraint)
*/
reduce-constraint(|typevars) =
?c@Constraint(_, a, f)
; let involves-typevar = {t:
?t; <fetch({tv: ?tv; <oncetd(?tv)> t})> typevars
}
in if not(<involves-typevar> f) then
![]
else
if !a => Null() then
![]
else
<map({tv:
?tv
; if <oncetd(?tv)> f then
<reduce-real-constraint(
reduce-constraint(|typevars)
| tv
)> c
else
![]
end
})> typevars
; concat
end
end
end

/**
* Form: A << F
*/
strategies

/**
* @type Constraint -> List(Constraint)
*/
reduce-real-constraint(rec | t) =
?Constraint(LeftRightConvertible(), _, _); (
reduce-left-right-prim-constraint(rec | t)
<+ reduce-left-right-simple-constraint(rec | t)
<+ reduce-left-right-array-constraint(rec |t)
<+ reduce-left-right-generic-constraint(rec | t)
<+ ![]
)

/**
* If A is primitive type.
*
* @todo Recursive invocation of reduction or fixpoint strategy?
* @type Constraint -> List(Constraint)
*/
reduce-left-right-prim-constraint(rec | t) =
?Constraint(LeftRightConvertible(), a, f)
; where(<is-primitive-type> a)
; <rec> Constraint(LeftRightConvertible(), <boxing-conversion-of-type> a, f)

/**
* If F is Tj
*
* @type Constraint -> List(Constraint)
*/
reduce-left-right-simple-constraint(rec | t) :
Constraint(LeftRightConvertible(), a, t) -> [Constraint(SuperType(), t, a)]

/**
* If F = U[]
*
* @todo Primitive arrays introduce no constraints. Test this.
* @todo TypeVariable upper bound case.
*/
reduce-left-right-array-constraint(rec | t) :
Constraint(LeftRightConvertible(), ArrayType(v), ArrayType(u))
->
<rec> Constraint(LeftRightConvertible(), v, u)
where
<is-reference-type> v

/**
* If F has the form G< .... U .... >, where U is a type expression
*
* @type Constraint -> List(Constraint)
*/
reduce-left-right-generic-constraint(rec | t) =
?Constraint(LeftRightConvertible(), a, ClassType(tn, Some(TypeArgs(<id>))))
; helper-reduce-generic-constraint(
?ClassType(tn, Some(TypeArgs(<id>)))
, rec
| a, t
)

reduce-left-right-generic-constraint(rec | t) =
?Constraint(LeftRightConvertible(), a, InterfaceType(tn, Some(TypeArgs(<id>))))
; helper-reduce-generic-constraint(
?InterfaceType(tn, Some(TypeArgs(<id>)))
, rec
| a, t
)

/**
* If F has the form G<..., Yk-1, ? extends U, Yk+1, ...>, where U involves Tj
*
* @todo Implement.
*/

/**
* If F has the form G<..., Yk-1, ? super U, Yk+1, ...>, where U involves Tj
*
* @todo Implement.
*/

strategies

/**
* Helper used for A << F and A = F.
*
* @todo Check that u is a type expression.
* @todo Check that v is a type expression.
* @todo Should the fetch-elem be a retain-all?
* @type List(ActualTypeArg) -> List(Constraint)
*/
helper-reduce-generic-constraint(s, rec | a, t) :
us -> <map(rec); concat> cs
where
<oncetd(?t)> us  // us inolves t
; <supertypes> a
; let consider(|u) =
where(<oncetd(?t)> u)
; !Constraint(Equal(), <id>, u)

in fetch-elem(s; filter-zip(consider | us))
end
; not(?[]) => cs

/**
* Form: A = F
*/
strategies

/**
* @type Constraint -> List(Constraint)
*/
reduce-real-constraint(rec | t) =
?Constraint(Equal(), _, _); (
reduce-equal-simple-constraint(rec | t)
<+ reduce-equal-array-constraint(rec | t)
<+ reduce-equal-generic-constraint(rec | t)
<+ ![]
)

/**
* If F is Tj, then the constraint Tj = A is implied.
*
* @type Constraint -> List(Constraint)
*/
reduce-equal-simple-constraint(rec | t) :
Constraint(Equal(), a, t) -> [Constraint(Equal(), t, a)]

/**
* If F = U[] where the type U involves Tj, then if A is an array
* type V[], or a type variable with an upper bound that is an array
* type V[], where V is a reference type, this algorithm is applied
* recursively to the constraint V = U.
*
* @todo Primitive arrays introduce no constraints. Test this.
* @todo TypeVariable upper bound case.
* @type Constraint -> List(Constraint)
*/
reduce-equal-array-constraint(rec | t) :
Constraint(Equal(), ArrayType(v), ArrayType(u))
->
<rec> Constraint(Equal(), v, u)
where
<is-reference-type> v

/**
* If F has the form G< .... U .... >, where U is a type expression
*
* @type Constraint -> List(Constraint)
*/
reduce-equal-generic-constraint(rec | t) =
?Constraint(Equal(), a, ClassType(tn, Some(TypeArgs(<id>))))
; helper-reduce-generic-constraint(
?ClassType(tn, Some(TypeArgs(<id>)))
, rec
| a, t
)

reduce-equal-generic-constraint(rec | t) =
?Constraint(Equal(), a, InterfaceType(tn, Some(TypeArgs(<id>))))
; helper-reduce-generic-constraint(
?InterfaceType(tn, Some(TypeArgs(<id>)))
, rec
| a, t
)

/**
* If F has the form G<..., Yk-1, ? extends U, Yk+1, ...>, where U involves Tj
*
* @todo Implement
*/

/**
* If F has the form G<..., Yk-1, ? super U, Yk+1 ,...>, where U involves Tj
*
* @todo Implement
*/

/**
* Form: A >> F
*/
strategies

reduce-real-constraint(rec | t) =
?Constraint(RightLeftConvertible(), _, _); (
fail
<+ log(|Error(), "A >> F constraints are not yet supported", <id>)
; fail
)

```