/
memo.go
82 lines (74 loc) · 2.48 KB
/
memo.go
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
// File provided by the K Framework Go backend. Timestamp: 2019-08-28 22:25:14.706
package ieletestingmodel
// MemoKey is a key in a memoization table
type MemoKey = KReference
// MemoTable is a reference to a memoization table
type MemoTable int
// GetMemoKey converts a reference to a memo key
func GetMemoKey(ref KReference) (MemoKey, bool) {
return ref, true
}
// GetMemoizedValue searches for a value in the memo tables structure of the model.
func (ms *ModelState) GetMemoizedValue(memoTable MemoTable, keys ...MemoKey) (KReference, bool) {
if ms.memoTables == nil {
return NullReference, false
}
currentObj, tableFound := ms.memoTables[memoTable]
if !tableFound {
return NullReference, false
}
for _, key := range keys {
currentMap, isMap := currentObj.(map[MemoKey]interface{})
if !isMap {
panic("wrong object found: memo tables need a level of map[MemoKey]interface{} for each key")
}
objectForKey, isKeyPresent := currentMap[key]
if !isKeyPresent {
return NullReference, false
}
currentObj = objectForKey
}
kref, isKref := currentObj.(KReference)
if !isKref {
panic("wrong object found: memo tables need to have a KReference on the last level")
}
return kref, true
}
// SetMemoizedValue inserts a value into the memo table structure, for a variable number of keys.
// It extends the tree up to where it is required.
func (ms *ModelState) SetMemoizedValue(memoized KReference, memoTable MemoTable, keys ...MemoKey) {
// value gets copied to the special memoization data container
// from where it never gets flushed
memoized = transfer(ms.mainData, ms.memoData, memoized)
// create necessary structures and insert
if ms.memoTables == nil {
ms.memoTables = make(map[MemoTable]interface{})
}
if len(keys) == 0 {
// no keys, memo table is not really a table, it just contains one value
ms.memoTables[memoTable] = memoized
return
}
currentMapObj, tableFound := ms.memoTables[memoTable]
if !tableFound {
currentMapObj = make(map[MemoKey]interface{})
ms.memoTables[memoTable] = currentMapObj
}
for i, key := range keys {
currentMap, isMap := currentMapObj.(map[MemoKey]interface{})
if !isMap {
panic("wrong object found: memo tables need a level of map[MemoKey]interface{} for each key")
}
if i < len(keys)-1 {
nextMap, nextMapExists := currentMap[key]
if !nextMapExists {
nextMap = make(map[MemoKey]interface{})
currentMap[key] = nextMap
currentMapObj = nextMap
}
} else {
// last key
currentMap[key] = memoized
}
}
}