From 89b53351ce19b46308aa7b931e432b34e7cdca9d Mon Sep 17 00:00:00 2001 From: Florian Steurer Date: Wed, 23 Dec 2015 13:25:43 +0100 Subject: [PATCH] martelli montanari unifikation --- .../unify/interfaces/IUnify.java | 2 +- .../unifynew/MartelliMontanariUnify.java | 77 +++++++++++++++---- .../typeinference/unifynew/RuleSet.java | 6 +- .../typeinference/unifynew/Unifier.java | 7 ++ 4 files changed, 73 insertions(+), 19 deletions(-) diff --git a/src/de/dhbwstuttgart/typeinference/unify/interfaces/IUnify.java b/src/de/dhbwstuttgart/typeinference/unify/interfaces/IUnify.java index 34e39738..92dd941d 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/interfaces/IUnify.java +++ b/src/de/dhbwstuttgart/typeinference/unify/interfaces/IUnify.java @@ -10,5 +10,5 @@ import de.dhbwstuttgart.typinference.unify.model.MPair; * @author Florian Steurer */ public interface IUnify { - public Unifier unify(Set terms); + public Set unify(Set terms); } diff --git a/src/de/dhbwstuttgart/typeinference/unifynew/MartelliMontanariUnify.java b/src/de/dhbwstuttgart/typeinference/unifynew/MartelliMontanariUnify.java index 3631ed24..89e02cbb 100644 --- a/src/de/dhbwstuttgart/typeinference/unifynew/MartelliMontanariUnify.java +++ b/src/de/dhbwstuttgart/typeinference/unifynew/MartelliMontanariUnify.java @@ -1,7 +1,12 @@ package de.dhbwstuttgart.typeinference.unifynew; import java.util.HashSet; +import java.util.LinkedList; +import java.util.Optional; +import java.util.Queue; import java.util.Set; +import java.util.Stack; +import java.util.stream.Collectors; import de.dhbwstuttgart.typeinference.unify.interfaces.IUnify; import de.dhbwstuttgart.typinference.unify.model.MPair; @@ -16,43 +21,85 @@ import de.dhbwstuttgart.typinference.unify.model.TypeParams; public class MartelliMontanariUnify implements IUnify { @Override - public Unifier unify(Set terms) { - // TODO Auto-generated method stub - return null; + public Set unify(Set terms) { + Queue termsQ = new LinkedList<>(terms); + Set result = new HashSet<>(); + + + while(!termsQ.isEmpty()) { + MPair pair = termsQ.poll(); + + if(delete(pair)) + continue; + + Optional> optSet = decompose(pair); + + if(optSet == null) + return new HashSet<>(); // Unification failed + + if(optSet.isPresent()) { + termsQ.addAll(optSet.get()); + continue; + } + + Optional optPair = swap(pair); + + if(optPair.isPresent()) { + termsQ.add(optPair.get()); + continue; + } + + Optional optUni = eliminate(pair); + + if(optUni.isPresent()) { + Unifier uni = optUni.get(); + termsQ = termsQ.stream().map(uni::apply).collect(Collectors.toCollection(LinkedList::new)); + result = result.stream().map(uni::apply).collect(Collectors.toCollection(HashSet::new)); + continue; + } + + // TODO occurs check? + } + + return result; } private boolean delete(MPair pair) { return pair.getRhsType().equals(pair.getLhsType()); } - private Set decompose(MPair pair) { + private Optional> decompose(MPair pair) { Set result = new HashSet<>(); Type rhs = pair.getRhsType(); Type lhs = pair.getLhsType(); - - if(!rhs.getName().equals(lhs.getName()) || rhs.getTypeParams().size() != lhs.getTypeParams().size()) - return null; // conflict - + TypeParams rhsTypeParams = rhs.getTypeParams(); TypeParams lhsTypeParams = lhs.getTypeParams(); + + if(rhsTypeParams.size() == 0 || lhsTypeParams.size() == 0) + return Optional.empty(); + + if(!rhs.getName().equals(lhs.getName()) || rhsTypeParams.size() != lhsTypeParams.size()) + return null; // conflict for(int i = 0; i < rhsTypeParams.size(); i++) result.add(new MPair(rhsTypeParams.get(i), lhsTypeParams.get(i), PairOperator.EQUALSDOT)); - return result; + return Optional.of(result); } - private MPair swap(MPair pair) { + private Optional swap(MPair pair) { Type rhs = pair.getRhsType(); Type lhs = pair.getLhsType(); if(lhs.getTypeParams().size() != 0 && rhs.getTypeParams().size() == 0) - return new MPair(rhs, lhs, PairOperator.EQUALSDOT); - return pair; + return Optional.of(new MPair(rhs, lhs, PairOperator.EQUALSDOT)); + + return Optional.empty(); } - private Unifier eliminate(MPair pair) { + private Optional eliminate(MPair pair) { Type rhs = pair.getRhsType(); Type lhs = pair.getLhsType(); @@ -60,9 +107,9 @@ public class MartelliMontanariUnify implements IUnify { for(Type t : rhsTypeParams) if(lhs.equals(t)) - return new Unifier(); //identity-"unifier" + return Optional.empty(); - return new Unifier(lhs, rhs); + return Optional.of(new Unifier(lhs, rhs)); } private boolean check(MPair pair) { diff --git a/src/de/dhbwstuttgart/typeinference/unifynew/RuleSet.java b/src/de/dhbwstuttgart/typeinference/unifynew/RuleSet.java index 3dff9384..1f5cd265 100644 --- a/src/de/dhbwstuttgart/typeinference/unifynew/RuleSet.java +++ b/src/de/dhbwstuttgart/typeinference/unifynew/RuleSet.java @@ -346,7 +346,7 @@ public class RuleSet implements IRuleSet{ for(int i = 1; i < typeDParams.size(); i++) unif.andThen(new Unifier(typeDgenParams.get(i), typeDParams.get(i))); - return Optional.of(new MPair(newLhs.apply(unif), typeDs, PairOperator.SMALLERDOT)); + return Optional.of(new MPair(unif.apply(newLhs), typeDs, PairOperator.SMALLERDOT)); } @Override @@ -392,7 +392,7 @@ public class RuleSet implements IRuleSet{ for(int i = 1; i < typeDParams.size(); i++) unif.andThen(new Unifier(typeDgenParams.get(i), typeDParams.get(i))); - return Optional.of(new MPair(newLhs.apply(unif), typeExtDs, PairOperator.SMALLERDOTWC)); + return Optional.of(new MPair(unif.apply(newLhs), typeExtDs, PairOperator.SMALLERDOTWC)); } @Override @@ -444,7 +444,7 @@ public class RuleSet implements IRuleSet{ for(int i = 1; i < typeDParams.size(); i++) unif.andThen(new Unifier(typeSupDsgenParams.get(i), typeDParams.get(i))); - return Optional.of(new MPair(newLhs.apply(unif), newRhs, PairOperator.SMALLERDOTWC)); + return Optional.of(new MPair(unif.apply(newLhs), newRhs, PairOperator.SMALLERDOTWC)); } /** diff --git a/src/de/dhbwstuttgart/typeinference/unifynew/Unifier.java b/src/de/dhbwstuttgart/typeinference/unifynew/Unifier.java index 4528a934..0428a84e 100644 --- a/src/de/dhbwstuttgart/typeinference/unifynew/Unifier.java +++ b/src/de/dhbwstuttgart/typeinference/unifynew/Unifier.java @@ -1,7 +1,10 @@ package de.dhbwstuttgart.typeinference.unifynew; +import java.util.Set; import java.util.function.Function; +import java.util.stream.Collectors; +import de.dhbwstuttgart.typinference.unify.model.MPair; import de.dhbwstuttgart.typinference.unify.model.Type; import de.dhbwstuttgart.typinference.unify.model.TypeParams; @@ -26,6 +29,10 @@ public class Unifier implements Function { return t.apply(this); } + public MPair apply(MPair p) { + return new MPair(this.apply(p.getLhsType()), this.apply(p.getRhsType()), p.getPairOp()); + } + public Type getSource() { return source; }