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

feat(library/init/lean/ir): add array_size, sarray_size and string_len

Browse source
This commit is contained in:
Leonardo de Moura 2018-05-10 10:02:16 -07:00
parent 68458aa97b
commit e882d9d7cf
5 changed files with 42 additions and 32 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

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

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

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

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

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

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

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

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

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