diff --git a/library/init/lean/ir/elim_phi.lean b/library/init/lean/ir/elim_phi.lean index e662b4eae3..c2068886c6 100644 --- a/library/init/lean/ir/elim_phi.lean +++ b/library/init/lean/ir/elim_phi.lean @@ -45,10 +45,8 @@ def instr.replace_vars : instr → elim_phi_m instr | (instr.apply x ys) := instr.apply <$> find x <*> ys.mmap find | (instr.array a sz c) := instr.array <$> find a <*> find sz <*> find c | (instr.write a i v) := instr.write <$> find a <*> find i <*> find v -| (instr.read x a i) := instr.read <$> find x <*> find a <*> find i | (instr.sarray a ty sz c) := instr.sarray <$> find a <*> pure ty <*> find sz <*> find c | (instr.swrite a i v) := instr.swrite <$> find a <*> find i <*> find v -| (instr.sread x ty a i) := instr.sread <$> find x <*> pure ty <*> find a <*> find i | (instr.inc x) := instr.inc <$> find x | (instr.decs x) := instr.decs <$> find x | (instr.free x) := instr.free <$> find x diff --git a/library/init/lean/ir/extract_cpp.lean b/library/init/lean/ir/extract_cpp.lean index e3cf3ceef8..3ebe417244 100644 --- a/library/init/lean/ir/extract_cpp.lean +++ b/library/init/lean/ir/extract_cpp.lean @@ -151,7 +151,10 @@ match op with | binop.gt := emit_arith t x y z ">" "lean::big_gt" | binop.eq := emit_arith t x y z "==" "lean::big_eq" | binop.ne := emit_arith t x y z "!=" "lean::big_nq" - +| binop.read := + (match t with + | type.object := emit_var x >> emit " := lean::array_obj(" >> emit_var y >> emit ", " >> emit_var z >> emit ")" + | _ := emit_var x >> emit " := lean::sarray_data<" >> emit_type t >> emit ">(" >> emit_var y >> emit ", " >> emit_var z >> emit ")") /-- Emit `x := op(y)` -/ def emit_x_op_y (x : var) (op : string) (y : var) : extract_m unit := @@ -205,10 +208,8 @@ ins.decorate_error $ | (instr.apply x ys) := return () -- TODO | (instr.array a sz c) := emit_var a >> emit " := lean::alloc_array(" >> emit_var sz >> emit ", " >> emit_var c >> emit ")" | (instr.write a i v) := emit "lean::set_array_obj(" >> emit_var a >> emit ", " >> emit_var i >> emit ", " >> emit_var v >> emit ")" - | (instr.read x a i) := emit_var x >> emit " := lean::array_obj(" >> emit_var a >> emit ", " >> emit_var i >> emit ")" | (instr.sarray a t sz c) := emit_var a >> emit " := lean::alloc_sarray(" >> emit_type_size t >> emit ", " >> emit_var sz >> emit ", " >> emit_var c >> emit ")" | (instr.swrite a i v) := emit "lean::set_sarray_data(" >> emit_var a >> emit ", " >> emit_var i >> emit ", " >> emit_var v >> emit ")" - | (instr.sread x t a i) := emit_var x >> emit " := lean::sarray_data<" >> emit_type t >> emit ">(" >> emit_var a >> emit ", " >> emit_var i >> emit ")" | (instr.inc x) := emit_op_x "lean::inc_ref" x | (instr.decs x) := emit_op_x "lean::dec_shared_ref" x | (instr.free x) := emit_op_x "free" x diff --git a/library/init/lean/ir/format.lean b/library/init/lean/ir/format.lean index 95727cc507..ff8fe98ea1 100644 --- a/library/init/lean/ir/format.lean +++ b/library/init/lean/ir/format.lean @@ -63,6 +63,7 @@ def binop.to_format : binop → format | binop.and := "and" | binop.or := "or" | binop.xor := "xor" | binop.le := "le" | binop.ge := "ge" | binop.lt := "lt" | binop.gt := "gt" | binop.eq := "eq" | binop.ne := "ne" +| binop.read := "read" instance binop.has_to_format : has_to_format binop := ⟨binop.to_format⟩ instance binop.has_to_string : has_to_string binop := ⟨pretty ∘ to_fmt⟩ @@ -100,10 +101,8 @@ def instr.to_format : instr → format | (instr.apply x ys) := to_fmt x ++ " := apply " ++ join_sep ys " " | (instr.array a sz c) := to_fmt a ++ " := array " ++ to_fmt sz ++ " " ++ to_fmt c | (instr.write a i v) := "write " ++ to_fmt a ++ " " ++ to_fmt i ++ " " ++ to_fmt v -| (instr.read x a i) := to_fmt x ++ " := read " ++ to_fmt a ++ " " ++ to_fmt i | (instr.sarray a ty sz c) := to_fmt a ++ " := sarray " ++ to_fmt ty ++ " " ++ to_fmt sz ++ " " ++ to_fmt c | (instr.swrite a i v) := "swrite " ++ to_fmt a ++ " " ++ to_fmt i ++ " " ++ to_fmt v -| (instr.sread x ty a i) := to_fmt x ++ " : " ++ to_fmt ty ++ " := sread " ++ to_fmt a ++ " " ++ to_fmt i | (instr.inc x) := "inc " ++ to_fmt x | (instr.decs x) := "decs " ++ to_fmt x | (instr.free x) := "free " ++ to_fmt x diff --git a/library/init/lean/ir/ir.lean b/library/init/lean/ir/ir.lean index b6454411da..a1d58f0878 100644 --- a/library/init/lean/ir/ir.lean +++ b/library/init/lean/ir/ir.lean @@ -54,6 +54,7 @@ inductive unop inductive binop | add | sub | mul | div | mod | shl | shr | and | or | xor | le | ge | lt | gt | eq | ne +| read -- (scalar) array read inductive literal | bool : bool → literal @@ -111,11 +112,9 @@ inductive instr /- Array of objects -/ | array (a sz c : var) -- Create array of objects with size `sz` and capacity `c` | write (a i v : var) -- Array write write a i v -| read (x a i : var) -- Array read x := a[i] /- Scalar arrays -/ | sarray (a : var) (ty : type) (sz c : var) -- Create scalar array | swrite (a i v : var) -- Scalar array write swrite a i v -| sread (x : var) (ty : type) (a i : var) -- Scalar array read x : type := a[i] /- Reference counting -/ | inc (x : var) -- inc var | decs (x : var) -- Decrement RC of shared object diff --git a/library/init/lean/ir/parser.lean b/library/init/lean/ir/parser.lean index 2500beb65e..72a7e73fa2 100644 --- a/library/init/lean/ir/parser.lean +++ b/library/init/lean/ir/parser.lean @@ -60,6 +60,7 @@ def parse_binop : parser binop := <|> (keyword "gt" >> return binop.gt) <|> (keyword "eq" >> return binop.eq) <|> (keyword "ne" >> return binop.ne) +<|> (keyword "read" >> return binop.read) def parse_literal : parser literal := (keyword "tt" >> return (literal.bool tt)) @@ -112,7 +113,6 @@ do symbol ":", ty ← parse_type, symbol ":=", (keyword "sget" >> instr.sget x ty <$> parse_var <*> parse_sizet) -<|> (keyword "sread" >> instr.sread x ty <$> parse_var <*> parse_var) <|> (instr.unop x ty <$> parse_unop <*> parse_var) <|> (instr.binop x ty <$> parse_binop <*> parse_var <*> parse_var) <|> (instr.lit x ty <$> parse_literal) @@ -121,9 +121,7 @@ def parse_untyped_assignment (x : var) : parser instr := do symbol ":=", (keyword "closure" >> instr.closure x <$> parse_fnid <*> many parse_var) <|> (keyword "apply" >> instr.apply x <$> many1 parse_var) -<|> (keyword "read" >> instr.read x <$> parse_var <*> parse_var) <|> (keyword "get" >> instr.get x <$> parse_var <*> parse_uint16) -<|> (keyword "read" >> instr.read x <$> parse_var <*> parse_var) <|> (keyword "call" >> instr.call [x] <$> parse_fnid <*> many parse_var) <|> (keyword "cnstr" >> instr.cnstr x <$> parse_uint16 <*> parse_uint16 <*> parse_sizet) <|> (keyword "array" >> instr.array x <$> parse_var <*> parse_var) diff --git a/library/init/lean/ir/ssa_check.lean b/library/init/lean/ir/ssa_check.lean index 05ed3bbb11..b0d612b347 100644 --- a/library/init/lean/ir/ssa_check.lean +++ b/library/init/lean/ir/ssa_check.lean @@ -28,9 +28,7 @@ def instr.declare_vars : instr → reader_t blockid ssa_pre_m unit | (instr.closure x _ _) := x.declare | (instr.apply x _) := x.declare | (instr.array a _ _) := a.declare -| (instr.read x _ _) := x.declare | (instr.sarray x _ _ _) := x.declare -| (instr.sread x _ _ _) := x.declare | _ := return () def phi.declare (p : phi) : reader_t blockid ssa_pre_m unit := @@ -96,10 +94,8 @@ match ins with | (instr.apply x ys) := x.define >> ys.mfor var.defined | (instr.array a sz c) := a.define >> sz.defined >> c.defined | (instr.write a i v) := a.defined >> i.defined >> v.defined -| (instr.read x a i) := x.define >> a.defined >> i.defined | (instr.sarray x _ sz c) := x.define >> sz.defined >> c.defined | (instr.swrite a i v) := a.defined >> i.defined >> v.defined -| (instr.sread x _ a i) := x.define >> a.defined >> i.defined | (instr.inc x) := x.defined | (instr.decs x) := x.defined | (instr.free x) := x.defined diff --git a/library/init/lean/ir/type_check.lean b/library/init/lean/ir/type_check.lean index 5d91f4c209..1d097e4a74 100644 --- a/library/init/lean/ir/type_check.lean +++ b/library/init/lean/ir/type_check.lean @@ -72,6 +72,7 @@ match op with | binop.gt := r = type.bool && t₁ = t₂ && is_arith_ty t₁ | binop.eq := r = type.bool && t₁ = t₂ | binop.ne := r = type.bool && t₁ = t₂ +| binop.read := t₁ = type.object && t₂ = type.usize @[reducible] def type_checker_m := except_t format (reader_t (environment × list result) (state_t context id)) @@ -142,9 +143,7 @@ match ins with | (instr.closure x f ys) := set_type x type.object | (instr.apply x ys) := set_type x type.object | (instr.array a sz c) := set_type a type.object -| (instr.read x a i) := set_type x type.object | (instr.sarray a t sz c) := set_type a type.object -| (instr.sread x t a i) := set_type x t | other := return () def phi.infer_types (p : phi) : type_checker_m unit := @@ -191,10 +190,8 @@ match ins with | (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.write a i v) := check_type a type.object >> check_type i type.usize >> check_type v type.object -| (instr.read x a i) := check_type a type.object >> check_type i 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.swrite a i v) := check_type a type.object >> check_type i type.usize >> check_ne_type v type.object -| (instr.sread x t a i) := check_ne_type x type.object >> check_type a type.object >> check_type a type.usize | (instr.inc x) := check_type x type.object | (instr.decs x) := check_type x type.object | (instr.dealloc x) := check_type x type.object