add CurryAtom and replace SetAtom

Author: schillic

docs/make.jl

@@ -10,8 +10,7 @@ makedocs(; sitename="MathematicalPredicates.jl",
                                 assets=["assets/aligned.css"]),
          pagesonly=true,
          pages=["Home" => "index.md",
-                "Library" => ["Predicates" => "lib/predicates.md",
-                              "LazySets integration" => "lib/LazySets.md"],
+                "Library" => ["Predicates" => "lib/predicates.md"],
                 "About" => "about.md"])
 
 deploydocs(; repo="github.com/JuliaReach/MathematicalPredicates.jl.git",

docs/src/lib/LazySets.md

@@ -39,3 +39,9 @@ Conjunction
 ```@docs
 Disjunction
 ```
+
+## CurryAtom
+
+```@docs
+CurryAtom
+```

docs/src/lib/predicates.md

@@ -0,0 +1,34 @@
+
+"""
+    CurryAtom{N,A,T} <: Predicate{N}
+
+An atomic predicate of arity `N` defined via a fixed first argument and an
+`N+1`-ary predicate.
+
+### Fields
+
+- `arg1` -- first argument
+- `p`    -- `N+1`-ary predicate that takes `arg1` as first argument
+"""
+struct CurryAtom{N,A,T<:Predicate} <: Predicate{N}
+    arg1::A
+    p::T
+
+    function CurryAtom(arg1::A, p::T; N::Int=1) where {A,T<:Predicate}
+        return new{Val{N},A,T}(arg1, p)
+    end
+end
+
+# function-like evaluation
+@inline function (ca::CurryAtom)(args...)
+    return evaluate(ca, args...)
+end
+
+function evaluate(ca::CurryAtom, args...)
+    assert_same_length(ca, args...)
+    return evaluate(ca.p, ca.arg1, args...)
+end
+
+function Base.:(==)(ca1::CurryAtom, ca2::CurryAtom)
+    return ca1.arg1 == ca2.arg1 && ca1.p == ca2.p
+end

src/CurryAtom.jl

@@ -1,13 +1,14 @@
 module MathematicalPredicates
 
-export Predicate, Atom, Negation, Conjunction, Disjunction,
+export Predicate, Atom, Negation, Conjunction, Disjunction, CurryAtom,
        evaluate
 
 include("Predicate.jl")
 include("Atom.jl")
 include("Negation.jl")
 include("Conjunction.jl")
 include("Disjunction.jl")
+include("CurryAtom.jl")
 
 # optional dependencies
 using Requires

src/MathematicalPredicates.jl

@@ -1,4 +1,4 @@
-export SetAtom, contains, is_contained_in, is_disjoint_from, intersects
+export contains, is_contained_in, is_disjoint_from, intersects
 import .LazySets: dim, project
 
 @static if VERSION >= v"1.5"
@@ -7,66 +7,35 @@ end
 
 using .LazySets: LazySet, ⊆, isdisjoint
 
-"""
-    SetAtom{S<:LazySet, T} <: Predicate{Val{1}}
-
-A unary atomic predicate defined with respect to a set.
-
-### Fields
-
-- `X` -- set
-- `f` -- function that takes the set `X` as first argument
-"""
-struct SetAtom{S<:LazySet,T} <: Predicate{Val{1}}
-    X::S
-    f::T
-
-    function SetAtom(X::S, f::T) where {S<:LazySet,T}
-        return new{S,T}(X, f)
-    end
-end
-
-# function-like evaluation
-@inline function (sa::SetAtom)(args...)
-    return evaluate(sa, args...)
-end
-
-function evaluate(sa::SetAtom, args...)
-    assert_same_length(sa, args...)
-    return sa.f(sa.X, args...)
-end
-
-function Base.:(==)(sa1::SetAtom, sa2::SetAtom)
-    return sa1.X == sa2.X && sa1.f == sa2.f
-end
+const SetAtom = CurryAtom{<:Any,<:LazySet}
 
 # ===========================
 # Dimension of set predicates
 # ===========================
 
 function dim(sa::SetAtom)
-    return dim(sa.X)
+    return dim(sa.arg1)
 end
 
 # fallback
 function dim(p::Predicate)
     throw(ArgumentError("`dim` cannot be applied to a `$(typeof(p))`; use a " *
-                        "`SetAtom` instead"))
+                        "`CurryAtom` with a set instead"))
 end
 
 # ============================
 # Projection of set predicates
 # ============================
 
 function project(sa::SetAtom, vars::AbstractVector{Int})
-    X_proj = project(sa.X, vars)
-    return SetAtom(X_proj, sa.f)
+    X_proj = project(sa.arg1, vars)
+    return CurryAtom(X_proj, sa.p)
 end
 
 # fallback
-function project(p::Predicate, vars::AbstractVector{Int})
+function project(p::Predicate, ::AbstractVector{Int})
     throw(ArgumentError("`project` cannot be applied to a `$(typeof(p))`; " *
-                        "use a `SetAtom` instead"))
+                        "use a `CurryAtom` with a set instead"))
 end
 
 function project(n::Negation, vars::AbstractVector{Int})
@@ -94,15 +63,15 @@ end
 # ==========================================
 
 function contains(X::LazySet)
-    return SetAtom(X, ⊆)
+    return CurryAtom(X, Atom(⊆; N=2))
 end
 
 function is_contained_in(X::LazySet)
