[KIP] - Record update syntax for modifying a single element of a record

[ehildenb]

@hjorthjort found a use-case where being able to update a single entry in a record-type would make the semantics much cleaner runtimeverification/wasm-semantics#333 (comment).

We have to use a work-around for now, but it would be nice if we could do something like:

configuration <k> $PGM:Pgm </k>
              <r> record(... a:0, b:true) </r>
              <someCell> .SomeData </someCell>

syntax Record ::= record ( a: Int, b: Bool )

syntax Pgm ::= setA ( Int ) | setB ( Bool )

syntax SomeData ::= ".SomeData" | transformData ( Record , SomeData ) [function]

rule <k> setA(I) => . ... </k>
     <r> record(... a: _ => I) #as R </r>
     <someCell> SOME_DATA => transformData(R(... a <- I)) </someCell>

rule <k> setB(B) => . ... </k>
     <r> record(... b: _ => B) #as R </r>
     <someCell> SOME_DATA => transformData(R(... b <- B)) </someCell>

In this example, transformData needs to get the updated record, but we don't want to have to mention all the fields of R to build the updated record and pass it into the function (because record could have many fields).

[hjorthjort]

Hmm, I think something even more general would be necessary because we need to do this in a function rule. But I'm not sure what is supposed to happen in the <someCell> above. What is the a <- I? If that is supposed to be a record update, them I'm all for that.

In our problematic case, we need to do this in a function rule, so to replicate the above example we would need to do a "nested rewrite" and capture the name. So in our case, it would look like this:

rule #t2aFuncSpec<ctx(... localIds: (_ => #ids2Idxs(T, LS)) #as C>(T:TypeUse LS:LocalDecls IS:Instrs)
  => #t2aTypeUse   <C>(T)
     #t2aLocalDecls<C>(LS)
     #t2aInstrs    <C>(IS)

Maybe it would be easier to just add syntax for updating records, similar to what exists for Maps?

R:Record [ a <- I ]

[ehildenb]

Yes, the above R(... a <- I) is meant as record update, but using record syntax instead of maps. I'm not fixed on the syntax, was just suggesting something, and thought it might be good to be distinct from the map update syntax.

Your example won't work I don't think because the #as C pattern should capture the record from before the rewrite, not after, AFAIK.

[hjorthjort]

Ah, now I get why the #as was needed in the cell. So in my example, it would look something like:

rule #t2aFuncSpec<C>(T:TypeUse LS:LocalDecls IS:Instrs)
  => #t2aTypeUse   <C(... localIds <- #ids2Idxs(T, LS))>(T)
     #t2aLocalDecls<C(... localIds <- #ids2Idxs(T, LS))>(LS)
     #t2aInstrs    <C(... localIds <- #ids2Idxs(T, LS))>(IS)

I like that.

[ehildenb]

With supported where clauses (#1685), this can be done pretty nicely with #fun usage:

rule 

  where newR := #fun(record(... a: A => B))(R)

[dwightguth]

Closing as a duplicate of #2477