From 084480c807b58947b8487eb3a7c6a71bb388a832 Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Wed, 3 Apr 2024 17:01:27 +0200
Subject: added Error and EError to expressions and propagated related changes

---
 compiler/Errors.ml          | 5 +++--
 compiler/Extract.ml         | 8 ++++++++
 compiler/ExtractBase.ml     | 4 +++-
 compiler/ExtractTypes.ml    | 1 +
 compiler/Interpreter.ml     | 3 ++-
 compiler/PrintPure.ml       | 4 ++++
 compiler/Pure.ml            | 8 ++++++++
 compiler/PureMicroPasses.ml | 4 +++-
 compiler/PureTypeCheck.ml   | 1 +
 compiler/PureUtils.ml       | 3 +++
 compiler/SymbolicAst.ml     | 1 +
 compiler/SymbolicToPure.ml  | 4 ++++
 12 files changed, 41 insertions(+), 5 deletions(-)

(limited to 'compiler')

diff --git a/compiler/Errors.ml b/compiler/Errors.ml
index 53e56c44..30887593 100644
--- a/compiler/Errors.ml
+++ b/compiler/Errors.ml
@@ -1,6 +1,7 @@
 let log = Logging.errors_log
 
-let meta_to_string (span : Meta.span) =
+let meta_to_string (meta : Meta.meta) =
+  let span = meta.span in
   let file = match span.file with Virtual s | Local s -> s in
   let loc_to_string (l : Meta.loc) : string =
     string_of_int l.line ^ ":" ^ string_of_int l.col
@@ -10,7 +11,7 @@ let meta_to_string (span : Meta.span) =
 
 let format_error_message (meta : Meta.meta option) (msg : string) =
   let meta =
-    match meta with None -> "" | Some meta -> "\n" ^ meta_to_string meta.span
+    match meta with None -> "" | Some meta -> "\n" ^ meta_to_string meta
   in
   msg ^ meta
 
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 1f9c9117..ef5d5dce 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -297,6 +297,13 @@ let lets_require_wrap_in_do (meta : Meta.meta)
     - application argument: [f (exp)]
     - match/if scrutinee: [if exp then _ else _]/[match exp | _ -> _]
  *)
+
+let extract_errors (fmt : F.formatter) =
+  match !Config.backend with
+  | FStar | Coq -> F.pp_print_string fmt "admit"
+  | Lean -> F.pp_print_string fmt "sorry"
+  | HOL4 -> F.pp_print_string fmt "(* ERROR: could not generate the code *)"
+
 let rec extract_texpression (meta : Meta.meta) (ctx : extraction_ctx)
     (fmt : F.formatter) (inside : bool) (e : texpression) : unit =
   match e.e with
@@ -323,6 +330,7 @@ let rec extract_texpression (meta : Meta.meta) (ctx : extraction_ctx)
   | Loop _ ->
       (* The loop nodes should have been eliminated in {!PureMicroPasses} *)
       craise __FILE__ __LINE__ meta "Unreachable"
+  | EError (_, _) -> extract_errors fmt
 
 (* Extract an application *or* a top-level qualif (function extraction has
  * to handle top-level qualifiers, so it seemed more natural to merge the
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 74ac9e32..faca2bde 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -1700,7 +1700,9 @@ let ctx_compute_var_basename (meta : Meta.meta) (ctx : extraction_ctx)
       | TLiteral lty -> (
           match lty with TBool -> "b" | TChar -> "c" | TInteger _ -> "i")
       | TArrow _ -> "f"
-      | TTraitType (_, name) -> name_from_type_ident name)
+      | TTraitType (_, name) -> name_from_type_ident name
+      | Error -> "@Error")
+(* TODO : Check*)
 
 (** Generates a type variable basename. *)
 let ctx_compute_type_var_basename (_ctx : extraction_ctx) (basename : string) :
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index 1f0abf8a..350866e9 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -566,6 +566,7 @@ let rec extract_ty (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.formatter)
               "Trait types are not supported yet when generating code for HOL4";
             extract_trait_ref meta ctx fmt no_params_tys false trait_ref;
             F.pp_print_string fmt ("." ^ add_brackets type_name))
+  | Error -> craise __FILE__ __LINE__ meta "TODO: Error message?"
 
 and extract_trait_ref (meta : Meta.meta) (ctx : extraction_ctx)
     (fmt : F.formatter) (no_params_tys : TypeDeclId.Set.t) (inside : bool)
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index a65e1663..d0a54750 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -612,7 +612,8 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx)
 
   (* Evaluate the function *)
   let symbolic =
-    eval_function_body config (Option.get fdef.body).body cf_finish ctx
+    try eval_function_body config (Option.get fdef.body).body cf_finish ctx
+    with CFailure (meta, msg) -> Some (Error (meta, msg))
   in
 
   (* Return *)
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml
index d0c243bb..12d554f2 100644
--- a/compiler/PrintPure.ml
+++ b/compiler/PrintPure.ml
@@ -164,6 +164,7 @@ let rec ty_to_string (env : fmt_env) (inside : bool) (ty : ty) : string =
       let trait_ref = trait_ref_to_string env false trait_ref in
       let s = trait_ref ^ "::" ^ type_name in
       if inside then "(" ^ s ^ ")" else s
+  | Error -> "@Error"
 
 and generic_args_to_strings (env : fmt_env) (inside : bool)
     (generics : generic_args) : string list =
@@ -615,6 +616,9 @@ let rec texpression_to_string ?(metadata : Meta.meta option = None)
           let e = meta_s ^ "\n" ^ indent ^ e in
           if inside then "(" ^ e ^ ")" else e
       | MPlace _ -> "(" ^ meta_s ^ " " ^ e ^ ")")
+  | EError (meta, msg) ->
+      if Option.is_none meta then msg
+      else meta_to_string (Option.get meta) ^ " " ^ msg (* TODO formatting *)
 
 and app_to_string ?(meta : Meta.meta option = None) (env : fmt_env)
     (inside : bool) (indent : string) (indent_incr : string) (app : texpression)
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index 7de7e0f4..7366783c 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -285,6 +285,7 @@ type ty =
   | TArrow of ty * ty
   | TTraitType of trait_ref * string
       (** The string is for the name of the associated type *)
+  | Error
 
 and trait_ref = {
   trait_id : trait_instance_id;
@@ -621,6 +622,7 @@ class ['self] iter_expression_base =
     method visit_qualif : 'env -> qualif -> unit = fun _ _ -> ()
     method visit_loop_id : 'env -> loop_id -> unit = fun _ _ -> ()
     method visit_field_id : 'env -> field_id -> unit = fun _ _ -> ()
+    method visit_meta : 'env -> Meta.meta -> unit = fun _ _ -> ()
   end
 
 (** Ancestor for {!map_expression} visitor *)
@@ -632,6 +634,7 @@ class ['self] map_expression_base =
     method visit_qualif : 'env -> qualif -> qualif = fun _ x -> x
     method visit_loop_id : 'env -> loop_id -> loop_id = fun _ x -> x
     method visit_field_id : 'env -> field_id -> field_id = fun _ x -> x
+    method visit_meta : 'env -> Meta.meta -> Meta.meta = fun _ x -> x
   end
 
 (** Ancestor for {!reduce_expression} visitor *)
@@ -643,6 +646,7 @@ class virtual ['self] reduce_expression_base =
     method visit_qualif : 'env -> qualif -> 'a = fun _ _ -> self#zero
     method visit_loop_id : 'env -> loop_id -> 'a = fun _ _ -> self#zero
     method visit_field_id : 'env -> field_id -> 'a = fun _ _ -> self#zero
+    method visit_meta : 'env -> Meta.meta -> 'a = fun _ _ -> self#zero
   end
 
 (** Ancestor for {!mapreduce_expression} visitor *)
@@ -662,6 +666,9 @@ class virtual ['self] mapreduce_expression_base =
 
     method visit_field_id : 'env -> field_id -> field_id * 'a =
       fun _ x -> (x, self#zero)
+
+    method visit_meta : 'env -> Meta.meta -> Meta.meta * 'a =
+      fun _ x -> (x, self#zero)
   end
 
 (** **Rk.:** here, {!expression} is not at all equivalent to the expressions
@@ -726,6 +733,7 @@ type expression =
   | Loop of loop  (** See the comments for {!loop} *)
   | StructUpdate of struct_update  (** See the comments for {!struct_update} *)
   | Meta of (emeta[@opaque]) * texpression  (** Meta-information *)
+  | EError of Meta.meta option * string
 
 and switch_body = If of texpression * texpression | Match of match_branch list
 and match_branch = { pat : typed_pattern; branch : texpression }
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 9fa07029..ebc5c65f 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -416,6 +416,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
       | StructUpdate supd -> update_struct_update supd ctx
       | Lambda (lb, e) -> update_lambda lb e ctx
       | Meta (meta, e) -> update_emeta meta e ctx
+      | EError (meta, msg) -> (ctx, EError (meta, msg))
     in
     (ctx, { e; ty })
   (* *)
@@ -1006,7 +1007,8 @@ let filter_useless (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
         match e with
         | Var _ | CVar _ | Const _ | App _ | Qualif _
         | Meta (_, _)
-        | StructUpdate _ | Lambda _ ->
+        | StructUpdate _ | Lambda _
+        | EError (_, _) ->
             super#visit_expression env e
         | Switch (scrut, switch) -> (
             match switch with
diff --git a/compiler/PureTypeCheck.ml b/compiler/PureTypeCheck.ml
index 53ff8983..098e2564 100644
--- a/compiler/PureTypeCheck.ml
+++ b/compiler/PureTypeCheck.ml
@@ -238,3 +238,4 @@ let rec check_texpression (meta : Meta.meta) (ctx : tc_ctx) (e : texpression) :
   | Meta (_, e_next) ->
       sanity_check __FILE__ __LINE__ (e_next.ty = e.ty) meta;
       check_texpression meta ctx e_next
+  | EError (meta, msg) -> craise_opt_meta __FILE__ __LINE__ meta msg
diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index 4bc90872..87f0b5f7 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -228,6 +228,9 @@ let rec let_group_requires_parentheses (meta : Meta.meta) (e : texpression) :
   | Loop _ ->
       (* Should have been eliminated *)
       craise __FILE__ __LINE__ meta "Unreachable"
+  | EError (meta, msg) ->
+      craise_opt_meta __FILE__ __LINE__ meta
+        msg (* TODO : check if true should'nt be returned instead ? *)
 
 let texpression_requires_parentheses meta e =
   match !Config.backend with
diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml
index e164fd49..f15a2c23 100644
--- a/compiler/SymbolicAst.ml
+++ b/compiler/SymbolicAst.ml
@@ -212,6 +212,7 @@ type expression =
           TODO: merge this with Return.
        *)
   | Meta of emeta * expression  (** Meta information *)
+  | Error of Meta.meta option * string
 
 and loop = {
   loop_id : loop_id;
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 0c30f44c..1701891f 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -1963,6 +1963,9 @@ let eval_ctx_to_symbolic_assignments_info (ctx : bs_ctx)
   (* Return the computed information *)
   !info
 
+let translate_meta (meta : Meta.meta option) (msg : string) : texpression =
+  { e = EError (meta, msg); ty = Error }
+
 let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression =
   match e with
   | S.Return (ectx, opt_v) ->
@@ -1989,6 +1992,7 @@ let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression =
       *)
       translate_forward_end ectx loop_input_values e back_e ctx
   | Loop loop -> translate_loop loop ctx
+  | Error (meta, msg) -> translate_meta meta msg
 
 and translate_panic (ctx : bs_ctx) : texpression =
   (* Here we use the function return type - note that it is ok because
-- 
cgit v1.2.3


From a2a219145587deb0ade9fa7d60171765cd722162 Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Wed, 3 Apr 2024 17:36:09 +0200
Subject: added extract_ty_errors and extract_texpression_errors to deal with
 the error case in their respective types

---
 compiler/Extract.ml      | 4 ++--
 compiler/ExtractTypes.ml | 9 ++++++++-
 2 files changed, 10 insertions(+), 3 deletions(-)

(limited to 'compiler')

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index ef5d5dce..af0bf98d 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -298,7 +298,7 @@ let lets_require_wrap_in_do (meta : Meta.meta)
     - match/if scrutinee: [if exp then _ else _]/[match exp | _ -> _]
  *)
 
-let extract_errors (fmt : F.formatter) =
+let extract_texpression_errors (fmt : F.formatter) =
   match !Config.backend with
   | FStar | Coq -> F.pp_print_string fmt "admit"
   | Lean -> F.pp_print_string fmt "sorry"
@@ -330,7 +330,7 @@ let rec extract_texpression (meta : Meta.meta) (ctx : extraction_ctx)
   | Loop _ ->
       (* The loop nodes should have been eliminated in {!PureMicroPasses} *)
       craise __FILE__ __LINE__ meta "Unreachable"
-  | EError (_, _) -> extract_errors fmt
+  | EError (_, _) -> extract_texpression_errors fmt
 
 (* Extract an application *or* a top-level qualif (function extraction has
  * to handle top-level qualifiers, so it seemed more natural to merge the
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index 350866e9..1c3657a3 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -433,6 +433,13 @@ let extract_literal_type (_ctx : extraction_ctx) (fmt : F.formatter)
       End
     ]}
  *)
+
+let extract_ty_errors (fmt : F.formatter) : unit =
+  match !Config.backend with
+  | FStar | Coq -> F.pp_print_string fmt "admit"
+  | Lean -> F.pp_print_string fmt "sorry"
+  | HOL4 -> F.pp_print_string fmt "(* ERROR: could not generate the code *)"
+
 let rec extract_ty (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.formatter)
     (no_params_tys : TypeDeclId.Set.t) (inside : bool) (ty : ty) : unit =
   let extract_rec = extract_ty meta ctx fmt no_params_tys in
@@ -566,7 +573,7 @@ let rec extract_ty (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.formatter)
               "Trait types are not supported yet when generating code for HOL4";
             extract_trait_ref meta ctx fmt no_params_tys false trait_ref;
             F.pp_print_string fmt ("." ^ add_brackets type_name))
-  | Error -> craise __FILE__ __LINE__ meta "TODO: Error message?"
+  | Error -> extract_ty_errors fmt
 
 and extract_trait_ref (meta : Meta.meta) (ctx : extraction_ctx)
     (fmt : F.formatter) (no_params_tys : TypeDeclId.Set.t) (inside : bool)
-- 
cgit v1.2.3


From e9bbac75812ef556585f14b72239133619cf1748 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 3 Apr 2024 17:49:00 +0200
Subject: Update the initial configuration

---
 compiler/Config.ml | 2 +-
 compiler/Main.ml   | 3 ---
 2 files changed, 1 insertion(+), 4 deletions(-)

(limited to 'compiler')

diff --git a/compiler/Config.ml b/compiler/Config.ml
index 099cdc8b..0b26e2ef 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -368,4 +368,4 @@ let backend_has_tuple_projectors () =
 let use_nested_tuple_projectors = ref false
 
 (** Generate name patterns for the external definitions we encounter *)
-let extract_external_name_patterns = ref false
+let extract_external_name_patterns = ref true
diff --git a/compiler/Main.ml b/compiler/Main.ml
index 64d8ae2b..db200f37 100644
--- a/compiler/Main.ml
+++ b/compiler/Main.ml
@@ -120,9 +120,6 @@ let () =
         Arg.Set use_nested_tuple_projectors,
         " Use nested projectors for tuples (e.g., (0, 1).snd.fst instead of \
          (0, 1).1)." );
-      ( "-ext-name-pats",
-        Arg.Set extract_external_name_patterns,
-        " Generate name patterns for the external definitions we find." );
     ]
   in
 
-- 
cgit v1.2.3


From 78cc58e3076ffd61add6d78b64371b6eb36d6ab2 Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Wed, 3 Apr 2024 17:52:10 +0200
Subject: resolved requested changes

---
 compiler/ExtractBase.ml    | 2 +-
 compiler/PrintPure.ml      | 4 +---
 compiler/SymbolicToPure.ml | 4 ++--
 3 files changed, 4 insertions(+), 6 deletions(-)

(limited to 'compiler')

diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index faca2bde..e399a89c 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -1701,7 +1701,7 @@ let ctx_compute_var_basename (meta : Meta.meta) (ctx : extraction_ctx)
           match lty with TBool -> "b" | TChar -> "c" | TInteger _ -> "i")
       | TArrow _ -> "f"
       | TTraitType (_, name) -> name_from_type_ident name
-      | Error -> "@Error")
+      | Error -> "x")
 (* TODO : Check*)
 
 (** Generates a type variable basename. *)
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml
index 12d554f2..97ea6048 100644
--- a/compiler/PrintPure.ml
+++ b/compiler/PrintPure.ml
@@ -616,9 +616,7 @@ let rec texpression_to_string ?(metadata : Meta.meta option = None)
           let e = meta_s ^ "\n" ^ indent ^ e in
           if inside then "(" ^ e ^ ")" else e
       | MPlace _ -> "(" ^ meta_s ^ " " ^ e ^ ")")
-  | EError (meta, msg) ->
-      if Option.is_none meta then msg
-      else meta_to_string (Option.get meta) ^ " " ^ msg (* TODO formatting *)
+  | EError (_, _) -> "@Error"
 
 and app_to_string ?(meta : Meta.meta option = None) (env : fmt_env)
     (inside : bool) (indent : string) (indent_incr : string) (app : texpression)
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 1701891f..53ab1c08 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -1963,7 +1963,7 @@ let eval_ctx_to_symbolic_assignments_info (ctx : bs_ctx)
   (* Return the computed information *)
   !info
 
-let translate_meta (meta : Meta.meta option) (msg : string) : texpression =
+let translate_error (meta : Meta.meta option) (msg : string) : texpression =
   { e = EError (meta, msg); ty = Error }
 
 let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression =
@@ -1992,7 +1992,7 @@ let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression =
       *)
       translate_forward_end ectx loop_input_values e back_e ctx
   | Loop loop -> translate_loop loop ctx
-  | Error (meta, msg) -> translate_meta meta msg
+  | Error (meta, msg) -> translate_error meta msg
 
 and translate_panic (ctx : bs_ctx) : texpression =
   (* Here we use the function return type - note that it is ok because
-- 
cgit v1.2.3


From cc0b77e4b75990916e331e9ff5c26c912341b13d Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Wed, 3 Apr 2024 17:58:10 +0200
Subject: resolved requested changes

---
 compiler/ExtractBase.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'compiler')

diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index e399a89c..ba75f580 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -1702,7 +1702,6 @@ let ctx_compute_var_basename (meta : Meta.meta) (ctx : extraction_ctx)
       | TArrow _ -> "f"
       | TTraitType (_, name) -> name_from_type_ident name
       | Error -> "x")
