`LazySets.jl` as case study about fixargs.jl HOT 1 OPEN

using LazySets: LazySets, Interval, VPolytope
using LazySets: intersection, cartesian_product
using LazySets: concretize
using LazySets: CartesianProduct, Intersection, CartesianProductArray, AbstractPolyhedron

using FixArgs: FixArgs, @fix, Fix, @FixT
using Polyhedra: Polyhedra # LazySets: package 'Polyhedra' not loaded (it is required for executing `default_polyhedra_backend`)

a = Interval(0.1, 0.9)
b = Interval(0.2, 0.8)
c = VPolytope([[0.0, 0.0], [1.0, 0.0], [0.0, 1.0]])

cap_now = Intersection(CartesianProductArray([a, b]), c)
cap_fix = @fix intersection((@fix reduce(cartesian_product, [a, b])), c)

# Note, this definition is not needed to create `cap_fix` above!
function LazySets.cartesian_product(a::Interval, b::Interval)
    cartesian_product(
        convert(VPolytope, a),
        convert(VPolytope, b)
    )
end

cap_now_concrete = concretize(cap_now)
cap_fix_concrete = cap_fix(())

println("\nconcretization evalautes to the same value:")
@show cap_now_concrete == cap_fix_concrete

println("\n")
@show typeof(cap_now)

println("\n")
@show typeof(cap_fix)

# type annotation on `cap` argument:
# https://github.com/JuliaReach/LazySets.jl/blob/53f21cb9c26355e7f218578e5b4036c3ff0091fe/src/Approximations/overapproximate.jl#L1202
T_now{N} = Intersection{
    N, 
    <:CartesianProductArray,
    <:AbstractPolyhedron
}

println("\nvalue type and annotation type now:")
@show typeof(cap_now) <: T_now

CartesianProductArray_fix{T} = FixArgs.@FixT reduce(::typeof(cartesian_product), ::Vector{T})
# @FixT wraps with `Some` unless `nothing`, and @fix leaves `Fix` unwrapped.
# TODO allow the following to work
# Intersection_fix{#=N, =#A, B} = FixArgs.@FixT intersection(::A, ::B)

# TODO allow extra type parameters in `Fix` type (maybe in a `Tuple`)
Intersection_fix{#=N, =#A, B} = Fix{typeof(intersection),Tuple{A, B}, NamedTuple{(), Tuple{}}} where B where A
T_fix#={N}=# = Intersection_fix{#=N, =#CartesianProductArray_fix{T}, Some{B}} where {T, B <: AbstractPolyhedron}

println("\nvalue type and annotation type using FixArgs.jl:")
@show typeof(cap_fix) <: T_fix
/Users/goretkin/projects/LazySetsFixArgs/Manifest.toml


println("\npieces of the types:")
@show typeof(cap_fix.args[1]) <: CartesianProductArray_fix
@show typeof(something(cap_fix.args[2])) <: AbstractPolyhedron