feat: v10

src/Std/Internal/Http/Protocol/H1.lean

@@ -1324,13 +1324,13 @@ private partial def processReceivingStartLine (machine : Machine .receiving) : M
 
   match result with
   | some (method, uri, version) =>
-      if version == some .v11 then
+      match version with
+      |  some (v@Version.v11) | some (v@Version.v10) =>
         machine
-        |>.modifyReader (.setMessageHead ({ method, version := .v11, uri, headers := .empty }))
+        |>.modifyReader (.setMessageHead { method, version := v, uri, headers := .empty })
         |>.setReaderState (.needHeader 0)
         |> processRead
-      else
-        machine.setFailure .unsupportedVersion
+      | _ => machine.setFailure .unsupportedVersion
   | none =>
       machine
 
@@ -1348,7 +1348,14 @@ private partial def processSendingStartLine (machine : Machine .sending) : Machi
   | some (status, version) =>
       if version == some .v11 then
         machine
-        |>.modifyReader (.setMessageHead ({ status, version := .v11, headers := .empty }))
+        |>.modifyReader (.setMessageHead { status, version := .v11, headers := .empty })
+        |>.setReaderState (.needHeader 0)
+        |> processRead
+      else if version == some .v10 then
+        -- HTTP/1.0 response: accept and disable keep-alive (shouldKeepAlive returns false
+        -- for version ≠ .v11).
+        machine
+        |>.modifyReader (.setMessageHead { status, version := .v10, headers := .empty })
         |>.setReaderState (.needHeader 0)
         |> processRead
       else

src/Std/Internal/Http/Protocol/H1/Parser.lean

@@ -278,6 +278,8 @@ public def parseRequestLine (limits : H1.Config) : Parser Request.Head := do
   let (uri, (major, minor)) ← parseRequestLineBody limits
   if major == 1 ∧ minor == 1 then
     return ⟨method, .v11, uri, .empty⟩
+  else if major == 1 ∧ minor == 0 then
+    return ⟨method, .v10, uri, .empty⟩
   else
     fail "unsupported HTTP version"
 
@@ -308,9 +310,12 @@ def parseFieldLine (limits : H1.Config) : Parser (String × String) := do
   return (name, value)
 
 /--
-Parses a single header.
+Parses a single header field line, or returns `none` when it sees the blank line that
+terminates the header section.
 
-field-line CRLF
+```
+field-line = field-name ":" OWS field-value OWS CRLF
+```
 -/
 public def parseSingleHeader (limits : H1.Config) : Parser (Option (String × String)) := do
   let next ← peek?
@@ -516,11 +521,9 @@ public def parseStatusLine (limits : H1.Config) : Parser Response.Head := do
   let (major, minor) ← parseHttpVersionNumber <* sp
   let status ← parseStatusCode limits
   if major == 1 ∧ minor == 1 then
-    return {
-      status
-      version := .v11
-      headers := .empty
-    }
+    return { status, version := .v11, headers := .empty }
+  else if major == 1 ∧ minor == 0 then
+    return { status, version := .v10, headers := .empty }
   else
     fail "unsupported HTTP version"