K-user mailing list

[Andrei Stefanescu <stefane1 AT illinois.edu>]

Hi Gurvan,

The issue you encountered is a limitation of K with regard to subsorting. The fix is to add the following extra subsort relation

  syntax PointExpInnerList ::= PointInnerList

to the definition. What happens is that with the current definition, "( 5 , 5 ) ; ( 2 , 4 )" has both sorts PointInnerList and PointExpInnerList. When K computes its least sort as the intersection of the two sorts, that intersection is Point. By adding the subsort relation above, the intersection becomes PointInnerList, and everything works.

We can detect and report this error, but unfortunately we did not prioritize it. I apologize for the trouble it caused you.

Andrei

On Thu, Sep 15, 2016 at 12:22 PM Gurvan Le Guernic <gleguern AT gmail.com> wrote:

   Hi,

 For the debugger, I just run "krun --debugger simple.points". I use K4.0

 $ krun --version
K framework version 4.0.0
Git revision: d310c7a
Git branch: v4.0.0
Build date: Thu Jul 28 04:10:26 CEST 2016

and java 1.8

$ java -version
java version "1.8.0_101"
Java(TM) SE Runtime Environment (build 1.8.0_101-b13)
Java HotSpot(TM) 64-Bit Server VM (build 25.101-b13, mixed mode)

Here's the output of kast -v

kast -v simple.points
Parse command line options                                   =    34
`___`(`{_}`(`___`(`(_,_)`(#token("0","Int"),#token("1","Int")),`+`(.KList),`___`(`(_,_)`(#token("4","Int"),#token("6","Int")),`/`(.KList),#token("2","Int")))),`U`(.KList),`___`(`{_}`(`(_,_)`(#token("5","Int"),#token("5","Int"))),`U`(.KList),`{_}`(`(_,_)`(#token("2","Int"),#token("4","Int")))))
Cleanup                                                      =  3715
Total                                                        =  3749
[Warning] Inner Parser: Parsing ambiguity. Arbitrarily choosing the first.
1: syntax PointSetExp ::= PointSetExp PsPsOp PointSetExp
[Location(#token("16",Int),#token("26",Int),#token("16",Int),#token("77",Int))
Source(#token("/mnt/partage/offices/gurvan/PFPML/K-definitions/points/./points-DSML.k4",KString))
klabel(#token("___",KString)) strict(#token("1,3",AttributeValue))]
  
___({_}(___((_,_)(#token(Int,"0"),#token(Int,"1")),+(),(_)(___((_,_)(#token(Int,"4"),#token(Int,"6")),/(),#token(Int,"2"))))),U(),___({_}((_,_)(#token(Int,"5"),#token(Int,"5"))),U(),{_}((_,_)(#token(Int,"2"),#token(Int,"4")))))
2: syntax PointSetExp ::= PointSetExp PsPsOp PointSetExp
[Location(#token("16",Int),#token("26",Int),#token("16",Int),#token("77",Int))
Source(#token("/mnt/partage/offices/gurvan/PFPML/K-definitions/points/./points-DSML.k4",KString))
klabel(#token("___",KString)) strict(#token("1,3",AttributeValue))]
  
___(___({_}(___((_,_)(#token(Int,"0"),#token(Int,"1")),+(),(_)(___((_,_)(#token(Int,"4"),#token(Int,"6")),/(),#token(Int,"2"))))),U(),{_}((_,_)(#token(Int,"5"),#token(Int,"5")))),U(),{_}((_,_)(#token(Int,"2"),#token(Int,"4"))))
    Source(/mnt/partage/offices/gurvan/PFPML/K-definitions/points/./simple.points)
    Location(1,1,1,49)

Oddly, the value of "Parse command line options" changes every time I run the above command (40, 32, 34, ...) as well as for "Cleanup" and "Total".

 There is an ambiguity about the associativity of 'U' but it seems to be all.

 From the debugger, it really seems that K maps "P2:Point" to "( 5 , 5 ) ; ( 2 , 4 )", adds parentheses around it (I have problems with automatically added parentheses especially when using '[function]') and put it back on the right side (where P2 stands).

 I used the work-around of expanding "P2:Point" into "( X2:Int , Y2:Int )" (and similar expansions), but it is only a work-around.

    Thanks,

    Gurvan

2016-09-15 18:50 GMT+02:00 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