K-user mailing list

[Dorel Lucanu <dlucanu AT info.uaic.ro>]

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