Update to new Bergamot version

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-09-15 10:33:40 -07:00
parent e4101f1396
commit dde7df4604
5 changed files with 63 additions and 8 deletions

View File

@ -45,6 +45,7 @@ defaultContentLanguage = 'en'
[params] [params]
bergamotJsUrl = "https://static.danilafe.com/bergamot/bergamot.js" bergamotJsUrl = "https://static.danilafe.com/bergamot/bergamot.js"
bergamotObjectLanguageJsUrl = "https://static.danilafe.com/bergamot/objectlang.js"
katexJsUrl = "https://static.danilafe.com/katex/katex.min.js" katexJsUrl = "https://static.danilafe.com/katex/katex.min.js"
plausibleAnalyticsDomain = "danilafe.com" plausibleAnalyticsDomain = "danilafe.com"
githubUsername = "DanilaFe" githubUsername = "DanilaFe"

View File

@ -171,7 +171,7 @@ to the tool than to type theory itself; I will denote these exercises as such wh
possible. Also, whenever the context of the exercise can be loaded into possible. Also, whenever the context of the exercise can be loaded into
Bergamot, I will denote this with a play button. Bergamot, I will denote this with a play button.
{{< bergamot_preset name="intro-preset" prompt="PromptConverter @ prompt(type(?term, ?t)) <- input(?term);" >}} {{< bergamot_preset name="intro-preset" prompt="type(TERM, ?t)" >}}
TNumber @ type(lit(?n), number) <- num(?n); TNumber @ type(lit(?n), number) <- num(?n);
TPlusI @ type(plus(?e_1, ?e_2), number) <- TPlusI @ type(plus(?e_1, ?e_2), number) <-
type(?e_1, number), type(?e_2, number); type(?e_1, number), type(?e_2, number);

View File

