Converts HaStABeL formulas into IDP formulas.

10 files changed, 245 insertions, 2 deletions

diff --git a/src/hastabel2idp/idp/Project.java b/src/hastabel2idp/idp/Project.java
index 037120e..c97af84 100644
--- a/src/hastabel2idp/idp/Project.java
+++ b/src/hastabel2idp/idp/Project.java
@@ -73,6 +73,8 @@ public class Project
          }
       }
 
+      theory.add_formula(property);
+
       vocabulary.write_footer();
       structure.write_footer();
       theory.write_footer();
diff --git a/src/hastabel2idp/idp/Theory.java b/src/hastabel2idp/idp/Theory.java
index fa48c5d..9a060ed 100644
--- a/src/hastabel2idp/idp/Theory.java
+++ b/src/hastabel2idp/idp/Theory.java
@@ -24,6 +24,13 @@ public class Theory
       out.insert_newline();
    }
 
+   public void add_formula (final hastabel.lang.Formula formula)
+   {
+      out.write(hastabel2idp.idp.lang.Formula.convert(formula).toString());
+      out.write(".");
+      out.insert_newline();
+   }
+
    public void write_footer ()
    {
       out.write("}");
diff --git a/src/hastabel2idp/idp/lang/Equals.java b/src/hastabel2idp/idp/lang/Equals.java
index 1632153..1a65ac7 100644
--- a/src/hastabel2idp/idp/lang/Equals.java
+++ b/src/hastabel2idp/idp/lang/Equals.java
@@ -21,4 +21,25 @@ public class Equals extends Formula
    {
       return b;
    }
+
+   @Override
+   public boolean equals (Object o)
+   {
+      final Equals e;
+
+      if ((o == null) || !(o instanceof Equals))
+      {
+         return false;
+      }
+
+      e = (Equals) o;
+
+      return (e.a.equals(a) && e.b.equals(b));
+   }
+
+   @Override
+   public String toString ()
+   {
+      return "(" + a.toString() + "=" + b.toString() + ")";
+   }
 }
diff --git a/src/hastabel2idp/idp/lang/Expression.java b/src/hastabel2idp/idp/lang/Expression.java
index e09955a..1b94120 100644
--- a/src/hastabel2idp/idp/lang/Expression.java
+++ b/src/hastabel2idp/idp/lang/Expression.java
@@ -23,7 +23,11 @@ public abstract class Expression
       final hastabel.lang.Expression hasta_f
    )
    {
-      if (hasta_f instanceof hastabel.lang.NamedExpression)
+      if (hasta_f == null)
+      {
+         return null;
+      }
+      else if (hasta_f instanceof hastabel.lang.NamedExpression)
       {
          return
             convert_named_expression
diff --git a/src/hastabel2idp/idp/lang/FunctionCall.java b/src/hastabel2idp/idp/lang/FunctionCall.java
index 938267c..ee0137e 100644
--- a/src/hastabel2idp/idp/lang/FunctionCall.java
+++ b/src/hastabel2idp/idp/lang/FunctionCall.java
@@ -29,4 +29,50 @@ class FunctionCall extends Expression
    {
       return params;
    }
+
+   @Override
+   public boolean equals (Object o)
+   {
+      final FunctionCall e;
+
+      if ((o == null) || !(o instanceof FunctionCall))
+      {
+         return false;
+      }
+
+      e = (FunctionCall) o;
+
+      return (e.parent.equals(parent) && e.params.equals(params));
+   }
+
+   @Override
+   public String toString ()
+   {
+      final StringBuilder sb;
+      boolean is_first;
+
+      is_first = true;
+      sb = new StringBuilder();
+
+      sb.append(parent.get_name());
+      // TODO: add signature suffix
+
+      for (final Expression param: params)
+      {
+         if (is_first)
+         {
+            is_first = false;
+         }
+         else
+         {
+            sb.append(",");
+         }
+
+         sb.append(param.toString());
+      }
+
+      sb.append(")");
+
+      return sb.toString();
+   }
 }
diff --git a/src/hastabel2idp/idp/lang/NamedExpression.java b/src/hastabel2idp/idp/lang/NamedExpression.java
index 614c6f6..07dc013 100644
--- a/src/hastabel2idp/idp/lang/NamedExpression.java
+++ b/src/hastabel2idp/idp/lang/NamedExpression.java
@@ -41,6 +41,6 @@ public class NamedExpression extends Expression
    @Override
    public String toString ()
    {
-      return (type.get_name() + " " + name);
+      return name;
    }
 }
diff --git a/src/hastabel2idp/idp/lang/Operator.java b/src/hastabel2idp/idp/lang/Operator.java
index 76ef779..a9826b6 100644
--- a/src/hastabel2idp/idp/lang/Operator.java
+++ b/src/hastabel2idp/idp/lang/Operator.java
@@ -55,4 +55,19 @@ public enum Operator
             return null;
       }
    }
