Improve union ergonomics.

Author: gebner

opt/pulse

@@ -714,15 +714,17 @@ impl<'a> Emitter<'a> {
                                 )),
                                 ExprKind::RValue(x_doc) => ExprKind::RValue(annotated(
                                     v,
-                                    self.nm
-                                        .emit(Name::UnionFieldConstructor(
-                                            union_name.val.clone(),
-                                            a.val.clone(),
-                                        ))
-                                        .append("?._0")
-                                        .append(Doc::line())
-                                        .append(x_doc)
-                                        .group(),
+                                    parens(
+                                        self.nm
+                                            .emit(Name::UnionFieldConstructor(
+                                                union_name.val.clone(),
+                                                a.val.clone(),
+                                            ))
+                                            .append("?._0")
+                                            .append(Doc::line())
+                                            .append(x_doc)
+                                            .group(),
+                                    ),
                                 )),
                             }
                         }
@@ -1556,7 +1558,13 @@ impl<'a> Emitter<'a> {
 
         let k = &TypeRefKind::Typedef(name.clone());
         let t = self.nm.emit(Name::TypeRef(k.into()));
-        let ty_decl = mk_let(t.clone(), &[], Doc::text("Type"), self.emit_type(env, body));
+        // The unfold here is important to trigger the loop detection in the Pulse prover
+        let ty_decl = Doc::text("unfold").append(Doc::line()).append(mk_let(
+            t.clone(),
+            &[],
+            Doc::text("Type"),
+            self.emit_type(env, body),
+        ));
         let env = &mut env.clone();
         let this = env
             .push_this(TypeT::TypeRef(k.clone()).with_loc(name.loc.clone()))

src/pass/emit.rs

@@ -23,35 +23,30 @@ void test1(u_context_t ctx)
     _requires(_is_uds(ctx))
 {
     uint8_t *uds_buf = ctx.uds;
-    _ghost_stmt(union__u_context_t__aux_raw_fold_uds $&(ctx) _);
 }
 
 void test2(u_context_t *ctx)
     _requires(_is_uds(*ctx))
 {
     uint8_t *uds_buf = ctx->uds;
-    _ghost_stmt(union__u_context_t__aux_raw_fold_uds $(ctx) _);
 }
 
 void test3a(context_t ctx)
     _requires(_is_uds(ctx.payload))
 {
     u_context_t *payload = &ctx.payload;
     uint8_t *uds_buf = payload->uds;
-    _ghost_stmt(union__u_context_t__aux_raw_fold_uds _ _);
 }
 
 
 void test3(context_t ctx)
     _requires(_is_uds(ctx.payload))
 {
     uint8_t *uds_buf = ctx.payload.uds;
-    _ghost_stmt(union__u_context_t__aux_raw_fold_uds _ _);
 }
 
 void test4(context_t *ctx)
     _requires(_is_uds(ctx->payload))
 {
     uint8_t *uds_buf = ctx->payload.uds;
-    _ghost_stmt(union__u_context_t__aux_raw_fold_uds _ _);
 }