arnekeller/Typicalc
1
0
Fork 0
mirror of https://gitlab.kit.edu/uskyk/typicalc.git synced 2024-11-08 18:30:42 +00:00
Code Issues Packages Projects Releases Wiki Activity

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

Browse Source
This commit is contained in:
Johanna Stuber 2021-02-21 11:38:49 +01:00
commit fd8638164f
6 changed files with 47 additions and 25 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
frontend/styles/view/image-slide.css
View File

@ -1,8 +1,7 @@
#slideLayout {
align-items: center;
justify-content: center;
padding-top: 0;
padding-bottom: 0;
padding: 0;
}
#explanation {

17
frontend/styles/view/start-page.css
View File

@ -6,21 +6,22 @@
#horizontalLine {
align-self: center;
width: 50%;
width: 55em;
max-width: 100%;
min-height: 1px;
}
#introduction {
width: 50%;
#textContainer {
max-width: 55em;
}
#linkContainer {
width: 50%;
margin-top: 0;
margin: 0;
}
#slideProgress {
width: 50%;
width: 55em;
max-width: 100%;
margin-top: 30px;
margin-bottom: 0;
}
@ -35,12 +36,10 @@
display: flex;
justify-content: center;
align-items: center;
overflow: hidden;
height: 100%;
width: 100%;
}
#slideShow {
height: 500px;
width: 100vw;
width: 100%;
}

7
src/main/java/edu/kit/typicalc/model/parser/LambdaParser.java
View File

