From 25bb3a845b5c7ff7cb051c132c2bb786b3227b07 Mon Sep 17 00:00:00 2001 From: Amade Nemes Date: Thu, 16 Nov 2023 22:14:16 +0100 Subject: [PATCH 1/8] Added auto-generated rules for ast replacement and marking children. --- .coveragerc | 4 +- src/renopro/asp/ast.lp | 117 ++++---- src/renopro/asp/child.lp | 518 +++++++++++++++++++++++++++++++++++ src/renopro/asp/replace.lp | 238 ++++++++++++++++ src/renopro/utils/codegen.py | 116 ++++++++ 5 files changed, 934 insertions(+), 59 deletions(-) create mode 100644 src/renopro/asp/child.lp create mode 100644 src/renopro/asp/replace.lp create mode 100644 src/renopro/utils/codegen.py diff --git a/.coveragerc b/.coveragerc index 6f85ed1..346670d 100644 --- a/.coveragerc +++ b/.coveragerc @@ -1,7 +1,9 @@ [run] source = renopro tests -omit = */renopro/__main__.py +omit = + */renopro/__main__.py + src/renopro/utils/codegen.py [report] exclude_lines = assert diff --git a/src/renopro/asp/ast.lp b/src/renopro/asp/ast.lp index 60543ee..d4a369a 100644 --- a/src/renopro/asp/ast.lp +++ b/src/renopro/asp/ast.lp @@ -1,59 +1,60 @@ -% tag ast facts. -ast(location(Id,position(F1,B1,E1),position(F2,B2,E2))) :- location(Id,position(F1,B1,E1),position(F2,B2,E2)). -ast(string(Id,Val)) :- string(Id,Val). -ast(number(Id,Val)) :- number(Id,Val). -ast(variable(Id,Name)) :- variable(Id,Name). -ast(unary_operation(Id,Operator,Argument)) :- unary_operation(Id,Operator,Argument). -ast(binary_operation(Id,Operator,Left,Right)) :- binary_operation(Id,Operator,Left,Right). -ast(interval(Id,Left,Right)) :- interval(Id,Left,Right). -ast(terms(Id,Pos,Element)) :- terms(Id,Pos,Element). -ast(function(Id,Name,Args)) :- function(Id,Name,Args). -ast(external_function(Id,Name,Args)) :- external_function(Id,Name,Args). -ast(pool(Id,Args)) :- pool(Id,Args). -ast(theory_terms(Id,Pos,Element)) :- theory_terms(Id,Pos,Element). -ast(theory_sequence(Id,SeqType,Terms)) :- theory_sequence(Id,SeqType,Terms). -ast(theory_function(Id,Name,Args)) :- theory_function(Id,Name,Args). -ast(theory_operators(Id,Pos,Operator)) :- theory_operators(Id,Pos,Operator). -ast(theory_unparsed_term_elements(Id,Pos,Operators,Term)) :- theory_unparsed_term_elements(Id,Pos,Operators,Term). -ast(theory_unparsed_term(Id,Elements)) :- theory_unparsed_term(Id,Elements). -ast(guard(Id,Op,Term)) :- guard(Id,Op,Term). -ast(guards(Id,Pos,Element)) :- guards(Id,Pos,Element). -ast(comparison(Id,Guards)) :- comparison(Id,Guards). -ast(boolean_constant(Id,Bool)) :- boolean_constant(Id,Bool). -ast(symbolic_atom(Id,Symbol)) :- symbolic_atom(Id,Symbol). -ast(literal(Id,Sign,Atom)) :- literal(Id,Sign,Atom). -ast(literals(Id,Pos,Element)) :- literals(Id,Pos,Element). -ast(conditional_literal(Id,Literal,Condition)) :- conditional_literal(Id,Literal,Condition). -ast(aggregate_elements(Id,Pos,Element)) :- aggregate_elements(Id,Pos,Element). -ast(aggregate(Id,LGuard,Elements,RGuard)) :- aggregate(Id,LGuard,Elements,RGuard). -ast(theory_atom_elements(Id,Pos,TheoryTerms,Condition)) :- theory_atom_elements(Id,Pos,TheoryTerms,Condition). -ast(theory_guard(Id,OpName,Term)) :- theory_guard(Id,OpName,Term). -ast(theory_atom(Id,Atom,Elements,TheoryGuard)) :- theory_atom(Id,Atom,Elements,TheoryGuard). -ast(body_aggregate_elements(Id,Pos,Terms,Condition)) :- body_aggregate_elements(Id,Pos,Terms,Condition). -ast(body_aggregate(Id,LGuard,Elements,RGuard)) :- body_aggregate(Id,LGuard,Elements,RGuard). -ast(body_literal(Id,Sign,Atom)) :- body_literal(Id,Sign,Atom). -ast(body_literals(Id,Pos,Element)) :- body_literals(Id,Pos,Element). -ast(head_aggregate_elements(Id,Pos,Terms,Condition)) :- head_aggregate_elements(Id,Pos,Terms,Condition). -ast(head_aggregate(Id,LGuard,Elements,RGuard)) :- head_aggregate(Id,LGuard,Elements,RGuard). -ast(conditional_literals(Id,Pos,CondLit)) :- conditional_literals(Id,Pos,CondLit). -ast(disjunction(Id,Pos,Element)) :- disjunction(Id,Pos,Element). -ast(rule(Id,Head,Body)) :- rule(Id,Head,Body). -ast(definition(Id,Name,Value,Default)) :- definition(Id,Name,Value,Default). -ast(show_signature(Id,Name,Arity,Positive)) :- show_signature(Id,Name,Arity,Positive). -ast(defined(Id,Name,Arity,Positive)) :- defined(Id,Name,Arity,Positive). -ast(minimize(Id,Weight,Priority,Terms,Body)) :- minimize(Id,Weight,Priority,Terms,Body). -ast(script(Id,Name,Code)) :- script(Id,Name,Code). -ast(statements(Id,Pos,Element)) :- statements(Id,Pos,Element). -ast(constants(Id,Pos,Element)) :- constants(Id,Pos,Element). -ast(program(Id,Name,Params,Statements)) :- program(Id,Name,Params,Statements). -ast(external(Atom,Body,Type)) :- external(Atom,Body,Type). -ast(edge(Id,U,V,Body)) :-edge(Id,U,V,Body). -ast(heuristic(Id,Atom,Body,Bias,Priority,Modifier)) :- heuristic(Id,Atom,Body,Bias,Priority,Modifier). -ast(project_atom(Id,Atom,Body)) :- project_atom(Id,Atom,Body). -ast(project_signature(Id,Name,Arity,Positive)) :- project_signature(Id,Name,Arity,Positive). -ast(theory_operator_definitions(Id,Pos,Name,Priority,OpType)) :- theory_operator_definitions(Id,Pos,Name,Priority,OpType). -ast(theory_term_definitions(Id,Pos,Name,Operators)) :- theory_term_definitions(Id,Pos,Name,Operators). -ast(theory_guard_definition(Id,Operators,Term)) :- theory_guard_definition(Id,Operators,Term). -ast(theory_atom_definitions(Id,Pos,AtomType,Name,Arity,Term,Guard)) :- theory_atom_definitions(Id,Pos,AtomType,Name,Arity,Term,Guard). -ast(theory_definition(Id,Name,Terms,Atoms)) :- theory_definition(Id,Name,Terms,Atoms). +% Rules to tag AST facts. +ast(string(X0,X1)) :- string(X0,X1). +ast(number(X0,X1)) :- number(X0,X1). +ast(variable(X0,X1)) :- variable(X0,X1). +ast(unary_operation(X0,X1,X2)) :- unary_operation(X0,X1,X2). +ast(binary_operation(X0,X1,X2,X3)) :- binary_operation(X0,X1,X2,X3). +ast(interval(X0,X1,X2)) :- interval(X0,X1,X2). +ast(terms(X0,X1,X2)) :- terms(X0,X1,X2). +ast(function(X0,X1,X2)) :- function(X0,X1,X2). +ast(external_function(X0,X1,X2)) :- external_function(X0,X1,X2). +ast(pool(X0,X1)) :- pool(X0,X1). +ast(theory_terms(X0,X1,X2)) :- theory_terms(X0,X1,X2). +ast(theory_sequence(X0,X1,X2)) :- theory_sequence(X0,X1,X2). +ast(theory_function(X0,X1,X2)) :- theory_function(X0,X1,X2). +ast(theory_operators(X0,X1,X2)) :- theory_operators(X0,X1,X2). +ast(theory_unparsed_term_elements(X0,X1,X2,X3)) :- theory_unparsed_term_elements(X0,X1,X2,X3). +ast(theory_unparsed_term(X0,X1)) :- theory_unparsed_term(X0,X1). +ast(guard(X0,X1,X2)) :- guard(X0,X1,X2). +ast(guards(X0,X1,X2)) :- guards(X0,X1,X2). +ast(comparison(X0,X1,X2)) :- comparison(X0,X1,X2). +ast(boolean_constant(X0,X1)) :- boolean_constant(X0,X1). +ast(symbolic_atom(X0,X1)) :- symbolic_atom(X0,X1). +ast(literal(X0,X1,X2)) :- literal(X0,X1,X2). +ast(literals(X0,X1,X2)) :- literals(X0,X1,X2). +ast(conditional_literal(X0,X1,X2)) :- conditional_literal(X0,X1,X2). +ast(aggregate_elements(X0,X1,X2)) :- aggregate_elements(X0,X1,X2). +ast(aggregate(X0,X1,X2,X3)) :- aggregate(X0,X1,X2,X3). +ast(theory_atom_elements(X0,X1,X2,X3)) :- theory_atom_elements(X0,X1,X2,X3). +ast(theory_guard(X0,X1,X2)) :- theory_guard(X0,X1,X2). +ast(theory_atom(X0,X1,X2,X3)) :- theory_atom(X0,X1,X2,X3). +ast(body_aggregate_elements(X0,X1,X2,X3)) :- body_aggregate_elements(X0,X1,X2,X3). +ast(body_aggregate(X0,X1,X2,X3,X4)) :- body_aggregate(X0,X1,X2,X3,X4). +ast(body_literal(X0,X1,X2)) :- body_literal(X0,X1,X2). +ast(body_literals(X0,X1,X2)) :- body_literals(X0,X1,X2). +ast(head_aggregate_elements(X0,X1,X2,X3)) :- head_aggregate_elements(X0,X1,X2,X3). +ast(head_aggregate(X0,X1,X2,X3,X4)) :- head_aggregate(X0,X1,X2,X3,X4). +ast(conditional_literals(X0,X1,X2)) :- conditional_literals(X0,X1,X2). +ast(disjunction(X0,X1)) :- disjunction(X0,X1). +ast(rule(X0,X1,X2)) :- rule(X0,X1,X2). +ast(definition(X0,X1,X2,X3)) :- definition(X0,X1,X2,X3). +ast(show_signature(X0,X1,X2,X3)) :- show_signature(X0,X1,X2,X3). +ast(defined(X0,X1,X2,X3)) :- defined(X0,X1,X2,X3). +ast(show_term(X0,X1,X2)) :- show_term(X0,X1,X2). +ast(minimize(X0,X1,X2,X3,X4)) :- minimize(X0,X1,X2,X3,X4). +ast(script(X0,X1,X2)) :- script(X0,X1,X2). +ast(statements(X0,X1,X2)) :- statements(X0,X1,X2). +ast(constants(X0,X1,X2)) :- constants(X0,X1,X2). +ast(program(X0,X1,X2,X3)) :- program(X0,X1,X2,X3). +ast(external(X0,X1,X2,X3)) :- external(X0,X1,X2,X3). +ast(edge(X0,X1,X2,X3)) :- edge(X0,X1,X2,X3). +ast(heuristic(X0,X1,X2,X3,X4,X5)) :- heuristic(X0,X1,X2,X3,X4,X5). +ast(project_atom(X0,X1,X2)) :- project_atom(X0,X1,X2). +ast(project_signature(X0,X1,X2,X3)) :- project_signature(X0,X1,X2,X3). +ast(theory_operator_definitions(X0,X1,X2,X3,X4)) :- theory_operator_definitions(X0,X1,X2,X3,X4). +ast(theory_term_definitions(X0,X1,X2,X3)) :- theory_term_definitions(X0,X1,X2,X3). +ast(theory_guard_definition(X0,X1,X2)) :- theory_guard_definition(X0,X1,X2). +ast(theory_atom_definitions(X0,X1,X2,X3,X4,X5,X6)) :- theory_atom_definitions(X0,X1,X2,X3,X4,X5,X6). +ast(theory_definition(X0,X1,X2,X3)) :- theory_definition(X0,X1,X2,X3). +ast(location(X0,X1,X2)) :- location(X0,X1,X2). diff --git a/src/renopro/asp/child.lp b/src/renopro/asp/child.lp new file mode 100644 index 0000000..3bad8ce --- /dev/null +++ b/src/renopro/asp/child.lp @@ -0,0 +1,518 @@ +% child(X,Y) holds if the ast fact with identifier X has a child fact +% with identifier Y. Note that identifiers X, Y are "typed"; +% that is, they are of the form ast_pred(id). + +child(unary_operation(X),string(Y)) :- unary_operation(X,_,Y), string(Y,_). + +child(unary_operation(X),number(Y)) :- unary_operation(X,_,Y), number(Y,_). + +child(unary_operation(X),variable(Y)) :- unary_operation(X,_,Y), variable(Y,_). + +child(unary_operation(X),unary_operation(Y)) :- unary_operation(X,_,Y), unary_operation(Y,_,_). + +child(unary_operation(X),binary_operation(Y)) :- unary_operation(X,_,Y), binary_operation(Y,_,_,_). + +child(unary_operation(X),interval(Y)) :- unary_operation(X,_,Y), interval(Y,_,_). + +child(unary_operation(X),function(Y)) :- unary_operation(X,_,Y), function(Y,_,_). + +child(unary_operation(X),external_function(Y)) :- unary_operation(X,_,Y), external_function(Y,_,_). + +child(unary_operation(X),pool(Y)) :- unary_operation(X,_,Y), pool(Y,_). + +child(binary_operation(X),string(Y)) :- binary_operation(X,_,Y,_), string(Y,_). + +child(binary_operation(X),number(Y)) :- binary_operation(X,_,Y,_), number(Y,_). + +child(binary_operation(X),variable(Y)) :- binary_operation(X,_,Y,_), variable(Y,_). + +child(binary_operation(X),unary_operation(Y)) :- binary_operation(X,_,Y,_), unary_operation(Y,_,_). + +child(binary_operation(X),binary_operation(Y)) :- binary_operation(X,_,Y,_), binary_operation(Y,_,_,_). + +child(binary_operation(X),interval(Y)) :- binary_operation(X,_,Y,_), interval(Y,_,_). + +child(binary_operation(X),function(Y)) :- binary_operation(X,_,Y,_), function(Y,_,_). + +child(binary_operation(X),external_function(Y)) :- binary_operation(X,_,Y,_), external_function(Y,_,_). + +child(binary_operation(X),pool(Y)) :- binary_operation(X,_,Y,_), pool(Y,_). + +child(binary_operation(X),string(Y)) :- binary_operation(X,_,_,Y), string(Y,_). + +child(binary_operation(X),number(Y)) :- binary_operation(X,_,_,Y), number(Y,_). + +child(binary_operation(X),variable(Y)) :- binary_operation(X,_,_,Y), variable(Y,_). + +child(binary_operation(X),unary_operation(Y)) :- binary_operation(X,_,_,Y), unary_operation(Y,_,_). + +child(binary_operation(X),binary_operation(Y)) :- binary_operation(X,_,_,Y), binary_operation(Y,_,_,_). + +child(binary_operation(X),interval(Y)) :- binary_operation(X,_,_,Y), interval(Y,_,_). + +child(binary_operation(X),function(Y)) :- binary_operation(X,_,_,Y), function(Y,_,_). + +child(binary_operation(X),external_function(Y)) :- binary_operation(X,_,_,Y), external_function(Y,_,_). + +child(binary_operation(X),pool(Y)) :- binary_operation(X,_,_,Y), pool(Y,_). + +child(interval(X),string(Y)) :- interval(X,Y,_), string(Y,_). + +child(interval(X),number(Y)) :- interval(X,Y,_), number(Y,_). + +child(interval(X),variable(Y)) :- interval(X,Y,_), variable(Y,_). + +child(interval(X),unary_operation(Y)) :- interval(X,Y,_), unary_operation(Y,_,_). + +child(interval(X),binary_operation(Y)) :- interval(X,Y,_), binary_operation(Y,_,_,_). + +child(interval(X),interval(Y)) :- interval(X,Y,_), interval(Y,_,_). + +child(interval(X),function(Y)) :- interval(X,Y,_), function(Y,_,_). + +child(interval(X),external_function(Y)) :- interval(X,Y,_), external_function(Y,_,_). + +child(interval(X),pool(Y)) :- interval(X,Y,_), pool(Y,_). + +child(interval(X),string(Y)) :- interval(X,_,Y), string(Y,_). + +child(interval(X),number(Y)) :- interval(X,_,Y), number(Y,_). + +child(interval(X),variable(Y)) :- interval(X,_,Y), variable(Y,_). + +child(interval(X),unary_operation(Y)) :- interval(X,_,Y), unary_operation(Y,_,_). + +child(interval(X),binary_operation(Y)) :- interval(X,_,Y), binary_operation(Y,_,_,_). + +child(interval(X),interval(Y)) :- interval(X,_,Y), interval(Y,_,_). + +child(interval(X),function(Y)) :- interval(X,_,Y), function(Y,_,_). + +child(interval(X),external_function(Y)) :- interval(X,_,Y), external_function(Y,_,_). + +child(interval(X),pool(Y)) :- interval(X,_,Y), pool(Y,_). + +child(terms(X),string(Y)) :- terms(X,_,Y), string(Y,_). + +child(terms(X),number(Y)) :- terms(X,_,Y), number(Y,_). + +child(terms(X),variable(Y)) :- terms(X,_,Y), variable(Y,_). + +child(terms(X),unary_operation(Y)) :- terms(X,_,Y), unary_operation(Y,_,_). + +child(terms(X),binary_operation(Y)) :- terms(X,_,Y), binary_operation(Y,_,_,_). + +child(terms(X),interval(Y)) :- terms(X,_,Y), interval(Y,_,_). + +child(terms(X),function(Y)) :- terms(X,_,Y), function(Y,_,_). + +child(terms(X),external_function(Y)) :- terms(X,_,Y), external_function(Y,_,_). + +child(terms(X),pool(Y)) :- terms(X,_,Y), pool(Y,_). + +child(function(X),terms(Y)) :- function(X,_,Y), terms(Y,_,_). + +child(external_function(X),terms(Y)) :- external_function(X,_,Y), terms(Y,_,_). + +child(pool(X),terms(Y)) :- pool(X,Y), terms(Y,_,_). + +child(theory_terms(X),string(Y)) :- theory_terms(X,_,Y), string(Y,_). + +child(theory_terms(X),number(Y)) :- theory_terms(X,_,Y), number(Y,_). + +child(theory_terms(X),function(Y)) :- theory_terms(X,_,Y), function(Y,_,_). + +child(theory_terms(X),variable(Y)) :- theory_terms(X,_,Y), variable(Y,_). + +child(theory_terms(X),theory_sequence(Y)) :- theory_terms(X,_,Y), theory_sequence(Y,_,_). + +child(theory_terms(X),theory_function(Y)) :- theory_terms(X,_,Y), theory_function(Y,_,_). + +child(theory_terms(X),theory_unparsed_term(Y)) :- theory_terms(X,_,Y), theory_unparsed_term(Y,_). + +child(theory_sequence(X),theory_terms(Y)) :- theory_sequence(X,_,Y), theory_terms(Y,_,_). + +child(theory_function(X),theory_terms(Y)) :- theory_function(X,_,Y), theory_terms(Y,_,_). + +child(theory_unparsed_term_elements(X),theory_operators(Y)) :- theory_unparsed_term_elements(X,_,Y,_), theory_operators(Y,_,_). + +child(theory_unparsed_term_elements(X),string(Y)) :- theory_unparsed_term_elements(X,_,_,Y), string(Y,_). + +child(theory_unparsed_term_elements(X),number(Y)) :- theory_unparsed_term_elements(X,_,_,Y), number(Y,_). + +child(theory_unparsed_term_elements(X),function(Y)) :- theory_unparsed_term_elements(X,_,_,Y), function(Y,_,_). + +child(theory_unparsed_term_elements(X),variable(Y)) :- theory_unparsed_term_elements(X,_,_,Y), variable(Y,_). + +child(theory_unparsed_term_elements(X),theory_sequence(Y)) :- theory_unparsed_term_elements(X,_,_,Y), theory_sequence(Y,_,_). + +child(theory_unparsed_term_elements(X),theory_function(Y)) :- theory_unparsed_term_elements(X,_,_,Y), theory_function(Y,_,_). + +child(theory_unparsed_term_elements(X),theory_unparsed_term(Y)) :- theory_unparsed_term_elements(X,_,_,Y), theory_unparsed_term(Y,_). + +child(theory_unparsed_term(X),theory_unparsed_term_elements(Y)) :- theory_unparsed_term(X,Y), theory_unparsed_term_elements(Y,_,_,_). + +child(guard(X),string(Y)) :- guard(X,_,Y), string(Y,_). + +child(guard(X),number(Y)) :- guard(X,_,Y), number(Y,_). + +child(guard(X),variable(Y)) :- guard(X,_,Y), variable(Y,_). + +child(guard(X),unary_operation(Y)) :- guard(X,_,Y), unary_operation(Y,_,_). + +child(guard(X),binary_operation(Y)) :- guard(X,_,Y), binary_operation(Y,_,_,_). + +child(guard(X),interval(Y)) :- guard(X,_,Y), interval(Y,_,_). + +child(guard(X),function(Y)) :- guard(X,_,Y), function(Y,_,_). + +child(guard(X),external_function(Y)) :- guard(X,_,Y), external_function(Y,_,_). + +child(guard(X),pool(Y)) :- guard(X,_,Y), pool(Y,_). + +child(guards(X),guard(Y)) :- guards(X,_,Y), guard(Y,_,_). + +child(comparison(X),string(Y)) :- comparison(X,Y,_), string(Y,_). + +child(comparison(X),number(Y)) :- comparison(X,Y,_), number(Y,_). + +child(comparison(X),variable(Y)) :- comparison(X,Y,_), variable(Y,_). + +child(comparison(X),unary_operation(Y)) :- comparison(X,Y,_), unary_operation(Y,_,_). + +child(comparison(X),binary_operation(Y)) :- comparison(X,Y,_), binary_operation(Y,_,_,_). + +child(comparison(X),interval(Y)) :- comparison(X,Y,_), interval(Y,_,_). + +child(comparison(X),function(Y)) :- comparison(X,Y,_), function(Y,_,_). + +child(comparison(X),external_function(Y)) :- comparison(X,Y,_), external_function(Y,_,_). + +child(comparison(X),pool(Y)) :- comparison(X,Y,_), pool(Y,_). + +child(comparison(X),guards(Y)) :- comparison(X,_,Y), guards(Y,_,_). + +child(symbolic_atom(X),function(Y)) :- symbolic_atom(X,Y), function(Y,_,_). + +child(literal(X),symbolic_atom(Y)) :- literal(X,_,Y), symbolic_atom(Y,_). + +child(literal(X),comparison(Y)) :- literal(X,_,Y), comparison(Y,_,_). + +child(literal(X),boolean_constant(Y)) :- literal(X,_,Y), boolean_constant(Y,_). + +child(literals(X),literal(Y)) :- literals(X,_,Y), literal(Y,_,_). + +child(conditional_literal(X),literal(Y)) :- conditional_literal(X,Y,_), literal(Y,_,_). + +child(conditional_literal(X),literals(Y)) :- conditional_literal(X,_,Y), literals(Y,_,_). + +child(aggregate_elements(X),conditional_literal(Y)) :- aggregate_elements(X,_,Y), conditional_literal(Y,_,_). + +child(aggregate(X),guard(Y)) :- aggregate(X,Y,_,_), guard(Y,_,_). + +child(aggregate(X),aggregate_elements(Y)) :- aggregate(X,_,Y,_), aggregate_elements(Y,_,_). + +child(aggregate(X),guard(Y)) :- aggregate(X,_,_,Y), guard(Y,_,_). + +child(theory_atom_elements(X),theory_terms(Y)) :- theory_atom_elements(X,_,Y,_), theory_terms(Y,_,_). + +child(theory_atom_elements(X),literals(Y)) :- theory_atom_elements(X,_,_,Y), literals(Y,_,_). + +child(theory_guard(X),string(Y)) :- theory_guard(X,_,Y), string(Y,_). + +child(theory_guard(X),number(Y)) :- theory_guard(X,_,Y), number(Y,_). + +child(theory_guard(X),function(Y)) :- theory_guard(X,_,Y), function(Y,_,_). + +child(theory_guard(X),variable(Y)) :- theory_guard(X,_,Y), variable(Y,_). + +child(theory_guard(X),theory_sequence(Y)) :- theory_guard(X,_,Y), theory_sequence(Y,_,_). + +child(theory_guard(X),theory_function(Y)) :- theory_guard(X,_,Y), theory_function(Y,_,_). + +child(theory_guard(X),theory_unparsed_term(Y)) :- theory_guard(X,_,Y), theory_unparsed_term(Y,_). + +child(theory_atom(X),function(Y)) :- theory_atom(X,Y,_,_), function(Y,_,_). + +child(theory_atom(X),theory_atom_elements(Y)) :- theory_atom(X,_,Y,_), theory_atom_elements(Y,_,_,_). + +child(theory_atom(X),theory_guard(Y)) :- theory_atom(X,_,_,Y), theory_guard(Y,_,_). + +child(body_aggregate_elements(X),terms(Y)) :- body_aggregate_elements(X,_,Y,_), terms(Y,_,_). + +child(body_aggregate_elements(X),literals(Y)) :- body_aggregate_elements(X,_,_,Y), literals(Y,_,_). + +child(body_aggregate(X),guard(Y)) :- body_aggregate(X,Y,_,_,_), guard(Y,_,_). + +child(body_aggregate(X),body_aggregate_elements(Y)) :- body_aggregate(X,_,_,Y,_), body_aggregate_elements(Y,_,_,_). + +child(body_aggregate(X),guard(Y)) :- body_aggregate(X,_,_,_,Y), guard(Y,_,_). + +child(body_literal(X),symbolic_atom(Y)) :- body_literal(X,_,Y), symbolic_atom(Y,_). + +child(body_literal(X),comparison(Y)) :- body_literal(X,_,Y), comparison(Y,_,_). + +child(body_literal(X),boolean_constant(Y)) :- body_literal(X,_,Y), boolean_constant(Y,_). + +child(body_literal(X),aggregate(Y)) :- body_literal(X,_,Y), aggregate(Y,_,_,_). + +child(body_literal(X),body_aggregate(Y)) :- body_literal(X,_,Y), body_aggregate(Y,_,_,_,_). + +child(body_literal(X),theory_atom(Y)) :- body_literal(X,_,Y), theory_atom(Y,_,_,_). + +child(body_literals(X),body_literal(Y)) :- body_literals(X,_,Y), body_literal(Y,_,_). + +child(body_literals(X),conditional_literal(Y)) :- body_literals(X,_,Y), conditional_literal(Y,_,_). + +child(head_aggregate_elements(X),terms(Y)) :- head_aggregate_elements(X,_,Y,_), terms(Y,_,_). + +child(head_aggregate_elements(X),conditional_literal(Y)) :- head_aggregate_elements(X,_,_,Y), conditional_literal(Y,_,_). + +child(head_aggregate(X),guard(Y)) :- head_aggregate(X,Y,_,_,_), guard(Y,_,_). + +child(head_aggregate(X),head_aggregate_elements(Y)) :- head_aggregate(X,_,_,Y,_), head_aggregate_elements(Y,_,_,_). + +child(head_aggregate(X),guard(Y)) :- head_aggregate(X,_,_,_,Y), guard(Y,_,_). + +child(conditional_literals(X),conditional_literal(Y)) :- conditional_literals(X,_,Y), conditional_literal(Y,_,_). + +child(disjunction(X),conditional_literals(Y)) :- disjunction(X,Y), conditional_literals(Y,_,_). + +child(rule(X),literal(Y)) :- rule(X,Y,_), literal(Y,_,_). + +child(rule(X),aggregate(Y)) :- rule(X,Y,_), aggregate(Y,_,_,_). + +child(rule(X),head_aggregate(Y)) :- rule(X,Y,_), head_aggregate(Y,_,_,_,_). + +child(rule(X),disjunction(Y)) :- rule(X,Y,_), disjunction(Y,_). + +child(rule(X),theory_atom(Y)) :- rule(X,Y,_), theory_atom(Y,_,_,_). + +child(rule(X),body_literals(Y)) :- rule(X,_,Y), body_literals(Y,_,_). + +child(definition(X),string(Y)) :- definition(X,_,Y,_), string(Y,_). + +child(definition(X),number(Y)) :- definition(X,_,Y,_), number(Y,_). + +child(definition(X),variable(Y)) :- definition(X,_,Y,_), variable(Y,_). + +child(definition(X),unary_operation(Y)) :- definition(X,_,Y,_), unary_operation(Y,_,_). + +child(definition(X),binary_operation(Y)) :- definition(X,_,Y,_), binary_operation(Y,_,_,_). + +child(definition(X),interval(Y)) :- definition(X,_,Y,_), interval(Y,_,_). + +child(definition(X),function(Y)) :- definition(X,_,Y,_), function(Y,_,_). + +child(definition(X),external_function(Y)) :- definition(X,_,Y,_), external_function(Y,_,_). + +child(definition(X),pool(Y)) :- definition(X,_,Y,_), pool(Y,_). + +child(show_term(X),string(Y)) :- show_term(X,Y,_), string(Y,_). + +child(show_term(X),number(Y)) :- show_term(X,Y,_), number(Y,_). + +child(show_term(X),variable(Y)) :- show_term(X,Y,_), variable(Y,_). + +child(show_term(X),unary_operation(Y)) :- show_term(X,Y,_), unary_operation(Y,_,_). + +child(show_term(X),binary_operation(Y)) :- show_term(X,Y,_), binary_operation(Y,_,_,_). + +child(show_term(X),interval(Y)) :- show_term(X,Y,_), interval(Y,_,_). + +child(show_term(X),function(Y)) :- show_term(X,Y,_), function(Y,_,_). + +child(show_term(X),external_function(Y)) :- show_term(X,Y,_), external_function(Y,_,_). + +child(show_term(X),pool(Y)) :- show_term(X,Y,_), pool(Y,_). + +child(show_term(X),body_literals(Y)) :- show_term(X,_,Y), body_literals(Y,_,_). + +child(minimize(X),string(Y)) :- minimize(X,Y,_,_,_), string(Y,_). + +child(minimize(X),number(Y)) :- minimize(X,Y,_,_,_), number(Y,_). + +child(minimize(X),variable(Y)) :- minimize(X,Y,_,_,_), variable(Y,_). + +child(minimize(X),unary_operation(Y)) :- minimize(X,Y,_,_,_), unary_operation(Y,_,_). + +child(minimize(X),binary_operation(Y)) :- minimize(X,Y,_,_,_), binary_operation(Y,_,_,_). + +child(minimize(X),interval(Y)) :- minimize(X,Y,_,_,_), interval(Y,_,_). + +child(minimize(X),function(Y)) :- minimize(X,Y,_,_,_), function(Y,_,_). + +child(minimize(X),external_function(Y)) :- minimize(X,Y,_,_,_), external_function(Y,_,_). + +child(minimize(X),pool(Y)) :- minimize(X,Y,_,_,_), pool(Y,_). + +child(minimize(X),string(Y)) :- minimize(X,_,Y,_,_), string(Y,_). + +child(minimize(X),number(Y)) :- minimize(X,_,Y,_,_), number(Y,_). + +child(minimize(X),variable(Y)) :- minimize(X,_,Y,_,_), variable(Y,_). + +child(minimize(X),unary_operation(Y)) :- minimize(X,_,Y,_,_), unary_operation(Y,_,_). + +child(minimize(X),binary_operation(Y)) :- minimize(X,_,Y,_,_), binary_operation(Y,_,_,_). + +child(minimize(X),interval(Y)) :- minimize(X,_,Y,_,_), interval(Y,_,_). + +child(minimize(X),function(Y)) :- minimize(X,_,Y,_,_), function(Y,_,_). + +child(minimize(X),external_function(Y)) :- minimize(X,_,Y,_,_), external_function(Y,_,_). + +child(minimize(X),pool(Y)) :- minimize(X,_,Y,_,_), pool(Y,_). + +child(minimize(X),terms(Y)) :- minimize(X,_,_,Y,_), terms(Y,_,_). + +child(minimize(X),body_literals(Y)) :- minimize(X,_,_,_,Y), body_literals(Y,_,_). + +child(statements(X),rule(Y)) :- statements(X,_,Y), rule(Y,_,_). + +child(statements(X),definition(Y)) :- statements(X,_,Y), definition(Y,_,_,_). + +child(statements(X),show_signature(Y)) :- statements(X,_,Y), show_signature(Y,_,_,_). + +child(statements(X),defined(Y)) :- statements(X,_,Y), defined(Y,_,_,_). + +child(statements(X),show_term(Y)) :- statements(X,_,Y), show_term(Y,_,_). + +child(statements(X),minimize(Y)) :- statements(X,_,Y), minimize(Y,_,_,_,_). + +child(statements(X),script(Y)) :- statements(X,_,Y), script(Y,_,_). + +child(statements(X),external(Y)) :- statements(X,_,Y), external(Y,_,_,_). + +child(statements(X),edge(Y)) :- statements(X,_,Y), edge(Y,_,_,_). + +child(statements(X),heuristic(Y)) :- statements(X,_,Y), heuristic(Y,_,_,_,_,_). + +child(statements(X),project_atom(Y)) :- statements(X,_,Y), project_atom(Y,_,_). + +child(statements(X),project_signature(Y)) :- statements(X,_,Y), project_signature(Y,_,_,_). + +child(statements(X),theory_definition(Y)) :- statements(X,_,Y), theory_definition(Y,_,_,_). + +child(constants(X),function(Y)) :- constants(X,_,Y), function(Y,_,_). + +child(program(X),constants(Y)) :- program(X,_,Y,_), constants(Y,_,_). + +child(program(X),statements(Y)) :- program(X,_,_,Y), statements(Y,_,_). + +child(external(X),symbolic_atom(Y)) :- external(X,Y,_,_), symbolic_atom(Y,_). + +child(external(X),body_literals(Y)) :- external(X,_,Y,_), body_literals(Y,_,_). + +child(edge(X),string(Y)) :- edge(X,Y,_,_), string(Y,_). + +child(edge(X),number(Y)) :- edge(X,Y,_,_), number(Y,_). + +child(edge(X),variable(Y)) :- edge(X,Y,_,_), variable(Y,_). + +child(edge(X),unary_operation(Y)) :- edge(X,Y,_,_), unary_operation(Y,_,_). + +child(edge(X),binary_operation(Y)) :- edge(X,Y,_,_), binary_operation(Y,_,_,_). + +child(edge(X),interval(Y)) :- edge(X,Y,_,_), interval(Y,_,_). + +child(edge(X),function(Y)) :- edge(X,Y,_,_), function(Y,_,_). + +child(edge(X),external_function(Y)) :- edge(X,Y,_,_), external_function(Y,_,_). + +child(edge(X),pool(Y)) :- edge(X,Y,_,_), pool(Y,_). + +child(edge(X),string(Y)) :- edge(X,_,Y,_), string(Y,_). + +child(edge(X),number(Y)) :- edge(X,_,Y,_), number(Y,_). + +child(edge(X),variable(Y)) :- edge(X,_,Y,_), variable(Y,_). + +child(edge(X),unary_operation(Y)) :- edge(X,_,Y,_), unary_operation(Y,_,_). + +child(edge(X),binary_operation(Y)) :- edge(X,_,Y,_), binary_operation(Y,_,_,_). + +child(edge(X),interval(Y)) :- edge(X,_,Y,_), interval(Y,_,_). + +child(edge(X),function(Y)) :- edge(X,_,Y,_), function(Y,_,_). + +child(edge(X),external_function(Y)) :- edge(X,_,Y,_), external_function(Y,_,_). + +child(edge(X),pool(Y)) :- edge(X,_,Y,_), pool(Y,_). + +child(edge(X),body_literals(Y)) :- edge(X,_,_,Y), body_literals(Y,_,_). + +child(heuristic(X),symbolic_atom(Y)) :- heuristic(X,Y,_,_,_,_), symbolic_atom(Y,_). + +child(heuristic(X),body_literals(Y)) :- heuristic(X,_,Y,_,_,_), body_literals(Y,_,_). + +child(heuristic(X),string(Y)) :- heuristic(X,_,_,Y,_,_), string(Y,_). + +child(heuristic(X),number(Y)) :- heuristic(X,_,_,Y,_,_), number(Y,_). + +child(heuristic(X),variable(Y)) :- heuristic(X,_,_,Y,_,_), variable(Y,_). + +child(heuristic(X),unary_operation(Y)) :- heuristic(X,_,_,Y,_,_), unary_operation(Y,_,_). + +child(heuristic(X),binary_operation(Y)) :- heuristic(X,_,_,Y,_,_), binary_operation(Y,_,_,_). + +child(heuristic(X),interval(Y)) :- heuristic(X,_,_,Y,_,_), interval(Y,_,_). + +child(heuristic(X),function(Y)) :- heuristic(X,_,_,Y,_,_), function(Y,_,_). + +child(heuristic(X),external_function(Y)) :- heuristic(X,_,_,Y,_,_), external_function(Y,_,_). + +child(heuristic(X),pool(Y)) :- heuristic(X,_,_,Y,_,_), pool(Y,_). + +child(heuristic(X),string(Y)) :- heuristic(X,_,_,_,Y,_), string(Y,_). + +child(heuristic(X),number(Y)) :- heuristic(X,_,_,_,Y,_), number(Y,_). + +child(heuristic(X),variable(Y)) :- heuristic(X,_,_,_,Y,_), variable(Y,_). + +child(heuristic(X),unary_operation(Y)) :- heuristic(X,_,_,_,Y,_), unary_operation(Y,_,_). + +child(heuristic(X),binary_operation(Y)) :- heuristic(X,_,_,_,Y,_), binary_operation(Y,_,_,_). + +child(heuristic(X),interval(Y)) :- heuristic(X,_,_,_,Y,_), interval(Y,_,_). + +child(heuristic(X),function(Y)) :- heuristic(X,_,_,_,Y,_), function(Y,_,_). + +child(heuristic(X),external_function(Y)) :- heuristic(X,_,_,_,Y,_), external_function(Y,_,_). + +child(heuristic(X),pool(Y)) :- heuristic(X,_,_,_,Y,_), pool(Y,_). + +child(heuristic(X),string(Y)) :- heuristic(X,_,_,_,_,Y), string(Y,_). + +child(heuristic(X),number(Y)) :- heuristic(X,_,_,_,_,Y), number(Y,_). + +child(heuristic(X),variable(Y)) :- heuristic(X,_,_,_,_,Y), variable(Y,_). + +child(heuristic(X),unary_operation(Y)) :- heuristic(X,_,_,_,_,Y), unary_operation(Y,_,_). + +child(heuristic(X),binary_operation(Y)) :- heuristic(X,_,_,_,_,Y), binary_operation(Y,_,_,_). + +child(heuristic(X),interval(Y)) :- heuristic(X,_,_,_,_,Y), interval(Y,_,_). + +child(heuristic(X),function(Y)) :- heuristic(X,_,_,_,_,Y), function(Y,_,_). + +child(heuristic(X),external_function(Y)) :- heuristic(X,_,_,_,_,Y), external_function(Y,_,_). + +child(heuristic(X),pool(Y)) :- heuristic(X,_,_,_,_,Y), pool(Y,_). + +child(project_atom(X),symbolic_atom(Y)) :- project_atom(X,Y,_), symbolic_atom(Y,_). + +child(project_atom(X),body_literals(Y)) :- project_atom(X,_,Y), body_literals(Y,_,_). + +child(theory_term_definitions(X),theory_operator_definitions(Y)) :- theory_term_definitions(X,_,_,Y), theory_operator_definitions(Y,_,_,_,_). + +child(theory_guard_definition(X),theory_operators(Y)) :- theory_guard_definition(X,Y,_), theory_operators(Y,_,_). + +child(theory_atom_definitions(X),theory_guard_definition(Y)) :- theory_atom_definitions(X,_,_,_,_,_,Y), theory_guard_definition(Y,_,_). + +child(theory_definition(X),theory_term_definitions(Y)) :- theory_definition(X,_,Y,_), theory_term_definitions(Y,_,_,_). + +child(theory_definition(X),theory_atom_definitions(Y)) :- theory_definition(X,_,_,Y), theory_atom_definitions(Y,_,_,_,_,_,_). + +node(theory_definition(X)) :- theory_definition(X,_,_,Y). + diff --git a/src/renopro/asp/replace.lp b/src/renopro/asp/replace.lp new file mode 100644 index 0000000..6c86fcb --- /dev/null +++ b/src/renopro/asp/replace.lp @@ -0,0 +1,238 @@ +% replace(A,B) replaces a child predicate identifier A +% with child predicate identifier B in each AST fact where A +% occurs as a term. + +ast_operation(add(unary_operation(X0,X1,B));delete(unary_operation(X0,X1,A))) + :- ast_operation(replace(A,B)), unary_operation(X0,X1,A). + +ast_operation(add(binary_operation(X0,X1,B,X3));delete(binary_operation(X0,X1,A,X3))) + :- ast_operation(replace(A,B)), binary_operation(X0,X1,A,X3). + +ast_operation(add(binary_operation(X0,X1,X2,B));delete(binary_operation(X0,X1,X2,A))) + :- ast_operation(replace(A,B)), binary_operation(X0,X1,X2,A). + +ast_operation(add(interval(X0,B,X2));delete(interval(X0,A,X2))) + :- ast_operation(replace(A,B)), interval(X0,A,X2). + +ast_operation(add(interval(X0,X1,B));delete(interval(X0,X1,A))) + :- ast_operation(replace(A,B)), interval(X0,X1,A). + +ast_operation(add(terms(X0,X1,B));delete(terms(X0,X1,A))) + :- ast_operation(replace(A,B)), terms(X0,X1,A). + +ast_operation(add(function(X0,X1,B));delete(function(X0,X1,A))) + :- ast_operation(replace(A,B)), function(X0,X1,A). + +ast_operation(add(external_function(X0,X1,B));delete(external_function(X0,X1,A))) + :- ast_operation(replace(A,B)), external_function(X0,X1,A). + +ast_operation(add(pool(X0,B));delete(pool(X0,A))) + :- ast_operation(replace(A,B)), pool(X0,A). + +ast_operation(add(theory_terms(X0,X1,B));delete(theory_terms(X0,X1,A))) + :- ast_operation(replace(A,B)), theory_terms(X0,X1,A). + +ast_operation(add(theory_sequence(X0,X1,B));delete(theory_sequence(X0,X1,A))) + :- ast_operation(replace(A,B)), theory_sequence(X0,X1,A). + +ast_operation(add(theory_function(X0,X1,B));delete(theory_function(X0,X1,A))) + :- ast_operation(replace(A,B)), theory_function(X0,X1,A). + +ast_operation(add(theory_unparsed_term_elements(X0,X1,B,X3));delete(theory_unparsed_term_elements(X0,X1,A,X3))) + :- ast_operation(replace(A,B)), theory_unparsed_term_elements(X0,X1,A,X3). + +ast_operation(add(theory_unparsed_term_elements(X0,X1,X2,B));delete(theory_unparsed_term_elements(X0,X1,X2,A))) + :- ast_operation(replace(A,B)), theory_unparsed_term_elements(X0,X1,X2,A). + +ast_operation(add(theory_unparsed_term(X0,B));delete(theory_unparsed_term(X0,A))) + :- ast_operation(replace(A,B)), theory_unparsed_term(X0,A). + +ast_operation(add(guard(X0,X1,B));delete(guard(X0,X1,A))) + :- ast_operation(replace(A,B)), guard(X0,X1,A). + +ast_operation(add(guards(X0,X1,B));delete(guards(X0,X1,A))) + :- ast_operation(replace(A,B)), guards(X0,X1,A). + +ast_operation(add(comparison(X0,B,X2));delete(comparison(X0,A,X2))) + :- ast_operation(replace(A,B)), comparison(X0,A,X2). + +ast_operation(add(comparison(X0,X1,B));delete(comparison(X0,X1,A))) + :- ast_operation(replace(A,B)), comparison(X0,X1,A). + +ast_operation(add(symbolic_atom(X0,B));delete(symbolic_atom(X0,A))) + :- ast_operation(replace(A,B)), symbolic_atom(X0,A). + +ast_operation(add(literal(X0,X1,B));delete(literal(X0,X1,A))) + :- ast_operation(replace(A,B)), literal(X0,X1,A). + +ast_operation(add(literals(X0,X1,B));delete(literals(X0,X1,A))) + :- ast_operation(replace(A,B)), literals(X0,X1,A). + +ast_operation(add(conditional_literal(X0,B,X2));delete(conditional_literal(X0,A,X2))) + :- ast_operation(replace(A,B)), conditional_literal(X0,A,X2). + +ast_operation(add(conditional_literal(X0,X1,B));delete(conditional_literal(X0,X1,A))) + :- ast_operation(replace(A,B)), conditional_literal(X0,X1,A). + +ast_operation(add(aggregate_elements(X0,X1,B));delete(aggregate_elements(X0,X1,A))) + :- ast_operation(replace(A,B)), aggregate_elements(X0,X1,A). + +ast_operation(add(aggregate(X0,B,X2,X3));delete(aggregate(X0,A,X2,X3))) + :- ast_operation(replace(A,B)), aggregate(X0,A,X2,X3). + +ast_operation(add(aggregate(X0,X1,B,X3));delete(aggregate(X0,X1,A,X3))) + :- ast_operation(replace(A,B)), aggregate(X0,X1,A,X3). + +ast_operation(add(aggregate(X0,X1,X2,B));delete(aggregate(X0,X1,X2,A))) + :- ast_operation(replace(A,B)), aggregate(X0,X1,X2,A). + +ast_operation(add(theory_atom_elements(X0,X1,B,X3));delete(theory_atom_elements(X0,X1,A,X3))) + :- ast_operation(replace(A,B)), theory_atom_elements(X0,X1,A,X3). + +ast_operation(add(theory_atom_elements(X0,X1,X2,B));delete(theory_atom_elements(X0,X1,X2,A))) + :- ast_operation(replace(A,B)), theory_atom_elements(X0,X1,X2,A). + +ast_operation(add(theory_guard(X0,X1,B));delete(theory_guard(X0,X1,A))) + :- ast_operation(replace(A,B)), theory_guard(X0,X1,A). + +ast_operation(add(theory_atom(X0,B,X2,X3));delete(theory_atom(X0,A,X2,X3))) + :- ast_operation(replace(A,B)), theory_atom(X0,A,X2,X3). + +ast_operation(add(theory_atom(X0,X1,B,X3));delete(theory_atom(X0,X1,A,X3))) + :- ast_operation(replace(A,B)), theory_atom(X0,X1,A,X3). + +ast_operation(add(theory_atom(X0,X1,X2,B));delete(theory_atom(X0,X1,X2,A))) + :- ast_operation(replace(A,B)), theory_atom(X0,X1,X2,A). + +ast_operation(add(body_aggregate_elements(X0,X1,B,X3));delete(body_aggregate_elements(X0,X1,A,X3))) + :- ast_operation(replace(A,B)), body_aggregate_elements(X0,X1,A,X3). + +ast_operation(add(body_aggregate_elements(X0,X1,X2,B));delete(body_aggregate_elements(X0,X1,X2,A))) + :- ast_operation(replace(A,B)), body_aggregate_elements(X0,X1,X2,A). + +ast_operation(add(body_aggregate(X0,B,X2,X3,X4));delete(body_aggregate(X0,A,X2,X3,X4))) + :- ast_operation(replace(A,B)), body_aggregate(X0,A,X2,X3,X4). + +ast_operation(add(body_aggregate(X0,X1,X2,B,X4));delete(body_aggregate(X0,X1,X2,A,X4))) + :- ast_operation(replace(A,B)), body_aggregate(X0,X1,X2,A,X4). + +ast_operation(add(body_aggregate(X0,X1,X2,X3,B));delete(body_aggregate(X0,X1,X2,X3,A))) + :- ast_operation(replace(A,B)), body_aggregate(X0,X1,X2,X3,A). + +ast_operation(add(body_literal(X0,X1,B));delete(body_literal(X0,X1,A))) + :- ast_operation(replace(A,B)), body_literal(X0,X1,A). + +ast_operation(add(body_literals(X0,X1,B));delete(body_literals(X0,X1,A))) + :- ast_operation(replace(A,B)), body_literals(X0,X1,A). + +ast_operation(add(head_aggregate_elements(X0,X1,B,X3));delete(head_aggregate_elements(X0,X1,A,X3))) + :- ast_operation(replace(A,B)), head_aggregate_elements(X0,X1,A,X3). + +ast_operation(add(head_aggregate_elements(X0,X1,X2,B));delete(head_aggregate_elements(X0,X1,X2,A))) + :- ast_operation(replace(A,B)), head_aggregate_elements(X0,X1,X2,A). + +ast_operation(add(head_aggregate(X0,B,X2,X3,X4));delete(head_aggregate(X0,A,X2,X3,X4))) + :- ast_operation(replace(A,B)), head_aggregate(X0,A,X2,X3,X4). + +ast_operation(add(head_aggregate(X0,X1,X2,B,X4));delete(head_aggregate(X0,X1,X2,A,X4))) + :- ast_operation(replace(A,B)), head_aggregate(X0,X1,X2,A,X4). + +ast_operation(add(head_aggregate(X0,X1,X2,X3,B));delete(head_aggregate(X0,X1,X2,X3,A))) + :- ast_operation(replace(A,B)), head_aggregate(X0,X1,X2,X3,A). + +ast_operation(add(conditional_literals(X0,X1,B));delete(conditional_literals(X0,X1,A))) + :- ast_operation(replace(A,B)), conditional_literals(X0,X1,A). + +ast_operation(add(disjunction(X0,B));delete(disjunction(X0,A))) + :- ast_operation(replace(A,B)), disjunction(X0,A). + +ast_operation(add(rule(X0,B,X2));delete(rule(X0,A,X2))) + :- ast_operation(replace(A,B)), rule(X0,A,X2). + +ast_operation(add(rule(X0,X1,B));delete(rule(X0,X1,A))) + :- ast_operation(replace(A,B)), rule(X0,X1,A). + +ast_operation(add(definition(X0,X1,B,X3));delete(definition(X0,X1,A,X3))) + :- ast_operation(replace(A,B)), definition(X0,X1,A,X3). + +ast_operation(add(show_term(X0,B,X2));delete(show_term(X0,A,X2))) + :- ast_operation(replace(A,B)), show_term(X0,A,X2). + +ast_operation(add(show_term(X0,X1,B));delete(show_term(X0,X1,A))) + :- ast_operation(replace(A,B)), show_term(X0,X1,A). + +ast_operation(add(minimize(X0,B,X2,X3,X4));delete(minimize(X0,A,X2,X3,X4))) + :- ast_operation(replace(A,B)), minimize(X0,A,X2,X3,X4). + +ast_operation(add(minimize(X0,X1,B,X3,X4));delete(minimize(X0,X1,A,X3,X4))) + :- ast_operation(replace(A,B)), minimize(X0,X1,A,X3,X4). + +ast_operation(add(minimize(X0,X1,X2,B,X4));delete(minimize(X0,X1,X2,A,X4))) + :- ast_operation(replace(A,B)), minimize(X0,X1,X2,A,X4). + +ast_operation(add(minimize(X0,X1,X2,X3,B));delete(minimize(X0,X1,X2,X3,A))) + :- ast_operation(replace(A,B)), minimize(X0,X1,X2,X3,A). + +ast_operation(add(statements(X0,X1,B));delete(statements(X0,X1,A))) + :- ast_operation(replace(A,B)), statements(X0,X1,A). + +ast_operation(add(constants(X0,X1,B));delete(constants(X0,X1,A))) + :- ast_operation(replace(A,B)), constants(X0,X1,A). + +ast_operation(add(program(X0,X1,B,X3));delete(program(X0,X1,A,X3))) + :- ast_operation(replace(A,B)), program(X0,X1,A,X3). + +ast_operation(add(program(X0,X1,X2,B));delete(program(X0,X1,X2,A))) + :- ast_operation(replace(A,B)), program(X0,X1,X2,A). + +ast_operation(add(external(X0,B,X2,X3));delete(external(X0,A,X2,X3))) + :- ast_operation(replace(A,B)), external(X0,A,X2,X3). + +ast_operation(add(external(X0,X1,B,X3));delete(external(X0,X1,A,X3))) + :- ast_operation(replace(A,B)), external(X0,X1,A,X3). + +ast_operation(add(edge(X0,B,X2,X3));delete(edge(X0,A,X2,X3))) + :- ast_operation(replace(A,B)), edge(X0,A,X2,X3). + +ast_operation(add(edge(X0,X1,B,X3));delete(edge(X0,X1,A,X3))) + :- ast_operation(replace(A,B)), edge(X0,X1,A,X3). + +ast_operation(add(edge(X0,X1,X2,B));delete(edge(X0,X1,X2,A))) + :- ast_operation(replace(A,B)), edge(X0,X1,X2,A). + +ast_operation(add(heuristic(X0,B,X2,X3,X4,X5));delete(heuristic(X0,A,X2,X3,X4,X5))) + :- ast_operation(replace(A,B)), heuristic(X0,A,X2,X3,X4,X5). + +ast_operation(add(heuristic(X0,X1,B,X3,X4,X5));delete(heuristic(X0,X1,A,X3,X4,X5))) + :- ast_operation(replace(A,B)), heuristic(X0,X1,A,X3,X4,X5). + +ast_operation(add(heuristic(X0,X1,X2,B,X4,X5));delete(heuristic(X0,X1,X2,A,X4,X5))) + :- ast_operation(replace(A,B)), heuristic(X0,X1,X2,A,X4,X5). + +ast_operation(add(heuristic(X0,X1,X2,X3,B,X5));delete(heuristic(X0,X1,X2,X3,A,X5))) + :- ast_operation(replace(A,B)), heuristic(X0,X1,X2,X3,A,X5). + +ast_operation(add(heuristic(X0,X1,X2,X3,X4,B));delete(heuristic(X0,X1,X2,X3,X4,A))) + :- ast_operation(replace(A,B)), heuristic(X0,X1,X2,X3,X4,A). + +ast_operation(add(project_atom(X0,B,X2));delete(project_atom(X0,A,X2))) + :- ast_operation(replace(A,B)), project_atom(X0,A,X2). + +ast_operation(add(project_atom(X0,X1,B));delete(project_atom(X0,X1,A))) + :- ast_operation(replace(A,B)), project_atom(X0,X1,A). + +ast_operation(add(theory_term_definitions(X0,X1,X2,B));delete(theory_term_definitions(X0,X1,X2,A))) + :- ast_operation(replace(A,B)), theory_term_definitions(X0,X1,X2,A). + +ast_operation(add(theory_guard_definition(X0,B,X2));delete(theory_guard_definition(X0,A,X2))) + :- ast_operation(replace(A,B)), theory_guard_definition(X0,A,X2). + +ast_operation(add(theory_atom_definitions(X0,X1,X2,X3,X4,X5,B));delete(theory_atom_definitions(X0,X1,X2,X3,X4,X5,A))) + :- ast_operation(replace(A,B)), theory_atom_definitions(X0,X1,X2,X3,X4,X5,A). + +ast_operation(add(theory_definition(X0,X1,B,X3));delete(theory_definition(X0,X1,A,X3))) + :- ast_operation(replace(A,B)), theory_definition(X0,X1,A,X3). + +ast_operation(add(theory_definition(X0,X1,X2,B));delete(theory_definition(X0,X1,X2,A))) + :- ast_operation(replace(A,B)), theory_definition(X0,X1,X2,A). + diff --git a/src/renopro/utils/codegen.py b/src/renopro/utils/codegen.py new file mode 100644 index 0000000..76afbc1 --- /dev/null +++ b/src/renopro/utils/codegen.py @@ -0,0 +1,116 @@ +# nocoverage +from pathlib import Path + +import renopro.predicates as preds + + +def generate_replace(): + "Generate replacement rules from predicates." + program = ( + "% replace(A,B) replaces a child predicate identifier A\n" + "% with child predicate identifier B in each AST fact where A\n" + "% occurs as a term.\n\n" + ) + for predicate in preds.AstPreds: + if predicate is preds.Location: + continue + replacements = [] + name = predicate.meta.name + arity = predicate.meta.arity + for idx, key in enumerate(predicate.meta.keys()): + if key == "id": + continue + field = getattr(predicate, key).meta.field + # we only care about replacing and combined + # fields - these are the terms that identify a child + # predicate + if field.complex is not None or hasattr(field, "fields"): + replacements.append(idx) + for idx in replacements: + old_args = ",".join( + ["X" + str(i) if i != idx else "A" for i in range(arity)] + ) + new_args = ",".join( + ["X" + str(i) if i != idx else "B" for i in range(arity)] + ) + program += ( + f"ast_operation(add({name}({new_args}));" + f"delete({name}({old_args})))\n :- " + f"ast_operation(replace(A,B)), {name}({old_args}).\n\n" + ) + Path("src", "renopro", "asp", "replace.lp").write_text(program) + + +def generate_ast(): + "Generate rules to tag AST facts." + program = "% Rules to tag AST facts.\n\n" + for predicate in preds.AstPreds: + name = predicate.meta.name + arity = predicate.meta.arity + args = ",".join(["X" + str(i) for i in range(arity)]) + fact = f"{name}({args})" + rule = f"ast({fact}) :- {fact}.\n" + program += rule + Path("src", "renopro", "asp", "ast.lp").write_text(program) + + +def generate_defined(): + "Generate defined statements for AST facts." + program = "% Defined statements for AST facts.\n\n" + for predicate in preds.AstPreds: + name = predicate.meta.name + arity = predicate.meta.arity + statement = f"#defined {name}/{arity}.\n" + program += statement + Path("src", "renopro", "asp", "defined.lp").write_text(program) + + +def generate_child(): + "Generate rules to define child relation among AST identifiers." + program = ( + "% child(X,Y) holds if the ast fact with identifier X has a child fact\n" + '% with identifier Y. Note that identifiers X, Y are "typed";\n' + "% that is, they are of the form ast_pred(id).\n\n" + ) + for predicate in preds.AstPreds: + if predicate is preds.Location: + continue + children = [] + name = predicate.meta.name + arity = predicate.meta.arity + for idx, key in enumerate(predicate.meta.keys()): + if key == "id": + continue + field = getattr(predicate, key).meta.field + # we only care about complex terms and combined + # fields - these are the terms that identify a child + # predicate + if field.complex is not None: + child_term = field.complex + child_name = child_term.meta.name + child_arity = child_term.non_unary.meta.arity + children.append((idx, child_name, child_arity)) + if hasattr(field, "fields"): + for f in field.fields: + child_term = f.complex + child_name = child_term.meta.name + child_arity = child_term.non_unary.meta.arity + children.append((idx, child_name, child_arity)) + ",".join(["_" for i in range(arity - 1)]) + for idx, child_name, child_arity in children: + parent_idx2arg = {0: "X", idx: "Y"} + parent_args = [parent_idx2arg.get(i, "_") for i in range(arity)] + parent_pred = f"{name}({','.join(parent_args)})" + child_pred = ( + f"{child_name}(Y,{','.join(['_' for _ in range(child_arity - 1)])})" + ) + child_relation = f"child({name}(X),{child_name}(Y))" + program += f"{child_relation} :- {parent_pred}, {child_pred}.\n\n" + Path("src", "renopro", "asp", "child.lp").write_text(program) + + +if __name__ == "__main__": + generate_replace() + generate_ast() + generate_defined() + generate_child() From f88310c5cd3a65c6107a40fb357490f8a938127f Mon Sep 17 00:00:00 2001 From: Amade Nemes Date: Thu, 16 Nov 2023 22:17:48 +0100 Subject: [PATCH 2/8] Moved back util codes to their respective modules. Separating them out into clorm_utils didn't work due to circular imports, so this seemed like the most straightforward way of fixing it. --- src/renopro/enum_fields.py | 79 +++++++++++- src/renopro/predicates.py | 50 +++++++- src/renopro/rast.py | 101 ++++++++++++++- src/renopro/utils/clorm_utils.py | 206 ------------------------------- 4 files changed, 220 insertions(+), 216 deletions(-) delete mode 100644 src/renopro/utils/clorm_utils.py diff --git a/src/renopro/enum_fields.py b/src/renopro/enum_fields.py index 9589396..c4d1a62 100644 --- a/src/renopro/enum_fields.py +++ b/src/renopro/enum_fields.py @@ -1,9 +1,84 @@ "Definitions of enum fields to be used in AST predicates." import enum +import inspect +from types import new_class +from typing import Type, TypeVar -from clorm import ConstantField, StringField +from clorm import BaseField, ConstantField, StringField -from renopro.utils.clorm_utils import define_enum_field + +def define_enum_field( + parent_field: Type[BaseField], enum_class: Type[enum.Enum], *, name: str = "" +) -> Type[BaseField]: # nocoverage + """Factory function that returns a BaseField sub-class for an + Enum. Essentially the same as the one defined in clorm, but stores + the enum that defines the field under attribute 'enum' for later + use. + + Enums are part of the standard library since Python 3.4. This method + provides an alternative to using refine_field() to provide a restricted set + of allowable values. + + Example: + .. code-block:: python + + class IO(str,Enum): + IN="in" + OUT="out" + + # A field that unifies against ASP constants "in" and "out" + IOField = define_enum_field(ConstantField,IO) + + Positional argument: + + field_class: the field that is being sub-classed + + enum_class: the Enum class + + Optional keyword-only arguments: + + name: name for new class (default: anonymously generated). + + """ + subclass_name = name if name else parent_field.__name__ + "_Restriction" + if not inspect.isclass(parent_field) or not issubclass(parent_field, BaseField): + raise TypeError(f"{parent_field} is not a subclass of BaseField") + + if not inspect.isclass(enum_class) or not issubclass(enum_class, enum.Enum): + raise TypeError(f"{enum_class} is not a subclass of enum.Enum") + + values = set(i.value for i in enum_class) + + def _pytocl(py): + val = py.value + if val not in values: + raise ValueError( + f"'{val}' is not a valid value of enum class '{enum_class.__name__}'" + ) + return val + + def body(ns): + ns.update({"pytocl": _pytocl, "cltopy": enum_class, "enum": enum_class}) + + return new_class(subclass_name, (parent_field,), {}, body) + + +A = TypeVar("A", bound=enum.Enum) +B = TypeVar("B", bound=enum.Enum) + + +def convert_enum(enum_member: A, other_enum: Type[B]) -> B: + """Given an enum_member, convert it to the other_enum member of + the same name. + """ + try: + return other_enum[enum_member.name] + except KeyError as exc: # nocoverage + msg = ( + f"Enum {other_enum} has no corresponding member " + f"with name {enum_member.name}" + ) + raise ValueError(msg) from exc class UnaryOperator(str, enum.Enum): diff --git a/src/renopro/predicates.py b/src/renopro/predicates.py index ea7c326..639cc89 100644 --- a/src/renopro/predicates.py +++ b/src/renopro/predicates.py @@ -26,17 +26,63 @@ TheorySequenceTypeField, UnaryOperatorField, ) -from renopro.utils.clorm_utils import combine_fields id_count = count() +def combine_fields( + fields: Sequence[Type[BaseField]], *, name: str = "" +) -> Type[BaseField]: + """Factory function that returns a field sub-class that combines + other fields lazily. + + Essentially the same as the combine_fields defined in the clorm + package, but exposes a 'fields' attrible, allowing us to add + additional fields after the initial combination of fields by + appending to the 'fields' attribute of the combined field. + + """ + subclass_name = name if name else "AnonymousCombinedBaseField" + + # Must combine at least two fields otherwise it doesn't make sense + for f in fields: + if not inspect.isclass(f) or not issubclass(f, BaseField): + raise TypeError("{f} is not BaseField or a sub-class.") + + fields = list(fields) + + def _pytocl(value): + for f in fields: + try: + return f.pytocl(value) + except (TypeError, ValueError, AttributeError): + pass + raise TypeError(f"No combined pytocl() match for value {value}.") + + def _cltopy(symbol): + for f in fields: + try: + return f.cltopy(symbol) + except (TypeError, ValueError): + pass + raise TypeError( + ( + f"Object '{symbol}' ({type(symbol)}) failed to unify " + f"with {subclass_name}." + ) + ) + + def body(ns): + ns.update({"fields": fields, "pytocl": _pytocl, "cltopy": _cltopy}) + + return new_class(subclass_name, (BaseField,), {}, body) + + # by default we use integer identifiers, but allow arbitrary symbols as well # for flexibility when these are user generated IdentifierField = combine_fields([IntegerField, RawField], name="IdentifierField") IdentifierField = IdentifierField(default=lambda: next(id_count)) # type: ignore - # Metaclass shenanigans to dynamically create unary versions of AST predicates, # which are used to identify child AST facts diff --git a/src/renopro/rast.py b/src/renopro/rast.py index 8231fcd..3a06901 100644 --- a/src/renopro/rast.py +++ b/src/renopro/rast.py @@ -27,34 +27,123 @@ parse_files, parse_string, ) +from clingo.script import enable_python from clingo.symbol import Symbol, SymbolType from clorm import ( BaseField, FactBase, Unifier, + UnifierNoMatchError, control_add_facts, parse_fact_files, parse_fact_string, ) +from thefuzz import process # type: ignore import renopro.enum_fields as enums import renopro.predicates as preds +from renopro.enum_fields import convert_enum from renopro.utils import assert_never -from renopro.utils.clorm_utils import ( - ChildQueryError, - ChildrenQueryError, - TryUnify, - convert_enum, -) from renopro.utils.logger import get_clingo_logger_callback logger = logging.getLogger(__name__) +enable_python() + + +class ChildQueryError(Exception): + """Exception raised when a required child fact of an AST fact + cannot be found. + + """ + + +class ChildrenQueryError(Exception): + """Exception raised when the expected number child facts of an AST + fact cannot be found. + + """ + + +class TransformationError(Exception): + """Exception raised when a transformation meta-encoding derives an + error or is unsatisfiable.""" + + +class TryUnify(AbstractContextManager): + """Context manager to try some operation that requires unification + of some set of ast facts. Enhance error message if unification fails. + """ + + def __exit__(self, exc_type, exc_value, traceback): + if exc_type is UnifierNoMatchError: + self.handle_unify_error(exc_value) + + @staticmethod + def handle_unify_error(error): + """Enhance UnifierNoMatchError with some more + useful error messages to help debug the reason unification failed. + + """ + unmatched = error.symbol + name2arity2pred = { + pred.meta.name: {pred.meta.arity: pred} for pred in preds.AstPreds + } + candidate = name2arity2pred.get(unmatched.name, {}).get( + len(unmatched.arguments) + ) + if candidate is None: + fuzzy_name = process.extractOne(unmatched.name, name2arity2pred.keys())[0] + signatures = [ + f"{fuzzy_name}/{arity}." for arity in name2arity2pred[fuzzy_name] + ] + msg = f"""No AST fact of matching signature found for symbol + '{unmatched}'. + Similar AST fact signatures are: + """ + "\n".join( + signatures + ) + raise UnifierNoMatchError( + inspect.cleandoc(msg), unmatched, error.predicates + ) from None + for idx, arg in enumerate(unmatched.arguments): + # This is very hacky. Should ask Dave for a better + # solution, if there is one. + arg_field = candidate[idx]._field # pylint: disable=protected-access + arg_field_str = re.sub(r"\(.*?\)", "", str(arg_field)) + try: + arg_field.cltopy(arg) + except (TypeError, ValueError): + msg = f"""Cannot unify symbol + '{unmatched}' + to only candidate AST fact of matching signature + {candidate.meta.name}/{candidate.meta.arity} + due to failure to unify symbol's argument + '{arg}' + against the corresponding field + '{arg_field_str}'.""" + raise UnifierNoMatchError( + inspect.cleandoc(msg), unmatched, (candidate,) + ) from None + raise RuntimeError("Code should be unreachable") # nocoverage + + DUMMY_LOC = Location(Position("", 1, 1), Position("", 1, 1)) NodeConstructor = Callable[..., Union[AST, Symbol]] NodeAttr = Union[AST, Symbol, Sequence[Symbol], ASTSequence, str, int, StrSequence] +log_lvl_str2int = {"debug": 10, "info": 20, "warning": 30, "error": 40} + + +def location_symb2str(location: Symbol) -> str: + pairs = [] + for pair in zip(location.arguments[1].arguments, location.arguments[2].arguments): + pairs.append( + str(pair[0]) if pair[0] == pair[1] else str(pair[0]) + "-" + str(pair[1]) + ) + return ":".join(pairs) + class ReifiedAST: """Class for converting between reified and non-reified diff --git a/src/renopro/utils/clorm_utils.py b/src/renopro/utils/clorm_utils.py deleted file mode 100644 index 42cbe08..0000000 --- a/src/renopro/utils/clorm_utils.py +++ /dev/null @@ -1,206 +0,0 @@ -"Clorm related utility functions." -import enum -import inspect -import re -from contextlib import AbstractContextManager -from types import new_class -from typing import Sequence, Type, TypeVar - -from clorm import BaseField, UnifierNoMatchError -from thefuzz import process # type: ignore - -from renopro import predicates as preds - - -def combine_fields( - fields: Sequence[Type[BaseField]], *, name: str = "" -) -> Type[BaseField]: - """Factory function that returns a field sub-class that combines - other fields lazily. - - Essentially the same as the combine_fields defined in the clorm - package, but exposes a 'fields' attrible, allowing us to add - additional fields after the initial combination of fields by - appending to the 'fields' attribute of the combined field. - - """ - subclass_name = name if name else "AnonymousCombinedBaseField" - - # Must combine at least two fields otherwise it doesn't make sense - for f in fields: - if not inspect.isclass(f) or not issubclass(f, BaseField): - raise TypeError("{f} is not BaseField or a sub-class.") - - fields = list(fields) - - def _pytocl(value): - for f in fields: - try: - return f.pytocl(value) - except (TypeError, ValueError, AttributeError): - pass - raise TypeError(f"No combined pytocl() match for value {value}.") - - def _cltopy(symbol): - for f in fields: - try: - return f.cltopy(symbol) - except (TypeError, ValueError): - pass - raise TypeError( - ( - f"Object '{symbol}' ({type(symbol)}) failed to unify " - f"with {subclass_name}." - ) - ) - - def body(ns): - ns.update({"fields": fields, "pytocl": _pytocl, "cltopy": _cltopy}) - - return new_class(subclass_name, (BaseField,), {}, body) - - -def define_enum_field( - parent_field: Type[BaseField], enum_class: Type[enum.Enum], *, name: str = "" -) -> Type[BaseField]: # nocoverage - """Factory function that returns a BaseField sub-class for an - Enum. Essentially the same as the one defined in clorm, but stores - the enum that defines the field under attribute 'enum' for later - use. - - Enums are part of the standard library since Python 3.4. This method - provides an alternative to using refine_field() to provide a restricted set - of allowable values. - - Example: - .. code-block:: python - - class IO(str,Enum): - IN="in" - OUT="out" - - # A field that unifies against ASP constants "in" and "out" - IOField = define_enum_field(ConstantField,IO) - - Positional argument: - - field_class: the field that is being sub-classed - - enum_class: the Enum class - - Optional keyword-only arguments: - - name: name for new class (default: anonymously generated). - - """ - subclass_name = name if name else parent_field.__name__ + "_Restriction" - if not inspect.isclass(parent_field) or not issubclass(parent_field, BaseField): - raise TypeError(f"{parent_field} is not a subclass of BaseField") - - if not inspect.isclass(enum_class) or not issubclass(enum_class, enum.Enum): - raise TypeError(f"{enum_class} is not a subclass of enum.Enum") - - values = set(i.value for i in enum_class) - - def _pytocl(py): - val = py.value - if val not in values: - raise ValueError( - f"'{val}' is not a valid value of enum class '{enum_class.__name__}'" - ) - return val - - def body(ns): - ns.update({"pytocl": _pytocl, "cltopy": enum_class, "enum": enum_class}) - - return new_class(subclass_name, (parent_field,), {}, body) - - -A = TypeVar("A", bound=enum.Enum) -B = TypeVar("B", bound=enum.Enum) - - -def convert_enum(enum_member: A, other_enum: Type[B]) -> B: - """Given an enum_member, convert it to the other_enum member of - the same name. - """ - try: - return other_enum[enum_member.name] - except KeyError as exc: # nocoverage - msg = ( - f"Enum {other_enum} has no corresponding member " - f"with name {enum_member.name}" - ) - raise ValueError(msg) from exc - - -class ChildQueryError(Exception): - """Exception raised when a required child fact of an AST fact - cannot be found. - - """ - - -class ChildrenQueryError(Exception): - """Exception raised when the expected number child facts of an AST - fact cannot be found. - - """ - - -class TryUnify(AbstractContextManager): - """Context manager to try some operation that requires unification - of some set of ast facts. Enhance error message if unification fails. - """ - - def __exit__(self, exc_type, exc_value, traceback): - if exc_type is UnifierNoMatchError: - self.handle_unify_error(exc_value) - - @staticmethod - def handle_unify_error(error): - """Enhance UnifierNoMatchError with some more - useful error messages to help debug the reason unification failed. - - """ - unmatched = error.symbol - name2arity2pred = { - pred.meta.name: {pred.meta.arity: pred} for pred in preds.AstPreds - } - candidate = name2arity2pred.get(unmatched.name, {}).get( - len(unmatched.arguments) - ) - if candidate is None: - fuzzy_name = process.extractOne(unmatched.name, name2arity2pred.keys())[0] - signatures = [ - f"{fuzzy_name}/{arity}." for arity in name2arity2pred[fuzzy_name] - ] - msg = f"""No AST fact of matching signature found for symbol - '{unmatched}'. - Similar AST fact signatures are: - """ + "\n".join( - signatures - ) - raise UnifierNoMatchError( - inspect.cleandoc(msg), unmatched, error.predicates - ) from None - for idx, arg in enumerate(unmatched.arguments): - # This is very hacky. Should ask Dave for a better - # solution, if there is one. - arg_field = candidate[idx]._field # pylint: disable=protected-access - arg_field_str = re.sub(r"\(.*?\)", "", str(arg_field)) - try: - arg_field.cltopy(arg) - except (TypeError, ValueError): - msg = f"""Cannot unify symbol - '{unmatched}' - to only candidate AST fact of matching signature - {candidate.meta.name}/{candidate.meta.arity} - due to failure to unify symbol's argument - '{arg}' - against the corresponding field - '{arg_field_str}'.""" - raise UnifierNoMatchError( - inspect.cleandoc(msg), unmatched, (candidate,) - ) from None - raise RuntimeError("Code should be unreachable") # nocoverage From 8e0d0e08e6be9c1090b471bc0feb16499e71acfd Mon Sep 17 00:00:00 2001 From: Amade Nemes Date: Thu, 16 Nov 2023 22:30:27 +0100 Subject: [PATCH 3/8] Add logging functionality in transformation meta-encodings. --- src/renopro/predicates.py | 52 +++---- src/renopro/rast.py | 72 ++++++++-- tests/asp/transform/log/error_no_loc.lp | 1 + tests/asp/transform/log/error_with_loc.lp | 1 + tests/asp/transform/log/info.lp | 1 + tests/asp/transform/log/info_no_loc.lp | 1 + tests/asp/transform/log/info_with_loc.lp | 1 + tests/asp/transform/log/input.lp | 7 + tests/test_transform.py | 164 ++++++++++++++++++---- 9 files changed, 236 insertions(+), 64 deletions(-) create mode 100644 tests/asp/transform/log/error_no_loc.lp create mode 100644 tests/asp/transform/log/error_with_loc.lp create mode 100644 tests/asp/transform/log/info.lp create mode 100644 tests/asp/transform/log/info_no_loc.lp create mode 100644 tests/asp/transform/log/info_with_loc.lp create mode 100644 tests/asp/transform/log/input.lp diff --git a/src/renopro/predicates.py b/src/renopro/predicates.py index 639cc89..7b65f2f 100644 --- a/src/renopro/predicates.py +++ b/src/renopro/predicates.py @@ -113,23 +113,6 @@ class AstPredicate(Predicate, metaclass=_AstPredicateMeta): """A predicate representing an AST node.""" -class Position(ComplexTerm): - """Complex field representing a position in a text file.""" - - filename = StringField - line = IntegerField - column = IntegerField - - -class Location(Predicate): - """Predicate linking an AST identifier to the range in a text - file from where it was reified.""" - - id = IdentifierField - begin = Position.Field - end = Position.Field - - class String(AstPredicate): """Predicate representing a string term. @@ -1064,6 +1047,26 @@ class TheoryDefinition(AstPredicate): ) +class Position(ComplexTerm): + """Complex field representing a position in a text file.""" + + filename = StringField + line = IntegerField + column = IntegerField + + +class Location(Predicate): + """Predicate linking an AST identifier to the range in a text + file from where it was reified.""" + + id = IdentifierField + begin = Position.Field + end = Position.Field + + +# Predicates for AST transformation + + AstPred = Union[ Location, String, @@ -1123,10 +1126,10 @@ class TheoryDefinition(AstPredicate): TheoryGuardDefinition, TheoryAtomDefinitions, TheoryDefinition, + Location, ] -AstPreds = [ - Location, +AstPreds = ( String, Number, Variable, @@ -1184,9 +1187,10 @@ class TheoryDefinition(AstPredicate): TheoryGuardDefinition, TheoryAtomDefinitions, TheoryDefinition, -] + Location, +) -SubprogramStatements = [ +SubprogramStatements = ( Rule, Definition, ShowSignature, @@ -1200,9 +1204,9 @@ class TheoryDefinition(AstPredicate): ProjectAtom, ProjectSignature, TheoryDefinition, -] +) -FlattenedTuples = [ +FlattenedTuples = ( TheoryUnparsedTermElements, TheoryAtomElements, BodyAggregateElements, @@ -1210,7 +1214,7 @@ class TheoryDefinition(AstPredicate): TheoryOperatorDefinitions, TheoryTermDefinitions, TheoryAtomDefinitions, -] +) # Predicates for AST transformation diff --git a/src/renopro/rast.py b/src/renopro/rast.py index 3a06901..8913bbf 100644 --- a/src/renopro/rast.py +++ b/src/renopro/rast.py @@ -1,6 +1,9 @@ # pylint: disable=too-many-lines """Module implementing reification and de-reification of non-ground programs""" +import inspect import logging +import re +from contextlib import AbstractContextManager from functools import singledispatchmethod from itertools import count from pathlib import Path @@ -791,30 +794,73 @@ def transform( logger.warning("Reified AST to be transformed is empty.") if meta_str is None and meta_files is None: raise ValueError("No meta-program provided for transformation.") - meta_prog = "" - if meta_str is not None: - meta_prog += meta_str - if meta_files is not None: - for meta_file in meta_files: - with meta_file.open() as f: - meta_prog += f.read() - logger.debug( - "Applying transformation defined in following meta-encoding:\n%s", meta_prog - ) clingo_logger = get_clingo_logger_callback(logger) clingo_options = [] if clingo_options is None else clingo_options ctl = Control(clingo_options, logger=clingo_logger) + if meta_files: + for meta_file in meta_files: + ctl.load(str(meta_file)) logger.debug( "Reified facts before applying transformation:\n%s", self.reified_string ) control_add_facts(ctl, self._reified) - ctl.add(meta_prog) + if meta_str: + ctl.add(meta_str) ctl.load("./src/renopro/asp/transform.lp") ctl.ground() with ctl.solve(yield_=True) as handle: # type: ignore model_iterator = iter(handle) - model = next(model_iterator) - ast_symbols = [final.arguments[0] for final in model.symbols(shown=True)] + try: + model = next(model_iterator) + except StopIteration as e: + raise TransformationError( + "Transformation encoding is unsatisfiable." + ) from e + ast_symbols = [] + logs = {40: [], 30: [], 20: [], 10: []} + logger.debug( + "Stable model obtained via transformation:\n%s", + model.symbols(shown=True), + ) + for symb in model.symbols(shown=True): + if ( + symb.type == SymbolType.Function + and symb.positive is True + and symb.name == "log" + ): + msg = "" + log_lvl_symb = symb.arguments[0] + log_lvl_strings = log_lvl_str2int.keys() + if ( + log_lvl_symb.type != SymbolType.String + or log_lvl_symb.string not in log_lvl_strings + ): + raise TransformationError( + "First argument of log term must be one of the string symbols: '" + + "', '".join(log_lvl_strings) + + "'" + ) + level = log_lvl_str2int[log_lvl_symb.string] + log_strings = [ + location_symb2str(s) + if s.match("location", 3) + else str(s).strip('"') + for s in symb.arguments[1:] + ] + msg += "".join(log_strings) + logs[level].append(msg) + elif symb.match("final", 1): + ast_symbols.append(symb.arguments[0]) + for level, msgs in logs.items(): + for msg in msgs: + if level == 40: + logger.error( + msg, exc_info=logger.getEffectiveLevel() == logging.DEBUG + ) + else: + logger.log(level, msg) + if msgs := logs[40]: + raise TransformationError("\n".join(msgs)) unifier = Unifier(preds.AstPreds) with TryUnify(): ast_facts = unifier.iter_unify(ast_symbols, raise_nomatch=True) diff --git a/tests/asp/transform/log/error_no_loc.lp b/tests/asp/transform/log/error_no_loc.lp new file mode 100644 index 0000000..782a50a --- /dev/null +++ b/tests/asp/transform/log/error_no_loc.lp @@ -0,0 +1 @@ +#show log("error","Found function with name ",a,". Sorry, no location.") : function(F,a,_). diff --git a/tests/asp/transform/log/error_with_loc.lp b/tests/asp/transform/log/error_with_loc.lp new file mode 100644 index 0000000..43e5e8a --- /dev/null +++ b/tests/asp/transform/log/error_with_loc.lp @@ -0,0 +1 @@ +#show log("error",location(F,B,E),": Found function with name ",a,".") : function(F,a,_); location(F,B,E). diff --git a/tests/asp/transform/log/info.lp b/tests/asp/transform/log/info.lp new file mode 100644 index 0000000..20252b1 --- /dev/null +++ b/tests/asp/transform/log/info.lp @@ -0,0 +1 @@ +log("info","This is an 'a' function symbol.",location(F,B,E)) :- function(F,a,_), location(F,B,E). diff --git a/tests/asp/transform/log/info_no_loc.lp b/tests/asp/transform/log/info_no_loc.lp new file mode 100644 index 0000000..4d18912 --- /dev/null +++ b/tests/asp/transform/log/info_no_loc.lp @@ -0,0 +1 @@ +#show log("info","Found function with name ",a,". Sorry, no location.") : function(F,a,_). diff --git a/tests/asp/transform/log/info_with_loc.lp b/tests/asp/transform/log/info_with_loc.lp new file mode 100644 index 0000000..611bd27 --- /dev/null +++ b/tests/asp/transform/log/info_with_loc.lp @@ -0,0 +1 @@ +#show log("info",location(F,B,E),": Found function with name ",a,".") : function(F,a,_); location(F,B,E). diff --git a/tests/asp/transform/log/input.lp b/tests/asp/transform/log/input.lp new file mode 100644 index 0000000..43961a8 --- /dev/null +++ b/tests/asp/transform/log/input.lp @@ -0,0 +1,7 @@ +program(0,"base",constants(1),statements(2)). +statements(2,0,rule(3)). +rule(3,literal(4),body_literals(8)). +% facts representing head literal a. +literal(4,"pos",symbolic_atom(5)). +symbolic_atom(5,function(6)). +function(6,a,terms(7)). diff --git a/tests/test_transform.py b/tests/test_transform.py index 7ff8f5c..5f5e3db 100644 --- a/tests/test_transform.py +++ b/tests/test_transform.py @@ -1,8 +1,14 @@ """Test cases for transformation of AST using a meta-encoding.""" +import re +from itertools import count from pathlib import Path +from typing import Dict, List, Literal from unittest import TestCase -from renopro.rast import ReifiedAST +from clingo import Control + +import renopro.predicates as preds +from renopro.rast import ReifiedAST, TransformationError tests_dir = Path("tests", "asp") test_transform_dir = tests_dir / "transform" @@ -11,45 +17,149 @@ class TestTransform(TestCase): """Tests for AST transformations defined via a meta-encodings.""" + def setUp(self): + # reset id generator between test cases so reification + # auto-generates the expected integers + preds.id_count = count() + + def assertTrasformEqual( + self, + input_files: List[Path], + meta_files: List[Path], + expected_output_file: Path, + reify_location=True, + ): + rast = ReifiedAST(reify_location=reify_location) + rast.reify_files(input_files) + rast.transform(meta_files=meta_files) + rast.reflect() + transformed_str = rast.program_string.strip() + with expected_output_file.open("r") as f: + expected_str = self.base_str + f.read().strip() + self.assertEqual(transformed_str, expected_str) + + def assertTransformLogs( + self, + input_files: List[Path], + meta_files: List[Path], + level: Literal["DEBUG", "INFO", "WARNING", "ERROR"], + message2num_matches: Dict[str, int], + reify_location=True, + ): + rast = ReifiedAST(reify_location=reify_location) + rast.reify_files(input_files) + with self.assertLogs("renopro.rast", level=level) as cm: + try: + rast.transform(meta_files=meta_files) + except TransformationError as e: + if level != "ERROR": + raise e + for message, expected_num in message2num_matches.items(): + assert_exc_msg = ( + f"Expected {expected_num} " + "matches for exception message " + f"'{message}', found " + ) + num_exception_matches = len(re.findall(message, str(e))) + self.assertEqual( + num_exception_matches, + expected_num, + msg=assert_exc_msg + str(num_exception_matches), + ) + logs = "\n".join(cm.output) + for message, expected_num in message2num_matches.items(): + assert_msg = ( + f"Expected {expected_num} " + "matches for log message " + f"'{message}', found " + ) + reo = re.compile(message) + num_log_matches = len(reo.findall(logs)) + self.assertEqual( + num_log_matches, expected_num, msg=assert_msg + str(num_log_matches) + ) + base_str = "#program base.\n" + +class TestTransformSimple(TestTransform): + """Test case for testing basic transform functionality and simple + transformations""" + + def test_transform_unsat(self): + "Test that unsatisfiable transformation meta-encoding raises error." + rast = ReifiedAST() + pattern = r"Transformation encoding is unsatisfiable." + with self.assertRaisesRegex(TransformationError, pattern): + rast.transform(meta_str="#false.") + + def test_transform_log(self): + "Test logging capabilities of transform." + files_dir = test_transform_dir / "log" + rast = ReifiedAST() + pattern = ( + r"First argument of log term must be one of the string " + r"symbols: 'debug', 'info', 'warning', 'error'" + ) + with self.assertRaisesRegex(TransformationError, pattern): + rast.transform(meta_str="#show log('hello', 'world') : #true.") + self.assertTransformLogs( + [files_dir / "input.lp"], + [files_dir / "info_with_loc.lp"], + "INFO", + {r"7:12-13: Found function with name a.": 1}, + ) + self.assertTransformLogs( + [files_dir / "input.lp"], + [files_dir / "info_no_loc.lp"], + "INFO", + {r"Found function with name a. Sorry, no location.": 1}, + ) + self.assertTransformLogs( + [files_dir / "input.lp"], + [files_dir / "error_no_loc.lp"], + "ERROR", + {r"Found function with name a. Sorry, no location.": 1}, + ) + self.assertTransformLogs( + [files_dir / "input.lp"], + [files_dir / "error_with_loc.lp"], + "ERROR", + {r"7:12-13: Found function with name a.": 1}, + ) + + def test_transform_bad_input(self): + """Test transform behavior under bad input.""" + rast = ReifiedAST() + # should log warning if rast has no facts before transformation + with self.assertLogs("renopro.rast", level="WARNING"): + rast.transform(meta_str="") + # should raise error if no meta program is provided + with self.assertRaises(ValueError): + rast.transform() + def test_transform_not_bad(self): """Test adding an additional literal to the body of rules. Desired outcome: for something to be good, we want to require that it's not bad. """ - rast = ReifiedAST() files_dir = test_transform_dir / "not_bad" - rast.reify_files([files_dir / "input.lp"]) - rast.transform(meta_files=[files_dir / "transform.lp"]) - rast.reflect() - transformed_str = rast.program_string.strip() - with (files_dir / "output.lp").open("r") as output: - expected_str = self.base_str + output.read().strip() - self.assertEqual(transformed_str, expected_str) + self.assertTrasformEqual( + [files_dir / "input.lp"], + [files_dir / "transform.lp"], + files_dir / "output.lp", + ) def test_transform_add_time(self): """Test transforming a temporal logic program with the previous operator into a program with explicit time points.""" + files_dir = test_transform_dir / "prev_to_timepoints" for testname in ["sad", "very_sad", "constant"]: with self.subTest(testname=testname): - rast = ReifiedAST() - files_dir = test_transform_dir / "prev_to_timepoints" - rast.reify_files([files_dir / (testname + "_input.lp")]) - rast.transform(meta_files=[files_dir / "transform.lp"]) - rast.reflect() - transformed_str = rast.program_string.strip() - with (files_dir / (testname + "_output.lp")).open("r") as output: - expected_str = self.base_str + output.read().strip() - self.assertEqual(transformed_str, expected_str) + self.assertTrasformEqual( + [files_dir / (testname + "_input.lp")], + [files_dir / "transform.lp"], + files_dir / (testname + "_output.lp"), + ) - def test_transform_bad_input(self): - """Test transform behavior under bad input.""" - rast = ReifiedAST() - # should log warning if rast has no facts before transformation - with self.assertLogs("renopro.rast", level="WARNING"): - rast.transform(meta_str="") - # should raise error if no meta program is provided - with self.assertRaises(ValueError): - rast.transform() From 6014606ad6b89ea83a1064501646b44b5410be1c Mon Sep 17 00:00:00 2001 From: Amade Nemes Date: Thu, 16 Nov 2023 22:42:09 +0100 Subject: [PATCH 4/8] Add command line option to make reification of locations optional. --- src/renopro/__main__.py | 4 ++- src/renopro/utils/parser.py | 12 +++++++ .../transform/not_bad/transform-decompose.lp | 31 +++++++++++++++++++ 3 files changed, 46 insertions(+), 1 deletion(-) create mode 100644 tests/asp/transform/not_bad/transform-decompose.lp diff --git a/src/renopro/__main__.py b/src/renopro/__main__.py index 04e8d38..8e99f4e 100644 --- a/src/renopro/__main__.py +++ b/src/renopro/__main__.py @@ -14,8 +14,8 @@ def main(): parser = get_parser() args = parser.parse_args() setup_logger("renopro", args.log) - rast = ReifiedAST() if args.command == "reify": + rast = ReifiedAST(reify_location=args.reify_location) rast.reify_files(args.infiles) if args.commented: print(rast.reified_string_doc) @@ -23,11 +23,13 @@ def main(): print(rast.reified_string) elif args.command == "reflect": + rast = ReifiedAST() rast.add_reified_files(args.infiles) rast.reflect() print(rast.program_string) elif args.command == "transform": + rast = ReifiedAST(reify_location=args.reify_location) if args.input_format == "reified": rast.add_reified_files(args.infiles) elif args.input_format == "reflected": diff --git a/src/renopro/utils/parser.py b/src/renopro/utils/parser.py index ccfc508..f777204 100644 --- a/src/renopro/utils/parser.py +++ b/src/renopro/utils/parser.py @@ -72,6 +72,12 @@ def get(levels, name): reify_parser = subparsers.add_parser( "reify", help="Reify input program into ASP facts.", parents=[common_arg_parser] ) + reify_parser.add_argument( + "--reify-location", + "-L", + action="store_true", + help="Enable reification of AST node locations.", + ) reify_parser.add_argument( "--commented", "-c", @@ -123,6 +129,12 @@ def get(levels, name): choices=["reified", "reflected"], default="reflected", ) + transform_parser.add_argument( + "--reify-location", + "-L", + action="store_true", + help="Enable reification of AST node locations.", + ) transform_parser.add_argument( "--clingo-options", "-C", diff --git a/tests/asp/transform/not_bad/transform-decompose.lp b/tests/asp/transform/not_bad/transform-decompose.lp new file mode 100644 index 0000000..1306eba --- /dev/null +++ b/tests/asp/transform/not_bad/transform-decompose.lp @@ -0,0 +1,31 @@ +% ast transformation: + +% transforms every rule with single symbolic head +% literal with name "good", adding a negated symbolic literal to the +% body with name "bad", and same arguments as the head literal + +% examples: +% good(X) :- person(X). +% -> +% good(X) :- person(X), not bad(X). +% +% good(dog(X,"spotty")) :- cute(dog(X,"spotty")). +% -> +% good(dog(X,"spotty")) :- cute(dog(X,"spotty")), not bad(dog(X,"spotty")). + +% auxiliary predicate to get maximal index within a tuple of rule body literals +max_lit_index(LT,Idx) +:- Idx = #max{ P : body_literals(LT,P,_); -1 }, rule(_,_,body_literals(LT)). + +ast_operation(add( + @decompose( + body_literals_( + LT,N+1,body_literal_( + "not",symbolic_atom_( + function_(bad,Fargs))))) +)) +:- rule(_,literal(L),body_literals(LT)), + literal(L,"pos",symbolic_atom(A)), + symbolic_atom(A,function(F)), + function(F,good,Fargs), + max_lit_index(LT,N). From 121a7c4ea1915b56062695eb5c0da71f40e1b350 Mon Sep 17 00:00:00 2001 From: Amade Nemes Date: Thu, 16 Nov 2023 22:44:46 +0100 Subject: [PATCH 5/8] Fix defined statements. --- src/renopro/asp/defined.lp | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) diff --git a/src/renopro/asp/defined.lp b/src/renopro/asp/defined.lp index 39d5845..a8394b9 100644 --- a/src/renopro/asp/defined.lp +++ b/src/renopro/asp/defined.lp @@ -1,3 +1,5 @@ +% Defined statements for AST facts. + #defined string/2. #defined number/2. #defined variable/2. @@ -6,6 +8,7 @@ #defined interval/3. #defined terms/3. #defined function/3. +#defined external_function/3. #defined pool/2. #defined theory_terms/3. #defined theory_sequence/3. @@ -15,7 +18,7 @@ #defined theory_unparsed_term/2. #defined guard/3. #defined guards/3. -#defined comparison/2. +#defined comparison/3. #defined boolean_constant/2. #defined symbolic_atom/2. #defined literal/3. @@ -27,29 +30,31 @@ #defined theory_guard/3. #defined theory_atom/4. #defined body_aggregate_elements/4. -#defined body_aggregate/4. +#defined body_aggregate/5. #defined body_literal/3. #defined body_literals/3. #defined head_aggregate_elements/4. -#defined head_aggregate/4. +#defined head_aggregate/5. #defined conditional_literals/3. -#defined disjunction/3. +#defined disjunction/2. #defined rule/3. #defined definition/4. #defined show_signature/4. #defined defined/4. +#defined show_term/3. #defined minimize/5. #defined script/3. #defined statements/3. #defined constants/3. #defined program/4. -#defined external/3. +#defined external/4. #defined edge/4. #defined heuristic/6. #defined project_atom/3. #defined project_signature/4. #defined theory_operator_definitions/5. -#defined theory_term_definitions/5. +#defined theory_term_definitions/4. #defined theory_guard_definition/3. #defined theory_atom_definitions/7. #defined theory_definition/4. +#defined location/3. From fc303a25682433ed5d9ab649acd3e67ee0e69af4 Mon Sep 17 00:00:00 2001 From: Amade Nemes Date: Thu, 16 Nov 2023 22:50:15 +0100 Subject: [PATCH 6/8] WIP theory parsing. --- pyproject.toml | 2 +- src/renopro/asp/transform.lp | 39 ++++- src/renopro/predicates.py | 8 +- src/renopro/rast.py | 6 +- tests/asp/transform/not_bad/transform.lp | 2 +- .../theory-parsing/clingo-operator-table.lp | 22 +++ .../determine_theory_term_types.lp | 67 ++++++++ .../inputs/clingo-theory-term-reified.lp | 14 ++ .../clingo-theory-term-unknown-reified.lp | 22 +++ .../inputs/clingo-unknown-operator.lp | 1 + .../inputs/clingo-unparsed-theory-term.lp | 2 + .../diff-constraint-theory-def-reified.lp | 27 ++++ .../outputs/clingo-unparsed-theory-term.lp | 2 + .../theory-parsing/parse-theory-terms.lp | 27 ++++ .../parse-unparsed-theory-terms.lp | 151 ++++++++++++++++++ .../theory-parsing/tables-from-theory-defs.lp | 15 ++ tests/test_reify_reflect.py | 2 - tests/test_transform.py | 72 +++++++++ 18 files changed, 469 insertions(+), 12 deletions(-) create mode 100644 tests/asp/transform/theory-parsing/clingo-operator-table.lp create mode 100644 tests/asp/transform/theory-parsing/determine_theory_term_types.lp create mode 100644 tests/asp/transform/theory-parsing/inputs/clingo-theory-term-reified.lp create mode 100644 tests/asp/transform/theory-parsing/inputs/clingo-theory-term-unknown-reified.lp create mode 100644 tests/asp/transform/theory-parsing/inputs/clingo-unknown-operator.lp create mode 100644 tests/asp/transform/theory-parsing/inputs/clingo-unparsed-theory-term.lp create mode 100644 tests/asp/transform/theory-parsing/inputs/diff-constraint-theory-def-reified.lp create mode 100644 tests/asp/transform/theory-parsing/outputs/clingo-unparsed-theory-term.lp create mode 100644 tests/asp/transform/theory-parsing/parse-theory-terms.lp create mode 100644 tests/asp/transform/theory-parsing/parse-unparsed-theory-terms.lp create mode 100644 tests/asp/transform/theory-parsing/tables-from-theory-defs.lp diff --git a/pyproject.toml b/pyproject.toml index be946fc..28ad3c1 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -10,4 +10,4 @@ skip_magic_trailing_comma = true line-length = 88 [tool.mypy] -disable_error_code = ["attr-defined"] \ No newline at end of file +disable_error_code = ["attr-defined"] diff --git a/src/renopro/asp/transform.lp b/src/renopro/asp/transform.lp index 02acf23..ef886ac 100644 --- a/src/renopro/asp/transform.lp +++ b/src/renopro/asp/transform.lp @@ -1,8 +1,43 @@ #include "ast.lp". #include "defined.lp". +#include "replace.lp". +#include "child.lp". -final(A) :- ast(A), not ast_operation(delete(A)), not ast_operation(replace(A,_)). -final(R) :- ast_operation(replace(_,R)). +#script (python) + +from clingo.symbol import Function, Number, SymbolType, Symbol, List + +from renopro.predicates import composed_pred_names + + +def _decompose(f: Symbol, top_id: Symbol, asts: List[Symbol], i: int, top_level=False, override_id=None): + current_id = override_id if override_id is not None else i + fresh_id = Function("_fresh", [top_id, Number(current_id)]) + i = i + 1 + ast_args = [fresh_id] if not top_level else [] + for arg in f.arguments: + if arg.type is SymbolType.Function and arg.name in composed_pred_names: + id_term, i = _decompose(arg, top_id, asts, i) + ast_args.append(id_term) + elif arg.type is SymbolType.Function and arg.name == "": + j = i + for element in arg.arguments: + id_term, i = _decompose(element, top_id, asts, i, override_id=j) + ast_args.append(id_term) + else: + ast_args.append(arg) + asts.append(Function(f.name.rstrip("_"), ast_args)) + return Function(f.name.rstrip("_"), [fresh_id]), i + + +def decompose(f: Symbol): + asts = [] + _decompose(f, Function(f.name, f.arguments[:1]), asts, 0, top_level=True) + return asts + + #end. + +final(A) :- ast(A), not ast_operation(delete(A)). final(N) :- ast_operation(add(N)). #defined ast_operation/1. diff --git a/src/renopro/predicates.py b/src/renopro/predicates.py index 7b65f2f..de5ef68 100644 --- a/src/renopro/predicates.py +++ b/src/renopro/predicates.py @@ -1,11 +1,13 @@ # pylint: disable=too-many-lines """Definitions of AST elements as clorm predicates.""" +import inspect import re from itertools import count from types import new_class -from typing import Union +from typing import Sequence, Type, Union from clorm import ( + BaseField, ComplexTerm, ConstantField, IntegerField, @@ -1216,7 +1218,9 @@ class Location(Predicate): TheoryAtomDefinitions, ) -# Predicates for AST transformation +composed_pred_names = tuple(predicate.meta.name + "_" for predicate in AstPreds) + +name2arity2pred = {pred.meta.name: {pred.meta.arity: pred} for pred in AstPreds} class Final(Predicate): diff --git a/src/renopro/rast.py b/src/renopro/rast.py index 8913bbf..bb159b9 100644 --- a/src/renopro/rast.py +++ b/src/renopro/rast.py @@ -473,11 +473,9 @@ def reify_node( # sign is a reserved field name in clorm, so we had use # sign_ instead if key == "sign_": - annotation = annotations["sign"] - attr = getattr(node, "sign") + annotation, attr = annotations["sign"], getattr(node, "sign") else: - annotation = annotations.get(key) - attr = getattr(node, key) + annotation, attr = annotations.get(key), getattr(node, key) field = getattr(predicate, key).meta.field reified_attr = self._reify_attr(annotation, attr, field) kwargs_dict.update({key: reified_attr}) diff --git a/tests/asp/transform/not_bad/transform.lp b/tests/asp/transform/not_bad/transform.lp index 85219b8..97601c7 100644 --- a/tests/asp/transform/not_bad/transform.lp +++ b/tests/asp/transform/not_bad/transform.lp @@ -18,7 +18,7 @@ max_lit_index(LT,Idx) :- Idx = #max{ P : body_literals(LT,P,_); -1 }, rule(_,_,body_literals(LT)). -% the transformation itself +%% the transformation itself ast_operation( add((body_literals(LT,N+1,body_literal(new_id(LT,0))); body_literal(new_id(LT,0),"not",symbolic_atom(new_id(LT,1))); diff --git a/tests/asp/transform/theory-parsing/clingo-operator-table.lp b/tests/asp/transform/theory-parsing/clingo-operator-table.lp new file mode 100644 index 0000000..9c7c7cb --- /dev/null +++ b/tests/asp/transform/theory-parsing/clingo-operator-table.lp @@ -0,0 +1,22 @@ +% operator table for clingo's built-in operators +% in the second argument of the third argument, +% 1 stands for left associative +% and 0 stands for right associative +% or no associativity in unary case. + +operator_table(clingo,("-",1),(5,0)). +operator_table(clingo,("~",1),(5,0)). +operator_table(clingo,("**",2),(4,0)). +operator_table(clingo,("*",2),(3,1)). +operator_table(clingo,("/",2),(3,1)). +operator_table(clingo,("\\",2),(3,1)). +operator_table(clingo,("+",2),(2,1)). +operator_table(clingo,("-",2),(2,1)). +operator_table(clingo,("&",2),(1,1)). +operator_table(clingo,("?",2),(1,1)). +operator_table(clingo,("^",2),(1,1)). +operator_table(clingo,("..",2),(0,1)). + +% interpret all theory terms as clingo terms +theory_term_type(Id,clingo) :- theory_unparsed_term(Id,_). +theory_term_type(TF,clingo) :- theory_function(TF,_,_). diff --git a/tests/asp/transform/theory-parsing/determine_theory_term_types.lp b/tests/asp/transform/theory-parsing/determine_theory_term_types.lp new file mode 100644 index 0000000..f0409c5 --- /dev/null +++ b/tests/asp/transform/theory-parsing/determine_theory_term_types.lp @@ -0,0 +1,67 @@ +func_arity(F,A) :- function(F,_,terms(TS)), A = #count{ P: terms(TS,P,_) }. + +theory_atom_type(A,body) :- body_literals(_,_,theory_atom(A)). + +theory_atom_type(A,head) +:- rule(_,theory_atom(A), body_literals(B)), body_literals(B,_,_). + +theory_atom_type(A,directive) +:- rule(_,theory_atom(A), body_literals(B)), not body_literals(B,_,_). + +#show log("error", location(A,Begin,End), ": No theory atom definition of name '", + AtomName, "' and arity '", Arity, "'.") +: theory_atom(A,function(F),_,_), function(F,AtomName,_), + func_arity(F,Arity), not atom_table((Name,Arity),_,_,_), + location(A,Begin,End). + +#show log("error", location(A,Begin,End), ": Theory atom expected to occur in context '", + AtomType, "', but found in context '", OccuranceType ,"'.") +: theory_atom(A,function(F),_,_), function(F,AtomName,_), + func_arity(F,Arity), atom_table((AtomName,Arity),AtomType,_,_), + theory_atom_type(A,OccuranceType), OccuranceType != AtomType. + +#show log("error") +: + + +% descendant is the transitive closure of child, but only +% defined starting from a theory atom node downward +descendant(theory_atom(X),Y):- child(theory_atom(X),Y). +descendant(X,Z) :- descendant(X,Y), child(Y,Z). + +root(theory_atom_elements(E),ElementTermType) +:- theory_atom(A,function(F),theory_atom_elements(E),_), + function(F,AtomName,_), + func_arity(F,Arity), theory_atom_type(A,AtomType), + atom_table((Name,Arity),AtomType,ElementTermType,_). + +root(theory_guard(E),GuardTermType) +:- theory_atom(A,function(F),_,theory_guard(TG)), + function(F,AtomName,_), + func_arity(F,Arity), theory_atom_type(A,Type), + theory_guard(TG,Opname,_), + atom_table((Name,Arity),Type,_,theory_guard_definition(GD)), + theory_guard_definition(GD,theory_operators(TOS),GuardTermType), + theory_operators(TOS,_,Opname). + +#show log("error","") +: theory_atom(A,function(F),_,theory_guard(TG)), + function(F,AtomName,_), + func_arity(F,Arity), theory_atom_type(A,Type), + theory_guard(TG,Opname,_), + atom_table((Name,Arity),Type,_,theory_guard_definition(GD)), + #false : theory_guard_definition(GD,theory_operators(TOS),GuardTermType), + theory_operators(TOS,_,Opname). + +% assign the theory term type assigned to the root node to it's descendants. + +theory_term_type(TF,Type) +:- root(X,Type), descendant(X,theory_function(TF)). + +theory_term_type(TU,Type) +:- root(X,Type), descendant(X,theory_unparsed_term(TU)). + +% need to write some error handing, in case the atom occurs in a place +% it isn't supposed to, or the theory guard contains an element it's +% not supposed - right now no error message is raised, just no +% transformation occurs diff --git a/tests/asp/transform/theory-parsing/inputs/clingo-theory-term-reified.lp b/tests/asp/transform/theory-parsing/inputs/clingo-theory-term-reified.lp new file mode 100644 index 0000000..2ab90aa --- /dev/null +++ b/tests/asp/transform/theory-parsing/inputs/clingo-theory-term-reified.lp @@ -0,0 +1,14 @@ +program(0,"base",constants(1),statements(2)). +function(5,eval,terms(6)). +number(13,1). +number(14,2). +theory_terms(12,0,number(13)). +theory_terms(10,0,theory_function(11)). +theory_terms(10,1,number(14)). +theory_terms(8,0,theory_function(9)). +theory_function(11,"-",theory_terms(12)). +theory_function(9,"+",theory_terms(10)). +theory_atom_elements(7,0,theory_terms(8),literals(15)). +theory_atom(4,function(5),theory_atom_elements(7),theory_guard(16)). +rule(3,theory_atom(4),body_literals(17)). +statements(2,0,rule(3)). diff --git a/tests/asp/transform/theory-parsing/inputs/clingo-theory-term-unknown-reified.lp b/tests/asp/transform/theory-parsing/inputs/clingo-theory-term-unknown-reified.lp new file mode 100644 index 0000000..e5dca06 --- /dev/null +++ b/tests/asp/transform/theory-parsing/inputs/clingo-theory-term-unknown-reified.lp @@ -0,0 +1,22 @@ +location(0,position("-",1,1),position("-",1,1)). +location(3,position("-",1,1),position("-",1,21)). +location(4,position("-",1,2),position("-",1,6)). +location(5,position("-",1,2),position("-",1,6)). +location(9,position("-",1,9),position("-",1,18)). +location(11,position("-",1,11),position("-",1,15)). +location(13,position("-",1,13),position("-",1,14)). +location(14,position("-",1,16),position("-",1,17)). +program(0,"base",constants(1),statements(2)). +function(5,eval,terms(6)). +number(13,1). +number(14,2). +theory_terms(12,0,number(13)). +theory_terms(10,0,theory_function(11)). +theory_terms(10,1,number(14)). +theory_terms(8,0,theory_function(9)). +theory_function(11,"+",theory_terms(12)). +theory_function(9,"!!",theory_terms(10)). +theory_atom_elements(7,0,theory_terms(8),literals(15)). +theory_atom(4,function(5),theory_atom_elements(7),theory_guard(16)). +rule(3,theory_atom(4),body_literals(17)). +statements(2,0,rule(3)). diff --git a/tests/asp/transform/theory-parsing/inputs/clingo-unknown-operator.lp b/tests/asp/transform/theory-parsing/inputs/clingo-unknown-operator.lp new file mode 100644 index 0000000..a241637 --- /dev/null +++ b/tests/asp/transform/theory-parsing/inputs/clingo-unknown-operator.lp @@ -0,0 +1 @@ +&eval{ * 1 * 2 ~ 3 }. diff --git a/tests/asp/transform/theory-parsing/inputs/clingo-unparsed-theory-term.lp b/tests/asp/transform/theory-parsing/inputs/clingo-unparsed-theory-term.lp new file mode 100644 index 0000000..b531692 --- /dev/null +++ b/tests/asp/transform/theory-parsing/inputs/clingo-unparsed-theory-term.lp @@ -0,0 +1,2 @@ +&eval { (1 / - 2 * 3 ** 4) }. +&eval { (- 1 * 2 + 3) }. diff --git a/tests/asp/transform/theory-parsing/inputs/diff-constraint-theory-def-reified.lp b/tests/asp/transform/theory-parsing/inputs/diff-constraint-theory-def-reified.lp new file mode 100644 index 0000000..b990e77 --- /dev/null +++ b/tests/asp/transform/theory-parsing/inputs/diff-constraint-theory-def-reified.lp @@ -0,0 +1,27 @@ +program(0,"base",constants(1),statements(2)). +statements(2,0,theory_definition(3)). +% #theory dc { +theory_definition(3,dc,theory_term_definitions(4),theory_atom_definitions(9)). +% constant { - : 0 , unary }; +theory_term_definitions(4,0,constant,theory_operator_definitions(5)). +theory_operator_definitions(5,0,"-",0,unary). +% diff_term { - : 0 , binary, left }; +theory_term_definitions(4,1,diff_term,theory_operator_definitions(6)). +theory_operator_definitions(6,0,"-",0,binary_left). +% domain_term { .. : 1 , binary, left }; +theory_term_definitions(4,2,domain_term,theory_operator_definitions(7)). +theory_operator_definitions(7,0,"..",1,binary_left). +% show_term { / : 1 , binary, left }; +theory_term_definitions(4,3,show_term,theory_operator_definitions(8)). +theory_operator_definitions(8,0,"/",1,binary_left). +% &dom/0 : domain_term, {=} , diff_term, any; +theory_atom_definitions(9,0,any,dom,0,domain_term,theory_guard_definition(10)). +theory_guard_definition(10,theory_operators(11),diff_term). +theory_operators(11,0,"="). +% &diff/0 : diff_term, { <=} , constant, any; +theory_atom_definitions(9,1,any,diff,0,diff_term,theory_guard_definition(12)). +theory_guard_definition(12,theory_operators(13),constant). +theory_operators(13,0,"<="). +% &show/0 : show_term, directive +theory_atom_definitions(9,2,directive,show,0,show_term,theory_guard_definition(14)). +% }. diff --git a/tests/asp/transform/theory-parsing/outputs/clingo-unparsed-theory-term.lp b/tests/asp/transform/theory-parsing/outputs/clingo-unparsed-theory-term.lp new file mode 100644 index 0000000..1cf24e0 --- /dev/null +++ b/tests/asp/transform/theory-parsing/outputs/clingo-unparsed-theory-term.lp @@ -0,0 +1,2 @@ +&eval { *(/(1,-(2)),**(3,4)) }. +&eval { +(*(-(1),2),3) }. diff --git a/tests/asp/transform/theory-parsing/parse-theory-terms.lp b/tests/asp/transform/theory-parsing/parse-theory-terms.lp new file mode 100644 index 0000000..93b6f7e --- /dev/null +++ b/tests/asp/transform/theory-parsing/parse-theory-terms.lp @@ -0,0 +1,27 @@ +#script (python) + +from clingo.symbol import String, Number + +def is_operator_name(name: String): + name_str = name.string + return Number(1) if (name_str and name_str[0] in "/!<=>+-*\\?&@|:;~^.") or (name_str == "not") else Number(0) + +#end. + +% parse unparsed theory terms + +#include "parse-unparsed-theory-terms.lp". + +% check that theory functions of arity 1 or 2 that +% represent operations agree with the grammar + +#show log("warning",Id,Name) : theory_function(Id,Name,_), theory_term_type(Id,T). + +undefined_operator(Type,N,Arity,location(TF,Begin,End)) +:- theory_function(TF,N,theory_terms(TT)), + theory_term_type(TF,Type), + Arity = #count{ P: theory_terms(TT,P,T) }, Arity<3, + @is_operator_name(N) = 1, + not operator_table(Type,(N,Arity),_), + location(TF,Begin,End). + diff --git a/tests/asp/transform/theory-parsing/parse-unparsed-theory-terms.lp b/tests/asp/transform/theory-parsing/parse-unparsed-theory-terms.lp new file mode 100644 index 0000000..b49dc37 --- /dev/null +++ b/tests/asp/transform/theory-parsing/parse-unparsed-theory-terms.lp @@ -0,0 +1,151 @@ +% determine implicit arities of theory operators based on their position in the +% unparsed theory term. + +arity(theory_operators(Ops,0,Opname),1) +:- theory_operators(Ops,0,Opname), theory_unparsed_term_elements(_,0,theory_operators(Ops),_). + +arity(theory_operators(Ops,0,Opname),2) +:- theory_operators(Ops,0,Opname), theory_unparsed_term_elements(_,P,theory_operators(Ops),_), P>0. + +arity(theory_operators(Ops,P,Opname),1) +:- theory_operators(Ops,P,Opname), P > 0. + + +% check that the implicit arities of all unparsed theory term operators +% match the arity in the operator table + +#show log("error",Location, + ": No definition for operator '", + Opname,"' of arity '",Arity,"' found for theory ", + "term type '", Type, "'.") +: undefined_operator(Type,Opname,Arity,Location). + +undefined_operator(Type,Opname,Arity,location(Id,Begin,End)) +:- theory_unparsed_term(Id,theory_unparsed_term_elements(Elements)), + theory_term_type(Id,Type), + location(Id,Begin,End), + theory_unparsed_term_elements(Elements,_,theory_operators(Ops),_), + arity(theory_operators(Ops,Pos,Opname),Arity), + not operator_table(Type,(Opname,Arity),_). + +% determine priority and associativity based on operator table + +prio_assoc(theory_operators(Ops,P,Opname),(Prio,Assoc)) +:- theory_unparsed_term(Id,theory_unparsed_term_elements(Elements)), + theory_term_type(Id,Type), + theory_operators(Ops,P,Opname), + theory_unparsed_term_elements(Elements,_,theory_operators(Ops),_), + arity(theory_operators(Ops,P,Opname),Arity), + operator_table(Type,(Opname,Arity),(Prio,Assoc)). + +% build sequence of terms and operators to be processed. +% We will go from back to front as it makes dealing with +% unary operators easier. + +last_operator(theory_operators(O,P',N)) +:- theory_operators(O,_,_), P'=#max{P: theory_operators(O,P,_)}, + theory_operators(O,P',N). + +first_operator(theory_operators(O,P',N)) +:- theory_operators(O,_,_), + T'=#min{P: theory_operators(O,P,_)}, theory_operators(O,P',N). + +_next(TheoryTerm,theory_operators(Ops,OpPos,OpName)) +:- theory_unparsed_term_elements(Elements,P,theory_operators(Ops),TheoryTerm), + last_operator(theory_operators(Ops,OpPos,OpName)). + +_next(theory_operators(Ops,P,Opname1),theory_operators(Ops,P-1,Opname2)) +:- theory_operators(Ops,P,Opname1), theory_operators(Ops,P-1,Opname2). + +_next(theory_operators(O,P,N),TheoryTerm) +:- first_operator(theory_operators(O,P,N)), + theory_unparsed_term_elements(E,EP,theory_operators(O),_), + theory_unparsed_term_elements(E,EP-1,_,TheoryTerm). + +next(X,Y) :- _next(X,Y). +% add a marker after the end of the next chain for use when parsing +next(Y,afterlast) :- _next(X,Y), not _next(Y,_). + +first(T) :- next(T,T'), not next(_,T). + +name(theory_operators(Ops,P,Name),Name) :- theory_operators(Ops,P,Name). + +% We now encode a (purely) functional Pratt parser by defining the function +% parse(Limit,Right,Next) +% where: +% Limit is the precedence limit. +% Right is the token being parsed. +% Next is the next token in our sequence. +% +% The facts call(parse(L,R,N)) gives us the set of function calls that occur. +% return(parse(L,R,N),(O,N')) gives us the return value of the call, +% where O is a token, and N' designates the token after O. + +% the recur(X,Y) holds when the return value of call(X) +% is set to the return value of call(Y). +call(Y) :- recur(X,Y). +return(X,O) :- recur(X,Y), return(Y,O). + +% If the next token is a unary operator with higher precedence, +% apply it and recur. +recur(parse(Limit,Right,Operator), + parse(Limit,theory_function_(Name, (theory_terms_(0,Right),)),Next)) +:- call(parse(Limit,Right,Operator)), + name(Operator,Name), + arity(Operator,1), + prio_assoc(Operator,(Prec,_)), + Prec>Limit, next(Operator,Next). + +% If the next token is a binary operator +% with higher priority, we start a child parser from the left operand +% with a new precedence limit, +call(parse(Prec-Assoc,Token,Operator')) +:- call(parse(Limit,Right,Operator)), + arity(Operator,2), + prio_assoc(Operator,(Prec,Assoc)), + Prec>Limit, next(Operator,Token), next(Token,Operator'). + +% and recur, having applied the binary operator to right, and +% whatever the child parser returned +recur(parse(Limit,Right,Operator), + parse(Limit,theory_function_(Name,(theory_terms_(0,Output), + theory_terms_(1,Right))),Next)) +:- call(parse(Limit,Right,Operator)), + name(Operator,Name), + arity(Operator,2), + prio_assoc(Operator,(Prec,Assoc)), + Prec>Limit, next(Operator,Token), next(Token,Operator'), + return(parse(Prec-Assoc,Token,Operator'),(Output,Next)). + +% If an operator has lower precedence than the limit, we are +% not allowed to parse it yet, just return. +return(parse(Limit,Right,Operator),(Right,Operator)) +:- call(parse(Limit,Right,Operator)), + prio_assoc(Operator,(Prec,_)), + Prec<=Limit. + +% Return if we run out of tokens. +return(parse(Limit,Right,afterlast),(Right,afterlast)) +:- call(parse(Limit,Right,afterlast)). + +% Start off recursion at the first token with precedence level 0. +call(parse(0,T,T')) :- first(T), next(T,T'). + +#show log("info", location(UT,Begin,End), "Output of parser: ", + theory_function_(Name,Args)) +: return(parse(0,T,T'),(theory_function_(Name,Args),_)), + first(T), next(T,T'), + theory_unparsed_term_elements(E,_,_,T), + theory_unparsed_term(UT,theory_unparsed_term_elements(E)), + location(UT,Begin,End). + +% Finally, add the output of out Pratt parser to the AST in the correct place + +ast_operation( + add(@decompose(theory_function(UT,Name,Args))); + replace(theory_unparsed_term(UT),theory_function(UT))) +:- return(parse(0,T,T'),(theory_function_(Name,Args),_)), + first(T), next(T,T'), + theory_unparsed_term_elements(E,_,_,T), + theory_unparsed_term(UT,theory_unparsed_term_elements(E)), + theory_terms(TT,P,theory_unparsed_term(UT)). diff --git a/tests/asp/transform/theory-parsing/tables-from-theory-defs.lp b/tests/asp/transform/theory-parsing/tables-from-theory-defs.lp new file mode 100644 index 0000000..35535db --- /dev/null +++ b/tests/asp/transform/theory-parsing/tables-from-theory-defs.lp @@ -0,0 +1,15 @@ +operator_table(TermType,(Name,1),(Prio,0)) +:- theory_term_definitions(_,_,TermType,theory_operator_definitions(OD)), + theory_operator_definitions(OD,_,Name,Prio,unary). + +operator_table(TermType,(Name,2),(Prio,1)) +:- theory_term_definitions(_,_,TermType,theory_operator_definitions(OD)), + theory_operator_definitions(OD,_,Name,Prio,binary_left). + +operator_table(TermType,(Name,2),(Prio,0)) +:- theory_term_definitions(_,_,TermType,theory_operator_definitions(OD)), + theory_operator_definitions(OD,_,Name,Prio,binary_right). + +atom_table((Name,Arity),AtomType,ElementTermType,theory_guard_definition(GD)) +:- theory_atom_definitions(_,_,AtomType,Name,Arity, + ElementTermType,theory_guard_definition(GD)). diff --git a/tests/test_reify_reflect.py b/tests/test_reify_reflect.py index 5c74e1d..dd2a671 100644 --- a/tests/test_reify_reflect.py +++ b/tests/test_reify_reflect.py @@ -19,8 +19,6 @@ class TestReifiedAST(TestCase): """Common base class for tests involving the ReifiedAST class.""" - maxDiff = 930 - def setUp(self): # reset id generator between test cases so reification # auto-generates the expected integers diff --git a/tests/test_transform.py b/tests/test_transform.py index 5f5e3db..04461ef 100644 --- a/tests/test_transform.py +++ b/tests/test_transform.py @@ -163,3 +163,75 @@ def test_transform_add_time(self): files_dir / (testname + "_output.lp"), ) + +class TestTransformTheoryParsing(TestTransform): + """Test case for transformation that parses theory terms.""" + + files_dir = test_transform_dir / "theory-parsing" + + def test_parse_theory_unparsed_theory_term_clingo_unknown(self): + """Theory operators without an entry in the operator table of + the appropriate theory term type should raise error.""" + self.assertTransformLogs( + [self.files_dir / "inputs" / "clingo-unknown-operator.lp"], + [ + self.files_dir / "parse-unparsed-theory-terms.lp", + self.files_dir / "clingo-operator-table.lp", + ], + "ERROR", + { + r"1:8-19: No definition for operator '\*' of arity '1' found " + r"for theory term type 'clingo'\.": 1, + r"1:8-19: No definition for operator '~' of arity '2' found " + r"for theory term type 'clingo'\.": 1, + }, + ) + + def test_parse_unparsed_theory_terms_clingo(self): + """Test that unparsed theory terms with clingo operators + (using provided operator table) are parsed correctly. + + """ + self.assertTrasformEqual( + [self.files_dir / "inputs" / "clingo-unparsed-theory-term.lp"], + [ + self.files_dir / "parse-unparsed-theory-terms.lp", + self.files_dir / "clingo-operator-table.lp", + ], + self.files_dir / "outputs" / "clingo-unparsed-theory-term.lp", + ) + + def test_parse_theory_terms_clingo(self): + """Test that theory terms with clingo operators + (using provided operator table) are parsed correctly. + + """ + rast1 = ReifiedAST(reify_location=True) + rast1.add_reified_files( + [self.files_dir / "inputs" / "clingo-theory-term-reified.lp"] + ) + rast1.transform(meta_files=[self.files_dir / "parse-theory-terms.lp", + self.files_dir / "clingo-operator-table.lp"],) + rast2 = ReifiedAST(reify_location=True) + rast2.add_reified_files( + [self.files_dir / "inputs" / "clingo-theory-term-reified.lp"] + ) + self.assertSetEqual(rast1.reified_facts, rast2.reified_facts) + rast3 = ReifiedAST() + rast3.add_reified_files( + [self.files_dir / "inputs" / "clingo-theory-term-unknown-reified.lp"] + ) + pattern = "No definition for operator '\+' of arity '1' found" + with self.assertRaisesRegex(TransformationError, pattern): + rast3.transform(meta_files=[self.files_dir / "parse-theory-terms.lp", + self.files_dir / "clingo-operator-table.lp"]) + pattern = "No definition for operator '!!' of arity '2' found" + with self.assertRaisesRegex(TransformationError, pattern): + rast3.transform(meta_files=[self.files_dir / "parse-theory-terms.lp", + self.files_dir / "clingo-operator-table.lp"]) + + def test_tables_from_theory_defs(self): + """Test that operator and atom tables are extracted correctly + from theory definitions.""" + ctl = Control() + From b192c9513403cdd54a115bd6dde5983d1bd49d00 Mon Sep 17 00:00:00 2001 From: Amade Nemes Date: Thu, 16 Nov 2023 22:54:04 +0100 Subject: [PATCH 7/8] Addo TODO.org. --- TODO.org | 10 ++++++++++ 1 file changed, 10 insertions(+) create mode 100644 TODO.org diff --git a/TODO.org b/TODO.org new file mode 100644 index 0000000..abcdeb2 --- /dev/null +++ b/TODO.org @@ -0,0 +1,10 @@ +* Refication of location should be a method parameter, not something that's permanently set on init. + +* Examine existing metaprogramming applications + +- HTLB +- TLHTC +- meta-telingo +- Deontic logic +- plingo meta encoding +- unsat stuff with Susana From 19e08e4d70f3631e60059d8b87c22fcc6cc2af68 Mon Sep 17 00:00:00 2001 From: Amade Nemes Date: Thu, 16 Nov 2023 22:54:14 +0100 Subject: [PATCH 8/8] Add wip meta-telingo externals. --- .../transform/meta-telingo-externals/input.lp | 15 +++++++++++ .../meta-telingo-externals/output.lp | 22 ++++++++++++++++ .../meta-telingo-externals/transform.lp | 25 +++++++++++++++++++ 3 files changed, 62 insertions(+) create mode 100644 tests/asp/transform/meta-telingo-externals/input.lp create mode 100644 tests/asp/transform/meta-telingo-externals/output.lp create mode 100644 tests/asp/transform/meta-telingo-externals/transform.lp diff --git a/tests/asp/transform/meta-telingo-externals/input.lp b/tests/asp/transform/meta-telingo-externals/input.lp new file mode 100644 index 0000000..bc80999 --- /dev/null +++ b/tests/asp/transform/meta-telingo-externals/input.lp @@ -0,0 +1,15 @@ +#program initially. +a(1). + +#program always. +next(a(X)) :- prev(prev(a(X))). +b :- not(a(X)). + +#program finally +a(1). + +modal(next,1,1). +modal(prev,1,1). + +modal(until,2,1). +modal(until,2,2). diff --git a/tests/asp/transform/meta-telingo-externals/output.lp b/tests/asp/transform/meta-telingo-externals/output.lp new file mode 100644 index 0000000..55f06dd --- /dev/null +++ b/tests/asp/transform/meta-telingo-externals/output.lp @@ -0,0 +1,22 @@ +a(1) :- initially. +next(a(X)) :- prev(prev(a(X))). +a(1) :- finally. +#external prev(prev(a(X))) : a(X). +#external a(X) : next(a(X)). + +c :- not(a(X)). +c :- while(false,a(X)). +#external not(a(X)) : a(X). +#external while(false,a(X)). + +#external until(a(X),b(X)) : a(X),b(X). + + + +a(f(X)) :- prev(a(X)). + +% this has infinite grounding though with the program above +#external prev(a(X)) : a(X). + +% argument restricted programs. +% diff --git a/tests/asp/transform/meta-telingo-externals/transform.lp b/tests/asp/transform/meta-telingo-externals/transform.lp new file mode 100644 index 0000000..fd8a3a5 --- /dev/null +++ b/tests/asp/transform/meta-telingo-externals/transform.lp @@ -0,0 +1,25 @@ +% auxiliary atoms +max_index(T,Index) :- Index = #max{ Pos : terms(T,Pos,_); -1 }, terms(T,_,_). +arity(F,N+1) :- function(F,_,terms(T)), max_index(T,N). + +% collect modal operators and delete them from the AST + +modal(OpName,Arity,Argument) +:- rule(_,literal(L),body_literals(Lt)), not body_literals(Lt,_,_) + literal(L,"pos",function(F)), function(F,modal,terms(T)), + terms(T,0,constant(C)), constant(C, OpName), + terms(T,1,number(N1)), number(N1, Arity), + terms(T,2,number(N2)), number(N2, Argument). + +delete(rule(R,literal(L),body_literals(Lt))) +:- rule(R,literal(L),body_literals(Lt)), not body_literals(Lt,_,_) + literal(L,"pos",function(F)), function(F,modal,terms(T)), + terms(T,0,constant(C)), constant(C, OpName), + terms(T,1,number(N1)), number(N1, Arity), + terms(T,2,number(N2)), number(N2, Argument). + +operator(OpName) :- modal(OpName,_). + +op_tree() +:- modal(Op,Arity,Argument), literal(L,_,function(F)), + function(F,Op,terms(T)), arity(F,Arity), terms(T,Argument-1,O).