diff options
Diffstat (limited to 'src/ExtractToFStar.ml')
| -rw-r--r-- | src/ExtractToFStar.ml | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index 8bf02bd0..1d144a40 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -13,13 +13,14 @@ module F = Format Controls whether we should use `type ...` or `and ...` (for mutually recursive datatypes). *) -type type_decl_qualif = Type | And +type type_decl_qualif = Type | And | AssumeType (** A qualifier for function definitions. - Controls whether we should use `let ...`, `let rec ...` or `and ...` + Controls whether we should use `let ...`, `let rec ...` or `and ...`, + or only generate a declaration with `val` or `assume val` *) -type fun_decl_qualif = Let | LetRec | And +type fun_decl_qualif = Let | LetRec | And | Val | AssumeVal (** Small helper to compute the name of an int type *) let fstar_int_name (int_ty : integer_type) = @@ -448,6 +449,9 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) : (ctx_add_variants def (VariantId.mapi (fun id v -> (id, v)) variants) ctx) + | Opaque -> + (* Nothing to do *) + ctx in (* Return *) ctx |