diff --git a/static/bergamot/rendering/lc.bergamot b/assets/bergamot/rendering/lc.bergamot similarity index 100% rename from static/bergamot/rendering/lc.bergamot rename to assets/bergamot/rendering/lc.bergamot diff --git a/content/blog/00_types_intro.md b/content/blog/00_types_intro/index.md similarity index 97% rename from content/blog/00_types_intro.md rename to content/blog/00_types_intro/index.md index 6f0b4b3..72c5795 100644 --- a/content/blog/00_types_intro.md +++ b/content/blog/00_types_intro/index.md @@ -6,7 +6,12 @@ series: "Everything I Know About Types" draft: true bergamot: render_presets: - default: "lc.bergamot" + default: "bergamot/rendering/lc.bergamot" + presets: + intro: + prompt: "type(TERM, ?t)" + query: "" + file: "intro.bergamot" --- I am in love with types and type systems. They are, quite probably, @@ -171,12 +176,6 @@ 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 Bergamot, I will denote this with a play button. -{{< bergamot_preset name="intro-preset" prompt="type(TERM, ?t)" >}} -TNumber @ type(lit(?n), number) <- num(?n); -TPlusI @ type(plus(?e_1, ?e_2), number) <- - type(?e_1, number), type(?e_2, number); -{{< /bergamot_preset >}} - -{{< bergamot_exercise label="bergamot; sample exercise" preset="intro-preset" id="exercise-2" >}} +{{< bergamot_exercise label="bergamot; sample exercise" preset="intro" id="exercise-2" >}} Try typing `1+1` into the input field! {{< /bergamot_exercise >}} diff --git a/content/blog/00_types_intro/intro.bergamot b/content/blog/00_types_intro/intro.bergamot new file mode 100644 index 0000000..c346529 --- /dev/null +++ b/content/blog/00_types_intro/intro.bergamot @@ -0,0 +1,3 @@ +TNumber @ type(lit(?n), number) <- num(?n); +TPlusI @ type(plus(?e_1, ?e_2), number) <- + type(?e_1, number), type(?e_2, number); diff --git a/content/blog/01_types_basics/conversion.bergamot b/content/blog/01_types_basics/conversion.bergamot new file mode 100644 index 0000000..ea85571 --- /dev/null +++ b/content/blog/01_types_basics/conversion.bergamot @@ -0,0 +1,19 @@ +section "Conversion rules" { + ConvertsIS @ converts(integer, string) <-; + ConvertsIF @ converts(integer, float) <-; + ConvertsFS @ converts(float, string) <-; +} + +section "Rules for literals" { + TInt @ type(lit(?n), integer) <- int(?n); + TFloat @ type(lit(?f), float) <- float(?f); + TString @ type(lit(?s), string) <- str(?s); +} + +section "" { + TPlusInt @ type(plus(?e_1, ?e_2), integer) <- type(?e_1, integer), type(?e_2, integer); + TPlusFloat @ type(plus(?e_1, ?e_2), float) <- type(?e_1, float), type(?e_2, float); + TPlusString @ type(plus(?e_1, ?e_2), string) <- type(?e_1, string), type(?e_2, string); +} + +TConverts @ type(?e, ?tau_2) <- type(?e, ?tau_1), converts(?tau_1, ?tau_2); diff --git a/content/blog/01_types_basics.md b/content/blog/01_types_basics/index.md similarity index 95% rename from content/blog/01_types_basics.md rename to content/blog/01_types_basics/index.md index af5ded9..bcf0a55 100644 --- a/content/blog/01_types_basics.md +++ b/content/blog/01_types_basics/index.md @@ -6,7 +6,21 @@ series: "Everything I Know About Types" draft: true bergamot: render_presets: - default: "lc.bergamot" + default: "bergamot/rendering/lc.bergamot" + presets: + notation: + prompt: "type(TERM, ?t)" + query: "" + file: "notation.bergamot" + string: + prompt: "type(TERM, ?t)" + query: "\"hello\"+\"world\"" + file: "string.bergamot" + conversion: + prompt: "type(TERM, ?t)" + query: "" + file: "conversion.bergamot" + --- It's finally time to start looking at types. As I mentioned, I want @@ -114,11 +128,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), 27 different ways of writing down substitutions were observed in the POPL conference alone. -{{< bergamot_preset name="notation-preset" prompt="type(TERM, ?t)" >}} -TNumber @ type(lit(?n), number) <- num(?n); -{{< /bergamot_preset >}} - -{{< bergamot_exercise label="bergamot; tweaking notation" preset="notation-preset" id="exercise-1" >}} +{{< bergamot_exercise label="bergamot; tweaking notation" preset="notation" 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`). @@ -317,13 +327,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}\). -{{< bergamot_preset name="string-preset" prompt="type(TERM, ?t)" query="\"hello\"+\"world\"">}} -TNumber @ type(lit(?n), number) <- num(?n); -TPlusI @ type(plus(?e_1, ?e_2), number) <- - type(?e_1, number), type(?e_2, number); -{{< /bergamot_preset >}} - -{{< bergamot_exercise label="bergamot; adding rules for strings" preset="string-preset" id="exercise-2" >}} +{{< bergamot_exercise label="bergamot; adding rules for strings" preset="string" 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. @@ -384,29 +388,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) ain't bad, either. -{{< bergamot_preset name="conversion-preset" prompt="type(TERM, ?t)" >}} -section "Conversion rules" { - ConvertsIS @ converts(integer, string) <-; - ConvertsIF @ converts(integer, float) <-; - ConvertsFS @ converts(float, string) <-; -} - -section "Rules for literals" { - TInt @ type(lit(?n), integer) <- int(?n); - TFloat @ type(lit(?f), float) <- float(?f); - TString @ type(lit(?s), string) <- str(?s); -} - -section "" { - TPlusInt @ type(plus(?e_1, ?e_2), integer) <- type(?e_1, integer), type(?e_2, integer); - TPlusFloat @ type(plus(?e_1, ?e_2), float) <- type(?e_1, float), type(?e_2, float); - TPlusString @ type(plus(?e_1, ?e_2), string) <- type(?e_1, string), type(?e_2, string); -} - -TConverts @ type(?e, ?tau_2) <- type(?e, ?tau_1), converts(?tau_1, ?tau_2); -{{< /bergamot_preset >}} - -{{< bergamot_exercise label="advanced; a taste of conversions" preset="conversion-preset" id="exercise-3" >}} +{{< bergamot_exercise label="advanced; a taste of conversions" preset="conversion" id="exercise-3" >}} This exercise is simply an early taste of formalizing conversions, which allow users to (for example) write numbers where the language expects strings, with the understanding that the number will be automatically turned into a string. diff --git a/content/blog/01_types_basics/notation.bergamot b/content/blog/01_types_basics/notation.bergamot new file mode 100644 index 0000000..fbb16a6 --- /dev/null +++ b/content/blog/01_types_basics/notation.bergamot @@ -0,0 +1 @@ +TNumber @ type(lit(?n), number) <- num(?n); diff --git a/content/blog/01_types_basics/string.bergamot b/content/blog/01_types_basics/string.bergamot new file mode 100644 index 0000000..c346529 --- /dev/null +++ b/content/blog/01_types_basics/string.bergamot @@ -0,0 +1,3 @@ +TNumber @ type(lit(?n), number) <- num(?n); +TPlusI @ type(plus(?e_1, ?e_2), number) <- + type(?e_1, number), type(?e_2, number); diff --git a/content/blog/bergamot/index.md b/content/blog/bergamot/index.md index cf1a512..645dff2 100644 --- a/content/blog/bergamot/index.md +++ b/content/blog/bergamot/index.md @@ -5,7 +5,7 @@ tags: ["Project", "Programming Languages"] description: "In this post, I show off Bergamot, a tiny logic programming language and an idea for teaching inference rules." bergamot: render_presets: - default: "lc.bergamot" + default: "bergamot/rendering/lc.bergamot" --- ### Inference Rules and the Study of Programming Languages diff --git a/themes/vanilla b/themes/vanilla index dee7579..3a281df 160000 --- a/themes/vanilla +++ b/themes/vanilla @@ -1 +1 @@ -Subproject commit dee7579b2956fda6ca64819fa7d08b2832a235a9 +Subproject commit 3a281dfa8aff1ac87d33d8f5ffcfc0a931a9656a