Add an Opaque variant to type_decl_kind and start updating the code

11 files changed, 60 insertions, 35 deletions

diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml
index 979ed780..0b65a372 100644
--- a/src/InterpreterExpansion.ml
+++ b/src/InterpreterExpansion.ml
@@ -686,7 +686,9 @@ let greedy_expand_symbolics_with_borrows (config : C.config) : cm_fun =
                      ("Attempted to greedily expand a symbolic enumeration \
                        with > 1 variants (option \
                        [greedy_expand_symbolics_with_borrows] of [config]): "
-                     ^ Print.name_to_string def.name)));
+                     ^ Print.name_to_string def.name))
+            | T.Opaque ->
+                raise (Failure "Attempted to greedily expand an opaque type"));
             (* Also, we need to check if the definition is recursive *)
             if C.ctx_type_decl_is_rec ctx def_id then
               raise
diff --git a/src/Print.ml b/src/Print.ml
index e03efd94..c3c80da0 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -172,6 +172,7 @@ module Types = struct
         in
         let variants = String.concat "\n" variants in
         "enum " ^ name ^ params ^ " =\n" ^ variants
+    | T.Opaque -> "opaque type " ^ name ^ params
 end
 
 module PT = Types (* local module *)
@@ -573,7 +574,7 @@ module Contexts = struct
    fun def_id variant_id ->
     let def = T.TypeDeclId.Map.find def_id ctx in
     match def.kind with
-    | Struct _ -> failwith "Unreachable"
+    | Struct _ | Opaque -> failwith "Unreachable"
     | Enum variants ->
         let variant = T.VariantId.nth variants variant_id in
         name_to_string def.name ^ "::" ^ variant.variant_name
diff --git a/src/PrintPure.ml b/src/PrintPure.ml
index e96edeed..65b151a3 100644
--- a/src/PrintPure.ml
+++ b/src/PrintPure.ml
@@ -189,6 +189,7 @@ let type_decl_to_string (fmt : type_formatter) (def : type_decl) : string =
       in
       let variants = String.concat "\n" variants in
       "enum " ^ name ^ params ^ " =\n" ^ variants
+  | Opaque -> "opaque type " ^ name ^ params
 
 let var_to_string (fmt : type_formatter) (v : var) : string =
   let varname =
diff --git a/src/Pure.ml b/src/Pure.ml
index bbbf72a6..422292b1 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -116,7 +116,7 @@ type field = { field_name : string option; field_ty : ty } [@@deriving show]
 
 type variant = { variant_name : string; fields : field list } [@@deriving show]
 
-type type_decl_kind = Struct of field list | Enum of variant list
+type type_decl_kind = Struct of field list | Enum of variant list | Opaque
 [@@deriving show]
 
 type type_var = T.type_var [@@deriving show]
diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml
index 4db5d2c5..2a00577e 100644
--- a/src/PureToExtract.ml
+++ b/src/PureToExtract.ml
@@ -392,7 +392,7 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
         | AdtId id -> (
             let def = TypeDeclId.Map.find id type_decls in
             match def.kind with
-            | Struct _ -> failwith "Unreachable"
+            | Struct _ | Opaque -> failwith "Unreachable"
             | Enum variants ->
                 let variant = VariantId.nth variants variant_id in
                 Print.name_to_string def.name ^ "::" ^ variant.variant_name)
@@ -409,7 +409,7 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
         | AdtId id -> (
             let def = TypeDeclId.Map.find id type_decls in
             match def.kind with
-            | Enum _ -> failwith "Unreachable"
+            | Enum _ | Opaque -> failwith "Unreachable"
             | Struct fields ->
                 let field = FieldId.nth fields field_id in
                 let field_name =
diff --git a/src/PureUtils.ml b/src/PureUtils.ml
index aa8d1f53..cfc8a270 100644
--- a/src/PureUtils.ml
+++ b/src/PureUtils.ml
@@ -102,7 +102,7 @@ let ty_as_integer (t : ty) : T.integer_type =
 
 (* TODO: move *)
 let type_decl_is_enum (def : T.type_decl) : bool =
-  match def.kind with T.Struct _ -> false | Enum _ -> true
+  match def.kind with T.Struct _ -> false | Enum _ -> true | Opaque -> false
 
 let mk_state_ty : ty = Adt (Assumed State, [])
 
@@ -186,8 +186,8 @@ let make_type_subst (vars : type_var list) (tys : ty list) : TypeVarId.id -> ty
 
     Raises [Invalid_argument] if the arguments are incorrect.
  *)
-let type_decl_get_fields (def : type_decl) (opt_variant_id : VariantId.id option)
-    : field list =
+let type_decl_get_fields (def : type_decl)
+    (opt_variant_id : VariantId.id option) : field list =
   match (def.kind, opt_variant_id) with
   | Enum variants, Some variant_id -> (VariantId.nth variants variant_id).fields
   | Struct fields, None -> fields
diff --git a/src/Substitute.ml b/src/Substitute.ml
index 4a1f42eb..0bc612ea 100644
--- a/src/Substitute.ml
+++ b/src/Substitute.ml
@@ -120,6 +120,8 @@ let type_decl_get_instantiated_variants_fields_rtypes (def : T.type_decl)
           (fun i v -> (Some (T.VariantId.of_int i), v.T.fields))
           variants
     | T.Struct fields -> [ (None, fields) ]
