From 699a65f704ac5ee73e7ed92dac3cbf6e5d36dcef Mon Sep 17 00:00:00 2001
From: Timon Meyer <timeyer@ethz.ch>
Date: Sat, 18 Nov 2023 10:27:00 +0100
Subject: [PATCH] initial implementation

---
 spec/lang/step/expressions.md      | 11 +++++++++++
 spec/lang/syntax.md                |  8 ++++++++
 spec/lang/well-formed.md           |  8 ++++++++
 tooling/miniutil/src/build/expr.rs |  8 ++++++++
 tooling/miniutil/src/fmt/expr.rs   |  6 ++++++
 5 files changed, 41 insertions(+)

diff --git a/spec/lang/step/expressions.md b/spec/lang/step/expressions.md
index ca7544ca..2f1a96c7 100644
--- a/spec/lang/step/expressions.md
+++ b/spec/lang/step/expressions.md
@@ -264,5 +264,16 @@ impl<M: Memory> Machine<M> {
         let ptr = self.ptr_offset_inbounds(root.ptr, offset.bytes())?;
         ret((Place { ptr, ..root }, field_ty))
     }
+
+    fn eval_place(&mut self, PlaceExpr::Downcast { root, variantIdx }: PlaceExpr) -> NdResult<(Place<M>, Type)> {
+        let (root, ty) = self.eval_place(root)?;
+        // We only need to downcast the enum type into the variant data type
+        // since all the enum data must have the same size with offset 0 (invariant).
+        let var_ty = match ty {
+            Type::Enum { variants, .. } => variants[variantIdx].ty,
+            _ => throw_ub!("enum downcast to invalid variant"),
+        };
+        ret((root, var_ty))
+    }
 }
 ```
diff --git a/spec/lang/syntax.md b/spec/lang/syntax.md
index 5fb79312..4ee1ff14 100644
--- a/spec/lang/syntax.md
+++ b/spec/lang/syntax.md
@@ -175,6 +175,14 @@ pub enum PlaceExpr {
         #[specr::indirection]
         index: ValueExpr,
     },
+    /// Enum variant downcast.
+    Downcast {
+        /// The base enum to project to the specific variant.
+        #[specr::indirection]
+        root: PlaceExpr,
+        /// The variant index to project to.
+        variantIdx: Int,
+    },
 }
 ```
 
diff --git a/spec/lang/well-formed.md b/spec/lang/well-formed.md
index c103b64e..379f5195 100644
--- a/spec/lang/well-formed.md
+++ b/spec/lang/well-formed.md
@@ -313,6 +313,14 @@ impl PlaceExpr {
                     _ => throw!(),
                 }
             }
+            Downcast { root, variantIdx } => {
+                let root = root.check_wf::<T>(locals, prog)?;
+                match root {
+                    // A valid downcast points to an existing variant.
+                    Type::Enum { variants, .. } => variants.get(variantIdx)?.ty,
+                    _ => throw!(),
+                }
+            }
         })
     }
 }
diff --git a/tooling/miniutil/src/build/expr.rs b/tooling/miniutil/src/build/expr.rs
index 56c7aef7..9f4634ad 100644
--- a/tooling/miniutil/src/build/expr.rs
+++ b/tooling/miniutil/src/build/expr.rs
@@ -216,6 +216,14 @@ pub fn index(root: PlaceExpr, index: ValueExpr) -> PlaceExpr {
     }
 }
 
+/// An enum downcast into the variant at the specified index.
+pub fn downcast(root: PlaceExpr, variantIdx: impl Into<Int>) -> PlaceExpr {
+    PlaceExpr::Downcast {
+        root: GcCow::new(root),
+        variantIdx: variantIdx.into(),
+    }
+}
+
 /// A place suited for zero-sized accesses.
 pub fn zst_place() -> PlaceExpr {
     let ptr = ValueExpr::Constant(Constant::InvalidPointer(1.into()), <*const ()>::get_type());
diff --git a/tooling/miniutil/src/fmt/expr.rs b/tooling/miniutil/src/fmt/expr.rs
index a7197535..f8aada0f 100644
--- a/tooling/miniutil/src/fmt/expr.rs
+++ b/tooling/miniutil/src/fmt/expr.rs
@@ -53,6 +53,12 @@ pub(super) fn fmt_place_expr(p: PlaceExpr, comptypes: &mut Vec<CompType>) -> Fmt
             // This can be considered atomic due to the same reasoning as for PlaceExpr::Field, see above.
             FmtExpr::Atomic(format!("{root}[{index}]"))
         }
+        PlaceExpr::Downcast { root, variantIdx } => {
+            let root = fmt_place_expr(root.extract(), comptypes).to_atomic_string();
+            // This is not atomic as `local(1) as variant 3.0` illustrates. (Field 0 of downcast)
+            // We can't do it nicely like in the Rust MIR ({root} as {variant name}) since we have no variant names.
+            FmtExpr::NonAtomic(format!("{root} as variant {variantIdx}"))
+        }
     }
 }