diff options
Diffstat (limited to 'compiler/SymbolicToPure.ml')
| -rw-r--r-- | compiler/SymbolicToPure.ml | 13 |
1 files changed, 2 insertions, 11 deletions
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 |