refactor(library/init/lean/ir): combine unary instructions

library/init/lean/ir/elim_phi.lean

@@ -47,11 +47,7 @@ def instr.replace_vars : instr → elim_phi_m instr
 | (instr.write a i v)       := instr.write <$> find a <*> find i <*> find v
 | (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.inc x)             := instr.inc <$> find x
-| (instr.decs x)            := instr.decs <$> find x
-| (instr.free x)            := instr.free <$> find x
-| (instr.dealloc x)         := instr.dealloc <$> find x
-| (instr.dec x)             := instr.dec <$> find x
+| (instr.unary op x)        := instr.unary op <$> find x
 
 def terminator.replace_vars : terminator → elim_phi_m terminator
 | (terminator.ret xs)    := terminator.ret <$> xs.mmap find

library/init/lean/ir/extract_cpp.lean

@@ -192,6 +192,16 @@ match l with
 | literal.float v := emit_var x >> emit " := " >> emit v
 | literal.num v   := emit_var x >> emit " := " >> emit v >> emit_num_suffix t
 
+def unins2cpp : unins → string
+| unins.inc            := "lean::inc_ref"
+| unins.decs           := "lean::dec_shared_ref"
+| unins.dec            := "lean::dec_ref"
+| unins.free           := "free"
+| unins.dealloc        := "lean::dealloc"
+
+def emit_unary (op : unins) (x : var) : extract_m unit :=
+emit (unins2cpp op) >> emit "(" >> emit_var x >> emit ")"
+
 def emit_instr (ins : instr) : extract_m unit :=
 ins.decorate_error $
 (match ins with
@@ -210,11 +220,7 @@ ins.decorate_error $
  | (instr.write a i v)      := emit "lean::set_array_obj(" >> emit_var a >> emit ", " >> emit_var i >> emit ", " >> emit_var v >> 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.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
- | (instr.dealloc x)        := emit_op_x "lean::dealloc" x
- | (instr.dec x)            := emit_op_x "lean::dec_ref" x)
+ | (instr.unary op x)       := emit_unary op x)
 >> emit_eos
 
 def emit_block (b : block) : extract_m unit :=

library/init/lean/ir/format.lean

@@ -68,6 +68,14 @@ def binop.to_format : binop → format
 instance binop.has_to_format : has_to_format binop := ⟨binop.to_format⟩
 instance binop.has_to_string : has_to_string binop := ⟨pretty ∘ to_fmt⟩
 
+def unins.to_format : unins → format
+| unins.inc  := "inc"
+| unins.dec  := "dec"  | unins.decs := "decs"
+| unins.free := "free" | unins.dealloc := "dealloc"
+
+instance unins.has_to_format : has_to_format unins := ⟨unins.to_format⟩
+instance unins.has_to_string : has_to_string unins := ⟨pretty ∘ to_fmt⟩
+
 def literal.to_format : literal → format
 | (literal.bool b)  := to_fmt b
 | (literal.str s)   := repr s
@@ -103,11 +111,7 @@ def instr.to_format : instr → format
 | (instr.write a i v)        := "write " ++ to_fmt a ++ " " ++ to_fmt i ++ " " ++ to_fmt v
 | (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.inc x)              := "inc " ++ to_fmt x
-| (instr.decs x)             := "decs " ++ to_fmt x
-| (instr.free x)             := "free " ++ to_fmt x
-| (instr.dealloc x)          := "dealloc " ++ to_fmt x
-| (instr.dec x)              := "dec " ++ to_fmt x
+| (instr.unary op x)         := to_fmt op ++ " " ++ to_fmt x
 
 instance instr.has_to_format : has_to_format instr := ⟨instr.to_format⟩
 instance instr.has_to_string : has_to_string instr := ⟨pretty ∘ to_fmt⟩

library/init/lean/ir/ir.lean

@@ -46,16 +46,26 @@ instance type_has_dec_eq : decidable_eq type :=
 
 /- END of TEMPORARY HACK for (decidable_eq type) -/
 
+/-- Operators for instructions of the form `x : t := op y` -/
 inductive unop
 | not | neg | is_scalar | is_shared | cast | box | unbox
 | array_copy
 | sarray_copy
 
