mirror of
https://gitlab.kit.edu/uskyk/typicalc.git
synced 2024-11-08 18:30:42 +00:00
Step-Paket implementiert, StepVisitor-Methoden angepasst
This commit is contained in:
parent
75d686d8af
commit
36c9f092c7
33
package.json
33
package.json
@ -36,7 +36,20 @@
|
|||||||
"lit-element": "2.3.1",
|
"lit-element": "2.3.1",
|
||||||
"@vaadin/form": "./target/flow-frontend/form",
|
"@vaadin/form": "./target/flow-frontend/form",
|
||||||
"@vaadin/vaadin-avatar": "1.0.3",
|
"@vaadin/vaadin-avatar": "1.0.3",
|
||||||
"open": "^7.2.1"
|
"open": "^7.2.1",
|
||||||
|
"@vaadin/vaadin-crud": "1.3.0",
|
||||||
|
"@vaadin/vaadin-cookie-consent": "1.2.0",
|
||||||
|
"@vaadin/vaadin-upload": "4.4.1",
|
||||||
|
"@vaadin/vaadin-board": "2.2.0",
|
||||||
|
"@vaadin/vaadin-date-time-picker": "1.4.0",
|
||||||
|
"@vaadin/vaadin-login": "1.2.0",
|
||||||
|
"@vaadin/vaadin-accordion": "1.2.0",
|
||||||
|
"@vaadin/vaadin-checkbox": "2.5.0",
|
||||||
|
"@vaadin/vaadin-time-picker": "2.4.0",
|
||||||
|
"@vaadin/vaadin-context-menu": "4.5.0",
|
||||||
|
"@vaadin/vaadin-tabs": "3.2.0",
|
||||||
|
"@vaadin/vaadin-radio-button": "1.5.1",
|
||||||
|
"@vaadin/vaadin-rich-text-editor": "1.3.0"
|
||||||
},
|
},
|
||||||
"devDependencies": {
|
"devDependencies": {
|
||||||
"webpack": "4.42.0",
|
"webpack": "4.42.0",
|
||||||
@ -96,7 +109,21 @@
|
|||||||
"@vaadin/vaadin-custom-field": "1.3.0",
|
"@vaadin/vaadin-custom-field": "1.3.0",
|
||||||
"lit-element": "2.3.1",
|
"lit-element": "2.3.1",
|
||||||
"@vaadin/vaadin-avatar": "1.0.3",
|
"@vaadin/vaadin-avatar": "1.0.3",
|
||||||
"open": "^7.2.1"
|
"open": "^7.2.1",
|
||||||
|
"@vaadin/vaadin-crud": "1.3.0",
|
||||||
|
"@vaadin/vaadin-cookie-consent": "1.2.0",
|
||||||
|
"@vaadin/vaadin-upload": "4.4.1",
|
||||||
|
"@vaadin/vaadin-board": "2.2.0",
|
||||||
|
"@vaadin/vaadin-charts": "7.0.0",
|
||||||
|
"@vaadin/vaadin-date-time-picker": "1.4.0",
|
||||||
|
"@vaadin/vaadin-login": "1.2.0",
|
||||||
|
"@vaadin/vaadin-date-picker": "4.4.1",
|
||||||
|
"@vaadin/vaadin-accordion": "1.2.0",
|
||||||
|
"@vaadin/vaadin-checkbox": "2.5.0",
|
||||||
|
"@vaadin/vaadin-time-picker": "2.4.0",
|
||||||
|
"@vaadin/vaadin-tabs": "3.2.0",
|
||||||
|
"@vaadin/vaadin-radio-button": "1.5.1",
|
||||||
|
"@vaadin/vaadin-rich-text-editor": "1.3.0"
|
||||||
},
|
},
|
||||||
"devDependencies": {
|
"devDependencies": {
|
||||||
"webpack-babel-multi-target-plugin": "2.3.3",
|
"webpack-babel-multi-target-plugin": "2.3.3",
|
||||||
@ -122,6 +149,6 @@
|
|||||||
"lit-css-loader": "0.0.4",
|
"lit-css-loader": "0.0.4",
|
||||||
"extract-loader": "5.1.0"
|
"extract-loader": "5.1.0"
|
||||||
},
|
},
|
||||||
"hash": "b905e6c0ab4b1f42dcee18553457275cfa5c59c2404c0d9d2acc51cdb43de40b"
|
"hash": "176a855b9845a8bd6e1b6138940c86e0431291e79479361d27a18a7b50bd4678"
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
@ -1,4 +1,29 @@
|
|||||||
package edu.kit.typicalc.model.step;
|
package edu.kit.typicalc.model.step;
|
||||||
|
|
||||||
public class AbsStepDefault {
|
import edu.kit.typicalc.model.Conclusion;
|
||||||
|
import edu.kit.typicalc.model.Constraint;
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Models one step of the inference tree where the abstraction rule
|
||||||
|
* is applied and no let rule is applied in the entire tree.
|
||||||
|
*/
|
||||||
|
public class AbsStepDefault extends AbsStep {
|
||||||
|
/**
|
||||||
|
* Initializes a new AbsStepDefault with the given values.
|
||||||
|
* @param premise the premise of this step
|
||||||
|
* @param conclusion the conclusion of this step
|
||||||
|
* @param constraint the constraint added in this step
|
||||||
|
*/
|
||||||
|
public AbsStepDefault(InferenceStep premise, Conclusion conclusion, Constraint constraint) {
|
||||||
|
super(premise, conclusion, constraint);
|
||||||
|
}
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Accepts a visitor.
|
||||||
|
* @param stepVisitor – the visitor that wants to visit this object
|
||||||
|
*/
|
||||||
|
@Override
|
||||||
|
public void accept(StepVisitor stepVisitor) {
|
||||||
|
stepVisitor.visit(this);
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
@ -1,4 +1,29 @@
|
|||||||
package edu.kit.typicalc.model.step;
|
package edu.kit.typicalc.model.step;
|
||||||
|
|
||||||
public class AbsStepWithLet {
|
import edu.kit.typicalc.model.Conclusion;
|
||||||
|
import edu.kit.typicalc.model.Constraint;
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Models one step of the inference tree where the abstraction rule is applied and at least
|
||||||
|
* one let rule is applied in the entire tree.
|
||||||
|
*/
|
||||||
|
public class AbsStepWithLet extends AbsStep {
|
||||||
|
/**
|
||||||
|
*Initializes a new AbsStepWithLet with the given values.
|
||||||
|
* @param premise the premise of this step
|
||||||
|
* @param conclusion the conclusion of this step
|
||||||
|
* @param constraint constraint that can be derived from this step
|
||||||
|
*/
|
||||||
|
public AbsStepWithLet(InferenceStep premise, Conclusion conclusion, Constraint constraint) {
|
||||||
|
super(premise, conclusion, constraint);
|
||||||
|
}
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Accepts a visitor.
|
||||||
|
* @param stepVisitor the visitor that wants to visit this object
|
||||||
|
*/
|
||||||
|
@Override
|
||||||
|
public void accept(StepVisitor stepVisitor) {
|
||||||
|
stepVisitor.visit(this);
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
@ -1,4 +1,31 @@
|
|||||||
package edu.kit.typicalc.model.step;
|
package edu.kit.typicalc.model.step;
|
||||||
|
|
||||||
public class AppStepDefault {
|
import edu.kit.typicalc.model.Conclusion;
|
||||||
|
import edu.kit.typicalc.model.Constraint;
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Models one step of the inference tree where the abstraction rule is applied and no let rule
|
||||||
|
* is applied in the entire tree.
|
||||||
|
*/
|
||||||
|
public class AppStepDefault extends AppStep {
|
||||||
|
/**
|
||||||
|
*Initializes a new AbsStepWithLet with the given values.
|
||||||
|
* @param premise1 the first premise of this step
|
||||||
|
* @param premise2 the second premise of this step
|
||||||
|
* @param conclusion the conclusion of this step
|
||||||
|
* @param constraint constraint that can be derived from this step
|
||||||
|
*/
|
||||||
|
public AppStepDefault(InferenceStep premise1, InferenceStep premise2,
|
||||||
|
Conclusion conclusion, Constraint constraint) {
|
||||||
|
super(premise1, premise2, conclusion, constraint);
|
||||||
|
}
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Accepts a visitor.
|
||||||
|
* @param stepVisitor – the visitor that wants to visit this object
|
||||||
|
*/
|
||||||
|
@Override
|
||||||
|
public void accept(StepVisitor stepVisitor) {
|
||||||
|
stepVisitor.visit(this);
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
@ -1,4 +1,29 @@
|
|||||||
package edu.kit.typicalc.model.step;
|
package edu.kit.typicalc.model.step;
|
||||||
|
|
||||||
public class ConstStepDefault {
|
import edu.kit.typicalc.model.Conclusion;
|
||||||
|
import edu.kit.typicalc.model.Constraint;
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Models one step of the inference tree where the constant rule is applied. As the constant
|
||||||
|
* rule is the same regardless of whether the tree contains a let step, this is the only subclass
|
||||||
|
* of ConstStep.
|
||||||
|
*/
|
||||||
|
public class ConstStepDefault extends ConstStep {
|
||||||
|
/**
|
||||||
|
* Initializes a new ConstStep with the given values.
|
||||||
|
* @param conclusion the conclusion of this step
|
||||||
|
* @param constraint the constraint added in this step
|
||||||
|
*/
|
||||||
|
public ConstStepDefault(Conclusion conclusion, Constraint constraint) {
|
||||||
|
super(conclusion, constraint);
|
||||||
|
}
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Accepts a visitor.
|
||||||
|
* @param stepVisitor the visitor that wants to visit this object
|
||||||
|
*/
|
||||||
|
@Override
|
||||||
|
public void accept(StepVisitor stepVisitor) {
|
||||||
|
stepVisitor.visit(this);
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
@ -1,18 +1,49 @@
|
|||||||
package edu.kit.typicalc.model.step;
|
package edu.kit.typicalc.model.step;
|
||||||
|
|
||||||
|
import edu.kit.typicalc.model.Conclusion;
|
||||||
|
import edu.kit.typicalc.model.Constraint;
|
||||||
/**
|
/**
|
||||||
* Models one step of the inference tree. Depending on the inference rule that is applied in
|
* Models one step of the inference tree.
|
||||||
* a step, different subclasses of InferenceStep should be used. A step always contains the
|
* Depending on the inference rule that is applied in a step,
|
||||||
* Constraint that is added to the set of constraints of the type inference algorithm because
|
* different subclasses of InferenceStep should be used.
|
||||||
* of this step and a Conclusion. The subclasses vary in the premise(s) they contain.
|
* A step always contains the Constraint that is added
|
||||||
|
* to the set of constraints of the type inference algorithm because
|
||||||
|
* of this step and a Conclusion.
|
||||||
|
* The subclasses vary in the premise(s) they contain.
|
||||||
*/
|
*/
|
||||||
public abstract class InferenceStep {
|
public abstract class InferenceStep {
|
||||||
// todo
|
private Conclusion conclusion;
|
||||||
|
private Constraint constraint;
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Initializes a new InferenceStep with the given values.
|
||||||
|
* @param conclusion the conclusion of this step
|
||||||
|
* @param constraint the constraint added in this step
|
||||||
|
*/
|
||||||
|
protected InferenceStep(Conclusion conclusion, Constraint constraint) {
|
||||||
|
this.conclusion = conclusion;
|
||||||
|
this.constraint = constraint;
|
||||||
|
}
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Getter for the Conclusion of this step.
|
||||||
|
* @return conclusion the conclusion of this step
|
||||||
|
*/
|
||||||
|
public Conclusion getConclusion() {
|
||||||
|
return conclusion;
|
||||||
|
}
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Getter for the Constraint added in this step.
|
||||||
|
* @return conclusion the constraint added in this step
|
||||||
|
*/
|
||||||
|
public Constraint getConstraint() {
|
||||||
|
return constraint;
|
||||||
|
}
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Accepts a visitor.
|
* Accepts a visitor.
|
||||||
* @param stepVisitor the visitor that wants to visit this object
|
* @param stepVisitor the visitor that wants to visit this object
|
||||||
*/
|
*/
|
||||||
public abstract void accept(StepVisitor stepVisitor);
|
public abstract void accept(StepVisitor stepVisitor);
|
||||||
|
}
|
||||||
}
|
|
||||||
|
@ -1,4 +1,32 @@
|
|||||||
package edu.kit.typicalc.model.step;
|
package edu.kit.typicalc.model.step;
|
||||||
|
|
||||||
public class LetStepDefault {
|
import edu.kit.typicalc.model.Conclusion;
|
||||||
|
import edu.kit.typicalc.model.Constraint;
|
||||||
|
import edu.kit.typicalc.model.TypeInfererLet;
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Models one step of the inference tree where the let rule is applied.
|
||||||
|
*/
|
||||||
|
public class LetStepDefault extends LetStep {
|
||||||
|
/**
|
||||||
|
* Initializes a new LetStep with the given values.
|
||||||
|
* @param conclusion the conclusion of this step
|
||||||
|
* @param constraint the constraint added in this step
|
||||||
|
* @param premise the right premise of this step
|
||||||
|
* @param typeInferer the typeInferer that performs the Type Inference for the premise
|
||||||
|
* that needs its own type Inference.
|
||||||
|
*/
|
||||||
|
public LetStepDefault(Conclusion conclusion, Constraint constraint, InferenceStep premise,
|
||||||
|
TypeInfererLet typeInferer) {
|
||||||
|
super(conclusion, constraint, premise, typeInferer);
|
||||||
|
}
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Accepts a visitor.
|
||||||
|
* @param stepVisitor the visitor that wants to visit this object
|
||||||
|
*/
|
||||||
|
@Override
|
||||||
|
public void accept(StepVisitor stepVisitor) {
|
||||||
|
stepVisitor.visit(this);
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
@ -9,43 +9,43 @@ public interface StepVisitor {
|
|||||||
* Visits an AbsStepDefault.
|
* Visits an AbsStepDefault.
|
||||||
* @param absD the AbsStepDefault to visit
|
* @param absD the AbsStepDefault to visit
|
||||||
*/
|
*/
|
||||||
void visitAbsStepDefault(AbsStepDefault absD);
|
void visit(AbsStepDefault absD);
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Visits an AbsStepWithLet.
|
* Visits an AbsStepWithLet.
|
||||||
* @param absL the AbsStepWithLet to visit
|
* @param absL the AbsStepWithLet to visit
|
||||||
*/
|
*/
|
||||||
void visitAbsStepWithLet(AbsStepWithLet absL);
|
void visit(AbsStepWithLet absL);
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Visits an AppStepDefault.
|
* Visits an AppStepDefault.
|
||||||
* @param appD the AppStepDefault to visit
|
* @param appD the AppStepDefault to visit
|
||||||
*/
|
*/
|
||||||
void visitAppStepDefault(AppStepDefault appD);
|
void visit(AppStepDefault appD);
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* ConstStepDefault.
|
* ConstStepDefault.
|
||||||
* @param constD the ConstStepDefault to visit
|
* @param constD the ConstStepDefault to visit
|
||||||
*/
|
*/
|
||||||
void visitConstStepDefault(ConstStepDefault constD);
|
void visit(ConstStepDefault constD);
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Visits a VarStepDefault.
|
* Visits a VarStepDefault.
|
||||||
* @param varD the VarStepDefault to visit
|
* @param varD the VarStepDefault to visit
|
||||||
*/
|
*/
|
||||||
void visitVarStepDefault(VarStepDefault varD);
|
void visit(VarStepDefault varD);
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Visits a VarStepWithLet.
|
* Visits a VarStepWithLet.
|
||||||
* @param varL the VarStepWithLet to visit
|
* @param varL the VarStepWithLet to visit
|
||||||
*/
|
*/
|
||||||
void visitVarStepWithLet(VarStepWithLet varL);
|
void visit(VarStepWithLet varL);
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Visits a LetStepDefault.
|
* Visits a LetStepDefault.
|
||||||
* @param letD the LetStepDefault to visit
|
* @param letD the LetStepDefault to visit
|
||||||
*/
|
*/
|
||||||
void visitLetStepDefault(LetStepDefault letD);
|
void visit(LetStepDefault letD);
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
@ -1,4 +1,26 @@
|
|||||||
package edu.kit.typicalc.model.step;
|
package edu.kit.typicalc.model.step;
|
||||||
|
|
||||||
public class VarStepDefault {
|
import edu.kit.typicalc.model.Conclusion;
|
||||||
|
import edu.kit.typicalc.model.Constraint;
|
||||||
|
import edu.kit.typicalc.model.type.TypeAbstraction;
|
||||||
|
|
||||||
|
public class VarStepDefault extends VarStep {
|
||||||
|
/**
|
||||||
|
* Initializes a new VarStep with the given values.
|
||||||
|
* @param conclusion the conclusion of this step
|
||||||
|
* @param constraint the constraint added in this step
|
||||||
|
* @param typeAbstractionInPremise the type abstraction in the premise of this step
|
||||||
|
*/
|
||||||
|
public VarStepDefault(Conclusion conclusion, Constraint constraint, TypeAbstraction typeAbstractionInPremise) {
|
||||||
|
super(conclusion, constraint, typeAbstractionInPremise);
|
||||||
|
}
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Accepts a visitor.
|
||||||
|
* @param stepVisitor the visitor that wants to visit this object
|
||||||
|
*/
|
||||||
|
@Override
|
||||||
|
public void accept(StepVisitor stepVisitor) {
|
||||||
|
stepVisitor.visit(this);
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
@ -1,4 +1,26 @@
|
|||||||
package edu.kit.typicalc.model.step;
|
package edu.kit.typicalc.model.step;
|
||||||
|
|
||||||
public class VarStepWithLet {
|
import edu.kit.typicalc.model.Conclusion;
|
||||||
|
import edu.kit.typicalc.model.Constraint;
|
||||||
|
import edu.kit.typicalc.model.type.TypeAbstraction;
|
||||||
|
|
||||||
|
public class VarStepWithLet extends VarStep {
|
||||||
|
/**
|
||||||
|
* Initializes a new VarStep with the given values.
|
||||||
|
* @param conclusion the conclusion of this step
|
||||||
|
* @param constraint the constraint added in this step
|
||||||
|
* @param typeAbstractionInPremise the type abstraction in the premise of this step
|
||||||
|
*/
|
||||||
|
public VarStepWithLet(Conclusion conclusion, Constraint constraint, TypeAbstraction typeAbstractionInPremise) {
|
||||||
|
super(conclusion, constraint, typeAbstractionInPremise);
|
||||||
|
}
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Accepts a visitor.
|
||||||
|
* @param stepVisitor the visitor that wants to visit this object
|
||||||
|
*/
|
||||||
|
@Override
|
||||||
|
public void accept(StepVisitor stepVisitor) {
|
||||||
|
stepVisitor.visit(this);
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
@ -90,44 +90,44 @@ public class LatexCreator implements StepVisitor, TermVisitor, TypeVisitor {
|
|||||||
}
|
}
|
||||||
|
|
||||||
@Override
|
@Override
|
||||||
public void visitAbsStepDefault(AbsStepDefault absD) {
|
public void visit(AbsStepDefault absD) {
|
||||||
generateConclusion(absD, LABEL_ABS, UIC);
|
generateConclusion(absD, LABEL_ABS, UIC);
|
||||||
|
|
||||||
|
|
||||||
}
|
}
|
||||||
|
|
||||||
@Override
|
@Override
|
||||||
public void visitAbsStepWithLet(AbsStepWithLet absL) {
|
public void visit(AbsStepWithLet absL) {
|
||||||
generateConclusion(absL, LABEL_ABS, UIC);
|
generateConclusion(absL, LABEL_ABS, UIC);
|
||||||
|
|
||||||
}
|
}
|
||||||
|
|
||||||
@Override
|
@Override
|
||||||
public void visitAppStepDefault(AppStepDefault appD) {
|
public void visit(AppStepDefault appD) {
|
||||||
generateConclusion(appD, LABEL_APP, UIC);
|
generateConclusion(appD, LABEL_APP, UIC);
|
||||||
|
|
||||||
}
|
}
|
||||||
|
|
||||||
@Override
|
@Override
|
||||||
public void visitConstStepDefault(ConstStepDefault constD) {
|
public void visit(ConstStepDefault constD) {
|
||||||
generateConclusion(constD, LABEL_CONST, UIC);
|
generateConclusion(constD, LABEL_CONST, UIC);
|
||||||
|
|
||||||
}
|
}
|
||||||
|
|
||||||
@Override
|
@Override
|
||||||
public void visitVarStepDefault(VarStepDefault varD) {
|
public void visit(VarStepDefault varD) {
|
||||||
generateConclusion(varD, LABEL_VAR, UIC);
|
generateConclusion(varD, LABEL_VAR, UIC);
|
||||||
|
|
||||||
}
|
}
|
||||||
|
|
||||||
@Override
|
@Override
|
||||||
public void visitVarStepWithLet(VarStepWithLet varL) {
|
public void visit(VarStepWithLet varL) {
|
||||||
generateConclusion(varL, LABEL_VAR, UIC);
|
generateConclusion(varL, LABEL_VAR, UIC);
|
||||||
|
|
||||||
}
|
}
|
||||||
|
|
||||||
@Override
|
@Override
|
||||||
public void visitLetStepDefault(LetStepDefault letD) {
|
public void visit(LetStepDefault letD) {
|
||||||
generateConclusion(letD, LABEL_LET, UIC);
|
generateConclusion(letD, LABEL_LET, UIC);
|
||||||
|
|
||||||
}
|
}
|
||||||
|
Loading…
Reference in New Issue
Block a user