feat: use captureStr

.github/workflows/build.yml

@@ -0,0 +1,22 @@
+on:
+  push:
+  pull_request:
+
+name: ci
+
+jobs:
+  build:
+    name: Build
+    runs-on: ubuntu-latest
+    steps:
+      - name: install elan
+        run: |
+          set -o pipefail
+          curl -sSfL https://github.com/leanprover/elan/releases/download/v1.4.2/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+          ./elan-init -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> $GITHUB_PATH
+
+      - uses: actions/checkout@v2
+
+      - name: build package
+        run: lake build

.gitignore

@@ -1,4 +1,4 @@
 *.olean
-result*
+lake-packages
 lean_packages
-build
+build

Http/HeaderName.lean

@@ -895,7 +895,7 @@ namespace Standard
 
 -- TODO: check if trie is faster than whatever leanc+llvm produce
 -- if you just pattern match on all the strings
-def trie := all.foldl (fun a b => a.insert b.toHeaderString b) (Lean.Parser.Trie.empty)
+def trie := all.foldl (fun a b => a.insert b.toHeaderString b) Lean.Data.Trie.empty
 def parse := trie.find?
 
 end HeaderName.Standard
@@ -917,10 +917,10 @@ def ofHeaderString (s : String) :=
   | some n => standard n
   | none => custom ⟨s, _, by congr⟩
 
-end Http.HeaderName open Parser open Http.Parser
+end Http.HeaderName open Parser Char open Http.Parser
 namespace Http.HeaderName
 
 def parse : Parser HeaderName := do
