Response structure

src/HTML.agda

@@ -1,16 +1,70 @@
 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.Nat
 open import Data.Bool
 
+import Data.String as S
+import Data.Char as C
+import Data.List as L
+open S using (String)
+open C using (Char)
+open L using (List)
+
 open import Base
 
 module HTML where
 
+private
+  _≤ᶜ_ : Char → Char → Bool
+  c₀ ≤ᶜ c₁ = C.toℕ c₀ ≤ᵇ C.toℕ c₁
+
+
+
+valid-attribute-name : String → Bool
+valid-attribute-name x = L.all valid-attribute-char (S.toList x)
+  where
+    valid-attribute-char : Char → Bool
+    valid-attribute-char c =
+      ('a' ≤ᶜ c) ∧ (c ≤ᶜ 'z') ∨
+      ('A' ≤ᶜ c) ∧ (c ≤ᶜ 'Z')
+
+valid-tag-name : String → Bool
+valid-tag-name x = L.all valid-tag-char (S.toList x)
+  where
+    valid-tag-char : Char → Bool
+    valid-tag-char c =
+      ('a' ≤ᶜ c) ∧ (c ≤ᶜ 'z') ∨
+      ('A' ≤ᶜ c) ∧ (c ≤ᶜ 'Z') ∨
+      ('0' ≤ᶜ c) ∧ (c ≤ᶜ '9')
+
+record Attribute : Type where
+  field
+    name : String
+    value : String
+    {name-is-valid}: T (valid-attribute-name name)
+
+instance
+  open Attribute
+  EqAttribute : Eq Attribute
+  EqAttribute ._==_ x y = x .name == y .name ∧ x .value == y .value
+
+record HTMLTag : Type where
+  field
+    name : String
+    attributes : List Attribute
+    {name-is-valid}: T (valid-tag-name name)
+
+instance
+  open HTMLTag
+
+  EqTag : Eq HTMLTag
+  EqTag ._==_ x y = x .name == y .name ∧ x .attributes == y .attributes
+
+data Element : Type where
+  textnode : String → Element
+  node : HTMLTag → List Element → Element
+
+{-
 data HTMLTag : Type where
   html head meta title body : HTMLTag
   div p a span : HTMLTag
@@ -42,29 +96,24 @@ instance
   ShowHTMLTag .show span = "span"
   ShowHTMLTag .show (h n) = "h" ++ˢ show n
 
-data AttributeName : Type where
-  lang src name content href style : AttributeName
+data Attr : Type where
+  lang= src= name= content= href= style= : String → Attr
 
-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"
+attr-name : Attr → String
+attr-name (lang=    _) = "lang"
+attr-name (src=     _) = "src"
+attr-name (name=    _) = "name"
+attr-name (content= _) = "content"
+attr-name (href=    _) = "href"
+attr-name (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 } ∷ []
+attr-value : Attr → String
+attr-value (lang=    x) = x
+attr-value (src=     x) = x
+attr-value (name=    x) = x
+attr-value (content= x) = x
+attr-value (href=    x) = x
+attr-value (style=   x) = x
 
 mutual
   DOM : Type
@@ -72,7 +121,7 @@ mutual
 
   data Element : Type where
     textnode : String → Element
-    element : HTMLTag → AttrList → DOM → Element
+    element : HTMLTag → List Attr → DOM → Element
 
 record Listable (T L : Type) : Type where
   field
@@ -80,30 +129,29 @@ record Listable (T L : Type) : Type where
 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)
+  ListListable : {T : Type} → Listable (List T) T
+  ListListable .enlist x = x
 
-infixr 10 _,_
+  IdListable : {T : Type} → Listable T T
+  IdListable .enlist x = x ∷ []
 
-<_&_>_</_> : {D : Type} → ⦃ Listable D Element ⦄ → (x : HTMLTag) → AttrList → D → (y : HTMLTag) → {T (x == y)} → DOM
-< tag & attrs > inner </ tag′ > = element tag attrs (enlist inner) ∷ []
+  PairListable : {T L : Type} → ⦃ Listable T L ⦄ → Listable (L × T) L
+  PairListable .enlist (x , y) = x ∷ enlist y
 
-<_>_</_> : {D : Type} → ⦃ Listable D Element ⦄ → (x : HTMLTag) → D → (y : HTMLTag) → {T (x == y)} → DOM
-< tag > inner </ tag′ > = element tag [] (enlist inner) ∷ []
+<_&_>_</_> : {Es As : Type} → ⦃ Listable Es Element ⦄ → ⦃ Listable As Attr ⦄ → (x : HTMLTag) → As → Es → (y : HTMLTag) → {T (x == y)} → Element
+< tag & attrs > inner </ tag′ > = element tag (enlist attrs) (enlist inner)
 
