improvements
This commit is contained in:
flupe
parent
35fb560b60
commit
24927f7028
|
|
@ -77,6 +77,15 @@ hr {
|
|||
margin: 2.5em 0;
|
||||
}
|
||||
|
||||
main > ul { list-style: none }
|
||||
main > ul li > span {
|
||||
font: 13px monospace;
|
||||
margin-right: 1em;
|
||||
padding: .1em .5em;
|
||||
border-radius: 3px;
|
||||
background: #eaeaef;
|
||||
}
|
||||
|
||||
details summary {
|
||||
cursor: pointer;
|
||||
padding: .5em 1em;
|
||||
|
|
@ -248,6 +257,23 @@ figure {
|
|||
text-align: center;
|
||||
}
|
||||
|
||||
ul.pages {
|
||||
padding: 0;
|
||||
margin: 2em 0 2.5em;
|
||||
list-style:none;
|
||||
border-radius: 3px;
|
||||
overflow: hidden;
|
||||
}
|
||||
ul.pages li a {
|
||||
display: block;
|
||||
line-height: 2.4em;
|
||||
padding: 0 1em;
|
||||
background: #eceff4;
|
||||
}
|
||||
ul.pages li a:hover {
|
||||
background: #f2f4f7;
|
||||
}
|
||||
|
||||
figure img {
|
||||
max-width: 100%;
|
||||
vertical-align: top;
|
||||
|
|
|
|||
|
|
@ -1,591 +0,0 @@
|
|||
---
|
||||
title: Parametricity for described datatypes
|
||||
draft: yes
|
||||
---
|
||||
|
||||
.. highlight:: agda
|
||||
.. default-role:: math
|
||||
|
||||
This entry is just me figuring stuff out by writing it down.
|
||||
The goal is to **derive automatically the logical relation generated by
|
||||
a datatype** in Agda, without metaprogramming. Or, to be correct,
|
||||
without *unsafe* metaprogramming --- no reflection allowed.
|
||||
|
||||
*The title means nothing and this is WIP.*
|
||||
|
||||
Only one thing to keep in mind: we are using the dirtiest of tricks, :code:`--type-in-type`.
|
||||
For the time being, this will do just fine.
|
||||
|
||||
.. raw:: html
|
||||
|
||||
<details>
|
||||
<summary>Prelude</summary>
|
||||
|
||||
::
|
||||
|
||||
{-# OPTIONS --type-in-type #-}
|
||||
|
||||
open import Agda.Primitive
|
||||
open import Agda.Builtin.Unit
|
||||
open import Agda.Builtin.Sigma
|
||||
open import Agda.Builtin.Equality
|
||||
open import Agda.Builtin.Nat
|
||||
open import Agda.Builtin.List
|
||||
|
||||
variable A B : Set
|
||||
|
||||
infixr -1 _$_
|
||||
infixl 2 _∘_
|
||||
|
||||
id : {A : Set} → A → A
|
||||
id x = x
|
||||
|
||||
const : {A : Set} → A → {B : Set} → B → A
|
||||
const x _ = x
|
||||
|
||||
_$_ : {A : Set} {P : A → Set} (f : ∀ x → P x) (x : A) → P x
|
||||
f $ x = f x
|
||||
|
||||
_×_ : (A B : Set) → Set
|
||||
A × B = Σ A (const B)
|
||||
|
||||
case_of_ : {A : Set} {P : A → Set} (x : A) → ((x : A) → P x) → P x
|
||||
case x of f = f x
|
||||
|
||||
_∘_ : {A : Set} {P : A → Set} {Q : {x : A} → P x → Set}
|
||||
(g : {x : A} → (y : P x) → Q y) (f : (x : A) → P x)
|
||||
→ (x : A) → Q (f x)
|
||||
_∘_ g f x = g (f x)
|
||||
|
||||
data Fin : Nat → Set where
|
||||
zero : ∀ {n} → Fin (suc n)
|
||||
suc : ∀ {n} → Fin n → Fin (suc n)
|
||||
|
||||
data Vec (A : Set) : Nat → Set where
|
||||
[] : Vec A 0
|
||||
_∷_ : ∀ {n} → A → Vec A n → Vec A (suc n)
|
||||
|
||||
lookup : {A : Set} {n : Nat}
|
||||
→ Vec A n → Fin n → A
|
||||
lookup (x ∷ _) zero = x
|
||||
lookup (_ ∷ xs) (suc n) = lookup xs n
|
||||
|
||||
map : (A → B) → {n : Nat} → Vec A n → Vec B n
|
||||
map f [] = []
|
||||
map f (x ∷ xs) = f x ∷ map f xs
|
||||
|
||||
Rel : Set → Set → Set
|
||||
Rel A B = A → B → Set
|
||||
|
||||
.. raw:: html
|
||||
|
||||
</details>
|
||||
|
||||
A universe of descriptions
|
||||
~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
|
||||
The first step is to equip ourselves with a universe of descriptions to encode
|
||||
inductive indexed datatypes. See the work from Pierre-Evariste Dagand[#dagand]_
|
||||
to learn about descriptions. The one chosen here is an extension of Yorick
|
||||
Sijsling's [#yorick]_, with some additions:
|
||||
|
||||
.. [#dagand] In particular, his PhD thesis:
|
||||
`Reusability and Dependent Types
|
||||
<https://gallium.inria.fr/~pdagand/stuffs/thesis-2011-phd/thesis.pdf>`_
|
||||
.. [#yorick] https://github.com/yoricksijsling/ornaments-thesis
|
||||
|
||||
- indices now depend on the parameters;
|
||||
- recursive occurences can have different parameters.
|
||||
**Actually I removed this for the time being, since it's not really important for what we are trying
|
||||
to achieve. Still, can be done.**
|
||||
|
||||
Encoding telescopes 🔭
|
||||
---------------------
|
||||
|
||||
So we begin by defining an encoding of telescopes to encode the parameters and
|
||||
indices of datatypes. I just found out it is very similar to what is
|
||||
introduced in [Akaposi2015]_. What we are apparently doing is adding telescopes
|
||||
and telescope substitutions in our theory, whereas they leave them outside of types.
|
||||
|
||||
.. [Akaposi2015] | **Towards cubical type theory**
|
||||
| Thorsten Altenkirch, Ambrus Kaposi
|
||||
| https://akaposi.github.io/nominal.pdf
|
||||
|
||||
In summary, we define **the type of telescopes** parametrized by some set `A`.
|
||||
And given a telescope, and an element of `A`, we define **the type of telescope substitutions**:
|
||||
|
||||
.. math::
|
||||
\gdef\set{\textsf{Set}}
|
||||
\gdef\tele#1{\textsf{Tele}\ #1}
|
||||
\gdef\rel#1#2{\textsf{Rel}\ #1\ #2}
|
||||
|
||||
A : \set\ &⊢\ \tele A : \set \\
|
||||
A : \set,\ Ω : \tele A,\ x : A\ &⊢ ⟦ Ω ⟧\ x \ : \set
|
||||
|
||||
For our purposes, a telescope substitution is a huge Σ-type containing an element for
|
||||
every type in the telescope. We can introduce empty telescopes or extend them by the right.
|
||||
|
||||
.. math::
|
||||
\frac{}{A : \set \ ⊢\ ε : \tele A} \quad
|
||||
\frac
|
||||
{A : \set,\ Ω : \tele A,\ ⊢\ F : Σ\ A\ ⟦ Ω ⟧ → \set}
|
||||
{A : \set,\ Ω : \tele A\ ⊢\ Ω\ ▷\ F : \tele A}
|
||||
|
||||
::
|
||||
|
||||
infixl 1 _▷_ _▷₀_
|
||||
|
||||
data Tele (A : Set) : Set
|
||||
⟦_⟧ : {A : Set} → Tele A → A → Set
|
||||
|
||||
data Tele A where
|
||||
ε : Tele A
|
||||
_▷_ : (T : Tele A) → (Σ A ⟦ T ⟧ → Set) → Tele A
|
||||
|
||||
⟦ ε ⟧ x = ⊤
|
||||
⟦ T ▷ F ⟧ x = Σ (⟦ T ⟧ x) (F ∘ (x ,_))
|
||||
|
||||
_▷₀_ : {A : Set} (T : Tele A) (B : Set) → Tele A
|
||||
T ▷₀ B = T ▷ const B
|
||||
|
||||
Because telescopes are parametrized by some :code:`Set`,
|
||||
we can define a telescope that depend on the telescope substitution of another telescope.
|
||||
**That's how we encode parameters-dependent indices**. Describing the parameters and indices
|
||||
of a datatype boils down to exhibiting some :code:`P` and :code:`I` such that
|
||||
:code:`P : Tele ⊤` and :code:`I : Tele (⟦ T ⟧ tt)`.
|
||||
|
||||
We too can **extend telescopes with telescopes**.
|
||||
For our purposes, it only makes sense to extend non-parametrized telescopes:
|
||||
|
||||
.. math::
|
||||
Ω : \tele ⊤,\ Ω' : \tele (⟦ Ω ⟧\ tt)\
|
||||
&⊢ \textsf{extend}\ Ω' : \tele ⊤ \\
|
||||
Ω : \tele ⊤,\ Ω' : \tele (⟦ Ω ⟧\ tt)\
|
||||
&⊢ \textsf{pr}\ : ⟦ \textsf{extend}\ Ω' ⟧\ tt → Σ\ (⟦ Ω ⟧\ tt)\ ⟦ Ω' ⟧
|
||||
|
||||
::
|
||||
|
||||
ExTele : Tele ⊤ → Set
|
||||
ExTele T = Tele (⟦ T ⟧ tt)
|
||||
|
||||
Ctx : {T : Tele ⊤} → ExTele T → Set
|
||||
Ctx Γ = Σ _ ⟦ Γ ⟧
|
||||
|
||||
extend : {T : Tele ⊤} → ExTele T → Tele ⊤
|
||||
pr : {T : Tele ⊤} {Γ : ExTele T}
|
||||
→ ⟦ extend Γ ⟧ tt → Ctx Γ
|
||||
|
||||
extend {T} ε = T
|
||||
extend (G ▷ F) = extend G ▷ F ∘ pr ∘ snd
|
||||
|
||||
pr {Γ = ε} γ = γ , tt
|
||||
pr {Γ = Γ ▷ F} (γ′ , x) =
|
||||
let (t , γ) = pr γ′ in t , γ , x
|
||||
|
||||
Constructors
|
||||
------------
|
||||
|
||||
Like Yorick we describe constructors first and datatypes second by giving a vector
|
||||
of constructor descriptions. This has the benefit of following more closely the structure
|
||||
of Agda datatypes::
|
||||
|
||||
data ConDesc {P : Tele ⊤} (Γ I : ExTele P) : Set
|
||||
|
||||
Both the constructor's current context :code:`Γ` and its indices :code:`I` are extensions
|
||||
of the datatype parameters. The rest is pretty standard:
|
||||
|
||||
- :code:`κ` **marks the end of a constructor**. We simply compute indices from the current context.
|
||||
- :code:`ι` **marks the position of a recursive occurence**. Here we provide indices
|
||||
computed from the context. I am saddened by the fact that this
|
||||
recursive occurence is not added to the context of the rest of the constructor.
|
||||
This can probably be done but would require too much effort for what it's worth.
|
||||
Who does that anyway?
|
||||
- :code:`σ` **marks the introduction of a variable**. Its type is computed from the local context,
|
||||
and the variable is added to the context for the rest of the constructor.
|
||||
|
||||
::
|
||||
|
||||
data ConDesc {P} Γ I where
|
||||
κ : (f : (γ : Ctx Γ) → ⟦ I ⟧ (γ .fst)) → ConDesc Γ I
|
||||
ι : (f : (γ : Ctx Γ) → ⟦ I ⟧ (γ .fst)) → ConDesc Γ I → ConDesc Γ I
|
||||
σ : (S : Ctx Γ → Set ) → ConDesc (Γ ▷ S) I → ConDesc Γ I
|
||||
|
||||
..
|
||||
|
||||
::
|
||||
|
||||
⟦_⟧ᶜ : {P : Tele ⊤} {Γ I : ExTele P}
|
||||
(C : ConDesc Γ I)
|
||||
→ (Ctx I → Set)
|
||||
→ (Σ (⟦ P ⟧ tt) (λ p → ⟦ Γ ⟧ p × ⟦ I ⟧ p) → Set)
|
||||
|
||||
⟦ κ f ⟧ᶜ X (p , γ , i) = f (p , γ) ≡ i
|
||||
⟦ ι f C ⟧ᶜ X g@(p , γ , _) = X (p , f (p , γ)) × ⟦ C ⟧ᶜ X g
|
||||
⟦ σ S C ⟧ᶜ X (p , γ , i) = Σ (S (p , γ)) λ s → ⟦ C ⟧ᶜ X (p , (γ , s) , i)
|
||||
|
||||
Datatypes
|
||||
---------
|
||||
|
||||
Moving on, we encode datatypes as a vector of constructor descriptions that
|
||||
share the same parameters and indices telescopes. Then we tie the knot::
|
||||
|
||||
Desc : (P : Tele ⊤) (I : ExTele P) → Nat → Set
|
||||
Desc P I n = Vec (ConDesc ε I) n
|
||||
|
||||
⟦_⟧ᵈ : {P : Tele ⊤} {I : ExTele P} {n : Nat}
|
||||
(D : Desc P I n)
|
||||
→ (Ctx I → Set)
|
||||
→ (Ctx I → Set)
|
||||
|
||||
⟦_⟧ᵈ {n = n} D X (p , i) = Σ (Fin n) λ k → ⟦ lookup D k ⟧ᶜ X (p , tt , i)
|
||||
|
||||
data μ {n} {P : Tele ⊤} {I : ExTele P}
|
||||
(D : Desc P I n) (pi : Ctx I) : Set where
|
||||
⟨_⟩ : ⟦ D ⟧ᵈ (μ D) pi → μ D pi
|
||||
|
||||
|
||||
We can also define some helper :code:`constr` to easily retrieve the `k` th constructor from a description::
|
||||
|
||||
module _ {P : Tele ⊤} {I : Tele (⟦ P ⟧ tt)} {n : Nat} (D : Desc P I n) where
|
||||
|
||||
Constr′ : {Γ : Tele (⟦ P ⟧ tt)}
|
||||
→ ConDesc Γ I
|
||||
→ Ctx Γ
|
||||
→ Set
|
||||
Constr′ (κ f ) pg = μ D (fst pg , f pg)
|
||||
Constr′ (ι f C) pg = μ D (fst pg , f pg) → Constr′ C pg
|
||||
Constr′ (σ S C) (p , γ) = (s : S (p , γ)) → Constr′ C (p , γ , s)
|
||||
|
||||
module _ {C′ : ConDesc ε I} (mk : {(p , i) : Ctx I} → ⟦ C′ ⟧ᶜ (μ D) (p , tt , i) → μ D (p , i)) where
|
||||
|
||||
constr′ : {Γ : Tele (⟦ P ⟧ tt)}
|
||||
(C : ConDesc Γ I)
|
||||
((p , γ) : Ctx Γ)
|
||||
→ ({i : ⟦ I ⟧ p} → ⟦ C ⟧ᶜ (μ D) (p , γ , i) → ⟦ C′ ⟧ᶜ (μ D) (p , tt , i))
|
||||
→ Constr′ C (p , γ)
|
||||
constr′ (κ f ) pg tie = mk (tie refl)
|
||||
constr′ (ι f C) pg tie x = constr′ C pg (tie ∘ (x ,_))
|
||||
constr′ (σ S C) (p , γ) tie s = constr′ C (p , γ , s) (tie ∘ (s ,_))
|
||||
|
||||
-- | type of the kth constructor
|
||||
Constr : (k : Fin n) (p : ⟦ P ⟧ tt) → Set
|
||||
Constr k p = Constr′ (lookup D k) (p , tt)
|
||||
|
||||
-- | kth constructor
|
||||
constr : (k : Fin n) (p : ⟦ P ⟧ tt) → Constr k p
|
||||
constr k p = constr′ (λ x → ⟨ k , x ⟩) (lookup D k) (p , tt) id
|
||||
|
||||
Another useful operation is to retrieve a telescope for every constructor of datatype.
|
||||
|
||||
::
|
||||
|
||||
module _ {P : Tele ⊤} {I : ExTele P} (X : Ctx I → Set) where
|
||||
contotele′ : {Γ : ExTele P}
|
||||
→ ConDesc Γ I
|
||||
→ (T : ExTele P)
|
||||
→ (((p , γ) : Ctx T) → ⟦ Γ ⟧ p)
|
||||
→ ExTele P
|
||||
contotele′ (κ _) T mk = T
|
||||
contotele′ (ι f C) T mk =
|
||||
contotele′ C (T ▷ λ (p , γ) → X (p , f (p , mk (p , γ))))
|
||||
λ (p , γ , x) → mk (p , γ)
|
||||
contotele′ (σ S C) T mk =
|
||||
contotele′ C (T ▷ λ (p , γ) → S (p , (mk (p , γ))))
|
||||
λ (p , γ , s) → (mk (p , γ)) , s
|
||||
|
||||
|
||||
contotele : {P : Tele ⊤} {I : ExTele P} {n : Nat}
|
||||
→ Desc P I n
|
||||
→ Fin n
|
||||
→ ExTele P
|
||||
contotele D k = contotele′ (μ D) (lookup D k) ε (const tt)
|
||||
|
||||
Examples
|
||||
--------
|
||||
|
||||
Some examples to reassure ourselves as to whether it works as intended::
|
||||
|
||||
module Examples where
|
||||
|
||||
natD : Desc ε ε 2
|
||||
natD = κ (const tt)
|
||||
∷ ι (const tt) (κ (const tt))
|
||||
∷ []
|
||||
|
||||
nat : Set
|
||||
nat = μ natD (tt , tt)
|
||||
|
||||
ze : Constr natD zero tt
|
||||
ze = constr natD zero tt
|
||||
|
||||
su : Constr natD (suc zero) tt
|
||||
su = constr natD (suc zero) tt
|
||||
|
||||
vecD : Desc (ε ▷₀ Set) (ε ▷₀ nat) 2
|
||||
vecD = κ (const (tt , ze))
|
||||
∷ σ (const nat)
|
||||
(σ (λ (p , _) → p .snd)
|
||||
(ι (λ (p , ((tt , n) , x )) → tt , n)
|
||||
(κ (λ (_ , ((tt , n) , _)) → tt , (su n)))))
|
||||
∷ []
|
||||
|
||||
vec : (A : Set) → nat → Set
|
||||
vec A n = μ vecD ((tt , A) , tt , n)
|
||||
|
||||
nil : {A : Set} → Constr vecD zero (tt , A)
|
||||
nil {A} = constr vecD zero (tt , A)
|
||||
|
||||
cons : {A : Set} → Constr vecD (suc zero) (tt , A)
|
||||
cons {A} = constr vecD (suc zero) (tt , A)
|
||||
|
||||
xs : vec nat (su (su ze))
|
||||
xs = cons _ (su ze) (cons _ (su (su ze)) nil)
|
||||
|
||||
So far so good. Let's move to the fun part, we're in for the big bucks.
|
||||
|
||||
|
||||
From descriptions to descriptions
|
||||
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
|
||||
To keep our goal in sight, here is what should happen for lists::
|
||||
|
||||
module Translation where
|
||||
|
||||
module Goal where
|
||||
|
||||
listD : Desc (ε ▷ const Set) ε 2
|
||||
listD = κ (const tt)
|
||||
∷ σ (λ ((tt , A) , γ) → A)
|
||||
(ι (λ (p , γ) → tt)
|
||||
(κ (const tt)))
|
||||
∷ []
|
||||
|
||||
list : Set → Set
|
||||
list A = μ listD ((tt , A) , tt)
|
||||
|
||||
nil : {A : Set} → list A
|
||||
nil {A} = ⟨ zero , refl ⟩
|
||||
|
||||
cons : {A : Set} → A → list A → list A
|
||||
cons x xs = ⟨ suc zero , x , xs , refl ⟩
|
||||
|
||||
-- the following is the description we want to derive
|
||||
-- listᵣD : Desc (ε ▷₀ Set ▷₀ Set ▷ λ (tt , (tt , A) , B) → Rel A B)
|
||||
-- (ε ▷ (λ ((((_ , A) , B) , R) , tt) → list A)
|
||||
-- ▷ (λ ((((_ , A) , B) , R) , tt , _) → list B)) 2
|
||||
-- listᵣD = κ (λ ((((tt , A) , B) , R) , tt) → (tt , nil) , nil)
|
||||
-- ∷ ( σ (λ (((( A) , B) , R) , tt) → A )
|
||||
-- $ σ (λ ((((tt , A) , B) , R) , tt , _) → B )
|
||||
-- $ σ (λ ((_ , R) , (tt , x) , y) → R x y )
|
||||
-- $ σ (λ ((((tt , A) , B ) , R) , _) → list A )
|
||||
-- $ σ (λ ((((tt , A) , B ) , R) , _) → list B )
|
||||
-- $ ι (λ (γ , (_ , xs) , ys) → γ , (tt , xs) , ys )
|
||||
-- $ κ (λ (_ , (((((_ , x) , y) , _) , xs) , ys)) → (tt , cons x xs) , cons y ys)
|
||||
-- )
|
||||
-- ∷ []
|
||||
|
||||
-- listᵣ : {A B : Set} (R : Rel A B) → list A → list B → Set
|
||||
-- listᵣ {A} {B} R xs ys = μ listᵣD ((((tt , A) , B) , R) , (tt , xs) , ys)
|
||||
|
||||
-- nilᵣ : {A B : Set} {R : Rel A B} → listᵣ R nil nil
|
||||
-- nilᵣ = ⟨ zero , refl ⟩
|
||||
|
||||
-- consᵣ : {A B : Set} {R : Rel A B}
|
||||
-- → ∀ {x y } (x≈y : R x y)
|
||||
-- → ∀ {xs ys} (xs≈ys : listᵣ R xs ys)
|
||||
-- → listᵣ R (cons x xs) (cons y ys)
|
||||
-- consᵣ {x = x} {y} x≈y {xs} {ys} xs≈ys =
|
||||
-- ⟨ suc zero , x , y , x≈y , xs , ys , xs≈ys , refl ⟩
|
||||
|
||||
Hm. What we expect to generate looks like a mess. On a positive note it does
|
||||
seem like we do not need to add recursive occurences to the context. It is also reassuring that
|
||||
we can indeed encode the relation. Tbh the relation on its own is not *that* useful.
|
||||
What would be great is if we were able to derive the abstraction theorem for this datatype too::
|
||||
|
||||
-- param : (R : Rel A A) (PA : ∀ x → R x x)
|
||||
-- → (xs : list A) → listᵣ R xs xs
|
||||
-- param R PA ⟨ zero , refl ⟩ = nilᵣ
|
||||
-- param R PA ⟨ suc zero , x , xs , refl ⟩ = consᵣ (PA x) (param R PA xs)
|
||||
|
||||
This also looks quite doable.
|
||||
|
||||
Moving forward while keeping our head down.
|
||||
|
||||
|
||||
Relating telescope substitutions
|
||||
--------------------------------
|
||||
|
||||
The first thing we need is a relation on telescope substitutions.
|
||||
Naturally, because substitutions are encoded as Σ-types, two substitutions are related
|
||||
iff their elements are related one to one, using the relational
|
||||
interpretation of their respective types.
|
||||
|
||||
.. math::
|
||||
T : \tele A,\ x_1 : A,\ x_2 : A,\ x_r : ⟦A⟧_p
|
||||
\ ⊢ ⟦Π\ A\ ⟦ T ⟧ ⟧_p\ x_1\ x_2\ x_r : \rel {(⟦ T ⟧\ x_1)} {(⟦ T ⟧\ x_2)}
|
||||
|
||||
.. math::
|
||||
⟦Π\ A\ ⟦ε⟧⟧_p\ x_1\ x_2\ x_r\ t_1\ t_2 &≡ ⊤ \\
|
||||
⟦Π\ A\ ⟦T\ ▷\ F⟧⟧_p\ x_1\ x_2\ x_r\ (t_1 , s_1)\ (t_2 , s_2) &≡
|
||||
Σ\ (⟦Π\ A\ ⟦T⟧⟧_p\ x_1\ x_2\ x_r\ t_1\ t_2)\ λ\ t_r\ .
|
||||
\ ⟦ F ⟧_p\ t_1\ t_2\ t_r\ s_1\ s_2
|
||||
|
||||
The only problem here is that we need `⟦A⟧_p` and `⟦F⟧_p`. We cannot possibly compute it,
|
||||
because `A` could be virtually *anything*, not just one of our friendly described datatypes.
|
||||
An easy way out is to kindly ask for these relations. Therefore we introduce a new type
|
||||
`\textsf{Help}\ T` associated with the telescope `T` we're trying to translate,
|
||||
whose inhabitants must hold every required relation.
|
||||
|
||||
::
|
||||
|
||||
Help : Tele A → A → A → Set
|
||||
|
||||
-- I suspect we don't care about xᵣ so I'm omitting it
|
||||
ₜ⟦_⟧ₚ : (T : Tele A) {x y : A} → Help T x y → Rel (⟦ T ⟧ x) (⟦ T ⟧ y)
|
||||
|
||||
Help ε _ _ = ⊤
|
||||
Help (T ▷ F) x₁ x₂ = Σ (Help T x₁ x₂)
|
||||
λ H → ∀ t₁ t₂ (tᵣ : ₜ⟦ T ⟧ₚ H t₁ t₂)
|
||||
→ Rel (F (x₁ , t₁)) (F (x₂ , t₂))
|
||||
|
||||
ₜ⟦ ε ⟧ₚ tt tt tt = ⊤
|
||||
ₜ⟦ T ▷ F ⟧ₚ (H , HF) (t₁ , s₁) (t₂ , s₂) =
|
||||
Σ (ₜ⟦ T ⟧ₚ H t₁ t₂) λ tᵣ → HF t₁ t₂ tᵣ s₁ s₂
|
||||
|
||||
ExHelp : {P : Tele ⊤} → ExTele P → Set
|
||||
ExHelp I = ∀ p₁ p₂ → Help I p₁ p₂
|
||||
|
||||
|
||||
Not my type
|
||||
-----------
|
||||
|
||||
Our relation will be inductively defined, so we need to figure out beforehand its
|
||||
parameters and indices. Parameters are easy, we expect two substitutions of the initial
|
||||
parameters' telescope, and a proof that they are related.
|
||||
|
||||
::
|
||||
|
||||
module _ {P : Tele ⊤} {I : ExTele P} {n : Nat}
|
||||
(D : Desc P I n)
|
||||
(HP : Help P tt tt) (HI : ExHelp I)
|
||||
where
|
||||
|
||||
Pₚ : Tele ⊤
|
||||
Pₚ = ε
|
||||
▷₀ ⟦ P ⟧ tt
|
||||
▷₀ ⟦ P ⟧ tt
|
||||
▷ λ (_ , (_ , p₁) , p₂) → ₜ⟦ P ⟧ₚ HP p₁ p₂
|
||||
|
||||
p₁ : ⟦ Pₚ ⟧ tt → ⟦ P ⟧ tt
|
||||
p₁ (((_ , p) , _) , _) = p
|
||||
|
||||
p₂ : ⟦ Pₚ ⟧ tt → ⟦ P ⟧ tt
|
||||
p₂ (((_ , _) , p) , _) = p
|
||||
|
||||
Iₚ : ExTele Pₚ
|
||||
Iₚ = ε
|
||||
▷ (λ ((((_ , p₁) , _) , _) , _) → ⟦ I ⟧ p₁)
|
||||
▷ (λ ((((_ , _) , p₂) , _) , _) → ⟦ I ⟧ p₂)
|
||||
▷ (λ ((((_ , p₁) , _) , _) , (_ , i₁) , _) → μ D (p₁ , i₁))
|
||||
▷ (λ ((((_ , _) , p₂) , _) , (_ , i₂) , _) → μ D (p₂ , i₂))
|
||||
|
||||
|
||||
Apart from the typical clumsiness of dealing with substitutions, we have our parameters and indices.
|
||||
|
||||
----
|
||||
|
||||
::
|
||||
|
||||
Cₚ′ : {Γₚ : ExTele Pₚ}
|
||||
{Γ : ExTele P}
|
||||
→ (C : ConDesc Γ I)
|
||||
→ (c₁ : {p : ⟦ Pₚ ⟧ tt} → ⟦ Γₚ ⟧ p → ⟦ Γ ⟧ (p₁ p))
|
||||
→ (c₂ : {p : ⟦ Pₚ ⟧ tt} → ⟦ Γₚ ⟧ p → ⟦ Γ ⟧ (p₂ p))
|
||||
→ (f₁ : ⟦ C ⟧ᶜ (μ D) ({!!} , {!!}) → μ D ({!!} , {!!}))
|
||||
→ (ConDesc Γₚ Iₚ → ConDesc ε Iₚ)
|
||||
→ ConDesc ε Iₚ
|
||||
|
||||
Cₚ′ (κ f) g₁ g₂ _ tie =
|
||||
tie (κ (λ (p , g) → (((tt , ( f (p₁ p , g₁ g)))
|
||||
, f (p₂ p , g₂ g))
|
||||
, {!!}) , {!!}))
|
||||
|
||||
Cₚ′ (ι f C) c₁ c₂ _ tie =
|
||||
Cₚ′ C
|
||||
(c₁ ∘ λ ((p , _) , _) → p)
|
||||
(c₂ ∘ λ ((p , _) , _) → p)
|
||||
{!!}
|
||||
(tie ∘ λ C → σ (λ (p , g) → μ D (p₁ p , f (p₁ p , c₁ g)))
|
||||
$ σ (λ (p , g , _) → μ D (p₂ p , f (p₂ p , c₂ g)))
|
||||
$ ι (λ (p , (_ , x) , y) → (((tt , _) , _) , x) , y)
|
||||
$ C)
|
||||
|
||||
Cₚ′ (σ S C) c₁ c₂ _ tie =
|
||||
Cₚ′ C
|
||||
(λ (((g , s₁) , _) , _) → c₁ g , s₁)
|
||||
(λ (((g , _) , s₂) , _) → c₂ g , s₂)
|
||||
{!!}
|
||||
(tie ∘ λ C → σ (λ (p , g) → S (p₁ p , c₁ g))
|
||||
$ σ (λ (p , g , _) → S (p₂ p , c₂ g))
|
||||
$ σ {!!} -- we need some some relation here
|
||||
$ C)
|
||||
|
||||
Cₚ : ConDesc ε I → ConDesc ε Iₚ
|
||||
Cₚ C = Cₚ′ C id id {!!} id
|
||||
|
||||
Dₚ : Desc Pₚ Iₚ n
|
||||
Dₚ = map Cₚ D
|
||||
|
||||
CPS all the way.
|
||||
|
||||
----
|
||||
|
||||
Assuming we had implement what's missing above, we would have the relation we wanted::
|
||||
|
||||
⟦_⟧ₚ : {p₁ p₂ : ⟦ P ⟧ tt} (pᵣ : ₜ⟦ P ⟧ₚ HP p₁ p₂)
|
||||
{i₁ : ⟦ I ⟧ p₁} {i₂ : ⟦ I ⟧ p₂}
|
||||
→ Rel (μ D (p₁ , i₁)) (μ D (p₂ , i₂))
|
||||
⟦_⟧ₚ pᵣ t₁ t₂ = μ Dₚ ((_ , pᵣ) , (_ , t₁) , t₂)
|
||||
|
||||
The abstraction theorem becomes::
|
||||
|
||||
-- param : ∀ {p i} (t : μ D (p , i)) → ⟦_⟧ₚ {!!} {!!} t t
|
||||
-- param = {!!}
|
||||
|
||||
|
||||
----
|
||||
|
||||
An exemple on lists:
|
||||
|
||||
----
|
||||
|
||||
Conclusion
|
||||
~~~~~~~~~~
|
||||
|
||||
Now, why should we care? Well, I don't really know just yet.
|
||||
I do think there is value in having such transformations implemented in a type-safe way.
|
||||
Still, because these representations are not intrinsic to how datatypes are defined in the theory,
|
||||
it make for a clumsy experience. Add the lack of cumulativity and everything becomes quite tedious.
|
||||
|
||||
Things I would like to explore next:
|
||||
|
||||
- Derive the proofs that any datatype and its constructors are univalently parametric.
|
||||
As of now we can derive the relation, what remains to be proven is deriving an equivalence (easy)
|
||||
and a proof that the two are equivalent.
|
||||
|
||||
- Get rid of the :code:`--type-in-type` flag, using Effectfully's technique, or embracing :code:`--cumulativity`?
|
||||
|
||||
- Investigate encodings of other constructions: Co-inductive types? Records?
|
||||
|
||||
- Look into Formality's encoding of datatypes and what it means for generic programming.
|
||||
|
||||
----
|
||||
|
||||
.. [Bernardy2010] | **Parametricity and Dependent Types**
|
||||
| Jean-Philippe Bernardy, Patrik Jansson, Ross Paterson
|
||||
| http://www.staff.city.ac.uk/~ross/papers/pts.pdf
|
||||
|
||||
.. [Tabareau2019] | **The Marriage of Univalence and Parametricity**
|
||||
| Nicolas Tabareau, Eric Tanter, Matthieu Sozeau
|
||||
| https://arxiv.org/pdf/1909.05027.pdf
|
||||
|
||||
|
|
@ -10,531 +10,5 @@ labels:
|
|||
**achille** [aʃil] is a tiny Haskell library for building your very own **static site
|
||||
generator**. It is in spirit a direct successor to [Hakyll][Hakyll].
|
||||
|
||||
## Motivation
|
||||
|
||||
Static site generators (SSG) have proven to be very useful tools for easily
|
||||
generating static websites from neatly organised content files. Most of them
|
||||
support using **markup languages** like markdown for writing content, and offer
|
||||
**incremental compilation** so that updating a website stays **fast**,
|
||||
regardless of its size. However, most SSGs are very opinionated about how you
|
||||
should manage your content. As soon as your specific needs deviate slightly
|
||||
from what your SSG supports, it becomes a lot more tedious.
|
||||
|
||||
This leads to many people writing their own personal static site generators
|
||||
from scratch. This results in a completely personalised workflow, but without
|
||||
good libraries it is a time-consuming endeavor, and incremental compilation is often
|
||||
out of the equation as it is hard to get right.
|
||||
|
||||
This is where **achille** and [Hakyll][Hakyll] come in: they provide a *domain
|
||||
specific language* embedded in Haskell to easily yet very precisely describe
|
||||
how to build your site. Compile this description and **you get a full-fledged
|
||||
static site generator with incremental compilation**, tailored specifically to
|
||||
your needs.
|
||||
|
||||
[Hakyll]: https://jaspervdj.be/hakyll
|
||||
|
||||
### Why Hakyll is not enough
|
||||
|
||||
To provide incremental compilation, Hakyll relies on a global store, in which
|
||||
all your *intermediate values* are stored. It is *your* responsibility to
|
||||
populate it with *snapshots*. There are some severe limitations to this
|
||||
approach:
|
||||
|
||||
- The store is **fundamentally untyped**, so **retrieving snapshots may fail at
|
||||
runtime** if you're not careful when writing your build rules. You may
|
||||
argue that's not very critical --- I think it shouldn't be possible in the
|
||||
first place. We are using a strongly typed language, so we shouldn't have
|
||||
to rely on flaky coercions at runtime to manipulate intermediate values.
|
||||
|
||||
- **Loading snapshots with glob patterns is awkward**. With Hakyll, *the*
|
||||
way to retrieve intermediate values is by querying the store,
|
||||
using glob patterns. This indirect way of managing values is very
|
||||
clumsy. In Haskell, the very purpose of variables is to store intermediate
|
||||
values, so we should only have to deal with plain old variables.
|
||||
|
||||
- **Dependencies are not explicit**. Because it relies on a global store for
|
||||
handling intermediate values, Hakyll has to make sure that the snaphots you
|
||||
want to load have been generated already. And because rules have no imposed
|
||||
order despite implicit inter-dependencies, Hakyll has to evaluate very
|
||||
carefully each rule, eventually pausing them to compute missing dependencies.
|
||||
This is very complex and quite frankly impressive, yet I believe we can strive
|
||||
for a simpler model of evaluation. If we used plain old variables to hold
|
||||
intermediate values, we simply would not be allowed to refer to an undefined
|
||||
variable.
|
||||
|
||||
There are other somewhat debatable design decisions:
|
||||
|
||||
- In Hakyll, every rule will produce an output file, and only one, if you're
|
||||
restricting yourself to the API they provide. I argue
|
||||
such a library should not care whether a rule produces any output on the
|
||||
filesystem. Its role is merely to know *if the rule must be executed*. Because of
|
||||
this requirement, producing multiple outputs from the same file is a tad
|
||||
cumbersome.
|
||||
- Because Hakyll stores many content files directly in the store, the resulting
|
||||
cache is *huge*. This is unnecessary, the files are right here in the content
|
||||
directory.
|
||||
- Hakyll uses a *lot* of abstractions --- `Compiler`, `Item`, `Rule`, `RuleSet`
|
||||
--- whose purpose is not obvious to a newcomer.
|
||||
- It defines monads to allow the convenient `do` notation to be used, but
|
||||
disregards completely the very benefit of using monads --- it composes!
|
||||
|
||||
### Other tools
|
||||
|
||||
As always when thinking I am onto something, I jumped straight into code
|
||||
and forgot to check whether there were alternatives. By fixating on Hakyll, I did not
|
||||
realize many people have had the same comments about the shortcomings of Hakyll
|
||||
and improved upon it. Therefore, it's only after building most of **achille**
|
||||
in a week that I realized there were many
|
||||
other similar tools available, namely: [rib][rib], [slick][slick], [Pencil][pencil] &
|
||||
[Lykah][lykah].
|
||||
|
||||
[rib]: https://rib.srid.ca/
|
||||
[slick]: https://hackage.haskell.org/package/slick
|
||||
[pencil]: http://elbenshira.com/pencil/
|
||||
[lykah]: https://hackage.haskell.org/package/Lykah
|
||||
|
||||
Fortunately, I still believe **achille** is a significant improvement over these libraries.
|
||||
|
||||
- As far as I can tell, **pencil** does not provide incremental generation.
|
||||
It also relies on a global store, no longer untyped but very
|
||||
restrictive about what you can store. It implements its own templating language.
|
||||
- Likewise, no incremental generation in **Lykah**.
|
||||
Reimplements its own HTML DSL rather than use *lucid*.
|
||||
Very opinionated, undocumented and unmaintained.
|
||||
- **rib** and **slick** are the most feature-complete of the lot.
|
||||
They both provide a minimalist web-focused interface over the very powerful build system
|
||||
[Shake][Shake].
|
||||
|
||||
[Shake]: https://shakebuild.com/
|
||||
|
||||
## How achille works
|
||||
|
||||
In **achille** there is a single abstraction for reasoning about build rules:
|
||||
`Recipe m a b`. A **recipe** of type `Recipe m a b` will produce a value of type
|
||||
`m b` given some input of type `a`.
|
||||
Conveniently, if `m` is a monad then **`Recipe m a` is a monad** too, so
|
||||
you can retrieve the output of a recipe to reuse it in another recipe.
|
||||
|
||||
*(Because of caching, a recipe is **not** just a Kleisli arrow)*
|
||||
|
||||
|
||||
```haskell
|
||||
-- the (>>=) operator, restricted to recipes
|
||||
(>>=) :: Monad m => Recipe m a b -> (b -> Recipe m a c) -> Recipe m a c
|
||||
```
|
||||
|
||||
With only this, **achille** tackles every single one of the limitations highlighted above.
|
||||
|
||||
- Intermediate values are plain old Haskell variables.
|
||||
|
||||
```haskell
|
||||
renderPost :: Recipe IO FilePath Post
|
||||
buildPostIndex :: [Post] -> Recipe a ()
|
||||
|
||||
renderPosts :: Task IO ()
|
||||
renderPosts = do
|
||||
posts <- match "posts/*" renderPost
|
||||
buildPostIndex posts
|
||||
```
|
||||
|
||||
See how a correct ordering of build rules is enforced by design: you can only
|
||||
use an intermediate value once the recipe it is originating from has been
|
||||
executed.
|
||||
|
||||
Note: a **task** is a recipe that takes no input.
|
||||
|
||||
```haskell
|
||||
type Task m = Recipe m ()
|
||||
```
|
||||
|
||||
- **achille** does not care what happens during the execution of a recipe.
|
||||
It only cares about the input and return type of the recipe --- that is, the
|
||||
type of intermediate values.
|
||||
In particullar, **achille** does not expect every recipe to produce a file,
|
||||
and lets you decide when to actually write on the filesystem.
|
||||
|
||||
For example, it is very easy to produce multiple versions of a same source file:
|
||||
|
||||
```haskell
|
||||
renderPage :: Recipe IO FilePath FilePath
|
||||
renderPage = do
|
||||
-- Copy the input file as is to the output directory
|
||||
copyFile
|
||||
|
||||
-- Render the input file with pandoc,
|
||||
-- then save it to the output dir with extension ".html"
|
||||
compilePandoc >>= saveTo (-<.> "html")
|
||||
```
|
||||
|
||||
Once you have defined the recipe for building your site, you forward
|
||||
this description to **achille** in order to get a command-line interface for
|
||||
your generator, just as you would using Hakyll:
|
||||
|
||||
```haskell
|
||||
buildSite :: Task IO ()
|
||||
|
||||
main :: IO ()
|
||||
main = achille buildSite
|
||||
```
|
||||
|
||||
Assuming we compiled the file above into an executable called `site`, running
|
||||
it gives the following output:
|
||||
|
||||
```bash
|
||||
$ site
|
||||
A static site generator for fun and profit
|
||||
|
||||
Usage: site COMMAND
|
||||
|
||||
Available options:
|
||||
-h,--help Show this help text
|
||||
|
||||
Available commands:
|
||||
build Build the site once
|
||||
deploy Server go brrr
|
||||
clean Delete all artefacts
|
||||
```
|
||||
|
||||
That's it, you now have your very own static site generator!
|
||||
|
||||
### Caching
|
||||
|
||||
So far we haven't talked about caching and incremental builds.
|
||||
Rest assured: **achille produces generators with robust incremental
|
||||
builds** for free. To understand how this is done, we can simply look at the
|
||||
definition of `Recipe m a b`:
|
||||
|
||||
```haskell
|
||||
-- the cache is simply a lazy bytestring
|
||||
type Cache = ByteString
|
||||
|
||||
newtype Recipe m a b = Recipe (Context a -> m (b, Cache))
|
||||
```
|
||||
|
||||
In other words, when a recipe is run, it is provided a **context** containing
|
||||
the input value, **a current cache** *local* to the recipe, and some more
|
||||
information. The IO action is executed, and we update the local cache with the
|
||||
new cache returned by the recipe. We say *local* because of how composition of
|
||||
recipes is handled internally. When the *composition* of two recipes (made with
|
||||
`>>=` or `>>`) is being run, we retrieve two bytestrings from the local cache
|
||||
and feed them as local cache to both recipes respectively. Then we gather the two updated
|
||||
caches, join them and make it the new cache of the composition.
|
||||
|
||||
This way, a recipe is guaranteed to receive the same local cache it returned
|
||||
during the last run, *untouched by other recipes*. And every recipe is free to
|
||||
dispose of this local cache however it wants.
|
||||
|
||||
As a friend noted, **achille** is "just a library for composing memoized
|
||||
computations".
|
||||
|
||||
----
|
||||
|
||||
#### High-level interface
|
||||
|
||||
Because we do not want the user to carry the burden of updating the cache
|
||||
manually, **achille** comes with many utilies for common operations, managing
|
||||
the cache for us under the hood. Here is an exemple highlighting how we keep
|
||||
fine-grained control over the cache at all times, while never having to
|
||||
manipulate it directly.
|
||||
|
||||
Say you want to run a recipe for every file maching a glob pattern, *but do
|
||||
not care about the output of the recipe*. A typical exemple would be to copy
|
||||
every static asset of your site to the output directory. **achille** provides
|
||||
the `match_` function for this very purpose:
|
||||
|
||||
```haskell
|
||||
match_ :: Glob.Pattern -> Recipe FilePath b -> Recipe a ()
|
||||
```
|
||||
|
||||
We would use it in this way:
|
||||
|
||||
```haskell
|
||||
copyAssets :: Recipe a ()
|
||||
copyAssets = match_ "assets/*" copyFile
|
||||
|
||||
main :: IO ()
|
||||
main = achille copyAssets
|
||||
```
|
||||
|
||||
Under the hood, `match_ p r` will cache every filepath for which the recipe was
|
||||
run. During the next run, for every filepath matching the pattern, `match_ p r` will
|
||||
lookup the path in its cache. If it is found and hasn't been modified since,
|
||||
then we do nothing for this path. Otherwise, the task is run and the filepath
|
||||
added to the cache.
|
||||
|
||||
Now assume we do care about the output of the recipe we want to run on every filepath.
|
||||
For example if we compile every blogpost, we want to retrieve each blogpost's title and
|
||||
the filepath of the compiled `.html` file. In that case, we can use the
|
||||
built-in `match` function:
|
||||
|
||||
```haskell
|
||||
match :: Binary b
|
||||
=> Glob.Pattern -> Recipe FilePath b -> Recipe a [b]
|
||||
```
|
||||
|
||||
Notice the difference here: we expect the type of the recipe output `b` to have
|
||||
an instance of `Binary`, **so that we can encode it in the cache**. Fortunately,
|
||||
many of the usual Haskell types have an instance available. Then we can do:
|
||||
|
||||
```haskell
|
||||
data PostMeta = PostMeta { title :: Text }
|
||||
renderPost :: Text -> Text -> Text
|
||||
renderIndex :: [(Text, FilePath)] -> Text
|
||||
|
||||
buildPost :: Recipe FilePath (Text, FilePath)
|
||||
buildPost = do
|
||||
(PostMeta title, pandoc) <- compilePandocMeta
|
||||
renderPost title pdc & saveAs (-<.> "html")
|
||||
<&> (title,)
|
||||
|
||||
buildPost :: Recipe a [(Text, FilePath)]
|
||||
buildPosts = match "posts/*.md" buildPost
|
||||
|
||||
buildIndex :: [(Text, FilePath)] -> Recipe
|
||||
```
|
||||
|
||||
#### Shortcomings
|
||||
|
||||
The assertion *"A recipe will always receive the same cache between two runs"*
|
||||
can only violated in the two following situations:
|
||||
|
||||
- There is **conditional branching in your recipes**, and more specifically,
|
||||
**branching for which the branch taken can differ between runs**.
|
||||
|
||||
For example, it is **not** problematic to do branching on the extension of a file,
|
||||
as the same path will be taken each execution.
|
||||
|
||||
But assuming you want to parametrize by some boolean value for whatever reason,
|
||||
whose value you may change between runs, then because the two branches will
|
||||
share the same cache, every time the boolean changes, the recipe will start
|
||||
from an inconsistent cache so it will recompute from scratch, and overwrite
|
||||
the existing cache.
|
||||
|
||||
```haskell
|
||||
buildSection :: Bool -> Task IO ()
|
||||
buildSection isProductionBuild =
|
||||
if isProductionBuild then
|
||||
someRecipe
|
||||
else
|
||||
someOtherRecipe
|
||||
```
|
||||
|
||||
Although I expect few people ever do this kind of conditional branching for
|
||||
generating a static site, **achille** still comes with combinators for branching.
|
||||
You can use `if` in order to keep two separate caches for the two branches:
|
||||
|
||||
```haskell
|
||||
if :: Bool -> Recipe m a b -> Recipe m a b -> Recipe m a b
|
||||
```
|
||||
|
||||
The previous example becomes:
|
||||
|
||||
```haskell
|
||||
buildSection :: Bool -> Task IO ()
|
||||
buildSection isProductionBuild =
|
||||
Achille.if isProductionBuild
|
||||
someRecipe
|
||||
someOtherRecipe
|
||||
```
|
||||
|
||||
### No runtime failures
|
||||
|
||||
All the built-in cached recipes **achille** provides are implemented carefully
|
||||
so that **they never fail in case of cache corruption**. That is, in the
|
||||
eventuality of failing to retrieve the desired values from the cache, our
|
||||
recipes will automatically recompute the result from the input, ignoring the
|
||||
cache entirely. To make sure this is indeed what happens, every cached recipe
|
||||
in **achille** has been tested carefully (not yet really, but it is on the todo
|
||||
list).
|
||||
|
||||
This means the only failures possible are those related to poor content
|
||||
formatting from the user part: missing frontmatter fields, watching files
|
||||
that do not exist, etc. All of those are errors are gracefully reported to the
|
||||
user.
|
||||
|
||||
### Parallelism
|
||||
|
||||
**achille** could very easily support parallelism for free, I just didn't take
|
||||
the time to make it a reality.
|
||||
|
||||
|
||||
## Making a blog from scratch
|
||||
|
||||
Let's see how to use **achille** for making a static site generator for a blog.
|
||||
First we decide what will be the structure of our source directory.
|
||||
We choose the following:
|
||||
|
||||
```bash
|
||||
content
|
||||
└── posts
|
||||
├── 2020-04-13-hello-world.md
|
||||
├── 2020-04-14-another-article.md
|
||||
└── 2020-05-21-some-more.md
|
||||
```
|
||||
|
||||
We define the kind of metadata we want to allow in the frontmatter header
|
||||
of our markdown files:
|
||||
|
||||
```haskell
|
||||
{-# LANGUAGE DeriveGeneric #-}
|
||||
|
||||
import GHC.Generics
|
||||
import Data.Aeson
|
||||
import Data.Text (Text)
|
||||
|
||||
data Meta = Meta
|
||||
{ title :: Text
|
||||
} deriving (Generic)
|
||||
|
||||
instance FromJSON Meta
|
||||
```
|
||||
|
||||
This way we enfore correct metadata when retrieving the content of our files.
|
||||
Every markdown file will have to begin with the following header for our
|
||||
generator to proceed:
|
||||
|
||||
```markdown
|
||||
---
|
||||
title: Something about efficiency
|
||||
---
|
||||
```
|
||||
|
||||
Then we create a generic template for displaying a page, thanks to lucid:
|
||||
|
||||
```haskell
|
||||
{-# LANGUAGE OverloadedStrings #-}
|
||||
{-# LANGUAGE BlockArguments #-}
|
||||
|
||||
import Lucid.Html5
|
||||
|
||||
renderPost :: Text -> Text -> Html a
|
||||
renderPost title content = wrapContent do
|
||||
h1_ $ toHtml title
|
||||
toHtmlRaw content
|
||||
|
||||
renderIndex :: [(Text, FilePath)] -> Html a
|
||||
renderIndex = wrapContent .
|
||||
ul_ . mconcat . map \(title, path) ->
|
||||
li_ $ a_ [href_ path] $ toHtml title
|
||||
|
||||
wrapContent :: Html a -> Html a
|
||||
wrapContent content = doctypehtml_ do
|
||||
head_ do
|
||||
meta_ [charset_ "utf-8"]
|
||||
title_ "my very first blog"
|
||||
|
||||
body_ do
|
||||
header_ $ h1_ "BLOG"
|
||||
content_
|
||||
```
|
||||
|
||||
We define a recipe for rendering every post:
|
||||
|
||||
```haskell
|
||||
buildPosts :: Task IO [(String, FilePath)]
|
||||
buildPosts =
|
||||
match "posts/*.md" do
|
||||
(Meta title, text) <- compilePandocMetadata
|
||||
saveFileAs (-<.> "html") (renderPost title text)
|
||||
<&> (title,)
|
||||
```
|
||||
|
||||
We can define a simple recipe for rendering the index, given a list of posts:
|
||||
|
||||
```haskell
|
||||
buildIndex :: [(Text, FilePath)] -> Task IO FilePath
|
||||
buildIndex posts =
|
||||
save (renderIndex posts) "index.html"
|
||||
```
|
||||
|
||||
Then, it's only a matter of composing the recipes and giving them to **achille**:
|
||||
|
||||
```haskell
|
||||
main :: IO ()
|
||||
main = achille do
|
||||
posts <- buildPosts
|
||||
buildIndex posts
|
||||
```
|
||||
|
||||
And that's it, you now have a very minimalist incremental blog generator!
|
||||
|
||||
## Recursive recipes
|
||||
|
||||
It is very easy to define recursive recipes in **achille**. This allows us to
|
||||
traverse and build tree-like structures, such as wikis.
|
||||
|
||||
For example, given the following structure:
|
||||
|
||||
```bash
|
||||
content
|
||||
├── index.md
|
||||
├── folder1
|
||||
│ └── index.md
|
||||
└── folder2
|
||||
├── index.md
|
||||
├── folder21
|
||||
│ └── index.md
|
||||
├── folder22
|
||||
│ └── index.md
|
||||
└── folder23
|
||||
├── index.md
|
||||
├── folder231
|
||||
│ └── index.md
|
||||
├── folder222
|
||||
│ └── index.md
|
||||
└── folder233
|
||||
└── index.md
|
||||
```
|
||||
|
||||
We can generate a site with the same structure and in which each index page has
|
||||
links to its children:
|
||||
|
||||
```haskell
|
||||
renderIndex :: PageMeta -> [(PageMeta, FilePath)] -> Text -> Html
|
||||
|
||||
buildIndex :: Recipe IO a (PageMeta, FilePath)
|
||||
buildIndex = do
|
||||
children <- walkDir
|
||||
|
||||
matchFile "index.*" do
|
||||
(meta, text) <- compilePandoc
|
||||
renderIndex meta children text >>= save (-<.> "html")
|
||||
return $ (meta,) <$> getInput
|
||||
|
||||
walkDir :: Recipe IO a [(PageMeta, FilePath)]
|
||||
walkDir = matchDir "*/" buildIndex
|
||||
|
||||
main :: IO ()
|
||||
main = achille buildIndex
|
||||
```
|
||||
|
||||
## Forcing the regeneration of output
|
||||
|
||||
Currently, **achille** doesn't track what files a recipe produces in the output
|
||||
dir. This means you cannot ask for things like *"Please rebuild
|
||||
output/index.html"*.
|
||||
|
||||
That's because we make the assumption that the output dir is untouched between
|
||||
builds. The only reason I can think of for wanting to rebuild a specific page
|
||||
is if the template used to generate it has changed.
|
||||
But in that case, the template is *just another input*.
|
||||
So you can treat it as such by putting it in your content directory and doing
|
||||
the following:
|
||||
|
||||
```haskell
|
||||
import Templates.Index (renderIndex)
|
||||
|
||||
buildIndex :: Task IO ()
|
||||
buildIndex =
|
||||
watchFile "Templates/Index.hs" $ match_ "index.*" do
|
||||
compilePandoc <&> renderIndex >>= write "index.html"
|
||||
```
|
||||
|
||||
This way, **achille** will automatically rebuild your index if the template has
|
||||
changed!
|
||||
|
||||
While writing these lines, I realized it would be very easy for **achille**
|
||||
to know which recipe produced which output file,
|
||||
so I might just add that. Still, it would still require you to ask for an output
|
||||
file to be rebuilt if a template has changed. With the above pattern, it is
|
||||
handled automatically!
|
||||
|
|
|
|||
|
|
@ -8,7 +8,20 @@ labels:
|
|||
---
|
||||
|
||||
**jibniz** is a javascript implementation of the IBNIZ virtual machine.
|
||||
IBNIZ is an esoteric stack-based programming language created by _, in which almost every
|
||||
IBNIZ is an esoteric stack-based programming language created by _, in which every
|
||||
instruction is one character long. The code is intended to be ran for each
|
||||
pixel on a 256x256 screen, at every frame, thus making it possible to produce
|
||||
animations.
|
||||
pixel on a 256x256 screen, at every frame --- making it possible to produce
|
||||
animations and interactive demos.
|
||||
|
||||
## Limitations
|
||||
|
||||
- Currently, this implementation has **no support for audio**. At the time I remember
|
||||
the WebAudio API to be very poorly designed, and I did not understand how it was
|
||||
implemented in the official IBNIZ VM.
|
||||
- I use WebGL for color conversion because I never figured out how to actually
|
||||
reliably convert YUV to RGB. The original C implementation uses SDL2
|
||||
Overlays or something, and I was not able to reverse engineer the conversion.
|
||||
I found floating-point formulas, hence the GLSL shader, etc.
|
||||
- At some point I wanted to compile the entire IBNIZ programs to WASM, rather
|
||||
than build an interpreter. The problem is that IBNIZ programs are *unstructured*.
|
||||
the `J` instruction allows you to jump *anywhere* in the program.
|
||||
|
|
|
|||
|
|
@ -7,8 +7,8 @@ otherwise. In other words, you are free to copy, redistribute and edit this
|
|||
content, provided you: give appropriate credit; indicate where changes were made
|
||||
and do not do so for commercial purposes.
|
||||
|
||||
This website is self-hosted on a OneProvider
|
||||
dedicated server in Paris. The domain name `acatalepsie.fr <https://acatalepsie.fr>`_ has
|
||||
This website is hosted on a 2014 RPi Model B+ somewhere in France.
|
||||
The domain name `acatalepsie.fr <https://acatalepsie.fr>`_ has
|
||||
been registered at `gandi.net <https://gandi.net>`_.
|
||||
|
||||
.. _CC BY-NC 2.0: https://creativecommons.org/licenses/by-nc/2.0/
|
||||
|
|
|
|||
|
|
@ -0,0 +1 @@
|
|||
../../.git/annex/objects/gZ/XG/SHA256E-s184840--08fe7d08c0d946d119eef787f31d0f28224fdfa001975450e83b66d7691072da.jpg/SHA256E-s184840--08fe7d08c0d946d119eef787f31d0f28224fdfa001975450e83b66d7691072da.jpg
|
||||
|
|
@ -0,0 +1 @@
|
|||
../../.git/annex/objects/k3/30/SHA256E-s631729--32753a717b3349dfdce80e732b32e53de3eb4361e8f77c76258b663c9e8cfa32.png/SHA256E-s631729--32753a717b3349dfdce80e732b32e53de3eb4361e8f77c76258b663c9e8cfa32.png
|
||||
|
|
@ -0,0 +1 @@
|
|||
../../.git/annex/objects/4p/V6/SHA256E-s918970--e7a695c389a762320704a52f5390c37a162dae81ff2df614ce38f40df03be73d.png/SHA256E-s918970--e7a695c389a762320704a52f5390c37a162dae81ff2df614ce38f40df03be73d.png
|
||||
|
|
@ -0,0 +1 @@
|
|||
../../.git/annex/objects/J5/jZ/SHA256E-s1346919--a6f9e1df5e2593fa1a868244769f16522defbf4bd2c38e0c9014e379d93fdd68.png/SHA256E-s1346919--a6f9e1df5e2593fa1a868244769f16522defbf4bd2c38e0c9014e379d93fdd68.png
|
||||
|
|
@ -0,0 +1 @@
|
|||
../../.git/annex/objects/wj/7m/SHA256E-s299494--9826507fe82e22161368e3b8008aab5df58d6f4fdb8b29c4f47279faa3a35f74.png/SHA256E-s299494--9826507fe82e22161368e3b8008aab5df58d6f4fdb8b29c4f47279faa3a35f74.png
|
||||
|
|
@ -0,0 +1 @@
|
|||
../../.git/annex/objects/9J/X7/SHA256E-s670715--d1841af7719367ad43becc186af1d3c520b775bb2bf54da2cb92c135911dbbfb.png/SHA256E-s670715--d1841af7719367ad43becc186af1d3c520b775bb2bf54da2cb92c135911dbbfb.png
|
||||
|
|
@ -0,0 +1 @@
|
|||
../../.git/annex/objects/wp/jK/SHA256E-s321424--297046f12e2941743a19183faaaa8ebd55428367bc0ee2f457c467495481423c.png/SHA256E-s321424--297046f12e2941743a19183faaaa8ebd55428367bc0ee2f457c467495481423c.png
|
||||
|
|
@ -0,0 +1 @@
|
|||
../../.git/annex/objects/m1/gJ/SHA256E-s1364718--8fdba85d9550064e2acab434042fcc0aeb376563516a8bf9ad3e2244db00021c.png/SHA256E-s1364718--8fdba85d9550064e2acab434042fcc0aeb376563516a8bf9ad3e2244db00021c.png
|
||||
|
|
@ -0,0 +1 @@
|
|||
../../.git/annex/objects/gF/87/SHA256E-s458925--e06294cd0c55b73f4ff119ac3299d4f96139ede37ae2fb18110a126b48eede91.jpg/SHA256E-s458925--e06294cd0c55b73f4ff119ac3299d4f96139ede37ae2fb18110a126b48eede91.jpg
|
||||
|
|
@ -0,0 +1 @@
|
|||
../../.git/annex/objects/Q6/MF/SHA256E-s1949616--8f6aee3703fcec5d6e16724c39ad938d26e96b477855b9e05de180bad5bf6e51.png/SHA256E-s1949616--8f6aee3703fcec5d6e16724c39ad938d26e96b477855b9e05de180bad5bf6e51.png
|
||||
|
|
@ -0,0 +1 @@
|
|||
../../.git/annex/objects/86/p5/SHA256E-s8693437--b5cde85117ffee4fc0ef1f9ae4a9887c12dced028baca4ce76939efef5568b84.png/SHA256E-s8693437--b5cde85117ffee4fc0ef1f9ae4a9887c12dced028baca4ce76939efef5568b84.png
|
||||
|
|
@ -0,0 +1 @@
|
|||
../../.git/annex/objects/27/kP/SHA256E-s600318--d1e1ae2cef2879eae698498f3c4e3b4907a9f39b227b0c3816fe020e34df066c.png/SHA256E-s600318--d1e1ae2cef2879eae698498f3c4e3b4907a9f39b227b0c3816fe020e34df066c.png
|
||||
|
|
@ -0,0 +1 @@
|
|||
../../.git/annex/objects/FF/Fp/SHA256E-s2521385--1ad730393c6d1c8159c966019893fbfacfef84b64eef47a26b4d0869e0f8fd58.png/SHA256E-s2521385--1ad730393c6d1c8159c966019893fbfacfef84b64eef47a26b4d0869e0f8fd58.png
|
||||
|
|
@ -0,0 +1 @@
|
|||
../../.git/annex/objects/42/v4/SHA256E-s1446118--c14985cde38d539fe967254266bcacd35feb89fb9c2817e969ce916ae8967989.png/SHA256E-s1446118--c14985cde38d539fe967254266bcacd35feb89fb9c2817e969ce916ae8967989.png
|
||||
|
|
@ -0,0 +1 @@
|
|||
../../.git/annex/objects/1p/9X/SHA256E-s1411058--46562b966839842feae88561bdd7cd0e6106138ac17b79de7aa0228846d32aad.png/SHA256E-s1411058--46562b966839842feae88561bdd7cd0e6106138ac17b79de7aa0228846d32aad.png
|
||||
|
|
@ -0,0 +1 @@
|
|||
../../.git/annex/objects/91/mZ/SHA256E-s1841625--21ce2fad4fa27a77c23eeb8dd2d84ab9d3a5c4b130ef1d4687b6a2c0122d9f24.png/SHA256E-s1841625--21ce2fad4fa27a77c23eeb8dd2d84ab9d3a5c4b130ef1d4687b6a2c0122d9f24.png
|
||||
|
|
@ -0,0 +1 @@
|
|||
../../.git/annex/objects/j1/04/SHA256E-s202502--d067dc4336ca30160227a30c48722e6df50626c5f777f56b6b2a5e8767c26848.png/SHA256E-s202502--d067dc4336ca30160227a30c48722e6df50626c5f777f56b6b2a5e8767c26848.png
|
||||
|
|
@ -0,0 +1 @@
|
|||
../../.git/annex/objects/07/26/SHA256E-s919785--393de0aeef6648c5dd5faba83ec92d182d7cc827e5d75599d155c99a826e5c26.png/SHA256E-s919785--393de0aeef6648c5dd5faba83ec92d182d7cc827e5d75599d155c99a826e5c26.png
|
||||
|
|
@ -0,0 +1 @@
|
|||
../../.git/annex/objects/xx/0f/SHA256E-s495379--3b920599ddf4ed84c19616f1bfd2cdc76a7a876785ebb2432b21e20085eaa2ea.png/SHA256E-s495379--3b920599ddf4ed84c19616f1bfd2cdc76a7a876785ebb2432b21e20085eaa2ea.png
|
||||
|
|
@ -1 +0,0 @@
|
|||
../../../.git/annex/objects/gZ/XG/SHA256E-s184840--08fe7d08c0d946d119eef787f31d0f28224fdfa001975450e83b66d7691072da.jpg/SHA256E-s184840--08fe7d08c0d946d119eef787f31d0f28224fdfa001975450e83b66d7691072da.jpg
|
||||
|
|
@ -1 +0,0 @@
|
|||
../../../.git/annex/objects/k3/30/SHA256E-s631729--32753a717b3349dfdce80e732b32e53de3eb4361e8f77c76258b663c9e8cfa32.png/SHA256E-s631729--32753a717b3349dfdce80e732b32e53de3eb4361e8f77c76258b663c9e8cfa32.png
|
||||
|
|
@ -1 +0,0 @@
|
|||
../../../.git/annex/objects/4p/V6/SHA256E-s918970--e7a695c389a762320704a52f5390c37a162dae81ff2df614ce38f40df03be73d.png/SHA256E-s918970--e7a695c389a762320704a52f5390c37a162dae81ff2df614ce38f40df03be73d.png
|
||||
|
|
@ -1 +0,0 @@
|
|||
../../../.git/annex/objects/J5/jZ/SHA256E-s1346919--a6f9e1df5e2593fa1a868244769f16522defbf4bd2c38e0c9014e379d93fdd68.png/SHA256E-s1346919--a6f9e1df5e2593fa1a868244769f16522defbf4bd2c38e0c9014e379d93fdd68.png
|
||||
|
|
@ -1 +0,0 @@
|
|||
../../../.git/annex/objects/wj/7m/SHA256E-s299494--9826507fe82e22161368e3b8008aab5df58d6f4fdb8b29c4f47279faa3a35f74.png/SHA256E-s299494--9826507fe82e22161368e3b8008aab5df58d6f4fdb8b29c4f47279faa3a35f74.png
|
||||
|
|
@ -1 +0,0 @@
|
|||
../../../.git/annex/objects/9J/X7/SHA256E-s670715--d1841af7719367ad43becc186af1d3c520b775bb2bf54da2cb92c135911dbbfb.png/SHA256E-s670715--d1841af7719367ad43becc186af1d3c520b775bb2bf54da2cb92c135911dbbfb.png
|
||||
|
|
@ -1 +0,0 @@
|
|||
../../../.git/annex/objects/wp/jK/SHA256E-s321424--297046f12e2941743a19183faaaa8ebd55428367bc0ee2f457c467495481423c.png/SHA256E-s321424--297046f12e2941743a19183faaaa8ebd55428367bc0ee2f457c467495481423c.png
|
||||
|
|
@ -1 +0,0 @@
|
|||
../../../.git/annex/objects/m1/gJ/SHA256E-s1364718--8fdba85d9550064e2acab434042fcc0aeb376563516a8bf9ad3e2244db00021c.png/SHA256E-s1364718--8fdba85d9550064e2acab434042fcc0aeb376563516a8bf9ad3e2244db00021c.png
|
||||
|
|
@ -1 +0,0 @@
|
|||
../../../.git/annex/objects/gF/87/SHA256E-s458925--e06294cd0c55b73f4ff119ac3299d4f96139ede37ae2fb18110a126b48eede91.jpg/SHA256E-s458925--e06294cd0c55b73f4ff119ac3299d4f96139ede37ae2fb18110a126b48eede91.jpg
|
||||
|
|
@ -1 +0,0 @@
|
|||
../../../.git/annex/objects/Q6/MF/SHA256E-s1949616--8f6aee3703fcec5d6e16724c39ad938d26e96b477855b9e05de180bad5bf6e51.png/SHA256E-s1949616--8f6aee3703fcec5d6e16724c39ad938d26e96b477855b9e05de180bad5bf6e51.png
|
||||
|
|
@ -1 +0,0 @@
|
|||
../../../.git/annex/objects/86/p5/SHA256E-s8693437--b5cde85117ffee4fc0ef1f9ae4a9887c12dced028baca4ce76939efef5568b84.png/SHA256E-s8693437--b5cde85117ffee4fc0ef1f9ae4a9887c12dced028baca4ce76939efef5568b84.png
|
||||
|
|
@ -1 +0,0 @@
|
|||
../../../.git/annex/objects/27/kP/SHA256E-s600318--d1e1ae2cef2879eae698498f3c4e3b4907a9f39b227b0c3816fe020e34df066c.png/SHA256E-s600318--d1e1ae2cef2879eae698498f3c4e3b4907a9f39b227b0c3816fe020e34df066c.png
|
||||
|
|
@ -1 +0,0 @@
|
|||
../../../.git/annex/objects/FF/Fp/SHA256E-s2521385--1ad730393c6d1c8159c966019893fbfacfef84b64eef47a26b4d0869e0f8fd58.png/SHA256E-s2521385--1ad730393c6d1c8159c966019893fbfacfef84b64eef47a26b4d0869e0f8fd58.png
|
||||
|
|
@ -1 +0,0 @@
|
|||
../../../.git/annex/objects/42/v4/SHA256E-s1446118--c14985cde38d539fe967254266bcacd35feb89fb9c2817e969ce916ae8967989.png/SHA256E-s1446118--c14985cde38d539fe967254266bcacd35feb89fb9c2817e969ce916ae8967989.png
|
||||
|
|
@ -1 +0,0 @@
|
|||
../../../.git/annex/objects/1p/9X/SHA256E-s1411058--46562b966839842feae88561bdd7cd0e6106138ac17b79de7aa0228846d32aad.png/SHA256E-s1411058--46562b966839842feae88561bdd7cd0e6106138ac17b79de7aa0228846d32aad.png
|
||||
|
|
@ -1 +0,0 @@
|
|||
../../../.git/annex/objects/91/mZ/SHA256E-s1841625--21ce2fad4fa27a77c23eeb8dd2d84ab9d3a5c4b130ef1d4687b6a2c0122d9f24.png/SHA256E-s1841625--21ce2fad4fa27a77c23eeb8dd2d84ab9d3a5c4b130ef1d4687b6a2c0122d9f24.png
|
||||
|
|
@ -1 +0,0 @@
|
|||
../../../.git/annex/objects/j1/04/SHA256E-s202502--d067dc4336ca30160227a30c48722e6df50626c5f777f56b6b2a5e8767c26848.png/SHA256E-s202502--d067dc4336ca30160227a30c48722e6df50626c5f777f56b6b2a5e8767c26848.png
|
||||
|
|
@ -1 +0,0 @@
|
|||
../../../.git/annex/objects/07/26/SHA256E-s919785--393de0aeef6648c5dd5faba83ec92d182d7cc827e5d75599d155c99a826e5c26.png/SHA256E-s919785--393de0aeef6648c5dd5faba83ec92d182d7cc827e5d75599d155c99a826e5c26.png
|
||||
|
|
@ -1 +0,0 @@
|
|||
../../../.git/annex/objects/xx/0f/SHA256E-s495379--3b920599ddf4ed84c19616f1bfd2cdc76a7a876785ebb2432b21e20085eaa2ea.png/SHA256E-s495379--3b920599ddf4ed84c19616f1bfd2cdc76a7a876785ebb2432b21e20085eaa2ea.png
|
||||
|
|
@ -15,6 +15,7 @@ executable site
|
|||
build-depends: base >=4.12 && <4.13
|
||||
, filepath
|
||||
, achille
|
||||
, data-default
|
||||
, blaze-html
|
||||
, blaze-markup
|
||||
, pandoc
|
||||
|
|
|
|||
81
src/Main.hs
81
src/Main.hs
|
|
@ -1,10 +1,14 @@
|
|||
{-# LANGUAGE OverloadedStrings #-}
|
||||
{-# LANGUAGE BlockArguments #-}
|
||||
{-# LANGUAGE TupleSections #-}
|
||||
{-# LANGUAGE DuplicateRecordFields #-}
|
||||
{-# LANGUAGE DisambiguateRecordFields #-}
|
||||
{-# LANGUAGE NamedFieldPuns #-}
|
||||
|
||||
import Data.Functor ((<&>))
|
||||
import Data.Functor
|
||||
import Data.Maybe (fromMaybe, mapMaybe)
|
||||
import System.FilePath ((-<.>))
|
||||
import Control.Monad (when)
|
||||
import System.FilePath
|
||||
import Text.Pandoc.Options
|
||||
|
||||
import Achille
|
||||
|
|
@ -12,21 +16,72 @@ import Achille.Recipe.Pandoc
|
|||
|
||||
import Page
|
||||
import Templates
|
||||
import Types
|
||||
|
||||
|
||||
config :: Config
|
||||
config = def
|
||||
{ deployCmd = Just "rsync -avzzr _site/ --chmod=755 flupe@duckduck.me:/var/www/acatalepsie"
|
||||
{ deployCmd = Just "rsync -avzzr _site/ --chmod=755 pi@192.168.0.45:/var/www/html"
|
||||
|
||||
-- by making everything absolute you can run the command from anywhere
|
||||
, contentDir = "/home/flupe/dev/acatalepsie/content"
|
||||
, outputDir = "/home/flupe/dev/acatalepsie/_site"
|
||||
, cacheFile = "/home/flupe/dev/acatalepsie/.cache"
|
||||
}
|
||||
|
||||
|
||||
-- pandoc options
|
||||
ropts :: ReaderOptions
|
||||
ropts = def
|
||||
{ readerExtensions =
|
||||
enableExtension Ext_smart githubMarkdownExtensions
|
||||
}
|
||||
|
||||
wopts :: WriterOptions
|
||||
wopts = def
|
||||
{ writerHTMLMathMethod = KaTeX ""
|
||||
}
|
||||
|
||||
|
||||
buildProject :: Recipe IO a (Project, FilePath)
|
||||
buildProject = do
|
||||
name <- takeBaseName <$> getCurrentDir
|
||||
|
||||
-- task $ match_ "*" copyFile
|
||||
match "*" copyFile
|
||||
|
||||
children <- buildChildren
|
||||
|
||||
watch children $ matchFile "index.*" do
|
||||
(meta, doc) <- readPandocMetadataWith ropts
|
||||
renderPandocWith wopts doc <&> renderProject meta children
|
||||
>>= saveFileAs (-<.> "html")
|
||||
>> (meta,) <$> getCurrentDir
|
||||
where
|
||||
buildChildren :: Recipe IO a [(String, FilePath)]
|
||||
buildChildren = match "pages/*" do
|
||||
(TitledPage title _, doc) <- readPandocMetadataWith ropts
|
||||
renderPandocWith wopts doc
|
||||
<&> outerWith (def {title = title})
|
||||
>>= saveFileAs ((-<.> "html") . takeFileName)
|
||||
<&> (title,)
|
||||
|
||||
|
||||
main :: IO ()
|
||||
main = achilleWith config do
|
||||
match_ "assets/*" copyFile
|
||||
match_ "./quid.rst" $ compilePandoc <&> outer >>= saveFileAs (-<.> "html")
|
||||
|
||||
-----------
|
||||
-- QUID
|
||||
|
||||
match_ "./quid.rst" $
|
||||
compilePandoc <&> outerWith def {title = "quid"}
|
||||
>>= saveFileAs (-<.> "html")
|
||||
|
||||
-----------
|
||||
-- VISUAL
|
||||
|
||||
pictures <- match "visual/*/*" do
|
||||
pictures <- match "visual/*" do
|
||||
copyFile
|
||||
runCommandWith (-<.> "thumb.png")
|
||||
(\a b -> "convert -resize 740x " <> a <> " " <> b)
|
||||
|
|
@ -39,13 +94,7 @@ main = achilleWith config do
|
|||
-------------
|
||||
-- PROJECTS
|
||||
|
||||
projects <- matchDir "projects/*/" do
|
||||
task $ match_ "*" copyFile
|
||||
matchFile "index.*" do
|
||||
(meta, doc) <- readPandocMetadataWith ropts
|
||||
renderPandoc doc <&> renderProject meta
|
||||
>>= saveFileAs (-<.> "html")
|
||||
>> (meta,) <$> getCurrentDir
|
||||
projects <- matchDir "projects/*/" buildProject
|
||||
|
||||
watch projects $ match_ "./projects.rst" do
|
||||
debug "rendering project index"
|
||||
|
|
@ -57,7 +106,7 @@ main = achilleWith config do
|
|||
|
||||
posts <- match "posts/*" do
|
||||
src <- copyFile
|
||||
(Page title d, pdc) <- readPandocMetadata
|
||||
(Page title d, pdc) <- readPandocMetadataWith ropts
|
||||
|
||||
renderPandocWith wopts pdc
|
||||
<&> renderPost title src
|
||||
|
|
@ -75,9 +124,3 @@ main = achilleWith config do
|
|||
compilePandoc
|
||||
<&> renderIndex visible
|
||||
>>= saveFileAs (-<.> "html")
|
||||
|
||||
ropts :: ReaderOptions
|
||||
ropts = def { readerExtensions = enableExtension Ext_smart githubMarkdownExtensions }
|
||||
|
||||
wopts :: WriterOptions
|
||||
wopts = def { writerHTMLMathMethod = KaTeX "" }
|
||||
|
|
|
|||
|
|
@ -1,10 +1,14 @@
|
|||
{-# LANGUAGE OverloadedStrings #-}
|
||||
{-# LANGUAGE BlockArguments #-}
|
||||
{-# LANGUAGE DuplicateRecordFields #-}
|
||||
{-# LANGUAGE DisambiguateRecordFields #-}
|
||||
{-# LANGUAGE NamedFieldPuns #-}
|
||||
{-# LANGUAGE RecordWildCards #-}
|
||||
|
||||
module Templates where
|
||||
|
||||
import Data.String (fromString)
|
||||
import Control.Monad (forM_)
|
||||
import Control.Monad (forM_, when)
|
||||
|
||||
import System.FilePath
|
||||
import Text.Blaze.Internal as I
|
||||
|
|
@ -13,17 +17,20 @@ import Text.Blaze.Html5.Attributes as A
|
|||
import Data.Dates.Types (DateTime(..), months, capitalize)
|
||||
|
||||
import Achille
|
||||
import Types (Project)
|
||||
import Types
|
||||
import qualified Types
|
||||
import qualified Data.Map.Strict as Map
|
||||
|
||||
showDate :: DateTime -> String
|
||||
showDate (DateTime y m d _ _ _) = month <> " " <> show d <> ", " <> show y
|
||||
where month = capitalize (months !! (m - 1))
|
||||
where month = take 3 $ capitalize (months !! (m - 1))
|
||||
|
||||
loading :: AttributeValue -> Attribute
|
||||
loading = I.customAttribute "loading"
|
||||
|
||||
property :: AttributeValue -> Attribute
|
||||
property = I.customAttribute "property"
|
||||
|
||||
toLink :: FilePath -> Html -> Html
|
||||
toLink url = H.a ! A.href (fromString $ "/" <> url)
|
||||
|
||||
|
|
@ -33,14 +40,14 @@ renderIndex posts content =
|
|||
outer do
|
||||
content
|
||||
H.h2 "Latest notes"
|
||||
H.ul $ forM_ posts \(Timestamped d (title, src)) ->
|
||||
H.ul ! A.id "pidx" $ forM_ posts \(Timestamped d (title, src)) ->
|
||||
H.li do
|
||||
H.span $ fromString $ showDate d <> ": "
|
||||
H.span $ fromString $ showDate d
|
||||
toLink src (fromString title)
|
||||
|
||||
renderPost :: String -> FilePath -> Html -> Html
|
||||
renderPost title source content =
|
||||
outer do
|
||||
outerWith def {Types.title = title} do
|
||||
H.h1 $ fromString title
|
||||
toLink source "View source"
|
||||
content
|
||||
|
|
@ -54,20 +61,23 @@ renderVisual txt imgs =
|
|||
H.figure $ H.img ! A.src (fromString p)
|
||||
! loading "lazy"
|
||||
|
||||
renderProject :: Project -> Html -> Html
|
||||
renderProject project content =
|
||||
outer do
|
||||
renderProject :: Project -> [(String, FilePath)] -> Html -> Html
|
||||
renderProject (project@Project{title,..}) children content =
|
||||
outerWith def {Types.title = title} do
|
||||
H.header ! A.class_ "project" $ do
|
||||
H.div $ H.img ! A.src "logo.svg"
|
||||
H.div do
|
||||
H.h1 $ fromString $ Types.title project
|
||||
H.p $ fromString $ Types.subtitle project
|
||||
H.ul $ forM_ (Map.toList $ Types.labels project) \(k, v) -> H.li do
|
||||
H.h1 $ fromString $ title
|
||||
H.p $ fromString $ subtitle
|
||||
H.ul $ forM_ (Map.toList labels) \(k, v) -> H.li do
|
||||
fromString k <> ": "
|
||||
if k == "repo" then
|
||||
H.a ! A.href (fromString $ "https://github.com/" <> v)
|
||||
$ fromString v
|
||||
else fromString v
|
||||
when (length children > 0) $
|
||||
H.ul ! A.class_ "pages" $ forM_ children \(t,l) ->
|
||||
H.li $ H.a ! A.href (fromString l) $ (fromString t)
|
||||
content
|
||||
|
||||
renderProjects :: Html -> [(Project, FilePath)] -> Html
|
||||
|
|
@ -75,11 +85,11 @@ renderProjects txt paths =
|
|||
outer do
|
||||
txt
|
||||
H.ul ! A.class_ "projects" $ do
|
||||
forM_ paths \(project, link) -> H.li $ H.a ! A.href (fromString link) $ do
|
||||
forM_ paths \(Project{title,..}, link) -> H.li $ H.a ! A.href (fromString link) $ do
|
||||
H.div $ H.img ! A.src (fromString $ link </> "logo.svg")
|
||||
H.div do
|
||||
H.h2 $ fromString (Types.title project)
|
||||
H.p $ fromString (Types.subtitle project)
|
||||
H.h2 $ fromString title
|
||||
H.p $ fromString subtitle
|
||||
-- H.ul $ forM_ (Map.toList $ Types.labels project) \(k, v) ->
|
||||
-- H.li $ (fromString k <> ": " <> fromString v)
|
||||
|
||||
|
|
@ -87,7 +97,10 @@ logo :: Html
|
|||
logo = preEscapedString "<svg xmlns=\"http://www.w3.org/2000/svg\" version=\"1.1\" height=\"19px\" width=\"29px\"><path d=\"M 2,2 A 5,5 0 0 1 7,7 L 7, 12 A 5, 5 0 0 1 2,17 M 7,7 A 5,5 0 0 1 12,2 L 22,2 A 5,5 0 0 1 27,7 L 27,12 A 5, 5 0 0 1 22,17 L 12,17\" style=\"stroke-width: 2; stroke-linecap: butt; stroke-linejoin: bevel; stroke: #fff\" fill=\"none\"/></svg>"
|
||||
|
||||
outer :: Html -> Html
|
||||
outer content = H.docTypeHtml do
|
||||
outer = outerWith def
|
||||
|
||||
outerWith :: SiteConfig -> Html -> Html
|
||||
outerWith SiteConfig{title,..} content = H.docTypeHtml do
|
||||
H.head do
|
||||
H.meta ! A.name "viewport"
|
||||
! A.content "width=device-width, initial-scale=1.0, user-scalable=yes"
|
||||
|
|
@ -95,7 +108,21 @@ outer content = H.docTypeHtml do
|
|||
H.meta ! A.name "robots" ! A.content "index, follow"
|
||||
H.meta ! charset "utf-8"
|
||||
H.link ! A.rel "stylesheet" ! A.href "/assets/theme.css"
|
||||
H.title "sbbls"
|
||||
|
||||
-- OpenGraph
|
||||
H.meta ! property "og:title"
|
||||
! A.content (fromString title)
|
||||
|
||||
H.meta ! property "og:type"
|
||||
! A.content "website"
|
||||
|
||||
H.meta ! property "og:image"
|
||||
! A.content (fromString image)
|
||||
|
||||
H.meta ! property "og:description"
|
||||
! A.content (fromString description)
|
||||
|
||||
H.title (fromString title)
|
||||
|
||||
H.body do
|
||||
H.header ! A.id "hd" $ H.section do
|
||||
|
|
@ -112,3 +139,4 @@ outer content = H.docTypeHtml do
|
|||
H.a ! A.href "https://creativecommons.org/licenses/by-nc/2.0/" $ "CC BY-NC 2.0"
|
||||
" · "
|
||||
H.a ! A.href "https://instagram.com/ba.bou.m/" $ "instagram"
|
||||
|
||||
|
|
|
|||
22
src/Types.hs
22
src/Types.hs
|
|
@ -1,10 +1,12 @@
|
|||
{-# LANGUAGE DeriveGeneric #-}
|
||||
{-# LANGUAGE DuplicateRecordFields #-}
|
||||
|
||||
module Types where
|
||||
|
||||
import GHC.Generics
|
||||
import Data.Aeson.Types (FromJSON)
|
||||
import Data.Binary (Binary, put, get)
|
||||
import Data.Default
|
||||
import qualified Data.Map.Strict as Map
|
||||
|
||||
data Project = Project
|
||||
|
|
@ -15,8 +17,28 @@ data Project = Project
|
|||
, gallery :: Maybe Bool
|
||||
} deriving (Generic, Eq, Show)
|
||||
|
||||
data TitledPage = TitledPage
|
||||
{ title :: String
|
||||
, description :: Maybe String
|
||||
} deriving (Generic, Eq, Show)
|
||||
|
||||
instance FromJSON Project
|
||||
instance FromJSON TitledPage
|
||||
|
||||
instance Binary Project where
|
||||
put (Project t s y l g) = put t >> put s >> put y >> put l >> put g
|
||||
get = Project <$> get <*> get <*> get <*> get <*> get
|
||||
|
||||
|
||||
data SiteConfig = SiteConfig
|
||||
{ title :: String
|
||||
, description :: String
|
||||
, image :: String
|
||||
}
|
||||
|
||||
instance Default SiteConfig where
|
||||
def = SiteConfig
|
||||
{ title = "sbbls"
|
||||
, description = "my personal web space, for your enjoyment"
|
||||
, image = "https://acatalepsie.fr/assets/card.png"
|
||||
}
|
||||
|
|
|
|||
Loading…
Reference in New Issue