k-user AT lists.cs.illinois.edu

Subject: K-user mailing list

List archive

[K-user] defining subset operator on Lists

From: Abdul Dakkak <abduld AT wolfram.com>
To: k-user <k-user AT cs.uiuc.edu>
Subject: [K-user] defining subset operator on Lists
Date: Wed, 8 May 2013 12:35:24 -0500 (CDT)
List-archive: <http://lists.cs.uiuc.edu/pipermail/k-user/>
List-id: <k-user.cs.uiuc.edu>

I have the following

syntax Field ::= Id
syntax RecordItem ::= Field ":" Type
syntax Record ::= List{RecordItem,","}

syntax Bool ::= ListItem "isInList" List [function]
syntax Bool ::= List "isSubset" List [function]

rule X:ListItem isInList (_ X _) => true

rule .List isSubset X:List => true
rule (L:ListItem Ls:List) isSubset X:List => Ls isSubset X when L isInList
X ==K true
rule (L:ListItem Ls:List) isSubset X:List => false when L isInList X =/=K
true

but when I use it

rule <k>(S:Record -> T:Type) S':Record => T ...</k>
when (S isSubset S') ==K true

I get an error stating that it expects S to be of Type ListItem and not
Record.

-adk-

[K-user] defining subset operator on Lists, Abdul Dakkak, 05/08/2013
- Re: [K-user] defining subset operator on Lists, Moore, Brandon Michael, 05/08/2013