More tests for sum types: records as option content

tests/fixtures/SumTypes.qnt

@@ -1,8 +1,9 @@
 module SumTypes {
 
-  type Option =
-    | Some(int)
+  type Option =    
     | None
+    | Some(int)
+    | SomeMore({x: int, y: bool})
 
   var value: Option
 
@@ -14,13 +15,27 @@ module SumTypes {
     value' = Some(x)
   }
 
+  action addComponent(y: bool) : bool = all {
+    match value {
+      | Some(x) => value' = SomeMore({x: x, y: y})
+      | SomeMore(r) => value' = SomeMore({x: r.x, y: y})
+      | None => value' = None
+    }
+  }
+
   action incrValue = all {
     match value {
       | Some(x) => value' = Some(x + 1)
       | None => value' = None
+      | SomeMore(r) => value' = SomeMore({x: r.x + 1, y: r.y})
     }
   }
 
-  run exampleTest = init.then(setValue(40)).then(incrValue).then(incrValue)
+  run exampleTest = 
+    init
+    .then(setValue(40))
+    .then(incrValue)
+    .then(addComponent(true))
+    .then(incrValue)
 
 }

tests/fixtures/SumTypes0.itf.json

@@ -1 +1 @@
-{"#meta":{"format":"ITF","format-description":"https://apalache.informal.systems/docs/adr/015adr-trace.html","source":"SumTypes.qnt","status":"passed","description":"Created by Quint on Thu Dec 07 2023 11:21:01 GMT+0100 (GMT+01:00)","timestamp":1701944461444},"vars":["value"],"states":[{"#meta":{"index":0},"value":{"tag":"None","value":{}}},{"#meta":{"index":1},"value":{"tag":"Some","value":{"#bigint":"40"}}},{"#meta":{"index":2},"value":{"tag":"Some","value":{"#bigint":"41"}}}]}
+{"#meta":{"format":"ITF","format-description":"https://apalache.informal.systems/docs/adr/015adr-trace.html","source":"SumTypes.qnt","status":"passed","description":"Created by Quint on Wed Dec 20 2023 10:52:13 GMT+0100 (Central European Standard Time)","timestamp":1703065933486},"vars":["value"],"states":[{"#meta":{"index":0},"value":{"tag":"None","value":{}}},{"#meta":{"index":1},"value":{"tag":"Some","value":{"#bigint":"40"}}},{"#meta":{"index":2},"value":{"tag":"Some","value":{"#bigint":"41"}}},{"#meta":{"index":3},"value":{"tag":"SomeMore","value":{"x":{"#bigint":"41"},"y":true}}}]}

tests/sum_types.rs

@@ -5,10 +5,17 @@ use serde_json::json;
 
 use itf::de::{As, Integer, Same};
 
+#[derive(Clone, Debug, Deserialize, PartialEq, Eq)]
+pub struct SomeMoreArgs {
+    pub x: BigInt,
+    pub y: bool,
+}
+
 #[derive(Debug, PartialEq, Eq, Deserialize)]
 #[serde(tag = "tag", content = "value")]
 enum IntOption {
     Some(BigInt),
+    SomeMore(SomeMoreArgs),
     None,
 }
 
@@ -25,6 +32,13 @@ fn parse_trace() {
     assert_eq!(trace.states[0].value.value, IntOption::None);
     assert_eq!(trace.states[1].value.value, IntOption::Some(40.into()));
     assert_eq!(trace.states[2].value.value, IntOption::Some(41.into()));
+    assert_eq!(
+        trace.states[3].value.value,
+        IntOption::SomeMore(SomeMoreArgs {
+            x: 41.into(),
+            y: true,
+        })
+    );
 }
 
 #[test]
@@ -93,3 +107,47 @@ fn test_deserialize_enum() {
     let foobar = itf::from_value::<Enum>(foobar_itf).unwrap();
     assert_eq!(foobar, Enum::FooBar("hello".to_string(), 42.into(), true));
 }
+
+#[derive(Debug, PartialEq, Eq, Deserialize)]
+#[serde(tag = "tag", content = "value")]
+enum EnumRecords {
+    None,
+    OptionA { x: String },
+    OptionB { x: String, y: bool },
+}
+
+#[test]
+fn test_deserialize_record_enum() {
+    let option_a_itf = json!({
+        "tag": "OptionA",
+        "value": {"x": "hello"},
+    });
+
+    let a = itf::from_value::<EnumRecords>(option_a_itf).unwrap();
+    assert_eq!(
+        a,
+        EnumRecords::OptionA {
+            x: "hello".to_string()
+        }
+    );
+
+    let option_b_itf = json!({
+        "tag": "OptionB",
+        "value": {"x": "hello", "y": true},
+    });
+    let b = itf::from_value::<EnumRecords>(option_b_itf).unwrap();
+    assert_eq!(
+        b,
+        EnumRecords::OptionB {
+            x: "hello".to_string(),
+            y: true
+        }
+    );
+
+    let option_none_itf = json!({
+        "tag": "None",
+        "value": {},
+    });
+    let no_args = itf::from_value::<EnumRecords>(option_none_itf).unwrap();
+    assert_eq!(no_args, EnumRecords::None);
+}