mirror of
https://gitlab.kit.edu/uskyk/typicalc.git
synced 2024-11-08 10:20:41 +00:00
Change type assumptions permalink format
This commit is contained in:
parent
c9cc12e922
commit
7d4c724338
@ -15,9 +15,7 @@ import com.vaadin.flow.i18n.LocaleChangeEvent;
|
|||||||
import com.vaadin.flow.i18n.LocaleChangeObserver;
|
import com.vaadin.flow.i18n.LocaleChangeObserver;
|
||||||
import org.apache.commons.lang3.tuple.Pair;
|
import org.apache.commons.lang3.tuple.Pair;
|
||||||
|
|
||||||
import java.util.*;
|
|
||||||
import java.util.function.Consumer;
|
import java.util.function.Consumer;
|
||||||
import java.util.stream.Collectors;
|
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Contains components which allow the user to enter a lambda term and start the type inference algorithm.
|
* Contains components which allow the user to enter a lambda term and start the type inference algorithm.
|
||||||
@ -41,7 +39,7 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver {
|
|||||||
|
|
||||||
private static final short MAX_INPUT_LENGTH = 1000;
|
private static final short MAX_INPUT_LENGTH = 1000;
|
||||||
|
|
||||||
private final transient Consumer<Pair<String, Map<String, String>>> callback;
|
private final transient Consumer<Pair<String, String>> callback;
|
||||||
private final Button infoIcon;
|
private final Button infoIcon;
|
||||||
private final TextField termInputField;
|
private final TextField termInputField;
|
||||||
private final AssumptionInputField assumptionInputField;
|
private final AssumptionInputField assumptionInputField;
|
||||||
@ -54,7 +52,7 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver {
|
|||||||
*
|
*
|
||||||
* @param callback Consumer to call the inferType()-method in UpperBar
|
* @param callback Consumer to call the inferType()-method in UpperBar
|
||||||
*/
|
*/
|
||||||
protected InputBar(Consumer<Pair<String, Map<String, String>>> callback) {
|
protected InputBar(Consumer<Pair<String, String>> callback) {
|
||||||
this.callback = callback;
|
this.callback = callback;
|
||||||
|
|
||||||
setId(INPUT_BAR_ID);
|
setId(INPUT_BAR_ID);
|
||||||
@ -126,7 +124,7 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver {
|
|||||||
|
|
||||||
/**
|
/**
|
||||||
* Set to provided input as the value of the termInputField and assumptionInputField.
|
* Set to provided input as the value of the termInputField and assumptionInputField.
|
||||||
*
|
*
|
||||||
* @param input pair of a term (left) and type assumptions (right)
|
* @param input pair of a term (left) and type assumptions (right)
|
||||||
*/
|
*/
|
||||||
protected void setInputAndClickTypeInfer(Pair<String, String> input) {
|
protected void setInputAndClickTypeInfer(Pair<String, String> input) {
|
||||||
@ -138,17 +136,7 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver {
|
|||||||
private void onTypeInferButtonClick() {
|
private void onTypeInferButtonClick() {
|
||||||
termInputField.blur();
|
termInputField.blur();
|
||||||
String assumptions = assumptionInputField.getValue();
|
String assumptions = assumptionInputField.getValue();
|
||||||
Map<String, String> assumptionsMap = Arrays.stream(assumptions.split(";"))
|
callback.accept(Pair.of(termInputField.getValue(), assumptions));
|
||||||
.filter(entry -> entry.length() > 0).map(entry -> {
|
|
||||||
if (entry.contains(":")) {
|
|
||||||
String[] parts = entry.split(":", 2);
|
|
||||||
return Pair.of(parts[0].trim(), parts[1].trim());
|
|
||||||
} else {
|
|
||||||
return Pair.of(entry, "");
|
|
||||||
}
|
|
||||||
}).collect(Collectors.toMap(Pair::getLeft, Pair::getRight,
|
|
||||||
(existing, replacement) -> existing, LinkedHashMap::new));
|
|
||||||
callback.accept(Pair.of(termInputField.getValue(), assumptionsMap));
|
|
||||||
}
|
}
|
||||||
|
|
||||||
private void onExampleButtonClick() {
|
private void onExampleButtonClick() {
|
||||||
|
@ -20,7 +20,6 @@ import java.net.URLDecoder;
|
|||||||
import java.net.URLEncoder;
|
import java.net.URLEncoder;
|
||||||
import java.nio.charset.StandardCharsets;
|
import java.nio.charset.StandardCharsets;
|
||||||
import java.util.*;
|
import java.util.*;
|
||||||
import java.util.stream.Collectors;
|
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Contains all the displayed components and builds the applications user interface (UI).
|
* Contains all the displayed components and builds the applications user interface (UI).
|
||||||
@ -43,6 +42,7 @@ public class MainViewImpl extends AppLayout
|
|||||||
* The title of the application
|
* The title of the application
|
||||||
*/
|
*/
|
||||||
public static final String PAGE_TITLE = "Typicalc";
|
public static final String PAGE_TITLE = "Typicalc";
|
||||||
|
private static final String ASSUMPTION_PARAMETER = "assumptions";
|
||||||
|
|
||||||
private final UpperBar upperBar;
|
private final UpperBar upperBar;
|
||||||
|
|
||||||
@ -74,10 +74,9 @@ public class MainViewImpl extends AppLayout
|
|||||||
if (url.getPath().matches(TypeInferenceView.ROUTE + "/.*")) {
|
if (url.getPath().matches(TypeInferenceView.ROUTE + "/.*")) {
|
||||||
List<String> segments = url.getSegments();
|
List<String> segments = url.getSegments();
|
||||||
String term = segments.get(segments.size() - 1);
|
String term = segments.get(segments.size() - 1);
|
||||||
String types = url.getQueryParameters().getParameters()
|
List<String> types = url.getQueryParameters().getParameters().get(ASSUMPTION_PARAMETER);
|
||||||
.entrySet().stream().map(kv -> kv.getKey() + ": " + kv.getValue().get(0))
|
String assumptions = types != null && types.size() == 1 ? types.get(0) : "";
|
||||||
.collect(Collectors.joining(", "));
|
upperBar.inferTerm(decodeURL(term), assumptions);
|
||||||
upperBar.inferTerm(decodeURL(term), types);
|
|
||||||
} else if (url.getPath().equals(TypeInferenceView.ROUTE)) {
|
} else if (url.getPath().equals(TypeInferenceView.ROUTE)) {
|
||||||
setContent(new StartPageView());
|
setContent(new StartPageView());
|
||||||
upperBar.inferTerm(StringUtils.EMPTY, "");
|
upperBar.inferTerm(StringUtils.EMPTY, "");
|
||||||
@ -86,18 +85,22 @@ public class MainViewImpl extends AppLayout
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
private void processInput(Pair<String, Map<String, String>> lambdaTermAndAssumptions) {
|
private void processInput(Pair<String, String> lambdaTermAndAssumptions) {
|
||||||
String lambdaTerm = lambdaTermAndAssumptions.getLeft();
|
String lambdaTerm = lambdaTermAndAssumptions.getLeft();
|
||||||
if (lambdaTerm.isBlank()) {
|
if (lambdaTerm.isBlank()) {
|
||||||
UI.getCurrent().navigate("./");
|
UI.getCurrent().navigate("./");
|
||||||
return;
|
return;
|
||||||
}
|
}
|
||||||
QueryParameters qp = new QueryParameters(lambdaTermAndAssumptions.getRight().entrySet().stream().map(entry ->
|
String assumptions = lambdaTermAndAssumptions.getRight();
|
||||||
Pair.of(entry.getKey(), List.of(entry.getValue()))
|
if (assumptions.isEmpty()) {
|
||||||
).collect(Collectors.toMap(Pair::getLeft, Pair::getRight,
|
UI.getCurrent().navigate(TypeInferenceView.ROUTE + "/"
|
||||||
(existing, replacement) -> existing, LinkedHashMap::new)));
|
+ URLEncoder.encode(lambdaTerm, StandardCharsets.UTF_8));
|
||||||
UI.getCurrent().navigate(TypeInferenceView.ROUTE + "/"
|
} else {
|
||||||
+ URLEncoder.encode(lambdaTerm, StandardCharsets.UTF_8), qp);
|
QueryParameters qp = new QueryParameters(
|
||||||
|
Map.of(ASSUMPTION_PARAMETER, List.of(lambdaTermAndAssumptions.getRight())));
|
||||||
|
UI.getCurrent().navigate(TypeInferenceView.ROUTE + "/"
|
||||||
|
+ URLEncoder.encode(lambdaTerm, StandardCharsets.UTF_8), qp);
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
private String decodeURL(String encodedUrl) {
|
private String decodeURL(String encodedUrl) {
|
||||||
|
@ -19,7 +19,6 @@ import edu.kit.typicalc.view.main.MainView.MainViewListener;
|
|||||||
import org.apache.commons.lang3.tuple.Pair;
|
import org.apache.commons.lang3.tuple.Pair;
|
||||||
|
|
||||||
import java.util.Locale;
|
import java.util.Locale;
|
||||||
import java.util.Map;
|
|
||||||
import java.util.function.Consumer;
|
import java.util.function.Consumer;
|
||||||
|
|
||||||
|
|
||||||
@ -48,7 +47,7 @@ public class UpperBar extends VerticalLayout implements LocaleChangeObserver {
|
|||||||
private final ItemLabelGenerator<Locale> renderer;
|
private final ItemLabelGenerator<Locale> renderer;
|
||||||
|
|
||||||
private final transient MainViewListener presenter;
|
private final transient MainViewListener presenter;
|
||||||
private final transient Consumer<Pair<String, Map<String, String>>> inputConsumer;
|
private final transient Consumer<Pair<String, String>> inputConsumer;
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Initializes a new UpperBar with the provided mainViewListener.
|
* Initializes a new UpperBar with the provided mainViewListener.
|
||||||
@ -56,7 +55,7 @@ public class UpperBar extends VerticalLayout implements LocaleChangeObserver {
|
|||||||
* @param presenter the listener used to communicate with the model
|
* @param presenter the listener used to communicate with the model
|
||||||
* @param inputConsumer function to handle user input
|
* @param inputConsumer function to handle user input
|
||||||
*/
|
*/
|
||||||
protected UpperBar(MainViewListener presenter, Consumer<Pair<String, Map<String, String>>> inputConsumer) {
|
protected UpperBar(MainViewListener presenter, Consumer<Pair<String, String>> inputConsumer) {
|
||||||
|
|
||||||
this.presenter = presenter;
|
this.presenter = presenter;
|
||||||
this.inputConsumer = inputConsumer;
|
this.inputConsumer = inputConsumer;
|
||||||
@ -90,7 +89,7 @@ public class UpperBar extends VerticalLayout implements LocaleChangeObserver {
|
|||||||
*
|
*
|
||||||
* @param termAndAssumptions the lambda term to be type-inferred and the type assumptions to use
|
* @param termAndAssumptions the lambda term to be type-inferred and the type assumptions to use
|
||||||
*/
|
*/
|
||||||
protected void typeInfer(Pair<String, Map<String, String>> termAndAssumptions) {
|
protected void typeInfer(Pair<String, String> termAndAssumptions) {
|
||||||
inputConsumer.accept(termAndAssumptions);
|
inputConsumer.accept(termAndAssumptions);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user