CHANGELOG.md

@@ -3,6 +3,7 @@
 ## 0.10
 
 * Bugfix: reparir equals-hashCode contract in `Abstraction`
+* More tree prunning
 
 ## 0.9
 

src/main/java/pl/wojciechkarpiel/jhou/termHead/BetaEtaNormalizer.java

@@ -5,6 +5,7 @@ import pl.wojciechkarpiel.jhou.ast.type.Type;
 import pl.wojciechkarpiel.jhou.ast.util.Visitor;
 import pl.wojciechkarpiel.jhou.normalizer.Normalizer;
 import pl.wojciechkarpiel.jhou.types.TypeCalculator;
+import pl.wojciechkarpiel.jhou.util.ListUtil;
 
 import java.util.ArrayList;
 import java.util.Collections;
@@ -13,7 +14,7 @@ import java.util.List;
 class BetaEtaNormalizer {
 
     static BetaEtaNormal normalize(Term term) {
-        return BetaEtaNormalizer.normalize(term, new ArrayList<Variable>());
+        return BetaEtaNormalizer.normalize(term, ListUtil.of());
     }
 
 

src/main/java/pl/wojciechkarpiel/jhou/termHead/Head.java

@@ -59,7 +59,7 @@ public interface Head {
             this.c = c;
         }
 
-        public Constant getC() {
+        public Constant getConstant() {
             return c;
         }
 

src/main/java/pl/wojciechkarpiel/jhou/types/inference/TypeInference.java

@@ -18,6 +18,7 @@ import pl.wojciechkarpiel.jhou.unifier.tree.WorkWorkNode;
 import pl.wojciechkarpiel.jhou.util.DevNullPrintStream;
 import pl.wojciechkarpiel.jhou.util.ListUtil;
 import pl.wojciechkarpiel.jhou.util.MapUtil;
+import pl.wojciechkarpiel.jhou.util.Pair;
 
 import java.io.PrintStream;
 import java.util.*;
@@ -42,6 +43,12 @@ public class TypeInference {
         return inferMissing(termsOfSameType, allowedTypeInference, System.out);
     }
 
+    public static Pair<Term, Term> inferMissing(Pair<Term, Term> termsOfEqualType, AllowedTypeInference allowedTypeInference, PrintStream printStream) {
+        List<Term> inputList = ListUtil.of(termsOfEqualType.getLeft(), termsOfEqualType.getRight());
+        List<Term> outputList = inferMissingInternal(inputList, allowedTypeInference, printStream);
+        return Pair.of(outputList.get(0), outputList.get(1));
+    }
+
     public static List<Term> inferMissing(List<Term> termsOfEqualType, AllowedTypeInference allowedTypeInference, PrintStream printStream) {
         return inferMissingInternal(termsOfEqualType, allowedTypeInference, printStream);
     }
@@ -77,7 +84,7 @@ public class TypeInference {
 
         DisagreementSet disagreementSet = new DisagreementSet(ds);
 
-        Tree tree = new WorkWorkNode(null, Substitution.empty(), disagreementSet, true);
+        Tree tree = WorkWorkNode.firstOrderTree(disagreementSet);
         SolutionIterator s = new SolutionIterator(tree, DevNullPrintStream.INSTANCE);
         Substitution nxt = s.next();
         return termsOfEqualType.stream().map(term -> l3l.recreateWithTypes(term, nxt)).collect(Collectors.toList());

src/main/java/pl/wojciechkarpiel/jhou/unifier/Unifier.java

@@ -1,14 +1,11 @@
 package pl.wojciechkarpiel.jhou.unifier;
 
 import pl.wojciechkarpiel.jhou.ast.Term;
-import pl.wojciechkarpiel.jhou.substitution.Substitution;
 import pl.wojciechkarpiel.jhou.types.TypeCalculator;
 import pl.wojciechkarpiel.jhou.types.inference.TypeInference;
 import pl.wojciechkarpiel.jhou.unifier.tree.Tree;
 import pl.wojciechkarpiel.jhou.unifier.tree.WorkWorkNode;
-import pl.wojciechkarpiel.jhou.util.ListUtil;
-
-import java.util.List;
+import pl.wojciechkarpiel.jhou.util.Pair;
 
 public class Unifier {
     private Unifier() {
@@ -19,16 +16,13 @@ public class Unifier {
     }
 
     public static SolutionIterator unify(Term a, Term b, UnificationSettings unificationSettings) {
-        List<Term> ab = TypeInference.inferMissing(
-                ListUtil.of(a, b),
+        Pair<Term, Term> ab = TypeInference.inferMissing(
+                Pair.of(a, b),
                 unificationSettings.getAllowedTypeInference(),
                 unificationSettings.getPrintStream()
         );
-        a = ab.get(0);
-        b = ab.get(1);
-        TypeCalculator.ensureEqualTypes(a, b);
-        DisagreementSet disagreementSet = DisagreementSet.of(new DisagreementPair(a, b));
-        Tree tree = new WorkWorkNode(null, Substitution.empty(), disagreementSet);
+        TypeCalculator.ensureEqualTypes(ab.getLeft(), ab.getRight());
+        Tree tree = WorkWorkNode.searchTreeRoot(ab.getLeft(), ab.getRight());
         return new SolutionIterator(tree, unificationSettings.getMaxIterations(), unificationSettings.getPrintStream());
     }
 }

src/main/java/pl/wojciechkarpiel/jhou/unifier/tree/NagmiNode.java

@@ -27,11 +27,10 @@ public class NagmiNode implements Tree {
 
     @Override
     public void expandOnce() {
-
     }
 
     @Override
     public Substitution inheritedSubstitution() {
-        return null;
+        throw new UnsupportedOperationException();
     }
 }

src/main/java/pl/wojciechkarpiel/jhou/unifier/tree/WeBackNode.java

@@ -19,10 +19,6 @@ public class WeBackNode implements Tree {
         this.usedUp = false;
     }
 
-    public Substitution getSubstitution() {
-        return substitution;
-    }
-
     public Tree getParent() {
         return parent;
     }

src/main/java/pl/wojciechkarpiel/jhou/unifier/tree/WorkWorkNode.java

@@ -3,7 +3,6 @@ package pl.wojciechkarpiel.jhou.unifier.tree;
 import pl.wojciechkarpiel.jhou.ast.Equality;
 import pl.wojciechkarpiel.jhou.ast.Term;
 import pl.wojciechkarpiel.jhou.ast.Variable;
-import pl.wojciechkarpiel.jhou.normalizer.Normalizer;
 import pl.wojciechkarpiel.jhou.substitution.Substitution;
 import pl.wojciechkarpiel.jhou.substitution.SubstitutionPair;
 import pl.wojciechkarpiel.jhou.unifier.DisagreementPair;
@@ -17,21 +16,40 @@ import pl.wojciechkarpiel.jhou.util.Pair;
 
 import java.util.*;
 import java.util.stream.Collectors;
+import java.util.stream.Stream;
 
 public class WorkWorkNode implements Tree {
 
     private final Substitution fromParent;
     private final DisagreementSet disagreementSet;
-    private final boolean pretendYoureDoingFirstOrder;
+    private final boolean pretendYoureDoingFirstOrder; // hack
 
     private List<Tree> children;
     private final Tree parent;
 
-    public WorkWorkNode(Tree parent, Substitution fromParent, DisagreementSet disagreementSet) {
-        this(parent, fromParent, disagreementSet, false);
+    public static WorkWorkNode searchTreeRoot(Term a, Term b) {
+        return searchTreeRoot(new DisagreementSet(ListUtil.of(new DisagreementPair(a, b))));
     }
 
-    public WorkWorkNode(Tree parent, Substitution fromParent, DisagreementSet disagreementSet, boolean pretendYoureDoingFirstOrder) {
+    public static WorkWorkNode searchTreeRoot(DisagreementSet disagreementSet) {
+        return new WorkWorkNode(disagreementSet, false);
+    }
+
+    /**
+     * Hack for solving first-order problems faster. Will break if presented with a higher-order problem.
+     */
+    public static Tree firstOrderTree(DisagreementSet disagreementSet) {
+        return new WorkWorkNode(disagreementSet, true);
+    }
+
+    private WorkWorkNode(DisagreementSet disagreementSet, boolean pretendYoureDoingFirstOrder) {
+        this(null, Substitution.empty(), disagreementSet, pretendYoureDoingFirstOrder);
+    }
+
+    /**
+     * @param pretendYoureDoingFirstOrder total hack, don't use. TODO: write a separate 1st order unification class
+     */
+    private WorkWorkNode(Tree parent, Substitution fromParent, DisagreementSet disagreementSet, boolean pretendYoureDoingFirstOrder) {
         this.parent = parent;
         this.fromParent = fromParent;
         this.disagreementSet = disagreementSet;
@@ -46,9 +64,10 @@ public class WorkWorkNode implements Tree {
     public boolean itsOver() {
         if (children == null) return false;
         else {
+            pruneDirectChildren();
             boolean itsOver = children.stream().allMatch(Tree::itsOver);
             // prune the tree
-            if (itsOver) {
+            if (itsOver && !fatherOfSingleFailure()) {
                 children = ListUtil.of(new NagmiNode(this));
             }
             return itsOver;
@@ -58,6 +77,7 @@ public class WorkWorkNode implements Tree {
     @Override
     public Optional<WeBackNode> weBack() {
         if (children == null) return Optional.empty();
+        pruneDirectChildren();
         return children.stream()
                 .map(Tree::weBack)
                 .filter(Optional::isPresent)
@@ -68,15 +88,14 @@ public class WorkWorkNode implements Tree {
     @Override
     public void expandOnce() {
         if (children != null) {
+            pruneDirectChildren();
             children.forEach(Tree::expandOnce);
         } else {
             SimplificationResult simplify = Simplifier.simplify(disagreementSet);
-
-            WorkWorkNode thiz = this;
             children = simplify.visit(new SimplificationVisitor<List<Tree>>() {
                 @Override
                 public List<Tree> visitSuccess(SimplificationSuccess success) {
-                    return ListUtil.of(new WeBackNode(thiz, success.getSolution()));
+                    return ListUtil.of(new WeBackNode(WorkWorkNode.this, success.getSolution()));
                 }
 
                 @Override
@@ -86,7 +105,7 @@ public class WorkWorkNode implements Tree {
 
                 @Override
                 public List<Tree> visitFailure(NonUnifiable nonUnifiable) {
-                    return ListUtil.of(new NagmiNode(thiz));
+                    return ListUtil.of(new NagmiNode(WorkWorkNode.this));
                 }
             });
         }
@@ -99,55 +118,57 @@ public class WorkWorkNode implements Tree {
 
     private List<Tree> createChildNodes(DisagreementSet disagreement) {
         List<Tree> result = new ArrayList<>();
-        List<Substitution> flattenedSubstitutions = disagreement.getDisagreements().stream()
+        Stream<Substitution> flattenedSubstitutionStream = disagreement.getDisagreements().stream()
                 .filter(dp -> dp.getType() == PairType.RIGID_FLEXIBLE)
                 .flatMap(disagreementPair ->
                         Matcher.match(disagreementPair.getMostRigid(), disagreementPair.getLeastRigid())
-                                .intoSubstitutionStream())
-                .collect(Collectors.toList());
-        flattenedSubstitutions = deduplicateSort(flattenedSubstitutions);
+                                .intoSubstitutionStream());
+        List<Substitution> flattenedSubstitutions;
         if (pretendYoureDoingFirstOrder) { // hack to seed up first order search
             // this works because in 1st order search any found substitution must be a good one,
             // so we don't need to create multiple tree branches (effectively turning exponential into linear)
-            if (!flattenedSubstitutions.isEmpty()) flattenedSubstitutions = ListUtil.of(flattenedSubstitutions.get(0));
+            // but really, a much saner option would be to wire another class for 1st order unification, it's simple
+            flattenedSubstitutions = flattenedSubstitutionStream.findFirst().map(ListUtil::of).orElse(ListUtil.of());
+        } else {
+            flattenedSubstitutions = deduplicateSort(flattenedSubstitutionStream.collect(Collectors.toList()));
         }
         for (Substitution possibleSolution : flattenedSubstitutions) {
-            DisagreementSet newDs = new DisagreementSet(disagreement.getDisagreements().stream().map(disagreementPair ->
-                    new DisagreementPair(
-                            Normalizer.betaNormalize(possibleSolution.substitute(disagreementPair.getMostRigid().backToTerm())),
-                            Normalizer.betaNormalize(possibleSolution.substitute(disagreementPair.getLeastRigid().backToTerm()))
-                    )).collect(Collectors.toList()));
-
-            Tree tree = new WorkWorkNode(this, possibleSolution, newDs, pretendYoureDoingFirstOrder);
+            DisagreementSet newDisagreementSet = new DisagreementSet(disagreement.getDisagreements().stream()
+                    .map(disagreementPair ->
+                            new DisagreementPair(
+                                    possibleSolution.substitute(disagreementPair.getMostRigid().backToTerm()),
+                                    possibleSolution.substitute(disagreementPair.getLeastRigid().backToTerm())
+                            )).collect(Collectors.toList()));
+
+            Tree tree = new WorkWorkNode(this, possibleSolution, newDisagreementSet, pretendYoureDoingFirstOrder);
             result.add(tree);
         }
-
         return result;
     }
 
     /*
-     * optiomize flatsubs in a folllowing way:
+     * Optimization pass aimed at minimizing tree branching
      *
-     * 1. deduplicate subs, ie let all x,S(x) be different
-     * 2. Sort by count of sobstitutions for a var
+     * 1. Deduplicate substitutions, identifying alpha-equal ones
+     * 2. Sort by count of possible substitution for a given variable
      * 3. generate children only for the least used var (but keep the other disagreement pairs!)
      *
      * method assumes that all inputs are single-variable substitutions
      */
     private static List<Substitution> deduplicateSort(List<Substitution> input) {
         if (input.isEmpty()) return input;
-
         // List<Term> and not Set<Term> because of alpha-equality problem
         Map<Variable, List<Term>> dedupByVar = new HashMap<>(input.size());
-        for (Substitution pair_ : input) {
-            if (pair_.getSubstitution().size() > 1) throw new RuntimeException();
-            if (pair_.getSubstitution().isEmpty()) continue;
-            SubstitutionPair pair = pair_.getSubstitution().get(0);
-            List<Term> s_ = new ArrayList<>();
-            List<Term> s = dedupByVar.putIfAbsent(pair.getVariable(), s_);
-            if (s == null) s = s_;
+        for (Substitution substitution : input) {
+            if (substitution.getSubstitution().size() > 1) throw new RuntimeException();
+            if (substitution.getSubstitution().isEmpty()) continue;
+            SubstitutionPair pair = substitution.getSubstitution().get(0);
+            dedupByVar.putIfAbsent(pair.getVariable(), new ArrayList<>());
+            List<Term> termsForVar = dedupByVar.get(pair.getVariable());
             // could be Set.add if not for alpha equality (bruijn would fix the problem of hashcode-equals for alpha)
-            if (s.stream().noneMatch(t -> Equality.alphaEqual(t, pair.getTerm()))) s.add(pair.getTerm());
+            if (termsForVar.stream().noneMatch(t -> Equality.alphaEqual(t, pair.getTerm()))) {
+                termsForVar.add(pair.getTerm());
+            }
         }
         if (dedupByVar.isEmpty()) {
             return input;
@@ -157,26 +178,34 @@ public class WorkWorkNode implements Tree {
         int minCount = dedupByVar.values().stream().mapToInt(List::size).min().getAsInt();
         dedupByVar.entrySet().stream().filter(p -> p.getValue().size() == minCount)
                 .forEach(p -> least.add(Pair.of(p.getKey(), p.getValue())));
-
         least.sort(Comparator.comparingInt(o -> o.getLeft().getId().getId()));
-
         Pair<Variable, List<Term>> minSized = least.get(0);
         return minSized.getRight().stream()
                 // Sorting here doesn't help the algorithm, it's here to ensure deterministic outputs
+                // (technically it's not truly deterministic because of hashcode overlap, but it's good enough)
                 .sorted(Comparator.comparingInt(Term::hashCode))
-                .map(sbs -> new Substitution(minSized.getLeft(), sbs))
+                .map(term -> new Substitution(minSized.getLeft(), term))
                 .collect(Collectors.toList());
     }
-}
-
-
-
-
-
-
-
-
-
 
+    private void pruneDirectChildren() {
+        if (fatherOfSingleFailure()) return;
+        if (children.stream().anyMatch(WorkWorkNode::canBePruned)) {
+            children = children.stream().filter(c -> !WorkWorkNode.canBePruned(c)).collect(Collectors.toList());
+            if (children.isEmpty()) children = ListUtil.of(new NagmiNode(this));
+        }
+    }
 
+    /**
+     * Checks only direct children
+     */
+    private static boolean canBePruned(Tree child) {
+        if (child instanceof NagmiNode) return child.itsOver();
+        if (child instanceof WeBackNode) return child.itsOver();
+        return false;
+    }
 
+    private boolean fatherOfSingleFailure() {
+        return children.size() == 1 && children.get(0) instanceof NagmiNode;
+    }
+}

src/main/java/pl/wojciechkarpiel/jhou/util/DevNullPrintStream.java

@@ -1,6 +1,5 @@
 package pl.wojciechkarpiel.jhou.util;
 
-import java.io.IOException;
 import java.io.OutputStream;
 import java.io.PrintStream;
 
@@ -10,8 +9,28 @@ public class DevNullPrintStream extends PrintStream {
     private DevNullPrintStream() {
         super(new OutputStream() {
             @Override
-            public void write(int b) throws IOException {
+            public void write(int b) {
             }
         });
     }
+
+    @Override
+    public void println() {
+    }
+
+    @Override
+    public void println(String x) {
+    }
+
+    @Override
+    public void print(String x) {
+    }
+
+    @Override
+    public void println(Object o) {
+    }
+
+    @Override
+    public void print(Object o) {
+    }
 }