Report more unsupported ail->core translations

Instead of failing with error on the first unsupported Ail
expression, keep a list of them, produce a message for each
one, and fail at the end of the pass.

This could be made optional if it were an issue for other
modes of the Lem output.

frontend/model/debug.lem

@@ -35,6 +35,11 @@ declare ocaml target_rep function print_debug_located = `Cerb_debug.print_debug_
 declare hol   target_rep function print_debug_located =
                                   `util$print_debug_located`
 
+val print_unsupported: string -> unit
+declare ocaml target_rep function print_unsupported = `Cerb_debug.print_unsupported`
+declare hol   target_rep function print_unsupported = `util$output_string`
+
+
 val warn: list domain -> (unit -> string) -> unit
 declare ocaml target_rep function warn = `Cerb_debug.warn`
 declare hol   target_rep function warn = `util$output_string`

frontend/model/translation.lem

@@ -2081,7 +2081,8 @@ end                       )
 
       | A.AilEcond e1 Nothing e3 ->
           (* GNU ?: operator *)
-          error "TODO: elaboration of ?: operator"
+          E.record_error_at loc "TODO: elaboration of ?: operator" >>= fun () ->
+          E.return Caux.mk_skip_e
 
       | A.AilEcond e1 (Just e2) e3 ->
           let apply_implicit_conversions expr =
@@ -2441,7 +2442,8 @@ end
 
       | A.AilEgeneric _ _ ->
           (* NOTE: this is already caught by the frontend *)
-          error ((Loc.stringFromLocation (Loc.locOf a_expr)) ^ ": C11 generics not yet supported")
+          E.record_error_at loc "TODO: elaboration of C11 generics" >>= fun () ->
+          E.return Caux.mk_skip_e
 
       | A.AilEarray _ _ e_opts ->
           let elem_ty = match result_ty with
@@ -2667,13 +2669,17 @@ end
       | A.AilEbuiltin b ->
         match b with
           | A.AilBatomic _ ->
-              error ((Loc.stringFromLocation (Loc.with_cursor loc)) ^ ": atomic builtins must be directly called")
+              E.record_error_at loc "atomic builtins must be directly called" >>= fun () ->
+              E.return Caux.mk_skip_e
           | A.AilBlinux _ ->
-              error ((Loc.stringFromLocation (Loc.with_cursor loc)) ^ ": atomic linux builtins must be directly called")
+              E.record_error_at loc "atomic linux builtins must be directly called" >>= fun () ->
+              E.return Caux.mk_skip_e
           | A.AilBcopy_alloc_id ->
-              error ((Loc.stringFromLocation (Loc.with_cursor loc)) ^ ": copy_alloc_id() must be directly called")
+              E.record_error_at loc "copy_alloc_id() must be directly called" >>= fun () ->
+              E.return Caux.mk_skip_e
           | A.AilBCHERI str ->
-              error ((Loc.stringFromLocation (Loc.with_cursor loc)) ^ ": "^str^"() must be directly called")
+              E.record_error_at loc (str^"() must be directly called") >>= fun () ->
+              E.return Caux.mk_skip_e
               (* NOTE: other builtins might be legally desugared here *)
         end
 
@@ -2734,9 +2740,10 @@ end
 
       | A.AilEva_start _ last_sym ->
           let (variadic_sym, last_arg_sym) =
-            match variadic_env with
+          match variadic_env with
             | (Just var_sym, Just last_sym) -> (var_sym, last_sym)
-            | _ -> error ((Loc.stringFromLocation (Loc.locOf a_expr)) ^ ": va_start not in a variadic function")
+            | _ ->
+              error (Loc.stringFromLocation (Loc.locOf a_expr) ^ ": va_start not in a variadic function")
             end in
           E.wrapped_fresh_symbol (C.BTy_object C.OTy_integer) >>= fun va_wrp ->
           E.return begin
@@ -2887,7 +2894,8 @@ else
           translate_function_designator self stdlib e
 
       | A.AilEgcc_statement ->
-          error ((Loc.stringFromLocation loc) ^ ": GCC statements as expressions not yet supported")
+          E.record_error_at loc "GCC statements as expressions not yet supported" >>= fun () ->
+          E.return Caux.mk_skip_e
     end
 
 
@@ -4008,7 +4016,7 @@ val translate:
 let translate (ailnames, stdlib_fun_map) impl prog =
   let translation_stdlib = mk_translation_stdlib (ailnames, stdlib_fun_map) in
   let ((core_tagDefs, cglobs, (*cdecls, *) cfuns, funinfo), st) =
-    E.runStateM (translate_program translation_stdlib prog) (E.elab_init ())
+    E.runStateM_errors (translate_program translation_stdlib prog) (E.elab_init ())
   in
   <| C.main= fst prog;
      C.tagDefs= core_tagDefs;

frontend/model/translation_effect.lem

@@ -22,6 +22,8 @@ type elab_state = <|
   string_literals: list (Loc.t * Symbol.sym * Ctype.ctype * C.pexpr);
   compound_literals: list compound_literal_info;
   visible_objects_types_markers_env: map nat (list (Symbol.sym * Ctype.ctype));
+
+  errors: list string
 
 |>
 
@@ -34,6 +36,7 @@ let elab_init () = <|
   string_literals= [];
   compound_literals= [];
   visible_objects_types_markers_env = Map.empty;
+  errors = [];
 |>
 
 type wrapped_symbol = <|
@@ -148,3 +151,24 @@ let record_object_types_marker () =
       return ()
   end >>
   return marker_id
+
+
+(* record that an (unrecoverable) error occured, but don't abandon
+   translation yet, so the user gets a full list of such errors *)
+val record_error: string -> elabM unit
+let record_error err =
+    let () = Debug.print_unsupported err in
+    update (fun st -> <| st with errors = err :: st.errors |>)
+
+val record_error_at: Loc.t -> string -> elabM unit
+let record_error_at loc err = record_error
+    ((Loc.stringFromLocation (Loc.with_cursor loc)) ^ ": " ^ err)
+
+val runStateM_errors: forall 'a. elabM 'a -> elab_state -> 'a * elab_state
+let runStateM_errors m st =
+  let (rv, st) = runStateM m st in
+  match List.reverse st.errors with
+    | [] -> (rv, st)
+    | (err1 :: _) -> error err1
+  end
+

util/cerb_debug.ml

@@ -40,6 +40,10 @@ let print_debug level _doms msg =
 let print_debug_located level doms loc msg =
   print_debug level doms (fun () -> "[" ^ Cerb_location.location_to_string loc ^ "] - " ^ msg ())
 
+let print_unsupported str =
+  prerr_string (Cerb_colour.ansi_format ~err:true [Red] "unsupported: ");
+  prerr_endline str
+
 let warn _doms msg =
   if !debug_level > 1 then
     prerr_endline Cerb_colour.(ansi_format [Yellow] ("WARNING: " ^ msg ()))

util/cerb_debug.mli

@@ -22,6 +22,7 @@ val get_debug_level: unit -> int
 val print_success: string -> unit
 val print_debug: int -> domain list -> (unit -> string) -> unit
 val print_debug_located: int -> domain list -> Cerb_location.t -> (unit -> string) -> unit
+val print_unsupported: string -> unit
 val warn: domain list -> (unit -> string) -> unit
 
 (* val print_deubg2: string -> 'a -> 'a *)