diff options
| -rw-r--r-- | src/ExtractToFStar.ml | 34 | ||||
| -rw-r--r-- | src/Translate.ml | 2 |
2 files changed, 21 insertions, 15 deletions
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index 2389d444..68d934d8 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -13,7 +13,11 @@ module F = Format Controls whether we should use `type ...` or `and ...` (for mutually recursive datatypes). *) -type type_decl_qualif = Type | And | AssumeType +type type_decl_qualif = + | Type (** `type t = ...` *) + | And (** `type t0 = ... and t1 = ...` *) + | AssumeType (** `assume type t` *) + | TypeVal (** In an fsti: `val t : Type0` *) (** A qualifier for function definitions. @@ -642,16 +646,12 @@ let extract_type_decl (ctx : extraction_ctx) (fmt : F.formatter) (* Open a box for "type TYPE_NAME (TYPE_PARAMS) =" *) F.pp_open_hovbox fmt ctx.indent_incr; (* > "type TYPE_NAME" *) - let is_opaque = - match def.kind with Struct _ | Enum _ -> false | Opaque -> true - in - let qualif = + let extract_body, qualif = match qualif with - | Type -> "type" - | And -> "and" - | AssumeType -> - assert is_opaque; - "assume type" + | Type -> (true, "type") + | And -> (true, "and") + | AssumeType -> (false, "assume type") + | TypeVal -> (false, "val") in F.pp_print_string fmt (qualif ^ " " ^ def_name); (* Print the type parameters *) @@ -667,13 +667,19 @@ let extract_type_decl (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_string fmt ":"; F.pp_print_space fmt (); F.pp_print_string fmt "Type0)"); - (* Print the "=" *) - if not is_opaque then ( + (* Print the "=" if we extract the body*) + if extract_body then ( F.pp_print_space fmt (); - F.pp_print_string fmt "="); + F.pp_print_string fmt "=") + else ( + (* Otherwise print ": Type0" *) + F.pp_print_space fmt (); + F.pp_print_string fmt ":"; + F.pp_print_space fmt (); + F.pp_print_string fmt "Type0"); (* Close the box for "type TYPE_NAME (TYPE_PARAMS) =" *) F.pp_close_box fmt (); - (if not is_opaque then + (if extract_body then match def.kind with | Struct fields -> extract_type_decl_struct_body ctx_body fmt def fields | Enum variants -> diff --git a/src/Translate.ml b/src/Translate.ml index a440cacd..76f8aa44 100644 --- a/src/Translate.ml +++ b/src/Translate.ml @@ -398,7 +398,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config) | Enum _ | Struct _ -> (false, qualif) | Opaque -> let qualif = - if config.interface then ExtractToFStar.Type + if config.interface then ExtractToFStar.TypeVal else ExtractToFStar.AssumeType in (true, qualif) |