Merge branch 'son/clean' into checked-ops

1 files changed, 75 insertions, 20 deletions

diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 348183c5..9460c5f4 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -41,7 +41,7 @@ let translate_function_to_symbolics (trans_ctx : trans_ctx) (fdef : fun_decl) :
     of backward functions, we also provide names for the outputs.
     TODO: maybe we should introduce a record for this.
 *)
-let translate_function_to_pure (trans_ctx : trans_ctx)
+let translate_function_to_pure_aux (trans_ctx : trans_ctx)
     (pure_type_decls : Pure.type_decl Pure.TypeDeclId.Map.t)
     (fun_dsigs : Pure.decomposed_fun_sig FunDeclId.Map.t) (fdef : fun_decl) :
     pure_fun_translation_no_loops =
@@ -158,6 +158,8 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
       inside_loop = false;
       loop_ids_map;
       loops = Pure.LoopId.Map.empty;
+      mk_return = None;
+      mk_panic = None;
     }
   in
 
@@ -195,6 +197,20 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
   | None -> SymbolicToPure.translate_fun_decl ctx None
   | Some (_, ast) -> SymbolicToPure.translate_fun_decl ctx (Some ast)
 
+let translate_function_to_pure (trans_ctx : trans_ctx)
+    (pure_type_decls : Pure.type_decl Pure.TypeDeclId.Map.t)
+    (fun_dsigs : Pure.decomposed_fun_sig FunDeclId.Map.t) (fdef : fun_decl) :
+    pure_fun_translation_no_loops option =
+  try
+    Some
+      (translate_function_to_pure_aux trans_ctx pure_type_decls fun_dsigs fdef)
+  with CFailure (meta, _) ->
+    let name = name_to_string trans_ctx fdef.name in
+    save_error __FILE__ __LINE__ meta
+      ("Could not translate the function '" ^ name
+     ^ "' because of previous error");
+    None
+
 (* TODO: factor out the return type *)
 let translate_crate_to_pure (crate : crate) :
     trans_ctx
@@ -220,32 +236,54 @@ let translate_crate_to_pure (crate : crate) :
   (* Compute the decomposed fun sigs for the whole crate *)
   let fun_dsigs =
     FunDeclId.Map.of_list
-      (List.map
+      (List.filter_map
          (fun (fdef : LlbcAst.fun_decl) ->
-           ( fdef.def_id,
-             SymbolicToPure.translate_fun_sig_from_decl_to_decomposed trans_ctx
-               fdef ))
+           try
+             Some
+               ( fdef.def_id,
+                 SymbolicToPure.translate_fun_sig_from_decl_to_decomposed
+                   trans_ctx fdef )
+           with CFailure (meta, _) ->
+             let name = name_to_string trans_ctx fdef.name in
+             save_error __FILE__ __LINE__ meta
+               ("Could not translate the function signature of '" ^ name
+              ^ "' because of previous error");
+             None)
          (FunDeclId.Map.values crate.fun_decls))
   in
 
   (* Translate all the *transparent* functions *)
   let pure_translations =
-    List.map
+    List.filter_map
       (translate_function_to_pure trans_ctx type_decls_map fun_dsigs)
       (FunDeclId.Map.values crate.fun_decls)
   in
 
   (* Translate the trait declarations *)
   let trait_decls =
-    List.map
-      (SymbolicToPure.translate_trait_decl trans_ctx)
+    List.filter_map
+      (fun a ->
+        try Some (SymbolicToPure.translate_trait_decl trans_ctx a)
+        with CFailure (meta, _) ->
+          let name = name_to_string trans_ctx a.name in
+          save_error __FILE__ __LINE__ meta
+            ("Could not translate the trait declaration '" ^ name
+           ^ "' because of previous error");
+          None)
       (TraitDeclId.Map.values trans_ctx.trait_decls_ctx.trait_decls)
   in
 
   (* Translate the trait implementations *)
   let trait_impls =
-    List.map
-      (SymbolicToPure.translate_trait_impl trans_ctx)
+    List.filter_map
+      (fun a ->
+        try Some (SymbolicToPure.translate_trait_impl trans_ctx a)
+        with CFailure (meta, _) ->
+          let name = name_to_string trans_ctx a.name in
+          save_error __FILE__ __LINE__ meta
+            ("Could not translate the trait instance '" ^ name
+           ^ "' because of previous error");
+          None)
       (TraitImplId.Map.values trans_ctx.trait_impls_ctx.trait_impls)
   in
 
@@ -471,7 +509,15 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
        groups are always singletons, so the [extract_global_decl] function
        takes care of generating the delimiters.
     *)
-    let global = SymbolicToPure.translate_global ctx.trans_ctx global in
+    let global =
+      try Some (SymbolicToPure.translate_global ctx.trans_ctx global)
+      with CFailure (meta, _) ->
+        let name = name_to_string ctx.trans_ctx global.name in
+        save_error __FILE__ __LINE__ meta
+          ("Could not translate the global declaration '" ^ name
+         ^ "' because of previous error");
+        None
+    in
     Extract.extract_global_decl ctx fmt global body config.interface
 
 (** Utility.
@@ -726,22 +772,28 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
     | TypeGroup (RecGroup ids) ->
         if config.extract_types then export_types_group true ids
     | FunGroup (NonRecGroup id) -> (
-        (* Lookup *)
-        let pure_fun = FunDeclId.Map.find id ctx.trans_funs in
+        (* Lookup - the translated function may not be in the map if we had
+           to ignore it because of errors *)
+        let pure_fun = FunDeclId.Map.find_opt id ctx.trans_funs in
         (* Special case: we skip trait method *declarations* (we will
            extract their type directly in the records we generate for
            the trait declarations themselves, there is no point in having
            separate type definitions) *)
-        match pure_fun.f.Pure.kind with
-        | TraitItemDecl _ -> ()
-        | _ ->
-            (* Translate *)
-            export_functions_group [ pure_fun ])
+        match pure_fun with
+        | Some pure_fun -> (
+            match pure_fun.f.Pure.kind with
+            | TraitItemDecl _ -> ()
+            | _ ->
+                (* Translate *)
+                export_functions_group [ pure_fun ])
+        | None -> ())
     | FunGroup (RecGroup ids) ->
         (* General case of mutually recursive functions *)
         (* Lookup *)
         let pure_funs =
-          List.map (fun id -> FunDeclId.Map.find id ctx.trans_funs) ids
+          List.filter_map
+            (fun id -> FunDeclId.Map.find_opt id ctx.trans_funs)
+            ids
         in
         (* Translate *)
         export_functions_group pure_funs
@@ -899,7 +951,10 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info)
   | Coq -> Printf.fprintf out "End %s.\n" fi.module_name);
 
   (* Some logging *)
-  log#linfo (lazy ("Generated: " ^ fi.filename));
+  if !Errors.error_list <> [] then
+    log#linfo
+      (lazy ("Generated the partial file (because of errors): " ^ fi.filename))
+  else log#linfo (lazy ("Generated: " ^ fi.filename));
 
   (* Flush and close the file *)
   close_out out