Case match fails to match 0

[eelcovisser]

The case statement below never enters the case for 0, if when i is 0.

 IfThen(IntV(i), e) --> v
  where
    printS(concatS("IfThen: ", printI(i))) => _;
    case i of {
      0 => 
        printS("zero") => _;
        UnitV() => v
      1 => 
        printS("one") => _;
        e --> v
      otherwise =>
        printS("no match") => _
    }.

[vvergu]

Very strange. Does it enter the 1 case? On Sun, 13 Nov 2016 at 15:18, Eelco Visser notifications@github.com wrote:

The case statement below never enters the case for 0, if when i is 0.

IfThen(IntV(i), e) --> v where printS(concatS("IfThen: ", printI(i))) => ; case i of { 0 => printS("zero") => ; UnitV() => v 1 => printS("one") => ; e --> v otherwise => printS("no match") => }.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/metaborg/dynsem/issues/124, or mute the thread https://github.com/notifications/unsubscribe-auth/AC0GA2Cpl4AfDdC53oYJYR5qOiNiIDh-ks5q9w4UgaJpZM4KwsFu .

[eelcovisser]

yes

[vvergu]

Thanks for reporting, i'll investigate.

[vvergu]

I cannot recreate this issue. I've built a DynSem rule that's similar to yours:

  Ifz(NumV(ci), e1, e2) --> v
  where
    case ci of {
      0 =>
        printS("zero") => _;
        e1 --> v
      1 =>
        printS("one") => _;
        e2 --> v
      otherwise =>
        printS("otherwise") => _;
        e2 --> v
    }.

And for an example program:

let
  iszero = a -> ifz(a) then 1 else 0
in {
  iszero(0)
  ;iszero(1)
  ;iszero(42)
}

The interpreter outputs:

zero
one
otherwise
NumV_1(0)

which is what i would expect.

[eelcovisser]

I'll compose a commit of tiger to reproduce it.

[vvergu]

Thanks.

[eelcovisser]

Here is an other example. With this order of the matches (no otherwise), I get failure. If I interchange the order (1 first), I get the correct behavior. Try your example without the otherwise.

  initArray(i, j, v, I) --> I'
  where 
    printS(concatS(concatS("initArray: ", printI(i)), concatS(" - ", printI(j)))) => _;
    case ltI(i, j) of {
      0 => 
        printS("0") => _;
        I => I'
      1 => 
        printS("1") => _; 
        allocate(v) --> a;
        initArray(addI(i, 1), j, v, {i |--> a, I}) --> I'
    }.

[eelcovisser]

Same behavior for this rule:

  IfThen(IntV(i), e) --> v
  where
    case i of {
      1 => e --> v
      0 => UnitV() => v
    }.

i.e. it succeeds in this order, but fails in the other order.

[eelcovisser]

See this commit:

https://github.com/MetaBorgCube/metaborg-tiger/commit/2fe0937ee777c0ec2d56b9731e57abc47cfc761f

and this program

https://github.com/MetaBorgCube/metaborg-tiger/blob/master/org.metaborg.lang.tiger.examples/xmpl/eval-test2.tig

behavior of If_3 is all over the place; I cannot detect a system; something is wrong with case.

[vvergu]

I have finally managed to confirm this issue. While i couldn't recreate it in Tiger (because of other errors) i managed to do it with Simpl.

Simpl equivalent

Here's the factorial program in Simpl:

let
  recf = box(-1)
in {
  let
    f = box(
      n -> 
        ifz(n)
        then 1
        else {
          let
            newn = n - 1
          in
            (n * unbox(recf)(newn))
        }
      )
  in {
    setbox(recf, unbox(f))
    ;unbox(f)(2)
  }
}

and here's the spec for Ifz:

  Ifz(NumV(i), e1, e2) --> v
  where
    printS(concatS("Ifz: ", i2s(i))) => _;
    case i of {
      0 =>
        printS("If => 0") => _;
        e1 --> v
      1 =>
        printS("If => 1") => _;
        e2 --> v
      otherwise =>
        printS("If => otherwise") => _;
        e2 --> v
    };
    printS("------------------") => _.

Analysis

There's only one behavior pattern that i can spot, namely that it works correctly on first invocation and incorrectly in subsequent invocations.

For example for factorial of 0 (unbox(f)(0)) the program correctly prints:

Ifz: 0
If => 0
------------------
NumV_1(1)

For factorial of 1 (unbox(f)(1)) the program correctly prints the first iteration but incorrectly prints the second iteration and never terminates:

Ifz: 1
If => 1
Ifz: 0
If => otherwise
Ifz: -1
If => otherwise
Ifz: -2
If => otherwise
Ifz: -3
...

A similar pattern can be observed for factorial of 2 (unbox(f)(2)) where we come from the otherwise case into a special case. The program correctly prints the otherwise case but incorrectly matches the subsequent two iterations, and never terminates:

Ifz: 2
If => otherwise
Ifz: 1
If => otherwise
Ifz: 0
If => otherwise
Ifz: -1
If => otherwise
Ifz: -2
If => otherwise
Ifz: -3
...

[vvergu]

An even smaller example can be obtained by replacing the Ifz rule with the following:

signature
  constructors
    IfzV : Int * Exp * Exp -> Exp

rules

  Ifz(NumV(i), e1, e2) --> IfzV(i, e1, e2)
  where
    printS(concatS("Ifz: ", i2s(i))) => _.

  IfzV(0, e1, _) --> e1
  where
    printS("If => 0") => _.

  IfzV(1, _, e2) --> e2
  where
    printS("If => 1") => _.

  IfzV(i, _, e2) --> e2
  where
    i != 0;
    i != 1;
    printS("If => otherwise") => _.

And the program with:

let
  iszero = a -> ifz(a) then 1 else 0
in {
  iszero(1)
  ;iszero(0)
}

I expect the program to succeed with NumV(1), instead the interpreter crashes with:

Ifz: 1
If => 1
Ifz: 0
Exception in thread "main" org.metaborg.meta.lang.dynsem.interpreter.nodes.rules.ReductionFailure: No rules applicable for term IfzV_3(0, Lit_1(1), Lit_1(0))
Frame: IfzV_3_Term -default-> 
Frame: Ifz_3_Term -default-> 
Frame: App_2_Term -default-> 
Frame: List_IExpTerm -default-> 
Frame: Block_1_Term -default-> 
Frame: Let_3_Term -default-> 
Frame: Program_1_Term -init->