Merge branch 'master' of https://git.scc.kit.edu/pse-typinferenz/typicalc

src/main/java/edu/kit/typicalc/Application.java

@@ -19,7 +19,6 @@ import org.vaadin.artur.helpers.LaunchUtil;
 public class Application extends SpringBootServletInitializer implements AppShellConfigurator {
 
     public static void main(String[] args) {
-        System.setProperty("user.home", "/home/arne/.cache");
         LaunchUtil.launchBrowserInDevelopmentMode(SpringApplication.run(Application.class, args));
     }
 

src/main/java/edu/kit/typicalc/model/Tree.java

@@ -11,6 +11,7 @@ import edu.kit.typicalc.model.term.VarTerm;
 import edu.kit.typicalc.model.type.Type;
 import edu.kit.typicalc.model.type.TypeAbstraction;
 import edu.kit.typicalc.model.type.TypeAssumption;
+import edu.kit.typicalc.model.type.TypeVariable;
 
 import java.util.List;
 import java.util.Map;
@@ -63,6 +64,16 @@ public class Tree implements TermVisitorTree {
         // TODO;
     }
 
+    /**
+     * Returns the first type variable the original lambda term was assigned in the first inference step.
+     *
+     * @return the first type variable
+     */
+    protected TypeVariable getFirstTypeVariable() {
+        return null;
+        // TODO;
+    }
+
     /**
      * Returns the list of constraints that formed while generating the inference step tree
      * structure, needed for the subsequent unification.

src/main/java/edu/kit/typicalc/model/TypeInferer.java

@@ -19,6 +19,10 @@ import java.util.Map;
  */
 public class TypeInferer implements TypeInfererInterface {
 
+    private final Tree tree;
+    private final Unification unification;
+    private final TypeInferenceResult typeInfResult;
+
     /**
      * Initializes a new TypeInferer for the given type assumptions and lambda term.
      * The inference step structure, unification steps, the most general unifier and the
@@ -28,31 +32,41 @@ public class TypeInferer implements TypeInfererInterface {
      * @param typeAssumptions the type assumptions to consider when generating the tree
      */
     protected TypeInferer(LambdaTerm lambdaTerm, Map<VarTerm, TypeAbstraction> typeAssumptions) {
-        // TODO
+        tree = new Tree(typeAssumptions, lambdaTerm);
+        // TODO: Abbrechen bei fehlgeschlagener let-Teilinferenz, evtl. getUnificationSteps() anpassen
+
+        unification = new Unification(tree.getConstraints());
+
+        // cancel algorithm if term can't be typified
+        if (!unification.getSubstitutions().isOk()) {
+            typeInfResult = null;
+            // TODO: schönere Methode, mit nicht typisierbar umzugehen?
+            //  getter unten anpassen!
+            return;
+        }
+
+        List<Substitution> substitutions = unification.getSubstitutions().getValue();
+        typeInfResult = new TypeInferenceResult(substitutions, tree.getFirstTypeVariable());
     }
 
 
     @Override
     public InferenceStep getFirstInferenceStep() {
-        return null;
+        return tree.getFirstInferenceStep();
-        // TODO
     }
 
     @Override
     public List<UnificationStep> getUnificationSteps() {
-        return null;
+        return unification.getUnificationSteps();
-        // TODO
     }
 
     @Override
     public List<Substitution> getMGU() {
-        return null;
+        return typeInfResult.getMGU();
-        // TODO
     }
 
     @Override
     public Type getType() {
-        return null;
+        return typeInfResult.getType();
-        // TODO
     }
 }

src/main/java/edu/kit/typicalc/model/Unification.java

@@ -0,0 +1,20 @@
+package edu.kit.typicalc.model;
+
+import edu.kit.typicalc.util.Result;
+
+import java.util.List;
+
+public class Unification {
+    protected Unification(List<Constraint> constraints) {
+
+    }
+
+    protected List<UnificationStep> getUnificationSteps() {
+        return null;
+    }
+
+    protected Result<List<Substitution>, UnificationError> getSubstitutions() {
+        return null;
+    }
+
+}

src/main/java/edu/kit/typicalc/model/UnificationError.java

@@ -0,0 +1,4 @@
+package edu.kit.typicalc.model;
+
+public enum UnificationError {
+}

src/main/java/edu/kit/typicalc/view/TypicalcI18NProvider.java

@@ -10,11 +10,11 @@ import org.apache.commons.lang3.StringUtils;
 import org.springframework.stereotype.Component;
 import com.vaadin.flow.i18n.I18NProvider;
 
-@Component
 /**
  * Provides a simple implementation of the I18NProvider.
  * Allows for multiple languages and retrieving static Strings from .property-files.
  */
+@Component
 public class TypicalcI18NProvider implements I18NProvider {
 
     private static final long serialVersionUID = 8261479587838699070L;

src/main/java/edu/kit/typicalc/view/content/ControlPanel.java

@@ -1,5 +1,6 @@
 package edu.kit.typicalc.view.content;
 
+import com.vaadin.flow.component.Component;
 import com.vaadin.flow.component.Key;
 import com.vaadin.flow.component.KeyModifier;
 import com.vaadin.flow.component.button.Button;
@@ -9,16 +10,17 @@ import com.vaadin.flow.component.icon.VaadinIcon;
 /**
  * Provides a GUI in form of buttons for the user to navigate through steps.
  */
-public class ControlPanel  {
+public class ControlPanel extends Component {
 
-    private Button firstStep;
+    private final Button firstStep;
-    private Button lastStep;
+    private final Button lastStep;
-    private Button nextStep;
+    private final Button nextStep;
-    private Button previousStep;
+    private final Button previousStep;
-    private Button share;
+    private final Button share;
 
     /**
      * Sets up buttons with click-listeners that call the corresponding method in the view.
+     *
      * @param view the view that reacts to the button clicks
      */
     public ControlPanel(ControlPanelView view) {
@@ -37,6 +39,7 @@ public class ControlPanel  {
 
     /**
      * Enables the firstStep-button if the parameter is true, disables it if hte parameter is false.
+     *
      * @param setEnabled true to enable the button,false to disable it
      */
     public void setEnabledFirstStep(boolean setEnabled) {
@@ -45,6 +48,7 @@ public class ControlPanel  {
 
     /**
      * Enables the lastStep-button if the parameter is true, disables it if hte parameter is false.
+     *
      * @param setEnabled true to enable the button,false to disable it
      */
     public void setEnabledLastStep(boolean setEnabled) {
@@ -53,6 +57,7 @@ public class ControlPanel  {
 
     /**
      * Enables the nextStep-button if the parameter is true, disables it if hte parameter is false.
+     *
      * @param setEnabled true to enable the button,false to disable it
      */
     public void setEnabledNextStep(boolean setEnabled) {
@@ -61,6 +66,7 @@ public class ControlPanel  {
 
     /**
      * Enables the previousStep-button if the parameter is true, disables it if hte parameter is false.
+     *
      * @param setEnabled true to enable the button,false to disable it
      */
     public void setEnabledPreviousStep(boolean setEnabled) {
@@ -69,6 +75,7 @@ public class ControlPanel  {
 
     /**
      * Enables the share-button if the parameter is true, disables it if hte parameter is false.
+     *
      * @param setEnabled true to enable the button,false to disable it
      */
     public void setEnabledShareButton(boolean setEnabled) {

src/main/resources/language/translation_de.properties

@@ -1,2 +1,14 @@
 root.close=Schließen
-root.copyLatex=Kopiere Latex-Code
+root.copyLatex=Kopiere Latex-Code
+
+abs-rule=\\begin{prooftree}\
+\\AxiomC{$\\Gamma=\\vdash t_1 : \\tau_1 \\rightarrow \\tau_2$}\
+\
+\\AxiomC{$\\Gamma \\vdash t_2 : \\tau_1$}\
+\
+\\LeftLabel{APP}\
+\\BinaryInfC{$\\Gamma \\vdash t_1 \\ t_2 : \\tau_2$}\
+\\end{prooftree}
+
+test=hello world
+