+    | T.Opaque ->
+        raise (Failure "Can't retrieve the variants of an opaque type")
   in
   List.map
     (fun (id, fields) ->
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 8f1eeb39..18b8f507 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -173,11 +173,12 @@ let get_instantiated_fun_sig (fun_id : A.fun_id)
   (* Apply *)
   fun_sig_substitute tsubst sg
 
-let bs_ctx_lookup_cfim_type_decl (id : TypeDeclId.id) (ctx : bs_ctx) : T.type_decl
-    =
+let bs_ctx_lookup_cfim_type_decl (id : TypeDeclId.id) (ctx : bs_ctx) :
+    T.type_decl =
   TypeDeclId.Map.find id ctx.type_context.cfim_type_decls
 
-let bs_ctx_lookup_cfim_fun_decl (id : FunDeclId.id) (ctx : bs_ctx) : A.fun_decl =
+let bs_ctx_lookup_cfim_fun_decl (id : FunDeclId.id) (ctx : bs_ctx) : A.fun_decl
+    =
   FunDeclId.Map.find id ctx.fun_context.cfim_fun_decls
 
 (* TODO: move *)
@@ -268,6 +269,7 @@ let translate_type_decl_kind (kind : T.type_decl_kind) : type_decl_kind =
   match kind with
   | T.Struct fields -> Struct (translate_fields fields)
   | T.Enum variants -> Enum (translate_variants variants)
+  | T.Opaque -> Opaque
 
 (** Translate a type definition from IM 
 
diff --git a/src/Types.ml b/src/Types.ml
index 013f511d..5ff407c9 100644
--- a/src/Types.ml
+++ b/src/Types.ml
@@ -199,7 +199,11 @@ type field = { field_name : string option; field_ty : sty } [@@deriving show]
 
 type variant = { variant_name : string; fields : field list } [@@deriving show]
 
-type type_decl_kind = Struct of field list | Enum of variant list
+type type_decl_kind =
+  | Struct of field list
+  | Enum of variant list
+  | Opaque
+      (** An opaque type: either a local type marked as opaque, or an external type *)
 [@@deriving show]
 
 type type_decl = {
diff --git a/src/TypesAnalysis.ml b/src/TypesAnalysis.ml
index d8895b55..e84b4f58 100644
--- a/src/TypesAnalysis.ml
+++ b/src/TypesAnalysis.ml
@@ -238,31 +238,41 @@ let analyze_full_ty (r_is_static : 'r -> bool) (updated : bool ref)
   (* Explore *)
   analyze expl_info_init ty_info ty
 
+let type_decl_is_opaque (d : type_decl) : bool =
+  match d.kind with Struct _ | Enum _ -> false | Opaque -> true
+
 let analyze_type_decl (updated : bool ref) (infos : type_infos)
     (def : type_decl) : type_infos =
-  (* Retrieve all the types of all the fields of all the variants *)
-  let fields_tys : sty list =
-    match def.kind with
-    | Struct fields -> List.map (fun f -> f.field_ty) fields
-    | Enum variants ->
-        List.concat
-          (List.map (fun v -> List.map (fun f -> f.field_ty) v.fields) variants)
-  in
-  (* Explore the types and accumulate information *)
-  let r_is_static r = r = Static in
-  let type_decl_info = TypeDeclId.Map.find def.def_id infos in
-  let type_decl_info = type_decl_info_to_partial_type_info type_decl_info in
-  let type_decl_info =
-    List.fold_left
-      (fun type_decl_info ty ->
-        analyze_full_ty r_is_static updated infos type_decl_info ty)
-      type_decl_info fields_tys
-  in
-  let type_decl_info = partial_type_info_to_type_decl_info type_decl_info in
-  (* Update the information for the type definition we explored *)
-  let infos = TypeDeclId.Map.add def.def_id type_decl_info infos in
-  (* Return *)
-  infos
+  (* We analyze the type declaration only if it is not opaque (we need to explore
+   * the variants of the ADTs *)
+  if type_decl_is_opaque def then infos
+  else
+    (* Retrieve all the types of all the fields of all the variants *)
+    let fields_tys : sty list =
+      match def.kind with
+      | Struct fields -> List.map (fun f -> f.field_ty) fields
+      | Enum variants ->
+          List.concat
+            (List.map
+               (fun v -> List.map (fun f -> f.field_ty) v.fields)
+               variants)
+      | Opaque -> raise (Failure "unreachable")
+    in
+    (* Explore the types and accumulate information *)
+    let r_is_static r = r = Static in
+    let type_decl_info = TypeDeclId.Map.find def.def_id infos in
+    let type_decl_info = type_decl_info_to_partial_type_info type_decl_info in
+    let type_decl_info =
+      List.fold_left
+        (fun type_decl_info ty ->
+          analyze_full_ty r_is_static updated infos type_decl_info ty)
+        type_decl_info fields_tys
+    in
+    let type_decl_info = partial_type_info_to_type_decl_info type_decl_info in
+    (* Update the information for the type definition we explored *)
+    let infos = TypeDeclId.Map.add def.def_id type_decl_info infos in
+    (* Return *)
+    infos
 
 let analyze_type_declaration_group (type_decls : type_decl TypeDeclId.Map.t)
     (infos : type_infos) (decl : type_declaration_group) : type_infos =
diff --git a/src/TypesUtils.ml b/src/TypesUtils.ml
index e463fbc5..58bb4803 100644
--- a/src/TypesUtils.ml
+++ b/src/TypesUtils.ml
@@ -2,6 +2,9 @@ open Types
 open Utils
 module TA = TypesAnalysis
 
+let type_decl_is_opaque (d : type_decl) : bool =
+  match d.kind with Struct _ | Enum _ -> false | Opaque -> true
+
 (** Retrieve the list of fields for the given variant of a [type_decl].
 
     Raises [Invalid_argument] if the arguments are incorrect.