GaloisInc/daedalus

Determinization gets iterated

benoitrazet opened this issue · 1 comments

The determinization is attempted when a biased/unbiased or is encountered. Currently this process is not iterated on the result of a determinization which prevents the determinization to apply in some cases.

See CrossRefEntry in pdf-simple for an instance of this issue:

proc CrossRefEntry() : CrossRefEntry =
  do ...
     do _x0 <- match1 { ... }
        case _x0 of
          0 ->
            try
              match1_ $cr()
            else
              match1_ $lf()
          9 ->
            try
              match1_ $cr()
            else
              match1_ $lf()
          12 ->
            try
              match1_ $cr()
            else
              match1_ $lf()
          13 ->
            match1_ $lf()
          32 ->
            try
              match1_ $cr()
            else
              match1_ $lf()
          _ ->
            fail_sys @()
     pure $$

This issue got resolved with this commit 1c79296