From b55c63acc01c025a858bf954070d87a81ad981f4 Mon Sep 17 00:00:00 2001
From: Arne Keller <arne.keller@student.kit.edu>
Date: Thu, 17 Jun 2021 08:45:28 +0200
Subject: [PATCH] Implement quantified variables in type assumptions

see issue #1
---
 .../java/edu/kit/typicalc/model/Tree.java     |  6 ++++-
 .../model/parser/TypeAssumptionParser.java    | 25 ++++++++++++++++---
 .../view/main/TypeAssumptionField.java        |  2 +-
 3 files changed, 28 insertions(+), 5 deletions(-)

diff --git a/src/main/java/edu/kit/typicalc/model/Tree.java b/src/main/java/edu/kit/typicalc/model/Tree.java
index beadc17..894dd5d 100644
--- a/src/main/java/edu/kit/typicalc/model/Tree.java
+++ b/src/main/java/edu/kit/typicalc/model/Tree.java
@@ -52,7 +52,11 @@ public class Tree implements TermVisitorTree {
         this.typeVarFactory = typeVariableFactory;
         this.constraints = new ArrayList<>();
 
-        this.stepFactory = lambdaTerm.hasLet() || partOfLetTerm ? new StepFactoryWithLet() : new StepFactoryDefault();
+        // quantified type assumptions have the same effect as let terms
+        // (both require VarStepWithLet)
+        this.stepFactory = typeAssumptions.entrySet().stream()
+                             .anyMatch(entry -> entry.getValue().hasQuantifiedVariables())
+                || lambdaTerm.hasLet() || partOfLetTerm ? new StepFactoryWithLet() : new StepFactoryDefault();
 
         this.failedSubInference = false;
 
diff --git a/src/main/java/edu/kit/typicalc/model/parser/TypeAssumptionParser.java b/src/main/java/edu/kit/typicalc/model/parser/TypeAssumptionParser.java
index 3d9dca0..eb1e638 100644
--- a/src/main/java/edu/kit/typicalc/model/parser/TypeAssumptionParser.java
+++ b/src/main/java/edu/kit/typicalc/model/parser/TypeAssumptionParser.java
@@ -36,7 +36,7 @@ public class TypeAssumptionParser {
                 return new Result<>(null, ParseError.UNEXPECTED_CHARACTER);
             }
             VarTerm var = new VarTerm(typeName);
-            Result<TypeAbstraction, ParseError> typeAbs = parseType(entry.getValue());
+            Result<TypeAbstraction, ParseError> typeAbs = parseTypeDefinition(entry.getValue());
             if (typeAbs.isError()) {
                 return new Result<>(typeAbs);
             }
@@ -45,14 +45,33 @@ public class TypeAssumptionParser {
         return new Result<>(typeAssumptions);
     }
 
-    public Result<TypeAbstraction, ParseError> parseType(String type) {
+    /**
+     * Parse a type definition that may use the all quantor.
+     * @param definition type definition
+     * @return parsed type
+     */
+    public Result<TypeAbstraction, ParseError> parseTypeDefinition(String definition) {
+        Set<TypeVariable> allQuantified = new HashSet<>();
+        // TODO: clarify syntax, this just (barely) accepts a comma separated list of t<number>
+        if (definition.startsWith("∀")) {
+            String[] parts = definition.split(":", 2);
+            for (String quantified : parts[0].substring(1).split(",")) {
+                int i = Integer.parseInt(quantified.trim().substring(1));
+                allQuantified.add(new TypeVariable(TypeVariableKind.USER_INPUT, i));
+            }
+            definition = parts[1];
+        }
+        return parseType(definition, allQuantified);
+    }
+
+    private Result<TypeAbstraction, ParseError> parseType(String type, Set<TypeVariable> allQuantified) {
         // this parser is using the same lexer as the LambdaParser (to avoid types named "let" etc.)
         LambdaLexer lexer = new LambdaLexer(type);
         Result<Pair<Type, Integer>, ParseError> parsedType = parseType(lexer, 0);
         if (parsedType.isError()) {
             return new Result<>(null, parsedType.unwrapError());
         }
-        return new Result<>(new TypeAbstraction(parsedType.unwrap().getLeft()));
+        return new Result<>(new TypeAbstraction(parsedType.unwrap().getLeft(), allQuantified));
     }
 
     private Result<Pair<Type, Integer>, ParseError> parseType(LambdaLexer lexer, int parenCount) {
diff --git a/src/main/java/edu/kit/typicalc/view/main/TypeAssumptionField.java b/src/main/java/edu/kit/typicalc/view/main/TypeAssumptionField.java
index 1428a1d..18fd6ea 100644
--- a/src/main/java/edu/kit/typicalc/view/main/TypeAssumptionField.java
+++ b/src/main/java/edu/kit/typicalc/view/main/TypeAssumptionField.java
@@ -109,7 +109,7 @@ public class TypeAssumptionField extends HorizontalLayout implements LocaleChang
      * @return true if the type matches the syntax, false if not
      */
     protected boolean hasCorrectType(String type) {
-        return parser.parseType(parseBackType(type)).isOk();
+        return parser.parseTypeDefinition(parseBackType(type)).isOk();
     }
 
     private void addValidator() {