summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authornsensfel <SpamShield0@noot-noot.org>2018-05-29 14:00:13 +0200
committernsensfel <SpamShield0@noot-noot.org>2018-05-29 14:00:13 +0200
commit2354098a6d9120852eaad36fa520bab4569dfc81 (patch)
tree7281e3fb881e5d48ec1f4d6dffe03accc8532582
parent08ef0f4dfe81e61bb41fd233b49028271ec3bee9 (diff)
downloadhastabel-2354098a6d9120852eaad36fa520bab4569dfc81.zip
hastabel-2354098a6d9120852eaad36fa520bab4569dfc81.tar.bz2
Trying (and failing) to use the async FF prop.
-rw-r--r--src/hastabel/LangLexer.g43
-rw-r--r--src/hastabel/LangParser.g425
-rw-r--r--src/hastabel/Predicates.java14
-rw-r--r--src/hastabel/PropertyParser.g417
-rw-r--r--src/hastabel/lang/OperatorFormula.java10
-rw-r--r--src/hastabel/lang/Predicate.java100
-rw-r--r--src/hastabel/lang/Quantifier.java8
7 files changed, 146 insertions, 31 deletions
diff --git a/src/hastabel/LangLexer.g4 b/src/hastabel/LangLexer.g4
index 773ae54..2de366f 100644
--- a/src/hastabel/LangLexer.g4
+++ b/src/hastabel/LangLexer.g4
@@ -13,7 +13,8 @@ SUB_TYPE_OF: '::';
STAR: '*';
ADD_TYPE_KW: 'add_type' SEP;
-ADD_PREDICATE_KW: ('add_predicate' | 'add_function') SEP;
+ADD_PREDICATE_KW: 'add_predicate' SEP;
+ADD_FUNCTION_KW: 'add_function' SEP;
ADD_TEMPLATE_KW: 'add_template' SEP;
WS: SEP;
diff --git a/src/hastabel/LangParser.g4 b/src/hastabel/LangParser.g4
index e71bf81..19f2ea0 100644
--- a/src/hastabel/LangParser.g4
+++ b/src/hastabel/LangParser.g4
@@ -37,6 +37,10 @@ lang_instr:
{
}
+ | (WS)* ADD_FUNCTION_KW (WS)* new_function (WS)*
+ {
+ }
+
| (WS)* ADD_PREDICATE_KW (WS)* new_predicate (WS)*
{
}
@@ -175,7 +179,26 @@ new_predicate:
signature.add(WORLD.get_types_manager().get(type_names.next()));
}
- WORLD.get_predicates_manager().declare(signature, ($ID.text));
+ WORLD.get_predicates_manager().declare(signature, ($ID.text), false);
+ }
+;
+
+new_function:
+ ID (WS)* L_PAREN (WS)* ident_list (WS)* R_PAREN
+ {
+ final List<Type> signature;
+ final Iterator<String> type_names;
+
+ signature = new ArrayList<Type>();
+
+ type_names = ($ident_list.list).iterator();
+
+ while (type_names.hasNext())
+ {
+ signature.add(WORLD.get_types_manager().get(type_names.next()));
+ }
+
+ WORLD.get_predicates_manager().declare(signature, ($ID.text), true);
}
;
diff --git a/src/hastabel/Predicates.java b/src/hastabel/Predicates.java
index 66eebd7..7999e1d 100644
--- a/src/hastabel/Predicates.java
+++ b/src/hastabel/Predicates.java
@@ -23,11 +23,16 @@ public class Predicates
this.parent_mgr = parent_mgr;
}
- public Predicate declare (final List<Type> signature, final String name)
+ public Predicate declare
+ (
+ final List<Type> signature,
+ final String name,
+ final boolean can_be_used_as_function
+ )
{
final Predicate result, previous_instance;
- result = new Predicate(signature, name);
+ result = new Predicate(signature, name, can_be_used_as_function);
previous_instance = from_name.get(name);
@@ -45,6 +50,11 @@ public class Predicates
previous_instance.add_signature(signature);
+ if (can_be_used_as_function)
+ {
+ previous_instance.mark_as_function();
+ }
+
return null;
}
diff --git a/src/hastabel/PropertyParser.g4 b/src/hastabel/PropertyParser.g4
index c58f0a6..051ba1a 100644
--- a/src/hastabel/PropertyParser.g4
+++ b/src/hastabel/PropertyParser.g4
@@ -338,6 +338,7 @@ regex_special_predicate [Variable current_node]
{
WORLD.invalidate();
}
+
string_type.mark_as_used();
string_matches.mark_as_used();
@@ -1255,7 +1256,7 @@ au_operator [Variable current_node]
f1_node,
Formula.implies
(
- is_before.as_formula_(f1_node, f2_node, next_path),
+ is_before.as_formula_(next_path, f1_node, f2_node),
($f1.result)
)
)
@@ -1369,7 +1370,7 @@ eu_operator [Variable current_node]
f1_node,
Formula.implies
(
- is_before.as_formula_(f1_node, f2_node, next_path),
+ is_before.as_formula_(next_path, f1_node, f2_node),
($f1.result)
)
)
@@ -1455,7 +1456,7 @@ depth_no_parent_operator [Variable current_node]
path_type.mark_as_used();
depth_type.mark_as_used();
- depth.mark_as_used();
+ depth.mark_as_used_as_function();
contains_node.mark_as_used();
is_path_of.mark_as_used();
is_before.mark_as_used();
@@ -1501,9 +1502,9 @@ depth_no_parent_operator [Variable current_node]
(
is_before.as_formula_
(
+ next_path,
node_of_path,
- node_for_f,
- next_path
+ node_for_f
),
Formula.not
(
@@ -1592,7 +1593,7 @@ depth_no_change_operator [Variable current_node]
path_type.mark_as_used();
depth_type.mark_as_used();
- depth.mark_as_used();
+ depth.mark_as_used_as_function();
contains_node.mark_as_used();
is_path_of.mark_as_used();
is_before.mark_as_used();
@@ -1634,9 +1635,9 @@ depth_no_change_operator [Variable current_node]
(
is_before.as_formula_
(
+ next_path,
node_of_path,
- node_for_f,
- next_path
+ node_for_f
),
Formula.equals
(
diff --git a/src/hastabel/lang/OperatorFormula.java b/src/hastabel/lang/OperatorFormula.java
index 190e6cb..8526293 100644
--- a/src/hastabel/lang/OperatorFormula.java
+++ b/src/hastabel/lang/OperatorFormula.java
@@ -55,7 +55,15 @@ public class OperatorFormula extends Formula
for (final Formula param: params)
{
sb.append(" ");
- sb.append(param.toString());
+
+ if (param == null)
+ {
+ sb.append("NULL");
+ }
+ else
+ {
+ sb.append(param.toString());
+ }
}
sb.append(")");
diff --git a/src/hastabel/lang/Predicate.java b/src/hastabel/lang/Predicate.java
index 37b8e9d..fceed3c 100644
--- a/src/hastabel/lang/Predicate.java
+++ b/src/hastabel/lang/Predicate.java
@@ -16,41 +16,49 @@ public class Predicate
private final Type function_type;
private final Set<List<Element>> members;
private final String name;
- private boolean is_used;
+ private boolean can_be_used_as_function;
+ private boolean is_used_as_predicate, is_used_as_function;
- public Predicate (final List<Type> signature, final String name)
+ public Predicate
+ (
+ final List<Type> signature,
+ final String name,
+ final boolean can_be_used_as_function
+ )
{
partial_signatures = new ArrayList<List<Type>>(0);
signatures = new ArrayList<List<Type>>(1);
signatures.add(signature);
this.function_type = signature.get(signature.size() - 1);
-
this.name = name;
+ this.can_be_used_as_function = can_be_used_as_function;
members = new HashSet<List<Element>>();
- is_used = false;
+ is_used_as_predicate = false;
+ is_used_as_function = false;
}
public Predicate
(
- final Collection<List<Type>> signatures,
- final Collection<List<Type>> partial_signatures,
- final Type function_type,
- final String name
+ final Predicate source
)
{
- this.signatures = new ArrayList<List<Type>>();
- this.signatures.addAll(signatures);
+ signatures = new ArrayList<List<Type>>();
+ signatures.addAll(source.signatures);
- this.partial_signatures = new ArrayList<List<Type>>(0);
- this.partial_signatures.addAll(partial_signatures);
+ partial_signatures = new ArrayList<List<Type>>(0);
+ partial_signatures.addAll(source.partial_signatures);
- this.name = name;
- this.function_type = function_type;
+ name = source.name;
+ function_type = source.function_type;
members = new HashSet<List<Element>>();
+
+ can_be_used_as_function = source.can_be_used_as_function;
+ is_used_as_predicate = source.is_used_as_predicate;
+ is_used_as_function = source.is_used_as_function;
}
public void add_member (final List<Element> elements)
@@ -172,6 +180,34 @@ public class Predicate
return true;
}
+ private boolean is_compatible_with_fun_signature
+ (
+ final List<Expression> elements,
+ final List<Type> signature
+ )
+ {
+ final Iterator<Expression> e_iter;
+ final Iterator<Type> s_iter;
+
+ if (elements.size() != (signature.size() - 1))
+ {
+ return false;
+ }
+
+ e_iter = elements.iterator();
+ s_iter = signature.iterator();
+
+ while (e_iter.hasNext())
+ {
+ if (!s_iter.next().includes(e_iter.next().get_type()))
+ {
+ return false;
+ }
+ }
+
+ return true;
+ }
+
// "incompatible types: List<Element> cannot be converted to List<Expression>"
private boolean is_compatible_with_signature2
(
@@ -432,7 +468,7 @@ public class Predicate
public Predicate shallow_copy ()
{
- return new Predicate(signatures, partial_signatures, function_type, name);
+ return new Predicate(this);
}
@Override
@@ -529,7 +565,7 @@ public class Predicate
public void mark_as_used ()
{
- is_used = true;
+ is_used_as_predicate = true;
}
public void mark_as_used_as_function ()
@@ -539,12 +575,27 @@ public class Predicate
signature.get(signature.size() - 1).mark_as_used();
}
- is_used = true;
+ is_used_as_function = true;
+ }
+
+ public void mark_as_function ()
+ {
+ can_be_used_as_function = true;
}
public boolean is_used ()
{
- return is_used;
+ return is_used_as_predicate || is_used_as_function;
+ }
+
+ public boolean is_used_as_predicate ()
+ {
+ return is_used_as_predicate;
+ }
+
+ public boolean is_used_as_function ()
+ {
+ return is_used_as_function;
}
@Override
@@ -586,6 +637,19 @@ public class Predicate
if (signature == null)
{
+ System.err.print
+ (
+ "[E] No compatible signature for ("
+ + name
+ );
+
+ for (final Expression expr: params)
+ {
+ System.err.print(" " + expr + "/" + expr.get_type().get_name());
+ }
+
+ System.err.println(").");
+
return null;
}
diff --git a/src/hastabel/lang/Quantifier.java b/src/hastabel/lang/Quantifier.java
index 5f059ae..ef77b28 100644
--- a/src/hastabel/lang/Quantifier.java
+++ b/src/hastabel/lang/Quantifier.java
@@ -15,6 +15,14 @@ public class Quantifier extends Formula
final boolean is_forall
)
{
+ if (parent == null)
+ {
+ System.out.println("Ooops f:" + formula.toString() + ", forall:" + is_forall);
+ }
+ if (formula == null)
+ {
+ System.out.println("p:" + parent.toString() + ", forall:" + is_forall);
+ }
this.parent = parent;
this.formula = formula;
this.is_forall = is_forall;