Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
53 commits
Select commit Hold shift + click to select a range
0e5f075
feat: introduce data type for HTTP
algebraic-dev Jan 23, 2026
21286eb
fix: domain name comment
algebraic-dev Jan 24, 2026
bad70e3
feat: request type has request target
algebraic-dev Jan 24, 2026
03843fd
fix: suggestions
algebraic-dev Feb 10, 2026
c498ea7
Merge branch 'sofia/async-http-headers' of https://github.com/leanpro…
algebraic-dev Feb 10, 2026
c4f179d
Merge branch 'sofia/async-http-headers' of https://github.com/leanpro…
algebraic-dev Feb 10, 2026
2c23680
fix: imports
algebraic-dev Feb 10, 2026
0c44b4a
Merge branch 'sofia/async-http-headers' of https://github.com/leanpro…
algebraic-dev Feb 11, 2026
2cc3292
feat: add parser features to path
algebraic-dev Feb 13, 2026
e92fcf6
Merge branch 'sofia/async-http-headers' of https://github.com/leanpro…
algebraic-dev Feb 13, 2026
451c11d
fix: make strict
algebraic-dev Feb 13, 2026
cacfe00
fix: test
algebraic-dev Feb 13, 2026
692c7c1
fix: test
algebraic-dev Feb 13, 2026
10337c6
fix: test
algebraic-dev Feb 13, 2026
d07f5c5
feat: specialize encodedstrings
algebraic-dev Feb 13, 2026
8c00ba4
fix: parser
algebraic-dev Feb 13, 2026
b042b8e
fix: parser path
algebraic-dev Feb 13, 2026
43d3b2d
merge: 'sofia/async-http-headers'
algebraic-dev Feb 13, 2026
c4737fb
fix: parse ab-empty
algebraic-dev Feb 13, 2026
1c564ed
fix: comment
algebraic-dev Feb 13, 2026
9dd5634
Merge branch 'sofia/async-http-headers' into sofia/async-http-uri
algebraic-dev Feb 17, 2026
37ec94e
Merge branch 'sofia/async-http-headers' into sofia/async-http-uri
algebraic-dev Feb 18, 2026
53fb1a2
Merge branch 'sofia/async-http-headers' into sofia/async-http-uri
algebraic-dev Feb 18, 2026
10a66e9
fix: uri duplication checkers
algebraic-dev Feb 18, 2026
42cfda2
Merge branch 'sofia/async-http-headers' into sofia/async-http-uri
algebraic-dev Feb 18, 2026
37c7b1e
feat: reuse char
algebraic-dev Feb 18, 2026
319214c
feat: config URI
algebraic-dev Feb 19, 2026
73bf2b5
Merge branch 'sofia/async-http-headers' into sofia/async-http-uri
algebraic-dev Feb 19, 2026
462e3d0
fix: import coe
algebraic-dev Feb 20, 2026
eddb5e1
Merge branch 'sofia/async-http-headers' into sofia/async-http-uri
algebraic-dev Feb 20, 2026
781b9f5
Merge branch 'sofia/async-http-headers' into sofia/async-http-uri
algebraic-dev Feb 20, 2026
530f686
Merge branch 'sofia/async-http-headers' into sofia/async-http-uri
algebraic-dev Feb 20, 2026
e0efb8a
fix: scheme parser
algebraic-dev Feb 20, 2026
bfa18ef
fix: uri builder
algebraic-dev Feb 20, 2026
0fb57a4
fix: wrong comment
algebraic-dev Feb 20, 2026
5ba3a6d
Merge branch 'sofia/async-http-headers' into sofia/async-http-uri
algebraic-dev Feb 24, 2026
21821ef
fix: encoding duplication
algebraic-dev Feb 24, 2026
03f1d47
Merge branch 'sofia/async-http-headers' into sofia/async-http-uri
algebraic-dev Feb 26, 2026
4de3e40
fix: builder
algebraic-dev Feb 26, 2026
819d4c6
fix: uri comments
algebraic-dev Feb 26, 2026
73cf41d
fix: comments
algebraic-dev Feb 26, 2026
a72de46
Merge branch 'sofia/async-http-headers' into sofia/async-http-uri
algebraic-dev Feb 26, 2026
5cb510c
fix: precedence
algebraic-dev Feb 26, 2026
ec833b5
Merge branch 'sofia/async-http-headers' into sofia/async-http-uri
algebraic-dev Feb 26, 2026
c5180b2
Merge branch 'sofia/async-http-headers' into sofia/async-http-uri
algebraic-dev Feb 26, 2026
2e60488
Merge branch 'sofia/async-http-headers' into sofia/async-http-uri
algebraic-dev Feb 26, 2026
81f76a2
fix:lower case scheme
algebraic-dev Feb 26, 2026
718e549
Merge branch 'sofia/async-http-headers' into sofia/async-http-uri
algebraic-dev Feb 26, 2026
cdfd241
fix: test
algebraic-dev Feb 26, 2026
6edc0c7
Merge branch 'sofia/async-http-headers' into sofia/async-http-uri
algebraic-dev Feb 27, 2026
c86f926
Merge branch 'sofia/async-http-headers' into sofia/async-http-uri
algebraic-dev Feb 27, 2026
3aa02ee
fix: comments
algebraic-dev Feb 27, 2026
0bb4ba7
Merge branch 'sofia/async-http-headers' into sofia/async-http-uri
algebraic-dev Feb 28, 2026
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions src/Std/Internal/Http/Data.lean
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ public import Std.Internal.Http.Data.Response
public import Std.Internal.Http.Data.Status
public import Std.Internal.Http.Data.Chunk
public import Std.Internal.Http.Data.Headers
public import Std.Internal.Http.Data.URI