+/-- Operators for instructions of the form `x : t := op y z` -/
 inductive binop
 | add | sub | mul | div | mod | shl | shr | and | or | xor
 | le  | ge  | lt  | gt  | eq  | ne
 | read -- (scalar) array read
 
+/-- Operators for instructions of the form `op x` -/
+inductive unins
+| inc     -- increment reference counter
+| dec     -- decrement reference counter
+| decs    -- decrement reference counter of shared object
+| free    -- free object memory, object must not be an external or big number
+| dealloc -- free object memory
+
 inductive literal
 | bool    : bool   → literal
 | str     : string → literal
@@ -115,12 +125,8 @@ inductive instr
 /- 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
-/- Reference counting -/
-| inc     (x : var)                                             -- inc var
-| decs    (x : var)                                             -- Decrement RC of shared object
-| free    (x : var)                                             -- Just free memory
-| dealloc (x : var)                                             -- If object may be a numeral/external, then invoke destructor and then free
-| dec     (x : var)                                             -- Remark: can be defined using `decs`, `dealloc` and `shared`
+/- Unary instructions -/
+| unary   (op : unins) (x : var)                                -- op x
 
 structure phi :=
 (x : var) (ty : type) (ys : list var)

library/init/lean/ir/parser.lean

@@ -62,6 +62,13 @@ def parse_binop : parser binop :=
 <|> (keyword "ne" >> return binop.ne)
 <|> (keyword "read" >> return binop.read)
 
+def parse_unins : parser unins :=
+    (keyword "inc" >> return unins.inc)
+<|> (keyword "dec" >> return unins.dec)
+<|> (keyword "decs" >> return unins.decs)
+<|> (keyword "free" >> return unins.free)
+<|> (keyword "dealloc" >> return unins.dealloc)
+
 def parse_literal : parser literal :=
     (keyword "tt" >> return (literal.bool tt))
 <|> (keyword "ff" >> return (literal.bool ff))
@@ -138,11 +145,7 @@ def parse_instr : parser instr :=
 <|> (keyword "swrite" >> instr.swrite <$> parse_var <*> parse_var <*> parse_var)
 <|> (keyword "set" >> instr.set <$> parse_var <*> parse_uint16 <*> parse_var)
 <|> (keyword "sset" >> instr.sset <$> parse_var <*> parse_sizet <*> parse_var)
-<|> (keyword "inc" >> instr.inc <$> parse_var)
-<|> (keyword "dec" >> instr.dec <$> parse_var)
-<|> (keyword "decs" >> instr.decs <$> parse_var)
-<|> (keyword "free" >> instr.free <$> parse_var)
-<|> (keyword "dealloc" >> instr.dealloc <$> parse_var)
+<|> (instr.unary <$> parse_unins <*> parse_var)
 <|> parse_assignment
 
 def parse_phi : parser phi :=

library/init/lean/ir/ssa_check.lean

@@ -96,11 +96,7 @@ match ins with
 | (instr.write a i v)     := a.defined >> i.defined >> v.defined
 | (instr.sarray x _ sz c) := x.define >> sz.defined >> c.defined
 | (instr.swrite a i v)    := a.defined >> i.defined >> v.defined
-| (instr.inc x)           := x.defined
-| (instr.decs x)          := x.defined
-| (instr.free x)          := x.defined
-| (instr.dealloc x)       := x.defined
-| (instr.dec x)           := x.defined
+| (instr.unary _ x)       := x.defined
 
 def terminator.valid_ssa (term : terminator) : ssa_valid_m unit :=
 term.decorate_error $

library/init/lean/ir/type_check.lean

@@ -192,11 +192,7 @@ match ins with
 | (instr.write a i v)      := check_type a type.object >> check_type i type.usize >> check_type v type.object
 | (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.inc x)            := check_type x type.object
-| (instr.decs x)           := check_type x type.object
-| (instr.dealloc x)        := check_type x type.object
-| (instr.free x)           := check_type x type.object
-| (instr.dec x)            := check_type x type.object
+| (instr.unary _ x)        := check_type x type.object
 
 def phi.check (p : phi) : type_checker_m unit :=
 p.decorate_error $ p.ys.mfor (flip check_type p.ty)