HTML templating

flake.nix

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

src/Base.agda

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

src/Bits-and-Bytes.agda

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

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 </ 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 &#60;3 &#60;&#47;p&#62;"
+  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 >

src/Main.agda

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

src/NonEmpty.agda

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

src/Parse-HTTP.agda

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