diff options
author | Son Ho | 2022-02-08 17:51:04 +0100 |
---|---|---|
committer | Son Ho | 2022-02-08 17:51:04 +0100 |
commit | 1e6f3fb7d8ac8e72ca38f08d7e4be5c835e3443a (patch) | |
tree | 5959874115481303a6f662ec4c1244307f1ee089 /src/ExtractToFStar.ml | |
parent | b583d18a8336b137b445cc01b713767f354168f4 (diff) |
Make progress on implementing support for types and functions like
Option and Vec
Diffstat (limited to '')
-rw-r--r-- | src/ExtractToFStar.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index 636c68d3..db09b316 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -284,6 +284,8 @@ let mk_formatter (ctx : trans_ctx) (variant_concatenate_type_name : bool) : (* The "pair" case is frequent enough to have its special treatment *) if List.length tys = 2 then "p" else "t" | Assumed Result -> "r" + | Assumed Option -> "opt" + | Assumed Vec -> "v" | AdtId adt_id -> let def = TypeDefId.Map.find adt_id ctx.type_context.type_defs @@ -719,7 +721,7 @@ let extract_place (ctx : extraction_ctx) (fmt : F.formatter) (p : place) : unit let def_id = match pe.pkind with | E.ProjAdt (def_id, None) -> def_id - | E.ProjAdt (_, Some _) | E.ProjTuple _ -> + | E.ProjAdt (_, Some _) | E.ProjOption _ | E.ProjTuple _ -> (* We can't have field accesses on enumerations (variables for * the fields are introduced upon the moment we match over the * enumeration). We also forbid field access on tuples, because |