-(* TODO : Check*)
 
 (** Generates a type variable basename. *)
 let ctx_compute_type_var_basename (_ctx : extraction_ctx) (basename : string) :
-- 
cgit v1.2.3


From a781ea75c1860c76c5577faa57efcdb0db910612 Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Fri, 29 Mar 2024 10:56:52 +0100
Subject: Added meta information to names_map_id field in names_map type

---
 compiler/ExtractBase.ml | 45 +++++++++++++++++++++++----------------------
 1 file changed, 23 insertions(+), 22 deletions(-)

(limited to 'compiler')

diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 74ac9e32..96f816cb 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -237,7 +237,7 @@ module IdSet = Collections.MakeSet (IdOrderedType)
   *)
 type names_map = {
   id_to_name : string IdMap.t;
-  name_to_id : id StringMap.t;
+  name_to_id : (id * Meta.meta option) StringMap.t;
       (** The name to id map is used to look for name clashes, and generate nice
           debugging messages: if there is a name clash, it is useful to know
           precisely which identifiers are mapped to the same name...
@@ -253,8 +253,8 @@ let empty_names_map : names_map =
   }
 
 (** Small helper to report name collision *)
-let report_name_collision (id_to_string : id -> string) (id1 : id) (id2 : id)
-    (name : string) : unit =
+let report_name_collision (id_to_string : id -> string)
+    (id1, meta : id * Meta.meta option) (id2 : id) (name : string) : unit =
   let id1 = "\n- " ^ id_to_string id1 in
   let id2 = "\n- " ^ id_to_string id2 in
   let err =
@@ -263,9 +263,10 @@ let report_name_collision (id_to_string : id -> string) (id1 : id) (id2 : id)
     ^ "\nYou may want to rename some of your definitions, or report an issue."
   in
   (* If we fail hard on errors, raise an exception *)
-  save_error __FILE__ __LINE__ None err
+  save_error __FILE__ __LINE__ meta err
 
-let names_map_get_id_from_name (name : string) (nm : names_map) : id option =
+let names_map_get_id_from_name (name : string) (nm : names_map) :
+    (id * Meta.meta option) option =
   StringMap.find_opt name nm.name_to_id
 
 let names_map_check_collision (id_to_string : id -> string) (id : id)
@@ -277,15 +278,15 @@ let names_map_check_collision (id_to_string : id -> string) (id : id)
       report_name_collision id_to_string clash id name
 
 (** Insert bindings in a names map without checking for collisions *)
-let names_map_add_unchecked (id : id) (name : string) (nm : names_map) :
+let names_map_add_unchecked (id, meta : id * Meta.meta option) (name : string) (nm : names_map) :
     names_map =
   (* Insert *)
   let id_to_name = IdMap.add id name nm.id_to_name in
-  let name_to_id = StringMap.add name id nm.name_to_id in
+  let name_to_id= StringMap.add name (id, meta) nm.name_to_id in
   let names_set = StringSet.add name nm.names_set in
   { id_to_name; name_to_id; names_set }
 
-let names_map_add (id_to_string : id -> string) (id : id) (name : string)
+let names_map_add (id_to_string : id -> string) (id, meta : id * meta option) (name : string)
     (nm : names_map) : names_map =
   (* Check if there is a clash *)
   names_map_check_collision id_to_string id name nm;
@@ -296,9 +297,9 @@ let names_map_add (id_to_string : id -> string) (id : id) (name : string)
        ^ ":\nThe chosen name is already in the names set: " ^ name
      in
      (* If we fail hard on errors, raise an exception *)
-     save_error __FILE__ __LINE__ None err);
+     save_error __FILE__ __LINE__ meta err);
   (* Insert *)
