summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/hastabel2idp/idp/Project.java23
-rw-r--r--src/hastabel2idp/idp/Structure.java13
-rw-r--r--src/hastabel2idp/idp/Theory.java4
-rw-r--r--src/hastabel2idp/idp/Vocabulary.java13
-rw-r--r--src/hastabel2idp/idp/lang/Expression.java21
-rw-r--r--src/hastabel2idp/idp/lang/Formula.java32
6 files changed, 93 insertions, 13 deletions
diff --git a/src/hastabel2idp/idp/Project.java b/src/hastabel2idp/idp/Project.java
index 26c806e..7678d7c 100644
--- a/src/hastabel2idp/idp/Project.java
+++ b/src/hastabel2idp/idp/Project.java
@@ -6,16 +6,18 @@ import hastabel.World;
import hastabel2idp.idp.lang.Expression;
-import hastabel.lang.Formula;
import hastabel.lang.Predicate;
import hastabel.lang.Type;
import hastabel.lang.Element;
+import java.util.HashMap;
+import java.util.Map;
import java.util.Collection;
import java.util.List;
public class Project
{
+ private final Map<String, Expression> constants;
private final VocabularyOut vocabulary_out;
private final Vocabulary vocabulary;
private final Structure structure;
@@ -27,18 +29,21 @@ public class Project
vocabulary = new Vocabulary(params.get_vocabulary_filename());
structure = new Structure(params.get_structure_filename());
theory = new Theory(params.get_theory_filename());
+ constants = new HashMap<String, Expression>();
}
public void generate
(
final String property_name,
final World world,
- final Formula property
+ final hastabel.lang.Formula property
)
{
+ final hastabel2idp.idp.lang.Formula idp_property;
final Collection<Type> types;
final Collection<Predicate> predicates;
+ idp_property = hastabel2idp.idp.lang.Formula.convert(constants, property);
types = world.get_types_manager().get_all();
predicates = world.get_predicates_manager().get_all();
@@ -91,11 +96,23 @@ public class Project
}
}
+ for (final Map.Entry<String, Expression> constant: constants.entrySet())
+ {
+ final String name, type;
+
+ name = constant.getKey();
+ type =
+ Project.type_name_to_idp(constant.getValue().get_type().get_name());
+
+ vocabulary.add_constant(type, name);
+ structure.add_constant(type, name);
+ }
+
theory.add_predicate
(
property_name,
world.get_variables_manager().get_all_seeked(),
- property
+ idp_property
);
vocabulary.add_target_predicate
diff --git a/src/hastabel2idp/idp/Structure.java b/src/hastabel2idp/idp/Structure.java
index 271a5df..9184fd9 100644
--- a/src/hastabel2idp/idp/Structure.java
+++ b/src/hastabel2idp/idp/Structure.java
@@ -234,4 +234,17 @@ public class Structure
add_function_signature(predicate, signature);
}
}
+
+ public void add_constant
+ (
+ final String type,
+ final String name
+ )
+ {
+ out.write(" ");
+ out.write(name);
+ out.write("=");
+ out.write(name);
+ out.insert_newline();
+ }
}
diff --git a/src/hastabel2idp/idp/Theory.java b/src/hastabel2idp/idp/Theory.java
index 46176ed..c706e7d 100644
--- a/src/hastabel2idp/idp/Theory.java
+++ b/src/hastabel2idp/idp/Theory.java
@@ -28,7 +28,7 @@ public class Theory
(
final String name,
final List<Variable> arguments,
- final hastabel.lang.Formula formula
+ final hastabel2idp.idp.lang.Formula formula
)
{
boolean is_first;
@@ -62,7 +62,7 @@ public class Theory
}
out.write(") <=> (");
- out.write(hastabel2idp.idp.lang.Formula.convert(formula).toString());
+ out.write(formula.toString());
out.write(").");
out.insert_newline();
}
diff --git a/src/hastabel2idp/idp/Vocabulary.java b/src/hastabel2idp/idp/Vocabulary.java
index d1d5fc0..813e73b 100644
--- a/src/hastabel2idp/idp/Vocabulary.java
+++ b/src/hastabel2idp/idp/Vocabulary.java
@@ -154,6 +154,19 @@ public class Vocabulary
}
}
+ public void add_constant
+ (
+ final String type,
+ final String name
+ )
+ {
+ out.write(" ");
+ out.write(name);
+ out.write(":");
+ out.write(type);
+ out.insert_newline();
+ }
+
public void add_target_predicate
(
final String name,
diff --git a/src/hastabel2idp/idp/lang/Expression.java b/src/hastabel2idp/idp/lang/Expression.java
index 1b94120..3953186 100644
--- a/src/hastabel2idp/idp/lang/Expression.java
+++ b/src/hastabel2idp/idp/lang/Expression.java
@@ -2,6 +2,8 @@ package hastabel2idp.idp.lang;
import hastabel.lang.Type;
+import java.util.Map;
+
import java.util.stream.Collectors;
public abstract class Expression
@@ -20,13 +22,28 @@ public abstract class Expression
public static hastabel2idp.idp.lang.Expression convert
(
+ final Map<String, Expression> constants,
final hastabel.lang.Expression hasta_f
)
{
+
if (hasta_f == null)
{
return null;
}
+ else if (hasta_f instanceof hastabel.lang.Element)
+ {
+ final hastabel.lang.Element e;
+ final Expression result;
+
+ e = (hastabel.lang.Element) hasta_f;
+
+ result = convert_named_expression(e);
+
+ constants.put(e.get_name(), result);
+
+ return result;
+ }
else if (hasta_f instanceof hastabel.lang.NamedExpression)
{
return
@@ -40,6 +57,7 @@ public abstract class Expression
return
convert_function_call
(
+ constants,
(hastabel.lang.FunctionCall) hasta_f
);
}
@@ -71,6 +89,7 @@ public abstract class Expression
private static hastabel2idp.idp.lang.Expression convert_function_call
(
+ final Map<String, Expression> constants,
final hastabel.lang.FunctionCall hasta_function_call
)
{
@@ -80,7 +99,7 @@ public abstract class Expression
hasta_function_call.get_function(),
hasta_function_call.get_arguments().stream().map
(
- hastabel2idp.idp.lang.Expression::convert
+ arg -> convert(constants, arg)
).collect(Collectors.toList())
);
}
diff --git a/src/hastabel2idp/idp/lang/Formula.java b/src/hastabel2idp/idp/lang/Formula.java
index c22878d..2f2afe1 100644
--- a/src/hastabel2idp/idp/lang/Formula.java
+++ b/src/hastabel2idp/idp/lang/Formula.java
@@ -1,23 +1,31 @@
package hastabel2idp.idp.lang;
+import java.util.Map;
import java.util.stream.Collectors;
public abstract class Formula
{
public static hastabel2idp.idp.lang.Formula convert
(
+ final Map<String, Expression> constants,
final hastabel.lang.Formula hasta_f
)
{
if (hasta_f instanceof hastabel.lang.Quantifier)
{
- return convert_quantifier((hastabel.lang.Quantifier) hasta_f);
+ return
+ convert_quantifier
+ (
+ constants,
+ (hastabel.lang.Quantifier) hasta_f
+ );
}
else if (hasta_f instanceof hastabel.lang.PredicateFormula)
{
return
convert_predicate_formula
(
+ constants,
(hastabel.lang.PredicateFormula) hasta_f
);
}
@@ -26,12 +34,18 @@ public abstract class Formula
return
convert_operator_formula
(
+ constants,
(hastabel.lang.OperatorFormula) hasta_f
);
}
else if (hasta_f instanceof hastabel.lang.Equals)
{
- return convert_equals((hastabel.lang.Equals) hasta_f);
+ return
+ convert_equals
+ (
+ constants,
+ (hastabel.lang.Equals) hasta_f
+ );
}
else
{
@@ -48,6 +62,7 @@ public abstract class Formula
private static hastabel2idp.idp.lang.Formula convert_quantifier
(
+ final Map<String, Expression> constants,
final hastabel.lang.Quantifier hasta_quantifier
)
{
@@ -55,26 +70,28 @@ public abstract class Formula
new hastabel2idp.idp.lang.Quantifier
(
hasta_quantifier.get_variable(),
- convert(hasta_quantifier.get_formula()),
+ convert(constants, hasta_quantifier.get_formula()),
hasta_quantifier.is_forall()
);
}
private static hastabel2idp.idp.lang.Formula convert_equals
(
+ final Map<String, Expression> constants,
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())
+ Expression.convert(constants, hasta_equals.get_first_operand()),
+ Expression.convert(constants, hasta_equals.get_second_operand())
);
}
private static hastabel2idp.idp.lang.Formula convert_predicate_formula
(
+ final Map<String, Expression> constants,
final hastabel.lang.PredicateFormula hasta_predicate_formula
)
{
@@ -85,13 +102,14 @@ public abstract class Formula
hasta_predicate_formula.get_signature(),
hasta_predicate_formula.get_parameters().stream().map
(
- hastabel2idp.idp.lang.Expression::convert
+ p -> hastabel2idp.idp.lang.Expression.convert(constants, p)
).collect(Collectors.toList())
);
}
private static hastabel2idp.idp.lang.Formula convert_operator_formula
(
+ final Map<String, Expression> constants,
final hastabel.lang.OperatorFormula hasta_operator_formula
)
{
@@ -104,7 +122,7 @@ public abstract class Formula
),
hasta_operator_formula.get_operands().stream().map
(
- hastabel2idp.idp.lang.Formula::convert
+ op -> convert(constants, op)
).collect(Collectors.toList())
);
}