diff options
author | Son Ho | 2023-03-07 12:00:40 +0100 |
---|---|---|
committer | Son HO | 2023-06-04 21:44:33 +0200 |
commit | 40a08afb20dd9bb36069407e3db37a03a8be0981 (patch) | |
tree | 3603dc14edc7dc909c88d2591718915ac146d0d3 /compiler/Translate.ml | |
parent | 13174c0e585181308a947f5b354c4f1393d91f14 (diff) |
Handle the "opaque_defs." prefix in a cleaner manner
Diffstat (limited to '')
-rw-r--r-- | compiler/Translate.ml | 25 |
1 files changed, 23 insertions, 2 deletions
diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 139f8891..7ee86b28 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -350,7 +350,14 @@ type gen_config = { extract_transparent : bool; (** If [true], extract the transparent declarations, otherwise ignore. *) extract_opaque : bool; - (** If [true], extract the opaque declarations, otherwise ignore. *) + (** If [true], extract the opaque declarations, otherwise ignore. + + For now, this controls only the opaque *functions*, not the opaque + globals or types. + TODO: update this. This is not trivial if we want to extract the opaque + types in an opaque module, because some non-opaque types may refer + to opaque types and vice-versa. + *) extract_state_type : bool; (** If [true], generate a definition/declaration for the state type *) extract_globals : bool; @@ -787,7 +794,15 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) : mk_formatter_and_names_map trans_ctx crate.name variant_concatenate_type_name in - let ctx = { ExtractBase.trans_ctx; names_map; fmt; indent_incr = 2 } in + let ctx = + { + ExtractBase.trans_ctx; + names_map; + fmt; + indent_incr = 2; + use_opaque_pre = !Config.split_files; + } + in (* We need to compute which functions are recursive, in order to know * whether we should generate a decrease clause or not. *) @@ -1035,6 +1050,12 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) : interface = true; } in + let gen_ctx = + { + gen_ctx with + extract_ctx = { gen_ctx.extract_ctx with use_opaque_pre = false }; + } + in extract_file opaque_config gen_ctx opaque_filename crate.A.name opaque_module ": opaque function definitions" [] [ types_module ]; [ opaque_module ]) |