Skip to content

Commit

Permalink
Miscellaneous fixes
Browse files Browse the repository at this point in the history 
1. Refs to rules that produce set or object docs were not being handled
correctly when the key value was a variable that had an existing binding. The
term evaluation code must check the bindings for variables it encounters while
processing references.

2. Refs to vars were not being handled correctly when the ref contained
variables that had existing bindings. This issue was similar to (1).

3. Refs to vars bound to arrays or objects with invalid indices/keys (e.g.,
out of range) were causing evaluation to panic. Invalid indices/keys are
now treated as undefined.

4. Header field composition wasn't taking objects and arrays into account.

5. An equality expr with vars on both sides will eval to true and the vars will
be unified. However, if this was the last expression in the body, the vars are
still non-ground and so the proof should not be considered successful.

6. Move traceSuccess call into evalExpr. This way it will be applied for all
built-ins automatically.

7. Address comments from PR #27:

- Rename isDefined to isTrue in evalContextNegated
- Add comment about substituting variables in partial set/object evaluation
- Add test cases involving multiple virtual docs and subsitution
  • Loading branch information
@tsandall
tsandall committed May 3, 2016
1 parent d1c3ca5 commit ffe9e58
Show file tree
Hide file tree
Showing 6 changed files with 149 additions and 47 deletions.
97 changes: 75 additions & 22 deletions eval/topdown.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -90,6 +90,7 @@ func (ctx *TopDownContext) Child(rule *opalog.Rule, bindings *hashMap) *TopDownC
cpy.Query = rule.Body
cpy.Bindings = bindings
cpy.Previous = ctx
cpy.Index = 0
return &cpy
}

