diff --git a/library/init/lean/ir/extract_cpp.lean b/library/init/lean/ir/extract_cpp.lean index 06f6be4a3e..b5e70eef62 100644 --- a/library/init/lean/ir/extract_cpp.lean +++ b/library/init/lean/ir/extract_cpp.lean @@ -167,8 +167,8 @@ match op with (match t with | type.object := emit_x_op_y x "lean::big_neg" y | _ := emit_x_op_y x "-" y) -| unop.scalar := emit_x_op_y x "lean::is_scalar" y -| unop.shared := emit_x_op_y x "lean::is_shared" y +| unop.is_scalar := emit_x_op_y x "lean::is_scalar" y +| unop.is_shared := emit_x_op_y x "lean::is_shared" y | unop.copy_array := emit_x_op_y x "lean::copy_array" y | unop.copy_sarray := emit_x_op_y x "lean::copy_sarray" y | unop.box := emit_x_op_y x "lean::box" y diff --git a/library/init/lean/ir/format.lean b/library/init/lean/ir/format.lean index 0179db28f3..3bb7b7945f 100644 --- a/library/init/lean/ir/format.lean +++ b/library/init/lean/ir/format.lean @@ -49,7 +49,7 @@ instance type.has_to_string : has_to_string type := ⟨pretty ∘ to_fmt⟩ def unop.to_format : unop → format | unop.not := "not" | unop.neg := "neg" -| unop.scalar := "scalar" | unop.shared := "shared" +| unop.is_scalar := "is_scalar" | unop.is_shared := "is_shared" | unop.box := "box" | unop.unbox := "unbox" | unop.cast := "cast" | unop.copy_array := "copy_array" | unop.copy_sarray := "copy_sarray" diff --git a/library/init/lean/ir/ir.lean b/library/init/lean/ir/ir.lean index 3fba59b078..77753c109f 100644 --- a/library/init/lean/ir/ir.lean +++ b/library/init/lean/ir/ir.lean @@ -47,7 +47,7 @@ instance type_has_dec_eq : decidable_eq type := /- END of TEMPORARY HACK for (decidable_eq type) -/ inductive unop -| not | neg | scalar | shared | cast | box | unbox +| not | neg | is_scalar | is_shared | cast | box | unbox | copy_array | copy_sarray inductive binop diff --git a/library/init/lean/ir/parser.lean b/library/init/lean/ir/parser.lean index fcd9427b32..2957a0cf48 100644 --- a/library/init/lean/ir/parser.lean +++ b/library/init/lean/ir/parser.lean @@ -35,8 +35,8 @@ def parse_type : parser type := def parse_unop : parser unop := (keyword "not" >> return unop.not) <|> (keyword "neg" >> return unop.neg) -<|> (keyword "scalar" >> return unop.scalar) -<|> (keyword "shared" >> return unop.shared) +<|> (keyword "is_scalar" >> return unop.is_scalar) +<|> (keyword "is_shared" >> return unop.is_shared) <|> (keyword "copy_array" >> return unop.copy_array) <|> (keyword "copy_sarray" >> return unop.copy_sarray) <|> (keyword "box" >> return unop.box) diff --git a/library/init/lean/ir/type_check.lean b/library/init/lean/ir/type_check.lean index 226021b4e0..deaeaa0697 100644 --- a/library/init/lean/ir/type_check.lean +++ b/library/init/lean/ir/type_check.lean @@ -45,8 +45,8 @@ def valid_unop_types (op : unop) (r : type) (t : type) : bool := match op with | unop.not := t = r && is_bitwise_ty t | unop.neg := t = r && is_signed_arith_ty t -| unop.scalar := t = type.object && r = type.bool -| unop.shared := t = type.object && r = type.bool +| unop.is_scalar := t = type.object && r = type.bool +| unop.is_shared := t = type.object && r = type.bool | unop.copy_array := t = type.object && r = type.object | unop.copy_sarray := t = type.object && r = type.object | unop.unbox := t = type.object && (r = type.uint32 || r = type.int32)