From 85dcdcde93e1680aa9f17f34ad9fe71eae056b87 Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Sat, 17 Jul 2021 15:13:22 -0700 Subject: [PATCH] chore: use NonScalar --- src/Init/System/IO.lean | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean index 0ad1b0bbdf..2fd37bd93c 100644 --- a/src/Init/System/IO.lean +++ b/src/Init/System/IO.lean @@ -496,19 +496,17 @@ instance : MonadLift (ST IO.RealWorld) (EIO ε) := ⟨fun x s => def mkRef (a : α) : IO (IO.Ref α) := ST.mkRef a -/-- An opaque type for use in pointers to Lean objects. -/ -private constant Object : Type u - /-- Keeps an object alive by ensuring that its RC >= 1. Unlike holding typed `Ref`s, this structure is homogeneous. The ref can safely be shared between threads. -/ -structure UntypedRef where - ref : IO.Ref Object +structure UntypedRef where + ref : IO.Ref NonScalar ptr : USize namespace UntypedRef -/-- Creation is unsafe because it must be ensured that the `ref` field is never used to access -the value as a type other than `α`. -/ +/-- Creation is unsafe because it must be ensured that: +- the `ref` field is never used to access the value as a type other than `α` +- the type `α` is not a scalar -/ unsafe def mkRefUnsafe {α : Type u} (a : α) : IO UntypedRef := do let ref ← IO.mkRef (unsafeCast a) let ptr := ptrAddrUnsafe a