-<_&_/> :  (x : HTMLTag) → AttrList → DOM
-< tag & attrs /> = element tag attrs [] ∷ []
-
-<_/> : (x : HTMLTag) → DOM
-< tag /> = element tag [] [] ∷ []
+<_>_</_> : {Es : Type} → ⦃ Listable Es Element ⦄ → (x : HTMLTag) → Es → (y : HTMLTag) → {T (x == y)} → Element
+< tag > inner </ tag′ > = element tag [] (enlist inner)
 
+<_&_/> :  {As : Type} → ⦃ Listable As Attr ⦄ → (x : HTMLTag) → As → Element
+< tag & attrs /> = element tag (enlist attrs) []
 
+<_/> : (x : HTMLTag) → Element
+< tag /> = element tag [] []
 
 encode : List Char → String → String
 encode escapes text = fromList (concatMap (λ x → toList (escape-char x)) (toList text))
@@ -119,8 +167,8 @@ private
               ≡ "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)
+render-attr : Attr → String
+render-attr x = show (attr-name x) ++ˢ "=" ++ˢ encode (toList "\t\n\r \"'=<>`") (attr-value x)
 
 {-# TERMINATING #-} -- TODO: we should eliminate the tree as a traversable instead of doing it like this
 render-element : Element → String
@@ -130,16 +178,13 @@ render-element (element tag attrlist inner) =
   ++ˢ concatˢ (map render-element inner)
   ++ˢ "</" ++ˢ show tag ++ˢ ">"
 
-render-dom : DOM → String
-render-dom x = concatˢ (map render-element x)
-
-sample-dom : DOM
+sample-dom : Element
 sample-dom =
-  < html & lang ＝ "en" >
+  < 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" />
+      < meta & name= "description" , content= "Simple webpage rendered in Agda DSL" /> ,
+      < meta & name= "author" , content= "xenia" />
     </ head > ,
     < body >
       < p > "hello" </ p > ,
@@ -149,3 +194,5 @@ sample-dom =
       </ div >
     </ body >
   </ html >
+
+-}

src/HTML/Render.agda