Expand Down Expand Up @@ -274,6 +275,23 @@ func dereferenceVar(v opalog.Var, ctx *TopDownContext) (interface{}, error) {
func evalContext(ctx *TopDownContext, iter TopDownIterator) error {

if ctx.Index >= len(ctx.Query) {

// Check if the bindings contain values that are non-ground. E.g.,
// suppose the query's final expression is "x = y" and "x" and "y"
// do not appear elsewhere in the query. In this case, "x" and "y"
// will be bound to each other; they will not be ground and so
// the proof should not be considered successful.
isNonGround := ctx.Bindings.Iter(func(k, v opalog.Value) bool {
if !v.IsGround() {
return true
}
return false
})

if isNonGround {
return nil
}

ctx.traceFinish()
return iter(ctx)
}
Expand All @@ -299,18 +317,18 @@ func evalContextNegated(ctx *TopDownContext, iter TopDownIterator) error {
negation.Index = 0
negation.Previous = ctx

isDefined := false
isTrue := false

err := evalContext(&negation, func(*TopDownContext) error {
isDefined = true
isTrue = true
return nil
})

if err != nil {
return err
}

if !isDefined {
if !isTrue {
return evalContext(ctx.Step(), iter)
}

Expand All @@ -323,10 +341,7 @@ func evalEq(ctx *TopDownContext, expr *opalog.Expr, iter TopDownIterator) error
a := operands[1].Value
b := operands[2].Value

return evalEqUnify(ctx, a, b, func(ctx *TopDownContext) error {
ctx.traceSuccess(expr)
return iter(ctx)
})
return evalEqUnify(ctx, a, b, iter)
}

func evalEqGround(ctx *TopDownContext, a opalog.Value, b opalog.Value, iter TopDownIterator) error {
Expand Down Expand Up @@ -592,7 +607,10 @@ func evalExpr(ctx *TopDownContext, iter TopDownIterator) error {
// this should never happen.
panic("unreachable")
}
return builtin(ctx, expr, iter)
return builtin(ctx, expr, func(ctx *TopDownContext) error {
ctx.traceSuccess(expr)
return iter(ctx)
})
case *opalog.Term:
switch tv := tt.Value.(type) {
case opalog.Boolean:
Expand Down Expand Up @@ -763,7 +781,21 @@ func evalRefRulePartialObjectDoc(ctx *TopDownContext, ref opalog.Ref, path opalo
return fmt.Errorf("not implemented: %v %v %v", ref, path, rule)
}

if !suffix[0].IsGround() {
key := plugValue(suffix[0].Value, ctx.Bindings)

// There are two cases being handled below. The first case is for when
// the object key is ground in the original expression or there is a
// binding available for the variable in the original expression.
//
// In the first case, the rule is evaluated and the value of the key variable
// in the child context is copied into the current context.
//
// In the second case, the rule is evaluated with the value of the key variable
// from this context.
//
// NOTE: if at some point multiple variables are supported here, it may be
// cleaner to generalize this (instead of having two separate branches).
if !key.IsGround() {
child := ctx.Child(rule, newHashMap())
return TopDown(child, func(child *TopDownContext) error {
key := child.Bindings.Get(rule.Key.Value)
Expand All @@ -780,7 +812,7 @@ func evalRefRulePartialObjectDoc(ctx *TopDownContext, ref opalog.Ref, path opalo
}

bindings := newHashMap()
bindings.Put(rule.Key.Value, suffix[0].Value)
bindings.Put(rule.Key.Value, key)
child := ctx.Child(rule, bindings)

return TopDown(child, func(child *TopDownContext) error {
Expand All @@ -804,7 +836,12 @@ func evalRefRulePartialSetDoc(ctx *TopDownContext, ref opalog.Ref, path opalog.R
return nil
}

if !suffix[0].IsGround() {
// See comment in evalRefRulePartialObjectDoc about the two branches below.
// The behaviour is similar for sets.

key := plugValue(suffix[0].Value, ctx.Bindings)

if !key.IsGround() {
child := ctx.Child(rule, newHashMap())
return TopDown(child, func(child *TopDownContext) error {
value := child.Bindings.Get(rule.Key.Value)
Expand All @@ -816,15 +853,16 @@ func evalRefRulePartialSetDoc(ctx *TopDownContext, ref opalog.Ref, path opalog.R
// so that expression will be defined. E.g., given a simple rule:
// "p = true :- q[x]", we say that "p" should be defined if "q"
// is defined for some value "x".
ctx = ctx.BindVar(suffix[0].Value.(opalog.Var), value)
ctx = ctx.BindVar(key.(opalog.Var), value)
ctx = ctx.BindRef(ref[:len(path)+1], opalog.Boolean(true))
return iter(ctx)
})
}

bindings := newHashMap()
bindings.Put(rule.Key.Value, suffix[0].Value)
bindings.Put(rule.Key.Value, key)
child := ctx.Child(rule, bindings)

return TopDown(child, func(child *TopDownContext) error {
// See comment above for explanation of why the reference is bound to true.
ctx = ctx.BindRef(ref[:len(path)+1], opalog.Boolean(true))
Expand Down Expand Up @@ -856,32 +894,47 @@ func evalRefRuleResult(ctx *TopDownContext, ref opalog.Ref, suffix opalog.Ref, r

case opalog.Array:
if len(suffix) > 0 {
return result.Query(suffix, func(keys map[opalog.Var]opalog.Value, value opalog.Value) error {
var pluggedSuffix opalog.Ref
for _, t := range suffix {
pluggedSuffix = append(pluggedSuffix, plugTerm(t, ctx.Bindings))
}
result.Query(pluggedSuffix, func(keys map[opalog.Var]opalog.Value, value opalog.Value) error {
ctx = ctx.BindRef(ref, value)
for k, v := range keys {
ctx = ctx.BindVar(k, v)
}
return iter(ctx)
})
// Ignore the error code. If the suffix references a non-existent document,
// the expression is undefined.
return nil
}
ctx.BindRef(ref, result)
return iter(ctx)
// This can't be hit because we have checks in the evalRefRule* functions that catch this.
panic(fmt.Sprintf("illegal value: %v %v %v", ref, suffix, result))

case opalog.Object:
if len(suffix) > 0 {
return result.Query(suffix, func(keys map[opalog.Var]opalog.Value, value opalog.Value) error {
var pluggedSuffix opalog.Ref
for _, t := range suffix {
pluggedSuffix = append(pluggedSuffix, plugTerm(t, ctx.Bindings))
}
result.Query(pluggedSuffix, func(keys map[opalog.Var]opalog.Value, value opalog.Value) error {
ctx = ctx.BindRef(ref, value)
for k, v := range keys {
ctx = ctx.BindVar(k, v)
}
return iter(ctx)
})
// Ignore the error code. If the suffix references a non-existent document,
// the expression is undefined.
return nil
}
ctx.BindRef(ref, result)
return iter(ctx)
// This can't be hit because we have checks in the evalRefRule* functions that catch this.
panic(fmt.Sprintf("illegal value: %v %v %v", ref, suffix, result))

default:
if len(suffix) > 0 {
// This is not defined because it attempts to dereference a scalar.
return nil
}
ctx = ctx.BindRef(ref, result)
Expand Down Expand Up @@ -1123,15 +1176,15 @@ func topDownQueryCompleteDoc(params *TopDownQueryParams, rules []*opalog.Rule) (
Tracer: params.Tracer,
}

isDefined := false
isTrue := false
err := TopDown(ctx, func(ctx *TopDownContext) error {
isDefined = true
isTrue = true
return nil
})
if err != nil {
return nil, err
}
if !isDefined {
if !isTrue {
return Undefined{}, nil
}

Expand Down
34 changes: 31 additions & 3 deletions eval/topdown_test.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -231,6 +231,7 @@ func TestTopDownCompleteDoc(t *testing.T) {
{`object/nested composites: {"a": [1], "b": [2], "c": [3]}`,
`p = {"a": [1], "b": [2], "c": [3]} :- true`,
`{"a": [1], "b": [2], "c": [3]}`},
{"var/var", "p = true :- x = y", ""},
}

data := loadSmallTestData()
Expand All @@ -254,6 +255,7 @@ func TestTopDownPartialSetDoc(t *testing.T) {
{"nested composites", "p[x] :- f[i] = x", `[{"xs": [1.0], "ys": [2.0]}, {"xs": [2.0], "ys": [3.0]}]`},
{"deep ref/heterogeneous", "p[x] :- c[i][j][k] = x", `[null, 3.14159, true, false, true, false, "foo"]`},
{"composite var value", "p[x] :- x = [i, a[i]]", "[[0,1],[1,2],[2,3],[3,4]]"},
{"var/var", "p[x] :- x = y", "[]"},
}

data := loadSmallTestData()
Expand All @@ -273,6 +275,8 @@ func TestTopDownPartialObjectDoc(t *testing.T) {
{"composites", "p[k] = v :- d[k] = v", `{"e": ["bar", "baz"]}`},
{"non-string key", "p[k] = v :- a[k] = v", fmt.Errorf("cannot produce object with non-string key: 0")},
{"body/join var", "p[k] = v :- a[i] = v, g[k][i] = v", `{"a": 1, "b": 2, "c": 4}`},
{"var/var key", "p[k] = v :- v = 1, k = x", "{}"},
{"var/var val", `p[k] = v :- k = "x", v = x`, "{}"},
}

data := loadSmallTestData()
Expand Down Expand Up @@ -375,6 +379,7 @@ func TestTopDownVirtualDocs(t *testing.T) {
{"input: set 2", []string{"p[x] :- q[1] = x", "q[x] :- a[i] = x"}, "[true]"},
{"input: set embedded", []string{`p[x] :- x = {"b": [q[2]]}`, `q[x] :- a[i] = x`}, `[{"b": [true]}]`},
{"input: set undefined", []string{"p = true :- q[1000]", "q[x] :- a[x] = y"}, ""},
{"input: set ground var", []string{"p[x] :- x = 1, q[x]", "q[y] :- a = [1,2,3,4], a[y] = i"}, "[1]"},
{"input: object 1", []string{"p = true :- q[1] = 2", "q[i] = x :- a[i] = x"}, "true"},
{"input: object 2", []string{"p = true :- q[1] = 0", "q[x] = i :- a[i] = x"}, "true"},
{"input: object embedded 1", []string{"p[x] :- x = [1, q[3], q[2]]", "q[i] = x :- a[i] = x"}, "[[1,4,3]]"},
Expand All @@ -384,6 +389,12 @@ func TestTopDownVirtualDocs(t *testing.T) {
{"input: object undefined key 2", []string{`p = true :- q["foo"] = 2`, `q[i] = x :- a[i] = x`}, ""},
{"input: object dereference ground", []string{`p = true :- q[0]["x"][1] = false`, `q[i] = x :- x = c[i]`}, "true"},
{"input: object defererence non-ground", []string{`p = true :- q[0][x][y] = false`, `q[i] = x :- x = c[i]`}, "true"},
{"input: object ground var key", []string{`p[y] :- x = "b", q[x] = y`, `q[k] = v :- a = {"a": 1, "b": 2}, a[k] = v`}, "[2]"},
{"input: variable binding substitution", []string{
"p[x] = y :- r[z] = y, q[x] = z",
`r[k] = v :- a = {"a": 1, "b": 2, "c": 3, "d": 4}, a[k] = v`,
`q[y] = x :- b = {"a": "a", "b": "b", "d": "d"}, b[y] = x`},
`{"a": 1, "b": 2, "d": 4}`},

// output from partial set and object docs
{"output: set", []string{"p[x] :- q[x]", "q[y] :- a[i] = y"}, "[1,2,3,4]"},
Expand All @@ -394,11 +405,26 @@ func TestTopDownVirtualDocs(t *testing.T) {
{"output: object dereference ground", []string{`p[i] :- q[i]["x"][1] = false`, `q[i] = x :- x = c[i]`}, "[0]"},
{"output: object defererence non-ground", []string{`p[r] :- q[x][y][z] = false, r = [x, y, z]`, `q[i] = x :- x = c[i]`}, `[[0, "x", 1], [0, "z", "q"]]`},

// input+output from partial set/object docs
{"i/o: objects", []string{
"p[x] :- q[x] = r[x]",
`q[x] = y :- a = {"a": 1, "b": 2, "d": 4}, a[x] = y`,
`r[t] = u :- b = {"a": 1, "b": 2, "c": 4, "d": 3}, b[t] = u`},
`["a", "b"]`},

{"i/o: undefined keys", []string{
"p[y] :- q[x], r[x] = y",
`q[x] :- a = ["a", "b", "c", "d"], a[i] = x`,
`r[k] = v :- b = {"a": 1, "b": 2, "d": 4}, b[k] = v`},
`[1, 2, 4]`},

// input/output to/from complete docs
{"input: complete array", []string{"p = true :- q[1] = 2", "q = [1,2,3,4] :- true"}, "true"},
{"input: complete object", []string{`p = true :- q["b"] = 2`, `q = {"a": 1, "b": 2} :- true`}, "true"},
{"input: complete array dereference ground", []string{"p = true :- q[1][1] = 3", "q = [[0,1], [2,3]] :- true"}, "true"},
{"input: complete object dereference ground", []string{`p = true :- q["b"][1] = 4`, `q = {"a": [1, 2], "b": [3, 4]} :- true`}, "true"},
{"input: complete array ground index", []string{"p[y] :- a=[1,2], a[i]=x, q[x]=y", "q = [1,2,3,4] :- true"}, "[2,3]"},
{"input: complete object ground key", []string{`p[y] :- a=["b","c"], a[i]=x, q[x]=y`, `q = {"a":1,"b":2,"c":3,"d":4} :- true`}, "[2,3]"},
{"output: complete array", []string{"p[x] :- q[i] = e, x = [i,e]", "q = [1,2,3,4] :- true"}, "[[0,1],[1,2],[2,3],[3,4]]"},
{"output: complete object", []string{"p[x] :- q[i] = e, x = [i,e]", `q = {"a": 1, "b": 2} :- true`}, `[["a", 1], ["b", 2]]`},
{"output: complete array dereference non-ground", []string{"p[r] :- q[i][j] = 2, r = [i, j]", "q = [[1,2], [3,2]] :- true"}, "[[0, 1], [1, 1]]"},
Expand Down Expand Up @@ -426,12 +452,14 @@ func TestTopDownVarReferences(t *testing.T) {
expected interface{}
}{
// TODO(tsandall) dereferenced variables must be bound beforehand (safety check)
{"var ground", []string{"p[x] :- v = [[1,2],[2,3],[3,4]], x = v[2][1]"}, "[4]"},
{"var non-ground", []string{"p[x] :- v = [[1,2],[2,3],[3,4]], x = v[i][j]"}, "[1,2,2,3,3,4]"},
{"var mixed", []string{`p[x] = y :- v = [{"a": 1, "b": 2}, {"c": 3, "z": [4]}], y = v[i][x][j]`}, `{"z": 4}`},
{"ground", []string{"p[x] :- v = [[1,2],[2,3],[3,4]], x = v[2][1]"}, "[4]"},
{"non-ground", []string{"p[x] :- v = [[1,2],[2,3],[3,4]], x = v[i][j]"}, "[1,2,2,3,3,4]"},
{"mixed", []string{`p[x] = y :- v = [{"a": 1, "b": 2}, {"c": 3, "z": [4]}], y = v[i][x][j]`}, `{"z": 4}`},
{"ref binding", []string{"p[x] :- v = c[i][j], x = v[k], x = true"}, "[true, true]"},
{"embedded", []string{`p[x] :- v = [1,2,3], x = [{"a": v[i]}]`}, `[[{"a": 1}], [{"a": 2}], [{"a": 3}]]`},
{"embedded ref binding", []string{"p[x] :- v = c[i][j], w = [v[0], v[1]], x = w[y]"}, "[null, false, true, 3.14159]"},
{"array: ground var", []string{"p[y] :- a = [1,2,3,4], b = [1,2,999], b[i] = x, a[x] = y"}, "[2,3]"},
{"object: ground var", []string{`p[y] :- a = {"a": 1, "b": 2, "c": 3}, b = ["a", "c", "deadbeef"], b[i] = x, a[x] = y`}, "[1, 3]"},
}

data := loadSmallTestData()
Expand Down
2 changes: 1 addition & 1 deletion opalog/term.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -413,7 +413,7 @@ func (arr Array) queryRec(ref Ref, keys map[Var]Value, iter QueryIterator) error
return nil
case Number:
idx := int(head)
if len(arr) < idx {
if len(arr) <= idx {
return fmt.Errorf("unexpected index in %v: out of bounds: %v", ref, idx)
}
tail := ref[1:]
Expand Down
2 changes: 1 addition & 1 deletion opalog/term_test.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -39,7 +39,7 @@ func TestQuery(t *testing.T) {
{"vars", `a[i][j][k]`, []string{`[[4], "d"]`, `[{i:0, j:1, k:"b"}, {i:0, j:2, k:"c"}]`}},
{"vars/mixed", `a[0][j][k]`, []string{`[[4], "d"]`, `[{j:1, k:"b"}, {j:2, k:"c"}]`}},
{"array bad index type", `a["0"]`, fmt.Errorf(`unexpected non-numeric index in ["0"]: "0" (opalog.String)`)},
{"array bad index value", "a[19999]", fmt.Errorf(`unexpected index in [19999]: out of bounds: 19999`)},
{"array bad index value", "a[1]", fmt.Errorf(`unexpected index in [1]: out of bounds: 1`)},
{"array bad element type", "a[0][0][1]", fmt.Errorf(`unexpected non-composite at [0][1]: true`)},
{"object bad key", `e["hello"]`, fmt.Errorf(`missing key "hello": ["hello"]`)},
{"object bad value type", "e[100][1]", fmt.Errorf(`unexpected non-composite at [100][1]: "true"`)},
Expand Down
46 changes: 26 additions & 20 deletions runtime/repl.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -302,28 +302,10 @@ func (r *Repl) printHeader(table *termtables.Table, body opalog.Body) {
switch ts := expr.Terms.(type) {
case []*opalog.Term:
for _, t := range ts[1:] {
switch v := t.Value.(type) {
case opalog.Ref:
for _, t := range v[1:] {
if !t.IsGround() {
fields[t.String()] = struct{}{}
}
}
case opalog.Var:
fields[v.String()] = struct{}{}
}
buildHeader(fields, t)
}
case *opalog.Term:
switch tv := ts.Value.(type) {
case opalog.Ref:
for _, t := range tv[1:] {
if !t.IsGround() {
fields[t.String()] = struct{}{}
}
}
case opalog.Var:
fields[tv.String()] = struct{}{}
}
buildHeader(fields, ts)
}
}

Expand All @@ -332,7 +314,9 @@ func (r *Repl) printHeader(table *termtables.Table, body opalog.Body) {
for k := range fields {
keys = append(keys, k)
}

sort.Strings(keys)

s := []interface{}{}
for _, k := range keys {
s = append(s, k)
Expand Down Expand Up @@ -399,3 +383,25 @@ func (r *Repl) saveHistory(prompt *liner.State) {
f.Close()
}
}

func buildHeader(fields map[string]struct{}, term *opalog.Term) {
switch v := term.Value.(type) {
case opalog.Ref:
for _, t := range v[1:] {
buildHeader(fields, t)
}
case opalog.Var:
fields[string(v)] = struct{}{}

case opalog.Object:
for _, i := range v {
buildHeader(fields, i[0])
buildHeader(fields, i[1])
}

case opalog.Array:
for _, e := range v {
buildHeader(fields, e)
}
}
}
Loading

0 comments on commit ffe9e58

Please sign in to comment.