-  names_map_add_unchecked id name nm
+  names_map_add_unchecked (id, meta) name nm
 
 (** The unsafe names map stores mappings from identifiers to names which might
     collide. For some backends and some names, it might be acceptable to have
@@ -384,7 +385,7 @@ let allow_collisions (id : id) : bool =
 
 (** The [id_to_string] function to print nice debugging messages if there are
     collisions *)
-let names_maps_add (id_to_string : id -> string) (id : id) (name : string)
+let names_maps_add (meta : Meta.meta option) (id_to_string : id -> string) (id : id) (name : string)
     (nm : names_maps) : names_maps =
   (* We do not use the same name map if we allow/disallow collisions.
      We notably use it for field names: some backends like Lean can use the
@@ -415,10 +416,10 @@ let names_maps_add (id_to_string : id -> string) (id : id) (name : string)
     *)
     let strict_names_map =
       if strict_collisions id then
-        names_map_add id_to_string id name nm.strict_names_map
+        names_map_add id_to_string (id, meta) name nm.strict_names_map
       else nm.strict_names_map
     in
-    let names_map = names_map_add id_to_string id name nm.names_map in
+    let names_map = names_map_add id_to_string (id, meta) name nm.names_map in
     { nm with strict_names_map; names_map }
 
 (** The [id_to_string] function to print nice debugging messages if there are
@@ -468,20 +469,20 @@ type names_map_init = {
 
 let names_maps_add_assumed_type (id_to_string : id -> string) (id : assumed_ty)
     (name : string) (nm : names_maps) : names_maps =
-  names_maps_add id_to_string (TypeId (TAssumed id)) name nm
+  names_maps_add None id_to_string (TypeId (TAssumed id)) name nm
 
 let names_maps_add_assumed_struct (id_to_string : id -> string)
     (id : assumed_ty) (name : string) (nm : names_maps) : names_maps =
-  names_maps_add id_to_string (StructId (TAssumed id)) name nm
+  names_maps_add None id_to_string (StructId (TAssumed id)) name nm
 
 let names_maps_add_assumed_variant (id_to_string : id -> string)
     (id : assumed_ty) (variant_id : VariantId.id) (name : string)
     (nm : names_maps) : names_maps =
-  names_maps_add id_to_string (VariantId (TAssumed id, variant_id)) name nm
+  names_maps_add None id_to_string (VariantId (TAssumed id, variant_id)) name nm
 
-let names_maps_add_function (id_to_string : id -> string) (fid : fun_id)
+let names_maps_add_function (id_to_string : id -> string) (fid, meta : fun_id * meta option)
     (name : string) (nm : names_maps) : names_maps =
-  names_maps_add id_to_string (FunId fid) name nm
+  names_maps_add meta id_to_string (FunId fid) name nm
 
 let bool_name () = if !backend = Lean then "Bool" else "bool"
 let char_name () = if !backend = Lean then "Char" else "char"
@@ -659,7 +660,7 @@ let id_to_string (meta : Meta.meta option) (id : id) (ctx : extraction_ctx) :
 let ctx_add (meta : Meta.meta) (id : id) (name : string) (ctx : extraction_ctx)
     : extraction_ctx =
   let id_to_string (id : id) : string = id_to_string (Some meta) id ctx in
-  let names_maps = names_maps_add id_to_string id name ctx.names_maps in
+  let names_maps = names_maps_add (Some meta) id_to_string id name ctx.names_maps in
   { ctx with names_maps }
 
 let ctx_get (meta : Meta.meta option) (id : id) (ctx : extraction_ctx) : string
@@ -1125,7 +1126,7 @@ let initialize_names_maps () : names_maps =
         (* There is duplication in the keywords so we don't check the collisions
            while registering them (what is important is that there are no collisions
            between keywords and user-defined identifiers) *)
-        names_map_add_unchecked UnknownId name nm)
+        names_map_add_unchecked (UnknownId, None) name nm)
       strict_names_map keywords
   in
   let nm = { names_map; unsafe_names_map; strict_names_map } in
@@ -1155,9 +1156,9 @@ let initialize_names_maps () : names_maps =
   in
   let assumed_functions =
     List.map
-      (fun (fid, name) -> (FromLlbc (Pure.FunId (FAssumed fid), None), name))
+      (fun (fid, name) -> ((FromLlbc (Pure.FunId (FAssumed fid), None), None), name))
       init.assumed_llbc_functions
-    @ List.map (fun (fid, name) -> (Pure fid, name)) init.assumed_pure_functions
+    @ List.map (fun (fid, name) -> ((Pure fid, None), name)) init.assumed_pure_functions
   in
   let nm =
     List.fold_left
-- 
cgit v1.2.3


From a25f3bc7fe1dcddc952b4dcbb7b732bdf095197e Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Wed, 3 Apr 2024 18:23:46 +0200
Subject: rebased branch

---
 compiler/ExtractBase.ml | 32 +++++++++++++++++++-------------
 1 file changed, 19 insertions(+), 13 deletions(-)

(limited to 'compiler')

diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 96f816cb..34b5ad64 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -254,7 +254,7 @@ let empty_names_map : names_map =
 
 (** Small helper to report name collision *)
 let report_name_collision (id_to_string : id -> string)
-    (id1, meta : id * Meta.meta option) (id2 : id) (name : string) : unit =
+    ((id1, meta) : id * Meta.meta option) (id2 : id) (name : string) : unit =
   let id1 = "\n- " ^ id_to_string id1 in
   let id2 = "\n- " ^ id_to_string id2 in
   let err =
@@ -278,16 +278,16 @@ let names_map_check_collision (id_to_string : id -> string) (id : id)
       report_name_collision id_to_string clash id name
 
 (** Insert bindings in a names map without checking for collisions *)
-let names_map_add_unchecked (id, meta : id * Meta.meta option) (name : string) (nm : names_map) :
-    names_map =
+let names_map_add_unchecked ((id, meta) : id * Meta.meta option) (name : string)
+    (nm : names_map) : names_map =
   (* Insert *)
   let id_to_name = IdMap.add id name nm.id_to_name in
-  let name_to_id= StringMap.add name (id, meta) nm.name_to_id in
+  let name_to_id = StringMap.add name (id, meta) nm.name_to_id in
   let names_set = StringSet.add name nm.names_set in
   { id_to_name; name_to_id; names_set }
 
-let names_map_add (id_to_string : id -> string) (id, meta : id * meta option) (name : string)
-    (nm : names_map) : names_map =
+let names_map_add (id_to_string : id -> string) ((id, meta) : id * meta option)
+    (name : string) (nm : names_map) : names_map =
   (* Check if there is a clash *)
   names_map_check_collision id_to_string id name nm;
   (* Sanity check *)
@@ -385,8 +385,8 @@ let allow_collisions (id : id) : bool =
 
 (** The [id_to_string] function to print nice debugging messages if there are
     collisions *)
-let names_maps_add (meta : Meta.meta option) (id_to_string : id -> string) (id : id) (name : string)
-    (nm : names_maps) : names_maps =
+let names_maps_add (meta : Meta.meta option) (id_to_string : id -> string)
+    (id : id) (name : string) (nm : names_maps) : names_maps =
   (* We do not use the same name map if we allow/disallow collisions.
      We notably use it for field names: some backends like Lean can use the
      type information to disambiguate field projections.
@@ -480,8 +480,9 @@ let names_maps_add_assumed_variant (id_to_string : id -> string)
     (nm : names_maps) : names_maps =
   names_maps_add None id_to_string (VariantId (TAssumed id, variant_id)) name nm
 
-let names_maps_add_function (id_to_string : id -> string) (fid, meta : fun_id * meta option)
-    (name : string) (nm : names_maps) : names_maps =
+let names_maps_add_function (id_to_string : id -> string)
+    ((fid, meta) : fun_id * meta option) (name : string) (nm : names_maps) :
+    names_maps =
   names_maps_add meta id_to_string (FunId fid) name nm
 
 let bool_name () = if !backend = Lean then "Bool" else "bool"
@@ -660,7 +661,9 @@ let id_to_string (meta : Meta.meta option) (id : id) (ctx : extraction_ctx) :
 let ctx_add (meta : Meta.meta) (id : id) (name : string) (ctx : extraction_ctx)
     : extraction_ctx =
   let id_to_string (id : id) : string = id_to_string (Some meta) id ctx in
-  let names_maps = names_maps_add (Some meta) id_to_string id name ctx.names_maps in
+  let names_maps =
+    names_maps_add (Some meta) id_to_string id name ctx.names_maps
+  in
   { ctx with names_maps }
 
 let ctx_get (meta : Meta.meta option) (id : id) (ctx : extraction_ctx) : string
@@ -1156,9 +1159,12 @@ let initialize_names_maps () : names_maps =
   in
   let assumed_functions =
     List.map
-      (fun (fid, name) -> ((FromLlbc (Pure.FunId (FAssumed fid), None), None), name))
+      (fun (fid, name) ->
+        ((FromLlbc (Pure.FunId (FAssumed fid), None), None), name))
       init.assumed_llbc_functions
-    @ List.map (fun (fid, name) -> ((Pure fid, None), name)) init.assumed_pure_functions
+    @ List.map
+        (fun (fid, name) -> ((Pure fid, None), name))
+        init.assumed_pure_functions
   in
   let nm =
     List.fold_left
-- 
cgit v1.2.3


From 8a8f3ee2e444542112a3b0ea0b4e6283b1893aaa Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 4 Apr 2024 10:57:01 +0200
Subject: Make minor modifications

---
 compiler/ExtractBase.ml | 36 +++++++++++++++++++++---------------
 1 file changed, 21 insertions(+), 15 deletions(-)

(limited to 'compiler')

diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 34b5ad64..451c2c41 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -254,28 +254,34 @@ let empty_names_map : names_map =
 
 (** Small helper to report name collision *)
 let report_name_collision (id_to_string : id -> string)
-    ((id1, meta) : id * Meta.meta option) (id2 : id) (name : string) : unit =
-  let id1 = "\n- " ^ id_to_string id1 in
-  let id2 = "\n- " ^ id_to_string id2 in
+    ((id1, meta1) : id * Meta.meta option) (id2 : id) (meta2 : Meta.meta option)
+    (name : string) : unit =
+  let meta_to_string (meta : Meta.meta option) =
+    match meta with
+    | None -> ""
+    | Some meta -> "\n  " ^ Errors.meta_to_string meta.span
+  in
+  let id1 = "\n- " ^ id_to_string id1 ^ meta_to_string meta1 in
+  let id2 = "\n- " ^ id_to_string id2 ^ meta_to_string meta2 in
   let err =
     "Name clash detected: the following identifiers are bound to the same name \
      \"" ^ name ^ "\":" ^ id1 ^ id2
     ^ "\nYou may want to rename some of your definitions, or report an issue."
   in
   (* If we fail hard on errors, raise an exception *)
-  save_error __FILE__ __LINE__ meta err
+  save_error __FILE__ __LINE__ meta1 err
 
 let names_map_get_id_from_name (name : string) (nm : names_map) :
     (id * Meta.meta option) option =
   StringMap.find_opt name nm.name_to_id
 
 let names_map_check_collision (id_to_string : id -> string) (id : id)
-    (name : string) (nm : names_map) : unit =
+    (meta : Meta.meta option) (name : string) (nm : names_map) : unit =
   match names_map_get_id_from_name name nm with
   | None -> () (* Ok *)
   | Some clash ->
       (* There is a clash: print a nice debugging message for the user *)
-      report_name_collision id_to_string clash id name
+      report_name_collision id_to_string clash id meta name
 
 (** Insert bindings in a names map without checking for collisions *)
 let names_map_add_unchecked ((id, meta) : id * Meta.meta option) (name : string)
@@ -289,7 +295,7 @@ let names_map_add_unchecked ((id, meta) : id * Meta.meta option) (name : string)
 let names_map_add (id_to_string : id -> string) ((id, meta) : id * meta option)
     (name : string) (nm : names_map) : names_map =
   (* Check if there is a clash *)
-  names_map_check_collision id_to_string id name nm;
+  names_map_check_collision id_to_string id meta name nm;
   (* Sanity check *)
   (if StringSet.mem name nm.names_set then
      let err =
@@ -385,8 +391,8 @@ let allow_collisions (id : id) : bool =
 
 (** The [id_to_string] function to print nice debugging messages if there are
     collisions *)
-let names_maps_add (meta : Meta.meta option) (id_to_string : id -> string)
-    (id : id) (name : string) (nm : names_maps) : names_maps =
+let names_maps_add (id_to_string : id -> string) (id : id)
+    (meta : Meta.meta option) (name : string) (nm : names_maps) : names_maps =
   (* We do not use the same name map if we allow/disallow collisions.
      We notably use it for field names: some backends like Lean can use the
      type information to disambiguate field projections.
@@ -401,7 +407,7 @@ let names_maps_add (meta : Meta.meta option) (id_to_string : id -> string)
   *)
   if allow_collisions id then (
     (* Check with the ids which are considered to be strict on collisions *)
-    names_map_check_collision id_to_string id name nm.strict_names_map;
+    names_map_check_collision id_to_string id meta name nm.strict_names_map;
     {
       nm with
       unsafe_names_map = unsafe_names_map_add id name nm.unsafe_names_map;
@@ -469,21 +475,21 @@ type names_map_init = {
 
 let names_maps_add_assumed_type (id_to_string : id -> string) (id : assumed_ty)
     (name : string) (nm : names_maps) : names_maps =
-  names_maps_add None id_to_string (TypeId (TAssumed id)) name nm
+  names_maps_add id_to_string (TypeId (TAssumed id)) None name nm
 
 let names_maps_add_assumed_struct (id_to_string : id -> string)
     (id : assumed_ty) (name : string) (nm : names_maps) : names_maps =
-  names_maps_add None id_to_string (StructId (TAssumed id)) name nm
+  names_maps_add id_to_string (StructId (TAssumed id)) None name nm
 
 let names_maps_add_assumed_variant (id_to_string : id -> string)
     (id : assumed_ty) (variant_id : VariantId.id) (name : string)
     (nm : names_maps) : names_maps =
-  names_maps_add None id_to_string (VariantId (TAssumed id, variant_id)) name nm
+  names_maps_add id_to_string (VariantId (TAssumed id, variant_id)) None name nm
 
 let names_maps_add_function (id_to_string : id -> string)
     ((fid, meta) : fun_id * meta option) (name : string) (nm : names_maps) :
     names_maps =
-  names_maps_add meta id_to_string (FunId fid) name nm
+  names_maps_add id_to_string (FunId fid) meta name nm
 
 let bool_name () = if !backend = Lean then "Bool" else "bool"
 let char_name () = if !backend = Lean then "Char" else "char"
@@ -662,7 +668,7 @@ let ctx_add (meta : Meta.meta) (id : id) (name : string) (ctx : extraction_ctx)
     : extraction_ctx =
   let id_to_string (id : id) : string = id_to_string (Some meta) id ctx in
   let names_maps =
-    names_maps_add (Some meta) id_to_string id name ctx.names_maps
+    names_maps_add id_to_string id (Some meta) name ctx.names_maps
   in
   { ctx with names_maps }
 
-- 
cgit v1.2.3


From eae7ce912c8bae44f98e1d489aba5618c0029bd2 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 4 Apr 2024 10:59:46 +0200
Subject: Make a minor modification

---
 compiler/ExtractBase.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'compiler')

diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 451c2c41..d760ab1e 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -268,8 +268,10 @@ let report_name_collision (id_to_string : id -> string)
      \"" ^ name ^ "\":" ^ id1 ^ id2
     ^ "\nYou may want to rename some of your definitions, or report an issue."
   in
-  (* If we fail hard on errors, raise an exception *)
-  save_error __FILE__ __LINE__ meta1 err
+  (* If we fail hard on errors, raise an exception - we don't link this error
+     to any meta information because we already put the span information about
+     the two problematic definitions in the error message above. *)
+  save_error __FILE__ __LINE__ None err
 
 let names_map_get_id_from_name (name : string) (nm : names_map) :
     (id * Meta.meta option) option =
-- 
cgit v1.2.3


From f58161f23ccb4bff2080a7c63105d80777c33362 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 4 Apr 2024 11:00:23 +0200
Subject: Update a comment

---
 compiler/ExtractBase.ml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'compiler')

diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index d760ab1e..f8d3cd96 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -268,9 +268,11 @@ let report_name_collision (id_to_string : id -> string)
      \"" ^ name ^ "\":" ^ id1 ^ id2
     ^ "\nYou may want to rename some of your definitions, or report an issue."
   in
-  (* If we fail hard on errors, raise an exception - we don't link this error
-     to any meta information because we already put the span information about
-     the two problematic definitions in the error message above. *)
+  (* Register the error.
+
+     We don't link this error to any meta information because we already put
+     the span information about the two problematic definitions in the error
+     message above. *)
   save_error __FILE__ __LINE__ None err
 
 let names_map_get_id_from_name (name : string) (nm : names_map) :
-- 
cgit v1.2.3


From 795e2107e305d425efdf6071b29f186cae83656b Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 4 Apr 2024 11:56:09 +0200
Subject: Update the names of the synthesized backward functions

---
 compiler/ExtractBase.ml    | 6 ++++--
 compiler/SymbolicToPure.ml | 9 +++++++++
 2 files changed, 13 insertions(+), 2 deletions(-)

(limited to 'compiler')

diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 74ac9e32..0a7c8df2 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -1662,9 +1662,11 @@ let ctx_compute_var_basename (meta : Meta.meta) (ctx : extraction_ctx)
   in
   (* If there is a basename, we use it *)
   match basename with
-  | Some basename ->
+  | Some basename -> (
       (* This should be a no-op *)
-      to_snake_case basename
+      match !Config.backend with
+      | Lean -> basename
+      | FStar | Coq | HOL4 -> to_snake_case basename)
   | None -> (
       (* No basename: we use the first letter of the type *)
       match ty with
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 0c30f44c..7e970029 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -1502,6 +1502,15 @@ let fresh_back_vars_for_current_fun (ctx : bs_ctx)
         match ty with None -> None | Some ty -> Some (name, ty))
       back_vars
   in
+  (* If there is one backward function or less, we use the name "back"
+     (there is no point in using the lifetime name, and it makes the
+     code generation more stable) *)
+  let num_back_vars = List.length (List.filter_map (fun x -> x) back_vars) in
+  let back_vars =
+    if num_back_vars = 1 then
+      List.map (Option.map (fun (_, ty) -> (Some "back", ty))) back_vars
+    else back_vars
+  in
   fresh_opt_vars back_vars ctx
 
 (** IMPORTANT: do not use this one directly, but rather {!symbolic_value_to_texpression} *)
-- 
cgit v1.2.3


From bac38f94aacf4a0d621b0b2d2c423db9e0c6f175 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 4 Apr 2024 13:21:08 +0200
Subject: Improve the name of the backward functions further

---
 compiler/PureUtils.ml      | 11 ++++++++---
 compiler/SymbolicToPure.ml | 13 +++++++++++--
 2 files changed, 19 insertions(+), 5 deletions(-)

(limited to 'compiler')

diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index 4bc90872..6f44bb74 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -75,10 +75,15 @@ let inputs_info_is_wf (info : inputs_info) : bool =
 let fun_sig_info_is_wf (info : fun_sig_info) : bool =
   inputs_info_is_wf info.fwd_info
 
+let opt_dest_arrow_ty (ty : ty) : (ty * ty) option =
+  match ty with TArrow (arg_ty, ret_ty) -> Some (arg_ty, ret_ty) | _ -> None
+
+let is_arrow_ty (ty : ty) : bool = Option.is_some (opt_dest_arrow_ty ty)
+
 let dest_arrow_ty (meta : Meta.meta) (ty : ty) : ty * ty =
-  match ty with
-  | TArrow (arg_ty, ret_ty) -> (arg_ty, ret_ty)
-  | _ -> craise __FILE__ __LINE__ meta "Not an arrow type"
+  match opt_dest_arrow_ty ty with
+  | Some (arg_ty, ret_ty) -> (arg_ty, ret_ty)
+  | None -> craise __FILE__ __LINE__ meta "Not an arrow type"
 
 let compute_literal_type (cv : literal) : literal_type =
   match cv with
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 7e970029..67fd2c9b 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -1499,7 +1499,14 @@ let fresh_back_vars_for_current_fun (ctx : bs_ctx)
   let back_vars =
     List.map
       (fun (name, ty) ->
-        match ty with None -> None | Some ty -> Some (name, ty))
+        match ty with
+        | None -> None
+        | Some ty ->
+            (* If the type is not an arrow type, don't use the name "back"
+               (it is a backward function with no inputs, that is to say a
+               value) *)
+            let name = if is_arrow_ty ty then name else None in
+            Some (name, ty))
       back_vars
   in
   (* If there is one backward function or less, we use the name "back"
@@ -1508,7 +1515,9 @@ let fresh_back_vars_for_current_fun (ctx : bs_ctx)
   let num_back_vars = List.length (List.filter_map (fun x -> x) back_vars) in
   let back_vars =
     if num_back_vars = 1 then
-      List.map (Option.map (fun (_, ty) -> (Some "back", ty))) back_vars
+      List.map
+        (Option.map (fun (name, ty) -> (Option.map (fun _ -> "back") name, ty)))
+        back_vars
     else back_vars
   in
   fresh_opt_vars back_vars ctx
-- 
cgit v1.2.3


From 16ea3ca854a77703487afa8732f247bc26cba695 Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Thu, 4 Apr 2024 13:23:50 +0200
Subject: Now prints all errors in the error_list

---
 compiler/Errors.ml | 6 ++++++
 compiler/Main.ml   | 8 +++++---
 2 files changed, 11 insertions(+), 3 deletions(-)

(limited to 'compiler')

diff --git a/compiler/Errors.ml b/compiler/Errors.ml
index 30887593..7dfe659a 100644
--- a/compiler/Errors.ml
+++ b/compiler/Errors.ml
@@ -20,6 +20,12 @@ let format_error_message_with_file_line (file : string) (line : int)
   "In file " ^ file ^ ", line " ^ string_of_int line ^ ":\n"
   ^ format_error_message meta msg
 
+let error_list_to_string (error_list : (Meta.meta option * string) list) :
+    string =
+  List.fold_left
+    (fun errors (meta, msg) -> errors ^ "\n" ^ format_error_message meta msg)
+    "" error_list
+
 exception CFailure of (Meta.meta option * string)
 
 let error_list : (Meta.meta option * string) list ref = ref []
diff --git a/compiler/Main.ml b/compiler/Main.ml
index db200f37..9e72a21b 100644
--- a/compiler/Main.ml
+++ b/compiler/Main.ml
@@ -274,12 +274,14 @@ let () =
 
          (* Translate the functions *)
          Aeneas.Translate.translate_crate filename dest_dir m
-       with Errors.CFailure (meta, msg) ->
+       with Errors.CFailure (_, _) ->
          (* In theory it shouldn't happen, but there may be uncaught errors -
             note that we let the [Failure] exceptions go through (they are
             send if we use the option [-abort-on-error] *)
-         log#serror (Errors.format_error_message meta msg);
-         exit 1);
+         if not (List.is_empty !Errors.error_list) then (
+           let errors = Errors.error_list_to_string !Errors.error_list in
+           log#serror errors;
+           exit 1));
 
       (* Print total elapsed time *)
       log#linfo
-- 
cgit v1.2.3


From ec7a1d3c94846a94481a487dd077efb6ddb108fe Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 4 Apr 2024 13:27:02 +0200
Subject: Make a minor update in SymbolicToPure

---
 compiler/SymbolicToPure.ml | 15 +++++++--------
 1 file changed, 7 insertions(+), 8 deletions(-)

(limited to 'compiler')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 67fd2c9b..5cd13072 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -2258,15 +2258,14 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
                  (fun ty ->
                    match ty with
                    | None -> None
-                   | Some (back_sg, ty) ->
-                       (* We insert a name for the variable only if the function
-                          can fail: if it can fail, it means the call returns a backward
-                          function. Otherwise, it directly returns the value given
-                          back by the backward function, which means we shouldn't
-                          give it a name like "back..." (it doesn't make sense) *)
+                   | Some (_back_sg, ty) ->
+                       (* We insert a name for the variable only if the type
+                          is an arrow type. If it is not, it means the backward
+                          function is degenerate (it takes no inputs) so it is
+                          not a function anymore but a value: it doesn't make
+                          sense to use a name like "back...". *)
                        let name =
-                         if back_sg.effect_info.can_fail then Some back_fun_name
-                         else None
+                         if is_arrow_ty ty then Some back_fun_name else None
                        in
                        Some (name, ty))
                  back_tys)
-- 
cgit v1.2.3


From 1f3ce79023d902d0145da38e878d991a6ba29236 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 4 Apr 2024 15:47:54 +0200
Subject: Update the way errors are reported

---
 compiler/Errors.ml |  6 ------
 compiler/Main.ml   | 11 +++++++----
 2 files changed, 7 insertions(+), 10 deletions(-)

(limited to 'compiler')

diff --git a/compiler/Errors.ml b/compiler/Errors.ml
index 7dfe659a..30887593 100644
--- a/compiler/Errors.ml
+++ b/compiler/Errors.ml
@@ -20,12 +20,6 @@ let format_error_message_with_file_line (file : string) (line : int)
   "In file " ^ file ^ ", line " ^ string_of_int line ^ ":\n"
   ^ format_error_message meta msg
 
-let error_list_to_string (error_list : (Meta.meta option * string) list) :
-    string =
-  List.fold_left
-    (fun errors (meta, msg) -> errors ^ "\n" ^ format_error_message meta msg)
-    "" error_list
-
 exception CFailure of (Meta.meta option * string)
 
 let error_list : (Meta.meta option * string) list ref = ref []
diff --git a/compiler/Main.ml b/compiler/Main.ml
index 9e72a21b..416f3a07 100644
--- a/compiler/Main.ml
+++ b/compiler/Main.ml
@@ -278,10 +278,13 @@ let () =
          (* In theory it shouldn't happen, but there may be uncaught errors -
             note that we let the [Failure] exceptions go through (they are
             send if we use the option [-abort-on-error] *)
-         if not (List.is_empty !Errors.error_list) then (
-           let errors = Errors.error_list_to_string !Errors.error_list in
-           log#serror errors;
-           exit 1));
+         ());
+
+      if !Errors.error_list <> [] then (
+        List.iter
+          (fun (meta, msg) -> log#serror (Errors.format_error_message meta msg))
+          !Errors.error_list;
+        exit 1);
 
       (* Print total elapsed time *)
       log#linfo
-- 
cgit v1.2.3


From 77208249c717579d1014f27592566069b8cd0eb2 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 4 Apr 2024 15:57:12 +0200
Subject: Fix a minor issue

---
 compiler/ExtractBase.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'compiler')

diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 6130528c..47b613c2 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -259,7 +259,7 @@ let report_name_collision (id_to_string : id -> string)
   let meta_to_string (meta : Meta.meta option) =
     match meta with
     | None -> ""
-    | Some meta -> "\n  " ^ Errors.meta_to_string meta.span
+    | Some meta -> "\n  " ^ Errors.meta_to_string meta
   in
   let id1 = "\n- " ^ id_to_string id1 ^ meta_to_string meta1 in
   let id2 = "\n- " ^ id_to_string id2 ^ meta_to_string meta2 in
-- 
cgit v1.2.3


From 57b71cb1bfde1832097163c7169aaf97cf8c7583 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 4 Apr 2024 16:19:08 +0200
Subject: Update the extraction

---
 compiler/Extract.ml         |  6 +++---
 compiler/ExtractBase.ml     |  8 ++++----
 compiler/PrintPure.ml       |  4 ++--
 compiler/Pure.ml            |  2 +-
 compiler/PureMicroPasses.ml | 21 ++++++++++-----------
 compiler/PureTypeCheck.ml   |  2 +-
 compiler/PureUtils.ml       | 14 ++++++--------
 compiler/SymbolicToPure.ml  |  7 +++----
 8 files changed, 30 insertions(+), 34 deletions(-)

(limited to 'compiler')

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 1f9c9117..27e9a62c 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -2853,7 +2853,7 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
         F.pp_print_string fmt "=";
         F.pp_print_space fmt ();
         let success =
-          ctx_get_variant def.meta (TAssumed TResult) result_return_id ctx
+          ctx_get_variant def.meta (TAssumed TResult) result_ok_id ctx
         in
         F.pp_print_string fmt (success ^ " ())")
     | Coq ->
@@ -2884,11 +2884,11 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
         F.pp_print_string fmt "==";
         F.pp_print_space fmt ();
         let success =
-          ctx_get_variant def.meta (TAssumed TResult) result_return_id ctx
+          ctx_get_variant def.meta (TAssumed TResult) result_ok_id ctx
         in
         F.pp_print_string fmt (success ^ " ())")
     | HOL4 ->
-        F.pp_print_string fmt "val _ = assert_return (";
+        F.pp_print_string fmt "val _ = assert_ok (";
         F.pp_print_string fmt "“";
         let fun_name =
           ctx_get_local_function def.meta def.def_id def.loop_id ctx
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index ce8c38ba..8b17591e 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -1020,7 +1020,7 @@ let assumed_variants () : (assumed_ty * VariantId.id * string) list =
   match !backend with
   | FStar ->
       [
-        (TResult, result_return_id, "Return");
+        (TResult, result_ok_id, "Ok");
         (TResult, result_fail_id, "Fail");
         (TError, error_failure_id, "Failure");
         (TError, error_out_of_fuel_id, "OutOfFuel");
@@ -1029,7 +1029,7 @@ let assumed_variants () : (assumed_ty * VariantId.id * string) list =
       ]
   | Coq ->
       [
-        (TResult, result_return_id, "Return");
+        (TResult, result_ok_id, "Ok");
         (TResult, result_fail_id, "Fail_");
         (TError, error_failure_id, "Failure");
         (TError, error_out_of_fuel_id, "OutOfFuel");
@@ -1038,7 +1038,7 @@ let assumed_variants () : (assumed_ty * VariantId.id * string) list =
       ]
   | Lean ->
       [
-        (TResult, result_return_id, "Result.ret");
+        (TResult, result_ok_id, "Result.ok");
         (TResult, result_fail_id, "Result.fail");
         (* For panic: we omit the prefix "Error." because the type is always
            clear from the context. Also, "Error" is often used by user-defined
@@ -1049,7 +1049,7 @@ let assumed_variants () : (assumed_ty * VariantId.id * string) list =
       ]
   | HOL4 ->
       [
-        (TResult, result_return_id, "Return");
+        (TResult, result_ok_id, "Ok");
         (TResult, result_fail_id, "Fail");
         (TError, error_failure_id, "Failure");
         (* No Fuel::Zero on purpose *)
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml
index d0c243bb..43ec083e 100644
--- a/compiler/PrintPure.ml
+++ b/compiler/PrintPure.ml
@@ -311,7 +311,7 @@ let adt_variant_to_string ?(meta = None) (env : fmt_env) (adt_id : type_id)
           craise_opt_meta __FILE__ __LINE__ meta "Unreachable"
       | TResult ->
           let variant_id = Option.get variant_id in
-          if variant_id = result_return_id then "@Result::Return"
+          if variant_id = result_ok_id then "@Result::Return"
           else if variant_id = result_fail_id then "@Result::Fail"
           else
             craise_opt_meta __FILE__ __LINE__ meta
@@ -394,7 +394,7 @@ let adt_g_value_to_string ?(meta : Meta.meta option = None) (env : fmt_env)
           craise_opt_meta __FILE__ __LINE__ meta "Unreachable"
       | TResult ->
           let variant_id = Option.get variant_id in
-          if variant_id = result_return_id then
+          if variant_id = result_ok_id then
             match field_values with
             | [ v ] -> "@Result::Return " ^ v
             | _ ->
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index 7de7e0f4..daf213cf 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -92,7 +92,7 @@ type assumed_ty =
 (* TODO: we should never directly manipulate [Return] and [Fail], but rather
  * the monadic functions [return] and [fail] (makes treatment of error and
  * state-error monads more uniform) *)
-let result_return_id = VariantId.of_int 0
+let result_ok_id = VariantId.of_int 0
 let result_fail_id = VariantId.of_int 1
 let option_some_id = T.option_some_id
 let option_none_id = T.option_none_id
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 9fa07029..b1c85d61 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -751,7 +751,7 @@ let simplify_let_bindings (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
               },
               x ) ->
             (* return/fail case *)
-            if variant_id = result_return_id then
+            if variant_id = result_ok_id then
               (* Return case - note that the simplification we just perform
                  might have unlocked the tuple simplification below *)
               self#visit_Let env false lv x next
@@ -1082,19 +1082,19 @@ let filter_useless (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
       let body = { body with body = body_exp; inputs_lvs } in
       { def with body = Some body }
 
-(** Simplify the lets immediately followed by a return.
+(** Simplify the lets immediately followed by an ok.
 
     Ex.:
     {[
       x <-- f y;
-      Return x
+      Ok x
 
         ~~>
 
       f y
     ]}
  *)
-let simplify_let_then_return _ctx (def : fun_decl) =
+let simplify_let_then_ok _ctx (def : fun_decl) =
   (* Match a pattern and an expression: evaluates to [true] if the expression
      is actually exactly the pattern *)
   let rec match_pattern_and_expr (pat : typed_pattern) (e : texpression) : bool
@@ -1150,7 +1150,7 @@ let simplify_let_then_return _ctx (def : fun_decl) =
               | Some e ->
                   if match_pattern_and_expr lv e then
                     (* We need to wrap the right-value in a ret *)
-                    (mk_result_return_texpression def.meta rv).e
+                    (mk_result_ok_texpression def.meta rv).e
                   else not_simpl_e
               | None ->
                   if match_pattern_and_expr lv next_e then rv.e else not_simpl_e
@@ -1789,7 +1789,7 @@ let unfold_monadic_let_bindings (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
               let err_v = mk_texpression_from_var err_var in
               let fail_value = mk_result_fail_texpression def.meta err_v e.ty in
               let fail_branch = { pat = fail_pat; branch = fail_value } in
-              let success_pat = mk_result_return_pattern lv in
+              let success_pat = mk_result_ok_pattern lv in
               let success_branch = { pat = success_pat; branch = e } in
               let switch_body = Match [ fail_branch; success_branch ] in
               let e = Switch (re, switch_body) in
@@ -1852,9 +1852,9 @@ let apply_end_passes_to_def (ctx : trans_ctx) (def : fun_decl) : fun_decl =
        f y
      ]}
   *)
-  let def = simplify_let_then_return ctx def in
+  let def = simplify_let_then_ok ctx def in
   log#ldebug
-    (lazy ("simplify_let_then_return:\n\n" ^ fun_decl_to_string ctx def ^ "\n"));
+    (lazy ("simplify_let_then_ok:\n\n" ^ fun_decl_to_string ctx def ^ "\n"));
 
   (* Simplify the aggregated ADTs.
 
@@ -1890,11 +1890,10 @@ let apply_end_passes_to_def (ctx : trans_ctx) (def : fun_decl) : fun_decl =
 
   (* Simplify the let-then return again (the lambda simplification may have
      unlocked more simplifications here) *)
-  let def = simplify_let_then_return ctx def in
+  let def = simplify_let_then_ok ctx def in
   log#ldebug
     (lazy
-      ("simplify_let_then_return (pass 2):\n\n" ^ fun_decl_to_string ctx def
-     ^ "\n"));
+      ("simplify_let_then_ok (pass 2):\n\n" ^ fun_decl_to_string ctx def ^ "\n"));
 
   (* Decompose the monadic let-bindings - used by Coq *)
   let def =
diff --git a/compiler/PureTypeCheck.ml b/compiler/PureTypeCheck.ml
index 53ff8983..9eed76b2 100644
--- a/compiler/PureTypeCheck.ml
+++ b/compiler/PureTypeCheck.ml
@@ -32,7 +32,7 @@ let get_adt_field_types (meta : Meta.meta)
       | TResult ->
           let ty = Collections.List.to_cons_nil generics.types in
           let variant_id = Option.get variant_id in
-          if variant_id = result_return_id then [ ty ]
+          if variant_id = result_ok_id then [ ty ]
           else if variant_id = result_fail_id then [ mk_error_ty ]
           else
             craise __FILE__ __LINE__ meta
diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index 6f44bb74..e8f2d95e 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -583,12 +583,12 @@ let mk_result_fail_texpression_with_error_id (meta : Meta.meta)
   let error = mk_error error in
   mk_result_fail_texpression meta error ty
 
-let mk_result_return_texpression (meta : Meta.meta) (v : texpression) :
-    texpression =
+let mk_result_ok_texpression (meta : Meta.meta) (v : texpression) : texpression
+    =
   let type_args = [ v.ty ] in
   let ty = TAdt (TAssumed TResult, mk_generic_args_from_types type_args) in
   let id =
-    AdtCons { adt_id = TAssumed TResult; variant_id = Some result_return_id }
+    AdtCons { adt_id = TAssumed TResult; variant_id = Some result_ok_id }
   in
   let qualif = { id; generics = mk_generic_args_from_types type_args } in
   let cons_e = Qualif qualif in
@@ -610,11 +610,9 @@ let mk_result_fail_pattern_ignore_error (ty : ty) : typed_pattern =
   let error_pat : pattern = PatDummy in
   mk_result_fail_pattern error_pat ty
 
-let mk_result_return_pattern (v : typed_pattern) : typed_pattern =
+let mk_result_ok_pattern (v : typed_pattern) : typed_pattern =
   let ty = TAdt (TAssumed TResult, mk_generic_args_from_types [ v.ty ]) in
-  let value =
-    PatAdt { variant_id = Some result_return_id; field_values = [ v ] }
-  in
+  let value = PatAdt { variant_id = Some result_ok_id; field_values = [ v ] } in
   { value; ty }
 
 let opt_unmeta_mplace (e : texpression) : mplace option * texpression =
@@ -788,6 +786,6 @@ let opt_destruct_ret (e : texpression) : texpression option =
           ty = _;
         },
         arg )
-    when variant_id = Some result_return_id ->
+    when variant_id = Some result_ok_id ->
       Some arg
   | _ -> None
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 5cd13072..38ee5df1 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -2102,7 +2102,7 @@ and translate_return (ectx : C.eval_ctx) (opt_v : V.typed_value option)
     else output
   in
   (* Wrap in a result - TODO: check effect_info.can_fail to not always wrap *)
-  mk_result_return_texpression ctx.meta output
+  mk_result_ok_texpression ctx.meta output
 
 and translate_return_with_loop (loop_id : V.LoopId.id) (is_continue : bool)
     (ctx : bs_ctx) : texpression =
@@ -2150,8 +2150,7 @@ and translate_return_with_loop (loop_id : V.LoopId.id) (is_continue : bool)
     else output
   in
   (* Wrap in a result - TODO: check effect_info.can_fail to not always wrap *)
-  mk_emeta (Tag "return_with_loop")
-    (mk_result_return_texpression ctx.meta output)
+  mk_emeta (Tag "return_with_loop") (mk_result_ok_texpression ctx.meta output)
 
 and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
     texpression =
@@ -3226,7 +3225,7 @@ and translate_forward_end (ectx : C.eval_ctx)
 
     let state_var = List.map mk_texpression_from_var state_var in
     let ret = mk_simpl_tuple_texpression ctx.meta (state_var @ [ ret ]) in
-    let ret = mk_result_return_texpression ctx.meta ret in
+    let ret = mk_result_ok_texpression ctx.meta ret in
 
     (* Introduce all the let-bindings *)
 
-- 
cgit v1.2.3


From 9c1773530a7056c161e69471b36eaa3603f6ed26 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 4 Apr 2024 17:58:32 +0200
Subject: Add field mk_return, mk_panic in SymbolicToPure.bs_ctx

---
 compiler/SymbolicToPure.ml | 240 ++++++++++++++++++++++++++++-----------------
 compiler/Translate.ml      |   2 +
 2 files changed, 152 insertions(+), 90 deletions(-)

(limited to 'compiler')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 38ee5df1..482ebf3a 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -268,6 +268,22 @@ type bs_ctx = {
           Note that when a function contains a loop, we group the function symbolic AST and the loop symbolic
           AST in a single function.
        *)
+  mk_return : (bs_ctx -> texpression option -> texpression) option;
+      (** Small helper: translate a [return] expression, given a value to "return".
+          The translation of [return] depends on the context, and in particular depends on
+          whether we are inside a subexpression like a loop or not.
+
+          Note that the function consumes an optional expression, which is:
+          - [Some] for a forward computation
+          - [None] for a backward computation
+
+          We initialize this at [None].
+      *)
+  mk_panic : texpression option;
+      (** Small helper: translate a [fail] expression.
+
+      We initialize this at [None].
+  *)
 }
 [@@deriving show]
 
@@ -2008,54 +2024,7 @@ let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression =
       translate_forward_end ectx loop_input_values e back_e ctx
   | Loop loop -> translate_loop loop ctx
 
-and translate_panic (ctx : bs_ctx) : texpression =
-  (* Here we use the function return type - note that it is ok because
-   * we don't match on panics which happen inside the function body -
-   * but it won't be true anymore once we translate individual blocks *)
-  (* If we use a state monad, we need to add a lambda for the state variable *)
-  (* Note that only forward functions return a state *)
-  let effect_info = ctx_get_effect_info ctx in
-  (* TODO: we should use a [Fail] function *)
-  let mk_output output_ty =
-    if effect_info.stateful then
-      (* Create the [Fail] value *)
-      let ret_ty = mk_simpl_tuple_ty [ mk_state_ty; output_ty ] in
-      let ret_v =
-        mk_result_fail_texpression_with_error_id ctx.meta error_failure_id
-          ret_ty
-      in
-      ret_v
-    else
-      mk_result_fail_texpression_with_error_id ctx.meta error_failure_id
-        output_ty
-  in
-  if ctx.inside_loop && Option.is_some ctx.bid then
-    (* We are synthesizing the backward function of a loop body *)
-    let bid = Option.get ctx.bid in
-    let loop_id = Option.get ctx.loop_id in
-    let loop = LoopId.Map.find loop_id ctx.loops in
-    let tys = RegionGroupId.Map.find bid loop.back_outputs in
-    let output = mk_simpl_tuple_ty tys in
-    mk_output output
-  else
-    (* Regular function, or forward function (the forward translation for
-       a loop has the same return type as the parent function)
-    *)
-    match ctx.bid with
-    | None ->
-        let back_tys = compute_back_tys ctx.sg None in
-        let back_tys = List.filter_map (fun x -> x) back_tys in
-        let tys =
-          if ctx.sg.fwd_info.ignore_output then back_tys
-          else ctx.sg.fwd_output :: back_tys
-        in
-        let output = mk_simpl_tuple_ty tys in
-        mk_output output
-    | Some bid ->
-        let output =
-          mk_simpl_tuple_ty (RegionGroupId.Map.find bid ctx.sg.back_sg).outputs
-        in
-        mk_output output
+and translate_panic (ctx : bs_ctx) : texpression = Option.get ctx.mk_panic
 
 (** [opt_v]: the value to return, in case we translate a forward body.
 
@@ -2067,42 +2036,8 @@ and translate_panic (ctx : bs_ctx) : texpression =
 *)
 and translate_return (ectx : C.eval_ctx) (opt_v : V.typed_value option)
     (ctx : bs_ctx) : texpression =
-  (* There are two cases:
-     - either we reach the return of a forward function or a forward loop body,
-       in which case the optional value should be [Some] (it is the returned value)
-     - or we are translating a backward function, in which case it should be [None]
-  *)
-  (* Compute the values that we should return *without the state and the result
-     wrapper* *)
-  let output =
-    match ctx.bid with
-    | None ->
-        (* Forward function *)
-        let v = Option.get opt_v in
-        typed_value_to_texpression ctx ectx v
-    | Some _ ->
-        (* Backward function *)
-        (* Sanity check *)
-        sanity_check __FILE__ __LINE__ (opt_v = None) ctx.meta;
-        (* Group the variables in which we stored the values we need to give back.
-           See the explanations for the [SynthInput] case in [translate_end_abstraction] *)
-        let backward_outputs = Option.get ctx.backward_outputs in
-        let field_values = List.map mk_texpression_from_var backward_outputs in
-        mk_simpl_tuple_texpression ctx.meta field_values
-  in
-  (* We may need to return a state
-   * - error-monad: Return x
-   * - state-error: Return (state, x)
-   * *)
-  let effect_info = ctx_get_effect_info ctx in
-  let output =
-    if effect_info.stateful then
-      let state_rvalue = mk_state_texpression ctx.state_var in
-      mk_simpl_tuple_texpression ctx.meta [ state_rvalue; output ]
-    else output
-  in
-  (* Wrap in a result - TODO: check effect_info.can_fail to not always wrap *)
-  mk_result_ok_texpression ctx.meta output
+  let opt_v = Option.map (typed_value_to_texpression ctx ectx) opt_v in
+  (Option.get ctx.mk_return) ctx opt_v
 
 and translate_return_with_loop (loop_id : V.LoopId.id) (is_continue : bool)
     (ctx : bs_ctx) : texpression =
@@ -3118,6 +3053,49 @@ and translate_forward_end (ectx : C.eval_ctx)
                 (ctx, backward_inputs_no_state @ [ var ])
               else (ctx, backward_inputs_no_state)
             in
+            (* Update the functions mk_return and mk_panic *)
+            let effect_info = back_sg.effect_info in
+            let mk_return ctx v =
+              assert (v = None);
+              let output =
+                (* Group the variables in which we stored the values we need to give back.
+                   See the explanations for the [SynthInput] case in [translate_end_abstraction] *)
+                let backward_outputs = Option.get ctx.backward_outputs in
+                let field_values =
+                  List.map mk_texpression_from_var backward_outputs
+                in
+                mk_simpl_tuple_texpression ctx.meta field_values
+              in
+              let output =
+                if effect_info.stateful then
+                  let state_rvalue = mk_state_texpression ctx.state_var in
+                  mk_simpl_tuple_texpression ctx.meta [ state_rvalue; output ]
+                else output
+              in
+              (* Wrap in a result - TODO: check effect_info.can_fail to not always wrap *)
+              mk_result_ok_texpression ctx.meta output
+            in
+            let mk_panic =
+              (* TODO: we should use a [Fail] function *)
+              let mk_output output_ty =
+                if effect_info.stateful then
+                  (* Create the [Fail] value *)
+                  let ret_ty = mk_simpl_tuple_ty [ mk_state_ty; output_ty ] in
+                  let ret_v =
+                    mk_result_fail_texpression_with_error_id ctx.meta
+                      error_failure_id ret_ty
+                  in
+                  ret_v
+                else
+                  mk_result_fail_texpression_with_error_id ctx.meta
+                    error_failure_id output_ty
+              in
+              let output =
+                mk_simpl_tuple_ty
+                  (RegionGroupId.Map.find bid ctx.sg.back_sg).outputs
+              in
+              mk_output output
+            in
             {
               ctx with
               backward_inputs_no_state =
@@ -3126,6 +3104,8 @@ and translate_forward_end (ectx : C.eval_ctx)
               backward_inputs_with_state =
                 RegionGroupId.Map.add bid backward_inputs_with_state
                   ctx.backward_inputs_with_state;
+              mk_return = Some mk_return;
+              mk_panic = Some mk_panic;
             }
           in
 
@@ -3470,7 +3450,6 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
   in
 
   (* Compute the backward outputs *)
-  let ctx = ref ctx in
   let rg_to_given_back_tys =
     RegionGroupId.Map.map
       (fun tys ->
@@ -3478,13 +3457,12 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
         List.map
           (fun ty ->
             cassert __FILE__ __LINE__
-              (not (TypesUtils.ty_has_borrows !ctx.type_ctx.type_infos ty))
-              !ctx.meta "The types shouldn't contain borrows";
-            ctx_translate_fwd_ty !ctx ty)
+              (not (TypesUtils.ty_has_borrows ctx.type_ctx.type_infos ty))
+              ctx.meta "The types shouldn't contain borrows";
+            ctx_translate_fwd_ty ctx ty)
           tys)
       loop.rg_to_given_back_tys
   in
-  let ctx = !ctx in
 
   (* The output type of the loop function *)
   let fwd_effect_info = { ctx.sg.fwd_info.effect_info with is_rec = true } in
@@ -3589,6 +3567,44 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
       { types; const_generics; trait_refs }
     in
 
+    (* Update the helpers to translate the fail and return expressions *)
+    let mk_panic =
+      (* Note that we reuse the effect information from the parent function *)
+      let effect_info = ctx_get_effect_info ctx in
+      let back_tys = compute_back_tys ctx.sg None in
+      let back_tys = List.filter_map (fun x -> x) back_tys in
+      let tys =
+        if ctx.sg.fwd_info.ignore_output then back_tys
+        else ctx.sg.fwd_output :: back_tys
+      in
+      let output_ty = mk_simpl_tuple_ty tys in
+      if effect_info.stateful then
+        (* Create the [Fail] value *)
+        let ret_ty = mk_simpl_tuple_ty [ mk_state_ty; output_ty ] in
+        let ret_v =
+          mk_result_fail_texpression_with_error_id ctx.meta error_failure_id
+            ret_ty
+        in
+        ret_v
+      else
+        mk_result_fail_texpression_with_error_id ctx.meta error_failure_id
+          output_ty
+    in
+    let mk_return ctx v =
+      match v with
+      | None -> raise (Failure "Unexpected")
+      | Some output ->
+          let effect_info = ctx_get_effect_info ctx in
+          let output =
+            if effect_info.stateful then
+              let state_rvalue = mk_state_texpression ctx.state_var in
+              mk_simpl_tuple_texpression ctx.meta [ state_rvalue; output ]
+            else output
+          in
+          (* Wrap in a result - TODO: check effect_info.can_fail to not always wrap *)
+          mk_result_ok_texpression ctx.meta output
+    in
+
     let loop_info =
       {
         loop_id;
@@ -3604,7 +3620,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
       }
     in
     let loops = LoopId.Map.add loop_id loop_info ctx.loops in
-    { ctx with loops }
+    { ctx with loops; mk_return = Some mk_return; mk_panic = Some mk_panic }
   in
 
   (* Update the context to translate the function end *)
@@ -3771,6 +3787,50 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
         let effect_info =
           get_fun_effect_info ctx (FunId (FRegular def_id)) None None
         in
+        let mk_return ctx v =
+          match v with
+          | None ->
+              raise
+                (Failure
+                   "Unexpected: reached a return expression without value in a \
+                    function forward expression")
+          | Some output ->
+              let output =
+                if effect_info.stateful then
+                  let state_rvalue = mk_state_texpression ctx.state_var in
+                  mk_simpl_tuple_texpression ctx.meta [ state_rvalue; output ]
+                else output
+              in
+              (* Wrap in a result - TODO: check effect_info.can_fail to not always wrap *)
+              mk_result_ok_texpression ctx.meta output
+        in
+        let mk_panic =
+          (* TODO: we should use a [Fail] function *)
+          let mk_output output_ty =
+            if effect_info.stateful then
+              (* Create the [Fail] value *)
+              let ret_ty = mk_simpl_tuple_ty [ mk_state_ty; output_ty ] in
+              let ret_v =
+                mk_result_fail_texpression_with_error_id ctx.meta
+                  error_failure_id ret_ty
+              in
+              ret_v
+            else
+              mk_result_fail_texpression_with_error_id ctx.meta error_failure_id
+                output_ty
+          in
+          let back_tys = compute_back_tys ctx.sg None in
+          let back_tys = List.filter_map (fun x -> x) back_tys in
+          let tys =
+            if ctx.sg.fwd_info.ignore_output then back_tys
+            else ctx.sg.fwd_output :: back_tys
+          in
+          let output = mk_simpl_tuple_ty tys in
+          mk_output output
+        in
+        let ctx =
+          { ctx with mk_return = Some mk_return; mk_panic = Some mk_panic }
+        in
         let body = translate_expression body ctx in
         (* Add a match over the fuel, if necessary *)
         let body =
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 348183c5..22288fe2 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -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
 
-- 
cgit v1.2.3


From fc51bfd88076a66000dbfe76e832d3fdd72aee76 Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Fri, 5 Apr 2024 10:36:40 +0200
Subject: error catching should now be able to tell when code couldn't be
 generated

---
 compiler/Extract.ml        | 181 +++++++++++++++++++++++----------------------
 compiler/SymbolicToPure.ml |   7 +-
 compiler/Translate.ml      |  57 +++++++++++---
 3 files changed, 144 insertions(+), 101 deletions(-)

(limited to 'compiler')

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index af0bf98d..1fc8a97f 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -1880,99 +1880,102 @@ let extract_global_decl_hol4_opaque (meta : Meta.meta) (ctx : extraction_ctx)
     and {!extract_fun_decl}.
  *)
 let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
