Equality between zero-arity Compounds and Consts, speed improvements.

Project.toml

@@ -1,7 +1,7 @@
 name = "Julog"
 uuid = "5d8bcb5e-2b2c-4a96-a2b1-d40b3d3c344f"
 authors = ["Xuan <[email protected]>"]
-version = "0.1.11"
+version = "0.1.12"
 
 [compat]
 julia = "1.0"

src/main.jl

@@ -94,52 +94,32 @@ function unify(src::Term, dst::Term,
         src, dst = pop!(src_stack), pop!(dst_stack)
         # Unify $src with $dst
         if isa(src, Const) && isa(dst, Const)
-            if src.name in keys(funcs) src = Const(funcs[src.name]) end
-            if dst.name in keys(funcs) dst = Const(funcs[dst.name]) end
-            if src.name == dst.name # "Yes: equal constants"
-                continue
-            else # "No: diff constants"
-                success = false; break
-            end
+            success = _unify!(src::Const, dst, funcs)
+            if !success break end
         elseif isa(src, Var)
-            if isa(dst, Var) && src.name == dst.name # "Yes: same variable"
-                continue
-            elseif occurs_check && occurs_in(src, dst) # "No: src occurs in dst"
-                success = false; break
-            end
-            # Replace src with dst in stack
-            for i in 1:length(src_stack)
-                s, d = src_stack[i], dst_stack[i]
-                ss = substitute(s, src, dst)
-                if s !== ss src_stack[i] = ss end
-                dd = substitute(d, src, dst)
-                if d !== dd dst_stack[i] = dd end
-            end
-            # Replace src with dst in substitution values
-            map!(v -> substitute(v, src, dst), values(subst))
-            # Add substitution of src to dst
-            subst[src] = dst
-        elseif isa(dst, Var) # "Swap $dst and $src"
-            push!(src_stack, dst)
-            push!(dst_stack, src)
+            success = _unify!(src::Var, dst, src_stack, dst_stack,
+                              subst, occurs_check)
+            if !success break end
+        elseif isa(dst, Var)
+            success = _unify!(dst::Var, src, dst_stack, src_stack,
+                              subst, occurs_check)
+            if !success break end
         elseif isa(src, Compound) && isa(dst, Compound)
-            if src.name != dst.name # "No: diff functors"
-                success = false; break
-            elseif length(src.args) != length(dst.args) # "No: diff arity"
-                success = false; break
-            end
-            # "Yes: pushing args onto stack"
-            append!(src_stack, src.args)
-            append!(dst_stack, dst.args)
-        else
-            # Reaches here if one term is compound and the other is constant
+            success = _unify!(src::Compound, dst, src_stack, dst_stack)
+            if !success break end
+        elseif isa(src, Const) && isempty(dst.args)
+            success = _unify!(src::Const, dst, funcs)
+            if !success break end
+        elseif isa(dst, Const) && isempty(src.args)
+            success = _unify!(dst::Const, src, funcs)
+            if !success break end
+        else # Reaches here if one term is compound and the other is constant
             push!(src_defer, src)
             push!(dst_defer, dst)
         end
     end
     # Try evaluating deferred Const vs Compound comparisons
-    while length(src_defer) > 0
-        src, dst = pop!(src_defer), pop!(dst_defer)
+    for (src, dst) in zip(src_defer, dst_defer)
         src, dst = eval_term(src, subst, funcs), eval_term(dst, subst, funcs)
         if src != dst # "No: cannot unify $src and $dst after evaluation"
             success = false; break
@@ -148,6 +128,49 @@ function unify(src::Term, dst::Term,
     return success ? subst : nothing
 end
 
+function _unify!(src::Const, dst::Term, funcs::Dict=Dict())
+     if src.name != dst.name
+         src_val = get(funcs, src.name, src.name)
+         dst_val = get(funcs, dst.name, dst.name)
+         return src_val == dst_val
+     end
+     return true
+end
+
+function _unify!(src::Var, dst::Term, src_stack, dst_stack,
+                 subst, occurs_check::Bool=true)
+    if isa(dst, Var) && src.name == dst.name # "Yes: same variable"
+        return true
+    elseif occurs_check && occurs_in(src, dst) # "No: src occurs in dst"
+        return false
+    end
+    # Replace src with dst in stack
+    for i in 1:length(src_stack)
+        s, d = src_stack[i], dst_stack[i]
+        ss = substitute(s, src, dst)
+        if s !== ss src_stack[i] = ss end
+        dd = substitute(d, src, dst)
+        if d !== dd dst_stack[i] = dd end
+    end
+    # Replace src with dst in substitution values
+    map!(v -> substitute(v, src, dst), values(subst))
+    # Add substitution of src to dst
+    subst[src] = dst
+    return true
+end
+
+function _unify!(src::Compound, dst::Term, src_stack, dst_stack)
+    if src.name != dst.name # "No: diff functors"
+        return false
+    elseif length(src.args) != length(dst.args) # "No: diff arity"
+        return false
+    end
+    # "Yes: pushing args onto stack"
+    append!(src_stack, src.args)
+    append!(dst_stack, dst.args)
+    return true
+end
+
 "Handle built-in predicates"
 function handle_builtins!(queue, clauses, goal, term; options...)
     funcs = get(options, :funcs, Dict())

src/structs.jl

@@ -30,6 +30,8 @@ const Subst = Dict{Var,Term}
 Base.:(==)(t1::Term, t2::Term) = false
 Base.:(==)(t1::Const, t2::Const) = t1.name == t2.name
 Base.:(==)(t1::Var, t2::Var) = t1.name == t2.name
+Base.:(==)(t1::Const, t2::Compound) = t1.name == t2.name && isempty(t2.args)
+Base.:(==)(t1::Compound, t2::Const) = t1.name == t2.name && isempty(t1.args)
 Base.:(==)(t1::Compound, t2::Compound) =
     (t1.name == t2.name && length(t1.args) == length(t2.args) &&
             all(a1 == a2 for (a1, a2) in zip(t1.args, t2.args)))
@@ -38,7 +40,8 @@ Base.:(==)(t1::Compound, t2::Compound) =
 Base.hash(t::Term, h::UInt) = error("Not implemented.")
 Base.hash(t::Const, h::UInt) = hash(t.name, h)
 Base.hash(t::Var, h::UInt) = hash(t.name, h)
-Base.hash(t::Compound, h::UInt) = hash(t.name, hash(Tuple(t.args), h))
+Base.hash(t::Compound, h::UInt) = isempty(t.args) ?
+    hash(t.name, h) : hash(t.name, hash(Tuple(t.args), h))
 
 "Check if two clauses are exactly equal."
 Base.:(==)(c1::Clause, c2::Clause) =
@@ -77,8 +80,9 @@ function Base.show(io::IO, t::Compound)
         else
             print(io, "[", repr(head), ", ", repr(tail)[2:end-1], "]")
         end
-    elseif t.name == :cend && length(t.args) == 0
-        print(io, "[]")
+    elseif isempty(t.args)
+        # Print zero-arity compounds as constants
+        t.name == :cend ? print(io, "[]") : print(io, t.name)
     else
         # Print compound term as "name(args...)"
         print(io, t.name, "(", join([repr(a) for a in t.args], ", ")..., ")")

test/unify.jl

@@ -1,5 +1,9 @@
 @testset "Unification" begin
 
+# Test unification of constant with zero-arity compound
+subst = unify(@julog(constant), @julog(constant()))
+@test subst == @varsub {}
+
 # Test unification of nested terms
 subst = unify(@julog(f(g(X, h(X, b)), Z)), @julog(f(g(a, Z), Y)))
 @test subst == @varsub {X => a, Z => h(a, b), Y => h(a, b)}