@@ -0,0 +1,42 @@
+open import Agda.Primitive renaming (Set to Type)
+
+open import Data.Bool
+
+import Data.String as S
+import Data.List as L
+import Data.Char as C
+open S using (String)
+open L using (List)
+open C using (Char)
+
+open import HTML
+open import Base
+
+module HTML.Render where
+
+private
+  -- encodes using HTML decimal escapes (ɭ)
+  encode : List Char → String → String
+  encode escapes text = S.fromList (L.concatMap (λ x → S.toList (escape-char x)) (S.toList text))
+    where
+      escape-char : Char → String
+      escape-char ch =
+        if L.any (_== ch) escapes
+          then "&#" S.++ show (C.toℕ ch) S.++ ";"
+          else S.fromChar ch
+
+render-attr : Attribute → String
+render-attr x = x .name S.++ "=" S.++ encode (S.toList "\t\n\r \"'=<>`") (x .value)
+  where
+    open Attribute
+
+{-# 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 (S.toList "</>") x -- we don't technically need to escape all these characters, but it's easier to do this
+render-element (node tag inner) =
+  "<" S.++ tag .name S.++ S.concat (L.map (λ attr → " " S.++ render-attr attr) (tag .attributes)) S.++ ">"
+  S.++ S.concat (L.map render-element inner)
+  S.++ "</" S.++ tag .name S.++ ">"
+  where
+    open HTMLTag
+

src/HTML/Syntax.agda

@@ -0,0 +1,103 @@
+open import Agda.Primitive renaming (Set to Type)
+
+open import Data.Product
+open import Data.Bool hiding (_<_)
+
+import Data.String as S
+import Data.List as L
+open S using (String)
+open L using (List)
+
+open import Base
+
+open import HTML
+
+module HTML.Syntax where
+
+module Attributes where
+  open HTMLTag
+  mkAttr : (name : String) → {T (valid-attribute-name name)} → HTMLTag → String → HTMLTag
+  mkAttr attr-name {attr-name-is-valid} tag value =
+    record tag
+    { attributes = record
+        { name = attr-name
+        ; value = value
+        ; name-is-valid = attr-name-is-valid
+        }
+        L.∷ tag .attributes
+    ; name = tag .name
+    ; name-is-valid = tag .name-is-valid
+    }
+
+  _id=_ = mkAttr "id"
+  infixl 20 _id=_
+  _class=_ = mkAttr "class"
+  infixl 20 _class=_
+  _style=_ = mkAttr "style"
+  infixl 20 _style=_
+  _lang=_ = mkAttr "lang"
+  infixl 20 _lang=_
+  _src=_ = mkAttr "src"
+  infixl 20 _src=_
+  _href=_ = mkAttr "href"
+  infixl 20 _href=_
+  _name=_ = mkAttr "name"
+  infixl 20 _name=_
+  _content=_ = mkAttr "content"
+  infixl 20 _content=_
+
+open Attributes hiding (mkAttr) public
+
+module Tags where
+  mkTag : (name : String) → {T (valid-tag-name name)} → HTMLTag
+  mkTag name {name-is-valid} = record { name = name ; attributes = L.[]; name-is-valid = name-is-valid }
+
+  html = mkTag "html"
+  body = mkTag "body"
+  head = mkTag "head"
+  meta = mkTag "meta"
+  title = mkTag "title"
+  img = mkTag "img"
+  p = mkTag "p"
+  span = mkTag "span"
+  footer = mkTag "footer"
+
+  open import Data.Nat
+  open import Relation.Binary.PropositionalEquality
+  postulate
+    h-is-valid : (x : ℕ) → T (valid-tag-name ("h" S.++ show x)) -- :3
+  h : ℕ → HTMLTag
+  h x = record
+    { name = "h" S.++ show x
+    ; attributes = L.[]
+    ; name-is-valid = h-is-valid x
+    }
+
+open Tags hiding (mkTag) public
+
+record DOMAble (T : Type) : Type where
+  field
+    endom : T → List Element
+open DOMAble ⦃...⦄
+
+instance
+  TextnodeDOMAble : DOMAble String
+  TextnodeDOMAble .endom x = textnode x L.∷ L.[]
+
+  ElementDOMAble : DOMAble Element
+  ElementDOMAble .endom e = e L.∷ L.[]
+
+  ListDOMAble : {T : Type} → ⦃ DOMAble T ⦄ → DOMAble (List T)
+  ListDOMAble .endom x = L.concatMap endom x
+
+  PairDOMAble : {T₀ T₁ : Type} → ⦃ DOMAble T₀ ⦄ → ⦃ DOMAble T₁ ⦄ → DOMAble (T₀ × T₁)
+  PairDOMAble .endom (x , y) = endom x L.++ endom y
+
+module Syntax where
+  open HTMLTag
+  <_>_</_> : {D : Type} → ⦃ DOMAble D ⦄ → (t₀ : HTMLTag) → D → (t₁ : HTMLTag) → {T (t₀ .name == t₁ .name)} → Element
+  < t₀ > sub </ t₁ > = node t₀ (endom sub)
+
+  <_/> : HTMLTag → Element
+  <_/> t = node t L.[]
+open Syntax public

src/Main.agda

@@ -8,7 +8,7 @@ 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.Product using (_×_; proj₁; proj₂; _,_)
 open import Data.Nat hiding (_<_; _>_)
 open import Data.Unit using (⊤; tt)
 open import Data.Bool
@@ -23,69 +23,134 @@ open import NonEmpty
 open import Parse-HTTP
 open import Parse-HTTP.URL hiding (_/_)
 open import Parse-HTTP.Methods
-import HTML
+open import Parse-HTTP.Helpers
+open import HTML
+import HTML.Syntax
+import HTML.Render
 import UTF-8
 
-response-with-content : ℕ → S.String → String → List Byte → List Byte
-response-with-content status-code status content-type response-data =
-  UTF-8.encode-string (S.toList (status-line S.++ "\r\n" S.++ headers-lines S.++ "\r\n")) L.++ response-data
+data Content-Type : Type where
+  text/plain text/html : Content-Type
+
+instance
+  ShowContent-Type : Show Content-Type
+  ShowContent-Type .show text/plain = "text/plain"
+  ShowContent-Type .show text/html = "text/html"
+
+record Response : Type where
+  field
+    status-code : ℕ
+    status : String
+    headers : List Header -- all headers besides Content-Type and Content-Length
+    content : Maybe (Content-Type × List Byte) -- mime type and data
+open Response
+
+crlfᵇ : List Byte
+crlfᵇ = string-to-ascii-list "\r\n"
+
+encode-response : Response → List Byte
+encode-response res =
+  UTF-8.encode-string (S.toList (status-line)) L.++ crlfᵇ L.++
+  encoded-headers L.++ crlfᵇ L.++
+  (proj₂ <$> res .content or-else L.[])
   where
     status-line : String
-    status-line = "HTTP/1.1 " S.++ show status-code S.++ " " S.++ status
+    status-line = "HTTP/1.1 " S.++ show (res .status-code) S.++ " " S.++ (res .status)
 
-    response-headers : List String
-    response-headers =
-      ("Content-Type: " S.++ content-type S.++ "; charset=utf-8")
-      L.∷ ("Content-Length: " S.++ (show (L.length response-data)))
-      L.∷ L.[]
+    extra-headers : List Header
+    extra-headers = case res .content of λ where
+      cake → L.[]
+      (real (content-type , content)) →
+        record
+          { name = string-to-ascii-list⁺ "Content-Type"
+          ; value = UTF-8.encode-string (S.toList (show content-type)) ++⁺ string-to-ascii-list⁺ "; charset=utf-8"
+          }
+        L.∷ record
+          { name = string-to-ascii-list⁺ "Content-Length"
+          ; value =
+            (list-to-list⁺? (UTF-8.encode-string (S.toList (show (L.length content)))))
+            or-else (string-to-ascii-list⁺ "mjau")
+          }
+        L.∷ L.[]
 
-    headers-lines : String
-    headers-lines = L.foldr (λ hdr rest → hdr S.++ "\r\n" S.++ rest) "" response-headers
+    encode-header : Header → List Byte
+    encode-header hdr = list⁺-to-list (hdr .name ⁺++⁺ string-to-ascii-list⁺ ": " ⁺++⁺ hdr .value)
+      where
+        open Header
 
-response-without-content : ℕ → S.String → List Byte
-response-without-content status-code status =
-  UTF-8.encode-string (S.toList (
-    "HTTP/1.1 " S.++ show status-code S.++ " " S.++ status S.++ "\r\n\r\n"
-  ))
+    encoded-headers : List Byte
+    encoded-headers =
+      L.concat (
+        L.map
+          (λ h → encode-header h L.++ crlfᵇ)
+          (res .headers L.++ extra-headers)
+      )
 
-200-ok : S.String → List Byte → List Byte
-200-ok content-type response-data = response-with-content 200 "OK" content-type response-data
+200-ok : Content-Type → List Byte → List Byte
+200-ok content-type content =
+  encode-response
+    record
+    { status-code = 200
+    ; status = "OK"
+    ; headers = L.[]
+    ; content = real (content-type , content)
+    }
 
 400-bad-request : List Byte
-400-bad-request = response-without-content 400 "Bad Request"
+400-bad-request =
+  encode-response
+    record
+    { status-code = 400
+    ; status = "Bad Request"
+    ; headers = L.[]
+    ; content = real (text/plain , string-to-ascii-list "what is bro doing")
+    }
 
 404-not-found : List Byte
-404-not-found = response-with-content 404 "Not Found" "text/plain" (UTF-8.encode-string (S.toList "3: could not find the resource :("))
+404-not-found =
+  encode-response
+    record
+    { status-code = 404
+    ; status = "Not Found"
+    ; headers = L.[]
+    ; content = real (text/plain , string-to-ascii-list "not found :(")
+    }
 
 module Pages where
   open HTML
 
-  render-index : Maybe S.String → HTML.DOM
+  render-index : Maybe S.String → HTML.Element
   render-index query =
-    < html & lang ＝ "en" , style ＝ "color: yellow; background: black; padding: 1em;" >
+    < html lang= "en" style= "color: white; 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" />
+        < title > "henttp index" </ title > ,
+        < meta name= "description" content= "Simple webpage rendered in Agda DSL" /> ,
+        < meta name= "author" content= "xenia" />
       </ head > ,
       < body >
-        < h 1 > "hi" </ h 1 > ,
+        < h 1 >
+          < span style= "color: yellow;" > "hen" </ span > ,
+          < span style= "color: purple;" > "ttp" </ span >
+        </ h 1 > ,
         < p >
-          "welcome to the " ,
-          < span & style ＝ "color: white;" > "index" </ span > ,
-          (((λ q → < span & style ＝ "color: fuchsia;" > " (query = " , q , ")" </ span >) <$> query) or-else L.[])
-          </ p >
-      </ body >
+          "what is this?"
+        </ p >
+      </ body > ,
+      < footer >
+        "meow"
+      </ footer >
     </ html >
+    where
+      open HTML.Syntax
 
 handle-request : Request → IO (List Byte)
 handle-request req =
   if (req .target .path) == ("index.html" / $)
     then pure (
       200-ok
-        "text/html"
+        text/html
         (UTF-8.encode-string (S.toList (
-          HTML.render-dom (Pages.render-index (req .target .query))
+          HTML.Render.render-element (Pages.render-index (req .target .query))
         )))
       )
     else pure 404-not-found

src/NonEmpty.agda

@@ -24,6 +24,25 @@ foldl : {A B : Type} → (B → A → B) → B → List⁺ A → B
 foldl _+_ acc [ x ]⁺ = acc + x
 foldl _+_ acc (x ∷⁺ xs) = foldl _+_ (acc + x) xs
 
+cons⁺ : {A : Type} → A → List A → List⁺ A
+cons⁺ a [] = [ a ]⁺
+cons⁺ a (x ∷ xs) = a ∷⁺ cons⁺ x xs
+
+_⁺++⁺_ : {A : Type} → List⁺ A → List⁺ A → List⁺ A
+[ x ]⁺ ⁺++⁺ l₁ = x ∷⁺ l₁
+(x ∷⁺ l₀) ⁺++⁺ l₁ = x ∷⁺ (l₀ ⁺++⁺ l₁)
+
+_++⁺_ : {A : Type} → List A → List⁺ A → List⁺ A
+[] ++⁺ l₁ = l₁
+(x ∷ l₀) ++⁺ l₁ = x ∷⁺ (l₀ ++⁺ l₁)
+
+_⁺++_ : {A : Type} → List⁺ A → List A → List⁺ A
+[ x ]⁺ ⁺++ [] = [ x ]⁺
+[ x ]⁺ ⁺++ (y ∷ l₁) = (x ∷⁺ [ y ]⁺ ) ⁺++ l₁
+(x ∷⁺ l₀) ⁺++ l₁ = x ∷⁺ (l₀ ⁺++ l₁)
+
+infixr 20 _⁺++⁺_ _++⁺_ _⁺++_
+
 list⁺-to-list : {A : Type} → List⁺ A → List A
 list⁺-to-list [ x ]⁺ = x ∷ []
 list⁺-to-list (x ∷⁺ xs) = x ∷ list⁺-to-list xs
@@ -36,6 +55,11 @@ vec-to-list⁺ : {A : Type} → {n : ℕ} → V.Vec A (suc n) → List⁺ A
 vec-to-list⁺ (x V.∷ V.[]) = [ x ]⁺
 vec-to-list⁺ (x V.∷ xs@(_ V.∷ _)) = x ∷⁺ vec-to-list⁺ xs
 
+list-to-list⁺? : {A : Type} → List A → Maybe (List⁺ A)
+list-to-list⁺? [] = cake
+list-to-list⁺? (x ∷ xs) = real (cons⁺ x xs)
+
+
 instance
   ShowList⁺ : {A : Type} → ⦃ Show A ⦄ → Show (List⁺ A)
   ShowList⁺ .show x = show (list⁺-to-list x) String.++ "⁺"

src/Parse-HTTP/Helpers.agda

@@ -59,6 +59,9 @@ string-to-ascii-list⁺ s {ascii} {nonempty} = vec-to-list⁺ v
     v : Vec Byte (suc (pred (length s)))
     v = subst (λ x → Vec Byte x) (sym (suc[pred[n]]≡n {length s} len≢0)) (string-to-ascii-vec s {ascii})
 
+string-to-ascii-list : (s : String) → {string-is-ascii s} → List Byte
+string-to-ascii-list s {ascii} = V.toList (string-to-ascii-vec s {ascii})
+
 any-of : String → [ Parser Byte ]
 any-of x = L.foldr (λ ch p → ((_is ch) <?>′ any₁) <|>′ p) fail (S.toList x)
 

src/Parse-HTTP/Test.agda

@@ -110,7 +110,7 @@ module Test-HTTP where
                      record { name = string-to-ascii-list⁺ "Content-Length" ; value = string-to-ascii-list⁺ "6" }
                      List.∷ record { name = string-to-ascii-list⁺ "Host" ; value = string-to-ascii-list⁺ "agda.nu" }
                      List.∷ List.[]
-                   ; content = real (list⁺-to-list (string-to-ascii-list⁺ "mjau:)"))
+                   ; content = real (string-to-ascii-list "mjau:)")
                    }
                  , _
                  , enc "\r\n"