From 2caca85e6fe48a5a5248926afa0d5c925442f4f1 Mon Sep 17 00:00:00 2001 From: xenia Date: Sun, 3 Sep 2023 13:51:45 +0200 Subject: [PATCH] HTML templating --- src/HTML.agda | 151 ++++++++++++++++++++++++++++++++++++++++++++++++++ src/Main.agda | 77 +++++++++++++++++-------- 2 files changed, 206 insertions(+), 22 deletions(-) create mode 100644 src/HTML.agda diff --git a/src/HTML.agda b/src/HTML.agda new file mode 100644 index 0000000..c4d894e --- /dev/null +++ b/src/HTML.agda @@ -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 = element tag attrs (enlist inner) ∷ [] + +<_>_ : {D : Type} → ⦃ Listable D Element ⦄ → (x : HTMLTag) → D → (y : HTMLTag) → {T (x == y)} → DOM +< tag > inner = 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

" + ≡ "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) + ++ˢ "" + +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" , + < meta & name = "description" , content = "Simple webpage rendered in Agda DSL" /> , + < meta & name = "author" , content = "xenia" /> + , + < body > + < p > "hello" , + < p > "world" , + < div > + < p > "hi from within the div" + + + diff --git a/src/Main.agda b/src/Main.agda index 8c8f5bb..75ac46d 100644 --- a/src/Main.agda +++ b/src/Main.agda @@ -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" , + < meta & name = "description" , content = "Simple webpage rendered in Agda DSL" /> , + < meta & name = "author" , content = "xenia" /> + , + < body > + < h 1 > "hi" , + < p > + "you requested " , + < span & style = "color: white;" > show path , + ((λ q → < span & style = "color: fuchsia;" > "?" , q ) <$> mquery or-else L.[]) + + + + +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