-    (global : global_decl) (body : fun_decl) (interface : bool) : unit =
+    (global : global_decl option) (body : fun_decl) (interface : bool) : unit =
   let meta = body.meta in
   sanity_check __FILE__ __LINE__ body.is_global_decl_body meta;
   sanity_check __FILE__ __LINE__ (body.signature.inputs = []) meta;
-
-  (* Add a break then the name of the corresponding LLBC declaration *)
-  F.pp_print_break fmt 0 0;
-  let name =
-    if !Config.extract_external_name_patterns && not global.is_local then
-      Some global.llbc_name
-    else None
-  in
-  extract_comment_with_span ctx fmt
-    [ "[" ^ name_to_string ctx global.llbc_name ^ "]" ]
-    name global.meta.span;
-  F.pp_print_space fmt ();
-
-  let decl_name = ctx_get_global meta global.def_id ctx in
-  let body_name =
-    ctx_get_function meta
-      (FromLlbc (Pure.FunId (FRegular global.body_id), None))
-      ctx
-  in
-  let decl_ty, body_ty =
-    let ty = body.signature.output in
-    if body.signature.fwd_info.effect_info.can_fail then
-      (unwrap_result_ty meta ty, ty)
-    else (ty, mk_result_ty ty)
-  in
-  (* Add the type parameters *)
-  let ctx, type_params, cg_params, trait_clauses =
-    ctx_add_generic_params meta global.llbc_name global.llbc_generics
-      global.generics ctx
-  in
-  match body.body with
-  | None ->
-      (* No body: only generate a [val x_c : u32] declaration *)
-      let kind = if interface then Declared else Assumed in
-      if !backend = HOL4 then
-        extract_global_decl_hol4_opaque meta ctx fmt decl_name global.generics
-          decl_ty
-      else
-        extract_global_decl_body_gen meta ctx fmt kind decl_name global.generics
-          type_params cg_params trait_clauses decl_ty None
-  | Some body ->
-      (* There is a body *)
-      (* Generate: [let x_body : result u32 = Return 3] *)
-      extract_global_decl_body_gen meta ctx fmt SingleNonRec body_name
-        global.generics type_params cg_params trait_clauses body_ty
-        (Some (fun fmt -> extract_texpression meta ctx fmt false body.body));
+  match global with
+  | Some global -> (
+      (* Add a break then the name of the corresponding LLBC declaration *)
       F.pp_print_break fmt 0 0;
-      (* Generate: [let x_c : u32 = eval_global x_body] *)
-      extract_global_decl_body_gen meta ctx fmt SingleNonRec decl_name
-        global.generics type_params cg_params trait_clauses decl_ty
-        (Some
-           (fun fmt ->
-             let all_params =
-               List.concat [ type_params; cg_params; trait_clauses ]
-             in
-             let extract_params () =
-               List.iter
-                 (fun p ->
-                   F.pp_print_space fmt ();
-                   F.pp_print_string fmt p)
-                 all_params
-             in
-             let use_brackets = all_params <> [] in
-             (* Extract the name *)
-             let before, after =
-               match !backend with
-               | FStar | Lean ->
-                   ( (fun () ->
-                       F.pp_print_string fmt "eval_global";
-                       F.pp_print_space fmt ()),
-                     fun () -> () )
-               | Coq ->
-                   ((fun () -> ()), fun () -> F.pp_print_string fmt "%global")
-               | HOL4 ->
-                   ( (fun () ->
-                       F.pp_print_string fmt "get_return_value";
-                       F.pp_print_space fmt ()),
-                     fun () -> () )
-             in
-             before ();
-             if use_brackets then F.pp_print_string fmt "(";
-             F.pp_print_string fmt body_name;
-             (* Extract the generic params *)
-             extract_params ();
-             if use_brackets then F.pp_print_string fmt ")";
-             (* *)
-             after ()));
-      (* Add a break to insert lines between declarations *)
-      F.pp_print_break fmt 0 0
+      let name =
+        if !Config.extract_external_name_patterns && not global.is_local then
+          Some global.llbc_name
+        else None
+      in
+      extract_comment_with_span ctx fmt
+        [ "[" ^ name_to_string ctx global.llbc_name ^ "]" ]
+        name global.meta.span;
+      F.pp_print_space fmt ();
+
+      let decl_name = ctx_get_global meta global.def_id ctx in
+      let body_name =
+        ctx_get_function meta
+          (FromLlbc (Pure.FunId (FRegular global.body_id), None))
+          ctx
+      in
+      let decl_ty, body_ty =
+        let ty = body.signature.output in
+        if body.signature.fwd_info.effect_info.can_fail then
+          (unwrap_result_ty meta ty, ty)
+        else (ty, mk_result_ty ty)
+      in
+      (* Add the type parameters *)
+      let ctx, type_params, cg_params, trait_clauses =
+        ctx_add_generic_params meta global.llbc_name global.llbc_generics
+          global.generics ctx
+      in
+      match body.body with
+      | None ->
+          (* No body: only generate a [val x_c : u32] declaration *)
+          let kind = if interface then Declared else Assumed in
+          if !backend = HOL4 then
+            extract_global_decl_hol4_opaque meta ctx fmt decl_name
+              global.generics decl_ty
+          else
+            extract_global_decl_body_gen meta ctx fmt kind decl_name
+              global.generics type_params cg_params trait_clauses decl_ty None
+      | Some body ->
+          (* There is a body *)
+          (* Generate: [let x_body : result u32 = Return 3] *)
+          extract_global_decl_body_gen meta ctx fmt SingleNonRec body_name
+            global.generics type_params cg_params trait_clauses body_ty
+            (Some (fun fmt -> extract_texpression meta ctx fmt false body.body));
+          F.pp_print_break fmt 0 0;
+          (* Generate: [let x_c : u32 = eval_global x_body] *)
+          extract_global_decl_body_gen meta ctx fmt SingleNonRec decl_name
+            global.generics type_params cg_params trait_clauses decl_ty
+            (Some
+               (fun fmt ->
+                 let all_params =
+                   List.concat [ type_params; cg_params; trait_clauses ]
+                 in
+                 let extract_params () =
+                   List.iter
+                     (fun p ->
+                       F.pp_print_space fmt ();
+                       F.pp_print_string fmt p)
+                     all_params
+                 in
+                 let use_brackets = all_params <> [] in
+                 (* Extract the name *)
+                 let before, after =
+                   match !backend with
+                   | FStar | Lean ->
+                       ( (fun () ->
+                           F.pp_print_string fmt "eval_global";
+                           F.pp_print_space fmt ()),
+                         fun () -> () )
+                   | Coq ->
+                       ( (fun () -> ()),
+                         fun () -> F.pp_print_string fmt "%global" )
+                   | HOL4 ->
+                       ( (fun () ->
+                           F.pp_print_string fmt "get_return_value";
+                           F.pp_print_space fmt ()),
+                         fun () -> () )
+                 in
+                 before ();
+                 if use_brackets then F.pp_print_string fmt "(";
+                 F.pp_print_string fmt body_name;
+                 (* Extract the generic params *)
+                 extract_params ();
+                 if use_brackets then F.pp_print_string fmt ")";
+                 (* *)
+                 after ()));
+          (* Add a break to insert lines between declarations *)
+          F.pp_print_break fmt 0 0)
+  | None -> ()
 
 (** Similar to {!extract_trait_decl_register_names} *)
 let extract_trait_decl_register_parent_clause_names (ctx : extraction_ctx)
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index f036cc37..b4c55d80 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -3861,7 +3861,12 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
   def
 
 let translate_type_decls (ctx : Contexts.decls_ctx) : type_decl list =
