/
dataCollections.go
145 lines (128 loc) · 4.63 KB
/
dataCollections.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
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
// File provided by the K Framework Go backend. Timestamp: 2019-08-28 22:25:14.706
package ieletestingmodel
// List is a KObject representing a list in K
type List struct {
Sort Sort
Label KLabel
Data []KReference
}
func (*List) referenceType() kreferenceType {
return listRef
}
// Array is a KObject holding an array that can grow
type Array struct {
Sort Sort
Data *DynamicArray
}
func (*Array) referenceType() kreferenceType {
return arrayRef
}
// CollectionSortName yields the sort name of a collection, if argument is a collection.
func (ms *ModelState) CollectionSortName(ref KReference) (string, bool) {
refType, _, sort, _, _, _ := parseKrefCollection(ref)
if refType == mapRef ||
refType == listRef ||
refType == setRef ||
refType == arrayRef {
return Sort(sort).Name(), true
}
return "", false
}
// IsList returns true if reference points to a list with given sort
func (ms *ModelState) IsList(ref KReference, expectedSort Sort) bool {
refType, _, sort, _, _, _ := parseKrefCollection(ref)
return refType == listRef && sort == uint64(expectedSort)
}
// IsArray returns true if reference points to an array with given sort
func (ms *ModelState) IsArray(ref KReference, expectedSort Sort) bool {
refType, _, sort, _, _, _ := parseKrefCollection(ref)
return refType == arrayRef && sort == uint64(expectedSort)
}
// GetListObject yields the cast object for a List reference, if possible.
func (ms *ModelState) GetListObject(ref KReference) (*List, bool) {
refType, dataRef, _, _, index, _ := parseKrefCollection(ref)
if refType != listRef {
return nil, false
}
obj := ms.getData(dataRef).getReferencedObject(index)
castObj, typeOk := obj.(*List)
if !typeOk {
panic("wrong object type for reference")
}
return castObj, true
}
// IsEmptyList returns true only if argument references an empty list, with given sort and label.
func (ms *ModelState) IsEmptyList(ref KReference, expectedSort Sort, expectedLabel KLabel) bool {
castObj, typeOk := ms.GetListObject(ref)
if !typeOk {
return false
}
if castObj.Sort != expectedSort {
return false
}
if castObj.Label != expectedLabel {
return false
}
return len(castObj.Data) == 0
}
// ListSplitHeadTail returns true only if argument references an empty list.
// Returns nothing if it is not a list, it is empty, or if sort or label do not match.
func (ms *ModelState) ListSplitHeadTail(ref KReference, expectedSort Sort, expectedLabel KLabel) (ok bool, head KReference, tail KReference) {
castObj, typeOk := ms.GetListObject(ref)
if !typeOk {
return false, NullReference, NullReference
}
if castObj.Sort != expectedSort {
return false, NullReference, NullReference
}
if castObj.Label != expectedLabel {
return !ok, NullReference, NullReference
}
if len(castObj.Data) == 0 {
return false, NullReference, NullReference
}
tailRef := ms.NewList(castObj.Sort, castObj.Label, castObj.Data[1:])
return true, castObj.Data[0], tailRef
}
// GetSetObject yields the cast object for a Set reference, if possible.
// func (ms *ModelState) GetSetObject(ref KReference) (*Set, bool) {
// refType, dataRef, _, _, index, _ := parseKrefCollection(ref)
// if refType != setRef {
// return nil, false
// }
// obj := ms.getData(dataRef).getReferencedObject(index)
// castObj, typeOk := obj.(*Set)
// if !typeOk {
// panic("wrong object type for reference")
// }
// return castObj, true
// }
// GetArrayObject yields the cast object for an Array reference, if possible.
func (ms *ModelState) GetArrayObject(ref KReference) (*Array, bool) {
refType, dataRef, _, _, index, _ := parseKrefCollection(ref)
if refType != arrayRef {
return nil, false
}
obj := ms.getData(dataRef).getReferencedObject(index)
castObj, typeOk := obj.(*Array)
if !typeOk {
panic("wrong object type for reference")
}
return castObj, true
}
func (md *ModelData) addCollectionObject(sort Sort, label KLabel, obj KObject) KReference {
newIndex := len(md.allObjects)
md.allObjects = append(md.allObjects, obj)
return createKrefCollection(obj.referenceType(), md.selfRef, uint64(sort), uint64(label), uint64(newIndex), 0)
}
func (ms *ModelState) addCollectionObject(sort Sort, label KLabel, obj KObject) KReference {
return ms.mainData.addCollectionObject(sort, label, obj)
}
// NewList creates a new object and returns the reference.
func (ms *ModelState) NewList(sort Sort, label KLabel, value []KReference) KReference {
return ms.addCollectionObject(sort, label, &List{Sort: sort, Label: label, Data: value})
}
// NewArray creates a new object and returns the reference.
func (ms *ModelState) NewArray(sort Sort, value *DynamicArray) KReference {
return ms.addCollectionObject(sort, KLabel(0), &Array{Sort: sort, Data: value})
}