-  let str ← capture <| dropMany1 (tokenFilter (fun c => Char.isAlphanum c ||
+  let str ← captureStr <| dropMany1 (tokenFilter (fun c => Char.isAlphanum c ||
             c ∈ ['-', '_', '!', '#', '$', '%', '&', '|', '*', '+', '.', '^', '"', '\'', '`']))
-  return HeaderName.ofHeaderString str.toString
+  return HeaderName.ofHeaderString str.2.toString

Http/Headers.lean

@@ -7,6 +7,7 @@ import Std
 import Http.Parser
 import Http.HeaderName
 
+open Parser Char
 open Http.Parser
 
 namespace Http
@@ -41,9 +42,9 @@ def parseHeader : Parser (HeaderName × String) := do
   ws
   let _ ← Parser.token ':'
   ws
-  let value ← capture <| Parser.dropMany <| Parser.tokenFilter (fun c => c != '\n')
+  let value ← captureStr <| Parser.dropMany <| Parser.tokenFilter (fun c => c != '\n')
   ws
-  return (key, value.toString)
+  return (key, value.2.toString)
 
 def parse : Parser Headers := do
   let headers ← Array.foldl (λ map (k, v) => map.add k v) .empty <$>

Http/Parser.lean

@@ -10,14 +10,14 @@ namespace Http
 nonrec abbrev Parser.Error := Parser.Error.Simple Substring Char
 nonrec abbrev Parser := Parser Parser.Error Substring Char
 
-def Parser.capture (p : Parser α) : Parser Substring := do
-  let p1 ← Parser.getPosition
-  let _ ← p
-  let p2 ← Parser.getPosition
-  return { (← StateT.get).stream with
-      startPos := p1
-      stopPos := p2
-    }
+-- def Parser.capture (p : Parser α) : Parser Substring := do
+--   let p1 ← Parser.getPosition
+--   let _ ← p
+--   let p2 ← Parser.getPosition
+--   return { (← StateT.get).stream with
+--       startPos := p1
+--       stopPos := p2
+--     }
 
 def Parser.ws : Parser Unit := do
   Parser.dropMany <| Parser.tokenFilter <| Char.isWhitespace

Http/URI.lean

@@ -31,7 +31,7 @@ def ofString (s : String) : Option Scheme :=
   else
     none
 
-instance : Inhabited Scheme := ⟨ofString "a" |>.get (by simp only)⟩
+instance : Inhabited Scheme := ⟨ofString "a" |>.get rfl⟩
 
 def HTTP := ofString "http" |>.get!
 def HTTPS := ofString "https" |>.get!
@@ -100,7 +100,7 @@ structure URI where
   fragment : Option Fragment
 deriving Inhabited
 
-end Http open Parser
+end Http open Parser Char
 namespace Http
 
 open Http.Parser
@@ -136,28 +136,28 @@ URLs.
 -/
 
 def Scheme.parse : Parser Scheme := do
-  let str ← capture <| do
+  let str ← captureStr <| do
     let _ ← tokenFilter (·.isAlpha)
     let _ ← dropMany <| tokenFilter (fun c => c.isAlphanum || c ∈ ['+', '-', '.'])
-  return Scheme.ofString str.toString |>.get!
+  return Scheme.ofString str.2.toString |>.get!
 
 def Authority.UserInfo.parse : Parser Authority.UserInfo := do
-  let user : Substring ←
-    capture <| dropMany <| tokenFilter (·.isAlphanum)
-  let pword : Option Substring ←
-    withBacktracking (token ':' *> some <$> (capture <| dropMany <| tokenFilter (·.isAlphanum)))
+  let user ←
+    captureStr <| dropMany <| tokenFilter (·.isAlphanum)
+  let pword : Option (Unit × Substring) ←
+    withBacktracking (token ':' *> some <$> (captureStr <| dropMany <| tokenFilter (·.isAlphanum)))
     <|> pure none
   let _ ← token '@'
-  return ⟨user.toString, pword.map (·.toString)⟩
+  return ⟨user.2.toString, pword.map (·.2.toString)⟩
 
 def Authority.Hostname.parse : Parser Authority.Hostname := do
-  let str ← capture <| dropMany <| tokenFilter (fun c => c.isAlphanum || c = '-' || c = '.')
-  return str.toString
+  let str ← captureStr <| dropMany <| tokenFilter (fun c => c.isAlphanum || c = '-' || c = '.')
+  return str.2.toString
 
 def Authority.Port.parse : Parser Authority.Port := do
   let _ ← token ':'
-  let digs ← capture <| dropMany <| tokenFilter (·.isDigit)
-  match digs.toString.toNat? with
+  let digs ← captureStr <| dropMany <| tokenFilter (·.isDigit)
+  match digs.2.toString.toNat? with
   | none =>
     throwUnexpectedWithMessage none s!"BUG: captured non-digit??: {digs}"
   | some num =>
@@ -185,7 +185,7 @@ def Path.allowedSegChars : ByteArray :=
     else 0
   )
 
-@[simp] theorem Path.allowedSegChars_size : Path.allowedSegChars.size = 256 := by
+theorem Path.allowedSegChars_size : Path.allowedSegChars.size = 256 := by
   simp [ByteArray.size, allowedSegChars]
 
 def Path.pctEnc : Parser Char := do
@@ -197,28 +197,27 @@ def Path.pctEnc : Parser Char := do
 
 def Path.parse : Parser Path := do
   let parts ← takeMany <|
-    token '/' *> (capture <| dropMany <|
+    token '/' *> (captureStr <| dropMany <|
       (tokenFilter (fun c =>
         if h : c.toNat < 256 then
-          have := by rw [←Path.allowedSegChars_size] at h; exact h
-          Path.allowedSegChars[c.toNat] > 0
+          Path.allowedSegChars[c.toNat]'(Path.allowedSegChars_size ▸ h) > 0
         else
           false
       )
       <|>
       Path.pctEnc)
     )
-  return parts.map (·.toString)
+  return parts.map (·.2.toString)
 
 def Query.parse : Parser Query := do
   let _ ← token '?'
-  let str ← capture <| dropMany <| tokenFilter (fun c => c != '#')
-  return str.toString
+  let str ← captureStr <| dropMany <| tokenFilter (fun c => c != '#')
+  return str.2.toString
 
 def Fragment.parse : Parser Fragment := do
   let _ ← token '#'
-  let str ← capture <| dropMany anyToken
-  return str.toString
+  let str ← captureStr <| dropMany anyToken
+  return str.2.toString
 
 def parse : Parser URI := do
   let scheme ← option? <| withBacktracking do
@@ -236,5 +235,3 @@ def fromString? (s : String) : Option URI :=
   | .ok ss u =>
     if ss.isEmpty then some u else none
   | _ => none
-
-#eval fromString? "https://api.github.com" |>.map (·.appendPath #["hi"])

lake-manifest.json

@@ -1,43 +1,41 @@
-{"version": 5,
- "packagesDir": "lake-packages",
+{"version": 7,
+ "packagesDir": ".lake/packages",
  "packages":
- [{"git":
-   {"url": "https://github.com/fgdorais/lean4-parser",
-    "subDir?": null,
-    "rev": "2d59ec7dcd5e36ed2e2fc8ea9dd06abe957cdb76",
-    "opts": {},
-    "name": "Parser",
-    "inputRev?": "main",
-    "inherited": false}},
-  {"git":
-   {"url": "https://github.com/gebner/quote4",
-    "subDir?": null,
-    "rev": "e75daed95ad1c92af4e577fea95e234d7a8401c1",
-    "opts": {},
-    "name": "Qq",
-    "inputRev?": "master",
-    "inherited": false}},
-  {"git":
-   {"url": "https://github.com/fgdorais/lean4-unicode-basic",
-    "subDir?": null,
-    "rev": "2491e781ae478b6e6f1d86a7157f1c58fc50f895",
-    "opts": {},
-    "name": "UnicodeBasic",
-    "inputRev?": "main",
-    "inherited": true}},
-  {"git":
-   {"url": "https://github.com/leanprover/std4",
-    "subDir?": null,
-    "rev": "54da53d93077d8bd1e3f0a9d318d50387fed1fd6",
-    "opts": {},
-    "name": "Std",
-    "inputRev?": "main",
-    "inherited": true}},
-  {"git":
-   {"url": "https://github.com/leanprover/std4",
-    "subDir?": null,
-    "rev": "ba5e5e3af519b4fc5221ad0fa4b2c87276f1d323",
-    "opts": {},
-    "name": "std",
-    "inputRev?": "main",
-    "inherited": false}}]}
+ [{"url": "https://github.com/gebner/quote4",
+   "type": "git",
+   "subDir": null,
+   "rev": "ccba5d35d07a448fab14c0e391c8105df6e2564c",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/std4",
+   "type": "git",
+   "subDir": null,
+   "rev": "7d065f253ed92e9c3b45751cdfc52bc1e9507561",
+   "name": "std",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/fgdorais/lean4-unicode-basic",
+   "type": "git",
+   "subDir": null,
+   "rev": "8603bb1d0d5edae780e3a85a0398fd83dbbb80a3",
+   "name": "UnicodeBasic",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/fgdorais/lean4-parser",
+   "type": "git",
+   "subDir": null,
+   "rev": "df99295b089c215baa7b2c5d5ef5359ba3283115",
+   "name": "Parser",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": false,
+   "configFile": "lakefile.lean"}],
+ "name": "Http",
+ "lakeDir": ".lake"}

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.0.0
+leanprover/lean4:v4.5.0-rc1