[Bug] Id created by String2Id contains quotation marks

[david-k]

K Version

K version:    v5.1.250-0-g07918e142
Build date:   Sat Nov 06 22:18:15 CET 2021

Description

The Id created by String2Id("x") is "x", i.e., the Id includes the quotation marks of the string, which seems wrong. This behavior is demonstrated by the following example:

module STRING2ID
  imports ID
  imports BOOL
  imports K-EQUAL
  imports STRING

  syntax Bool ::= "test" [function]
  
  // Evaluates to true
  rule test => String2Id("x") ==K #token("\"x\"", "Id")
endmodule

[Baltoli]

Both the Haskell and LLVM backends produce the same behaviour on this example, FWIW.

[dwightguth]

FYI, this is not actually a bug in the String2Id hook. If you look at the output of krun -cPGM='String2Id("x")', you will see that String2Id actually behaves correctly. So I can only assume the problem involves the translation of the #token

[david-k]

@dwightguth That's strange, because rule test => String2Id("x") results in the Id "x", i.e., including the quotation marks. So it seems to depend on whether String2Id is part of a program or part of a rule.

[dwightguth]

Interesting. That's quite surprising since the parser used by -cPGM and by the rule parser is generally pretty similar. Thanks for the info though. We'll definitely make sure to triage this when we meet on Thursday.

[radumereuta]

Most likely something in the front-end. Needs more investigation.
Should be simple to figure out what is going on.

[ehildenb]

I have confirmed that this si still hapenning on K version 5.4.30:

Inptu file test.k:

module TEST 
  imports ID
  imports BOOL
  imports K-EQUAL
  imports STRING

  syntax Bool ::= "test" [function]

  // Evaluates to true
  rule test => String2Id("x") ==K #token("\"x\"", "Id")
endmodule

Input file in.test:

test

Reproduction:

% kompile test.k
[Warning] Compiler: Could not find main syntax module with name TEST-SYNTAX in
definition.  Use --syntax-module to specify one. Using TEST as default.

% krun in.test
<k>
  true ~> .
</k>

It should be outputting false.

[radumereuta]

@Baltoli is this safe to close?
I don't know why GH didn't close it automatically.