Unifier

The unifier will be the basis of the type-resolution algorithm.

We have two unifiers:
 * A simple unifier that implements Robinson's unification algorithm,
   and is based upon code in https://github.com/google/CallBuilder.
 * And a superior unifier that implements the unification algorithm
   discovered by Martelli, Montanari (1976) and Paterson, Wegman (1978).

Tests are based on documentation for
https://github.com/HeshamAlassaf/UnificationAlgorithmJava.

We deal with cycles in the substitution maps produced by unification.

LICENSE

@@ -199,3 +199,15 @@
    WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
    See the License for the specific language governing permissions and
    limitations under the License.
+
+
+-------
+Unifier is based upon code in https://github.com/google/CallBuilder.
+
+Copyright (C) 2015 Google, Inc.
+
+-------
+UnifierTest is based upon the comments in
+https://github.com/HeshamAlassaf/UnificationAlgorithmJava
+
+Copyright (C) 2017 Hesham Alassaf

pom.xml

@@ -77,6 +77,7 @@ License.
 
     <!-- Component and plugin versions, in alphabetical order. -->
     <checkstyle.version>7.8.2</checkstyle.version>
+    <findbugs.version>1.3.9</findbugs.version>
     <!-- We support guava versions 19.0 to 27.0.1-jre. -->
     <guava.version>19.0</guava.version>
     <hamcrest.version>1.3</hamcrest.version>
@@ -115,6 +116,11 @@ License.
   </scm>
 
   <dependencies>
+    <dependency>
+      <groupId>com.google.code.findbugs</groupId>
+      <artifactId>jsr305</artifactId>
+      <version>${findbugs.version}</version>
+    </dependency>
     <dependency>
       <groupId>com.google.guava</groupId>
       <artifactId>guava</artifactId>

src/main/java/net/hydromatic/sml/util/MartelliUnifier.java

@@ -0,0 +1,160 @@
+/*
+ * Licensed to Julian Hyde under one or more contributor license
+ * agreements.  See the NOTICE file distributed with this work
+ * for additional information regarding copyright ownership.
+ * Julian Hyde licenses this file to you under the Apache
+ * License, Version 2.0 (the "License"); you may not use this
+ * file except in compliance with the License.  You may obtain a
+ * copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing,
+ * software distributed under the License is distributed on an
+ * "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND,
+ * either express or implied.  See the License for the specific
+ * language governing permissions and limitations under the
+ * License.
+ */
+package net.hydromatic.sml.util;
+
+import com.google.common.collect.ImmutableMap;
+
+import java.util.ArrayList;
+import java.util.LinkedHashMap;
+import java.util.List;
+import java.util.Map;
+import javax.annotation.Nullable;
+
+/** Unification algorithm due to Martelli, Montanari (1976) and
+ * Paterson, Wegman (1978). */
+public class MartelliUnifier extends Unifier {
+  public @Nullable Substitution unify(List<TermTerm> termPairs) {
+
+    // delete: G u { t = t }
+    //   => G
+
+    // decompose: G u { f(s0, ..., sk) = f(t0, ..., tk) }
+    //   => G u {s0 = t0, ..., sk = tk}
+
+    // conflict: G u { f(s0, ..., sk) = g(t0, ..., tm) }
+    //   => fail
+    // if f <> g or k <> m
+
+    // swap: G u { f(s0, ..., sk) = x }
+    //  => G u { x = f(s0, ..., sk) }
+
+    // eliminate: G u { x = t }
+    //  => G { x |-> t } u { x = t }
+    // if x not in vars(t) and x in vars(G)
+
+    // check: G u { x = f(s0, ..., sk)}
+    //  => fail
+    // if x in vars(f(s0, ..., sk))
+
+    termPairs = new ArrayList<>(termPairs);
+    final Map<Variable, Term> result = new LinkedHashMap<>();
+    for (;;) {
+      if (termPairs.isEmpty()) {
+        return new Substitution(result);
+      }
+      int i = findDelete(termPairs);
+      if (i >= 0) {
+        termPairs.remove(i); // delete
+        continue;
+      }
+
+      i = findSeqSeq(termPairs);
+      if (i >= 0) {
+        final TermTerm pair = termPairs.get(i);
+        final Sequence left = (Sequence) pair.left;
+        final Sequence right = (Sequence) pair.right;
+
+        if (left.terms.get(0) != right.terms.get(0)
+            || left.terms.size() != right.terms.size()) {
+          return null; // conflict
+        }
+        termPairs.remove(i); // decompose
+        for (int j = 1; j < left.terms.size(); j++) {
+          termPairs.add(new TermTerm(left.terms.get(j), right.terms.get(j)));
+        }
+        continue;
+      }
+
+      i = findNonVarVar(termPairs);
+      if (i >= 0) {
+        final TermTerm pair = termPairs.get(i);
+        termPairs.set(i, new TermTerm(pair.right, pair.left));
+        continue; // swap
+      }
+
+      i = findVarAny(termPairs);
+      if (i >= 0) {
+        final TermTerm pair = termPairs.remove(i);
+        final Variable variable = (Variable) pair.left;
+        final Term term = pair.right;
+        if (term.contains(variable)) {
+          return null; // check
+        }
+        final Map<Variable, Term> map = ImmutableMap.of(variable, term);
+        result.put(variable, term);
+        for (int j = 0; j < termPairs.size(); j++) {
+          if (j != i) {
+            final TermTerm pair2 = termPairs.get(j);
+            final Term left2 = pair2.left.apply(map);
+            final Term right2 = pair2.right.apply(map);
+            if (left2 != pair2.left
+                || right2 != pair2.right) {
+              termPairs.set(j, new TermTerm(left2, right2));
+            }
+          }
+        }
+      }
+    }
+  }
+
+  private int findDelete(List<TermTerm> termPairs) {
+    for (int i = 0; i < termPairs.size(); i++) {
+      TermTerm termTerm = termPairs.get(i);
+      if (termTerm.left.equals(termTerm.right)) {
+        return i;
+      }
+    }
+    return -1;
+  }
+
+  private int findSeqSeq(List<TermTerm> termPairs) {
+    for (int i = 0; i < termPairs.size(); i++) {
+      TermTerm termTerm = termPairs.get(i);
+      if (termTerm.left instanceof Sequence
+          && termTerm.right instanceof Sequence) {
+        return i;
+      }
+    }
+    return -1;
+  }
+
+  private int findNonVarVar(List<TermTerm> termPairs) {
+    for (int i = 0; i < termPairs.size(); i++) {
+      TermTerm termTerm = termPairs.get(i);
+      if (!(termTerm.left instanceof Variable)
+          && termTerm.right instanceof Variable) {
+        return i;
+      }
+    }
+    return -1;
+  }
+
+  private int findVarAny(List<TermTerm> termPairs) {
+    for (int i = 0; i < termPairs.size(); i++) {
+      TermTerm termTerm = termPairs.get(i);
+      if (termTerm.left instanceof Variable) {
+        return i;
+      }
+    }
+    return -1;
+  }
+
+}
+
+// End MartelliUnifier.java

