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
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335 | class ClifParser(Parser):
"""
A parser for Common Logic Interchange Format (CLIF) documents.
Example:
-------
>>> parser = ClifParser()
>>> theory = parser.parse('''
... (cl-text friends
... (FriendOf Alice Bob)
... (forall (x y) (if (FriendOf x y) (FriendOf y x)))
... )
... ''')
>>> theory.name
'friends'
>>> for s in theory.sentences:
... print(s)
FriendOf(Alice, Bob)
∀x: None, y: None : (FriendOf(?x, ?y) -> FriendOf(?y, ?x))
"""
default_suffix = "clif"
def parse(self, source: Union[Path, str, TextIO], **kwargs) -> Theory:
"""
Parse a CLIF document into a Theory.
:param source: a path to a file, CLIF text, or a file-like object
:param kwargs: unused
:return: the parsed theory
"""
text = self._read_source(source)
theory = Theory()
for form in _read_forms(text):
self._process_form(form, theory)
theory.predicate_definitions = self._infer_predicate_definitions(theory)
return theory
def parse_ground_terms(self, source: Union[Path, str, TextIO], **kwargs) -> List[Term]:
"""
Parse a CLIF document and return all ground terms (facts).
:param source: a path to a file, CLIF text, or a file-like object
:param kwargs: unused
:return: ground terms
"""
theory = self.parse(source, **kwargs)
return [s for s in theory.sentences if isinstance(s, Term) and s.is_ground]
def validate_iter(self, source: Union[Path, str, TextIO, ModuleType], **kwargs) -> Iterator[ValidationMessage]:
"""
Validate a CLIF document.
:param source: a path to a file, CLIF text, or a file-like object
:param kwargs: unused
:return: iterator of validation messages
"""
if isinstance(source, ModuleType):
raise ValueError("ClifParser cannot validate python modules")
try:
self.parse(source, **kwargs)
except ClifSyntaxError as e:
yield ValidationMessage(message=str(e))
def _read_source(self, source: Union[Path, str, TextIO]) -> str:
if isinstance(source, Path):
return source.read_text(encoding="utf-8")
if hasattr(source, "read"):
return source.read() # type: ignore[union-attr]
return str(source)
def _process_form(self, form: Any, theory: Theory) -> None:
if not isinstance(form, list):
raise ClifSyntaxError(f"Unexpected top-level atom: {form!r}")
if form and isinstance(form[0], _Symbol):
keyword = str(form[0])
if keyword in TEXT_KEYWORDS:
if len(form) < 2:
raise ClifSyntaxError(f"({keyword} ...) requires a name")
theory.name = str(form[1])
for sub_form in form[2:]:
self._process_form(sub_form, theory)
return
if keyword in COMMENT_KEYWORDS or keyword in IMPORT_KEYWORDS:
return
theory.add(self._sentence(form, {}))
def _sentence(self, form: Any, bound: Dict[str, Variable]) -> Sentence:
if not isinstance(form, list):
raise ClifSyntaxError(f"Expected a sentence, got atom: {form!r}")
if not form:
raise ClifSyntaxError("Empty sentence: ()")
head = form[0]
operator = str(head) if isinstance(head, _Symbol) else None
if operator in ("forall", "exists"):
return self._quantified(form, bound)
if operator == "and":
return And(*[self._sentence(f, bound) for f in form[1:]])
if operator == "or":
return Or(*[self._sentence(f, bound) for f in form[1:]])
if operator == "not":
if len(form) != 2:
raise ClifSyntaxError(f"(not ...) requires exactly one sentence: {form!r}")
return Not(self._sentence(form[1], bound))
if operator == "if":
if len(form) != 3:
raise ClifSyntaxError(f"(if ...) requires exactly two sentences: {form!r}")
return Implies(self._sentence(form[1], bound), self._sentence(form[2], bound))
if operator == "iff":
if len(form) != 3:
raise ClifSyntaxError(f"(iff ...) requires exactly two sentences: {form!r}")
return Iff(self._sentence(form[1], bound), self._sentence(form[2], bound))
if operator == "=":
return Term("eq", *[self._argument(f, bound) for f in form[1:]])
return self._atom(form, bound)
def _quantified(self, form: List[Any], bound: Dict[str, Variable]) -> Sentence:
quantifier = str(form[0])
if len(form) < 3 or not isinstance(form[1], list):
raise ClifSyntaxError(f"({quantifier} ...) requires a binding list and a body: {form!r}")
variables = [self._binding(b, quantifier) for b in form[1]]
inner_bound = {**bound, **{v.name: v for v in variables}}
bodies = [self._sentence(f, inner_bound) for f in form[2:]]
body = bodies[0] if len(bodies) == 1 else And(*bodies)
if quantifier == "forall":
return Forall(variables, body)
return Exists(variables, body)
def _binding(self, form: Any, quantifier: str) -> Variable:
domain: Optional[str] = None
if isinstance(form, list):
if len(form) != 2:
raise ClifSyntaxError(f"Invalid binding in ({quantifier} ...): {form!r}")
form, domain_form = form
domain = str(domain_form)
if not isinstance(form, str):
raise ClifSyntaxError(f"Invalid binding in ({quantifier} ...): {form!r}")
name = str(form)
if name.startswith("?"):
name = name[1:]
return Variable(name, domain)
def _atom(self, form: List[Any], bound: Dict[str, Variable]) -> Term:
head = form[0]
if isinstance(head, list):
raise ClifSyntaxError(f"Compound terms in operator position are not supported: {form!r}")
predicate: Union[str, Variable]
name = str(head)
if isinstance(head, _Symbol) and name.startswith("?"):
predicate = bound.get(name[1:], Variable(name[1:]))
elif isinstance(head, _Symbol) and name in bound:
predicate = bound[name]
else:
predicate = name
arguments = [self._argument(f, bound) for f in form[1:]]
# Term supports Variable predicates at runtime (hilog-style), but is annotated as str-only
return Term(predicate, *arguments) # type: ignore[arg-type]
def _argument(self, form: Any, bound: Dict[str, Variable]) -> Any:
if isinstance(form, list):
return self._sentence(form, bound)
if isinstance(form, _Symbol):
name = str(form)
if name.startswith("?"):
return bound.get(name[1:], Variable(name[1:]))
if name in bound:
return bound[name]
if name == "true":
return True
if name == "false":
return False
if name == "null":
return None
return name
return form
def _infer_predicate_definitions(self, theory: Theory) -> List[PredicateDefinition]:
"""Infer predicate definitions from the atoms used in the parsed sentences."""
inferred: Dict[str, Dict[str, str]] = {}
def argument_type(value: Any) -> str:
if isinstance(value, Variable):
return value.domain or "str"
if isinstance(value, bool):
return "bool"
if isinstance(value, (int, float)):
return type(value).__name__
return "str"
def visit(sentence: Sentence) -> None:
if isinstance(sentence, Term):
predicate = sentence.predicate
if isinstance(predicate, str) and predicate not in NAME_TO_INFIX_OP:
arguments = {f"arg{i}": argument_type(v) for i, v in enumerate(sentence.bindings.values())}
if predicate not in inferred or len(arguments) > len(inferred[predicate]):
inferred[predicate] = arguments
for value in sentence.bindings.values():
if isinstance(value, Sentence):
visit(value)
return
if isinstance(sentence, QuantifiedSentence):
visit(sentence.sentence)
return
if isinstance(sentence, BooleanSentence):
for operand in sentence.operands:
visit(operand)
for s in theory.sentences:
visit(s)
return [PredicateDefinition(predicate, arguments) for predicate, arguments in inferred.items()]
|