src/HTML.agda

@@ -1,70 +1,16 @@
 open import Agda.Primitive renaming (Set to Type)
 
-open import Data.Nat
+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
 
-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
@@ -96,24 +42,29 @@ instance
   ShowHTMLTag .show span = "span"
   ShowHTMLTag .show (h n) = "h" ++ˢ show n
 
-data Attr : Type where
+data AttributeName : Type where
-  lang= src= name= content= href= style= : String → Attr
+  lang src name content href style : AttributeName
 
-attr-name : Attr → String
+instance
-attr-name (lang=    _) = "lang"
+  ShowAttributeName : Show AttributeName
-attr-name (src=     _) = "src"
+  ShowAttributeName .show lang = "lang"
-attr-name (name=    _) = "name"
+  ShowAttributeName .show src = "src"
-attr-name (content= _) = "content"
+  ShowAttributeName .show name = "name"
-attr-name (href=    _) = "href"
+  ShowAttributeName .show content = "content"
-attr-name (style=   _) = "style"
+  ShowAttributeName .show href = "href"
+  ShowAttributeName .show style = "style"
 
-attr-value : Attr → String
+record Attribute : Type where
-attr-value (lang=    x) = x
+  field
-attr-value (src=     x) = x
+    attrname : AttributeName
-attr-value (name=    x) = x
+    value : String -- maybe string ? how to handle syntax?
-attr-value (content= x) = x
+open Attribute
-attr-value (href=    x) = x
+
-attr-value (style=   x) = x
+AttrList : Type
+AttrList = List Attribute
+
+_＝_ : AttributeName → String → AttrList
+attrname ＝ value = record { attrname = attrname ; value = value } ∷ []
 
 mutual
   DOM : Type
@@ -121,7 +72,7 @@ mutual
 
   data Element : Type where
     textnode : String → Element
-    element : HTMLTag → List Attr → DOM → Element
+    element : HTMLTag → AttrList → DOM → Element
 
 record Listable (T L : Type) : Type where
   field
@@ -129,29 +80,30 @@ 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 ∷ []
 
-  ListListable : {T : Type} → Listable (List T) T
+_,_ : {D₁ D₂ L : Type} → ⦃ Listable D₁ L ⦄ → ⦃ Listable D₂ L ⦄ → D₁ → D₂ → List L
-  ListListable .enlist x = x
+x , y = (enlist x) Data.List.++ (enlist y)
 
-  IdListable : {T : Type} → Listable T T
+infixr 10 _,_
-  IdListable .enlist x = x ∷ []
 
-  PairListable : {T L : Type} → ⦃ Listable T L ⦄ → Listable (L × T) L
+<_&_>_</_> : {D : Type} → ⦃ Listable D Element ⦄ → (x : HTMLTag) → AttrList → D → (y : HTMLTag) → {T (x == y)} → DOM
-  PairListable .enlist (x , y) = x ∷ enlist y
+< tag & attrs > inner </ tag′ > = element tag attrs (enlist inner) ∷ []
 
-<_&_>_</_> : {Es As : Type} → ⦃ Listable Es Element ⦄ → ⦃ Listable As Attr ⦄ → (x : HTMLTag) → As → Es → (y : HTMLTag) → {T (x == y)} → Element
+<_>_</_> : {D : Type} → ⦃ Listable D Element ⦄ → (x : HTMLTag) → D → (y : HTMLTag) → {T (x == y)} → DOM
-< tag & attrs > inner </ tag′ > = element tag (enlist attrs) (enlist inner)
+< tag > inner </ tag′ > = element tag [] (enlist inner) ∷ []
 
-<_>_</_> : {Es : Type} → ⦃ Listable Es Element ⦄ → (x : HTMLTag) → Es → (y : HTMLTag) → {T (x == y)} → Element
+<_&_/> :  (x : HTMLTag) → AttrList → DOM
-< tag > inner </ tag′ > = element tag [] (enlist inner)
+< tag & attrs /> = element tag attrs [] ∷ []
+
+<_/> : (x : HTMLTag) → DOM
+< tag /> = element tag [] [] ∷ []
 
-<_&_/> :  {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))
@@ -167,8 +119,8 @@ private
               ≡ "hi &#60;3 &#60;&#47;p&#62;"
   encode-test = refl
 
-render-attr : Attr → String
+render-attr : Attribute → String
-render-attr x = show (attr-name x) ++ˢ "=" ++ˢ encode (toList "\t\n\r \"'=<>`") (attr-value x)
+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
@@ -178,13 +130,16 @@ render-element (element tag attrlist inner) =
   ++ˢ concatˢ (map render-element inner)
   ++ˢ "</" ++ˢ show tag ++ˢ ">"
 
-sample-dom : Element
+render-dom : DOM → String
+render-dom x = concatˢ (map render-element x)
+
+sample-dom : DOM
 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 ＝ "description" , content ＝ "Simple webpage rendered in Agda DSL" /> ,
-      < meta & name= "author" , content= "xenia" />
+      < meta & name ＝ "author" , content ＝ "xenia" />
     </ head > ,
     < body >
       < p > "hello" </ p > ,
@@ -194,5 +149,3 @@ sample-dom =
       </ div >
     </ body >
   </ html >
-
--}

src/HTML/Render.agda

@@ -1,42 +0,0 @@
-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

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

src/NonEmpty.agda

@@ -24,25 +24,6 @@ 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
@@ -55,11 +36,6 @@ 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,9 +59,6 @@ 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 (string-to-ascii-list "mjau:)")
+                   ; content = real (list⁺-to-list (string-to-ascii-list⁺ "mjau:)"))
                    }
                  , _
                  , enc "\r\n"