summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authornsensfel <SpamShield0@noot-noot.org>2018-05-29 15:40:37 +0200
committernsensfel <SpamShield0@noot-noot.org>2018-05-29 15:40:37 +0200
commit9684cef91215ddcf229894ffd63edac2392b4165 (patch)
tree2455e2f31302dc6f08316f4bf3253e1acd635d2d
parent115448b0b5b5f3df329c34890462d06c4f56e018 (diff)
downloadhastabel2idp-9684cef91215ddcf229894ffd63edac2392b4165.zip
hastabel2idp-9684cef91215ddcf229894ffd63edac2392b4165.tar.bz2
Seems to work now, albeit too slowly for real use.
-rw-r--r--src/hastabel2idp/idp/Project.java16
-rw-r--r--src/hastabel2idp/idp/Structure.java19
-rw-r--r--src/hastabel2idp/idp/Theory.java2
-rw-r--r--src/hastabel2idp/idp/Vocabulary.java25
-rw-r--r--src/hastabel2idp/idp/lang/FunctionCall.java14
-rw-r--r--src/hastabel2idp/idp/lang/Quantifier.java4
6 files changed, 66 insertions, 14 deletions
diff --git a/src/hastabel2idp/idp/Project.java b/src/hastabel2idp/idp/Project.java
index f0aeab7..26c806e 100644
--- a/src/hastabel2idp/idp/Project.java
+++ b/src/hastabel2idp/idp/Project.java
@@ -127,7 +127,7 @@ public class Project
if (t != null)
{
sb.append("_");
- sb.append(t.get_name());
+ sb.append(Project.type_name_to_idp(t.get_name()));
}
}
@@ -145,10 +145,22 @@ public class Project
if (param != null)
{
sb.append("_");
- sb.append(param.get_type().get_name());
+ sb.append(Project.type_name_to_idp(param.get_type().get_name()));
}
}
return sb.toString();
}
+
+ public static String type_name_to_idp (final String type_name)
+ {
+ /** IDP doesn't like us using the 'string' type name. **/
+
+ if (type_name.equals("string"))
+ {
+ return "hastastring";
+ }
+
+ return type_name;
+ }
}
diff --git a/src/hastabel2idp/idp/Structure.java b/src/hastabel2idp/idp/Structure.java
index c7fb09e..271a5df 100644
--- a/src/hastabel2idp/idp/Structure.java
+++ b/src/hastabel2idp/idp/Structure.java
@@ -35,7 +35,7 @@ public class Structure
boolean is_first_member;
out.write(" ");
- out.write(type.get_name());
+ out.write(Project.type_name_to_idp(type.get_name()));
out.write("={");
out.insert_newline();
@@ -135,6 +135,16 @@ public class Structure
final Collection<List<Type>> partial_signatures
)
{
+ if (relevant_signatures.size() == 0)
+ {
+ System.err.println
+ (
+ "[E] Predicate "
+ + predicate.get_name()
+ + " has no signatures."
+ );
+ }
+
for (final List<Type> signature: relevant_signatures)
{
add_predicate_signature(predicate, signature, false);
@@ -198,11 +208,14 @@ public class Structure
out.write(", ");
}
- out.write(member.get(i).get_name());
+ out.write(Project.type_name_to_idp(member.get(i).get_name()));
}
out.write("->");
- out.write(member.get(signature_size_m1).get_name());
+ out.write
+ (
+ Project.type_name_to_idp(member.get(signature_size_m1).get_name())
+ );
}
out.insert_newline();
diff --git a/src/hastabel2idp/idp/Theory.java b/src/hastabel2idp/idp/Theory.java
index 282c518..46176ed 100644
--- a/src/hastabel2idp/idp/Theory.java
+++ b/src/hastabel2idp/idp/Theory.java
@@ -40,7 +40,7 @@ public class Theory
out.write("!");
out.write(argument.get_name());
out.write(" [");
- out.write(argument.get_type().get_name());
+ out.write(Project.type_name_to_idp(argument.get_type().get_name()));
out.write("]: ");
}
diff --git a/src/hastabel2idp/idp/Vocabulary.java b/src/hastabel2idp/idp/Vocabulary.java
index ca9f591..d1d5fc0 100644
--- a/src/hastabel2idp/idp/Vocabulary.java
+++ b/src/hastabel2idp/idp/Vocabulary.java
@@ -34,7 +34,7 @@ public class Vocabulary
public void add_type (final Type type)
{
out.write(" type ");
- out.write(type.get_name());
+ out.write(Project.type_name_to_idp(type.get_name()));
out.insert_newline();
}
@@ -69,7 +69,7 @@ public class Vocabulary
out.write(", ");
}
- out.write(sig_type.get_name());
+ out.write(Project.type_name_to_idp(sig_type.get_name()));
}
out.write(")");
@@ -97,17 +97,20 @@ public class Vocabulary
if (0 < signature_size_m1)
{
- out.write(signature.get(0).get_name());
+ out.write(Project.type_name_to_idp(signature.get(0).get_name()));
}
for (int i = 1; i < signature_size_m1; ++i)
{
out.write(", ");
- out.write(signature.get(i).get_name());
+ out.write(Project.type_name_to_idp(signature.get(i).get_name()));
}
out.write("):");
- out.write(signature.get(signature_size_m1).get_name());
+ out.write
+ (
+ Project.type_name_to_idp(signature.get(signature_size_m1).get_name())
+ );
out.insert_newline();
}
@@ -118,6 +121,16 @@ public class Vocabulary
final Collection<List<Type>> partial_signatures
)
{
+ if (relevant_signatures.size() == 0)
+ {
+ System.err.println
+ (
+ "[E] Predicate "
+ + predicate.get_name()
+ + " has no signatures."
+ );
+ }
+
for (final List<Type> signature: relevant_signatures)
{
add_predicate_signature(predicate, signature);
@@ -166,7 +179,7 @@ public class Vocabulary
out.write(", ");
}
- out.write(argument.get_type().get_name());
+ out.write(Project.type_name_to_idp(argument.get_type().get_name()));
}
out.write(")");
diff --git a/src/hastabel2idp/idp/lang/FunctionCall.java b/src/hastabel2idp/idp/lang/FunctionCall.java
index cd81c7b..6a0f755 100644
--- a/src/hastabel2idp/idp/lang/FunctionCall.java
+++ b/src/hastabel2idp/idp/lang/FunctionCall.java
@@ -20,6 +20,16 @@ class FunctionCall extends Expression
super(parent.get_function_type());
this.parent = parent;
this.params = params;
+
+ if (type == null)
+ {
+ System.err.println
+ (
+ "[E] Use of 'function' "
+ + parent.get_name()
+ + ", despite its function type being NULL."
+ );
+ }
}
public Predicate get_function ()
@@ -57,7 +67,9 @@ class FunctionCall extends Expression
sb = new StringBuilder();
sb.append(parent.get_name());
- Project.parameters_to_suffix(params);
+ sb.append(Project.parameters_to_suffix(params));
+ sb.append("_");
+ sb.append(Project.type_name_to_idp(type.get_name()));
sb.append("_f(");
is_first = true;
diff --git a/src/hastabel2idp/idp/lang/Quantifier.java b/src/hastabel2idp/idp/lang/Quantifier.java
index 040ff21..37a8cc2 100644
--- a/src/hastabel2idp/idp/lang/Quantifier.java
+++ b/src/hastabel2idp/idp/lang/Quantifier.java
@@ -1,5 +1,7 @@
package hastabel2idp.idp.lang;
+import hastabel2idp.idp.Project;
+
import hastabel.lang.Variable;
import java.util.List;
@@ -67,7 +69,7 @@ public class Quantifier extends Formula
sb.append(is_forall ? "!" : "?");
sb.append(parent.get_name());
sb.append(" [");
- sb.append(parent.get_type().get_name());
+ sb.append(Project.type_name_to_idp(parent.get_type().get_name()));
sb.append("]: (");
sb.append(formula.toString());
sb.append(")");