K-user mailing list

[Eric Huber <echuber2 AT illinois.edu>]

The first thing that jumps out at me is you have a parsing ambiguity between PointInnerList and PointExpInnerList. You should check what kast -v shows you to see. By the way, how did you get the debugger to work? I haven't been able to show me anything but bytecode or something.

Regards

Eric Huber

On Thu, Sep 15, 2016 at 9:16 AM, Gurvan Le Guernic <gleguern AT gmail.com> wrote:

   Hi,

 I'm experimenting with K4.0. It seems I've hit a bug (If not checking rule types is a bug).

 I have the following K definition :

module POINTS-DSML-SYNTAX

  syntax Point ::= "(" Int "," Int ")"
  syntax PointExp ::= Point
                 |  PointExp PointPointOp PointExp   [strict(1,3)]
           |  PointExp PointIntOp Int          [strict(1)]
           |  "(" PointExp ")"                 [bracket]
  syntax PointPointOp ::= "+" | "-"
  syntax PointIntOp ::= "*" | "/"

  syntax PointExpInnerList ::= PointExp
                   |  PointExp ";" PointExpInnerList   [strict]
  syntax PointExpSet ::= "{" PointExpInnerList "}"              [strict]
  syntax PointSetExp ::= PointExpSet
                 |  PointSetExp PsPsOp PointSetExp         [strict(1,3)]
              |  "(" PointSetExp ")"                    [bracket]
  syntax PsPsOp ::= "U"
         
endmodule

module POINTS-DSML
  imports POINTS-DSML-SYNTAX

  configuration
    <k> $PGM:K </k>

  syntax KResult ::= Point

  rule ( X1:Int , Y1:Int ) + ( X2:Int , Y2:Int ) => ( X1 +Int X2 , Y1 +Int Y2 )
  rule ( X1:Int , Y1:Int ) - ( X2:Int , Y2:Int ) => ( X1 -Int X2 , Y1 -Int Y2 )

  rule ( X:Int , Y:Int ) * I:Int => ( X *Int I , Y *Int I )
  rule ( X:Int , Y:Int ) / I:Int => ( X /Int I , Y /Int I ) requires I =/=Int 0

  // Using my own 'PointSet' to handle point sets
  syntax PointInnerList ::= Point | Point ";" PointInnerList
  syntax PointSet ::= "[" PointInnerList "]"
  syntax PointSetExp ::= PointSet
  syntax KResult ::= PointSet
  rule { P:Point } => [ P ]
  rule [ P1:Point ] U [ P2:Point ] => [ P1 ; P2 ] requires P1 =/=K P2
  rule [ P1:Point ] U [ P2:Point ] => [ P1 ] requires P1 ==K P2
 
endmodule

When executing the program :

{ (0,1) + ( (4,6) / 2) } U { ( 5,5)} U { ( 2,4)}

 

in debug mode, I get the following trace :

...
 KDebug> peek
<k> [ ( 2 , 4 ) ] U [ ( 5 , 5 ) ; ( 2 , 4 ) ] </k>
KDebug> step
1 Step(s) Taken.
KDebug> peek
<k> [ ( 2 , 4 ) ; ( ( 5 , 5 ) ; ( 2 , 4 ) ) ] </k>

K4.0 seems to be applying rule "rule [ P1:Point ] U [ P2:Point ] => [ P1 ; P2 ] requires P1 =/=K P2" with P2 equal to "( ( 5 , 5 ) ; ( 2 , 4 ) )" which imho is not a "Point".

Imho, I would expect the computation to be stuck at "<k> [ ( 2 , 4 ) ] U [ ( 5 , 5 ) ; ( 2 , 4 ) ] </k>". Is there a bug, or am I misunderstanding something ?

   Thanks for the feedback and the great framework,

   Gurvan Le Guernic