kframework - K 框架：无法转换为子类型

Question

我正在尝试将表达式评估为值（Exps ::= Values）以进行函数调用。

这是一个简单的例子：

module ERL-SYNTAX

  imports INT-SYNTAX
  imports STRING
  syntax Atom ::= "main" | "f"
  syntax Exp ::=  Atom | Int
  syntax Exp ::= Exp "(" Exps ")"             [seqstrict]
  syntax Exps ::= List{Exp, ","}              [seqstrict]

endmodule

module ERL-CONFIGURATION

  imports ERL-SYNTAX
  imports MAP

  syntax Value ::=  Atom | Int | "{" Values "}"
  syntax Values ::= List{Value, ","}
  syntax Exp ::= Value
  syntax Exps ::= Values
  syntax KResult ::= Value
  syntax KResult ::= Values

  configuration <cfg color="yellow">
                  <k color="green"> $PGM:Exp </k>
                  <fundefs> //some default function definitions
                    .Map (f |-> 5 , .Exps 
                    main |-> f ( 2 , 3 , .Exps ) , .Exps )
                  </fundefs>
                </cfg>
endmodule

module ERL

  imports ERL-SYNTAX
  imports ERL-CONFIGURATION

  //rule .Exps => .Values
  rule <k>F:Atom(_:Values) =>  L ...</k>
       <fundefs>...  F |-> L ...</fundefs>

endmodule

这被困在

.Exps ~> #freezer_(_) ERL-SYNTAX1 ( main )

所以我尝试了这条规则：.Exps => .Values 来评估 main()。

对我来说，奇怪的是，这次加热 3 是可以的：

.Values ~> #freezer_, ERL-SYNTAX1 ( 3 ) ~> #freezer ,_ ERL-SYNTAX1 ( 2 ) ~> ...

将会

3 , .Values ~> #freezer_,_ ERL-SYNTAX1 ( 2 ) ~> ..

但在这里它又卡住了。

我应该如何解决这个问题？

Answer 1

将 和 的产生式放在Exps同Vals一个模块中，并赋予它们相同的klabel属性。这将使它们彼此过载，此时， .Values 是 KResult 的事实应该可以解决您的问题。