Merge pull request #182 from ichiban/succ

add succ/2

bootstrap.pl

@@ -250,7 +250,7 @@
 :- built_in(phrase/2).
 phrase(GRBody, S0) :- phrase(GRBody, S0, []).
 
-:-built_in(select/3).
+:- built_in(select/3).
 select(E, [E|Xs], Xs).
 select(E, [X|Xs], [X|Ys]) :-
    select(E, Xs, Ys).

engine/builtin.go

@@ -2808,3 +2808,48 @@ func nth(base Integer, n, list, elem Term, k func(*Env) *Promise, env *Env) *Pro
 		return Error(TypeErrorInteger(n))
 	}
 }
+
+// Succ succeeds if s is the successor of non-negative integer x.
+func Succ(x, s Term, k func(*Env) *Promise, env *Env) *Promise {
+	switch x := x.(type) {
+	case Variable:
+		switch s := s.(type) {
+		case Variable:
+			return Error(ErrInstantiation)
+		case Integer:
+			switch {
+			case s < Integer(0):
+				return Error(domainErrorNotLessThanZero(s))
+			case s == Integer(0):
+				return Bool(false)
+			default:
+				return Unify(x, s-Integer(1), k, env)
+			}
+		default:
+			return Error(TypeErrorInteger(s))
+		}
+	case Integer:
+		if x < Integer(0) {
+			return Error(domainErrorNotLessThanZero(x))
+		}
+
+		r, err := Add(x, Integer(1))
+		if err != nil {
+			return Error(err)
+		}
+
+		switch s := s.(type) {
+		case Variable:
+			return Unify(s, r, k, env)
+		case Integer:
+			if s < Integer(0) {
+				return Error(domainErrorNotLessThanZero(s))
+			}
+			return Unify(s, r, k, env)
+		default:
+			return Error(TypeErrorInteger(s))
+		}
+	default:
+		return Error(TypeErrorInteger(x))
+	}
+}

engine/builtin_test.go

@@ -7567,3 +7567,83 @@ func TestNth1(t *testing.T) {
 		assert.Equal(t, TypeErrorInteger(Atom("foo")), err)
 	})
 }
+
+func TestSucc(t *testing.T) {
+	t.Run("x is a variable", func(t *testing.T) {
+		t.Run("s is a variable", func(t *testing.T) {
+			_, err := Succ(Variable("X"), Variable("S"), Success, nil).Force(context.Background())
+			assert.Equal(t, ErrInstantiation, err)
+		})
+
+		t.Run("s is an integer", func(t *testing.T) {
+			t.Run("ok", func(t *testing.T) {
+				x := Variable("X")
+				ok, err := Succ(x, Integer(1), func(env *Env) *Promise {
+					assert.Equal(t, Integer(0), env.Resolve(x))
+					return Bool(true)
+				}, nil).Force(context.Background())
+				assert.NoError(t, err)
+				assert.True(t, ok)
+			})
+
+			t.Run("s < 0", func(t *testing.T) {
+				_, err := Succ(Variable("X"), Integer(-1), Success, nil).Force(context.Background())
+				assert.Equal(t, domainErrorNotLessThanZero(Integer(-1)), err)
+			})
+
+			t.Run("s = 0", func(t *testing.T) {
+				ok, err := Succ(Variable("X"), Integer(0), Success, nil).Force(context.Background())
+				assert.NoError(t, err)
+				assert.False(t, ok)
+			})
+		})
+
+		t.Run("s is neither a variable nor an integer", func(t *testing.T) {
+			_, err := Succ(Variable("X"), Float(1), Success, nil).Force(context.Background())
+			assert.Equal(t, TypeErrorInteger(Float(1)), err)
+		})
+	})
+
+	t.Run("x is an integer", func(t *testing.T) {
+		t.Run("s is a variable", func(t *testing.T) {
+			s := Variable("S")
+			ok, err := Succ(Integer(0), s, func(env *Env) *Promise {
+				assert.Equal(t, Integer(1), env.Resolve(s))
+				return Bool(true)
+			}, nil).Force(context.Background())
+			assert.NoError(t, err)
+			assert.True(t, ok)
+		})
+
+		t.Run("s is an integer", func(t *testing.T) {
+			ok, err := Succ(Integer(0), Integer(1), Success, nil).Force(context.Background())
+			assert.NoError(t, err)
+			assert.True(t, ok)
+		})
+
+		t.Run("s is neither a variable nor an integer", func(t *testing.T) {
+			_, err := Succ(Integer(0), Float(1), Success, nil).Force(context.Background())
+			assert.Equal(t, TypeErrorInteger(Float(1)), err)
+		})
+
+		t.Run("x is negative", func(t *testing.T) {
+			_, err := Succ(Integer(-1), Integer(0), Success, nil).Force(context.Background())
+			assert.Equal(t, domainErrorNotLessThanZero(Integer(-1)), err)
+		})
+
+		t.Run("x is math.MaxInt64", func(t *testing.T) {
+			_, err := Succ(Integer(math.MaxInt64), Integer(0), Success, nil).Force(context.Background())
+			assert.Equal(t, ErrIntOverflow, err)
+		})
+
+		t.Run("s is negative", func(t *testing.T) {
+			_, err := Succ(Integer(0), Integer(-1), Success, nil).Force(context.Background())
+			assert.Equal(t, domainErrorNotLessThanZero(Integer(-1)), err)
+		})
+	})
+
+	t.Run("x is neither a variable nor an integer", func(t *testing.T) {
+		_, err := Succ(Float(0), NewVariable(), Success, nil).Force(context.Background())
+		assert.Equal(t, TypeErrorInteger(Float(0)), err)
+	})
+}

interpreter.go

@@ -110,6 +110,7 @@ func New(in io.Reader, out io.Writer) *Interpreter {
 	i.Register3("phrase", i.Phrase)
 	i.Register3("nth0", engine.Nth0)
 	i.Register3("nth1", engine.Nth1)
+	i.Register2("succ", engine.Succ)
 	if err := i.Exec(bootstrap); err != nil {
 		panic(err)
 	}