64 lines
2.4 KiB
HTML
64 lines
2.4 KiB
HTML
<!DOCTYPE HTML>
|
|
<html>
|
|
<head>
|
|
<meta charset="UTF-8">
|
|
<meta name="viewport" content="width=device-width, initial-scale=1" />
|
|
<title>Main</title>
|
|
<script type="module" src="https://unpkg.com/@navsnpm/katex-expression/dist/katex-expression/katex-expression.esm.js"></script>
|
|
<script nomodule="" src="https://unpkg.com/@navsnpm/katex-expression/dist/katex-expression/katex-expression.js"></script>
|
|
<style>body { padding: 0; margin: 0; }</style>
|
|
<style>
|
|
textarea {
|
|
display: block;
|
|
width: 100%;
|
|
height: 10em;
|
|
resize: none;
|
|
}
|
|
|
|
input[type="text"] {
|
|
width: 100%;
|
|
}
|
|
|
|
.rule-list {
|
|
display: flex;
|
|
flex-direction: row;
|
|
flex-wrap: wrap;
|
|
justify-content: center;
|
|
}
|
|
|
|
.rule-list katex-expression {
|
|
margin-left: .5em;
|
|
margin-right: .5em;
|
|
flex-grow: 1;
|
|
flex-basis: 0;
|
|
}
|
|
|
|
.elm-root {
|
|
max-width: 800px;
|
|
margin: auto;
|
|
padding: 1em;
|
|
border: 1px solid #c3c3c3;
|
|
border-radius: 0.5em;
|
|
margin-top: 1em;
|
|
}
|
|
|
|
.elm-root h2 {
|
|
margin-bottom: 0.5em;
|
|
font-family: sans-serif;
|
|
font-weight: normal;
|
|
}
|
|
</style>
|
|
</head>
|
|
|
|
<body>
|
|
<div id="elm"></div>
|
|
<script src="index.js"></script>
|
|
<script>
|
|
var app = Elm.Main.init({
|
|
node: document.getElementById('elm'),
|
|
flags: { rules: "TInt @ type(?Gamma, intlit(?n), tint) <-;\nTString @ type(?Gamma, strlit(?s), tstr) <-;\nTVar @ type(?Gamma, var(?x), ?tau) <- inenv(?x, ?tau, ?Gamma);\nTPlusI @ type(?Gamma, plus(?e_1, ?e_2), tint) <- type(?Gamma, ?e_1, tint), type(?Gamma, ?e_2, tint);\nTPlusS @ type(?Gamma, plus(?e_1, ?e_2), tstr) <- type(?Gamma, ?e_1, tstr), type(?Gamma, ?e_2, tstr);\nTPair @ type(?Gamma, pair(?e_1, ?e_2), tpair(?tau_1, ?tau_2)) <- type(?Gamma, ?e_1, ?tau_1), type(?Gamma, ?e_2, ?tau_2);\nTFst @ type(?Gamma, fst(?e), ?tau_1) <- type(?Gamma, ?e, tpair(?tau_1, ?tau_2));\nTSnd @ type(?Gamma, snd(?e), ?tau_2) <- type(?Gamma, ?e, tpair(?tau_1, ?tau_2));\nTAbs @ type(?Gamma, abs(?x, ?tau_1, ?e), tarr(?tau_1, ?tau_2)) <- type(extend(?Gamma, ?x, ?tau_1), ?e, ?tau_2);\nTApp @ type(?Gamma, app(?e_1, ?e_2), ?tau_2) <- type(?Gamma, ?e_1, tarr(?tau_1, ?tau_2)), type(?Gamma, ?e_2, ?tau_1);\n\nGammaTake @ inenv(?x, ?tau_1, extend(?Gamma, ?x, ?tau_1)) <-;\nGammaSkip @ inenv(?x, ?tau_1, extend(?Gamma, ?y, ?tau_2)) <- inenv(?x, ?tau_1, ?Gamma);", query: "type(empty, app(abs(x, tint, var(x)), intlit(1)), ?tau)" }
|
|
});
|
|
</script>
|
|
</body>
|
|
</html>
|