-  List.map (translate_type_decl ctx)
+  List.filter_map
+    (fun a ->
+      try Some (translate_type_decl ctx a)
+      with CFailure (meta, _) ->
+        let () = save_error __FILE__ __LINE__ meta "Could not generate code, see previous error" in
+        None)
     (TypeDeclId.Map.values ctx.type_ctx.type_decls)
 
 let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl)
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 348183c5..28e5531d 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_hook (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 =
@@ -195,6 +195,17 @@ 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_hook trans_ctx pure_type_decls fun_dsigs fdef)
+  with CFailure (meta, _) ->
+    let () = save_error __FILE__ __LINE__ meta "Could not generate code, see previous error" in
+    None
+
 (* TODO: factor out the return type *)
 let translate_crate_to_pure (crate : crate) :
     trans_ctx
@@ -220,32 +231,51 @@ 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 () =
+               save_error __FILE__ __LINE__ meta "Could not generate code, see previous error"
+             in
+             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 () =
+            save_error __FILE__ __LINE__ meta "Could not generate code, see previous error"
+          in
+          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 () =
+            save_error __FILE__ __LINE__ meta "Could not generate code, see previous error"
+          in
+          None)
       (TraitImplId.Map.values trans_ctx.trait_impls_ctx.trait_impls)
   in
 
