HTML templating
This commit is contained in:
parent
ab1d2306d9
commit
2caca85e6f
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,48 +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
|
||||
|
||||
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
|
||||
|
|
@ -52,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
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user