From b9ec36d0897a7946e990d6fd3640cc856d701f5d Mon Sep 17 00:00:00 2001 From: Siddharth Date: Sun, 30 Jul 2023 01:39:40 -0700 Subject: [PATCH] chore: get rid of all inline C annotations for LLVM (#2363) --- src/Init/Core.lean | 4 +- src/Init/Meta.lean | 12 +++--- src/Init/Prelude.lean | 2 +- src/Lean/Compiler/IR/Checker.lean | 8 ++-- src/Lean/Data/HashMap.lean | 2 +- src/Lean/Data/HashSet.lean | 2 +- src/Lean/Expr.lean | 6 ++- src/include/lean/lean.h | 62 ++++++++++++++++++++++++++++++- 8 files changed, 80 insertions(+), 18 deletions(-) diff --git a/src/Init/Core.lean b/src/Init/Core.lean index f4ba9d7045..1a214ee163 100644 --- a/src/Init/Core.lean +++ b/src/Init/Core.lean @@ -464,13 +464,13 @@ theorem optParam_eq (α : Sort u) (default : α) : optParam α default = α := r `strictOr` is the same as `or`, but it does not use short-circuit evaluation semantics: both sides are evaluated, even if the first value is `true`. -/ -@[extern c inline "#1 || #2"] def strictOr (b₁ b₂ : Bool) := b₁ || b₂ +@[extern "lean_strict_or"] def strictOr (b₁ b₂ : Bool) := b₁ || b₂ /-- `strictAnd` is the same as `and`, but it does not use short-circuit evaluation semantics: both sides are evaluated, even if the first value is `false`. -/ -@[extern c inline "#1 && #2"] def strictAnd (b₁ b₂ : Bool) := b₁ && b₂ +@[extern "lean_strict_and"] def strictAnd (b₁ b₂ : Bool) := b₁ && b₂ /-- `x != y` is boolean not-equal. It is the negation of `x == y` which is supplied by diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean index 3c2854684b..bc31d1f969 100644 --- a/src/Init/Meta.lean +++ b/src/Init/Meta.lean @@ -11,15 +11,15 @@ import Init.Data.Option.BasicAux namespace Lean -@[extern c inline "lean_box(LEAN_VERSION_MAJOR)"] +@[extern "lean_version_get_major"] private opaque version.getMajor (u : Unit) : Nat def version.major : Nat := version.getMajor () -@[extern c inline "lean_box(LEAN_VERSION_MINOR)"] +@[extern "lean_version_get_minor"] private opaque version.getMinor (u : Unit) : Nat def version.minor : Nat := version.getMinor () -@[extern c inline "lean_box(LEAN_VERSION_PATCH)"] +@[extern "lean_version_get_patch"] private opaque version.getPatch (u : Unit) : Nat def version.patch : Nat := version.getPatch () @@ -27,12 +27,12 @@ def version.patch : Nat := version.getPatch () opaque getGithash (u : Unit) : String def githash : String := getGithash () -@[extern c inline "LEAN_VERSION_IS_RELEASE"] +@[extern "lean_version_get_is_release"] opaque version.getIsRelease (u : Unit) : Bool def version.isRelease : Bool := version.getIsRelease () /-- Additional version description like "nightly-2018-03-11" -/ -@[extern c inline "lean_mk_string(LEAN_SPECIAL_VERSION_DESC)"] +@[extern "lean_version_get_special_desc"] opaque version.getSpecialDesc (u : Unit) : String def version.specialDesc : String := version.getSpecialDesc () @@ -61,7 +61,7 @@ def toolchain := else "" -@[extern c inline "LEAN_IS_STAGE0"] +@[extern "lean_internal_is_stage0"] opaque Internal.isStage0 (u : Unit) : Bool /-- Valid identifier names -/ diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index b1045b40eb..fcf7b02636 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -1615,7 +1615,7 @@ The predecessor function on natural numbers. This definition is overridden in the compiler to use `n - 1` instead. The definition provided here is the logical model. -/ -@[extern c inline "lean_nat_sub(#1, lean_box(1))"] +@[extern "lean_nat_pred"] def Nat.pred : (@& Nat) → Nat | 0 => 0 | succ a => a diff --git a/src/Lean/Compiler/IR/Checker.lean b/src/Lean/Compiler/IR/Checker.lean index 4122454c89..36b3c7254a 100644 --- a/src/Lean/Compiler/IR/Checker.lean +++ b/src/Lean/Compiler/IR/Checker.lean @@ -8,19 +8,19 @@ import Lean.Compiler.IR.Format namespace Lean.IR.Checker -@[extern c inline "lean_box(LEAN_MAX_CTOR_FIELDS)"] +@[extern "lean_get_max_ctor_fields"] opaque getMaxCtorFields : Unit → Nat def maxCtorFields := getMaxCtorFields () -@[extern c inline "lean_box(LEAN_MAX_CTOR_SCALARS_SIZE)"] +@[extern "lean_get_max_ctor_scalars_size"] opaque getMaxCtorScalarsSize : Unit → Nat def maxCtorScalarsSize := getMaxCtorScalarsSize () -@[extern c inline "lean_box(LeanMaxCtorTag)"] +@[extern "lean_get_max_ctor_tag"] opaque getMaxCtorTag : Unit → Nat def maxCtorTag := getMaxCtorTag () -@[extern c inline "lean_box(sizeof(size_t))"] +@[extern "lean_get_usize_size"] opaque getUSizeSize : Unit → Nat def usizeSize := getUSizeSize () diff --git a/src/Lean/Data/HashMap.lean b/src/Lean/Data/HashMap.lean index fed2405b7e..99660540ba 100644 --- a/src/Lean/Data/HashMap.lean +++ b/src/Lean/Data/HashMap.lean @@ -31,7 +31,7 @@ namespace HashMapImp variable {α : Type u} {β : Type v} /- Remark: we use a C implementation because this function is performance critical. -/ -@[extern "lean_data_hashmap_mk_idx"] +@[extern "lean_hashmap_mk_idx"] private def mkIdx {sz : Nat} (hash : UInt64) (h : sz.isPowerOfTwo) : { u : USize // u.toNat < sz } := -- TODO: avoid `if` in the reference implementation let u := hash.toUSize &&& (sz.toUSize - 1) diff --git a/src/Lean/Data/HashSet.lean b/src/Lean/Data/HashSet.lean index 70c1ebdc47..43f77c721f 100644 --- a/src/Lean/Data/HashSet.lean +++ b/src/Lean/Data/HashSet.lean @@ -27,7 +27,7 @@ namespace HashSetImp variable {α : Type u} /- Remark: we use a C implementation because this function is performance critical. -/ -@[extern c inline "(size_t)(#2) & (lean_unbox(#1) - 1)"] +@[extern "lean_hashset_mk_idx"] private def mkIdx {sz : Nat} (hash : UInt64) (h : sz.isPowerOfTwo) : { u : USize // u.toNat < sz } := -- TODO: avoid `if` in the reference implementation let u := hash.toUSize &&& (sz.toUSize - 1) diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean index a5bd765174..e03f24ce17 100644 --- a/src/Lean/Expr.lean +++ b/src/Lean/Expr.lean @@ -152,7 +152,9 @@ def Expr.Data.hasLevelMVar (c : Expr.Data) : Bool := def Expr.Data.hasLevelParam (c : Expr.Data) : Bool := ((c.shiftRight 43).land 1) == 1 -@[extern c inline "(uint64_t)#1"] +-- NOTE: the `extern` clause of `BinderInfo.toUInt64` is ABI sensitive. +-- It exploits the fact that a small enum compiles to `uint8`. +@[extern "lean_uint8_to_uint64"] def BinderInfo.toUInt64 : BinderInfo → UInt64 | .default => 0 | .implicit => 1 @@ -459,7 +461,7 @@ inductive Expr where -/ | proj (typeName : Name) (idx : Nat) (struct : Expr) with - @[computed_field, extern c inline "lean_ctor_get_uint64(#1, lean_ctor_num_objs(#1)*sizeof(void*))"] + @[computed_field, extern "lean_expr_data"] data : @& Expr → Data | .const n lvls => mkData (mixHash 5 <| mixHash (hash n) (hash lvls)) 0 0 false false (lvls.any Level.hasMVar) (lvls.any Level.hasParam) | .bvar idx => mkData (mixHash 7 <| hash idx) (idx+1) diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h index aa0df809fa..c28aec98e6 100644 --- a/src/include/lean/lean.h +++ b/src/include/lean/lean.h @@ -1923,10 +1923,70 @@ static inline uint8_t lean_float_decLt(double a, double b) { return a < b; } static inline double lean_uint64_to_float(uint64_t a) { return (double) a; } /* Efficient C implementations of defns used by the compiler */ -static inline size_t lean_data_hashmap_mk_idx(lean_object* sz, uint64_t hash) { +static inline size_t lean_hashmap_mk_idx(lean_obj_arg sz, uint64_t hash) { return (size_t)(hash & (lean_unbox(sz) - 1)); } +static inline size_t lean_hashset_mk_idx(lean_obj_arg sz, uint64_t hash) { + return (size_t)(hash & (lean_unbox(sz) - 1)); +} + +static inline uint64_t lean_expr_data(lean_obj_arg expr) { + return lean_ctor_get_uint64(expr, lean_ctor_num_objs(expr)*sizeof(void*)); +} + +static inline lean_obj_res lean_get_max_ctor_fields(lean_obj_arg _unit) { + return lean_box(LEAN_MAX_CTOR_FIELDS); +} + +static inline lean_obj_res lean_get_max_ctor_scalars_size(lean_obj_arg _unit) { + return lean_box(LEAN_MAX_CTOR_SCALARS_SIZE); +} + +static inline lean_obj_res lean_get_usize_size(lean_obj_arg _unit) { + return lean_box(sizeof(size_t)); +} + +static inline lean_obj_res lean_get_max_ctor_tag(lean_obj_arg _unit) { + return lean_box(LeanMaxCtorTag); +} + +static inline uint8_t lean_strict_or(uint8_t b1, uint8_t b2) { + return b1 || b2; +} + +static inline uint8_t lean_strict_and(uint8_t b1, uint8_t b2) { + return b1 && b2; +} + +static inline lean_obj_res lean_version_get_major(lean_obj_arg _unit) { + return lean_box(LEAN_VERSION_MAJOR); +} + +static inline lean_obj_res lean_version_get_minor(lean_obj_arg _unit) { + return lean_box(LEAN_VERSION_MINOR); +} + +static inline lean_obj_res lean_version_get_patch(lean_obj_arg _unit) { + return lean_box(LEAN_VERSION_PATCH); +} + +static inline uint8_t lean_version_get_is_release(lean_obj_arg _unit) { + return LEAN_VERSION_IS_RELEASE; +} + +static inline lean_obj_res lean_version_get_special_desc(lean_obj_arg _unit) { + return lean_mk_string(LEAN_SPECIAL_VERSION_DESC); +} + +static inline uint8_t lean_internal_is_stage0(lean_obj_arg _unit) { + return LEAN_IS_STAGE0; +} + +static inline lean_obj_res lean_nat_pred(b_lean_obj_arg n) { + return lean_nat_sub(n, lean_box(1)); +} + #ifdef __cplusplus } #endif