fix: problem with URI, for some reason it was upper cased in github

Author: algebraic-dev

Http/Data.lean

@@ -4,5 +4,5 @@ import Http.Data.Method
 import Http.Data.Request
 import Http.Data.Status
 import Http.Data.Response
-import Http.Data.Uri
+import Http.Data.URI
 import Http.Data.Version

Http/Data/Request.lean

@@ -2,7 +2,7 @@ import Http.Data.Headers
 import Http.Data.Version
 import Http.Data.Method
 import Http.Data.Body
-import Http.Data.Uri
+import Http.Data.URI
 import Http.Classes
 
 namespace Http.Data
@@ -12,15 +12,15 @@ open Http.Classes
 headers and a [Incoming] body, that can be a stream. -/
 structure Request where
   method  : Method
-  uri     : Uri
+  uri     : URI
   version : Version
   headers : Headers
   deriving Repr, Inhabited
 
 namespace Request
 
 def empty : Request :=
-  Request.mk Method.get Uri.empty Version.v10 Inhabited.default
+  Request.mk Method.get URI.empty Version.v10 Inhabited.default
 
 instance : Canonical .text Request where
   repr r :=

Http/Data/Status.lean

@@ -248,7 +248,7 @@ instance : Canonical .text Status where
     | .lengthRequired => "Length Required"
     | .preconditionFailed => "Precondition Failed"
     | .payloadTooLarge => "Request Entity Too Large"
-    | .uriTooLong => "Request Uri Too Long"
+    | .uriTooLong => "Request URI Too Long"
     | .unsupportedMediaType => "Unsupported Media Type"
     | .rangeNotSatisfiable => "Requested Range Not Satisfiable"
     | .expectationFailed => "Expectation Failed"

Http/Data/URI/Authority.lean

@@ -1,7 +1,7 @@
 import CaseInsensitive
 import Http.Classes
 
-namespace Http.Data.Uri
+namespace Http.Data.URI
 open Http.Classes
 
 /-- TCP number port -/

Http/Data/URI/Grammar.lean

@@ -1,7 +1,7 @@
 import Parse
 import Parse.DSL
 
-namespace Http.Data.Uri
+namespace Http.Data.URI
 
 /-! This code defines an incremental parser for parsing different components of a URI. -/
 

Http/Data/URI/Parser.lean

@@ -1,9 +1,9 @@
-import Http.Data.Uri.Grammar
-import Http.Data.Uri
+import Http.Data.URI.Grammar
+import Http.Data.URI
 
-namespace Http.Data.Uri
+namespace Http.Data.URI
 
-structure Uri.State where
+structure URI.State where
   authority : Option String
   path      : Option String
   query     : Option String
@@ -15,9 +15,9 @@ structure Uri.State where
 /-! Defines an incremental parser handler using the `Grammar` module. This parser is designed to handle
     URI components incrementally.
 -/
-abbrev Parser := Grammar.Data Uri.State
+abbrev Parser := Grammar.Data URI.State
 
-private def setField (func: String → Uri.State → Uri.State) : Nat → Nat → ByteArray → Uri.State → IO (Uri.State × Nat) :=
+private def setField (func: String → URI.State → URI.State) : Nat → Nat → ByteArray → URI.State → IO (URI.State × Nat) :=
   fun st en bs acc => pure (func (String.fromAscii $ bs.extract st en) acc, 0)
 
 /-- Creates a new parser structure. This parser uses various field-setting functions to update the
@@ -44,7 +44,7 @@ def Parser.feed (parser: Parser) (data: ByteArray) : IO Parser :=
 
 /-- Retrieves the parsed URI data from the parser. This function extracts the accumulated URI
 information from the parser. -/
-def Parser.data (parser: Parser) : Except Nat Uri :=
+def Parser.data (parser: Parser) : Except Nat URI :=
   if parser.error ≠ 0 then
     .error parser.error
   else
@@ -57,4 +57,4 @@ def Parser.data (parser: Parser) : Except Nat Uri :=
       | [] => (none, none)
       | _ => panic "impossible uri"
     let authority := Authority.mk userinfo host port
-    .ok (Uri.mk authority state.path state.query state.fragment)
+    .ok (URI.mk authority state.path state.query state.fragment)

Http/Data/URI/Scheme.lean

@@ -1,7 +1,7 @@
 import CaseInsensitive
 import Http.Classes
 
-namespace Http.Data.Uri
+namespace Http.Data.URI
 open Http.Classes
 
 /-- The standard schemes described in the HTTP core semantics. -/

Http/Data/Uri.lean

@@ -1,6 +1,6 @@
-import Http.Data.Uri.Authority
-import Http.Data.Uri.Scheme
-import Http.Data.Uri.Query
+import Http.Data.URI.Authority
+import Http.Data.URI.Scheme
+import Http.Data.URI.Query
 import Http.Util.Format
 import Http.Util
 import Http.Classes
@@ -14,22 +14,22 @@ open Lean
 
 * Reference: https://www.rfc-editor.org/rfc/rfc3986.html#section-3.2.2
 -/
-structure Uri where
-  authority : Uri.Authority := {}
+structure URI where
+  authority : URI.Authority := {}
   path      : Option String := none
   query     : Option String := none
   fragment  : Option String := none
   deriving BEq, Repr, Inhabited
 
-def Uri.encode (input: String) : String :=
+def URI.encode (input: String) : String :=
     input.toUTF8.foldl (λs c => s ++ encodeChar c) ""
   where
     encodeChar char :=
       if (char ≥ 97 ∧ char ≤ 122) ∨ (char ≥ 65 ∧ char ≤ 90) ∨ (char ≥ 48 ∧ char ≤ 57)
         then (Char.ofNat (UInt8.toNat char)).toString
         else s!"%{(toHex char.toNat).toUpper}"
 
-def Uri.componentDecode (input: String) : Option String := Id.run do
+def URI.componentDecode (input: String) : Option String := Id.run do
   let mut result := ByteArray.empty
   let mut acc := 0
   let mut start := none
@@ -65,7 +65,7 @@ def Uri.componentDecode (input: String) : Option String := Id.run do
 
   return String.fromAscii result
 
-instance : Canonical .text Uri where
+instance : Canonical .text URI where
   repr u :=
     let authority := Canonical.text u.authority
     let path := Option.getD u.path ""
@@ -74,6 +74,6 @@ instance : Canonical .text Uri where
     let notEncoded := String.join [authority, path, query, fragment]
     notEncoded
 
-namespace Uri
+namespace URI
 
-def empty : Uri := Uri.mk Inhabited.default none none none
+def empty : URI := URI.mk Inhabited.default none none none

Http/IO/Client.lean

@@ -2,7 +2,7 @@ import Http.Protocols.Http1.Parser
 import Http.Protocols.Http1.Data
 import Http.IO.Server.Config
 import Http.IO.Server.Connection
-import Http.Data.Uri.Parser
+import Http.Data.URI.Parser
 import Http.Data
 import Http.Util
 import Http.Classes

Http/IO/Server.lean

@@ -2,7 +2,7 @@ import Http.Protocols.Http1.Parser
 import Http.Protocols.Http1.Data
 import Http.IO.Server.Config
 import Http.IO.Server.Connection
-import Http.Data.Uri.Parser
+import Http.Data.URI.Parser
 import Http.Data
 import Http.Util
 import Http.Classes