@ -114,7 +114,7 @@ Another consequence of this is that not everyone agrees on notation; according
to [this paper](https://labs.oracle.com/pls/apex/f?p=LABS:0::APPLICATION_PROCESS%3DGETDOC_INLINE:::DOC_ID:959), to [this paper](https://labs.oracle.com/pls/apex/f?p=LABS:0::APPLICATION_PROCESS%3DGETDOC_INLINE:::DOC_ID:959),
27 different ways of writing down substitutions were observed in the POPL conference alone. 27 different ways of writing down substitutions were observed in the POPL conference alone.
{{< bergamot_preset name="notation-preset" prompt="PromptConverter @ prompt(type(?term, ?t)) <- input(?term);" >}} {{< bergamot_preset name="notation-preset" prompt="type(TERM, ?t)" >}}
TNumber @ type(lit(?n), number) <- num(?n); TNumber @ type(lit(?n), number) <- num(?n);
{{< /bergamot_preset >}} {{< /bergamot_preset >}}
@ -317,7 +317,7 @@ This rule is read as follows:
> If \(e_1\) and \(e_2\) have type \(\text{string}\), then \(e_1+e_2\) has type \(\text{string}\). > If \(e_1\) and \(e_2\) have type \(\text{string}\), then \(e_1+e_2\) has type \(\text{string}\).
{{< bergamot_preset name="string-preset" prompt="PromptConverter @ prompt(type(?term, ?t)) <- input(?term);" query="\"hello\"+\"world\"">}} {{< bergamot_preset name="string-preset" prompt="type(TERM, ?t)" query="\"hello\"+\"world\"">}}
TNumber @ type(lit(?n), number) <- num(?n); TNumber @ type(lit(?n), number) <- num(?n);
TPlusI @ type(plus(?e_1, ?e_2), number) <- TPlusI @ type(plus(?e_1, ?e_2), number) <-
type(?e_1, number), type(?e_2, number); type(?e_1, number), type(?e_2, number);
@ -384,7 +384,7 @@ from the conversion rules. Chapter 15 of _Types and Programming Languages_
by Benjamin Pierce is a nice explanation, but the [Wikipedia page](https://en.wikipedia.org/wiki/Subtyping) by Benjamin Pierce is a nice explanation, but the [Wikipedia page](https://en.wikipedia.org/wiki/Subtyping)
ain't bad, either. ain't bad, either.
{{< bergamot_preset name="conversion-preset" prompt="PromptConverter @ prompt(type(?term, ?t)) <- input(?term);" >}} {{< bergamot_preset name="conversion-preset" prompt="type(TERM, ?t)" >}}
section "Conversion rules" { section "Conversion rules" {
ConvertsIS @ converts(integer, string) <-; ConvertsIS @ converts(integer, string) <-;
ConvertsIF @ converts(integer, float) <-; ConvertsIF @ converts(integer, float) <-;
@ -564,7 +564,7 @@ and already be up-to-speed on a big chunk of the content.
| {{< latex >}}\frac{e_1 : \text{number}\quad e_2 : \text{number}}{e_1+e_2 : \text{number}} {{< /latex >}}| Adding numbers gives a number | | {{< latex >}}\frac{e_1 : \text{number}\quad e_2 : \text{number}}{e_1+e_2 : \text{number}} {{< /latex >}}| Adding numbers gives a number |
#### Playground #### Playground
{{< bergamot_widget id="widget" query="" prompt="PromptConverter @ prompt(type(?term, ?t)) <- input(?term);" >}} {{< bergamot_widget id="widget" query="" prompt="type(TERM, ?t)" >}}
section "" { section "" {
TNumber @ type(lit(?n), number) <- num(?n); TNumber @ type(lit(?n), number) <- num(?n);
TString @ type(lit(?s), string) <- str(?s); TString @ type(lit(?s), string) <- str(?s);

View File

@ -261,7 +261,7 @@ It has two modes:
`type(empty, ?e, tpair(number, string))` to search for expressions that have `type(empty, ?e, tpair(number, string))` to search for expressions that have
the type "a pair of a number and a string". the type "a pair of a number and a string".
{{< bergamot_widget id="widget" query="" prompt="PromptConverter @ prompt(type(empty, ?term, ?t)) <- input(?term);" >}} {{< bergamot_widget id="widget" query="" prompt="type(empty, TERM, ?t)" >}}
section "" { section "" {
TNumber @ type(?Gamma, lit(?n), number) <- num(?n); TNumber @ type(?Gamma, lit(?n), number) <- num(?n);
TString @ type(?Gamma, lit(?s), string) <- str(?s); TString @ type(?Gamma, lit(?s), string) <- str(?s);

View File

@ -1,4 +1,5 @@
<script defer src="{{ .Site.Params.bergamotJsUrl }}"></script> <script defer src="{{ .Site.Params.bergamotJsUrl }}"></script>
<script defer src="{{ .Site.Params.bergamotObjectLanguageJsUrl }}"></script>
{{ $style := resources.Get "scss/bergamot.scss" | resources.ToCSS | resources.Minify }} {{ $style := resources.Get "scss/bergamot.scss" | resources.ToCSS | resources.Minify }}
<link rel="stylesheet" href="{{ $style.Permalink }}"> <link rel="stylesheet" href="{{ $style.Permalink }}">
<script defer> <script defer>
@ -95,11 +96,64 @@ const setRunning = (inputGroup, running) => {
} }
} }
// The object language parsing is handling by a separate standalone Elm
// application in the ObjectLanguage module, which has two ports:
//
// * `parseString` requests a string to be parsed
// * `parsedString` returns the parsed string, or null
//
// We want there to be a single global ObjectLanguage object, but it works
// on a "subscription" model (we have to give a callback to its port).
// Configure this callback to invoke `resolve` functions from a list,
// so that callers can just get a promise. This way we aren't continuously
// registering more and more handlers for each parsed string, and we can
// use a convenient promise API.
const parsingPromiseResolvers = {};
const ensureObjectLanguage = () => {
if (!window.Bergamot.ObjectLanguage) {
window.Bergamot.ObjectLanguage = Elm.Bergamot.ObjectLanguage.init({});
window.Bergamot.ObjectLanguage.ports.parsedString.subscribe(({ string, term }) => {
if (string in parsingPromiseResolvers) {
for (const resolver of parsingPromiseResolvers[string]) {
resolver(term);
}
parsingPromiseResolvers[string] = [];
}
});
}
return window.Bergamot.ObjectLanguage;
}
const parseString = (str) => {
if (!(str in parsingPromiseResolvers)) {
parsingPromiseResolvers[str] = [];
}
return new Promise(resolve => {
parsingPromiseResolvers[str].push(resolve);
ensureObjectLanguage().ports.parseString.send(str);
});
}
window.Bergamot = {}; window.Bergamot = {};
window.Bergamot.run = (inputGroup, nodeId, inputPrompt, rules, renderRules, query) => { window.Bergamot.run = (inputGroup, nodeId, inputPrompt, rules, renderRules, input) => {
var app = Elm.Main.init({ var app = Elm.Main.init({
node: document.getElementById(nodeId), node: document.getElementById(nodeId),
flags: { renderRules, inputRules: inputPrompt, rules , query } flags: {
inputModes: {
"Languge Term": { "custom": "Language Term" },
"Query": "query"
},
renderRules, rules, input
}
});
app.ports.convertInput.subscribe(async ({ mode, input }) => {
let query = await parseString(input);
if (query !== null) {
query = inputPrompt.replace("TERM", query);
app.ports.receiveConverted.send({ input, result: { query } });
} else {
app.ports.receiveConverted.send({ input, result: { error: "Unable to parse object language term" } });
}
}); });
loadedWidgets[nodeId] = { app, parentNode: inputGroup ? inputGroup.parentElement : null }; loadedWidgets[nodeId] = { app, parentNode: inputGroup ? inputGroup.parentElement : null };
setRunning(inputGroup, true); setRunning(inputGroup, true);