adding definitions for a_if and a_while

theories/c_translation/translation.v

@@ -26,11 +26,11 @@ Definition a_load : val := λ: "x",
   ) "x".
 
 Definition a_un_op (op : un_op) : val := λ: "x",
-  a_bind (λ: "v", UnOp op "v") "x".
+  a_bind (λ: "v", a_ret (λ: <>, UnOp op "v")) "x".
 
 Definition a_bin_op (op : bin_op) : val := λ: "x1" "x2",
   a_bind (λ: "vv",
-    BinOp op (Fst "vv") (Snd "vv")
+    a_ret (BinOp op (Fst "vv") (Snd "vv"))
   ) (a_par "x1" "x2").
 
 (* M () *)
@@ -38,6 +38,23 @@ Definition a_bin_op (op : bin_op) : val := λ: "x1" "x2",
 Definition a_seq : val := λ: "env",
   a_atomic_env (λ: "env", mset_clear "env") "env".
 
+Definition a_sequence : val := λ: "e1" "e2",
+  a_bind (λ: <>,
+    a_bind (λ: <>, (a_bind (λ: "v", a_ret "v") "e2")) a_seq
+  ) "e1".
+
+Definition a_if : val := λ: "cnd" "e1" "e2",
+  a_bind (λ: "c", if: "c" then "e1" else "e2") "cnd".
+
+Definition a_while: val := λ: "cond" "body",
+  let: "rwhile" :=
+     rec: "while" "cnd" "bdy" :=
+       a_if "cnd"
+         (a_sequence "bdy"
+            (λ: "env" "l", ("while" "cnd" "bdy") "env" "l"))
+         (a_ret #())
+  in "rwhile" "cond" "body".
+
 Section proofs.
   Context `{locking_heapG Σ, heapG Σ, flockG Σ, spawnG Σ}.