@@ -471,7 +501,12 @@ 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 () = save_error __FILE__ __LINE__ meta "Could not generate code, see previous error" in
+        None
+    in
     Extract.extract_global_decl ctx fmt global body config.interface
 
 (** Utility.
-- 
cgit v1.2.3


From 760e8374533bd7e13059e18c223428baab4535ea Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Fri, 5 Apr 2024 12:29:33 +0200
Subject: resolved comments

---
 compiler/Extract.ml        | 184 +++++++++++++++++++++++----------------------
 compiler/SymbolicToPure.ml |   5 +-
 compiler/Translate.ml      |  23 ++++--
 3 files changed, 113 insertions(+), 99 deletions(-)

(limited to 'compiler')

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 1fc8a97f..f7d08fdb 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -1879,102 +1879,104 @@ let extract_global_decl_hol4_opaque (meta : Meta.meta) (ctx : extraction_ctx)
     [{start,end}_gloabl_decl_group], contrary to {!extract_type_decl}
     and {!extract_fun_decl}.
  *)
-let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
-    (global : global_decl option) (body : fun_decl) (interface : bool) : unit =
+let extract_global_decl_aux (ctx : extraction_ctx) (fmt : F.formatter)
+    (global : global_decl) (body : fun_decl) (interface : bool) : unit =
   let meta = body.meta in
   sanity_check __FILE__ __LINE__ body.is_global_decl_body meta;
   sanity_check __FILE__ __LINE__ (body.signature.inputs = []) meta;
-  match global with
-  | Some global -> (
-      (* Add a break then the name of the corresponding LLBC declaration *)
+  (* Add a break then the name of the corresponding LLBC declaration *)
+  F.pp_print_break fmt 0 0;
+  let name =
+    if !Config.extract_external_name_patterns && not global.is_local then
+      Some global.llbc_name
+    else None
+  in
+  extract_comment_with_span ctx fmt
+    [ "[" ^ name_to_string ctx global.llbc_name ^ "]" ]
+    name global.meta.span;
+  F.pp_print_space fmt ();
+
+  let decl_name = ctx_get_global meta global.def_id ctx in
+  let body_name =
+    ctx_get_function meta
+      (FromLlbc (Pure.FunId (FRegular global.body_id), None))
+      ctx
+  in
+  let decl_ty, body_ty =
+    let ty = body.signature.output in
+    if body.signature.fwd_info.effect_info.can_fail then
+      (unwrap_result_ty meta ty, ty)
+    else (ty, mk_result_ty ty)
+  in
+  (* Add the type parameters *)
+  let ctx, type_params, cg_params, trait_clauses =
+    ctx_add_generic_params meta global.llbc_name global.llbc_generics
+      global.generics ctx
+  in
+  match body.body with
+  | None ->
+      (* No body: only generate a [val x_c : u32] declaration *)
+      let kind = if interface then Declared else Assumed in
+      if !backend = HOL4 then
+        extract_global_decl_hol4_opaque meta ctx fmt decl_name global.generics
+          decl_ty
+      else
+        extract_global_decl_body_gen meta ctx fmt kind decl_name global.generics
+          type_params cg_params trait_clauses decl_ty None
+  | Some body ->
+      (* There is a body *)
+      (* Generate: [let x_body : result u32 = Return 3] *)
+      extract_global_decl_body_gen meta ctx fmt SingleNonRec body_name
+        global.generics type_params cg_params trait_clauses body_ty
+        (Some (fun fmt -> extract_texpression meta ctx fmt false body.body));
       F.pp_print_break fmt 0 0;
-      let name =
-        if !Config.extract_external_name_patterns && not global.is_local then
-          Some global.llbc_name
-        else None
-      in
-      extract_comment_with_span ctx fmt
-        [ "[" ^ name_to_string ctx global.llbc_name ^ "]" ]
-        name global.meta.span;
-      F.pp_print_space fmt ();
+      (* Generate: [let x_c : u32 = eval_global x_body] *)
+      extract_global_decl_body_gen meta ctx fmt SingleNonRec decl_name
+        global.generics type_params cg_params trait_clauses decl_ty
+        (Some
+           (fun fmt ->
+             let all_params =
+               List.concat [ type_params; cg_params; trait_clauses ]
+             in
+             let extract_params () =
+               List.iter
+                 (fun p ->
+                   F.pp_print_space fmt ();
+                   F.pp_print_string fmt p)
+                 all_params
+             in
+             let use_brackets = all_params <> [] in
+             (* Extract the name *)
+             let before, after =
+               match !backend with
+               | FStar | Lean ->
+                   ( (fun () ->
+                       F.pp_print_string fmt "eval_global";
+                       F.pp_print_space fmt ()),
+                     fun () -> () )
+               | Coq ->
+                   ((fun () -> ()), fun () -> F.pp_print_string fmt "%global")
+               | HOL4 ->
+                   ( (fun () ->
+                       F.pp_print_string fmt "get_return_value";
+                       F.pp_print_space fmt ()),
+                     fun () -> () )
+             in
+             before ();
+             if use_brackets then F.pp_print_string fmt "(";
+             F.pp_print_string fmt body_name;
+             (* Extract the generic params *)
+             extract_params ();
+             if use_brackets then F.pp_print_string fmt ")";
+             (* *)
+             after ()));
+      (* Add a break to insert lines between declarations *)
+      F.pp_print_break fmt 0 0
 
-      let decl_name = ctx_get_global meta global.def_id ctx in
-      let body_name =
-        ctx_get_function meta
-          (FromLlbc (Pure.FunId (FRegular global.body_id), None))
-          ctx
-      in
-      let decl_ty, body_ty =
-        let ty = body.signature.output in
-        if body.signature.fwd_info.effect_info.can_fail then
-          (unwrap_result_ty meta ty, ty)
-        else (ty, mk_result_ty ty)
-      in
-      (* Add the type parameters *)
-      let ctx, type_params, cg_params, trait_clauses =
-        ctx_add_generic_params meta global.llbc_name global.llbc_generics
-          global.generics ctx
-      in
-      match body.body with
-      | None ->
-          (* No body: only generate a [val x_c : u32] declaration *)
-          let kind = if interface then Declared else Assumed in
-          if !backend = HOL4 then
-            extract_global_decl_hol4_opaque meta ctx fmt decl_name
-              global.generics decl_ty
-          else
-            extract_global_decl_body_gen meta ctx fmt kind decl_name
-              global.generics type_params cg_params trait_clauses decl_ty None
-      | Some body ->
-          (* There is a body *)
-          (* Generate: [let x_body : result u32 = Return 3] *)
-          extract_global_decl_body_gen meta ctx fmt SingleNonRec body_name
-            global.generics type_params cg_params trait_clauses body_ty
-            (Some (fun fmt -> extract_texpression meta ctx fmt false body.body));
-          F.pp_print_break fmt 0 0;
-          (* Generate: [let x_c : u32 = eval_global x_body] *)
-          extract_global_decl_body_gen meta ctx fmt SingleNonRec decl_name
-            global.generics type_params cg_params trait_clauses decl_ty
-            (Some
-               (fun fmt ->
-                 let all_params =
-                   List.concat [ type_params; cg_params; trait_clauses ]
-                 in
-                 let extract_params () =
-                   List.iter
-                     (fun p ->
-                       F.pp_print_space fmt ();
-                       F.pp_print_string fmt p)
-                     all_params
-                 in
-                 let use_brackets = all_params <> [] in
-                 (* Extract the name *)
-                 let before, after =
-                   match !backend with
-                   | FStar | Lean ->
-                       ( (fun () ->
-                           F.pp_print_string fmt "eval_global";
-                           F.pp_print_space fmt ()),
-                         fun () -> () )
-                   | Coq ->
-                       ( (fun () -> ()),
-                         fun () -> F.pp_print_string fmt "%global" )
-                   | HOL4 ->
-                       ( (fun () ->
-                           F.pp_print_string fmt "get_return_value";
-                           F.pp_print_space fmt ()),
-                         fun () -> () )
-                 in
-                 before ();
-                 if use_brackets then F.pp_print_string fmt "(";
-                 F.pp_print_string fmt body_name;
-                 (* Extract the generic params *)
-                 extract_params ();
-                 if use_brackets then F.pp_print_string fmt ")";
-                 (* *)
-                 after ()));
-          (* Add a break to insert lines between declarations *)
-          F.pp_print_break fmt 0 0)
+let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
+    (global : global_decl option) (body : fun_decl) (interface : bool) : unit =
+  match global with
+  | Some global -> extract_global_decl_aux ctx fmt global body interface
   | None -> ()
 
 (** Similar to {!extract_trait_decl_register_names} *)
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index b4c55d80..eac4adb9 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -3865,7 +3865,10 @@ let translate_type_decls (ctx : Contexts.decls_ctx) : type_decl list =
     (fun a ->
       try Some (translate_type_decl ctx a)
       with CFailure (meta, _) ->
-        let () = save_error __FILE__ __LINE__ meta "Could not generate code, see previous error" in
+        let () =
+          save_error __FILE__ __LINE__ meta
+            "Could not generate code, see previous error"
+        in
         None)
     (TypeDeclId.Map.values ctx.type_ctx.type_decls)
 
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 28e5531d..c23b2a47 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_hook (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 =
@@ -201,9 +201,12 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
     pure_fun_translation_no_loops option =
   try
     Some
-      (translate_function_to_pure_hook trans_ctx pure_type_decls fun_dsigs fdef)
+      (translate_function_to_pure_aux trans_ctx pure_type_decls fun_dsigs fdef)
   with CFailure (meta, _) ->
-    let () = save_error __FILE__ __LINE__ meta "Could not generate code, see previous error" in
+    let () =
+      save_error __FILE__ __LINE__ meta
+        "Could not translate function because of previous error"
+    in
     None
 
 (* TODO: factor out the return type *)
@@ -240,7 +243,8 @@ let translate_crate_to_pure (crate : crate) :
                    trans_ctx fdef )
            with CFailure (meta, _) ->
              let () =
-               save_error __FILE__ __LINE__ meta "Could not generate code, see previous error"
+               save_error __FILE__ __LINE__ meta
+                 "Could not translate function because of previous error"
              in
              None)
          (FunDeclId.Map.values crate.fun_decls))
@@ -260,7 +264,8 @@ let translate_crate_to_pure (crate : crate) :
         try Some (SymbolicToPure.translate_trait_decl trans_ctx a)
         with CFailure (meta, _) ->
           let () =
-            save_error __FILE__ __LINE__ meta "Could not generate code, see previous error"
+            save_error __FILE__ __LINE__ meta
+              "Could not translate trait decl because of previous error"
           in
           None)
       (TraitDeclId.Map.values trans_ctx.trait_decls_ctx.trait_decls)
@@ -273,7 +278,8 @@ let translate_crate_to_pure (crate : crate) :
         try Some (SymbolicToPure.translate_trait_impl trans_ctx a)
         with CFailure (meta, _) ->
           let () =
-            save_error __FILE__ __LINE__ meta "Could not generate code, see previous error"
+            save_error __FILE__ __LINE__ meta
+              "Could not translate trait impl because of previous error"
           in
           None)
       (TraitImplId.Map.values trans_ctx.trait_impls_ctx.trait_impls)
@@ -504,7 +510,10 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
     let global =
       try Some (SymbolicToPure.translate_global ctx.trans_ctx global)
       with CFailure (meta, _) ->
-        let () = save_error __FILE__ __LINE__ meta "Could not generate code, see previous error" in
+        let () =
+          save_error __FILE__ __LINE__ meta
+            "Could not translate global because of previous error"
+        in
         None
     in
     Extract.extract_global_decl ctx fmt global body config.interface
-- 
cgit v1.2.3


From 3a470ec6661a494631a12594989126804aeb044d Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Fri, 5 Apr 2024 14:44:17 +0200
Subject: Resolved comments and added the name of the not translated element

---
 compiler/SymbolicToPure.ml |  5 ++++-
 compiler/Translate.ml      | 20 ++++++++++++++------
 2 files changed, 18 insertions(+), 7 deletions(-)

