Support purification inside fold/unfold.

Author: gebner

src/checker/Pulse.Checker.AssertWithBinders.fst

@@ -19,6 +19,7 @@ module Pulse.Checker.AssertWithBinders
 open Pulse.Syntax
 open Pulse.Typing
 open Pulse.Checker.Base
+open Pulse.Checker.ImpureSpec
 open Pulse.Elaborate.Pure
 open Pulse.Typing.Env
 
@@ -486,6 +487,7 @@ let check
 
     check_unfoldable g v;
 
+    let v_opened = purify_term g { ctxt_now = pre; ctxt_old = None } v_opened in
     let v_opened, t_rem = PC.instantiate_term_implicits (push_env g uvs) v_opened None false in
 
     let uvs, v_opened =

test/ImpureSpec.fst

@@ -111,4 +111,13 @@ fn test12 ()
 {
   let mut x = 2;
   rewrite x |-> !x as x |-> (0 + !x * 1);
+}
+
+let p13 (x: ref int) = live x
+fn test13 ()
+{
+  let mut x = 42;
+  let mut y = x;
+  fold p13 (!y);
+  unfold p13 (!y);
 }