diff --git a/plugin/remark-agda.ts b/plugin/remark-agda.ts
index 65a11c3..e014761 100644
--- a/plugin/remark-agda.ts
+++ b/plugin/remark-agda.ts
@@ -1,5 +1,5 @@
import type { RemarkPlugin } from "@astrojs/markdown-remark";
-import type { Node, Parent, Root, RootContent } from "hast";
+import type { RootContent } from "hast";
import { fromMarkdown } from "mdast-util-from-markdown";
import { fromHtml } from "hast-util-from-html";
import { toHtml } from "hast-util-to-html";
@@ -12,11 +12,11 @@ import { visit } from "unist-util-visit";
const remarkAgda: RemarkPlugin = () => {
return (tree, { history }) => {
- // console.log("args", arguments)
- const path: string = history[history.length - 1];
- console.log("path", history);
+ const path: string = history[history.length - 1]!;
if (!(path.endsWith(".lagda.md") || path.endsWith(".agda"))) return;
+ console.log("AGDA:processing path", path);
+
const tempDir = mkdtempSync(join(tmpdir(), "agdaRender."));
const outDir = join(tempDir, "output");
mkdirSync(outDir, { recursive: true });
@@ -33,34 +33,25 @@ const remarkAgda: RemarkPlugin = () => {
{},
);
- console.log("output", childOutput.output.toString());
const filename = parse(path).base.replace(/\.lagda.md/, ".md");
const htmlname = parse(path).base.replace(/\.lagda.md/, ".html");
- console.log();
- console.log("filename", filename);
-
const fullOutputPath = join(outDir, filename);
- console.log("outDir", fullOutputPath);
- console.log();
const doc = readFileSync(fullOutputPath);
+
+ // This is the post-processed markdown with HTML code blocks replacing the Agda code blocks
const tree2 = fromMarkdown(doc);
- // console.log("tree", tree);
const collectedCodeBlocks: RootContent[] = [];
visit(tree2, "html", (node) => {
- // console.log("node", node);
- // collectedCodeBlocks.push
const html = fromHtml(node.value, { fragment: true });
const firstChild: RootContent = html.children[0]!;
- console.log("child", firstChild);
visit(html, "element", (node) => {
if (node.tagName !== "a") return;
if (node.properties.href && node.properties.href.includes(htmlname)) {
- console.log("a", node.properties);
node.properties.href = node.properties.href.replace(htmlname, "");
}
});
@@ -68,24 +59,19 @@ const remarkAgda: RemarkPlugin = () => {
if (!firstChild?.properties?.className?.includes("Agda")) return;
const stringContents = toHtml(firstChild);
- // console.log("result", stringContents);
collectedCodeBlocks.push({
contents: stringContents,
});
});
- console.log("collected len", collectedCodeBlocks.length);
-
let idx = 0;
visit(tree, "code", (node) => {
- if (node.lang !== "agda") return;
+ if (!(node.lang === null || node.lang === "agda")) return;
- // console.log("node", node);
node.type = "html";
node.value = collectedCodeBlocks[idx].contents;
idx += 1;
});
- console.log("len", idx);
};
};
diff --git a/src/content/posts/2022-09-20-higher-inductive-types.lagda.md b/src/content/posts/2022-09-20-higher-inductive-types.md
similarity index 100%
rename from src/content/posts/2022-09-20-higher-inductive-types.lagda.md
rename to src/content/posts/2022-09-20-higher-inductive-types.md
diff --git a/src/content/posts/2023-04-21-proving-true-from-false.lagda.md b/src/content/posts/2023-04-21-proving-true-from-false.lagda.md
index b424dd7..3171a25 100644
--- a/src/content/posts/2023-04-21-proving-true-from-false.lagda.md
+++ b/src/content/posts/2023-04-21-proving-true-from-false.lagda.md
@@ -137,6 +137,7 @@ definition of the `NotBool` type. Since this is an intrinsic equality, we can't
map `true1` and `true2` to divergent types. Let's see what happens:
```
+{-# NON_COVERING #-}
notbool-map : NotBool → Type
notbool-map true1 = ⊤
notbool-map true2 = ⊥
diff --git a/src/content/posts/2023-05-06-equivalences.lagda.md b/src/content/posts/2023-05-06-equivalences.md
similarity index 100%
rename from src/content/posts/2023-05-06-equivalences.lagda.md
rename to src/content/posts/2023-05-06-equivalences.md
diff --git a/src/content/posts/2023-10-10-dtt-project.lagda.md b/src/content/posts/2023-10-10-dtt-project.md
similarity index 100%
rename from src/content/posts/2023-10-10-dtt-project.lagda.md
rename to src/content/posts/2023-10-10-dtt-project.md
diff --git a/src/content/posts/2023-10-23-path-induction-gadt-perspective.lagda.md b/src/content/posts/2023-10-23-path-induction-gadt-perspective.lagda.md
index 04387f8..7fabc84 100644
--- a/src/content/posts/2023-10-23-path-induction-gadt-perspective.lagda.md
+++ b/src/content/posts/2023-10-23-path-induction-gadt-perspective.lagda.md
@@ -9,7 +9,7 @@ tags: ["type-theory", "programming-languages"]
Imports
```
-open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.PropositionalEquality hiding (J)
open import Data.Integer
open import Data.Bool
open import Data.String
diff --git a/src/content/posts/2024-06-11-logical-relations.lagda.md b/src/content/posts/2024-06-11-logical-relations.lagda.md
deleted file mode 100644
index 8d310a4..0000000
--- a/src/content/posts/2024-06-11-logical-relations.lagda.md
+++ /dev/null
@@ -1,133 +0,0 @@
----
-title: "Logical Relations"
-slug: 2024-06-11-logical-relations
-date: 2024-06-11
-tags: ["programming-languages", "formal-verification"]
-draft: true
----
-
-
-Imports
-
-```
-open import Agda.Builtin.Sigma
-open import Data.Bool
-open import Data.Empty
-open import Data.Fin
-open import Data.Maybe
-open import Data.Nat
-open import Data.Product
-open import Data.Sum
-open import Relation.Nullary
-
-id : {A : Set} → A → A
-id {A} x = x
-```
-
-
-
-## Syntax
-
-```
-data type : Set where
- bool : type
- _-→_ : type → type → type
-
-data term : Set where
- `_ : ℕ → term
- `true : term
- `false : term
- `if_then_else_ : term → term → term → term
- `λ[_]_ : (τ : type) → (e : term) → term
- _∙_ : term → term → term
-```
-
-## Substitution
-
-```
-data ctx : Set where
- nil : ctx
- cons : ctx → type → ctx
-
-lookup : ctx → ℕ → Maybe type
-lookup nil _ = nothing
-lookup (cons ctx₁ x) zero = just x
-lookup (cons ctx₁ x) (suc n) = lookup ctx₁ n
-
-data sub : Set where
- nil : sub
- cons : sub → term → sub
-
-subst : term → term → term
-subst (` zero) v = v
-subst (` suc x) v = ` x
-subst `true v = `true
-subst `false v = `false
-subst (`if x then x₁ else x₂) v = `if (subst x v) then (subst x₁ v) else (subst x₂ v)
-subst (`λ[ τ ] x) v = `λ[ τ ] subst x v
-subst (x ∙ x₁) v = (subst x v) ∙ (subst x₁ v)
-
-data value-rel : type → term → Set where
- v-`true : value-rel bool `true
- v-`false : value-rel bool `false
- v-`λ[_]_ : ∀ {τ e} → value-rel τ (`λ[ τ ] e)
-
-data good-subst : ctx → sub → Set where
- nil : good-subst nil nil
- cons : ∀ {ctx τ γ v}
- → good-subst ctx γ
- → value-rel τ v
- → good-subst (cons ctx τ) γ
-```
-
-## Semantics
-
-```
-data step : term → term → Set where
- step-if-1 : ∀ {e₁ e₂} → step (`if `true then e₁ else e₂) e₁
- step-if-2 : ∀ {e₁ e₂} → step (`if `false then e₁ else e₂) e₂
- step-`λ : ∀ {τ e v} → step ((`λ[ τ ] e) ∙ v) (subst e v)
-
-data steps : ℕ → term → term → Set where
- zero : ∀ {e} → steps zero e e
- suc : ∀ {e e' e''} → (n : ℕ) → step e e' → steps n e' e'' → steps (suc n) e e''
-
-data _⊢_∶_ : ctx → term → type → Set where
- type-`true : ∀ {ctx} → ctx ⊢ `true ∶ bool
- type-`false : ∀ {ctx} → ctx ⊢ `false ∶ bool
- type-`ifthenelse : ∀ {ctx e e₁ e₂ τ}
- → ctx ⊢ e ∶ bool
- → ctx ⊢ e₁ ∶ τ
- → ctx ⊢ e₂ ∶ τ
- → ctx ⊢ (`if e then e₁ else e₂) ∶ τ
- type-`x : ∀ {ctx x}
- → (p : Is-just (lookup ctx x))
- → ctx ⊢ (` x) ∶ (to-witness p)
- type-`λ : ∀ {ctx τ τ₂ e}
- → (cons ctx τ) ⊢ e ∶ τ₂
- → ctx ⊢ (`λ[ τ ] e) ∶ (τ -→ τ₂)
- type-∙ : ∀ {ctx τ₁ τ₂ e₁ e₂}
- → ctx ⊢ e₁ ∶ (τ₁ -→ τ₂)
- → ctx ⊢ e₂ ∶ τ₂
- → ctx ⊢ (e₁ ∙ e₂) ∶ τ₂
-
-irreducible : term → Set
-irreducible e = ¬ (∃ λ e' → step e e')
-
-data term-relation : type → term → Set where
- e-term : ∀ {τ e}
- → (∀ {n} → (e' : term) → steps n e e' → irreducible e' → value-rel τ e')
- → term-relation τ e
-
-type-sound : ∀ {Γ e τ} → Γ ⊢ e ∶ τ → Set
-type-sound {Γ} {e} {τ} s = ∀ {n} → (e' : term) → steps n e e' → value-rel τ e' ⊎ ∃ λ e'' → step e' e''
-
-_⊨_∶_ : (Γ : ctx) → (e : term) → (τ : type) → Set
-_⊨_∶_ Γ e τ = (γ : sub) → (good-subst Γ γ) → term-relation τ e
-
-fundamental : ∀ {Γ e τ} → (well-typed : Γ ⊢ e ∶ τ) → type-sound well-typed → Γ ⊨ e ∶ τ
-fundamental {Γ} {e} {τ} well-typed type-sound γ good-sub = e-term f
- where
- f : {n : ℕ} (e' : term) → steps n e e' → irreducible e' → value-rel τ e'
- f e' steps irred = [ id , (λ exists → ⊥-elim (irred exists)) ] (type-sound e' steps)
-```