diff --git a/LICENSE b/LICENSE
index 261eeb9e..842f78c7 100644
--- a/LICENSE
+++ b/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
diff --git a/pom.xml b/pom.xml
index f8d2cc28..5e6b45c2 100644
--- a/pom.xml
+++ b/pom.xml
@@ -77,6 +77,7 @@ License.
7.8.2
+ 1.3.919.01.3
@@ -115,6 +116,11 @@ License.
+
+ com.google.code.findbugs
+ jsr305
+ ${findbugs.version}
+ com.google.guavaguava
diff --git a/src/main/java/net/hydromatic/sml/util/MartelliUnifier.java b/src/main/java/net/hydromatic/sml/util/MartelliUnifier.java
new file mode 100644
index 00000000..d539e0c2
--- /dev/null
+++ b/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 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 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 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 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 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 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 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
diff --git a/src/main/java/net/hydromatic/sml/util/RobinsonUnifier.java b/src/main/java/net/hydromatic/sml/util/RobinsonUnifier.java
new file mode 100644
index 00000000..5a2f53db
--- /dev/null
+++ b/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 compose(Map s1,
+ Map s2) {
+ Map composed = new HashMap<>(s1);
+ for (Map.Entry 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 joined = new HashMap<>();
+ joined.putAll(subs1.resultMap);
+ joined.putAll(subs2.resultMap);
+ return new Substitution(joined);
+ }
+ }
+ return null;
+ }
+
+ private static List skip(List list) {
+ return list.subList(1, list.size());
+ }
+
+ public @Nullable Substitution unify(List 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
diff --git a/src/main/java/net/hydromatic/sml/util/Unifier.java b/src/main/java/net/hydromatic/sml/util/Unifier.java
new file mode 100644
index 00000000..7b091073
--- /dev/null
+++ b/src/main/java/net/hydromatic/sml/util/Unifier.java
@@ -0,0 +1,352 @@
+/*
+ * 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.base.Preconditions;
+import com.google.common.collect.ImmutableList;
+import com.google.common.collect.ImmutableMap;
+import com.google.common.collect.ImmutableSortedMap;
+import com.google.common.collect.Ordering;
+
+import java.util.HashMap;
+import java.util.IdentityHashMap;
+import java.util.List;
+import java.util.Locale;
+import java.util.Map;
+import java.util.Objects;
+import javax.annotation.Nullable;
+
+/** Given pairs of terms, finds a substitution to minimize those pairs of
+ * terms. */
+public abstract class Unifier {
+ static final Substitution EMPTY = new Substitution(ImmutableMap.of());
+
+ private int varId;
+ private final Map variableMap = new HashMap<>();
+ private final Map atomMap = new HashMap<>();
+ private final Map sequenceMap = new HashMap<>();
+
+ /** Whether this unifier checks for cycles in substitutions. */
+ public boolean occurs() {
+ return false;
+ }
+
+ /** Creates a sequence, or returns an existing one with the same terms. */
+ public Sequence apply(String first, Term... args) {
+ final Sequence sequence =
+ new Sequence(ImmutableList.builder().add(atom(first))
+ .add(args).build());
+ return sequenceMap.computeIfAbsent(sequence.toString(), n -> sequence);
+ }
+
+ /** Creates a variable, or returns an existing one with the same name. */
+ public Variable variable(String name) {
+ return variableMap.computeIfAbsent(name, Variable::new);
+ }
+
+ /** Creates a new variable, with a new name. */
+ public Variable variable() {
+ for (;;) {
+ final String name = "T" + varId++;
+ if (!variableMap.containsKey(name)) {
+ final Variable variable = new Variable(name);
+ variableMap.put(name, variable);
+ return variable;
+ }
+ }
+ }
+
+ /** Creates an atom, or returns an existing one with the same name. */
+ public Atom atom(String name) {
+ return atomMap.computeIfAbsent(name, Atom::new);
+ }
+
+ /** Creates a substitution.
+ *
+ *
The arguments are alternating variable / term pairs. For example,
+ * {@code substitution(a, x, b, y)} becomes [a/X, b/Y]. */
+ public Substitution substitution(Term... varTerms) {
+ final ImmutableMap.Builder mapBuilder =
+ ImmutableMap.builder();
+ if (varTerms.length % 2 != 0) {
+ throw new AssertionError();
+ }
+ for (int i = 0; i < varTerms.length; i += 2) {
+ mapBuilder.put((Variable) varTerms[i + 1], varTerms[i]);
+ }
+ return new Substitution(mapBuilder.build());
+ }
+
+ static Sequence sequenceApply(Map substitutions,
+ Iterable terms) {
+ final ImmutableList.Builder newTerms = ImmutableList.builder();
+ for (Term term : terms) {
+ newTerms.add(term.apply(substitutions));
+ }
+ return new Sequence(newTerms.build());
+ }
+
+ public @Nullable abstract Substitution unify(List termPairs);
+
+ private static void checkCycles(Map map,
+ Map active) throws CycleException {
+ for (Term term : map.values()) {
+ term.checkCycle(map, active);
+ }
+ }
+
+ /** The results of a successful unification. Gives access to the raw variable
+ * mapping that resulted from the algorithm, but can also resolve a variable
+ * to the fullest extent possible with the {@link #resolve} method. */
+ public static final class Substitution {
+ /** The result of the unification algorithm proper. This does not have
+ * everything completely resolved: some variable substitutions are required
+ * before getting the most atom-y representation. */
+ final Map resultMap;
+
+ Substitution(Map resultMap) {
+ this.resultMap =
+ ImmutableSortedMap.copyOf(resultMap, Ordering.usingToString());
+ }
+
+ @Override public int hashCode() {
+ return resultMap.hashCode();
+ }
+
+ @Override public boolean equals(Object obj) {
+ return this == obj
+ || obj instanceof Substitution
+ && resultMap.equals(((Substitution) obj).resultMap);
+ }
+
+ @Override public String toString() {
+ final StringBuilder builder = new StringBuilder("[");
+ for (Ord> e : Ord.zip(resultMap.entrySet())) {
+ if (e.i > 0) {
+ builder.append(", ");
+ }
+ builder.append(e.e.getValue()).append("/").append(e.e.getKey());
+ }
+ return builder.append("]").toString();
+ }
+
+ Term resolve(Term term) {
+ Term previous;
+ Term current = term;
+ do {
+ previous = current;
+ current = current.apply(resultMap);
+ } while (!current.equals(previous));
+ return current;
+ }
+
+ private boolean hasCycles(Map map) {
+ try {
+ checkCycles(map, new IdentityHashMap<>());
+ return false;
+ } catch (CycleException e) {
+ return true;
+ }
+ }
+
+ public Substitution resolve() {
+ if (hasCycles(resultMap)) {
+ return this;
+ }
+ final ImmutableMap.Builder builder =
+ ImmutableMap.builder();
+ for (Map.Entry entry : resultMap.entrySet()) {
+ builder.put(entry.getKey(), resolve(entry.getValue()));
+ }
+ return new Substitution(builder.build());
+ }
+ }
+
+ /** Term (variable, symbol or node). */
+ public interface Term {
+ Term apply(Map substitutions);
+
+ boolean contains(Variable variable);
+
+ /** Throws CycleException if expanding this term leads to a cycle. */
+ void checkCycle(Map map, Map active)
+ throws CycleException;
+ }
+
+ /** Control flow exception, thrown by {@link Term#checkCycle(Map, Map)} if
+ * it finds a cycle in a substitution map. */
+ private static class CycleException extends Exception {
+ }
+
+ /** A symbol that has no children. */
+ public static final class Atom implements Term {
+ final String name;
+ Atom(String name) {
+ this.name = Objects.requireNonNull(name);
+ }
+
+ @Override public String toString() {
+ return name;
+ }
+
+ public Term apply(Map substitutions) {
+ return this;
+ }
+
+ public boolean contains(Variable variable) {
+ return false;
+ }
+
+ public void checkCycle(Map map,
+ Map active) {
+ // cycle not possible
+ }
+ }
+
+ /** A variable that represents a symbol or a sequence; unification's
+ * task is to find the substitutions for such variables. */
+ public static final class Variable implements Term {
+ final String name;
+ Variable(String name) {
+ this.name = Objects.requireNonNull(name);
+ Preconditions.checkArgument(!name.equals(name.toLowerCase(Locale.ROOT)));
+ }
+
+ @Override public String toString() {
+ return name;
+ }
+
+ public Term apply(Map substitutions) {
+ return substitutions.getOrDefault(this, this);
+ }
+
+ public boolean contains(Variable variable) {
+ return variable == this;
+ }
+
+ public void checkCycle(Map map,
+ Map active) throws CycleException {
+ final Term term = map.get(this);
+ if (term != null) {
+ if (active.put(this, this) != null) {
+ throw new CycleException();
+ }
+ term.checkCycle(map, active);
+ active.remove(this);
+ }
+ }
+ }
+
+ /** A pair of terms. */
+ public static final class TermTerm {
+ final Term left;
+ final Term right;
+
+ public TermTerm(Term left, Term right) {
+ this.left = Objects.requireNonNull(left);
+ this.right = Objects.requireNonNull(right);
+ }
+
+ @Override public String toString() {
+ return left + " = " + right;
+ }
+ }
+
+ /** A sequence of terms.
+ *
+ *
A sequence [a b c] is often printed "a(b, c)", as if "a" is the type of
+ * node and "b" and "c" are its children. */
+ public static final class Sequence implements Term {
+ final List terms;
+
+ Sequence(List terms) {
+ this.terms = ImmutableList.copyOf(terms);
+ }
+
+ @Override public int hashCode() {
+ return terms.hashCode();
+ }
+
+ @Override public boolean equals(Object obj) {
+ return this == obj
+ || obj instanceof Sequence
+ && terms.equals(((Sequence) obj).terms);
+ }
+
+ @Override public String toString() {
+ if (terms.size() == 1) {
+ return terms.get(0).toString();
+ }
+ final StringBuilder builder = new StringBuilder();
+ for (int i = 0; i < terms.size(); i++) {
+ Term term = terms.get(i);
+ builder.append(term);
+ builder.append(i == 0 ? "("
+ : i == terms.size() - 1 ? ")"
+ : ", ");
+ }
+ return builder.toString();
+ }
+
+ public Term apply(Map substitutions) {
+ final Sequence sequence = sequenceApply(substitutions, terms);
+ if (sequence.equalsShallow(this)) {
+ return this;
+ }
+ return sequence;
+ }
+
+ public void checkCycle(Map map,
+ Map active) throws CycleException {
+ for (Term term : terms) {
+ term.checkCycle(map, active);
+ }
+ }
+
+ /** Compares whether two sequences have the same terms.
+ * Compares addresses, not contents, to avoid hitting cycles
+ * if any of the terms are cyclic (e.g. "X = f(X)"). */
+ private boolean equalsShallow(Sequence sequence) {
+ return this == sequence || listEqual(terms, sequence.terms);
+ }
+
+ private static boolean listEqual(List list0, List list1) {
+ if (list0.size() != list1.size()) {
+ return false;
+ }
+ for (int i = 0; i < list0.size(); i++) {
+ if (list0.get(i) != list1.get(i)) {
+ return false;
+ }
+ }
+ return true;
+ }
+
+ public boolean contains(Variable variable) {
+ for (Term term : terms) {
+ if (term.contains(variable)) {
+ return true;
+ }
+ }
+ return false;
+ }
+ }
+}
+
+// End Unifier.java
diff --git a/src/test/java/net/hydromatic/sml/MainTest.java b/src/test/java/net/hydromatic/sml/MainTest.java
index 609eb369..119922bc 100644
--- a/src/test/java/net/hydromatic/sml/MainTest.java
+++ b/src/test/java/net/hydromatic/sml/MainTest.java
@@ -30,6 +30,7 @@
import org.hamcrest.Description;
import org.hamcrest.Matcher;
import org.hamcrest.TypeSafeMatcher;
+import org.junit.Ignore;
import org.junit.Test;
import java.io.ByteArrayInputStream;
@@ -47,6 +48,110 @@
* Kick the tires.
*/
public class MainTest {
+ private void withParser(String ml, Consumer action) {
+ final SmlParserImpl parser = new SmlParserImpl(new StringReader(ml));
+ action.accept(parser);
+ }
+
+ private void checkParseLiteral(String ml, Matcher matcher) {
+ withParser(ml, parser -> {
+ try {
+ final Ast.Literal literal = parser.literal();
+ assertThat(literal, matcher);
+ } catch (ParseException e) {
+ throw new RuntimeException(e);
+ }
+ });
+ }
+
+ private void checkParseDecl(String ml, Matcher matcher) {
+ withParser(ml, parser -> {
+ try {
+ final Ast.VarDecl varDecl = parser.varDecl();
+ assertThat(varDecl, matcher);
+ } catch (ParseException e) {
+ throw new RuntimeException(e);
+ }
+ });
+ }
+
+ private void checkStmt(String ml, Matcher matcher) {
+ try {
+ final AstNode statement =
+ new SmlParserImpl(new StringReader(ml)).statement();
+ assertThat(statement, matcher);
+ } catch (ParseException e) {
+ throw new RuntimeException(e);
+ }
+ }
+
+ /** Checks that an expression can be parsed and returns the identical
+ * expression when unparsed. */
+ private void assertParseSame(String ml) {
+ checkStmt(ml, isAst(AstNode.class, ml));
+ }
+
+ /** Matches a literal by value. */
+ private static Matcher isLiteral(Comparable comparable) {
+ return new TypeSafeMatcher() {
+ protected boolean matchesSafely(Ast.Literal literal) {
+ return literal.value.equals(comparable);
+ }
+
+ public void describeTo(Description description) {
+ description.appendText("literal with value " + comparable);
+ }
+ };
+ }
+
+ /** Matches an AST node by its string representation. */
+ private static Matcher isAst(Class clazz,
+ String expected) {
+ return new TypeSafeMatcher() {
+ protected boolean matchesSafely(T t) {
+ assertThat(clazz.isInstance(t), is(true));
+ return Ast.toString(t).equals(expected);
+ }
+
+ public void describeTo(Description description) {
+ description.appendText("ast with value " + expected);
+ }
+ };
+ }
+
+ private void withPrepare(String ml,
+ Consumer action) {
+ withParser(ml, parser -> {
+ try {
+ final AstNode statement = parser.statement();
+ final Environment env = Environments.empty();
+ final Compiler.CompiledStatement compiled =
+ new Compiler().compileStatement(env, statement);
+ action.accept(compiled);
+ } catch (ParseException e) {
+ throw new RuntimeException(e);
+ }
+ });
+ }
+
+ private void assertType(String ml, Matcher matcher) {
+ withPrepare(ml, compiledStatement ->
+ assertThat(compiledStatement.getType().description(), matcher));
+ }
+
+ private void checkEval(String ml, Matcher