From a0049feb8490b85c5ffbc70813755fc8ee5d67c1 Mon Sep 17 00:00:00 2001
From: Bryan Parno <parno@cmu.edu>
Date: Tue, 8 Dec 2020 13:59:33 -0500
Subject: [PATCH] Create a fixed name for the while loop counter (loop_ctr)

---
 tools/Vale/src/emit_common_lemmas.fs | 2 +-
 tools/Vale/src/emit_dafny_text.fs    | 2 +-
 tools/Vale/src/typechecker.fs        | 1 +
 3 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/tools/Vale/src/emit_common_lemmas.fs b/tools/Vale/src/emit_common_lemmas.fs
index e54eaec7..197c0bf7 100644
--- a/tools/Vale/src/emit_common_lemmas.fs
+++ b/tools/Vale/src/emit_common_lemmas.fs
@@ -255,7 +255,7 @@ let rec build_lemma_stmt (senv:stmt_env) (s:stmt):ghost * bool * stmt list =
       let codeBody = vaApp "get_whileBody" [code] in
       let i1 = string (gen_lemma_sym ()) in
       let i2 = string (gen_lemma_sym ()) in
-      let (n1, s1, sw1, fw1) = (Reserved ("n" + i1), Reserved ("s" + i1), Reserved ("sW" + i1), Reserved ("fW" + i1)) in
+      let (n1, s1, sw1, fw1) = (Id "loop_ctr", Reserved ("s" + i1), Reserved ("sW" + i1), Reserved ("fW" + i1)) in
       let (sw2, fw2) = (Reserved ("sW" + i2), Reserved ("fW" + i2)) in
       let (codeCond, codeBody, sCodeVars) =
         if !fstar then
diff --git a/tools/Vale/src/emit_dafny_text.fs b/tools/Vale/src/emit_dafny_text.fs
index 092b8071..0bbd27c0 100644
--- a/tools/Vale/src/emit_dafny_text.fs
+++ b/tools/Vale/src/emit_dafny_text.fs
@@ -149,7 +149,7 @@ let rec emit_stmt (ps:print_state) (s:stmt):unit =
       ps.PrintLine ("ghost var " + (String.concat ", " (List.map string_of_lhs_formal lhss)) + " := " + (string_of_exp e) + ";")
   | SAssign _ -> emit_stmts ps (eliminate_assign_lhss s)
   | SLetUpdates _ -> internalErr "SLetUpdates"
-  | SBlock ss -> notImplemented "block"
+  | SBlock ss -> emit_block ps ss
   | SIfElse (_, e, ss1, []) ->
       ps.PrintLine ("if (" + (string_of_exp e) + ")");
       emit_block ps ss1
diff --git a/tools/Vale/src/typechecker.fs b/tools/Vale/src/typechecker.fs
index d82f9d5e..e2b4bbe4 100644
--- a/tools/Vale/src/typechecker.fs
+++ b/tools/Vale/src/typechecker.fs
@@ -1931,6 +1931,7 @@ let rec tc_stmt (env:env) (s:stmt):stmt =
       SIfElse (g, e, b1, b2)
   | SWhile (e, invs, ed, b) ->
       let (t, e) = tc_exp env e (Some tBool) in
+      let env = push_id env (Id "loop_ctr") (TInt (NegInf, Inf)) in
       let invs = List_mapSnd (fun e -> let (_, e) = tc_exp env e (Some tProp) in e) invs in
       let ed = mapSnd (List.map (fun e -> let (_, e) = tc_exp env e None in e)) ed in
       let (_, b) = tc_stmts env b in