diff options
| -rw-r--r-- | compiler/Extract.ml | 8 | ||||
| -rw-r--r-- | compiler/ExtractBase.ml | 6 | ||||
| -rw-r--r-- | compiler/Translate.ml | 4 |
3 files changed, 9 insertions, 9 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 5c0a08ad..204fee04 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -2326,7 +2326,7 @@ let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx) (** Compute the names for all the pure functions generated from a rust function (forward function and backward functions). *) -let extract_fun_decl_register_names (ctx : extraction_ctx) (keep_fwd : bool) +let extract_fun_decl_register_names (ctx : extraction_ctx) (has_decreases_clause : fun_decl -> bool) (def : pure_fun_translation) : extraction_ctx = let { f = fwd; loops = loop_fwds } = def.fwd in @@ -2344,7 +2344,7 @@ let extract_fun_decl_register_names (ctx : extraction_ctx) (keep_fwd : bool) else ctx in let ctx = List.fold_left register_decreases ctx (fwd :: loop_fwds) in - let register_fun ctx f = ctx_add_fun_decl (keep_fwd, def) f ctx in + let register_fun ctx f = ctx_add_fun_decl def f ctx in let register_funs ctx fl = List.fold_left register_fun ctx fl in (* Register the forward functions' names *) let ctx = register_funs ctx (fwd :: loop_fwds) in @@ -3971,7 +3971,9 @@ let extract_trait_decl_register_names (ctx : extraction_ctx) (* TODO: for the methods, we need to add fields for the forward/backward functions *) raise (Failure "TODO"); List.fold_left - (fun ctx (name, id) -> ctx_add_trait_method trait_decl name ctx) + (fun ctx (name, id) -> + (* We add one field per required forward/backward function *) + ctx_add_trait_method trait_decl name ctx) ctx required_methods (** Similar to {!extract_type_decl_register_names} *) diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index 885467c2..17f5b693 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -1185,8 +1185,8 @@ let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) : let ctx = ctx_add is_opaque body (name ^ "_body") ctx in ctx -let ctx_add_fun_decl (trans_group : bool * pure_fun_translation) - (def : fun_decl) (ctx : extraction_ctx) : extraction_ctx = +let ctx_add_fun_decl (trans_group : pure_fun_translation) (def : fun_decl) + (ctx : extraction_ctx) : extraction_ctx = (* Sanity check: the function should not be a global body - those are handled * separately *) assert (not def.is_global_decl_body); @@ -1197,7 +1197,7 @@ let ctx_add_fun_decl (trans_group : bool * pure_fun_translation) in let sg = llbc_def.signature in let num_rgs = List.length sg.regions_hierarchy in - let keep_fwd, { fwd = _; backs } = trans_group in + let { keep_fwd; fwd = _; backs } = trans_group in let num_backs = List.length backs in let rg_info = match def.back_id with diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 835edd46..a4041751 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -1084,9 +1084,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : * those are handled later *) let is_global = fwd_def.Pure.is_global_decl_body in if is_global then ctx - else - Extract.extract_fun_decl_register_names ctx trans.keep_fwd - gen_decr_clause trans) + else Extract.extract_fun_decl_register_names ctx gen_decr_clause trans) ctx (A.FunDeclId.Map.values trans_funs) in |