Formatting: tabs -> spaces

This commit is contained in:
Arne Keller 2021-01-30 10:37:27 +01:00
parent b716b204b3
commit e25a947621
7 changed files with 176 additions and 174 deletions

View File

@ -11,12 +11,13 @@ public interface TermVisitorTree {
* Returns an {@link edu.kit.typicalc.model.step.AppStep} suiting the given application (lambda term) * Returns an {@link edu.kit.typicalc.model.step.AppStep} suiting the given application (lambda term)
* to type-infer and the type assumptions to consider. * to type-infer and the type assumptions to consider.
* Simultaneously assembles the tree's constraint list. * Simultaneously assembles the tree's constraint list.
*
* @param appTerm the application (lambda term) to build the inference step structure for, * @param appTerm the application (lambda term) to build the inference step structure for,
* i.e. the lambda term in the conclusion of the returned inference step * i.e. the lambda term in the conclusion of the returned inference step
* @param typeAssumptions the type assumptions to consider, * @param typeAssumptions the type assumptions to consider,
* i.e. the type assumptions in the conclusion of the returned inference step * i.e. the type assumptions in the conclusion of the returned inference step
* @param conclusionType the type that the lambda term in the conclusion * @param conclusionType the type that the lambda term in the conclusion
* of the returned inference step will be assigned * of the returned inference step will be assigned
* @return an {@link edu.kit.typicalc.model.step.AppStep} * @return an {@link edu.kit.typicalc.model.step.AppStep}
*/ */
InferenceStep visit(AppTerm appTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType); InferenceStep visit(AppTerm appTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType);
@ -25,12 +26,13 @@ public interface TermVisitorTree {
* Returns an {@link edu.kit.typicalc.model.step.AbsStep} suiting the given abstraction (lambda term) * Returns an {@link edu.kit.typicalc.model.step.AbsStep} suiting the given abstraction (lambda term)
* to type-infer and the type assumptions to consider. * to type-infer and the type assumptions to consider.
* Simultaneously assembles the tree's constraint list. * Simultaneously assembles the tree's constraint list.
*
* @param absTerm the abstraction (lambda term) to build the inference step structure for, * @param absTerm the abstraction (lambda term) to build the inference step structure for,
* i.e. the lambda term in the conclusion of the returned inference step * i.e. the lambda term in the conclusion of the returned inference step
* @param typeAssumptions the type assumptions to consider, * @param typeAssumptions the type assumptions to consider,
* i.e. the type assumptions in the conclusion of the returned inference step * i.e. the type assumptions in the conclusion of the returned inference step
* @param conclusionType the type that the lambda term in the conclusion * @param conclusionType the type that the lambda term in the conclusion
* of the returned inference step will be assigned * of the returned inference step will be assigned
* @return an {@link edu.kit.typicalc.model.step.AbsStep} * @return an {@link edu.kit.typicalc.model.step.AbsStep}
*/ */
InferenceStep visit(AbsTerm absTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType); InferenceStep visit(AbsTerm absTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType);
@ -39,12 +41,13 @@ public interface TermVisitorTree {
* Returns an {@link edu.kit.typicalc.model.step.LetStep} suiting the given let expression (lambda term) * Returns an {@link edu.kit.typicalc.model.step.LetStep} suiting the given let expression (lambda term)
* to type-infer and the type assumptions to consider. * to type-infer and the type assumptions to consider.
* Simultaneously assembles the tree's constraint list. * Simultaneously assembles the tree's constraint list.
*
* @param letTerm the let expression (lambda term) to build the inference step structure for, * @param letTerm the let expression (lambda term) to build the inference step structure for,
* i.e. the lambda term in the conclusion of the returned inference step * i.e. the lambda term in the conclusion of the returned inference step
* @param typeAssumptions the type assumptions to consider, * @param typeAssumptions the type assumptions to consider,
* i.e. the type assumptions in the conclusion of the returned inference step * i.e. the type assumptions in the conclusion of the returned inference step
* @param conclusionType the type that the lambda term in the conclusion * @param conclusionType the type that the lambda term in the conclusion
* of the returned inference step will be assigned * of the returned inference step will be assigned
* @return an {@link edu.kit.typicalc.model.step.LetStep} * @return an {@link edu.kit.typicalc.model.step.LetStep}
*/ */
InferenceStep visit(LetTerm letTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType); InferenceStep visit(LetTerm letTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType);
@ -53,12 +56,13 @@ public interface TermVisitorTree {
* Returns an {@link edu.kit.typicalc.model.step.ConstStep} suiting the given constant * Returns an {@link edu.kit.typicalc.model.step.ConstStep} suiting the given constant
* to type-infer and the type assumptions to consider. * to type-infer and the type assumptions to consider.
* Simultaneously assembles the tree's constraint list. * Simultaneously assembles the tree's constraint list.
*
* @param constTerm the constant to build the inference step structure for, * @param constTerm the constant to build the inference step structure for,
* i.e. the lambda term in the conclusion of the returned inference step * i.e. the lambda term in the conclusion of the returned inference step
* @param typeAssumptions the type assumptions to consider, * @param typeAssumptions the type assumptions to consider,
* i.e. the type assumptions in the conclusion of the returned inference step * i.e. the type assumptions in the conclusion of the returned inference step
* @param conclusionType the type that the lambda term in the conclusion * @param conclusionType the type that the lambda term in the conclusion
* of the returned inference step will be assigned * of the returned inference step will be assigned
* @return an {@link edu.kit.typicalc.model.step.ConstStep} * @return an {@link edu.kit.typicalc.model.step.ConstStep}
*/ */
InferenceStep visit(ConstTerm constTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType); InferenceStep visit(ConstTerm constTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType);
@ -67,12 +71,13 @@ public interface TermVisitorTree {
* Returns an {@link edu.kit.typicalc.model.step.VarStep} suiting the given variable (lambda term) * Returns an {@link edu.kit.typicalc.model.step.VarStep} suiting the given variable (lambda term)
* to type-infer and the type assumptions to consider. * to type-infer and the type assumptions to consider.
* Simultaneously assembles the tree's constraint list. * Simultaneously assembles the tree's constraint list.
*
* @param varTerm the variable (lambda term) to build the inference step structure for, * @param varTerm the variable (lambda term) to build the inference step structure for,
* i.e. the lambda term in the conclusion of the returned inference step * i.e. the lambda term in the conclusion of the returned inference step
* @param typeAssumptions the type assumptions to consider, * @param typeAssumptions the type assumptions to consider,
* i.e. the type assumptions in the conclusion of the returned inference step * i.e. the type assumptions in the conclusion of the returned inference step
* @param conclusionType the type that the lambda term in the conclusion * @param conclusionType the type that the lambda term in the conclusion
* of the returned inference step will be assigned * of the returned inference step will be assigned
* @return an {@link edu.kit.typicalc.model.step.VarStep} * @return an {@link edu.kit.typicalc.model.step.VarStep}
*/ */
InferenceStep visit(VarTerm varTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType) InferenceStep visit(VarTerm varTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType)

View File

@ -9,121 +9,121 @@ import java.util.Objects;
* Models a simple named type. * Models a simple named type.
*/ */
public class NamedType extends Type { public class NamedType extends Type {
/** /**
* boolean type * boolean type
*/ */
public static final NamedType BOOLEAN = new NamedType("boolean"); public static final NamedType BOOLEAN = new NamedType("boolean");
/** /**
* int type * int type
*/ */
public static final NamedType INT = new NamedType("int"); public static final NamedType INT = new NamedType("int");
private final String name; private final String name;
/** /**
* Initializes a new NamedType with the given name. * Initializes a new NamedType with the given name.
* @param name the name of this type * @param name the name of this type
*/ */
public NamedType(String name) { public NamedType(String name) {
this.name = name; this.name = name;
} }
/** /**
* Returns the name of the named type. * Returns the name of the named type.
* @return the name of this type * @return the name of this type
*/ */
public String getName() { public String getName() {
return name; return name;
} }
/** /**
* Checks whether some type occurs in this type. * Checks whether some type occurs in this type.
* @param x the type to look for * @param x the type to look for
* @return whether the specified type is equal to this type * @return whether the specified type is equal to this type
*/ */
public boolean contains(Type x) { public boolean contains(Type x) {
return this.equals(x); return this.equals(x);
} }
/** /**
* Substitutes a type variable for a different type. * Substitutes a type variable for a different type.
* @param a the type to replace * @param a the type to replace
* @param b the type to insert * @param b the type to insert
* @return itself, or b if a is equal to this object * @return itself, or b if a is equal to this object
*/ */
@Override @Override
public Type substitute(TypeVariable a, Type b) { public Type substitute(TypeVariable a, Type b) {
return this; return this;
} }
/** /**
* Accepts a visitor. * Accepts a visitor.
* @param typeVisitor the visitor that wants to visit this * @param typeVisitor the visitor that wants to visit this
*/ */
@Override @Override
public void accept(TypeVisitor typeVisitor) { public void accept(TypeVisitor typeVisitor) {
typeVisitor.visit(this); typeVisitor.visit(this);
} }
/** /**
* Computes the necessary constraints (and substitution) to unify this type with * Computes the necessary constraints (and substitution) to unify this type with
* another. This method uses the constrainEqualToNamedType method on the other * another. This method uses the constrainEqualToNamedType method on the other
* type. * type.
* @param type the other type * @param type the other type
* @return unification steps necessary, or an error if that is impossible * @return unification steps necessary, or an error if that is impossible
*/ */
@Override @Override
public Result<UnificationActions, UnificationError> constrainEqualTo(Type type) { public Result<UnificationActions, UnificationError> constrainEqualTo(Type type) {
return type.constrainEqualToNamedType(this); return type.constrainEqualToNamedType(this);
} }
/** /**
* Computes the necessary constraints (and substitution) to unify this type with a * Computes the necessary constraints (and substitution) to unify this type with a
* function type. * function type.
* @param type the function type * @param type the function type
* @return unification steps necessary, or an error if that is impossible * @return unification steps necessary, or an error if that is impossible
*/ */
@Override @Override
public Result<UnificationActions, UnificationError> constrainEqualToFunction(FunctionType type) { public Result<UnificationActions, UnificationError> constrainEqualToFunction(FunctionType type) {
return UnificationUtil.functionNamed(type, this); return UnificationUtil.functionNamed(type, this);
} }
/** /**
* Computes the necessary constraints (and substitution) to unify this type with a * Computes the necessary constraints (and substitution) to unify this type with a
* named type. * named type.
* @param type the named type * @param type the named type
* @return unification steps necessary, or an error if that is impossible * @return unification steps necessary, or an error if that is impossible
*/ */
@Override @Override
public Result<UnificationActions, UnificationError> constrainEqualToNamedType(NamedType type) { public Result<UnificationActions, UnificationError> constrainEqualToNamedType(NamedType type) {
return UnificationUtil.namedNamed(this, type); return UnificationUtil.namedNamed(this, type);
} }
/** /**
* Computes the necessary constraints (and substitution) to unify this type with a * Computes the necessary constraints (and substitution) to unify this type with a
* type variable. * type variable.
* @param type the type variable * @param type the type variable
* @return the unification steps necessary, or an error if that is impossible * @return the unification steps necessary, or an error if that is impossible
*/ */
@Override @Override
public Result<UnificationActions, UnificationError> constrainEqualToVariable(TypeVariable type) { public Result<UnificationActions, UnificationError> constrainEqualToVariable(TypeVariable type) {
return UnificationUtil.variableNamed(type, this); return UnificationUtil.variableNamed(type, this);
} }
@Override @Override
public boolean equals(Object o) { public boolean equals(Object o) {
if (this == o) { if (this == o) {
return true; return true;
} }
if (o == null || getClass() != o.getClass()) { if (o == null || getClass() != o.getClass()) {
return false; return false;
} }
NamedType namedType = (NamedType) o; NamedType namedType = (NamedType) o;
return Objects.equals(name, namedType.name); return Objects.equals(name, namedType.name);
} }
@Override @Override
public int hashCode() { public int hashCode() {
return Objects.hash(name); return Objects.hash(name);
} }
} }

View File

@ -4,21 +4,21 @@ package edu.kit.typicalc.model.type;
* Can be implemented to process Type objects. * Can be implemented to process Type objects.
*/ */
public interface TypeVisitor { public interface TypeVisitor {
/** /**
* Visit a named type. * Visit a named type.
* @param named the type to be visited * @param named the type to be visited
*/ */
void visit(NamedType named); void visit(NamedType named);
/** /**
* Visit a type variable * Visit a type variable
* @param variable the variable to be visited * @param variable the variable to be visited
*/ */
void visit(TypeVariable variable); void visit(TypeVariable variable);
/** /**
* Visit a function. * Visit a function.
* @param function the function to be visited * @param function the function to be visited
*/ */
void visit(FunctionType function); void visit(FunctionType function);
} }

View File

@ -10,16 +10,16 @@ import com.vaadin.flow.i18n.LocaleChangeObserver;
public class DrawerContent extends VerticalLayout implements LocaleChangeObserver { public class DrawerContent extends VerticalLayout implements LocaleChangeObserver {
private static final long serialVersionUID = -5751275682270653335L; private static final long serialVersionUID = -5751275682270653335L;
/* /*
* Id's for the imported css-file * IDs for the imported CSS file
*/ */
private static final String RULE_CONTAINER_ID = "ruleContainer"; private static final String RULE_CONTAINER_ID = "ruleContainer";
private static final String DRAWER_CONTENT_ID = "drawerContent"; private static final String DRAWER_CONTENT_ID = "drawerContent";
private final H3 heading; private final H3 heading;
private final VerticalLayout ruleContainer; private final VerticalLayout ruleContainer;
public DrawerContent() { public DrawerContent() {
heading = new H3(getTranslation("root.inferenceRules")); heading = new H3(getTranslation("root.inferenceRules"));
ruleContainer = new VerticalLayout(); ruleContainer = new VerticalLayout();
@ -28,18 +28,18 @@ public class DrawerContent extends VerticalLayout implements LocaleChangeObserve
add(heading, ruleContainer); add(heading, ruleContainer);
setId(DRAWER_CONTENT_ID); setId(DRAWER_CONTENT_ID);
} }
private void initRuleContainer() { private void initRuleContainer() {
//TODO just demo content, exchange with correct rules //TODO just demo content, exchange with correct rules
ruleContainer.add(new InferenceRuleField(getTranslation("abs-rule"), "root.absRule")); ruleContainer.add(new InferenceRuleField(getTranslation("abs-rule"), "root.absRule"));
ruleContainer.add(new InferenceRuleField(getTranslation("abs-rule"), "root.absRule")); ruleContainer.add(new InferenceRuleField(getTranslation("abs-rule"), "root.absRule"));
ruleContainer.add(new InferenceRuleField(getTranslation("abs-rule"), "root.absRule")); ruleContainer.add(new InferenceRuleField(getTranslation("abs-rule"), "root.absRule"));
ruleContainer.add(new InferenceRuleField(getTranslation("abs-rule"), "root.absRule")); ruleContainer.add(new InferenceRuleField(getTranslation("abs-rule"), "root.absRule"));
ruleContainer.add(new InferenceRuleField(getTranslation("abs-rule"), "root.absRule")); ruleContainer.add(new InferenceRuleField(getTranslation("abs-rule"), "root.absRule"));
} }
@Override @Override
public void localeChange(LocaleChangeEvent event) { public void localeChange(LocaleChangeEvent event) {
heading.setText(getTranslation("root.inferenceRules")); heading.setText(getTranslation("root.inferenceRules"));
} }
} }

View File

@ -11,34 +11,33 @@ import com.vaadin.flow.i18n.LocaleChangeObserver;
@CssImport("./styles/view/main/help-dialog.css") @CssImport("./styles/view/main/help-dialog.css")
public class HelpDialog extends Dialog implements LocaleChangeObserver { public class HelpDialog extends Dialog implements LocaleChangeObserver {
private static final long serialVersionUID = 4470277770276296164L; private static final long serialVersionUID = 4470277770276296164L;
/* /*
* Id's for the imported css-file * IDs for the imported CSS file
*/ */
private static final String HEADING_LAYOUT_ID = "headingLayout"; private static final String HEADING_LAYOUT_ID = "headingLayout";
private static final String CONTENT_LAYOUT_ID = "contentLayout"; private static final String CONTENT_LAYOUT_ID = "contentLayout";
private final H3 heading; private final H3 heading;
private final H5 inputSyntax; private final H5 inputSyntax;
public HelpDialog() { public HelpDialog() {
final HorizontalLayout headingLayout = new HorizontalLayout(); final HorizontalLayout headingLayout = new HorizontalLayout();
heading = new H3(getTranslation("root.operatingHelp")); heading = new H3(getTranslation("root.operatingHelp"));
headingLayout.setId(HEADING_LAYOUT_ID); headingLayout.setId(HEADING_LAYOUT_ID);
headingLayout.add(heading); headingLayout.add(heading);
final VerticalLayout contentLayout = new VerticalLayout(); final VerticalLayout contentLayout = new VerticalLayout();
inputSyntax = new H5(getTranslation("root.inputSyntax")); inputSyntax = new H5(getTranslation("root.inputSyntax"));
contentLayout.setId(CONTENT_LAYOUT_ID); contentLayout.setId(CONTENT_LAYOUT_ID);
contentLayout.add(inputSyntax); contentLayout.add(inputSyntax);
add(headingLayout, contentLayout); add(headingLayout, contentLayout);
} }
@Override @Override
public void localeChange(LocaleChangeEvent event) { public void localeChange(LocaleChangeEvent event) {
heading.setText(getTranslation("root.operatingHelp")); heading.setText(getTranslation("root.operatingHelp"));
inputSyntax.setText(getTranslation("root.inputSyntax")); inputSyntax.setText(getTranslation("root.inputSyntax"));
} }
} }

View File

@ -24,15 +24,14 @@ import com.vaadin.flow.i18n.LocaleChangeObserver;
*/ */
@CssImport("./styles/view/main/input-bar.css") @CssImport("./styles/view/main/input-bar.css")
public class InputBar extends HorizontalLayout implements LocaleChangeObserver { public class InputBar extends HorizontalLayout implements LocaleChangeObserver {
private static final long serialVersionUID = -6099700300418752958L; private static final long serialVersionUID = -6099700300418752958L;
/* /*
* Id's for the imported css-file * Id's for the imported css-file
*/ */
private static final String INPUT_FIELD_ID = "inputField"; private static final String INPUT_FIELD_ID = "inputField";
private static final String INPUT_BAR_ID = "inputBar"; private static final String INPUT_BAR_ID = "inputBar";
private final Tooltip infoTooltip; private final Tooltip infoTooltip;
private final Icon infoIcon; private final Icon infoIcon;
private final Button exampleButton; private final Button exampleButton;
@ -42,17 +41,17 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver {
/** /**
* Creates an InputBar with a Consumer-object to call the inferType()-method in UpperBar. * Creates an InputBar with a Consumer-object to call the inferType()-method in UpperBar.
* The current user input is passed as the methods argument. * The current user input is passed as the methods argument.
* *
* @param callback Consumer to call the inferType()-method in UpperBar * @param callback Consumer to call the inferType()-method in UpperBar
*/ */
protected InputBar(final Consumer<String> callback) { protected InputBar(final Consumer<String> callback) {
infoIcon = new Icon(VaadinIcon.INFO_CIRCLE); infoIcon = new Icon(VaadinIcon.INFO_CIRCLE);
// TODO: where is this tooltip supposed to show up? next to icon, currently not working // TODO: where is this tooltip supposed to show up? next to icon, currently not working
infoTooltip = new Tooltip(infoIcon, TooltipPosition.LEFT, TooltipAlignment.LEFT); infoTooltip = new Tooltip(infoIcon, TooltipPosition.LEFT, TooltipAlignment.LEFT);
infoTooltip.add(new H5("Hallo")); infoTooltip.add(new H5("Hallo"));
initInfoTooltip(); initInfoTooltip();
inputField = new TextField(); inputField = new TextField();
inputField.setId(INPUT_FIELD_ID); inputField.setId(INPUT_FIELD_ID);
inputField.setClearButtonVisible(true); inputField.setClearButtonVisible(true);
@ -93,7 +92,7 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver {
} }
private void initInfoTooltip() { private void initInfoTooltip() {
infoTooltip.add(new H5("Hallo")); infoTooltip.add(new H5("Hallo"));
} }
@Override @Override

View File

@ -20,7 +20,7 @@ import edu.kit.typicalc.view.content.typeinferencecontent.TypeInferenceView;
/** /**
* Contains all the displayed components and builds the applications user interface (UI). * Contains all the displayed components and builds the applications user interface (UI).
* Vaadins app layout provides the rough structure of the UI. Using this structure the UI always * Vaadin's app layout provides the rough structure of the UI. Using this structure the UI always
* consists of an upper bar at the top of the screen and a drawer on the left side of * consists of an upper bar at the top of the screen and a drawer on the left side of
* the screen. * the screen.
*/ */
@ -28,7 +28,6 @@ import edu.kit.typicalc.view.content.typeinferencecontent.TypeInferenceView;
@JsModule("./styles/shared-styles.js") @JsModule("./styles/shared-styles.js")
@JavaScript("./src/tex-svg-full.js") @JavaScript("./src/tex-svg-full.js")
public class MainViewImpl extends AppLayout implements MainView { public class MainViewImpl extends AppLayout implements MainView {
private static final long serialVersionUID = -2411433187835906976L; private static final long serialVersionUID = -2411433187835906976L;
/** /**
@ -48,8 +47,8 @@ public class MainViewImpl extends AppLayout implements MainView {
@Override @Override
public void displayError(final ParseError error) { public void displayError(final ParseError error) {
//TODO add error keys to bundle //TODO add error keys to bundle
final VerticalLayout container = new VerticalLayout(); final VerticalLayout container = new VerticalLayout();
final Span errorText = new Span(getTranslation("root." + error.toString())); final Span errorText = new Span(getTranslation("root." + error.toString()));
final Notification errorNotification = new Notification(); final Notification errorNotification = new Notification();
final Button closeButton = new Button(getTranslation("root.close"), event -> errorNotification.close()); final Button closeButton = new Button(getTranslation("root.close"), event -> errorNotification.close());