Skip to content

Commit

Permalink
Validate.hs: Disallow variable shadowing in rules.
Browse files Browse the repository at this point in the history
In a rule like this:

```
Bar(x+y) :- Foo(x, y), var y = x.
```

there are two legitimate choices for handling the re-introduction of
variable `y` in the second clause: (1) let the new declaration shadow
the existing one in the rest of then rule, and (2) fail.

The existing implementation did neither of those an generated invalid
Rust code instead.

This commit implements option 2.  Note that we already allow variable
shadowing inside expressions, but this does not seem like a good choice
in a rule scope.  Rules contain implicit variable declarations (e.g.,
variable `x` above), making shadowing extra confusing for users.  We
therefore err on the side of caution and simply disallow such
conflicting declarations.
  • Loading branch information
ryzhyk committed Oct 23, 2020
1 parent e90ca2f commit 0bd5640
Show file tree
Hide file tree
Showing 3 changed files with 37 additions and 2 deletions.
9 changes: 7 additions & 2 deletions src/Language/DifferentialDatalog/Validate.hs
Original file line number Diff line number Diff line change
Expand Up @@ -359,8 +359,13 @@ ruleRHSValidate :: (MonadError String me) => DatalogProgram -> Rule -> RuleRHS -
ruleRHSValidate d rl@Rule{..} (RHSLiteral _ atom) idx =
atomValidate d (CtxRuleRAtom rl idx) atom

ruleRHSValidate _ _ RHSCondition{} _ = return ()
ruleRHSValidate _ _ RHSFlatMap{} _ = return ()
ruleRHSValidate d rl RHSCondition{..} i = do
let ctx = CtxRuleRCond rl i
mapM_ (\v -> checkNoVar (pos v) d ctx (name v))
(exprVarDecls d ctx rhsExpr)
ruleRHSValidate d rl RHSFlatMap{..} i = do
let ctx = CtxRuleRFlatMap rl i
checkNoVar (pos rhsMapExpr) d ctx rhsVar
ruleRHSValidate _ _ RHSInspect{} _ = return ()

ruleRHSValidate d rl RHSGroupBy{} idx = do
Expand Down
8 changes: 8 additions & 0 deletions test/datalog_tests/rules.fail.ast.expected
Original file line number Diff line number Diff line change
Expand Up @@ -77,3 +77,11 @@ in
variable 'x'
var x = FlatMap(v).
^

error: ./test/datalog_tests/rules.fail.dl:10:5-10:11: Variable y already defined in this scope
var y = x.
^^^^^^

error: ./test/datalog_tests/rules.fail.dl:10:21-10:22: Variable y already defined in this scope
var y = FlatMap(y).
^
22 changes: 22 additions & 0 deletions test/datalog_tests/rules.fail.dl
Original file line number Diff line number Diff line change
Expand Up @@ -153,3 +153,25 @@ relation Flat(x: usize)
Flat(x) :-
Vecs(v),
var x = FlatMap(v).

//---

// Variable shadowing in a rule.

input relation Foo(x: usize, y: usize)
output relation Bar(z: usize)

Bar(x+y) :-
Foo(x, y),
var y = x.

//---

// Variable shadowing in a rule.

input relation Foo(x: usize, y: Vec<usize>)
output relation Bar(z: usize)

Bar(x+y) :-
Foo(x, y),
var y = FlatMap(y).

0 comments on commit 0bd5640

Please sign in to comment.