How to check if there exist a sub list of a list in a Map?

Question

I am stuck in the implementation of a function and also I am not sure if it is the correct way to solve my problem.

Description of my problem

For the context, I want to be able to borrow (a unary operation) a field of a structure only if no references on this field or its parent already exist. Let me clarify my this with the following example. I hope things will become more clear with code.

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

Here I have a structure p with nested fields and 3 references: one on p and 2 on its fields.

I use a Map to store the mapping between referred and their 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>

So now, If I want to do the unary operator borrow on p.p2.p3.x:

borrow p.p2.p3.x;

This operation should fail because a,b and c exists in my env.

My code

So, I tried to implement this in this snippet:

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

I am stuck on how I can implement the #checkborrow function. My idea is to first generate all the sub path of a given paths, for example:

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

After, make a projection function on env to see if the element exist or not:

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

Then reducing this returned Set with a folding OR #checkborrow({True, True, True, False}) => True

For now, I am stuck in the implementation of #pathToSubPath.

Thank you if you had the courage to read the whole question :). I am unfamiliar with K, so I am looking for help.

NOTE: We are using this version of K Framework: https://github.com/kframework/k/releases/tag/nightly-f5ea5c7