src/main/java/net/hydromatic/sml/util/RobinsonUnifier.java

@@ -0,0 +1,99 @@
+/*
+ * Licensed to Julian Hyde under one or more contributor license
+ * agreements.  See the NOTICE file distributed with this work
+ * for additional information regarding copyright ownership.
+ * Julian Hyde licenses this file to you under the Apache
+ * License, Version 2.0 (the "License"); you may not use this
+ * file except in compliance with the License.  You may obtain a
+ * copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing,
+ * software distributed under the License is distributed on an
+ * "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND,
+ * either express or implied.  See the License for the specific
+ * language governing permissions and limitations under the
+ * License.
+ */
+package net.hydromatic.sml.util;
+
+import com.google.common.collect.ImmutableMap;
+
+import java.util.HashMap;
+import java.util.List;
+import java.util.Map;
+import javax.annotation.Nullable;
+
+/** Robinson's unification algorithm. */
+public class RobinsonUnifier extends Unifier {
+  /**
+   * Applies s1 to the elements of s2 and adds them into a single list.
+   */
+  static Map<Variable, Term> compose(Map<Variable, Term> s1,
+      Map<Variable, Term> s2) {
+    Map<Variable, Term> composed = new HashMap<>(s1);
+    for (Map.Entry<Variable, Term> entry2 : s2.entrySet()) {
+      composed.put(entry2.getKey(), entry2.getValue().apply(s1));
+    }
+    return composed;
+  }
+
+  private @Nullable Substitution sequenceUnify(Sequence lhs,
+      Sequence rhs) {
+    if (lhs.terms.size() != rhs.terms.size()) {
+      return null;
+    }
+    if (lhs.terms.isEmpty()) {
+      return EMPTY;
+    }
+    Term firstLhs = lhs.terms.get(0);
+    Term firstRhs = rhs.terms.get(0);
+    Substitution subs1 = unify(firstLhs, firstRhs);
+    if (subs1 != null) {
+      Sequence restLhs = sequenceApply(subs1.resultMap, skip(lhs.terms));
+      Sequence restRhs = sequenceApply(subs1.resultMap, skip(rhs.terms));
+      Substitution subs2 = sequenceUnify(restLhs, restRhs);
+      if (subs2 != null) {
+        Map<Variable, Term> joined = new HashMap<>();
+        joined.putAll(subs1.resultMap);
+        joined.putAll(subs2.resultMap);
+        return new Substitution(joined);
+      }
+    }
+    return null;
+  }
+
+  private static <E> List<E> skip(List<E> list) {
+    return list.subList(1, list.size());
+  }
+
+  public @Nullable Substitution unify(List<TermTerm> termPairs) {
+    switch (termPairs.size()) {
+    case 1:
+      return unify(termPairs.get(0).left, termPairs.get(0).right);
+    default:
+      throw new AssertionError();
+    }
+  }
+
+
+  public @Nullable Substitution unify(Term lhs, Term rhs) {
+    if (lhs instanceof Variable) {
+      return new Substitution(ImmutableMap.of((Variable) lhs, rhs));
+    }
+    if (rhs instanceof Variable) {
+      return new Substitution(ImmutableMap.of((Variable) rhs, lhs));
+    }
+    if (lhs instanceof Atom && rhs instanceof Atom) {
+      return lhs == rhs ? EMPTY : null;
+    }
+    if (lhs instanceof Sequence && rhs instanceof Sequence) {
+      return sequenceUnify((Sequence) lhs, (Sequence) rhs);
+    }
+    return null;
+  }
+
+}
+
+// End RobinsonUnifier.java