Skip to content

Commit

Permalink
add subsumes_term/2
Browse files Browse the repository at this point in the history
  • Loading branch information
ichiban committed Feb 11, 2022
1 parent c552b76 commit e568962
Show file tree
Hide file tree
Showing 4 changed files with 53 additions and 0 deletions.
14 changes: 14 additions & 0 deletions engine/builtin.go
Original file line number Diff line number Diff line change
Expand Up @@ -164,6 +164,20 @@ func UnifyWithOccursCheck(t1, t2 Term, k func(*Env) *Promise, env *Env) *Promise
return k(env)
}

// SubsumesTerm succeeds if general and specific are unifiable without binding variables in specific.
func SubsumesTerm(general, specific Term, k func(*Env) *Promise, env *Env) *Promise {
theta, ok := general.Unify(specific, true, env)
if !ok {
return Bool(false)
}

if d := theta.Simplify(general).Compare(specific, env); d != 0 {
return Bool(false)
}

return k(env)
}

// TypeVar checks if t is a variable.
func TypeVar(t Term, k func(*Env) *Promise, env *Env) *Promise {
if _, ok := env.Resolve(t).(Variable); !ok {
Expand Down
20 changes: 20 additions & 0 deletions engine/builtin_test.go
Original file line number Diff line number Diff line change
Expand Up @@ -344,6 +344,26 @@ func TestUnifyWithOccursCheck(t *testing.T) {
})
}

func TestSubsumesTerm(t *testing.T) {
t.Run("ok", func(t *testing.T) {
ok, err := SubsumesTerm(Variable("X"), Atom("a"), Success, nil).Force(context.Background())
assert.NoError(t, err)
assert.True(t, ok)
})

t.Run("not unifiable", func(t *testing.T) {
ok, err := SubsumesTerm(Atom("a"), Atom("b"), Success, nil).Force(context.Background())
assert.NoError(t, err)
assert.False(t, ok)
})

t.Run("specific-general", func(t *testing.T) {
ok, err := SubsumesTerm(Atom("a"), Variable("X"), Success, nil).Force(context.Background())
assert.NoError(t, err)
assert.False(t, ok)
})
}

func TestTypeVar(t *testing.T) {
t.Run("var", func(t *testing.T) {
ok, err := TypeVar(NewVariable(), Success, nil).Force(context.Background())
Expand Down
1 change: 1 addition & 0 deletions interpreter.go
Original file line number Diff line number Diff line change
Expand Up @@ -40,6 +40,7 @@ func New(in io.Reader, out io.Writer) *Interpreter {
i.Register1("throw", engine.Throw)
i.Register2("=", engine.Unify)
i.Register2("unify_with_occurs_check", engine.UnifyWithOccursCheck)
i.Register2("subsumes_term", engine.SubsumesTerm)
i.Register2("=..", engine.Univ)
i.Register2("copy_term", engine.CopyTerm)
i.Register3("arg", engine.Arg)
Expand Down
18 changes: 18 additions & 0 deletions interpreter_test.go
Original file line number Diff line number Diff line change
Expand Up @@ -612,3 +612,21 @@ sentence --> noun_phrase, verb_phrase.
// Sentence = [the boy likes]
// Rest = [scares the boy]
}

func ExampleInterpreter_Query_subsumes_term() {
i := New(nil, nil)
fmt.Printf("%t\n", i.QuerySolution(`subsumes_term(a, a).`).Err() == nil)
fmt.Printf("%t\n", i.QuerySolution(`subsumes_term(f(X,Y), f(Z,Z)).`).Err() == nil)
fmt.Printf("%t\n", i.QuerySolution(`subsumes_term(f(Z,Z), f(X,Y)).`).Err() == nil)
fmt.Printf("%t\n", i.QuerySolution(`subsumes_term(g(X), g(f(X))).`).Err() == nil)
fmt.Printf("%t\n", i.QuerySolution(`subsumes_term(X, f(X)).`).Err() == nil)
fmt.Printf("%t\n", i.QuerySolution(`subsumes_term(X, Y), subsumes_term(Y, f(X)).`).Err() == nil)

// Output:
// true
// true
// false
// false
// false
// true
}

0 comments on commit e568962

Please sign in to comment.