file io / string.to_nat

Stream: new members

[Logan Murphy]

Trying to get lean to read a sequence of nat (not delimited by commas or anything) and put it into a list. Tried doing so by reading the file line by line, seems to work fine. But when I try to map the list of string's to a list nat it's giving me weird results. Any clue what I'm doing wrong?

import system.io
open tactic
variable α : Type

meta def read_line (f : io.handle) : tactic char_buffer :=
 do buf ←  tactic.unsafe_run_io (io.fs.get_line f),
 return buf

meta def main : io unit :=
do
 f ← io.mk_file_handle "src/foo.txt" io.mode.read,
 io.run_tactic $
 do list1 ←
  iterate_at_most 5 (do
    input ←  read_line f,
    str ← pure input.to_list.as_string,
    return str),
   list2 ← pure $ list.map string.to_nat list1,
   trace list1,
   trace list2

Produces the output

[1977
, 1802
, 1856
, 1309
, 2003
]
[19732, 17982, 18522, 13052, 19992]

The first list is the correct data, I have no clue where the data in the second list is coming from.

[Reid Barton]

looks like it's multiplying by 10 and subtracting 38 = 0 - \n

[Reid Barton]

which isn't exactly ideal, but try removing trailing newlines from the strings before passing them to string.to_nat

[Logan Murphy]

Yes, I was trying to figure out what the pattern was! Thanks Reid

[Logan Murphy]

Yes, this did it.

meta def main : io unit :=
do
 f ← io.mk_file_handle "src/foo.txt" io.mode.read,
 io.run_tactic $
 do list1 ←
  iterate_at_most 5 (do
    input ← read_line f,
    input ← pure input.pop_back,
    str ← pure input.to_list.as_string,
    return str),
   list2 ← pure $ list.map string.to_nat list1,
   trace list1,
   trace list2

[Bryan Gin-ge Chen]

Mario used the data.buffer.parser library in core Lean to write some nice functions for parsing in the Advent of Code thread.