K-user mailing list

[Charles Jacobsen <charlie.jacobsen AT utah.edu>]

When I kompile and krun the following, the k cell does not reduce to true, as I was expecting. Notice that I did not include a rule for foo when the input is an integer, so foo(5) cannot reduce.

module TEST

  syntax Val  ::= Int | Bool

  // Using the [function] attribute on foo.
  syntax Bool ::= "foo" "(" Val ")" [function]
  rule foo(B:Bool) => B

  syntax Bool ::= "is-bool" "(" Val ")" [function]
  rule is-bool(B:Bool) => true
  rule is-bool(I:Int) => false

  // This expr will not reduce to true.
  configuration <k> is-bool( foo(5) ) </k>

endmodule

The k-cell in the following -does- reduce when the [function] attribute is removed from foo:

module TEST

  syntax Val  ::= Int | Bool

  // Using the [function] attribute on foo.
  syntax Bool ::= "foo" "(" Val ")"
  rule foo(B:Bool) => B

  syntax Bool ::= "is-bool" "(" Val ")" [function]
  rule is-bool(B:Bool) => true
  rule is-bool(I:Int) => false

  // This expr will not reduce to true.
  configuration <k> is-bool( foo(5) ) </k>

endmodule

I'm trying to use andBool inside 'when' conditions without needing to worry about whether all terms reduce (if one reduces to false, that should be sufficient).

Thanks guys, Charlie