CHANGELOG.md

@@ -3,7 +3,8 @@
 ## 0.9
 
 * Performance improvement: search tree pruning
-* Alpha equality check done lazily
+* Performance: alpha equality check done lazily
+  (i.e. alpha equality check does not eagerly replace variables in the entire abstraction body)
 
 ## 0.8
 

pom.xml

@@ -16,7 +16,7 @@
     <licenses>
         <license>
             <name>MIT License</name>
-            <url>http://www.opensource.org/licenses/mit-license.php</url>
+            <url>https://www.opensource.org/licenses/mit-license.php</url>
         </license>
     </licenses>
 

src/main/java/pl/wojciechkarpiel/jhou/ast/Constant.java

@@ -17,7 +17,7 @@ public class Constant implements Term {
     }
 
     /**
-     * @param name For printing only, equality is decided by Id
+     * @param name For printing only, equality is decided by the ID
      */
     public Constant(Id id, Type type, String name) {
         this.id = id;

src/main/java/pl/wojciechkarpiel/jhou/substitution/SubstitutionPair.java

@@ -2,6 +2,7 @@ package pl.wojciechkarpiel.jhou.substitution;
 
 import pl.wojciechkarpiel.jhou.ast.Term;
 import pl.wojciechkarpiel.jhou.ast.Variable;
+import pl.wojciechkarpiel.jhou.normalizer.Normalizer;
 import pl.wojciechkarpiel.jhou.types.TypeCalculator;
 
 import java.util.Objects;
@@ -13,7 +14,7 @@ public class SubstitutionPair {
 
     public SubstitutionPair(Variable variable, Term term) {
         this.variable = variable;
-        this.term = term;
+        this.term = Normalizer.betaNormalize(term);
         TypeCalculator.ensureEqualTypes(variable, term);
     }
 

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

@@ -77,11 +77,15 @@ public class BetaEtaNormal {
         if (o == null || getClass() != o.getClass()) return false;
         BetaEtaNormal that = (BetaEtaNormal) o;
         return Objects.equals(head, that.head) && Objects.equals(binder, that.binder) && Objects.equals(arguments, that.arguments);
+        // TODO decide if BEN equality should be alpha. Counterpoint: Aplha-equalizing is core functionality of BEN, and making BEN alpha-equal would not allow to differentiate BENs before and after the core functionality is used
+        // return to term for alpha-conversion handling
+//        return backToTerm().equals(that.backToTerm());
     }
 
     @Override
     public int hashCode() {
         return Objects.hash(head, binder, arguments);
+//        return backToTerm().hashCode();
     }
 
     @Override

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

@@ -10,6 +10,15 @@ public class HeadOps {
     }
 
 
+    public static class HeadIsNotAVariableException extends RuntimeException {
+        private HeadIsNotAVariableException(Head head) {
+            super(head + " is not a variable");
+        }
+    }
+
+    public static Variable asVariableYolo(Head h) {
+        return asVariable(h).orElseThrow(() -> new HeadIsNotAVariableException(h));
+    }
     public static Optional<Variable> asVariable(Head h) {
         return h.visit(new Head.HeadVisitor<Optional<Variable>>() {
             @Override

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

@@ -20,10 +20,7 @@ import pl.wojciechkarpiel.jhou.util.ListUtil;
 import pl.wojciechkarpiel.jhou.util.MapUtil;
 
 import java.io.PrintStream;
-import java.util.ArrayList;
-import java.util.HashMap;
-import java.util.List;
-import java.util.Map;
+import java.util.*;
 import java.util.stream.Collectors;
 
 // TODO: this entire class is hideous
@@ -115,24 +112,27 @@ public class TypeInference {
     private final PrintStream printStream;
     private final AllowedTypeInference allowedInference;
 
+    private Set<Type> newTypes = null;
+
     private TypeInference(PrintStream printStream, AllowedTypeInference allowedTypeInference) {
         this.printStream = printStream;
         this.allowedInference = allowedTypeInference;
     }
 
-    private boolean inventedNewTypes = false;
-
+    public final Set<Type> getNewTypes() {
+        if (newTypes == null) newTypes = new HashSet<>();
+        return newTypes;
+    }
 
     private Type getT(Term t, Substitution s) {
-        Type tt = null;
+        Type tt;
         Term b = null;
 
-        Term a = t;
-        if (a instanceof Variable) {
-            b = getAnon(a);
+        if (t instanceof Variable) {
+            b = getAnon(t);
         }
-        if (a instanceof Constant) {
-            b = getAnon(a);
+        if (t instanceof Constant) {
+            b = getAnon(t);
         }
         if (b != null) {
             Term q = s.substitute(b);
@@ -184,15 +184,15 @@ public class TypeInference {
             public Type visitConstant(Constant constant) {
                 Type type = constanTypeMap.get(constant);
                 if (type == null) {
-                    inventedNewTypes = true;
                     if (AllowedTypeInference.PERMISSIVE != allowedInference) {
                         throw new InferenceHasArbitrarySolutionsException();
 
                     }
                     Id id = Id.uniqueId();
-                    BaseType value = new BaseType(id, "infered_arbitrarty_" + id.getId());
-                    printStream.println("Creating a new, arbitrary type: " + value);
-                    constanTypeMap.put(constant, value);
+                    BaseType freshType = new BaseType(id, "infered_arbitrarty_" + id.getId());
+                    printStream.println("Creating a new, arbitrary type: " + freshType);
+                    getNewTypes().add(freshType);
+                    constanTypeMap.put(constant, freshType);
                     return fakeVarToRealType(constant);
                 }
                 return type;
@@ -254,11 +254,10 @@ public class TypeInference {
             }
             {
                 Type rlType = null;
-                Term orig = origTerm;
-                if (orig instanceof Constant) {
-                    rlType = ((Constant) orig).getType();
-                } else if (orig instanceof Variable) {
-                    rlType = ((Variable) orig).getType();
+                if (origTerm instanceof Constant) {
+                    rlType = ((Constant) origTerm).getType();
+                } else if (origTerm instanceof Variable) {
+                    rlType = ((Variable) origTerm).getType();
                 }
                 if (rlType == null) continue;
 

src/main/java/pl/wojciechkarpiel/jhou/unifier/simplifier/Matcher.java

@@ -60,7 +60,7 @@ public class Matcher {
 
     public static List<Substitution> matchS(BetaEtaNormal rigid, BetaEtaNormal flexible) {
         List<Term> matches = match(rigid, flexible);
-        Variable v = HeadOps.asVariable(flexible.getHead()).get();
+        Variable v = HeadOps.asVariableYolo(flexible.getHead());
         List<Substitution> substitutions = new ArrayList<>(matches.size());
         for (Term match : matches) {
             Substitution sub = new Substitution(v, match);
@@ -78,7 +78,6 @@ public class Matcher {
 
     public static List<Term> match(RigidFlexible rigidFlexible) {
         BetaEtaNormal rigid = rigidFlexible.getRigid();
-        BetaEtaNormal flexible = rigidFlexible.getFlexible();
         List<Term> res = new ArrayList<>();
         Optional<Constant> rigidConstant = HeadOps.asConstant(rigid.getHead());
         rigidConstant.ifPresent(c -> res.add(imitate(rigidFlexible)));
@@ -95,7 +94,7 @@ public class Matcher {
             // yooo check if the type matches
             Type pType = TypeCalculator.calculateType(e);
             Type acType = ((Variable) rigidFlexible.flexible.getHead().getTerm()).getType();
-            //  it's not mentioned in paper, but it can (and likely) will) happen that the type of arg is different than contnt
+            //  it's not mentioned in paper, but it can (and likely will) happen that the type of arg is different from content
             if (pType.equals(acType)) {
                 res.add(e);
             }
@@ -113,20 +112,7 @@ public class Matcher {
         for (int j = 0; j < headType.arity(); j++) {
             // arg od benheadBinder, index J
             Term l3l = benHeadBinder.getArguments().get(j);
-            Type targetType = TypeCalculator.calculateType(l3l);
-
-            for (int k = binders.size() - 1; k >= 0; k--) {
-                targetType = new ArrowType(binders.get(k).getType(), targetType);
-            }
-            Variable hi = new Variable(Id.uniqueId(), targetType);
-            BetaEtaNormal arg = BetaEtaNormal.fromFakeNormal(
-                    new Head.HeadVariable(hi),
-                    new ArrayList<>(),
-                    new ArrayList<>(binders) // replacement binders are arg's argyments
-            );
-            Term term = arg.backToTerm();
-            TypeCalculator.calculateType(term); //sanity check
-            args.add(term);
+            args.add(argOfArg(binders, l3l));
         }
         Term term = BetaEtaNormal.fromFakeNormal(newHead, binders, args).backToTerm();
         TypeCalculator.calculateType(term);
@@ -147,23 +133,30 @@ public class Matcher {
         Head newHead = rigidFlexible.getRigid().getHead();
         List<Term> args = new ArrayList<>(rigidFlexible.rigidTermsArgumentsSize());
         for (Term rigidArg : rigidFlexible.rigidTermArguments()) {
-            Type targetType = TypeCalculator.calculateType(rigidArg);
-            for (int i = binders.size() - 1; i >= 0; i--) {
-                targetType = new ArrowType(binders.get(i).getType(), targetType);
-            }
-            Variable hi = new Variable(Id.uniqueId(), targetType);
-            BetaEtaNormal arg = BetaEtaNormal.fromFakeNormal(
-                    new Head.HeadVariable(hi),
-                    new ArrayList<>(),
-                    new ArrayList<>(binders) // replacement binders are arg's arguments
-            );
-            Term term = arg.backToTerm();
-            TypeCalculator.calculateType(term); //sanity check
-            args.add(term);
+            args.add(argOfArg(binders, rigidArg));
         }
 
         Term term = BetaEtaNormal.fromFakeNormal(newHead, binders, args).backToTerm();
         TypeCalculator.calculateType(term);
         return term;
     }
+
+    private static Term argOfArg(List<Variable> binders, Term realArgUponWhichTheArgArgIsBased) {
+
+        Type targetType = TypeCalculator.calculateType(realArgUponWhichTheArgArgIsBased);
+
+        for (int k = binders.size() - 1; k >= 0; k--) {
+            targetType = new ArrowType(binders.get(k).getType(), targetType);
+        }
+        Variable hi = new Variable(Id.uniqueId(), targetType);
+        BetaEtaNormal arg = BetaEtaNormal.fromFakeNormal(
+                new Head.HeadVariable(hi),
+                new ArrayList<>(),
+                new ArrayList<>(binders) // replacement binders are arg's arguments
+        );
+        Term term = arg.backToTerm();
+        TypeCalculator.calculateType(term); //sanity check
+        return term;
+    }
+
 }

src/main/java/pl/wojciechkarpiel/jhou/unifier/simplifier/Simplifier.java

@@ -44,18 +44,17 @@ public class Simplifier {
             }
             ds = newL;
         }
-        ;
 
 
-        // 2. check if its the end (flex-flex)
+        // 2. check if it's the end (flex-flex)
         if (ds.stream().allMatch(q -> q.getType() == PairType.FLEXIBLE_FLEXIBLE)) {
             List<SubstitutionPair> fin = new ArrayList<>();
             Map<Type, Constant> cs = new HashMap<>();
             for (DisagreementPair d : ds) {
                 BetaEtaNormal aN = d.getMostRigid();
                 BetaEtaNormal bN = d.getLeastRigid();
-                Variable va = HeadOps.asVariable(aN.getHead()).get();
-                Variable vb = HeadOps.asVariable(bN.getHead()).get();
+                Variable va = HeadOps.asVariableYolo(aN.getHead());
+                Variable vb = HeadOps.asVariableYolo(bN.getHead());
                 Type t = va.getType();
                 cs.putIfAbsent(t, new Constant(Id.uniqueId(), t));
                 Constant c = cs.get(t);
@@ -71,39 +70,6 @@ public class Simplifier {
         return new SimplificationNode(new DisagreementSet(ds));
     }
 
-    /**
-     * Remove arguments from the normal form and check the rest (i.e. the heading)
-     */
-//    private static boolean equalHeadings(BetaEtaNormal a, BetaEtaNormal b) {
-//        BetaEtaNormal aLol = BetaEtaNormal.fromFakeNormal(a.getHead(), a.getBinder(), new ArrayList<>());
-//        BetaEtaNormal bLol = BetaEtaNormal.fromFakeNormal(b.getHead(), b.getBinder(), new ArrayList<>());
-//        return aLol.backToTerm().equals(bLol.backToTerm());
-//    }
-//
-//    public static Optional<List<DisagreementPair>> breakdownRigidRigid(BetaEtaNormal a, BetaEtaNormal b) {
-//        if ((a.getArguments().size() == b.getArguments().size()) && equalHeadings(a, b)) {
-//            Optional<BetaEtaNormal> bnO = HeaderUnifier.alphaUnifyHeaderReturnNewRight(a, b);
-//            if (bnO.isPresent()) {
-//                BetaEtaNormal bNN = bnO.get();
-//
-//                List<DisagreementPair> ds = new ArrayList<>();
-//                for (int i = 0; i < bNN.getArguments().size(); i++) {
-//
-//                    DisagreementPair dp = new DisagreementPair(
-//                            extract(a, a.getArguments().get(i)),
-//                            extract(bNN, bNN.getArguments().get(i))
-//                    );
-//                    ds.add(dp);
-//                }
-//
-//                return Optional.of(ds);
-//            } else {
-//                return Optional.empty();
-//            }
-//        } else {
-//            return Optional.empty();
-//        }
-//    }
     public static Optional<List<DisagreementPair>> breakdownRigidRigid(BetaEtaNormal a_, BetaEtaNormal b_) {
         Optional<AlphaEqual.BenPair> benPair = AlphaEqual.alphaEqualizeHeading(a_, b_);
         if (!benPair.isPresent()) return Optional.empty();