From 7a2c2c62b71b52c25806895adfbb048fbd52ce73 Mon Sep 17 00:00:00 2001
From: ivan-gavran <ivan@informal.systems>
Date: Wed, 20 Dec 2023 10:42:25 +0100
Subject: [PATCH 1/2] deserialization of the record enum

---
 tests/sum_types.rs | 44 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 44 insertions(+)

diff --git a/tests/sum_types.rs b/tests/sum_types.rs
index eb1b2bc..d2f5c75 100644
--- a/tests/sum_types.rs
+++ b/tests/sum_types.rs
@@ -93,3 +93,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);
+}

From 0090cb1f33ef1a142399fd21342b5369424d5691 Mon Sep 17 00:00:00 2001
From: ivan-gavran <ivan@informal.systems>
Date: Wed, 20 Dec 2023 11:00:13 +0100
Subject: [PATCH 2/2] added an option with records to the quint model and the
 parse test

---
 tests/fixtures/SumTypes.qnt       | 21 ++++++++++++++++++---
 tests/fixtures/SumTypes0.itf.json |  2 +-
 tests/sum_types.rs                | 14 ++++++++++++++
 3 files changed, 33 insertions(+), 4 deletions(-)

diff --git a/tests/fixtures/SumTypes.qnt b/tests/fixtures/SumTypes.qnt
index e3e96e9..0ccc0c1 100644
--- a/tests/fixtures/SumTypes.qnt
+++ b/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)
 
 }
diff --git a/tests/fixtures/SumTypes0.itf.json b/tests/fixtures/SumTypes0.itf.json
index 8ff32cb..3e11e18 100644
--- a/tests/fixtures/SumTypes0.itf.json
+++ b/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"}}}]}
\ No newline at end of file
+{"#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}}}]}
\ No newline at end of file
diff --git a/tests/sum_types.rs b/tests/sum_types.rs
index d2f5c75..b60ee60 100644
--- a/tests/sum_types.rs
+++ b/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]