diff options
| -rw-r--r-- | src/PureToExtract.ml | 7 | ||||
| -rw-r--r-- | src/Translate.ml | 11 |
2 files changed, 12 insertions, 6 deletions
diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml index 255d4e1b..07a1732c 100644 --- a/src/PureToExtract.ml +++ b/src/PureToExtract.ml @@ -585,6 +585,9 @@ let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) : let ctx_add_fun_decl (trans_group : bool * 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); (* Lookup the LLBC def to compute the region group information *) let def_id = def.def_id in let llbc_def = @@ -613,9 +616,7 @@ let ctx_add_fun_decl (trans_group : bool * pure_fun_translation) let name = ctx.fmt.fun_name def_id def.basename num_rgs rg_info (keep_fwd, num_backs) in - (* Add the function name if it's not a global *) - if def.is_global_decl_body then ctx - else ctx_add (FunId (def_id, def.back_id)) name ctx + ctx_add (FunId (def_id, def.back_id)) name ctx type names_map_init = { keywords : string list; diff --git a/src/Translate.ml b/src/Translate.ml index c9dc7943..61300ed8 100644 --- a/src/Translate.ml +++ b/src/Translate.ml @@ -670,12 +670,17 @@ let translate_module (filename : string) (dest_dir : string) (config : config) let ctx = List.fold_left (fun ctx (keep_fwd, def) -> - (* Note that we generate a decrease clause for all the recursive functions *) + (* We generate a decrease clause for all the recursive functions *) let gen_decr_clause = A.FunDeclId.Set.mem (fst def).Pure.def_id rec_functions in - ExtractToFStar.extract_fun_decl_register_names ctx keep_fwd - gen_decr_clause def) + (* Register the names, only if the function is not a global body - + * those are handled later *) + let is_global = (fst def).Pure.is_global_decl_body in + if is_global then ctx + else + ExtractToFStar.extract_fun_decl_register_names ctx keep_fwd + gen_decr_clause def) ctx trans_funs in |