diff --git a/Project.toml b/Project.toml index c05aeab..f2c1879 100644 --- a/Project.toml +++ b/Project.toml @@ -1,7 +1,7 @@ name = "Julog" uuid = "5d8bcb5e-2b2c-4a96-a2b1-d40b3d3c344f" authors = ["Xuan "] -version = "0.1.11" +version = "0.1.12" [compat] julia = "1.0" diff --git a/src/main.jl b/src/main.jl index 09072fc..8e03fda 100644 --- a/src/main.jl +++ b/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()) diff --git a/src/structs.jl b/src/structs.jl index 07942d1..635db60 100644 --- a/src/structs.jl +++ b/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], ", ")..., ")") diff --git a/test/unify.jl b/test/unify.jl index 7679b32..5f946e6 100644 --- a/test/unify.jl +++ b/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)}