Merge pull request #3085 from mtzguido/norm_unfold_tac

Do not unfold logical connectives in norm requests

src/typechecker/FStar.TypeChecker.Normalize.fst

@@ -798,16 +798,17 @@ let get_norm_request cfg (full_norm:term -> term) args =
       @ (if cfg.steps.allow_unbound_universes then [AllowUnboundUniverses] else [])
       @ (if cfg.steps.nbe_step then [NBE] else []) // ZOE : NBE can be set as the default mode
     in
+    (* We always set UnfoldTac: do not unfold logical connectives *)
     match args with
     | [_; (tm, _)]
     | [(tm, _)] ->
       let s = [Beta; Zeta; Iota; Primops; UnfoldUntil delta_constant; Reify] in
-      Some (inherited_steps @ s, tm)
+      Some (UnfoldTac :: inherited_steps @ s, tm)
     | [(steps, _); _; (tm, _)] ->
       begin
       match parse_steps (full_norm steps) with
       | None -> None
-      | Some s -> Some (inherited_steps @ s, tm)
+      | Some s -> Some (UnfoldTac :: inherited_steps @ s, tm)
       end
     | _ ->
       None
@@ -963,11 +964,6 @@ let should_unfold cfg should_reify fv qninfo : should_unfold_res =
         log_unfolding cfg (fun () -> BU.print_string " >> HasMaskedEffect, not unfolding\n");
         no
 
-    // UnfoldTac means never unfold FVs marked [@"tac_opaque"]
-    | _, _, _, _, _, _ when cfg.steps.unfold_tac && BU.for_some (U.attr_eq U.tac_opaque_attr) attrs ->
-        log_unfolding cfg (fun () -> BU.print_string " >> tac_opaque, not unfolding\n");
-        no
-
     // Recursive lets may only be unfolded when Zeta is on
     | Some (Inr ({sigquals=qs; sigel=Sig_let {lbs=(is_rec, _)}}, _), _), _, _, _, _, _ when
             is_rec && not cfg.steps.zeta && not cfg.steps.zeta_full ->
@@ -1021,6 +1017,11 @@ let should_unfold cfg should_reify fv qninfo : should_unfold_res =
         in
         meets_some_criterion
 
+    // UnfoldTac means never unfold FVs marked [@"tac_opaque"]
+    | _, _, _, _, _, _ when cfg.steps.unfold_tac && BU.for_some (U.attr_eq U.tac_opaque_attr) attrs ->
+        log_unfolding cfg (fun () -> BU.print_string " >> tac_opaque, not unfolding\n");
+        no
+
     // Nothing special, just check the depth
     | _ ->
         default_unfolding()

tests/error-messages/AssertNorm.fst