/-!
# HTTP Data Types
Expand Down
40 changes: 24 additions & 16 deletions src/Std/Internal/Http/Data/Request.lean
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@ public import Std.Internal.Http.Data.Extensions
public import Std.Internal.Http.Data.Method
public import Std.Internal.Http.Data.Version
public import Std.Internal.Http.Data.Headers
public import Std.Internal.Http.Data.URI

public section

Expand Down Expand Up @@ -50,7 +51,7 @@ structure Request.Head where
/--
The raw request-target string (commonly origin-form path/query, `"*"`, or authority-form).
-/
uri : String
uri : RequestTarget := .asteriskForm

/--
Collection of HTTP headers for the request (Content-Type, Authorization, etc.).
Expand Down Expand Up @@ -85,7 +86,7 @@ structure Request.Builder where
/--
The head of the request.
-/
head : Head := { method := .get, version := .v11, uri := "*" }
head : Head := { method := .get, version := .v11, uri := .asteriskForm }

/--
Optional dynamic metadata attached to the request.
Expand All @@ -108,7 +109,7 @@ instance : Encode .v11 Head where
encode buffer req :=
let buffer := Encode.encode (v := .v11) buffer req.method
let buffer := buffer.writeChar ' '
let buffer := buffer.writeString req.uri
let buffer := Encode.encode (v := .v11) buffer req.uri
let buffer := buffer.writeChar ' '
let buffer := Encode.encode (v := .v11) buffer req.version
let buffer := buffer.writeString "\r\n"
Expand Down Expand Up @@ -144,11 +145,18 @@ def version (builder : Builder) (version : Version) : Builder :=
/--
Sets the request target/URI for the request being built.
-/
def uri (builder : Builder) (uri : String) : Builder :=
def uri (builder : Builder) (uri : RequestTarget) : Builder :=
{ builder with head := { builder.head with uri := uri } }

/--
Sets the headers for the request being built.
Sets the request target/URI for the request being built
-/
def uri! (builder : Builder) (uri : String) : Builder :=
let uri := RequestTarget.parse! uri
{ builder with head := { builder.head with uri } }

/--
Sets the headers for the request being built
-/
def headers (builder : Builder) (headers : Headers) : Builder :=
{ builder with head := { builder.head with headers } }
Expand Down Expand Up @@ -201,39 +209,39 @@ end Builder
/--
Creates a new HTTP GET Request with the specified URI.
-/
def get (uri : String) : Builder :=
def get (uri : RequestTarget) : Builder :=
new
|>.method .get
|>.uri uri

/--
Creates a new HTTP POST Request builder with the specified URI.
-/
def post (uri : String) : Builder :=
def post (uri : RequestTarget) : Builder :=
new
|>.method .post
|>.uri uri

