initial implementation

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))
+    }
 }
 ```

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,
+    },
 }
 ```
 

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!(),
+                }
+            }
         })
     }
 }

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());

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}"))
+        }
     }
 }