K-user mailing list

[<danielsf AT ifi.uio.no>]

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