kframework - K 框架:无法转换为子类型
问题描述
我正在尝试将表达式评估为值(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 ) ~> ..
但在这里它又卡住了。
我应该如何解决这个问题?
解决方案
将 和 的产生式放在Exps
同Vals
一个模块中,并赋予它们相同的klabel
属性。这将使它们彼此过载,此时, .Values 是 KResult 的事实应该可以解决您的问题。
推荐阅读
- android - 在 raspberryPi 上通过 REST 保存图像以进行图像识别
- docker - 为 Windows Server 2016 升级 Docker EE
- kotlin - Kotlin:字符串包含特定符号之一
- javascript - 我想在 html 下拉列表中显示 JSON 数据键(不是值)
- tfs - 防止在 Gated 版本上发布添加的工件
- bash - 接收后挂钩内的 Git 标记
- python - get the last column in every file using open
- javascript - Streaming data from Firebase Realtime Database
- symfony - Sonata 管理员添加类以编辑表单
- java - 何时提交事务?