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:
Moritz Dieing 2021-01-28 13:22:55 +01:00
commit 539c45e5d5
18 changed files with 317 additions and 1306 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

32
frontend/src/mathjax-adapter.ts
View File

@ -1,6 +1,5 @@
import {LitElement, html} from 'lit-element'; import {LitElement, html} from 'lit-element';
import {TemplateResult} from "lit-html"; import {TemplateResult} from "lit-html";
declare let window: { declare let window: {
MathJax: { MathJax: {
typesetShadow: (arg0: ShadowRoot | null, arg1: () => void) => void, typesetShadow: (arg0: ShadowRoot | null, arg1: () => void) => void,
@ -10,21 +9,8 @@ declare let window: {
}; };
export abstract class MathjaxAdapter extends LitElement { export abstract class MathjaxAdapter extends LitElement {
protected execTypeset() { constructor() {
if (window.MathJax !== undefined) { super();
window.MathJax.typesetShadow(this.shadowRoot, () => this.calculateSteps());
}
}
render(): TemplateResult {
return html`<mjx-doc><mjx-head></mjx-head><mjx-body>
<div id="tc-content"></div>
</mjx-body></mjx-doc>`;
}
connectedCallback() {
super.connectedCallback();
if (window.MathJax === undefined || !window.MathJax.isInitialized) { if (window.MathJax === undefined || !window.MathJax.isInitialized) {
window.addEventListener('mathjax-initialized', () => this.execTypeset()); window.addEventListener('mathjax-initialized', () => this.execTypeset());
} else { } else {
@ -32,6 +18,20 @@ export abstract class MathjaxAdapter extends LitElement {
} }
} }
protected execTypeset() {
if (window.MathJax !== undefined) {
window.MathJax.typesetShadow(this.shadowRoot, () => this.calculateSteps());
}
}
// @ts-ignore
render(): TemplateResult {
return html`<mjx-doc id="mjx-document"><mjx-head></mjx-head><mjx-body>
<div id="tc-content"></div>
</mjx-body></mjx-doc>`;
}
protected abstract showStep(n: number): void; protected abstract showStep(n: number): void;
protected abstract calculateSteps(): void; protected abstract calculateSteps(): void;

114
frontend/src/mathjax-setup.js Normal file
View File

@ -0,0 +1,114 @@
window.MathJax = {
loader: {load: ['[tex]/bussproofs', '[tex]/html', '[tex]/action']},
tex: {
packages: {'[+]': ['bussproofs', 'html', 'action']},
inlineMath: [['$', '$'], ['\\(', '\\)']]
},
startup: {
ready: () => {
const mathjax = MathJax._.mathjax.mathjax;
const HTMLAdaptor = MathJax._.adaptors.HTMLAdaptor.HTMLAdaptor;
const HTMLHandler = MathJax._.handlers.html.HTMLHandler.HTMLHandler;
const AbstractHandler = MathJax._.core.Handler.AbstractHandler.prototype;
const startup = MathJax.startup;
//
// Extend HTMLAdaptor to handle shadowDOM as the document
//
class ShadowAdaptor extends HTMLAdaptor {
create(kind, ns) {
const document = (this.document.createElement ? this.document : this.window.document);
return (ns ?
document.createElementNS(ns, kind) :
document.createElement(kind));
}
text(text) {
const document = (this.document.createTextNode ? this.document : this.window.document);
return document.createTextNode(text);
}
head(doc) {
return doc.head || (doc.getElementById("mjx-document") || {}).firstChild || doc;
}
body(doc) {
return doc.body || (doc.getElementById("mjx-document") || {}).lastChild || doc;
}
root(doc) {
return doc.documentElement || doc.getElementById("mjx-document") || doc;
}
}
//
// Extend HTMLHandler to handle shadowDOM as document
//
class ShadowHandler extends HTMLHandler {
create(document, options) {
const adaptor = this.adaptor;
if (typeof (document) === 'string') {
document = adaptor.parse(document, 'text/html');
} else if ((document instanceof adaptor.window.HTMLElement ||
document instanceof adaptor.window.DocumentFragment) &&
!(document instanceof window.ShadowRoot)) {
let child = document;
document = adaptor.parse('', 'text/html');
adaptor.append(adaptor.body(document), child);
}
//
// We can't use super.create() here, since that doesn't
// handle shadowDOM correctly, so call HTMLHandler's parent class
// directly instead.
//
return AbstractHandler.create.call(this, document, options);
}
}
//
// Register the new handler and adaptor
//
startup.registerConstructor('HTMLHandler', ShadowHandler);
startup.registerConstructor('browserAdaptor', () => new ShadowAdaptor(window));
//
// A service function that creates a new MathDocument from the
// shadow root with the configured input and output jax, and then
// renders the document. The MathDocument is returned in case
// you need to rerender the shadowRoot later.
//
MathJax.typesetShadow = function (root, callback) {
const InputJax = startup.getInputJax();
const OutputJax = startup.getOutputJax();
const html = mathjax.document(root, {InputJax, OutputJax});
html.render();
if (callback != null) {
callback(html);
}
return html;
}
//
// Now do the usual startup now that the extensions are in place
//
let event = new Event('mathjax-initialized', {
bubbles: true,
composed: true,
detail: "composed"
})
MathJax.startup.defaultReady();
MathJax.startup.promise.then(() => {
console.log("MathJax initialized");
MathJax.isInitialized = true;
document.dispatchEvent(event);
})
}
}
};
(function () {
let script = document.createElement('script');
script.src = 'http://cdn.jsdelivr.net/npm/mathjax@3.1.2/es5/tex-svg.js';
// script.async = true;
document.head.appendChild(script);
})();

128
package.json
View File

@ -1,5 +1,5 @@
{ {
"name": "typicalc", "name": "no-name",
"license": "UNLICENSED", "license": "UNLICENSED",
"dependencies": { "dependencies": {
"@polymer/iron-icon": "3.0.1", "@polymer/iron-icon": "3.0.1",
@ -68,81 +68,133 @@
"webpack-dev-server": "3.11.0", "webpack-dev-server": "3.11.0",
"webpack-merge": "4.2.2" "webpack-merge": "4.2.2"
}, },
"vaadin": { "vaadin": {
"dependencies": { "dependencies": {
"lit-element": "2.3.1",
"@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",
"@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",
"@vaadin/vaadin-combo-box": "5.4.7", "@vaadin/vaadin-combo-box": "5.4.7",
"@vaadin/vaadin-core-shrinkwrap": "18.0.5",
"@vaadin/vaadin-upload": "4.4.1",
"@vaadin/vaadin-dialog": "2.5.2", "@vaadin/vaadin-dialog": "2.5.2",
"@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-notification": "1.6.0", "@vaadin/vaadin-notification": "1.6.0",
"@vaadin/vaadin-progress-bar": "1.3.0", "@vaadin/vaadin-progress-bar": "1.3.0",
"@vaadin/vaadin-date-time-picker": "1.4.0",
"@vaadin/vaadin-ordered-layout": "1.4.0", "@vaadin/vaadin-ordered-layout": "1.4.0",
"@vaadin/vaadin-login": "1.2.0",
"@vaadin/vaadin-button": "2.4.0", "@vaadin/vaadin-button": "2.4.0",
"@vaadin/vaadin-date-picker": "4.4.1",
"@vaadin/vaadin-text-field": "2.8.2", "@vaadin/vaadin-text-field": "2.8.2",
"@vaadin/vaadin-menu-bar": "1.2.1", "@vaadin/vaadin-menu-bar": "1.2.1",
"@vaadin/vaadin-custom-field": "1.3.0",
"@vaadin/vaadin-form-layout": "2.3.0", "@vaadin/vaadin-form-layout": "2.3.0",
"@vaadin/vaadin-accordion": "1.2.0",
"@polymer/iron-list": "3.1.0", "@polymer/iron-list": "3.1.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-lumo-styles": "1.6.0",
"@vaadin/vaadin-material-styles": "1.3.2",
"@vaadin/vaadin-custom-field": "1.3.0",
"lit-element": "2.3.1",
"@vaadin/vaadin-avatar": "1.0.3",
"open": "^7.2.1",
"@vaadin/vaadin-crud": "1.3.0",
"@vaadin/vaadin-cookie-consent": "1.2.0",
"@vaadin/vaadin-core-shrinkwrap": "18.0.5",
"@vaadin/vaadin-upload": "4.4.1",
"@vaadin/vaadin-board": "2.2.0",
"@vaadin/vaadin-charts": "7.0.0",
"@vaadin/vaadin-grid-pro": "2.2.2",
"@vaadin/vaadin-shrinkwrap": "18.0.5",
"@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-time-picker": "2.4.0",
"@vaadin/vaadin-avatar": "1.0.3",
"@vaadin/vaadin-context-menu": "4.5.0",
"@vaadin/vaadin-tabs": "3.2.0", "@vaadin/vaadin-tabs": "3.2.0",
"@vaadin/vaadin-radio-button": "1.5.1", "@vaadin/vaadin-radio-button": "1.5.1",
"@vaadin/vaadin-rich-text-editor": "1.3.0", "@vaadin/vaadin-rich-text-editor": "1.3.0",
"@vaadin-component-factory/vcf-tooltip": "1.3.13" "@vaadin-component-factory/vcf-tooltip": "1.3.13"
"@vaadin/vaadin-lumo-styles": "1.6.0",
"@vaadin/vaadin-material-styles": "1.3.2",
"open": "^7.2.1"
}, },
"devDependencies": { "devDependencies": {
"webpack-babel-multi-target-plugin": "2.3.3",
"copy-webpack-plugin": "5.1.2",
"compression-webpack-plugin": "4.0.1", "compression-webpack-plugin": "4.0.1",
"raw-loader": "4.0.0",
"webpack-cli": "3.3.11", "webpack-cli": "3.3.11",
"css-loader": "4.2.1",
"script-ext-html-webpack-plugin": "2.1.4",
"validator": "13.1.17",
"awesome-typescript-loader": "5.2.1",
"lit-css-loader": "0.0.4",
"lit-html": "1.2.1",
"@types/validator": "13.1.0",
"copy-webpack-plugin": "5.1.2",
"lit-element": "2.3.1",
"webpack": "4.42.0", "webpack": "4.42.0",
"html-webpack-plugin": "3.2.0", "html-webpack-plugin": "3.2.0",
"script-ext-html-webpack-plugin": "2.1.4", "chokidar": "^3.4.0",
"awesome-typescript-loader": "5.2.1",
"typescript": "4.0.3", "typescript": "4.0.3",
"webpack-merge": "4.2.2", "webpack-merge": "4.2.2",
"webpack-dev-server": "3.11.0", "webpack-dev-server": "3.11.0",
"terser": "4.6.7",
"progress-webpack-plugin": "0.0.24",
"lit-element": "2.3.1",
"chokidar": "^3.4.0",
"validator": "13.1.17",
"lit-html": "1.2.1",
"@types/validator": "13.1.0",
"css-loader": "4.2.1",
"lit-css-loader": "0.0.4",
"extract-loader": "5.1.0" "extract-loader": "5.1.0"
}, },
"hash": "9a8381007196d77745c03255bc222102472ce461f37b2742f39962e71d14929a" "hash": "8a8bb65418f58834b30cd258cd47da52573731720ea8967d4078487cb1253498"
},
"dependencies": {
"lit-element": "2.3.1",
"@vaadin/router": "1.7.2",
"@polymer/polymer": "3.2.0",
"@vaadin/flow-frontend": "./target/flow-frontend",
"@vaadin/form": "./target/flow-frontend/form",
"@vaadin/vaadin-grid": "5.7.7",
"@vaadin/vaadin-icons": "4.3.2",
"@vaadin/vaadin-split-layout": "4.3.0",
"@vaadin/vaadin-combo-box": "5.4.7",
"@vaadin/vaadin-core-shrinkwrap": "18.0.5",
"@vaadin/vaadin-upload": "4.4.1",
"@vaadin/vaadin-dialog": "2.5.2",
"@vaadin/vaadin-select": "2.4.0",
"@vaadin/vaadin-app-layout": "2.2.0",
"@vaadin/vaadin-item": "2.3.0",
"@vaadin/vaadin-notification": "1.6.0",
"@vaadin/vaadin-progress-bar": "1.3.0",
"@vaadin/vaadin-date-time-picker": "1.4.0",
"@vaadin/vaadin-ordered-layout": "1.4.0",
"@vaadin/vaadin-login": "1.2.0",
"@vaadin/vaadin-button": "2.4.0",
"@vaadin/vaadin-date-picker": "4.4.1",
"@vaadin/vaadin-text-field": "2.8.2",
"@vaadin/vaadin-menu-bar": "1.2.1",
"@vaadin/vaadin-custom-field": "1.3.0",
"@vaadin/vaadin-form-layout": "2.3.0",
"@vaadin/vaadin-accordion": "1.2.0",
"@polymer/iron-list": "3.1.0",
"@vaadin/vaadin-list-box": "1.4.0",
"@vaadin/vaadin-checkbox": "2.5.0",
"@vaadin/vaadin-details": "1.2.0",
"@polymer/iron-icon": "3.0.1",
"@vaadin/vaadin-time-picker": "2.4.0",
"@vaadin/vaadin-avatar": "1.0.3",
"@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-material-styles": "1.3.2",
"open": "^7.2.1"
},
"devDependencies": {
"compression-webpack-plugin": "4.0.1",
"webpack-cli": "3.3.11",
"css-loader": "4.2.1",
"script-ext-html-webpack-plugin": "2.1.4",
"validator": "13.1.17",
"awesome-typescript-loader": "5.2.1",
"lit-css-loader": "0.0.4",
"lit-html": "1.2.1",
"@types/validator": "13.1.0",
"copy-webpack-plugin": "5.1.2",
"lit-element": "2.3.1",
"webpack": "4.42.0",
"html-webpack-plugin": "3.2.0",
"chokidar": "^3.4.0",
"typescript": "4.0.3",
"webpack-merge": "4.2.2",
"webpack-dev-server": "3.11.0",
"extract-loader": "5.1.0"
} }
} }

1215
pnpm-lock.yaml
View File

File diff suppressed because it is too large Load Diff

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

@ -150,7 +150,19 @@ public class Tree implements TermVisitorTree {
} }
@Override @Override
public InferenceStep visit(VarTerm varTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType) { public InferenceStep visit(VarTerm varTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType)
return null; // TODO throws IllegalStateException {
TypeAbstraction premiseAbs = typeAssumptions.get(varTerm);
if (premiseAbs == null) {
throw new IllegalStateException("Cannot create VarStep for VarTerm '"
+ varTerm.getName() + "' without appropriate type assumption");
}
Type instantiation = premiseAbs.instantiate(typeVarFactory);
Constraint newConstraint = new Constraint(conclusionType, instantiation);
constraints.add(newConstraint);
Conclusion conclusion = new Conclusion(typeAssumptions, varTerm, conclusionType);
return stepFactory.createVarStep(premiseAbs, instantiation, conclusion, newConstraint);
} }
} }

7
src/main/java/edu/kit/typicalc/model/step/StepFactory.java
View File

@ -2,6 +2,7 @@ package edu.kit.typicalc.model.step;
import edu.kit.typicalc.model.Conclusion; import edu.kit.typicalc.model.Conclusion;
import edu.kit.typicalc.model.Constraint; import edu.kit.typicalc.model.Constraint;
import edu.kit.typicalc.model.type.Type;
import edu.kit.typicalc.model.type.TypeAbstraction; import edu.kit.typicalc.model.type.TypeAbstraction;
/** /**
@ -34,14 +35,16 @@ public interface StepFactory {
* @return the created ConstStep * @return the created ConstStep
*/ */
ConstStep createConstStep(Conclusion conclusion, Constraint constraint); ConstStep createConstStep(Conclusion conclusion, Constraint constraint);
/** /**
* Creates a VarStep. * Creates a VarStep.
* @param typeAbstraction the type abstraction of this step * @param typeAbstraction the type abstraction of this step
* @param instantiatedTypeAbs an instantiation of the type abstraction used in this step
* @param conclusion the conclusion of this step * @param conclusion the conclusion of this step
* @param constraint the constraint that can be derived from this step * @param constraint the constraint that can be derived from this step
* @return the created AbsStep * @return the created AbsStep
*/ */
VarStep createVarStep(TypeAbstraction typeAbstraction, Conclusion conclusion, VarStep createVarStep(TypeAbstraction typeAbstraction, Type instantiatedTypeAbs,
Constraint constraint); Conclusion conclusion, Constraint constraint);
//TODO LetStep //TODO LetStep
} }

