Add AggregatedOption

5 files changed, 37 insertions, 8 deletions

diff --git a/src/Expressions.ml b/src/Expressions.ml
index a118ca67..61a2f95c 100644
--- a/src/Expressions.ml
+++ b/src/Expressions.ml
@@ -16,11 +16,8 @@ type projection_elem =
 [@@deriving show]
 
 type projection = projection_elem list [@@deriving show]
-
 type place = { var_id : VarId.id; projection : projection } [@@deriving show]
-
 type borrow_kind = Shared | Mut | TwoPhaseMut [@@deriving show]
-
 type unop = Not | Neg [@@deriving show, ord]
 
 (** A binary operation
@@ -118,6 +115,8 @@ type operand =
  *)
 type aggregate_kind =
   | AggregatedTuple
+  | AggregatedOption of VariantId.id * ety
+  (* TODO: AggregatedOption should be merged with AggregatedAdt *)
   | AggregatedAdt of
       TypeDeclId.id * VariantId.id option * erased_region list * ety list
 [@@deriving show]
diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml
index f4d97b9d..e46ca721 100644
--- a/src/InterpreterExpressions.ml
+++ b/src/InterpreterExpressions.ml
@@ -608,6 +608,20 @@ let eval_rvalue_aggregate (config : C.config)
         let aggregated : V.typed_value = { V.value = v; ty } in
         (* Call the continuation *)
         cf aggregated ctx
+    | E.AggregatedOption (variant_id, ty) ->
+        (* Sanity check *)
+        if variant_id == T.option_none_id then assert (values == [])
+        else if variant_id == T.option_some_id then
+          assert (List.length values == 1)
+        else raise (Failure "Unreachable");
+        (* Construt the value *)
+        let aty = T.Adt (T.Assumed T.Option, [], [ ty ]) in
+        let av : V.adt_value =
+          { V.variant_id = Some variant_id; V.field_values = values }
+        in
+        let aggregated : V.typed_value = { V.value = Adt av; ty = aty } in
+        (* Call the continuation *)
+        cf aggregated ctx
     | E.AggregatedAdt (def_id, opt_variant_id, regions, types) ->
         (* Sanity checks *)
         let type_decl = C.ctx_lookup_type_decl ctx def_id in
diff --git a/src/LlbcOfJson.ml b/src/LlbcOfJson.ml
index 75e9cbf7..32ca802e 100644
--- a/src/LlbcOfJson.ml
+++ b/src/LlbcOfJson.ml
@@ -423,6 +423,10 @@ let aggregate_kind_of_json (js : json) : (E.aggregate_kind, string) result =
   combine_error_msgs js "operand_kind_of_json"
     (match js with
     | `String "AggregatedTuple" -> Ok E.AggregatedTuple
+    | `Assoc [ ("AggregatedOption", `List [ variant_id; ty ]) ] ->
+        let* variant_id = T.VariantId.id_of_json variant_id in
+        let* ty = ety_of_json ty in
+        Ok (E.AggregatedOption (variant_id, ty))
     | `Assoc [ ("AggregatedAdt", `List [ id; opt_variant_id; regions; tys ]) ]
       ->
         let* id = T.TypeDeclId.id_of_json id in
diff --git a/src/Print.ml b/src/Print.ml
index 8df3001f..0c4ef20a 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -12,7 +12,6 @@ let option_to_string (to_string : 'a -> string) (x : 'a option) : string =
   match x with Some x -> "Some (" ^ to_string x ^ ")" | None -> "None"
 
 let name_to_string (name : name) : string = Names.name_to_string name
-
 let fun_name_to_string (name : fun_name) : string = name_to_string name
 
 (** Pretty-printing for types *)
@@ -48,9 +47,7 @@ module Types = struct
   }
 
   type stype_formatter = T.RegionVarId.id T.region type_formatter
-
   type rtype_formatter = T.RegionId.id T.region type_formatter
-
   type etype_formatter = T.erased_region type_formatter
 
   let integer_type_to_string = function
@@ -906,6 +903,15 @@ module LlbcAst = struct
         let ops = List.map (operand_to_string fmt) ops in
         match akind with
         | E.AggregatedTuple -> "(" ^ String.concat ", " ops ^ ")"
+        | E.AggregatedOption (variant_id, _ty) ->
+            if variant_id == T.option_none_id then (
+              assert (ops == []);
+              "@Option::None")
+            else if variant_id == T.option_some_id then (
+              assert (List.length ops == 1);
+              let op = List.hd ops in
+              "@Option::Some(" ^ op ^ ")")
+            else raise (Failure "Unreachable")
         | E.AggregatedAdt (def_id, opt_variant_id, _regions, _types) ->
             let adt_name = fmt.type_decl_id_to_string def_id in
             let variant_name =
diff --git a/src/Substitute.ml b/src/Substitute.ml
index c76f1da4..711e438b 100644
--- a/src/Substitute.ml
+++ b/src/Substitute.ml
@@ -121,7 +121,10 @@ let type_decl_get_instantiated_variants_fields_rtypes (def : T.type_decl)
           variants
     | T.Struct fields -> [ (None, fields) ]
     | T.Opaque ->
-        raise (Failure ("Can't retrieve the variants of an opaque type: " ^ Names.name_to_string def.name))
+        raise
+          (Failure
+             ("Can't retrieve the variants of an opaque type: "
+             ^ Names.name_to_string def.name))
   in
   List.map
     (fun (id, fields) ->
@@ -243,8 +246,11 @@ let rvalue_substitute (tsubst : T.TypeVarId.id -> T.ety) (rv : E.rvalue) :
       let kind =
         match kind with
         | E.AggregatedTuple -> E.AggregatedTuple
+        | E.AggregatedOption (variant_id, ty) ->
+            let rsubst r = r in
+            E.AggregatedOption (variant_id, ty_substitute rsubst tsubst ty)
         | E.AggregatedAdt (def_id, variant_id, regions, tys) ->
-            let rsubst x = x in
+            let rsubst r = r in
             E.AggregatedAdt
               ( def_id,
                 variant_id,