0

我有以下 K 文件：

require "substitution.k"

module PURE
    imports DOMAINS
    imports SUBSTITUTION

    syntax PSort ::= "$Type" [token]
                   | "$Kind" [token]

    syntax Type ::= PSort
                  | KVar
                  | "Pi" KVar ":" Term "." Term [binder]

    syntax Term ::= Type
                  | "(" Term ")" [bracket]
                  > Term Term    [left]
                  > "declare" KVar ":" Term "in" Term

    syntax KResult ::= Type

    configuration
    <T>
        <k> typeof($PGM:Term, ?T) ~> ?T </k>
        <typeEnv> .Map </typeEnv>
    </T>

    syntax KItem ::= typeof(Term, Term)

    rule <k> typeof(declare X : T in E, T2) => typeof(E, T2) ... </k>
         <typeEnv> TEnv => TEnv[X <- T] </typeEnv>

    // VAR
    rule <k> typeof(X:KVar, T) => . ... </k>
         <typeEnv> ... X |-> T ... </typeEnv>

    // APP
    syntax KItem ::= Term "=" Term
    rule T = T => .

    rule typeof(M N, T) =>
         typeof(M, Pi ?X : ?T1. ?T2) ~>
         typeof(N, ?T1) ~>
         ?T2[N/?X] = T
endmodule

当我使用 Java 后端编译它并运行以下文件时：

declare nat : $Type in
declare Z : nat in
declare Vector : Pi n : nat . $Type in
declare blah : Pi n : nat . (Vector n) in
blah Z

我得到：

<T>
  <k>
    Vector n
  </k>
  <typeEnv>
    Vector |-> Pi n : nat . $Type
    Z |-> nat
    blah |-> Pi n : nat . ( Vector n )
    nat |-> $Type
  </typeEnv>
</T>

但我希望它代替Z并n得到Vector Z.

4

1 回答 1

0

这似乎是 java 后端中的一个错误，它过早地应用了替换运算符，而它的参数仍然是符号变量。结果，替换运算符过早消失，然后当被替换的术语通过统一实例化时，它没有被替换，这导致了你描述的问题。这是一个跟踪问题的问题：https ://github.com/kframework/k/issues/1165

我尝试修复它，但事实证明这是不平凡的，我现在没有时间深入挖掘。如果您愿意，欢迎您尝试在拉取请求中修复它，尽管我不确定为什么我写的修复会破坏其他东西。您更好的选择可能是重写您的键入规则，以便它们不会尝试对变量执行替换。一种方法是让应用程序的规则修改类型环境，然后在完全键入时恢复它。您可以查看 K 教程文件夹 1_k/5_types，了解如何键入类似 lambda 演算的语言的一些示例。

于 2020-03-13T14:46:23.993 回答