Try to set up drone for live CI uploads

.drone.yml

@@ -9,3 +9,14 @@ steps:
     - pacman -Sy cmake gcc make llvm bison flex gettext --noconfirm
     - cd code/compiler
     - ./test.sh
+  - name: upload-live
+    image: jguyomard/hugo-builder
+    commands:
+    - echo "$CUSTOM_KEY" | ssh-add -
+    - mkdir -p ~/.ssh
+    - echo -e "Host *\n\tStrictHostKeyChecking no\n\n" > ~/.ssh/config
+    - hugo -D --baseUrl "http://danilafe.com:8080"
+    - rsync -rv -e "ssh -p 22" ./public blog-live@danilafe.com:/var/www/blog-live --checksum
+    environment:
+      CUSTOM_KEY:
+        from_secret: live_ssh_key

content/blog/10_compiler_polymorphism.md

@@ -1,11 +1,11 @@
 ---
 title: Compiling a Functional Language Using C++, Part 10 - Polymorphism
-date: 2019-12-09T23:26:46-08:00
+date: 2020-02-29T20:09:37-08:00
 tags: ["C and C++", "Functional Languages", "Compilers"]
 draft: true
 ---
 
-Last time, we wrote some pretty interesting programs in our little language.
+[In part 8]({{< relref "08_compiler_llvm.md" >}}), we wrote some pretty interesting programs in our little language.
 We successfully expressed arithmetic and recursion. But there's one thing
 that we cannot express in our language without further changes: an `if` statement.
 
@@ -49,17 +49,40 @@ set of rules to describe our program's types. One such set of rules is
 the [Hindley-Milner type system](https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system),
 which we have previously alluded to. In fact, the rules we came up
 with were already very close to Hindley-Milner, with the exception of two:
-__generalization__ and __instantiation__. Instantiation first:
+__generalization__ and __instantiation__. It's been quite a while since the last time we worked on typechecking, so I'm going
+to present a table with these new rules, as well as all of the ones that we previously used. I will also give a quick
+summary of each of these rules.
 
-$$
+Rule|Name and Description
+-----|-------
+{{< latex >}}
 \frac
-{\\Gamma \\vdash e : \\sigma \\quad \\sigma' \\sqsubseteq \\sigma}
-{\\Gamma \\vdash e : \\sigma'}
-$$
-
-Next, generalization:
-$$
+    {x:\sigma \in \Gamma}
+    {\Gamma \vdash x:\sigma}
+{{< /latex >}}| __Var__: If the variable \\(x\\) is known to have some polymorphic type \\(\\sigma\\) then an expression consisting only of that variable is of that type.
+{{< latex >}}
 \frac
-{\\Gamma \\vdash e : \\sigma \\quad \\alpha \\not \\in \\text{free}(\\Gamma)}
-{\\Gamma \\vdash e : \\forall a . \\sigma}
-$$
+    {\Gamma \vdash e_1 : \tau_1 \rightarrow \tau_2 \quad \Gamma \vdash e_2 : \tau_1}
+    {\Gamma \vdash e_1 \; e_2 : \tau_2}
+{{< /latex >}}| __App__: If an expression \\(e\_1\\), which is a function from monomorphic type \\(\\tau\_1\\) to another monomorphic type \\(\\tau\_2\\), is applied to an argument \\(e\_2\\) of type \\(\\tau\_1\\), then the result is of type \\(\\tau\_2\\).
+{{< latex >}}
+\frac
+    {\Gamma, x:\tau \vdash e : \tau'}
+    {\Gamma \vdash \lambda x.e : \tau \rightarrow \tau'}
+{{< /latex >}}| __Abs__: If the body \\(e\\) of a lambda abstraction \\(\\lambda x.e\\) is of type \\(\\tau'\\) when \\(x\\) is of type \\(\\tau\\) then the whole lambda abstraction is of type \\(\\tau \\rightarrow \\tau'\\).
+{{< latex >}}
+\frac
+    {\Gamma \vdash e : \tau \quad \text{matcht}(\tau, p_i) = b_i
+        \quad \Gamma,b_i \vdash e_i : \tau_c}
+    {\Gamma \vdash \text{case} \; e \; \text{of} \;
+        \{ (p_1,e_1) \ldots (p_n, e_n) \} : \tau_c }
+{{< /latex >}}| __Case__: This rule is not part of Hindley-Milner, and is specific to our language. If the expression being case-analyzed is of type \\(\\tau\\) and each branch \\((p\_i, e\_i)\\) is of the same type \\(\\tau\_c\\) when the pattern \\(p\_i\\) works with type \\(\\tau\\) producing extra bindings \\(b\_i\\), the whole case expression is of type \\(\\tau\_c\\).
+{{< latex >}}
+\frac{\Gamma \vdash e : \sigma \quad \sigma' \sqsubseteq \sigma}
+    {\Gamma \vdash e : \sigma'}
+{{< /latex >}}| __Inst (New)__: If type \\(\\sigma'\\) is an instantiation of type \\(\\sigma\\) then an expression of type \\(\\sigma\\) is also an expression of type \\(\\sigma'\\).
+{{< latex >}}
+\frac
+    {\Gamma \vdash e : \sigma \quad \alpha \not \in \text{free}(\Gamma)}
+    {\Gamma \vdash e : \forall \alpha . \sigma}
+{{< /latex >}}| __Gen (New)__: If an expression has a type with free variables, this rule allows us generalize it to allow all possible types to be used for these free variables.

themes/vanilla/assets/scss/style.scss

@@ -149,3 +149,13 @@ a {
 img {
   max-width: 100%
 }
+
+table {
+    @include bordered-block;
+    margin: auto;
+    padding: 0.5rem;
+}
+
+td {
+    padding: 0.5rem;
+}

themes/vanilla/layouts/shortcodes/latex.html

@@ -0,0 +1,3 @@
+$$
+{{ .Inner }}
+$$