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

Browse Source
This commit is contained in:
me 2021-01-28 01:12:09 +01:00
commit 93882c2f0b
19 changed files with 209 additions and 72 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
frontend/src/copy-to-clipboard.js Normal file
View File

@ -0,0 +1,10 @@
window.copyToClipboard = (str) => {
const textarea = document.createElement("textarea");
textarea.value = str;
textarea.style.position = "absolute";
textarea.style.opacity = "0";
document.body.appendChild(textarea);
textarea.select();
document.execCommand("copy");
document.body.removeChild(textarea);
};

42
src/main/java/edu/kit/typicalc/model/Tree.java
View File

@ -1,6 +1,9 @@
package edu.kit.typicalc.model;
import edu.kit.typicalc.model.step.InferenceStep;
import edu.kit.typicalc.model.step.StepFactory;
import edu.kit.typicalc.model.step.StepFactoryDefault;
import edu.kit.typicalc.model.step.StepFactoryWithLet;
import edu.kit.typicalc.model.term.AbsTerm;
import edu.kit.typicalc.model.term.AppTerm;
import edu.kit.typicalc.model.term.ConstTerm;
@ -10,9 +13,9 @@ import edu.kit.typicalc.model.term.TermVisitorTree;
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.ArrayList;
import java.util.List;
import java.util.Map;
@ -24,6 +27,13 @@ import java.util.Map;
*/
public class Tree implements TermVisitorTree {
private final TypeVariableFactory typeVarFactory;
private final StepFactory stepFactory;
private final TypeVariable firstTypeVariable;
private final InferenceStep firstInferenceStep;
private final List<Constraint> constraints;
/**
* Initializes a new Tree representing the proof tree for the type inference of the given
* lambda term considering the given type assumptions. The inference step structure
@ -33,7 +43,7 @@ public class Tree implements TermVisitorTree {
* @param lambdaTerm the lambda term to generate the tree for
*/
protected Tree(Map<VarTerm, TypeAbstraction> typeAssumptions, LambdaTerm lambdaTerm) {
// TODO
this(typeAssumptions, lambdaTerm, new TypeVariableFactory());
}
/**
@ -49,7 +59,14 @@ public class Tree implements TermVisitorTree {
*/
protected Tree(Map<VarTerm, TypeAbstraction> typeAssumptions, LambdaTerm lambdaTerm,
TypeVariableFactory typeVariableFactory) {
// TODO
// TODO: null checks
this.typeVarFactory = typeVariableFactory;
this.constraints = new ArrayList<>();
this.stepFactory = lambdaTerm.hasLet() ? new StepFactoryWithLet() : new StepFactoryDefault();
this.firstTypeVariable = typeVarFactory.nextTypeVariable();
this.firstInferenceStep = lambdaTerm.accept(this, typeAssumptions, firstTypeVariable);
}
/**
@ -60,8 +77,7 @@ public class Tree implements TermVisitorTree {
* @return the first inference step of the tree
*/
protected InferenceStep getFirstInferenceStep() {
return null;
// TODO;
return firstInferenceStep;
}
/**
@ -70,8 +86,7 @@ public class Tree implements TermVisitorTree {
* @return the first type variable
*/
protected TypeVariable getFirstTypeVariable() {
return null;
// TODO;
return firstTypeVariable;
}
/**
@ -81,32 +96,31 @@ public class Tree implements TermVisitorTree {
* @return the constraint list of the tree
*/
protected List<Constraint> getConstraints() {
return null;
// TODO
return constraints;
}
@Override
public InferenceStep visit(AppTerm appTerm, List<TypeAssumption> typeAssumptions, Type conclusionType) {
public InferenceStep visit(AppTerm appTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType) {
return null; // TODO
}
@Override
public InferenceStep visit(AbsTerm absTerm, List<TypeAssumption> typeAssumptions, Type conclusionType) {
public InferenceStep visit(AbsTerm absTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType) {
return null; // TODO
}
@Override
public InferenceStep visit(LetTerm letTerm, List<TypeAssumption> typeAssumptions, Type conclusionType) {
public InferenceStep visit(LetTerm letTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType) {
return null; // TODO
}
@Override
public InferenceStep visit(ConstTerm constTerm, List<TypeAssumption> typeAssumptions, Type conclusionType) {
public InferenceStep visit(ConstTerm constTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType) {
return null; // TODO
}
@Override
public InferenceStep visit(VarTerm varTerm, List<TypeAssumption> typeAssumptions, Type conclusionType) {
public InferenceStep visit(VarTerm varTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType) {
return null; // TODO
}
}

1
src/main/java/edu/kit/typicalc/model/TypeInferer.java
View File

@ -32,6 +32,7 @@ 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: null checks
tree = new Tree(typeAssumptions, lambdaTerm);
// TODO: Abbrechen bei fehlgeschlagener let-Teilinferenz, evtl. getUnificationSteps() anpassen

11
src/main/java/edu/kit/typicalc/model/term/AbsTerm.java
View File

@ -1,5 +1,10 @@
package edu.kit.typicalc.model.term;
import edu.kit.typicalc.model.step.InferenceStep;
import edu.kit.typicalc.model.type.Type;
import edu.kit.typicalc.model.type.TypeAbstraction;
import java.util.Map;
import java.util.Objects;
/**
@ -44,6 +49,12 @@ public class AbsTerm extends LambdaTerm {
termVisitor.visit(this);
}
@Override
public InferenceStep accept(TermVisitorTree termVisitorTree, Map<VarTerm, TypeAbstraction> assumptions, Type type) {
//todo implement
return null;
}
@Override
public boolean equals(Object o) {
if (this == o) {

11
src/main/java/edu/kit/typicalc/model/term/AppTerm.java
View File

@ -1,5 +1,10 @@
package edu.kit.typicalc.model.term;
import edu.kit.typicalc.model.step.InferenceStep;
import edu.kit.typicalc.model.type.Type;
import edu.kit.typicalc.model.type.TypeAbstraction;
import java.util.Map;
import java.util.Objects;
public class AppTerm extends LambdaTerm {
@ -29,6 +34,12 @@ public class AppTerm extends LambdaTerm {
termVisitor.visit(this);
}
@Override
public InferenceStep accept(TermVisitorTree termVisitorTree, Map<VarTerm, TypeAbstraction> assumptions, Type type) {
// todo implement
return null;
}
@Override
public boolean equals(Object o) {
if (this == o) {

12
src/main/java/edu/kit/typicalc/model/term/ConstTerm.java
View File

@ -1,5 +1,11 @@
package edu.kit.typicalc.model.term;
import edu.kit.typicalc.model.step.InferenceStep;
import edu.kit.typicalc.model.type.Type;
import edu.kit.typicalc.model.type.TypeAbstraction;
import java.util.Map;
public class ConstTerm extends LambdaTerm {
@Override
public boolean hasLet() {
@ -10,4 +16,10 @@ public class ConstTerm extends LambdaTerm {
public void accept(TermVisitor termVisitor) {
termVisitor.visit(this);
}
@Override
public InferenceStep accept(TermVisitorTree termVisitorTree, Map<VarTerm, TypeAbstraction> assumptions, Type type) {
// todo implment
return null;
}
}

10
src/main/java/edu/kit/typicalc/model/term/LambdaTerm.java
View File

@ -1,5 +1,11 @@
package edu.kit.typicalc.model.term;
import edu.kit.typicalc.model.step.InferenceStep;
import edu.kit.typicalc.model.type.Type;
import edu.kit.typicalc.model.type.TypeAbstraction;
import java.util.Map;
public abstract class LambdaTerm {
/**
* @return whether the lambda term contains a let expression
@ -11,4 +17,8 @@ public abstract class LambdaTerm {
* @param termVisitor a visitor
*/
public abstract void accept(TermVisitor termVisitor);
public abstract InferenceStep accept(TermVisitorTree termVisitorTree,
Map<VarTerm, TypeAbstraction> assumptions, Type type);
}

12
src/main/java/edu/kit/typicalc/model/term/LetTerm.java
View File

@ -1,5 +1,11 @@
package edu.kit.typicalc.model.term;
import edu.kit.typicalc.model.step.InferenceStep;
import edu.kit.typicalc.model.type.Type;
import edu.kit.typicalc.model.type.TypeAbstraction;
import java.util.Map;
public class LetTerm extends LambdaTerm {
public LetTerm(VarTerm var, LambdaTerm def, LambdaTerm body) {
}
@ -13,4 +19,10 @@ public class LetTerm extends LambdaTerm {
public void accept(TermVisitor termVisitor) {
termVisitor.visit(this);
}
@Override
public InferenceStep accept(TermVisitorTree termVisitorTree, Map<VarTerm, TypeAbstraction> assumptions, Type type) {
//todo implement
return null;
}
}

14
src/main/java/edu/kit/typicalc/model/term/TermVisitorTree.java
View File

@ -2,9 +2,9 @@ package edu.kit.typicalc.model.term;
import edu.kit.typicalc.model.step.InferenceStep;
import edu.kit.typicalc.model.type.Type;
import edu.kit.typicalc.model.type.TypeAssumption;
import edu.kit.typicalc.model.type.TypeAbstraction;
import java.util.List;
import java.util.Map;
public interface TermVisitorTree {
/**
@ -19,7 +19,7 @@ public interface TermVisitorTree {
* of the returned inference step will be assigned
* @return an {@link edu.kit.typicalc.model.step.AppStep}
*/
InferenceStep visit(AppTerm appTerm, List<TypeAssumption> typeAssumptions, Type conclusionType);
InferenceStep visit(AppTerm appTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType);
/**
* Returns an {@link edu.kit.typicalc.model.step.AbsStep} suiting the given abstraction (lambda term)
@ -33,7 +33,7 @@ public interface TermVisitorTree {
* of the returned inference step will be assigned
* @return an {@link edu.kit.typicalc.model.step.AbsStep}
*/
InferenceStep visit(AbsTerm absTerm, List<TypeAssumption> typeAssumptions, Type conclusionType);
InferenceStep visit(AbsTerm absTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType);
/**
* Returns an {@link edu.kit.typicalc.model.step.LetStep} suiting the given let expression (lambda term)
@ -47,7 +47,7 @@ public interface TermVisitorTree {
* of the returned inference step will be assigned
* @return an {@link edu.kit.typicalc.model.step.LetStep}
*/
InferenceStep visit(LetTerm letTerm, List<TypeAssumption> typeAssumptions, Type conclusionType);
InferenceStep visit(LetTerm letTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType);
/**
* Returns an {@link edu.kit.typicalc.model.step.ConstStep} suiting the given constant
@ -61,7 +61,7 @@ public interface TermVisitorTree {
* of the returned inference step will be assigned
* @return an {@link edu.kit.typicalc.model.step.ConstStep}
*/
InferenceStep visit(ConstTerm constTerm, List<TypeAssumption> typeAssumptions, Type conclusionType);
InferenceStep visit(ConstTerm constTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType);
/**
* Returns an {@link edu.kit.typicalc.model.step.VarStep} suiting the given variable (lambda term)
@ -75,5 +75,5 @@ public interface TermVisitorTree {
* of the returned inference step will be assigned
* @return an {@link edu.kit.typicalc.model.step.VarStep}
*/
InferenceStep visit(VarTerm varTerm, List<TypeAssumption> typeAssumptions, Type conclusionType);
InferenceStep visit(VarTerm varTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType);
}

11
src/main/java/edu/kit/typicalc/model/term/VarTerm.java
View File

@ -1,5 +1,10 @@
package edu.kit.typicalc.model.term;
import edu.kit.typicalc.model.step.InferenceStep;
import edu.kit.typicalc.model.type.Type;
import edu.kit.typicalc.model.type.TypeAbstraction;
import java.util.Map;
import java.util.Objects;
public class VarTerm extends LambdaTerm {
@ -20,6 +25,12 @@ public class VarTerm extends LambdaTerm {
termVisitor.visit(this);
}
@Override
public InferenceStep accept(TermVisitorTree termVisitorTree, Map<VarTerm, TypeAbstraction> assumptions, Type type) {
//todo implement
return null;
}
@Override
public boolean equals(Object o) {
if (this == o) {

4
src/main/java/edu/kit/typicalc/model/type/TypeAssumption.java
View File

@ -1,4 +0,0 @@
package edu.kit.typicalc.model.type;
public class TypeAssumption {
}

2
src/main/java/edu/kit/typicalc/model/type/TypeVariable.java
View File

@ -1,6 +1,6 @@
package edu.kit.typicalc.model.type;
public class TypeVariable {
public class TypeVariable extends Type {
public TypeVariable(int index) {
}

10
src/main/java/edu/kit/typicalc/view/main/DrawerContent.java Normal file
View File

@ -0,0 +1,10 @@
package edu.kit.typicalc.view.main;
import com.vaadin.flow.component.orderedlayout.VerticalLayout;
public class DrawerContent extends VerticalLayout {
public DrawerContent() {
//TODO implement
}
}

30
src/main/java/edu/kit/typicalc/view/main/InferenceRuleField.java Normal file
View File

@ -0,0 +1,30 @@
package edu.kit.typicalc.view.main;
import com.vaadin.flow.component.UI;
import com.vaadin.flow.component.button.Button;
import com.vaadin.flow.component.dependency.JsModule;
import com.vaadin.flow.component.html.Div;
import com.vaadin.flow.i18n.LocaleChangeEvent;
import com.vaadin.flow.i18n.LocaleChangeObserver;
@JsModule(".src/copy-to-clipboard.js")
public class InferenceRuleField extends Div implements LocaleChangeObserver {
private final String latex;
private final String nameKey;
private final Button copyButton;
public InferenceRuleField(final String latex, final String nameKey) {
this.latex = latex;
this.nameKey = nameKey;
this.copyButton = new Button(getTranslation("root.copyLatex"),
event -> UI.getCurrent().getPage().executeJs("window.copyToClipboard($0)", latex));
}
@Override
public void localeChange(LocaleChangeEvent event) {
copyButton.setText(getTranslation("root.copyLatex"));
//TODO use nameKey to change name of rule, when attribute is created
}
}

19
src/main/java/edu/kit/typicalc/view/main/InputBar.java Normal file
View File

@ -0,0 +1,19 @@
package edu.kit.typicalc.view.main;
import com.vaadin.flow.component.orderedlayout.HorizontalLayout;
import com.vaadin.flow.i18n.LocaleChangeEvent;
import com.vaadin.flow.i18n.LocaleChangeObserver;
public class InputBar extends HorizontalLayout implements LocaleChangeObserver {
public InputBar() {
//TODO implement
}
@Override
public void localeChange(LocaleChangeEvent event) {
// TODO Auto-generated method stub
}
}

40
src/main/java/edu/kit/typicalc/view/main/MainViewImpl.java
View File

@ -38,14 +38,12 @@ import java.util.Optional;
@JsModule("./styles/shared-styles.js")
public class MainViewImpl extends AppLayout implements MainView {
private final Tabs menu;
private H1 viewTitle;
public MainViewImpl() {
setDrawerOpened(false);
addToNavbar(true, createHeaderContent());
menu = createMenu();
addToDrawer(createDrawerContent(menu));
addToNavbar(true, new UpperBar());
addToDrawer(new DrawerContent());
}
private Component createHeaderContent() {
@ -78,38 +76,6 @@ public class MainViewImpl extends AppLayout implements MainView {
return layout;
}
private Tabs createMenu() {
final Tabs tabs = new Tabs();
tabs.setOrientation(Tabs.Orientation.VERTICAL);
tabs.addThemeVariants(TabsVariant.LUMO_MINIMAL);
tabs.setId("tabs");
return tabs;
}
private static Tab createTab(String text, Class<? extends Component> navigationTarget) {
final Tab tab = new Tab();
tab.add(new RouterLink(text, navigationTarget));
ComponentUtil.setData(tab, Class.class, navigationTarget);
return tab;
}
@Override
protected void afterNavigation() {
super.afterNavigation();
getTabForComponent(getContent()).ifPresent(menu::setSelectedTab);
viewTitle.setText(getCurrentPageTitle());
}
private Optional<Tab> getTabForComponent(Component component) {
return menu.getChildren().filter(tab -> ComponentUtil.getData(tab, Class.class).equals(component.getClass()))
.findFirst().map(Tab.class::cast);
}
private String getCurrentPageTitle() {
return getContent().getClass().getAnnotation(PageTitle.class).value();
}
@Override
public void setTypeInferenceView(final TypeInfererInterface typeInferer) {
this.getUI().ifPresent(ui -> ui.navigate(TypeInferenceView.class, typeInferer));

18
src/main/java/edu/kit/typicalc/view/main/UpperBar.java Normal file
View File

@ -0,0 +1,18 @@
package edu.kit.typicalc.view.main;
import com.vaadin.flow.component.orderedlayout.HorizontalLayout;
import com.vaadin.flow.i18n.LocaleChangeEvent;
import com.vaadin.flow.i18n.LocaleChangeObserver;
public class UpperBar extends HorizontalLayout implements LocaleChangeObserver {
public UpperBar() {
//TODO implement
}
@Override
public void localeChange(LocaleChangeEvent event) {
// TODO Auto-generated method stub
}
}

20
src/main/resources/language/translation_de.properties
View File

@ -1,10 +1,14 @@
abs-rule=\
\\begin{prooftree}\n\
\\AxiomC{$\\Gamma=\\vdash t_1 : \\tau_1 \\rightarrow \\tau_2$}\n\
\\AxiomC{$\\Gamma \\vdash t_2 : \\tau_1$}\n\
\n\
\\LeftLabel{APP}\n\
\\BinaryInfC{$\\Gamma \\vdash t_1 \\ t_2 : \\tau_2$}\n\
root.close=Schlie<EFBFBD>en
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
test=hello world

4
src/main/resources/language/translation_en.properties
View File

@ -7,4 +7,6 @@ abs-rule=\
\\BinaryInfC{$\\Gamma \\vdash t_1 \\ t_2 : \\tau_2$}\n\
\\end{prooftree}
test=hello world
test=hello world
root.close=Close
root.copyLatex=Copy latex code