diff options
Diffstat (limited to 'compiler/Translate.ml')
| -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 ]) |