agda plugin

This commit is contained in:
Michael Zhang 2024-06-26 18:18:47 -05:00
parent b5a5f9cf0a
commit a8f1ce9acd
7 changed files with 9 additions and 155 deletions

View file

@ -1,5 +1,5 @@
import type { RemarkPlugin } from "@astrojs/markdown-remark"; 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 { fromMarkdown } from "mdast-util-from-markdown";
import { fromHtml } from "hast-util-from-html"; import { fromHtml } from "hast-util-from-html";
import { toHtml } from "hast-util-to-html"; import { toHtml } from "hast-util-to-html";
@ -12,11 +12,11 @@ import { visit } from "unist-util-visit";
const remarkAgda: RemarkPlugin = () => { const remarkAgda: RemarkPlugin = () => {
return (tree, { history }) => { return (tree, { history }) => {
// console.log("args", arguments) const path: string = history[history.length - 1]!;
const path: string = history[history.length - 1];
console.log("path", history);
if (!(path.endsWith(".lagda.md") || path.endsWith(".agda"))) return; if (!(path.endsWith(".lagda.md") || path.endsWith(".agda"))) return;
console.log("AGDA:processing path", path);
const tempDir = mkdtempSync(join(tmpdir(), "agdaRender.")); const tempDir = mkdtempSync(join(tmpdir(), "agdaRender."));
const outDir = join(tempDir, "output"); const outDir = join(tempDir, "output");
mkdirSync(outDir, { recursive: true }); 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 filename = parse(path).base.replace(/\.lagda.md/, ".md");
const htmlname = parse(path).base.replace(/\.lagda.md/, ".html"); const htmlname = parse(path).base.replace(/\.lagda.md/, ".html");
console.log();
console.log("filename", filename);
const fullOutputPath = join(outDir, filename); const fullOutputPath = join(outDir, filename);
console.log("outDir", fullOutputPath);
console.log();
const doc = readFileSync(fullOutputPath); const doc = readFileSync(fullOutputPath);
// This is the post-processed markdown with HTML code blocks replacing the Agda code blocks
const tree2 = fromMarkdown(doc); const tree2 = fromMarkdown(doc);
// console.log("tree", tree);
const collectedCodeBlocks: RootContent[] = []; const collectedCodeBlocks: RootContent[] = [];
visit(tree2, "html", (node) => { visit(tree2, "html", (node) => {
// console.log("node", node);
// collectedCodeBlocks.push
const html = fromHtml(node.value, { fragment: true }); const html = fromHtml(node.value, { fragment: true });
const firstChild: RootContent = html.children[0]!; const firstChild: RootContent = html.children[0]!;
console.log("child", firstChild);
visit(html, "element", (node) => { visit(html, "element", (node) => {
if (node.tagName !== "a") return; if (node.tagName !== "a") return;
if (node.properties.href && node.properties.href.includes(htmlname)) { if (node.properties.href && node.properties.href.includes(htmlname)) {
console.log("a", node.properties);
node.properties.href = node.properties.href.replace(htmlname, ""); node.properties.href = node.properties.href.replace(htmlname, "");
} }
}); });
@ -68,24 +59,19 @@ const remarkAgda: RemarkPlugin = () => {
if (!firstChild?.properties?.className?.includes("Agda")) return; if (!firstChild?.properties?.className?.includes("Agda")) return;
const stringContents = toHtml(firstChild); const stringContents = toHtml(firstChild);
// console.log("result", stringContents);
collectedCodeBlocks.push({ collectedCodeBlocks.push({
contents: stringContents, contents: stringContents,
}); });
}); });
console.log("collected len", collectedCodeBlocks.length);
let idx = 0; let idx = 0;
visit(tree, "code", (node) => { 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.type = "html";
node.value = collectedCodeBlocks[idx].contents; node.value = collectedCodeBlocks[idx].contents;
idx += 1; idx += 1;
}); });
console.log("len", idx);
}; };
}; };

View file

@ -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: map `true1` and `true2` to divergent types. Let's see what happens:
``` ```
{-# NON_COVERING #-}
notbool-map : NotBool → Type notbool-map : NotBool → Type
notbool-map true1 = notbool-map true1 =
notbool-map true2 = ⊥ notbool-map true2 = ⊥

View file

@ -9,7 +9,7 @@ tags: ["type-theory", "programming-languages"]
<summary>Imports</summary> <summary>Imports</summary>
``` ```
open import Relation.Binary.PropositionalEquality open import Relation.Binary.PropositionalEquality hiding (J)
open import Data.Integer open import Data.Integer
open import Data.Bool open import Data.Bool
open import Data.String open import Data.String

View file

@ -1,133 +0,0 @@
---
title: "Logical Relations"
slug: 2024-06-11-logical-relations
date: 2024-06-11
tags: ["programming-languages", "formal-verification"]
draft: true
---
<details>
<summary>Imports</summary>
```
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
```
</details>
## 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)
```