From 284a6042ca9d5d7bcbc19a10909156769443c9be Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 23 Feb 2022 22:17:20 +0100
Subject: Add the `State` assumed type in Pure.ml

---
 src/ExtractToFStar.ml | 15 +++++++++++----
 1 file changed, 11 insertions(+), 4 deletions(-)

(limited to 'src/ExtractToFStar.ml')

diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index 02005f2b..3840ea1e 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -302,6 +302,7 @@ let mk_formatter (ctx : trans_ctx) (variant_concatenate_type_name : bool) :
             | Assumed Result -> "r"
             | Assumed Option -> "opt"
             | Assumed Vec -> "v"
+            | Assumed State -> "st"
             | AdtId adt_id ->
                 let def =
                   TypeDefId.Map.find adt_id ctx.type_context.type_defs
@@ -317,15 +318,13 @@ let mk_formatter (ctx : trans_ctx) (variant_concatenate_type_name : bool) :
                 let cl = List.filter (fun s -> String.length s > 0) cl in
                 assert (List.length cl > 0);
                 let cl = List.map (fun s -> s.[0]) cl in
-                StringUtils.string_of_chars cl
-                (* let c = (get_type_name def.name).[0] in
-                   let c = StringUtils.lowercase_ascii c in
-                     String.make 1 c *))
+                StringUtils.string_of_chars cl)
         | TypeVar _ -> "x" (* lacking imagination here... *)
         | Bool -> "b"
         | Char -> "c"
         | Integer _ -> "i"
         | Str -> "s"
+        | Arrow _ -> "f"
         | Array _ | Slice _ -> raise Unimplemented)
   in
   let type_var_basename (_varset : StringSet.t) (basename : string) : string =
@@ -406,6 +405,14 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
   | Char -> F.pp_print_string fmt ctx.fmt.char_name
   | Integer int_ty -> F.pp_print_string fmt (ctx.fmt.int_name int_ty)
   | Str -> F.pp_print_string fmt ctx.fmt.str_name
+  | Arrow (arg_ty, ret_ty) ->
+      if inside then F.pp_print_string fmt "(";
+      extract_ty ctx fmt false arg_ty;
+      F.pp_print_space fmt ();
+      F.pp_print_string fmt "->";
+      F.pp_print_space fmt ();
+      extract_ty ctx fmt false ret_ty;
+      if inside then F.pp_print_string fmt ")"
   | Array _ | Slice _ -> raise Unimplemented
 
 (** Compute the names for all the top-level identifiers used in a type
-- 
cgit v1.2.3