+
+   @Override
+   public String toString ()
+   {
+      switch (this)
+      {
+         case NOT: return "~";
+         case AND: return "&";
+         case OR: return "|";
+         case IFF: return "<=>";
+         case IMPLIES: return "=>";
+      }
+
+      return "???";
+   }
 }
diff --git a/src/hastabel2idp/idp/lang/OperatorFormula.java b/src/hastabel2idp/idp/lang/OperatorFormula.java
index 1d422c8..818ea6d 100644
--- a/src/hastabel2idp/idp/lang/OperatorFormula.java
+++ b/src/hastabel2idp/idp/lang/OperatorFormula.java
@@ -26,4 +26,56 @@ class OperatorFormula extends Formula
    {
       return params;
    }
+
+   @Override
+   public boolean equals (Object o)
+   {
+      final OperatorFormula e;
+
+      if ((o == null) || !(o instanceof OperatorFormula))
+      {
+         return false;
+      }
+
+      e = (OperatorFormula) o;
+
+      return (e.parent.equals(parent) && e.params.equals(params));
+   }
+
+   @Override
+   public String toString ()
+   {
+      final StringBuilder sb;
+      boolean is_first;
+
+      sb = new StringBuilder();
+      is_first = true;
+
+      if (parent == Operator.NOT)
+      {
+         sb.append("~");
+      }
+
+      sb.append("(");
+
+      for (final Formula param: params)
+      {
+         if (is_first)
+         {
+            is_first = false;
+         }
+         else
+         {
+            sb.append(" ");
+            sb.append(parent.toString());
+            sb.append(" ");
+         }
+
+         sb.append(param.toString());
+      }
+
+      sb.append(")");
+
+      return sb.toString();
+   }
 }
diff --git a/src/hastabel2idp/idp/lang/PredicateFormula.java b/src/hastabel2idp/idp/lang/PredicateFormula.java
index 54e7032..d82ff35 100644
--- a/src/hastabel2idp/idp/lang/PredicateFormula.java
+++ b/src/hastabel2idp/idp/lang/PredicateFormula.java
@@ -1,5 +1,7 @@
 package hastabel2idp.idp.lang;
 
+import hastabel2idp.idp.Project;
+
 import hastabel.lang.Predicate;
 import hastabel.lang.Type;
 
@@ -37,4 +39,61 @@ class PredicateFormula extends Formula
    {
       return signature;
    }
+
+   @Override
+   public boolean equals (Object o)
+   {
+      final PredicateFormula e;
+
+      if ((o == null) || !(o instanceof PredicateFormula))
+      {
+         return false;
+      }
+
+      e = (PredicateFormula) o;
+
+      return
+         (
+            e.parent.equals(parent)
+            && e.params.equals(params)
+            && e.signature.equals(signature)
+         );
+   }
+
+   @Override
+   public String toString ()
+   {
+      final StringBuilder sb;
+      boolean is_first;
+
+      sb = new StringBuilder();
+      is_first = true;
+
+      sb.append(parent.get_name());
+      sb.append(Project.signature_to_suffix(signature));
+
+      sb.append("(");
+      for (final Expression param: params)
+      {
+         if (param == null)
+         {
+            continue;
+         }
+
+         if (is_first)
+         {
+            is_first = false;
+         }
+         else
+         {
+            sb.append(",");
+         }
+
+         sb.append(param.toString());
+      }
+
+      sb.append(")");
+
+      return sb.toString();
+   }
 }
diff --git a/src/hastabel2idp/idp/lang/Quantifier.java b/src/hastabel2idp/idp/lang/Quantifier.java
index 8f02498..66c030f 100644
--- a/src/hastabel2idp/idp/lang/Quantifier.java
+++ b/src/hastabel2idp/idp/lang/Quantifier.java
@@ -36,4 +36,41 @@ public class Quantifier extends Formula
    {
       return formula;
    }
+
+   @Override
+   public boolean equals (Object o)
+   {
+      final Quantifier e;
+
+      if ((o == null) || !(o instanceof Quantifier))
+      {
+         return false;
+      }
+
+      e = (Quantifier) o;
+
+      return
+         (
+            e.parent.equals(parent)
+            && e.formula.equals(formula)
+            && (e.is_forall == is_forall)
+         );
+   }
+
+   @Override
+   public String toString ()
+   {
+      final StringBuilder sb;
+
+      sb = new StringBuilder();
+
+      sb.append(is_forall ? "!" : "?");
+      sb.append(parent.get_name());
+      sb.append(" [");
+      sb.append(parent.get_type().get_name());
+      sb.append("]: ");
+      sb.append(formula.toString());
+
+      return sb.toString();
+   }
 }