Whether a string of aux construction can be constructed. Args: string: str: the string describing aux construction. g: gh.Graph: the current proof state. Returns: str: whether this construction is valid. If not, starts with "ERROR:".
(string: str, g: gh.Graph)
| 369 | |
| 370 | |
| 371 | def try_translate_constrained_to_construct(string: str, g: gh.Graph) -> str: |
| 372 | """Whether a string of aux construction can be constructed. |
| 373 | |
| 374 | Args: |
| 375 | string: str: the string describing aux construction. |
| 376 | g: gh.Graph: the current proof state. |
| 377 | |
| 378 | Returns: |
| 379 | str: whether this construction is valid. If not, starts with "ERROR:". |
| 380 | """ |
| 381 | if string[-1] != ';': |
| 382 | return 'ERROR: must end with ;' |
| 383 | |
| 384 | head, prem_str = string.split(' : ') |
| 385 | point = head.strip() |
| 386 | |
| 387 | if len(point) != 1 or point == ' ': |
| 388 | return f'ERROR: invalid point name {point}' |
| 389 | |
| 390 | existing_points = [p.name for p in g.all_points()] |
| 391 | if point in existing_points: |
| 392 | return f'ERROR: point {point} already exists.' |
| 393 | |
| 394 | prem_toks = prem_str.split()[:-1] # remove the EOS ' ;' |
| 395 | prems = [[]] |
| 396 | |
| 397 | for i, tok in enumerate(prem_toks): |
| 398 | if tok.isdigit(): |
| 399 | if i < len(prem_toks) - 1: |
| 400 | prems.append([]) |
| 401 | else: |
| 402 | prems[-1].append(tok) |
| 403 | |
| 404 | if len(prems) > 2: |
| 405 | return 'ERROR: there cannot be more than two predicates.' |
| 406 | |
| 407 | clause_txt = point + ' = ' |
| 408 | constructions = [] |
| 409 | |
| 410 | for prem in prems: |
| 411 | name, *args = prem |
| 412 | |
| 413 | if point not in args: |
| 414 | return f'ERROR: {point} not found in predicate args.' |
| 415 | |
| 416 | if not check_valid_args(pt.map_symbol(name), args): |
| 417 | return 'ERROR: Invalid predicate ' + name + ' ' + ' '.join(args) |
| 418 | |
| 419 | for a in args: |
| 420 | if a != point and a not in existing_points: |
| 421 | return f'ERROR: point {a} does not exist.' |
| 422 | |
| 423 | try: |
| 424 | name, args = translate_constrained_to_constructive(point, name, args) |
| 425 | except: # pylint: disable=bare-except |
| 426 | return 'ERROR: Invalid predicate ' + name + ' ' + ' '.join(args) |
| 427 | |
| 428 | if name == 'on_aline': |
no test coverage detected