K-user mailing list

[Daniel Schnetzer Fava <danielsf AT ifi.uio.no>]

I have a similar question to my previous one:

https://lists.cs.illinois.edu/lists/arc/k-user/2017-02/msg00015.html

but now initializing a map of Id to Set (as opposed to List of Nat)

Following the same idea, it seems like I would do the following to initialize it to an empty set:

       <H> HMap:Map (. => Z |-> .Set ) </H>

And something like this to initialize it to a Set with one item (that item being N):

       <H> HMap:Map (. => Z |-> SetItem(N) ) </H>

But neighter of these work.

It seems like kompile complais about the last parenthesis of those lines:

[Error] Critical: Parse error: Syntax error near unexpected character ‘)'

Thanks again,

Daniel

On 13 Feb 2017, at 13:23, Dorel Lucanu <dlucanu AT info.uaic.ro> wrote:

You may initialize with any value you want, so it should work.
Dorel

On 13/02/2017 14:15, Daniel Schnetzer Fava wrote:

Indeed, its 3.4.

The list of nats does work, though I have a follow up question.
Can it be initialized to a non-empty list? For example:

       <H> HMap:Map (. => Z |-> N,.NatList ) </H>   requires fresh(N:Nat)

Does this seem legitimate?
Assuming .NatList is the empty list of nats and , is cons.

Thanks Dorel!

On 13 Feb 2017, at 13:02, Dorel Lucanu <dlucanu AT info.uaic.ro> wrote:

What version of K do you use? It seems to me that it is 3.4, correct?

A possible solution is:
- declare a sort for list of naturals

 syntax NatList ::= List{Nat,"","}

- initialize the store with the empty lists:
rule <k> nat (Z:Id,Zs:Globals => Zs) </k>
      <H> HMap:Map (. => Z |-> .NatList ) </H>

Dorel

On 13/02/2017 13:44, danielsf AT ifi.uio.no wrote:

What would be a good way to create a store from Id to List[Nat] as opposed to
Id to Nat?

I created a simple example where it parses
    nat x, y, z
and creates a configuration:
<H>
        x |-> #symNat(1)
        y |-> #symNat(2)
        z |-> #symNat(3)
</H>

But I would like x, y, and z to map to lists of Nats as opposed to a Nat.

Can you point me in the right direction?

Thanks!

Daniel

module SIMPLE
  syntax Globals ::= List{Id,","}
  syntax Pgm ::= "nat" Globals
  configuration <T><k> $PGM:Pgm </k><H> .Map </H></T>

  rule <k> nat (Z:Id,Zs:Globals => Zs) </k>
       // I would like to somehow say this instead:
       // <H> HMap:Map (. => Z|-> ListItem(N) ) </H>
       <H> HMap:Map (. => Z|-> N ) </H>
       requires fresh(N:Nat) andBool
        notBool(Z in keys(HMap)) // no repeated declaration
endmodule