-
Notifications
You must be signed in to change notification settings - Fork 2
/
named_tuples.pvl
95 lines (78 loc) · 6.13 KB
/
named_tuples.pvl
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
(**
Copyright 2022 Google LLC
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
*)
#ifndef _NAMED_TUPLES_PVL
#define _NAMED_TUPLES_PVL
#define REDUCE_FORALL2(TypeName, field, result, var0, type0, var1, type1) \
reduc forall var0: type0, var1: type1; \
TypeName##_##field(Build##TypeName(var0, var1)) = result
#define DEFINE_DATA_TYPE2(TypeName, var0, type0, var1, type1) \
type TypeName. \
fun Build##TypeName(type0, type1): TypeName [data]. \
REDUCE_FORALL2(TypeName, var0, var0, var0, type0, var1, type1). \
REDUCE_FORALL2(TypeName, var1, var1, var0, type0, var1, type1)
#define REDUCE_FORALL3(TypeName, field, result, var0, type0, var1, type1, var2, type2) \
reduc forall var0: type0, var1: type1, var2: type2; \
TypeName##_##field(Build##TypeName(var0, var1, var2)) = result
#define DEFINE_DATA_TYPE3(TypeName, var0, type0, var1, type1, var2, type2) \
type TypeName. \
fun Build##TypeName(type0, type1, type2): TypeName [data]. \
REDUCE_FORALL3(TypeName, var0, var0, var0, type0, var1, type1, var2, type2). \
REDUCE_FORALL3(TypeName, var1, var1, var0, type0, var1, type1, var2, type2). \
REDUCE_FORALL3(TypeName, var2, var2, var0, type0, var1, type1, var2, type2)
#define REDUCE_FORALL4(TypeName, field, result, var0, type0, var1, type1, var2, type2, var3, type3) \
reduc forall var0: type0, var1: type1, var2: type2, var3: type3; \
TypeName##_##field(Build##TypeName(var0, var1, var2, var3)) = result
#define DEFINE_DATA_TYPE4(TypeName, var0, type0, var1, type1, var2, type2, var3, type3) \
type TypeName. \
fun Build##TypeName(type0, type1, type2, type3): TypeName [data]. \
REDUCE_FORALL4(TypeName, var0, var0, var0, type0, var1, type1, var2, type2, var3, type3). \
REDUCE_FORALL4(TypeName, var1, var1, var0, type0, var1, type1, var2, type2, var3, type3). \
REDUCE_FORALL4(TypeName, var2, var2, var0, type0, var1, type1, var2, type2, var3, type3). \
REDUCE_FORALL4(TypeName, var3, var3, var0, type0, var1, type1, var2, type2, var3, type3)
#define REDUCE_FORALL5(TypeName, field, result, var0, type0, var1, type1, var2, type2, var3, type3, var4, type4) \
reduc forall var0: type0, var1: type1, var2: type2, var3: type3, var4: type4; \
TypeName##_##field(Build##TypeName(var0, var1, var2, var3, var4)) = result
#define DEFINE_DATA_TYPE5(TypeName, var0, type0, var1, type1, var2, type2, var3, type3, var4, type4) \
type TypeName. \
fun Build##TypeName(type0, type1, type2, type3, type4): TypeName [data]. \
REDUCE_FORALL5(TypeName, var0, var0, var0, type0, var1, type1, var2, type2, var3, type3, var4, type4). \
REDUCE_FORALL5(TypeName, var1, var1, var0, type0, var1, type1, var2, type2, var3, type3, var4, type4). \
REDUCE_FORALL5(TypeName, var2, var2, var0, type0, var1, type1, var2, type2, var3, type3, var4, type4). \
REDUCE_FORALL5(TypeName, var3, var3, var0, type0, var1, type1, var2, type2, var3, type3, var4, type4). \
REDUCE_FORALL5(TypeName, var4, var4, var0, type0, var1, type1, var2, type2, var3, type3, var4, type4)
#define REDUCE_FORALL6(TypeName, field, result, var0, type0, var1, type1, var2, type2, var3, type3, var4, type4, var5, type5) \
reduc forall var0: type0, var1: type1, var2: type2, var3: type3, var4: type4, var5: type5; \
TypeName##_##field(Build##TypeName(var0, var1, var2, var3, var4, var5)) = result
#define DEFINE_DATA_TYPE6(TypeName, var0, type0, var1, type1, var2, type2, var3, type3, var4, type4, var5, type5) \
type TypeName. \
fun Build##TypeName(type0, type1, type2, type3, type4, type5): TypeName [data]. \
REDUCE_FORALL6(TypeName, var0, var0, var0, type0, var1, type1, var2, type2, var3, type3, var4, type4, var5, type5). \
REDUCE_FORALL6(TypeName, var1, var1, var0, type0, var1, type1, var2, type2, var3, type3, var4, type4, var5, type5). \
REDUCE_FORALL6(TypeName, var2, var2, var0, type0, var1, type1, var2, type2, var3, type3, var4, type4, var5, type5). \
REDUCE_FORALL6(TypeName, var3, var3, var0, type0, var1, type1, var2, type2, var3, type3, var4, type4, var5, type5). \
REDUCE_FORALL6(TypeName, var4, var4, var0, type0, var1, type1, var2, type2, var3, type3, var4, type4, var5, type5). \
REDUCE_FORALL6(TypeName, var5, var5, var0, type0, var1, type1, var2, type2, var3, type3, var4, type4, var5, type5)
#define REDUCE_FORALL7(TypeName, field, result, var0, type0, var1, type1, var2, type2, var3, type3, var4, type4, var5, type5, var6, type6) \
reduc forall var0: type0, var1: type1, var2: type2, var3: type3, var4: type4, var5: type5, var6: type6; \
TypeName##_##field(Build##TypeName(var0, var1, var2, var3, var4, var5, var6)) = result
#define DEFINE_DATA_TYPE7(TypeName, var0, type0, var1, type1, var2, type2, var3, type3, var4, type4, var5, type5, var6, type6) \
type TypeName. \
fun Build##TypeName(type0, type1, type2, type3, type4, type5, type6): TypeName [data]. \
REDUCE_FORALL7(TypeName, var0, var0, var0, type0, var1, type1, var2, type2, var3, type3, var4, type4, var5, type5, var6, type6). \
REDUCE_FORALL7(TypeName, var1, var1, var0, type0, var1, type1, var2, type2, var3, type3, var4, type4, var5, type5, var6, type6). \
REDUCE_FORALL7(TypeName, var2, var2, var0, type0, var1, type1, var2, type2, var3, type3, var4, type4, var5, type5, var6, type6). \
REDUCE_FORALL7(TypeName, var3, var3, var0, type0, var1, type1, var2, type2, var3, type3, var4, type4, var5, type5, var6, type6). \
REDUCE_FORALL7(TypeName, var4, var4, var0, type0, var1, type1, var2, type2, var3, type3, var4, type4, var5, type5, var6, type6). \
REDUCE_FORALL7(TypeName, var5, var5, var0, type0, var1, type1, var2, type2, var3, type3, var4, type4, var5, type5, var6, type6). \
REDUCE_FORALL7(TypeName, var6, var6, var0, type0, var1, type1, var2, type2, var3, type3, var4, type4, var5, type5, var6, type6)
#endif /* _NAMED_TUPLES_PVL */