mirror of
https://gitlab.kit.edu/uskyk/typicalc.git
synced 2024-11-08 18:30:42 +00:00
merge
This commit is contained in:
commit
0eefcd71ad
16
package.json
16
package.json
@ -1,5 +1,5 @@
|
|||||||
{
|
{
|
||||||
"name": "no-name",
|
"name": "typicalc",
|
||||||
"license": "UNLICENSED",
|
"license": "UNLICENSED",
|
||||||
"dependencies": {
|
"dependencies": {
|
||||||
"@polymer/iron-icon": "3.0.1",
|
"@polymer/iron-icon": "3.0.1",
|
||||||
@ -7,17 +7,12 @@
|
|||||||
"@polymer/polymer": "3.2.0",
|
"@polymer/polymer": "3.2.0",
|
||||||
"@vaadin/flow-frontend": "./target/flow-frontend",
|
"@vaadin/flow-frontend": "./target/flow-frontend",
|
||||||
"@vaadin/router": "1.7.2",
|
"@vaadin/router": "1.7.2",
|
||||||
"@vaadin/vaadin-accordion": "1.2.0",
|
|
||||||
"@vaadin/vaadin-app-layout": "2.2.0",
|
"@vaadin/vaadin-app-layout": "2.2.0",
|
||||||
"@vaadin/vaadin-board": "2.2.0",
|
|
||||||
"@vaadin/vaadin-button": "2.4.0",
|
"@vaadin/vaadin-button": "2.4.0",
|
||||||
"@vaadin/vaadin-charts": "7.0.0",
|
"@vaadin/vaadin-charts": "7.0.0",
|
||||||
"@vaadin/vaadin-checkbox": "2.5.0",
|
|
||||||
"@vaadin/vaadin-combo-box": "5.4.7",
|
"@vaadin/vaadin-combo-box": "5.4.7",
|
||||||
"@vaadin/vaadin-confirm-dialog": "1.3.0",
|
"@vaadin/vaadin-confirm-dialog": "1.3.0",
|
||||||
"@vaadin/vaadin-context-menu": "4.5.0",
|
|
||||||
"@vaadin/vaadin-core-shrinkwrap": "18.0.5",
|
"@vaadin/vaadin-core-shrinkwrap": "18.0.5",
|
||||||
"@vaadin/vaadin-crud": "1.3.0",
|
|
||||||
"@vaadin/vaadin-custom-field": "1.3.0",
|
"@vaadin/vaadin-custom-field": "1.3.0",
|
||||||
"@vaadin/vaadin-date-picker": "4.4.1",
|
"@vaadin/vaadin-date-picker": "4.4.1",
|
||||||
"@vaadin/vaadin-details": "1.2.0",
|
"@vaadin/vaadin-details": "1.2.0",
|
||||||
@ -28,17 +23,15 @@
|
|||||||
"@vaadin/vaadin-icons": "4.3.2",
|
"@vaadin/vaadin-icons": "4.3.2",
|
||||||
"@vaadin/vaadin-item": "2.3.0",
|
"@vaadin/vaadin-item": "2.3.0",
|
||||||
"@vaadin/vaadin-list-box": "1.4.0",
|
"@vaadin/vaadin-list-box": "1.4.0",
|
||||||
"@vaadin/vaadin-lumo-styles": "1.6.0",
|
"@vaadin/vaadin-lumo-styles": "1.6.1",
|
||||||
"@vaadin/vaadin-material-styles": "1.3.2",
|
"@vaadin/vaadin-material-styles": "1.3.2",
|
||||||
"@vaadin/vaadin-menu-bar": "1.2.1",
|
"@vaadin/vaadin-menu-bar": "1.2.1",
|
||||||
"@vaadin/vaadin-notification": "1.6.0",
|
"@vaadin/vaadin-notification": "1.6.0",
|
||||||
"@vaadin/vaadin-ordered-layout": "1.4.0",
|
"@vaadin/vaadin-ordered-layout": "1.4.0",
|
||||||
"@vaadin/vaadin-progress-bar": "1.3.0",
|
"@vaadin/vaadin-progress-bar": "1.3.0",
|
||||||
"@vaadin/vaadin-radio-button": "1.5.1",
|
|
||||||
"@vaadin/vaadin-select": "2.4.0",
|
"@vaadin/vaadin-select": "2.4.0",
|
||||||
"@vaadin/vaadin-shrinkwrap": "18.0.5",
|
"@vaadin/vaadin-shrinkwrap": "18.0.5",
|
||||||
"@vaadin/vaadin-split-layout": "4.3.0",
|
"@vaadin/vaadin-split-layout": "4.3.0",
|
||||||
"@vaadin/vaadin-tabs": "3.2.0",
|
|
||||||
"@vaadin/vaadin-text-field": "2.8.2",
|
"@vaadin/vaadin-text-field": "2.8.2",
|
||||||
"lit-element": "2.3.1",
|
"lit-element": "2.3.1",
|
||||||
"@vaadin/form": "./target/flow-frontend/form",
|
"@vaadin/form": "./target/flow-frontend/form",
|
||||||
@ -74,7 +67,6 @@
|
|||||||
"@vaadin/router": "1.7.2",
|
"@vaadin/router": "1.7.2",
|
||||||
"@polymer/polymer": "3.2.0",
|
"@polymer/polymer": "3.2.0",
|
||||||
"@webcomponents/webcomponentsjs": "^2.2.10",
|
"@webcomponents/webcomponentsjs": "^2.2.10",
|
||||||
"@vaadin/vaadin-crud": "1.3.0",
|
|
||||||
"@vaadin/vaadin-grid": "5.7.7",
|
"@vaadin/vaadin-grid": "5.7.7",
|
||||||
"@vaadin/vaadin-icons": "4.3.2",
|
"@vaadin/vaadin-icons": "4.3.2",
|
||||||
"@vaadin/vaadin-split-layout": "4.3.0",
|
"@vaadin/vaadin-split-layout": "4.3.0",
|
||||||
@ -84,7 +76,6 @@
|
|||||||
"@vaadin/vaadin-select": "2.4.0",
|
"@vaadin/vaadin-select": "2.4.0",
|
||||||
"@vaadin/vaadin-app-layout": "2.2.0",
|
"@vaadin/vaadin-app-layout": "2.2.0",
|
||||||
"@vaadin/vaadin-item": "2.3.0",
|
"@vaadin/vaadin-item": "2.3.0",
|
||||||
"@vaadin/vaadin-board": "2.2.0",
|
|
||||||
"@vaadin/vaadin-notification": "1.6.0",
|
"@vaadin/vaadin-notification": "1.6.0",
|
||||||
"@vaadin/vaadin-grid-pro": "2.2.2",
|
"@vaadin/vaadin-grid-pro": "2.2.2",
|
||||||
"@vaadin/vaadin-progress-bar": "1.3.0",
|
"@vaadin/vaadin-progress-bar": "1.3.0",
|
||||||
@ -97,12 +88,9 @@
|
|||||||
"@polymer/iron-list": "3.1.0",
|
"@polymer/iron-list": "3.1.0",
|
||||||
"@vaadin/vaadin-confirm-dialog": "1.3.0",
|
"@vaadin/vaadin-confirm-dialog": "1.3.0",
|
||||||
"@vaadin/vaadin-list-box": "1.4.0",
|
"@vaadin/vaadin-list-box": "1.4.0",
|
||||||
"@vaadin/vaadin-checkbox": "2.5.0",
|
|
||||||
"@vaadin/vaadin-details": "1.2.0",
|
"@vaadin/vaadin-details": "1.2.0",
|
||||||
"@polymer/iron-icon": "3.0.1",
|
"@polymer/iron-icon": "3.0.1",
|
||||||
"@vaadin/vaadin-context-menu": "4.5.0",
|
"@vaadin/vaadin-context-menu": "4.5.0",
|
||||||
"@vaadin/vaadin-tabs": "3.2.0",
|
|
||||||
"@vaadin/vaadin-radio-button": "1.5.1",
|
|
||||||
"@vaadin/vaadin-lumo-styles": "1.6.0",
|
"@vaadin/vaadin-lumo-styles": "1.6.0",
|
||||||
"@vaadin/vaadin-material-styles": "1.3.2",
|
"@vaadin/vaadin-material-styles": "1.3.2",
|
||||||
"@vaadin/vaadin-custom-field": "1.3.0",
|
"@vaadin/vaadin-custom-field": "1.3.0",
|
||||||
|
@ -13,6 +13,10 @@ import java.util.Map;
|
|||||||
*/
|
*/
|
||||||
public class Conclusion {
|
public class Conclusion {
|
||||||
|
|
||||||
|
private final Map<VarTerm, TypeAbstraction> typeAssumptions;
|
||||||
|
private final LambdaTerm lambdaTerm;
|
||||||
|
private final Type type;
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Initializes a new Conclusion with the given type assumptions, lambda term and type.
|
* Initializes a new Conclusion with the given type assumptions, lambda term and type.
|
||||||
*
|
*
|
||||||
@ -21,30 +25,30 @@ public class Conclusion {
|
|||||||
* @param type the type assigned to the lambda term in the conclusion
|
* @param type the type assigned to the lambda term in the conclusion
|
||||||
*/
|
*/
|
||||||
protected Conclusion(Map<VarTerm, TypeAbstraction> typeAssumptions, LambdaTerm lambdaTerm, Type type) {
|
protected Conclusion(Map<VarTerm, TypeAbstraction> typeAssumptions, LambdaTerm lambdaTerm, Type type) {
|
||||||
// TODO
|
// TODO: null checks?
|
||||||
|
this.typeAssumptions = typeAssumptions;
|
||||||
|
this.lambdaTerm = lambdaTerm;
|
||||||
|
this.type = type;
|
||||||
}
|
}
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* @return the type assumptions used in the conclusion
|
* @return the type assumptions used in the conclusion
|
||||||
*/
|
*/
|
||||||
public Map<VarTerm, TypeAbstraction> getTypeAssumptions() {
|
public Map<VarTerm, TypeAbstraction> getTypeAssumptions() {
|
||||||
return null;
|
return typeAssumptions;
|
||||||
// TODO
|
|
||||||
}
|
}
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* @return the lambda term in the conclusion
|
* @return the lambda term in the conclusion
|
||||||
*/
|
*/
|
||||||
public LambdaTerm getLambdaTerm() {
|
public LambdaTerm getLambdaTerm() {
|
||||||
return null;
|
return lambdaTerm;
|
||||||
// TODO
|
|
||||||
}
|
}
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* @return the type assigned to the lambda term in the conclusion
|
* @return the type assigned to the lambda term in the conclusion
|
||||||
*/
|
*/
|
||||||
public Type getType() {
|
public Type getType() {
|
||||||
return null;
|
return type;
|
||||||
// TODO
|
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
@ -6,6 +6,10 @@ import edu.kit.typicalc.model.type.Type;
|
|||||||
* Constrains two types to be equal.
|
* Constrains two types to be equal.
|
||||||
*/
|
*/
|
||||||
public class Constraint {
|
public class Constraint {
|
||||||
|
|
||||||
|
private final Type a;
|
||||||
|
private final Type b;
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Creates a new constraint using the two types.
|
* Creates a new constraint using the two types.
|
||||||
*
|
*
|
||||||
@ -13,23 +17,23 @@ public class Constraint {
|
|||||||
* @param b second type
|
* @param b second type
|
||||||
*/
|
*/
|
||||||
public Constraint(Type a, Type b) {
|
public Constraint(Type a, Type b) {
|
||||||
// TODO
|
// TODO: null checks?
|
||||||
|
this.a = a;
|
||||||
|
this.b = b;
|
||||||
}
|
}
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* @return the first type
|
* @return the first type
|
||||||
*/
|
*/
|
||||||
public Type getFirstType() {
|
public Type getFirstType() {
|
||||||
return null;
|
return a;
|
||||||
// TODO
|
|
||||||
}
|
}
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* @return the second type
|
* @return the second type
|
||||||
*/
|
*/
|
||||||
public Type getSecondType() {
|
public Type getSecondType() {
|
||||||
return null;
|
return b;
|
||||||
// TODO
|
|
||||||
}
|
}
|
||||||
|
|
||||||
}
|
}
|
||||||
|
@ -7,6 +7,10 @@ import edu.kit.typicalc.model.type.TypeVariable;
|
|||||||
* A substitution specifies that some type should be replaced by a different type.
|
* A substitution specifies that some type should be replaced by a different type.
|
||||||
*/
|
*/
|
||||||
public class Substitution {
|
public class Substitution {
|
||||||
|
|
||||||
|
private final TypeVariable a;
|
||||||
|
private final Type b;
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Creates a new substitution using a type variable a and a type b. When the substitution is applied to a type,
|
* Creates a new substitution using a type variable a and a type b. When the substitution is applied to a type,
|
||||||
* all occurring instances of a should be substituted with b.
|
* all occurring instances of a should be substituted with b.
|
||||||
@ -15,22 +19,22 @@ public class Substitution {
|
|||||||
* @param b type to insert
|
* @param b type to insert
|
||||||
*/
|
*/
|
||||||
public Substitution(TypeVariable a, Type b) {
|
public Substitution(TypeVariable a, Type b) {
|
||||||
// TODO
|
// TODO: null checks?
|
||||||
|
this.a = a;
|
||||||
|
this.b = b;
|
||||||
}
|
}
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* @return the type variable
|
* @return the type variable
|
||||||
*/
|
*/
|
||||||
public TypeVariable getVariable() {
|
public TypeVariable getVariable() {
|
||||||
return null;
|
return a;
|
||||||
// TODO
|
|
||||||
}
|
}
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* @return the replacement type
|
* @return the replacement type
|
||||||
*/
|
*/
|
||||||
Type getType() {
|
Type getType() {
|
||||||
return null;
|
return b;
|
||||||
// TODO
|
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
@ -0,0 +1,4 @@
|
|||||||
|
package edu.kit.typicalc.model.step;
|
||||||
|
|
||||||
|
public class AbsStepDefault {
|
||||||
|
}
|
@ -0,0 +1,4 @@
|
|||||||
|
package edu.kit.typicalc.model.step;
|
||||||
|
|
||||||
|
public class AbsStepWithLet {
|
||||||
|
}
|
@ -0,0 +1,4 @@
|
|||||||
|
package edu.kit.typicalc.model.step;
|
||||||
|
|
||||||
|
public class AppStepDefault {
|
||||||
|
}
|
@ -0,0 +1,4 @@
|
|||||||
|
package edu.kit.typicalc.model.step;
|
||||||
|
|
||||||
|
public class ConstStepDefault {
|
||||||
|
}
|
@ -0,0 +1,4 @@
|
|||||||
|
package edu.kit.typicalc.model.step;
|
||||||
|
|
||||||
|
public class LetStepDefault {
|
||||||
|
}
|
@ -37,7 +37,7 @@ public interface StepVisitor {
|
|||||||
|
|
||||||
/**
|
/**
|
||||||
* Visits a VarStepWithLet.
|
* Visits a VarStepWithLet.
|
||||||
* @param varD the VarStepWithLet to visit
|
* @param varL the VarStepWithLet to visit
|
||||||
*/
|
*/
|
||||||
void visitVarStepWithLet(VarStepWithLet varL);
|
void visitVarStepWithLet(VarStepWithLet varL);
|
||||||
|
|
||||||
|
@ -0,0 +1,4 @@
|
|||||||
|
package edu.kit.typicalc.model.step;
|
||||||
|
|
||||||
|
public class VarStepDefault {
|
||||||
|
}
|
@ -0,0 +1,4 @@
|
|||||||
|
package edu.kit.typicalc.model.step;
|
||||||
|
|
||||||
|
public class VarStepWithLet {
|
||||||
|
}
|
@ -0,0 +1,4 @@
|
|||||||
|
package edu.kit.typicalc.model.type;
|
||||||
|
|
||||||
|
public interface TypeVisitor {
|
||||||
|
}
|
@ -3,9 +3,9 @@ package edu.kit.typicalc.view.content.typeinferencecontent;
|
|||||||
|
|
||||||
import edu.kit.typicalc.model.Conclusion;
|
import edu.kit.typicalc.model.Conclusion;
|
||||||
import edu.kit.typicalc.model.TypeInfererInterface;
|
import edu.kit.typicalc.model.TypeInfererInterface;
|
||||||
import edu.kit.typicalc.model.step.InferenceStep;
|
import edu.kit.typicalc.model.step.*;
|
||||||
import edu.kit.typicalc.model.step.StepVisitor;
|
|
||||||
import edu.kit.typicalc.model.term.TermVisitor;
|
import edu.kit.typicalc.model.term.TermVisitor;
|
||||||
|
import edu.kit.typicalc.model.type.TypeVisitor;
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Generates LaTeX-code from a TypeInfererInterface object. Two mostly independent pie-
|
* Generates LaTeX-code from a TypeInfererInterface object. Two mostly independent pie-
|
||||||
@ -122,13 +122,13 @@ public class LatexCreator implements StepVisitor, TermVisitor, TypeVisitor {
|
|||||||
|
|
||||||
@Override
|
@Override
|
||||||
public void visitVarStepWithLet(VarStepWithLet varL) {
|
public void visitVarStepWithLet(VarStepWithLet varL) {
|
||||||
generateConclusion(varL, LABEL_ABS, UIC);
|
generateConclusion(varL, LABEL_VAR, UIC);
|
||||||
|
|
||||||
}
|
}
|
||||||
|
|
||||||
@Override
|
@Override
|
||||||
public void visitLetStepDefault(LetStepDefault letD) {
|
public void visitLetStepDefault(LetStepDefault letD) {
|
||||||
generateConclusion(letD, LABEL_ABS, UIC);
|
generateConclusion(letD, LABEL_LET, UIC);
|
||||||
|
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
@ -14,7 +14,7 @@ public class ShareDialog extends Dialog implements LocaleChangeObserver {
|
|||||||
* to the String that is passed as corresponding parameter.
|
* to the String that is passed as corresponding parameter.
|
||||||
* @param url a permalink to share with other users
|
* @param url a permalink to share with other users
|
||||||
* @param latexPackages the needed LaTeX-packages to use the displayed mathmatics
|
* @param latexPackages the needed LaTeX-packages to use the displayed mathmatics
|
||||||
* in other LaTeX documents. Should be in the form „\usepackage<package>“
|
* in other LaTeX documents. Should be in the form „\\usepackage<package>“
|
||||||
* @param latexCode LaTeX code for users to copy into their own LaTeX document(s)
|
* @param latexCode LaTeX code for users to copy into their own LaTeX document(s)
|
||||||
*/
|
*/
|
||||||
protected ShareDialog(String url, String latexPackages, String latexCode) {
|
protected ShareDialog(String url, String latexPackages, String latexCode) {
|
||||||
|
Loading…
Reference in New Issue
Block a user