From a9900bf02a0187005308914df64bc1669f1f8996 Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Fri, 26 Jul 2024 16:43:01 +0100 Subject: [PATCH 01/21] Add support for unsigned 8-bit integer UInt8 Support is only provided in the Core and Anoma backends currently --- src/Juvix/Compiler/Asm/Extra/Memory.hs | 1 + src/Juvix/Compiler/Asm/Extra/Recursors.hs | 2 + .../Compiler/Backend/C/Translation/FromReg.hs | 2 + .../Backend/Rust/Translation/FromReg.hs | 2 + src/Juvix/Compiler/Builtins.hs | 2 + src/Juvix/Compiler/Builtins/UInt8.hs | 18 +++++++ .../Compiler/Casm/Translation/FromReg.hs | 2 + src/Juvix/Compiler/Concrete/Data/Builtins.hs | 6 +++ src/Juvix/Compiler/Core/Evaluator.hs | 16 ++++++ src/Juvix/Compiler/Core/Extra/Base.hs | 6 +++ src/Juvix/Compiler/Core/Extra/Utils.hs | 1 + src/Juvix/Compiler/Core/Language/Builtins.hs | 6 +++ src/Juvix/Compiler/Core/Language/Nodes.hs | 1 + .../Compiler/Core/Language/Primitives.hs | 9 ++++ src/Juvix/Compiler/Core/Pretty/Base.hs | 8 +++ .../Core/Transformation/Check/Base.hs | 4 ++ .../Core/Transformation/Check/Cairo.hs | 2 +- .../Core/Transformation/ComputeTypeInfo.hs | 2 + .../Transformation/ConvertBuiltinTypes.hs | 1 + .../Compiler/Core/Translation/FromInternal.hs | 7 +++ .../Compiler/Core/Translation/FromSource.hs | 6 +++ .../Core/Translation/FromSource/Lexer.hs | 3 ++ .../Core/Translation/Stripped/FromCore.hs | 2 + src/Juvix/Compiler/Internal/Language.hs | 4 +- .../Internal/Translation/FromConcrete.hs | 2 + .../Compiler/Nockma/Translation/FromTree.hs | 5 ++ src/Juvix/Compiler/Tree/Evaluator.hs | 1 + src/Juvix/Compiler/Tree/Evaluator/Builtins.hs | 9 ++++ src/Juvix/Compiler/Tree/Extra/Type.hs | 3 ++ src/Juvix/Compiler/Tree/Language/Base.hs | 1 + src/Juvix/Compiler/Tree/Language/Builtins.hs | 2 + src/Juvix/Compiler/Tree/Language/Value.hs | 2 + src/Juvix/Compiler/Tree/Pretty/Base.hs | 5 ++ .../Compiler/Tree/Transformation/Validate.hs | 2 + .../Compiler/Tree/Translation/FromCore.hs | 3 ++ src/Juvix/Extra/Strings.hs | 12 +++++ src/Juvix/Parser/Lexer.hs | 6 +++ test/Anoma/Compilation/Positive.hs | 9 ++++ test/Compilation/Positive.hs | 7 ++- .../Anoma/Compilation/positive/test081.juvix | 13 +++++ tests/Compilation/positive/out/test078.out | 1 + tests/Compilation/positive/test078.juvix | 52 +++++++++++++++++++ tests/Core/positive/out/test063.out | 1 + tests/Core/positive/test063.jvc | 5 ++ 44 files changed, 250 insertions(+), 4 deletions(-) create mode 100644 src/Juvix/Compiler/Builtins/UInt8.hs create mode 100644 tests/Anoma/Compilation/positive/test081.juvix create mode 100644 tests/Compilation/positive/out/test078.out create mode 100644 tests/Compilation/positive/test078.juvix create mode 100644 tests/Core/positive/out/test063.out create mode 100644 tests/Core/positive/test063.jvc diff --git a/src/Juvix/Compiler/Asm/Extra/Memory.hs b/src/Juvix/Compiler/Asm/Extra/Memory.hs index 17e98ddc9a..729940469f 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 abeaae4f22..03732e1472 100644 --- a/src/Juvix/Compiler/Asm/Extra/Recursors.hs +++ b/src/Juvix/Compiler/Asm/Extra/Recursors.hs @@ -189,6 +189,8 @@ recurse' sig = go True checkUnop mkTypeInteger TyField OpFieldToInt -> checkUnop TyField 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 9749de1da0..9e17358564 100644 --- a/src/Juvix/Compiler/Backend/C/Translation/FromReg.hs +++ b/src/Juvix/Compiler/Backend/C/Translation/FromReg.hs @@ -311,6 +311,7 @@ fromRegInstr bNoStack info = \case Reg.OpArgsNum -> "JUVIX_ARGS_NUM" Reg.OpFieldToInt -> unsupported "field type" Reg.OpIntToField -> unsupported "field type" + Reg.OpIntToUInt8 -> unsupported "uint8 type" fromVarRef :: Reg.VarRef -> Expression fromVarRef Reg.VarRef {..} = @@ -347,6 +348,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 {} -> impossible 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 6ac25e5b84..0f49d67864 100644 --- a/src/Juvix/Compiler/Backend/Rust/Translation/FromReg.hs +++ b/src/Juvix/Compiler/Backend/Rust/Translation/FromReg.hs @@ -205,6 +205,7 @@ fromRegInstr info = \case (mkCall "mem.get_closure_largs" [fromValue _instrUnopArg]) Reg.OpFieldToInt -> unsupported "field type" Reg.OpIntToField -> unsupported "field type" + Reg.OpIntToUInt8 -> unsupported "uint8 type" mkVarRef :: Reg.VarRef -> Text mkVarRef Reg.VarRef {..} = case _varRefGroup of @@ -242,6 +243,7 @@ fromRegInstr info = \case Reg.ConstString {} -> unsupported "strings" Reg.ConstUnit -> mkVar "OBJ_UNIT" Reg.ConstVoid -> mkVar "OBJ_VOID" + Reg.ConstUInt8 {} -> impossible fromAlloc :: Reg.InstrAlloc -> [Statement] fromAlloc Reg.InstrAlloc {..} = diff --git a/src/Juvix/Compiler/Builtins.hs b/src/Juvix/Compiler/Builtins.hs index 87c92dda3f..c946ba9458 100644 --- a/src/Juvix/Compiler/Builtins.hs +++ b/src/Juvix/Compiler/Builtins.hs @@ -12,6 +12,7 @@ module Juvix.Compiler.Builtins module Juvix.Compiler.Builtins.Control, module Juvix.Compiler.Builtins.Anoma, module Juvix.Compiler.Builtins.Cairo, + module Juvix.Compiler.Builtins.UInt8, ) where @@ -28,3 +29,4 @@ import Juvix.Compiler.Builtins.List import Juvix.Compiler.Builtins.Maybe import Juvix.Compiler.Builtins.Nat import Juvix.Compiler.Builtins.String +import Juvix.Compiler.Builtins.UInt8 diff --git a/src/Juvix/Compiler/Builtins/UInt8.hs b/src/Juvix/Compiler/Builtins/UInt8.hs new file mode 100644 index 0000000000..b6de6a640c --- /dev/null +++ b/src/Juvix/Compiler/Builtins/UInt8.hs @@ -0,0 +1,18 @@ +module Juvix.Compiler.Builtins.UInt8 where + +import Juvix.Compiler.Builtins.Effect +import Juvix.Compiler.Internal.Extra +import Juvix.Prelude + +registerUInt8 :: (Member Builtins r) => AxiomDef -> Sem r () +registerUInt8 d = do + unless (isSmallUniverse' (d ^. axiomType)) (error "UInt8 should be in the small universe") + registerBuiltin BuiltinUInt8 (d ^. axiomName) + +registerUInt8FromNat :: (Member Builtins r) => AxiomDef -> Sem r () +registerUInt8FromNat d = do + let l = getLoc d + uint8 <- getBuiltinName l BuiltinUInt8 + nat <- getBuiltinName l BuiltinNat + unless (d ^. axiomType === (nat --> uint8)) (error "uint8-from-nat has the wrong type signature") + registerBuiltin BuiltinUInt8FromNat (d ^. axiomName) diff --git a/src/Juvix/Compiler/Casm/Translation/FromReg.hs b/src/Juvix/Compiler/Casm/Translation/FromReg.hs index 9e3f3b2887..4a8ec5bb68 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,7 @@ fromReg tab = mkResult $ run $ runLabelInfoBuilderWithNextId (Reg.getNextSymbolI Reg.OpFieldToInt -> goAssignValue _instrUnopResult _instrUnopArg Reg.OpIntToField -> goAssignValue _instrUnopResult _instrUnopArg Reg.OpArgsNum -> goUnop' goOpArgsNum _instrUnopResult _instrUnopArg + Reg.OpIntToUInt8 -> unsupported "uint8" 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 7c59b05647..2ba915371b 100644 --- a/src/Juvix/Compiler/Concrete/Data/Builtins.hs +++ b/src/Juvix/Compiler/Concrete/Data/Builtins.hs @@ -218,6 +218,8 @@ data BuiltinAxiom | BuiltinPoseidon | BuiltinEcOp | BuiltinRandomEcPoint + | BuiltinUInt8 + | BuiltinUInt8FromNat deriving stock (Show, Eq, Ord, Enum, Bounded, Generic, Data) instance HasNameKind BuiltinAxiom where @@ -255,6 +257,8 @@ instance HasNameKind BuiltinAxiom where BuiltinPoseidon -> KNameFunction BuiltinEcOp -> KNameFunction BuiltinRandomEcPoint -> KNameFunction + BuiltinUInt8 -> KNameInductive + BuiltinUInt8FromNat -> KNameFunction getNameKindPretty :: BuiltinAxiom -> NameKind getNameKindPretty = getNameKind @@ -300,6 +304,8 @@ instance Pretty BuiltinAxiom where BuiltinPoseidon -> Str.cairoPoseidon BuiltinEcOp -> Str.cairoEcOp BuiltinRandomEcPoint -> Str.cairoRandomEcPoint + BuiltinUInt8 -> Str.uint8 + BuiltinUInt8FromNat -> Str.uint8FromNat data BuiltinType = BuiltinTypeInductive BuiltinInductive diff --git a/src/Juvix/Compiler/Core/Evaluator.hs b/src/Juvix/Compiler/Core/Evaluator.hs index 957860479c..32a88e8252 100644 --- a/src/Juvix/Compiler/Core/Evaluator.hs +++ b/src/Juvix/Compiler/Core/Evaluator.hs @@ -213,6 +213,7 @@ geval opts herr tab env0 = eval' env0 OpPoseidonHash -> poseidonHashOp OpEc -> ecOp OpRandomEcPoint -> randomEcPointOp + OpUInt8FromInt -> uint8FromIntOp where err :: Text -> a err msg = evalError msg n @@ -509,6 +510,17 @@ 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 #-} {-# INLINE applyBuiltin #-} -- secretKey, publicKey are not encoded with their length as @@ -530,6 +542,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 diff --git a/src/Juvix/Compiler/Core/Extra/Base.hs b/src/Juvix/Compiler/Core/Extra/Base.hs index 9765916b77..d4b1bf6072 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 042c354c2a..f8f892c15c 100644 --- a/src/Juvix/Compiler/Core/Extra/Utils.hs +++ b/src/Juvix/Compiler/Core/Extra/Utils.hs @@ -433,6 +433,7 @@ builtinOpArgTypes = \case OpPoseidonHash -> [mkDynamic'] OpEc -> [mkDynamic', mkTypeField', mkDynamic'] OpRandomEcPoint -> [] + 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 3fd914cb32..501ff33f90 100644 --- a/src/Juvix/Compiler/Core/Language/Builtins.hs +++ b/src/Juvix/Compiler/Core/Language/Builtins.hs @@ -36,6 +36,7 @@ data BuiltinOp | OpPoseidonHash | OpEc | OpRandomEcPoint + | OpUInt8FromInt deriving stock (Eq, Generic) instance Serialize BuiltinOp @@ -90,6 +91,7 @@ builtinOpArgsNum = \case OpPoseidonHash -> 1 OpEc -> 3 OpRandomEcPoint -> 0 + OpUInt8FromInt -> 1 builtinConstrArgsNum :: BuiltinDataTag -> Int builtinConstrArgsNum = \case @@ -133,6 +135,7 @@ builtinIsFoldable = \case OpPoseidonHash -> False OpEc -> False OpRandomEcPoint -> False + OpUInt8FromInt -> True builtinIsCairo :: BuiltinOp -> Bool builtinIsCairo op = op `elem` builtinsCairo @@ -156,3 +159,6 @@ builtinsAnoma = OpAnomaVerifyWithMessage, OpAnomaSignDetached ] + +builtinsUInt8 :: [BuiltinOp] +builtinsUInt8 = [OpUInt8FromInt] diff --git a/src/Juvix/Compiler/Core/Language/Nodes.hs b/src/Juvix/Compiler/Core/Language/Nodes.hs index d12ff25658..c956a73a94 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 839d47b3ab..ea008e0a08 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 b0f102a844..3aac181709 100644 --- a/src/Juvix/Compiler/Core/Pretty/Base.hs +++ b/src/Juvix/Compiler/Core/Pretty/Base.hs @@ -62,6 +62,7 @@ instance PrettyCode BuiltinOp where OpPoseidonHash -> return primPoseidonHash OpEc -> return primEc OpRandomEcPoint -> return primRandomEcPoint + OpUInt8FromInt -> return primFieldFromInt instance PrettyCode BuiltinDataTag where ppCode = \case @@ -107,6 +108,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 +117,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 +737,9 @@ primFieldDiv = primitive Str.fdiv primFieldFromInt :: Doc Ann primFieldFromInt = primitive Str.itof +primUInt8FromInt :: Doc Ann +primUInt8FromInt = primitive Str.itou8 + primFieldToInt :: Doc Ann primFieldToInt = primitive Str.ftoi diff --git a/src/Juvix/Compiler/Core/Transformation/Check/Base.hs b/src/Juvix/Compiler/Core/Transformation/Check/Base.hs index 953a57a9be..26020a0893 100644 --- a/src/Juvix/Compiler/Core/Transformation/Check/Base.hs +++ b/src/Juvix/Compiler/Core/Transformation/Check/Base.hs @@ -53,6 +53,8 @@ checkBuiltins allowUntypedFail = dmapRM go NPrim TypePrim {..} | _typePrimPrimitive == PrimString -> throw $ unsupportedError "strings" node (getInfoLocation _typePrimInfo) + | _typePrimPrimitive == primitiveUInt8 -> + throw $ unsupportedError "uint8" node (getInfoLocation _typePrimInfo) NBlt BuiltinApp {..} -> case _builtinAppOp of OpTrace -> throw $ unsupportedError "tracing" node (getInfoLocation _builtinAppInfo) @@ -71,6 +73,8 @@ checkBuiltins allowUntypedFail = dmapRM go throw $ unsupportedError "cairo" node (getInfoLocation _builtinAppInfo) | _builtinAppOp `elem` builtinsAnoma -> throw $ unsupportedError "anoma" node (getInfoLocation _builtinAppInfo) + | _builtinAppOp `elem` builtinsUInt8 -> + throw $ unsupportedError "uint8" node (getInfoLocation _builtinAppInfo) | otherwise -> return $ Recur node _ -> return $ Recur node diff --git a/src/Juvix/Compiler/Core/Transformation/Check/Cairo.hs b/src/Juvix/Compiler/Core/Transformation/Check/Cairo.hs index 8279878046..daabb5b6a9 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 [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 272dc8e8a2..bb58693465 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,7 @@ computeNodeTypeInfo md = umapL go OpRandomEcPoint -> case _builtinAppArgs of [] -> mkDynamic' _ -> error "incorrect random_ec_point builtin application" + 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 8f496beb55..b124cc4d2f 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 BuiltinUInt8) -> 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 6042918124..41eac4d1e0 100644 --- a/src/Juvix/Compiler/Core/Translation/FromInternal.hs +++ b/src/Juvix/Compiler/Core/Translation/FromInternal.hs @@ -614,6 +614,8 @@ goAxiomInductive a = whenJust (a ^. Internal.axiomBuiltin) builtinInductive Internal.BuiltinPoseidon -> return () Internal.BuiltinEcOp -> return () Internal.BuiltinRandomEcPoint -> return () + Internal.BuiltinUInt8 -> registerInductiveAxiom (Just BuiltinUInt8) [] + Internal.BuiltinUInt8FromNat -> return () registerInductiveAxiom :: Maybe BuiltinAxiom -> [(Tag, Text, Type -> Type, Maybe BuiltinConstructor)] -> Sem r () registerInductiveAxiom ax ctrs = do @@ -815,6 +817,9 @@ goAxiomDef a = maybe goAxiomNotBuiltin builtinBody (a ^. Internal.axiomBuiltin) $ mkBuiltinApp' OpEc [mkVar' 2, mkVar' 1, mkVar' 0] Internal.BuiltinRandomEcPoint -> do registerAxiomDef (mkBuiltinApp' OpRandomEcPoint []) + Internal.BuiltinUInt8 -> return () + Internal.BuiltinUInt8FromNat -> + registerAxiomDef (mkLambda' mkTypeInteger' (mkBuiltinApp' OpUInt8FromInt [mkVar' 0])) axiomType' :: Sem r Type axiomType' = fromTopIndex (goType (a ^. Internal.axiomType)) @@ -1212,6 +1217,8 @@ goApplication a = do Just Internal.BuiltinPoseidon -> app Just Internal.BuiltinEcOp -> app Just Internal.BuiltinRandomEcPoint -> app + Just Internal.BuiltinUInt8 -> app + Just Internal.BuiltinUInt8FromNat -> 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 1bb09ffd4e..2592087272 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 7b8038fc2a..2983361adc 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 0afe527cf2..22e71e67f0 100644 --- a/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs +++ b/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs @@ -108,6 +108,8 @@ fromCore fsize tab = BuiltinPoseidon -> False BuiltinEcOp -> False BuiltinRandomEcPoint -> False + BuiltinUInt8 -> False + BuiltinUInt8FromNat -> 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 8a98ffc9a0..15f19ac030 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 `Natural` 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 a605dd60a1..b647042197 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs @@ -587,6 +587,8 @@ registerBuiltinAxiom d = \case BuiltinPoseidon -> registerPoseidon d BuiltinEcOp -> registerEcOp d BuiltinRandomEcPoint -> registerRandomEcPoint d + BuiltinUInt8 -> registerUInt8 d + BuiltinUInt8FromNat -> registerUInt8FromNat 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 d8431233b3..22c8758908 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,10 @@ compile = \case in sub (getF ClosureTotalArgsNum) (getF ClosureArgsNum) Tree.OpIntToField -> fieldErr Tree.OpFieldToInt -> fieldErr + Tree.OpIntToUInt8 -> callStdlib StdlibMod [arg, nockIntegralLiteral @Natural (2 ^ uint8Size)] + where + uint8Size :: Natural + uint8Size = 8 goAnomaGet :: [Term Natural] -> Sem r (Term Natural) goAnomaGet key = do diff --git a/src/Juvix/Compiler/Tree/Evaluator.hs b/src/Juvix/Compiler/Tree/Evaluator.hs index e598d192e5..c3c79b2ddf 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 e9ea9bd8bd..9c29231cd9 100644 --- a/src/Juvix/Compiler/Tree/Evaluator/Builtins.hs +++ b/src/Juvix/Compiler/Tree/Evaluator/Builtins.hs @@ -63,6 +63,7 @@ evalUnop tab op v = case op of OpFieldToInt -> goFieldToInt v OpIntToField -> goIntToField v OpArgsNum -> goArgsNum v + OpIntToUInt8 -> goIntToUInt8 v where strToInt :: Text -> Either ErrorMsg Value strToInt s = case T.readMaybe (fromText s) of @@ -100,6 +101,13 @@ 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" + printValue :: InfoTable' t e -> Value -> Text printValue tab = \case ValString s -> s @@ -113,6 +121,7 @@ constantToValue = \case ConstString s -> ValString s ConstUnit -> ValUnit ConstVoid -> ValVoid + ConstUInt8 i -> ValUInt8 i valueToConstant :: Value -> Constant valueToConstant = \case diff --git a/src/Juvix/Compiler/Tree/Extra/Type.hs b/src/Juvix/Compiler/Tree/Extra/Type.hs index 2425f0d2eb..1dfc32409a 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 f3711f8b13..99208bd703 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 7d99a39839..e2809b3517 100644 --- a/src/Juvix/Compiler/Tree/Language/Builtins.hs +++ b/src/Juvix/Compiler/Tree/Language/Builtins.hs @@ -47,6 +47,8 @@ data UnaryOp OpIntToField | -- | Convert a field element to an integer. JV* opcode: `ftoi`. OpFieldToInt + | -- | Convert an integer to a UInt8. JV* opcode: `itou8` + OpIntToUInt8 | -- | 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 601d6e3036..2e4387a6f0 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 aeae737a27..8f91d64857 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,7 @@ instance PrettyCode UnaryOp where OpFieldToInt -> Str.instrFieldToInt OpIntToField -> Str.instrIntToField OpArgsNum -> Str.instrArgsNum + OpIntToUInt8 -> Str.instrIntToUInt8 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 e05f67a00a..667bf43010 100644 --- a/src/Juvix/Compiler/Tree/Transformation/Validate.hs +++ b/src/Juvix/Compiler/Tree/Transformation/Validate.hs @@ -82,6 +82,7 @@ inferType tab funInfo = goInfer mempty OpArgsNum -> checkUnop TyDynamic mkTypeInteger OpIntToField -> checkUnop mkTypeInteger TyField OpFieldToInt -> checkUnop TyField mkTypeInteger + OpIntToUInt8 -> checkUnop mkTypeInteger mkTypeUInt8 goCairo :: BinderList Type -> NodeCairo -> Sem r Type goCairo bl NodeCairo {..} = do @@ -101,6 +102,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 422ce1ecc7..9081bc1c09 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,7 @@ genCode infoTable fi = Core.OpFieldToInt -> PrimUnop OpFieldToInt Core.OpTrace -> OpTrace Core.OpFail -> OpFail + Core.OpUInt8FromInt -> PrimUnop OpIntToUInt8 _ -> impossible genCairoOp :: Core.BuiltinOp -> CairoOp diff --git a/src/Juvix/Extra/Strings.hs b/src/Juvix/Extra/Strings.hs index fd13d8d8fc..185d7cb2c8 100644 --- a/src/Juvix/Extra/Strings.hs +++ b/src/Juvix/Extra/Strings.hs @@ -173,6 +173,12 @@ error = "error" string :: (IsString s) => s string = "string" +uint8 :: (IsString s) => s +uint8 = "uint8" + +uint8FromNat :: (IsString s) => s +uint8FromNat = "uint8-from-nat" + nat :: (IsString s) => s nat = "nat" @@ -389,6 +395,9 @@ ftoi = "ftoi" itof :: (IsString s) => s itof = "itof" +itou8 :: (IsString s) => s +itou8 = "itou8" + delimiter :: (IsString s) => s delimiter = "delimiter" @@ -770,6 +779,9 @@ instrFieldToInt = "ftoi" instrIntToField :: (IsString s) => s instrIntToField = "itof" +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 cffbf31ee1..8d4acd47d6 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 3843af88ba..dc8c25ec9d 100644 --- a/test/Anoma/Compilation/Positive.hs +++ b/test/Anoma/Compilation/Positive.hs @@ -594,5 +594,14 @@ allTests = [nock| 2 |], [nock| 3 |], [nock| nil |] + ], + mkAnomaCallTest + "Test081: UInt8" + $(mkRelDir ".") + $(mkRelFile "test081.juvix") + [] + $ checkOutput + [ [nock| 255 |], + [nock| 0 |] ] ] diff --git a/test/Compilation/Positive.hs b/test/Compilation/Positive.hs index 941bbbab93..e9f877fb90 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 UInt8" + $(mkRelDir ".") + $(mkRelFile "test078.juvix") + $(mkRelFile "out/test078.out") ] diff --git a/tests/Anoma/Compilation/positive/test081.juvix b/tests/Anoma/Compilation/positive/test081.juvix new file mode 100644 index 0000000000..47a6c850e2 --- /dev/null +++ b/tests/Anoma/Compilation/positive/test081.juvix @@ -0,0 +1,13 @@ +module test081; + +import Stdlib.Data.Nat open hiding {fromNat}; +import Stdlib.Debug.Trace open; +import Stdlib.Function open using {>->}; + +builtin uint8 +axiom UInt8 : Type; + +builtin uint8-from-nat +axiom fromNat : Nat -> UInt8; + +main : UInt8 := trace (fromNat 0xff) >-> fromNat 0x100; diff --git a/tests/Compilation/positive/out/test078.out b/tests/Compilation/positive/out/test078.out new file mode 100644 index 0000000000..d00491fd7e --- /dev/null +++ b/tests/Compilation/positive/out/test078.out @@ -0,0 +1 @@ +1 diff --git a/tests/Compilation/positive/test078.juvix b/tests/Compilation/positive/test078.juvix new file mode 100644 index 0000000000..8e06c576fc --- /dev/null +++ b/tests/Compilation/positive/test078.juvix @@ -0,0 +1,52 @@ +module test078; + +import Stdlib.Data.Nat open hiding {fromNat}; +import Stdlib.Debug.Trace open; +import Stdlib.Function open using {>->}; +import Stdlib.Data.List open; +import Stdlib.Trait.FromNatural open; + +builtin uint8 +axiom UInt8 : Type; + +builtin uint8-from-nat +axiom fromNat : Nat -> UInt8; + +builtin uint8-to-nat +axiom toNat : UInt8 -> Nat; + +instance +UInt8FromNaturalI : FromNatural UInt8 := + mkFromNatural@{ + fromNat + }; + +n1 : UInt8 := fromNat 1; + +n2 : UInt8 := fromNat 0xff; + +n3 : UInt8 := fromNat 0x101; + +l1 : UInt8 := 1; + +l2 : UInt8 := 0xee; + +l3 : UInt8 := 0x101; + +xs : List UInt8 := [l1; l2; l3; 2]; + +main : List UInt8 := + trace n1 + >-> trace n2 + >-> trace n3 + >-> trace l1 + >-> trace l2 + >-> trace l3 + >-> trace (toNat n1) + >-> trace (toNat n2) + >-> trace (toNat n3) + >-> trace (toNat l1) + >-> trace (toNat l2) + >-> trace (toNat l3) + >-> trace (toNat 0xf0) + >-> xs; diff --git a/tests/Core/positive/out/test063.out b/tests/Core/positive/out/test063.out new file mode 100644 index 0000000000..d00491fd7e --- /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 0000000000..246b87d2c7 --- /dev/null +++ b/tests/Core/positive/test063.jvc @@ -0,0 +1,5 @@ +-- UInt8 + +def f := \x x; + +f 257u8 From de9b0480b4dc81dbf4fc53e38e05f616354ef206 Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Mon, 29 Jul 2024 17:40:02 +0100 Subject: [PATCH 02/21] Add builtin uint8-to-nat and uint8-eq OpUint8ToInt --- src/Juvix/Compiler/Asm/Extra/Recursors.hs | 2 ++ .../Compiler/Backend/C/Translation/FromReg.hs | 1 + .../Backend/Rust/Translation/FromReg.hs | 1 + src/Juvix/Compiler/Builtins/UInt8.hs | 14 ++++++++++++++ src/Juvix/Compiler/Casm/Translation/FromReg.hs | 1 + src/Juvix/Compiler/Concrete/Data/Builtins.hs | 6 ++++++ src/Juvix/Compiler/Core/Evaluator.hs | 18 ++++++++++++++++++ src/Juvix/Compiler/Core/Extra/Utils.hs | 1 + src/Juvix/Compiler/Core/Language/Builtins.hs | 3 +++ src/Juvix/Compiler/Core/Pretty/Base.hs | 4 ++++ .../Core/Transformation/ComputeTypeInfo.hs | 1 + .../Compiler/Core/Translation/FromInternal.hs | 8 ++++++++ .../Core/Translation/Stripped/FromCore.hs | 2 ++ .../Internal/Translation/FromConcrete.hs | 2 ++ .../Compiler/Nockma/Translation/FromTree.hs | 12 ++++++++---- src/Juvix/Compiler/Tree/Evaluator/Builtins.hs | 9 +++++++++ src/Juvix/Compiler/Tree/Language/Builtins.hs | 2 ++ src/Juvix/Compiler/Tree/Pretty/Base.hs | 1 + .../Compiler/Tree/Transformation/Validate.hs | 1 + src/Juvix/Extra/Strings.hs | 12 ++++++++++++ 20 files changed, 97 insertions(+), 4 deletions(-) diff --git a/src/Juvix/Compiler/Asm/Extra/Recursors.hs b/src/Juvix/Compiler/Asm/Extra/Recursors.hs index 03732e1472..f51515a925 100644 --- a/src/Juvix/Compiler/Asm/Extra/Recursors.hs +++ b/src/Juvix/Compiler/Asm/Extra/Recursors.hs @@ -189,6 +189,8 @@ recurse' sig = go True checkUnop mkTypeInteger TyField OpFieldToInt -> checkUnop TyField mkTypeInteger + OpUInt8ToInt -> + checkUnop mkTypeUInt8 mkTypeInteger OpIntToUInt8 -> checkUnop mkTypeInteger mkTypeUInt8 where diff --git a/src/Juvix/Compiler/Backend/C/Translation/FromReg.hs b/src/Juvix/Compiler/Backend/C/Translation/FromReg.hs index 9e17358564..55bf011c1e 100644 --- a/src/Juvix/Compiler/Backend/C/Translation/FromReg.hs +++ b/src/Juvix/Compiler/Backend/C/Translation/FromReg.hs @@ -311,6 +311,7 @@ fromRegInstr bNoStack info = \case Reg.OpArgsNum -> "JUVIX_ARGS_NUM" Reg.OpFieldToInt -> unsupported "field type" Reg.OpIntToField -> unsupported "field type" + Reg.OpUInt8ToInt -> unsupported "uint8 type" Reg.OpIntToUInt8 -> unsupported "uint8 type" fromVarRef :: Reg.VarRef -> Expression diff --git a/src/Juvix/Compiler/Backend/Rust/Translation/FromReg.hs b/src/Juvix/Compiler/Backend/Rust/Translation/FromReg.hs index 0f49d67864..b4815ef67d 100644 --- a/src/Juvix/Compiler/Backend/Rust/Translation/FromReg.hs +++ b/src/Juvix/Compiler/Backend/Rust/Translation/FromReg.hs @@ -205,6 +205,7 @@ fromRegInstr info = \case (mkCall "mem.get_closure_largs" [fromValue _instrUnopArg]) Reg.OpFieldToInt -> unsupported "field type" Reg.OpIntToField -> unsupported "field type" + Reg.OpUInt8ToInt -> unsupported "uint8 type" Reg.OpIntToUInt8 -> unsupported "uint8 type" mkVarRef :: Reg.VarRef -> Text diff --git a/src/Juvix/Compiler/Builtins/UInt8.hs b/src/Juvix/Compiler/Builtins/UInt8.hs index b6de6a640c..8892e65f6f 100644 --- a/src/Juvix/Compiler/Builtins/UInt8.hs +++ b/src/Juvix/Compiler/Builtins/UInt8.hs @@ -9,6 +9,13 @@ registerUInt8 d = do unless (isSmallUniverse' (d ^. axiomType)) (error "UInt8 should be in the small universe") registerBuiltin BuiltinUInt8 (d ^. axiomName) +registerUInt8Eq :: (Member Builtins r) => AxiomDef -> Sem r () +registerUInt8Eq f = do + uint8 <- getBuiltinName (getLoc f) BuiltinUInt8 + bool_ <- getBuiltinName (getLoc f) BuiltinBool + unless (f ^. axiomType === (uint8 --> uint8 --> bool_)) (error "UInt8 equality has the wrong type signature") + registerBuiltin BuiltinUInt8Eq (f ^. axiomName) + registerUInt8FromNat :: (Member Builtins r) => AxiomDef -> Sem r () registerUInt8FromNat d = do let l = getLoc d @@ -16,3 +23,10 @@ registerUInt8FromNat d = do nat <- getBuiltinName l BuiltinNat unless (d ^. axiomType === (nat --> uint8)) (error "uint8-from-nat has the wrong type signature") registerBuiltin BuiltinUInt8FromNat (d ^. axiomName) + +registerUInt8ToNat :: (Member Builtins r) => AxiomDef -> Sem r () +registerUInt8ToNat f = do + uint8 <- getBuiltinName (getLoc f) BuiltinUInt8 + nat_ <- getBuiltinName (getLoc f) BuiltinNat + unless (f ^. axiomType === (uint8 --> nat_)) (error "uint8-to-nat conversion has the wrong type signature") + registerBuiltin BuiltinUInt8ToNat (f ^. axiomName) diff --git a/src/Juvix/Compiler/Casm/Translation/FromReg.hs b/src/Juvix/Compiler/Casm/Translation/FromReg.hs index 4a8ec5bb68..73b87649f7 100644 --- a/src/Juvix/Compiler/Casm/Translation/FromReg.hs +++ b/src/Juvix/Compiler/Casm/Translation/FromReg.hs @@ -460,6 +460,7 @@ fromReg tab = mkResult $ run $ runLabelInfoBuilderWithNextId (Reg.getNextSymbolI Reg.OpIntToField -> goAssignValue _instrUnopResult _instrUnopArg Reg.OpArgsNum -> goUnop' goOpArgsNum _instrUnopResult _instrUnopArg Reg.OpIntToUInt8 -> unsupported "uint8" + Reg.OpUInt8ToInt -> unsupported "uint8" 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 2ba915371b..606503c28f 100644 --- a/src/Juvix/Compiler/Concrete/Data/Builtins.hs +++ b/src/Juvix/Compiler/Concrete/Data/Builtins.hs @@ -219,6 +219,8 @@ data BuiltinAxiom | BuiltinEcOp | BuiltinRandomEcPoint | BuiltinUInt8 + | BuiltinUInt8Eq + | BuiltinUInt8ToNat | BuiltinUInt8FromNat deriving stock (Show, Eq, Ord, Enum, Bounded, Generic, Data) @@ -258,6 +260,8 @@ instance HasNameKind BuiltinAxiom where BuiltinEcOp -> KNameFunction BuiltinRandomEcPoint -> KNameFunction BuiltinUInt8 -> KNameInductive + BuiltinUInt8Eq -> KNameFunction + BuiltinUInt8ToNat -> KNameFunction BuiltinUInt8FromNat -> KNameFunction getNameKindPretty :: BuiltinAxiom -> NameKind @@ -305,6 +309,8 @@ instance Pretty BuiltinAxiom where BuiltinEcOp -> Str.cairoEcOp BuiltinRandomEcPoint -> Str.cairoRandomEcPoint BuiltinUInt8 -> Str.uint8 + BuiltinUInt8Eq -> Str.uint8Eq + BuiltinUInt8ToNat -> Str.uint8ToNat BuiltinUInt8FromNat -> Str.uint8FromNat data BuiltinType diff --git a/src/Juvix/Compiler/Core/Evaluator.hs b/src/Juvix/Compiler/Core/Evaluator.hs index 32a88e8252..163c102a4e 100644 --- a/src/Juvix/Compiler/Core/Evaluator.hs +++ b/src/Juvix/Compiler/Core/Evaluator.hs @@ -213,6 +213,7 @@ geval opts herr tab env0 = eval' env0 OpPoseidonHash -> poseidonHashOp OpEc -> ecOp OpRandomEcPoint -> randomEcPointOp + OpUInt8ToInt -> uint8ToIntOp OpUInt8FromInt -> uint8FromIntOp where err :: Text -> a @@ -521,6 +522,17 @@ geval opts herr tab env0 = eval' env0 . integerFromNode $ v {-# INLINE uint8FromIntOp #-} + + uint8ToIntOp :: [Node] -> Node + uint8ToIntOp = + unary $ \node -> + let !v = eval' env node + in nodeFromInteger + . toInteger + . fromMaybe (evalError "expected field element" v) + . uint8FromNode + $ v + {-# INLINE uint8ToIntOp #-} {-# INLINE applyBuiltin #-} -- secretKey, publicKey are not encoded with their length as @@ -593,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/Utils.hs b/src/Juvix/Compiler/Core/Extra/Utils.hs index f8f892c15c..5c4c573a05 100644 --- a/src/Juvix/Compiler/Core/Extra/Utils.hs +++ b/src/Juvix/Compiler/Core/Extra/Utils.hs @@ -433,6 +433,7 @@ builtinOpArgTypes = \case OpPoseidonHash -> [mkDynamic'] OpEc -> [mkDynamic', mkTypeField', mkDynamic'] OpRandomEcPoint -> [] + OpUInt8ToInt -> [mkTypeUInt8'] OpUInt8FromInt -> [mkTypeInteger'] translateCase :: (Node -> Node -> Node -> a) -> a -> Case -> a diff --git a/src/Juvix/Compiler/Core/Language/Builtins.hs b/src/Juvix/Compiler/Core/Language/Builtins.hs index 501ff33f90..6f1036b4c4 100644 --- a/src/Juvix/Compiler/Core/Language/Builtins.hs +++ b/src/Juvix/Compiler/Core/Language/Builtins.hs @@ -36,6 +36,7 @@ data BuiltinOp | OpPoseidonHash | OpEc | OpRandomEcPoint + | OpUInt8ToInt | OpUInt8FromInt deriving stock (Eq, Generic) @@ -91,6 +92,7 @@ builtinOpArgsNum = \case OpPoseidonHash -> 1 OpEc -> 3 OpRandomEcPoint -> 0 + OpUInt8ToInt -> 1 OpUInt8FromInt -> 1 builtinConstrArgsNum :: BuiltinDataTag -> Int @@ -135,6 +137,7 @@ builtinIsFoldable = \case OpPoseidonHash -> False OpEc -> False OpRandomEcPoint -> False + OpUInt8ToInt -> True OpUInt8FromInt -> True builtinIsCairo :: BuiltinOp -> Bool diff --git a/src/Juvix/Compiler/Core/Pretty/Base.hs b/src/Juvix/Compiler/Core/Pretty/Base.hs index 3aac181709..f90e309510 100644 --- a/src/Juvix/Compiler/Core/Pretty/Base.hs +++ b/src/Juvix/Compiler/Core/Pretty/Base.hs @@ -62,6 +62,7 @@ instance PrettyCode BuiltinOp where OpPoseidonHash -> return primPoseidonHash OpEc -> return primEc OpRandomEcPoint -> return primRandomEcPoint + OpUInt8ToInt -> return primUInt8ToInt OpUInt8FromInt -> return primFieldFromInt instance PrettyCode BuiltinDataTag where @@ -737,6 +738,9 @@ 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 diff --git a/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs b/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs index bb58693465..e79b027f47 100644 --- a/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs +++ b/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs @@ -83,6 +83,7 @@ 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 diff --git a/src/Juvix/Compiler/Core/Translation/FromInternal.hs b/src/Juvix/Compiler/Core/Translation/FromInternal.hs index 41eac4d1e0..86b2272427 100644 --- a/src/Juvix/Compiler/Core/Translation/FromInternal.hs +++ b/src/Juvix/Compiler/Core/Translation/FromInternal.hs @@ -615,6 +615,8 @@ goAxiomInductive a = whenJust (a ^. Internal.axiomBuiltin) builtinInductive Internal.BuiltinEcOp -> return () Internal.BuiltinRandomEcPoint -> return () Internal.BuiltinUInt8 -> registerInductiveAxiom (Just BuiltinUInt8) [] + Internal.BuiltinUInt8Eq -> return () + Internal.BuiltinUInt8ToNat -> return () Internal.BuiltinUInt8FromNat -> return () registerInductiveAxiom :: Maybe BuiltinAxiom -> [(Tag, Text, Type -> Type, Maybe BuiltinConstructor)] -> Sem r () @@ -818,6 +820,10 @@ goAxiomDef a = maybe goAxiomNotBuiltin builtinBody (a ^. Internal.axiomBuiltin) Internal.BuiltinRandomEcPoint -> do registerAxiomDef (mkBuiltinApp' OpRandomEcPoint []) Internal.BuiltinUInt8 -> return () + Internal.BuiltinUInt8Eq -> + registerAxiomDef (mkLambda' mkTypeUInt8' (mkLambda' mkTypeUInt8' (mkBuiltinApp' OpEq [mkVar' 1, mkVar' 0]))) + Internal.BuiltinUInt8ToNat -> + registerAxiomDef (mkLambda' mkTypeUInt8' (mkBuiltinApp' OpUInt8ToInt [mkVar' 0])) Internal.BuiltinUInt8FromNat -> registerAxiomDef (mkLambda' mkTypeInteger' (mkBuiltinApp' OpUInt8FromInt [mkVar' 0])) @@ -1218,6 +1224,8 @@ goApplication a = do Just Internal.BuiltinEcOp -> app Just Internal.BuiltinRandomEcPoint -> app Just Internal.BuiltinUInt8 -> app + Just Internal.BuiltinUInt8Eq -> app + Just Internal.BuiltinUInt8ToNat -> app Just Internal.BuiltinUInt8FromNat -> app Nothing -> app Internal.ExpressionIden (Internal.IdenFunction n) -> do diff --git a/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs b/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs index 22e71e67f0..3a147b2bac 100644 --- a/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs +++ b/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs @@ -109,6 +109,8 @@ fromCore fsize tab = BuiltinEcOp -> False BuiltinRandomEcPoint -> False BuiltinUInt8 -> False + BuiltinUInt8Eq -> False + BuiltinUInt8ToNat -> False BuiltinUInt8FromNat -> False BuiltinTypeInductive i -> case i of BuiltinList -> True diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs index b647042197..17d5238255 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs @@ -588,6 +588,8 @@ registerBuiltinAxiom d = \case BuiltinEcOp -> registerEcOp d BuiltinRandomEcPoint -> registerRandomEcPoint d BuiltinUInt8 -> registerUInt8 d + BuiltinUInt8Eq -> registerUInt8Eq d + BuiltinUInt8ToNat -> registerUInt8ToNat d BuiltinUInt8FromNat -> registerUInt8FromNat d goInductive :: diff --git a/src/Juvix/Compiler/Nockma/Translation/FromTree.hs b/src/Juvix/Compiler/Nockma/Translation/FromTree.hs index 22c8758908..e8c7d8639a 100644 --- a/src/Juvix/Compiler/Nockma/Translation/FromTree.hs +++ b/src/Juvix/Compiler/Nockma/Translation/FromTree.hs @@ -509,10 +509,8 @@ compile = \case in sub (getF ClosureTotalArgsNum) (getF ClosureArgsNum) Tree.OpIntToField -> fieldErr Tree.OpFieldToInt -> fieldErr - Tree.OpIntToUInt8 -> callStdlib StdlibMod [arg, nockIntegralLiteral @Natural (2 ^ uint8Size)] - where - uint8Size :: Natural - uint8Size = 8 + Tree.OpIntToUInt8 -> intToUInt8 arg + Tree.OpUInt8ToInt -> arg goAnomaGet :: [Term Natural] -> Sem r (Term Natural) goAnomaGet key = do @@ -1188,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/Builtins.hs b/src/Juvix/Compiler/Tree/Evaluator/Builtins.hs index 9c29231cd9..58b8e53772 100644 --- a/src/Juvix/Compiler/Tree/Evaluator/Builtins.hs +++ b/src/Juvix/Compiler/Tree/Evaluator/Builtins.hs @@ -63,6 +63,7 @@ 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 @@ -108,6 +109,13 @@ evalUnop tab op v = case op of _ -> 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 @@ -131,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/Language/Builtins.hs b/src/Juvix/Compiler/Tree/Language/Builtins.hs index e2809b3517..94b04cfa2a 100644 --- a/src/Juvix/Compiler/Tree/Language/Builtins.hs +++ b/src/Juvix/Compiler/Tree/Language/Builtins.hs @@ -49,6 +49,8 @@ data UnaryOp 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/Pretty/Base.hs b/src/Juvix/Compiler/Tree/Pretty/Base.hs index 8f91d64857..bf5e665d0e 100644 --- a/src/Juvix/Compiler/Tree/Pretty/Base.hs +++ b/src/Juvix/Compiler/Tree/Pretty/Base.hs @@ -244,6 +244,7 @@ instance PrettyCode UnaryOp where 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 667bf43010..2565c76982 100644 --- a/src/Juvix/Compiler/Tree/Transformation/Validate.hs +++ b/src/Juvix/Compiler/Tree/Transformation/Validate.hs @@ -82,6 +82,7 @@ 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 diff --git a/src/Juvix/Extra/Strings.hs b/src/Juvix/Extra/Strings.hs index 185d7cb2c8..1bf554da7a 100644 --- a/src/Juvix/Extra/Strings.hs +++ b/src/Juvix/Extra/Strings.hs @@ -176,6 +176,12 @@ string = "string" uint8 :: (IsString s) => s uint8 = "uint8" +uint8Eq :: (IsString s) => s +uint8Eq = "uint8-eq" + +uint8ToNat :: (IsString s) => s +uint8ToNat = "uint8-to-nat" + uint8FromNat :: (IsString s) => s uint8FromNat = "uint8-from-nat" @@ -395,6 +401,9 @@ ftoi = "ftoi" itof :: (IsString s) => s itof = "itof" +u8toi :: (IsString s) => s +u8toi = "u8toi" + itou8 :: (IsString s) => s itou8 = "itou8" @@ -779,6 +788,9 @@ instrFieldToInt = "ftoi" instrIntToField :: (IsString s) => s instrIntToField = "itof" +instrUInt8ToInt :: (IsString s) => s +instrUInt8ToInt = "u8toi" + instrIntToUInt8 :: (IsString s) => s instrIntToUInt8 = "itou8" From b23cb31c4dbef8bbaeb9df85d5a86ecf4459491d Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Wed, 31 Jul 2024 10:58:45 +0100 Subject: [PATCH 03/21] Update name of utf8FromNat --- tests/Compilation/positive/test078.juvix | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/Compilation/positive/test078.juvix b/tests/Compilation/positive/test078.juvix index 8e06c576fc..44c5e7d2bb 100644 --- a/tests/Compilation/positive/test078.juvix +++ b/tests/Compilation/positive/test078.juvix @@ -10,7 +10,7 @@ builtin uint8 axiom UInt8 : Type; builtin uint8-from-nat -axiom fromNat : Nat -> UInt8; +axiom uint8FromNat : Nat -> UInt8; builtin uint8-to-nat axiom toNat : UInt8 -> Nat; @@ -18,7 +18,7 @@ axiom toNat : UInt8 -> Nat; instance UInt8FromNaturalI : FromNatural UInt8 := mkFromNatural@{ - fromNat + fromNat := uint8FromNat }; n1 : UInt8 := fromNat 1; From 780a1ed4ed1bc8ad64146e8726bd3d8b611bfb51 Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Wed, 31 Jul 2024 16:32:43 +0100 Subject: [PATCH 04/21] Update UInt8 test --- tests/Compilation/positive/out/test078.out | 7 +++++ tests/Compilation/positive/test078.juvix | 36 +++++++++++----------- 2 files changed, 25 insertions(+), 18 deletions(-) diff --git a/tests/Compilation/positive/out/test078.out b/tests/Compilation/positive/out/test078.out index d00491fd7e..586cfa0b6d 100644 --- a/tests/Compilation/positive/out/test078.out +++ b/tests/Compilation/positive/out/test078.out @@ -1 +1,8 @@ 1 +255 +2 +1 +238 +3 +240 +(1 :: 238 :: 3 :: 2 :: nil) diff --git a/tests/Compilation/positive/test078.juvix b/tests/Compilation/positive/test078.juvix index 44c5e7d2bb..ce867ab511 100644 --- a/tests/Compilation/positive/test078.juvix +++ b/tests/Compilation/positive/test078.juvix @@ -2,9 +2,11 @@ module test078; import Stdlib.Data.Nat open hiding {fromNat}; import Stdlib.Debug.Trace open; -import Stdlib.Function open using {>->}; +import Stdlib.Function open using {>->; >>}; import Stdlib.Data.List open; import Stdlib.Trait.FromNatural open; +import Stdlib.Trait.Functor open; +import Stdlib.System.IO open; builtin uint8 axiom UInt8 : Type; @@ -25,28 +27,26 @@ n1 : UInt8 := fromNat 1; n2 : UInt8 := fromNat 0xff; -n3 : UInt8 := fromNat 0x101; +n3 : UInt8 := fromNat 0x102; l1 : UInt8 := 1; l2 : UInt8 := 0xee; -l3 : UInt8 := 0x101; +l3 : UInt8 := 0x103; xs : List UInt8 := [l1; l2; l3; 2]; -main : List UInt8 := - trace n1 - >-> trace n2 - >-> trace n3 - >-> trace l1 - >-> trace l2 - >-> trace l3 - >-> trace (toNat n1) - >-> trace (toNat n2) - >-> trace (toNat n3) - >-> trace (toNat l1) - >-> trace (toNat l2) - >-> trace (toNat l3) - >-> trace (toNat 0xf0) - >-> xs; +printUInt8Ln : UInt8 -> IO := toNat >> printNatLn; + +printListUInt8Ln : List UInt8 -> IO := map toNat >> Show.show >> printStringLn; + +main : IO := + printUInt8Ln n1 + >>> printUInt8Ln n2 + >>> printUInt8Ln n3 + >>> printNatLn (toNat l1) + >>> printNatLn (toNat l2) + >>> printNatLn (toNat l3) + >>> printNatLn (toNat 0xf0) + >>> printListUInt8Ln xs; From e6ca93f8f3f56c151a0ba88332b3818876d76bf6 Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Wed, 31 Jul 2024 16:46:09 +0100 Subject: [PATCH 05/21] Rename builtin UInt8 to Byte --- src/Juvix/Compiler/Builtins.hs | 4 +- src/Juvix/Compiler/Builtins/Byte.hs | 32 ++++++++++++++ src/Juvix/Compiler/Builtins/UInt8.hs | 32 -------------- src/Juvix/Compiler/Concrete/Data/Builtins.hs | 24 +++++------ .../Transformation/ConvertBuiltinTypes.hs | 2 +- .../Compiler/Core/Translation/FromInternal.hs | 24 +++++------ .../Core/Translation/Stripped/FromCore.hs | 8 ++-- .../Internal/Translation/FromConcrete.hs | 8 ++-- src/Juvix/Extra/Strings.hs | 16 +++---- test/Compilation/Positive.hs | 2 +- tests/Compilation/positive/test078.juvix | 42 +++++++++---------- 11 files changed, 97 insertions(+), 97 deletions(-) create mode 100644 src/Juvix/Compiler/Builtins/Byte.hs delete mode 100644 src/Juvix/Compiler/Builtins/UInt8.hs diff --git a/src/Juvix/Compiler/Builtins.hs b/src/Juvix/Compiler/Builtins.hs index c946ba9458..2648a6620f 100644 --- a/src/Juvix/Compiler/Builtins.hs +++ b/src/Juvix/Compiler/Builtins.hs @@ -12,12 +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.UInt8, + 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 @@ -29,4 +30,3 @@ import Juvix.Compiler.Builtins.List import Juvix.Compiler.Builtins.Maybe import Juvix.Compiler.Builtins.Nat import Juvix.Compiler.Builtins.String -import Juvix.Compiler.Builtins.UInt8 diff --git a/src/Juvix/Compiler/Builtins/Byte.hs b/src/Juvix/Compiler/Builtins/Byte.hs new file mode 100644 index 0000000000..51d9123702 --- /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 "UInt8 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 + bool_ <- getBuiltinName (getLoc f) BuiltinBool + unless (f ^. axiomType === (uint8 --> uint8 --> bool_)) (error "UInt8 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 + nat <- getBuiltinName l BuiltinNat + unless (d ^. axiomType === (nat --> uint8)) (error "uint8-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 + nat_ <- getBuiltinName (getLoc f) BuiltinNat + unless (f ^. axiomType === (uint8 --> nat_)) (error "uint8-to-nat conversion has the wrong type signature") + registerBuiltin BuiltinByteToNat (f ^. axiomName) diff --git a/src/Juvix/Compiler/Builtins/UInt8.hs b/src/Juvix/Compiler/Builtins/UInt8.hs deleted file mode 100644 index 8892e65f6f..0000000000 --- a/src/Juvix/Compiler/Builtins/UInt8.hs +++ /dev/null @@ -1,32 +0,0 @@ -module Juvix.Compiler.Builtins.UInt8 where - -import Juvix.Compiler.Builtins.Effect -import Juvix.Compiler.Internal.Extra -import Juvix.Prelude - -registerUInt8 :: (Member Builtins r) => AxiomDef -> Sem r () -registerUInt8 d = do - unless (isSmallUniverse' (d ^. axiomType)) (error "UInt8 should be in the small universe") - registerBuiltin BuiltinUInt8 (d ^. axiomName) - -registerUInt8Eq :: (Member Builtins r) => AxiomDef -> Sem r () -registerUInt8Eq f = do - uint8 <- getBuiltinName (getLoc f) BuiltinUInt8 - bool_ <- getBuiltinName (getLoc f) BuiltinBool - unless (f ^. axiomType === (uint8 --> uint8 --> bool_)) (error "UInt8 equality has the wrong type signature") - registerBuiltin BuiltinUInt8Eq (f ^. axiomName) - -registerUInt8FromNat :: (Member Builtins r) => AxiomDef -> Sem r () -registerUInt8FromNat d = do - let l = getLoc d - uint8 <- getBuiltinName l BuiltinUInt8 - nat <- getBuiltinName l BuiltinNat - unless (d ^. axiomType === (nat --> uint8)) (error "uint8-from-nat has the wrong type signature") - registerBuiltin BuiltinUInt8FromNat (d ^. axiomName) - -registerUInt8ToNat :: (Member Builtins r) => AxiomDef -> Sem r () -registerUInt8ToNat f = do - uint8 <- getBuiltinName (getLoc f) BuiltinUInt8 - nat_ <- getBuiltinName (getLoc f) BuiltinNat - unless (f ^. axiomType === (uint8 --> nat_)) (error "uint8-to-nat conversion has the wrong type signature") - registerBuiltin BuiltinUInt8ToNat (f ^. axiomName) diff --git a/src/Juvix/Compiler/Concrete/Data/Builtins.hs b/src/Juvix/Compiler/Concrete/Data/Builtins.hs index 606503c28f..6adf2536c3 100644 --- a/src/Juvix/Compiler/Concrete/Data/Builtins.hs +++ b/src/Juvix/Compiler/Concrete/Data/Builtins.hs @@ -218,10 +218,10 @@ data BuiltinAxiom | BuiltinPoseidon | BuiltinEcOp | BuiltinRandomEcPoint - | BuiltinUInt8 - | BuiltinUInt8Eq - | BuiltinUInt8ToNat - | BuiltinUInt8FromNat + | BuiltinByte + | BuiltinByteEq + | BuiltinByteToNat + | BuiltinByteFromNat deriving stock (Show, Eq, Ord, Enum, Bounded, Generic, Data) instance HasNameKind BuiltinAxiom where @@ -259,10 +259,10 @@ instance HasNameKind BuiltinAxiom where BuiltinPoseidon -> KNameFunction BuiltinEcOp -> KNameFunction BuiltinRandomEcPoint -> KNameFunction - BuiltinUInt8 -> KNameInductive - BuiltinUInt8Eq -> KNameFunction - BuiltinUInt8ToNat -> KNameFunction - BuiltinUInt8FromNat -> KNameFunction + BuiltinByte -> KNameInductive + BuiltinByteEq -> KNameFunction + BuiltinByteToNat -> KNameFunction + BuiltinByteFromNat -> KNameFunction getNameKindPretty :: BuiltinAxiom -> NameKind getNameKindPretty = getNameKind @@ -308,10 +308,10 @@ instance Pretty BuiltinAxiom where BuiltinPoseidon -> Str.cairoPoseidon BuiltinEcOp -> Str.cairoEcOp BuiltinRandomEcPoint -> Str.cairoRandomEcPoint - BuiltinUInt8 -> Str.uint8 - BuiltinUInt8Eq -> Str.uint8Eq - BuiltinUInt8ToNat -> Str.uint8ToNat - BuiltinUInt8FromNat -> Str.uint8FromNat + BuiltinByte -> Str.byte_ + BuiltinByteEq -> Str.byteEq + BuiltinByteToNat -> Str.byteToNat + BuiltinByteFromNat -> Str.byteFromNat data BuiltinType = BuiltinTypeInductive BuiltinInductive diff --git a/src/Juvix/Compiler/Core/Transformation/ConvertBuiltinTypes.hs b/src/Juvix/Compiler/Core/Transformation/ConvertBuiltinTypes.hs index b124cc4d2f..5746972dd2 100644 --- a/src/Juvix/Compiler/Core/Transformation/ConvertBuiltinTypes.hs +++ b/src/Juvix/Compiler/Core/Transformation/ConvertBuiltinTypes.hs @@ -19,7 +19,7 @@ convertNode md = umap go Just (BuiltinTypeInductive BuiltinInt) -> mkTypeInteger' Just (BuiltinTypeAxiom BuiltinString) -> mkTypeString' Just (BuiltinTypeAxiom BuiltinField) -> mkTypeField' - Just (BuiltinTypeAxiom BuiltinUInt8) -> mkTypeUInt8' + 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 86b2272427..6551eb4b7d 100644 --- a/src/Juvix/Compiler/Core/Translation/FromInternal.hs +++ b/src/Juvix/Compiler/Core/Translation/FromInternal.hs @@ -614,10 +614,10 @@ goAxiomInductive a = whenJust (a ^. Internal.axiomBuiltin) builtinInductive Internal.BuiltinPoseidon -> return () Internal.BuiltinEcOp -> return () Internal.BuiltinRandomEcPoint -> return () - Internal.BuiltinUInt8 -> registerInductiveAxiom (Just BuiltinUInt8) [] - Internal.BuiltinUInt8Eq -> return () - Internal.BuiltinUInt8ToNat -> return () - Internal.BuiltinUInt8FromNat -> 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 @@ -819,12 +819,12 @@ goAxiomDef a = maybe goAxiomNotBuiltin builtinBody (a ^. Internal.axiomBuiltin) $ mkBuiltinApp' OpEc [mkVar' 2, mkVar' 1, mkVar' 0] Internal.BuiltinRandomEcPoint -> do registerAxiomDef (mkBuiltinApp' OpRandomEcPoint []) - Internal.BuiltinUInt8 -> return () - Internal.BuiltinUInt8Eq -> + Internal.BuiltinByte -> return () + Internal.BuiltinByteEq -> registerAxiomDef (mkLambda' mkTypeUInt8' (mkLambda' mkTypeUInt8' (mkBuiltinApp' OpEq [mkVar' 1, mkVar' 0]))) - Internal.BuiltinUInt8ToNat -> + Internal.BuiltinByteToNat -> registerAxiomDef (mkLambda' mkTypeUInt8' (mkBuiltinApp' OpUInt8ToInt [mkVar' 0])) - Internal.BuiltinUInt8FromNat -> + Internal.BuiltinByteFromNat -> registerAxiomDef (mkLambda' mkTypeInteger' (mkBuiltinApp' OpUInt8FromInt [mkVar' 0])) axiomType' :: Sem r Type @@ -1223,10 +1223,10 @@ goApplication a = do Just Internal.BuiltinPoseidon -> app Just Internal.BuiltinEcOp -> app Just Internal.BuiltinRandomEcPoint -> app - Just Internal.BuiltinUInt8 -> app - Just Internal.BuiltinUInt8Eq -> app - Just Internal.BuiltinUInt8ToNat -> app - Just Internal.BuiltinUInt8FromNat -> 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/Stripped/FromCore.hs b/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs index 3a147b2bac..34c051b24e 100644 --- a/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs +++ b/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs @@ -108,10 +108,10 @@ fromCore fsize tab = BuiltinPoseidon -> False BuiltinEcOp -> False BuiltinRandomEcPoint -> False - BuiltinUInt8 -> False - BuiltinUInt8Eq -> False - BuiltinUInt8ToNat -> False - BuiltinUInt8FromNat -> 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/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs index 17d5238255..677ec97b02 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs @@ -587,10 +587,10 @@ registerBuiltinAxiom d = \case BuiltinPoseidon -> registerPoseidon d BuiltinEcOp -> registerEcOp d BuiltinRandomEcPoint -> registerRandomEcPoint d - BuiltinUInt8 -> registerUInt8 d - BuiltinUInt8Eq -> registerUInt8Eq d - BuiltinUInt8ToNat -> registerUInt8ToNat d - BuiltinUInt8FromNat -> registerUInt8FromNat 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/Extra/Strings.hs b/src/Juvix/Extra/Strings.hs index 1bf554da7a..df249563a9 100644 --- a/src/Juvix/Extra/Strings.hs +++ b/src/Juvix/Extra/Strings.hs @@ -173,17 +173,17 @@ error = "error" string :: (IsString s) => s string = "string" -uint8 :: (IsString s) => s -uint8 = "uint8" +byte_ :: (IsString s) => s +byte_ = "byte" -uint8Eq :: (IsString s) => s -uint8Eq = "uint8-eq" +byteEq :: (IsString s) => s +byteEq = "byte-eq" -uint8ToNat :: (IsString s) => s -uint8ToNat = "uint8-to-nat" +byteToNat :: (IsString s) => s +byteToNat = "byte-to-nat" -uint8FromNat :: (IsString s) => s -uint8FromNat = "uint8-from-nat" +byteFromNat :: (IsString s) => s +byteFromNat = "byte-from-nat" nat :: (IsString s) => s nat = "nat" diff --git a/test/Compilation/Positive.hs b/test/Compilation/Positive.hs index e9f877fb90..3a65505b66 100644 --- a/test/Compilation/Positive.hs +++ b/test/Compilation/Positive.hs @@ -462,7 +462,7 @@ tests = $(mkRelFile "test077.juvix") $(mkRelFile "out/test077.out"), posTestEval - "Test078: Builtin UInt8" + "Test078: Builtin Byte" $(mkRelDir ".") $(mkRelFile "test078.juvix") $(mkRelFile "out/test078.out") diff --git a/tests/Compilation/positive/test078.juvix b/tests/Compilation/positive/test078.juvix index ce867ab511..81ab048a57 100644 --- a/tests/Compilation/positive/test078.juvix +++ b/tests/Compilation/positive/test078.juvix @@ -8,45 +8,45 @@ import Stdlib.Trait.FromNatural open; import Stdlib.Trait.Functor open; import Stdlib.System.IO open; -builtin uint8 -axiom UInt8 : Type; +builtin byte +axiom Byte : Type; -builtin uint8-from-nat -axiom uint8FromNat : Nat -> UInt8; +builtin byte-from-nat +axiom byteFromNat : Nat -> Byte; -builtin uint8-to-nat -axiom toNat : UInt8 -> Nat; +builtin byte-to-nat +axiom toNat : Byte -> Nat; instance -UInt8FromNaturalI : FromNatural UInt8 := +ByteFromNaturalI : FromNatural Byte := mkFromNatural@{ - fromNat := uint8FromNat + fromNat := byteFromNat }; -n1 : UInt8 := fromNat 1; +n1 : Byte := fromNat 1; -n2 : UInt8 := fromNat 0xff; +n2 : Byte := fromNat 0xff; -n3 : UInt8 := fromNat 0x102; +n3 : Byte := fromNat 0x102; -l1 : UInt8 := 1; +l1 : Byte := 1; -l2 : UInt8 := 0xee; +l2 : Byte := 0xee; -l3 : UInt8 := 0x103; +l3 : Byte := 0x103; -xs : List UInt8 := [l1; l2; l3; 2]; +xs : List Byte := [l1; l2; l3; 2]; -printUInt8Ln : UInt8 -> IO := toNat >> printNatLn; +printByteLn : Byte -> IO := toNat >> printNatLn; -printListUInt8Ln : List UInt8 -> IO := map toNat >> Show.show >> printStringLn; +printListByteLn : List Byte -> IO := map toNat >> Show.show >> printStringLn; main : IO := - printUInt8Ln n1 - >>> printUInt8Ln n2 - >>> printUInt8Ln n3 + printByteLn n1 + >>> printByteLn n2 + >>> printByteLn n3 >>> printNatLn (toNat l1) >>> printNatLn (toNat l2) >>> printNatLn (toNat l3) >>> printNatLn (toNat 0xf0) - >>> printListUInt8Ln xs; + >>> printListByteLn xs; From 68963c4d339fecdcb39c20d741a1b7f171913b98 Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Wed, 31 Jul 2024 18:17:35 +0100 Subject: [PATCH 06/21] Compile UInt8 to smallint in C backend --- runtime/c/src/juvix/api.h | 3 +++ src/Juvix/Compiler/Backend/C/Translation/FromReg.hs | 6 +++--- src/Juvix/Compiler/Tree/Translation/FromCore.hs | 1 + 3 files changed, 7 insertions(+), 3 deletions(-) diff --git a/runtime/c/src/juvix/api.h b/runtime/c/src/juvix/api.h index 5002188e89..158971db7e 100644 --- a/runtime/c/src/juvix/api.h +++ b/runtime/c/src/juvix/api.h @@ -100,6 +100,9 @@ #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/src/Juvix/Compiler/Backend/C/Translation/FromReg.hs b/src/Juvix/Compiler/Backend/C/Translation/FromReg.hs index 55bf011c1e..d312c80762 100644 --- a/src/Juvix/Compiler/Backend/C/Translation/FromReg.hs +++ b/src/Juvix/Compiler/Backend/C/Translation/FromReg.hs @@ -311,8 +311,8 @@ fromRegInstr bNoStack info = \case Reg.OpArgsNum -> "JUVIX_ARGS_NUM" Reg.OpFieldToInt -> unsupported "field type" Reg.OpIntToField -> unsupported "field type" - Reg.OpUInt8ToInt -> unsupported "uint8 type" - Reg.OpIntToUInt8 -> unsupported "uint8 type" + Reg.OpUInt8ToInt -> "JUVIX_UINT8_TO_INT" + Reg.OpIntToUInt8 -> "JUVIX_INT_TO_UINT8" fromVarRef :: Reg.VarRef -> Expression fromVarRef Reg.VarRef {..} = @@ -349,7 +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 {} -> impossible + Reg.ConstUInt8 x -> macroCall "make_smallint" [integer x] fromPrealloc :: Reg.InstrPrealloc -> Statement fromPrealloc Reg.InstrPrealloc {..} = diff --git a/src/Juvix/Compiler/Tree/Translation/FromCore.hs b/src/Juvix/Compiler/Tree/Translation/FromCore.hs index 9081bc1c09..587b4241df 100644 --- a/src/Juvix/Compiler/Tree/Translation/FromCore.hs +++ b/src/Juvix/Compiler/Tree/Translation/FromCore.hs @@ -305,6 +305,7 @@ genCode infoTable fi = Core.OpTrace -> OpTrace Core.OpFail -> OpFail Core.OpUInt8FromInt -> PrimUnop OpIntToUInt8 + Core.OpUInt8ToInt -> PrimUnop OpUInt8ToInt _ -> impossible genCairoOp :: Core.BuiltinOp -> CairoOp From 832108381dc019d806504e46672b3b3c19e6a2b0 Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Wed, 31 Jul 2024 18:44:25 +0100 Subject: [PATCH 07/21] Compile UInt8 to smallint in Rust backend --- runtime/rust/juvix/src/defs.rs | 8 ++++++++ runtime/rust/juvix/src/integer.rs | 17 +++++++++++++++++ .../Backend/Rust/Translation/FromReg.hs | 12 +++++++++--- 3 files changed, 34 insertions(+), 3 deletions(-) diff --git a/runtime/rust/juvix/src/defs.rs b/runtime/rust/juvix/src/defs.rs index ca1d475c63..f4d08547f1 100644 --- a/runtime/rust/juvix/src/defs.rs +++ b/runtime/rust/juvix/src/defs.rs @@ -36,3 +36,11 @@ pub fn word_to_bool(x: Word) -> bool { true } } + +pub fn uint8_to_int(x : Word) -> Word { + x +} + +pub fn int_to_uint8(x : Word) -> Word { + x +} diff --git a/runtime/rust/juvix/src/integer.rs b/runtime/rust/juvix/src/integer.rs index 41282da4db..d947adcd7e 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) & 0xFF) as i32) +} + #[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/Backend/Rust/Translation/FromReg.hs b/src/Juvix/Compiler/Backend/Rust/Translation/FromReg.hs index b4815ef67d..274ab200dd 100644 --- a/src/Juvix/Compiler/Backend/Rust/Translation/FromReg.hs +++ b/src/Juvix/Compiler/Backend/Rust/Translation/FromReg.hs @@ -205,8 +205,14 @@ fromRegInstr info = \case (mkCall "mem.get_closure_largs" [fromValue _instrUnopArg]) Reg.OpFieldToInt -> unsupported "field type" Reg.OpIntToField -> unsupported "field type" - Reg.OpUInt8ToInt -> unsupported "uint8 type" - Reg.OpIntToUInt8 -> unsupported "uint8 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 @@ -244,7 +250,7 @@ fromRegInstr info = \case Reg.ConstString {} -> unsupported "strings" Reg.ConstUnit -> mkVar "OBJ_UNIT" Reg.ConstVoid -> mkVar "OBJ_VOID" - Reg.ConstUInt8 {} -> impossible + Reg.ConstUInt8 x -> mkCall "make_smallint" [mkInteger x] fromAlloc :: Reg.InstrAlloc -> [Statement] fromAlloc Reg.InstrAlloc {..} = From 6b408fb399d4d35e0fe88448470a559a4370786c Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Wed, 31 Jul 2024 18:59:26 +0100 Subject: [PATCH 08/21] Represent a UInt8 as an integer in Casm --- src/Juvix/Compiler/Casm/Translation/FromReg.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Juvix/Compiler/Casm/Translation/FromReg.hs b/src/Juvix/Compiler/Casm/Translation/FromReg.hs index 73b87649f7..aaec1fc6ac 100644 --- a/src/Juvix/Compiler/Casm/Translation/FromReg.hs +++ b/src/Juvix/Compiler/Casm/Translation/FromReg.hs @@ -249,7 +249,7 @@ fromReg tab = mkResult $ run $ runLabelInfoBuilderWithNextId (Reg.getNextSymbolI Reg.ConstUnit -> 0 Reg.ConstVoid -> 0 Reg.ConstString {} -> unsupported "strings" - Reg.ConstUInt8 {} -> unsupported "uint8" + Reg.ConstUInt8 x -> toInteger x mkLoad :: Reg.ConstrField -> Sem r RValue mkLoad Reg.ConstrField {..} = do From aa4e0777c87dcb49fa5be28612922f151762f18d Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Wed, 31 Jul 2024 19:00:28 +0100 Subject: [PATCH 09/21] Define converions UInt8 <-> Int in CASM --- src/Juvix/Compiler/Casm/Translation/FromReg.hs | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/Juvix/Compiler/Casm/Translation/FromReg.hs b/src/Juvix/Compiler/Casm/Translation/FromReg.hs index aaec1fc6ac..fef090244b 100644 --- a/src/Juvix/Compiler/Casm/Translation/FromReg.hs +++ b/src/Juvix/Compiler/Casm/Translation/FromReg.hs @@ -459,8 +459,11 @@ fromReg tab = mkResult $ run $ runLabelInfoBuilderWithNextId (Reg.getNextSymbolI Reg.OpFieldToInt -> goAssignValue _instrUnopResult _instrUnopArg Reg.OpIntToField -> goAssignValue _instrUnopResult _instrUnopArg Reg.OpArgsNum -> goUnop' goOpArgsNum _instrUnopResult _instrUnopArg - Reg.OpIntToUInt8 -> unsupported "uint8" - Reg.OpUInt8ToInt -> unsupported "uint8" + Reg.OpUInt8ToInt -> goAssignValue _instrUnopResult _instrUnopArg + Reg.OpIntToUInt8 -> goUnop' mod256 _instrUnopResult _instrUnopArg + where + mod256 :: Reg.VarRef -> MemRef -> Sem r () + mod256 res arg1 = goExtraBinop IntMod res arg1 (Imm 256) goCairo :: Reg.InstrCairo -> Sem r () goCairo Reg.InstrCairo {..} = case _instrCairoOpcode of From 7591605c25293a5b31d0895fad23c868c78c16b1 Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Wed, 31 Jul 2024 19:02:21 +0100 Subject: [PATCH 10/21] Fix Anoma Byte test --- tests/Anoma/Compilation/positive/test081.juvix | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/tests/Anoma/Compilation/positive/test081.juvix b/tests/Anoma/Compilation/positive/test081.juvix index 47a6c850e2..cb5f437ab6 100644 --- a/tests/Anoma/Compilation/positive/test081.juvix +++ b/tests/Anoma/Compilation/positive/test081.juvix @@ -4,10 +4,10 @@ import Stdlib.Data.Nat open hiding {fromNat}; import Stdlib.Debug.Trace open; import Stdlib.Function open using {>->}; -builtin uint8 -axiom UInt8 : Type; +builtin byte +axiom Byte : Type; -builtin uint8-from-nat -axiom fromNat : Nat -> UInt8; +builtin byte-from-nat +axiom fromNat : Nat -> Byte; -main : UInt8 := trace (fromNat 0xff) >-> fromNat 0x100; +main : Byte := trace (fromNat 0xff) >-> fromNat 0x100; From 79e27fbecf7fd0839910c2c37f1decce226b45b4 Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Wed, 31 Jul 2024 20:26:52 +0100 Subject: [PATCH 11/21] clang-format --- runtime/c/src/juvix/api.h | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/runtime/c/src/juvix/api.h b/runtime/c/src/juvix/api.h index 158971db7e..07fa995336 100644 --- a/runtime/c/src/juvix/api.h +++ b/runtime/c/src/juvix/api.h @@ -101,7 +101,8 @@ #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_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()) From 4906d3a0784df73cd1e7fc87607998a468eeb999 Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Thu, 1 Aug 2024 09:02:06 +0100 Subject: [PATCH 12/21] Use rem_euclid to compute the modulus for int_to_uint8 --- runtime/rust/juvix/src/integer.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/runtime/rust/juvix/src/integer.rs b/runtime/rust/juvix/src/integer.rs index d947adcd7e..61aeecd8b0 100644 --- a/runtime/rust/juvix/src/integer.rs +++ b/runtime/rust/juvix/src/integer.rs @@ -44,7 +44,7 @@ pub fn uint8_to_int(x : Word) -> Word { } pub fn int_to_uint8(x : Word) -> Word { - make_smallint((smallint_value(x) & 0xFF) as i32) + make_smallint(smallint_value(x).rem_euclid(256)) } #[cfg(test)] From 45ea281cda0ba780e9ce1e2f400af503b9d60cdb Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Thu, 1 Aug 2024 09:22:41 +0100 Subject: [PATCH 13/21] Remove support for OpIntToUInt8 in Cairo The IntMod op is not availble in the Cairo VM --- src/Juvix/Compiler/Casm/Translation/FromReg.hs | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/src/Juvix/Compiler/Casm/Translation/FromReg.hs b/src/Juvix/Compiler/Casm/Translation/FromReg.hs index fef090244b..51caa02a7c 100644 --- a/src/Juvix/Compiler/Casm/Translation/FromReg.hs +++ b/src/Juvix/Compiler/Casm/Translation/FromReg.hs @@ -460,10 +460,7 @@ fromReg tab = mkResult $ run $ runLabelInfoBuilderWithNextId (Reg.getNextSymbolI Reg.OpIntToField -> goAssignValue _instrUnopResult _instrUnopArg Reg.OpArgsNum -> goUnop' goOpArgsNum _instrUnopResult _instrUnopArg Reg.OpUInt8ToInt -> goAssignValue _instrUnopResult _instrUnopArg - Reg.OpIntToUInt8 -> goUnop' mod256 _instrUnopResult _instrUnopArg - where - mod256 :: Reg.VarRef -> MemRef -> Sem r () - mod256 res arg1 = goExtraBinop IntMod res arg1 (Imm 256) + Reg.OpIntToUInt8 -> unsupported "OpIntTOUInt8" goCairo :: Reg.InstrCairo -> Sem r () goCairo Reg.InstrCairo {..} = case _instrCairoOpcode of From e6dbb4bb099abfb0773d2b2e931163283b8f12ef Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Thu, 1 Aug 2024 11:38:53 +0100 Subject: [PATCH 14/21] Update native and anoma bytes test to use stdlib --- juvix-stdlib | 2 +- test/Anoma/Compilation/Positive.hs | 13 ++++++- .../Anoma/Compilation/positive/test081.juvix | 36 ++++++++++++++---- tests/Compilation/positive/out/test078.out | 3 ++ tests/Compilation/positive/test078.juvix | 38 +++++-------------- 5 files changed, 54 insertions(+), 38 deletions(-) diff --git a/juvix-stdlib b/juvix-stdlib index 297601a98d..d8eea7a203 160000 --- a/juvix-stdlib +++ b/juvix-stdlib @@ -1 +1 @@ -Subproject commit 297601a98dcace657aaff6e42945f1430647885b +Subproject commit d8eea7a2038f93fa2f2100434742cd9773300b43 diff --git a/test/Anoma/Compilation/Positive.hs b/test/Anoma/Compilation/Positive.hs index dc8c25ec9d..fea8d489cf 100644 --- a/test/Anoma/Compilation/Positive.hs +++ b/test/Anoma/Compilation/Positive.hs @@ -601,7 +601,16 @@ allTests = $(mkRelFile "test081.juvix") [] $ checkOutput - [ [nock| 255 |], - [nock| 0 |] + [ [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/tests/Anoma/Compilation/positive/test081.juvix b/tests/Anoma/Compilation/positive/test081.juvix index cb5f437ab6..a34823b9b3 100644 --- a/tests/Anoma/Compilation/positive/test081.juvix +++ b/tests/Anoma/Compilation/positive/test081.juvix @@ -1,13 +1,35 @@ module test081; -import Stdlib.Data.Nat open hiding {fromNat}; +import Stdlib.Prelude open; import Stdlib.Debug.Trace open; -import Stdlib.Function open using {>->}; -builtin byte -axiom Byte : Type; +n1 : Byte := fromNat 1; -builtin byte-from-nat -axiom fromNat : Nat -> Byte; +n2 : Byte := fromNat 0xff; -main : Byte := trace (fromNat 0xff) >-> fromNat 0x100; +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 index 586cfa0b6d..6224a0c855 100644 --- a/tests/Compilation/positive/out/test078.out +++ b/tests/Compilation/positive/out/test078.out @@ -1,6 +1,9 @@ 1 255 2 +true +true +false 1 238 3 diff --git a/tests/Compilation/positive/test078.juvix b/tests/Compilation/positive/test078.juvix index 81ab048a57..898160edb7 100644 --- a/tests/Compilation/positive/test078.juvix +++ b/tests/Compilation/positive/test078.juvix @@ -1,27 +1,6 @@ module test078; -import Stdlib.Data.Nat open hiding {fromNat}; -import Stdlib.Debug.Trace open; -import Stdlib.Function open using {>->; >>}; -import Stdlib.Data.List open; -import Stdlib.Trait.FromNatural open; -import Stdlib.Trait.Functor open; -import Stdlib.System.IO open; - -builtin byte -axiom Byte : Type; - -builtin byte-from-nat -axiom byteFromNat : Nat -> Byte; - -builtin byte-to-nat -axiom toNat : Byte -> Nat; - -instance -ByteFromNaturalI : FromNatural Byte := - mkFromNatural@{ - fromNat := byteFromNat - }; +import Stdlib.Prelude open; n1 : Byte := fromNat 1; @@ -37,16 +16,19 @@ l3 : Byte := 0x103; xs : List Byte := [l1; l2; l3; 2]; -printByteLn : Byte -> IO := toNat >> printNatLn; +printByteLn : Byte -> IO := Show.show >> printStringLn; -printListByteLn : List Byte -> IO := map toNat >> Show.show >> printStringLn; +printListByteLn : List Byte -> IO := Show.show >> printStringLn; main : IO := printByteLn n1 >>> printByteLn n2 >>> printByteLn n3 - >>> printNatLn (toNat l1) - >>> printNatLn (toNat l2) - >>> printNatLn (toNat l3) - >>> printNatLn (toNat 0xf0) + >>> 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; From f37b4016080118563aaef08f33c596d94339c20c Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Thu, 1 Aug 2024 12:28:36 +0100 Subject: [PATCH 15/21] Allow UInt8 ops in base core check --- src/Juvix/Compiler/Core/Language/Builtins.hs | 2 +- src/Juvix/Compiler/Core/Transformation/Check/Base.hs | 4 ---- 2 files changed, 1 insertion(+), 5 deletions(-) diff --git a/src/Juvix/Compiler/Core/Language/Builtins.hs b/src/Juvix/Compiler/Core/Language/Builtins.hs index 6f1036b4c4..c63684c1cd 100644 --- a/src/Juvix/Compiler/Core/Language/Builtins.hs +++ b/src/Juvix/Compiler/Core/Language/Builtins.hs @@ -164,4 +164,4 @@ builtinsAnoma = ] builtinsUInt8 :: [BuiltinOp] -builtinsUInt8 = [OpUInt8FromInt] +builtinsUInt8 = [OpUInt8FromInt, OpUInt8ToInt] diff --git a/src/Juvix/Compiler/Core/Transformation/Check/Base.hs b/src/Juvix/Compiler/Core/Transformation/Check/Base.hs index 26020a0893..953a57a9be 100644 --- a/src/Juvix/Compiler/Core/Transformation/Check/Base.hs +++ b/src/Juvix/Compiler/Core/Transformation/Check/Base.hs @@ -53,8 +53,6 @@ checkBuiltins allowUntypedFail = dmapRM go NPrim TypePrim {..} | _typePrimPrimitive == PrimString -> throw $ unsupportedError "strings" node (getInfoLocation _typePrimInfo) - | _typePrimPrimitive == primitiveUInt8 -> - throw $ unsupportedError "uint8" node (getInfoLocation _typePrimInfo) NBlt BuiltinApp {..} -> case _builtinAppOp of OpTrace -> throw $ unsupportedError "tracing" node (getInfoLocation _builtinAppInfo) @@ -73,8 +71,6 @@ checkBuiltins allowUntypedFail = dmapRM go throw $ unsupportedError "cairo" node (getInfoLocation _builtinAppInfo) | _builtinAppOp `elem` builtinsAnoma -> throw $ unsupportedError "anoma" node (getInfoLocation _builtinAppInfo) - | _builtinAppOp `elem` builtinsUInt8 -> - throw $ unsupportedError "uint8" node (getInfoLocation _builtinAppInfo) | otherwise -> return $ Recur node _ -> return $ Recur node From 979ad5997af44ee5bfb95bf2a682ff3f6de922bf Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Thu, 1 Aug 2024 12:29:04 +0100 Subject: [PATCH 16/21] Do not allow uint8 ops in CASM as it's not possible to support OpIntToUIn8 currently --- src/Juvix/Compiler/Casm/Translation/FromReg.hs | 6 +++--- src/Juvix/Compiler/Core/Transformation/Check/Cairo.hs | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Juvix/Compiler/Casm/Translation/FromReg.hs b/src/Juvix/Compiler/Casm/Translation/FromReg.hs index 51caa02a7c..1cac6232ed 100644 --- a/src/Juvix/Compiler/Casm/Translation/FromReg.hs +++ b/src/Juvix/Compiler/Casm/Translation/FromReg.hs @@ -249,7 +249,7 @@ fromReg tab = mkResult $ run $ runLabelInfoBuilderWithNextId (Reg.getNextSymbolI Reg.ConstUnit -> 0 Reg.ConstVoid -> 0 Reg.ConstString {} -> unsupported "strings" - Reg.ConstUInt8 x -> toInteger x + Reg.ConstUInt8 {} -> unsupported "uint8" mkLoad :: Reg.ConstrField -> Sem r RValue mkLoad Reg.ConstrField {..} = do @@ -459,8 +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 -> goAssignValue _instrUnopResult _instrUnopArg - Reg.OpIntToUInt8 -> unsupported "OpIntTOUInt8" + 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/Core/Transformation/Check/Cairo.hs b/src/Juvix/Compiler/Core/Transformation/Check/Cairo.hs index daabb5b6a9..8b7b3fb7e9 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, primitiveUInt8]) md + mapAllNodesM (checkBuiltins' (builtinsString ++ builtinsUInt8) [PrimString, primitiveUInt8]) md where checkMainType :: Sem r () checkMainType = From fbdb1e4b77329ad5364df2510e9507339db504c7 Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Thu, 1 Aug 2024 13:38:44 +0100 Subject: [PATCH 17/21] Add builtin byte test for Rust backend --- test/Rust/Compilation/Positive.hs | 7 ++++++- tests/Rust/Compilation/positive/out/test074.out | 2 +- tests/Rust/Compilation/positive/test074.juvix | 7 +++++++ 3 files changed, 14 insertions(+), 2 deletions(-) create mode 100644 tests/Rust/Compilation/positive/test074.juvix diff --git a/test/Rust/Compilation/Positive.hs b/test/Rust/Compilation/Positive.hs index 05d4e38fa7..c8ff0bc99d 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/Rust/Compilation/positive/out/test074.out b/tests/Rust/Compilation/positive/out/test074.out index eb3e83f932..0cfbf08886 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 0000000000..7ac631c51d --- /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); From 1850062a5c5e20fd8f71155a68d535f4a2299a27 Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Thu, 1 Aug 2024 16:03:54 +0100 Subject: [PATCH 18/21] Remove unused functions from rust runtime --- runtime/rust/juvix/src/defs.rs | 8 -------- 1 file changed, 8 deletions(-) diff --git a/runtime/rust/juvix/src/defs.rs b/runtime/rust/juvix/src/defs.rs index f4d08547f1..ca1d475c63 100644 --- a/runtime/rust/juvix/src/defs.rs +++ b/runtime/rust/juvix/src/defs.rs @@ -36,11 +36,3 @@ pub fn word_to_bool(x: Word) -> bool { true } } - -pub fn uint8_to_int(x : Word) -> Word { - x -} - -pub fn int_to_uint8(x : Word) -> Word { - x -} From 04b0df971c11de6d4db2960f9bbd2f3b11f1d9b6 Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Thu, 1 Aug 2024 18:39:17 +0100 Subject: [PATCH 19/21] Rename uint8 to byte in builtin registration errors --- src/Juvix/Compiler/Builtins/Byte.hs | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/Juvix/Compiler/Builtins/Byte.hs b/src/Juvix/Compiler/Builtins/Byte.hs index 51d9123702..477398509e 100644 --- a/src/Juvix/Compiler/Builtins/Byte.hs +++ b/src/Juvix/Compiler/Builtins/Byte.hs @@ -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) From c6e1439c076c2cac1f6a79ad517a36f1ed3bc05d Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Thu, 1 Aug 2024 19:33:30 +0100 Subject: [PATCH 20/21] Fix evaluator error message --- src/Juvix/Compiler/Core/Evaluator.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Juvix/Compiler/Core/Evaluator.hs b/src/Juvix/Compiler/Core/Evaluator.hs index 163c102a4e..b30f90b581 100644 --- a/src/Juvix/Compiler/Core/Evaluator.hs +++ b/src/Juvix/Compiler/Core/Evaluator.hs @@ -529,7 +529,7 @@ geval opts herr tab env0 = eval' env0 let !v = eval' env node in nodeFromInteger . toInteger - . fromMaybe (evalError "expected field element" v) + . fromMaybe (evalError "expected uint8" v) . uint8FromNode $ v {-# INLINE uint8ToIntOp #-} From c91f3095bf89081ba30efe2d7c03e23a27fa4386 Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Thu, 1 Aug 2024 19:47:57 +0100 Subject: [PATCH 21/21] Fix comment to refer to FromNatural, i.e the trait with `fromNat` --- src/Juvix/Compiler/Internal/Language.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Juvix/Compiler/Internal/Language.hs b/src/Juvix/Compiler/Internal/Language.hs index 15f19ac030..44da1c09d0 100644 --- a/src/Juvix/Compiler/Internal/Language.hs +++ b/src/Juvix/Compiler/Internal/Language.hs @@ -172,7 +172,7 @@ data Literal LitNumeric Integer | -- | `LitInteger` represents a literal with trait `Integral` LitInteger Integer - | -- | `LitNatural` represents a literal with trait `Natural` + | -- | `LitNatural` represents a literal with trait `FromNatural` LitNatural Integer deriving stock (Show, Eq, Ord, Generic, Data)