chore(library): remove >>, we should use *>
This commit is contained in:
Leonardo de Moura
parent
1be71cf725
commit
afd54039ab
20 changed files with 257 additions and 265 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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 _ _,
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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<lean::lean_cfun>(" >> emit fname >> emit ")" <+> emit arity <+> emit ys.length,
|
||||
emit "reinterpret_cast<lean::lean_cfun>(" *> 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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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))
|
||||
|
|
|
|||
|
|
@ -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 = '_'),
|
||||
|
|
|
|||
|
|
@ -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 :=
|
||||
|
|
|
|||
|
|
@ -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 []
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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"
|
||||
⟩
|
||||
⟩)
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue