From fe2a2cb34148e46e32cdcfbf100e38d9986082cd Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 8 Mar 2024 16:06:35 +0100
Subject: Make progress on propagating the changes

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

(limited to 'compiler/SymbolicToPure.ml')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 859d6f17..2db5f66c 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -2035,7 +2035,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
     | S.Fun (fid, call_id) ->
         (* Regular function call *)
         let fid_t = translate_fun_id_or_trait_method_ref ctx fid in
-        let func = Fun (FromLlbc (fid_t, None, None)) in
+        let func = Fun (FromLlbc (fid_t, None)) in
         (* Retrieve the effect information about this function (can fail,
          * takes a state as input, etc.) *)
         let effect_info = get_fun_effect_info ctx fid None None in
@@ -2539,8 +2539,6 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs)
         get_fun_effect_info ctx (FunId fun_id) (Some vloop_id) (Some rg_id)
       in
       let loop_info = LoopId.Map.find loop_id ctx.loops in
-      let generics = loop_info.generics in
-      let fwd_inputs = Option.get loop_info.forward_inputs in
       (* Retrieve the additional backward inputs. Note that those are actually
          the backward inputs of the function we are synthesizing (and that we
          need to *transmit* to the loop backward function): they are not the
@@ -2582,10 +2580,6 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs)
           (fun (arg, mp) -> mk_opt_mplace_texpression mp arg)
           (List.combine inputs args_mplaces)
       in
-      let input_tys = (List.map (fun (x : texpression) -> x.ty)) args in
-      let ret_ty =
-        if effect_info.can_fail then mk_result_ty output.ty else output.ty
-      in
       (* Create the expression for the function:
          - it is either a call to a top-level function, if we split the
            forward/backward functions
@@ -3218,7 +3212,7 @@ and translate_forward_end (ectx : C.eval_ctx)
       let out_pat = mk_simpl_tuple_pattern out_pats in
 
       let loop_call =
-        let fun_id = Fun (FromLlbc (FunId fid, Some loop_id, None)) in
+        let fun_id = Fun (FromLlbc (FunId fid, Some loop_id)) in
         let func = { id = FunOrOp fun_id; generics = loop_info.generics } in
         let input_tys = (List.map (fun (x : texpression) -> x.ty)) args in
         let ret_ty =
@@ -3567,9 +3561,6 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
   let name = name_to_string ctx llbc_name in
   (* Translate the signature *)
   let signature = translate_fun_sig_from_decomposed ctx.sg in
-  let regions_hierarchy =
-    FunIdMap.find (FRegular def_id) ctx.fun_ctx.regions_hierarchies
-  in
   (* Translate the body, if there is *)
   let body =
     match body with
-- 
cgit v1.2.3