From 8929a59e82486cd44197627eb54331944e701090 Mon Sep 17 00:00:00 2001
From: uogau <uogau@student.kit.edu>
Date: Mon, 1 Feb 2021 14:14:18 +0100
Subject: [PATCH] =?UTF-8?q?createLetStep=20hinzugef=C3=BCgt?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 .../kit/typicalc/model/step/StepFactory.java   | 12 +++++++++++-
 .../model/step/StepFactoryDefault.java         | 18 ++++++++++++++++++
 .../model/step/StepFactoryWithLet.java         | 16 +++++++++++++++-
 3 files changed, 44 insertions(+), 2 deletions(-)

diff --git a/src/main/java/edu/kit/typicalc/model/step/StepFactory.java b/src/main/java/edu/kit/typicalc/model/step/StepFactory.java
index d2adb02..a9bda9f 100644
--- a/src/main/java/edu/kit/typicalc/model/step/StepFactory.java
+++ b/src/main/java/edu/kit/typicalc/model/step/StepFactory.java
@@ -2,6 +2,7 @@ package edu.kit.typicalc.model.step;
 
 import edu.kit.typicalc.model.Conclusion;
 import edu.kit.typicalc.model.Constraint;
+import edu.kit.typicalc.model.TypeInfererLet;
 import edu.kit.typicalc.model.type.Type;
 import edu.kit.typicalc.model.type.TypeAbstraction;
 
@@ -46,5 +47,14 @@ public interface StepFactory {
      */
     VarStep createVarStep(TypeAbstraction typeAbstraction, Type instantiatedTypeAbs,
                           Conclusion conclusion, Constraint constraint);
-    //TODO LetStep
+    /**
+     * Creates a LetStep.
+     * @param conclusion the conclusion of this step
+     * @param constraint the constraint that can be derived from this step
+     * @param premise the premise that doesn't need its own type inference
+     * @param typeInferer the typeInferer for the premise that needs its own type inference
+     * @return the created AppStep
+     */
+    LetStep createLetStep(Conclusion conclusion, Constraint constraint,
+                          InferenceStep premise, TypeInfererLet typeInferer);
 }
diff --git a/src/main/java/edu/kit/typicalc/model/step/StepFactoryDefault.java b/src/main/java/edu/kit/typicalc/model/step/StepFactoryDefault.java
index 459d0fe..e3a3dc1 100644
--- a/src/main/java/edu/kit/typicalc/model/step/StepFactoryDefault.java
+++ b/src/main/java/edu/kit/typicalc/model/step/StepFactoryDefault.java
@@ -2,6 +2,7 @@ package edu.kit.typicalc.model.step;
 
 import edu.kit.typicalc.model.Conclusion;
 import edu.kit.typicalc.model.Constraint;
+import edu.kit.typicalc.model.TypeInfererLet;
 import edu.kit.typicalc.model.type.Type;
 import edu.kit.typicalc.model.type.TypeAbstraction;
 
@@ -60,4 +61,21 @@ public class StepFactoryDefault implements StepFactory {
                                         Conclusion conclusion, Constraint constraint) {
         return new VarStepDefault(typeAbstraction, instantiatedTypeAbs, conclusion, constraint);
     }
+
+    /**
+     * Throws an UnsupportedOperationException.
+     * This method should never be called, as a StepFactoryDefault should only be used
+     * for lambda terms without any let polymorphism and therefore should never have
+     * to create a step where the let rule is applied.
+     * @param conclusion the conclusion of this step
+     * @param constraint the constraint that can be derived from this step
+     * @param premise the premise that doesn't need its own type inference
+     * @param typeInferer the typeInferer for the premise that needs its own type inference
+     * @return nothing
+     */
+    @Override
+    public LetStep createLetStep(Conclusion conclusion, Constraint constraint,
+                                 InferenceStep premise, TypeInfererLet typeInferer) {
+        throw new UnsupportedOperationException("Not possible to create LetStep when no let is present in the term");
+    }
 }
diff --git a/src/main/java/edu/kit/typicalc/model/step/StepFactoryWithLet.java b/src/main/java/edu/kit/typicalc/model/step/StepFactoryWithLet.java
index a311018..e5e9171 100644
--- a/src/main/java/edu/kit/typicalc/model/step/StepFactoryWithLet.java
+++ b/src/main/java/edu/kit/typicalc/model/step/StepFactoryWithLet.java
@@ -2,6 +2,7 @@ package edu.kit.typicalc.model.step;
 
 import edu.kit.typicalc.model.Conclusion;
 import edu.kit.typicalc.model.Constraint;
+import edu.kit.typicalc.model.TypeInfererLet;
 import edu.kit.typicalc.model.type.Type;
 import edu.kit.typicalc.model.type.TypeAbstraction;
 
@@ -49,7 +50,6 @@ public class StepFactoryWithLet implements StepFactory {
 
     /**
      * Creates a VarStepWithLet.
-     *
      * @param typeAbstraction the type abstraction of this step
      * @param instantiatedTypeAbs an instantiation of the type abstraction used in this step
      * @param conclusion the conclusion of this step
@@ -61,4 +61,18 @@ public class StepFactoryWithLet implements StepFactory {
                                         Conclusion conclusion, Constraint constraint) {
         return new VarStepWithLet(typeAbstraction, instantiatedTypeAbs, conclusion, constraint);
     }
+
+    /**
+     * Creates a LetStepDefault.
+     * @param conclusion the conclusion of this step
+     * @param constraint the constraint that can be derived from this step
+     * @param premise the premise that doesn't need its own type inference
+     * @param typeInferer the typeInferer for the premise that needs its own type inference
+     * @return the created LetStepDefault
+     */
+    @Override
+    public LetStepDefault createLetStep(Conclusion conclusion, Constraint constraint,
+                                        InferenceStep premise, TypeInfererLet typeInferer) {
+        return new LetStepDefault(conclusion, constraint, premise, typeInferer);
+    }
 }