K-user mailing list

[Abdul Dakkak <abduld AT wolfram.com>]

I have a simple k file that defines a `MY` language. My question is why the 
following does not work

module MY-SYNTAX
  syntax Integer ::= Int
  syntax Literal ::= String
                   | Integer
                   | Real
  syntax Identifier ::= Id
                      | ":" Id
  syntax Value ::= Identifier
                 | Literal
  syntax AExpr ::=
                  Expr "+" Expr           [left, strict]
                | Expr "-" Expr           [left, strict]
                | Expr "/" Expr           [left, strict]
                | Expr "*" Expr           [left, strict]
  syntax Expr ::= Value
                | "(" Expr ")"            [bracket]
                > AExpr
                > Identifier "=" Expr     [strict(2), right]
endmodule

module MY
  imports MY-SYNTAX
  syntax KResult ::= Literal

  configuration <T color="yellow">
                  <k color="green"> $PGM:K </k>
                  <env color="LightSkyblue"> .Map </env>
                  <store color="red"> .Map </store>
                </T>
  rule <k>X:Identifier = E => . ...</k>
       <env> ... Rho => Rho[N/X] </env>
       <store> ... . => (N |-> E) ... </store>
    when fresh(N:Int)
  rule I1:Int + I2:Int => I1 +Int I2
endmodule


If I inline the AExpr then it works fine

module MY-SYNTAX
  syntax Integer ::= Int
  syntax Literal ::= String
                   | Integer
                   | Real
  syntax Identifier ::= Id
                      | ":" Id
  syntax Value ::= Identifier
                 | Literal
  syntax Expr ::= Value
                | "(" Expr ")"            [bracket]
                > AExpr
                > Expr "+" Expr           [left, strict]
                > Expr "-" Expr           [left, strict]
                > Expr "/" Expr           [left, strict]
                > Expr "*" Expr           [left, strict]
                > Identifier "=" Expr     [strict(2), right]
endmodule

module MY
  imports MY-SYNTAX
  syntax KResult ::= Literal

  configuration <T color="yellow">
                  <k color="green"> $PGM:K </k>
                  <env color="LightSkyblue"> .Map </env>
                  <store color="red"> .Map </store>
                </T>
  rule <k>X:Identifier = E => . ...</k>
       <env> ... Rho => Rho[N/X] </env>
       <store> ... . => (N |-> E) ... </store>
    when fresh(N:Int)
  rule I1:Int + I2:Int => I1 +Int I2
endmodule


the example does not fail on kompile, but on krun with this simple program

g = 1 + 2

any insight is appreciated.

-adk-