CN: Exit program early if well-formedness fails

Now the executable spec runs conditionally on a well-formed
specification (except loop invariants and CN statements).

backend/cn/main.ml

@@ -125,7 +125,12 @@ let check_input_file filename =
     if not (ext ".c" || ext ".h") then
       CF.Pp_errors.fatal ("file \""^filename^"\" has wrong file extension")
 
-
+let maybe_executable_check ~with_ownership_checking ~filename ?output_filename ?output_dir ail_prog mu_file statement_locs =
+  Option.iter (fun output_filename ->
+      Cerb_colour.without_colour (fun () ->
+          Executable_spec.main ~with_ownership_checking filename ail_prog output_dir output_filename mu_file statement_locs)
+        ())
+    output_filename
 
 let main
       filename
@@ -193,27 +198,30 @@ let main
      | (_, Some times) -> Some (times, "log")
      | _ -> None);
   try
+    let handle_error e =
+      if json then TypeErrors.report_json ?state_file e
+      else TypeErrors.report ?state_file e;
+      match e.msg with
+      | TypeErrors.Unsupported _ -> exit 2
+      | _ -> exit 1 in
     let result =
       let open Resultat in
       let@ prog5 = Core_to_mucore.normalise_file ~inherit_loc:(not(no_inherit_loc)) (markers_env, snd ail_prog) prog4 in
       print_log_file ("mucore", MUCORE prog5);
       let paused = Typing.run_to_pause Context.empty (Check.check_decls_lemmata_fun_specs prog5) in
-      Option.iter (fun output_filename ->
-          Cerb_colour.without_colour (fun () ->
-              Executable_spec.main ~with_ownership_checking filename ail_prog output_decorated_dir output_filename prog5 statement_locs)
-            ())
-        output_decorated ;
-    Typing.run_from_pause (fun paused -> Check.check paused lemmata) paused
+      Result.iter_error handle_error (Typing.pause_to_result paused);
+      maybe_executable_check
+        ~with_ownership_checking
+        ~filename
+        ?output_filename:output_decorated
+        ?output_dir:output_decorated_dir
+        ail_prog
+        prog5
+        statement_locs;
+      Typing.run_from_pause (fun paused -> Check.check paused lemmata) paused
     in
     Pp.maybe_close_times_channel ();
-    match result with
-    | Ok () -> exit 0
-    | Error e ->
-      if json then TypeErrors.report_json ?state_file e
-      else TypeErrors.report ?state_file e;
-      match e.msg with
-      | TypeErrors.Unsupported _ -> exit 2
-      | _ -> exit 1
+    Result.fold ~ok:(fun () -> exit 0) ~error:handle_error result
   with
   | exc ->
       Pp.maybe_close_times_channel ();
@@ -321,13 +329,13 @@ let skip =
 
 
 let output_decorated_dir =
-  let doc = "output a version of the translation unit decorated with C runtime translations of the CN annotations to the provided directory" in
+  let doc = "output a version of the translation unit decorated with C runtime
+  translations of the CN annotations to the provided directory" in
   Arg.(value & opt (some string) None & info ["output_decorated_dir"] ~docv:"FILE" ~doc)
 
 let output_decorated =
   let doc = "output a version of the translation unit decorated with C runtime
-  translations of the CN annotations. Warning: this does not check whether
-  specifications are well-formed." in
+  translations of the CN annotations." in
   Arg.(value & opt (some string) None & info ["output_decorated"] ~docv:"FILE" ~doc)
 
 let with_ownership_checking =
@@ -347,7 +355,8 @@ let use_vip =
   Arg.(value & flag & info["vip"] ~doc)
 
 let no_use_ity =
-  let doc = "(this switch should go away) in WellTyped.BaseTyping, do not use integer type annotations placed by the Core elaboration" in
+  let doc = "(this switch should go away) in WellTyped.BaseTyping, do not use
+  integer type annotations placed by the Core elaboration" in
   Arg.(value & flag & info["no-use-ity"] ~doc)
 
 let use_peval =

backend/cn/typing.ml

@@ -84,6 +84,8 @@ let run_from_pause (f : 'a -> 'b t) (pause: 'a pause) =
   | Ok (a, s) -> Result.map fst @@ f a s
   | Error e -> Error e
 
+let pause_to_result (pause : 'a pause) : 'a Resultat.t =
+  Result.map fst pause
 
 let pure (m : ('a) t) : ('a) t =
   fun s ->

backend/cn/typing.mli

@@ -17,6 +17,7 @@ val fail : failure -> 'a m
 val run : Context.t -> 'a m -> ('a, TypeErrors.t) Result.t
 val run_to_pause : Context.t -> 'a m -> 'a pause
 val run_from_pause : ('a -> 'b m) -> 'a pause -> ('b, TypeErrors.t) Result.t
+val pause_to_result : 'a pause -> ('a, TypeErrors.t) Result.t
 val sandbox : 'a t -> ('a Resultat.t) t
 
 val get_typing_context: unit -> Context.t m