@ -19,7 +19,7 @@ import java.util.Set;
*
* @see LambdaTerm
*/
public class LambdaParser { // TODO: document syntax above ^ ?
public class LambdaParser {
/**
* lexer to translate a String into tokens
*/
@ -152,10 +152,13 @@ public class LambdaParser { // TODO: document syntax above ^ ?
if (left.isError()) {
return left;
}
while (ATOM_START_TOKENS.contains(token.getType()) || token.getType() == TokenType.LAMBDA) {
while (ATOM_START_TOKENS.contains(token.getType())
|| token.getType() == TokenType.LAMBDA || token.getType() == TokenType.LET) {
Result<LambdaTerm, ParseError> atom;
if (token.getType() == TokenType.LAMBDA) {
atom = new Result<>(parseAbstraction());
} else if (token.getType() == TokenType.LET) {
atom = new Result<>(parseLet());
} else {
atom = parseAtom();
}

22
src/main/java/edu/kit/typicalc/view/content/infocontent/StartPageView.java
View File

@ -6,8 +6,10 @@ import com.vaadin.flow.component.Text;
import com.vaadin.flow.component.dependency.CssImport;
import com.vaadin.flow.component.dependency.JsModule;
import com.vaadin.flow.component.html.Anchor;
import com.vaadin.flow.component.html.Div;
import com.vaadin.flow.component.html.H1;
import com.vaadin.flow.component.html.Hr;
import com.vaadin.flow.component.html.Paragraph;
import com.vaadin.flow.component.html.Span;
import com.vaadin.flow.component.orderedlayout.VerticalLayout;
import com.vaadin.flow.component.progressbar.ProgressBar;
@ -32,7 +34,7 @@ public class StartPageView extends VerticalLayout implements ControlPanelView, L
private static final String HEADING_ID = "startPage-Heading";
private static final String H_LINE_ID = "horizontalLine";
private static final String INTRODUCTION_ID = "introduction";
private static final String TEXT_CONTAINER_ID = "textContainer";
private static final String LINK_CONTAINER_ID = "linkContainer";
private static final String SLIDE_PROGRESS_ID = "slideProgress";
private static final String CONTROL_PANEL_ID = "controlPanel";
@ -41,7 +43,6 @@ public class StartPageView extends VerticalLayout implements ControlPanelView, L
private static final String DOT = ".";
private final ControlPanel controlPanel;
private final Span introduction;
private final Carousel slideShow;
private final ProgressBar slideProgress;
@ -52,11 +53,11 @@ public class StartPageView extends VerticalLayout implements ControlPanelView, L
* Fills the view with content.
*/
public StartPageView() {
controlPanel = new ControlPanel(this, this);
ControlPanel controlPanel = new ControlPanel(this, this);
controlPanel.setId(CONTROL_PANEL_ID);
controlPanel.setEnabledShareButton(false);
slideShow = createSzenarioCarousel();
slideShow = createScenarioCarousel();
slideShow.setId(SLIDE_SHOW_ID);
H1 heading = new H1(getTranslation("root.typicalc"));
@ -65,23 +66,26 @@ public class StartPageView extends VerticalLayout implements ControlPanelView, L
line1.setId(H_LINE_ID);
Hr line2 = new Hr();
line2.setId(H_LINE_ID);
introduction = new Span(getTranslation("root.slideExp"));
introduction.setId(INTRODUCTION_ID);
Div textContainer = new Div();
textContainer.setId(TEXT_CONTAINER_ID);
introduction = new Span();
linkText = new Text(getTranslation("root.linkText"));
link = new Anchor(getTranslation("root.link"), getTranslation("root.here"));
link.setTarget("_blank"); // opens new tab
Span linkContainer = new Span(linkText, link, new Text(DOT));
Paragraph linkContainer = new Paragraph(linkText, link, new Text(DOT));
linkContainer.setId(LINK_CONTAINER_ID);
textContainer.add(introduction, linkContainer);
slideProgress = new ProgressBar(slideShow.getStartPosition(), slideShow.getSlides().length - 1);
slideProgress.setId(SLIDE_PROGRESS_ID);
add(heading, line1, introduction, linkContainer, slideProgress, slideShow, line2, controlPanel);
add(heading, line1, textContainer, slideProgress, slideShow, line2, controlPanel);
setId(START_PAGE_ID);
}
private Carousel createSzenarioCarousel() {
private Carousel createScenarioCarousel() {
Slide slide1 = new ImageSlide(getTranslation("root.image1"), "root.text1");
Slide slide2 = new ImageSlide(getTranslation("root.image2"), "root.text2");
Slide slide3 = new ImageSlide(getTranslation("root.image3"), "root.text3");

1
src/main/java/edu/kit/typicalc/view/main/TypeAssumptionsArea.java
View File

@ -73,7 +73,6 @@ public class TypeAssumptionsArea extends Dialog implements LocaleChangeObserver
initializeWithAssumptions(types);
layout.add(heading, buttons, assumptionContainer);
add(layout);
setCloseOnOutsideClick(false);
}
/**

18
src/test/java/edu/kit/typicalc/model/parser/LambdaParserTest.java
View File

@ -10,6 +10,7 @@ import static org.junit.jupiter.api.Assertions.assertEquals;
class LambdaParserTest {
private static final VarTerm X = new VarTerm("x");
private static final VarTerm Y = new VarTerm("y");
@Test
void varTerm() {
@ -155,6 +156,23 @@ class LambdaParserTest {
assertEquals(new AppTerm(new AbsTerm(X, X), new AbsTerm(X, X)), term.unwrap());
}
@Test
void bugFoundByJohanna() {
// original term: (λx.λy.y (x y)) (λz. λa. z g a) let f = λx. let g = λy. y in g x in f 3
// reduced:
LambdaParser parser = new LambdaParser("(λx.x) let id = λy.y in id");
Result<LambdaTerm, ParseError> term = parser.parse();
if (term.isError()) {
System.err.println(term.unwrapError());
System.err.println(term.unwrapError().getCause());
}
assertEquals(new AppTerm(
new AbsTerm(X, X),
new LetTerm(new VarTerm("id"), new AbsTerm(Y, Y), new VarTerm("id"))
),
term.unwrap());
}
@Test
void complicatedIdentity() {
LambdaParser parser = new LambdaParser("(λx. x) (λx. x) λx. x");