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
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255 | def check_constraints(module: Module) -> list[Violation]:
"""Return every well-formedness violation in ``module``.
Walks the statements in source order, building up the symbol
tables (residuated universes, enum sets, free monoids, declared
rule / schema / bundle names) incrementally so that out-of-order
references are flagged.
"""
out: list[Violation] = []
residuated_universes: dict[str, TypeFreeResiduated] = {}
enum_sets: dict[str, TypeEnumSet] = {}
free_monoids: dict[str, TypeFreeMonoid] = {}
aliased_names: dict[str, ObjectExpr] = {}
rule_names: set[str] = set()
schema_names: set[str] = set()
bundle_names: set[str] = set()
category_atoms: set[str] = set()
builtin_schemas = set(SCHEMA_REGISTRY.keys())
def is_residuated_object(name: str) -> bool:
"""True iff ``name`` resolves (via aliases) to a residuated universe."""
seen: set[str] = set()
cur = name
while cur not in seen:
seen.add(cur)
if cur in residuated_universes:
return True
if cur in aliased_names:
rhs = aliased_names[cur]
if isinstance(rhs, TypeName):
cur = rhs.name
continue
return False
return False
def is_known_effect(name: str) -> bool:
"""True iff ``name`` matches the conventional effect-naming pattern."""
return bool(name) and (name[0].isupper() or "_" in name)
def walk_pattern(
texpr: ObjectExpr,
*,
in_residuated_context: bool,
line_hint: int = 0,
col_hint: int = 0,
) -> None:
if isinstance(texpr, TypeName):
return
if isinstance(texpr, ObjectProduct):
for c in texpr.components:
walk_pattern(
c,
in_residuated_context=in_residuated_context,
line_hint=line_hint,
col_hint=col_hint,
)
return
if isinstance(texpr, ObjectCoproduct):
for c in texpr.components:
walk_pattern(
c,
in_residuated_context=in_residuated_context,
line_hint=line_hint,
col_hint=col_hint,
)
return
if isinstance(texpr, ObjectSlash):
if not in_residuated_context:
line = texpr.line or line_hint
col = texpr.col or col_hint
out.append(
Violation(
code="residuated_constraint",
message=(
f"ObjectSlash {texpr.direction!r} appears "
"outside a residuated context; either "
"declare a FreeResiduated universe and "
"parameterize the schema by it, or remove "
"the slash"
),
line=line,
col=col,
)
)
walk_pattern(
texpr.result,
in_residuated_context=in_residuated_context,
line_hint=line_hint,
col_hint=col_hint,
)
walk_pattern(
texpr.argument,
in_residuated_context=in_residuated_context,
line_hint=line_hint,
col_hint=col_hint,
)
return
if isinstance(texpr, ObjectEffectApply):
if not is_known_effect(texpr.effect):
line = texpr.line or line_hint
col = texpr.col or col_hint
out.append(
Violation(
code="effect_constraint",
message=(
f"effect {texpr.effect!r} has no "
"recognized naming pattern; effect names "
"must start with an uppercase letter or "
"contain an underscore"
),
line=line,
col=col,
)
)
for arg in texpr.args:
walk_pattern(
arg,
in_residuated_context=in_residuated_context,
line_hint=line_hint,
col_hint=col_hint,
)
return
for stmt in module.statements:
if isinstance(stmt, ObjectDecl):
init = stmt.init
if isinstance(init, TypeFreeResiduated):
residuated_universes[stmt.name] = init
elif isinstance(init, TypeEnumSet):
enum_sets[stmt.name] = init
elif isinstance(init, TypeFreeMonoid):
free_monoids[stmt.name] = init
elif isinstance(init, TypeFromExpr):
aliased_names[stmt.name] = init.expr
elif isinstance(stmt, CategoryDecl):
for name in stmt.names:
category_atoms.add(name)
elif isinstance(stmt, RuleDecl):
rule_names.add(stmt.name)
for prem in stmt.premises:
walk_pattern(
prem,
in_residuated_context=True,
line_hint=stmt.line,
col_hint=stmt.col,
)
walk_pattern(
stmt.conclusion,
in_residuated_context=True,
line_hint=stmt.line,
col_hint=stmt.col,
)
elif isinstance(stmt, SchemaDecl):
schema_names.add(stmt.name)
in_res = any(
isinstance(p.type_expr, TypeName)
and is_residuated_object(p.type_expr.name)
for p in stmt.parameters
)
walk_pattern(
stmt.domain,
in_residuated_context=in_res,
line_hint=stmt.line,
col_hint=stmt.col,
)
walk_pattern(
stmt.codomain,
in_residuated_context=in_res,
line_hint=stmt.line,
col_hint=stmt.col,
)
elif isinstance(stmt, BundleDecl):
bundle_names.add(stmt.name)
for member in stmt.rules:
if (
member not in rule_names
and member not in schema_names
and member not in bundle_names
and member not in builtin_schemas
):
out.append(
Violation(
code="bundle_unknown_member",
message=(
f"bundle {stmt.name!r} references "
f"unknown member {member!r}; not a "
"declared rule / schema / bundle, "
"nor a built-in schema"
),
line=stmt.line,
col=stmt.col,
)
)
return out
|