Merge pull request #2850 from FStarLang/guido_2849

Normalizer fix for mutually recursive functions (#2849)

src/typechecker/FStar.TypeChecker.Normalize.fst

@@ -1628,8 +1628,11 @@ let rec norm : cfg -> env -> stack -> term -> term =
                     let rec_env = (None, Clos(env, fix_f_i, memo, true))::rec_env in
                     rec_env, memo::memos, i + 1) (snd lbs) (env, [], 0) in
             let _ = List.map2 (fun lb memo -> memo := Some (rec_env, lb.lbdef)) (snd lbs) memos in //tying the knot
-            let body_env = List.fold_right (fun lb env -> (None, Clos(rec_env, lb.lbdef, BU.mk_ref None, false))::env)
-                               (snd lbs) env in
+            // NB: fold_left, since the binding structure of lbs is that righmost is closer, while in the env leftmost
+            // is closer. In other words, the last element of lbs is index 0 for body, hence needs to be pushed last.
+            let body_env = List.fold_left (fun env lb -> (None, Clos(rec_env, lb.lbdef, BU.mk_ref None, false))::env)
+                               env (snd lbs) in
+            log cfg (fun () -> BU.print1 "reducing with knot %s\n" "");
             norm cfg body_env stack body
 
           | Tm_meta (head, m) ->

tests/bug-reports/Bug2849a.fst

@@ -0,0 +1,18 @@
+module Bug2849a
+
+module T = FStar.Tactics
+
+let visit_terms (t: T.term): T.Tac unit =
+  let rec tm (t: T.term): T.Tac unit = match T.inspect_unascribe t with
+    | T.Tv_Match sc _ brs ->
+      // do work then recurse...
+      T.iter br brs;
+      tm sc
+    | _ -> ()
+  and br (b: T.branch): T.Tac unit = tm (snd b)
+  in tm t
+
+let nothing (): unit =
+  assert (true) by (
+    visit_terms (`true)
+  )

tests/bug-reports/Bug2849b.fst

@@ -0,0 +1,28 @@
+module Bug2849b
+
+let pure () : int =
+  let rec f () : int = 1
+  and g () = 2
+  and h () = 3
+  in f ()
+
+let _ = assert_norm (pure () == 1)
+
+module T = FStar.Tactics
+
+let t1 () : T.Tac unit =
+  let rec f (): T.Tac unit = T.fail "fail_f"
+  and g () : T.Tac unit = ()
+  and h () : T.Tac unit = T.fail "fail_g"
+  in g ()
+
+let tac1 (): unit = assert (True) by (t1 ())
+
+let t2 () : T.Tac unit =
+  let rec f (): T.Tac unit = T.fail "fail_f"
+  and g () : T.Tac unit = ()
+  and h () : T.Tac unit = T.fail "fail_g"
+  in f ()
+
+[@@expect_failure]
+let tac2 (): unit = assert (True) by (t2 ())

tests/bug-reports/Makefile

@@ -49,7 +49,8 @@ SHOULD_VERIFY_CLOSED=Bug022.fst Bug024.fst Bug025.fst Bug026.fst Bug026b.fst Bug
   Bug2552.fst Bug2597.fst Bug2471_B.fst Bug2605.fst Bug2614.fst Bug2622.fst \
   Bug2635.fst Bug2637.fst Bug2641.fst Bug1486.fst PropProofs.fst \
   Bug2684a.fst Bug2684b.fst Bug2684c.fst Bug2684d.fst Bug2659b.fst\
-  Bug2756.fst MutualRecPositivity.fst Bug2806a.fst Bug2806b.fst Bug2806c.fst Bug2806d.fst Bug2809.fst
+  Bug2756.fst MutualRecPositivity.fst Bug2806a.fst Bug2806b.fst Bug2806c.fst Bug2806d.fst Bug2809.fst\
+  Bug2849a.fst Bug2849b.fst
 
 SHOULD_VERIFY_INTERFACE_CLOSED=Bug771.fsti Bug771b.fsti
 SHOULD_VERIFY_AND_WARN_CLOSED=Bug016.fst