Compare commits
8 Commits
ffca10f447
...
master
| Author | SHA1 | Date | |
|---|---|---|---|
| 98e2e7da6c | |||
| f57e3d370b | |||
| 8795003ce7 | |||
| 487681df16 | |||
| 51964e1d9f | |||
| 3695dd561f | |||
| 38ae57792a | |||
| 0b9612f138 |
5
.gitignore
vendored
5
.gitignore
vendored
@@ -1 +1,6 @@
|
||||
**/build/*
|
||||
.DS_Store
|
||||
/.hugo_build.lock
|
||||
/.hugo_cache/
|
||||
/public/
|
||||
/resources/
|
||||
|
||||
@@ -1,174 +0,0 @@
|
||||
@import "variables.scss";
|
||||
@import "mixins.scss";
|
||||
|
||||
.bergamot-exercise {
|
||||
counter-increment: bergamot-exercise;
|
||||
|
||||
.bergamot-root {
|
||||
border: none;
|
||||
padding: 0;
|
||||
margin-top: 1em;
|
||||
}
|
||||
|
||||
|
||||
.bergamot-exercise-label {
|
||||
.bergamot-exercise-number::after {
|
||||
content: "Exercise " counter(bergamot-exercise);
|
||||
font-weight: bold;
|
||||
text-decoration: underline;
|
||||
}
|
||||
}
|
||||
|
||||
.bergamot-button {
|
||||
@include bordered-block;
|
||||
padding: 0.25em;
|
||||
padding-left: 1em;
|
||||
padding-right: 1em;
|
||||
background-color: inherit;
|
||||
display: inline-flex;
|
||||
align-items: center;
|
||||
justify-content: center;
|
||||
transition: 0.25s;
|
||||
font-family: $font-body;
|
||||
@include var(color, text-color);
|
||||
|
||||
&.bergamot-hidden {
|
||||
display: none;
|
||||
}
|
||||
|
||||
.feather {
|
||||
margin-right: 0.5em;
|
||||
}
|
||||
}
|
||||
|
||||
.bergamot-play {
|
||||
.feather { color: $primary-color; }
|
||||
&:hover, &:focus {
|
||||
.feather { color: lighten($primary-color, 20%); }
|
||||
}
|
||||
}
|
||||
|
||||
.bergamot-reset {
|
||||
.feather { color: #0099CC; }
|
||||
&:hover, &:focus {
|
||||
.feather { color: lighten(#0099CC, 20%); }
|
||||
}
|
||||
|
||||
svg {
|
||||
fill: none;
|
||||
}
|
||||
}
|
||||
|
||||
.bergamot-close {
|
||||
.feather { color: tomato; }
|
||||
&:hover, &:focus {
|
||||
.feather { color: lighten(tomato, 20%); }
|
||||
}
|
||||
}
|
||||
|
||||
.bergamot-button-group {
|
||||
margin-top: 1em;
|
||||
}
|
||||
}
|
||||
|
||||
.bergamot-root {
|
||||
@include bordered-block;
|
||||
padding: 1em;
|
||||
|
||||
.bergamot-section-heading {
|
||||
margin-bottom: 0.5em;
|
||||
font-family: $font-body;
|
||||
font-style: normal;
|
||||
font-weight: bold;
|
||||
font-size: 1.25em;
|
||||
}
|
||||
|
||||
.bergamot-section {
|
||||
margin-bottom: 1em;
|
||||
}
|
||||
|
||||
textarea {
|
||||
display: block;
|
||||
width: 100%;
|
||||
height: 10em;
|
||||
resize: none;
|
||||
}
|
||||
|
||||
input[type="text"] {
|
||||
width: 100%;
|
||||
@include textual-input;
|
||||
}
|
||||
|
||||
.bergamot-rule-list {
|
||||
display: flex;
|
||||
flex-direction: row;
|
||||
flex-wrap: wrap;
|
||||
justify-content: center;
|
||||
}
|
||||
|
||||
.bergamot-rule-list katex-expression {
|
||||
margin-left: .5em;
|
||||
margin-right: .5em;
|
||||
flex-grow: 1;
|
||||
flex-basis: 0;
|
||||
}
|
||||
|
||||
.bergamot-rule-section {
|
||||
.bergamot-rule-section-name {
|
||||
text-align: center;
|
||||
margin: 0.25em;
|
||||
font-weight: bold;
|
||||
}
|
||||
}
|
||||
|
||||
.bergamot-proof-tree {
|
||||
overflow: auto;
|
||||
}
|
||||
|
||||
.bergamot-error {
|
||||
@include bordered-block;
|
||||
padding: 0.5rem;
|
||||
border-color: tomato;
|
||||
background-color: rgba(tomato, 0.25);
|
||||
margin-top: 1rem;
|
||||
}
|
||||
|
||||
.bergamot-selector {
|
||||
button {
|
||||
@include var(background-color, background-color);
|
||||
@include var(color, text-color);
|
||||
@include bordered-block;
|
||||
padding: 0.5rem;
|
||||
font-family: $font-body;
|
||||
border-style: dotted;
|
||||
|
||||
&.active {
|
||||
border-color: $primary-color;
|
||||
border-style: solid;
|
||||
font-weight: bold;
|
||||
}
|
||||
|
||||
&:not(:first-child) {
|
||||
border-bottom-left-radius: 0;
|
||||
border-top-left-radius: 0;
|
||||
}
|
||||
|
||||
&:not(:last-child) {
|
||||
border-bottom-right-radius: 0;
|
||||
border-top-right-radius: 0;
|
||||
border-right-width: 0;
|
||||
}
|
||||
}
|
||||
|
||||
button.active + button {
|
||||
border-left-color: $primary-color;
|
||||
border-left-style: solid;
|
||||
}
|
||||
|
||||
margin-bottom: 1rem;
|
||||
}
|
||||
|
||||
.bergamot-no-proofs {
|
||||
text-align: center;
|
||||
}
|
||||
}
|
||||
@@ -1,47 +0,0 @@
|
||||
@import "variables.scss";
|
||||
|
||||
body {
|
||||
background-color: #1c1e26;
|
||||
--text-color: white;
|
||||
font-family: $font-code;
|
||||
}
|
||||
|
||||
h1, h2, h3, h4, h5, h6 {
|
||||
text-align: left;
|
||||
font-family: $font-code;
|
||||
}
|
||||
|
||||
h1::after {
|
||||
content: "(writing)";
|
||||
font-size: 1rem;
|
||||
margin-left: 0.5em;
|
||||
position: relative;
|
||||
bottom: -0.5em;
|
||||
color: $primary-color;
|
||||
}
|
||||
|
||||
nav .container {
|
||||
justify-content: flex-start;
|
||||
|
||||
a {
|
||||
padding-left: 0;
|
||||
margin-right: 1em;
|
||||
}
|
||||
}
|
||||
|
||||
.header-divider {
|
||||
visibility: hidden;
|
||||
}
|
||||
|
||||
hr {
|
||||
height: auto;
|
||||
border: none;
|
||||
|
||||
&::after {
|
||||
content: "* * *";
|
||||
color: $primary-color;
|
||||
font-size: 2rem;
|
||||
display: block;
|
||||
text-align: center;
|
||||
}
|
||||
}
|
||||
@@ -1,7 +1,5 @@
|
||||
baseURL = "https://danilafe.com"
|
||||
theme = "vanilla"
|
||||
pygmentsCodeFences = true
|
||||
pygmentsUseClasses = true
|
||||
summaryLength = 20
|
||||
|
||||
defaultContentLanguage = 'en'
|
||||
@@ -22,6 +20,9 @@ defaultContentLanguage = 'en'
|
||||
home = ["html","rss","toml"]
|
||||
|
||||
[markup]
|
||||
[markup.highlight]
|
||||
codeFences = true
|
||||
noClasses = false
|
||||
[markup.tableOfContents]
|
||||
endLevel = 4
|
||||
ordered = false
|
||||
|
||||
@@ -130,7 +130,7 @@ by one, leading to another `suc n` in the final type. This makes sense because i
|
||||
|
||||
Here's my definition of `Graph`s written using `Fin`:
|
||||
|
||||
{{< codelines "Agda" "agda-spa/Language/Graphs.agda" 24 39 >}}
|
||||
{{< codelines "Agda" "agda-spa/Language/Graphs.agda" 23 38 >}}
|
||||
|
||||
I explicitly used a `size` field, which determines how many nodes are in the
|
||||
graph, and serves as the upper bound for the edge indices. From there, an
|
||||
@@ -176,7 +176,7 @@ we will connect each of the outputs of one to each of the inputs of the other.
|
||||
|
||||
This is defined by the operation `g₁ ↦ g₂`, which sequences two graphs `g₁` and `g₂`:
|
||||
|
||||
{{< codelines "Agda" "agda-spa/Language/Graphs.agda" 72 83 >}}
|
||||
{{< codelines "Agda" "agda-spa/Language/Graphs.agda" 71 82 >}}
|
||||
|
||||
The definition starts out pretty innocuous, but gets a bit complicated by the
|
||||
end. The sum of the numbers of nodes in the two operands becomes the new graph
|
||||
@@ -238,7 +238,7 @@ operation when combining the sub-CFGs of the "if" and "else" branches of an
|
||||
`if`/`else`, which both follow the condition, and both proceed to the code after
|
||||
the conditional.
|
||||
|
||||
{{< codelines "Agda" "agda-spa/Language/Graphs.agda" 59 70 >}}
|
||||
{{< codelines "Agda" "agda-spa/Language/Graphs.agda" 58 69 >}}
|
||||
|
||||
Everything here is just concatenation; we pool together the nodes, edges,
|
||||
inputs, and outputs, and the main source of complexity is the re-indexing.
|
||||
@@ -250,12 +250,12 @@ from the graph for `while` loops I showed above; the reason for that is that
|
||||
I currently don't include the conditional expressions in my CFG. This is a
|
||||
limitation that I will address in future work.
|
||||
|
||||
{{< codelines "Agda" "agda-spa/Language/Graphs.agda" 85 95 >}}
|
||||
{{< codelines "Agda" "agda-spa/Language/Graphs.agda" 84 94 >}}
|
||||
|
||||
Given these thee operations, I construct Control Flow Graphs as follows, where
|
||||
`singleton` creates a new CFG node with the given list of simple statements:
|
||||
|
||||
{{< codelines "Agda" "agda-spa/Language/Graphs.agda" 122 126 >}}
|
||||
{{< codelines "Agda" "agda-spa/Language/Graphs.agda" 121 125 >}}
|
||||
|
||||
Throughout this, I've been liberal to include empty CFG nodes as was convenient.
|
||||
This is a departure from the formal definition I gave above, but it makes
|
||||
|
||||
@@ -1,5 +1,5 @@
|
||||
{
|
||||
"agda-spa": "https://dev.danilafe.com/DanilaFe/agda-spa/src/commit/828b652d3b9266e27ef7cf5a8a7fb82e3fd3133f",
|
||||
"agda-spa": "https://dev.danilafe.com/DanilaFe/agda-spa/src/commit/913121488069a20cdfd40777a8777eb3744c415e",
|
||||
"aoc-2020": "https://dev.danilafe.com/Advent-of-Code/AdventOfCode-2020/src/commit/7a8503c3fe1aa7e624e4d8672aa9b56d24b4ba82",
|
||||
"blog-static-flake": "https://dev.danilafe.com/Nix-Configs/blog-static-flake/src/commit/67b47d9c298e7476c2ca211aac5c5fd961637b7b",
|
||||
"compiler": "https://dev.danilafe.com/DanilaFe/bloglang/src/commit/137455b0f4365ba3fd11c45ce49781cdbe829ec3",
|
||||
|
||||
4
layouts/_partials/spiderweb.html
Normal file
4
layouts/_partials/spiderweb.html
Normal file
@@ -0,0 +1,4 @@
|
||||
<svg class="spiderweb" viewBox="0 0 197.21727 106.16592">
|
||||
{{ $spiderweb := resources.Get "svg/spiderweb.svg" | resources.Fingerprint }}
|
||||
<use href="{{ $spiderweb.Permalink }}#mainlayer"></use>
|
||||
</svg>
|
||||
|
After Width: | Height: | Size: 207 B |
2
layouts/_shortcodes/donate_css.html
Normal file
2
layouts/_shortcodes/donate_css.html
Normal file
@@ -0,0 +1,2 @@
|
||||
{{ $style := resources.Get "scss/donate.scss" | css.Sass | resources.Minify | resources.Fingerprint }}
|
||||
<link rel="stylesheet" href="{{ $style.Permalink }}" integrity="{{ $style.Data.Integrity }}">
|
||||
2
layouts/_shortcodes/gmachine_css.html
Normal file
2
layouts/_shortcodes/gmachine_css.html
Normal file
@@ -0,0 +1,2 @@
|
||||
{{ $style := resources.Get "scss/gmachine.scss" | css.Sass | resources.Minify | resources.Fingerprint }}
|
||||
<link rel="stylesheet" href="{{ $style.Permalink }}" integrity="{{ $style.Data.Integrity }}">
|
||||
2
layouts/_shortcodes/stack_css.html
Normal file
2
layouts/_shortcodes/stack_css.html
Normal file
@@ -0,0 +1,2 @@
|
||||
{{ $style := resources.Get "scss/stack.scss" | css.Sass | resources.Minify | resources.Fingerprint }}
|
||||
<link rel="stylesheet" href="{{ $style.Permalink }}" integrity="{{ $style.Data.Integrity }}">
|
||||
@@ -1,3 +0,0 @@
|
||||
<svg class="spiderweb" viewBox="0 0 197.21727 106.16592">
|
||||
<use href="{{ (resources.Get "svg/spiderweb.svg").Permalink }}#mainlayer"></use>
|
||||
</svg>
|
||||
|
Before Width: | Height: | Size: 150 B |
@@ -1,2 +0,0 @@
|
||||
{{ $style := resources.Get "scss/donate.scss" | css.Sass | resources.Minify }}
|
||||
<link rel="stylesheet" href="{{ $style.Permalink }}">
|
||||
@@ -1,2 +0,0 @@
|
||||
{{ $style := resources.Get "scss/gmachine.scss" | css.Sass | resources.Minify }}
|
||||
<link rel="stylesheet" href="{{ $style.Permalink }}">
|
||||
@@ -1,2 +0,0 @@
|
||||
{{ $style := resources.Get "scss/stack.scss" | css.Sass | resources.Minify }}
|
||||
<link rel="stylesheet" href="{{ $style.Permalink }}">
|
||||
Submodule themes/vanilla updated: 20217e0b97...b1b5408301
Reference in New Issue
Block a user