max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor(library/init/lean/ir): read and sread instructions are now binop

Browse source
This commit is contained in:
Leonardo de Moura 2018-05-10 08:47:16 -07:00
parent 7b89a8c910
commit 655cfbf3b0
7 changed files with 8 additions and 20 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/init/lean/ir/elim_phi.lean
View file

@ -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

7
library/init/lean/ir/extract_cpp.lean
View file

@ -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

3
library/init/lean/ir/format.lean
View file

@ -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

3
library/init/lean/ir/ir.lean
View file

@ -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

4
library/init/lean/ir/parser.lean
View file

@ -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)

4
library/init/lean/ir/ssa_check.lean
View file

@ -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

5
library/init/lean/ir/type_check.lean
View file

@ -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