exit properly

driver/Main.ml

@@ -4,12 +4,20 @@ open Parser
 open MenhirLibParser.Inter
 open Entrypoint
 
+let get_exit_code result : int =
+  match result with
+  | AllGood _ -> 0
+  | TypeCheckingFailure _ -> 1
+  | ElaborationFailure _ -> 2
+  | ParserFailure _ -> 3
+  | ParserTimeout _ -> 4
+
 let main_of_lexbuf lexbuf =
   Lexer.lexbuf_to_token_buffer lexbuf
   (* Here, the integer argument is a *log* version of fuel.
      Thus, 500 means 2^500. *)
   |> Entrypoint.main 500
-  |> Format.printf "%a@." PrettyPrinter.format_main_result
+  |> fun r -> Format.printf "%a@." PrettyPrinter.format_main_result r; get_exit_code r
 
 let main_of_filename filename =
   Lexing.from_channel (open_in filename) |> main_of_lexbuf

driver/Main.mli

@@ -1,2 +1,2 @@
-val main_of_filename : string -> unit
-val main_of_program_string : string -> unit
+val main_of_filename : string -> int
+val main_of_program_string : string -> int

driver/Mcltt.ml

@@ -5,7 +5,8 @@ let () =
   then begin
     Printf.fprintf stderr
       "Missing <input-file> argument.\nUsage: %s <input-file>\n" Sys.argv.(0);
-    exit 1
+    exit 5
   end;
   let filename = Sys.argv.(1) in
-  main_of_filename filename
+  let code = main_of_filename filename in
+  exit code

driver/Test.ml

@@ -11,7 +11,7 @@ let main_of_example s = main_of_filename ("../examples/" ^ s)
 (* We never expect parser timeout. 2^500 fuel should be large enough! *)
 
 let%expect_test "Type@0 is of Type@1" =
-  main_of_program_string "Type@0 : Type@1";
+  let _ = main_of_program_string "Type@0 : Type@1" in
   [%expect
     {|
     Parsed:
@@ -23,7 +23,7 @@ let%expect_test "Type@0 is of Type@1" =
   |}]
 
 let%expect_test "zero is of Nat" =
-  main_of_program_string "zero : Nat";
+  let _ = main_of_program_string "zero : Nat" in
   [%expect
     {|
     Parsed:
@@ -35,7 +35,7 @@ let%expect_test "zero is of Nat" =
   |}]
 
 let%expect_test "zero is not of Type@0" =
-  main_of_program_string "zero : Type@0";
+  let _ = main_of_program_string "zero : Type@0" in
   [%expect
     {|
     Type Checking Failure:
@@ -45,7 +45,7 @@ let%expect_test "zero is not of Type@0" =
   |}]
 
 let%expect_test "succ zero is of Nat" =
-  main_of_program_string "succ zero : Nat";
+  let _ = main_of_program_string "succ zero : Nat" in
   [%expect
     {|
     Parsed:
@@ -57,7 +57,7 @@ let%expect_test "succ zero is of Nat" =
   |}]
 
 let%expect_test "succ Type@0 is not of Nat (as it is ill-typed)" =
-  main_of_program_string "succ Type@0 : Nat";
+  let _ = main_of_program_string "succ Type@0 : Nat" in
   [%expect
     {|
     Type Checking Failure:
@@ -67,15 +67,15 @@ let%expect_test "succ Type@0 is not of Nat (as it is ill-typed)" =
   |}]
 
 let%expect_test "variable x is ill-scoped" =
-  main_of_program_string "x : Type@0";
+  let _ = main_of_program_string "x : Type@0" in
   [%expect {|
     Elaboration Failure:
       x
     cannot be elaborated
   |}]
 
 let%expect_test "identity function of Nat is of forall (x : Nat) -> Nat" =
-  main_of_program_string "fun (y : Nat) -> y : forall (x : Nat) -> Nat";
+  let _ = main_of_program_string "fun (y : Nat) -> y : forall (x : Nat) -> Nat" in
   [%expect
     {|
     Parsed:
@@ -88,8 +88,8 @@ let%expect_test "identity function of Nat is of forall (x : Nat) -> Nat" =
 
 let%expect_test "recursion on a natural number that always returns zero is of \
                  Nat" =
-  main_of_program_string
-    "rec 3 return y -> Nat | zero => 0 | succ n, r => 0 end : Nat";
+  let _ = main_of_program_string
+    "rec 3 return y -> Nat | zero => 0 | succ n, r => 0 end : Nat" in
   [%expect
     {|
     Parsed:
@@ -101,7 +101,7 @@ let%expect_test "recursion on a natural number that always returns zero is of \
   |}]
 
 let%expect_test "simple_nat.mcl works" =
-  main_of_example "simple_nat.mcl";
+  let _ = main_of_example "simple_nat.mcl" in
   [%expect
     {|
     Parsed:
@@ -113,7 +113,7 @@ let%expect_test "simple_nat.mcl works" =
   |}]
 
 let%expect_test "simple_rec.mcl works" =
-  main_of_example "simple_rec.mcl";
+  let _ = main_of_example "simple_rec.mcl" in
   [%expect
     {|
     Parsed:
@@ -131,7 +131,7 @@ let%expect_test "simple_rec.mcl works" =
   |}]
 
 let%expect_test "pair.mcl works" =
-  main_of_example "pair.mcl";
+  let _ = main_of_example "pair.mcl" in
   [%expect
     {|
     Parsed:
@@ -257,7 +257,7 @@ let%expect_test "pair.mcl works" =
   |}]
 
 let%expect_test "vector.mcl works" =
-  main_of_example "vector.mcl";
+  let _ = main_of_example "vector.mcl" in
   [%expect
     {|
     Parsed:
@@ -465,7 +465,7 @@ let%expect_test "vector.mcl works" =
   |}]
 
 let%expect_test "nary.mcl works" =
-  main_of_example "nary.mcl";
+  let _ = main_of_example "nary.mcl" in
   [%expect
     {|
     Parsed: