Merge vcg_solver and splitenv into new file called proofmode.

_CoqProject

@@ -12,9 +12,8 @@ theories/c_translation/proofmode.v
 theories/c_translation/translation.v
 theories/vcgen/dcexpr.v
 theories/vcgen/denv.v
-theories/vcgen/splitenv.v
 theories/vcgen/vcgen.v
-theories/vcgen/vcg_solver.v
+theories/vcgen/proofmode.v
 theories/tests/basics.v
 theories/tests/invoke.v
 theories/tests/unknowns.v

theories/tests/basics.v

 (** Testing basic connectives *)
-From iris_c.vcgen Require Import vcg_solver.
+From iris_c.vcgen Require Import proofmode.
 
 Section test.
   Context `{amonadG Σ}.

theories/tests/binop.v

-From iris_c.vcgen Require Import vcg_solver.
+From iris_c.vcgen Require Import proofmode.
 
 Section test.
   Context `{amonadG Σ}.

theories/tests/fact.v

-From iris_c.vcgen Require Import vcg_solver.
+From iris_c.vcgen Require Import proofmode.
 Local Open Scope Z_scope.
 
 Definition incr : val := λ: "l",

theories/tests/gcd.v

-From iris_c.vcgen Require Import vcg_solver.
+From iris_c.vcgen Require Import proofmode.
 Local Open Scope Z_scope.
 
 (* TODO: Notation, get rid of parenthesis around the while loop *)

theories/tests/invoke.v

 (** Testing function calls and AWP resources *)
-From iris_c.vcgen Require Import vcg_solver.
+From iris_c.vcgen Require Import proofmode.
 
 Section tests_vcg.
   Context `{amonadG Σ}.

theories/tests/lists.v

-From iris_c.vcgen Require Import vcg_solver.
+From iris_c.vcgen Require Import proofmode.
 
 Definition a_list_nil : val := λ:<>, a_ret NONEV.
 

theories/tests/memcpy.v

-From iris_c.vcgen Require Import vcg_solver.
+From iris_c.vcgen Require Import proofmode.
 Local Open Scope Z_scope.
 
 Section memcpy.

theories/tests/swap.v

-From iris_c.vcgen Require Import vcg_solver.
+From iris_c.vcgen Require Import proofmode.
 
 Section tests_vcg.
   Context `{amonadG Σ}.

theories/tests/unknowns.v

 (** Testing vcgen on expressions contaning unknown subexpressions *)
-From iris_c.vcgen Require Import vcg_solver.
+From iris_c.vcgen Require Import proofmode.
 Local Open Scope Z_scope.
 
 Section tests_vcg.

theories/vcgen/vcg_solver.v → theories/vcgen/proofmode.v

-From iris_c.vcgen Require Export vcgen.
-From iris_c.vcgen Require Import splitenv.
+From iris_c.c_translation Require Export translation.
+From iris_c.vcgen Require Import vcgen denv.
 From iris.proofmode Require Import environments coq_tactics.
 Import env_notations.
 