@@ -0,0 +1,9 @@
+module AssertNorm
+
+(* The failure is in the assert_norm that's what should be highlighted. *)
+
+[@@expect_failure [19]]
+let f (x y z : int) =
+  assert_norm (x + x == y + y);
+  assert (x + y == y + x);
+  42

tests/error-messages/AssertNorm.fst.expected

@@ -0,0 +1,9 @@
+>> Got issues: [
+* Error 19 at AssertNorm.fst(7,2-7,13):
+  - Assertion failed
+  - The SMT solver could not prove the query. Use --query_stats for more details.
+  - See also AssertNorm.fst(7,14-7,30)
+
+>>]
+Verified module: AssertNorm
+All verification conditions discharged successfully

tests/error-messages/Bug1997.fst.expected

@@ -317,178 +317,178 @@ let _ = FStar.Pervasives.assert_norm (Bug1997.n0 == Bug1997.n1)
 ]
 
 >> Got issues: [
-* Error 19 at Bug1997.fst(13,19-13,55):
+* Error 19 at Bug1997.fst(13,27-13,38):
   - Assertion failed
   - The SMT solver could not prove the query. Use --query_stats for more details.
-  - Also see: prims.fst(96,32-96,42)
+  - See also Bug1997.fst(13,39-13,55)
 
 >>]
 >> Got issues: [
-* Error 19 at Bug1997.fst(21,19-21,67):
+* Error 19 at Bug1997.fst(21,27-21,38):
   - Assertion failed
   - The SMT solver could not prove the query. Use --query_stats for more details.
-  - Also see: prims.fst(96,32-96,42)
+  - See also Bug1997.fst(21,39-21,67)
 
 >>]
 >> Got issues: [
-* Error 19 at Bug1997.fst(29,19-29,63):
+* Error 19 at Bug1997.fst(29,27-29,38):
   - Assertion failed
   - The SMT solver could not prove the query. Use --query_stats for more details.
-  - Also see: prims.fst(96,32-96,42)
+  - See also Bug1997.fst(29,39-29,63)
 
 >>]
 >> Got issues: [
-* Error 19 at Bug1997.fst(38,19-38,65):
+* Error 19 at Bug1997.fst(38,27-38,38):
   - Assertion failed
   - The SMT solver could not prove the query. Use --query_stats for more details.
-  - Also see: prims.fst(96,32-96,42)
+  - See also Bug1997.fst(38,39-38,65)
 
 >>]
 >> Got issues: [
-* Error 19 at Bug1997.fst(39,19-39,65):
+* Error 19 at Bug1997.fst(39,27-39,38):
   - Assertion failed
   - The SMT solver could not prove the query. Use --query_stats for more details.
-  - Also see: prims.fst(96,32-96,42)
+  - See also Bug1997.fst(39,39-39,65)
 
 >>]
 >> Got issues: [
-* Error 19 at Bug1997.fst(40,19-40,65):
+* Error 19 at Bug1997.fst(40,27-40,38):
   - Assertion failed
   - The SMT solver could not prove the query. Use --query_stats for more details.
-  - Also see: prims.fst(96,32-96,42)
+  - See also Bug1997.fst(40,39-40,65)
 
 >>]
 >> Got issues: [
-* Error 19 at Bug1997.fst(41,19-41,65):
+* Error 19 at Bug1997.fst(41,27-41,38):
   - Assertion failed
   - The SMT solver could not prove the query. Use --query_stats for more details.
-  - Also see: prims.fst(96,32-96,42)
+  - See also Bug1997.fst(41,39-41,65)
 
 >>]
 >> Got issues: [
-* Error 19 at Bug1997.fst(42,19-42,65):
+* Error 19 at Bug1997.fst(42,27-42,38):
   - Assertion failed
   - The SMT solver could not prove the query. Use --query_stats for more details.
-  - Also see: prims.fst(96,32-96,42)
+  - See also Bug1997.fst(42,39-42,65)
 
 >>]
 >> Got issues: [
-* Error 19 at Bug1997.fst(51,19-51,59):
+* Error 19 at Bug1997.fst(51,27-51,38):
   - Assertion failed
   - The SMT solver could not prove the query. Use --query_stats for more details.
-  - Also see: prims.fst(96,32-96,42)
+  - See also Bug1997.fst(51,39-51,59)
 
 >>]
 >> Got issues: [
-* Error 19 at Bug1997.fst(52,19-52,59):
+* Error 19 at Bug1997.fst(52,27-52,38):
   - Assertion failed
   - The SMT solver could not prove the query. Use --query_stats for more details.
-  - Also see: prims.fst(96,32-96,42)
+  - See also Bug1997.fst(52,39-52,59)
 
 >>]
 >> Got issues: [
-* Error 19 at Bug1997.fst(53,19-53,59):
+* Error 19 at Bug1997.fst(53,27-53,38):
   - Assertion failed
   - The SMT solver could not prove the query. Use --query_stats for more details.
-  - Also see: prims.fst(96,32-96,42)
+  - See also Bug1997.fst(53,39-53,59)
 
 >>]
 >> Got issues: [
-* Error 19 at Bug1997.fst(54,19-54,59):
+* Error 19 at Bug1997.fst(54,27-54,38):
   - Assertion failed
   - The SMT solver could not prove the query. Use --query_stats for more details.
-  - Also see: prims.fst(96,32-96,42)
+  - See also Bug1997.fst(54,39-54,59)
 
 >>]
 >> Got issues: [
-* Error 19 at Bug1997.fst(55,19-55,59):
+* Error 19 at Bug1997.fst(55,27-55,38):
   - Assertion failed
   - The SMT solver could not prove the query. Use --query_stats for more details.
-  - Also see: prims.fst(96,32-96,42)
+  - See also Bug1997.fst(55,39-55,59)
 
 >>]
 >> Got issues: [
-* Error 19 at Bug1997.fst(63,19-63,51):
+* Error 19 at Bug1997.fst(63,27-63,38):
   - Assertion failed
   - The SMT solver could not prove the query. Use --query_stats for more details.
-  - Also see: prims.fst(96,32-96,42)
+  - See also Bug1997.fst(63,39-63,51)
 
 >>]
 >> Got issues: [
-* Error 19 at Bug1997.fst(64,19-64,51):
+* Error 19 at Bug1997.fst(64,27-64,38):
   - Assertion failed
   - The SMT solver could not prove the query. Use --query_stats for more details.
-  - Also see: prims.fst(96,32-96,42)
+  - See also Bug1997.fst(64,39-64,51)
 
 >>]
 >> Got issues: [
-* Error 19 at Bug1997.fst(75,19-75,49):
+* Error 19 at Bug1997.fst(75,27-75,38):
   - Assertion failed
   - The SMT solver could not prove the query. Use --query_stats for more details.
-  - Also see: prims.fst(96,32-96,42)
+  - See also Bug1997.fst(75,39-75,49)
 
 >>]
 >> Got issues: [
-* Error 19 at Bug1997.fst(76,19-76,49):
+* Error 19 at Bug1997.fst(76,27-76,38):
   - Assertion failed
   - The SMT solver could not prove the query. Use --query_stats for more details.
-  - Also see: prims.fst(96,32-96,42)
+  - See also Bug1997.fst(76,39-76,49)
 
 >>]
 >> Got issues: [
-* Error 19 at Bug1997.fst(77,19-77,49):
+* Error 19 at Bug1997.fst(77,27-77,38):
   - Assertion failed
   - The SMT solver could not prove the query. Use --query_stats for more details.
-  - Also see: prims.fst(96,32-96,42)
+  - See also Bug1997.fst(77,39-77,49)
 
 >>]
 >> Got issues: [
-* Error 19 at Bug1997.fst(78,19-78,49):
+* Error 19 at Bug1997.fst(78,27-78,38):
   - Assertion failed
   - The SMT solver could not prove the query. Use --query_stats for more details.
-  - Also see: prims.fst(96,32-96,42)
+  - See also Bug1997.fst(78,39-78,49)
 
 >>]
 >> Got issues: [
-* Error 19 at Bug1997.fst(87,19-87,49):
+* Error 19 at Bug1997.fst(87,27-87,38):
   - Assertion failed
   - The SMT solver could not prove the query. Use --query_stats for more details.
-  - Also see: prims.fst(96,32-96,42)
+  - See also Bug1997.fst(87,39-87,49)
 
 >>]
 >> Got issues: [
-* Error 19 at Bug1997.fst(88,19-88,49):
+* Error 19 at Bug1997.fst(88,27-88,38):
   - Assertion failed
   - The SMT solver could not prove the query. Use --query_stats for more details.
-  - Also see: prims.fst(96,32-96,42)
+  - See also Bug1997.fst(88,39-88,49)
 
 >>]
 >> Got issues: [
-* Error 19 at Bug1997.fst(89,19-89,49):
+* Error 19 at Bug1997.fst(89,27-89,38):
   - Assertion failed
   - The SMT solver could not prove the query. Use --query_stats for more details.
-  - Also see: prims.fst(96,32-96,42)
+  - See also Bug1997.fst(89,39-89,49)
 
 >>]
 >> Got issues: [
-* Error 19 at Bug1997.fst(90,19-90,49):
+* Error 19 at Bug1997.fst(90,27-90,38):
   - Assertion failed
   - The SMT solver could not prove the query. Use --query_stats for more details.
-  - Also see: prims.fst(96,32-96,42)
+  - See also Bug1997.fst(90,39-90,49)
 
 >>]
 >> Got issues: [
-* Error 19 at Bug1997.fst(91,19-91,49):
+* Error 19 at Bug1997.fst(91,27-91,38):
   - Assertion failed
   - The SMT solver could not prove the query. Use --query_stats for more details.
-  - Also see: prims.fst(96,32-96,42)
+  - See also Bug1997.fst(91,39-91,49)
 
 >>]
 >> Got issues: [
-* Error 19 at Bug1997.fst(92,19-92,49):
+* Error 19 at Bug1997.fst(92,27-92,38):
   - Assertion failed
   - The SMT solver could not prove the query. Use --query_stats for more details.
-  - Also see: prims.fst(96,32-96,42)
+  - See also Bug1997.fst(92,39-92,49)
 
 >>]
 Module after type checking:

ulib/FStar.Classical.fst

@@ -72,7 +72,9 @@ let impl_intro_gen #p #q f =
 
 (*** Universal quantification *)
 let get_forall #a p =
-  assert_norm ((forall (x: a). p x) == squash ((x: a -> GTot (p x))));
+  let t = (forall (x:a). p x) in
+  assert (norm [delta; delta_only [`%l_Forall]] t == (squash (x:a -> GTot (p x))));
+  norm_spec [delta; delta_only [`%l_Forall]] t;
   get_squashed #(x: a -> GTot (p x)) (forall (x: a). p x)
 
 (* TODO: Maybe this should move to FStar.Squash.fst *)