ocaml - K 框架在 OCaml 后端产生错误

Question

我正在使用K 语义框架并运行教程，这是我的 TEST1.k ：

module TEST1-SYNTAX 
import DOMAINS


syntax Fun ::= "add(" Pgm "," Pgm ")"        [strict]
syntax Pgm ::= Int 
            | Fun

endmodule

module TEST1
import TEST1-SYNTAX

    rule add( I1:Int , I2:Int) => I1 +Int I2

    configuration <T  color="blue">
                <k color ="red"> $PGM:Pgm </k> 


    </T>
endmodule

但是在运行命令 Komile Test1.k 时出现此错误：

File "realdef.ml", line 2151, characters 331-338:
Error: This variant expression is expected to have type bool
   The constructor KApply1 does not belong to type bool
 [Error] Critical: ocamlopt returned nonzero exit code: 2
Examine output to see errors.

标签： ocamlformal-verificationformal-methodsformal-semanticskframework