commit 989197d48825c1585069853365c04a80ab5951dc
Author: xenia <xenia.agda@gmail.com>
Date:   Sun Sep 3 00:05:29 2023 +0200

    Initial commit: UTF-8 encoding + decoding, parsing framework based on agdarsec, starts of a HTTP parser, fucked up socket FFI, simple HTTP server

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..7e66ae2
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,3 @@
+**/artifacts
+**/result
+**/*.agdai
diff --git a/flake.lock b/flake.lock
new file mode 100644
index 0000000..853ea8a
--- /dev/null
+++ b/flake.lock
@@ -0,0 +1,61 @@
+{
+  "nodes": {
+    "flake-utils": {
+      "inputs": {
+        "systems": "systems"
+      },
+      "locked": {
+        "lastModified": 1689068808,
+        "narHash": "sha256-6ixXo3wt24N/melDWjq70UuHQLxGV8jZvooRanIHXw0=",
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "rev": "919d646de7be200f3bf08cb76ae1f09402b6f9b4",
+        "type": "github"
+      },
+      "original": {
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "type": "github"
+      }
+    },
+    "nixpkgs": {
+      "locked": {
+        "lastModified": 1692543165,
+        "narHash": "sha256-3Zar2aWrNbzSCnN2Q5A05zX1W9tvAqyibNkVJryID+c=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "52e3c9e18f8ff4a930b444675b6325552f12d104",
+        "type": "github"
+      },
+      "original": {
+        "owner": "NixOS",
+        "ref": "release-23.05",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "root": {
+      "inputs": {
+        "flake-utils": "flake-utils",
+        "nixpkgs": "nixpkgs"
+      }
+    },
+    "systems": {
+      "locked": {
+        "lastModified": 1681028828,
+        "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
+        "owner": "nix-systems",
+        "repo": "default",
+        "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nix-systems",
+        "repo": "default",
+        "type": "github"
+      }
+    }
+  },
+  "root": "root",
+  "version": 7
+}
diff --git a/flake.nix b/flake.nix
new file mode 100644
index 0000000..e57c15d
--- /dev/null
+++ b/flake.nix
@@ -0,0 +1,65 @@
+{
+  description = "henttp - agda web library";
+
+  inputs = {
+    nixpkgs.url = "github:NixOS/nixpkgs/release-23.05";
+    flake-utils.url = "github:numtide/flake-utils";
+  };
+
+  outputs = { self, nixpkgs, flake-utils }: flake-utils.lib.eachDefaultSystem (sys:
+    let pkgs = nixpkgs.legacyPackages.${sys};
+
+        agda = pkgs.agda.withPackages {
+          pkgs = pkgs: [ pkgs.standard-library ];
+          ghc = pkgs.ghc.withPackages (pkgs: with pkgs; [ bytestring network network-run utf8-string ]);
+        };
+        buildInputs = with pkgs; [
+          agda
+        ];
+
+        common = ''
+          build() {
+            mkdir -p ./artifacts
+            ${agda}/bin/agda --compile-dir ./artifacts --compile "''${1:-./Main.agda}"
+          }
+        '';
+
+        henttp = pkgs.stdenv.mkDerivation {
+          name = "henttp";
+          src = ./src;
+          inherit buildInputs;
+          buildPhase = common + ''
+            build
+            mkdir -p $out/bin
+            mv artifacts/main $out/bin/henttp
+          '';
+        };
+
+        check-all = pkgs.stdenv.mkDerivation {
+          name = "henttp-run-tests";
+          src = ./src;
+          buildInputs = buildInputs ++ [ pkgs.fd ];
+          buildPhase = common + ''
+            set -e
+            check() {
+              echo "[ Checking $1 ]"
+              agda "$1"
+            }
+            export -f check
+            fd 'Test.agda$' --exec bash -c 'check "$@"' _ {}
+            echo "All test passed :)"
+            touch $out
+          '';
+        };
+    in {
+      packages = {
+        henttp = henttp;
+        default = henttp;
+      };
+      devShell = pkgs.mkShell { packages = buildInputs; shellHook = common; };
+      checks = {
+        default = check-all;
+      };
+    }
+  );
+}
diff --git a/src/Base.agda b/src/Base.agda
new file mode 100644
index 0000000..4b8f19f
--- /dev/null
+++ b/src/Base.agda
@@ -0,0 +1,95 @@
+open import Agda.Primitive renaming (Set to Type)
+open import Data.Bool
+open import Data.Empty
+open import Data.Unit
+open import Data.Nat
+import Data.String as String
+open import Data.List
+
+module Base where
+
+case_of_ : {A B : Type} → A → (A → B) → B
+case x of f = f x
+
+is-false : Bool → Type
+is-false true = ⊥
+is-false false = ⊤
+
+record Monad (M : Type → Type) : Type₁ where
+  field
+    pure : {A : Type} → A → M A
+    _>>=_ : {A B : Type} → M A → (A → M B) → M B
+
+  _>>_ : {A B : Type} → M A → M B → M B
+  a >> b = a >>= λ _ → b
+
+  _<$>_ : {A B : Type} → (A → B) → M A → M B
+  f <$> x = x >>= (λ a → pure (f a))
+
+open Monad ⦃...⦄ public
+
+data Maybe (A : Type) : Type where
+  cake : Maybe A
+  real : A → Maybe A
+
+{-# COMPILE GHC Maybe = data Maybe (Nothing | Just) #-}
+
+_or-else_ : {A : Type} → Maybe A → A → A
+(real x) or-else _ = x
+cake or-else x = x
+
+is-real : {A : Type} → Maybe A → Type
+is-real cake = ⊥
+is-real (real x) = ⊤
+
+get-real : {A : Type} → (x : Maybe A) → { is-real x } → A
+get-real (real x) = x
+
+instance
+  MonadMaybe : Monad Maybe
+  MonadMaybe .pure = real
+  (MonadMaybe ._>>=_) cake f = cake
+  (MonadMaybe ._>>=_) (real x) f = f x
+
+record Eq (T : Type) : Type₁ where
+  field
+    _==_ : T → T → Bool
+open Eq ⦃...⦄ public
+
+instance
+  import Data.Nat
+  import Data.Char
+  import Data.String
+
+  Eqℕ : Eq Data.Nat.ℕ
+  Eqℕ ._==_ a b = a Data.Nat.≡ᵇ b
+
+  EqCh : Eq Data.Char.Char
+  EqCh ._==_ a b = a Data.Char.== b
+
+  EqString : Eq Data.String.String
+  EqString ._==_ a b = a Data.String.== b
+
+record Show (T : Type) : Type₁ where
+  field
+    showPrec : T → ℕ → String.String
+  show : T → String.String
+  show x = showPrec x 0
+open Show ⦃...⦄ public
+
+instance
+  open import Data.Nat.Show using () renaming (show to show-ℕ)
+  ShowNat : Show ℕ
+  ShowNat .showPrec x _ = show-ℕ x
+
+  ShowString : Show String.String
+  ShowString .showPrec x _ = String.show x
+
+  ShowList : {A : Type} → ⦃ Show A ⦄ → Show (List A)
+  ShowList {A} .showPrec x _ = "[" String.++ go x String.++ "]"
+    where
+      go : List A → String.String
+      go [] = ""
+      go (x ∷ []) = showPrec x 0
+      go (x ∷ xs) = showPrec x 0 String.++ ", " String.++ go xs
+
diff --git a/src/Bits-and-Bytes.agda b/src/Bits-and-Bytes.agda
new file mode 100644
index 0000000..8c9a2ba
--- /dev/null
+++ b/src/Bits-and-Bytes.agda
@@ -0,0 +1,143 @@
+open import Agda.Primitive renaming (Set to Type)
+
+open import Data.Nat
+open import Data.Nat.DivMod
+open import Data.Nat.Properties using (<ᵇ⇒<; *-comm; *-monoˡ-≤; *-monoˡ-<)
+open import Data.Fin using () renaming (zero to zeroᶠ; suc to sucᶠ)
+open import Data.Bool hiding (_<_; _≤_; _<?_)
+open import Data.Vec
+open import Data.Product
+open import Relation.Binary.PropositionalEquality
+open import Relation.Nullary
+
+open import Base
+
+module Bits-and-Bytes where
+
+record Byte : Type where
+  field
+    value : ℕ
+    {in-range} : value < 256
+open Byte public
+
+<_> : (v : ℕ) → {T (v <ᵇ 256)} → Byte
+< v > {prf} = record { value = v ; in-range = <ᵇ⇒< v 256 prf }
+
+module bytes where
+  NULL CR LF SPACE BIG : Byte
+  NULL    = < 0 >
+  LF      = < 10 >
+  CR      = < 13 >
+  SPACE   = < 32 >
+  SLASH   = < 47 >
+  PERCENT = < 37 >
+  BIG     = < 0xff >
+
+instance
+  EqByte : Eq Byte
+  EqByte ._==_ a b = a .value == b .value
+
+  ShowByte : Show Byte
+  ShowByte .showPrec x _ = "< " String.++ showPrec (x .value) 1 String.++ " >"
+    where
+      import Data.String as String
+
+mkClip : ℕ → Byte
+mkClip v = case v <? 256 of λ where
+  (yes v<256) → record { value = v ; in-range = v<256 }
+  (no _) → bytes.BIG
+
+data Bit : Type where
+  𝟘 𝟙 : Bit
+
+-- LSB first‼
+Bits : ℕ → Type
+Bits n = Vec Bit n
+
+Bit8 : Type
+Bit8 = Bits 8
+
+rshift1 : {max : ℕ} → (n : ℕ) → n < 2 * max → Σ (ℕ × Bit) λ (quot , _) → quot < max
+rshift1 {max} n n<2m = (quot , shift-out) , quot<max
+  where
+    divmod : DivMod n 2
+    divmod = n divMod 2
+
+    quot : ℕ
+    quot = DivMod.quotient divmod
+
+    shift-out : Bit
+    shift-out = case (DivMod.remainder divmod) of λ where
+      (zeroᶠ) → 𝟘
+      (sucᶠ zeroᶠ) → 𝟙
+
+    postulate
+      quot<max : quot < max
+    -- quot<max = {!!} -- TODO
+
+enbits : {n : ℕ} → (x : ℕ) → x < 2 ^ n → Bits n
+enbits {zero} zero x<2^n = []
+enbits {zero} (suc x) (s≤s ())
+enbits {n@(suc pn)} x x<2^n = shift-out ∷ enbits {pn} quot quot<2^pn
+  where
+    a : (Σ (ℕ × Bit) λ (quot , _) → quot < 2 ^ pn)
+    a = rshift1 {2 ^ pn} x x<2^n
+
+    quot : ℕ
+    quot = proj₁ (proj₁ a)
+
+    shift-out : Bit
+    shift-out = proj₂ (proj₁ a)
+
+    quot<2^pn : quot < 2 ^ pn
+    quot<2^pn = proj₂ a
+
+unbits : {n : ℕ} → Bits n → Σ ℕ λ x → x < 2 ^ n
+unbits {zero} [] = (0 , s≤s z≤n)
+unbits {n@(suc pn)} (x ∷ xs) = crazy-hamburger
+  where
+    -- suc x ≤ n → suc (suc (2 * x)) ≤ 2 * n
+    x<n→s2x<2n : {x n : ℕ} → x < n → suc (2 * x) < 2 * n
+    x<n→s2x<2n {x} {n} x<n = subst₂ (λ a b → suc (suc a) ≤ b) (*-comm x 2) (*-comm n 2) (*-monoˡ-≤ 2 x<n)
+
+    x<n→2x<2n : {x n : ℕ} → x < n → 2 * x < 2 * n -- 2 * x < 2 * n
+    x<n→2x<2n {x} {n} x<n = subst₂ (λ a b → a < b) (*-comm x 2) (*-comm n 2) (*-monoˡ-< 1 x<n)
+
+    rest : Σ ℕ λ x → x < 2 ^ pn
+    rest = unbits {pn} xs
+
+    crazy-hamburger : Σ ℕ λ x → x < 2 ^ n
+    crazy-hamburger = case x of λ where
+      𝟘 → (2 * proj₁ rest , x<n→2x<2n (proj₂ rest))
+      𝟙 → (suc (2 * proj₁ rest) , x<n→s2x<2n (proj₂ rest))
+
+Byte-to-Bit8 : Byte → Bit8
+Byte-to-Bit8 b = enbits (b .value) (b .in-range)
+
+Bit8-to-Byte : Bit8 → Byte
+Bit8-to-Byte x =
+  let b , b<256 = unbits x
+  in record { value = b ; in-range = b<256 }
+
+module Foreign where
+  {-# FOREIGN GHC
+    import qualified Data.Word as Word
+  #-}
+
+  postulate
+    Word8 : Type
+    ℕ-to-Word8 : ℕ → Word8 -- wraps
+    Word8-to-ℕ : Word8 → ℕ
+
+    Word8-to-ℕ-in-range : (w : Word8) → Word8-to-ℕ w < 256
+
+  {-# COMPILE GHC Word8 = type Word.Word8 #-}
+  {-# COMPILE GHC ℕ-to-Word8 = fromIntegral :: Integer -> Word.Word8 #-}
+  {-# COMPILE GHC Word8-to-ℕ = fromIntegral :: Word.Word8 -> Integer #-}
+
+  Byte-to-Word8 : Byte → Word8
+  Byte-to-Word8 b = ℕ-to-Word8 (b .value)
+
+  Word8-to-Byte : Word8 → Byte
+  Word8-to-Byte w = record { value = Word8-to-ℕ w ; in-range = Word8-to-ℕ-in-range w }
+open Foreign using (Word8; Byte-to-Word8; Word8-to-Byte) public
diff --git a/src/Indexed.agda b/src/Indexed.agda
new file mode 100644
index 0000000..0c6cc57
--- /dev/null
+++ b/src/Indexed.agda
@@ -0,0 +1,144 @@
+{-# OPTIONS --postfix-projections #-}
+
+module Indexed where
+
+open import Relation.Binary.PropositionalEquality hiding ([_])
+open import Data.Nat renaming (_≡ᵇ_ to _==ⁿ_; _<ᵇ_ to _<ⁿ_)
+open import Data.Nat.Properties using (≤-refl; ≤-step; ≤-trans)
+open import Data.Nat.DivMod hiding (result)
+open import Data.Vec hiding ([_]; _>>=_; foldr; foldl) renaming (map to mapᵥ)
+open import Data.List using (List; length) renaming ([] to []ₗ; _∷_ to _∷ₗ_; _++_ to _++ₗ_)
+open import Data.Bool hiding (_<_; _≤_) renaming (_∧_ to _&&_; _∨_ to _||_; T to is-true)
+open import Data.Product hiding (map; map₁; map₂)
+open import Data.Unit using (⊤; tt)
+open import Data.Empty using (⊥)
+
+open import Agda.Primitive renaming (Set to Type)
+
+open import Base
+open import NonEmpty
+
+module boolean-compare where
+  if′_then_else_ : {A : Type} → (b : Bool) → (is-true b → A) → (is-false b → A) → A
+  if′ true then a else _ = a tt
+  if′ false then _ else b = b tt
+
+  _≤ⁿ_ : ℕ → ℕ → Bool
+  0 ≤ⁿ y = true
+  suc x ≤ⁿ y = x <ⁿ y
+
+  _>ⁿ_ : ℕ → ℕ → Bool
+  a >ⁿ b = b <ⁿ a
+
+  _≥ⁿ_ : ℕ → ℕ → Bool
+  a ≥ⁿ b = b ≤ⁿ a
+
+  <ⁿ-trans : (a b c : ℕ) → is-true (a <ⁿ b) → is-true (b <ⁿ c) → is-true (a <ⁿ c)
+  <ⁿ-trans zero    (suc b) (suc c) tt sb<sc = tt
+  <ⁿ-trans (suc a) (suc b) (suc c) sa<sb sb<sc = <ⁿ-trans a b c sa<sb sb<sc
+
+  -- needed for conversion because DivMod uses nat's comparisons and we want to use them
+  <→<ⁿ : {a b : ℕ} → a < b → is-true (a <ⁿ b)
+  <→<ⁿ {zero} {suc b} (s≤s z≤n) = tt
+  <→<ⁿ {suc a} {suc b} (s≤s sa<sb) = <→<ⁿ {a} {b} sa<sb
+
+  ≤→≤ⁿ : {a b : ℕ} → a ≤ b → is-true (a ≤ⁿ b)
+  ≤→≤ⁿ {zero} {b} a≤b = tt
+  ≤→≤ⁿ {suc a} {b} a≤b = <→<ⁿ {a} {b} a≤b
+
+  <ⁿ→< : {a b : ℕ} → is-true (a <ⁿ b) → a < b
+  <ⁿ→< {zero} {suc b} t = s≤s z≤n
+  <ⁿ→< {suc a} {suc b} t = s≤s (<ⁿ→< {a} {b} t)
+
+  ≤ⁿ→≤ : {a b : ℕ} → is-true (a ≤ⁿ b) → a ≤ b
+  ≤ⁿ→≤ {zero} {b} t = z≤n
+  ≤ⁿ→≤ {suc a} {b} t = <ⁿ→< {a} {b} t
+open boolean-compare public
+
+k′ : Type → (ℕ → Type)
+(k′ A) i = A
+
+-- lift functions
+_→′_ : (ℕ → Type) → (ℕ → Type) → (ℕ → Type)
+(A →′ B) i = A i → B i
+
+-- lift products
+_×′_ : (ℕ → Type) → (ℕ → Type) → (ℕ → Type)
+(A ×′ B) i = A i × B i
+
+-- lower to implicit
+[_] : (ℕ → Type) → Type
+[ A ] = {i : ℕ} → A i
+
+record □_ (A : ℕ → Type) (n : ℕ) : Type where
+  constructor mk□
+  field
+    call : {m : ℕ} → m < n → A m
+open □_ public
+
+□-0 : {A : ℕ → Type} → (□ A) 0
+□-0 .call ()
+
+infix 0 [_]
+infixr 1 _×′_
+infixr 1 _→′_
+infixl 100 □_
+
+map : {A B : ℕ → Type} → [ A →′ B ] → [ □ A →′ □ B ]
+map f □a .call lt = f (□a .call lt)
+
+module map-elaborate where
+  map₁ map₂ : {A B : ℕ → Type}
+      → ({i : ℕ} →    A  i →    B  i)
+      → ({n : ℕ} → (□ A) n → (□ B) n)
+  map₁ f {n} □a .call {m} m<n = f (□a .call {m} m<n)
+  map₂ f = λ □a → mk□ λ m<n → f (□a .call m<n)
+
+-- we have for all n, for all m<n, A
+-- specialize n = suc i, supply i < suc i
+extract : {A : ℕ → Type} → [ □ A ] → [ A ]
+extract □a {i} = □a .call {i} (≤-refl {suc i})
+
+enbox : {A : ℕ → Type} → [ A ] → [ □ A ]
+enbox a = mk□ λ {m} pf → a {m}
+
+strong-induction : {A : ℕ → Type}
+                 → ((n : ℕ) → ((m : ℕ) → m < n → A m) → A n)
+                 → (n : ℕ)
+                 → A n
+strong-induction {A} ind = λ n → helper (suc n) n ≤-refl
+  where
+    data _∨_ (A B : Type) : Type where
+      inl : A → A ∨ B
+      inr : B → A ∨ B
+
+    lt-split : (a b : ℕ) → a < suc b → (a < b) ∨ (a ≡ b)
+    lt-split zero zero p = inr refl
+    lt-split zero (suc b) p = inl (s≤s z≤n)
+    lt-split (suc a) zero (s≤s ())
+    lt-split (suc a) (suc b) (s≤s p) with lt-split a b p
+    ... | inl a<b = inl (s≤s a<b)
+    ... | inr a≡b = inr (cong suc a≡b)
+
+    helper : (n : ℕ) → (m : ℕ) → m < n → A m
+    helper zero m ()
+    helper n@(suc pn) m m<n with lt-split m pn m<n
+    ... | inl m<pn = helper pn m m<pn
+    ... | inr m≡pn = ind m (subst (λ a → (m′ : ℕ) → m′ < a → A m′) (sym m≡pn) (helper pn))
+
+ℕ-ind : {P : ℕ → Type}
+      → ((n : ℕ) → ((m : ℕ) → @0 m < n → P m) → P n)
+      → (n : ℕ)
+      → P n
+ℕ-ind {P} f n = f n (go n ≤-refl)
+  where
+    -- m < p ≤ n
+    go : (p : ℕ) → @0 p ≤ n → (m : ℕ) → @0 m < p → P m
+    go _ _ zero _ = f zero (λ m ())
+    go p@(suc pp) (s≤s l) m@(suc pm) (s≤s q) = f m λ k x → go pp (≤-step l) k (≤-trans x q)
+
+fix : {A : ℕ → Type}
+    → [ □ A →′ A ]
+    → [ A ]
+--fix {A} □a→a {n} = strong-induction (λ n ind → □a→a (mk□ λ {m} m<n → ind m m<n)) n
+fix {A} □a→a {n} = ℕ-ind (λ n ind → □a→a (mk□ λ {m} m<n → ind m m<n)) n
diff --git a/src/Main.agda b/src/Main.agda
new file mode 100644
index 0000000..90aa188
--- /dev/null
+++ b/src/Main.agda
@@ -0,0 +1,62 @@
+{-# OPTIONS --guardedness --postfix-projections #-}
+
+module main where
+
+open import Agda.Primitive renaming (Set to Type)
+import Data.String as String
+import Data.Char as Char
+open import Data.Product
+open import Data.Nat
+open import Data.Unit using (⊤; tt)
+open import Data.Vec using (fromList)
+open import Data.List hiding (take; [_])
+
+open import Base
+open import Bits-and-Bytes
+open import SysIO
+open import Socket
+open import Indexed
+open import Parsing (Byte)
+open import NonEmpty
+open import Parse-HTTP
+import UTF-8
+
+parse-digit : [ Parser Byte ]
+parse-digit = (\ b → b .value <ᵇ 58) <?>′ any₁
+
+parse-thing : [ Parser (List⁺ Byte) ]
+parse-thing = many parse-digit -- (\ (a , b) → a ∷⁺ [ b ]⁺ ) <$>′ (parse-digit <&>′ enbox parse-digit)
+
+200-ok : String.String → List Byte → List Byte
+200-ok content-type content = UTF-8.encode-string (String.toList (headers String.++ "\r\n\r\n")) ++ content
+  where
+    headers : String.String
+    headers = "HTTP/1.1 200 OK\r\nContent-Type: " String.++ content-type String.++ "; charset=utf-8\r\nContent-Length: " String.++ (show (length content))
+
+mk-response : (Path × Maybe String.String) → String.String
+mk-response req = "hiii from agda‼ \nmjau mjau mjau :3 <^_^> ∷3\nyou queried the path " String.++ show (proj₁ req) String.++ " :)\n"
+
+
+handle : Socket → IO (List Byte)
+handle sock = do
+  putStrLn "handle: new connection‼"
+  let got = get-bytes sock
+
+  let parsed = parse-get-request .parse (fromList got)
+
+  case parsed of λ where
+    (real res) → putStrLn ("handle: path = " String.++ show (proj₁ (res .result)) String.++ ", query = " String.++ proj₂ (res .result) or-else "(no query)")
+    cake → putStrLn "handle: parser died"
+
+  case parsed of λ where
+    (real res) → pure (200-ok "text/plain" (UTF-8.encode-string (String.toList (mk-response (res .result)))))
+    cake → pure (UTF-8.encode-string (String.toList "epic fail\n"))
+
+run-port : ℕ
+run-port = 1337
+
+main : IO ⊤
+main = do
+  putStrLn "main: starting"
+  putStrLn ("main: running on port " String.++ show run-port)
+  run-server "localhost" run-port handle
diff --git a/src/NonEmpty.agda b/src/NonEmpty.agda
new file mode 100644
index 0000000..f772d83
--- /dev/null
+++ b/src/NonEmpty.agda
@@ -0,0 +1,30 @@
+module NonEmpty where
+
+open import Data.List using (List; []; _∷_)
+open import Agda.Primitive renaming (Set to Type)
+
+open import Base
+
+data List⁺ (A : Type) : Type where
+  [_]⁺ : A → List⁺ A
+  _∷⁺_ : A → List⁺ A → List⁺ A
+
+infixr 0 _∷⁺_
+
+foldr : {A B : Type} → (A → B → B) → B → List⁺ A → B
+foldr _+_ base [ x ]⁺ = x + base
+foldr _+_ base (x ∷⁺ xs) = x + foldr _+_ base xs
+
+foldl : {A B : Type} → (B → A → B) → B → List⁺ A → B
+foldl _+_ acc [ x ]⁺ = acc + x
+foldl _+_ acc (x ∷⁺ xs) = foldl _+_ (acc + x) xs
+
+list⁺-to-list : {A : Type} → List⁺ A → List A
+list⁺-to-list [ x ]⁺ = x ∷ []
+list⁺-to-list (x ∷⁺ xs) = x ∷ list⁺-to-list xs
+
+instance
+  ShowList⁺ : {A : Type} → ⦃ Show A ⦄ → Show (List⁺ A)
+  ShowList⁺ .showPrec x p = showPrec (list⁺-to-list x) p String.++ "⁺"
+    where
+      import Data.String as String
diff --git a/src/Parse-HTTP.agda b/src/Parse-HTTP.agda
new file mode 100644
index 0000000..03cb498
--- /dev/null
+++ b/src/Parse-HTTP.agda
@@ -0,0 +1,185 @@
+open import Agda.Primitive renaming (Set to Type)
+
+open import Data.Vec renaming (map to mapᵥ) hiding ([_]; foldr; foldl)
+import Data.List as List
+open import Data.Nat
+open import Data.Nat.Properties using (<ᵇ⇒<)
+open import Data.Bool hiding (_<_)
+open import Data.Unit
+open import Data.Product
+
+import Data.String as String
+import Data.Char as Char
+
+open import Base
+
+open import Indexed
+open import NonEmpty
+open import Bits-and-Bytes
+import UTF-8
+
+open import Parsing (Byte)
+open import Parse-HTTP.Helpers
+
+module Parse-HTTP where
+
+-- HTTP Method: GET, POST, etc.
+data HTTP-Method : Type where
+  GET HEAD POST PUT DELETE CONNECT OPTIONS TRACE PATCH : HTTP-Method
+
+instance
+  ShowMethod : Show HTTP-Method
+  ShowMethod .showPrec x _ = go x
+    where
+      go : HTTP-Method → String.String
+      go GET     = "GET"
+      go HEAD    = "HEAD"
+      go POST    = "POST"
+      go PUT     = "PUT"
+      go DELETE  = "DELETE"
+      go CONNECT = "CONNECT"
+      go OPTIONS = "OPTIONS"
+      go TRACE   = "TRACE"
+      go PATCH   = "PATCH"
+
+name-of-enc : HTTP-Method → Σ ℕ λ n → Vec Byte (suc n)
+name-of-enc GET     = _ , < 71 > ∷ < 69 > ∷ < 84 > ∷ []
+name-of-enc HEAD    = _ , < 72 > ∷ < 69 > ∷ < 65 > ∷ < 68 > ∷ []
+name-of-enc POST    = _ , < 80 > ∷ < 79 > ∷ < 83 > ∷ < 84 > ∷ []
+name-of-enc PUT     = _ , < 80 > ∷ < 85 > ∷ < 84 > ∷ []
+name-of-enc DELETE  = _ , < 68 > ∷ < 69 > ∷ < 76 > ∷ < 69 > ∷ < 84 > ∷ < 69 > ∷ []
+name-of-enc CONNECT = _ , < 67 > ∷ < 79 > ∷ < 78 > ∷ < 78 > ∷ < 69 > ∷ < 67 > ∷ < 84 > ∷ []
+name-of-enc OPTIONS = _ , < 79 > ∷ < 80 > ∷ < 84 > ∷ < 73 > ∷ < 79 > ∷ < 78 > ∷ < 83 > ∷ []
+name-of-enc TRACE   = _ , < 84 > ∷ < 82 > ∷ < 65 > ∷ < 67 > ∷ < 69 > ∷ []
+name-of-enc PATCH   = _ , < 80 > ∷ < 65 > ∷ < 84 > ∷ < 67 > ∷ < 72 > ∷ []
+
+http-methods : List⁺ HTTP-Method
+http-methods = GET ∷⁺ HEAD ∷⁺ POST ∷⁺ PUT ∷⁺ DELETE ∷⁺ CONNECT ∷⁺ OPTIONS ∷⁺ TRACE ∷⁺ [ PATCH ]⁺
+
+parse-specific-http-method : HTTP-Method → [ Parser HTTP-Method ]
+parse-specific-http-method m = (λ _ → m) <$>′ exact name
+  where
+    name-len : ℕ
+    name-len = proj₁ (name-of-enc m)
+    name : Vec Byte (suc name-len)
+    name = proj₂ (name-of-enc m)
+
+    parse-name : [ Parser ⊤ ]
+    parse-name = exact name
+
+parse-http-method : [ Parser HTTP-Method ]
+parse-http-method = foldl (λ p m → p <|>′ (parse-specific-http-method m)) fail http-methods
+
+
+
+module Parse-URL where
+  record Authority : Type where
+    constructor _꞉_
+    field
+      host : String.String -- TODO: Split out IP:s as a separate type?
+      port : ℕ
+      -- TODO: maybe include {port-in-range} : port < 2 ^ 16
+  open Authority public
+
+  infix 10 _꞉_
+
+  data Path : Type where
+    $ : Path -- end
+    _/_ : String.String → Path → Path
+  open Path public
+
+  instance
+    ShowPath : Show Path
+    ShowPath .showPrec $ _ = "(empty path)"
+    ShowPath .showPrec (p / $) _ = p
+    ShowPath .showPrec (p / rest@(_ / _)) n = p String.++ "/" String.++ showPrec rest n
+
+  infixr 5 _/_
+
+  record URL : Type where
+    constructor http://_/_¿_#_
+    field
+      authority : Authority
+      path : Path
+      query : Maybe String.String
+      fragment : Maybe String.String
+  open URL public
+
+  infix 0 http://_/_¿_#_
+
+  private
+    sample-url : URL
+    sample-url = http:// "coral.shoes" ꞉ 80 / ("pages" / "index.html" / $) ¿ real "key=value" # cake
+
+  -- helper functions
+  private
+
+    decode-utf8⁺ : List⁺ Byte → Maybe String.String
+    decode-utf8⁺ bs = String.fromList <$> UTF-8.decode-string (list⁺-to-list bs)
+
+  -- commonly used sub-parsers
+  private
+    gen-delims sub-delims reserved unreserved : [ Parser Byte ]
+    gen-delims = any-of ":/?#[]@"
+    sub-delims = any-of "!$&'()*+,;="
+    reserved = gen-delims <|>′ sub-delims
+    unreserved = letter <|>′ digit <|>′ any-of "-._~"
+
+    pchar : [ Parser Byte ]
+    pchar = unreserved <|>′ percent-encoded <|>′ sub-delims <|>′ any-of ":@"
+
+  parse-scheme : [ Parser String.String ]
+  parse-scheme = decode-utf8⁺ <$?>′ many (letter <|>′ digit <|>′ any-of "+-.")
+
+  parse-authority : [ Parser Authority ]
+  parse-authority = (λ auth → auth .port <ᵇ 2 ^ 16) <?>′ unchecked
+    where
+      reg-name : [ Parser String.String ]
+      reg-name = decode-utf8⁺ <$?>′ (many (unreserved <|>′ percent-encoded <|>′ sub-delims))
+
+      unchecked : [ Parser Authority ]
+      unchecked = (λ (host , rest) → host ꞉ (proj₂ <$> rest) or-else 80)
+                  <$>′ (reg-name <&?>′ enbox (any-of ":" <&>′ enbox number))
+
+  parse-path : [ Parser Path ]
+  parse-path = foldr (λ (slash , seg) path → seg / path) $ <$>′ (many (any-of "/" <&>′ enbox segment))
+    where
+      segment : [ Parser String.String ]
+      segment = decode-utf8⁺ <$?>′ many pchar
+
+  parse-query parse-fragment : [ Parser String.String ]
+  parse-query = decode-utf8⁺ <$?>′ many (pchar <|>′ any-of "/?")
+  parse-fragment = parse-query
+
+  parse-path-and-query : [ Parser (Path × Maybe String.String) ]
+  parse-path-and-query = parse-path <&?>□ (any-of "?" <&⃗>□ parse-query)
+
+  parse-url : [ Parser URL ]
+  parse-url = enurl <$?>′ parse-parts
+    where
+      enurl : String.String × Authority × (Path × Maybe String.String) × Maybe String.String → Maybe URL
+      enurl (scheme , auth , (path , mquery) , mfrag) =
+        if true -- scheme == "http"
+          then real (http:// auth / path ¿ mquery # mfrag)
+          else cake
+
+      parse-parts : [ Parser (String.String × Authority × (Path × Maybe String.String) × Maybe String.String) ]
+      parse-parts =
+        parse-scheme <&>□
+        (any-of ":" <&>□ repeat 2 (any-of "/")) <&⃗>□
+        parse-authority <&>□
+        (parse-path <&?>□ (any-of "?" <&⃗>□ parse-query))
+          <&?>□ (any-of "#" <&⃗>□ parse-fragment)
+open Parse-URL public
+
+parse-http-version : [ Parser ⊤ ]
+parse-http-version = (λ _ → tt) <$>′ (exact (< 72 > ∷ < 84 > ∷ < 84 > ∷ < 80 > ∷ < 47 > ∷ []) <&>□ many (digit <|>′ any-of "."))
+
+parse-get-request : [ Parser (Path × Maybe String.String) ]
+parse-get-request =
+  parse-specific-http-method GET <&⃗>□
+  spaces <&⃗>□
+  parse-path-and-query <&⃖>□
+  spaces <&>□
+  parse-http-version
+
diff --git a/src/Parse-HTTP/Helpers.agda b/src/Parse-HTTP/Helpers.agda
new file mode 100644
index 0000000..3d3bf77
--- /dev/null
+++ b/src/Parse-HTTP/Helpers.agda
@@ -0,0 +1,71 @@
+open import Agda.Primitive renaming (Set to Type)
+
+open import Data.Nat
+open import Data.Bool hiding (_<_)
+open import Data.Unit
+open import Data.Vec hiding ([_]; foldl)
+import Data.List as List
+
+import Data.String as String
+import Data.Char as Char
+
+open import Base
+
+open import Indexed
+open import NonEmpty
+open import Bits-and-Bytes
+import UTF-8
+
+open import Parsing (Byte)
+
+module Parse-HTTP.Helpers where
+
+-- Bytes are compared against codepoints, meaning any non-ascii Chars will be death
+_is_ : Byte → Char.Char → Bool
+x is c = x .value == Char.toℕ c
+
+_between_and_ : Byte → Char.Char → Char.Char → Bool
+x between a and b = (Char.toℕ a ≤ᵇ x .value) ∧ (x .value ≤ᵇ Char.toℕ b)
+
+any-of : String.String → [ Parser Byte ]
+any-of x = List.foldr (λ ch p → ((_is ch) <?>′ any₁) <|>′ p) fail (String.toList x)
+
+uppercase lowercase letter digit : [ Parser Byte ]
+uppercase = (_between 'A' and 'Z') <?>′ any₁
+lowercase = (_between 'a' and 'z') <?>′ any₁
+digit     = (_between '0' and '9') <?>′ any₁
+letter = uppercase <|>′ lowercase
+
+cr lf crlf : [ Parser ⊤ ]
+cr = (λ _ → tt) <$>′ any-of "\r"
+lf = (λ _ → tt) <$>′ any-of "\n"
+crlf = cr >>′ enbox lf
+
+space spaces : [ Parser ⊤ ]
+space = (λ _ → tt) <$>′ any-of " "
+spaces = (λ _ → tt) <$>′ many space
+
+percent-encoded : [ Parser Byte ]
+percent-encoded = (λ where (a ∷ b ∷ []) → mkClip (a * 16 + b)) <$>′ unencoded-percent-encoding
+  where
+    unhex : Byte → Maybe ℕ -- char to hex digit
+    unhex x =
+      if x between '0' and '9'
+         then real (x .value ∸ (Char.toℕ '0'))
+         else if x between 'a' and 'f'
+           then real (x .value ∸ (Char.toℕ 'a') + 10)
+           else if x between 'A' and 'F'
+             then real (x .value ∸ (Char.toℕ 'A') + 10)
+             else cake
+
+    hex-digit : [ Parser ℕ ]
+    hex-digit = unhex <$?>′ any₁
+
+    unencoded-percent-encoding : [ Parser (Vec ℕ 2) ]
+    unencoded-percent-encoding = exact (bytes.PERCENT ∷ []) >>′ enbox (repeat 2 hex-digit)
+
+digit-ℕ : [ Parser ℕ ]
+digit-ℕ = (λ x → x .value ∸ Char.toℕ '0') <$>′ digit
+
+number : [ Parser ℕ ]
+number = foldl (λ n d → n * 10 + d) 0 <$>′ many digit-ℕ
diff --git a/src/Parse-HTTP/Test.agda b/src/Parse-HTTP/Test.agda
new file mode 100644
index 0000000..35bef46
--- /dev/null
+++ b/src/Parse-HTTP/Test.agda
@@ -0,0 +1,89 @@
+open import Relation.Binary.PropositionalEquality
+open import Data.String
+open import Data.Char
+open import Data.Product
+import Data.List as List
+import Data.Vec as Vec
+
+open import Base
+open import Bits-and-Bytes
+open import Parsing
+open import UTF-8
+
+open import Parse-HTTP
+open import Parse-HTTP.Helpers
+
+module Parse-HTTP.Test where
+
+enc : (s : String) → Vec.Vec Byte (List.length (encode-string (toList s)))
+enc x = Vec.fromList (encode-string (toList x))
+
+module Test-Helpers where
+  test-percent-encoding : percent-encoded .parse (enc "%69abc")
+                        ≡ real ⟨ < 0x69 > , _ , enc "abc" ⟩
+  test-percent-encoding = refl
+
+module Test-HTTP where
+  test-GET : (parse-http-method .parse (enc "GET /mjau.html"))
+                   ≡ real ⟨ GET , _ , enc " /mjau.html" ⟩
+  test-GET = refl
+
+  test-DELETE : parse-http-method .parse (enc "DELETE haters.list")
+               ≡ real ⟨ DELETE , _ , enc " haters.list" ⟩
+  test-DELETE = refl
+
+  test-PUT : parse-http-method .parse (enc "PUT /")
+            ≡ real ⟨ PUT , _ , enc " /" ⟩
+  test-PUT = refl
+
+  test-POST : parse-http-method .parse (enc "POST")
+             ≡ real ⟨ POST , _ , enc "" ⟩
+  test-POST = refl
+
+  test-CONNECT : parse-http-method .parse (enc "CONNECT")
+                ≡ real ⟨ CONNECT , _ , enc "" ⟩
+  test-CONNECT = refl
+
+  test-OPTIONS : parse-http-method .parse (enc "OPTIONS")
+                ≡ real ⟨ OPTIONS , _ , enc "" ⟩
+  test-OPTIONS = refl
+
+  test-TRACE : parse-http-method .parse (enc "TRACE")
+              ≡ real ⟨ TRACE , _ , enc "" ⟩
+  test-TRACE = refl
+
+  test-PATCH : parse-http-method .parse (enc "PATCH")
+              ≡ real ⟨ PATCH , _ , enc "" ⟩
+  test-PATCH = refl
+
+  test-scheme : parse-scheme .parse (enc "http://")
+              ≡ real ⟨ "http" , _ , enc "://" ⟩
+  test-scheme = refl
+
+  test-auth-portless : parse-authority .parse (enc "coral.shoes/mjau.html")
+                     ≡ real ⟨ "coral.shoes" ꞉ 80 , _ , enc "/mjau.html" ⟩
+  test-auth-portless = refl
+
+  test-auth-portful : parse-authority .parse (enc "coral.shoes:80/mjau.html")
+                    ≡ real ⟨ "coral.shoes" ꞉ 80 , _ , enc "/mjau.html" ⟩
+  test-auth-portful = refl
+
+  test-auth-port-out-of-range : parse-authority .parse (enc "coral.shoes:13372137/mjau.html")
+                              ≡ cake
+  test-auth-port-out-of-range = refl
+
+  test-path₁ : parse-path .parse (enc "/mjau/cat.html?meowing=true")
+             ≡ real ⟨ "mjau" / "cat.html" / $ , _ , enc "?meowing=true" ⟩
+  test-path₁ = refl
+
+  test-path₂ : parse-path .parse (enc "/%68%65%77%77%6f/%3f%5e%2f%2f%5e%3f?mjau")
+             ≡ real ⟨ "hewwo" / "?^//^?" / $ , _ , enc "?mjau" ⟩
+  test-path₂ = refl
+
+  test-url : parse-url .parse (enc "http://www.rfc-editor.org/rfc/rfc3986.html#section-2.1")
+           ≡ real ⟨ http:// "www.rfc-editor.org" ꞉ 80 / ("rfc" / "rfc3986.html" / $) ¿ cake # real "section-2.1" , _ , enc "" ⟩
+  test-url = refl
+
+  test-request : parse-get-request .parse (enc "GET /site/index.html?mjau HTTP/1.1\nHeaders...")
+           ≡ real ⟨ ( ( "site" / "index.html" / $ ) , real "mjau" ) , _ , enc "\nHeaders..." ⟩
+  test-request = refl
diff --git a/src/Parsing.agda b/src/Parsing.agda
new file mode 100644
index 0000000..8988df3
--- /dev/null
+++ b/src/Parsing.agda
@@ -0,0 +1,194 @@
+open import Data.Nat renaming (_≡ᵇ_ to _==ⁿ_; _<ᵇ_ to _<ⁿ_)
+open import Data.Nat.Properties using (≤-refl; <-trans; 0<1+n)
+open import Data.Nat.DivMod hiding (result)
+open import Data.Vec hiding ([_]; _>>=_; foldr; foldl) renaming (map to mapᵥ)
+open import Data.List using (List; length) renaming ([] to []ₗ; _∷_ to _∷ₗ_; _++_ to _++ₗ_)
+open import Data.Bool hiding (_<_; _≤_) renaming (_∧_ to _&&_; _∨_ to _||_; T to is-true)
+open import Data.Product hiding (map; map₁; map₂)
+open import Data.Unit using (⊤; tt)
+open import Data.Empty using (⊥)
+
+open import Agda.Primitive renaming (Set to Type)
+
+open import Base
+open import NonEmpty
+open import Indexed
+
+module Parsing (T : Type) ⦃ EqT : Eq T ⦄ where
+
+record Parse (A : Type) (n : ℕ) : Type where
+  constructor ⟨_,_,_⟩
+  field
+    result : A
+    {m} : ℕ
+    m<n : m < n
+    rest : Vec T m
+open Parse public
+
+record Parser (A : Type) (n : ℕ) : Type where
+  field
+    parse : Vec T n → Maybe (Parse A n)
+open Parser public
+
+-- Parser combinators
+_<$>′_ : {A B : Type} → (A → B) → [ Parser A →′ Parser B ]
+(f <$>′ p) .parse a = do
+  ⟨ x , m<n , rest ⟩ ← p .parse a
+  pure ⟨ f x , m<n , rest ⟩
+
+_<$?>′_ : {A B : Type} → (A → Maybe B) → [ Parser A →′ Parser B ]
+(f <$?>′ p) .parse a = do
+  ⟨ x , m<n , rest ⟩ ← p .parse a
+  y ← f x
+  pure ⟨ y , m<n , rest ⟩
+
+_<?>′_ : {A : Type} → (A → Bool) → [ Parser A →′ Parser A ]
+pred <?>′ p = (λ a → if pred a then real a else cake) <$?>′ p
+
+_<|>′_ : {A : Type} → [ Parser A →′ Parser A →′ Parser A ]
+(p₀ <|>′ p₁) .parse a = case p₀ .parse a of λ where
+  (real x) → real x
+  cake → p₁ .parse a
+
+infixr 20 _<|>′_
+
+_<&>′_ : {A B : Type} → [ Parser A →′ □ (Parser B) →′ Parser (A × B) ]
+(p₀ <&>′ p₁) .parse a = do
+  ⟨ x₀ , m<i , rest ⟩ ← p₀ .parse a
+  ⟨ x₁ , n<m , rest ⟩ ← (p₁ .call m<i) .parse rest
+  pure ⟨ (x₀ , x₁) , <-trans n<m m<i , rest ⟩
+
+_<&⃖>′_ : {A B : Type} → [ Parser A →′ □ (Parser B) →′ Parser A ]
+(p₀ <&⃖>′ p₁) .parse a = do
+  ⟨ x₀ , m<i , rest ⟩ ← p₀ .parse a
+  ⟨ _ , n<m , rest ⟩ ← (p₁ .call m<i) .parse rest
+  pure ⟨ x₀ , <-trans n<m m<i , rest ⟩
+
+_<&⃗>′_ : {A B : Type} → [ Parser A →′ □ (Parser B) →′ Parser B ]
+(p₀ <&⃗>′ p₁) .parse a = do
+  ⟨ _ , m<i , rest ⟩ ← p₀ .parse a
+  ⟨ x₁ , n<m , rest ⟩ ← (p₁ .call m<i) .parse rest
+  pure ⟨ x₁ , <-trans n<m m<i , rest ⟩
+
+_<&?>′_ : {A B : Type} → [ Parser A →′ □ (Parser B) →′ Parser (A × Maybe B) ]
+(p₀ <&?>′ p₁) .parse a = do
+  ⟨ x₀ , m<i , rest ⟩ ← p₀ .parse a
+  case (p₁ .call m<i) .parse rest of λ where
+    (real ⟨ x₁ , n<m , rest ⟩) → pure ⟨ (x₀ , real x₁) , <-trans n<m m<i , rest ⟩
+    cake → pure ⟨ (x₀ , cake) , m<i , rest ⟩
+
+_<&>□_ : {A B : Type} → [ Parser A ] → [ Parser B ] → [ Parser (A × B) ]
+p₀ <&>□ p₁ = p₀ <&>′ enbox p₁
+
+_<&⃖>□_ : {A B : Type} → [ Parser A ] → [ Parser B ] → [ Parser A ]
+p₀ <&⃖>□ p₁ = p₀ <&⃖>′ enbox p₁
+
+_<&⃗>□_ : {A B : Type} → [ Parser A ] → [ Parser B ] → [ Parser B ]
+p₀ <&⃗>□ p₁ = p₀ <&⃗>′ enbox p₁
+
+_<&?>□_ : {A B : Type} → [ Parser A ] → [ Parser B ] → [ Parser (A × Maybe B) ]
+p₀ <&?>□ p₁ = p₀ <&?>′ enbox p₁
+
+infix 20 _<&>′_
+infix 20 _<&⃗>′_
+infix 20 _<&⃖>′_
+infix 20 _<&?>′_
+
+infixr 20 _<&>□_
+infixr 20 _<&⃗>□_
+infixr 20 _<&⃖>□_
+infixr 20 _<&?>□_
+
+many-fix : {A : Type} → [ Parser A ] → [ Parser (List⁺ A) ]
+many-fix p = fix λ x → ((λ (a , b) → a ∷⁺ b) <$>′ (p <&>′ x))
+                       <|>′ ([_]⁺ <$>′ p)
+
+-- many has the exact same definition as many-fix
+-- as many-fix is terminating, this must be as well
+-- :3
+{-# TERMINATING #-}
+many-recursing : {A : Type} → [ Parser A ] → [ Parser (List⁺ A) ]
+many-recursing p = ((λ (a , b) → a ∷⁺ b) <$>′ (p <&>′ enbox (many-recursing p)))
+                   <|>′ ([_]⁺ <$>′ p)
+
+many : {A : Type} → [ Parser A ] → [ Parser (List⁺ A) ]
+many = many-recursing
+
+upto : {A : Type} → (n : ℕ) → {is-true (0 <ⁿ n)} → [ Parser A ] → [ Parser (List⁺ A) ]
+upto {A} (suc pn) p = go pn
+  where
+    go : ℕ → [ Parser (List⁺ A) ]
+    go 0 = [_]⁺ <$>′ p
+    go n@(suc pn) =
+       ((λ (x , xs) → x ∷⁺ xs) <$>′ (p <&>′ enbox upto-pn))
+       <|>′ upto-pn
+      where
+        upto-pn : [ Parser (List⁺ A) ]
+        upto-pn = go pn
+
+_>>=′_ : {A B : Type} → [ Parser A →′ ((k′ A) →′ □ Parser B) →′ Parser B ]
+(pa >>=′ f) .parse inp = do
+  ⟨ a , lt , inp′ ⟩ ← pa .parse inp
+  let pb = f a
+  ⟨ b , lt′ , inp′′ ⟩ ← (pb .call lt) .parse inp′
+  pure ⟨ b , <-trans lt′ lt , inp′′ ⟩
+
+_>>′_ : {A B : Type} → [ Parser A →′ □ Parser B →′ Parser B ]
+pa >>′ pb = pa >>=′ λ _ → pb
+
+fail : {A : Type} → [ Parser A ]
+fail .parse _ = cake
+
+-- simple parsers
+
+any₁ : [ Parser T ]
+any₁ .parse [] = cake
+any₁ .parse (x ∷ xs) = real ⟨ x , ≤-refl , xs ⟩
+
+repeat : {A : Type} → (n : ℕ) → .{nonempty : is-true (0 <ⁿ n)} → [ Parser A ] → [ Parser (Vec A n) ]
+repeat 1 p = (λ x → x ∷ []) <$>′ p
+repeat n@(suc pn@(suc _)) p =
+  p >>=′ λ x →
+  enbox ((λ xs → x ∷ xs) <$>′ repeat pn p)
+
+exact : {n : ℕ} → Vec T (suc n) → [ Parser ⊤ ]
+exact {n} x = go x
+  where
+    check : T → T → Maybe ⊤
+    check x y = if x == y then real tt else cake
+
+    go : {n : ℕ} → .{is-true (0 <ⁿ n)} → Vec T n → [ Parser ⊤ ]
+    go (x ∷ []) = check x <$?>′ any₁
+    go {n@(suc pn)} (x ∷ xs@(_ ∷ _)) =
+      (check x <$?>′ any₁) >>=′ λ _ → enbox (go xs)
+
+{-
+module parse-example where
+  open import Data.String
+  open import Data.Char renaming (_==_ to _==ᶜ_)
+
+  open parse (Char) (_==ᶜ_)
+
+  parse-digit : [ Parser ℕ ]
+  parse-digit = (decode-char <$?> any₁)
+    where
+      decode-char : Char → Maybe ℕ
+      decode-char '0' = real 0
+      decode-char '1' = real 1
+      decode-char '2' = real 2
+      decode-char '3' = real 3
+      decode-char '4' = real 4
+      decode-char '5' = real 5
+      decode-char '6' = real 6
+      decode-char '7' = real 7
+      decode-char '8' = real 8
+      decode-char '9' = real 9
+      decode-char _ = cake
+
+  parse-ℕ : [ Parser ℕ ]
+  parse-ℕ = foldl (λ n d → n * 10 + d) 0 <$> some parse-digit
+
+  sample : parse-ℕ .parse (toVec "123xy")
+         ≡ real ⟨ 123 , _ , toVec "xy" ⟩
+  sample = refl
+-}
diff --git a/src/Socket.agda b/src/Socket.agda
new file mode 100644
index 0000000..9627190
--- /dev/null
+++ b/src/Socket.agda
@@ -0,0 +1,154 @@
+{-# OPTIONS --guardedness --postfix-projections #-}
+module Socket where
+
+open import Agda.Primitive renaming (Set to Type)
+
+open import Data.Product hiding (map)
+open import Data.Nat
+open import Data.String
+open import Data.List
+open import Data.Unit
+
+open import Base
+open import SysIO
+open import Bits-and-Bytes
+
+module SocketForeign where
+  {-# FOREIGN GHC
+    import qualified Data.Word as Word
+    import qualified Data.Functor as Funct
+    import qualified Control.Monad as Monad
+    import qualified Data.Text as T
+    import qualified System.IO as SIO
+    import qualified Control.Concurrent.STM as STM
+    import qualified Control.Concurrent.STM.TVar as TVar
+
+    import qualified Data.ByteString as BS
+
+    import System.IO.Unsafe as Unsafe
+
+    import qualified Network.Socket as Socket
+    import qualified Network.Socket.ByteString as SocketBS
+    import qualified Network.Run.TCP as RunTCP
+  #-}
+
+  -- Data.Product doesn't do any FFI, and we can't define the FFI outside the module,
+  -- so we define our own product type
+  data Tuple2 (A B : Type) : Type where
+    mkTuple2 : A → B → Tuple2 A B
+
+  {-# FOREIGN GHC data Tuple2 a b = MKTuple2 a b #-}
+  {-# COMPILE GHC Tuple2 = data Tuple2 (MKTuple2) #-}
+
+  postulate
+    RawSocket : Type
+    raw-uncons : RawSocket → Maybe (Tuple2 Word8 RawSocket)
+
+    run-raw-server : String → ℕ → (RawSocket → IO (List Word8)) → IO ⊤
+
+  {-# FOREIGN GHC
+    innerSockSize :: Int
+    innerSockSize = 1 -- TODO: Increase
+
+    debug :: Bool
+    debug = False
+
+    info :: Bool
+    info = False
+
+    gray :: String
+    gray = "\x1b[38;5;8m"
+
+    blue :: String
+    blue = "\x1b[38;5;4m"
+
+    reset :: String
+    reset = "\x1b[0m"
+
+    printDebug :: String -> String -> IO ()
+    printDebug f x = Monad.when debug (SIO.putStrLn $ gray ++ "  [" ++ f ++ "] " ++ x ++ reset)
+
+    printInfo :: String -> String -> IO ()
+    printInfo f x = Monad.when info (SIO.putStrLn $ blue ++ "  [" ++ f ++ "] " ++ x ++ reset)
+
+    data BufferedSocket = BufferedSocket
+      { getSocket :: Socket.Socket
+      , getBuffer :: TVar.TVar BS.ByteString
+      , getOffset :: Int
+      }
+
+    mkBuff :: Socket.Socket -> IO BufferedSocket
+    mkBuff s = do
+      buf <- TVar.newTVarIO BS.empty
+      pure BufferedSocket
+        { getSocket = s
+        , getBuffer = buf
+        , getOffset = 0
+        }
+
+    fillBuffer :: BufferedSocket -> IO ()
+    fillBuffer s = do
+      remaining <- (TVar.readTVarIO $ getBuffer s) >>= (\buf -> pure $ innerSockSize - (BS.length buf) + getOffset s)
+      printDebug "fillBuffer" $ "remaining = " ++ show remaining
+      if remaining <= 0
+        then pure ()
+        else do
+          printDebug "fillBuffer" $ "Reading " ++ show remaining ++ " bytes"
+          got <- SocketBS.recv (getSocket s) remaining
+          printInfo "fillBuffer" $ "got: " ++ show got
+          STM.atomically $ TVar.modifyTVar (getBuffer s) (flip BS.append got)
+
+    unconsIO :: BufferedSocket -> IO (Maybe (Word.Word8, BufferedSocket))
+    unconsIO s = do
+      buf <- TVar.readTVarIO $ getBuffer s
+      printDebug "unconsIO" $ "buffer = " ++ show buf ++ ", offset = " ++ show (getOffset s)
+      let next = s { getOffset = 1 + getOffset s }
+      let offset = getOffset s
+      if offset < BS.length buf
+        then pure $ pure (BS.index buf offset, next)
+        else do
+          printDebug "unconsIO" $ "filling buffer"
+          fillBuffer s
+          buf <- TVar.readTVarIO $ getBuffer s
+          printDebug "unconsIO" $ "after: buffer = " ++ show buf ++ ", offset = " ++ show (getOffset s)
+          if offset < BS.length buf
+            then pure $ pure (BS.index buf offset, next)
+            else pure Nothing
+  #-}
+
+  {-# COMPILE GHC RawSocket = type BufferedSocket #-}
+  {-# COMPILE GHC raw-uncons = \s -> (\(x, y) -> MKTuple2 x y) Funct.<$> Unsafe.unsafePerformIO (unconsIO s) #-}
+
+  {-# COMPILE GHC run-raw-server =
+      \ hostname port runFn ->
+        RunTCP.runTCPServer
+          (Just (T.unpack hostname))
+          (show port)
+          (\socket -> do
+            sock <- mkBuff socket ;
+            dat <- (BS.singleton <$>) <$> runFn sock ;
+            Monad.forM_ dat (\b -> printInfo "run-raw-server" ("sending " ++ show b) >> SocketBS.sendAll socket b)
+          )
+  #-}
+open SocketForeign using (RawSocket; raw-uncons; run-raw-server)
+
+record Socket : Type where
+  coinductive
+  field
+    split : Maybe (Byte × Socket)
+open Socket public
+
+module SocketTrans where
+  unraw : RawSocket → Socket
+  unraw raw-sock .split with raw-uncons raw-sock
+  ...                   | real ( SocketForeign.mkTuple2 w rest ) = real ( Word8-to-Byte w , unraw rest)
+  ...                   | cake = cake
+
+run-server : String → ℕ → (Socket → IO (List Byte)) → IO ⊤
+run-server hostname port f = run-raw-server hostname port (λ rs → map Byte-to-Word8 <$> (f (SocketTrans.unraw rs)))
+
+{-# TERMINATING #-} -- hopefully the user hangs up at some point :)
+get-bytes : Socket → List Byte
+get-bytes sock with sock .split
+...            | real (ch , sock′) = ch ∷ get-bytes sock′
+...            | cake = []
diff --git a/src/SysIO.agda b/src/SysIO.agda
new file mode 100644
index 0000000..de493d4
--- /dev/null
+++ b/src/SysIO.agda
@@ -0,0 +1,41 @@
+module SysIO where
+
+open import Agda.Primitive renaming (Set to Type)
+
+open import Data.String using (String; _++_)
+open import Data.Unit using (⊤; tt)
+
+open import Base
+open import Bits-and-Bytes
+
+module IOForeign where
+  postulate
+    IO : Type → Type
+    io-pure : {A : Type} → A → IO A
+    io-bind : {A B : Type} → IO A → (A → IO B) → IO B
+
+    putStr : String → IO ⊤
+
+  {-# BUILTIN IO IO #-}
+  {-# FOREIGN GHC
+    import qualified Control.Monad as Monad
+    import qualified Control.Applicative as Applicative
+
+    import qualified System.IO as SIO
+    import qualified Data.Text as T
+    import qualified Data.Text.IO as TIO
+  #-}
+  {-# COMPILE GHC IO = type IO #-}
+  {-# COMPILE GHC io-pure = \ty a -> Applicative.pure a #-}
+  {-# COMPILE GHC io-bind = \tya tyb a f -> (Monad.>>=) a f #-}
+  {-# COMPILE GHC putStr = TIO.putStr #-}
+
+open IOForeign using (IO; putStr) public
+
+instance
+  MonadIO : Monad IO
+  MonadIO .pure = IOForeign.io-pure
+  MonadIO ._>>=_ = IOForeign.io-bind
+
+putStrLn : String → IO ⊤
+putStrLn x = putStr (x ++ "\n")
diff --git a/src/UTF-8.agda b/src/UTF-8.agda
new file mode 100644
index 0000000..3b97f07
--- /dev/null
+++ b/src/UTF-8.agda
@@ -0,0 +1,159 @@
+{-# OPTIONS --postfix-projections #-}
+module UTF-8 where
+
+open import Agda.Primitive renaming (Set to Type)
+
+open import Data.Product
+open import Data.Unit using (⊤; tt)
+open import Data.Empty
+open import Data.Vec hiding ([_])
+open import Data.List using (List) renaming (_∷_ to _∷ˡ_; [] to []ˡ; _++_ to _++ˡ_)
+open import Data.Bool using (Bool; true; false; T)
+open import Data.Nat
+open import Relation.Binary.PropositionalEquality hiding ([_])
+open import Relation.Nullary
+
+open import Base
+open import NonEmpty
+open import Bits-and-Bytes
+
+import Data.Char as C
+open import Data.Nat.Properties using (<-trans; <ᵇ⇒<; ≤-refl; m≤n+m)
+
+postulate
+  char-toℕ-in-range : (c : C.Char) → C.toℕ c < 0x110000
+
+encode-char : C.Char → List Byte
+encode-char ch = case x <? 0x80 of λ where
+    (yes x<0x80) → encode-1 x x<0x80
+    (no _) → case x <? 0x800 of λ where
+      (yes x<0x800) → encode-2 x x<0x800
+      (no _) → case x <? 0x10000 of λ where
+        (yes x<0x10000) → encode-3 x x<0x10000
+        (no _) → encode-4 x x<0x110000
+  where
+    x : ℕ
+    x = C.toℕ ch
+
+    x<0x110000 : x < 0x110000
+    x<0x110000 = char-toℕ-in-range ch
+
+    encode-1 : (n : ℕ) → n < 0x80 → List Byte
+    encode-1 n n<0x80 = case enbits {7} n n<0x80 of λ where
+      (b0 ∷ b1 ∷ b2 ∷ b3 ∷ b4 ∷ b5 ∷ b6 ∷ []) →
+        Bit8-to-Byte (b0 ∷ b1 ∷ b2 ∷ b3 ∷ b4 ∷ b5 ∷ b6 ∷ 𝟘 ∷ []) ∷ˡ
+        []ˡ
+
+    encode-2 : (n : ℕ) → n < 0x800 → List Byte
+    encode-2 n n<0x800 = case enbits {11} n n<0x800 of λ where
+      (b0 ∷ b1 ∷ b2 ∷ b3 ∷ b4 ∷ b5 ∷ b6 ∷ b7 ∷ b8 ∷ b9 ∷ b10 ∷ []) →
+        Bit8-to-Byte (b6 ∷ b7 ∷ b8 ∷ b9 ∷ b10 ∷ 𝟘  ∷ 𝟙 ∷ 𝟙 ∷ []) ∷ˡ
+        Bit8-to-Byte (b0 ∷ b1 ∷ b2 ∷ b3 ∷ b4  ∷ b5 ∷ 𝟘 ∷ 𝟙 ∷ []) ∷ˡ
+        []ˡ
+
+    encode-3 : (n : ℕ) → n < 0x10000 → List Byte
+    encode-3 n n<0x10000 = case enbits {16} n n<0x10000 of λ where
+      (b0 ∷ b1 ∷ b2 ∷ b3 ∷ b4 ∷ b5 ∷ b6 ∷ b7 ∷ b8 ∷ b9 ∷ b10 ∷ b11 ∷ b12 ∷ b13 ∷ b14 ∷ b15 ∷ []) →
+        Bit8-to-Byte (b12 ∷ b13 ∷ b14 ∷ b15 ∷ 𝟘   ∷ 𝟙   ∷ 𝟙 ∷ 𝟙 ∷ []) ∷ˡ
+        Bit8-to-Byte (b6  ∷ b7  ∷ b8  ∷ b9  ∷ b10 ∷ b11 ∷ 𝟘 ∷ 𝟙 ∷ []) ∷ˡ
+        Bit8-to-Byte (b0  ∷ b1  ∷ b2  ∷ b3  ∷ b4  ∷ b5  ∷ 𝟘 ∷ 𝟙 ∷ []) ∷ˡ
+        []ˡ
+
+    encode-4 : (n : ℕ) → n < 0x110000 → List Byte
+    encode-4 n n<0x110000 = case enbits {21} n (<-trans n<0x110000 (<ᵇ⇒< 0x110000 (2 ^ 21) tt)) of λ where
+      (b0  ∷ b1  ∷ b2  ∷ b3  ∷ b4  ∷ b5 ∷ b6 ∷ b7 ∷ b8 ∷ b9 ∷ b10 ∷ b11 ∷ b12 ∷ b13 ∷ b14 ∷ b15 ∷
+       b16 ∷ b17 ∷ b18 ∷ b19 ∷ b20 ∷ []) →
+        Bit8-to-Byte (b18 ∷ b19 ∷ b20 ∷ 𝟘   ∷ 𝟙   ∷ 𝟙   ∷ 𝟙 ∷ 𝟙 ∷ []) ∷ˡ
+        Bit8-to-Byte (b12 ∷ b13 ∷ b14 ∷ b15 ∷ b16 ∷ b17 ∷ 𝟘 ∷ 𝟙 ∷ []) ∷ˡ
+        Bit8-to-Byte (b6  ∷ b7  ∷ b8  ∷ b9  ∷ b10 ∷ b11 ∷ 𝟘 ∷ 𝟙 ∷ []) ∷ˡ
+        Bit8-to-Byte (b0  ∷ b1  ∷ b2  ∷ b3  ∷ b4  ∷ b5  ∷ 𝟘 ∷ 𝟙 ∷ []) ∷ˡ
+        []ˡ
+
+encode-string : List C.Char → List Byte
+encode-string []ˡ = []ˡ
+encode-string (c ∷ˡ cs) = encode-char c ++ˡ encode-string cs
+
+module decode where
+  open import Indexed using ([_]; _→′_; □_; fix)
+  open import Parsing (Byte)
+  import Data.Fin as F
+
+  decode-≤-1 : {m : ℕ} → Vec Byte (1 + m) → Maybe (Parse C.Char (1 + m))
+  decode-≤-1 (x ∷ xs) with Byte-to-Bit8 x
+  ...                 | (b0 ∷ b1 ∷ b2 ∷ b3 ∷ b4 ∷ b5 ∷ b6 ∷ 𝟘 ∷ [])
+                        = real
+                          ⟨ C.fromℕ (proj₁ (unbits {7} (b0 ∷ b1 ∷ b2 ∷ b3 ∷ b4 ∷ b5 ∷ b6 ∷ [])))
+                          , ≤-refl
+                          , xs ⟩
+  ...                 | _ = cake
+
+  decode-≤-2 : {m : ℕ} → Vec Byte (2 + m) → Maybe (Parse C.Char (2 + m))
+  decode-≤-2 {m} x@(x₁ ∷ x₂ ∷ xs) with Byte-to-Bit8 x₁ ,′ Byte-to-Bit8 x₂
+  ...                 | (b6 ∷ b7 ∷ b8 ∷ b9 ∷ b10 ∷ 𝟘  ∷ 𝟙 ∷ 𝟙 ∷ [])
+                      , (b0 ∷ b1 ∷ b2 ∷ b3 ∷ b4  ∷ b5 ∷ 𝟘 ∷ 𝟙 ∷ [])
+                        = real
+                          ⟨ C.fromℕ (proj₁ (unbits {11}
+                            ( b0 ∷ b1 ∷ b2  ∷ b3 ∷ b4 ∷ b5 ∷ b6 ∷ b7
+                            ∷ b8 ∷ b9 ∷ b10 ∷ []
+                            )))
+                          , m≤n+m (suc m) 1
+                          , xs ⟩
+  ...                 | _ = cake
+
+  decode-≤-3 : {m : ℕ} → Vec Byte (3 + m) → Maybe (Parse C.Char (3 + m))
+  decode-≤-3 {m} x@(x₁ ∷ x₂ ∷ x₃ ∷ xs) with Byte-to-Bit8 x₁ ,′ Byte-to-Bit8 x₂ ,′ Byte-to-Bit8 x₃
+  ...                 | (b12 ∷ b13 ∷ b14 ∷ b15 ∷ 𝟘   ∷ 𝟙   ∷ 𝟙 ∷ 𝟙 ∷ [])
+                      , (b6  ∷ b7  ∷ b8  ∷ b9  ∷ b10 ∷ b11 ∷ 𝟘 ∷ 𝟙 ∷ [])
+                      , (b0  ∷ b1  ∷ b2  ∷ b3  ∷ b4  ∷ b5  ∷ 𝟘 ∷ 𝟙 ∷ [])
+                        = real
+                          ⟨ C.fromℕ (proj₁ (unbits {16}
+                            ( b0 ∷ b1 ∷ b2  ∷ b3  ∷ b4  ∷ b5  ∷ b6  ∷ b7
+                            ∷ b8 ∷ b9 ∷ b10 ∷ b11 ∷ b12 ∷ b13 ∷ b14 ∷ b15 ∷ []
+                            )))
+                          , m≤n+m (suc m) 2
+                          , xs ⟩
+  ...                 | _ = cake
+
+  decode-≤-4 : {m : ℕ} → Vec Byte (4 + m) → Maybe (Parse C.Char (4 + m))
+  decode-≤-4 {m} x@(x₁ ∷ x₂ ∷ x₃ ∷ x₄ ∷ xs) with Byte-to-Bit8 x₁ ,′ Byte-to-Bit8 x₂ ,′ Byte-to-Bit8 x₃ ,′ Byte-to-Bit8 x₄
+  ...                 | (b18 ∷ b19 ∷ b20 ∷ 𝟘   ∷ 𝟙   ∷ 𝟙   ∷ 𝟙 ∷ 𝟙 ∷ [])
+                      , (b12 ∷ b13 ∷ b14 ∷ b15 ∷ b16 ∷ b17 ∷ 𝟘 ∷ 𝟙 ∷ [])
+                      , (b6  ∷ b7  ∷ b8  ∷ b9  ∷ b10 ∷ b11 ∷ 𝟘 ∷ 𝟙 ∷ [])
+                      , (b0  ∷ b1  ∷ b2  ∷ b3  ∷ b4  ∷ b5  ∷ 𝟘 ∷ 𝟙 ∷ [])
+                        = real
+                          ⟨ C.fromℕ (proj₁ (unbits {21}
+                            ( b0  ∷ b1  ∷ b2  ∷ b3  ∷ b4  ∷ b5  ∷ b6  ∷ b7
+                            ∷ b8  ∷ b9  ∷ b10 ∷ b11 ∷ b12 ∷ b13 ∷ b14 ∷ b15
+                            ∷ b16 ∷ b17 ∷ b18 ∷ b19 ∷ b20 ∷ []
+                            )))
+                          , m≤n+m (suc m) 3
+                          , xs ⟩
+  ...                 | _ = cake
+
+  parse-char : [ Parser C.Char ]
+  parse-char {n} .parse [] = cake
+  parse-char {n} .parse xs@(_ ∷ _) = case decode-≤-1 xs of λ where
+    (real x) → real x
+    cake → case xs of λ where
+      (_ ∷ []) → cake
+      (_ ∷ _ ∷ _) → case decode-≤-2 xs of λ where
+        (real x) → real x
+        cake → case xs of λ where
+          (_ ∷ _ ∷ []) → cake
+          (_ ∷ _ ∷ _ ∷ _) → case decode-≤-3 xs of λ where
+            (real x) → real x
+            cake → case xs of λ where
+              (_ ∷ _ ∷ _ ∷ []) → cake
+              (_ ∷ _ ∷ _ ∷ _ ∷ _) → decode-≤-4 xs
+
+  parse-string : [ Parser (List⁺ C.Char) ]
+  parse-string = many-fix parse-char
+
+  decode-string : List Byte → Maybe (List C.Char)
+  decode-string []ˡ = real []ˡ
+  decode-string xs@(_ ∷ˡ _) with parse-string .parse (fromList xs)
+  ...                      | real ⟨ r , _ , [] ⟩ = real (list⁺-to-list r)
+  ...                      | _ = cake
+
+open decode using (decode-string; parse-string; parse-char) public
+
diff --git a/src/UTF-8/Test.agda b/src/UTF-8/Test.agda
new file mode 100644
index 0000000..84aa4f0
--- /dev/null
+++ b/src/UTF-8/Test.agda
@@ -0,0 +1,50 @@
+open import Relation.Binary.PropositionalEquality
+open import Data.List using (List) renaming (_∷_ to _∷ˡ_; [] to []ˡ; _++_ to _++ˡ_)
+open import Data.Nat.Properties using (<ᵇ⇒<)
+open import Data.Vec
+open import Data.Product
+
+import Data.String as S
+
+open import Base
+open import UTF-8
+open import Bits-and-Bytes
+
+module UTF-8.Test where
+
+en-ex4 : enbits 0x5 (<ᵇ⇒< _ _ _) ≡ 𝟙 ∷ 𝟘 ∷ 𝟙 ∷ 𝟘 ∷ []
+en-ex4 = refl
+en-ex8 : enbits 0x69 (<ᵇ⇒< _ _ _) ≡ 𝟙 ∷ 𝟘 ∷ 𝟘 ∷ 𝟙 ∷ 𝟘 ∷ 𝟙 ∷ 𝟙 ∷ 𝟘 ∷ []
+en-ex8 = refl
+un-ex4 : unbits (𝟙 ∷ 𝟘 ∷ 𝟙 ∷ 𝟘 ∷ []) ≡ (0x5 , _)
+un-ex4 = refl
+un-ex8 : unbits (𝟙 ∷ 𝟘 ∷ 𝟘 ∷ 𝟙 ∷ 𝟘 ∷ 𝟙 ∷ 𝟙 ∷ 𝟘 ∷ []) ≡ (0x69 , _)
+un-ex8 = refl
+bb8-ex : Byte-to-Bit8 (< 0x69 >) ≡ 𝟙 ∷ 𝟘 ∷ 𝟘 ∷ 𝟙 ∷ 𝟘 ∷ 𝟙 ∷ 𝟙 ∷ 𝟘 ∷ []
+bb8-ex = refl
+b8b-ex : Bit8-to-Byte (𝟙 ∷ 𝟘 ∷ 𝟘 ∷ 𝟙 ∷ 𝟘 ∷ 𝟙 ∷ 𝟙 ∷ 𝟘 ∷ []) ≡ < 0x69 >
+b8b-ex = refl
+
+encode-a : encode-char 'a' ≡ < 97 > ∷ˡ []ˡ
+encode-a = refl
+encode-ö : encode-char 'ö' ≡ < 0xc3 > ∷ˡ < 0xb6 > ∷ˡ []ˡ
+encode-ö = refl
+encode-∘ : encode-char '∘' ≡ < 0xe2 > ∷ˡ < 0x88 > ∷ˡ < 0x98 > ∷ˡ []ˡ
+encode-∘ = refl
+encode-𐄣 : encode-char '𐄣' ≡ < 0xf0 > ∷ˡ < 0x90 > ∷ˡ < 0x84 > ∷ˡ < 0xa3 > ∷ˡ []ˡ
+encode-𐄣 = refl
+encode-blah : encode-string (S.toList "aö∘𐄣")
+            ≡ < 0x61 >
+            ∷ˡ < 0xc3 > ∷ˡ < 0xb6 >
+            ∷ˡ < 0xe2 > ∷ˡ < 0x88 > ∷ˡ < 0x98 >
+            ∷ˡ < 0xf0 > ∷ˡ < 0x90 > ∷ˡ < 0x84 > ∷ˡ < 0xa3 >
+            ∷ˡ []ˡ
+encode-blah = refl
+decode-blah : decode-string
+            ( < 0x61 >
+            ∷ˡ < 0xc3 > ∷ˡ < 0xb6 >
+            ∷ˡ < 0xe2 > ∷ˡ < 0x88 > ∷ˡ < 0x98 >
+            ∷ˡ < 0xf0 > ∷ˡ < 0x90 > ∷ˡ < 0x84 > ∷ˡ < 0xa3 >
+            ∷ˡ []ˡ )
+            ≡ real (S.toList "aö∘𐄣")
+decode-blah = refl
diff --git a/src/henttp.agda-lib b/src/henttp.agda-lib
new file mode 100644
index 0000000..35cfb52
--- /dev/null
+++ b/src/henttp.agda-lib
@@ -0,0 +1,3 @@
+name: henttp
+include: .
+depend: standard-library