(limited to 'compiler')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index eac4adb9..607da445 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -3865,9 +3865,12 @@ let translate_type_decls (ctx : Contexts.decls_ctx) : type_decl list =
     (fun a ->
       try Some (translate_type_decl ctx a)
       with CFailure (meta, _) ->
+        let env = PrintPure.decls_ctx_to_fmt_env ctx in
+        let name = PrintPure.name_to_string env a.name in
         let () =
           save_error __FILE__ __LINE__ meta
-            "Could not generate code, see previous error"
+            ("Could not translate type decl '" ^ name
+           ^ "' because of previous error")
         in
         None)
     (TypeDeclId.Map.values ctx.type_ctx.type_decls)
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index c23b2a47..2fcf5b43 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -203,9 +203,10 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
     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
     let () =
       save_error __FILE__ __LINE__ meta
-        "Could not translate function because of previous error"
+        ("Could not translate function '" ^ name ^ "' because of previous error")
     in
     None
 
@@ -230,7 +231,6 @@ let translate_crate_to_pure (crate : crate) :
     Pure.TypeDeclId.Map.of_list
       (List.map (fun (def : Pure.type_decl) -> (def.def_id, def)) type_decls)
   in
-
   (* Compute the decomposed fun sigs for the whole crate *)
   let fun_dsigs =
     FunDeclId.Map.of_list
@@ -242,9 +242,11 @@ let translate_crate_to_pure (crate : crate) :
                  SymbolicToPure.translate_fun_sig_from_decl_to_decomposed
                    trans_ctx fdef )
            with CFailure (meta, _) ->
+             let name = name_to_string trans_ctx fdef.name in
              let () =
                save_error __FILE__ __LINE__ meta
-                 "Could not translate function because of previous error"
+                 ("Could not translate function signature '" ^ name
+                ^ "' because of previous error")
              in
              None)
          (FunDeclId.Map.values crate.fun_decls))
@@ -263,9 +265,11 @@ let translate_crate_to_pure (crate : crate) :
       (fun a ->
         try Some (SymbolicToPure.translate_trait_decl trans_ctx a)
         with CFailure (meta, _) ->
+          let name = name_to_string trans_ctx a.name in
           let () =
             save_error __FILE__ __LINE__ meta
-              "Could not translate trait decl because of previous error"
+              ("Could not translate trait decl '" ^ name
+             ^ "' because of previous error")
           in
           None)
       (TraitDeclId.Map.values trans_ctx.trait_decls_ctx.trait_decls)
@@ -277,9 +281,11 @@ let translate_crate_to_pure (crate : crate) :
       (fun a ->
         try Some (SymbolicToPure.translate_trait_impl trans_ctx a)
         with CFailure (meta, _) ->
+          let name = name_to_string trans_ctx a.name in
           let () =
             save_error __FILE__ __LINE__ meta
-              "Could not translate trait impl because of previous error"
+              ("Could not translate trait impl '" ^ name
+             ^ "' because of previous error")
           in
           None)
       (TraitImplId.Map.values trans_ctx.trait_impls_ctx.trait_impls)
@@ -511,8 +517,10 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
       try Some (SymbolicToPure.translate_global ctx.trans_ctx global)
       with CFailure (meta, _) ->
         let () =
+          let name = name_to_string ctx.trans_ctx global.name in
           save_error __FILE__ __LINE__ meta
-            "Could not translate global because of previous error"
+            ("Could not translate global '" ^ name
+           ^ "' because of previous error")
         in
         None
     in
-- 
cgit v1.2.3


From 581d5c0cb8e618382fa41e5a42175560283ff0a1 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 7 Apr 2024 14:27:14 +0200
Subject: Cleanup a bit and improve the error messages

---
 compiler/Extract.ml                |  3 +-
 compiler/InterpreterBorrows.ml     | 26 ++++++--------
 compiler/InterpreterBorrowsCore.ml |  4 +--
 compiler/InterpreterPaths.ml       | 21 ++++++------
 compiler/InterpreterProjectors.ml  |  4 +--
 compiler/Invariants.ml             |  5 ++-
 compiler/Main.ml                   |  4 ++-
 compiler/PrePasses.ml              | 19 +++++++++--
 compiler/Print.ml                  |  1 +
 compiler/PureTypeCheck.ml          |  9 +++--
 compiler/SymbolicToPure.ml         |  8 ++---
 compiler/Translate.ml              | 69 +++++++++++++++++++-------------------
 12 files changed, 91 insertions(+), 82 deletions(-)

(limited to 'compiler')

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index f7d08fdb..985fb470 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -219,7 +219,7 @@ let fun_builtin_filter_types (id : FunDeclId.id) (types : 'a list)
           ^ string_of_int (List.length types)
           ^ " type arguments"
         in
-        log#serror err;
+        save_error __FILE__ __LINE__ None err;
         Result.Error (types, err))
       else
         let types = List.combine filter types in
@@ -1884,6 +1884,7 @@ let extract_global_decl_aux (ctx : extraction_ctx) (fmt : F.formatter)
   let meta = body.meta in
   sanity_check __FILE__ __LINE__ body.is_global_decl_body meta;
   sanity_check __FILE__ __LINE__ (body.signature.inputs = []) meta;
+
   (* Add a break then the name of the corresponding LLBC declaration *)
   F.pp_print_break fmt 0 0;
   let name =
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index e593ae75..a158ed9a 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -303,13 +303,11 @@ let give_back_value (config : config) (meta : Meta.meta) (bid : BorrowId.id)
             if bid' = bid then (
               (* Sanity check *)
               let expected_ty = ty in
-              if nv.ty <> expected_ty then (
-                log#serror
-                  ("give_back_value: improper type:\n- expected: "
-                 ^ ty_to_string ctx ty ^ "\n- received: "
-                 ^ ty_to_string ctx nv.ty);
+              if nv.ty <> expected_ty then
                 craise __FILE__ __LINE__ meta
-                  "Value given back doesn't have the proper type");
+                  ("Value given back doesn't have the proper type:\n\
+                    - expected: " ^ ty_to_string ctx ty ^ "\n- received: "
+                 ^ ty_to_string ctx nv.ty);
               (* Replace *)
               set_replaced ();
               nv.value)
@@ -540,13 +538,11 @@ let give_back_avalue_to_same_abstraction (_config : config) (meta : Meta.meta)
                * see the comment at the level of the definition of
                * {!typed_avalue} *)
               let _, expected_ty, _ = ty_get_ref ty in
-              if nv.ty <> expected_ty then (
-                log#serror
-                  ("give_back_avalue_to_same_abstraction: improper type:\n\
+              if nv.ty <> expected_ty then
+                craise __FILE__ __LINE__ meta
+                  ("Value given back doesn't have the proper type:\n\
                     - expected: " ^ ty_to_string ctx ty ^ "\n- received: "
                  ^ ty_to_string ctx nv.ty);
-                craise __FILE__ __LINE__ meta
-                  "Value given back doesn't have the proper type");
               (* This is the loan we are looking for: apply the projection to
                * the value we give back and replaced this mutable loan with
                * an ended loan *)
@@ -836,26 +832,26 @@ let check_borrow_disappeared (meta : Meta.meta) (fun_name : string)
       match lookup_borrow_opt ek_all l ctx with
       | None -> () (* Ok *)
       | Some _ ->
-          log#lerror
+          log#ltrace
             (lazy
               (fun_name ^ ": " ^ BorrowId.to_string l
              ^ ": borrow didn't disappear:\n- original context:\n"
               ^ eval_ctx_to_string ~meta:(Some meta) ctx0
               ^ "\n\n- new context:\n"
               ^ eval_ctx_to_string ~meta:(Some meta) ctx));
-          craise __FILE__ __LINE__ meta "Borrow not eliminated"
+          internal_error __FILE__ __LINE__ meta
     in
     match lookup_loan_opt meta ek_all l ctx with
     | None -> () (* Ok *)
     | Some _ ->
-        log#lerror
+        log#ltrace
           (lazy
             (fun_name ^ ": " ^ BorrowId.to_string l
            ^ ": loan didn't disappear:\n- original context:\n"
             ^ eval_ctx_to_string ~meta:(Some meta) ctx0
             ^ "\n\n- new context:\n"
             ^ eval_ctx_to_string ~meta:(Some meta) ctx));
-        craise __FILE__ __LINE__ meta "Loan not eliminated"
+        internal_error __FILE__ __LINE__ meta
   in
   unit_to_cm_fun check_disappeared
 
diff --git a/compiler/InterpreterBorrowsCore.ml b/compiler/InterpreterBorrowsCore.ml
index 6e65b11d..a01be046 100644
--- a/compiler/InterpreterBorrowsCore.ml
+++ b/compiler/InterpreterBorrowsCore.ml
@@ -162,11 +162,11 @@ let rec compare_rtys (meta : Meta.meta) (default : bool)
       sanity_check __FILE__ __LINE__ (ty1 = ty2) meta;
       default
   | _ ->
-      log#lerror
+      log#ltrace
         (lazy
           ("compare_rtys: unexpected inputs:" ^ "\n- ty1: " ^ show_ty ty1
          ^ "\n- ty2: " ^ show_ty ty2));
-      craise __FILE__ __LINE__ meta "Unreachable"
+      internal_error __FILE__ __LINE__ meta
 
 (** Check if two different projections intersect. This is necessary when
     giving a symbolic value to an abstraction: we need to check that
diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index f2c0bcb1..ab3daa72 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -83,7 +83,7 @@ let rec access_projection (meta : Meta.meta) (access : projection_access)
       let nv = update v in
       (* Type checking *)
       if nv.ty <> v.ty then (
-        log#lerror
+        log#ltrace
           (lazy
             ("Not the same type:\n- nv.ty: " ^ show_ety nv.ty ^ "\n- v.ty: "
            ^ show_ety v.ty));
@@ -252,8 +252,8 @@ let rec access_projection (meta : Meta.meta) (access : projection_access)
           let pe = "- pe: " ^ show_projection_elem pe in
           let v = "- v:\n" ^ show_value v in
           let ty = "- ty:\n" ^ show_ety ty in
-          log#serror ("Inconsistent projection:\n" ^ pe ^ "\n" ^ v ^ "\n" ^ ty);
-          craise __FILE__ __LINE__ meta "Inconsistent projection")
+          craise __FILE__ __LINE__ meta
+            ("Inconsistent projection:\n" ^ pe ^ "\n" ^ v ^ "\n" ^ ty))
 
 (** Generic function to access (read/write) the value at a given place.
 
@@ -319,14 +319,13 @@ let try_read_place (meta : Meta.meta) (access : access_kind) (p : place)
       (* Note that we ignore the new environment: it should be the same as the
          original one.
       *)
-      if !Config.sanity_checks then
-        if ctx1 <> ctx then (
-          let msg =
-            "Unexpected environment update:\nNew environment:\n"
-            ^ show_env ctx1.env ^ "\n\nOld environment:\n" ^ show_env ctx.env
-          in
-          log#serror msg;
-          craise __FILE__ __LINE__ meta "Unexpected environment update");
+      (if !Config.sanity_checks then
+         if ctx1 <> ctx then
+           let msg =
+             "Unexpected environment update:\nNew environment:\n"
+             ^ show_env ctx1.env ^ "\n\nOld environment:\n" ^ show_env ctx.env
+           in
+           craise __FILE__ __LINE__ meta msg);
       Ok read_value
 
 let read_place (meta : Meta.meta) (access : access_kind) (p : place)
diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml
index 6e86e6a4..3993d845 100644
--- a/compiler/InterpreterProjectors.ml
+++ b/compiler/InterpreterProjectors.ml
@@ -217,12 +217,12 @@ let rec apply_proj_borrows (meta : Meta.meta) (check_symbolic_no_ended : bool)
               meta);
           ASymbolic (AProjBorrows (s, ty))
       | _ ->
-          log#lerror
+          log#ltrace
             (lazy
               ("apply_proj_borrows: unexpected inputs:\n- input value: "
               ^ typed_value_to_string ~meta:(Some meta) ctx v
               ^ "\n- proj rty: " ^ ty_to_string ctx ty));
-          craise __FILE__ __LINE__ meta "Unreachable"
+          internal_error __FILE__ __LINE__ meta
     in
     { value; ty }
 
diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml
index 642d7a37..2ccf3ad4 100644
--- a/compiler/Invariants.ml
+++ b/compiler/Invariants.ml
@@ -185,7 +185,6 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) :
           "find_info: could not find the representant of borrow "
           ^ BorrowId.to_string bid ^ ":\nContext:\n" ^ context_to_string ()
         in
-        log#serror err;
         craise __FILE__ __LINE__ meta err
   in
 
@@ -706,13 +705,13 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit =
             | AEndedProjBorrows _ | AIgnoredProjBorrows -> ())
         | AIgnored, _ -> ()
         | _ ->
-            log#lerror
+            log#ltrace
               (lazy
                 ("Erroneous typing:" ^ "\n- raw value: " ^ show_typed_avalue atv
                ^ "\n- value: "
                 ^ typed_avalue_to_string ~meta:(Some meta) ctx atv
                 ^ "\n- type: " ^ ty_to_string ctx atv.ty));
-            craise __FILE__ __LINE__ meta "Erroneous typing");
+            internal_error __FILE__ __LINE__ meta);
         (* Continue exploring to inspect the subterms *)
         super#visit_typed_avalue info atv
     end
