/* -----------------------------------------------------------------------------
Copyright 2020-2021 Kevin P. Barry

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    http://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
----------------------------------------------------------------------------- */

// Author: Kevin P. Barry [ta0kira@gmail.com]

testcase "simple inference" {
  success
}

unittest test {
  Int value1, String value2 <- Test.get<?, ?>(10, "message")
  \ Testing.checkEquals<?>(value1, 10)
  \ Testing.checkEquals<?>(value2, "message")
}

unittest testImplicit {
  Int value1, String value2 <- Test.get(10, "message")
  \ Testing.checkEquals<?>(value1, 10)
  \ Testing.checkEquals<?>(value2, "message")
}

concrete Test {
  @type get<#x, #y> (#x, #y) -> (#x, #y)
}

define Test {
  get (x, y) {
    return x, y
  }
}


testcase "wrong param count" {
  error
  require "mismatch"
  require "get"
}

unittest test {
  Int value1, String value2 <- Test.get<?>(10, "message")
}

concrete Test {
  @type get<#x, #y> (#x, #y) -> (#x, #y)
}

define Test {
  get (x, y) {
    return x, y
  }
}


testcase "inference mismatch" {
  error
  require "get"
  require "String"
  require "Int"
}

unittest test {
  String value <- Test.get<?>(10)
}

concrete Test {
  @type get<#x> (#x) -> (#x)
}

define Test {
  get (x) {
    return x
  }
}


testcase "nested inference" {
  success
}

unittest test {
  Type<Int> value <- Test.get<?>(Type<Int>.create())
}

concrete Type<#x> {
  @type create () -> (Type<#x>)
}

define Type {
  create () {
    return Type<#x>{ }
  }
}

concrete Test {
  @type get<#x> (Type<#x>) -> (Type<#x>)
}

define Test {
  get (x) {
    return x
  }
}


testcase "simple inference with qualification" {
  success
}

unittest test {
  Int value <- Test.get<?>(10)
}

concrete Test {
  @type get<#x> (#x) -> (#x)
}

define Test {
  get (x) {
    return x
  }
}


testcase "inference mismatch with qualification" {
  error
  require "get"
  require "String"
  require "Int"
}

unittest test {
  String value <- Test.get<?>(10)
}

concrete Test {
  @type get<#x> (#x) -> (#x)
}

define Test {
  get (x) {
    return x
  }
}


testcase "nested inference with qualification" {
  success
}

unittest test {
  Type<Int> value <- Test.get<?>(Type<Int>.create())
}

concrete Type<#x> {
  @type create () -> (Type<#x>)
}

define Type {
  create () {
    return Type<#x>{ }
  }
}

concrete Test {
  @type get<#x> (Type<#x>) -> (Type<#x>)
}

define Test {
  get (x) {
    return x
  }
}


testcase "inference conflict" {
  error
  require "get"
  require "#x"
}

unittest test {
  Type<Int> value <- Test.get<?>(Type<Int>.create(), "bad")
}

concrete Type<#x> {
  @type create () -> (Type<#x>)
}

define Type {
  create () {
    return Type<#x>{ }
  }
}

concrete Test {
  @type get<#x> (Type<#x>, #x) -> (Type<#x>)
}

define Test {
  get (x, _) {
    return x
  }
}


testcase "elimination by filter" {
  error
  require "get"
  require "#x"
  require "Formatted.+String"
}

unittest test {
  \ Test.get<?>(Type<String>.new())
}

concrete Type<#x> {
  @type new () -> (#self)
}

