diff --git a/src/Main.agda b/src/Main.agda index 4dd94c1..621a351 100644 --- a/src/Main.agda +++ b/src/Main.agda @@ -3,11 +3,14 @@ module main where open import Agda.Primitive renaming (Set to Type) + import Data.String as S import Data.Vec as V import Data.List as L open S using (String) open L using (List) +open V using (Vec) + open import Data.Product using (_×_; proj₁; proj₂; _,_) open import Data.Nat hiding (_<_; _>_) open import Data.Unit using (⊤; tt) @@ -146,6 +149,19 @@ module Pages where handle-request : HTTP.Request → IO Response handle-request req = case req .target .path of λ where + ($) → + pure ( + record + { status-code = 302 + ; status = "Found" + ; headers = + record + { name = ASCII.encode-list⁺ "Location" + ; value = ASCII.encode-list⁺ ("/" S.++ show ("index.html" / $)) + } L.∷ L.[] + ; content = cake + } + ) ("index.html" / $) → pure ( 200-ok text/html (HTML.Render.render-element (Pages.render-index (req .target .query)))