Pull out common util functions

Author: wimmers

ML/Muntac.sml

@@ -1,22 +1,15 @@
 open Model_Checker;
-
-(*** Printing utilites ***)
-fun println s = print (s ^ "\n")
-
-fun list_to_string f = (fn x => "[" ^ x ^ "]") o String.concatWith ", " o map f;
-
-fun print_result NONE = println("Invalid input\n")
-    | print_result (SOME true) = println("Property is satisfied\n")
-    | print_result (SOME false) = println("Property is not satisfied\n")
+open Util;
 
 fun print_timings () =
   let
     val tab = Timing.get_timings ();
     fun print_time (s, t) = println(s ^ ": " ^ Time.toString t);
-  in map print_time tab; () end;
+  in map print_time tab; () end
 
 (*** Wrapping up the checker ***)
-fun run_and_print implementation num_threads check_deadlock s =
+fun 
+ implementation num_threads check_deadlock s =
   let
     val debug_level: Int32.int Unsynchronized.ref = ref 0
     val _ = debug_level := 2
@@ -44,16 +37,6 @@ fun run_and_print implementation num_threads check_deadlock s =
   *)
   end;
 
-fun read_lines stream =
-  let
-    val input = TextIO.inputLine stream
-      handle Size => (println "Input line too long!"; raise Size)
-  in
-    case input of
-      NONE => ""
-    | SOME input => input ^ read_lines stream
-  end;
-
 fun check_and_verify_from_stream implementation num_threads model check_deadlock =
   let
     val stream = TextIO.openIn model
@@ -63,20 +46,10 @@ fun check_and_verify_from_stream implementation num_threads model check_deadlock
     if input = ""
     then println "Failed to read line from input!"
       (* We append a space to terminate the input for the parser *)
-    else input ^ " " |> run_and_print implementation num_threads check_deadlock
+    else input ^ " " |> 
+     implementation num_threads check_deadlock
   end;
 
-fun find_with_arg P [] = NONE
-  | find_with_arg P [_] = NONE
-  | find_with_arg P (x :: y :: xs) = if P x then SOME y else find_with_arg P (y :: xs)
-
-fun read_file f =
-  let
-    val file = TextIO.openIn f
-    val s = read_lines file
-    val _ = TextIO.closeIn file
-  in s end;
-
 (* For IntInf as the default int type *)
 (* val to_large_int = IntInf.fromInt; *)
 (* For Int as the default int type *)

ML/Muntax.sml

@@ -1,13 +1,5 @@
 open Model_Checker;
-
-(*** Printing utilites ***)
-fun println s = print (s ^ "\n")
-
-fun list_to_string f = (fn x => "[" ^ x ^ "]") o String.concatWith ", " o map f;
-
-fun print_result NONE = println("Invalid input\n")
-    | print_result (SOME true) = println("Property is satisfied\n")
-    | print_result (SOME false) = println("Property is not satisfied\n")
+open Util;
 
 (*** Wrapping up the checker ***)
 fun run_and_print check_deadlock s =
@@ -34,16 +26,6 @@ fun run_and_print check_deadlock s =
       in println r end
   end;
 
-fun read_lines stream =
-  let
-    val input = TextIO.inputLine stream
-      handle Size => (println "Input line too long!"; raise Size)
-  in
-    case input of
-      NONE => ""
-    | SOME input => input ^ read_lines stream
-  end;
-
 fun check_and_verify_from_stream stream _ =
   let
     val args = CommandLine.arguments()
@@ -56,17 +38,6 @@ fun check_and_verify_from_stream stream _ =
     else input ^ " " |> run_and_print check_deadlock
   end;
 
-fun find_with_arg P [] = NONE
-  | find_with_arg P [_] = NONE
-  | find_with_arg P (x :: y :: xs) = if P x then SOME y else find_with_arg P (y :: xs)
-
-fun read_file f =
-  let
-    val file = TextIO.openIn f
-    val s = read_lines file
-    val _ = TextIO.closeIn file
-  in s end;
-
 val to_large_int = fn x => x;
 
 fun print_usage () =
@@ -101,15 +72,6 @@ fun print_explored () =
     val _ = if length final > 0 then map println final else [()]
   in () end
 
-fun print_json () =
-  let
-    val messages = Logging.get_trace ()
-    val jsons = filter (fn (i, s) => i = 2) messages |> map snd
-    val _ = println ""
-    val _ = println "The following JSON was read by the parser:"
-    val _ = if length jsons > 0 then println (hd jsons) else ()
-  in () end
-
 fun main () =
   let
     val args = CommandLine.arguments()

ML/Util.sml

@@ -0,0 +1,43 @@
+structure Util =
+struct
+
+(*** Printing utilites ***)
+fun println s = print (s ^ "\n")
+
+fun list_to_string f = (fn x => "[" ^ x ^ "]") o String.concatWith ", " o map f
+
+fun print_result NONE = println("Invalid input\n")
+    | print_result (SOME true) = println("Property is satisfied\n")
+    | print_result (SOME false) = println("Property is not satisfied\n")
+
+fun read_lines stream =
+  let
+    val input = TextIO.inputLine stream
+      handle Size => (println "Input line too long!"; raise Size)
+  in
+    case input of
+      NONE => ""
+    | SOME input => input ^ read_lines stream
+  end
+
+fun find_with_arg P [] = NONE
+  | find_with_arg P [_] = NONE
+  | find_with_arg P (x :: y :: xs) = if P x then SOME y else find_with_arg P (y :: xs)
+
+fun read_file f =
+  let
+    val file = TextIO.openIn f
+    val s = read_lines file
+    val _ = TextIO.closeIn file
+  in s end
+
+fun print_json () =
+  let
+    val messages = Logging.get_trace ()
+    val jsons = filter (fn (i, s) => i = 2) messages |> map snd
+    val _ = println ""
+    val _ = println "The following JSON was read by the parser:"
+    val _ = if length jsons > 0 then println (hd jsons) else ()
+  in () end
+
+end

ML/muntac.mlb

@@ -29,5 +29,6 @@ Unsynchronized.sml
 $(MLUNTA_CERT)/prelude.sml
 $(MLUNTA_CERT)/serializable.sml
 $(MLUNTA_CERT)/certificate.sml
+Util.sml
 Muntac.sml
 Mlton_Main.sml

ML/muntax.mlb

@@ -20,5 +20,6 @@ ann "nonexhaustiveMatch ignore" in
     library.ML
 end
 Unsynchronized.sml
+Util.sml
 Muntax.sml
 Mlton_Main.sml