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

chore(library/init/lean/ir): shared ==> is_shared, scalar ==> is_scalar

Browse source
This commit is contained in:
Leonardo de Moura 2018-05-10 08:30:28 -07:00
parent 2e0629133f
commit d2c4918ca3
5 changed files with 8 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

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

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

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

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

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

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

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

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

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