为什么值的列表在K的LLVM后台不酷？

Question

在尝试定义类似Scheme语言的语法时，我发现用java后端编译文件的运行结果是

kompile --backend java scheme.k -d .

与llvm后端不同的行为。

kompile --backend llvm scheme.k -d .

这是我的scheme.k.的代码。

module SCHEME-COMMON
  imports DOMAINS-SYNTAX

  syntax Name ::= "+" | "-" | "*" | "/"
                | "display" | "newline"

  syntax Names ::= List{Name," "}

  syntax Exp ::= Int | Bool | String | Name
               | "[" Name Exps "]"                 [strict(2)]

  syntax Exps  ::= List{Exp," "}                   [strict]
  syntax Val
  syntax Vals ::= List{Val," "}
  syntax Bottom
  syntax Bottoms ::= List{Bottom," "}

  syntax Pgm ::= Exp Pgm            [strict(1)] 
               | "eof"

endmodule


module SCHEME-SYNTAX
  imports SCHEME-COMMON
  imports BUILTIN-ID-TOKENS

  syntax Name ::= r"[a-z][_a-zA-Z0-9]*"           [token, prec(2)]
                | #LowerId                        [token]
endmodule


module SCHEME-MACROS
  imports SCHEME-COMMON

endmodule


module SCHEME
  imports SCHEME-COMMON
  imports SCHEME-MACROS
  imports DOMAINS

  configuration <T color="yellow">
                  <k color="green"> $PGM:Pgm </k>
                  <env color="violet"> .Map </env>
                  <store color="white"> .Map </store>
                  <input color="magenta" stream="stdin"> .List </input>
                  <output color="brown" stream="stdout"> .List </output>
                </T>

  syntax Val ::= Int | Bool | String
  syntax Exp ::= Val
  syntax Exps ::= Vals
  syntax Vals ::= Bottoms
  syntax Exps ::= Names
  syntax Names ::= Bottoms
  syntax KResult ::= Vals | Val

  rule _:Val P:Pgm => P
    when notBool(P ==K eof)
  rule V:Val eof => V

  rule [+ I1 I2 Vals] => [+ (I1 +Int I2) Vals]              [arith]
  rule [+ I .Vals] => I                                     [arith]
  rule [- I1 I2 Vals] => [- (I1 -Int I2) Vals]              [arith]
  rule [- I .Vals] => I                                     [arith]
  rule [* I1 I2 Vals] => [* (I1 *Int I2) Vals]              [arith]
  rule [* I .Vals] => I                                     [arith]
  rule [/ I1 I2 Vals] => [/ (I1 /Int I2) Vals]
    when I2 =/=K 0                                          [arith]
  rule [/ I .Vals] => I                                     [arith]

  rule <k> [newline .Exps] => "" ...</k>
       <output>... .List => ListItem("\n") </output>        [io]

  rule <k> [display V:Val] => "" ...</k>
       <output>... .List => ListItem(V) </output>           [io]

endmodule

这是我要运行的测试文件:

[display 8]
eof

奇怪的是，用java编译的版本可以正常运行这个测试用例， 而用llvm编译的版本则停留在... ...

<k>
    8  .Bottoms ~> #freezer[__]_SCHEME-COMMON_Exp_Name_Exps0_ ( display ) ~> #freezer___SCHEME-COMMON_Pgm_Exp_Pgm1_ ( eof )
</k>

可能的原因是什么？kompile的版本信息是

RV-K version 1.0-SNAPSHOT
Git revision: a7c2937
Git branch: UNKNOWN  
Build date: Wed Feb 12 09:46:03 CST 2020

Answer 1

在LLVM和Haskell后端中，有两个制作说是 过载 当它们共享相同的arity和klabel属性，并且一个产品的所有参数种类小于或等于另一个产品的参数种类，并且第一个产品的结果种类小于另一个产品的结果时，它们就会相互匹配。在匹配过程中，要特别考虑超载的项。例如，在你的例子中，如果一个Exps的列表和一个Vals的列表被说成是超载的，那么如果你有一个模式 V:Vals，它将符合术语 V:Val, .Exps 某种 Exps.

默认情况下，Java后端假设所有的Lists之间的sorts，都有一个subsort关系过载。然而，LLVM和Haskell后端并不做这个假设。因此，如果你给你的Exps List和Vals list赋予相同的klabel属性，你的例子就会工作。我们没有在llvm后端做同样的事情，因为我们发现，它往往会在你不期望的地方导致你的语法出现严重的歧义。

比如说

module SCHEME-COMMON
  imports DOMAINS-SYNTAX

  syntax Name ::= "+" | "-" | "*" | "/"
                | "display" | "newline"

  syntax Names ::= List{Name," "}                  [klabel(exps)]

  syntax Exp ::= Int | Bool | String | Name
               | "[" Name Exps "]"                 [strict(2)]

  syntax Exps  ::= List{Exp," "}                   [strict, klabel(exps)]
  syntax Val
  syntax Vals ::= List{Val," "}                    [klabel(exps)]
  syntax Bottom
  syntax Bottoms ::= List{Bottom," "}              [klabel(exps)]

  syntax Pgm ::= Exp Pgm            [strict(1)] 
               | "eof"

endmodule