diff --git a/x/logic/predicate/address_test.go b/x/logic/predicate/address_test.go index 3d44ca479..5c624dfdb 100644 --- a/x/logic/predicate/address_test.go +++ b/x/logic/predicate/address_test.go @@ -39,6 +39,12 @@ func TestBech32(t *testing.T) { }}, wantSuccess: true, }, + { + program: `okp4_addr(Addr) :- bech32_address(-('okp4', _), Addr).`, + query: `okp4_addr('okp41p8u47en82gmzfm259y6z93r9qe63l25dfwwng6').`, + wantResult: []testutil.TermResults{{}}, + wantSuccess: true, + }, { query: `bech32_address(Address, 'okp415wn30a9z4uc692s0kkx5fp5d4qfr3ac7sj9dqn').`, wantResult: []testutil.TermResults{{ diff --git a/x/logic/predicate/did_test.go b/x/logic/predicate/did_test.go index a6f3b3a0f..6f349a1cd 100644 --- a/x/logic/predicate/did_test.go +++ b/x/logic/predicate/did_test.go @@ -34,6 +34,11 @@ func TestDID(t *testing.T) { query: `did_components('did:example:123456',did_components(X,Y,_,_,_)).`, wantResult: []testutil.TermResults{{"X": "example", "Y": "'123456'"}}, }, + { + program: `is_did_key(DID) :- did_components(DID, Components), Components = did_components('key',_,_,_,_).`, + query: `is_did_key('did:key:123456').`, + wantResult: []testutil.TermResults{{}}, + }, { query: `did_components('did:example:123456',did_components(X,Y,Z,_,_)).`, wantResult: []testutil.TermResults{{"X": "example", "Y": "'123456'", "Z": "_1"}}, diff --git a/x/logic/prolog/assert_test.go b/x/logic/prolog/assert_test.go index 7119e7e68..310e42fb5 100644 --- a/x/logic/prolog/assert_test.go +++ b/x/logic/prolog/assert_test.go @@ -9,6 +9,7 @@ import ( . "github.com/smartystreets/goconvey/convey" + "github.com/okp4/okp4d/x/logic/testutil" "github.com/okp4/okp4d/x/logic/util" ) @@ -183,12 +184,10 @@ func TestWhitelistBlacklistMatches(t *testing.T) { } func TestAreGround(t *testing.T) { - groundTerm := func(value string) engine.Term { - return engine.NewAtom(value) - } - nonGroundTerm := func() engine.Term { - return engine.NewVariable() - } + X := engine.NewVariable() + Y := engine.NewVariable() + foo := engine.NewAtom("foo") + fortyTwo := engine.Integer(42) Convey("Given a test cases", t, func() { cases := []struct { @@ -198,12 +197,22 @@ func TestAreGround(t *testing.T) { }{ { name: "all terms are ground", - terms: []engine.Term{groundTerm("a"), groundTerm("b")}, + terms: []engine.Term{X, foo, foo.Apply(X), fortyTwo, engine.List(X, fortyTwo)}, expected: true, }, { - name: "one term is not ground", - terms: []engine.Term{groundTerm("a"), nonGroundTerm()}, + name: "one term is a variable", + terms: []engine.Term{X, foo, Y, foo.Apply(X)}, + expected: false, + }, + { + name: "one term is a list containing a variable", + terms: []engine.Term{X, foo, engine.List(X, Y, foo), fortyTwo}, + expected: false, + }, + { + name: "one term is a compound containing a variable", + terms: []engine.Term{X, foo, foo.Apply(X, foo.Apply(X, Y, fortyTwo)), fortyTwo}, expected: false, }, { @@ -219,8 +228,7 @@ func TestAreGround(t *testing.T) { } Convey("and an environment", func() { - env := engine.NewEnv() - + env, _ := engine.NewEnv().Unify(X, engine.NewAtom("x")) for nc, tc := range cases { Convey( fmt.Sprintf("Given the test case %s (#%d)", tc.name, nc), func() { @@ -236,3 +244,73 @@ func TestAreGround(t *testing.T) { }) }) } + +func TestAssertIsGround(t *testing.T) { + X := engine.NewVariable() + Y := engine.NewVariable() + foo := engine.NewAtom("foo") + fortyTwo := engine.Integer(42) + + Convey("Given a test cases", t, func() { + cases := []struct { + name string + term engine.Term + expected error + }{ + { + name: "A variable unified", + term: X, + }, + { + name: "an atom", + term: foo, + }, + { + name: "an integer", + term: fortyTwo, + }, + { + name: "a grounded list", + term: engine.List(foo, X, fortyTwo), + }, + { + name: "a grounded compound", + term: foo.Apply(X, foo.Apply(foo, X, fortyTwo)), + }, + { + name: "a variable", + term: Y, + expected: engine.InstantiationError(engine.NewEnv()), + }, + { + name: "a list containing a variable", + term: engine.List(foo, X, Y, fortyTwo), + expected: engine.InstantiationError(engine.NewEnv()), + }, + { + name: "a compound containing a variable", + term: foo.Apply(X, foo.Apply(X, Y, fortyTwo)), + expected: engine.InstantiationError(engine.NewEnv()), + }, + } + + Convey("and an environment", func() { + env, _ := engine.NewEnv().Unify(X, engine.NewAtom("x")) + for nc, tc := range cases { + Convey( + fmt.Sprintf("Given the test case %s (#%d)", tc.name, nc), func() { + Convey("When the function AreGround() is called", func() { + result, err := AssertIsGround(tc.term, env) + Convey("Then it should return the expected output", func() { + if tc.expected == nil { + So(result, testutil.ShouldBeGrounded) + } else { + So(err, ShouldBeError, tc.expected) + } + }) + }) + }) + } + }) + }) +} diff --git a/x/logic/testutil/logic.go b/x/logic/testutil/logic.go index f83aeb019..44f1ea6cd 100644 --- a/x/logic/testutil/logic.go +++ b/x/logic/testutil/logic.go @@ -89,3 +89,35 @@ func ReindexUnknownVariables(s prolog.TermString) prolog.TermString { return fmt.Sprintf("_%d", index) })) } + +// ShouldBeGrounded is a goconvey assertion that asserts that the given term does not hold any +// uninstantiated variables. +func ShouldBeGrounded(actual any, expected ...any) string { + if len(expected) != 0 { + return fmt.Sprintf("This assertion requires exactly %d comparison values (you provided %d).", 0, len(expected)) + } + + var containsVariable func(engine.Term) bool + containsVariable = func(term engine.Term) bool { + switch t := term.(type) { + case engine.Variable: + return true + case engine.Compound: + for i := 0; i < t.Arity(); i++ { + if containsVariable(t.Arg(i)) { + return true + } + } + } + return false + } + if t, ok := actual.(engine.Term); ok { + if containsVariable(t) { + return "Expected term to NOT hold a free variable (but it was)." + } + + return "" + } + + return fmt.Sprintf("The argument to this assertion must be a term (you provided %v).", actual) +} diff --git a/x/logic/util/prolog.go b/x/logic/util/prolog.go new file mode 100644 index 000000000..1cb08815c --- /dev/null +++ b/x/logic/util/prolog.go @@ -0,0 +1,81 @@ +package util + +import ( + "context" + "strings" + + "github.com/ichiban/prolog" + "github.com/ichiban/prolog/engine" + "github.com/samber/lo" + + sdkmath "cosmossdk.io/math" + + "github.com/okp4/okp4d/x/logic/types" +) + +// QueryInterpreter interprets a query and returns the solutions up to the given limit. +func QueryInterpreter( + ctx context.Context, i *prolog.Interpreter, query string, limit sdkmath.Uint) (*types.Answer, error) { + p := engine.NewParser(&i.VM, strings.NewReader(query)) + t, err := p.Term() + if err != nil { + return nil, err + } + + var env *engine.Env + count := sdkmath.ZeroUint() + envs := make([]*engine.Env, 0, limit.Uint64()) + _, callErr := engine.Call(&i.VM, t, func(env *engine.Env) *engine.Promise { + if count.LT(limit) { + envs = append(envs, env) + } + count = count.Incr() + return engine.Bool(count.GT(limit)) + }, env).Force(ctx) + + answerErr := lo.IfF(callErr != nil, func() string { + return callErr.Error() + }).Else("") + success := len(envs) > 0 + hasMore := count.GT(limit) + vars := parsedVarsToVars(p.Vars) + results, err := envsToResults(envs, p.Vars, i) + if err != nil { + return nil, err + } + + return &types.Answer{ + Success: success, + Error: answerErr, + HasMore: hasMore, + Variables: vars, + Results: results, + }, nil +} + +func parsedVarsToVars(vars []engine.ParsedVariable) []string { + return lo.Map(vars, func(v engine.ParsedVariable, _ int) string { + return v.Name.String() + }) +} + +func envsToResults(envs []*engine.Env, vars []engine.ParsedVariable, i *prolog.Interpreter) ([]types.Result, error) { + results := make([]types.Result, 0, len(envs)) + for _, rEnv := range envs { + substitutions := make([]types.Substitution, 0, len(vars)) + for _, v := range vars { + var expression prolog.TermString + err := expression.Scan(&i.VM, v.Variable, rEnv) + if err != nil { + return nil, err + } + substitution := types.Substitution{ + Variable: v.Name.String(), + Expression: string(expression), + } + substitutions = append(substitutions, substitution) + } + results = append(results, types.Result{Substitutions: substitutions}) + } + return results, nil +}