diff options
author | Son Ho | 2023-12-18 12:06:07 +0100 |
---|---|---|
committer | Son Ho | 2023-12-18 12:06:07 +0100 |
commit | 999f48d032107722aa6ca714da828ab2788ca412 (patch) | |
tree | 2d68732fcd506ed7181423186c72da0c31d9e88b | |
parent | 17973e99e4784ff5e31565622d183ad89e3d9cd7 (diff) |
Fix a minor mistake in SymbolicToPure
-rw-r--r-- | compiler/PrintPure.ml | 12 | ||||
-rw-r--r-- | compiler/PureMicroPasses.ml | 9 | ||||
-rw-r--r-- | compiler/SymbolicToPure.ml | 5 |
3 files changed, 15 insertions, 11 deletions
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 |