Skip to content

Commit

Permalink
Rename uint8 to byte in builtin registration errors
Browse files Browse the repository at this point in the history
  • Loading branch information
paulcadman committed Aug 1, 2024
1 parent 1850062 commit 04b0df9
Showing 1 changed file with 7 additions and 7 deletions.
14 changes: 7 additions & 7 deletions src/Juvix/Compiler/Builtins/Byte.hs
Original file line number Diff line number Diff line change
Expand Up @@ -6,27 +6,27 @@ import Juvix.Prelude

registerByte :: (Member Builtins r) => AxiomDef -> Sem r ()
registerByte d = do
unless (isSmallUniverse' (d ^. axiomType)) (error "UInt8 should be in the small universe")
unless (isSmallUniverse' (d ^. axiomType)) (error "Byte should be in the small universe")
registerBuiltin BuiltinByte (d ^. axiomName)

registerByteEq :: (Member Builtins r) => AxiomDef -> Sem r ()
registerByteEq f = do
uint8 <- getBuiltinName (getLoc f) BuiltinByte
byte_ <- getBuiltinName (getLoc f) BuiltinByte
bool_ <- getBuiltinName (getLoc f) BuiltinBool
unless (f ^. axiomType === (uint8 --> uint8 --> bool_)) (error "UInt8 equality has the wrong type signature")
unless (f ^. axiomType === (byte_ --> byte_ --> bool_)) (error "Byte equality has the wrong type signature")
registerBuiltin BuiltinByteEq (f ^. axiomName)

registerByteFromNat :: (Member Builtins r) => AxiomDef -> Sem r ()
registerByteFromNat d = do
let l = getLoc d
uint8 <- getBuiltinName l BuiltinByte
byte_ <- getBuiltinName l BuiltinByte
nat <- getBuiltinName l BuiltinNat
unless (d ^. axiomType === (nat --> uint8)) (error "uint8-from-nat has the wrong type signature")
unless (d ^. axiomType === (nat --> byte_)) (error "byte-from-nat has the wrong type signature")
registerBuiltin BuiltinByteFromNat (d ^. axiomName)

registerByteToNat :: (Member Builtins r) => AxiomDef -> Sem r ()
registerByteToNat f = do
uint8 <- getBuiltinName (getLoc f) BuiltinByte
byte_ <- getBuiltinName (getLoc f) BuiltinByte
nat_ <- getBuiltinName (getLoc f) BuiltinNat
unless (f ^. axiomType === (uint8 --> nat_)) (error "uint8-to-nat conversion has the wrong type signature")
unless (f ^. axiomType === (byte_ --> nat_)) (error "byte-to-nat has the wrong type signature")
registerBuiltin BuiltinByteToNat (f ^. axiomName)

0 comments on commit 04b0df9

Please sign in to comment.