# The MIT License (MIT)

# Copyright (c) 2016-2024 Objectionary.com

# Permission is hereby granted, free of charge, to any person obtaining a copy
# of this software and associated documentation files (the "Software"), to deal
# in the Software without restriction, including without limitation the rights
# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
# copies of the Software, and to permit persons to whom the Software is
# furnished to do so, subject to the following conditions:

# The above copyright notice and this permission notice shall be included
# in all copies or substantial portions of the Software.

# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
# FITNESS FOR A PARTICULAR PURPOSE AND NON-INFRINGEMENT. IN NO EVENT SHALL THE
# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
# SOFTWARE.

title: "Rules for Java Streams"
rules:
  - name: "[java.util.Stream] map ↦ for-each"
    description: |
      Replacing Java Stream's map with a for-each loop.
    context:
    forall:
      - '!τ1'
      - '!b1'
      - '!b2'
      - '!t1'
      - '!B1'
    pattern: |
       ⟦
        !τ1 ↦ !b1.java_util_Stream$map(α0 ↦ !b2) * !t1,
        !B1
       ⟧
    result: |
      ⟦
        !τ2 ↦ !b1,
        !τ3 ↦ Φ.opeo.map-for-each(
          α0 ↦ ξ.!τ2,
          α1 ↦ !b2
        ),
        !τ1 ↦ ξ.!τ3 * !t1,
        !B1
      ⟧
    fresh:
      - name: '!τ2'
        prefix: 'foreach_body'
      - name: '!τ3'
        prefix: 'java_util_Stream$map_result'
    when: []
    tests:
      - name: Simple map to for-each example works
        input: |
          ⟦
            list ↦ ∅,
            result ↦ ξ.list.java_util_Stream$filter(
              α0 ↦ ⟦
                el ↦ ∅,
                φ ↦ ξ.el.equals(
                  α0 ↦ Φ.org.eolang.string(as-bytes ↦ Φ.org.eolang.bytes (Δ ⤍ 00-))
                ).not
              ⟧
            ).java_util_Stream$map(
              α0 ↦ ⟦
                el ↦ ∅,
                φ ↦ Φ.java_util_Integer.parseInt(
                  α0 ↦ ξ.el
                )
              ⟧
            ).java_util_Stream$toList
          ⟧
        output:
          - |
            ⟦
              foreach_body$1 ↦ ξ.list.java_util_Stream$filter (α0 ↦ ⟦
                el ↦ ∅, φ ↦ ξ.el.equals (α0 ↦ Φ.org.eolang.string (as-bytes ↦ Φ.org.eolang.bytes (Δ ⤍ 00-))).not
              ⟧),
              java_util_Stream$map_result$1 ↦ Φ.opeo.map-for-each (α0 ↦ ξ.foreach_body$1, α1 ↦ ⟦
                el ↦ ∅, φ ↦ Φ.java_util_Integer.parseInt (α0 ↦ ξ.el)
              ⟧),
              result ↦ ξ.java_util_Stream$map_result$1.java_util_Stream$toList, list ↦ ∅
            ⟧