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
|
module analysis/names
imports
signatures/TemplateLang-sig
analysis/types
libstrc
namespaces
Module Sort
Constructor Label
DeclSort
properties
def of Constructor : SdfProduction
sort of Constructor : Sort
ast of Module : Module
constructorName of Sort : Constructor
binding rules
mod@Module(Unparameterized(m), i*, s*):
defines Module m
scopes Sort, Constructor
Module(Unparameterized(m)):
imports Sort, Constructor from Module m
//Kernel Productions
p@SdfProductionWithCons(SortCons(Lex(SortDef(s)), Constructor(c)), rhs, attrs):
defines non-unique Sort s of type SortType(s) of constructorName c
defines unique Constructor c
of type FunType(ty*, SortType(s))
where rhs has type ty*
scopes Label
p@SdfProduction(Lex(SortDef(s)), rhs, attrs):
defines non-unique Sort s of type SortType(s)
scopes Label
p@SdfProductionWithCons(SortCons(Cf(SortDef(s)), Constructor(c)), rhs, attrs):
defines non-unique Sort s of type SortType(s) of constructorName c
defines unique Constructor c
of type FunType(ty*, SortType(s))
where rhs has type ty*
scopes Label
p@SdfProduction(Cf(SortDef(s)), rhs, attrs):
defines non-unique Sort s of type SortType(s)
scopes Label
//Regular Productions
p@SdfProductionWithCons(SortCons(SortDef(s), Constructor(c)), rhs, attrs):
defines non-unique Sort s of type SortType(s) of constructorName c
defines unique Constructor c
of type FunType(ty*, SortType(s))
where rhs has type ty*
scopes Label
p@SdfProduction(SortDef(s), rhs, attrs):
defines non-unique Sort s of type SortType(s)
scopes Label
p@TemplateProductionWithCons(SortCons(SortDef(s), Constructor(c)), t, attrs):
defines non-unique Sort s of type SortType(s) of constructorName c
defines unique Constructor c
of type FunType(ty*, SortType(s))
where t has type ty*
scopes Label
p@TemplateProduction(SortDef(s), t, attrs):
defines non-unique Sort s of type SortType(s)
scopes Label
DeclSort(s): // context-free
defines non-unique Sort s of type SortType(s)
// defines DeclSort s
DeclSortLex(s):
defines non-unique Sort s of type SortType(s)
// defines DeclSort s
DeclSortVar(s):
defines non-unique Sort s of type SortType(s)
// defines DeclSort s
SortConsRef(Sort(), Constructor(c)):
refers to Sort s
refers to Constructor c of sort s
SortConsRef(Lex(Sort()), Constructor(c)):
refers to Sort s
refers to Constructor c of sort s
SortConsRef(Cf(Sort()), Constructor(c)):
refers to Sort s
refers to Constructor c of sort s
Sort(s):
refers to Sort s
Label(Unquoted(l), _):
defines unique Label l
LabelRef(l):
refers to Label l
|