Allow rules that don't start with a positive lit.

Introduce a singleton relation that contains exactly one value in `ddlog_std.dl`.

```
relation Singleton()
Singleton().
```

use this relation to enable rules that do not start with a positively
relation by injecting a singleton literal in the body of such rules,
e..g.:
`R() :- not R2(...).` --> `R() :- Singleton(), not R2(...)`
`R() :- var x = 5.` --> `R() :- Singleton(), var x = 5.`

Addresses #770, #97, and #938.

CHANGELOG.md

@@ -9,6 +9,14 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 
 - Experimental compiler support for D3log (wip).
 
+### New features
+
+- We now support rules that don't start with a positive literal, e.g.,
+  ```
+  R() :- not R2(...).
+  R() :- var x = 5.
+  ```
+
 ## [0.38.0] - Mar 11, 2021
 
 ### API changes

java/test_flatbuf1/fb.dump.expected

@@ -69,7 +69,7 @@ From 64 Insert 100
 From 65 Insert 100
 From 66 Insert ZJ{5.0}
 From 67 Insert ZK{5.0}
-From 103 Insert module::ZI16{"zi16"}
-From 104 Insert "zi17"
-From 105 Insert module::ZI18{(4294967295, "ZZZ")}
-From 106 Insert (4294967293, "zi19")
+From 104 Insert module::ZI16{"zi16"}
+From 105 Insert "zi17"
+From 106 Insert module::ZI18{(4294967295, "ZZZ")}
+From 107 Insert (4294967293, "zi19")

lib/ddlog_std.dl

@@ -868,3 +868,6 @@ typedef DDlogGroup<'K, 'V> = DDlogGroup {
 
 /* Unique ID of a node or a sink in a distributed DDlog system. */
 typedef D3logLocationId = u128
+
+relation Singleton()
+Singleton().

src/Language/DifferentialDatalog/Validate.hs

@@ -51,6 +51,9 @@ import Language.DifferentialDatalog.Attribute
 import Language.DifferentialDatalog.Error
 import Language.DifferentialDatalog.Config
 
+sINGLETON_RELATION :: String
+sINGLETON_RELATION = "ddlog_std::Singleton"
+
 -- | Validate Datalog program
 validate :: (MonadError String me, ?cfg::Config) => DatalogProgram -> me DatalogProgram
 validate d = do
@@ -303,15 +306,21 @@ indexValidate d idx = do
     return idx'
 
 ruleValidate :: (MonadError String me, ?cfg::Config) => DatalogProgram -> Rule -> me Rule
-ruleValidate d rl@Rule{..} = do
-    when (not $ null ruleRHS) $ do
-        case head ruleRHS of
-             RHSLiteral True _ -> return ()
-             _                 -> err d (pos rl) "Rule must start with a positive literal"
-    mapIdxM_ (ruleRHSValidate d rl) ruleRHS
-    mapM_ (ruleLHSValidate d rl) ruleLHS
+ruleValidate d rl = do
+    -- Make sure that all rules start with a positive literal by injecting a
+    -- singleton literal in the RHS of rules that don't start with a positive
+    -- literal.
+    let singleton_literal = RHSLiteral True
+                            $ Atom nopos sINGLETON_RELATION delayZero False (E $ EStruct nopos sINGLETON_RELATION [])
+    let rl' = if (not $ null $ ruleRHS rl)
+              then case head $ ruleRHS rl of
+                        RHSLiteral True _ -> rl
+                        _                 -> rl {ruleRHS = singleton_literal:(ruleRHS rl)}
+              else rl
+    mapIdxM_ (ruleRHSValidate d rl') $ ruleRHS rl'
+    mapM_ (ruleLHSValidate d rl') $ ruleLHS rl'
     -- It is now safe to perform type inference
-    ruleValidateExpressions d rl
+    ruleValidateExpressions d rl'
 
 -- We must perform type inference on all parts of the rule at the same time.
 ruleValidateExpressions :: (MonadError String me) => DatalogProgram -> Rule -> me Rule

test/datalog_tests/simple2.dat

@@ -109,3 +109,9 @@ insert GroupThis(2, "2"),
 insert GroupThis(222, "2"),
 
 commit dump_changes;
+
+start;
+
+insert DataForSingletonTest(100),
+
+commit dump_changes;

test/datalog_tests/simple2.dl

@@ -597,3 +597,14 @@ FlatMapTests(6, "${f2} ${s2}") :-
     FMapMaps(),
     ForStruct1{var set, var f2} = FlatMap(testVec()),
     ForStruct2{.f2 = ForStruct1{_, var s2}} = FlatMap(set).
+
+/*
+ * Rules that don't start with a positive literal.
+ */
+
+input relation DataForSingletonTest(x: usize)
+
+output relation SingletonTest(s: string)
+
+SingletonTest("DataForSingletonTest is empty") :- not DataForSingletonTest().
+SingletonTest("${v}") :- var v = 5.

test/datalog_tests/simple2.dump.expected

@@ -125,6 +125,9 @@ Rque{.x = 65596}: +1
 Rque{.x = 65597}: +1
 Rque{.x = 65598}: +1
 Rque{.x = 65599}: +1
+SingletonTest:
+SingletonTest{.s = "5"}: +1
+SingletonTest{.s = "DataForSingletonTest is empty"}: +1
 StringMaps:
 StringMaps{.m = [("bar", (2, false)), ("foo", (1, true)), ("foobar", (3, false))]}: +1
 Strings:
@@ -199,3 +202,5 @@ FlatGroup{.x = 2}: +1
 FlatGroup{.x = 11}: +1
 FlatGroup{.x = 111}: +1
 FlatGroup{.x = 222}: +1
+SingletonTest:
+SingletonTest{.s = "DataForSingletonTest is empty"}: -1

test/datalog_tests/three.dump.expected

@@ -1,6 +1,11 @@
+ddlog_std::Singleton:
+ddlog_std::Singleton{}: +1
 M:
 M{.x = 10}
 
 O:
 O{.x = 10}
 
+ddlog_std::Singleton:
+ddlog_std::Singleton{}
+