K-user mailing list

[Gurvan Le Guernic <gleguern AT gmail.com>]

   Hi,

 I'm experimenting with K4. With the following definition :

module POINTS-DSL-SYNTAX

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

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

module POINTS-DSL
  imports POINTS-DSL-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

 

  rule { P:Point ; T:PointExpInnerSet } => { P } U { T }

  // Using my own 'PointSet' to handle point sets
  syntax PointSet ::= "[" PointInnerSet "]"
  syntax PointInnerSet ::= Point | Point ";" PointInnerSet
  //syntax PointExpInnerSet ::= PointInnerSet // I now get an error with this line
  syntax PointSetExp ::= PointSet
  syntax KResult ::= PointSet
 
  rule { P:Point } => [ P ]

  syntax PointInnerSet ::= "merge" "(" PointInnerSet "&" PointInnerSet ")"   [function]
  rule merge( P1:Point & P2:Point ) => P1 ; P2 requires P1 =/=K P2
  rule merge( P1:Point & P2:Point ) => P1 requires P1 ==K P2
  rule merge( P1:Point ; Tail:PointInnerSet & P2:Point ) => P1 ; merge( Tail & P2 )
    requires P1 =/=K P2
  rule merge( P1:Point ; Tail:PointInnerSet & P2:Point ) => P1 ; Tail
    requires P1 ==K P2
  rule merge( S:PointInnerSet & P2:Point ; Tail:PointInnerSet ) => merge( merge( S & P2 ) & Tail )
 
  rule [ S1:PointInnerSet ] U [ S2:PointInnerSet ] => [ merge( S1 & S2 ) ]
 
endmodule

I get the following compilation error :

[Error] Compiler: Had 1 parsing errors.
[Error] Inner Parser: Parse error: unexpected end of file.
    Source(/mnt/partage/offices/gurvan/PFPML/K-definitions/points/./points-DSL.k4)
    Location(...,55,...,56)

If I replace the last rule by the following one :

  rule [ S1:PointInnerSet ] U [ S2:PointInnerSet ] => [ ( merge( S1 & S2 ) ) ]

compilation goes thru, but I get parentheses added everywhere. For example, the following program :

{ (2,4) } U { ( 5,5)} U { ( 2,5) ;  (3,3)} U {(7,8)}

produces :

<k> [ ( 2 , 4 ) ; ( ( 5 , 5 ) ; ( ( 2 , 5 ) ; ( ( 3 , 3 ) ; ( 7 , 8 ) ) ) ) ] </k>

Why do I get the compilation error and how do I fix it ?

   Thanks,

   Gurvan