Skip to content

ReadKnownIn DefaultUni term Int64 should extract the Int directly #7501

@effectfully

Description

@effectfully

The instance is defined as

instance KnownBuiltinTypeIn DefaultUni term Integer => ReadKnownIn DefaultUni term Int64 where
  readKnown = readKnownAsInteger

where

readKnownAsInteger
  :: forall term a
   . (KnownBuiltinTypeIn DefaultUni term Integer, Integral a, Bounded a, Typeable a)
  => term -> ReadKnownM a
readKnownAsInteger term =
  inline readKnownConstant term >>= oneShot \(i :: Integer) ->
    if fromIntegral (minBound :: a) <= i && i <= fromIntegral (maxBound :: a)
      then pure $ fromIntegral i
      else
        throwError . operationalUnliftingError $ <...>

While readKnownAsInteger makes sense for most Integral types, it's very inefficient for Int64 specifically, because all you actually need to convert an Integer to Int64 on a 64-bit platform is to unwrap the latter from the IS constructor:

-- If the value is small (i.e., fits into an 'Int'), the 'IS' constructor is
-- used. Otherwise 'IP' and 'IN' constructors are used to store a 'BigNat'
-- representing the positive or the negative value magnitude, respectively.
--
-- Invariant: 'IP' and 'IN' are used iff the value does not fit in 'IS'.
data Integer
   = IS !Int#    -- ^ iff value in @[minBound::'Int', maxBound::'Int']@ range
   | IP !BigNat# -- ^ iff value in @]maxBound::'Int', +inf[@ range
   | IN !BigNat# -- ^ iff value in @]-inf, minBound::'Int'[@ range

Currently the ReadKnownIn DefaultUni term Int instance is under the #if WORD_SIZE_IN_BITS == 64 CPP pragma, but that one is guaranteed to be correct without the pragma if you just unwrap from the IS constructor and similarly ReadKnownIn DefaultUni term Word is guaranteed to be correct if you just use readKnownAsInteger there as nearly everywhere else, so I recommend doing it the other way around and deriving the instance for Int64 from the Int one -- and placing the former under the CPP pragma.

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions