| summaryrefslogtreecommitdiff |
diff options
| -rw-r--r-- | src/hastabel/LangLexer.g4 | 3 | ||||
| -rw-r--r-- | src/hastabel/LangParser.g4 | 25 | ||||
| -rw-r--r-- | src/hastabel/Predicates.java | 14 | ||||
| -rw-r--r-- | src/hastabel/PropertyParser.g4 | 17 | ||||
| -rw-r--r-- | src/hastabel/lang/OperatorFormula.java | 10 | ||||
| -rw-r--r-- | src/hastabel/lang/Predicate.java | 100 | ||||
| -rw-r--r-- | src/hastabel/lang/Quantifier.java | 8 |
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; |