Skip to content

Commit

Permalink
Implement reflect/reify for binary operations, implement transform.
Browse files Browse the repository at this point in the history
  • Loading branch information
namcsi committed Jun 1, 2023
1 parent 6018fc7 commit b7393ea
Show file tree
Hide file tree
Showing 12 changed files with 358 additions and 53 deletions.
9 changes: 9 additions & 0 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,15 @@ a set of facts encoding an asp program into it's string
representation. This operation can be used to derive new programs
which may then e.g. be passed along to an ASP solver.

An application `renopro` implements which makes use of both
reification and reflection is syntactic transformation of input
programs using ASP itself. First the input program is reified into a
set of facts. Then, these facts are combined with a user-provided
meta-program which encodes the desired transformations, and passed
along to `clingo`. Finally, the derived facts representing the
transformed program are reflected back into a program string and
returned to the user.

## Installation

```shell
Expand Down
10 changes: 10 additions & 0 deletions src/renopro/asp/encodings/transform.lp
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
% tagging of input ast elements
ast(rule(H,B)) :- rule(H,B).
ast(literal_tuple(I,P,E)) :- literal_tuple(I,P,E).
ast(term_tuple(I,P,E)) :- term_tuple(I,P,E).

final(A) :- ast(A), not delete(A), not replace(A,_).
final(R) :- replace(_,R).
final(N) :- new(N).

#show final/1.
1 change: 1 addition & 0 deletions src/renopro/asp/examples/transform/good_input.lp
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
good(X) :- person(X).
1 change: 1 addition & 0 deletions src/renopro/asp/examples/transform/good_output.lp
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
good(X) :- person(X); not bad(X).
5 changes: 5 additions & 0 deletions src/renopro/asp/examples/transform/good_transform.lp
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
new(literal_tuple(L,M+1,literal(1,function("bad",term_tuple(T)))))
:- rule(literal(0,function("good",term_tuple(T))),
literal_tuple(L)),
M = #max{ P : literal_tuple(L,P,_) }.

1 change: 1 addition & 0 deletions src/renopro/asp/examples/transform/robot_input.lp
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
sad(robot(X)) :- prev(sad(robot(X))), not cheer_up(robot(X)).
1 change: 1 addition & 0 deletions src/renopro/asp/examples/transform/robot_output.lp
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
sad(robot(X),T) :- sad(robot(X),(T-1)); not cheer_up(robot(X),T).
16 changes: 16 additions & 0 deletions src/renopro/asp/examples/transform/robot_reified.lp
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
rule(literal(0,function("sad",term_tuple(0)))
,literal_tuple(0)).

literal_tuple(0,0,literal(0,function("prev",term_tuple(2)))).
literal_tuple(0,1,literal(1,function("cheer_up",term_tuple(5)))).


term_tuple(0,0,function("robot",term_tuple(1))).
term_tuple(1,0,variable("X")).

term_tuple(2,0,function("sad",term_tuple(3))).
term_tuple(3,0,function("robot",term_tuple(4))).
term_tuple(4,0,variable("X")).

term_tuple(5,0,function("robot",term_tuple(6))).
term_tuple(6,0,variable("X")).
30 changes: 30 additions & 0 deletions src/renopro/asp/examples/transform/robot_transform.lp
Original file line number Diff line number Diff line change
@@ -0,0 +1,30 @@
% helper predicates
max_index(T,M) :- M = #max{ P : term_tuple(T,P,_) }, term_tuple(T,_,_).


% head literal (assume that prev is not allowed in the head).

new(term_tuple(T,M+1,variable("T")))
:- rule(literal(S,function(N,term_tuple(T))),_),
max_index(T,M).

% body literal with prev operator

replace(literal_tuple(L,P,literal(S,function("prev",term_tuple(T)))),
literal_tuple(L,P,literal(S,function(FN,term_tuple(T')))))
:- literal_tuple(L,P,literal(S,function("prev",term_tuple(T)))),
term_tuple(T,0,function(FN, term_tuple(T'))),
not term_tuple(T,1,_).

new(term_tuple(T',M+1,binary_operation("-",variable("T"),number(1))))
:- literal_tuple(L,P,literal(S,function("prev",term_tuple(T)))),
term_tuple(T,0,function(FN, term_tuple(T'))),
not term_tuple(T,1,_),
max_index(T',M).

% body literal without prev operator

new(term_tuple(T,M+1,variable("T")))
:- literal_tuple(L,P,literal(S,function(N,term_tuple(T)))),
N != "prev",
max_index(T,M).
110 changes: 100 additions & 10 deletions src/renopro/clorm_predicates.py
Original file line number Diff line number Diff line change
@@ -1,14 +1,46 @@
"""Definitions of AST elements as clorm predicates."""
from typing import Union, Iterable
import enum

from clorm import IntegerField, Predicate, StringField, combine_fields
from clorm import (IntegerField, Predicate, StringField, RawField,
BaseField, combine_fields, define_enum_field)
from clingo import ast

# by default we use integer identifiers, but allow arbitrary symbols as well
# for flexibility when these are user generated
Identifier = combine_fields([IntegerField, RawField])

term_fields = list()


class Term(BaseField):

def pytocl(v):
global term_fields
for f in term_fields:
try:
return f.pytocl(v)
except (TypeError, ValueError, AttributeError):
pass
raise TypeError("No combined pytocl() match for value {}".format(v))

def cltopy(r):
global term_fields
for f in term_fields:
try:
return f.cltopy(r)
except (TypeError, ValueError):
pass
raise TypeError(
f"Object '{r}' ({type(r)}) failed to unify with Term"
)


class String(Predicate):
value = StringField


class Integer(Predicate):
class Number(Predicate):
value = IntegerField


Expand All @@ -17,7 +49,7 @@ class Variable(Predicate):


class Term_Tuple_Id(Predicate):
identifier = IntegerField
identifier = Identifier

class Meta:
name = "term_tuple"
Expand All @@ -28,11 +60,39 @@ class Function(Predicate):
arguments = Term_Tuple_Id.Field


Term = combine_fields([String.Field, Integer.Field, Variable.Field, Function.Field])
term_fields.extend([String.Field, Number.Field, Variable.Field,
Function.Field])


# Term = combine_fields([String.Field, Integer.Field, Variable.Field,
# Function.Field])


class BinaryOperator(str, enum.Enum):
And = "&" # bitwise and
Division = "/" # arithmetic division
Minus = "-" # arithmetic subtraction
Modulo = "%" # arithmetic modulo
Multiplication = "*" # arithmetic multiplication
Or = "?" # bitwise or
Plus = "+" # arithmetic addition
Power = "**" # arithmetic exponentiation
XOr = "^" # bitwise exclusive or


class Binary_Operation(Predicate):
operator = define_enum_field(parent_field=StringField,
enum_class=BinaryOperator,
name="OperatorField")
left = Term
right = Term


term_fields.append(Binary_Operation.Field)


class Term_Tuple(Predicate):
identifier = IntegerField # identifier of collection
identifier = Identifier # identifier of collection
position = IntegerField # 0 indexed position of element in collection
element = Term

Expand All @@ -43,14 +103,14 @@ class Literal(Predicate):


class Literal_Tuple_Id(Predicate):
identifier = IntegerField
identifier = Identifier

class Meta:
name = "literal_tuple"


class Literal_Tuple(Predicate):
identifier = IntegerField
identifier = Identifier
position = IntegerField # should we keep track of position?
element = Literal.Field

Expand All @@ -62,15 +122,45 @@ class Rule(Predicate):

AST_Predicate = Union[
String,
Integer,
Number,
Variable,
Term_Tuple_Id,
Function,
Term_Tuple,
Literal,
Literal_Tuple_Id,
Literal_Tuple,
Rule,
Rule
]

AST_Facts = Iterable[AST_Predicate]
AST_Predicates = [
String,
Number,
Variable,
Term_Tuple_Id,
Function,
Term_Tuple,
Literal,
Literal_Tuple_Id,
Literal_Tuple,
Rule
]


AST_Fact = Union[
Term_Tuple,
Literal_Tuple,
Rule
]

AST_Facts = [
Term_Tuple,
Literal_Tuple,
Rule
]

# Predicates for AST transformation


class Final(Predicate):
ast = RawField
Loading

0 comments on commit b7393ea

Please sign in to comment.