diff --git a/juvix-stdlib b/juvix-stdlib index 297601a98..d8eea7a20 160000 --- a/juvix-stdlib +++ b/juvix-stdlib @@ -1 +1 @@ -Subproject commit 297601a98dcace657aaff6e42945f1430647885b +Subproject commit d8eea7a2038f93fa2f2100434742cd9773300b43 diff --git a/runtime/c/src/juvix/api.h b/runtime/c/src/juvix/api.h index 5002188e8..07fa99533 100644 --- a/runtime/c/src/juvix/api.h +++ b/runtime/c/src/juvix/api.h @@ -100,6 +100,10 @@ closure_label: #define JUVIX_ASSIGN(var0, val) (var0 = val) +#define JUVIX_UINT8_TO_INT(var0, var1) (var0 = var1) +#define JUVIX_INT_TO_UINT8(var0, var1) \ + (var0 = make_smallint((word_t)((uint8_t)(get_unboxed_int(var1) & 0xFF)))) + #define JUVIX_TRACE(val) (io_trace(val)) #define JUVIX_DUMP (stacktrace_dump()) #define JUVIX_FAILURE(val) \ diff --git a/runtime/rust/juvix/src/integer.rs b/runtime/rust/juvix/src/integer.rs index 41282da4d..61aeecd8b 100644 --- a/runtime/rust/juvix/src/integer.rs +++ b/runtime/rust/juvix/src/integer.rs @@ -38,6 +38,15 @@ pub fn smallint_le(x: Word, y: Word) -> Word { bool_to_word(smallint_value(x) <= smallint_value(y)) } + +pub fn uint8_to_int(x : Word) -> Word { + x +} + +pub fn int_to_uint8(x : Word) -> Word { + make_smallint(smallint_value(x).rem_euclid(256)) +} + #[cfg(test)] mod tests { use super::*; @@ -65,4 +74,12 @@ mod tests { assert_eq!(make_smallint(x), y); } } + + #[test] + fn test_int_to_uint8() { + assert_eq!(smallint_value(int_to_uint8(make_smallint(-1))), 255); + assert_eq!(smallint_value(int_to_uint8(make_smallint(255))), 255); + assert_eq!(smallint_value(int_to_uint8(make_smallint(-256))), 0); + assert_eq!(smallint_value(int_to_uint8(make_smallint(256))), 0); + } } diff --git a/src/Juvix/Compiler/Asm/Extra/Memory.hs b/src/Juvix/Compiler/Asm/Extra/Memory.hs index 17e98ddc9..729940469 100644 --- a/src/Juvix/Compiler/Asm/Extra/Memory.hs +++ b/src/Juvix/Compiler/Asm/Extra/Memory.hs @@ -109,6 +109,7 @@ getConstantType = \case ConstString {} -> TyString ConstUnit -> TyUnit ConstVoid -> TyVoid + ConstUInt8 {} -> mkTypeUInt8 getValueType' :: (Member (Error AsmError) r) => Maybe Location -> InfoTable -> Memory -> Value -> Sem r Type getValueType' loc tab mem = \case diff --git a/src/Juvix/Compiler/Asm/Extra/Recursors.hs b/src/Juvix/Compiler/Asm/Extra/Recursors.hs index abeaae4f2..f51515a92 100644 --- a/src/Juvix/Compiler/Asm/Extra/Recursors.hs +++ b/src/Juvix/Compiler/Asm/Extra/Recursors.hs @@ -189,6 +189,10 @@ recurse' sig = go True checkUnop mkTypeInteger TyField OpFieldToInt -> checkUnop TyField mkTypeInteger + OpUInt8ToInt -> + checkUnop mkTypeUInt8 mkTypeInteger + OpIntToUInt8 -> + checkUnop mkTypeInteger mkTypeUInt8 where checkUnop :: Type -> Type -> Sem r Memory checkUnop ty1 ty2 = do diff --git a/src/Juvix/Compiler/Backend/C/Translation/FromReg.hs b/src/Juvix/Compiler/Backend/C/Translation/FromReg.hs index 9749de1da..d312c8076 100644 --- a/src/Juvix/Compiler/Backend/C/Translation/FromReg.hs +++ b/src/Juvix/Compiler/Backend/C/Translation/FromReg.hs @@ -311,6 +311,8 @@ fromRegInstr bNoStack info = \case Reg.OpArgsNum -> "JUVIX_ARGS_NUM" Reg.OpFieldToInt -> unsupported "field type" Reg.OpIntToField -> unsupported "field type" + Reg.OpUInt8ToInt -> "JUVIX_UINT8_TO_INT" + Reg.OpIntToUInt8 -> "JUVIX_INT_TO_UINT8" fromVarRef :: Reg.VarRef -> Expression fromVarRef Reg.VarRef {..} = @@ -347,6 +349,7 @@ fromRegInstr bNoStack info = \case Reg.ConstString x -> macroCall "GET_CONST_CSTRING" [integer (getStringId info x)] Reg.ConstUnit -> macroVar "OBJ_UNIT" Reg.ConstVoid -> macroVar "OBJ_VOID" + Reg.ConstUInt8 x -> macroCall "make_smallint" [integer x] fromPrealloc :: Reg.InstrPrealloc -> Statement fromPrealloc Reg.InstrPrealloc {..} = diff --git a/src/Juvix/Compiler/Backend/Rust/Translation/FromReg.hs b/src/Juvix/Compiler/Backend/Rust/Translation/FromReg.hs index 6ac25e5b8..274ab200d 100644 --- a/src/Juvix/Compiler/Backend/Rust/Translation/FromReg.hs +++ b/src/Juvix/Compiler/Backend/Rust/Translation/FromReg.hs @@ -205,6 +205,14 @@ fromRegInstr info = \case (mkCall "mem.get_closure_largs" [fromValue _instrUnopArg]) Reg.OpFieldToInt -> unsupported "field type" Reg.OpIntToField -> unsupported "field type" + Reg.OpUInt8ToInt -> + stmtAssign + (mkVarRef _instrUnopResult) + (mkCall "uint8_to_int" [fromValue _instrUnopArg]) + Reg.OpIntToUInt8 -> + stmtAssign + (mkVarRef _instrUnopResult) + (mkCall "int_to_uint8" [fromValue _instrUnopArg]) mkVarRef :: Reg.VarRef -> Text mkVarRef Reg.VarRef {..} = case _varRefGroup of @@ -242,6 +250,7 @@ fromRegInstr info = \case Reg.ConstString {} -> unsupported "strings" Reg.ConstUnit -> mkVar "OBJ_UNIT" Reg.ConstVoid -> mkVar "OBJ_VOID" + Reg.ConstUInt8 x -> mkCall "make_smallint" [mkInteger x] fromAlloc :: Reg.InstrAlloc -> [Statement] fromAlloc Reg.InstrAlloc {..} = diff --git a/src/Juvix/Compiler/Builtins.hs b/src/Juvix/Compiler/Builtins.hs index 87c92dda3..2648a6620 100644 --- a/src/Juvix/Compiler/Builtins.hs +++ b/src/Juvix/Compiler/Builtins.hs @@ -12,11 +12,13 @@ module Juvix.Compiler.Builtins module Juvix.Compiler.Builtins.Control, module Juvix.Compiler.Builtins.Anoma, module Juvix.Compiler.Builtins.Cairo, + module Juvix.Compiler.Builtins.Byte, ) where import Juvix.Compiler.Builtins.Anoma import Juvix.Compiler.Builtins.Bool +import Juvix.Compiler.Builtins.Byte import Juvix.Compiler.Builtins.Cairo import Juvix.Compiler.Builtins.Control import Juvix.Compiler.Builtins.Debug diff --git a/src/Juvix/Compiler/Builtins/Byte.hs b/src/Juvix/Compiler/Builtins/Byte.hs new file mode 100644 index 000000000..477398509 --- /dev/null +++ b/src/Juvix/Compiler/Builtins/Byte.hs @@ -0,0 +1,32 @@ +module Juvix.Compiler.Builtins.Byte where + +import Juvix.Compiler.Builtins.Effect +import Juvix.Compiler.Internal.Extra +import Juvix.Prelude + +registerByte :: (Member Builtins r) => AxiomDef -> Sem r () +registerByte d = do + 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 + byte_ <- getBuiltinName (getLoc f) BuiltinByte + bool_ <- getBuiltinName (getLoc f) BuiltinBool + 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 + byte_ <- getBuiltinName l BuiltinByte + nat <- getBuiltinName l BuiltinNat + 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 + byte_ <- getBuiltinName (getLoc f) BuiltinByte + nat_ <- getBuiltinName (getLoc f) BuiltinNat + unless (f ^. axiomType === (byte_ --> nat_)) (error "byte-to-nat has the wrong type signature") + registerBuiltin BuiltinByteToNat (f ^. axiomName) diff --git a/src/Juvix/Compiler/Casm/Translation/FromReg.hs b/src/Juvix/Compiler/Casm/Translation/FromReg.hs index 9e3f3b288..1cac6232e 100644 --- a/src/Juvix/Compiler/Casm/Translation/FromReg.hs +++ b/src/Juvix/Compiler/Casm/Translation/FromReg.hs @@ -249,6 +249,7 @@ fromReg tab = mkResult $ run $ runLabelInfoBuilderWithNextId (Reg.getNextSymbolI Reg.ConstUnit -> 0 Reg.ConstVoid -> 0 Reg.ConstString {} -> unsupported "strings" + Reg.ConstUInt8 {} -> unsupported "uint8" mkLoad :: Reg.ConstrField -> Sem r RValue mkLoad Reg.ConstrField {..} = do @@ -458,6 +459,8 @@ fromReg tab = mkResult $ run $ runLabelInfoBuilderWithNextId (Reg.getNextSymbolI Reg.OpFieldToInt -> goAssignValue _instrUnopResult _instrUnopArg Reg.OpIntToField -> goAssignValue _instrUnopResult _instrUnopArg Reg.OpArgsNum -> goUnop' goOpArgsNum _instrUnopResult _instrUnopArg + Reg.OpUInt8ToInt -> unsupported "OpUInt8ToInt" + Reg.OpIntToUInt8 -> unsupported "OpIntToUInt8" goCairo :: Reg.InstrCairo -> Sem r () goCairo Reg.InstrCairo {..} = case _instrCairoOpcode of diff --git a/src/Juvix/Compiler/Concrete/Data/Builtins.hs b/src/Juvix/Compiler/Concrete/Data/Builtins.hs index 7c59b0564..6adf2536c 100644 --- a/src/Juvix/Compiler/Concrete/Data/Builtins.hs +++ b/src/Juvix/Compiler/Concrete/Data/Builtins.hs @@ -218,6 +218,10 @@ data BuiltinAxiom | BuiltinPoseidon | BuiltinEcOp | BuiltinRandomEcPoint + | BuiltinByte + | BuiltinByteEq + | BuiltinByteToNat + | BuiltinByteFromNat deriving stock (Show, Eq, Ord, Enum, Bounded, Generic, Data) instance HasNameKind BuiltinAxiom where @@ -255,6 +259,10 @@ instance HasNameKind BuiltinAxiom where BuiltinPoseidon -> KNameFunction BuiltinEcOp -> KNameFunction BuiltinRandomEcPoint -> KNameFunction + BuiltinByte -> KNameInductive + BuiltinByteEq -> KNameFunction + BuiltinByteToNat -> KNameFunction + BuiltinByteFromNat -> KNameFunction getNameKindPretty :: BuiltinAxiom -> NameKind getNameKindPretty = getNameKind @@ -300,6 +308,10 @@ instance Pretty BuiltinAxiom where BuiltinPoseidon -> Str.cairoPoseidon BuiltinEcOp -> Str.cairoEcOp BuiltinRandomEcPoint -> Str.cairoRandomEcPoint + BuiltinByte -> Str.byte_ + BuiltinByteEq -> Str.byteEq + BuiltinByteToNat -> Str.byteToNat + BuiltinByteFromNat -> Str.byteFromNat data BuiltinType = BuiltinTypeInductive BuiltinInductive diff --git a/src/Juvix/Compiler/Core/Evaluator.hs b/src/Juvix/Compiler/Core/Evaluator.hs index 957860479..b30f90b58 100644 --- a/src/Juvix/Compiler/Core/Evaluator.hs +++ b/src/Juvix/Compiler/Core/Evaluator.hs @@ -213,6 +213,8 @@ geval opts herr tab env0 = eval' env0 OpPoseidonHash -> poseidonHashOp OpEc -> ecOp OpRandomEcPoint -> randomEcPointOp + OpUInt8ToInt -> uint8ToIntOp + OpUInt8FromInt -> uint8FromIntOp where err :: Text -> a err msg = evalError msg n @@ -509,6 +511,28 @@ geval opts herr tab env0 = eval' env0 !publicKey = publicKeyFromInteger publicKeyInt in nodeFromBool (E.dverify publicKey message sig) {-# INLINE verifyDetached #-} + + uint8FromIntOp :: [Node] -> Node + uint8FromIntOp = + unary $ \node -> + let !v = eval' env node + in nodeFromUInt8 + . fromIntegral + . fromMaybe (evalError "expected integer" v) + . integerFromNode + $ v + {-# INLINE uint8FromIntOp #-} + + uint8ToIntOp :: [Node] -> Node + uint8ToIntOp = + unary $ \node -> + let !v = eval' env node + in nodeFromInteger + . toInteger + . fromMaybe (evalError "expected uint8" v) + . uint8FromNode + $ v + {-# INLINE uint8ToIntOp #-} {-# INLINE applyBuiltin #-} -- secretKey, publicKey are not encoded with their length as @@ -530,6 +554,10 @@ geval opts herr tab env0 = eval' env0 nodeFromField !fld = mkConstant' (ConstField fld) {-# INLINE nodeFromField #-} + nodeFromUInt8 :: Word8 -> Node + nodeFromUInt8 !w = mkConstant' (ConstUInt8 w) + {-# INLINE nodeFromUInt8 #-} + nodeFromBool :: Bool -> Node nodeFromBool b = mkConstr' (BuiltinTag tag) [] where @@ -577,6 +605,12 @@ geval opts herr tab env0 = eval' env0 _ -> Nothing {-# INLINE fieldFromNode #-} + uint8FromNode :: Node -> Maybe Word8 + uint8FromNode = \case + NCst (Constant _ (ConstUInt8 i)) -> Just i + _ -> Nothing + {-# INLINE uint8FromNode #-} + printNode :: Node -> Text printNode = \case NCst (Constant _ (ConstString s)) -> s diff --git a/src/Juvix/Compiler/Core/Extra/Base.hs b/src/Juvix/Compiler/Core/Extra/Base.hs index 9765916b7..d4b1bf607 100644 --- a/src/Juvix/Compiler/Core/Extra/Base.hs +++ b/src/Juvix/Compiler/Core/Extra/Base.hs @@ -194,6 +194,12 @@ mkTypeField i = mkTypePrim i PrimField mkTypeField' :: Type mkTypeField' = mkTypeField Info.empty +mkTypeUInt8 :: Info -> Type +mkTypeUInt8 i = mkTypePrim i primitiveUInt8 + +mkTypeUInt8' :: Type +mkTypeUInt8' = mkTypeUInt8 Info.empty + mkDynamic :: Info -> Type mkDynamic i = NDyn (DynamicTy i) diff --git a/src/Juvix/Compiler/Core/Extra/Utils.hs b/src/Juvix/Compiler/Core/Extra/Utils.hs index 042c354c2..5c4c573a0 100644 --- a/src/Juvix/Compiler/Core/Extra/Utils.hs +++ b/src/Juvix/Compiler/Core/Extra/Utils.hs @@ -433,6 +433,8 @@ builtinOpArgTypes = \case OpPoseidonHash -> [mkDynamic'] OpEc -> [mkDynamic', mkTypeField', mkDynamic'] OpRandomEcPoint -> [] + OpUInt8ToInt -> [mkTypeUInt8'] + OpUInt8FromInt -> [mkTypeInteger'] translateCase :: (Node -> Node -> Node -> a) -> a -> Case -> a translateCase translateIfFun dflt Case {..} = case _caseBranches of diff --git a/src/Juvix/Compiler/Core/Language/Builtins.hs b/src/Juvix/Compiler/Core/Language/Builtins.hs index 3fd914cb3..c63684c1c 100644 --- a/src/Juvix/Compiler/Core/Language/Builtins.hs +++ b/src/Juvix/Compiler/Core/Language/Builtins.hs @@ -36,6 +36,8 @@ data BuiltinOp | OpPoseidonHash | OpEc | OpRandomEcPoint + | OpUInt8ToInt + | OpUInt8FromInt deriving stock (Eq, Generic) instance Serialize BuiltinOp @@ -90,6 +92,8 @@ builtinOpArgsNum = \case OpPoseidonHash -> 1 OpEc -> 3 OpRandomEcPoint -> 0 + OpUInt8ToInt -> 1 + OpUInt8FromInt -> 1 builtinConstrArgsNum :: BuiltinDataTag -> Int builtinConstrArgsNum = \case @@ -133,6 +137,8 @@ builtinIsFoldable = \case OpPoseidonHash -> False OpEc -> False OpRandomEcPoint -> False + OpUInt8ToInt -> True + OpUInt8FromInt -> True builtinIsCairo :: BuiltinOp -> Bool builtinIsCairo op = op `elem` builtinsCairo @@ -156,3 +162,6 @@ builtinsAnoma = OpAnomaVerifyWithMessage, OpAnomaSignDetached ] + +builtinsUInt8 :: [BuiltinOp] +builtinsUInt8 = [OpUInt8FromInt, OpUInt8ToInt] diff --git a/src/Juvix/Compiler/Core/Language/Nodes.hs b/src/Juvix/Compiler/Core/Language/Nodes.hs index d12ff2565..c956a73a9 100644 --- a/src/Juvix/Compiler/Core/Language/Nodes.hs +++ b/src/Juvix/Compiler/Core/Language/Nodes.hs @@ -38,6 +38,7 @@ data ConstantValue = ConstInteger !Integer | ConstField !FField | ConstString !Text + | ConstUInt8 !Word8 deriving stock (Eq, Generic) -- | Info about a single binder. Associated with Lambda, Pi, Let, Case or Match. diff --git a/src/Juvix/Compiler/Core/Language/Primitives.hs b/src/Juvix/Compiler/Core/Language/Primitives.hs index 839d47b3a..ea008e0a0 100644 --- a/src/Juvix/Compiler/Core/Language/Primitives.hs +++ b/src/Juvix/Compiler/Core/Language/Primitives.hs @@ -17,6 +17,15 @@ data Primitive | PrimField deriving stock (Eq, Generic) +primitiveUInt8 :: Primitive +primitiveUInt8 = + PrimInteger + ( PrimIntegerInfo + { _infoMinValue = Just 0, + _infoMaxValue = Just 255 + } + ) + -- | Info about a type represented as an integer. data PrimIntegerInfo = PrimIntegerInfo { _infoMinValue :: Maybe Integer, diff --git a/src/Juvix/Compiler/Core/Pretty/Base.hs b/src/Juvix/Compiler/Core/Pretty/Base.hs index b0f102a84..f90e30951 100644 --- a/src/Juvix/Compiler/Core/Pretty/Base.hs +++ b/src/Juvix/Compiler/Core/Pretty/Base.hs @@ -62,6 +62,8 @@ instance PrettyCode BuiltinOp where OpPoseidonHash -> return primPoseidonHash OpEc -> return primEc OpRandomEcPoint -> return primRandomEcPoint + OpUInt8ToInt -> return primUInt8ToInt + OpUInt8FromInt -> return primFieldFromInt instance PrettyCode BuiltinDataTag where ppCode = \case @@ -107,6 +109,8 @@ instance PrettyCode ConstantValue where return $ annotate AnnLiteralInteger (pretty int) ConstField fld -> return $ annotate AnnLiteralInteger (pretty fld) + ConstUInt8 i -> + return $ annotate AnnLiteralInteger (pretty i) ConstString txt -> return $ annotate AnnLiteralString (pretty (show txt :: String)) @@ -114,6 +118,8 @@ instance PrettyCode (Constant' i) where ppCode Constant {..} = case _constantValue of ConstField fld -> return $ annotate AnnLiteralInteger (pretty fld <> "F") + ConstUInt8 i -> + return $ annotate AnnLiteralInteger (pretty i <> "u8") _ -> ppCode _constantValue instance (PrettyCode a, HasAtomicity a) => PrettyCode (App' i a) where @@ -732,6 +738,12 @@ primFieldDiv = primitive Str.fdiv primFieldFromInt :: Doc Ann primFieldFromInt = primitive Str.itof +primUInt8ToInt :: Doc Ann +primUInt8ToInt = primitive Str.u8toi + +primUInt8FromInt :: Doc Ann +primUInt8FromInt = primitive Str.itou8 + primFieldToInt :: Doc Ann primFieldToInt = primitive Str.ftoi diff --git a/src/Juvix/Compiler/Core/Transformation/Check/Cairo.hs b/src/Juvix/Compiler/Core/Transformation/Check/Cairo.hs index 827987804..8b7b3fb7e 100644 --- a/src/Juvix/Compiler/Core/Transformation/Check/Cairo.hs +++ b/src/Juvix/Compiler/Core/Transformation/Check/Cairo.hs @@ -12,7 +12,7 @@ checkCairo md = do checkMainType checkNoAxioms md mapAllNodesM checkNoIO md - mapAllNodesM (checkBuiltins' builtinsString [PrimString]) md + mapAllNodesM (checkBuiltins' (builtinsString ++ builtinsUInt8) [PrimString, primitiveUInt8]) md where checkMainType :: Sem r () checkMainType = diff --git a/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs b/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs index 272dc8e8a..e79b027f4 100644 --- a/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs +++ b/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs @@ -34,6 +34,7 @@ computeNodeTypeInfo md = umapL go ConstInteger {} -> mkTypeInteger' ConstField {} -> mkTypeField' ConstString {} -> mkTypeString' + ConstUInt8 {} -> mkTypeUInt8' NApp {} -> let (fn, args) = unfoldApps' node fty = Info.getNodeType fn @@ -82,6 +83,8 @@ computeNodeTypeInfo md = umapL go OpRandomEcPoint -> case _builtinAppArgs of [] -> mkDynamic' _ -> error "incorrect random_ec_point builtin application" + OpUInt8ToInt -> mkTypeInteger' + OpUInt8FromInt -> mkTypeUInt8' NCtr Constr {..} -> let ci = lookupConstructorInfo md _constrTag ii = lookupInductiveInfo md (ci ^. constructorInductive) diff --git a/src/Juvix/Compiler/Core/Transformation/ConvertBuiltinTypes.hs b/src/Juvix/Compiler/Core/Transformation/ConvertBuiltinTypes.hs index 8f496beb5..5746972dd 100644 --- a/src/Juvix/Compiler/Core/Transformation/ConvertBuiltinTypes.hs +++ b/src/Juvix/Compiler/Core/Transformation/ConvertBuiltinTypes.hs @@ -19,6 +19,7 @@ convertNode md = umap go Just (BuiltinTypeInductive BuiltinInt) -> mkTypeInteger' Just (BuiltinTypeAxiom BuiltinString) -> mkTypeString' Just (BuiltinTypeAxiom BuiltinField) -> mkTypeField' + Just (BuiltinTypeAxiom BuiltinByte) -> mkTypeUInt8' _ -> node where ii = lookupInductiveInfo md _typeConstrSymbol diff --git a/src/Juvix/Compiler/Core/Translation/FromInternal.hs b/src/Juvix/Compiler/Core/Translation/FromInternal.hs index 604291812..6551eb4b7 100644 --- a/src/Juvix/Compiler/Core/Translation/FromInternal.hs +++ b/src/Juvix/Compiler/Core/Translation/FromInternal.hs @@ -614,6 +614,10 @@ goAxiomInductive a = whenJust (a ^. Internal.axiomBuiltin) builtinInductive Internal.BuiltinPoseidon -> return () Internal.BuiltinEcOp -> return () Internal.BuiltinRandomEcPoint -> return () + Internal.BuiltinByte -> registerInductiveAxiom (Just BuiltinByte) [] + Internal.BuiltinByteEq -> return () + Internal.BuiltinByteToNat -> return () + Internal.BuiltinByteFromNat -> return () registerInductiveAxiom :: Maybe BuiltinAxiom -> [(Tag, Text, Type -> Type, Maybe BuiltinConstructor)] -> Sem r () registerInductiveAxiom ax ctrs = do @@ -815,6 +819,13 @@ goAxiomDef a = maybe goAxiomNotBuiltin builtinBody (a ^. Internal.axiomBuiltin) $ mkBuiltinApp' OpEc [mkVar' 2, mkVar' 1, mkVar' 0] Internal.BuiltinRandomEcPoint -> do registerAxiomDef (mkBuiltinApp' OpRandomEcPoint []) + Internal.BuiltinByte -> return () + Internal.BuiltinByteEq -> + registerAxiomDef (mkLambda' mkTypeUInt8' (mkLambda' mkTypeUInt8' (mkBuiltinApp' OpEq [mkVar' 1, mkVar' 0]))) + Internal.BuiltinByteToNat -> + registerAxiomDef (mkLambda' mkTypeUInt8' (mkBuiltinApp' OpUInt8ToInt [mkVar' 0])) + Internal.BuiltinByteFromNat -> + registerAxiomDef (mkLambda' mkTypeInteger' (mkBuiltinApp' OpUInt8FromInt [mkVar' 0])) axiomType' :: Sem r Type axiomType' = fromTopIndex (goType (a ^. Internal.axiomType)) @@ -1212,6 +1223,10 @@ goApplication a = do Just Internal.BuiltinPoseidon -> app Just Internal.BuiltinEcOp -> app Just Internal.BuiltinRandomEcPoint -> app + Just Internal.BuiltinByte -> app + Just Internal.BuiltinByteEq -> app + Just Internal.BuiltinByteToNat -> app + Just Internal.BuiltinByteFromNat -> app Nothing -> app Internal.ExpressionIden (Internal.IdenFunction n) -> do funInfoBuiltin <- Internal.getFunctionBuiltinInfo n diff --git a/src/Juvix/Compiler/Core/Translation/FromSource.hs b/src/Juvix/Compiler/Core/Translation/FromSource.hs index 1bb09ffd4..259208727 100644 --- a/src/Juvix/Compiler/Core/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Core/Translation/FromSource.hs @@ -599,6 +599,7 @@ atom :: ParsecS r Node atom varsNum vars = exprConstField + <|> exprConstUInt8 <|> exprConstInt <|> exprConstString <|> exprUniverse @@ -630,6 +631,11 @@ exprConstField = P.try $ do (n, i) <- field return $ mkConstant (Info.singleton (LocationInfo i)) (ConstField (fieldFromInteger defaultFieldSize n)) +exprConstUInt8 :: ParsecS r Node +exprConstUInt8 = P.try $ do + (n, i) <- uint8 + return $ mkConstant (Info.singleton (LocationInfo i)) (ConstUInt8 (fromIntegral n)) + exprUniverse :: ParsecS r Type exprUniverse = do kw kwType diff --git a/src/Juvix/Compiler/Core/Translation/FromSource/Lexer.hs b/src/Juvix/Compiler/Core/Translation/FromSource/Lexer.hs index 7b8038fc2..2983361ad 100644 --- a/src/Juvix/Compiler/Core/Translation/FromSource/Lexer.hs +++ b/src/Juvix/Compiler/Core/Translation/FromSource/Lexer.hs @@ -30,6 +30,9 @@ kw = void . lexeme . kw' field :: ParsecS r (Integer, Interval) field = lexemeInterval field' +uint8 :: ParsecS r (Integer, Interval) +uint8 = lexemeInterval uint8' + integer :: ParsecS r (WithLoc Integer) integer = lexeme integer' diff --git a/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs b/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs index 0afe527cf..34c051b24 100644 --- a/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs +++ b/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs @@ -108,6 +108,10 @@ fromCore fsize tab = BuiltinPoseidon -> False BuiltinEcOp -> False BuiltinRandomEcPoint -> False + BuiltinByte -> False + BuiltinByteEq -> False + BuiltinByteToNat -> False + BuiltinByteFromNat -> False BuiltinTypeInductive i -> case i of BuiltinList -> True BuiltinMaybe -> True diff --git a/src/Juvix/Compiler/Internal/Language.hs b/src/Juvix/Compiler/Internal/Language.hs index 8a98ffc9a..44da1c09d 100644 --- a/src/Juvix/Compiler/Internal/Language.hs +++ b/src/Juvix/Compiler/Internal/Language.hs @@ -170,9 +170,9 @@ data Literal = LitString Text | -- | `LitNumeric` represents a numeric literal of undetermined type LitNumeric Integer - | -- | `LitInteger` represents a literal of type `Int` + | -- | `LitInteger` represents a literal with trait `Integral` LitInteger Integer - | -- | `LitNatural` represents a literal of type `Nat` + | -- | `LitNatural` represents a literal with trait `FromNatural` LitNatural Integer deriving stock (Show, Eq, Ord, Generic, Data) diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs index a605dd60a..677ec97b0 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs @@ -587,6 +587,10 @@ registerBuiltinAxiom d = \case BuiltinPoseidon -> registerPoseidon d BuiltinEcOp -> registerEcOp d BuiltinRandomEcPoint -> registerRandomEcPoint d + BuiltinByte -> registerByte d + BuiltinByteEq -> registerByteEq d + BuiltinByteToNat -> registerByteToNat d + BuiltinByteFromNat -> registerByteFromNat d goInductive :: (Members '[Reader EntryPoint, Reader DefaultArgsStack, NameIdGen, Reader Pragmas, Builtins, Error ScoperError, State ConstructorInfos, Reader S.InfoTable] r) => diff --git a/src/Juvix/Compiler/Nockma/Translation/FromTree.hs b/src/Juvix/Compiler/Nockma/Translation/FromTree.hs index d8431233b..e8c7d8639 100644 --- a/src/Juvix/Compiler/Nockma/Translation/FromTree.hs +++ b/src/Juvix/Compiler/Nockma/Translation/FromTree.hs @@ -440,6 +440,7 @@ compile = \case Tree.ConstUnit -> OpQuote # constUnit Tree.ConstVoid -> OpQuote # constVoid Tree.ConstField {} -> fieldErr + Tree.ConstUInt8 i -> nockIntegralLiteral i goConstString :: Text -> Term Natural goConstString t = @@ -508,6 +509,8 @@ compile = \case in sub (getF ClosureTotalArgsNum) (getF ClosureArgsNum) Tree.OpIntToField -> fieldErr Tree.OpFieldToInt -> fieldErr + Tree.OpIntToUInt8 -> intToUInt8 arg + Tree.OpUInt8ToInt -> arg goAnomaGet :: [Term Natural] -> Sem r (Term Natural) goAnomaGet key = do @@ -1183,3 +1186,9 @@ add a b = callStdlib StdlibAdd [a, b] dec :: Term Natural -> Term Natural dec = callStdlib StdlibDec . pure + +intToUInt8 :: Term Natural -> Term Natural +intToUInt8 i = callStdlib StdlibMod [i, nockIntegralLiteral @Natural (2 ^ uint8Size)] + where + uint8Size :: Natural + uint8Size = 8 diff --git a/src/Juvix/Compiler/Tree/Evaluator.hs b/src/Juvix/Compiler/Tree/Evaluator.hs index e598d192e..c3c79b2dd 100644 --- a/src/Juvix/Compiler/Tree/Evaluator.hs +++ b/src/Juvix/Compiler/Tree/Evaluator.hs @@ -231,6 +231,7 @@ valueToNode = \case _nodeAllocClosureFunSymbol = _closureSymbol, _nodeAllocClosureArgs = map valueToNode _closureArgs } + ValUInt8 i -> mkConst $ ConstUInt8 i hEvalIO :: (MonadIO m) => Handle -> Handle -> InfoTable -> FunctionInfo -> m Value hEvalIO hin hout infoTable funInfo = do diff --git a/src/Juvix/Compiler/Tree/Evaluator/Builtins.hs b/src/Juvix/Compiler/Tree/Evaluator/Builtins.hs index e9ea9bd8b..58b8e5377 100644 --- a/src/Juvix/Compiler/Tree/Evaluator/Builtins.hs +++ b/src/Juvix/Compiler/Tree/Evaluator/Builtins.hs @@ -63,6 +63,8 @@ evalUnop tab op v = case op of OpFieldToInt -> goFieldToInt v OpIntToField -> goIntToField v OpArgsNum -> goArgsNum v + OpUInt8ToInt -> goUInt8ToInt v + OpIntToUInt8 -> goIntToUInt8 v where strToInt :: Text -> Either ErrorMsg Value strToInt s = case T.readMaybe (fromText s) of @@ -100,6 +102,20 @@ evalUnop tab op v = case op of _ -> Left "expected an integer" + goIntToUInt8 :: Value -> Either ErrorMsg Value + goIntToUInt8 = \case + ValInteger i -> + Right $ ValUInt8 $ fromIntegral i + _ -> + Left "expected an integer" + + goUInt8ToInt :: Value -> Either ErrorMsg Value + goUInt8ToInt = \case + ValUInt8 i -> + Right $ ValInteger $ toInteger i + _ -> + Left "expected a uint8" + printValue :: InfoTable' t e -> Value -> Text printValue tab = \case ValString s -> s @@ -113,6 +129,7 @@ constantToValue = \case ConstString s -> ValString s ConstUnit -> ValUnit ConstVoid -> ValVoid + ConstUInt8 i -> ValUInt8 i valueToConstant :: Value -> Constant valueToConstant = \case @@ -122,6 +139,7 @@ valueToConstant = \case ValString s -> ConstString s ValUnit -> ConstUnit ValVoid -> ConstVoid + ValUInt8 i -> ConstUInt8 i _ -> impossible evalBinop' :: BinaryOp -> Constant -> Constant -> Either ErrorMsg Constant diff --git a/src/Juvix/Compiler/Tree/Extra/Type.hs b/src/Juvix/Compiler/Tree/Extra/Type.hs index 2425f0d2e..1dfc32409 100644 --- a/src/Juvix/Compiler/Tree/Extra/Type.hs +++ b/src/Juvix/Compiler/Tree/Extra/Type.hs @@ -14,6 +14,9 @@ import Juvix.Compiler.Tree.Pretty mkTypeInteger :: Type mkTypeInteger = TyInteger (TypeInteger Nothing Nothing) +mkTypeUInt8 :: Type +mkTypeUInt8 = TyInteger (TypeInteger (Just 0) (Just 255)) + mkTypeBool :: Type mkTypeBool = TyBool (TypeBool (BuiltinTag TagTrue) (BuiltinTag TagFalse)) diff --git a/src/Juvix/Compiler/Tree/Language/Base.hs b/src/Juvix/Compiler/Tree/Language/Base.hs index f3711f8b1..99208bd70 100644 --- a/src/Juvix/Compiler/Tree/Language/Base.hs +++ b/src/Juvix/Compiler/Tree/Language/Base.hs @@ -18,6 +18,7 @@ data Constant | ConstField FField | ConstUnit | ConstVoid + | ConstUInt8 Word8 deriving stock (Eq, Generic) instance (Hashable Constant) diff --git a/src/Juvix/Compiler/Tree/Language/Builtins.hs b/src/Juvix/Compiler/Tree/Language/Builtins.hs index 7d99a3983..94b04cfa2 100644 --- a/src/Juvix/Compiler/Tree/Language/Builtins.hs +++ b/src/Juvix/Compiler/Tree/Language/Builtins.hs @@ -47,6 +47,10 @@ data UnaryOp OpIntToField | -- | Convert a field element to an integer. JV* opcode: `ftoi`. OpFieldToInt + | -- | Convert an integer to a UInt8. JV* opcode: `itou8` + OpIntToUInt8 + | -- | Convert an UInt8 to an integer. JV* opcode: `u8toi` + OpUInt8ToInt | -- | Compute the number of expected arguments for the given closure. JV* -- opcode: `argsnum`. OpArgsNum diff --git a/src/Juvix/Compiler/Tree/Language/Value.hs b/src/Juvix/Compiler/Tree/Language/Value.hs index 601d6e303..2e4387a6f 100644 --- a/src/Juvix/Compiler/Tree/Language/Value.hs +++ b/src/Juvix/Compiler/Tree/Language/Value.hs @@ -23,6 +23,7 @@ data Value | ValVoid | ValConstr Constr | ValClosure Closure + | ValUInt8 Word8 deriving stock (Eq) data Constr = Constr @@ -60,3 +61,4 @@ instance HasAtomicity Value where ValVoid -> Atom ValConstr c -> atomicity c ValClosure cl -> atomicity cl + ValUInt8 {} -> Atom diff --git a/src/Juvix/Compiler/Tree/Pretty/Base.hs b/src/Juvix/Compiler/Tree/Pretty/Base.hs index aeae737a2..bf5e665d0 100644 --- a/src/Juvix/Compiler/Tree/Pretty/Base.hs +++ b/src/Juvix/Compiler/Tree/Pretty/Base.hs @@ -99,6 +99,8 @@ instance PrettyCode Value where ppCode c ValClosure cl -> ppCode cl + ValUInt8 i -> + return $ integer i instance PrettyCode TypeInductive where ppCode :: (Member (Reader Options) r) => TypeInductive -> Sem r (Doc Ann) @@ -197,6 +199,8 @@ instance PrettyCode Constant where return $ annotate (AnnKind KNameConstructor) Str.unit ConstVoid {} -> return $ annotate (AnnKind KNameConstructor) Str.void + ConstUInt8 v -> + return $ annotate AnnLiteralInteger (pretty v) instance PrettyCode BoolOp where ppCode op = return $ primitive $ case op of @@ -239,6 +243,8 @@ instance PrettyCode UnaryOp where OpFieldToInt -> Str.instrFieldToInt OpIntToField -> Str.instrIntToField OpArgsNum -> Str.instrArgsNum + OpIntToUInt8 -> Str.instrIntToUInt8 + OpUInt8ToInt -> Str.instrUInt8ToInt instance PrettyCode CairoOp where ppCode op = return $ primitive $ case op of diff --git a/src/Juvix/Compiler/Tree/Transformation/Validate.hs b/src/Juvix/Compiler/Tree/Transformation/Validate.hs index e05f67a00..2565c7698 100644 --- a/src/Juvix/Compiler/Tree/Transformation/Validate.hs +++ b/src/Juvix/Compiler/Tree/Transformation/Validate.hs @@ -82,6 +82,8 @@ inferType tab funInfo = goInfer mempty OpArgsNum -> checkUnop TyDynamic mkTypeInteger OpIntToField -> checkUnop mkTypeInteger TyField OpFieldToInt -> checkUnop TyField mkTypeInteger + OpUInt8ToInt -> checkUnop mkTypeUInt8 mkTypeInteger + OpIntToUInt8 -> checkUnop mkTypeInteger mkTypeUInt8 goCairo :: BinderList Type -> NodeCairo -> Sem r Type goCairo bl NodeCairo {..} = do @@ -101,6 +103,7 @@ inferType tab funInfo = goInfer mempty ConstField {} -> return TyField ConstUnit {} -> return TyUnit ConstVoid {} -> return TyVoid + ConstUInt8 {} -> return mkTypeUInt8 goMemRef :: BinderList Type -> NodeMemRef -> Sem r Type goMemRef bl NodeMemRef {..} = case _nodeMemRef of diff --git a/src/Juvix/Compiler/Tree/Translation/FromCore.hs b/src/Juvix/Compiler/Tree/Translation/FromCore.hs index 422ce1ecc..587b4241d 100644 --- a/src/Juvix/Compiler/Tree/Translation/FromCore.hs +++ b/src/Juvix/Compiler/Tree/Translation/FromCore.hs @@ -85,6 +85,8 @@ genCode infoTable fi = mkConst (ConstString s) Core.Constant _ (Core.ConstField fld) -> mkConst (ConstField fld) + Core.Constant _ (Core.ConstUInt8 i) -> + mkConst (ConstUInt8 i) goApps :: Int -> BinderList MemRef -> Core.Apps -> Node goApps tempSize refs Core.Apps {..} = @@ -302,6 +304,8 @@ genCode infoTable fi = Core.OpFieldToInt -> PrimUnop OpFieldToInt Core.OpTrace -> OpTrace Core.OpFail -> OpFail + Core.OpUInt8FromInt -> PrimUnop OpIntToUInt8 + Core.OpUInt8ToInt -> PrimUnop OpUInt8ToInt _ -> impossible genCairoOp :: Core.BuiltinOp -> CairoOp diff --git a/src/Juvix/Extra/Strings.hs b/src/Juvix/Extra/Strings.hs index fd13d8d8f..df249563a 100644 --- a/src/Juvix/Extra/Strings.hs +++ b/src/Juvix/Extra/Strings.hs @@ -173,6 +173,18 @@ error = "error" string :: (IsString s) => s string = "string" +byte_ :: (IsString s) => s +byte_ = "byte" + +byteEq :: (IsString s) => s +byteEq = "byte-eq" + +byteToNat :: (IsString s) => s +byteToNat = "byte-to-nat" + +byteFromNat :: (IsString s) => s +byteFromNat = "byte-from-nat" + nat :: (IsString s) => s nat = "nat" @@ -389,6 +401,12 @@ ftoi = "ftoi" itof :: (IsString s) => s itof = "itof" +u8toi :: (IsString s) => s +u8toi = "u8toi" + +itou8 :: (IsString s) => s +itou8 = "itou8" + delimiter :: (IsString s) => s delimiter = "delimiter" @@ -770,6 +788,12 @@ instrFieldToInt = "ftoi" instrIntToField :: (IsString s) => s instrIntToField = "itof" +instrUInt8ToInt :: (IsString s) => s +instrUInt8ToInt = "u8toi" + +instrIntToUInt8 :: (IsString s) => s +instrIntToUInt8 = "itou8" + instrShow :: (IsString s) => s instrShow = "show" diff --git a/src/Juvix/Parser/Lexer.hs b/src/Juvix/Parser/Lexer.hs index cffbf31ee..8d4acd47d 100644 --- a/src/Juvix/Parser/Lexer.hs +++ b/src/Juvix/Parser/Lexer.hs @@ -166,6 +166,12 @@ field' = do P.chunk "F" return d +uint8' :: ParsecS r Integer +uint8' = do + d <- L.decimal + P.chunk "u8" + return d + -- | The caller is responsible of consuming space after it. delim' :: Text -> ParsecS r Interval delim' d = P.label (unpack d) . fmap snd . interval $ chunk d diff --git a/test/Anoma/Compilation/Positive.hs b/test/Anoma/Compilation/Positive.hs index 3843af88b..fea8d489c 100644 --- a/test/Anoma/Compilation/Positive.hs +++ b/test/Anoma/Compilation/Positive.hs @@ -594,5 +594,23 @@ allTests = [nock| 2 |], [nock| 3 |], [nock| nil |] + ], + mkAnomaCallTest + "Test081: UInt8" + $(mkRelDir ".") + $(mkRelFile "test081.juvix") + [] + $ checkOutput + [ [nock| 1 |], + [nock| 255 |], + [nock| 2 |], + [nock| true |], + [nock| true |], + [nock| false |], + [nock| 1 |], + [nock| 238 |], + [nock| 3 |], + [nock| 240 |], + [nock| [1 238 3 2 nil] |] ] ] diff --git a/test/Compilation/Positive.hs b/test/Compilation/Positive.hs index 941bbbab9..3a65505b6 100644 --- a/test/Compilation/Positive.hs +++ b/test/Compilation/Positive.hs @@ -460,5 +460,10 @@ tests = "Test077: Instance fields" $(mkRelDir ".") $(mkRelFile "test077.juvix") - $(mkRelFile "out/test077.out") + $(mkRelFile "out/test077.out"), + posTestEval + "Test078: Builtin Byte" + $(mkRelDir ".") + $(mkRelFile "test078.juvix") + $(mkRelFile "out/test078.out") ] diff --git a/test/Rust/Compilation/Positive.hs b/test/Rust/Compilation/Positive.hs index 05d4e38fa..c8ff0bc99 100644 --- a/test/Rust/Compilation/Positive.hs +++ b/test/Rust/Compilation/Positive.hs @@ -344,5 +344,10 @@ tests = "Test073: Import and use a syntax alias" $(mkRelDir "test073") $(mkRelFile "test073.juvix") - $(mkRelFile "out/test073.out") + $(mkRelFile "out/test073.out"), + posTest + "Test074: Builtin Byte" + $(mkRelDir ".") + $(mkRelFile "test074.juvix") + $(mkRelFile "out/test074.out") ] diff --git a/tests/Anoma/Compilation/positive/test081.juvix b/tests/Anoma/Compilation/positive/test081.juvix new file mode 100644 index 000000000..a34823b9b --- /dev/null +++ b/tests/Anoma/Compilation/positive/test081.juvix @@ -0,0 +1,35 @@ +module test081; + +import Stdlib.Prelude open; +import Stdlib.Debug.Trace open; + +n1 : Byte := fromNat 1; + +n2 : Byte := fromNat 0xff; + +n3 : Byte := fromNat 0x102; + +l1 : Byte := 1; + +l2 : Byte := 0xee; + +l3 : Byte := 0x103; + +xs : List Byte := [l1; l2; l3; 2]; + +printByteLn : Byte -> IO := Show.show >> printStringLn; + +printListByteLn : List Byte -> IO := Show.show >> printStringLn; + +main : List Byte := + trace n1 + >-> trace n2 + >-> trace n3 + >-> trace (n1 == l1) + >-> trace (l1 == 0x101) + >-> trace (l2 == n2) + >-> trace (Byte.toNat l1) + >-> trace (Byte.toNat l2) + >-> trace (Byte.toNat l3) + >-> trace (Byte.toNat 0xf0) + >-> xs; diff --git a/tests/Compilation/positive/out/test078.out b/tests/Compilation/positive/out/test078.out new file mode 100644 index 000000000..6224a0c85 --- /dev/null +++ b/tests/Compilation/positive/out/test078.out @@ -0,0 +1,11 @@ +1 +255 +2 +true +true +false +1 +238 +3 +240 +(1 :: 238 :: 3 :: 2 :: nil) diff --git a/tests/Compilation/positive/test078.juvix b/tests/Compilation/positive/test078.juvix new file mode 100644 index 000000000..898160edb --- /dev/null +++ b/tests/Compilation/positive/test078.juvix @@ -0,0 +1,34 @@ +module test078; + +import Stdlib.Prelude open; + +n1 : Byte := fromNat 1; + +n2 : Byte := fromNat 0xff; + +n3 : Byte := fromNat 0x102; + +l1 : Byte := 1; + +l2 : Byte := 0xee; + +l3 : Byte := 0x103; + +xs : List Byte := [l1; l2; l3; 2]; + +printByteLn : Byte -> IO := Show.show >> printStringLn; + +printListByteLn : List Byte -> IO := Show.show >> printStringLn; + +main : IO := + printByteLn n1 + >>> printByteLn n2 + >>> printByteLn n3 + >>> printBoolLn (n1 == l1) + >>> printBoolLn (l1 == 0x101) + >>> printBoolLn (l2 == n2) + >>> printNatLn (Byte.toNat l1) + >>> printNatLn (Byte.toNat l2) + >>> printNatLn (Byte.toNat l3) + >>> printNatLn (Byte.toNat 0xf0) + >>> printListByteLn xs; diff --git a/tests/Core/positive/out/test063.out b/tests/Core/positive/out/test063.out new file mode 100644 index 000000000..d00491fd7 --- /dev/null +++ b/tests/Core/positive/out/test063.out @@ -0,0 +1 @@ +1 diff --git a/tests/Core/positive/test063.jvc b/tests/Core/positive/test063.jvc new file mode 100644 index 000000000..246b87d2c --- /dev/null +++ b/tests/Core/positive/test063.jvc @@ -0,0 +1,5 @@ +-- UInt8 + +def f := \x x; + +f 257u8 diff --git a/tests/Rust/Compilation/positive/out/test074.out b/tests/Rust/Compilation/positive/out/test074.out index eb3e83f93..0cfbf0888 100644 --- a/tests/Rust/Compilation/positive/out/test074.out +++ b/tests/Rust/Compilation/positive/out/test074.out @@ -1 +1 @@ --1085550836599839364109196834928521031686932164599479009991927616840761606155 +2 diff --git a/tests/Rust/Compilation/positive/test074.juvix b/tests/Rust/Compilation/positive/test074.juvix new file mode 100644 index 000000000..7ac631c51 --- /dev/null +++ b/tests/Rust/Compilation/positive/test074.juvix @@ -0,0 +1,7 @@ +module test074; + +import Stdlib.Prelude open; + +n1 : Byte := Byte.fromNat 0xff; + +main : Byte := Byte.fromNat (Byte.toNat 0x103 + Byte.toNat n1);