From a6f3bccf649193aa29c669f54dabe68e4fe31ee2 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Thu, 28 Dec 2023 16:05:15 -0800 Subject: [PATCH] Use markdown for exercises, since it works fine out of the box. Signed-off-by: Danila Fedorin --- content/blog/00_types_intro.md | 2 +- content/blog/01_types_basics.md | 48 ++++++++++++----------- layouts/shortcodes/bergamot_exercise.html | 2 +- 3 files changed, 28 insertions(+), 24 deletions(-) diff --git a/content/blog/00_types_intro.md b/content/blog/00_types_intro.md index db1fa57..751e748 100644 --- a/content/blog/00_types_intro.md +++ b/content/blog/00_types_intro.md @@ -178,5 +178,5 @@ TPlusI @ type(plus(?e_1, ?e_2), number) <- {{< /bergamot_preset >}} {{< bergamot_exercise label="bergamot; sample exercise" preset="intro-preset" id="exercise-2" >}} -Try typing 1+1 into the input field! +Try typing `1+1` into the input field! {{< /bergamot_exercise >}} diff --git a/content/blog/01_types_basics.md b/content/blog/01_types_basics.md index 59e11bc..e319558 100644 --- a/content/blog/01_types_basics.md +++ b/content/blog/01_types_basics.md @@ -120,16 +120,16 @@ TNumber @ type(lit(?n), number) <- num(?n); {{< bergamot_exercise label="bergamot; tweaking notation" preset="notation-preset" id="exercise-1" >}} Bergamot, the interactive tool I've developed for doing exercises, supports -customizing the notation for rules. Try changing the \(:\) symbol to -the \(\sim\) symbol (denoted in latex as \sim).
-
+customizing the notation for rules. Try changing the \\(:\\) symbol to +the \\(\\sim\\) symbol (denoted in latex as `\sim`). + To change the way that rules are rendered, click the "Presentation Rules" tab in the "Rules" section. There will be a lot there: I've added rules for pretty-printing a fair amount of the standard programming languages notation. -Scroll down to LatexTypeBin, and change : to -\\sim on that line (the extra backslash is to handle string +Scroll down to `LatexTypeBin`, and change `:` to +`\\sim` on that line (the extra backslash is to handle string escaping). Now try typing numbers into the input box; you should see -something like \(1 \sim \text{number} \) +something like \\(1 \\sim \text{number} \\) {{< /bergamot_exercise >}} One more thing. So far, we've only written down one claim: the value 1 is a number. @@ -326,26 +326,30 @@ TPlusI @ type(plus(?e_1, ?e_2), number) <- {{< bergamot_exercise label="bergamot; adding rules for strings" preset="string-preset" id="exercise-2" >}} Try writing the Bergamot rules that correspond to the inference rule for strings above. I've provided the rules for numbers; the rules for strings should be quite -similar.
-
-In Bergamot, the claim that an expression e has type t -is written as type(e, t). A rule looks like RuleName @ conclusion <- premise1, premise2;. -Thus, the rule 
TNumber @ type(lit(?n), number) <- num(?n);
-
-Has one premise, that the term \(n\) is a number, and the conclusion is that -a number literal has type \(\text{number}\). The num condition -is a Bergamot builtin, corresponding to our earlier notation of \(n \in \texttt{Num}\). -It holds for all numbers: it's always true that num(1), num(2), -etc. The equivalent builtin for something being a string is str.
-
+similar. + +In Bergamot, the claim that an expression `e` has type `t` +is written as `type(e, t)`. A rule looks like `RuleName @ conclusion <- premise1, premise2;`. +Thus, the rule + +``` +TNumber @ type(lit(?n), number) <- num(?n); +``` + +Has one premise, that the term \\(n\\) is a number, and the conclusion is that +a number literal has type \\(\\text{number}\\). The `num` condition +is a Bergamot builtin, corresponding to our earlier notation of \\(n \\in \\texttt{Num}\\). +It holds for all numbers: it's always true that `num(1)`, `num(2)`, +etc. The equivalent builtin for something being a string is `str`. + To edit the rules in Bergamot, click the "Editor" button in the "Rules" section. You will need to add two rules, just like we did for numbers: -a rule for string literals (something like \(\texttt{"Hello"} : \text{string}\), +a rule for string literals (something like \\(\\texttt{\"Hello\"} : \\text{string}\\), but more general) and for adding two strings together. I suggest naming -these two rules TString and TPlusS respectively.
-
+these two rules `TString` and `TPlusS` respectively. + When you're done, you should be able to properly determine the types of -expressions such as "Hello" and "Hello" + "World". +expressions such as `"Hello"` and `"Hello" + "World"`. {{< /bergamot_exercise >}} These rules generally work in other languages. Things get more complicated in languages like Java and Rust, diff --git a/layouts/shortcodes/bergamot_exercise.html b/layouts/shortcodes/bergamot_exercise.html index 817c3ba..444406d 100644 --- a/layouts/shortcodes/bergamot_exercise.html +++ b/layouts/shortcodes/bergamot_exercise.html @@ -6,7 +6,7 @@ {{ if or (eq (.Get "label") "") (eq (.Get "label") nil) }}{{ else }}({{ .Get "label" }}){{ end }}: - {{ .Inner }} + {{ transform.Markdownify .Inner }}
{{ if or (eq (.Get "preset") "") (eq (.Get "preset") nil) }}