From ade8cb729618568a61035ad5d3afa0993b243dbd Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 15 May 2018 15:58:58 -0700
Subject: [PATCH] chore(library/init/lean/ir): make it clear that big number
 may be a tagged pointer

---
 library/init/lean/ir/extract_cpp.lean | 28 +++++++++++++--------------
 library/init/lean/ir/ir.lean          |  6 +++---
 2 files changed, 17 insertions(+), 17 deletions(-)

diff --git a/library/init/lean/ir/extract_cpp.lean b/library/init/lean/ir/extract_cpp.lean
index ef0773dcdc..130acc0b60 100644
--- a/library/init/lean/ir/extract_cpp.lean
+++ b/library/init/lean/ir/extract_cpp.lean
@@ -195,22 +195,22 @@ match t with
 
 def emit_assign_binop (x : var) (t : type) (op : assign_binop) (y z : var) : extract_m unit :=
 match op with
-| assign_binop.add  := emit_arith t x y z "+" "lean::big_add"
-| assign_binop.sub  := emit_arith t x y z "-" "lean::big_sub"
-| assign_binop.mul  := emit_arith t x y z "*" "lean::big_mul"
-| assign_binop.div  := emit_arith t x y z "/" "lean::big_div"
-| assign_binop.mod  := emit_arith t x y z "%" "lean::big_mod"
+| assign_binop.add  := emit_arith t x y z "+" "lean::add"
+| assign_binop.sub  := emit_arith t x y z "-" "lean::sub"
+| assign_binop.mul  := emit_arith t x y z "*" "lean::mul"
+| assign_binop.div  := emit_arith t x y z "/" "lean::div"
+| assign_binop.mod  := emit_arith t x y z "%" "lean::mod"
 | assign_binop.shl  := emit_infix x y z "<<"
 | assign_binop.shr  := emit_infix x y z ">>"
-| assign_binop.and  := emit_logical_arith t x y z "&&" "&" (some "lean::big_and")
-| assign_binop.or   := emit_logical_arith t x y z "||" "|" (some "lean::big_or")
+| assign_binop.and  := emit_logical_arith t x y z "&&" "&" (some "lean::and")
+| assign_binop.or   := emit_logical_arith t x y z "||" "|" (some "lean::or")
 | assign_binop.xor  := emit_logical_arith t x y z "!=" "^" none
-| assign_binop.le   := emit_arith t x y z "<=" "lean::big_le"
-| assign_binop.ge   := emit_arith t x y z ">=" "lean::big_ge"
-| assign_binop.lt   := emit_arith t x y z "<" "lean::big_lt"
-| assign_binop.gt   := emit_arith t x y z ">" "lean::big_gt"
-| assign_binop.eq   := emit_arith t x y z "==" "lean::big_eq"
-| assign_binop.ne   := emit_arith t x y z "!=" "lean::big_nq"
+| assign_binop.le   := emit_arith t x y z "<=" "lean::le"
+| assign_binop.ge   := emit_arith t x y z ">=" "lean::ge"
+| assign_binop.lt   := emit_arith t x y z "<" "lean::lt"
+| assign_binop.gt   := emit_arith t x y z ">" "lean::gt"
+| assign_binop.eq   := emit_arith t x y z "==" "lean::eq"
+| assign_binop.ne   := emit_arith t x y z "!=" "lean::ne"
 | assign_binop.array_read :=
   (match t with
    | type.object := emit_var x >> emit " = lean::array_obj" >> paren (emit_var y <+> emit_var z)
@@ -222,7 +222,7 @@ emit_var x >> emit " = " >> emit op >> paren(emit_var y)
 
 def assign_unop2cpp (t : type) : assign_unop → string
 | assign_unop.not          := if t = type.bool then "!" else "~"
-| assign_unop.neg          := if t = type.object then "lean::big_neg" else "-"
+| assign_unop.neg          := if t = type.object then "lean::neg" else "-"
 | assign_unop.is_scalar    := "lean::is_scalar"
 | assign_unop.is_shared    := "lean::is_shared"
 | assign_unop.is_null      := "lean::is_null"
diff --git a/library/init/lean/ir/ir.lean b/library/init/lean/ir/ir.lean
index 51731b6604..83dc33e56c 100644
--- a/library/init/lean/ir/ir.lean
+++ b/library/init/lean/ir/ir.lean
@@ -32,7 +32,7 @@ uint64 | usize | int16 | int32 | int64 | float | double | object
 Otherwise, it is bitwise negation if `t` is `uint32/uint64/usize`.
 
 - `x : t := neg y`, arithmetical `-`. `t` is `int16/int32/int64/float/double/object`.
-If `t` is `object`, the instruction is unspecified if `t` is not a big number.
+If `t = object`, the instruction is unspecified if `t` is not a big number nor a tagged pointer.
 
 - `x : bool := is_scalar y`, set `x` to `tt` iff `y : object` is a tagged
 pointer.
@@ -74,8 +74,8 @@ inductive assign_unop
 /-- Operators for instructions of the form `x : t := op y z`
 
 - `x : t := add y z`: addition. Remark: `t ≠ bool`.
-When `t` is a big number (i.e., `t` is `object`), a new big number is
-allocated to store the result.
+When `t = object`, i.e., `t` is big number or tagged pointer, a new big number may be allocated
+if the result does not fit in a tagged pointer.
 
 - `x : t := sub y z`: subtraction. Remark: `t ≠ bool`. See `add` for big number case.