diff options
| author | Escherichia | 2024-03-22 15:59:22 +0100 |
|---|---|---|
| committer | Escherichia | 2024-03-28 15:25:52 +0100 |
| commit | 76fda6b5d205a4422c2360b676227690714c9ac5 (patch) | |
| tree | 3e1a69d896afd9ff2277c83d9d8926d3864ff882 /compiler/SymbolicToPure.ml | |
| parent | 5209cea7012cfa3b39a5a289e65e2ea5e166d730 (diff) | |
Still need to fill the TODO: error message and check some meta but it builds
Diffstat (limited to 'compiler/SymbolicToPure.ml')
| -rw-r--r-- | compiler/SymbolicToPure.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 6e3a537e..63605b9c 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -878,7 +878,7 @@ let mk_fuel_input_as_list (ctx : bs_ctx) (info : fun_effect_info) : if function_uses_fuel info then [ mk_fuel_texpression ctx.fuel ] else [] (** Small utility. *) -let compute_raw_fun_effect_info (* (meta : Meta.meta) *) (fun_infos : fun_info A.FunDeclId.Map.t) +let compute_raw_fun_effect_info (meta : Meta.meta) (fun_infos : fun_info A.FunDeclId.Map.t) (fun_id : A.fun_id_or_trait_method_ref) (lid : V.LoopId.id option) (gid : T.RegionGroupId.id option) : fun_effect_info = match fun_id with @@ -896,7 +896,7 @@ let compute_raw_fun_effect_info (* (meta : Meta.meta) *) (fun_infos : fun_info A is_rec = info.is_rec || Option.is_some lid; } | FunId (FAssumed aid) -> - assert (lid = None) (* meta "TODO: error message" *); + cassert (lid = None) meta "TODO: error message"; { can_fail = Assumed.assumed_fun_can_fail aid; stateful_group = false; @@ -921,7 +921,7 @@ let get_fun_effect_info (ctx : bs_ctx) (fun_id : A.fun_id_or_trait_method_ref) in { info with is_rec = info.is_rec || Option.is_some lid } | FunId (FAssumed _) -> - compute_raw_fun_effect_info (* ctx.fun_decl.meta *) ctx.fun_ctx.fun_infos fun_id lid gid) + compute_raw_fun_effect_info ctx.fun_decl.meta ctx.fun_ctx.fun_infos fun_id lid gid) | Some lid -> ( (* This is necessarily for the current function *) match fun_id with @@ -981,7 +981,7 @@ let translate_fun_sig_with_regions_hierarchy_to_decomposed (meta : Meta.meta) (* Is the forward function stateful, and can it fail? *) let fwd_effect_info = - compute_raw_fun_effect_info fun_infos fun_id None None + compute_raw_fun_effect_info meta fun_infos fun_id None None in (* Compute the forward inputs *) let fwd_fuel = mk_fuel_input_ty_as_list fwd_effect_info in @@ -1099,7 +1099,7 @@ let translate_fun_sig_with_regions_hierarchy_to_decomposed (meta : Meta.meta) RegionGroupId.id * back_sg_info = let gid = rg.id in let back_effect_info = - compute_raw_fun_effect_info fun_infos fun_id None (Some gid) + compute_raw_fun_effect_info meta fun_infos fun_id None (Some gid) in let inputs_no_state = translate_back_inputs_for_gid gid in let inputs_no_state = |