| summaryrefslogtreecommitdiff |
diff options
| -rw-r--r-- | Makefile | 4 | ||||
| -rw-r--r-- | src/hastabel2idp/Main.java | 37 | ||||
| -rw-r--r-- | src/hastabel2idp/idp/Project.java | 3 | ||||
| -rw-r--r-- | src/hastabel2idp/idp/lang/Equals.java | 24 | ||||
| -rw-r--r-- | src/hastabel2idp/idp/lang/Expression.java | 83 | ||||
| -rw-r--r-- | src/hastabel2idp/idp/lang/Formula.java | 111 | ||||
| -rw-r--r-- | src/hastabel2idp/idp/lang/FunctionCall.java | 32 | ||||
| -rw-r--r-- | src/hastabel2idp/idp/lang/NamedExpression.java | 46 | ||||
| -rw-r--r-- | src/hastabel2idp/idp/lang/Operator.java | 58 | ||||
| -rw-r--r-- | src/hastabel2idp/idp/lang/OperatorFormula.java | 29 | ||||
| -rw-r--r-- | src/hastabel2idp/idp/lang/PredicateFormula.java | 40 | ||||
| -rw-r--r-- | src/hastabel2idp/idp/lang/Quantifier.java | 39 |
12 files changed, 491 insertions, 15 deletions
@@ -46,9 +46,7 @@ CLASSPATH = "$(SRC_DIR):$(BIN_DIR):$(ANTLR_JAR):$(HASTABEL_JAR)" ## Makefile Magic ############################################################## MANIFEST = $(SRC_DIR)/Manifest.txt -JAVA_SOURCES = \ - $(wildcard $(SRC_DIR)/hastabel2idp/*.java) \ - $(wildcard $(SRC_DIR)/hastabel2idp/*/*.java) +JAVA_SOURCES = $(shell find $(SRC_DIR)/hastabel2idp/ -name "*.java") CLASSES = $(patsubst $(SRC_DIR)/%,$(BIN_DIR)/%, $(JAVA_SOURCES:.java=.class)) ## Makefile Rules ############################################################## diff --git a/src/hastabel2idp/Main.java b/src/hastabel2idp/Main.java index 05266ff..0974623 100644 --- a/src/hastabel2idp/Main.java +++ b/src/hastabel2idp/Main.java @@ -3,6 +3,7 @@ package hastabel2idp; import hastabel2idp.idp.Project; import hastabel.World; +import hastabel.lang.Formula; import java.io.IOException; @@ -12,6 +13,7 @@ public class Main { final Parameters params; final World world; + final Formula property; System.out.println("#### HaStABeL to IDP ####"); System.out.println("# Parsing parameters..."); @@ -24,6 +26,8 @@ public class Main world = new World(); + System.out.println("# Loading model..."); + load_model(world, params); if (!world.is_valid()) @@ -33,13 +37,21 @@ public class Main return; } - write_idp(world, params); + System.out.println("# Loading property..."); - if (!world.is_valid()) + property = load_property(world, params); + + if ((!world.is_valid()) || (property == null)) { + System.out.println("# Failure."); + return; } + System.out.println("# Generating IDP..."); + + write_idp(world, property, params); + OutputFile.close_all(); System.out.println("# Done."); @@ -94,16 +106,17 @@ public class Main System.out.println("# Modeling graphs in first-order..."); world.ensure_first_order(); + } - if (!world.is_valid()) - { - return; - } - - System.out.println("# Loading property..."); + private static Formula load_property + ( + final World world, + final Parameters params + ) + { try { - world.load_property(params.get_property_file()); + return world.load_property(params.get_property_file()); } catch (final IOException ioe) { @@ -117,20 +130,22 @@ public class Main world.invalidate(); } + + return null; } private static void write_idp ( final World world, + final Formula property, final Parameters params ) { final Project project; - System.out.println("# Generating IDP..."); project = new Project(params); - project.generate(world); + project.generate(world, property); } } diff --git a/src/hastabel2idp/idp/Project.java b/src/hastabel2idp/idp/Project.java index fcb37b5..037120e 100644 --- a/src/hastabel2idp/idp/Project.java +++ b/src/hastabel2idp/idp/Project.java @@ -4,6 +4,7 @@ import hastabel2idp.Parameters; import hastabel.World; +import hastabel.lang.Formula; import hastabel.lang.Predicate; import hastabel.lang.Type; import hastabel.lang.Element; @@ -24,7 +25,7 @@ public class Project theory = new Theory(params.get_theory_filename()); } - public void generate (final World world) + public void generate (final World world, final Formula property) { final Collection<Type> types; final Collection<Predicate> predicates; diff --git a/src/hastabel2idp/idp/lang/Equals.java b/src/hastabel2idp/idp/lang/Equals.java new file mode 100644 index 0000000..1632153 --- /dev/null +++ b/src/hastabel2idp/idp/lang/Equals.java @@ -0,0 +1,24 @@ +package hastabel2idp.idp.lang; + +import java.util.List; + +public class Equals extends Formula +{ + private final Expression a, b; + + public Equals (final Expression a, final Expression b) + { + this.a = a; + this.b = b; + } + + public Expression get_first_operand () + { + return a; + } + + public Expression get_second_operand () + { + return b; + } +} diff --git a/src/hastabel2idp/idp/lang/Expression.java b/src/hastabel2idp/idp/lang/Expression.java new file mode 100644 index 0000000..e09955a --- /dev/null +++ b/src/hastabel2idp/idp/lang/Expression.java @@ -0,0 +1,83 @@ +package hastabel2idp.idp.lang; + +import hastabel.lang.Type; + +import java.util.stream.Collectors; + +public abstract class Expression +{ + protected final Type type; + + public Expression (final Type type) + { + this.type = type; + } + + public Type get_type() + { + return type; + } + + public static hastabel2idp.idp.lang.Expression convert + ( + final hastabel.lang.Expression hasta_f + ) + { + if (hasta_f instanceof hastabel.lang.NamedExpression) + { + return + convert_named_expression + ( + (hastabel.lang.NamedExpression) hasta_f + ); + } + else if (hasta_f instanceof hastabel.lang.FunctionCall) + { + return + convert_function_call + ( + (hastabel.lang.FunctionCall) hasta_f + ); + } + else + { + System.err.println + ( + "[F] HaStABeL to IDP does not recognize the following HaStABeL" + + " expression: " + + hasta_f.toString() + ); + + return null; + } + } + + private static hastabel2idp.idp.lang.Expression convert_named_expression + ( + final hastabel.lang.NamedExpression hasta_named_expression + ) + { + return + new hastabel2idp.idp.lang.NamedExpression + ( + hasta_named_expression.get_type(), + hasta_named_expression.get_name() + ); + } + + private static hastabel2idp.idp.lang.Expression convert_function_call + ( + final hastabel.lang.FunctionCall hasta_function_call + ) + { + return + new hastabel2idp.idp.lang.FunctionCall + ( + hasta_function_call.get_function(), + hasta_function_call.get_arguments().stream().map + ( + hastabel2idp.idp.lang.Expression::convert + ).collect(Collectors.toList()) + ); + } +} diff --git a/src/hastabel2idp/idp/lang/Formula.java b/src/hastabel2idp/idp/lang/Formula.java new file mode 100644 index 0000000..c22878d --- /dev/null +++ b/src/hastabel2idp/idp/lang/Formula.java @@ -0,0 +1,111 @@ +package hastabel2idp.idp.lang; + +import java.util.stream.Collectors; + +public abstract class Formula +{ + public static hastabel2idp.idp.lang.Formula convert + ( + final hastabel.lang.Formula hasta_f + ) + { + if (hasta_f instanceof hastabel.lang.Quantifier) + { + return convert_quantifier((hastabel.lang.Quantifier) hasta_f); + } + else if (hasta_f instanceof hastabel.lang.PredicateFormula) + { + return + convert_predicate_formula + ( + (hastabel.lang.PredicateFormula) hasta_f + ); + } + else if (hasta_f instanceof hastabel.lang.OperatorFormula) + { + return + convert_operator_formula + ( + (hastabel.lang.OperatorFormula) hasta_f + ); + } + else if (hasta_f instanceof hastabel.lang.Equals) + { + return convert_equals((hastabel.lang.Equals) hasta_f); + } + else + { + System.err.println + ( + "[F] HaStABeL to IDP does not recognize the following HaStABeL" + + " formula: " + + hasta_f.toString() + ); + + return null; + } + } + + private static hastabel2idp.idp.lang.Formula convert_quantifier + ( + final hastabel.lang.Quantifier hasta_quantifier + ) + { + return + new hastabel2idp.idp.lang.Quantifier + ( + hasta_quantifier.get_variable(), + convert(hasta_quantifier.get_formula()), + hasta_quantifier.is_forall() + ); + } + + private static hastabel2idp.idp.lang.Formula convert_equals + ( + final hastabel.lang.Equals hasta_equals + ) + { + return + new hastabel2idp.idp.lang.Equals + ( + Expression.convert(hasta_equals.get_first_operand()), + Expression.convert(hasta_equals.get_second_operand()) + ); + } + + private static hastabel2idp.idp.lang.Formula convert_predicate_formula + ( + final hastabel.lang.PredicateFormula hasta_predicate_formula + ) + { + return + new hastabel2idp.idp.lang.PredicateFormula + ( + hasta_predicate_formula.get_predicate(), + hasta_predicate_formula.get_signature(), + hasta_predicate_formula.get_parameters().stream().map + ( + hastabel2idp.idp.lang.Expression::convert + ).collect(Collectors.toList()) + ); + } + + private static hastabel2idp.idp.lang.Formula convert_operator_formula + ( + final hastabel.lang.OperatorFormula hasta_operator_formula + ) + { + return + new hastabel2idp.idp.lang.OperatorFormula + ( + hastabel2idp.idp.lang.Operator.convert + ( + hasta_operator_formula.get_operator() + ), + hasta_operator_formula.get_operands().stream().map + ( + hastabel2idp.idp.lang.Formula::convert + ).collect(Collectors.toList()) + ); + } +} diff --git a/src/hastabel2idp/idp/lang/FunctionCall.java b/src/hastabel2idp/idp/lang/FunctionCall.java new file mode 100644 index 0000000..938267c --- /dev/null +++ b/src/hastabel2idp/idp/lang/FunctionCall.java @@ -0,0 +1,32 @@ +package hastabel2idp.idp.lang; + +import hastabel.lang.Predicate; + +import java.util.List; + +class FunctionCall extends Expression +{ + private final Predicate parent; + private final List<Expression> params; + + public FunctionCall + ( + final Predicate parent, + final List<Expression> params + ) + { + super(parent.get_function_type()); + this.parent = parent; + this.params = params; + } + + public Predicate get_function () + { + return parent; + } + + public List<Expression> get_arguments () + { + return params; + } +} diff --git a/src/hastabel2idp/idp/lang/NamedExpression.java b/src/hastabel2idp/idp/lang/NamedExpression.java new file mode 100644 index 0000000..614c6f6 --- /dev/null +++ b/src/hastabel2idp/idp/lang/NamedExpression.java @@ -0,0 +1,46 @@ +package hastabel2idp.idp.lang; + +import hastabel.lang.Type; + +public class NamedExpression extends Expression +{ + public final String name; + + public NamedExpression (final Type type, final String name) + { + super(type); + this.name = name; + } + + public String get_name () + { + return name; + } + + @Override + public boolean equals (Object o) + { + final NamedExpression e; + + if ((o == null) || !(o instanceof NamedExpression)) + { + return false; + } + + e = (NamedExpression) o; + + return (e.name.equals(name) && e.type.equals(type)); + } + + @Override + public int hashCode () + { + return (name + '@' + type.get_name()).hashCode(); + } + + @Override + public String toString () + { + return (type.get_name() + " " + name); + } +} diff --git a/src/hastabel2idp/idp/lang/Operator.java b/src/hastabel2idp/idp/lang/Operator.java new file mode 100644 index 0000000..76ef779 --- /dev/null +++ b/src/hastabel2idp/idp/lang/Operator.java @@ -0,0 +1,58 @@ +package hastabel2idp.idp.lang; + +import java.util.List; +import java.util.ArrayList; + +public enum Operator +{ + NOT, + AND, + OR, + IFF, + IMPLIES; + + public Formula as_formula (final List<Formula> params) + { + final OperatorFormula result; + + result = new OperatorFormula(this, params); + + return result; + } + + public Formula as_formula_ (final Formula... e_params) + { + final ArrayList<Formula> params; + + params = new ArrayList<Formula>(); + + for (final Formula f: e_params) + { + params.add(f); + } + + return as_formula(params); + } + + public static Operator convert (final hastabel.lang.Operator operator) + { + switch (operator) + { + case NOT: return NOT; + case AND: return AND; + case OR: return OR; + case IFF: return IFF; + case IMPLIES: return IMPLIES; + + default: + System.err.println + ( + "[F] HaStABeL to IDP can't handle the " + + operator.toString() + + " operator." + ); + + return null; + } + } +} diff --git a/src/hastabel2idp/idp/lang/OperatorFormula.java b/src/hastabel2idp/idp/lang/OperatorFormula.java new file mode 100644 index 0000000..1d422c8 --- /dev/null +++ b/src/hastabel2idp/idp/lang/OperatorFormula.java @@ -0,0 +1,29 @@ +package hastabel2idp.idp.lang; + +import java.util.List; + +class OperatorFormula extends Formula +{ + private final Operator parent; + private final List<Formula> params; + + public OperatorFormula + ( + final Operator parent, + final List<Formula> params + ) + { + this.parent = parent; + this.params = params; + } + + public Operator get_operator () + { + return parent; + } + + public List<Formula> get_operands () + { + return params; + } +} diff --git a/src/hastabel2idp/idp/lang/PredicateFormula.java b/src/hastabel2idp/idp/lang/PredicateFormula.java new file mode 100644 index 0000000..54e7032 --- /dev/null +++ b/src/hastabel2idp/idp/lang/PredicateFormula.java @@ -0,0 +1,40 @@ +package hastabel2idp.idp.lang; + +import hastabel.lang.Predicate; +import hastabel.lang.Type; + +import java.util.List; + +class PredicateFormula extends Formula +{ + private final Predicate parent; + private final List<Expression> params; + private final List<Type> signature; + + public PredicateFormula + ( + final Predicate parent, + final List<Type> signature, + final List<Expression> params + ) + { + this.parent = parent; + this.signature = signature; + this.params = params; + } + + public Predicate get_predicate () + { + return parent; + } + + public List<Expression> get_parameters () + { + return params; + } + + public List<Type> get_signature () + { + return signature; + } +} diff --git a/src/hastabel2idp/idp/lang/Quantifier.java b/src/hastabel2idp/idp/lang/Quantifier.java new file mode 100644 index 0000000..8f02498 --- /dev/null +++ b/src/hastabel2idp/idp/lang/Quantifier.java @@ -0,0 +1,39 @@ +package hastabel2idp.idp.lang; + +import hastabel.lang.Variable; + +import java.util.List; + +public class Quantifier extends Formula +{ + private final boolean is_forall; + private final Variable parent; + private final Formula formula; + + public Quantifier + ( + final Variable parent, + final Formula formula, + final boolean is_forall + ) + { + this.parent = parent; + this.formula = formula; + this.is_forall = is_forall; + } + + public boolean is_forall () + { + return is_forall; + } + + public Variable get_variable () + { + return parent; + } + + public Formula get_formula () + { + return formula; + } +} |