From afd54039abaa616e5292cc69a904e440b0e489a3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 12 Sep 2018 17:30:37 -0700 Subject: [PATCH] chore(library): remove `>>`, we should use `*>` --- library/init/control/combinators.lean | 4 +- library/init/control/monad.lean | 8 - library/init/data/rbmap/basic.lean | 2 +- library/init/data/rbtree/basic.lean | 2 +- library/init/io.lean | 8 +- library/init/lean/ir/elim_phi.lean | 2 +- library/init/lean/ir/extract_cpp.lean | 172 +++++++++--------- library/init/lean/ir/lirc.lean | 6 +- library/init/lean/ir/parser.lean | 180 +++++++++---------- library/init/lean/ir/ssa_check.lean | 42 ++--- library/init/lean/ir/type_check.lean | 30 ++-- library/init/lean/name_mangling.lean | 4 +- library/init/lean/parser/identifier.lean | 4 +- library/init/lean/parser/module.lean | 2 +- library/init/lean/parser/parsec.lean | 8 +- library/init/lean/parser/string_literal.lean | 2 +- tests/lean/parsec1.lean | 28 +-- tests/lean/run/lirc1.lean | 2 +- tests/lean/run/parser_ir1.lean | 12 +- tests/lean/trace1.lean | 4 +- 20 files changed, 257 insertions(+), 265 deletions(-) diff --git a/library/init/control/combinators.lean b/library/init/control/combinators.lean index 1e0f1f887d..77d7ef9870 100644 --- a/library/init/control/combinators.lean +++ b/library/init/control/combinators.lean @@ -10,7 +10,7 @@ import init.control.monad init.control.alternative init.data.list.basic init.coe universes u v w def nat.mrepeat {m} [monad m] (n : nat) (f : nat → m unit) : m unit := -n.repeat (λ i a, a >> f i) (pure ()) +n.repeat (λ i a, a *> f i) (pure ()) def list.mmap {m : Type u → Type v} [monad m] {α : Type w} {β : Type u} (f : α → m β) : list α → m (list β) | [] := pure [] @@ -18,7 +18,7 @@ def list.mmap {m : Type u → Type v} [monad m] {α : Type w} {β : Type u} (f : def list.mmap' {m : Type u → Type v} [monad m] {α : Type w} {β : Type u} (f : α → m β) : list α → m punit | [] := pure ⟨⟩ -| (h :: t) := f h >> list.mmap' t +| (h :: t) := f h *> list.mmap' t def list.mfor {m : Type u → Type v} [monad m] {α : Type w} {β : Type u} (f : α → m β) : list α → m punit := list.mmap' f diff --git a/library/init/control/monad.lean b/library/init/control/monad.lean index 4aeca832e1..140f2058b2 100644 --- a/library/init/control/monad.lean +++ b/library/init/control/monad.lean @@ -14,16 +14,8 @@ class has_bind (m : Type u → Type v) := export has_bind (bind) -@[inline] def has_bind.and_then {α β : Type u} {m : Type u → Type v} [has_bind m] (x : m α) (y : m β) : m β := -do x, y - infixl ` >>= `:55 := bind -infixl ` >> `:55 := has_bind.and_then class monad (m : Type u → Type v) extends applicative m, has_bind m : Type (max (u+1) v) := (map := λ α β f x, x >>= pure ∘ f) (seq := λ α β f x, f >>= (<$> x)) - -/- Identical to has_bind.and_then, but it is not inlined. -/ -def has_bind.seq {α β : Type u} {m : Type u → Type v} [has_bind m] (x : m α) (y : m β) : m β := -do x, y diff --git a/library/init/data/rbmap/basic.lean b/library/init/data/rbmap/basic.lean index 6d4953d786..e2ae913b9e 100644 --- a/library/init/data/rbmap/basic.lean +++ b/library/init/data/rbmap/basic.lean @@ -45,7 +45,7 @@ def mfold {m : Type w → Type w'} [monad m] (f : α → β → δ → m δ) (mp mp.mfold (λ e, f e.1 e.2) d def mfor {m : Type w → Type w'} [monad m] (f : α → β → m δ) (mp : rbmap α β lt) : m punit := -mp.mfold (λ a b _, f a b >> pure ⟨⟩) ⟨⟩ +mp.mfold (λ a b _, f a b *> pure ⟨⟩) ⟨⟩ /- We don't assume β is inhabited when in membership predicate `mem` and diff --git a/library/init/data/rbtree/basic.lean b/library/init/data/rbtree/basic.lean index f3c73bce2b..4297ca1806 100644 --- a/library/init/data/rbtree/basic.lean +++ b/library/init/data/rbtree/basic.lean @@ -194,7 +194,7 @@ def mfold {m : Type v → Type w} [monad m] (f : α → β → m β) : rbtree α | ⟨t, _⟩ b := t.mfold f b def mfor {m : Type v → Type w} [monad m] (f : α → m β) (t : rbtree α lt) : m punit := -t.mfold (λ a _, f a >> pure ⟨⟩) ⟨⟩ +t.mfold (λ a _, f a *> pure ⟨⟩) ⟨⟩ def empty : rbtree α lt → bool | ⟨leaf, _⟩ := tt diff --git a/library/init/io.lean b/library/init/io.lean index c1a7551659..c27a574f50 100644 --- a/library/init/io.lean +++ b/library/init/io.lean @@ -82,7 +82,7 @@ def print {α} [has_to_string α] (s : α) : m unit := put_str ∘ to_string $ s def println {α} [has_to_string α] (s : α) : m unit := -print s >> put_str "\n" +print s *> put_str "\n" end namespace fs @@ -110,7 +110,7 @@ def handle.put_str (h : handle) (s : string) : m unit := h.write s def handle.put_str_ln (h : handle) (s : string) : m unit := -h.put_str s >> h.put_str "\n" +h.put_str s *> h.put_str "\n" def handle.read_to_end (h : handle) : m string := prim.lift_eio $ prim.iterate_eio "" $ λ r, do @@ -344,7 +344,7 @@ protected def bind : coroutine_io α δ β → (β → coroutine_io α δ γ) | yielded d c, h := -- have direct_subcoroutine_io c (mk k), { apply direct_subcoroutine.mk k a d, rw h }, pure $ yielded d (bind c f) --- using_well_founded { dec_tac := unfold_wf_rel >> process_lex (tactic.assumption) } +-- using_well_founded { dec_tac := unfold_wf_rel *> process_lex (tactic.assumption) } def pipe : coroutine_io α δ β → coroutine_io δ γ β → coroutine_io α γ β | (mk k₁) (mk k₂) := mk $ λ a, do @@ -358,7 +358,7 @@ def pipe : coroutine_io α δ β → coroutine_io δ γ β → coroutine_io α | yielded r k₂' := -- have direct_subcoroutine_io k₁' (mk k₁), { apply direct_subcoroutine.mk k₁ a d, rw h }, yielded r (pipe k₁' k₂') --- using_well_founded { dec_tac := unfold_wf_rel >> process_lex (tactic.assumption) } +-- using_well_founded { dec_tac := unfold_wf_rel *> process_lex (tactic.assumption) } instance : monad (coroutine_io α δ) := { pure := @coroutine_io.pure _ _, diff --git a/library/init/lean/ir/elim_phi.lean b/library/init/lean/ir/elim_phi.lean index 40fb27d89c..5dc17396ec 100644 --- a/library/init/lean/ir/elim_phi.lean +++ b/library/init/lean/ir/elim_phi.lean @@ -73,7 +73,7 @@ def decl.replace_vars : decl → elim_phi_m decl | other := pure other def elim_phi_aux (d : decl) : elim_phi_m decl := -group_vars d >> d.replace_vars +group_vars d *> d.replace_vars def elim_phi (d : decl) : decl := (elim_phi_aux d).run diff --git a/library/init/lean/ir/extract_cpp.lean b/library/init/lean/ir/extract_cpp.lean index e7c44cdd0c..2a3beba95a 100644 --- a/library/init/lean/ir/extract_cpp.lean +++ b/library/init/lean/ir/extract_cpp.lean @@ -51,10 +51,10 @@ def emit_line : extract_m unit := emit "\n" def paren {α} (a : extract_m α) : extract_m α := -emit "(" >> a <* emit ")" +emit "(" *> a <* emit ")" def comma (a b : extract_m unit) : extract_m unit := -a >> emit ", " >> b +a *> emit ", " *> b local infix `<+>`:65 := comma @@ -98,7 +98,7 @@ emit (type2cpp ty) def emit_sep_aux {α} (f : α → extract_m unit) (sep : string) : list α → extract_m unit | [] := pure () | [a] := f a -| (a::as) := f a >> emit sep >> emit " " >> emit_sep_aux as +| (a::as) := f a *> emit sep *> emit " " *> emit_sep_aux as def emit_sep {α} (l : list α) (f : α → extract_m unit) (sep := ",") : extract_m unit := emit_sep_aux f sep l @@ -107,7 +107,7 @@ def emit_var_list (xs : list var) : extract_m unit := emit_sep xs emit_var def emit_template_params (ts : list type) : extract_m unit := -emit "<" >> emit_sep ts emit_type >> emit ">" +emit "<" *> emit_sep ts emit_type *> emit ">" def emit_template_param (t : type) : extract_m unit := emit_template_params [t] @@ -115,66 +115,66 @@ emit_template_params [t] def emit_return : list result → extract_m unit | [] := emit "void" | [r] := emit_type r.ty -| rs := emit "std::tuple" >> emit_template_params (rs.map result.ty) +| rs := emit "std::tuple" *> emit_template_params (rs.map result.ty) def emit_arg_list (args : list arg) : extract_m unit := -emit_sep args $ λ a, emit_type a.ty >> emit " " >> emit_var a.n +emit_sep args $ λ a, emit_type a.ty *> emit " " *> emit_var a.n /-- Emit end-of-statement -/ def emit_eos : extract_m unit := -emit ";" >> emit_line +emit ";" *> emit_line def emit_return_vars : list var → extract_m unit | [] := pure () | [x] := emit_var x -| xs := emit "std::make_tuple" >> paren(emit_var_list xs) +| xs := emit "std::make_tuple" *> paren(emit_var_list xs) def emit_cases : list blockid → nat → extract_m unit | [] n := throw "ill-formed case terminator" -| [b] n := emit "default: goto " >> emit_blockid b >> emit_eos -| (b::bs) n := emit "case " >> emit n >> emit ": goto " >> emit_blockid b >> emit_eos >> emit_cases bs (n+1) +| [b] n := emit "default: goto " *> emit_blockid b *> emit_eos +| (b::bs) n := emit "case " *> emit n *> emit ": goto " *> emit_blockid b *> emit_eos *> emit_cases bs (n+1) def emit_case : var → list blockid → extract_m unit -| x [b] := emit "goto " >> emit_blockid b >> emit_eos +| x [b] := emit "goto " *> emit_blockid b *> emit_eos | x [b₁,b₂] := do env ← read, (match env.ctx.find x with - | some type.bool := emit "if (" >> emit_var x >> emit ") goto " >> emit_blockid b₂ >> emit "; else goto " >> emit_blockid b₁ - | some type.uint32 := emit "if (" >> emit_var x >> emit " == 0) goto " >> emit_blockid b₁ >> emit "; else goto " >> emit_blockid b₂ + | some type.bool := emit "if (" *> emit_var x *> emit ") goto " *> emit_blockid b₂ *> emit "; else goto " *> emit_blockid b₁ + | some type.uint32 := emit "if (" *> emit_var x *> emit " == 0) goto " *> emit_blockid b₁ *> emit "; else goto " *> emit_blockid b₂ | _ := throw "ill-formed case"), emit_eos | x bs := do env ← read, emit "switch ", paren (emit_var x), - emit " {" >> emit_line >> emit_cases bs 0 >> emit "}" >> emit_line + emit " {" *> emit_line *> emit_cases bs 0 *> emit "}" *> emit_line def emit_terminator (term : terminator) : extract_m unit := term.decorate_error $ match term with -| (terminator.jmp b) := emit "goto " >> emit_blockid b >> emit_eos -| (terminator.ret xs) := emit "return " >> emit_return_vars xs >> emit_eos +| (terminator.jmp b) := emit "goto " *> emit_blockid b *> emit_eos +| (terminator.ret xs) := emit "return " *> emit_return_vars xs *> emit_eos | (terminator.case x bs) := emit_case x bs def emit_call_lhs : list var → extract_m unit | [] := pure () -| [x] := emit_var x >> emit " = " -| xs := emit "std::tie" >> paren(emit_var_list xs) >> emit " = " +| [x] := emit_var x *> emit " = " +| xs := emit "std::tie" *> paren(emit_var_list xs) *> emit " = " def emit_type_size (ty : type) : extract_m unit := -emit "sizeof" >> paren(emit_type ty) +emit "sizeof" *> paren(emit_type ty) /-- Emit `op(x)` -/ def emit_op_x (op : string) (x : var) : extract_m unit := -emit op >> paren (emit_var x) +emit op *> paren (emit_var x) /-- Emit `x := y op z` -/ def emit_infix (x y z : var) (op : string) : extract_m unit := -emit_var x >> emit " = " >> emit_var y >> emit " " >> emit op >> emit " " >> emit_var z +emit_var x *> emit " = " *> emit_var y *> emit " " *> emit op *> emit " " *> emit_var z /- Emit `x := big_op(y, z)` -/ def emit_big_binop (x y z : var) (big_op : string) : extract_m unit := -emit_var x >> emit " = " >> emit big_op >> paren (emit_var y <+> emit_var z) +emit_var x *> emit " = " *> emit big_op *> paren (emit_var y <+> emit_var z) def emit_arith (t : type) (x y z : var) (op : string) (big_op : string) : extract_m unit := match t with @@ -214,18 +214,18 @@ match op with | assign_binop.ine := emit_big_binop x y z "lean::int_ne" | assign_binop.array_read := (match t with - | type.object := emit_var x >> emit " = lean::array_obj" >> paren (emit_var y <+> emit_var z) - | _ := emit_var x >> emit " = lean::sarray_data" >> emit_template_param t >> paren (emit_var y <+> emit_var z)) + | type.object := emit_var x *> emit " = lean::array_obj" *> paren (emit_var y <+> emit_var z) + | _ := emit_var x *> emit " = lean::sarray_data" *> emit_template_param t *> paren (emit_var y <+> emit_var z)) | assign_binop.array_push := do env ← read, emit_var x, emit " = ", if env.ctx.find z = some type.object then emit "lean::array_push" else emit "lean::sarray_push", paren(emit_var y <+> emit_var z) -| assign_binop.string_push := emit_var x >> emit " = lean::string_push" >> paren (emit_var y <+> emit_var z) -| assign_binop.string_append := emit_var x >> emit " = lean::string_append" >> paren (emit_var y <+> emit_var z) +| assign_binop.string_push := emit_var x *> emit " = lean::string_push" *> paren (emit_var y <+> emit_var z) +| assign_binop.string_append := emit_var x *> emit " = lean::string_append" *> paren (emit_var y <+> emit_var z) /-- Emit `x := op(y)` -/ def emit_x_op_y (x : var) (op : string) (y : var) : extract_m unit := -emit_var x >> emit " = " >> emit op >> paren(emit_var y) +emit_var x *> emit " = " *> emit op *> paren(emit_var y) def assign_unop2cpp (t : type) : assign_unop → string | assign_unop.not := if t = type.bool then "!" else "~" @@ -248,7 +248,7 @@ def assign_unop2cpp (t : type) : assign_unop → string | assign_unop.tag := "lean::obj_tag" def emit_assign_unop (x : var) (t : type) (op : assign_unop) (y : var) : extract_m unit := -emit_var x >> emit " = " >> emit (assign_unop2cpp t op) >> paren(emit_var y) +emit_var x *> emit " = " *> emit (assign_unop2cpp t op) *> paren(emit_var y) def emit_num_suffix : type → extract_m unit | type.uint32 := emit "u" @@ -258,17 +258,17 @@ def emit_num_suffix : type → extract_m unit def emit_assign_lit (x : var) (t : type) (l : literal) : extract_m unit := match l with -| literal.bool tt := emit_var x >> emit " = true" -| literal.bool ff := emit_var x >> emit " = false" -| literal.str s := emit_var x >> emit " = lean::mk_string" >> paren(emit (repr s)) -| literal.float v := emit_var x >> emit " = " >> emit v +| literal.bool tt := emit_var x *> emit " = true" +| literal.bool ff := emit_var x *> emit " = false" +| literal.str s := emit_var x *> emit " = lean::mk_string" *> paren(emit (repr s)) +| literal.float v := emit_var x *> emit " = " *> emit v | literal.num v := match t with | type.object := - emit_var x >> emit " = " >> - if v < uint32_sz then emit "lean::mk_nat_obj" >> paren(emit v >> emit "u") - else emit "lean::mk_mpz_core(lean::mpz(\"" >> emit v >> emit "\"))" - | _ := emit_var x >> emit " = " >> emit v >> emit_num_suffix t + emit_var x *> emit " = " *> + if v < uint32_sz then emit "lean::mk_nat_obj" *> paren(emit v *> emit "u") + else emit "lean::mk_mpz_core(lean::mpz(\"" *> emit v *> emit "\"))" + | _ := emit_var x *> emit " = " *> emit v *> emit_num_suffix t def unop2cpp : unop → string | unop.inc_ref := "lean::inc_ref" @@ -282,16 +282,16 @@ def unop2cpp : unop → string | unop.sarray_pop := "lean::sarray_pop" def emit_unop (op : unop) (x : var) : extract_m unit := -emit (unop2cpp op) >> paren(emit_var x) +emit (unop2cpp op) *> paren(emit_var x) def emit_apply (x : var) (ys : list var) : extract_m unit := match ys with | (f::as) := let n := as.length in if n > closure_max_args - then emit "{ obj * as[" >> emit n >> emit "] = {" >> emit_var_list as >> emit "}; " - >> emit_var x >> emit " = apply_m" >> paren(emit_var f <+> emit n <+> emit "as") >> emit "; }" - else emit_var x >> emit " = apply_" >> emit n >> paren(emit_var_list ys) + then emit "{ obj * as[" *> emit n *> emit "] = {" *> emit_var_list as *> emit "}; " + *> emit_var x *> emit " = apply_m" *> paren(emit_var f <+> emit n <+> emit "as") *> emit "; }" + else emit_var x *> emit " = apply_" *> emit n *> paren(emit_var_list ys) | _ := throw "ill-formed apply" def emit_closure (x : var) (f : fnid) (ys : list var) : extract_m unit := @@ -302,16 +302,16 @@ do env ← read, let arity := d.header.args.length, fname ← fid2cpp f, let fname := if arity > closure_max_args then "uncurry" ++ fname else fname, - emit "reinterpret_cast(" >> emit fname >> emit ")" <+> emit arity <+> emit ys.length, + emit "reinterpret_cast(" *> emit fname *> emit ")" <+> emit arity <+> emit ys.length, emit ")", - ys.mfoldl (λ i y, emit ";\nlean::closure_set_arg" >> paren (emit_var x <+> emit i <+> emit_var y) >> pure (i+1)) 0, + ys.mfoldl (λ i y, emit ";\nlean::closure_set_arg" *> paren (emit_var x <+> emit i <+> emit_var y) *> pure (i+1)) 0, pure () | none := throw "invalid closure" def emit_instr (ins : instr) : extract_m unit := ins.decorate_error $ (match ins with - | (instr.assign x t y) := emit_var x >> emit " = " >> emit_var y + | (instr.assign x t y) := emit_var x *> emit " = " *> emit_var y | (instr.assign_lit x t l) := emit_assign_lit x t l | (instr.assign_unop x t op y) := emit_assign_unop x t op y | (instr.assign_binop x t op y z) := emit_assign_binop x t op y z @@ -319,34 +319,34 @@ ins.decorate_error $ | (instr.call xs f ys) := do emit_call_lhs xs, c ← is_const f, if c then emit_global f - else (emit_fnid f >> paren(emit_var_list ys)) - | (instr.cnstr o t n sz) := emit_var o >> emit " = lean::alloc_cnstr" >> paren(emit t <+> emit n <+> emit sz) - | (instr.set o i x) := emit "lean::cnstr_set_obj" >> paren (emit_var o <+> emit i <+> emit_var x) - | (instr.get x o i) := emit_var x >> emit " = lean::cnstr_obj" >> paren(emit_var o <+> emit i) - | (instr.sset o d x) := emit "lean::cnstr_set_scalar" >> paren(emit_var o <+> emit d <+> emit_var x) - | (instr.sget x t o d) := emit_var x >> emit " = lean::cnstr_scalar" >> emit_template_param t >> paren(emit_var o <+> emit d) + else (emit_fnid f *> paren(emit_var_list ys)) + | (instr.cnstr o t n sz) := emit_var o *> emit " = lean::alloc_cnstr" *> paren(emit t <+> emit n <+> emit sz) + | (instr.set o i x) := emit "lean::cnstr_set_obj" *> paren (emit_var o <+> emit i <+> emit_var x) + | (instr.get x o i) := emit_var x *> emit " = lean::cnstr_obj" *> paren(emit_var o <+> emit i) + | (instr.sset o d x) := emit "lean::cnstr_set_scalar" *> paren(emit_var o <+> emit d <+> emit_var x) + | (instr.sget x t o d) := emit_var x *> emit " = lean::cnstr_scalar" *> emit_template_param t *> paren(emit_var o <+> emit d) | (instr.closure x f ys) := emit_closure x f ys | (instr.apply x ys) := emit_apply x ys - | (instr.array a sz c) := emit_var a >> emit " = lean::alloc_array" >> paren(emit_var sz <+> emit_var c) - | (instr.sarray a t sz c) := emit_var a >> emit " = lean::alloc_sarray" >> paren(emit_type_size t <+> emit_var sz <+> emit_var c) + | (instr.array a sz c) := emit_var a *> emit " = lean::alloc_array" *> paren(emit_var sz <+> emit_var c) + | (instr.sarray a t sz c) := emit_var a *> emit " = lean::alloc_sarray" *> paren(emit_type_size t <+> emit_var sz <+> emit_var c) | (instr.array_write a i v) := do env ← read, if env.ctx.find v = some type.object - then emit "lean::array_set_obj" >> paren(emit_var a <+> emit_var i <+> emit_var v) - else emit "lean::sarray_set_data" >> paren(emit_var a <+> emit_var i <+> emit_var v)) ->> emit_eos + then emit "lean::array_set_obj" *> paren(emit_var a <+> emit_var i <+> emit_var v) + else emit "lean::sarray_set_data" *> paren(emit_var a <+> emit_var i <+> emit_var v)) +*> emit_eos def emit_block (b : block) : extract_m unit := unless b.phis.empty (throw "failed to extract C++ code, definition contains phi nodes") ->> emit_blockid b.id >> emit ":" >> emit_line ->> b.instrs.mfor emit_instr ->> emit_terminator b.term +*> emit_blockid b.id *> emit ":" *> emit_line +*> b.instrs.mfor emit_instr +*> emit_terminator b.term def emit_header (h : header) : extract_m unit := -emit_return h.return >> emit " " >> emit_fnid h.name >> paren(emit_arg_list h.args) +emit_return h.return *> emit " " *> emit_fnid h.name *> paren(emit_arg_list h.args) def decl_local (x : var) (ty : type) : extract_m unit := -emit_type ty >> emit " " >> emit_var x >> emit_eos +emit_type ty *> emit " " *> emit_var x *> emit_eos def decl_locals (args : list arg) : extract_m unit := do env ← read, @@ -360,21 +360,21 @@ d.header.return.all (λ a, a.ty = type.object) && d.header.args.all (λ a, a.ty = type.object) def emit_uncurry_header (d : decl) : extract_m unit := -emit "obj* uncurry" >> emit_fnid d.header.name >> emit "(obj** as)" +emit "obj* uncurry" *> emit_fnid d.header.name *> emit "(obj** as)" def emit_uncurry (d : decl) : extract_m unit := let nargs := d.header.args.length in - emit_uncurry_header d >> emit " {\n" ->> emit "return " >> emit_fnid d.header.name >> paren (emit "as[0]" >> (nargs-1).mrepeat (λ i, emit ", " >> emit "as[" >> emit (i+1) >> emit "]")) >> emit_eos ->> emit "}\n" + emit_uncurry_header d *> emit " {\n" +*> emit "return " *> emit_fnid d.header.name *> paren (emit "as[0]" *> (nargs-1).mrepeat (λ i, emit ", " *> emit "as[" *> emit (i+1) *> emit "]")) *> emit_eos +*> emit "}\n" def emit_def_core (d : decl) : extract_m unit := d.decorate_error $ match d with | (decl.defn h bs) := - emit_header h >> emit " {" >> emit_line - >> decl_locals h.args >> bs.mfor emit_block - >> emit "}" >> emit_line >> + emit_header h *> emit " {" *> emit_line + *> decl_locals h.args *> bs.mfor emit_block + *> emit "}" *> emit_line *> when (need_uncurry d) (emit_uncurry d) | _ := pure () @@ -398,21 +398,21 @@ do env ← read, used.mfor (λ fid, match env.cfg.env fid with | some d := do unless (env.cfg.external_names fid = none) (emit "extern \"C\" "), - emit_header d.header >> emit ";\n" >> when (need_uncurry d) (emit_uncurry_header d >> emit ";\n") + emit_header d.header *> emit ";\n" *> when (need_uncurry d) (emit_uncurry_header d *> emit ";\n") | _ := pure ()) def emit_global_var_decls (ds : list decl) : extract_m unit := ds.mfor $ λ d, when d.header.is_const $ - emit_type d.header.return.head.ty >> emit " " >> emit_global d.header.name >> emit ";\n" + emit_type d.header.return.head.ty *> emit " " *> emit_global d.header.name *> emit ";\n" def emit_initialize_proc (ds : list decl) : extract_m unit := do env ← read, emit "void ", emit initialize_prefix, emit env.cfg.unit_name, emit "() {\n", emit "if (_G_initialized) return;\n", emit "_G_initialized = true;\n", - env.cfg.unit_deps.mfor $ λ dep, emit initialize_prefix >> emit dep >> emit "();\n", + env.cfg.unit_deps.mfor $ λ dep, emit initialize_prefix *> emit dep *> emit "();\n", ds.mfor $ λ d, when d.header.is_const $ - emit_global d.header.name >> emit " = " >> emit_fnid d.header.name >> emit "();\n", + emit_global d.header.name *> emit " = " *> emit_fnid d.header.name *> emit "();\n", emit "}\n" def emit_finalize_proc (ds : list decl) : extract_m unit := @@ -420,9 +420,9 @@ do env ← read, emit "void ", emit finalize_prefix, emit env.cfg.unit_name, emit "() {\n", emit "if (_G_finalized) return;\n", emit "_G_finalized = true;\n", - env.cfg.unit_deps.mfor $ λ dep, emit finalize_prefix >> emit dep >> emit "();\n", + env.cfg.unit_deps.mfor $ λ dep, emit finalize_prefix *> emit dep *> emit "();\n", ds.mfor $ λ d, when (d.header.is_const && d.header.return.head.ty = type.object) $ - emit "if (!is_scalar(" >> emit_global d.header.name >> emit ")) lean::dec_ref(" >> emit_global d.header.name >> emit ");\n", + emit "if (!is_scalar(" *> emit_global d.header.name *> emit ")) lean::dec_ref(" *> emit_global d.header.name *> emit ");\n", emit "}\n" def emit_main_proc : extract_m unit := @@ -432,12 +432,12 @@ do env ← read, (match env.cfg.env fid with | some d := unless (d.header.args.length = 0) (throw $ "invalid main function '" ++ to_string fid ++ "', it must not take any arguments") - >> unless (d.header.return.length = 1 && d.header.return.head.ty = type.int32) (throw $ "invalid main function '" ++ to_string fid ++ "', return type must be int32") - >> emit "int main() {\n" - >> emit initialize_prefix >> emit env.cfg.unit_name >> emit "();\n" - >> emit "int r = " >> emit_fnid fid >> emit "();\n" - >> emit finalize_prefix >> emit env.cfg.unit_name >> emit "();\n" - >> emit "return r;\n}\n" + *> unless (d.header.return.length = 1 && d.header.return.head.ty = type.int32) (throw $ "invalid main function '" ++ to_string fid ++ "', return type must be int32") + *> emit "int main() {\n" + *> emit initialize_prefix *> emit env.cfg.unit_name *> emit "();\n" + *> emit "int r = " *> emit_fnid fid *> emit "();\n" + *> emit finalize_prefix *> emit env.cfg.unit_name *> emit "();\n" + *> emit "return r;\n}\n" | none := throw ("unknown main function '" ++ to_string fid ++ "'")) | none := pure () @@ -448,14 +448,14 @@ open cpp def extract_cpp (ds : list decl) (cfg : extract_cpp_config := {}) : except format string := let out := file_header cfg.runtime_dir ++ "\n" in run (emit_used_headers ds - >> emit "static bool _G_initialized = false;\n" - >> emit "static bool _G_finalized = false;\n" - >> emit_global_var_decls ds - >> emit_initialize_proc ds - >> emit_finalize_proc ds - >> ds.mfor emit_def - >> emit_main_proc - >> get) + *> emit "static bool _G_initialized = false;\n" + *> emit "static bool _G_finalized = false;\n" + *> emit_global_var_decls ds + *> emit_initialize_proc ds + *> emit_finalize_proc ds + *> ds.mfor emit_def + *> emit_main_proc + *> get) {cfg := cfg} out end ir diff --git a/library/init/lean/ir/lirc.lean b/library/init/lean/ir/lirc.lean index dd22543564..f02677615a 100644 --- a/library/init/lean/ir/lirc.lean +++ b/library/init/lean/ir/lirc.lean @@ -20,7 +20,7 @@ open lean.parser.monad_parsec def parse_input_aux : nat → list decl → fnid2string → parsec' (list decl × fnid2string) | 0 ds m := pure (ds.reverse, m) | (n+1) ds m := - (eoi >> pure (ds.reverse, m)) + (eoi *> pure (ds.reverse, m)) <|> (do cid ← (do symbol "[", n ← lexeme $ c_identifier, symbol "]", pure (some n)) <|> pure none, d ← parse_decl, @@ -29,12 +29,12 @@ def parse_input_aux : nat → list decl → fnid2string → parsec' (list decl | none := parse_input_aux n (d::ds) m) def parse_input (s : string) : except format (list decl × fnid2string) := -match parsec.parse (whitespace >> parse_input_aux s.length [] mk_fnid2string) s with +match parsec.parse (whitespace *> parse_input_aux s.length [] mk_fnid2string) s with | except.ok r := pure r | except.error m := throw m.to_string def check (env : environment) (ssa : bool) (d : decl) : except format unit := -when ssa (d.valid_ssa >> pure ()) >> check_blockids d >> type_check d env >> pure () +when ssa (d.valid_ssa *> pure ()) *> check_blockids d *> type_check d env *> pure () local attribute [instance] name.has_lt_quick diff --git a/library/init/lean/ir/parser.lean b/library/init/lean/ir/parser.lean index ca486d73fe..36fbcd1c7c 100644 --- a/library/init/lean/ir/parser.lean +++ b/library/init/lean/ir/parser.lean @@ -14,90 +14,90 @@ open lean.parser open lean.parser.monad_parsec def symbol (s : string) : parsec' unit := -(str s >> whitespace) ("'" ++ s ++ "'") +(str s *> whitespace) ("'" ++ s ++ "'") def keyword (s : string) : parsec' unit := -(try $ str s >> not_followed_by_sat is_id_rest >> whitespace) ("'" ++ s ++ "'") +(try $ str s *> not_followed_by_sat is_id_rest *> whitespace) ("'" ++ s ++ "'") def parse_type : parsec' type := - (keyword "bool" >> pure type.bool) -<|> (keyword "byte" >> pure type.byte) -<|> (keyword "uint16" >> pure type.uint16) -<|> (keyword "uint32" >> pure type.uint32) -<|> (keyword "uint64" >> pure type.uint64) -<|> (keyword "usize" >> pure type.usize) -<|> (keyword "int16" >> pure type.int16) -<|> (keyword "int32" >> pure type.int32) -<|> (keyword "int64" >> pure type.int64) -<|> (keyword "float" >> pure type.float) -<|> (keyword "double" >> pure type.double) -<|> (keyword "object" >> pure type.object) + (keyword "bool" *> pure type.bool) +<|> (keyword "byte" *> pure type.byte) +<|> (keyword "uint16" *> pure type.uint16) +<|> (keyword "uint32" *> pure type.uint32) +<|> (keyword "uint64" *> pure type.uint64) +<|> (keyword "usize" *> pure type.usize) +<|> (keyword "int16" *> pure type.int16) +<|> (keyword "int32" *> pure type.int32) +<|> (keyword "int64" *> pure type.int64) +<|> (keyword "float" *> pure type.float) +<|> (keyword "double" *> pure type.double) +<|> (keyword "object" *> pure type.object) def parse_assign_unop : parsec' assign_unop := - (keyword "not" >> pure assign_unop.not) -<|> (keyword "neg" >> pure assign_unop.neg) -<|> (keyword "ineg" >> pure assign_unop.ineg) -<|> (keyword "nat2int" >> pure assign_unop.nat2int) -<|> (keyword "is_scalar" >> pure assign_unop.is_scalar) -<|> (keyword "is_shared" >> pure assign_unop.is_shared) -<|> (keyword "is_null" >> pure assign_unop.is_null) -<|> (keyword "array_copy" >> pure assign_unop.array_copy) -<|> (keyword "sarray_copy" >> pure assign_unop.sarray_copy) -<|> (keyword "box" >> pure assign_unop.box) -<|> (keyword "unbox" >> pure assign_unop.unbox) -<|> (keyword "cast" >> pure assign_unop.cast) -<|> (keyword "array_size" >> pure assign_unop.array_size) -<|> (keyword "sarray_size" >> pure assign_unop.sarray_size) -<|> (keyword "string_len" >> pure assign_unop.string_len) -<|> (keyword "succ" >> pure assign_unop.succ) -<|> (keyword "tag" >> pure assign_unop.tag) -<|> (keyword "tag_ref" >> pure assign_unop.tag_ref) + (keyword "not" *> pure assign_unop.not) +<|> (keyword "neg" *> pure assign_unop.neg) +<|> (keyword "ineg" *> pure assign_unop.ineg) +<|> (keyword "nat2int" *> pure assign_unop.nat2int) +<|> (keyword "is_scalar" *> pure assign_unop.is_scalar) +<|> (keyword "is_shared" *> pure assign_unop.is_shared) +<|> (keyword "is_null" *> pure assign_unop.is_null) +<|> (keyword "array_copy" *> pure assign_unop.array_copy) +<|> (keyword "sarray_copy" *> pure assign_unop.sarray_copy) +<|> (keyword "box" *> pure assign_unop.box) +<|> (keyword "unbox" *> pure assign_unop.unbox) +<|> (keyword "cast" *> pure assign_unop.cast) +<|> (keyword "array_size" *> pure assign_unop.array_size) +<|> (keyword "sarray_size" *> pure assign_unop.sarray_size) +<|> (keyword "string_len" *> pure assign_unop.string_len) +<|> (keyword "succ" *> pure assign_unop.succ) +<|> (keyword "tag" *> pure assign_unop.tag) +<|> (keyword "tag_ref" *> pure assign_unop.tag_ref) def parse_assign_binop : parsec' assign_binop := - (keyword "add" >> pure assign_binop.add) -<|> (keyword "sub" >> pure assign_binop.sub) -<|> (keyword "mul" >> pure assign_binop.mul) -<|> (keyword "div" >> pure assign_binop.div) -<|> (keyword "mod" >> pure assign_binop.mod) -<|> (keyword "iadd" >> pure assign_binop.iadd) -<|> (keyword "isub" >> pure assign_binop.isub) -<|> (keyword "imul" >> pure assign_binop.imul) -<|> (keyword "idiv" >> pure assign_binop.idiv) -<|> (keyword "imod" >> pure assign_binop.imod) -<|> (keyword "shl" >> pure assign_binop.shl) -<|> (keyword "shr" >> pure assign_binop.shr) -<|> (keyword "and" >> pure assign_binop.and) -<|> (keyword "or" >> pure assign_binop.or) -<|> (keyword "xor" >> pure assign_binop.xor) -<|> (keyword "le" >> pure assign_binop.le) -<|> (keyword "lt" >> pure assign_binop.lt) -<|> (keyword "eq" >> pure assign_binop.eq) -<|> (keyword "ne" >> pure assign_binop.ne) -<|> (keyword "ile" >> pure assign_binop.ile) -<|> (keyword "ilt" >> pure assign_binop.ilt) -<|> (keyword "ieq" >> pure assign_binop.ieq) -<|> (keyword "ine" >> pure assign_binop.ine) -<|> (keyword "array_read" >> pure assign_binop.array_read) -<|> (keyword "array_push" >> pure assign_binop.array_push) -<|> (keyword "string_push" >> pure assign_binop.string_push) -<|> (keyword "string_append" >> pure assign_binop.string_append) + (keyword "add" *> pure assign_binop.add) +<|> (keyword "sub" *> pure assign_binop.sub) +<|> (keyword "mul" *> pure assign_binop.mul) +<|> (keyword "div" *> pure assign_binop.div) +<|> (keyword "mod" *> pure assign_binop.mod) +<|> (keyword "iadd" *> pure assign_binop.iadd) +<|> (keyword "isub" *> pure assign_binop.isub) +<|> (keyword "imul" *> pure assign_binop.imul) +<|> (keyword "idiv" *> pure assign_binop.idiv) +<|> (keyword "imod" *> pure assign_binop.imod) +<|> (keyword "shl" *> pure assign_binop.shl) +<|> (keyword "shr" *> pure assign_binop.shr) +<|> (keyword "and" *> pure assign_binop.and) +<|> (keyword "or" *> pure assign_binop.or) +<|> (keyword "xor" *> pure assign_binop.xor) +<|> (keyword "le" *> pure assign_binop.le) +<|> (keyword "lt" *> pure assign_binop.lt) +<|> (keyword "eq" *> pure assign_binop.eq) +<|> (keyword "ne" *> pure assign_binop.ne) +<|> (keyword "ile" *> pure assign_binop.ile) +<|> (keyword "ilt" *> pure assign_binop.ilt) +<|> (keyword "ieq" *> pure assign_binop.ieq) +<|> (keyword "ine" *> pure assign_binop.ine) +<|> (keyword "array_read" *> pure assign_binop.array_read) +<|> (keyword "array_push" *> pure assign_binop.array_push) +<|> (keyword "string_push" *> pure assign_binop.string_push) +<|> (keyword "string_append" *> pure assign_binop.string_append) def parse_unop : parsec' unop := - (keyword "inc_ref" >> pure unop.inc_ref) -<|> (keyword "dec_ref" >> pure unop.dec_ref) -<|> (keyword "inc" >> pure unop.inc) -<|> (keyword "dec" >> pure unop.dec) -<|> (keyword "dec_sref" >> pure unop.dec_sref) -<|> (keyword "free" >> pure unop.free) -<|> (keyword "dealloc" >> pure unop.dealloc) -<|> (keyword "array_pop" >> pure unop.array_pop) -<|> (keyword "sarray_pop" >> pure unop.sarray_pop) + (keyword "inc_ref" *> pure unop.inc_ref) +<|> (keyword "dec_ref" *> pure unop.dec_ref) +<|> (keyword "inc" *> pure unop.inc) +<|> (keyword "dec" *> pure unop.dec) +<|> (keyword "dec_sref" *> pure unop.dec_sref) +<|> (keyword "free" *> pure unop.free) +<|> (keyword "dealloc" *> pure unop.dealloc) +<|> (keyword "array_pop" *> pure unop.array_pop) +<|> (keyword "sarray_pop" *> pure unop.sarray_pop) def parse_literal : parsec' literal := - (keyword "tt" >> pure (literal.bool tt)) -<|> (keyword "ff" >> pure (literal.bool ff)) + (keyword "tt" *> pure (literal.bool tt)) +<|> (keyword "ff" *> pure (literal.bool ff)) <|> (do n ← lexeme num "numeral", pure (literal.num n)) -<|> (do n ← (ch '-' >> lexeme num), pure (literal.num (- n))) +<|> (do n ← (ch '-' *> lexeme num), pure (literal.num (- n))) <|> literal.str <$> parse_string_literal def parse_uint16 : parsec' uint16 := @@ -142,7 +142,7 @@ def parse_typed_assignment (x : var) : parsec' instr := do symbol ":", ty ← parse_type, symbol ":=", - (keyword "sget" >> instr.sget x ty <$> parse_var <*> parse_usize) + (keyword "sget" *> instr.sget x ty <$> parse_var <*> parse_usize) <|> (instr.assign x ty <$> parse_var) <|> (instr.assign_unop x ty <$> parse_assign_unop <*> parse_var) <|> (instr.assign_binop x ty <$> parse_assign_binop <*> parse_var <*> parse_var) @@ -150,13 +150,13 @@ do symbol ":", def parse_untyped_assignment (x : var) : parsec' instr := do symbol ":=", - (keyword "closure" >> instr.closure x <$> parse_fnid <*> many parse_var) -<|> (keyword "apply" >> instr.apply x <$> many1 parse_var) -<|> (keyword "get" >> instr.get x <$> parse_var <*> parse_uint16) -<|> (keyword "call" >> instr.call [x] <$> parse_fnid <*> many parse_var) -<|> (keyword "cnstr" >> instr.cnstr x <$> parse_uint16 <*> parse_uint16 <*> parse_usize) -<|> (keyword "array" >> instr.array x <$> parse_var <*> parse_var) -<|> (keyword "sarray" >> instr.sarray x <$> parse_type <*> parse_var <*> parse_var) + (keyword "closure" *> instr.closure x <$> parse_fnid <*> many parse_var) +<|> (keyword "apply" *> instr.apply x <$> many1 parse_var) +<|> (keyword "get" *> instr.get x <$> parse_var <*> parse_uint16) +<|> (keyword "call" *> instr.call [x] <$> parse_fnid <*> many parse_var) +<|> (keyword "cnstr" *> instr.cnstr x <$> parse_uint16 <*> parse_uint16 <*> parse_usize) +<|> (keyword "array" *> instr.array x <$> parse_var <*> parse_var) +<|> (keyword "sarray" *> instr.sarray x <$> parse_type <*> parse_var <*> parse_var) def parse_assignment : parsec' instr := do x ← parse_var, @@ -165,10 +165,10 @@ do x ← parse_var, else parse_nary_call x def parse_instr : parsec' instr := - (keyword "array_write" >> instr.array_write <$> parse_var <*> parse_var <*> parse_var) -<|> (keyword "set" >> instr.set <$> parse_var <*> parse_uint16 <*> parse_var) -<|> (keyword "sset" >> instr.sset <$> parse_var <*> parse_usize <*> parse_var) -<|> (keyword "call" >> instr.call [] <$> parse_fnid <*> many parse_var) + (keyword "array_write" *> instr.array_write <$> parse_var <*> parse_var <*> parse_var) +<|> (keyword "set" *> instr.set <$> parse_var <*> parse_uint16 <*> parse_var) +<|> (keyword "sset" *> instr.sset <$> parse_var <*> parse_usize <*> parse_var) +<|> (keyword "call" *> instr.call [] <$> parse_fnid <*> many parse_var) <|> (instr.unop <$> parse_unop <*> parse_var) <|> parse_assignment @@ -178,9 +178,9 @@ do (x, ty) ← try $ do { x ← parse_var, symbol ":", ty ← parse_type, symbol pure {x := x, ty := ty, ys := ys} def parse_terminator : parsec' terminator := - (keyword "jmp" >> terminator.jmp <$> parse_blockid) -<|> (keyword "ret" >> terminator.ret <$> many parse_var) -<|> (keyword "case" >> terminator.case <$> parse_var <*> (symbol "[" >> sep_by1 parse_blockid (symbol ",") <* symbol "]")) + (keyword "jmp" *> terminator.jmp <$> parse_blockid) +<|> (keyword "ret" *> terminator.ret <$> many parse_var) +<|> (keyword "case" *> terminator.case <$> parse_var <*> (symbol "[" *> sep_by1 parse_blockid (symbol ",") <* symbol "]")) def parse_block : parsec' block := do id ← try (parse_blockid <* symbol ":"), @@ -197,17 +197,17 @@ do n ← parse_fnid, as ← if is_const then pure [] else many parse_arg, r ← if is_const then do symbol ":", t ← parse_type, pure [result.mk t] - else try (symbol ":" >> many1 (result.mk <$> parse_type)) <|> pure [], + else try (symbol ":" *> many1 (result.mk <$> parse_type)) <|> pure [], pure { name := n, args := as, return := r, is_const := is_const } def parse_def : parsec' decl := -keyword "def" >> decl.defn <$> parse_header ff <*> (symbol ":=" >> many parse_block) +keyword "def" *> decl.defn <$> parse_header ff <*> (symbol ":=" *> many parse_block) def parse_defconst : parsec' decl := -keyword "defconst" >> decl.defn <$> parse_header tt <*> (symbol ":=" >> many parse_block) +keyword "defconst" *> decl.defn <$> parse_header tt <*> (symbol ":=" *> many parse_block) def parse_external : parsec' decl := -keyword "external" >> decl.external <$> parse_header ff +keyword "external" *> decl.external <$> parse_header ff def parse_decl : parsec' decl := parse_def <|> parse_defconst <|> parse_external diff --git a/library/init/lean/ir/ssa_check.lean b/library/init/lean/ir/ssa_check.lean index 53007c2489..b5e18b0415 100644 --- a/library/init/lean/ir/ssa_check.lean +++ b/library/init/lean/ir/ssa_check.lean @@ -34,7 +34,7 @@ def phi.declare (p : phi) : reader_t blockid ssa_pre_m unit := p.decorate_error p.x.declare def block.declare_vars (b : block) : ssa_pre_m unit := -b.decorate_error $ (b.phis.mfor phi.declare >> b.instrs.mfor instr.declare_vars).run b.id +b.decorate_error $ (b.phis.mfor phi.declare *> b.instrs.mfor instr.declare_vars).run b.id def arg.declare (a : arg) : reader_t blockid ssa_pre_m unit := a.n.declare @@ -44,14 +44,14 @@ a.n.declare def decl.declare_vars : decl → ssa_pre_m unit | (decl.defn h (b::bs)) := /- We assume that arguments are declared in the first basic block. -/ - h.decorate_error $ (h.args.mfor arg.declare).run b.id >> b.declare_vars >> bs.mfor block.declare_vars + h.decorate_error $ (h.args.mfor arg.declare).run b.id *> b.declare_vars *> bs.mfor block.declare_vars | (decl.defn _ []) := throw "declaration must have at least one basic block" | _ := pure () /- Generate the mapping from variable to blockid for the given declaration. This function assumes `d` is in SSA. -/ def decl.var2blockid (d : decl) : except format var2blockid := -run (d.declare_vars >> get) mk_var2blockid +run (d.declare_vars *> get) mk_var2blockid @[reducible] def ssa_valid_m := except_t format (reader_t var2blockid (state_t var_set id)) @@ -83,22 +83,22 @@ do m ← read, def instr.valid_ssa (ins : instr) : ssa_valid_m unit := ins.decorate_error $ match ins with -| (instr.assign x _ y) := x.define >> y.defined +| (instr.assign x _ y) := x.define *> y.defined | (instr.assign_lit x _ _) := x.define -| (instr.assign_unop x _ _ y) := x.define >> y.defined -| (instr.assign_binop x _ _ y z) := x.define >> y.defined >> z.defined +| (instr.assign_unop x _ _ y) := x.define *> y.defined +| (instr.assign_binop x _ _ y z) := x.define *> y.defined *> z.defined | (instr.unop _ x) := x.defined -| (instr.call xs _ ys) := xs.mfor var.define >> ys.mfor var.defined +| (instr.call xs _ ys) := xs.mfor var.define *> ys.mfor var.defined | (instr.cnstr o _ _ _) := o.define -| (instr.set o _ x) := o.defined >> x.defined -| (instr.get x y _) := x.define >> y.defined -| (instr.sset o _ x) := o.defined >> x.defined -| (instr.sget x _ y _) := x.define >> y.defined -| (instr.closure x _ ys) := x.define >> ys.mfor var.defined -| (instr.apply x ys) := x.define >> ys.mfor var.defined -| (instr.array a sz c) := a.define >> sz.defined >> c.defined -| (instr.sarray x _ sz c) := x.define >> sz.defined >> c.defined -| (instr.array_write a i v) := a.defined >> i.defined >> v.defined +| (instr.set o _ x) := o.defined *> x.defined +| (instr.get x y _) := x.define *> y.defined +| (instr.sset o _ x) := o.defined *> x.defined +| (instr.sget x _ y _) := x.define *> y.defined +| (instr.closure x _ ys) := x.define *> ys.mfor var.defined +| (instr.apply x ys) := x.define *> ys.mfor var.defined +| (instr.array a sz c) := a.define *> sz.defined *> c.defined +| (instr.sarray x _ sz c) := x.define *> sz.defined *> c.defined +| (instr.array_write a i v) := a.defined *> i.defined *> v.defined def terminator.valid_ssa (term : terminator) : ssa_valid_m unit := term.decorate_error $ @@ -146,9 +146,9 @@ d.decorate_error $ do m ← d.var2blockid, match d with | decl.defn {args:=args, ..} (b::bs) := - (args.mfor arg.define >> block.valid_ssa_core b).run m - >> (bs.mfor block.valid_ssa_core).run m - >> pure m + (args.mfor arg.define *> block.valid_ssa_core b).run m + *> (bs.mfor block.valid_ssa_core).run m + *> pure m | _ := pure m /- Check blockids -/ @@ -179,11 +179,11 @@ def block.check_blockids (b : block) : blockid_check_m unit := b.term.check_blockids def decl.check_blockids : decl → blockid_check_m unit -| (decl.defn h bs) := h.decorate_error $ bs.mfor block.declare >> bs.mfor block.check_blockids +| (decl.defn h bs) := h.decorate_error $ bs.mfor block.declare *> bs.mfor block.check_blockids | _ := pure () def check_blockids (d : decl) : except format blockid_set := -(d.check_blockids >> get).run +(d.check_blockids *> get).run end ir end lean diff --git a/library/init/lean/ir/type_check.lean b/library/init/lean/ir/type_check.lean index 7fd6838bdc..82e6c2ae3e 100644 --- a/library/init/lean/ir/type_check.lean +++ b/library/init/lean/ir/type_check.lean @@ -133,7 +133,7 @@ def literal.check (l : literal) (t : type) : type_checker_m unit := match l with | literal.bool _ := unless (t = type.bool) invalid_literal | literal.str _ := unless (t = type.object) invalid_literal -| literal.num v := unless (is_nonfloat_arith_ty t) invalid_literal >> +| literal.num v := unless (is_nonfloat_arith_ty t) invalid_literal *> when (v < 0) (unless (is_signed_arith_ty t) invalid_literal) | literal.float _ := unless (t = type.float || t = type.double) invalid_literal @@ -145,7 +145,7 @@ do (env, _) ← read, def set_result_types : list var → list result → type_checker_m unit | [] [] := pure () -| (x::xs) (t::ts) := set_type x t.ty >> set_result_types xs ts +| (x::xs) (t::ts) := set_type x t.ty *> set_result_types xs ts | _ _ := throw "unexpected number of return values" def instr.infer_types (ins : instr) : type_checker_m unit := @@ -172,10 +172,10 @@ def arg.infer_types (a : arg) : type_checker_m unit := set_type a.n a.ty def block.infer_types (b : block) : type_checker_m unit := -b.decorate_error $ b.phis.mfor phi.infer_types >> b.instrs.mfor instr.infer_types +b.decorate_error $ b.phis.mfor phi.infer_types *> b.instrs.mfor instr.infer_types def decl.infer_types : decl → type_checker_m context -| (decl.defn h bs) := h.decorate_error $ h.args.mfor arg.infer_types >> bs.mfor block.infer_types >> get +| (decl.defn h bs) := h.decorate_error $ h.args.mfor arg.infer_types *> bs.mfor block.infer_types *> get | _ := get /-- Return context with the type of variables used in the given declaration. @@ -185,7 +185,7 @@ d.infer_types.run env d.header.return def check_arg_types : list var → list arg → type_checker_m unit | [] [] := pure () -| (x::xs) (t::ts) := check_type x t.ty >> check_arg_types xs ts +| (x::xs) (t::ts) := check_type x t.ty *> check_arg_types xs ts | _ _ := throw "unexpected number of arguments" /-- Check whether the given instruction is type correct or not. It assumes the context already contains @@ -200,25 +200,25 @@ match ins with | (instr.unop _ x) := check_type x type.object | (instr.call xs f ys) := do d ← get_decl f, check_arg_types ys d.header.args | (instr.cnstr o _ _ _) := pure () -| (instr.set o _ x) := check_type o type.object >> check_type x type.object +| (instr.set o _ x) := check_type o type.object *> check_type x type.object | (instr.get x o _) := check_type o type.object -| (instr.sset o _ x) := check_type o type.object >> check_ne_type x type.object -| (instr.sget x t o _) := check_type o type.object >> check_ne_type x type.object +| (instr.sset o _ x) := check_type o type.object *> check_ne_type x type.object +| (instr.sget x t o _) := check_type o type.object *> check_ne_type x type.object | (instr.closure x f ys) := do ys.mfor (flip check_type type.object), d ← get_decl f, unless (d.header.return.length = 1) $ throw "unexpected number of return values", unless (d.header.args.length ≥ ys.length) $ throw "too many arguments", d.header.args.mfor (λ a, unless (a.ty = type.object) $ throw "invalid closure, arguments must have type object") | (instr.apply x ys) := ys.mfor (flip check_type type.object) -| (instr.array a sz c) := check_type sz type.usize >> check_type c type.usize -| (instr.sarray a t sz c) := check_type sz type.usize >> check_type c type.usize >> unless (t ≠ type.object) (throw "invalid scalar array") -| (instr.array_write a i _) := check_type a type.object >> check_type i type.usize +| (instr.array a sz c) := check_type sz type.usize *> check_type c type.usize +| (instr.sarray a t sz c) := check_type sz type.usize *> check_type c type.usize *> unless (t ≠ type.object) (throw "invalid scalar array") +| (instr.array_write a i _) := check_type a type.object *> check_type i type.usize def phi.check (p : phi) : type_checker_m unit := p.decorate_error $ p.ys.mfor (flip check_type p.ty) def check_result_types : list var → list result → type_checker_m unit | [] [] := pure () -| (x::xs) (t::ts) := check_type x t.ty >> check_result_types xs ts +| (x::xs) (t::ts) := check_type x t.ty *> check_result_types xs ts | _ _ := throw "unexpected number of return values" def terminator.check (term : terminator) : type_checker_m unit := @@ -229,16 +229,16 @@ match term with | (terminator.jmp _) := pure () def block.check (b : block) : type_checker_m unit := -b.decorate_error $ b.phis.mfor phi.check >> b.instrs.mfor instr.check >> b.term.check +b.decorate_error $ b.phis.mfor phi.check *> b.instrs.mfor instr.check *> b.term.check def decl.check : decl → type_checker_m unit | (decl.defn h bs) := h.decorate_error $ when (h.is_const && (h.return.length ≠ 1 || h.args.length ≠ 0)) (throw "invalid constant definition") - >> bs.mfor block.check + *> bs.mfor block.check | _ := pure () def type_check (d : decl) (env : environment := λ _, none) : except format context := -(d.infer_types >> d.check >> get).run env d.header.return +(d.infer_types *> d.check *> get).run env d.header.return end ir end lean diff --git a/library/init/lean/name_mangling.lean b/library/init/lean/name_mangling.lean index b3023d8af6..b2505e14bc 100644 --- a/library/init/lean/name_mangling.lean +++ b/library/init/lean/name_mangling.lean @@ -40,7 +40,7 @@ string.mangle_aux s.length s.mk_iterator "" private def parse_mangled_string_aux : nat → string → parsec' string | 0 r := pure r | (i+1) r := - (eoi >> pure r) + (eoi *> pure r) <|> (do c ← alpha, parse_mangled_string_aux i (r.push c)) <|> (do c ← digit, parse_mangled_string_aux i (r.push c)) <|> (do str "__", parse_mangled_string_aux i (r.push '_')) @@ -71,7 +71,7 @@ name.mangle_aux pre n private def parse_mangled_name_aux : nat → name → parsec' name | 0 r := pure r | (i+1) r := - (eoi >> pure r) + (eoi *> pure r) <|> (do str "_s", n ← num, ch '_', (some s) ← string.demangle <$> take n, parse_mangled_name_aux i (r.mk_string s)) diff --git a/library/init/lean/parser/identifier.lean b/library/init/lean/parser/identifier.lean index 8c025f0241..d7a95eee99 100644 --- a/library/init/lean/parser/identifier.lean +++ b/library/init/lean/parser/identifier.lean @@ -46,7 +46,7 @@ do c ← satisfy is_id_first, take_while_cont is_id_rest (to_string c) def id_part_escaped : m string := -ch id_begin_escape >> take_until1 is_id_end_escape <* ch id_end_escape +ch id_begin_escape *> take_until1 is_id_end_escape <* ch id_end_escape def id_part : m string := cond is_id_begin_escape @@ -55,7 +55,7 @@ cond is_id_begin_escape def identifier : m name := (try $ do s ← id_part, - foldl name.mk_string (mk_simple_name s) (ch '.' >> id_part)) "identifier" + foldl name.mk_string (mk_simple_name s) (ch '.' *> id_part)) "identifier" def c_identifier : m string := (try $ do c ← satisfy (λ c, c.is_alpha || c = '_'), diff --git a/library/init/lean/parser/module.lean b/library/init/lean/parser/module.lean index eb734be941..d67f9ff15b 100644 --- a/library/init/lean/parser/module.lean +++ b/library/init/lean/parser/module.lean @@ -71,7 +71,7 @@ private def commands_aux : bool → list syntax → nat → module_parser pure (tt, some msg.custom) }, match c with - | some c := yield c >> commands_aux recovering (c :: cs) n + | some c := yield c *> commands_aux recovering (c :: cs) n | none := commands_aux recovering cs n def commands.parser : module_parser := diff --git a/library/init/lean/parser/parsec.lean b/library/init/lean/parser/parsec.lean index 754e778b70..4b49a1fb84 100644 --- a/library/init/lean/parser/parsec.lean +++ b/library/init/lean/parser/parsec.lean @@ -451,7 +451,7 @@ string.iterator.offset <$> left_over @[inline] def not_followed_by [monad_except message m] (p : m α) (msg : string := "input") : m unit := do it ← left_over, - b ← lookahead $ catch (p >> pure ff) (λ _, pure tt), + b ← lookahead $ catch (p *> pure ff) (λ _, pure tt), if b then pure () else error msg dlist.empty it def eoi : m unit := @@ -472,8 +472,8 @@ def many [alternative m] (p : m α) : m (list α) := many1 p <|> pure [] def many1_aux' [alternative m] (p : m α) : nat → m unit -| 0 := p >> pure () -| (n+1) := p >> (many1_aux' n <|> pure ()) +| 0 := p *> pure () +| (n+1) := p *> (many1_aux' n <|> pure ()) def many1' [alternative m] (p : m α) : m unit := do r ← remaining, many1_aux' p r @@ -482,7 +482,7 @@ def many' [alternative m] (p : m α) : m unit := many1' p <|> pure () def sep_by1 [alternative m] (p : m α) (sep : m β) : m (list α) := -(::) <$> p <*> many (sep >> p) +(::) <$> p <*> many (sep *> p) def sep_by [alternative m] (p : m α) (sep : m β) : m (list α) := sep_by1 p sep <|> pure [] diff --git a/library/init/lean/parser/string_literal.lean b/library/init/lean/parser/string_literal.lean index 5b0f5444b6..fc5db3b7ec 100644 --- a/library/init/lean/parser/string_literal.lean +++ b/library/init/lean/parser/string_literal.lean @@ -37,7 +37,7 @@ do it ← left_over, else unexpected_at "quoted character" it def parse_string_literal_aux : nat → string → parsec' string -| 0 s := ch '\"' >> pure s +| 0 s := ch '\"' *> pure s | (n+1) s := do c ← any, if c = '\\' then do c ← parse_quoted_char, parse_string_literal_aux n (s.push c) diff --git a/tests/lean/parsec1.lean b/tests/lean/parsec1.lean index 7c51b37383..4fd0bb2f0b 100644 --- a/tests/lean/parsec1.lean +++ b/tests/lean/parsec1.lean @@ -14,28 +14,28 @@ match parsec.parse p s with def show_result {α} [has_to_string α] (p : parsec' α) (s : string) : eio unit := match parsec.parse p s with -| except.ok a := io.println "result: " >> io.println (repr $ to_string a) +| except.ok a := io.println "result: " *> io.println (repr $ to_string a) | except.error e := io.println e #eval test (ch 'a') "a" 'a' #eval test any "a" 'a' #eval test any "b" 'b' #eval test (str "foo" <|> str "bla" <|> str "boo") "bla" "bla" -#eval test ((str "foo" >> str "foo") <|> str "bla" <|> str "boo") "bla" "bla" -#eval test_failure ((str "foo" >> str "foo") <|> str "foo2" <|> str "boo") "foo2" -#eval test (try (str "foo" >> str "foo") <|> str "foo2" <|> str "boo") "foo2" "foo2" +#eval test ((str "foo" *> str "foo") <|> str "bla" <|> str "boo") "bla" "bla" +#eval test_failure ((str "foo" *> str "foo") <|> str "foo2" <|> str "boo") "foo2" +#eval test (try (str "foo" *> str "foo") <|> str "foo2" <|> str "boo") "foo2" "foo2" #eval test num "1000" 1000 #eval test (do n ← num, whitespace, m ← num, pure (n, m)) "1000 200" (1000, 200) #eval test (do n ← num, whitespace, m ← num, pure (n, m)) "1000 200" (1000, 200) #eval test (do n ← lexeme num, m ← num, pure (n, m)) "1000 200" (1000, 200) -#eval test (whitespace >> prod.mk <$> (lexeme num) <*> (lexeme num)) " 1000 200 " (1000, 200) -#eval test (whitespace >> prod.mk <$> (lexeme num) <*> (lexeme num) <* eoi) " 1000 200 " (1000, 200) -#eval test_failure (whitespace >> prod.mk <$> (lexeme num) <*> num <* eoi) " 1000 200 " +#eval test (whitespace *> prod.mk <$> (lexeme num) <*> (lexeme num)) " 1000 200 " (1000, 200) +#eval test (whitespace *> prod.mk <$> (lexeme num) <*> (lexeme num) <* eoi) " 1000 200 " (1000, 200) +#eval test_failure (whitespace *> prod.mk <$> (lexeme num) <*> num <* eoi) " 1000 200 " -#eval test_failure ((ch 'a' >> ch 'b') <|> (ch 'a' >> ch 'c')) "ac" -#eval test ((lookahead (str "ab") >> ch 'a' >> ch 'b') <|> (ch 'a' >> ch 'c')) "ac" 'c' -#eval test (str "ab" >> pure () <|> (ch 'a' >> ch 'c' >> pure ())) "ac" () -#eval test (try (ch 'a' >> ch 'b') <|> (ch 'a' >> ch 'c')) "ac" 'c' +#eval test_failure ((ch 'a' *> ch 'b') <|> (ch 'a' *> ch 'c')) "ac" +#eval test ((lookahead (str "ab") *> ch 'a' *> ch 'b') <|> (ch 'a' *> ch 'c')) "ac" 'c' +#eval test (str "ab" *> pure () <|> (ch 'a' *> ch 'c' *> pure ())) "ac" () +#eval test (try (ch 'a' *> ch 'b') <|> (ch 'a' *> ch 'c')) "ac" 'c' #eval test (lookahead (ch 'a')) "abc" 'a' #eval test_failure (not_followed_by (lookahead (ch 'a'))) "abc" @@ -43,7 +43,7 @@ def symbol (c : char) : parsec' char := lexeme (ch c) repr c def paren {α} (p : parsec' α) : parsec' α := -symbol '(' >> lexeme p <* symbol ')' +symbol '(' *> lexeme p <* symbol ')' #eval test (paren num) "( 10 )" 10 #eval test (paren num) "(12)" 12 @@ -166,7 +166,7 @@ do l ← parse_atom p, (do symbol '+', r ← p, pure $ Add l r) <|> pure l def parse_expr : parsec' Expr := -whitespace >> fix (λ F, parse_add F) <* eoi +whitespace *> fix (λ F, parse_add F) <* eoi #eval test parse_expr "10" (Num 10) #eval test parse_expr "(20)" (Num 20) @@ -186,7 +186,7 @@ namespace paper_ex #print "Failure 3" def digit : parsec' char := monad_parsec.digit "digit" def letter : parsec' char := monad_parsec.alpha "letter" -def tst : parsec' char := (digit <|> pure '0') >> letter +def tst : parsec' char := (digit <|> pure '0') *> letter #eval test tst "*" 'a' #print "---------" end paper_ex diff --git a/tests/lean/run/lirc1.lean b/tests/lean/run/lirc1.lean index 58a37084d8..43b5f48b58 100644 --- a/tests/lean/run/lirc1.lean +++ b/tests/lean/run/lirc1.lean @@ -4,7 +4,7 @@ open lean.ir 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 +| except.error e := io.print "Error: " *> io.print e def PRG1 := " [make_my_pair] external foo (a : object) (b : object) : object diff --git a/tests/lean/run/parser_ir1.lean b/tests/lean/run/parser_ir1.lean index c55f259363..f1f0a2d877 100644 --- a/tests/lean/run/parser_ir1.lean +++ b/tests/lean/run/parser_ir1.lean @@ -15,7 +15,7 @@ match type_check d with def show_result (p : parsec' decl) (s : string) : m unit := match parsec.parse p s with -| except.ok d := io.println (lean.to_fmt d) >> check_decl d +| except.ok d := io.println (lean.to_fmt d) *> check_decl d | except.error e := io.println e def IR1 := " @@ -23,7 +23,7 @@ def succ (x : uint32) : uint32 := main: one : uint32 := 1; x1 : uint32 := add x one; ret x1; " -#eval show_result (whitespace >> parse_def) IR1 +#eval show_result (whitespace *> parse_def) IR1 def IR2 := " def add_n (x : uint32) (y : uint32) (n : uint32) : uint32 := @@ -43,10 +43,10 @@ end: ret r3; " -#eval show_result (whitespace >> parse_def) IR2 +#eval show_result (whitespace *> parse_def) IR2 def tst_elim_phi (s : string) : m unit := -do d ← monad_except.lift_except $ parsec.parse (whitespace >> parse_def) s, +do d ← monad_except.lift_except $ parsec.parse (whitespace *> parse_def) s, check_decl d, io.println (lean.to_fmt (elim_phi d)) @@ -64,10 +64,10 @@ main: sset o 25 d6; ret o; " -#eval show_result (whitespace >> parse_def) IR3 +#eval show_result (whitespace *> parse_def) IR3 def tst_extract_cpp (s : string) : m unit := -do d ← monad_except.lift_except $ parsec.parse (whitespace >> parse_def) s, +do d ← monad_except.lift_except $ parsec.parse (whitespace *> parse_def) s, check_decl d, match extract_cpp [elim_phi d] with | except.ok code := io.println code diff --git a/tests/lean/trace1.lean b/tests/lean/trace1.lean index b0ceb3fd29..65039fc024 100644 --- a/tests/lean/trace1.lean +++ b/tests/lean/trace1.lean @@ -8,9 +8,9 @@ prod.snd <$> trace_t.run opts ( trace_root ⟨1, 0⟩ `trace.type_context.is_def_eq "type_context.is_def_eq trace" ⟨λ _, trace_ctx `trace.type_context.is_def_eq "f 0 =?= f a (approximate mode)" ⟨λ _, trace_ctx `trace.type_context.is_def_eq_detail "f 0 =?= f a" ⟨λ _, - trace `trace.type_context.is_def_eq_detail "0 =?= a" >> + trace `trace.type_context.is_def_eq_detail "0 =?= a" *> trace `trace.type_context.is_def_eq_detail "...failed" - ⟩ >> + ⟩ *> trace `trace.type_context.is_def_eq "...failed" ⟩ ⟩)