From 999f48d032107722aa6ca714da828ab2788ca412 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 18 Dec 2023 12:06:07 +0100
Subject: Fix a minor mistake in SymbolicToPure

---
 compiler/PrintPure.ml       | 12 +++++++-----
 compiler/PureMicroPasses.ml |  9 +++++++--
 compiler/SymbolicToPure.ml  |  5 +----
 3 files changed, 15 insertions(+), 11 deletions(-)

(limited to 'compiler')

diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml
index 79506c04..1ce146a4 100644
--- a/compiler/PrintPure.ml
+++ b/compiler/PrintPure.ml
@@ -103,10 +103,13 @@ let adt_field_names (env : fmt_env) =
   Print.Types.adt_field_names (fmt_env_to_llbc_fmt_env env)
 
 let option_to_string = Print.option_to_string
-let type_var_to_string = Print.Types.type_var_to_string
-let const_generic_var_to_string = Print.Types.const_generic_var_to_string
-let integer_type_to_string = Print.Values.integer_type_to_string
 let literal_type_to_string = Print.Values.literal_type_to_string
+let type_var_to_string (v : type_var) = "(" ^ v.name ^ ": Type)"
+
+let const_generic_var_to_string (v : const_generic_var) =
+  "(" ^ v.name ^ " : " ^ literal_type_to_string v.ty ^ ")"
+
+let integer_type_to_string = Print.Values.integer_type_to_string
 let scalar_value_to_string = Print.Values.scalar_value_to_string
 let literal_to_string = Print.Values.literal_to_string
 
@@ -203,13 +206,12 @@ and trait_instance_id_to_string (env : fmt_env) (inside : bool)
   | UnknownTrait msg -> "UNKNOWN(" ^ msg ^ ")"
 
 let trait_clause_to_string (env : fmt_env) (clause : trait_clause) : string =
-  let clause_id = trait_clause_id_to_string env clause.clause_id in
   let trait_id = trait_decl_id_to_string env clause.trait_id in
   let generics = generic_args_to_strings env true clause.generics in
   let generics =
     if generics = [] then "" else " " ^ String.concat " " generics
   in
-  "[" ^ clause_id ^ "]: " ^ trait_id ^ generics
+  trait_id ^ generics
 
 let generic_params_to_strings (env : fmt_env) (generics : generic_params) :
     string list =
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index a7c2f154..34597d32 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -11,6 +11,10 @@ let fun_decl_to_string (ctx : trans_ctx) (def : Pure.fun_decl) : string =
   let fmt = trans_ctx_to_pure_fmt_env ctx in
   PrintPure.fun_decl_to_string fmt def
 
+let fun_sig_to_string (ctx : trans_ctx) (sg : Pure.fun_sig) : string =
+  let fmt = trans_ctx_to_pure_fmt_env ctx in
+  PrintPure.fun_sig_to_string fmt sg
+
 (** Small utility.
 
     We sometimes have to insert new fresh variables in a function body, in which
@@ -1303,7 +1307,8 @@ let filter_if_backward_with_no_outputs (def : fun_decl) : fun_decl option =
     those function bodies into independent definitions while removing
     occurrences of the {!Pure.Loop} node.
  *)
-let decompose_loops (def : fun_decl) : fun_decl * fun_decl list =
+let decompose_loops (_ctx : trans_ctx) (def : fun_decl) :
+    fun_decl * fun_decl list =
   match def.body with
   | None -> (def, [])
   | Some body ->
@@ -1982,7 +1987,7 @@ let apply_passes_to_def (ctx : trans_ctx) (def : fun_decl) :
         (lazy ("not filtered (not backward with no outputs): " ^ name ^ "\n"));
 
       (* Extract the loop definitions by removing the {!Loop} node *)
-      let def, loops = decompose_loops def in
+      let def, loops = decompose_loops ctx def in
 
       (* Apply the remaining passes *)
       let f = apply_end_passes_to_def ctx def in
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index a79340b6..7359f68a 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -950,7 +950,7 @@ let translate_fun_sig_to_decomposed (decls_ctx : C.decls_ctx)
   let fwd_info =
     (* *)
     let has_fuel = fwd_fuel <> [] in
-    let num_inputs_no_fuel_no_state = List.length fwd_inputs in
+    let num_inputs_no_fuel_no_state = List.length fwd_inputs_no_fuel_no_state in
     let num_inputs_with_fuel_no_state =
       (* We use the fact that [fuel] has length 1 if we use some fuel, 0 otherwise *)
       List.length fwd_fuel + num_inputs_no_fuel_no_state
@@ -2620,9 +2620,6 @@ and translate_forward_end (ectx : C.eval_ctx)
     (loop_input_values : V.typed_value S.symbolic_value_id_map option)
     (fwd_e : S.expression) (back_e : S.expression S.region_group_id_map)
     (ctx : bs_ctx) : texpression =
-  (* TODO: *)
-  assert (not !Config.return_back_funs);
-
   let translate_one_end ctx (bid : RegionGroupId.id option) =
     let ctx = { ctx with bid } in
     (* Update the current state with the additional state received by the backward
-- 
cgit v1.2.3