diff options
author | Son Ho | 2022-09-22 18:24:40 +0200 |
---|---|---|
committer | Son Ho | 2022-09-22 18:24:40 +0200 |
commit | 65b7bcbb95d39e680cd7c579dd969dff9195eb5a (patch) | |
tree | aa24d3af9170b4c582cf3c1e81e324418e3b39d6 /src/Translate.ml | |
parent | 2b79c533d98f1bec8d332f660b36a05152b4c7dc (diff) |
Update the name registration for globals
Diffstat (limited to '')
-rw-r--r-- | src/Translate.ml | 11 |
1 files changed, 8 insertions, 3 deletions
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 |