From dbe579c977373404b1e68734c68a9373d043857a Mon Sep 17 00:00:00 2001 From: Julian Hyde Date: Fri, 18 Jan 2019 11:03:31 -0800 Subject: [PATCH] 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 | 12 + pom.xml | 6 + .../hydromatic/sml/util/MartelliUnifier.java | 160 ++++++++ .../hydromatic/sml/util/RobinsonUnifier.java | 99 +++++ .../java/net/hydromatic/sml/util/Unifier.java | 352 ++++++++++++++++++ .../java/net/hydromatic/sml/MainTest.java | 212 ++++++----- .../java/net/hydromatic/sml/UnifierTest.java | 321 ++++++++++++++++ 7 files changed, 1062 insertions(+), 100 deletions(-) create mode 100644 src/main/java/net/hydromatic/sml/util/MartelliUnifier.java create mode 100644 src/main/java/net/hydromatic/sml/util/RobinsonUnifier.java create mode 100644 src/main/java/net/hydromatic/sml/util/Unifier.java create mode 100644 src/test/java/net/hydromatic/sml/UnifierTest.java 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.9 19.0 1.3 @@ -115,6 +116,11 @@ License. + + com.google.code.findbugs + jsr305 + ${findbugs.version} + com.google.guava guava 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 matcher) { + try { + final Ast.Exp expression = + new SmlParserImpl(new StringReader(ml)).expression(); + final Environment env = Environments.empty(); + final Code code = new Compiler().compile(env, expression); + final Object value = code.eval(env); + assertThat(value, matcher); + } catch (ParseException e) { + throw new RuntimeException(e); + } + } + @Test public void testEmptyRepl() { final String[] args = new String[0]; final ByteArrayOutputStream out = new ByteArrayOutputStream(); @@ -112,10 +217,6 @@ public class MainTest { assertParseSame("if true then 1 else if false then 2 else 3"); } - private void assertParseSame(String ml) { - checkStmt(ml, isAst(AstNode.class, ml)); - } - @Test public void testType() { assertType("1", is("int")); assertType("0e0", is("real")); @@ -128,10 +229,13 @@ private void assertParseSame(String ml) { assertType("if true then 1.0 else 2.0", is("real")); } - private void assertType(String ml, Matcher matcher) { - withPrepare(ml, compiledStatement -> { - assertThat(compiledStatement.getType().description(), matcher); - }); + @Ignore // enable this test when we have polymorphic type resolution + @Test public void testType2() { + // cannot be typed, since the parameter f is in a monomorphic position + assertType("fn f => (f true, f 0)", is("invalid")); + // f has been introduced in a let-expression and is therefore treated as + // polymorphic. + assertType("let val f = fn x => x in (f true, f 0) end", is("bool * int")); } @Test public void testEval() { @@ -195,98 +299,6 @@ private void assertType(String ml, Matcher matcher) { @Test public void testEvalFnCurried() { checkEval("(fn x => fn y => x + y) 2 3", is(5)); } - - 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); - } - } - - /** 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) { - return Ast.toString(t).equals(expected); - } - - public void describeTo(Description description) { - description.appendText("ast with value " + expected); - } - }; - } - - private void checkEval(String ml, Matcher matcher) { - try { - final Ast.Exp expression = - new SmlParserImpl(new StringReader(ml)).expression(); - final Environment env = Environments.empty(); - final Code code = new Compiler().compile(env, expression); - final Object value = code.eval(env); - assertThat(value, matcher); - } catch (ParseException e) { - throw new RuntimeException(e); - } - } - - 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); - } - }); - } } // End MainTest.java diff --git a/src/test/java/net/hydromatic/sml/UnifierTest.java b/src/test/java/net/hydromatic/sml/UnifierTest.java new file mode 100644 index 00000000..91a246da --- /dev/null +++ b/src/test/java/net/hydromatic/sml/UnifierTest.java @@ -0,0 +1,321 @@ +/* + * 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; + +import com.google.common.collect.ImmutableList; + +import net.hydromatic.sml.util.MartelliUnifier; +import net.hydromatic.sml.util.RobinsonUnifier; +import net.hydromatic.sml.util.Unifier; + +import org.hamcrest.Matcher; +import org.junit.Test; + +import java.util.Arrays; + +import static org.hamcrest.core.Is.is; +import static org.hamcrest.core.IsNull.notNullValue; +import static org.hamcrest.core.IsNull.nullValue; +import static org.junit.Assert.assertThat; + +/** Test for {@link RobinsonUnifier}. */ +public abstract class UnifierTest { + final Unifier unifier = createUnifier(); + + protected abstract Unifier createUnifier(); + + private Unifier.Sequence a(Unifier.Term... terms) { + return unifier.apply("a", terms); + } + + private Unifier.Sequence b(Unifier.Term... terms) { + return unifier.apply("b", terms); + } + + private Unifier.Sequence c(Unifier.Term... terms) { + return unifier.apply("c", terms); + } + + private Unifier.Sequence d(Unifier.Term... terms) { + return unifier.apply("d", terms); + } + + private Unifier.Sequence f(Unifier.Term... terms) { + return unifier.apply("f", terms); + } + + private Unifier.Sequence g(Unifier.Term... terms) { + return unifier.apply("g", terms); + } + + private Unifier.Sequence h(Unifier.Term... terms) { + return unifier.apply("h", terms); + } + + private Unifier.Sequence p(Unifier.Term... terms) { + return unifier.apply("p", terms); + } + + private Unifier.Sequence bill(Unifier.Term... terms) { + return unifier.apply("bill", terms); + } + + private Unifier.Sequence bob(Unifier.Term... terms) { + return unifier.apply("bob", terms); + } + + private Unifier.Sequence john(Unifier.Term... terms) { + return unifier.apply("john", terms); + } + + private Unifier.Sequence tom(Unifier.Term... terms) { + return unifier.apply("tom", terms); + } + + private Unifier.Sequence father(Unifier.Term... terms) { + return unifier.apply("father", terms); + } + + private Unifier.Sequence mother(Unifier.Term... terms) { + return unifier.apply("mother", terms); + } + + private Unifier.Sequence parents(Unifier.Term... terms) { + return unifier.apply("parents", terms); + } + + private Unifier.Sequence parent(Unifier.Term... terms) { + return unifier.apply("parent", terms); + } + + private Unifier.Sequence grandParent(Unifier.Term... terms) { + return unifier.apply("grandParent", terms); + } + + private Unifier.Sequence connected(Unifier.Term... terms) { + return unifier.apply("connected", terms); + } + + private Unifier.Sequence part(Unifier.Term... terms) { + return unifier.apply("part", terms); + } + + // Turn off checkstyle, because non-static fields are conventionally + // lower-case. + // CHECKSTYLE: IGNORE 4 + private final Unifier.Variable X = unifier.variable("X"); + private final Unifier.Variable Y = unifier.variable("Y"); + private final Unifier.Variable W = unifier.variable("W"); + private final Unifier.Variable Z = unifier.variable("Z"); + + void assertThatUnify(Unifier.Term e1, Unifier.Term e2, + Matcher matcher) { + final Unifier.Substitution unify = + unifier.unify(ImmutableList.of(new Unifier.TermTerm(e1, e2))); + assertThat(unify, notNullValue()); + assertThat(unify.resolve().toString(), matcher); + } + + void assertThatCannotUnify(Unifier.Term e1, Unifier.Term e2) { + assertThat(unifier.unify(ImmutableList.of(new Unifier.TermTerm(e1, e2))), + nullValue()); + } + + @Test public void test1() { + final Unifier.Term e1 = p(f(a()), g(b()), Y); + final Unifier.Term e2 = p(Z, g(d()), c()); + assertThat(e1.toString(), is("p(f(a), g(b), Y)")); + assertThat(unifier.substitution(f(a(), Y), Z).toString(), + is("[f(a, Y)/Z]")); + assertThatCannotUnify(e1, e2); + } + + @Test public void test2() { + final Unifier.Term e1 = p(f(a()), g(b()), Y); + final Unifier.Term e2 = p(Z, g(W), c()); + assertThatUnify(e1, e2, is("[b/W, c/Y, f(a)/Z]")); + } + + @Test public void test3() { + // Note: Hesham Alassaf's test says that these cannot be unified; I think + // because X is free, and so it assumes that Xs are distinct. + final Unifier.Term e1 = p(f(f(b())), X); + final Unifier.Term e2 = p(f(Y), X); + if (unifier instanceof RobinsonUnifier) { + assertThatUnify(e1, e2, is("[X/X, f(b)/Y]")); + } else { + assertThatUnify(e1, e2, is("[f(b)/Y]")); + } + } + + @Test public void test4() { + final Unifier.Term e1 = p(f(f(b())), c()); + final Unifier.Term e2 = p(f(Y), X); + assertThatUnify(e1, e2, is("[c/X, f(b)/Y]")); + } + + @Test public void test5() { + final Unifier.Term e1 = p(a(), X); + final Unifier.Term e2 = p(b(), Y); + assertThatCannotUnify(e1, e2); + } + + @Test public void test6() { + final Unifier.Term e1 = p(X, a()); + final Unifier.Term e2 = p(b(), Y); + assertThatUnify(e1, e2, is("[b/X, a/Y]")); + } + + @Test public void test7() { + final Unifier.Term e1 = f(a(), X); + final Unifier.Term e2 = f(a(), b()); + assertThatUnify(e1, e2, is("[b/X]")); + } + + @Test public void test8() { + final Unifier.Term e1 = f(X); + final Unifier.Term e2 = f(Y); + assertThatUnify(e1, e2, is("[Y/X]")); + } + + @Test public void test9() { + final Unifier.Term e1 = f(g(X), X); + final Unifier.Term e2 = f(Y); + assertThatCannotUnify(e1, e2); + } + + @Test public void test10() { + final Unifier.Term e1 = f(g(X)); + final Unifier.Term e2 = f(Y); + assertThatUnify(e1, e2, is("[g(X)/Y]")); + } + + @Test public void test11() { + final Unifier.Term e1 = f(g(X), X); + final Unifier.Term e2 = f(Y, a()); + assertThatUnify(e1, e2, is("[a/X, g(a)/Y]")); + } + + @Test public void test12() { + final Unifier.Term e1 = father(X, Y); + final Unifier.Term e2 = father(bob(), tom()); + assertThatUnify(e1, e2, is("[bob/X, tom/Y]")); + } + + @Test public void test13() { + final Unifier.Term e1 = parents(X, father(X), mother(bill())); + final Unifier.Term e2 = parents(bill(), father(bill()), Y); + assertThatUnify(e1, e2, is("[bill/X, mother(bill)/Y]")); + } + + @Test public void test14() { + final Unifier.Term e1 = grandParent(X, parent(parent(X))); + final Unifier.Term e2 = grandParent(john(), parent(Y)); + assertThatUnify(e1, e2, is("[john/X, parent(john)/Y]")); + } + + @Test public void test15() { + final Unifier.Term e1 = p(f(a(), g(X))); + final Unifier.Term e2 = p(Y, Y); + assertThatCannotUnify(e1, e2); + } + + @Test public void test16() { + final Unifier.Term e1 = p(a(), X, h(g(Z))); + final Unifier.Term e2 = p(Z, h(Y), h(Y)); + assertThatUnify(e1, e2, is("[h(g(a))/X, g(a)/Y, a/Z]")); + } + + @Test public void test17() { + final Unifier.Term e1 = p(X, X); + final Unifier.Term e2 = p(Y, f(Y)); + if (unifier.occurs()) { + assertThatCannotUnify(e1, e2); + } else if (unifier instanceof RobinsonUnifier) { + assertThatUnify(e1, e2, is("[Y/X, f(Y)/Y]")); + } else { + assertThatUnify(e1, e2, is("[f(Y)/X]")); + } + } + + @Test public void test18() { + final Unifier.Term e1 = part(W, X); + final Unifier.Term e2 = connected(f(W, X), W); + assertThatCannotUnify(e1, e2); + } + + @Test public void test19() { + final Unifier.Term e1 = p(f(X), a(), Y); + final Unifier.Term e2 = p(f(bill()), Z, g(b())); + assertThatUnify(e1, e2, is("[bill/X, g(b)/Y, a/Z]")); + } + + /** Variant of test that uses + * {@link net.hydromatic.sml.util.RobinsonUnifier}. */ + public static class RobinsonUnifierTest extends UnifierTest { + protected Unifier createUnifier() { + return new RobinsonUnifier(); + } + } + + /** Variant of test that uses + * {@link net.hydromatic.sml.util.MartelliUnifier}. */ + public static class MartelliUnifierTest extends UnifierTest { + protected Unifier createUnifier() { + return new MartelliUnifier(); + } + + /** Solves the equations from the S combinator, + * "{@code fn x => fn y => fn z => x z (z y)}", in [ + * Wand 87]. */ + @Test public void test20() { + final Unifier.Variable t0 = unifier.variable("T0"); + final Unifier.Variable t1 = unifier.variable("T1"); + final Unifier.Variable t2 = unifier.variable("T2"); + final Unifier.Variable t3 = unifier.variable("T3"); + final Unifier.Variable t4 = unifier.variable("T4"); + final Unifier.Variable t5 = unifier.variable("T5"); + final Unifier.Variable t6 = unifier.variable("T6"); + final Unifier.Variable t7 = unifier.variable("T7"); + final Unifier.Variable t8 = unifier.variable("T8"); + final Unifier.Variable t9 = unifier.variable("T9"); + final Unifier.TermTerm[] termTerms = { + new Unifier.TermTerm(t0, unifier.apply("->", t1, t2)), + new Unifier.TermTerm(t2, unifier.apply("->", t3, t4)), + new Unifier.TermTerm(t4, unifier.apply("->", t5, t6)), + new Unifier.TermTerm(t1, + unifier.apply("->", t8, unifier.apply("->", t7, t6))), + new Unifier.TermTerm(t8, t5), + new Unifier.TermTerm(unifier.apply("->", t9, t7), t3), + new Unifier.TermTerm(t9, t5) + }; + final Unifier.Substitution unify = + unifier.unify(Arrays.asList(termTerms)); + assertThat(unify, notNullValue()); + assertThat(unify.toString(), + is("[->(T1, T2)/T0, ->(T8, ->(T7, T6))/T1, ->(T3, T4)/T2," + + " ->(T9, T7)/T3, ->(T5, T6)/T4, T5/T8, T5/T9]")); + } + } + + +} + +// End UnifierTest.java