From d2a7a767087b35980d4b239ce2adfd106f8dc577 Mon Sep 17 00:00:00 2001
From: cedretaber <cedretaber@gmail.com>
Date: Fri, 22 Nov 2024 01:24:54 +0900
Subject: [PATCH] Use Arg module to parse args.

---
 bin/verify.ml           | 32 ++++++++++----------------------
 examples/verify_comp.dl | 24 ++++++++++++++++++++++++
 2 files changed, 34 insertions(+), 22 deletions(-)
 create mode 100644 examples/verify_comp.dl

diff --git a/bin/verify.ml b/bin/verify.ml
index 5654abc..dc83de5 100644
--- a/bin/verify.ml
+++ b/bin/verify.ml
@@ -1,28 +1,16 @@
 open Birds
 
-type args = {
-  filename: string;
-  timeout: int;
-}
-
-let default_timeout = 180
-let default_args = {
-  filename = "";
-  timeout = default_timeout;
-}
-
-let rec parse_argv args = function
-  | [] -> args
-  | "--timeout" :: timeout :: tail ->
-    begin match int_of_string_opt timeout with
-    | Some timeout -> parse_argv { args with timeout } tail
-    | None -> failwith @@ Printf.sprintf "Invalid timeout: %s" timeout
-    end
-  | filename :: tail -> parse_argv { args with filename } tail
+let usage_message = "Usage: verify [--timeout <timeout>] <filename>"
+let filename = ref ""
+let timeout = ref 180
+let parse_rest filename' = filename := filename'
+let speclist = [
+  ("--timeout", Arg.Set_int timeout, "Set the timeout in seconds");
+]
 
 let _ =
-  let args = parse_argv default_args @@ List.tl @@ Array.to_list Sys.argv in
-  let chan = open_in args.filename in
+  Arg.parse speclist parse_rest usage_message;
+  let chan = open_in !filename in
   let lexbuf = Lexing.from_channel chan in
   let ast = Parser.main Lexer.token lexbuf in
-  Verify.verify true args.timeout ast
+  Verify.verify true !timeout ast
diff --git a/examples/verify_comp.dl b/examples/verify_comp.dl
new file mode 100644
index 0000000..2d6ef62
--- /dev/null
+++ b/examples/verify_comp.dl
@@ -0,0 +1,24 @@
+source classes('CLASS_ID':int, 'CLASS_NAME':string, 'FACULTY_ID':int).
+source faculty('FACULTY_ID':int, 'FACULTY_NAME':string, 'OFFICE':string).
+view v('CLASS_ID':int, 'CLASS_NAME':string, 'FACULTY_NAME':string).
+v(C,CN,FN) :- classes(C,CN,F), faculty(F,FN,O).
+all_classes(C,CN,F,FN,O) :- classes(C,CN,F), faculty(F,FN,O).
+mac(C,CN,F,FN,O) :- all_classes(C,CN,F,FN,O), not v(C,CN,FN).
+pac(C,CN,F,FN,O) :- v(C,CN,FN), not all_classes(C,CN,_,FN,_), not mac(_,_,_,_,_), faculty(F,FN,O).
+pac(C,CN,F,FN,O) :- v(C,CN,FN), not all_classes(C,CN,_,FN,_), not mac(_,_,_,_,_), not faculty(_,FN,_), F=-100, O='New'.
+pac(C,CN,F,FN,O) :- v(C,CN,FN), not all_classes(C,CN,_,FN,_), mac(_,_,F,_,O).
+uac(C,CN,F,FN,O) :- pac(C,CN,F,FN,O).
+uac(C,CN,F,FN,O) :- all_classes(C,CN,F,FN,O), not mac(C,CN,F,FN,O).
+% foreign key on base tables
+_|_ :- classes(_,_,F), not faculty(F,_,_).
+% constraints on views
+_|_ :- uac(_,_,F,FN1,_), uac(_,_,F,FN2,_), FN1<>FN2.
+_|_ :- uac(_,_,F,_,O1), uac(_,_,F,_,O2), O1<>O2.
+% faculty_name -> faculty_id on faculty
+_|_ :- faculty(F1, FN, _), faculty(F2, FN, _), F1<>F2.
+-classes(C,CN,F) :- classes(C,CN,F), not uac(C,CN,F,_,_).
++classes(C,CN,F) :- uac(C,CN,F,_,_), not classes(C,CN,F).
+-faculty(F,FN,O) :- faculty(F,FN,O), uac(_,_,F,_,_), not uac(_,_,F,FN,O).
+% The following rule is for strategy 2
+-faculty(F,FN,O) :- faculty(F,FN,O), uac(_,_,_,FN,_), not uac(_,_,F,FN,_).
++faculty(F,FN,O) :- uac(_,_,F,FN,O), not faculty(F,FN,O).