diff --git a/compiler/Main.ml b/compiler/Main.ml
index 416f3a07..6161f2f2 100644
--- a/compiler/Main.ml
+++ b/compiler/Main.ml
@@ -283,7 +283,9 @@ let () =
       if !Errors.error_list <> [] then (
         List.iter
           (fun (meta, msg) -> log#serror (Errors.format_error_message meta msg))
-          !Errors.error_list;
+          (* Reverse the list of error messages so that we print them from the
+             earliest to the latest. *)
+          (List.rev !Errors.error_list);
         exit 1);
 
       (* Print total elapsed time *)
diff --git a/compiler/PrePasses.ml b/compiler/PrePasses.ml
index 0b39f64a..a46ef79c 100644
--- a/compiler/PrePasses.ml
+++ b/compiler/PrePasses.ml
@@ -238,9 +238,9 @@ let remove_loop_breaks (crate : crate) (f : fun_decl) : fun_decl =
       method! visit_Sequence env st1 st2 =
         match st1.content with
         | Loop _ ->
-            sanity_check __FILE__ __LINE__
+            cassert __FILE__ __LINE__
               (statement_has_no_loop_break_continue st2)
-              st2.meta;
+              st2.meta "Sequences of loops are not supported yet";
             (replace_breaks_with st1 st2).content
         | _ -> super#visit_Sequence env st1 st2
     end
@@ -437,9 +437,22 @@ let remove_shallow_borrows (crate : crate) (f : fun_decl) : fun_decl =
 
 let apply_passes (crate : crate) : crate =
   let passes = [ remove_loop_breaks crate; remove_shallow_borrows crate ] in
+  (* Attempt to apply a pass: if it fails we replace the body by [None] *)
+  let apply_pass (pass : fun_decl -> fun_decl) (f : fun_decl) =
+    try pass f
+    with CFailure (_, _) ->
+      (* The error was already registered, we don't need to register it twice.
+         However, we replace the body of the function, and save an error to
+         report to the user the fact that we will ignore the function body *)
+      let fmt = Print.Crate.crate_to_fmt_env crate in
+      let name = Print.name_to_string fmt f.name in
+      save_error __FILE__ __LINE__ (Some f.meta)
+        ("Ignoring the body of '" ^ name ^ "' because of previous error");
+      { f with body = None }
+  in
   let fun_decls =
     List.fold_left
-      (fun fl pass -> FunDeclId.Map.map pass fl)
+      (fun fl pass -> FunDeclId.Map.map (apply_pass pass) fl)
       crate.fun_decls passes
   in
   let crate = { crate with fun_decls } in
diff --git a/compiler/Print.ml b/compiler/Print.ml
index dad1aea3..51286553 100644
--- a/compiler/Print.ml
+++ b/compiler/Print.ml
@@ -1,4 +1,5 @@
 include Charon.PrintUtils
+include Charon.PrintTypes
 include Charon.PrintLlbcAst
 open Charon.PrintTypes
 open Charon.PrintExpressions
diff --git a/compiler/PureTypeCheck.ml b/compiler/PureTypeCheck.ml
index 098e2564..27044c27 100644
--- a/compiler/PureTypeCheck.ml
+++ b/compiler/PureTypeCheck.ml
@@ -93,12 +93,11 @@ let rec check_typed_pattern (meta : Meta.meta) (ctx : tc_ctx)
         get_adt_field_types meta ctx.type_decls type_id av.variant_id generics
       in
       let check_value (ctx : tc_ctx) (ty : ty) (v : typed_pattern) : tc_ctx =
-        if ty <> v.ty then (
+        if ty <> v.ty then
           (* TODO: we need to normalize the types *)
-          log#serror
-            ("check_typed_pattern: not the same types:" ^ "\n- ty: "
-           ^ show_ty ty ^ "\n- v.ty: " ^ show_ty v.ty);
-          craise __FILE__ __LINE__ meta "Inconsistent types");
+          craise __FILE__ __LINE__ meta
+            ("Inconsistent types:" ^ "\n- ty: " ^ show_ty ty ^ "\n- v.ty: "
+           ^ show_ty v.ty);
         check_typed_pattern meta ctx v
       in
       (* Check the field types: check that the field patterns have the expected
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 607da445..93f9ef75 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -3867,11 +3867,9 @@ let translate_type_decls (ctx : Contexts.decls_ctx) : type_decl list =
       with CFailure (meta, _) ->
         let env = PrintPure.decls_ctx_to_fmt_env ctx in
         let name = PrintPure.name_to_string env a.name in
-        let () =
-          save_error __FILE__ __LINE__ meta
-            ("Could not translate type decl '" ^ name
-           ^ "' because of previous error")
-        in
+        save_error __FILE__ __LINE__ meta
+          ("Could not translate type decl '" ^ name
+         ^ "' because of previous error");
         None)
     (TypeDeclId.Map.values ctx.type_ctx.type_decls)
 
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 2fcf5b43..870f8a22 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -204,10 +204,9 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
       (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
-    let () =
-      save_error __FILE__ __LINE__ meta
-        ("Could not translate function '" ^ name ^ "' because of previous error")
-    in
+    save_error __FILE__ __LINE__ meta
+      ("Could not translate the function '" ^ name
+     ^ "' because of previous error");
     None
 
 (* TODO: factor out the return type *)
@@ -231,6 +230,7 @@ let translate_crate_to_pure (crate : crate) :
     Pure.TypeDeclId.Map.of_list
       (List.map (fun (def : Pure.type_decl) -> (def.def_id, def)) type_decls)
   in
+
   (* Compute the decomposed fun sigs for the whole crate *)
   let fun_dsigs =
     FunDeclId.Map.of_list
@@ -243,11 +243,9 @@ let translate_crate_to_pure (crate : crate) :
                    trans_ctx fdef )
            with CFailure (meta, _) ->
              let name = name_to_string trans_ctx fdef.name in
-             let () =
-               save_error __FILE__ __LINE__ meta
-                 ("Could not translate function signature '" ^ name
-                ^ "' because of previous error")
-             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
@@ -266,11 +264,9 @@ let translate_crate_to_pure (crate : crate) :
         try Some (SymbolicToPure.translate_trait_decl trans_ctx a)
         with CFailure (meta, _) ->
           let name = name_to_string trans_ctx a.name in
-          let () =
-            save_error __FILE__ __LINE__ meta
-              ("Could not translate trait decl '" ^ name
-             ^ "' because of previous error")
-          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
@@ -282,11 +278,9 @@ let translate_crate_to_pure (crate : crate) :
         try Some (SymbolicToPure.translate_trait_impl trans_ctx a)
         with CFailure (meta, _) ->
           let name = name_to_string trans_ctx a.name in
-          let () =
-            save_error __FILE__ __LINE__ meta
-              ("Could not translate trait impl '" ^ name
-             ^ "' because of previous error")
-          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
@@ -516,12 +510,10 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
     let global =
       try Some (SymbolicToPure.translate_global ctx.trans_ctx global)
       with CFailure (meta, _) ->
-        let () =
-          let name = name_to_string ctx.trans_ctx global.name in
-          save_error __FILE__ __LINE__ meta
-            ("Could not translate global '" ^ name
-           ^ "' because of previous error")
-        in
+        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
@@ -778,22 +770,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
@@ -951,7 +949,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
-- 
cgit v1.2.3


From a9a2f81e365eeef4fd157fb56cd5107f95c91163 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 7 Apr 2024 14:47:36 +0200
Subject: Improve the error messages further

---
 compiler/Interpreter.ml           | 12 ++++++++++++
 compiler/InterpreterStatements.ml | 13 ++++++++++++-
 compiler/TypesUtils.ml            | 20 ++++++++++++++++++++
 3 files changed, 44 insertions(+), 1 deletion(-)

(limited to 'compiler')

diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index d0a54750..769e3144 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -191,6 +191,18 @@ let initialize_symbolic_context_for_fun (ctx : decls_ctx) (fdef : fun_decl) :
    * do it, and because it gives a bit of sanity.
    * *)
   let sg = fdef.signature in
+  (* Sanity check: no nested borrows, borrows in ADTs, etc. *)
+  cassert __FILE__ __LINE__
+    (List.for_all
+       (fun ty -> not (ty_has_nested_borrows ctx.type_ctx.type_infos ty))
+       (sg.output :: sg.inputs))
+    fdef.meta "Nested borrows are not supported yet";
+  cassert __FILE__ __LINE__
+    (List.for_all
+       (fun ty -> not (ty_has_adt_with_borrows ctx.type_ctx.type_infos ty))
+       (sg.output :: sg.inputs))
+    fdef.meta "ADTs containing borrows are not supported yet";
+
   (* Create the context *)
   let regions_hierarchy =
     FunIdMap.find (FRegular fdef.def_id) ctx.fun_ctx.regions_hierarchies
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 1cf1c5ef..de89f316 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -1365,10 +1365,21 @@ and eval_transparent_function_call_symbolic (config : config) (meta : Meta.meta)
   let func, generics, trait_method_generics, def, regions_hierarchy, inst_sg =
     eval_transparent_function_call_symbolic_inst meta call ctx
   in
-  (* Sanity check *)
+  (* Sanity check: same number of inputs *)
   sanity_check __FILE__ __LINE__
     (List.length call.args = List.length def.signature.inputs)
     def.meta;
+  (* Sanity check: no nested borrows, borrows in ADTs, etc. *)
+  cassert __FILE__ __LINE__
+    (List.for_all
+       (fun ty -> not (ty_has_nested_borrows ctx.type_ctx.type_infos ty))
+       (inst_sg.output :: inst_sg.inputs))
+    meta "Nested borrows are not supported yet";
+  cassert __FILE__ __LINE__
+    (List.for_all
+       (fun ty -> not (ty_has_adt_with_borrows ctx.type_ctx.type_infos ty))
+       (inst_sg.output :: inst_sg.inputs))
+    meta "ADTs containing borrows are not supported yet";
   (* Evaluate the function call *)
   eval_function_call_symbolic_from_inst_sig config def.meta func def.signature
     regions_hierarchy inst_sg generics trait_method_generics call.args call.dest
diff --git a/compiler/TypesUtils.ml b/compiler/TypesUtils.ml
index f5dd7df4..b2c60cc6 100644
--- a/compiler/TypesUtils.ml
+++ b/compiler/TypesUtils.ml
@@ -12,6 +12,26 @@ let ty_has_borrows (infos : TypesAnalysis.type_infos) (ty : ty) : bool =
   let info = TypesAnalysis.analyze_ty infos ty in
   info.TypesAnalysis.contains_borrow
 
+let ty_has_adt_with_borrows (infos : TypesAnalysis.type_infos) (ty : ty) : bool
+    =
+  let visitor =
+    object
+      inherit [_] iter_ty as super
+
+      method! visit_ty env ty =
+        match ty with
+        | TAdt (type_id, _) when type_id <> TTuple ->
+            let info = TypesAnalysis.analyze_ty infos ty in
+            if info.TypesAnalysis.contains_borrow then raise Found
+            else super#visit_ty env ty
+        | _ -> super#visit_ty env ty
+    end
+  in
+  try
+    visitor#visit_ty () ty;
+    false
+  with Found -> true
+
 (** Retuns true if the type contains nested borrows.
 
     Note that we can't simply explore the type and look for regions: sometimes
-- 
cgit v1.2.3


From 143a68b2c43c4302abbbd39c28cac3f9c5f52f4a Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Wed, 10 Apr 2024 16:46:24 +0200
Subject: Trust rustc regarding `Copy` bounds

---
 compiler/InterpreterExpressions.ml | 10 +++++-----
 compiler/Invariants.ml             |  2 +-
 compiler/ValuesUtils.ml            |  2 +-
 3 files changed, 7 insertions(+), 7 deletions(-)

(limited to 'compiler')

diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index 48a1cce6..444e5788 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -146,7 +146,7 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config)
             "Can't copy an assumed value other than Option"
       | TAdt (TAdtId _, _) as ty ->
           sanity_check __FILE__ __LINE__
-            (allow_adt_copy || ty_is_primitively_copyable ty)
+            (allow_adt_copy || ty_is_copyable ty)
             meta
       | TAdt (TTuple, _) -> () (* Ok *)
       | TAdt
@@ -158,7 +158,7 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config)
               trait_refs = [];
             } ) ->
           exec_assert __FILE__ __LINE__
-            (ty_is_primitively_copyable ty)
+            (ty_is_copyable ty)
             meta "The type is not primitively copyable"
       | _ -> exec_raise __FILE__ __LINE__ meta "Unreachable");
       let ctx, fields =
@@ -195,7 +195,7 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config)
        * thus requires calling the proper function. Here, we copy values
        * for very simple types such as integers, shared borrows, etc. *)
       cassert __FILE__ __LINE__
-        (ty_is_primitively_copyable (Substitute.erase_regions sp.sv_ty))
+        (ty_is_copyable (Substitute.erase_regions sp.sv_ty))
         meta "Not primitively copyable";
       (* If the type is copyable, we simply return the current value. Side
        * remark: what is important to look at when copying symbolic values
@@ -529,7 +529,7 @@ let eval_binary_op_concrete_compute (meta : Meta.meta) (binop : binop)
       "The arguments given to the binop don't have the same type";
     (* Equality/inequality check is primitive only for a subset of types *)
     exec_assert __FILE__ __LINE__
-      (ty_is_primitively_copyable v1.ty)
+      (ty_is_copyable v1.ty)
       meta "Type is not primitively copyable";
     let b = v1 = v2 in
     Ok { value = VLiteral (VBool b); ty = TLiteral TBool })
@@ -622,7 +622,7 @@ let eval_binary_op_symbolic (config : config) (meta : Meta.meta) (binop : binop)
         sanity_check __FILE__ __LINE__ (v1.ty = v2.ty) meta;
         (* Equality/inequality check is primitive only for a subset of types *)
         exec_assert __FILE__ __LINE__
-          (ty_is_primitively_copyable v1.ty)
+          (ty_is_copyable v1.ty)
           meta "The type is not primitively copyable";
         TLiteral TBool)
       else
diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml
index 2ccf3ad4..6e448cc4 100644
--- a/compiler/Invariants.ml
+++ b/compiler/Invariants.ml
@@ -827,7 +827,7 @@ let check_symbolic_values (meta : Meta.meta) (ctx : eval_ctx) : unit =
       sanity_check __FILE__ __LINE__ (info.env_count <= 1) meta;
     (* A duplicated symbolic value is necessarily primitively copyable *)
     sanity_check __FILE__ __LINE__
-      (info.env_count <= 1 || ty_is_primitively_copyable info.ty)
+      (info.env_count <= 1 || ty_is_copyable info.ty)
       meta;
 
     sanity_check __FILE__ __LINE__
diff --git a/compiler/ValuesUtils.ml b/compiler/ValuesUtils.ml
index 91010e07..b6ee66f5 100644
--- a/compiler/ValuesUtils.ml
+++ b/compiler/ValuesUtils.ml
@@ -160,7 +160,7 @@ let find_first_primitively_copyable_sv_with_borrows
 
       method! visit_VSymbolic _ sv =
         let ty = sv.sv_ty in
-        if ty_is_primitively_copyable ty && ty_has_borrows type_infos ty then
+        if ty_is_copyable ty && ty_has_borrows type_infos ty then
           raise (FoundSymbolicValue sv)
         else ()
     end
-- 
cgit v1.2.3


From c63284e3f9d7723b24f2d226355747e91ebb06aa Mon Sep 17 00:00:00 2001
From: Son HO
Date: Thu, 11 Apr 2024 10:54:12 +0200
Subject: Update a comment

---
 compiler/Invariants.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'compiler')

diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml
index 6e448cc4..689db0c4 100644
--- a/compiler/Invariants.ml
+++ b/compiler/Invariants.ml
@@ -825,7 +825,7 @@ let check_symbolic_values (meta : Meta.meta) (ctx : eval_ctx) : unit =
      * it must be expanded first *)
     if ty_has_borrows ctx.type_ctx.type_infos info.ty then
       sanity_check __FILE__ __LINE__ (info.env_count <= 1) meta;
-    (* A duplicated symbolic value is necessarily primitively copyable *)
+    (* A duplicated symbolic value is necessarily copyable *)
     sanity_check __FILE__ __LINE__
       (info.env_count <= 1 || ty_is_copyable info.ty)
       meta;
-- 
cgit v1.2.3


From 8894c310cd995f2f1f2abb1ca5232f98aa046274 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 11 Apr 2024 19:05:12 +0200
Subject: Reformat the code

---
 compiler/InterpreterExpressions.ml | 15 ++++++---------
 1 file changed, 6 insertions(+), 9 deletions(-)

(limited to 'compiler')

diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index 444e5788..5f849230 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -157,9 +157,8 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config)
               const_generics = [];
               trait_refs = [];
             } ) ->
-          exec_assert __FILE__ __LINE__
-            (ty_is_copyable ty)
-            meta "The type is not primitively copyable"
+          exec_assert __FILE__ __LINE__ (ty_is_copyable ty) meta
+            "The type is not primitively copyable"
       | _ -> exec_raise __FILE__ __LINE__ meta "Unreachable");
       let ctx, fields =
         List.fold_left_map
@@ -528,9 +527,8 @@ let eval_binary_op_concrete_compute (meta : Meta.meta) (binop : binop)
     exec_assert __FILE__ __LINE__ (v1.ty = v2.ty) meta
       "The arguments given to the binop don't have the same type";
     (* Equality/inequality check is primitive only for a subset of types *)
-    exec_assert __FILE__ __LINE__
-      (ty_is_copyable v1.ty)
-      meta "Type is not primitively copyable";
+    exec_assert __FILE__ __LINE__ (ty_is_copyable v1.ty) meta
+      "Type is not primitively copyable";
     let b = v1 = v2 in
     Ok { value = VLiteral (VBool b); ty = TLiteral TBool })
   else
@@ -621,9 +619,8 @@ let eval_binary_op_symbolic (config : config) (meta : Meta.meta) (binop : binop)
         (* Equality operations *)
         sanity_check __FILE__ __LINE__ (v1.ty = v2.ty) meta;
         (* Equality/inequality check is primitive only for a subset of types *)
-        exec_assert __FILE__ __LINE__
-          (ty_is_copyable v1.ty)
-          meta "The type is not primitively copyable";
+        exec_assert __FILE__ __LINE__ (ty_is_copyable v1.ty) meta
+          "The type is not primitively copyable";
         TLiteral TBool)
       else
         (* Other operations: input types are integers *)
-- 
cgit v1.2.3


From 46567dcdab21b85d20a317a37265b037f36ad737 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 11 Apr 2024 20:08:40 +0200
Subject: Update a comment

---
 compiler/SymbolicToPure.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'compiler')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index cf03fddf..15b52237 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -282,8 +282,8 @@ type bs_ctx = {
   mk_panic : texpression option;
       (** Small helper: translate a [fail] expression.
 
-      We initialize this at [None].
-  *)
+           We initialize this at [None].
+       *)
 }
 [@@deriving show]
 
-- 
cgit v1.2.3