Add verify command.

bin/dune

@@ -46,3 +46,9 @@
   (modules removebottom)
   (libraries birds))
 
+(executable
+  (public_name verify)
+  (name verify)
+  (modules verify)
+  (libraries birds))
+

bin/verify.ml

@@ -0,0 +1,8 @@
+open Birds
+
+let _ =
+  let filename = Sys.argv.(1) in
+  let chan = open_in filename in
+  let lexbuf = Lexing.from_channel chan in
+  let ast = Parser.main Lexer.token lexbuf in
+  Verify.verify true 600 ast

examples/verify_invalid_getput1.dl

@@ -0,0 +1,9 @@
+source tracks2('TRACK':string,'RATING':int,'ALBUM':string,'QUANTITY':int).
+view tracks3('TRACK':string,'RATING':int,'ALBUM':string,'QUANTITY':int).
+% view definition:
+tracks3(T,R,A,Q) :- tracks2(T,R,A,Q),Q > 2.
+% putdelta
++tracks2(T,R,A,Q) :- tracks3(T,R,A,Q), not tracks2(T,R,A,Q).
+-tracks2(T,R,A,Q) :- tracks2(T,R,A,Q), not tracks3(T,R,A,Q).
+% constraints
+_|_ :- tracks3(T,R,A,Q), Q <= 2.

examples/verify_invalid_getput2.dl

@@ -0,0 +1,13 @@
+source a('A':int, 'B':int).
+source b('B':int, 'C':int).
+view s('A':int, 'B':int, 'C':int).
+% view definition
+s(A,B,C) :- a(A,B), b(B,C).
+% putdelta
+-a(A,B) :- a(A,B), not s(A,B,_).
++a(A,B) :- s(A,B,_), not a(A,B).
+-b(B,C) :- b(B,C), s(_,B,_), not s(_,B,C).
++b(B,C) :- s(_,B,C), not b(B,C).
+% constraints
+%_|_ :- a(_,B), not b(B,_).
+_|_ :- s(_,B,C1), s(_,B,C2), C1<>C2.

examples/verify_invalid_putget1.dl

@@ -0,0 +1,9 @@
+source tracks2('TRACK':string,'RATING':int,'ALBUM':string,'QUANTITY':int).
+view tracks3('TRACK':string,'RATING':int,'ALBUM':string,'QUANTITY':int).
+% view definition:
+tracks3(T,R,A,Q) :- tracks2(T,R,A,Q),Q > 2.
+% putdelta
++tracks2(T,R,A,Q) :- tracks3(T,R,A,Q), not tracks2(T,R,A,Q).
+-tracks2(T,R,A,Q) :- tracks2(T,R,A,Q), not tracks3(T,R,A,Q).
+% constraints
+%_|_ :- tracks3(T,R,A,Q), Q <= 2.

examples/verify_invalid_putget2.dl

@@ -0,0 +1,13 @@
+source a('A':int, 'B':int).
+source b('B':int, 'C':int).
+view s('A':int, 'B':int, 'C':int).
+% view definition
+s(A,B,C) :- a(A,B), b(B,C).
+% putdelta
+%-a(A,B) :- a(A,B), not s(A,B,_).
++a(A,B) :- s(A,B,_), not a(A,B).
+-b(B,C) :- b(B,C), s(_,B,_), not s(_,B,C).
++b(B,C) :- s(_,B,C), not b(B,C).
+% constraints
+_|_ :- a(_,B), not b(B,_).
+_|_ :- s(_,B,C1), s(_,B,C2), C1<>C2.

examples/verify_valid1.dl

@@ -0,0 +1,9 @@
+source tracks2('TRACK':string,'RATING':int,'ALBUM':string,'QUANTITY':int).
+view tracks3('TRACK':string,'RATING':int,'ALBUM':string,'QUANTITY':int).
+% view definition:
+tracks3(T,R,A,Q) :- tracks2(T,R,A,Q),Q > 2.
+% putdelta
++tracks2(T,R,A,Q) :- tracks3(T,R,A,Q), not tracks2(T,R,A,Q).
+-tracks2(T,R,A,Q) :- tracks2(T,R,A,Q), not tracks3(T,R,A,Q), Q > 2.
+% constraints
+_|_ :- tracks3(T,R,A,Q), Q <= 2.

examples/verify_valid2.dl

@@ -0,0 +1,13 @@
+source a('A':int, 'B':int).
+source b('B':int, 'C':int).
+view s('A':int, 'B':int, 'C':int).
+% view definition
+s(A,B,C) :- a(A,B), b(B,C).
+% putdelta
+-a(A,B) :- a(A,B), not s(A,B,_).
++a(A,B) :- s(A,B,_), not a(A,B).
+-b(B,C) :- b(B,C), s(_,B,_), not s(_,B,C).
++b(B,C) :- s(_,B,C), not b(B,C).
+% constraints
+_|_ :- a(_,B), not b(B,_).
+_|_ :- s(_,B,C1), s(_,B,C2), C1<>C2.