/--
Creates a new HTTP PUT Request builder with the specified URI.
-/
def put (uri : String) : Builder :=
def put (uri : RequestTarget) : Builder :=
new
|>.method .put
|>.uri uri

/--
Creates a new HTTP DELETE Request builder with the specified URI.
-/
def delete (uri : String) : Builder :=
def delete (uri : RequestTarget) : Builder :=
new
|>.method .delete
|>.uri uri

/--
Creates a new HTTP PATCH Request builder with the specified URI.
-/
def patch (uri : String) : Builder :=
def patch (uri : RequestTarget) : Builder :=
new
|>.method .patch
|>.uri uri
Expand All @@ -242,33 +250,33 @@ def patch (uri : String) : Builder :=
Creates a new HTTP HEAD Request builder with the specified URI.
Named `head'` to avoid conflict with the `head` field accessor.
-/
def head' (uri : String) : Builder :=
def head' (uri : RequestTarget) : Builder :=
new
|>.method .head
|>.uri uri

/--
Creates a new HTTP OPTIONS Request builder with the specified URI.
Use `Request.options "*"` for server-wide OPTIONS.
Use `Request.options (RequestTarget.asteriskForm)` for server-wide OPTIONS.
-/
def options (uri : String) : Builder :=
def options (uri : RequestTarget) : Builder :=
new
|>.method .options
|>.uri uri

/--
Creates a new HTTP CONNECT Request builder with the specified URI.
Typically used with authority-form URIs such as `"example.com:443"` for tunneling.
Typically used with `RequestTarget.authorityForm` for tunneling.
-/
def connect (uri : String) : Builder :=
def connect (uri : RequestTarget) : Builder :=
new
|>.method .connect
|>.uri uri

/--
Creates a new HTTP TRACE Request builder with the specified URI.
-/
def trace (uri : String) : Builder :=
def trace (uri : RequestTarget) : Builder :=
new
|>.method .trace
|>.uri uri
Expand Down
79 changes: 79 additions & 0 deletions src/Std/Internal/Http/Data/URI.lean
Original file line number Diff line number Diff line change
@@ -0,0 +1,79 @@
/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sofia Rodrigues
-/
module

prelude
public import Std.Internal.Http.Data.URI.Basic
public import Std.Internal.Http.Data.URI.Parser

public section

/-!
# URI

This module defines the `URI` and `RequestTarget` types that represent and manipulate components of
URIs as defined by RFC 3986. It provides parsing, rendering, and normalization utilities for working
with URIs and request targets in HTTP messages.

References:
* https://www.rfc-editor.org/rfc/rfc3986.html
* https://www.rfc-editor.org/rfc/rfc9112.html#section-3.3
-/

namespace Std.Http.RequestTarget

set_option linter.all true

/--
Attempts to parse a `RequestTarget` from the given string.
-/
@[inline]
def parse? (string : String) : Option RequestTarget :=
(URI.Parser.parseRequestTarget <* Std.Internal.Parsec.eof).run string.toUTF8 |>.toOption

/--
Parses a `RequestTarget` from the given string. Panics if parsing fails. Use `parse?`
if you need a safe option-returning version.
-/
@[inline]
def parse! (string : String) : RequestTarget :=
match parse? string with
| some res => res
| none => panic! "invalid request target"

/--
Creates an origin-form request target from a path string.
The path should start with '/' (e.g., "/api/users" or "/search?q=test").
Panics if the string is not a valid origin-form request target.
-/
@[inline]
def originForm! (path : String) : RequestTarget :=
match parse? path with
| some (.originForm p q) => .originForm p q
| _ => panic! s!"invalid origin-form request target: {path}"

end RequestTarget

namespace URI

/--
Attempts to parse a `URI` from the given string.
-/
@[inline]
def parse? (string : String) : Option URI :=
(Parser.parseURI <* Std.Internal.Parsec.eof).run string.toUTF8 |>.toOption

/--
Parses a `URI` from the given string. Panics if parsing fails. Use `parse?` if you need a safe
option-returning version.
-/
@[inline]
def parse! (string : String) : URI :=
match parse? string with
| some res => res
| none => panic! "invalid URI"

end URI
Loading
Loading