Normalize sub-terms of a `match`

[W95Psp]

Hi,

I've noticed that normalizing a term blocks whenever the normalizer encounters a match (well, I think so at least), for instance :

module Test
open FStar.Tactics

let foo x = 2 + x

let f y = match y with
    | true -> foo 1
    | false -> foo 2

let s: string = _ by (
  let t = norm_term [primops;iota;zeta;delta] (`f) in //`
  let s = term_to_string t in
  exact (quote s)
)
let _ = assert (
  s == "fun y ->
  (match y with
    | true -> Test.foo 1
    | false -> Test.foo 2)
  <:
  Prims.int"
)

Is this behaviour normal? If it's the case, how do I normalize "inside" matches?

Normalization by evaluation works in this case, however, I need selective normalization and nbe is failing in my actual terms (I get de Bruijn index out of bounds error).

Thanks :)

[mtzguido]

This is caused by this change to the delta level when descending into the branches of an irreducible match, cf. https://github.com/FStarLang/FStar/blob/655aab8b44d4274dd60e4867da4ed833c0e6eaf8/src/typechecker/FStar.TypeChecker.Normalize.fs#L2405-L2421

Not sure why this is in place, maybe @nikswamy knows. I can try to fiddle with this in a couple of days.

[nikswamy]

That's also a surprise to me ... I do recall that we disable zeta in the bodies of unreduced matches (to prevent loops) but not sure why other delta reduction is forbidden. Will investigate.

[W95Psp]

Oh, right, make sense, looking at that part of the code! Thanks for pointing it out (I get lost very fast in F* compiler sources), I'll make a dirty patch for now to get what I'm doing working :)

[mtzguido]

So as far as I can tell, simply disabling zeta is enough to prevent looping, and we do not need to touch the delta level. However, I got a few regression with that patch (ef70220e7475fe17f559b3c6622db2fdc625277a / bc71397009e40b5cb9555624fdf175544288aba3), which I think are just size explosions. It's not that anything loops, but that now reduction can unfold more things exponentially. See this example:

module Blow

open FStar.Tactics

assume val x : bool

let dup (a:int) : int = if x then a else a

let big = dup (dup (dup (dup (dup (dup (dup (dup (dup (dup (dup (dup (dup (dup (dup (dup (dup (dup (dup 0))))))))))))))))))

let test () =
    assert True by
        (let t = `big in
         let t' = norm_term [delta] t in
         print ("t  = " ^ term_to_string t);
         print ("t' = " ^ term_to_string t'))

Before this patch, it would print:

TAC>> t  = Blow.big
TAC>> t' = (if Blow.x
  then
    Blow.dup (Blow.dup (Blow.dup (Blow.dup (Blow.dup (Blow.dup (Blow.dup (Blow.dup (Blow.dup (Blow.dup 
                                          (Blow.dup (Blow.dup (Blow.dup (Blow.dup (Blow.dup (Blow.dup 
                                                                  (Blow.dup (Blow.dup 0)))))))))))))
                  ))))
  else
    Blow.dup (Blow.dup (Blow.dup (Blow.dup (Blow.dup (Blow.dup (Blow.dup (Blow.dup (Blow.dup (Blow.dup 
                                          (Blow.dup (Blow.dup (Blow.dup (Blow.dup (Blow.dup (Blow.dup 
                                                                  (Blow.dup (Blow.dup 0)))))))))))))
                  )))))
<:
Prims.Tot Prims.int
Verified module: Blow
All verification conditions discharged successfully

Simply unfolding the dup once, and then being blocked since it appears under a match. Now as you can probably guess, with the patch we get an exponential explosion:

TAC>> t  = Blow.big
TAC>> t' = (if Blow.x
  then
    if Blow.x
    then
      if Blow.x
      then
        if Blow.x
        then
          if Blow.x
          then
            if Blow.x
            then
              if Blow.x
              then
                if Blow.x
                then
                  if Blow.x
                  then
                    if Blow.x
                    then
                      if Blow.x
                      then
                        if Blow.x
                        then
                          if Blow.x
                          then
                            if Blow.x
                            then
                              if Blow.x
                              then
                                if Blow.x
                                then
                                  if Blow.x
                                  then
                                    if Blow.x
                                    then if Blow.x then 0 else 0
                                    else if Blow.x then 0 else 0
                                  else
                                    if Blow.x
             (* ... 786388 more lines ... *)
                                    then if Blow.x then 0 else 0
                                    else if Blow.x then 0 else 0)
<:
Prims.Tot Prims.int
Verified module: Blow
All verification conditions discharged successfully

This seems like expected behaviour to me. but it does cause regressions in at least StringPrinterTest.Aux (which I think we can just disable...) and LowStar.BufferView.Down.fst. By regressions I mean they never come back.

Any thoughts?