-Section vcg_continue.
+Section tactics.
   Context `{amonadG Σ}.
 
+  Class MapstoListFromEnv (Γin Γout : env (iProp Σ)) (Γls : penv) := {
+    mapsto_list_from_env : [∗] Γin ⊢ [∗] Γout ∗ penv_interp Γls;
+    mapsto_list_from_env_wf : env_wf Γin → env_wf Γout;
+    mapsto_list_from_env_lookup_None i: Γin !! i = None → Γout !! i = None
+  }.
+
+  Global Instance mapsto_list_from_env_nil : MapstoListFromEnv Enil Enil nil.
+  Proof. split; unfold penv_interp; eauto. Qed.
+
+  Global Instance mapsto_list_from_env_snoc_Γout Γin Γout Γls i P  :
+    MapstoListFromEnv Γin Γout Γls →
+    MapstoListFromEnv (Esnoc Γin i P) (Esnoc Γout i P) Γls | 100.
+  Proof.
+    destruct 1; split; simpl.
+    - rewrite mapsto_list_from_env0. iIntros "(H1 & H2 & H3)". iFrame.
+    - intro Hwf. inversion Hwf; subst. apply mapsto_list_from_env_wf0 in H4.
+      apply Esnoc_wf; last done. by apply mapsto_list_from_env_lookup_None0.
+    - intros j Hj. destruct (ident_beq j i); simplify_eq /=.
+        by apply mapsto_list_from_env_lookup_None0.
+  Qed.
+
+  Global Instance mapsto_list_from_env_snoc_Γls Γin Γout Γls i l q v lvl :
+    MapstoListFromEnv Γin Γout Γls →
+    MapstoListFromEnv (Esnoc Γin i (l ↦C[lvl]{q} v))
+                      Γout
+                      (PenvItem l lvl q v :: Γls) | 3.
+  Proof.
+    destruct 1. split.
+    - iIntros "[H1 H2] /=". iFrame.
+      by rewrite mapsto_list_from_env0.
+    - intros Heq. inversion Heq; simplify_eq /=. by apply mapsto_list_from_env_wf0.
+    - intros j Hsnoc. apply mapsto_list_from_env_lookup_None0.
+      destruct (decide (i = j)) as [->|]. simplify_eq /=. by destruct (ident_beq j j ).
+        by rewrite env_lookup_snoc_ne in Hsnoc.
+  Qed.
+
+  Class ListOfMapsto (Γls : penv) (E : known_locs) (ps : denv) :=
+    list_of_mapsto : penv_interp Γls ⊢ denv_interp E ps.
+
+  Global Instance list_of_mapsto_nil E : ListOfMapsto [] E [].
+  Proof. unfold ListOfMapsto. simpl. eauto. Qed.
+
+  Global Instance list_of_mapsto_cons E Γls ps v dv i l x q :
+    LocLookup E l i →
+    IntoDVal E v dv →
+    ListOfMapsto Γls E ps →
+    ListOfMapsto (PenvItem l x q v :: Γls) E
+                 (denv_insert i x q dv ps).
+  Proof.
+    rewrite /LocLookup /ListOfMapsto /penv_interp=> Hi [-> ?] HΓls /=.
+    iIntros "[Hl H] /=". rewrite HΓls -denv_insert_interp /= Hi. iFrame.
+  Qed.
+
+  Lemma tac_envs_split_mapsto  Γs_in Γs_out Γls Γp c ps P:
+    MapstoListFromEnv Γs_in Γs_out Γls →
+    ListOfMapsto Γls (penv_to_known_locs Γls) ps →
+    envs_entails (Envs Γp Γs_out c) (denv_interp (penv_to_known_locs Γls) ps -∗ P)%I →
+    envs_entails (Envs Γp Γs_in c) P.
+  Proof.
+    intros Hsplit. rewrite /ListOfMapsto environments.envs_entails_eq=> Hexhale.
+    unfold of_envs. simpl.
+    rewrite mapsto_list_from_env. intros Hz.
+    iIntros "(Hwf & #Hp & Hs & Hls)". iDestruct "Hwf" as %Hwf.
+    iApply (Hz with "[Hs]").
+    - iFrame "Hp Hs". iPureIntro.
+      split; eauto.
+      + apply Hwf.
+      + apply Hsplit. apply Hwf.
+      + intros i. simpl. destruct (envs_disjoint _ Hwf i) as [Hp | Hp]; simpl in Hp.
+        * by left.
+        * right. by apply Hsplit.
+    - by iApply Hexhale.
+  Qed.
+
   Class FromKnownLocs (Γls : penv) (E_old : known_locs) (E_new : known_locs).
   (*dom Γls ⊂ (elem_of E_old) disj_Union (elem_of E) *)
 
@@ -68,7 +142,7 @@ Section vcg_continue.
       * by left.
       * right. by apply Hsplit.
   Qed.
-End vcg_continue.
+End tactics.
 
 Arguments vcg_wp_continuation {_ _ _ _}.
 

theories/vcgen/splitenv.v

-From iris.proofmode Require Import environments coq_tactics.
-From iris_c.vcgen Require Export denv.
-Import env_notations.
-
-Section splitenv.
-  Context `{amonadG Σ}.
-
-  Class MapstoListFromEnv (Γin Γout : env (iProp Σ)) (Γls : penv) := {
-    mapsto_list_from_env : [∗] Γin ⊢ [∗] Γout ∗ penv_interp Γls;
-    mapsto_list_from_env_wf : env_wf Γin → env_wf Γout;
-    mapsto_list_from_env_lookup_None i: Γin !! i = None → Γout !! i = None
-  }.
-
-  Global Instance mapsto_list_from_env_nil : MapstoListFromEnv Enil Enil nil.
-  Proof. split; unfold penv_interp; eauto. Qed.
-
-  Global Instance mapsto_list_from_env_snoc_Γout Γin Γout Γls i P  :
-    MapstoListFromEnv Γin Γout Γls →
-    MapstoListFromEnv (Esnoc Γin i P) (Esnoc Γout i P) Γls | 100.
-  Proof.
-    destruct 1; split; simpl.
-    - rewrite mapsto_list_from_env0. iIntros "(H1 & H2 & H3)". iFrame.
-    - intro Hwf. inversion Hwf; subst. apply mapsto_list_from_env_wf0 in H4.
-      apply Esnoc_wf; last done. by apply mapsto_list_from_env_lookup_None0.
-    - intros j Hj. destruct (ident_beq j i); simplify_eq /=.
-        by apply mapsto_list_from_env_lookup_None0.
-  Qed.
-
-  Global Instance mapsto_list_from_env_snoc_Γls Γin Γout Γls i l q v lvl :
-    MapstoListFromEnv Γin Γout Γls →
-    MapstoListFromEnv (Esnoc Γin i (l ↦C[lvl]{q} v))
-                      Γout
-                      (PenvItem l lvl q v :: Γls) | 3.
-  Proof.
-    destruct 1. split.
-    - iIntros "[H1 H2] /=". iFrame.
-      by rewrite mapsto_list_from_env0.
-    - intros Heq. inversion Heq; simplify_eq /=. by apply mapsto_list_from_env_wf0.
-    - intros j Hsnoc. apply mapsto_list_from_env_lookup_None0.
-      destruct (decide (i = j)) as [->|]. simplify_eq /=. by destruct (ident_beq j j ).
-        by rewrite env_lookup_snoc_ne in Hsnoc.
-  Qed.
-
-  Class ListOfMapsto (Γls : penv) (E : known_locs) (ps : denv) :=
-    list_of_mapsto : penv_interp Γls ⊢ denv_interp E ps.
-
-  Global Instance list_of_mapsto_nil E : ListOfMapsto [] E [].
-  Proof. unfold ListOfMapsto. simpl. eauto. Qed.
-
-  Global Instance list_of_mapsto_cons E Γls ps v dv i l x q :
-    LocLookup E l i →
-    IntoDVal E v dv →
-    ListOfMapsto Γls E ps →
-    ListOfMapsto (PenvItem l x q v :: Γls) E
-                 (denv_insert i x q dv ps).
-  Proof.
-    rewrite /LocLookup /ListOfMapsto /penv_interp=> Hi [-> ?] HΓls /=.
-    iIntros "[Hl H] /=". rewrite HΓls -denv_insert_interp /= Hi. iFrame.
-  Qed.
-
-  Lemma tac_envs_split_mapsto  Γs_in Γs_out Γls Γp c ps P:
-    MapstoListFromEnv Γs_in Γs_out Γls →
-    ListOfMapsto Γls (penv_to_known_locs Γls) ps →
-    envs_entails (Envs Γp Γs_out c) (denv_interp (penv_to_known_locs Γls) ps -∗ P)%I →
-    envs_entails (Envs Γp Γs_in c) P.
-  Proof.
-    intros Hsplit. rewrite /ListOfMapsto environments.envs_entails_eq=> Hexhale.
-    unfold of_envs. simpl.
-    rewrite mapsto_list_from_env. intros Hz.
-    iIntros "(Hwf & #Hp & Hs & Hls)". iDestruct "Hwf" as %Hwf.
-    iApply (Hz with "[Hs]").
-    - iFrame "Hp Hs". iPureIntro.
-      split; eauto.
-      + apply Hwf.
-      + apply Hsplit. apply Hwf.
-      + intros i. simpl. destruct (envs_disjoint _ Hwf i) as [Hp | Hp]; simpl in Hp.
-        * by left.
-        * right. by apply Hsplit.
-    - by iApply Hexhale.
-  Qed.
-End splitenv.