11 files changed, 490 insertions, 12 deletions
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;
+   }
+}