WIP

Author: TwoFX

src/Init/Data/String/Repr.lean

@@ -39,7 +39,7 @@ Examples:
  * `"0xff".toInt? = none`
 -/
 def String.toInt? (s : String) : Option Int := do
-  if s.get 0 = '-' then do
+  if s.front = '-' then do
     let v ← (s.toSubstring.drop 1).toNat?;
     pure <| - Int.ofNat v
   else
@@ -67,7 +67,7 @@ Examples:
  * `"0xff".isInt = false`
 -/
 def String.isInt (s : String) : Bool :=
-  if s.get 0 = '-' then
+  if s.front = '-' then
     (s.toSubstring.drop 1).isNat
   else
     s.isNat

src/Init/Data/String/Stream.lean

@@ -12,6 +12,6 @@ public import Init.Data.Stream
 public instance : Std.Stream Substring Char where
   next? s :=
     if s.startPos < s.stopPos then
-      some (s.str.get s.startPos, { s with startPos := s.str.next s.startPos })
+      some (s.startPos.get s.str, { s with startPos := s.startPos.next s.str })
     else
       none

src/lake/Lake/Util/Cli.lean

@@ -69,27 +69,27 @@ variable [Monad m] [MonadStateOf ArgList m]
 
 /-- Process a short option of the form `-x=arg`. -/
 @[inline] public def shortOptionWithEq (handle : Char → m α) (opt : String) : m α := do
-  consArg (opt.drop 3); handle (opt.get ⟨1⟩)
+  consArg (opt.drop 3); handle (String.Pos.Raw.get opt ⟨1⟩)
 
 /-- Process a short option of the form `"-x arg"`. -/
 @[inline] public def shortOptionWithSpace (handle : Char → m α) (opt : String) : m α := do
-  consArg <| opt.drop 2 |>.trimLeft; handle (opt.get ⟨1⟩)
+  consArg <| opt.drop 2 |>.trimLeft; handle (String.Pos.Raw.get opt ⟨1⟩)
 
 /-- Process a short option of the form `-xarg`. -/
 @[inline] public def shortOptionWithArg (handle : Char → m α) (opt : String) : m α := do
-  consArg (opt.drop 2); handle (opt.get ⟨1⟩)
+  consArg (opt.drop 2); handle (String.Pos.Raw.get opt ⟨1⟩)
 
 /-- Process a multiple short options grouped together (ex. `-xyz` as `x`, `y`, `z`). -/
 @[inline] public def multiShortOption (handle : Char → m PUnit) (opt : String) : m PUnit := do
   let rec loop (p : String.Pos.Raw) := do
-    if h : opt.atEnd p then
+    if h : p.atEnd opt then
       return
     else
-      handle (opt.get' p h)
-      loop (opt.next' p h)
+      handle (p.get' opt h)
+      loop (p.next' opt h)
   termination_by opt.utf8ByteSize - p.byteIdx
   decreasing_by
-    simp [String.atEnd] at h
+    simp [String.Pos.Raw.atEnd] at h
     apply Nat.sub_lt_sub_left h
     exact String.Pos.Raw.byteIdx_lt_byteIdx_next opt p
   loop ⟨1⟩
@@ -100,17 +100,17 @@ variable [Monad m] [MonadStateOf ArgList m]
   if pos = opt.endPos then
     handle opt
   else do
-    consArg <| opt.extract (opt.next pos) opt.endPos
-    handle <| opt.extract 0 pos
+    consArg <| (pos.next opt).extract opt opt.endPos
+    handle <| String.Pos.Raw.extract opt 0 pos
 
 /-- Splits a long option of the form `--long=arg` into `--long` and `arg`. -/
 @[inline] public def longOptionOrEq (handle : String → m α) (opt : String) : m α :=
   let pos := opt.posOf '='
   if pos = opt.endPos then
     handle opt
   else do
-    consArg <| opt.extract (opt.next pos) opt.endPos
-    handle <| opt.extract 0 pos
+    consArg <| (pos.next opt).extract opt opt.endPos
+    handle <| String.Pos.Raw.extract opt 0 pos
 
 /-- Process a long option  of the form `--long`, `--long=arg`, `"--long arg"`. -/
 @[inline] public def longOption (handle : String → m α) : String → m α :=
@@ -122,9 +122,9 @@ variable [Monad m] [MonadStateOf ArgList m]
   (opt : String)
 : m α :=
   if opt.length == 2 then -- `-x`
-    shortHandle (opt.get ⟨1⟩)
+    shortHandle (String.Pos.Raw.get opt ⟨1⟩)
   else -- `-c(.+)`
-    match opt.get ⟨2⟩ with
+    match String.Pos.Raw.get opt ⟨2⟩ with
     | '=' => -- `-x=arg`
       shortOptionWithEq shortHandle opt
     | ' ' => -- `"-x arg"`
@@ -138,7 +138,7 @@ An option is an argument of length > 1 starting with a dash (`-`).
 An option may consume additional elements of the argument list.
 -/
 @[inline] public def option (handlers : OptionHandlers m α) (opt : String) : m α :=
-  if opt.get ⟨1⟩ == '-' then -- `--(.*)`
+  if String.Pos.Raw.get opt ⟨1⟩ == '-' then -- `--(.*)`
     longOption handlers.long opt
   else
     shortOption handlers.short handlers.longShort opt
@@ -148,7 +148,7 @@ public def processLeadingOption (handle : String → m PUnit) : m PUnit := do
   match (← getArgs) with
   | [] => pure ()
   | arg :: args =>
-    if arg.length > 1 && arg.get 0 == '-' then -- `-(.+)`
+    if arg.length > 1 && String.Pos.Raw.get arg 0 == '-' then -- `-(.+)`
       setArgs args
       handle arg
 
@@ -159,7 +159,7 @@ Consumes empty leading arguments in the argument list.
 public partial def processLeadingOptions (handle : String → m PUnit) : m PUnit := do
   if let arg :: args ← getArgs then
     let len := arg.length
-    if len > 1 && arg.get 0 == '-' then -- `-(.+)`
+    if len > 1 && String.Pos.Raw.get arg 0 == '-' then -- `-(.+)`
       setArgs args
       handle arg
       processLeadingOptions handle
@@ -173,7 +173,7 @@ public partial def collectArgs
 : m (Array String) := do
   if let some arg ← takeArg? then
     let len := arg.length
-    if len > 1 && arg.get 0 == '-' then -- `-(.+)`
+    if len > 1 && String.Pos.Raw.get arg 0 == '-' then -- `-(.+)`
       option arg
       collectArgs option args
     else if len == 0 then -- skip empty args