Skip to content

Commit

Permalink
HTTP answers with the Pluto name + cache informations
Browse files Browse the repository at this point in the history
  • Loading branch information
clarus committed Dec 8, 2014
1 parent 73506c1 commit 3cced2a
Showing 1 changed file with 18 additions and 9 deletions.
27 changes: 18 additions & 9 deletions Answer.v
Original file line number Diff line number Diff line change
Expand Up @@ -34,13 +34,15 @@ End Status.
Module Header.
Module Kind.
Inductive t : Set :=
| CacheControl : t
| ContentType : t
| ContentLength : t
| Date : t
| Server : t.

Definition to_string (kind : t) : LString.t :=
LString.s @@ match kind with
| CacheControl => "Cache-Control"
| ContentType => "Content-Type"
| ContentLength => "Content-Length"
| Date => "Date"
Expand Down Expand Up @@ -68,14 +70,21 @@ Definition to_string (answer : t) : LString.t :=
[LString.s ""; body answer]).

Definition ok (mime_type : MimeType.t) (content : LString.t) (time : Moment.t)
: t := {|
status := Status.OK;
headers := [
Header.New Header.Kind.ContentType (MimeType.to_string mime_type);
Header.New Header.Kind.ContentLength (LString.of_N 10 12 None @@ Iterable.length content);
Header.New Header.Kind.Date (Moment.Print.rfc1123 time);
Header.New Header.Kind.Server (LString.s "Coq")];
body := content |}.
: t :=
let cache_control :=
if LString.eqb (MimeType.to_string mime_type) (LString.s "text/html") then
LString.s "no-cache"
else
LString.s "max-age=604800, public" in
{|
status := Status.OK;
headers := [
Header.New Header.Kind.CacheControl cache_control;
Header.New Header.Kind.ContentType (MimeType.to_string mime_type);
Header.New Header.Kind.ContentLength (LString.of_N 10 12 None @@ Iterable.length content);
Header.New Header.Kind.Date (Moment.Print.rfc1123 time);
Header.New Header.Kind.Server (LString.s "Pluto")];
body := content |}.

Definition error (time : Moment.t) : t :=
let mime_type := MimeType.New (LString.s "text") (LString.s "plain") in
Expand All @@ -86,5 +95,5 @@ Definition error (time : Moment.t) : t :=
Header.New Header.Kind.ContentType (MimeType.to_string mime_type);
Header.New Header.Kind.ContentLength (LString.of_N 10 12 None @@ Iterable.length content);
Header.New Header.Kind.Date (Moment.Print.rfc1123 time);
Header.New Header.Kind.Server (LString.s "Coq")];
Header.New Header.Kind.Server (LString.s "Pluto")];
body := content |}.

0 comments on commit 3cced2a

Please sign in to comment.