/**
 * 15.12.2.7: Reduction of Constraints (the huge itemize in this section)
 *
 * @author Martin Bravenboer
 */
module dryad/type-check/invoke/ConstraintReduction
imports
  dryad/type-check/invoke/Constraints

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
    )