Compare commits

...

5 Commits

Author SHA1 Message Date
2caca85e6f HTML templating 2023-09-03 13:51:45 +02:00
ab1d2306d9 devshell -> devshells 2023-09-03 13:51:19 +02:00
d2bd03a17e infix or-else 2023-09-03 13:51:16 +02:00
3216656638 clean 2023-09-03 12:25:32 +02:00
5103fc0996 Remove showPrec, use show everywhere 2023-09-03 12:25:28 +02:00
7 changed files with 228 additions and 44 deletions

View File

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

View File

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

View File

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

151
src/HTML.agda Normal file
View 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 &#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 >

View File

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

View File

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

View File

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