Zulip Chat Archive

Stream: new members

Topic: file io / string.to_nat


view this post on Zulip Logan Murphy (Dec 02 2020 at 15:44):

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.

view this post on Zulip Reid Barton (Dec 02 2020 at 15:47):

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

view this post on Zulip Reid Barton (Dec 02 2020 at 15:48):

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

view this post on Zulip Logan Murphy (Dec 02 2020 at 15:48):

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

view this post on Zulip Logan Murphy (Dec 02 2020 at 15:55):

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

view this post on Zulip Bryan Gin-ge Chen (Dec 02 2020 at 16:08):

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


Last updated: May 09 2021 at 19:11 UTC