diff options
author | Son Ho | 2022-02-08 18:14:13 +0100 |
---|---|---|
committer | Son Ho | 2022-02-08 18:14:13 +0100 |
commit | ef59256fb354edb9d6ffee81bb3f9e82648a6d5a (patch) | |
tree | d88bbfbfdfcd719e92c27ca19c690c916f77d3e2 /src/ExtractToFStar.ml | |
parent | 1e6f3fb7d8ac8e72ca38f08d7e4be5c835e3443a (diff) |
Fix some issues
Diffstat (limited to '')
-rw-r--r-- | src/ExtractToFStar.ml | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index db09b316..aecd6c68 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -95,7 +95,7 @@ let fstar_keywords = List.concat [ named_unops; named_binops; misc ] let fstar_assumed_adts : (assumed_ty * string) list = - [ (Result, "result"); (Option, "option") ] + [ (Result, "result"); (Option, "option"); (Vec, "vec") ] let fstar_assumed_structs : (assumed_ty * string) list = [] @@ -397,7 +397,13 @@ let extract_type_def_register_names (ctx : extraction_ctx) (def : type_def) : let ctx = match def.kind with | Struct fields -> - fst (ctx_add_fields def (FieldId.mapi (fun id f -> (id, f)) fields) ctx) + (* Add the fields *) + let ctx = + fst + (ctx_add_fields def (FieldId.mapi (fun id f -> (id, f)) fields) ctx) + in + (* Add the constructor name *) + fst (ctx_add_struct def ctx) | Enum variants -> fst (ctx_add_variants def |