K-user mailing list

[Traian Florin Șerbănuță <tserban2 AT illinois.edu>]

Dear Hossein,

There are two ways.

The preferred one is to use matching to match the key you want to remove and eliminate it from the right side.

For example, the following rule

rule <k> remove X => .  ...</k>  <state>... X |-> _ => . ...</state>

will remove X from the state cell (prompted by the remove command in the K cell.   Its meaning is, if "remove X" is at the top (left) of the <k> cell then match the binding of C in the state and remove it, which is specified as "X |-> _ => ."

Moreover, the remove command is itself removed, specified by " remove X => . "  (The "." symbol is the unit of the corresponding type).

There exists another way, which is less commonly used, and not guaranteed to be preserved by future versions.  But this one is more in the spirit of your attempts.

rule <k> remove X => .  ...</k>  <state> Map => Map[undef/X] </state>

here, _[undef/_] is a special function which removes the key from the map.

One suggestion would be to check the k-prelude.maude from $K_BASE/core/maude/lib directory  for the syntax and definitions of the basic Set/Map constructs.  This would require some familiarity with Maude, though.

best wishes,

- traian

2012/2/23 Seyed H. HAERI (Hossein) <hossein.haeri AT gmail.com>

Dear all,

What's the syntax for removing the key X from Map M? I tried all what
I could think of and got error messages: M[X |-> .], M[X |-> _|_],
M[./X], and M[_|_/X]. Is that available at all by the way?

More fundamentally, how can I lookup the interfaces for the built-in
types? I tried pl-builtins.maude and couldn't find any occurrence of
the string literal "Map".

TIA,
--Hossein

--------------------------------------------------------------------------------------------------------------

Seyed H. HAERI (Hossein)

Research Assistant
Institute for Software Systems (STS)
Technical University of Hamburg (TUHH)
Hamburg, Germany

ACCU - Professionalism in programming - http://www.accu.org/
--------------------------------------------------------------------------------------------------------------
_______________________________________________
k-user mailing list
k-user AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/k-user