generate axioms for overloaded productions
@@ -8,6 +8,10 @@ import com.google.common.collect.SetMultimap;
import com.google.common.collect.Sets;
import edu.uci.ics.jung.graph.DirectedGraph;
import edu.uci.ics.jung.graph.DirectedSparseGraph;
+import org.kframework.Collections;
+import org.kframework.Collections;
+import org.kframework.Collections;
+import org.kframework.Collections;
import org.kframework.attributes.Att;
import org.kframework.builtin.BooleanUtils;
import org.kframework.builtin.KLabels;
@@ -465,6 +469,51 @@ public class ModuleToKORE {
}
sb.append("\n");
}
+ for (Production lesser : iterable(module.overloads().elements())) {
+ for (Production greater : iterable(module.overloads().relations().get(lesser).getOrElse(() -> Collections.<Production>Set()))) {
+ sb.append(" axiom{R} \\equals{");
+ convert(greater.sort(), greater);
+ sb.append(", R} (");
+ convert(greater.klabel().get(), greater);
+ sb.append("(");
+ String conn = "";
+ for (int i = 0; i < greater.nonterminals().size(); i++) {
+ sb.append(conn);
+ if (greater.nonterminal(i).sort().equals(lesser.nonterminal(i).sort())) {
+ sb.append("K").append(i).append(":");
+ convert(greater.nonterminal(i).sort(), greater);
+ } else {
+ sb.append("inj{");
+ convert(lesser.nonterminal(i).sort(), lesser);
+ sb.append(", ");
+ convert(greater.nonterminal(i).sort(), greater);
+ sb.append("} (K").append(i).append(":");
+ convert(lesser.nonterminal(i).sort(), lesser);
+ sb.append(")");
+ }
+ conn = ",";
+ }
+ sb.append("), inj{");
+ convert(lesser.sort(), lesser);
+ sb.append(", ");
+ convert(greater.sort(), greater);
+ sb.append("} (");
+ convert(lesser.klabel().get(), lesser);
+ sb.append("(");
+ conn = "";
+ for (int i = 0; i < lesser.nonterminals().size(); i++) {
+ sb.append(conn);
+ sb.append("K").append(i).append(":");
+ convert(lesser.nonterminal(i).sort(), lesser);
+ conn = ",";
+ }
+ sb.append("))) [overload{}(");
+ convert(greater.klabel().get(), greater);
+ sb.append("(), ");
+ convert(lesser.klabel().get(), lesser);
+ sb.append("())] // overloaded production\n");
+ }
+ }
sb.append("\n// rules\n");
for (Rule rule : iterable(module.rules())) {
boolean equation = false;
