Skip to content

Commit

Permalink
Merge pull request #269 from ichiban/simplify-env-unify
Browse files Browse the repository at this point in the history 
simplify env.Unify() by unexposing occursCheck flag
  • Loading branch information
@ichiban
ichiban authored Dec 2, 2022
2 parents 8dff549 + 51aa675 commit 46b6c0d
Show file tree
Hide file tree
Showing 7 changed files with 45 additions and 36 deletions.
10 changes: 5 additions & 5 deletions engine/builtin.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -146,7 +146,7 @@ func CallNth(vm *VM, goal, nth Term, k Cont, env *Env) *Promise {

// Unify unifies x and y without occurs check (i.e., X = f(X) is allowed).
func Unify(_ *VM, x, y Term, k Cont, env *Env) *Promise {
env, ok := env.Unify(x, y, false)
env, ok := env.Unify(x, y)
if !ok {
return Bool(false)
}
Expand All @@ -155,7 +155,7 @@ func Unify(_ *VM, x, y Term, k Cont, env *Env) *Promise {

// UnifyWithOccursCheck unifies x and y with occurs check (i.e., X = f(X) is not allowed).
func UnifyWithOccursCheck(_ *VM, x, y Term, k Cont, env *Env) *Promise {
env, ok := env.Unify(x, y, true)
env, ok := env.unifyWithOccursCheck(x, y)
if !ok {
return Bool(false)
}
Expand All @@ -164,7 +164,7 @@ func UnifyWithOccursCheck(_ *VM, x, y Term, k Cont, env *Env) *Promise {

// SubsumesTerm succeeds if general and specific are unifiable without binding variables in specific.
func SubsumesTerm(_ *VM, general, specific Term, k Cont, env *Env) *Promise {
theta, ok := env.Unify(general, specific, true)
theta, ok := env.unifyWithOccursCheck(general, specific)
if !ok {
return Bool(false)
}
Expand Down Expand Up @@ -739,7 +739,7 @@ func collectionOf(vm *VM, agg func([]Term, *Env) Term, template, goal, instances
ks = append(ks, func(context.Context) *Promise {
env := env
for _, w = range wList {
env, _ = env.Unify(witness, w, false)
env, _ = env.Unify(witness, w)
}
return Unify(vm, agg(tList, env), instances, k, env)
})
Expand Down Expand Up @@ -932,7 +932,7 @@ func Catch(vm *VM, goal, catcher, recover Term, k Cont, env *Env) *Promise {
e = Exception{term: atomError.Apply(NewAtom("system_error"), NewAtom(err.Error()))}
}

env, ok := env.Unify(catcher, e.term, false)
env, ok := env.Unify(catcher, e.term)
if !ok {
return nil
}
Expand Down
26 changes: 13 additions & 13 deletions engine/builtin_test.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -370,7 +370,7 @@ func TestUnify(t *testing.T) {
t.Run(tt.title, func(t *testing.T) {
ok, err := Unify(nil, tt.x, tt.y, func(env *Env) *Promise {
for k, v := range tt.env {
_, ok := env.Unify(k, v, false)
_, ok := env.Unify(k, v)
assert.True(t, ok)
}
return Bool(true)
Expand Down Expand Up @@ -424,7 +424,7 @@ func TestUnifyWithOccursCheck(t *testing.T) {
t.Run(tt.title, func(t *testing.T) {
ok, err := UnifyWithOccursCheck(nil, tt.x, tt.y, func(env *Env) *Promise {
for k, v := range tt.env {
_, ok := env.Unify(k, v, false)
_, ok := env.Unify(k, v)
assert.True(t, ok)
}
return Bool(true)
Expand Down Expand Up @@ -609,7 +609,7 @@ func TestFunctor(t *testing.T) {
t.Run(tt.title, func(t *testing.T) {
ok, err := Functor(nil, tt.term, tt.name, tt.arity, func(env *Env) *Promise {
for k, v := range tt.env {
_, ok := env.Unify(k, v, false)
_, ok := env.Unify(k, v)
assert.True(t, ok)
}
return Bool(true)
Expand Down Expand Up @@ -1468,7 +1468,7 @@ func TestBagOf(t *testing.T) {
}
_, err := BagOf(&vm, tt.template, tt.goal, tt.instances, func(env *Env) *Promise {
for k, v := range tt.env[0] {
_, ok := env.Unify(v, k, false)
_, ok := env.Unify(v, k)
assert.True(t, ok)
}
tt.env = tt.env[1:]
Expand Down Expand Up @@ -1860,7 +1860,7 @@ func TestSetOf(t *testing.T) {
}
_, err := SetOf(&vm, tt.template, tt.goal, tt.instances, func(env *Env) *Promise {
for k, v := range tt.env[0] {
_, ok := env.Unify(v, k, false)
_, ok := env.Unify(v, k)
assert.True(t, ok)
}
tt.env = tt.env[1:]
Expand Down Expand Up @@ -1923,7 +1923,7 @@ func TestFindAll(t *testing.T) {
t.Run(tt.title, func(t *testing.T) {
ok, err := FindAll(&vm, tt.template, tt.goal, tt.instances, func(env *Env) *Promise {
for k, v := range tt.env {
_, ok := env.Unify(v, k, false)
_, ok := env.Unify(v, k)
assert.True(t, ok)
}
return Bool(true)
Expand Down Expand Up @@ -3739,7 +3739,7 @@ func TestClose(t *testing.T) {
t.Run("force but the argument is a variable", func(t *testing.T) {
var vm VM
_, err := Close(&vm, &Stream{}, List(atomForce.Apply(NewVariable())), Success, nil).Force(context.Background())
_, ok := NewEnv().Unify(domainError(validDomainStreamOption, atomForce.Apply(NewVariable()), nil).term, err.(Exception).term, false)
_, ok := NewEnv().Unify(domainError(validDomainStreamOption, atomForce.Apply(NewVariable()), nil).term, err.(Exception).term)
assert.True(t, ok)
})

Expand Down Expand Up @@ -3913,7 +3913,7 @@ func TestWriteTerm(t *testing.T) {
if tt.err == nil {
assert.NoError(t, err)
} else if te, ok := tt.err.(*Exception); ok {
_, ok := NewEnv().Unify(te.term, err.(*Exception).term, false)
_, ok := NewEnv().Unify(te.term, err.(*Exception).term)
assert.True(t, ok)
}
if tt.outputPattern == nil {
Expand Down Expand Up @@ -5662,7 +5662,7 @@ func TestAtomChars(t *testing.T) {
t.Run(tt.title, func(t *testing.T) {
ok, err := AtomChars(nil, tt.atom, tt.list, func(env *Env) *Promise {
for k, v := range tt.env {
_, ok := env.Unify(k, v, false)
_, ok := env.Unify(k, v)
assert.True(t, ok)
}
return Bool(true)
Expand Down Expand Up @@ -5727,7 +5727,7 @@ func TestAtomCodes(t *testing.T) {
t.Run(tt.title, func(t *testing.T) {
ok, err := AtomCodes(nil, tt.atom, tt.list, func(env *Env) *Promise {
for k, v := range tt.env {
_, ok := env.Unify(k, v, false)
_, ok := env.Unify(k, v)
assert.True(t, ok)
}
return Bool(true)
Expand Down Expand Up @@ -5821,7 +5821,7 @@ func TestNumberChars(t *testing.T) {

t.Run("list-ish", func(t *testing.T) {
_, err := NumberChars(nil, Integer(0), PartialList(NewAtom("b"), NewVariable()), Success, nil).Force(context.Background())
_, ok := NewEnv().Unify(err.(Exception).Term(), typeError(validTypeList, PartialList(NewAtom("b"), NewVariable()), nil).Term(), false)
_, ok := NewEnv().Unify(err.(Exception).Term(), typeError(validTypeList, PartialList(NewAtom("b"), NewVariable()), nil).Term())
assert.True(t, ok)
})
})
Expand Down Expand Up @@ -6054,7 +6054,7 @@ func TestStreamProperty(t *testing.T) {
t.Run(tt.title, func(t *testing.T) {
ok, err := StreamProperty(&vm, tt.stream, tt.property, func(env *Env) *Promise {
for k, v := range tt.env[0] {
_, ok := env.Unify(k, v, false)
_, ok := env.Unify(k, v)
assert.True(t, ok)
}
tt.env = tt.env[1:]
Expand Down Expand Up @@ -7359,7 +7359,7 @@ func TestAppend(t *testing.T) {
t.Run(tt.title, func(t *testing.T) {
ok, err := Append(nil, tt.xs, tt.ys, tt.zs, func(env *Env) *Promise {
for k, v := range tt.env[0] {
_, ok := env.Unify(k, v, false)
_, ok := env.Unify(k, v)
assert.True(t, ok)
}
tt.env = tt.env[1:]
Expand Down
17 changes: 13 additions & 4 deletions engine/env.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -264,7 +264,16 @@ func (e *Env) appendFreeVariables(fvs variables, t Term) variables {
return fvs
}

func (e *Env) Unify(x, y Term, occursCheck bool) (*Env, bool) {
// Unify unifies 2 terms.
func (e *Env) Unify(x, y Term) (*Env, bool) {
return e.unify(x, y, false)
}

func (e *Env) unifyWithOccursCheck(x, y Term) (*Env, bool) {
return e.unify(x, y, true)
}

func (e *Env) unify(x, y Term, occursCheck bool) (*Env, bool) {
x, y = e.Resolve(x), e.Resolve(y)
switch x := x.(type) {
case Variable:
Expand All @@ -279,7 +288,7 @@ func (e *Env) Unify(x, y Term, occursCheck bool) (*Env, bool) {
case Compound:
switch y := y.(type) {
case Variable:
return e.Unify(y, x, occursCheck)
return e.unify(y, x, occursCheck)
case Compound:
if x.Functor() != y.Functor() {
return e, false
Expand All @@ -289,7 +298,7 @@ func (e *Env) Unify(x, y Term, occursCheck bool) (*Env, bool) {
}
var ok bool
for i := 0; i < x.Arity(); i++ {
e, ok = e.Unify(x.Arg(i), y.Arg(i), occursCheck)
e, ok = e.unify(x.Arg(i), y.Arg(i), occursCheck)
if !ok {
return e, false
}
Expand All @@ -301,7 +310,7 @@ func (e *Env) Unify(x, y Term, occursCheck bool) (*Env, bool) {
default: // atomic
switch y := y.(type) {
case Variable:
return e.Unify(y, x, occursCheck)
return e.unify(y, x, occursCheck)
default:
return e, x == y
}
Expand Down
2 changes: 1 addition & 1 deletion engine/text_test.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -366,7 +366,7 @@ func TestVM_Consult(t *testing.T) {
ok, err := Consult(&vm, tt.files, Success, nil).Force(context.Background())
assert.Equal(t, tt.ok, ok)
if e, ok := tt.err.(Exception); ok {
_, ok := NewEnv().Unify(e.Term(), err.(Exception).Term(), false)
_, ok := NewEnv().Unify(e.Term(), err.(Exception).Term())
assert.True(t, ok)
} else {
assert.Equal(t, tt.err, err)
Expand Down
20 changes: 10 additions & 10 deletions engine/vm.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -229,7 +229,7 @@ func (*VM) execConst(r *registers) *Promise {
x := r.xr[r.pc[0].operand]
arest := NewVariable()
var ok bool
r.env, ok = r.env.Unify(r.args, Cons(x, arest), false)
r.env, ok = r.env.Unify(r.args, Cons(x, arest))
if !ok {
return Bool(false)
}
Expand All @@ -242,7 +242,7 @@ func (*VM) execVar(r *registers) *Promise {
v := r.vars[r.pc[0].operand]
arest := NewVariable()
var ok bool
r.env, ok = r.env.Unify(Cons(v, arest), r.args, false)
r.env, ok = r.env.Unify(Cons(v, arest), r.args)
if !ok {
return Bool(false)
}
Expand All @@ -255,7 +255,7 @@ func (vm *VM) execFunctor(r *registers) *Promise {
pi := r.xr[r.pc[0].operand].(procedureIndicator)
arg, arest := NewVariable(), NewVariable()
var ok bool
r.env, ok = r.env.Unify(r.args, Cons(arg, arest), false)
r.env, ok = r.env.Unify(r.args, Cons(arg, arest))
if !ok {
return Bool(false)
}
Expand All @@ -281,13 +281,13 @@ func (vm *VM) execFunctor(r *registers) *Promise {

func (*VM) execPop(r *registers) *Promise {
var ok bool
r.env, ok = r.env.Unify(r.args, List(), false)
r.env, ok = r.env.Unify(r.args, List())
if !ok {
return Bool(false)
}
r.pc = r.pc[1:]
a, arest := NewVariable(), NewVariable()
r.env, ok = r.env.Unify(r.astack, Cons(a, arest), false)
r.env, ok = r.env.Unify(r.astack, Cons(a, arest))
if !ok {
return Bool(false)
}
Expand All @@ -298,11 +298,11 @@ func (*VM) execPop(r *registers) *Promise {

func (*VM) execEnter(r *registers) *Promise {
var ok bool
r.env, ok = r.env.Unify(r.args, List(), false)
r.env, ok = r.env.Unify(r.args, List())
if !ok {
return Bool(false)
}
r.env, ok = r.env.Unify(r.astack, List(), false)
r.env, ok = r.env.Unify(r.astack, List())
if !ok {
return Bool(false)
}
Expand All @@ -316,7 +316,7 @@ func (*VM) execEnter(r *registers) *Promise {
func (vm *VM) execCall(r *registers) *Promise {
pi := r.xr[r.pc[0].operand].(procedureIndicator)
var ok bool
r.env, ok = r.env.Unify(r.args, List(), false)
r.env, ok = r.env.Unify(r.args, List())
if !ok {
return Bool(false)
}
Expand Down Expand Up @@ -361,7 +361,7 @@ func (vm *VM) execList(r *registers) *Promise {
l := r.xr[r.pc[0].operand].(Integer)
arg, arest := NewVariable(), NewVariable()
var ok bool
r.env, ok = r.env.Unify(r.args, Cons(arg, arest), false)
r.env, ok = r.env.Unify(r.args, Cons(arg, arest))
if !ok {
return Bool(false)
}
Expand All @@ -376,7 +376,7 @@ func (vm *VM) execPartial(r *registers) *Promise {
l := r.xr[r.pc[0].operand].(Integer)
arg, arest := NewVariable(), NewVariable()
var ok bool
r.env, ok = r.env.Unify(r.args, Cons(arg, arest), false)
r.env, ok = r.env.Unify(r.args, Cons(arg, arest))
if !ok {
return Bool(false)
}
Expand Down
2 changes: 1 addition & 1 deletion examples/call_go_from_prolog/main.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@ func main() {
}

// Return values by unification with the output arguments.
env, ok = env.Unify(status, engine.Integer(resp.StatusCode), false)
env, ok = env.Unify(status, engine.Integer(resp.StatusCode))
if !ok {
return engine.Bool(false)
}
Expand Down
4 changes: 2 additions & 2 deletions solutions_test.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ func TestSolutions_Close(t *testing.T) {
func TestSolutions_Next(t *testing.T) {
t.Run("ok", func(t *testing.T) {
v := engine.NewVariable()
env, _ := engine.NewEnv().Unify(v, engine.NewAtom("foo"), false)
env, _ := engine.NewEnv().Unify(v, engine.NewAtom("foo"))
more := make(chan bool, 1)
defer close(more)
next := make(chan *engine.Env, 1)
Expand Down Expand Up @@ -68,7 +68,7 @@ func TestSolutions_Scan(t *testing.T) {
varBar: engine.NewAtom("bar"),
varBaz: engine.NewAtom("baz"),
} {
env, _ = env.Unify(k, v, false)
env, _ = env.Unify(k, v)
}

sols := Solutions{
Expand Down

0 comments on commit 46b6c0d

Please sign in to comment.