-
Notifications
You must be signed in to change notification settings - Fork 479
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[plc] Support for Natural
numbers in the universe, backed by Integer
#6346
Changes from all commits
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,3 @@ | ||
### Added | ||
|
||
- Support for `Natural` numbers in the default universe, backed by `Integer`. |
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -489,6 +489,26 @@ deriving newtype instance KnownBuiltinTypeIn DefaultUni term [a] => | |
deriving newtype instance KnownBuiltinTypeIn DefaultUni term [a] => | ||
ReadKnownIn DefaultUni term (ListCostedByLength a) | ||
|
||
deriving via AsInteger Natural instance | ||
KnownTypeAst tyname DefaultUni Natural | ||
deriving via AsInteger Natural instance HasConstantIn DefaultUni term => | ||
MakeKnownIn DefaultUni term Natural | ||
instance HasConstantIn DefaultUni term => ReadKnownIn DefaultUni term Natural where | ||
readKnown term = | ||
-- See Note [Performance of ReadKnownIn and MakeKnownIn instances]. | ||
-- Funnily, we don't need 'inline' here, unlike in the default implementation of 'readKnown' | ||
-- (go figure why). | ||
inline readKnownConstant term >>= oneShot \(i :: Integer) -> | ||
-- TODO: benchmark alternatives:signumInteger,integerIsNegative,integerToNaturalThrow | ||
if i >= 0 | ||
-- TODO: benchmark alternatives: ghc8.10 naturalFromInteger, ghc>=9 integerToNatural | ||
then pure $ fromInteger i | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. From a quick look There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I can't use integerToNatural since it is not in GHC8.10 without some macro switching. I will optimise later. |
||
else throwing _OperationalUnliftingError . MkUnliftingError $ fold | ||
[ Text.pack $ show i | ||
, " is not within the bounds of Natural" | ||
] | ||
{-# INLINE readKnown #-} | ||
|
||
{- Note [Stable encoding of tags] | ||
'encodeUni' and 'decodeUni' are used for serialisation and deserialisation of types from the | ||
universe and we need serialised things to be extremely stable, hence the definitions of 'encodeUni' | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The code duplication is unfortunate, but I don't have any better ideas either.