0

我被困在一个功能的实现中，而且我不确定这是否是解决我的问题的正确方法。

我的问题描述

对于上下文，我希望能够borrow（一元操作）结构的字段，仅当该字段或其父字段上不存在引用时。让我用下面的例子来澄清我的这一点。我希望通过代码让事情变得更加清晰。

struct p{ x, p2:{ x, p3: {x} }
let a = ref p
let b = ref p.p2
let c = ref p.p2.p3

在这里，我有一个p包含嵌套字段和 3 个引用的结构：一个在 p 上，2 个在其字段上。

我使用 aMap来存储引用和它们之间的映射ref：

<env>
1 |-> 0      // 1 is a and 0 is p
2 |-> 0.1    // 2 is b and 0.1 is p.p2
3 |-> 0.1.2  // 3 is c and 0.1.2 is p.p2.p3 
</env>

所以现在，如果我想在 p.p2.p3.x 上做一元运算符借用：

borrow p.p2.p3.x;

此操作应该失败，因为a,b and c存在于我的env.

我的代码

所以，我试图在这个片段中实现它：

module TEST-SYNTAX 

import DOMAINS

syntax Ref ::= "ref" "{" Path "}"

syntax Path ::= List{Int,","}

syntax Stmts ::= List{Stmt, ";"}

syntax Stmt ::= Ref
            | Int "borrow" "{" Path "}"
endmodule

module TEST

import TEST-SYNTAX

configuration <T> 
    <k>$PGM:Stmts</k>
    <env> .Map </env>
</T>

rule S:Stmt ; Ss:Stmts => S ~> Ss
rule .Stmts => .

rule <k> ref { P:Path } => . ... </k>
    <env> Rho:Map => Rho[!I:Int <- P] </env>

syntax Bool::= #checkborrow(Int, List, Path)    [function]

syntax List ::= #pathToSubPaths(Path, List) [function]

rule <k> N:Int borrow { P:Path } => #checkborrow(N, #pathToSubPaths(P, .List), P) ...  </k>

rule #pathToSubPaths(.Path, S:List) => S

endmodule

我被困在如何实现该#checkborrow功能上。我的想法是首先生成给定路径的所有子路径，例如：

#pathToSubPath(p.p2.p3.x) => { {p} , { p.p2 }, { p.p2.p3 }, { p.p2.p3.x } }

之后，做一个投影函数env来查看元素是否存在：

#refForSubPathsExist(SubPaths:Set) => {True, True, True, False}

然后Set通过折叠OR #checkborrow({True, True, True, False}) => True减少返回值

目前，我被困在#pathToSubPath.

如果您有勇气阅读整个问题，谢谢您:)。我对K不熟悉，所以我正在寻求帮助。

注意： 我们使用的是这个版本的 K 框架：https ://github.com/kframework/k/releases/tag/nightly-f5ea5c7

4

0 回答 0