diff --git a/library/init/lean/ir/extract_cpp.lean b/library/init/lean/ir/extract_cpp.lean index 301f0b51c9..5bb86a1c9b 100644 --- a/library/init/lean/ir/extract_cpp.lean +++ b/library/init/lean/ir/extract_cpp.lean @@ -36,7 +36,7 @@ do env ← read, | some s := emit s | none := emit (name.mangle fid) -def to_cpp_type : type → string +def type2cpp : type → string | type.bool := "unsigned char" | type.byte := "unsigned char" | type.uint16 := "unsigned short" | type.uint32 := "unsigned" | type.uint64 := "unsigned long long" | type.usize := "size_t" | type.int16 := "short" | type.int32 := "int" | type.int64 := "long long" @@ -44,7 +44,7 @@ def to_cpp_type : type → string | type.object := "lean_obj*" def emit_type (ty : type) : extract_m unit := -emit (to_cpp_type ty) +emit (type2cpp ty) def emit_sep_aux {α} (f : α → extract_m unit) (sep : string) : list α → extract_m unit | [] := return () @@ -160,23 +160,22 @@ match op with def emit_x_op_y (x : var) (op : string) (y : var) : extract_m unit := emit_var x >> emit " := " >> emit op >> emit "(" >> emit_var y >> emit ")" +def unop2cpp (t : type) : unop → string +| unop.not := if t = type.bool then "!" else "~" +| unop.neg := if t = type.object then "lean::big_neg" else "-" +| unop.is_scalar := "lean::is_scalar" +| unop.is_shared := "lean::is_shared" +| unop.box := "lean::box" +| unop.unbox := "lean::unbox" +| unop.cast := "static_cast<" ++ type2cpp t ++ ">" +| unop.array_copy := "lean::array_copy" +| unop.sarray_copy := "lean::sarray_copy" +| unop.array_size := "lean::array_size" +| unop.sarray_size := "lean::sarray_size" +| unop.string_len := "lean::string_len" + def emit_unop (x : var) (t : type) (op : unop) (y : var) : extract_m unit := -match op with -| unop.not := - (match t with - | type.bool := emit_x_op_y x "!" y - | _ := emit_x_op_y x "~" y) -| unop.neg := - (match t with - | type.object := emit_x_op_y x "lean::big_neg" y - | _ := emit_x_op_y x "-" 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.array_copy := emit_x_op_y x "lean::array_copy" y -| unop.sarray_copy := emit_x_op_y x "lean::sarray_copy" y -| unop.box := emit_x_op_y x "lean::box" y -| unop.unbox := emit_x_op_y x "lean::unbox" y -| unop.cast := emit_var x >> emit " := static_cast<" >> emit_type t >> emit ">(" >> emit_var y >> emit ")" +emit_var x >> emit " := " >> emit (unop2cpp t op) >> emit "(" >> emit_var y >> emit ")" def emit_num_suffix : type → extract_m unit | type.uint32 := emit "u" diff --git a/library/init/lean/ir/format.lean b/library/init/lean/ir/format.lean index 45e795f8d9..78261655b2 100644 --- a/library/init/lean/ir/format.lean +++ b/library/init/lean/ir/format.lean @@ -48,11 +48,13 @@ instance type.has_to_format : has_to_format type := ⟨type.to_format⟩ 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.is_scalar := "is_scalar" | unop.is_shared := "is_shared" -| unop.box := "box" | unop.unbox := "unbox" -| unop.cast := "cast" -| unop.array_copy := "array_copy" | unop.sarray_copy := "sarray_copy" +| unop.not := "not" | unop.neg := "neg" +| unop.is_scalar := "is_scalar" | unop.is_shared := "is_shared" +| unop.box := "box" | unop.unbox := "unbox" +| unop.cast := "cast" +| unop.array_copy := "array_copy" | unop.sarray_copy := "sarray_copy" +| unop.array_size := "array_size" | unop.sarray_size := "sarray_size" +| unop.string_len := "string_len" instance unop.has_to_format : has_to_format unop := ⟨unop.to_format⟩ instance unop.has_to_string : has_to_string unop := ⟨pretty ∘ to_fmt⟩ diff --git a/library/init/lean/ir/ir.lean b/library/init/lean/ir/ir.lean index 082a3ebe63..478f84cfbc 100644 --- a/library/init/lean/ir/ir.lean +++ b/library/init/lean/ir/ir.lean @@ -51,6 +51,9 @@ inductive unop | not | neg | is_scalar | is_shared | cast | box | unbox | array_copy | sarray_copy +| array_size +| sarray_size +| string_len /-- Operators for instructions of the form `x : t := op y z` -/ inductive binop diff --git a/library/init/lean/ir/parser.lean b/library/init/lean/ir/parser.lean index 4cdf068628..19b4f68497 100644 --- a/library/init/lean/ir/parser.lean +++ b/library/init/lean/ir/parser.lean @@ -42,6 +42,9 @@ def parse_unop : parser unop := <|> (keyword "box" >> return unop.box) <|> (keyword "unbox" >> return unop.unbox) <|> (keyword "cast" >> return unop.cast) +<|> (keyword "array_size" >> return unop.array_size) +<|> (keyword "sarray_size" >> return unop.sarray_size) +<|> (keyword "string_len" >> return unop.string_len) def parse_binop : parser binop := (keyword "add" >> return binop.add) diff --git a/library/init/lean/ir/type_check.lean b/library/init/lean/ir/type_check.lean index 87244fce19..7cc99b1768 100644 --- a/library/init/lean/ir/type_check.lean +++ b/library/init/lean/ir/type_check.lean @@ -43,15 +43,18 @@ match ty with /-- Return `tt` iff the instruction `x : r := op y` is type correct where `y : t` -/ 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.is_scalar := t = type.object && r = type.bool -| unop.is_shared := t = type.object && r = type.bool -| unop.array_copy := t = type.object && r = type.object -| unop.sarray_copy := t = type.object && r = type.object -| unop.unbox := t = type.object && (r = type.uint32 || r = type.int32) -| unop.box := r = type.object && (t = type.uint32 || t = type.int32) -| unop.cast := r ≠ type.object && r ≠ type.object +| unop.not := t = r && is_bitwise_ty t +| unop.neg := t = r && is_signed_arith_ty t +| unop.is_scalar := t = type.object && r = type.bool +| unop.is_shared := t = type.object && r = type.bool +| unop.array_copy := t = type.object && r = type.object +| unop.sarray_copy := t = type.object && r = type.object +| unop.unbox := t = type.object && (r = type.uint32 || r = type.int32) +| unop.box := r = type.object && (t = type.uint32 || t = type.int32) +| unop.cast := r ≠ type.object && r ≠ type.object +| unop.array_size := r = type.usize && t = type.object +| unop.sarray_size := r = type.usize && t = type.object +| unop.string_len := r = type.usize && t = type.object /-- Return `tt` iff the instruction `x : r := op y z` is type correct where `y z : t` -/ def valid_binop_types (op : binop) (r : type) (t₁ t₂ : type) : bool :=