diff --git a/src/komet/kdist/soroban-semantics/configuration.md b/src/komet/kdist/soroban-semantics/configuration.md index 0748778..1c10a31 100644 --- a/src/komet/kdist/soroban-semantics/configuration.md +++ b/src/komet/kdist/soroban-semantics/configuration.md @@ -333,7 +333,7 @@ If `SCV` is a small value, `allocObject(SCV)` returns a small `HostVal` directly rule [loadObject-rel]: loadObject(VAL) - => loadObject(RELS {{ getIndex(VAL) }} orDefault HostVal(0)) + => loadObject(rel2abs(RELS, VAL)) ... RELS @@ -371,6 +371,24 @@ If `SCV` is a small value, `allocObject(SCV)` returns a small `HostVal` directly ``` +- rel2abs, rel2absMany: Convert relative handles to absolute handles + +```k + syntax HostVal ::= rel2abs(List, HostVal) [function, total, symbol(rel2abs)] + // ------------------------------------------------------------------------ + rule rel2abs(RELS, HV) => RELS {{ getIndex(HV) }} orDefault HV + requires isObject(HV) andBool isRelativeObjectHandle(HV) + rule rel2abs(_, HV) => HV + [owise] + + syntax List ::= rel2absMany(List, List) [function, total, symbol(rel2absMany)] + // -------------------------------------------------------------------------------- + rule rel2absMany(RELS, ListItem(HV) L) => ListItem(rel2abs(RELS, HV)) rel2absMany(RELS, L) + rule rel2absMany(_, L) => L + [owise] + +``` + ### Auxiliary functions ```k diff --git a/src/komet/kdist/soroban-semantics/host/map.md b/src/komet/kdist/soroban-semantics/host/map.md index 1f4fec8..aef32ca 100644 --- a/src/komet/kdist/soroban-semantics/host/map.md +++ b/src/komet/kdist/soroban-semantics/host/map.md @@ -91,7 +91,7 @@ The function returns a `HostVal` pointing to the new map object. ScMap( mapFromLists( KEYS, - Bytes2Vals(VALS_BS) + rel2absMany(RELS, Bytes2Vals(VALS_BS)) ) ) ) @@ -99,6 +99,7 @@ The function returns a `HostVal` pointing to the new map object. ... KEYS : VALS_BS : S => S + RELS requires size(KEYS) ==Int lengthBytes(VALS_BS) /Int 8 ``` diff --git a/src/komet/kdist/soroban-semantics/host/vector.md b/src/komet/kdist/soroban-semantics/host/vector.md index 8e77e56..47c0c74 100644 --- a/src/komet/kdist/soroban-semantics/host/vector.md +++ b/src/komet/kdist/soroban-semantics/host/vector.md @@ -76,8 +76,15 @@ module HOST-VECTOR U32(VALS_POS) : U32(LEN) : S => S rule [vecNewFromLinearMemoryAux]: - vecNewFromLinearMemoryAux => allocObject(ScVec(Bytes2Vals(BS))) ... + vecNewFromLinearMemoryAux + => allocObject( + ScVec( + rel2absMany(RELS, Bytes2Vals(BS)) + ) + ) ... + BS : S => S + RELS syntax Bytes ::= Vals2Bytes(List) [function, total]