-    return SetAtom(X, (X, Y) -> Y ⊆ X)
+    return CurryAtom(X, Atom((X, Y) -> Y ⊆ X; N=2))
 end
 
 function is_disjoint_from(X::LazySet)
-    return SetAtom(X, isdisjoint)
+    return CurryAtom(X, Atom(isdisjoint; N=2))
 end
 
 function intersects(X::LazySet)

src/init_LazySets.jl

@@ -13,21 +13,21 @@ P1 = is_contained_in(B1)
 P2 = contains(S)
 @test P2(S) && P2(B1) && !P2(B2)
 
-# dim is only available for SetAtom types
+# dim is only available for CurryAtom types
 A1 = Atom(x -> x > 1)
 @test_throws ArgumentError dim(A1)
 
-# project is only available for SetAtom (and their Negation) types
+# project is only available for CurryAtom (and their Negation) types
 @test_throws ArgumentError project(A1, [1])
 
 @test project(Negation(P1), [1]) == Negation(project(P1, [1]))
 
 @test dim(P1) == dim(P2) == 2
 P1_proj = project(P1, [1])
 P2_proj = project(P2, [1])
-@test P1_proj isa SetAtom && dim(P1_proj) == 1 && P1_proj.X == B1_proj
+@test P1_proj isa CurryAtom && dim(P1_proj) == 1 && P1_proj.arg1 == B1_proj
 @test P1_proj(S_proj) && P1_proj(B1_proj) && !P1_proj(B2_proj)
-@test P2_proj isa SetAtom && dim(P2_proj) == 1 && P2_proj.X == S_proj
+@test P2_proj isa CurryAtom && dim(P2_proj) == 1 && P2_proj.arg1 == S_proj
 @test P2_proj(S_proj) && P2_proj(B1_proj) && !P2_proj(B2_proj)
 
 Pc = Conjunction([P1, P2])

test/LazySets.jl

@@ -1,4 +1,4 @@
-# atom
+# Atom
 a0 = Atom(() -> true; N=0)
 a1 = Atom(x -> x > 1)
 a2 = Atom((x, y) -> x > y; N=2)
@@ -9,7 +9,7 @@ a2 = Atom((x, y) -> x > y; N=2)
 @test !evaluate(a2, 4, 5) && !a2(4, 5)
 @test evaluate(a2, 6, 5) && a2(6, 5)
 
-# negation
+# Negation
 n0 = Negation(a0)
 n1 = Negation(a1)
 n2 = Negation(a2)
@@ -20,7 +20,7 @@ n2 = Negation(a2)
 @test evaluate(n2, 4, 5) && n2(4, 5)
 @test !evaluate(n2, 6, 5) && !n2(6, 5)
 
-# conjunction
+# Conjunction
 c0 = Conjunction([(n0, Int[]), (a0, Int[])]; N=0)
 c0_3 = Conjunction([(a0, Int[]), (a0, Int[]), (a0, Int[])]; N=0)
 c1 = Conjunction([(a0, Int[]), (a1, Int[1])]; N=1)
@@ -40,7 +40,7 @@ c2_3 = Conjunction([(a0, Int[]), (a1, Int[2]), (a2, Int[2, 1])]; N=2)
 @test Conjunction([(a0, Int[]), (a0, Int[]), (a0, Int[])]) isa Conjunction{Val{0}}
 @test Conjunction([(a0, Int[]), (a1, Int[2]), (a2, Int[2, 1])]) isa Conjunction{Val{2}}
 
-# disjunction
+# Disjunction
 d0 = Disjunction([(n0, Int[]), (a0, Int[])]; N=0)
 d0_3 = Disjunction([(n0, Int[]), (n0, Int[]), (n0, Int[])]; N=0)
 d1 = Disjunction([(c0, Int[]), (a1, Int[1])]; N=1)
@@ -56,18 +56,27 @@ d2_3 = Disjunction([(a0, Int[]), (a1, Int[2]), (a2, Int[2, 1])]; N=2)
 @test evaluate(d2, 4, 5) && d2(4, 5)
 @test evaluate(d2_3, 4, 5) && d2_3(4, 5)
 
+# CurryAtom
+ca0a = CurryAtom(2, a1; N=0)
+@test evaluate(ca0a)
+ca0b = CurryAtom(0, a1; N=0)
+@test !evaluate(ca0b)
+@test ca0a == ca0a && ca0a != ca0b
+ca1 = CurryAtom(3, a2; N=1)
+@test evaluate(ca1, 2) && !evaluate(ca1, 4)
+
 # default constructor
 @test Disjunction([(a0, Int[]), (a0, Int[]), (a0, Int[])]) isa Disjunction{Val{0}}
 @test Disjunction([(a0, Int[]), (a1, Int[2]), (a2, Int[2, 1])]) isa Disjunction{Val{2}}
 
-# unary conjunction
+# unary Conjunction
 cu = Conjunction([n1, a1])
 cu_3 = Conjunction([c1, a1, d1])
 
 @test !evaluate(cu, 5) && !cu(5)
 @test evaluate(cu_3, 5) && cu_3(5)
 
-# unary disjunction
+# unary Disjunction
 du = Disjunction([n1, a1])
 du_1 = Disjunction([n1])