define Type {
  new () { return #self{ } }
}

concrete Test {
  @type get<#x>
    #x allows Formatted
  (Type<#x>) -> (Type<#x>)
}

define Test {
  get (x) {
    return x
  }
}


testcase "elimination by filter without param" {
  error
  require "get"
  require "#x"
  require "Formatted.+String"
}

unittest test {
  \ Test.get<Formatted, ?>(Type<String>.new())
}

concrete Type<#x> {
  @type new () -> (#self)
}

define Type {
  new () { return #self{ } }
}

concrete Test {
  @type get<#y, #x>
    #x allows #y
  (Type<#x>) -> (Type<#x>)
}

define Test {
  get (x) {
    return x
  }
}


testcase "elimination by filter including param" {
  error
  require "get"
  require "#x"
  require "String.+Type"
  require "Type.+String"
}

unittest test {
  \ Test.get<?>(Type<String>.new())
}

concrete Type<#x> {
  @type new () -> (#self)
}

define Type {
  new () {
    return #self{ }
  }
}

concrete Test {
  @type get<#x>
    #x allows Type<#x>
  (Type<#x>) -> (Type<#x>)
}

define Test {
  get (x) {
    return x
  }
}


testcase "clashing param filter in the same scope" {
  success
}

unittest test {
  \ Test.get1<Int>()
}

concrete Test {
  @type get1<#x>
    #x requires Int
  () -> ()
}

define Test {
  get1 () {
    String value <- get2<?>("message")
  }

  @type get2<#x> (#x) -> (#x)
  get2 (x) {
    return x
  }
}


testcase "mutually dependent filters" {
  success
}

unittest test {
  Type<String> x <- Type<String>.create()
  Type<String> y <- Type<String>.create()
  \ Test.get<?, ?>(x, y)
}

concrete Type<#x> {
  @type create () -> (Type<#x>)
}

define Type {
  create () {
    return Type<#x>{ }
  }
}

concrete Test {
  @type get<#x, #y>
    #x defines LessThan<#y>
    #y defines LessThan<#x>
  (Type<#x>, Type<#y>) -> ()
}

define Test {
  get (_, _) { }
}


testcase "two inferences in one filter" {
  success
}

unittest test {
  Type z <- Type.create()
  \ Test.get<?, ?, ?>(z, 1, "message")
}

@type interface Base<#x, #y> { }

concrete Type {
  defines Base<Int, String>
  @type create () -> (Type)
}

define Type {
  create () {
    return Type{ }
  }
}

concrete Test {
  @type get<#z, #x, #y>
    #z defines Base<#x, #y>
  (#z, #x, #y) -> ()
}

define Test {
  get (_, _, _) { }
}


testcase "all/any as valid lower/upper bounds" {
  compiles
}

concrete Test {
  @type call<#x, #y> (Convert<#x, #y>) -> (#x, #y)
}

define Test {
  call (_) {
    fail("this allows faking the return")
  }

  @value run () -> ()
  run () {
    any x1, all y1 <- call<?, ?>(Convert<any, all>.create())
    all x2, any y2 <- call<?, ?>(Convert<all, any>.create())
  }
}

concrete Convert<#x|#y> {
  @type create () -> (#self)
}

define Convert {
  create () {
    return #self{ }
  }
}


testcase "dependent implicit param inferred from requires" {
  failure
  require "m e s s a g e"
}

unittest test {
  \ Type.run()
}

concrete Type {
  @type run () -> ()
}

define Type {
  run () {
    \ call<?, ?>("message")
    \ call<String, ?>("message")
  }

  @type call<#x, #c>
    #c requires Formatted
    #x requires DefaultOrder<#c>
  (#x) -> ()
  call (value) {
    [Append<Formatted> & Build<String>] builder <- String.builder()
    traverse (value.defaultOrder() -> #c char) {
      \ builder.append(char).append(" ")
    }
    fail(builder.build())
  }
}


testcase "dependent implicit param inferred from defines" {
  failure
  require "String"
}

unittest test {
  \ Type.run()
}

concrete Type {
  @type run () -> ()
}

define Type {
  run () {
    \ call<?, ?>("message")
    \ call<String, ?>("message")
  }

  @type call<#x, #c>
    #x defines LessThan<#c>
  (#x) -> ()
  call (value) {
    fail(typename<#c>())
  }
}


testcase "dependent implicit param inferred from allows" {
  failure
  require "String"
}

unittest test {
  \ Type.run()
}

concrete Type {
  @type run () -> ()
}

define Type {
  run () {
    \ call<?, ?>("message")
    \ call<String, ?>("message")
  }

  @type call<#x, #c>
    #x allows #c
  (#x) -> ()
  call (value) {
    fail(typename<#c>())
  }
}


testcase "dependent implicit param inferred from reverse allows" {
  failure
  require "String"
}

unittest test {
  \ Type.run()
}

concrete Type {
  @type run () -> ()
}

define Type {
  run () {
    \ call<?, ?>("message")
    \ call<String, ?>("message")
  }

  @type call<#x, #c>
    #c allows #x
  (#x) -> ()
  call (value) {
    fail(typename<#c>())
  }
}


testcase "dependent implicit param inferred from reverse requires" {
  failure
  require "String"
}

unittest test {
  \ Type.run()
}

concrete Type {
  @type run () -> ()
}

define Type {
  run () {
    \ call<?, ?>("message")
    \ call<String, ?>("message")
  }

  @type call<#x, #c>
    #c requires #x
  (#x) -> ()
  call (value) {
    fail(typename<#c>())
  }
}


testcase "immutable filter excludes guess" {
  error
  require "#x"
  require "guesses"
  require "Formatted"
  require "immutable"
}

unittest test {
    Formatted value <- "message"
    \ Type.call<?>(value)
}

concrete Type {
  @type call<#x>
    #x immutable
    #x requires Formatted
  (#x) -> ()
}

define Type {
  call (value) { }
}


testcase "filter guess merged with arg guess" {
  failure
  require "String"
  exclude "Formatted"
}

unittest test {
    \ Type.call<?>("message")
}

concrete Type {
  @type call<#x>
    #x requires Formatted
  (#x) -> ()
}

define Type {
  call (value) {
    fail(typename<#x>())
  }
}


testcase "multiple alternative guesses" {
  error
  require "#x"
  require "guesses"
  require "Int"
  require "String"
}

unittest test {
  \ Test.call<?>(Type.create())
}

@value interface Base1<|#x> { }

@value interface Base2<|#x> { }

concrete Type {
  refines Base1<Int>
  refines Base2<String>

  @type create () -> (Type)
}

define Type {
  create () {
    return #self{ }
  }
}

concrete Test {
  @type call<#x> ([Base1<#x> | Base2<#x>]) -> ()
}

define Test {
  call (_) { }
}


testcase "unable to merge guesses" {
  error
  require "#x"
  require "guesses"
}

unittest test {
  \ Test.call<?>(Type.create())
}

@value interface Base1<#x> { }

@value interface Base2<#x> { }

concrete Type {
  refines Base1<Int>
  refines Base2<String>

  @type create () -> (Type)
}

define Type {
  create () {
    return #self{ }
  }
}

concrete Test {
  @type call<#x> ([Base1<#x> & Base2<#x>]) -> ()
}

define Test {
  call (_) { }
}


testcase "variance allows guesses to be merged using meta type" {
  failure
  require "\[Int\|String\]"
}

unittest test {
  \ Test.call<?>(Type.create())
}

@value interface Base1<|#x> { }

@value interface Base2<|#x> { }

concrete Type {
  refines Base1<Int>
  refines Base2<String>

  @type create () -> (Type)
}

define Type {
  create () {
    return #self{ }
  }
}

concrete Test {
  @type call<#x> ([Base1<#x> & Base2<#x>]) -> ()
}

define Test {
  call (_) {
    fail(typename<#x>())
  }
}


testcase "alternative guess eliminated by filter" {
  failure
  require "Int"
}

unittest test {
  \ Test.call<?>(Type.create())
}

@value interface Base1<|#x> { }

@value interface Base2<|#x> { }

concrete Type {
  refines Base1<Int>
  refines Base2<String>

  @type create () -> (Type)
}

define Type {
  create () {
    return #self{ }
  }
}

concrete Test {
  @type call<#x>
    #x requires AsChar
  ([Base1<#x> | Base2<#x>]) -> ()
}

define Test {
  call (_) {
    fail(typename<#x>())
  }
}