From 9db688f4c24324db0cecb63c252e85f2620acda7 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 16 Aug 2018 17:05:31 -0700 Subject: [PATCH] fix(library/{vm/vm_io,init/io}): fix bugs and tests --- library/init/io.lean | 4 +--- src/library/tactic/tactic_state.cpp | 4 ++-- src/library/vm/vm_io.cpp | 8 ++++---- tests/lean/parsec1.lean | 8 ++++---- tests/lean/reader1.lean | 6 +++--- tests/lean/run/deriv.lean | 6 +++--- tests/lean/run/lirc1.lean | 3 +-- tests/lean/run/parser_ir1.lean | 7 +++---- 8 files changed, 21 insertions(+), 25 deletions(-) diff --git a/library/init/io.lean b/library/init/io.lean index 290b868478..bb208e2b40 100644 --- a/library/init/io.lean +++ b/library/init/io.lean @@ -202,13 +202,11 @@ prim.lift_ioe $ prim.iterate_ioe "" $ λ r, except_t.run $ do c ← h.get_line, return $ sum.inl (r ++ c) -- continue -/- def read_file (fname : string) (bin := ff) : m string := do h ← handle.mk fname mode.read bin, r ← h.read_to_end, - close h, + h.close, return r --/ def write_file (fname : string) (data : string) (bin := ff) : m unit := do h ← handle.mk fname mode.write bin, diff --git a/src/library/tactic/tactic_state.cpp b/src/library/tactic/tactic_state.cpp index 5f5e064b67..f35a7a2e72 100644 --- a/src/library/tactic/tactic_state.cpp +++ b/src/library/tactic/tactic_state.cpp @@ -824,8 +824,8 @@ vm_obj tactic_add_aux_decl(vm_obj const & n, vm_obj const & type, vm_obj const & } } -vm_obj tactic_unsafe_run_io(vm_obj const &, vm_obj const & a, vm_obj const &) { - return run_io(a); +vm_obj tactic_unsafe_run_io(vm_obj const &, vm_obj const & a, vm_obj const & s) { + return tactic::mk_success(run_io(a), s); } vm_obj io_run_tactic(vm_obj const &, vm_obj const & tac, vm_obj const &) { diff --git a/src/library/vm/vm_io.cpp b/src/library/vm/vm_io.cpp index 75ae10a6e2..383f508042 100644 --- a/src/library/vm/vm_io.cpp +++ b/src/library/vm/vm_io.cpp @@ -70,7 +70,7 @@ static vm_obj io_put_str(vm_obj const & str, vm_obj const &) { if ((get_global_ios().get_regular_stream() << to_string(str)).bad()) return mk_ioe_failure("io.put_str failed"); else - return mk_io_result(mk_vm_unit()); + return mk_ioe_result(mk_vm_unit()); } static vm_obj io_get_line(vm_obj const &) { @@ -280,11 +280,11 @@ static vm_obj io_process_wait(vm_obj const & ch, vm_obj const &) { } */ -/* (iterate : Π e (α β : Type), α → (α → io e (sum α β)) → io e β) */ -static vm_obj io_iterate(vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const & a, vm_obj const & fn, vm_obj const &) { +/* (iterate : Π (α β : Type), α → (α → io (sum α β)) → io β) */ +static vm_obj io_iterate(vm_obj const &, vm_obj const &, vm_obj const & a, vm_obj const & fn, vm_obj const &) { vm_obj r = a; while (true) { - vm_obj sum = invoke(fn, r, REAL_WORLD); + vm_obj sum = cfield(invoke(fn, r, REAL_WORLD), 0); if (cidx(sum) == 1) { return mk_io_result(cfield(sum, 0)); } else { diff --git a/tests/lean/parsec1.lean b/tests/lean/parsec1.lean index 4f9d29b5bf..c0aa0aaccc 100644 --- a/tests/lean/parsec1.lean +++ b/tests/lean/parsec1.lean @@ -1,18 +1,18 @@ -import init.io init.lean.parser.identifier init.lean.ir.parser init.lean.ir.format +import init.lean.parser.identifier init.lean.ir.parser init.lean.ir.format open lean.parser open lean.parser.monad_parsec -def test {α} [decidable_eq α] (p : parsec' α) (s : string) (e : α) : io unit := +def test {α} [decidable_eq α] (p : parsec' α) (s : string) (e : α) : eio unit := match parsec.parse p s with | except.ok a := if a = e then return () else io.print_ln "unexpected result" | except.error e := io.print_ln e -def test_failure {α} (p : parsec' α) (s : string) : io unit := +def test_failure {α} (p : parsec' α) (s : string) : eio unit := match parsec.parse p s with | except.ok a := io.print_ln "unexpected success" | except.error e := return () -def show_result {α} [has_to_string α] (p : parsec' α) (s : string) : io unit := +def show_result {α} [has_to_string α] (p : parsec' α) (s : string) : eio unit := match parsec.parse p s with | except.ok a := io.print_ln "result: " >> io.print_ln (repr $ to_string a) | except.error e := io.print_ln e diff --git a/tests/lean/reader1.lean b/tests/lean/reader1.lean index f4b784a010..cfb5ddc623 100644 --- a/tests/lean/reader1.lean +++ b/tests/lean/reader1.lean @@ -2,7 +2,7 @@ import init.lean.parser.reader.module init.io open lean.parser open lean.parser.reader -def show_result (p : lean.parser.reader) (s : string) : io unit := +def show_result (p : lean.parser.reader) (s : string) : eio unit := let (stx, errors) := p.parse ⟨⟩ s in when (stx.reprint ≠ s) ( io.print_ln "reprint fail:" *> @@ -49,10 +49,10 @@ end b" #eval (do { let (stx, _) := mixfix.reader.parse ⟨⟩ "prefix `+`:10 := _", some {root := stx, ..} ← pure $ reader.parse.view stx, - some stx ← pure $ mixfix.expand stx | io.fail "expand fail", + some stx ← pure $ mixfix.expand stx | throw "expand fail", io.print_ln stx, io.print_ln stx.reprint -} : io unit) +} : eio unit) -- slowly progressing... #eval do diff --git a/tests/lean/run/deriv.lean b/tests/lean/run/deriv.lean index aa2c673e78..f5e7c74940 100644 --- a/tests/lean/run/deriv.lean +++ b/tests/lean/run/deriv.lean @@ -78,18 +78,18 @@ def Expr.to_string : Expr → string instance : has_to_string Expr := ⟨Expr.to_string⟩ -meta def nest (f : Expr → io Expr) : nat → Expr → io Expr +meta def nest (f : Expr → eio Expr) : nat → Expr → eio Expr | 0 x := return x | (n+1) x := f x >>= nest n -meta def deriv (f : Expr) : io Expr := +meta def deriv (f : Expr) : eio Expr := do let d := d "x" f, io.put_str "count: ", io.put_str_ln (to_string (count f)), return d -meta def main : io unit := +meta def main : eio unit := do let x := Var "x", let f := pow x x, nest deriv 9 f, diff --git a/tests/lean/run/lirc1.lean b/tests/lean/run/lirc1.lean index 2696ebd588..58a37084d8 100644 --- a/tests/lean/run/lirc1.lean +++ b/tests/lean/run/lirc1.lean @@ -1,8 +1,7 @@ -import init.io import init.lean.ir.lirc open lean.ir -def comp (s : string) : io unit := +def comp (s : string) : eio unit := match lirc s with | except.ok r := io.print r | except.error e := io.print "Error: " >> io.print e diff --git a/tests/lean/run/parser_ir1.lean b/tests/lean/run/parser_ir1.lean index 8a8f339190..8a456f114f 100644 --- a/tests/lean/run/parser_ir1.lean +++ b/tests/lean/run/parser_ir1.lean @@ -1,4 +1,3 @@ -import init.io import init.lean.ir.parser init.lean.ir.format import init.lean.ir.elim_phi init.lean.ir.type_check import init.lean.ir.extract_cpp @@ -7,12 +6,12 @@ open lean.parser open lean.parser.monad_parsec open lean.ir -def check_decl (d : decl) : io unit := +def check_decl (d : decl) : eio unit := match type_check d with | except.ok _ := return () | except.error e := io.print_ln (to_string e) -def show_result (p : parsec' decl) (s : string) : io unit := +def show_result (p : parsec' decl) (s : string) : eio unit := match parsec.parse p s with | except.ok d := io.print_ln (lean.to_fmt d) >> check_decl d | except.error e := io.print_ln e @@ -44,7 +43,7 @@ end: #eval show_result (whitespace >> parse_def) IR2 -def tst_elim_phi (s : string) : io unit := +def tst_elim_phi (s : string) : eio unit := do (except.ok d) ← return $ parsec.parse (whitespace >> parse_def) s, check_decl d, io.print_ln (lean.to_fmt (elim_phi d))