add vcg_wp_unknown

theories/vcgen/vcgen.v

@@ -131,8 +131,18 @@ Section vcg.
     | dCAlloc _ |  dCUnknown _ => None
     end.
 
-  (* TODO: change the fail though cases, in the same way as the unknown case
-  of vcg_wp. Also factor that out in a function vcg_unknown *)
+
+  Definition vcg_wp_unknown (R : iProp Σ) (E: known_locs) (de: dcexpr) (m: denv)
+      (Φ : known_locs → denv → dval → wp_expr) : wp_expr :=
+    mapsto_wand_list m $ Base $
+      awp (dcexpr_interp E de) R (λ v,
+        ∃ E' m' dv,
+        ⌜ v = dval_interp E' dv ⌝ ∧
+        ⌜ E `prefix_of` E' ⌝ ∧
+        denv_interp E' m' ∗
+        wp_interp_sane E' (Φ E' m' dv))%I.
+  Arguments vcg_wp_unknown : simpl never.
+
   Definition vcg_wp_load (E : known_locs) (dv : dval) (m : denv)
       (Φ : denv → dval → wp_expr) : wp_expr :=
     match is_dloc E dv with
@@ -188,9 +198,7 @@ Section vcg.
           | Some (mIn, mOut, dv2) =>
              vcg_wp E mIn de1 R (λ E mIn dv1,
                vcg_wp_store E dv1 dv2 (denv_merge mOut mIn) (Φ E))
-          | None =>
-             mapsto_wand_list m $ Base $
-               awp (dcexpr_interp E de) R (λ v, wp_interp E (Φ E [] (dValUnknown v)))
+          | None => vcg_wp_unknown R E de m Φ
           end
         end
     | dCBinOp op de1 de2 =>
@@ -203,9 +211,7 @@ Section vcg.
           | Some (mIn, mOut, dv2) =>
              vcg_wp E mIn de1 R (λ E mIn dv1,
                vcg_wp_bin_op E op dv1 dv2 (denv_merge mOut mIn) (Φ E))
-          | None =>
-             mapsto_wand_list m $ Base $
-               awp (dcexpr_interp E de) R (λ v, wp_interp E (Φ E [] (dValUnknown v)))
+          | None => vcg_wp_unknown R E de m Φ
           end
        end
     | dCUnOp op de =>
@@ -217,14 +223,7 @@ Section vcg.
     | dCSeq de1 de2 =>
        vcg_wp E m de1 R (λ E m _,
          UMod (vcg_wp E (denv_unlock m) de2 R Φ))
-    | _ =>
-       mapsto_wand_list m $ Base $
-         awp (dcexpr_interp E de) R (λ v,
-           ∃ E' m' dv,
-           ⌜ v = dval_interp E' dv ⌝ ∧
-           ⌜ E `prefix_of` E' ⌝ ∧
-           denv_interp E' m' ∗
-           wp_interp_sane E' (Φ E' m' dv))%I
+    | _ => vcg_wp_unknown R E de m Φ
     end.
 End vcg.
 
@@ -248,9 +247,6 @@ Section vcg_spec.
     - simpl. intros E. by apply U_mono.
   Qed.
 
-
-
-
   Lemma mapsto_wand_list_spec E m t :
     wp_interp E (mapsto_wand_list m t) -∗ denv_interp E m -∗ wp_interp E t.
   Proof.