From 3e9083a10b0dc8caf6cebcd89aba27ec7d0a1dac Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 3 Mar 2022 13:02:00 +0100
Subject: Make good progress updating Translate

---
 src/ExtractToFStar.ml | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

(limited to 'src/ExtractToFStar.ml')

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
-- 
cgit v1.2.3