15
src/main/java/edu/kit/typicalc/model/step/StepFactoryDefault.java
View File

@ -2,12 +2,14 @@ package edu.kit.typicalc.model.step;
import edu.kit.typicalc.model.Conclusion; import edu.kit.typicalc.model.Conclusion;
import edu.kit.typicalc.model.Constraint; import edu.kit.typicalc.model.Constraint;
import edu.kit.typicalc.model.type.Type;
import edu.kit.typicalc.model.type.TypeAbstraction; import edu.kit.typicalc.model.type.TypeAbstraction;
/** /**
* A factory to create InferenceStep objects when let polymorphism is not used. * A factory to create InferenceStep objects when let polymorphism is not used.
*/ */
public class StepFactoryDefault implements StepFactory { public class StepFactoryDefault implements StepFactory {
/** /**
* Creates an AbsStepDefault. * Creates an AbsStepDefault.
* @param premise the premise of this step * @param premise the premise of this step
@ -15,6 +17,7 @@ public class StepFactoryDefault implements StepFactory {
* @param constraint the constraint that can be derived from this step * @param constraint the constraint that can be derived from this step
* @return the created AbsStepDefault * @return the created AbsStepDefault
*/ */
@Override
public AbsStepDefault createAbsStep(InferenceStep premise, Conclusion conclusion, Constraint constraint) { public AbsStepDefault createAbsStep(InferenceStep premise, Conclusion conclusion, Constraint constraint) {
return new AbsStepDefault(premise, conclusion, constraint); return new AbsStepDefault(premise, conclusion, constraint);
} }
@ -27,28 +30,34 @@ public class StepFactoryDefault implements StepFactory {
* @param constraint the constraint that can be derived from this step * @param constraint the constraint that can be derived from this step
* @return the created AppStepDefault * @return the created AppStepDefault
*/ */
@Override
public AppStepDefault createAppStep(InferenceStep premise1, InferenceStep premise2, public AppStepDefault createAppStep(InferenceStep premise1, InferenceStep premise2,
Conclusion conclusion, Constraint constraint) { Conclusion conclusion, Constraint constraint) {
return new AppStepDefault(premise1, premise2, conclusion, constraint); return new AppStepDefault(premise1, premise2, conclusion, constraint);
} }
/** /**
* Creates an ConstStepDefault. * Creates an ConstStepDefault.
* @param conclusion the conclusion of this step * @param conclusion the conclusion of this step
* @param constraint the constraint that can be derived from this step * @param constraint the constraint that can be derived from this step
* @return the created ConstStepDefault * @return the created ConstStepDefault
*/ */
@Override
public ConstStepDefault createConstStep(Conclusion conclusion, Constraint constraint) { public ConstStepDefault createConstStep(Conclusion conclusion, Constraint constraint) {
return new ConstStepDefault(conclusion, constraint); return new ConstStepDefault(conclusion, constraint);
} }
/** /**
* Creates a VarStepDefault. * Creates a VarStepDefault.
* @param typeAbstraction the type abstraction of this step * @param typeAbstraction the type abstraction of this step
* @param instantiatedTypeAbs an instantiation of the type abstraction used in this step
* @param conclusion the conclusion of this step * @param conclusion the conclusion of this step
* @param constraint the constraint that can be derived from this step * @param constraint the constraint that can be derived from this step
* @return the created AbsStepDefault * @return the created AbsStepDefault
*/ */
public VarStepDefault createVarStep(TypeAbstraction typeAbstraction, Conclusion conclusion, @Override
Constraint constraint) { public VarStepDefault createVarStep(TypeAbstraction typeAbstraction, Type instantiatedTypeAbs,
return new VarStepDefault(typeAbstraction, conclusion, constraint); Conclusion conclusion, Constraint constraint) {
return new VarStepDefault(typeAbstraction, instantiatedTypeAbs, conclusion, constraint);
} }
} }

16
src/main/java/edu/kit/typicalc/model/step/StepFactoryWithLet.java
View File

@ -2,12 +2,14 @@ package edu.kit.typicalc.model.step;
import edu.kit.typicalc.model.Conclusion; import edu.kit.typicalc.model.Conclusion;
import edu.kit.typicalc.model.Constraint; import edu.kit.typicalc.model.Constraint;
import edu.kit.typicalc.model.type.Type;
import edu.kit.typicalc.model.type.TypeAbstraction; import edu.kit.typicalc.model.type.TypeAbstraction;
/** /**
* A factory to create InferenceStep objects when let polymorphism is used. * A factory to create InferenceStep objects when let polymorphism is used.
*/ */
public class StepFactoryWithLet implements StepFactory { public class StepFactoryWithLet implements StepFactory {
/** /**
* Creates an AbsStepWithLet. * Creates an AbsStepWithLet.
* @param premise the premise of this step * @param premise the premise of this step
@ -15,6 +17,7 @@ public class StepFactoryWithLet implements StepFactory {
* @param constraint the constraint that can be derived from this step * @param constraint the constraint that can be derived from this step
* @return the created AbsStepWithLet * @return the created AbsStepWithLet
*/ */
@Override
public AbsStepWithLet createAbsStep(InferenceStep premise, Conclusion conclusion, Constraint constraint) { public AbsStepWithLet createAbsStep(InferenceStep premise, Conclusion conclusion, Constraint constraint) {
return new AbsStepWithLet(premise, conclusion, constraint); return new AbsStepWithLet(premise, conclusion, constraint);
} }
@ -27,28 +30,35 @@ public class StepFactoryWithLet implements StepFactory {
* @param constraint the constraint that can be derived from this step * @param constraint the constraint that can be derived from this step
* @return the created AppStepDefault * @return the created AppStepDefault
*/ */
@Override
public AppStepDefault createAppStep(InferenceStep premise1, InferenceStep premise2, public AppStepDefault createAppStep(InferenceStep premise1, InferenceStep premise2,
Conclusion conclusion, Constraint constraint) { Conclusion conclusion, Constraint constraint) {
return new AppStepDefault(premise1, premise2, conclusion, constraint); return new AppStepDefault(premise1, premise2, conclusion, constraint);
} }
/** /**
* Creates an ConstStepDefault. * Creates an ConstStepDefault.
* @param conclusion the conclusion of this step * @param conclusion the conclusion of this step
* @param constraint the constraint that can be derived from this step * @param constraint the constraint that can be derived from this step
* @return the created ConstStepDefault * @return the created ConstStepDefault
*/ */
@Override
public ConstStepDefault createConstStep(Conclusion conclusion, Constraint constraint) { public ConstStepDefault createConstStep(Conclusion conclusion, Constraint constraint) {
return new ConstStepDefault(conclusion, constraint); return new ConstStepDefault(conclusion, constraint);
} }
/** /**
* Creates a VarStepWithLet. * Creates a VarStepWithLet.
*
* @param typeAbstraction the type abstraction of this step * @param typeAbstraction the type abstraction of this step
* @param instantiatedTypeAbs an instantiation of the type abstraction used in this step
* @param conclusion the conclusion of this step * @param conclusion the conclusion of this step
* @param constraint the constraint that can be derived from this step * @param constraint the constraint that can be derived from this step
* @return the created VarStepWithLet * @return the created VarStepWithLet
*/ */
public VarStepWithLet createVarStep(TypeAbstraction typeAbstraction, Conclusion conclusion, @Override
Constraint constraint) { public VarStepWithLet createVarStep(TypeAbstraction typeAbstraction, Type instantiatedTypeAbs,
return new VarStepWithLet(typeAbstraction, conclusion, constraint); Conclusion conclusion, Constraint constraint) {
return new VarStepWithLet(typeAbstraction, instantiatedTypeAbs, conclusion, constraint);
} }
} }

23
src/main/java/edu/kit/typicalc/model/step/VarStep.java
View File

@ -2,6 +2,7 @@ package edu.kit.typicalc.model.step;
import edu.kit.typicalc.model.Conclusion; import edu.kit.typicalc.model.Conclusion;
import edu.kit.typicalc.model.Constraint; import edu.kit.typicalc.model.Constraint;
import edu.kit.typicalc.model.type.Type;
import edu.kit.typicalc.model.type.TypeAbstraction; import edu.kit.typicalc.model.type.TypeAbstraction;
/** /**
@ -9,24 +10,40 @@ import edu.kit.typicalc.model.type.TypeAbstraction;
* abstraction that is identified as the type of the variable in the premise of the step. * abstraction that is identified as the type of the variable in the premise of the step.
*/ */
public abstract class VarStep extends InferenceStep { public abstract class VarStep extends InferenceStep {
private TypeAbstraction typeAbstractionInPremise;
private final TypeAbstraction typeAbstractionInPremise;
private final Type instantiatedTypeAbs;
/** /**
* Initializes a new VarStep with the given values. * Initializes a new VarStep with the given values.
*
* @param typeAbstractionInPremise the type abstraction in the premise of this step
* @param instantiatedTypeAbs an instantiation of the type abstraction used in this step
* @param conclusion the conclusion of this step * @param conclusion the conclusion of this step
* @param constraint the constraint added in this step * @param constraint the constraint added in this step
* @param typeAbstractionInPremise the type abstraction in the premise of this step
*/ */
protected VarStep(TypeAbstraction typeAbstractionInPremise, Conclusion conclusion, Constraint constraint) { protected VarStep(TypeAbstraction typeAbstractionInPremise, Type instantiatedTypeAbs, Conclusion conclusion,
Constraint constraint) {
super(conclusion, constraint); super(conclusion, constraint);
this.typeAbstractionInPremise = typeAbstractionInPremise; this.typeAbstractionInPremise = typeAbstractionInPremise;
this.instantiatedTypeAbs = instantiatedTypeAbs;
} }
/** /**
* Returns the type abstraction in the premise of the step, that is identified as the * Returns the type abstraction in the premise of the step, that is identified as the
* variable’s type. * variable’s type.
*
* @return the type abstraction in the premise of this step * @return the type abstraction in the premise of this step
*/ */
public TypeAbstraction getTypeAbsInPremise() { public TypeAbstraction getTypeAbsInPremise() {
return typeAbstractionInPremise; return typeAbstractionInPremise;
} }
/**
* Returns the instantiation of the type abstraction.
*
* @return the instantiation of the type abstraction.
*/
public Type getInstantiatedTypeAbs() {
return instantiatedTypeAbs;
}
} }

10
src/main/java/edu/kit/typicalc/model/step/VarStepDefault.java
View File

@ -2,17 +2,21 @@ package edu.kit.typicalc.model.step;
import edu.kit.typicalc.model.Conclusion; import edu.kit.typicalc.model.Conclusion;
import edu.kit.typicalc.model.Constraint; import edu.kit.typicalc.model.Constraint;
import edu.kit.typicalc.model.type.Type;
import edu.kit.typicalc.model.type.TypeAbstraction; import edu.kit.typicalc.model.type.TypeAbstraction;
public class VarStepDefault extends VarStep { public class VarStepDefault extends VarStep {
/** /**
* Initializes a new VarStep with the given values. * Initializes a new VarStep with the given values.
*
* @param typeAbstractionInPremise the type abstraction in the premise of this step
* @param instantiatedTypeAbs an instantiation of the type abstraction used in this step
* @param conclusion the conclusion of this step * @param conclusion the conclusion of this step
* @param constraint the constraint added in this step * @param constraint the constraint added in this step
* @param typeAbstractionInPremise the type abstraction in the premise of this step
*/ */
public VarStepDefault(TypeAbstraction typeAbstractionInPremise, Conclusion conclusion, Constraint constraint) { public VarStepDefault(TypeAbstraction typeAbstractionInPremise, Type instantiatedTypeAbs, Conclusion conclusion,
super(typeAbstractionInPremise, conclusion, constraint); Constraint constraint) {
super(typeAbstractionInPremise, instantiatedTypeAbs, conclusion, constraint);
} }
/** /**

10
src/main/java/edu/kit/typicalc/model/step/VarStepWithLet.java
View File

@ -2,17 +2,21 @@ package edu.kit.typicalc.model.step;
import edu.kit.typicalc.model.Conclusion; import edu.kit.typicalc.model.Conclusion;
import edu.kit.typicalc.model.Constraint; import edu.kit.typicalc.model.Constraint;
import edu.kit.typicalc.model.type.Type;
import edu.kit.typicalc.model.type.TypeAbstraction; import edu.kit.typicalc.model.type.TypeAbstraction;
public class VarStepWithLet extends VarStep { public class VarStepWithLet extends VarStep {
/** /**
* Initializes a new VarStep with the given values. * Initializes a new VarStep with the given values.
*
* @param typeAbstractionInPremise the type abstraction in the premise of this step
* @param instantiatedTypeAbs an instantiation of the type abstraction used in this step
* @param conclusion the conclusion of this step * @param conclusion the conclusion of this step
* @param constraint the constraint added in this step * @param constraint the constraint added in this step
* @param typeAbstractionInPremise the type abstraction in the premise of this step
*/ */
public VarStepWithLet(TypeAbstraction typeAbstractionInPremise, Conclusion conclusion, Constraint constraint) { public VarStepWithLet(TypeAbstraction typeAbstractionInPremise, Type instantiatedTypeAbs, Conclusion conclusion,
super(typeAbstractionInPremise, conclusion, constraint); Constraint constraint) {
super(typeAbstractionInPremise, instantiatedTypeAbs, conclusion, constraint);
} }
/** /**

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

@ -75,5 +75,6 @@ public interface TermVisitorTree {
* of the returned inference step will be assigned * of the returned inference step will be assigned
* @return an {@link edu.kit.typicalc.model.step.VarStep} * @return an {@link edu.kit.typicalc.model.step.VarStep}
*/ */
InferenceStep visit(VarTerm varTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType); InferenceStep visit(VarTerm varTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType)
throws IllegalStateException;
} }

5
src/main/java/edu/kit/typicalc/model/type/TypeAbstraction.java
View File

@ -1,5 +1,7 @@
package edu.kit.typicalc.model.type; package edu.kit.typicalc.model.type;
import edu.kit.typicalc.model.TypeVariableFactory;
import java.util.List; import java.util.List;
public class TypeAbstraction { public class TypeAbstraction {
@ -9,4 +11,7 @@ public class TypeAbstraction {
public TypeAbstraction(Type type) { public TypeAbstraction(Type type) {
} }
public Type instantiate(TypeVariableFactory typeVarFactory) {
return null;
}
} }

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

@ -1,9 +1,8 @@
package edu.kit.typicalc.view.content.infocontent; package edu.kit.typicalc.view.content.infocontent;
import com.vaadin.flow.component.button.Button; import com.vaadin.flow.component.button.Button;
import com.vaadin.flow.component.notification.Notification; import com.vaadin.flow.component.dependency.JsModule;
import com.vaadin.flow.component.orderedlayout.VerticalLayout; import com.vaadin.flow.component.orderedlayout.VerticalLayout;
import com.vaadin.flow.component.textfield.TextArea;
import com.vaadin.flow.router.PageTitle; import com.vaadin.flow.router.PageTitle;
import com.vaadin.flow.router.Route; import com.vaadin.flow.router.Route;
import com.vaadin.flow.router.RouteAlias; import com.vaadin.flow.router.RouteAlias;
@ -13,23 +12,17 @@ import edu.kit.typicalc.view.main.MathjaxDisplay;
@Route(value = "home", layout = MainViewImpl.class) @Route(value = "home", layout = MainViewImpl.class)
@PageTitle("Typicalc") @PageTitle("Typicalc")
@RouteAlias(value = "", layout = MainViewImpl.class) @RouteAlias(value = "", layout = MainViewImpl.class)
@JsModule("./src/mathjax-setup.js")
public class StartPageView extends VerticalLayout { public class StartPageView extends VerticalLayout {
private TextArea name;
private Button sayHello; private Button sayHello;
public StartPageView() { public StartPageView() {
// todo implement correctly // todo implement correctly
setId("start-page"); setId("start-page");
name = new TextArea("translation test");
name.setValue(getTranslation("abs-rule"));
name.setWidthFull();
add(new MathjaxDisplay()); add(new MathjaxDisplay());
sayHello = new Button("Say hello"); sayHello = new Button("Say hello");
add(name, sayHello); add(sayHello);
sayHello.addClickListener(e -> {
Notification.show("Hello " + name.getValue());
});
} }
} }

2
src/main/java/edu/kit/typicalc/view/main/MathjaxDisplay.java
View File

@ -16,7 +16,7 @@ public class MathjaxDisplay extends LitTemplate {
* Creates the hello world template. * Creates the hello world template.
*/ */
public MathjaxDisplay() { public MathjaxDisplay() {
content.add("testtestetstest"); content.add(getTranslation("abs-rule"));
} }
} }

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

@ -2,7 +2,6 @@ package edu.kit.typicalc.view.main;
import com.vaadin.flow.component.applayout.DrawerToggle; import com.vaadin.flow.component.applayout.DrawerToggle;
import com.vaadin.flow.component.dependency.CssImport; import com.vaadin.flow.component.dependency.CssImport;
import com.vaadin.flow.component.dialog.Dialog;
import com.vaadin.flow.component.html.H1; import com.vaadin.flow.component.html.H1;
import com.vaadin.flow.component.icon.Icon; import com.vaadin.flow.component.icon.Icon;
import com.vaadin.flow.component.icon.VaadinIcon; import com.vaadin.flow.component.icon.VaadinIcon;

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

@ -1,5 +1,6 @@
root.close=Schließen root.close=Schließen
root.copyLatex=Kopiere Latex-Code root.copyLatex=Kopiere Latex-Code
root.typicalc=Typicalc
abs-rule=\\begin{prooftree}\ abs-rule=\\begin{prooftree}\
\\AxiomC{$\\Gamma=\\vdash t_1 : \\tau_1 \\rightarrow \\tau_2$}\ \\AxiomC{$\\Gamma=\\vdash t_1 : \\tau_1 \\rightarrow \\tau_2$}\
@ -13,4 +14,6 @@ abs-rule=\\begin{prooftree}\
test=hello world test=hello world
root.typicalc=Typicalc root.typicalc=Typicalc
root.lambda=\u03BB root.lambda=\u03BB
root.typeInfer=Typisieren root.typeInfer=Typisieren

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

@ -1,3 +1,7 @@
root.close=Close
root.copyLatex=Copy latex code
root.typicalc=Typicalc
abs-rule=\ abs-rule=\
\\begin{prooftree}\n\ \\begin{prooftree}\n\
\\AxiomC{$\\Gamma=\\vdash t_1 : \\tau_1 \\rightarrow \\tau_2$}\n\ \\AxiomC{$\\Gamma=\\vdash t_1 : \\tau_1 \\rightarrow \\tau_2$}\n\
@ -6,7 +10,3 @@ abs-rule=\
\\LeftLabel{APP}\n\ \\LeftLabel{APP}\n\
\\BinaryInfC{$\\Gamma \\vdash t_1 \\ t_2 : \\tau_2$}\n\ \\BinaryInfC{$\\Gamma \\vdash t_1 \\ t_2 : \\tau_2$}\n\
\\end{prooftree} \\end{prooftree}
test=hello world
root.close=Close
root.copyLatex=Copy latex code