diff --git a/src/main/java/edu/kit/typicalc/Application.java b/src/main/java/edu/kit/typicalc/Application.java index 88b6e57..5b52a7f 100644 --- a/src/main/java/edu/kit/typicalc/Application.java +++ b/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)); } diff --git a/src/main/java/edu/kit/typicalc/model/Tree.java b/src/main/java/edu/kit/typicalc/model/Tree.java index b7b6fe9..8142133 100644 --- a/src/main/java/edu/kit/typicalc/model/Tree.java +++ b/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. diff --git a/src/main/java/edu/kit/typicalc/model/TypeInferer.java b/src/main/java/edu/kit/typicalc/model/TypeInferer.java index 67de596..4402862 100644 --- a/src/main/java/edu/kit/typicalc/model/TypeInferer.java +++ b/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 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 substitutions = unification.getSubstitutions().getValue(); + typeInfResult = new TypeInferenceResult(substitutions, tree.getFirstTypeVariable()); } @Override public InferenceStep getFirstInferenceStep() { - return null; - // TODO + return tree.getFirstInferenceStep(); } @Override public List getUnificationSteps() { - return null; - // TODO + return unification.getUnificationSteps(); } @Override public List getMGU() { - return null; - // TODO + return typeInfResult.getMGU(); } @Override public Type getType() { - return null; - // TODO + return typeInfResult.getType(); } } diff --git a/src/main/java/edu/kit/typicalc/model/Unification.java b/src/main/java/edu/kit/typicalc/model/Unification.java new file mode 100644 index 0000000..1f496ee --- /dev/null +++ b/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 constraints) { + + } + + protected List getUnificationSteps() { + return null; + } + + protected Result, UnificationError> getSubstitutions() { + return null; + } + +} diff --git a/src/main/java/edu/kit/typicalc/model/UnificationError.java b/src/main/java/edu/kit/typicalc/model/UnificationError.java new file mode 100644 index 0000000..6a50c7e --- /dev/null +++ b/src/main/java/edu/kit/typicalc/model/UnificationError.java @@ -0,0 +1,4 @@ +package edu.kit.typicalc.model; + +public enum UnificationError { +} diff --git a/src/main/java/edu/kit/typicalc/view/TypicalcI18NProvider.java b/src/main/java/edu/kit/typicalc/view/TypicalcI18NProvider.java index adf0db2..69dfda5 100644 --- a/src/main/java/edu/kit/typicalc/view/TypicalcI18NProvider.java +++ b/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; diff --git a/src/main/java/edu/kit/typicalc/view/content/ControlPanel.java b/src/main/java/edu/kit/typicalc/view/content/ControlPanel.java index e799e0a..539365a 100644 --- a/src/main/java/edu/kit/typicalc/view/content/ControlPanel.java +++ b/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 Button lastStep; - private Button nextStep; - private Button previousStep; - private Button share; + private final Button firstStep; + private final Button lastStep; + private final Button nextStep; + private final Button previousStep; + 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) { diff --git a/src/main/resources/language/translation_de.properties b/src/main/resources/language/translation_de.properties index c7c4d5e..9d97fc3 100644 --- a/src/main/resources/language/translation_de.properties +++ b/src/main/resources/language/translation_de.properties @@ -1,2 +1,14 @@ root.close=Schließen -root.copyLatex=Kopiere Latex-Code \ No newline at end of file +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 +