Compare commits
5 Commits
989197d488
...
2caca85e6f
Author | SHA1 | Date | |
---|---|---|---|
2caca85e6f | |||
ab1d2306d9 | |||
d2bd03a17e | |||
3216656638 | |||
5103fc0996 |
|
@ -22,6 +22,9 @@
|
|||
mkdir -p ./artifacts
|
||||
${agda}/bin/agda --compile-dir ./artifacts --compile "''${1:-./Main.agda}"
|
||||
}
|
||||
clean() {
|
||||
fd -I '.agdai|artifacts' --exec rm -rf
|
||||
}
|
||||
'';
|
||||
|
||||
henttp = pkgs.stdenv.mkDerivation {
|
||||
|
@ -56,7 +59,9 @@
|
|||
henttp = henttp;
|
||||
default = henttp;
|
||||
};
|
||||
devShell = pkgs.mkShell { packages = buildInputs; shellHook = common; };
|
||||
devShells = {
|
||||
default = pkgs.mkShell { packages = buildInputs; shellHook = common; };
|
||||
};
|
||||
checks = {
|
||||
default = check-all;
|
||||
};
|
||||
|
|
|
@ -38,6 +38,8 @@ _or-else_ : {A : Type} → Maybe A → A → A
|
|||
(real x) or-else _ = x
|
||||
cake or-else x = x
|
||||
|
||||
infix 10 _or-else_
|
||||
|
||||
is-real : {A : Type} → Maybe A → Type
|
||||
is-real cake = ⊥
|
||||
is-real (real x) = ⊤
|
||||
|
@ -72,24 +74,23 @@ instance
|
|||
|
||||
record Show (T : Type) : Type₁ where
|
||||
field
|
||||
showPrec : T → ℕ → String.String
|
||||
show : T → String.String
|
||||
show x = showPrec x 0
|
||||
show : T → String.String
|
||||
|
||||
open Show ⦃...⦄ public
|
||||
|
||||
instance
|
||||
open import Data.Nat.Show using () renaming (show to show-ℕ)
|
||||
ShowNat : Show ℕ
|
||||
ShowNat .showPrec x _ = show-ℕ x
|
||||
ShowNat .show x = show-ℕ x
|
||||
|
||||
ShowString : Show String.String
|
||||
ShowString .showPrec x _ = String.show x
|
||||
ShowString .show x = String.show x
|
||||
|
||||
ShowList : {A : Type} → ⦃ Show A ⦄ → Show (List A)
|
||||
ShowList {A} .showPrec x _ = "[" String.++ go x String.++ "]"
|
||||
ShowList {A} .show 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
|
||||
go (x ∷ []) = show x
|
||||
go (x ∷ xs) = show x String.++ ", " String.++ go xs
|
||||
|
||||
|
|
|
@ -38,7 +38,7 @@ instance
|
|||
EqByte ._==_ a b = a .value == b .value
|
||||
|
||||
ShowByte : Show Byte
|
||||
ShowByte .showPrec x _ = "< " String.++ showPrec (x .value) 1 String.++ " >"
|
||||
ShowByte .show x = "< " String.++ show (x .value) String.++ " >"
|
||||
where
|
||||
import Data.String as String
|
||||
|
||||
|
|
151
src/HTML.agda
Normal file
151
src/HTML.agda
Normal file
|
@ -0,0 +1,151 @@
|
|||
open import Agda.Primitive renaming (Set to Type)
|
||||
|
||||
open import Relation.Binary.PropositionalEquality
|
||||
open import Data.List hiding (head; span)
|
||||
open import Data.Nat using (ℕ; _<ᵇ_)
|
||||
open import Data.String hiding (_==_; show; head) renaming (_++_ to _++ˢ_; concat to concatˢ)
|
||||
open import Data.Char hiding (_==_; show)
|
||||
open import Data.Bool
|
||||
|
||||
open import Base
|
||||
|
||||
module HTML where
|
||||
|
||||
data HTMLTag : Type where
|
||||
html head meta title body : HTMLTag
|
||||
div p a span : HTMLTag
|
||||
h : (n : ℕ) → {T (n <ᵇ 7)} → HTMLTag
|
||||
|
||||
instance
|
||||
EqHTMLTag : Eq HTMLTag
|
||||
EqHTMLTag ._==_ html html = true
|
||||
EqHTMLTag ._==_ head head = true
|
||||
EqHTMLTag ._==_ meta meta = true
|
||||
EqHTMLTag ._==_ title title = true
|
||||
EqHTMLTag ._==_ body body = true
|
||||
EqHTMLTag ._==_ div div = true
|
||||
EqHTMLTag ._==_ p p = true
|
||||
EqHTMLTag ._==_ a a = true
|
||||
EqHTMLTag ._==_ span span = true
|
||||
EqHTMLTag ._==_ (h n) (h m) = n == m
|
||||
EqHTMLTag ._==_ _ _ = false
|
||||
|
||||
ShowHTMLTag : Show HTMLTag
|
||||
ShowHTMLTag .show html = "html"
|
||||
ShowHTMLTag .show head = "head"
|
||||
ShowHTMLTag .show meta = "meta"
|
||||
ShowHTMLTag .show title = "title"
|
||||
ShowHTMLTag .show body = "body"
|
||||
ShowHTMLTag .show div = "div"
|
||||
ShowHTMLTag .show a = "a"
|
||||
ShowHTMLTag .show p = "p"
|
||||
ShowHTMLTag .show span = "span"
|
||||
ShowHTMLTag .show (h n) = "h" ++ˢ show n
|
||||
|
||||
data AttributeName : Type where
|
||||
lang src name content href style : AttributeName
|
||||
|
||||
instance
|
||||
ShowAttributeName : Show AttributeName
|
||||
ShowAttributeName .show lang = "lang"
|
||||
ShowAttributeName .show src = "src"
|
||||
ShowAttributeName .show name = "name"
|
||||
ShowAttributeName .show content = "content"
|
||||
ShowAttributeName .show href = "href"
|
||||
ShowAttributeName .show style = "style"
|
||||
|
||||
record Attribute : Type where
|
||||
field
|
||||
attrname : AttributeName
|
||||
value : String -- maybe string ? how to handle syntax?
|
||||
open Attribute
|
||||
|
||||
AttrList : Type
|
||||
AttrList = List Attribute
|
||||
|
||||
_=_ : AttributeName → String → AttrList
|
||||
attrname = value = record { attrname = attrname ; value = value } ∷ []
|
||||
|
||||
mutual
|
||||
DOM : Type
|
||||
DOM = List Element
|
||||
|
||||
data Element : Type where
|
||||
textnode : String → Element
|
||||
element : HTMLTag → AttrList → DOM → Element
|
||||
|
||||
record Listable (T L : Type) : Type where
|
||||
field
|
||||
enlist : T → List L
|
||||
open Listable ⦃...⦄
|
||||
|
||||
instance
|
||||
ListListable : {T : Type} → Listable (List T) T
|
||||
ListListable .enlist l = l
|
||||
|
||||
StringDOMAble : Listable String Element
|
||||
StringDOMAble .enlist x = textnode x ∷ []
|
||||
|
||||
_,_ : {D₁ D₂ L : Type} → ⦃ Listable D₁ L ⦄ → ⦃ Listable D₂ L ⦄ → D₁ → D₂ → List L
|
||||
x , y = (enlist x) Data.List.++ (enlist y)
|
||||
|
||||
infixr 10 _,_
|
||||
|
||||
<_&_>_</_> : {D : Type} → ⦃ Listable D Element ⦄ → (x : HTMLTag) → AttrList → D → (y : HTMLTag) → {T (x == y)} → DOM
|
||||
< tag & attrs > inner </ tag′ > = element tag attrs (enlist inner) ∷ []
|
||||
|
||||
<_>_</_> : {D : Type} → ⦃ Listable D Element ⦄ → (x : HTMLTag) → D → (y : HTMLTag) → {T (x == y)} → DOM
|
||||
< tag > inner </ tag′ > = element tag [] (enlist inner) ∷ []
|
||||
|
||||
<_&_/> : (x : HTMLTag) → AttrList → DOM
|
||||
< tag & attrs /> = element tag attrs [] ∷ []
|
||||
|
||||
<_/> : (x : HTMLTag) → DOM
|
||||
< tag /> = element tag [] [] ∷ []
|
||||
|
||||
|
||||
|
||||
encode : List Char → String → String
|
||||
encode escapes text = fromList (concatMap (λ x → toList (escape-char x)) (toList text))
|
||||
where
|
||||
escape-char : Char → String
|
||||
escape-char ch =
|
||||
if any (_== ch) escapes
|
||||
then "&#" ++ˢ show (toℕ ch) ++ˢ ";"
|
||||
else fromChar ch
|
||||
|
||||
private
|
||||
encode-test : encode (toList "</>") "hi <3 </p>"
|
||||
≡ "hi <3 </p>"
|
||||
encode-test = refl
|
||||
|
||||
render-attr : Attribute → String
|
||||
render-attr x = show (x .attrname) ++ˢ "=" ++ˢ encode (toList "\t\n\r \"'=<>`") (x .value)
|
||||
|
||||
{-# TERMINATING #-} -- TODO: we should eliminate the tree as a traversable instead of doing it like this
|
||||
render-element : Element → String
|
||||
render-element (textnode x) = encode (toList "</>") x -- we don't technically need to escape all these characters, but it's easier to do this
|
||||
render-element (element tag attrlist inner) =
|
||||
"<" ++ˢ show tag ++ˢ concatˢ (map (λ attr → " " ++ˢ render-attr attr) attrlist) ++ˢ ">"
|
||||
++ˢ concatˢ (map render-element inner)
|
||||
++ˢ "</" ++ˢ show tag ++ˢ ">"
|
||||
|
||||
render-dom : DOM → String
|
||||
render-dom x = concatˢ (map render-element x)
|
||||
|
||||
sample-dom : DOM
|
||||
sample-dom =
|
||||
< html & lang = "en" >
|
||||
< head >
|
||||
< title > "Test page in Agda" </ title > ,
|
||||
< meta & name = "description" , content = "Simple webpage rendered in Agda DSL" /> ,
|
||||
< meta & name = "author" , content = "xenia" />
|
||||
</ head > ,
|
||||
< body >
|
||||
< p > "hello" </ p > ,
|
||||
< p > "world" </ p > ,
|
||||
< div >
|
||||
< p > "hi from within the div" </ p >
|
||||
</ div >
|
||||
</ body >
|
||||
</ html >
|
|
@ -3,54 +3,81 @@
|
|||
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
|
||||
import Data.String as S
|
||||
import Data.Vec as V
|
||||
import Data.List as L
|
||||
open S using (String)
|
||||
open L using (List)
|
||||
open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to _,,,_)
|
||||
open import Data.Nat hiding (_<_; _>_)
|
||||
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 Bits-and-Bytes using (Byte)
|
||||
open import SysIO
|
||||
open import Socket
|
||||
open import Indexed
|
||||
open import Parsing (Byte)
|
||||
open import NonEmpty
|
||||
open import Parse-HTTP
|
||||
open import Parse-HTTP hiding (_/_)
|
||||
open import HTML
|
||||
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
|
||||
200-ok : S.String → List Byte → List Byte
|
||||
200-ok content-type response-data = UTF-8.encode-string (S.toList (headers S.++ "\r\n\r\n")) L.++ response-data
|
||||
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))
|
||||
headers : String
|
||||
headers = "HTTP/1.1 200 OK\r\nContent-Type: " S.++ content-type S.++ "; charset=utf-8\r\nContent-Length: " S.++ (show (L.length response-data))
|
||||
|
||||
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"
|
||||
400-bad-request : List Byte
|
||||
400-bad-request = UTF-8.encode-string (S.toList "400 Bad Request\r\n\r\n")
|
||||
|
||||
render-page : (Path × Maybe String) → DOM
|
||||
render-page (path ,,, mquery) =
|
||||
< html & lang = "en" , style = "color: yellow; background: black; padding: 1em;" >
|
||||
< head >
|
||||
< title > "Test page in Agda" </ title > ,
|
||||
< meta & name = "description" , content = "Simple webpage rendered in Agda DSL" /> ,
|
||||
< meta & name = "author" , content = "xenia" />
|
||||
</ head > ,
|
||||
< body >
|
||||
< h 1 > "hi" </ h 1 > ,
|
||||
< p >
|
||||
"you requested " ,
|
||||
< span & style = "color: white;" > show path </ span > ,
|
||||
((λ q → < span & style = "color: fuchsia;" > "?" , q </ span >) <$> mquery or-else L.[])
|
||||
</ p >
|
||||
</ body >
|
||||
</ html >
|
||||
|
||||
handle-request : (Path × Maybe String) → IO (List Byte)
|
||||
handle-request req =
|
||||
pure (
|
||||
200-ok
|
||||
"text/html"
|
||||
(UTF-8.encode-string (S.toList (
|
||||
render-dom (render-page req)
|
||||
)))
|
||||
)
|
||||
|
||||
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)
|
||||
let parsed = parse-get-request .parse (V.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"))
|
||||
(real ⟨ req@(path ,,, mquery) , _ , _ ⟩) →
|
||||
(do
|
||||
putStrLn ("handle: path = " S.++ show path S.++ ", query = " S.++ mquery or-else "(no query)")
|
||||
handle-request req
|
||||
)
|
||||
cake →
|
||||
(do
|
||||
putStrLn "Got an invalid request"
|
||||
pure 400-bad-request
|
||||
)
|
||||
|
||||
run-port : ℕ
|
||||
run-port = 1337
|
||||
|
@ -58,5 +85,5 @@ run-port = 1337
|
|||
main : IO ⊤
|
||||
main = do
|
||||
putStrLn "main: starting"
|
||||
putStrLn ("main: running on port " String.++ show run-port)
|
||||
putStrLn ("main: running on port " S.++ show run-port)
|
||||
run-server "localhost" run-port handle
|
||||
|
|
|
@ -25,6 +25,6 @@ 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.++ "⁺"
|
||||
ShowList⁺ .show x = show (list⁺-to-list x) String.++ "⁺"
|
||||
where
|
||||
import Data.String as String
|
||||
|
|
|
@ -29,7 +29,7 @@ data HTTP-Method : Type where
|
|||
|
||||
instance
|
||||
ShowMethod : Show HTTP-Method
|
||||
ShowMethod .showPrec x _ = go x
|
||||
ShowMethod .show x = go x
|
||||
where
|
||||
go : HTTP-Method → String.String
|
||||
go GET = "GET"
|
||||
|
@ -90,9 +90,9 @@ module Parse-URL where
|
|||
|
||||
instance
|
||||
ShowPath : Show Path
|
||||
ShowPath .showPrec $ _ = "(empty path)"
|
||||
ShowPath .showPrec (p / $) _ = p
|
||||
ShowPath .showPrec (p / rest@(_ / _)) n = p String.++ "/" String.++ showPrec rest n
|
||||
ShowPath .show $ = "(empty path)"
|
||||
ShowPath .show (p / $) = p
|
||||
ShowPath .show (p / rest@(_ / _)) = p String.++ "/" String.++ show rest
|
||||
|
||||
infixr 5 _/_
|
||||
|
||||
|
@ -138,7 +138,7 @@ module Parse-URL where
|
|||
reg-name = decode-utf8⁺ <$?>′ (many (unreserved <|>′ percent-encoded <|>′ sub-delims))
|
||||
|
||||
unchecked : [ Parser Authority ]
|
||||
unchecked = (λ (host , rest) → host ꞉ (proj₂ <$> rest) or-else 80)
|
||||
unchecked = (λ (host , rest) → host ꞉ (proj₂ <$> rest or-else 80))
|
||||
<$>′ (reg-name <&?>′ enbox (any-of ":" <&>′ enbox number))
|
||||
|
||||
parse-path : [ Parser Path ]
|
||||
|
|
Loading…
Reference in New Issue
Block a user