kframework - 如何正确重用其他类型的产品？

Question

我有一个语法：

syntax Exp ::= Int | Bool
             | Exp Exp
             > Exp + Exp           [left] 
             > "fun" KVar "->" Exp [binder]
             | "(" Exp ")"         [bracket]
syntax Val ::= Int | Bool | "fun" KVar "->" Exp [binder]

其中 lambda 项"fun" KVar "->" Exp是值和表达式。什么是同时成为和"fun" KVar "->" Exp的一部分的正确方法是什么？ExpVal

我尝试创建一个新的排序syntax Lambda ::= "fun" KVar "->" Exp并添加Lambda到两者Val和Exp. 但是，这与Lambda.

标签： kframework

Answer 1

你可以这样做：

syntax Exp ::= Val
             | Exp Exp
             | Exp + Exp           [left, add] 
             | "(" Exp ")"         [bracket]
syntax Val ::= Int | Bool | "fun" KVar "->" Exp [binder, fun]
syntax priorities add > fun

编辑我已经更新了我的答案以包括@dwight.guth 的建议。