xenia/henttp
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

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

Browse Source
This commit is contained in:
xenia 2023-09-03 00:05:29 +02:00
commit 989197d488
17 changed files with 1549 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
.gitignore vendored Normal file
View File

@ -0,0 +1,3 @@
**/artifacts
**/result
**/*.agdai

61
flake.lock Normal file
View File

@ -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
}

65
flake.nix Normal file
View File

@ -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;
};
}
);
}

95
src/Base.agda Normal file
View File

@ -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

143
src/Bits-and-Bytes.agda Normal file
View File

@ -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

144
src/Indexed.agda Normal file
View File

@ -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

62
src/Main.agda Normal file
View File

@ -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

30
src/NonEmpty.agda Normal file
View File

@ -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

185
src/Parse-HTTP.agda Normal file
View File

@ -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

71
src/Parse-HTTP/Helpers.agda Normal file
View File

@ -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-ℕ

89
src/Parse-HTTP/Test.agda Normal file
View File

@ -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

194
src/Parsing.agda Normal file
View File

@ -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
-}

154
src/Socket.agda Normal file
View File

@ -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 = []

41
src/SysIO.agda Normal file
View File

@ -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")

159
src/UTF-8.agda Normal file
View File

@ -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

50
src/UTF-8/Test.agda Normal file
View File

@ -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

3
src/henttp.agda-lib Normal file
View File

@ -0,0 +1,3 @@
name: henttp
include: .
depend: standard-library