`LazySets.jl` as case study

[goretkin]

Types at https://github.com/JuliaReach/LazySets.jl/tree/master/src/LazyOperations could be subsumed by the referencing "eager"/"concrete" operations.

For example

struct Translation{N, VN<:AbstractVector{N}, S<:LazySet{N}} <: AbstractAffineMap{N, S}
    X::S
    v::VN
    # [...]
end

Translation(X, v)

could be @fix LazySets.translate(X, v)

and the concretize operation concretize(Translation(X,v)) would be translate(X, v) ? The reason it is a case study is because it's hard to reconcile whether "eager" or "lazy" is the default. One of the intentions of FixArgs.jl is to take a system that is eager by default and allow it to be lazy.

[goretkin]

with ] add FixArgs#nested (see Manifest.toml for full details)

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

output

concretization evalautes to the same value:
cap_now_concrete == cap_fix_concrete = true

typeof(cap_now) = Intersection{Float64,CartesianProductArray{Float64,Interval{Float64,IntervalArithmetic.Interval{Float64}}},VPolytope{Float64,Array{Float64,1}}}

typeof(cap_fix) = Fix{typeof(intersection),Tuple{Fix{typeof(reduce),Tuple{Some{typeof(cartesian_product)},Some{Array{Interval{Float64,IntervalArithmetic.Interval{Float64}},1}}},NamedTuple{(),Tuple{}}},Some{VPolytope{Float64,Array{Float64,1}}}},NamedTuple{(),Tuple{}}}

value type and annotation type now:
typeof(cap_now) <: T_now = true

value type and annotation type using FixArgs.jl:
typeof(cap_fix) <: T_fix = true

pieces of the types:
typeof(cap_fix.args[1]) <: CartesianProductArray_fix = true
typeof(something(cap_fix.args[2])) <: AbstractPolyhedron = true
true