diff --git a/app/Commands/Dev/Core/Eval.hs b/app/Commands/Dev/Core/Eval.hs index 247dec4c2..72d454ee9 100644 --- a/app/Commands/Dev/Core/Eval.hs +++ b/app/Commands/Dev/Core/Eval.hs @@ -9,9 +9,10 @@ runCommand :: forall r. (Members '[EmbedIO, App] r) => CoreEvalOptions -> Sem r runCommand opts = do f :: Path Abs File <- fromAppPathFile b s <- readFile f + gopts <- askGlobalOptions case Core.runParser f defaultModuleId mempty s of Left err -> exitJuvixError (JuvixError err) - Right (tab, Just node) -> do evalAndPrint opts tab node + Right (tab, Just node) -> do evalAndPrint gopts opts tab node Right (_, Nothing) -> return () where b :: AppPath File diff --git a/app/Commands/Dev/Core/FromConcrete.hs b/app/Commands/Dev/Core/FromConcrete.hs index 3885ce255..e4761ee45 100644 --- a/app/Commands/Dev/Core/FromConcrete.hs +++ b/app/Commands/Dev/Core/FromConcrete.hs @@ -51,14 +51,14 @@ runCommand localOpts = do newline goEval :: Sem r () - goEval = evalAndPrint localOpts tab' evalNode + goEval = evalAndPrint gopts localOpts tab' evalNode where evalNode :: Core.Node | isJust (localOpts ^. coreFromConcreteSymbolName) = getNode' selInfo | otherwise = getNode' mainInfo goNormalize :: Sem r () - goNormalize = normalizeAndPrint localOpts tab' evalNode + goNormalize = normalizeAndPrint gopts localOpts tab' evalNode where evalNode :: Core.Node | isJust (localOpts ^. coreFromConcreteSymbolName) = getNode' selInfo diff --git a/app/Commands/Dev/Core/Normalize.hs b/app/Commands/Dev/Core/Normalize.hs index 4970cf28c..7fbf51d59 100644 --- a/app/Commands/Dev/Core/Normalize.hs +++ b/app/Commands/Dev/Core/Normalize.hs @@ -9,9 +9,10 @@ runCommand :: forall r. (Members '[EmbedIO, App] r) => CoreNormalizeOptions -> S runCommand opts = do f :: Path Abs File <- fromAppPathFile b s <- readFile f + gopts <- askGlobalOptions case Core.runParser f defaultModuleId mempty s of Left err -> exitJuvixError (JuvixError err) - Right (tab, Just node) -> do normalizeAndPrint opts tab node + Right (tab, Just node) -> do normalizeAndPrint gopts opts tab node Right (_, Nothing) -> return () where b :: AppPath File diff --git a/app/Commands/Dev/Core/Read.hs b/app/Commands/Dev/Core/Read.hs index 9d03e2542..6dc57fa34 100644 --- a/app/Commands/Dev/Core/Read.hs +++ b/app/Commands/Dev/Core/Read.hs @@ -30,21 +30,21 @@ runCommand opts = do embed (Scoper.scopeTrace tab') unless (project opts ^. coreReadNoPrint) $ do renderStdOut (Pretty.ppOut opts tab') - whenJust (tab' ^. Core.infoMain) $ \sym -> doEval tab' (fromJust $ tab' ^. Core.identContext . at sym) + whenJust (tab' ^. Core.infoMain) $ \sym -> doEval gopts tab' (fromJust $ tab' ^. Core.identContext . at sym) where - doEval :: Core.InfoTable -> Core.Node -> Sem r () - doEval tab' node = + doEval :: GlobalOptions -> Core.InfoTable -> Core.Node -> Sem r () + doEval gopts tab' node = if | project opts ^. coreReadEval -> do putStrLn "--------------------------------" putStrLn "| Eval |" putStrLn "--------------------------------" - Eval.evalAndPrint opts tab' node + Eval.evalAndPrint gopts opts tab' node | project opts ^. coreReadNormalize -> do putStrLn "--------------------------------" putStrLn "| Normalize |" putStrLn "--------------------------------" - Eval.normalizeAndPrint opts tab' node + Eval.normalizeAndPrint gopts opts tab' node | otherwise -> return () sinputFile :: AppPath File sinputFile = project opts ^. coreReadInputFile diff --git a/app/Commands/Dev/Core/Repl.hs b/app/Commands/Dev/Core/Repl.hs index 7752ee08b..bcfea5de0 100644 --- a/app/Commands/Dev/Core/Repl.hs +++ b/app/Commands/Dev/Core/Repl.hs @@ -14,6 +14,7 @@ import Juvix.Compiler.Core.Pretty qualified as Core import Juvix.Compiler.Core.Transformation.ComputeTypeInfo qualified as Core import Juvix.Compiler.Core.Transformation.DisambiguateNames qualified as Core import Juvix.Compiler.Core.Translation.FromSource qualified as Core +import Juvix.Data.Field import Juvix.Extra.Paths runCommand :: forall r. (Members '[EmbedIO, App] r) => CoreReplOptions -> Sem r () @@ -98,7 +99,7 @@ runRepl opts tab = do where replEval :: Bool -> Core.InfoTable -> Core.Node -> Sem r () replEval noIO tab' node = do - r <- Core.doEval noIO defaultLoc tab' node + r <- Core.doEval Nothing noIO defaultLoc tab' node case r of Left err -> do printJuvixError (JuvixError err) @@ -115,7 +116,7 @@ runRepl opts tab = do replNormalize :: Core.InfoTable -> Core.Node -> Sem r () replNormalize tab' node = let md' = Core.moduleFromInfoTable tab' - node' = normalize md' node + node' = normalize (maximum allowedFieldSizes) md' node in if | Info.member Info.kNoDisplayInfo (Core.getInfo node') -> runRepl opts tab' diff --git a/app/Commands/Dev/Core/Strip.hs b/app/Commands/Dev/Core/Strip.hs index 92b5c0d6a..aa64969e0 100644 --- a/app/Commands/Dev/Core/Strip.hs +++ b/app/Commands/Dev/Core/Strip.hs @@ -16,7 +16,7 @@ runCommand opts = do run $ runReader (project gopts) $ runError @JuvixError (Core.toStripped' Core.Identity (Core.moduleFromInfoTable tab) :: Sem '[Error JuvixError, Reader Core.CoreOptions] Core.Module) - tab' <- getRight $ mapLeft JuvixError $ mapRight (Stripped.fromCore . Core.computeCombinedInfoTable) r + tab' <- getRight $ mapLeft JuvixError $ mapRight (Stripped.fromCore (project gopts ^. Core.optFieldSize) . Core.computeCombinedInfoTable) r unless (project opts ^. coreStripNoPrint) $ do renderStdOut (Core.ppOut opts tab') where diff --git a/app/Commands/Eval.hs b/app/Commands/Eval.hs index 9b763b782..b037d2093 100644 --- a/app/Commands/Eval.hs +++ b/app/Commands/Eval.hs @@ -22,7 +22,7 @@ runCommand opts@EvalOptions {..} = do | otherwise -> getNode tab (mainInfo tab) case mevalNode of Just evalNode -> - Eval.evalAndPrint opts tab evalNode + Eval.evalAndPrint gopts opts tab evalNode Nothing -> do let name = fromMaybe Str.main _evalSymbolName printFailureExit ("function not found: " <> name) diff --git a/app/Commands/Repl.hs b/app/Commands/Repl.hs index f02a52730..0e8e14278 100644 --- a/app/Commands/Repl.hs +++ b/app/Commands/Repl.hs @@ -171,6 +171,7 @@ replCommand opts input_ = catchAll $ do eval :: Core.Node -> Repl Core.Node eval n = do + gopts <- State.gets (^. replStateGlobalOptions) ep <- getReplEntryPointFromPrepath (mkPrepath (toFilePath P.replPath)) let shouldDisambiguate :: Bool shouldDisambiguate = not (opts ^. replNoDisambiguate) @@ -182,12 +183,12 @@ replCommand opts input_ = catchAll $ do . runState artif . runTransformations shouldDisambiguate (opts ^. replTransformations) $ n - liftIO (doEvalIO' artif' n') >>= replFromEither + liftIO (doEvalIO' (project gopts ^. Core.optFieldSize) artif' n') >>= replFromEither - doEvalIO' :: Artifacts -> Core.Node -> IO (Either JuvixError Core.Node) - doEvalIO' artif' n = + doEvalIO' :: Natural -> Artifacts -> Core.Node -> IO (Either JuvixError Core.Node) + doEvalIO' fsize artif' n = mapLeft (JuvixError @Core.CoreError) - <$> Core.doEvalIO False replDefaultLoc (Core.computeCombinedInfoTable $ artif' ^. artifactCoreModule) n + <$> Core.doEvalIO (Just fsize) False replDefaultLoc (Core.computeCombinedInfoTable $ artif' ^. artifactCoreModule) n compileString :: Repl (Maybe Core.Node) compileString = do diff --git a/app/CommonOptions.hs b/app/CommonOptions.hs index 327d50568..46e5f244e 100644 --- a/app/CommonOptions.hs +++ b/app/CommonOptions.hs @@ -11,6 +11,7 @@ import Data.List.NonEmpty qualified as NonEmpty import Juvix.Compiler.Core.Data.TransformationId.Parser qualified as Core import Juvix.Compiler.Reg.Data.TransformationId.Parser qualified as Reg import Juvix.Compiler.Tree.Data.TransformationId.Parser qualified as Tree +import Juvix.Data.Field import Juvix.Data.FileExt import Juvix.Prelude import Options.Applicative @@ -111,6 +112,23 @@ naturalNumberOpt = eitherReader aux aux :: String -> Either String Word aux s = maybe (Left $ s <> " is not a nonnegative number") Right (readMaybe s :: Maybe Word) +fieldSizeOpt :: ReadM (Maybe Natural) +fieldSizeOpt = eitherReader aux + where + aux :: String -> Either String (Maybe Natural) + aux s = case s of + "cairo" -> Right $ Just cairoFieldSize + "small" -> Right $ Just smallFieldSize + _ -> + mapRight Just $ + either Left checkAllowed $ + maybe (Left $ s <> " is not a valid field size") Right (readMaybe s :: Maybe Natural) + + checkAllowed :: Natural -> Either String Natural + checkAllowed n + | n `elem` allowedFieldSizes = Right n + | otherwise = Left $ Prelude.show n <> " is not a recognized field size" + extCompleter :: FileExt -> Completer extCompleter ext = mkCompleter $ \word -> do let cmd = unwords ["compgen", "-o", "plusdirs", "-f", "-X", "!*" <> Prelude.show ext, "--", requote word] diff --git a/app/Evaluator.hs b/app/Evaluator.hs index 5b21cfd5d..31131a2da 100644 --- a/app/Evaluator.hs +++ b/app/Evaluator.hs @@ -20,15 +20,16 @@ data EvalOptions = EvalOptions makeLenses ''EvalOptions evalAndPrint :: - forall r a. - (Members '[EmbedIO, App] r, CanonicalProjection a EvalOptions, CanonicalProjection a Core.Options) => + forall r a b. + (Members '[EmbedIO, App] r, CanonicalProjection a EvalOptions, CanonicalProjection b Core.CoreOptions, CanonicalProjection a Core.Options) => + b -> a -> Core.InfoTable -> Core.Node -> Sem r () -evalAndPrint opts tab node = do +evalAndPrint gopts opts tab node = do loc <- defaultLoc - r <- Core.doEval (project opts ^. evalNoIO) loc tab node + r <- Core.doEval (Just $ project gopts ^. Core.optFieldSize) (project opts ^. evalNoIO) loc tab node case r of Left err -> exitJuvixError (JuvixError err) Right node' @@ -50,14 +51,15 @@ evalAndPrint opts tab node = do f = project opts ^. evalInputFile normalizeAndPrint :: - forall r a. - (Members '[EmbedIO, App] r, CanonicalProjection a EvalOptions, CanonicalProjection a Core.Options) => + forall r a b. + (Members '[EmbedIO, App] r, CanonicalProjection a EvalOptions, CanonicalProjection b Core.CoreOptions, CanonicalProjection a Core.Options) => + b -> a -> Core.InfoTable -> Core.Node -> Sem r () -normalizeAndPrint opts tab node = - let node' = normalize (Core.moduleFromInfoTable tab) node +normalizeAndPrint gopts opts tab node = + let node' = normalize (project gopts ^. Core.optFieldSize) (Core.moduleFromInfoTable tab) node in if | Info.member Info.kNoDisplayInfo (Core.getInfo node') -> return () diff --git a/app/GlobalOptions.hs b/app/GlobalOptions.hs index 30771bee4..0e1230a98 100644 --- a/app/GlobalOptions.hs +++ b/app/GlobalOptions.hs @@ -11,6 +11,7 @@ import Juvix.Compiler.Pipeline import Juvix.Compiler.Pipeline.Root import Juvix.Data.Effect.TaggedLock import Juvix.Data.Error.GenericError qualified as E +import Juvix.Data.Field data GlobalOptions = GlobalOptions { _globalNoColors :: Bool, @@ -23,6 +24,7 @@ data GlobalOptions = GlobalOptions _globalNoCoverage :: Bool, _globalNoStdlib :: Bool, _globalUnrollLimit :: Int, + _globalFieldSize :: Maybe Natural, _globalOffline :: Bool } deriving stock (Eq, Show) @@ -46,6 +48,7 @@ instance CanonicalProjection GlobalOptions Core.CoreOptions where Core.CoreOptions { Core._optCheckCoverage = not _globalNoCoverage, Core._optUnrollLimit = _globalUnrollLimit, + Core._optFieldSize = fromMaybe defaultFieldSize _globalFieldSize, Core._optOptimizationLevel = defaultOptimizationLevel, Core._optInliningDepth = defaultInliningDepth } @@ -63,6 +66,7 @@ defaultGlobalOptions = _globalNoCoverage = False, _globalNoStdlib = False, _globalUnrollLimit = defaultUnrollLimit, + _globalFieldSize = Nothing, _globalOffline = False } @@ -112,6 +116,13 @@ parseGlobalFlags = do ( long "no-stdlib" <> help "Do not use the standard library" ) + _globalFieldSize <- + option + fieldSizeOpt + ( long "field-size" + <> value Nothing + <> help "Field type size [cairo,small,11] (default: small)" + ) _globalUnrollLimit <- option (fromIntegral <$> naturalNumberOpt) @@ -162,7 +173,8 @@ entryPointFromGlobalOptions root mainFile opts = do _entryPointUnrollLimit = opts ^. globalUnrollLimit, _entryPointGenericOptions = project opts, _entryPointBuildDir = maybe (def ^. entryPointBuildDir) (CustomBuildDir . Abs) mabsBuildDir, - _entryPointOffline = opts ^. globalOffline + _entryPointOffline = opts ^. globalOffline, + _entryPointFieldSize = fromMaybe defaultFieldSize $ opts ^. globalFieldSize } where optBuildDir :: Maybe (Prepath Dir) @@ -184,7 +196,8 @@ entryPointFromGlobalOptionsNoFile root opts = do _entryPointUnrollLimit = opts ^. globalUnrollLimit, _entryPointGenericOptions = project opts, _entryPointBuildDir = maybe (def ^. entryPointBuildDir) (CustomBuildDir . Abs) mabsBuildDir, - _entryPointOffline = opts ^. globalOffline + _entryPointOffline = opts ^. globalOffline, + _entryPointFieldSize = fromMaybe defaultFieldSize $ opts ^. globalFieldSize } where optBuildDir :: Maybe (Prepath Dir) diff --git a/examples/milestone/Bank/Bank.juvix b/examples/milestone/Bank/Bank.juvix index a6af6a0c7..e7b26d9ae 100644 --- a/examples/milestone/Bank/Bank.juvix +++ b/examples/milestone/Bank/Bank.juvix @@ -12,12 +12,6 @@ Address : Type := Nat; bankAddress : Address := 1234; ---- Some field type. -axiom Field : Type; - ---- Equality test for ;Field;. -axiom eqField : Field -> Field -> Bool; - module Token; type Token := --- Arguments are: owner, gates, amount. @@ -47,7 +41,7 @@ module Balances; | f n nil := (f, n) :: nil | f n ((b, bn) :: bs) := if - (eqField f b) + (f == b) ((b, bn + n) :: bs) ((b, bn) :: increment f n bs); @@ -58,7 +52,7 @@ module Balances; | _ _ nil := nil | f n ((b, bn) :: bs) := if - (eqField f b) + (f == b) ((b, sub bn n) :: bs) ((b, bn) :: decrement f n bs); diff --git a/include/package-base/Juvix/Builtin/V1/Nat.juvix b/include/package-base/Juvix/Builtin/V1/Nat.juvix index 954177413..f243bbe06 100644 --- a/include/package-base/Juvix/Builtin/V1/Nat.juvix +++ b/include/package-base/Juvix/Builtin/V1/Nat.juvix @@ -10,7 +10,5 @@ naturalNatI : Natural Nat := mkNatural@{ + := (Nat.+); * := (Nat.*); - div := Nat.div; - mod := Nat.mod; fromNat (x : Nat) : Nat := x }; diff --git a/include/package-base/Juvix/Builtin/V1/Trait/Natural.juvix b/include/package-base/Juvix/Builtin/V1/Trait/Natural.juvix index 5b7233552..97693a9c4 100644 --- a/include/package-base/Juvix/Builtin/V1/Trait/Natural.juvix +++ b/include/package-base/Juvix/Builtin/V1/Trait/Natural.juvix @@ -10,8 +10,6 @@ type Natural A := + : A -> A -> A; syntax operator * multiplicative; * : A -> A -> A; - div : A -> A -> A; - mod : A -> A -> A; builtin from-nat fromNat : Nat -> A }; diff --git a/juvix-stdlib b/juvix-stdlib index 183d4e932..6eb7ac818 160000 --- a/juvix-stdlib +++ b/juvix-stdlib @@ -1 +1 @@ -Subproject commit 183d4e9329a648b339ebecf2122b3e9621c99ee8 +Subproject commit 6eb7ac818f8f2e4e28c208fa8ec32ba7411cab04 diff --git a/runtime/src/vampir/stdlib.pir b/runtime/src/vampir/stdlib.pir index 246ae2de1..31f2237d5 100644 --- a/runtime/src/vampir/stdlib.pir +++ b/runtime/src/vampir/stdlib.pir @@ -63,6 +63,19 @@ def mul (x, e1) (y, e2) = { (x * y, e1 * e2 * range_check (x * y)) }; +def fadd (x, e1) (y, e2) = { + (x + y, e1 * e2) +}; +def fsub (x, e1) (y, e2) = { + (x - y, e1 * e2) +}; +def fmul (x, e1) (y, e2) = { + (x * y, e1 * e2) +}; +def fdiv (x, e1) (y, e2) = { + (x / y, e1 * e2) +}; + def equal (x, e1) (y, e2) = (isZero (x - y), e1 * e2); def if (b, e) (x, e1) (y, e2) = (b * x + (1 - b) * y, e * (b * e1 + (1 - b) * e2)); diff --git a/runtime/src/vampir/stdlib_unsafe.pir b/runtime/src/vampir/stdlib_unsafe.pir index f27cf0079..0855d2a73 100644 --- a/runtime/src/vampir/stdlib_unsafe.pir +++ b/runtime/src/vampir/stdlib_unsafe.pir @@ -41,6 +41,11 @@ def add x y = x + y; def sub x y = x - y; def mul x y = x * y; +def fadd x y = x + y; +def fsub x y = x - y; +def fmul x y = x * y; +def fdiv x y = x / y; + def equal x y = isZero (x - y); def if b x y = b * x + (1 - b) * y; diff --git a/src/Juvix/Compiler/Asm/Extra/Memory.hs b/src/Juvix/Compiler/Asm/Extra/Memory.hs index 96aab847d..17e98ddc9 100644 --- a/src/Juvix/Compiler/Asm/Extra/Memory.hs +++ b/src/Juvix/Compiler/Asm/Extra/Memory.hs @@ -104,6 +104,7 @@ getDirectRefType dr mem = case dr of getConstantType :: Constant -> Type getConstantType = \case ConstInt {} -> mkTypeInteger + ConstField {} -> TyField ConstBool {} -> mkTypeBool ConstString {} -> TyString ConstUnit -> TyUnit diff --git a/src/Juvix/Compiler/Asm/Extra/Recursors.hs b/src/Juvix/Compiler/Asm/Extra/Recursors.hs index 42ab09b31..0151dd492 100644 --- a/src/Juvix/Compiler/Asm/Extra/Recursors.hs +++ b/src/Juvix/Compiler/Asm/Extra/Recursors.hs @@ -131,14 +131,17 @@ recurse' sig = go True Return -> return (dropTempStack mem) - fixMemIntOp :: Memory -> Sem r Memory - fixMemIntOp mem = fixMemBinOp' mem mkTypeInteger mkTypeInteger mkTypeInteger - fixMemBinOp' :: Memory -> Type -> Type -> Type -> Sem r Memory fixMemBinOp' mem ty0 ty1 rty = do checkValueStack' loc (sig ^. recursorInfoTable) [ty0, ty1] mem return $ pushValueStack rty (popValueStack 2 mem) + fixMemIntOp :: Memory -> Sem r Memory + fixMemIntOp mem = fixMemBinOp' mem mkTypeInteger mkTypeInteger mkTypeInteger + + fixMemFieldOp :: Memory -> Sem r Memory + fixMemFieldOp mem = fixMemBinOp' mem TyField TyField TyField + fixMemBinop :: Memory -> BinaryOp -> Sem r Memory fixMemBinop mem op = case op of OpIntAdd -> @@ -155,6 +158,14 @@ recurse' sig = go True fixMemBinOp' mem mkTypeInteger mkTypeInteger mkTypeBool OpIntLe -> fixMemBinOp' mem mkTypeInteger mkTypeInteger mkTypeBool + OpFieldAdd -> + fixMemFieldOp mem + OpFieldSub -> + fixMemFieldOp mem + OpFieldMul -> + fixMemFieldOp mem + OpFieldDiv -> + fixMemFieldOp mem OpEq -> fixMemBinOp' mem TyDynamic TyDynamic mkTypeBool OpStrConcat -> @@ -164,15 +175,23 @@ recurse' sig = go True fixMemUnop mem op = case op of OpShow -> return (pushValueStack TyString (popValueStack 1 mem)) - OpStrToInt -> do - checkValueStack' loc (sig ^. recursorInfoTable) [TyString] mem - return (pushValueStack mkTypeInteger (popValueStack 1 mem)) + OpStrToInt -> + checkUnop TyString mkTypeInteger OpArgsNum -> do when (null (mem ^. memoryValueStack)) $ throw $ AsmError loc "empty value stack" checkFunType (topValueStack' 0 mem) return $ pushValueStack mkTypeInteger (popValueStack 1 mem) + OpIntToField -> + checkUnop mkTypeInteger TyField + OpFieldToInt -> + checkUnop TyField mkTypeInteger + where + checkUnop :: Type -> Type -> Sem r Memory + checkUnop ty1 ty2 = do + checkValueStack' loc (sig ^. recursorInfoTable) [ty1] mem + return (pushValueStack ty2 (popValueStack 1 mem)) fixMemExtendClosure :: Memory -> InstrExtendClosure -> Sem r Memory fixMemExtendClosure mem InstrExtendClosure {..} = do diff --git a/src/Juvix/Compiler/Asm/Interpreter.hs b/src/Juvix/Compiler/Asm/Interpreter.hs index 623aa1697..bd08890e8 100644 --- a/src/Juvix/Compiler/Asm/Interpreter.hs +++ b/src/Juvix/Compiler/Asm/Interpreter.hs @@ -159,6 +159,7 @@ runCodeR infoTable funInfo = goCode (funInfo ^. functionCode) >> popLastValueSta getConstantVal :: Constant -> Val getConstantVal = \case ConstInt i -> ValInteger i + ConstField f -> ValField f ConstBool b -> ValBool b ConstString s -> ValString s ConstUnit -> ValUnit diff --git a/src/Juvix/Compiler/Asm/Translation/FromSource.hs b/src/Juvix/Compiler/Asm/Translation/FromSource.hs index 222d10b2f..e513fa308 100644 --- a/src/Juvix/Compiler/Asm/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Asm/Translation/FromSource.hs @@ -73,6 +73,14 @@ command = do return $ mkBinop' loc OpIntLe "eq" -> return $ mkBinop' loc OpEq + "fadd" -> + return $ mkBinop' loc OpFieldAdd + "fsub" -> + return $ mkBinop' loc OpFieldSub + "fmul" -> + return $ mkBinop' loc OpFieldMul + "fdiv" -> + return $ mkBinop' loc OpFieldDiv "strcat" -> return $ mkBinop' loc OpStrConcat "show" -> diff --git a/src/Juvix/Compiler/Asm/Translation/FromTree.hs b/src/Juvix/Compiler/Asm/Translation/FromTree.hs index cb9e89514..55734b18b 100644 --- a/src/Juvix/Compiler/Asm/Translation/FromTree.hs +++ b/src/Juvix/Compiler/Asm/Translation/FromTree.hs @@ -16,7 +16,8 @@ fromTree tab = { _infoMainFunction = tab ^. Tree.infoMainFunction, _infoFunctions = genCode <$> tab ^. Tree.infoFunctions, _infoInductives = tab ^. Tree.infoInductives, - _infoConstrs = tab ^. Tree.infoConstrs + _infoConstrs = tab ^. Tree.infoConstrs, + _infoFieldSize = tab ^. Tree.infoFieldSize } -- Generate code for a single function. diff --git a/src/Juvix/Compiler/Backend/C/Translation/FromReg.hs b/src/Juvix/Compiler/Backend/C/Translation/FromReg.hs index 99f316842..d0d25fbeb 100644 --- a/src/Juvix/Compiler/Backend/C/Translation/FromReg.hs +++ b/src/Juvix/Compiler/Backend/C/Translation/FromReg.hs @@ -256,6 +256,9 @@ fromRegInstr bNoStack info = \case Reg.Block Reg.InstrBlock {..} -> fromRegCode bNoStack info _instrBlockCode where + unsupported :: Text -> a + unsupported x = error ("unsupported: " <> x) + fromBinaryOp :: Reg.InstrBinop -> Statement fromBinaryOp Reg.InstrBinop {..} = StatementExpr $ @@ -277,6 +280,10 @@ fromRegInstr bNoStack info = \case Reg.OpIntLe -> "JUVIX_INT_LE" Reg.OpEq -> "JUVIX_VAL_EQ" Reg.OpStrConcat -> "JUVIX_STR_CONCAT" + Reg.OpFieldAdd -> unsupported "field type" + Reg.OpFieldSub -> unsupported "field type" + Reg.OpFieldMul -> unsupported "field type" + Reg.OpFieldDiv -> unsupported "field type" fromUnaryOp :: Reg.InstrUnop -> Statement fromUnaryOp Reg.InstrUnop {..} = @@ -292,6 +299,8 @@ fromRegInstr bNoStack info = \case Reg.OpShow -> "JUVIX_SHOW" Reg.OpStrToInt -> "JUVIX_STR_TO_INT" Reg.OpArgsNum -> "JUVIX_ARGS_NUM" + Reg.OpFieldToInt -> unsupported "field type" + Reg.OpIntToField -> unsupported "field type" fromVarRef :: Reg.VarRef -> Expression fromVarRef Reg.VarRef {..} = @@ -322,6 +331,7 @@ fromRegInstr bNoStack info = \case fromConst :: Reg.Constant -> Expression fromConst = \case Reg.ConstInt x -> macroCall "make_smallint" [integer x] + Reg.ConstField {} -> impossible Reg.ConstBool True -> macroVar "BOOL_TRUE" Reg.ConstBool False -> macroVar "BOOL_FALSE" Reg.ConstString x -> macroCall "GET_CONST_CSTRING" [integer (getStringId info x)] diff --git a/src/Juvix/Compiler/Backend/Geb/Translation/FromCore.hs b/src/Juvix/Compiler/Backend/Geb/Translation/FromCore.hs index 43c21e717..b81bfdaf2 100644 --- a/src/Juvix/Compiler/Backend/Geb/Translation/FromCore.hs +++ b/src/Juvix/Compiler/Backend/Geb/Translation/FromCore.hs @@ -156,6 +156,7 @@ fromCore tab = case tab ^. Core.infoMain of convertConstant :: Core.Constant -> Trans Morphism convertConstant Core.Constant {..} = case _constantValue of Core.ConstInteger n -> return $ MorphismInteger (BitChoice {_bitChoice = n}) + Core.ConstField {} -> unsupported Core.ConstString {} -> unsupported convertApp :: Core.App -> Trans Morphism @@ -543,6 +544,7 @@ fromCore tab = case tab ^. Core.infoMain of case _typePrimPrimitive of Core.PrimInteger {} -> ObjectInteger Core.PrimBool {} -> objectBool + Core.PrimField {} -> unsupported Core.PrimString -> unsupported convertInductive :: Symbol -> Object diff --git a/src/Juvix/Compiler/Backend/VampIR/Language.hs b/src/Juvix/Compiler/Backend/VampIR/Language.hs index 96b5a14f1..11c08d519 100644 --- a/src/Juvix/Compiler/Backend/VampIR/Language.hs +++ b/src/Juvix/Compiler/Backend/VampIR/Language.hs @@ -16,6 +16,10 @@ data OpCode | OpMul | OpDiv | OpMod + | OpFieldAdd + | OpFieldSub + | OpFieldMul + | OpFieldDiv | OpEq | OpLt | OpLe diff --git a/src/Juvix/Compiler/Backend/VampIR/Pretty/Base.hs b/src/Juvix/Compiler/Backend/VampIR/Pretty/Base.hs index ca3375380..4c05c0286 100644 --- a/src/Juvix/Compiler/Backend/VampIR/Pretty/Base.hs +++ b/src/Juvix/Compiler/Backend/VampIR/Pretty/Base.hs @@ -29,6 +29,10 @@ instance PrettyCode OpCode where OpMul -> return kwMul OpDiv -> return kwDiv OpMod -> return kwMod + OpFieldAdd -> return kwFieldAdd + OpFieldSub -> return kwFieldSub + OpFieldMul -> return kwFieldMul + OpFieldDiv -> return kwFieldDiv OpEq -> return kwEqual OpLt -> return kwLessThan OpLe -> return kwLessOrEqual diff --git a/src/Juvix/Compiler/Backend/VampIR/Pretty/Keywords.hs b/src/Juvix/Compiler/Backend/VampIR/Pretty/Keywords.hs index a54fdb596..c40416fa7 100644 --- a/src/Juvix/Compiler/Backend/VampIR/Pretty/Keywords.hs +++ b/src/Juvix/Compiler/Backend/VampIR/Pretty/Keywords.hs @@ -31,6 +31,18 @@ kwDiv = keyword Str.vampirDiv kwMod :: Doc Ann kwMod = keyword Str.vampirMod +kwFieldAdd :: Doc Ann +kwFieldAdd = keyword Str.fadd + +kwFieldSub :: Doc Ann +kwFieldSub = keyword Str.fsub + +kwFieldMul :: Doc Ann +kwFieldMul = keyword Str.fmul + +kwFieldDiv :: Doc Ann +kwFieldDiv = keyword Str.fdiv + kwEqual :: Doc Ann kwEqual = keyword Str.vampirEqual diff --git a/src/Juvix/Compiler/Backend/VampIR/Translation/FromCore.hs b/src/Juvix/Compiler/Backend/VampIR/Translation/FromCore.hs index 77bb107a3..2e7e86071 100644 --- a/src/Juvix/Compiler/Backend/VampIR/Translation/FromCore.hs +++ b/src/Juvix/Compiler/Backend/VampIR/Translation/FromCore.hs @@ -92,11 +92,18 @@ fromCoreNode ii node = OpIntMod -> OpMod OpIntLt -> OpLt OpIntLe -> OpLe + Core.OpFieldAdd -> VampIR.OpFieldAdd + Core.OpFieldSub -> VampIR.OpFieldSub + Core.OpFieldMul -> VampIR.OpFieldMul + Core.OpFieldDiv -> VampIR.OpFieldDiv Core.OpEq -> VampIR.OpEq _ -> impossible - _ -> case _builtinAppOp of + [x] -> case _builtinAppOp of OpFail -> ExpressionFail + OpFieldToInt -> convertExpr x + OpFieldFromInt -> convertExpr x _ -> impossible + _ -> impossible goConstructor :: Constr -> Expression goConstructor Constr {..} = case _constrTag of diff --git a/src/Juvix/Compiler/Builtins.hs b/src/Juvix/Compiler/Builtins.hs index 4b91a0919..00a2d1e8d 100644 --- a/src/Juvix/Compiler/Builtins.hs +++ b/src/Juvix/Compiler/Builtins.hs @@ -6,6 +6,7 @@ module Juvix.Compiler.Builtins module Juvix.Compiler.Builtins.Bool, module Juvix.Compiler.Builtins.List, module Juvix.Compiler.Builtins.String, + module Juvix.Compiler.Builtins.Field, module Juvix.Compiler.Builtins.Debug, module Juvix.Compiler.Builtins.Control, ) @@ -15,6 +16,7 @@ import Juvix.Compiler.Builtins.Bool import Juvix.Compiler.Builtins.Control import Juvix.Compiler.Builtins.Debug import Juvix.Compiler.Builtins.Effect +import Juvix.Compiler.Builtins.Field import Juvix.Compiler.Builtins.IO import Juvix.Compiler.Builtins.Int import Juvix.Compiler.Builtins.List diff --git a/src/Juvix/Compiler/Builtins/Field.hs b/src/Juvix/Compiler/Builtins/Field.hs new file mode 100644 index 000000000..a2c305ce2 --- /dev/null +++ b/src/Juvix/Compiler/Builtins/Field.hs @@ -0,0 +1,55 @@ +module Juvix.Compiler.Builtins.Field where + +import Juvix.Compiler.Builtins.Effect +import Juvix.Compiler.Internal.Extra +import Juvix.Prelude + +registerField :: (Member Builtins r) => AxiomDef -> Sem r () +registerField d = do + unless (isSmallUniverse' (d ^. axiomType)) (error "String should be in the small universe") + registerBuiltin BuiltinField (d ^. axiomName) + +registerFieldEq :: (Member Builtins r) => AxiomDef -> Sem r () +registerFieldEq f = do + field_ <- getBuiltinName (getLoc f) BuiltinField + bool_ <- getBuiltinName (getLoc f) BuiltinBool + unless (f ^. axiomType === (field_ --> field_ --> bool_)) (error "field equality has the wrong type signature") + registerBuiltin BuiltinFieldEq (f ^. axiomName) + +registerFieldAdd :: (Member Builtins r) => AxiomDef -> Sem r () +registerFieldAdd f = do + field_ <- getBuiltinName (getLoc f) BuiltinField + unless (f ^. axiomType === (field_ --> field_ --> field_)) (error "field addition has the wrong type signature") + registerBuiltin BuiltinFieldAdd (f ^. axiomName) + +registerFieldSub :: (Member Builtins r) => AxiomDef -> Sem r () +registerFieldSub f = do + field_ <- getBuiltinName (getLoc f) BuiltinField + unless (f ^. axiomType === (field_ --> field_ --> field_)) (error "field subtraction has the wrong type signature") + registerBuiltin BuiltinFieldSub (f ^. axiomName) + +registerFieldMul :: (Member Builtins r) => AxiomDef -> Sem r () +registerFieldMul f = do + field_ <- getBuiltinName (getLoc f) BuiltinField + unless (f ^. axiomType === (field_ --> field_ --> field_)) (error "field multiplication has the wrong type signature") + registerBuiltin BuiltinFieldMul (f ^. axiomName) + +registerFieldDiv :: (Member Builtins r) => AxiomDef -> Sem r () +registerFieldDiv f = do + field_ <- getBuiltinName (getLoc f) BuiltinField + unless (f ^. axiomType === (field_ --> field_ --> field_)) (error "field division has the wrong type signature") + registerBuiltin BuiltinFieldDiv (f ^. axiomName) + +registerFieldFromInt :: (Member Builtins r) => AxiomDef -> Sem r () +registerFieldFromInt f = do + field_ <- getBuiltinName (getLoc f) BuiltinField + int_ <- getBuiltinName (getLoc f) BuiltinInt + unless (f ^. axiomType === (int_ --> field_)) (error "integer to field conversion has the wrong type signature") + registerBuiltin BuiltinFieldFromInt (f ^. axiomName) + +registerFieldToNat :: (Member Builtins r) => AxiomDef -> Sem r () +registerFieldToNat f = do + field_ <- getBuiltinName (getLoc f) BuiltinField + nat_ <- getBuiltinName (getLoc f) BuiltinNat + unless (f ^. axiomType === (field_ --> nat_)) (error "field to nat conversion has the wrong type signature") + registerBuiltin BuiltinFieldToNat (f ^. axiomName) diff --git a/src/Juvix/Compiler/Casm/Interpreter.hs b/src/Juvix/Compiler/Casm/Interpreter.hs index 43dc431c8..103425997 100644 --- a/src/Juvix/Compiler/Casm/Interpreter.hs +++ b/src/Juvix/Compiler/Casm/Interpreter.hs @@ -15,11 +15,12 @@ import Juvix.Compiler.Casm.Data.LabelInfo import Juvix.Compiler.Casm.Error import Juvix.Compiler.Casm.Interpreter.Error import Juvix.Compiler.Casm.Language hiding (ap) +import Juvix.Data.Field -type Memory s = MV.MVector s (Maybe Integer) +type Memory s = MV.MVector s (Maybe FField) -- | Runs Cairo Assembly. Returns the value of `[ap - 1]` at program exit. -runCode :: LabelInfo -> [Instruction] -> Integer +runCode :: LabelInfo -> [Instruction] -> FField runCode (LabelInfo labelInfo) instrs0 = runST goCode where instrs :: Vec.Vector Instruction @@ -28,7 +29,10 @@ runCode (LabelInfo labelInfo) instrs0 = runST goCode initialMemSize :: Int initialMemSize = 1024 - goCode :: ST s Integer + fsize :: Natural + fsize = cairoFieldSize + + goCode :: ST s FField goCode = do mem <- MV.replicate initialMemSize Nothing go 0 0 0 mem @@ -38,7 +42,7 @@ runCode (LabelInfo labelInfo) instrs0 = runST goCode Address -> Address -> Memory s -> - ST s Integer + ST s FField go pc ap fp mem | Vec.length instrs <= pc = do when (Vec.length instrs < pc) $ @@ -81,14 +85,14 @@ runCode (LabelInfo labelInfo) instrs0 = runST goCode Ap -> ap Fp -> fp - readMem :: Memory s -> Address -> ST s Integer + readMem :: Memory s -> Address -> ST s FField readMem mem addr = do mv <- MV.read mem addr case mv of Just v -> return v Nothing -> throwRunError ("reading uninitialized memory at address " <> show addr) - writeMem :: Memory s -> Address -> Integer -> ST s (Memory s) + writeMem :: Memory s -> Address -> FField -> ST s (Memory s) writeMem mem addr v = do let len = MV.length mem mem' <- @@ -104,59 +108,62 @@ runCode (LabelInfo labelInfo) instrs0 = runST goCode MV.write mem' addr (Just v) return mem' - writeMemRef :: Address -> Address -> Memory s -> MemRef -> Integer -> ST s (Memory s) + writeMemRef :: Address -> Address -> Memory s -> MemRef -> FField -> ST s (Memory s) writeMemRef ap fp mem MemRef {..} v = do let r = readReg ap fp _memRefReg off :: Int = fromIntegral _memRefOff writeMem mem (r + off) v - readMemRef :: Address -> Address -> Memory s -> MemRef -> ST s Integer + readMemRef :: Address -> Address -> Memory s -> MemRef -> ST s FField readMemRef ap fp mem MemRef {..} = do let r = readReg ap fp _memRefReg off :: Int = fromIntegral _memRefOff readMem mem (r + off) - readLabel :: LabelRef -> Integer + readLabel :: LabelRef -> FField readLabel LabelRef {..} = - fromIntegral $ fromMaybe (throwRunError "invalid label") $ HashMap.lookup _labelRefSymbol labelInfo + fieldFromInteger fsize $ + fromIntegral $ + fromMaybe (throwRunError "invalid label") $ + HashMap.lookup _labelRefSymbol labelInfo - readValue :: Address -> Address -> Memory s -> Value -> ST s Integer + readValue :: Address -> Address -> Memory s -> Value -> ST s FField readValue ap fp mem = \case - Imm v -> return v + Imm v -> return $ fieldFromInteger fsize v Ref r -> readMemRef ap fp mem r Lab l -> return $ readLabel l - readLoadValue :: Address -> Address -> Memory s -> LoadValue -> ST s Integer + readLoadValue :: Address -> Address -> Memory s -> LoadValue -> ST s FField readLoadValue ap fp mem LoadValue {..} = do src <- readMemRef ap fp mem _loadValueSrc let off :: Int = fromIntegral _loadValueOff - addr :: Int = fromInteger src + off + addr :: Int = fromInteger (fieldToInteger src) + off readMem mem addr - readBinopValue :: Address -> Address -> Memory s -> BinopValue -> ST s Integer + readBinopValue :: Address -> Address -> Memory s -> BinopValue -> ST s FField readBinopValue ap fp mem BinopValue {..} = do v1 <- readMemRef ap fp mem _binopValueArg1 v2 <- readValue ap fp mem _binopValueArg2 return $ goOp v1 v2 _binopValueOpcode where - goOp :: Integer -> Integer -> Opcode -> Integer + goOp :: FField -> FField -> Opcode -> FField goOp x y = \case - FieldAdd -> x + y - FieldMul -> x * y + FieldAdd -> fieldAdd x y + FieldMul -> fieldMul x y - readRValue :: Address -> Address -> Memory s -> RValue -> ST s Integer + readRValue :: Address -> Address -> Memory s -> RValue -> ST s FField readRValue ap fp mem = \case Val x -> readValue ap fp mem x Load x -> readLoadValue ap fp mem x Binop x -> readBinopValue ap fp mem x - goAssign :: InstrAssign -> Address -> Address -> Address -> Memory s -> ST s Integer + goAssign :: InstrAssign -> Address -> Address -> Address -> Memory s -> ST s FField goAssign InstrAssign {..} pc ap fp mem = do v <- readRValue ap fp mem _instrAssignValue mem' <- writeMemRef ap fp mem _instrAssignResult v go (pc + 1) (ap + fromEnum _instrAssignIncAp) fp mem' - goExtraBinop :: InstrExtraBinop -> Address -> Address -> Address -> Memory s -> ST s Integer + goExtraBinop :: InstrExtraBinop -> Address -> Address -> Address -> Memory s -> ST s FField goExtraBinop InstrExtraBinop {..} pc ap fp mem = do v1 <- readMemRef ap fp mem _instrExtraBinopArg1 v2 <- readValue ap fp mem _instrExtraBinopArg2 @@ -164,51 +171,61 @@ runCode (LabelInfo labelInfo) instrs0 = runST goCode mem' <- writeMemRef ap fp mem _instrExtraBinopResult v go (pc + 1) (ap + fromEnum _instrExtraBinopIncAp) fp mem' where - goOp :: Integer -> Integer -> ExtraOpcode -> Integer + goOp :: FField -> FField -> ExtraOpcode -> FField goOp x y = \case - FieldSub -> x - y - IntAdd -> x + y - IntSub -> x - y - IntMul -> x * y - IntDiv -> x `quot` y - IntMod -> x `rem` y - IntLt -> if x < y then 1 else 0 + FieldSub -> fieldSub x y + FieldDiv -> fieldDiv x y + IntAdd -> fieldAdd x y + IntSub -> fieldSub x y + IntMul -> fieldMul x y + IntDiv -> fieldFromInteger fsize (fieldToInt x `quot` fieldToInt y) + IntMod -> fieldFromInteger fsize (fieldToInt x `rem` fieldToInt y) + IntLt -> + fieldFromInteger fsize $ + if fieldToInt x < fieldToInt y then 1 else 0 - goJump :: InstrJump -> Address -> Address -> Address -> Memory s -> ST s Integer + fieldToInt :: FField -> Integer + fieldToInt f + | v < fromIntegral fsize `div` 2 = v + | otherwise = v - fromIntegral fsize + where + v = fieldToInteger f + + goJump :: InstrJump -> Address -> Address -> Address -> Memory s -> ST s FField goJump InstrJump {..} _ ap fp mem = do tgt <- readValue ap fp mem _instrJumpTarget - go (fromInteger tgt) (ap + fromEnum _instrJumpIncAp) fp mem + go (fromInteger (fieldToInteger tgt)) (ap + fromEnum _instrJumpIncAp) fp mem - goJumpIf :: InstrJumpIf -> Address -> Address -> Address -> Memory s -> ST s Integer + goJumpIf :: InstrJumpIf -> Address -> Address -> Address -> Memory s -> ST s FField goJumpIf InstrJumpIf {..} pc ap fp mem = do tgt <- readValue ap fp mem _instrJumpIfTarget v <- readMemRef ap fp mem _instrJumpIfValue - go (if v /= 0 then fromInteger tgt else pc + 1) (ap + fromEnum _instrJumpIfIncAp) fp mem + go (if fieldToInteger v /= 0 then fromInteger (fieldToInteger tgt) else pc + 1) (ap + fromEnum _instrJumpIfIncAp) fp mem - goJumpRel :: InstrJumpRel -> Address -> Address -> Address -> Memory s -> ST s Integer + goJumpRel :: InstrJumpRel -> Address -> Address -> Address -> Memory s -> ST s FField goJumpRel InstrJumpRel {..} pc ap fp mem = do tgt <- readRValue ap fp mem _instrJumpRelTarget - go (pc + fromInteger tgt) (ap + fromEnum _instrJumpRelIncAp) fp mem + go (pc + fromInteger (fieldToInteger tgt)) (ap + fromEnum _instrJumpRelIncAp) fp mem - goCall :: InstrCall -> Address -> Address -> Address -> Memory s -> ST s Integer + goCall :: InstrCall -> Address -> Address -> Address -> Memory s -> ST s FField goCall InstrCall {..} pc ap fp mem = do tgt <- readValue ap fp mem _instrCallTarget - mem' <- writeMem mem ap (fromIntegral fp) - mem'' <- writeMem mem' (ap + 1) (fromIntegral pc + 1) - go (fromInteger tgt) (ap + 2) (ap + 2) mem'' + mem' <- writeMem mem ap (fieldFromInteger fsize (fromIntegral fp)) + mem'' <- writeMem mem' (ap + 1) (fieldFromInteger fsize (fromIntegral pc + 1)) + go (fromInteger (fieldToInteger tgt)) (ap + 2) (ap + 2) mem'' - goReturn :: Address -> Address -> Address -> Memory s -> ST s Integer + goReturn :: Address -> Address -> Address -> Memory s -> ST s FField goReturn _ ap fp mem = do pc' <- readMem mem (fp - 1) fp' <- readMem mem (fp - 2) - go (fromInteger pc') ap (fromInteger fp') mem + go (fromInteger (fieldToInteger pc')) ap (fromInteger (fieldToInteger fp')) mem - goAlloc :: InstrAlloc -> Address -> Address -> Address -> Memory s -> ST s Integer + goAlloc :: InstrAlloc -> Address -> Address -> Address -> Memory s -> ST s FField goAlloc InstrAlloc {..} pc ap fp mem = do v <- readRValue ap fp mem _instrAllocSize - go (pc + 1) (ap + fromInteger v) fp mem + go (pc + 1) (ap + fromInteger (fieldToInteger v)) fp mem - goTrace :: InstrTrace -> Address -> Address -> Address -> Memory s -> ST s Integer + goTrace :: InstrTrace -> Address -> Address -> Address -> Memory s -> ST s FField goTrace InstrTrace {..} pc ap fp mem = do v <- readRValue ap fp mem _instrTraceValue GHC.unsafePerformIO (print v >> return (pure ())) diff --git a/src/Juvix/Compiler/Casm/Keywords.hs b/src/Juvix/Compiler/Casm/Keywords.hs index d319d36dd..347598714 100644 --- a/src/Juvix/Compiler/Casm/Keywords.hs +++ b/src/Juvix/Compiler/Casm/Keywords.hs @@ -12,6 +12,7 @@ import Juvix.Data.Keyword.All kwApPlusPlus, kwCall, kwColon, + kwDiv, kwEq, kwFp, kwIf, @@ -43,6 +44,7 @@ allKeywords = kwApPlusPlus, kwCall, kwColon, + kwDiv, kwEq, kwFp, kwIf, diff --git a/src/Juvix/Compiler/Casm/Language.hs b/src/Juvix/Compiler/Casm/Language.hs index d2dd13dcd..6d78172b3 100644 --- a/src/Juvix/Compiler/Casm/Language.hs +++ b/src/Juvix/Compiler/Casm/Language.hs @@ -72,6 +72,7 @@ data RValue -- `ap` arbitrarily. data ExtraOpcode = FieldSub + | FieldDiv | IntAdd | IntSub | IntMul diff --git a/src/Juvix/Compiler/Casm/Pretty/Base.hs b/src/Juvix/Compiler/Casm/Pretty/Base.hs index 0f4a51ea6..14c3d460b 100644 --- a/src/Juvix/Compiler/Casm/Pretty/Base.hs +++ b/src/Juvix/Compiler/Casm/Pretty/Base.hs @@ -69,6 +69,7 @@ instance PrettyCode Opcode where instance PrettyCode ExtraOpcode where ppCode = \case FieldSub -> return Str.minus + FieldDiv -> return Str.div IntAdd -> return Str.iadd IntSub -> return Str.isub IntMul -> return Str.imul diff --git a/src/Juvix/Compiler/Casm/Translation/FromSource.hs b/src/Juvix/Compiler/Casm/Translation/FromSource.hs index d48169d7a..6a17bb91d 100644 --- a/src/Juvix/Compiler/Casm/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Casm/Translation/FromSource.hs @@ -253,6 +253,7 @@ parseAssign = do parseExtraValue :: ExtraOpcode -> ParsecS r Value parseExtraValue = \case FieldSub -> Ref <$> parseMemRef + FieldDiv -> Ref <$> parseMemRef _ -> parseValue registerAP :: ParsecS r Reg @@ -276,6 +277,7 @@ opcode = extraOpcode :: ParsecS r ExtraOpcode extraOpcode = (kw kwMinus >> return FieldSub) + <|> (kw kwDiv >> return FieldDiv) <|> (kw kwIntAdd >> return IntAdd) <|> (kw kwIntSub >> return IntSub) <|> (kw kwIntMul >> return IntMul) diff --git a/src/Juvix/Compiler/Concrete/Data/Builtins.hs b/src/Juvix/Compiler/Concrete/Data/Builtins.hs index 7e749e61e..df4a6c936 100644 --- a/src/Juvix/Compiler/Concrete/Data/Builtins.hs +++ b/src/Juvix/Compiler/Concrete/Data/Builtins.hs @@ -161,6 +161,14 @@ data BuiltinAxiom | BuiltinStringEq | BuiltinStringToNat | BuiltinBoolPrint + | BuiltinFieldEq + | BuiltinFieldAdd + | BuiltinFieldSub + | BuiltinFieldMul + | BuiltinFieldDiv + | BuiltinField + | BuiltinFieldFromInt + | BuiltinFieldToNat | BuiltinString | BuiltinIO | BuiltinIOSequence @@ -183,6 +191,14 @@ instance Pretty BuiltinAxiom where BuiltinStringConcat -> Str.stringConcat BuiltinStringEq -> Str.stringEq BuiltinStringToNat -> Str.stringToNat + BuiltinFieldEq -> Str.fieldEq + BuiltinFieldAdd -> Str.fieldAdd + BuiltinFieldSub -> Str.fieldSub + BuiltinFieldMul -> Str.fieldMul + BuiltinFieldDiv -> Str.fieldDiv + BuiltinField -> Str.field + BuiltinFieldFromInt -> Str.fieldFromInt + BuiltinFieldToNat -> Str.fieldToNat BuiltinBoolPrint -> Str.boolPrint BuiltinIO -> Str.io BuiltinString -> Str.string diff --git a/src/Juvix/Compiler/Core/Data/Stripped/InfoTable.hs b/src/Juvix/Compiler/Core/Data/Stripped/InfoTable.hs index c3e9e78ca..01ebb2706 100644 --- a/src/Juvix/Compiler/Core/Data/Stripped/InfoTable.hs +++ b/src/Juvix/Compiler/Core/Data/Stripped/InfoTable.hs @@ -7,7 +7,8 @@ data InfoTable = InfoTable { _infoMain :: Maybe Symbol, _infoFunctions :: HashMap Symbol FunctionInfo, _infoInductives :: HashMap Symbol InductiveInfo, - _infoConstructors :: HashMap Tag ConstructorInfo + _infoConstructors :: HashMap Tag ConstructorInfo, + _infoFieldSize :: Natural } data FunctionInfo = FunctionInfo diff --git a/src/Juvix/Compiler/Core/Evaluator.hs b/src/Juvix/Compiler/Core/Evaluator.hs index 98c102296..932b8398b 100644 --- a/src/Juvix/Compiler/Core/Evaluator.hs +++ b/src/Juvix/Compiler/Core/Evaluator.hs @@ -12,12 +12,14 @@ import Juvix.Compiler.Core.Extra import Juvix.Compiler.Core.Info qualified as Info import Juvix.Compiler.Core.Info.NoDisplayInfo import Juvix.Compiler.Core.Pretty +import Juvix.Data.Field import Text.Read qualified as T data EvalOptions = EvalOptions { _evalOptionsNormalize :: Bool, _evalOptionsNoFailure :: Bool, - _evalOptionsSilent :: Bool + _evalOptionsSilent :: Bool, + _evalOptionsFieldSize :: Natural } makeLenses ''EvalOptions @@ -27,7 +29,8 @@ defaultEvalOptions = EvalOptions { _evalOptionsNormalize = False, _evalOptionsNoFailure = False, - _evalOptionsSilent = False + _evalOptionsSilent = False, + _evalOptionsFieldSize = defaultFieldSize } data EvalError = EvalError @@ -169,6 +172,12 @@ geval opts herr ctx env0 = eval' env0 OpIntMul -> binNumOp (*) OpIntLt -> binNumCmpOp (<) OpIntLe -> binNumCmpOp (<=) + OpFieldAdd -> binFieldOp fieldAdd + OpFieldSub -> binFieldOp fieldSub + OpFieldMul -> binFieldOp fieldMul + OpFieldDiv -> binFieldOp fieldDiv + OpFieldFromInt -> fieldFromIntOp + OpFieldToInt -> fieldToIntOp OpEq -> eqOp OpIntDiv -> divOp quot OpIntMod -> divOp rem @@ -223,6 +232,30 @@ geval opts herr ctx env0 = eval' env0 binNumOp = binOp nodeFromInteger integerFromNode {-# INLINE binNumOp #-} + binFieldOp :: (FField -> FField -> FField) -> [Node] -> Node + binFieldOp = binOp nodeFromField fieldFromNode + {-# INLINE binFieldOp #-} + + fieldFromIntOp :: [Node] -> Node + fieldFromIntOp = + unary $ \node -> + let !v = eval' env node + in nodeFromField $ + fieldFromInteger (opts ^. evalOptionsFieldSize) $ + fromMaybe (evalError "expected integer" v) $ + integerFromNode v + {-# INLINE fieldFromIntOp #-} + + fieldToIntOp :: [Node] -> Node + fieldToIntOp = + unary $ \node -> + let !v = eval' env node + in nodeFromInteger $ + fieldToInteger $ + fromMaybe (evalError "expected field element" v) $ + fieldFromNode v + {-# INLINE fieldToIntOp #-} + eqOp :: [Node] -> Node eqOp | opts ^. evalOptionsNormalize = @@ -285,6 +318,10 @@ geval opts herr ctx env0 = eval' env0 nodeFromInteger !int = mkConstant' (ConstInteger int) {-# INLINE nodeFromInteger #-} + nodeFromField :: FField -> Node + nodeFromField !fld = mkConstant' (ConstField fld) + {-# INLINE nodeFromField #-} + nodeFromBool :: Bool -> Node nodeFromBool b = mkConstr' (BuiltinTag tag) [] where @@ -299,6 +336,12 @@ geval opts herr ctx env0 = eval' env0 _ -> Nothing {-# INLINE integerFromNode #-} + fieldFromNode :: Node -> Maybe FField + fieldFromNode = \case + NCst (Constant _ (ConstField fld)) -> Just fld + _ -> Nothing + {-# INLINE fieldFromNode #-} + printNode :: Node -> Text printNode = \case NCst (Constant _ (ConstString s)) -> s @@ -395,22 +438,30 @@ evalIO = hEvalIO stderr stdin stdout doEval :: forall r. (MonadIO (Sem r)) => + Maybe Natural -> Bool -> Interval -> InfoTable -> Node -> Sem r (Either CoreError Node) -doEval noIO loc tab node +doEval mfsize noIO loc tab node | noIO = catchEvalError loc (eval stderr (tab ^. identContext) [] node) - | otherwise = liftIO (catchEvalErrorIO loc (evalIO (tab ^. identContext) [] node)) + | otherwise = liftIO (catchEvalErrorIO loc (hEvalIO' opts stderr stdin stdout (tab ^. identContext) [] node)) + where + opts = + maybe + defaultEvalOptions + (\fsize -> defaultEvalOptions {_evalOptionsFieldSize = fsize}) + mfsize doEvalIO :: + Maybe Natural -> Bool -> Interval -> InfoTable -> Node -> IO (Either CoreError Node) -doEvalIO noIO i tab node = runM (doEval noIO i tab node) +doEvalIO mfsize noIO i tab node = runM (doEval mfsize noIO i tab node) -- | Catch EvalError and convert it to CoreError. Needs a default location in case -- no location is available in EvalError. diff --git a/src/Juvix/Compiler/Core/Extra/Base.hs b/src/Juvix/Compiler/Core/Extra/Base.hs index 1aec5f293..a72f8729d 100644 --- a/src/Juvix/Compiler/Core/Extra/Base.hs +++ b/src/Juvix/Compiler/Core/Extra/Base.hs @@ -188,6 +188,12 @@ mkTypeString i = mkTypePrim i PrimString mkTypeString' :: Type mkTypeString' = mkTypeString Info.empty +mkTypeField :: Info -> Type +mkTypeField i = mkTypePrim i PrimField + +mkTypeField' :: Type +mkTypeField' = mkTypeField Info.empty + mkDynamic :: Info -> Type mkDynamic i = NDyn (Dynamic i) diff --git a/src/Juvix/Compiler/Core/Extra/Utils.hs b/src/Juvix/Compiler/Core/Extra/Utils.hs index 171ecdaea..e8479a875 100644 --- a/src/Juvix/Compiler/Core/Extra/Utils.hs +++ b/src/Juvix/Compiler/Core/Extra/Utils.hs @@ -410,6 +410,12 @@ builtinOpArgTypes = \case OpIntMod -> [mkTypeInteger', mkTypeInteger'] OpIntLt -> [mkTypeInteger', mkTypeInteger'] OpIntLe -> [mkTypeInteger', mkTypeInteger'] + OpFieldAdd -> [mkTypeField', mkTypeField'] + OpFieldSub -> [mkTypeField', mkTypeField'] + OpFieldMul -> [mkTypeField', mkTypeField'] + OpFieldDiv -> [mkTypeField', mkTypeField'] + OpFieldFromInt -> [mkTypeInteger'] + OpFieldToInt -> [mkTypeField'] OpEq -> [mkDynamic', mkDynamic'] OpShow -> [mkDynamic'] OpStrConcat -> [mkTypeString', mkTypeString'] diff --git a/src/Juvix/Compiler/Core/Keywords.hs b/src/Juvix/Compiler/Core/Keywords.hs index cc572d591..68effbf32 100644 --- a/src/Juvix/Compiler/Core/Keywords.hs +++ b/src/Juvix/Compiler/Core/Keywords.hs @@ -21,6 +21,10 @@ import Juvix.Data.Keyword.All kwElse, kwEq, kwFail, + kwFieldAdd, + kwFieldDiv, + kwFieldMul, + kwFieldSub, kwGe, kwGt, kwIf, @@ -67,6 +71,10 @@ allKeywords = kwDiv, kwElse, kwEq, + kwFieldAdd, + kwFieldDiv, + kwFieldMul, + kwFieldSub, kwIf, kwIn, kwInductive, diff --git a/src/Juvix/Compiler/Core/Language/Builtins.hs b/src/Juvix/Compiler/Core/Language/Builtins.hs index c8672130d..5df7f075f 100644 --- a/src/Juvix/Compiler/Core/Language/Builtins.hs +++ b/src/Juvix/Compiler/Core/Language/Builtins.hs @@ -13,6 +13,12 @@ data BuiltinOp | OpIntMod | OpIntLt | OpIntLe + | OpFieldAdd + | OpFieldSub + | OpFieldMul + | OpFieldDiv + | OpFieldFromInt + | OpFieldToInt | OpEq | OpShow | OpStrConcat @@ -47,6 +53,12 @@ builtinOpArgsNum = \case OpIntMod -> 2 OpIntLt -> 2 OpIntLe -> 2 + OpFieldAdd -> 2 + OpFieldSub -> 2 + OpFieldMul -> 2 + OpFieldDiv -> 2 + OpFieldFromInt -> 1 + OpFieldToInt -> 1 OpEq -> 2 OpShow -> 1 OpStrConcat -> 2 diff --git a/src/Juvix/Compiler/Core/Language/Nodes.hs b/src/Juvix/Compiler/Core/Language/Nodes.hs index 2dec75ed0..43fb0bbc8 100644 --- a/src/Juvix/Compiler/Core/Language/Nodes.hs +++ b/src/Juvix/Compiler/Core/Language/Nodes.hs @@ -11,6 +11,7 @@ import Data.Serialize import Juvix.Compiler.Core.Language.Base import Juvix.Compiler.Core.Language.Builtins import Juvix.Compiler.Core.Language.Primitives +import Juvix.Data.Field -- | De Bruijn index of a locally bound variable. data Var' i = Var @@ -35,6 +36,7 @@ data Constant' i = Constant data ConstantValue = ConstInteger !Integer + | ConstField !FField | ConstString !Text deriving stock (Eq, Generic) diff --git a/src/Juvix/Compiler/Core/Language/Primitives.hs b/src/Juvix/Compiler/Core/Language/Primitives.hs index 17f4e4cdd..3ef3a3d53 100644 --- a/src/Juvix/Compiler/Core/Language/Primitives.hs +++ b/src/Juvix/Compiler/Core/Language/Primitives.hs @@ -14,6 +14,7 @@ data Primitive = PrimInteger PrimIntegerInfo | PrimBool PrimBoolInfo | PrimString + | PrimField deriving stock (Eq, Generic) -- | Info about a type represented as an integer. diff --git a/src/Juvix/Compiler/Core/Normalizer.hs b/src/Juvix/Compiler/Core/Normalizer.hs index 289b80a2f..d447e6e47 100644 --- a/src/Juvix/Compiler/Core/Normalizer.hs +++ b/src/Juvix/Compiler/Core/Normalizer.hs @@ -20,8 +20,8 @@ makeLenses ''NormEnv type Norm = Sem '[Reader NormEnv, InfoTableBuilder] -normalize :: Module -> Node -> Node -normalize md = run . evalInfoTableBuilder md . runReader normEnv . normalize' +normalize :: Natural -> Module -> Node -> Node +normalize fsize md = run . evalInfoTableBuilder md . runReader normEnv . normalize' where normEnv = NormEnv @@ -43,7 +43,8 @@ normalize md = run . evalInfoTableBuilder md . runReader normEnv . normalize' where opts = defaultEvalOptions - { _evalOptionsNormalize = True + { _evalOptionsNormalize = True, + _evalOptionsFieldSize = fsize } go :: Node -> Norm Node diff --git a/src/Juvix/Compiler/Core/Options.hs b/src/Juvix/Compiler/Core/Options.hs index 3a99eabc1..ffb9b6534 100644 --- a/src/Juvix/Compiler/Core/Options.hs +++ b/src/Juvix/Compiler/Core/Options.hs @@ -1,13 +1,15 @@ module Juvix.Compiler.Core.Options where import Juvix.Compiler.Pipeline.EntryPoint +import Juvix.Data.Field import Juvix.Prelude data CoreOptions = CoreOptions { _optCheckCoverage :: Bool, _optUnrollLimit :: Int, _optOptimizationLevel :: Int, - _optInliningDepth :: Int + _optInliningDepth :: Int, + _optFieldSize :: Natural } makeLenses ''CoreOptions @@ -18,7 +20,8 @@ defaultCoreOptions = { _optCheckCoverage = True, _optUnrollLimit = defaultUnrollLimit, _optOptimizationLevel = defaultOptimizationLevel, - _optInliningDepth = defaultInliningDepth + _optInliningDepth = defaultInliningDepth, + _optFieldSize = defaultFieldSize } fromEntryPoint :: EntryPoint -> CoreOptions @@ -27,5 +30,6 @@ fromEntryPoint EntryPoint {..} = { _optCheckCoverage = not _entryPointNoCoverage, _optUnrollLimit = _entryPointUnrollLimit, _optOptimizationLevel = _entryPointOptimizationLevel, - _optInliningDepth = _entryPointInliningDepth + _optInliningDepth = _entryPointInliningDepth, + _optFieldSize = _entryPointFieldSize } diff --git a/src/Juvix/Compiler/Core/Pretty/Base.hs b/src/Juvix/Compiler/Core/Pretty/Base.hs index 9d6a82c4d..f81018b08 100644 --- a/src/Juvix/Compiler/Core/Pretty/Base.hs +++ b/src/Juvix/Compiler/Core/Pretty/Base.hs @@ -39,6 +39,12 @@ instance PrettyCode BuiltinOp where OpIntMod -> return primMod OpIntLt -> return primLess OpIntLe -> return primLessEquals + OpFieldAdd -> return primFieldAdd + OpFieldSub -> return primFieldSub + OpFieldMul -> return primFieldMul + OpFieldDiv -> return primFieldDiv + OpFieldFromInt -> return primFieldFromInt + OpFieldToInt -> return primFieldToInt OpEq -> return primEquals OpShow -> return primShow OpStrConcat -> return primStrConcat @@ -64,6 +70,7 @@ instance PrettyCode Tag where instance PrettyCode Primitive where ppCode = \case PrimInteger _ -> return $ annotate (AnnKind KNameInductive) (pretty ("Int" :: String)) + PrimField -> return $ annotate (AnnKind KNameInductive) (pretty ("Field" :: String)) PrimBool _ -> return $ annotate (AnnKind KNameInductive) (pretty ("Bool" :: String)) PrimString -> return $ annotate (AnnKind KNameInductive) (pretty ("String" :: String)) @@ -88,11 +95,16 @@ instance PrettyCode ConstantValue where ppCode = \case ConstInteger int -> return $ annotate AnnLiteralInteger (pretty int) + ConstField fld -> + return $ annotate AnnLiteralInteger (pretty fld) ConstString txt -> return $ annotate AnnLiteralString (pretty (show txt :: String)) instance PrettyCode (Constant' i) where - ppCode Constant {..} = ppCode _constantValue + ppCode Constant {..} = case _constantValue of + ConstField fld -> + return $ annotate AnnLiteralInteger (pretty fld <> "F") + _ -> ppCode _constantValue instance (PrettyCode a, HasAtomicity a) => PrettyCode (App' i a) where ppCode App {..} = do @@ -695,6 +707,24 @@ kwUnnamedConstr = keyword Str.exclamation kwQuestion :: Doc Ann kwQuestion = keyword Str.questionMark +primFieldAdd :: Doc Ann +primFieldAdd = primitive Str.fadd + +primFieldSub :: Doc Ann +primFieldSub = primitive Str.fsub + +primFieldMul :: Doc Ann +primFieldMul = primitive Str.fmul + +primFieldDiv :: Doc Ann +primFieldDiv = primitive Str.fdiv + +primFieldFromInt :: Doc Ann +primFieldFromInt = primitive Str.itof + +primFieldToInt :: Doc Ann +primFieldToInt = primitive Str.ftoi + primLess :: Doc Ann primLess = primitive Str.less diff --git a/src/Juvix/Compiler/Core/Transformation.hs b/src/Juvix/Compiler/Core/Transformation.hs index 397e8c24a..396d8eef0 100644 --- a/src/Juvix/Compiler/Core/Transformation.hs +++ b/src/Juvix/Compiler/Core/Transformation.hs @@ -77,7 +77,7 @@ applyTransformations ts tbl = foldM (flip appTrans) tbl ts CheckExec -> mapError (JuvixError @CoreError) . checkExec CheckVampIR -> mapError (JuvixError @CoreError) . checkVampIR CheckAnoma -> mapError (JuvixError @CoreError) . checkAnoma - Normalize -> return . normalize + Normalize -> normalize LetFolding -> return . letFolding LambdaFolding -> return . lambdaFolding LetHoisting -> return . letHoisting diff --git a/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs b/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs index 1726d280e..a2a1cb2f6 100644 --- a/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs +++ b/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs @@ -32,6 +32,7 @@ computeNodeTypeInfo md = umapL go NCst Constant {..} -> case _constantValue of ConstInteger {} -> mkTypeInteger' + ConstField {} -> mkTypeField' ConstString {} -> mkTypeString' NApp {} -> let (fn, args) = unfoldApps' node @@ -48,6 +49,12 @@ computeNodeTypeInfo md = umapL go OpIntMod -> mkTypeInteger' OpIntLt -> mkTypeBool' OpIntLe -> mkTypeBool' + OpFieldAdd -> mkTypeField' + OpFieldSub -> mkTypeField' + OpFieldMul -> mkTypeField' + OpFieldDiv -> mkTypeField' + OpFieldFromInt -> mkTypeField' + OpFieldToInt -> mkTypeInteger' OpEq -> mkTypeBool' OpShow -> mkTypeString' OpStrConcat -> mkTypeString' diff --git a/src/Juvix/Compiler/Core/Transformation/ConvertBuiltinTypes.hs b/src/Juvix/Compiler/Core/Transformation/ConvertBuiltinTypes.hs index 67847765e..8f496beb5 100644 --- a/src/Juvix/Compiler/Core/Transformation/ConvertBuiltinTypes.hs +++ b/src/Juvix/Compiler/Core/Transformation/ConvertBuiltinTypes.hs @@ -18,6 +18,7 @@ convertNode md = umap go Just (BuiltinTypeInductive BuiltinNat) -> mkTypeInteger' Just (BuiltinTypeInductive BuiltinInt) -> mkTypeInteger' Just (BuiltinTypeAxiom BuiltinString) -> mkTypeString' + Just (BuiltinTypeAxiom BuiltinField) -> mkTypeField' _ -> node where ii = lookupInductiveInfo md _typeConstrSymbol diff --git a/src/Juvix/Compiler/Core/Transformation/Normalize.hs b/src/Juvix/Compiler/Core/Transformation/Normalize.hs index a33586966..d0848ddcd 100644 --- a/src/Juvix/Compiler/Core/Transformation/Normalize.hs +++ b/src/Juvix/Compiler/Core/Transformation/Normalize.hs @@ -2,14 +2,17 @@ module Juvix.Compiler.Core.Transformation.Normalize where import Data.HashMap.Strict qualified as HashMap import Juvix.Compiler.Core.Normalizer qualified as Normalizer +import Juvix.Compiler.Core.Options import Juvix.Compiler.Core.Transformation.Base -normalize :: Module -> Module -normalize md = - pruneInfoTable $ - set (moduleInfoTable . identContext) (HashMap.singleton sym node) $ - set (moduleInfoTable . infoIdentifiers) (HashMap.singleton sym ii) md +normalize :: (Member (Reader CoreOptions) r) => Module -> Sem r Module +normalize md = do + opts <- ask + let node = Normalizer.normalize (opts ^. optFieldSize) md (lookupIdentifierNode md sym) + return $ + pruneInfoTable $ + set (moduleInfoTable . identContext) (HashMap.singleton sym node) $ + set (moduleInfoTable . infoIdentifiers) (HashMap.singleton sym ii) md where sym = fromJust $ getInfoMain md - node = Normalizer.normalize md (lookupIdentifierNode md sym) ii = lookupIdentifierInfo md sym diff --git a/src/Juvix/Compiler/Core/Transformation/Optimize/ConstantFolding.hs b/src/Juvix/Compiler/Core/Transformation/Optimize/ConstantFolding.hs index f05751127..fc86c5804 100644 --- a/src/Juvix/Compiler/Core/Transformation/Optimize/ConstantFolding.hs +++ b/src/Juvix/Compiler/Core/Transformation/Optimize/ConstantFolding.hs @@ -5,10 +5,11 @@ import Juvix.Compiler.Core.Data.IdentDependencyInfo import Juvix.Compiler.Core.Evaluator import Juvix.Compiler.Core.Extra import Juvix.Compiler.Core.Info.FreeVarsInfo as Info +import Juvix.Compiler.Core.Options import Juvix.Compiler.Core.Transformation.Base -convertNode :: HashSet Symbol -> InfoTable -> Module -> Node -> Node -convertNode nonRecSyms tab md = umap go +convertNode :: CoreOptions -> HashSet Symbol -> InfoTable -> Module -> Node -> Node +convertNode opts nonRecSyms tab md = umap go where go :: Node -> Node go node = case node of @@ -54,24 +55,27 @@ convertNode nonRecSyms tab md = umap go _ -> isType' node doEval' :: Node -> Node - doEval' = removeClosures . geval opts stderr (tab ^. identContext) [] + doEval' = removeClosures . geval eopts stderr (tab ^. identContext) [] where - opts = + eopts = defaultEvalOptions { _evalOptionsNoFailure = True, - _evalOptionsSilent = True + _evalOptionsSilent = True, + _evalOptionsFieldSize = opts ^. optFieldSize } -constantFolding' :: HashSet Symbol -> InfoTable -> Module -> Module -constantFolding' nonRecSyms tab md = +constantFolding' :: CoreOptions -> HashSet Symbol -> InfoTable -> Module -> Module +constantFolding' opts nonRecSyms tab md = mapAllNodes ( removeInfo kFreeVarsInfo - . convertNode nonRecSyms tab md + . convertNode opts nonRecSyms tab md . computeFreeVarsInfo ) md -constantFolding :: Module -> Module -constantFolding md = constantFolding' (nonRecursiveIdents' tab) tab md +constantFolding :: (Member (Reader CoreOptions) r) => Module -> Sem r Module +constantFolding md = do + opts <- ask + return $ constantFolding' opts (nonRecursiveIdents' tab) tab md where tab = computeCombinedInfoTable md diff --git a/src/Juvix/Compiler/Core/Transformation/Optimize/Phase/Main.hs b/src/Juvix/Compiler/Core/Transformation/Optimize/Phase/Main.hs index 172babf0a..0c60f7fd4 100644 --- a/src/Juvix/Compiler/Core/Transformation/Optimize/Phase/Main.hs +++ b/src/Juvix/Compiler/Core/Transformation/Optimize/Phase/Main.hs @@ -16,7 +16,7 @@ import Juvix.Compiler.Core.Transformation.Optimize.SimplifyIfs import Juvix.Compiler.Core.Transformation.Optimize.SpecializeArgs optimize' :: CoreOptions -> Module -> Module -optimize' CoreOptions {..} md = +optimize' opts@CoreOptions {..} md = filterUnreachable . compose (4 * _optOptimizationLevel) @@ -40,7 +40,7 @@ optimize' CoreOptions {..} md = nonRecs = nonRecursiveIdents' tab doConstantFolding :: Module -> Module - doConstantFolding md' = constantFolding' nonRecs' tab' md' + doConstantFolding md' = constantFolding' opts nonRecs' tab' md' where tab' = computeCombinedInfoTable md' nonRecs' diff --git a/src/Juvix/Compiler/Core/Transformation/Optimize/SimplifyArithmetic.hs b/src/Juvix/Compiler/Core/Transformation/Optimize/SimplifyArithmetic.hs index c1d4d79f4..b75467650 100644 --- a/src/Juvix/Compiler/Core/Transformation/Optimize/SimplifyArithmetic.hs +++ b/src/Juvix/Compiler/Core/Transformation/Optimize/SimplifyArithmetic.hs @@ -2,6 +2,7 @@ module Juvix.Compiler.Core.Transformation.Optimize.SimplifyArithmetic (simplifyA import Juvix.Compiler.Core.Extra import Juvix.Compiler.Core.Transformation.Base +import Juvix.Data.Field convertNode :: Node -> Node convertNode = dmap go @@ -58,6 +59,67 @@ convertNode = dmap go | _builtinAppOp == OpIntMul, [NCst (Constant _ (ConstInteger 1)), x] <- _builtinAppArgs -> x + NBlt BuiltinApp {..} + | _builtinAppOp == OpFieldAdd, + [NBlt blt', n] <- _builtinAppArgs, + blt' ^. builtinAppOp == OpFieldSub, + [x, m] <- blt' ^. builtinAppArgs, + m == n -> + x + NBlt BuiltinApp {..} + | _builtinAppOp == OpFieldSub, + [NBlt blt', n] <- _builtinAppArgs, + blt' ^. builtinAppOp == OpFieldAdd, + [x, m] <- blt' ^. builtinAppArgs -> + if + | m == n -> + x + | x == n -> + m + | otherwise -> + node + NBlt BuiltinApp {..} + | _builtinAppOp == OpFieldAdd, + [n, NBlt blt'] <- _builtinAppArgs, + blt' ^. builtinAppOp == OpFieldSub, + [x, m] <- blt' ^. builtinAppArgs, + m == n -> + x + NBlt BuiltinApp {..} + | _builtinAppOp == OpFieldAdd || _builtinAppOp == OpFieldSub, + [x, NCst (Constant _ (ConstField f))] <- _builtinAppArgs, + fieldToInteger f == 0 -> + x + NBlt BuiltinApp {..} + | _builtinAppOp == OpFieldAdd, + [NCst (Constant _ (ConstField f)), x] <- _builtinAppArgs, + fieldToInteger f == 0 -> + x + NBlt BuiltinApp {..} + | _builtinAppOp == OpFieldMul, + [_, c@(NCst (Constant _ (ConstField f)))] <- _builtinAppArgs, + fieldToInteger f == 0 -> + c + NBlt BuiltinApp {..} + | _builtinAppOp == OpFieldMul, + [c@(NCst (Constant _ (ConstField f))), _] <- _builtinAppArgs, + fieldToInteger f == 0 -> + c + NBlt BuiltinApp {..} + | _builtinAppOp == OpFieldMul, + [x, NCst (Constant _ (ConstField f))] <- _builtinAppArgs, + fieldToInteger f == 1 -> + x + NBlt BuiltinApp {..} + | _builtinAppOp == OpFieldMul, + [NCst (Constant _ (ConstField f)), x] <- _builtinAppArgs, + fieldToInteger f == 1 -> + x + NBlt BuiltinApp {..} + | _builtinAppOp == OpFieldDiv, + [x, NCst (Constant _ (ConstField f))] <- _builtinAppArgs, + fieldToInteger f == 1 -> + x _ -> node simplifyArithmetic :: Module -> Module diff --git a/src/Juvix/Compiler/Core/Translation/FromInternal.hs b/src/Juvix/Compiler/Core/Translation/FromInternal.hs index a6bb82b3a..b355a49d8 100644 --- a/src/Juvix/Compiler/Core/Translation/FromInternal.hs +++ b/src/Juvix/Compiler/Core/Translation/FromInternal.hs @@ -559,6 +559,7 @@ goAxiomInductive a = whenJust (a ^. Internal.axiomBuiltin) builtinInductive Internal.BuiltinBoolPrint -> return () Internal.BuiltinIOSequence -> return () Internal.BuiltinIOReadline -> return () + Internal.BuiltinField -> registerInductiveAxiom (Just BuiltinField) [] Internal.BuiltinString -> registerInductiveAxiom (Just BuiltinString) [] Internal.BuiltinIO -> registerInductiveAxiom (Just BuiltinIO) builtinIOConstrs Internal.BuiltinTrace -> return () @@ -569,6 +570,13 @@ goAxiomInductive a = whenJust (a ^. Internal.axiomBuiltin) builtinInductive Internal.BuiltinNatToString -> return () Internal.BuiltinIntToString -> return () Internal.BuiltinIntPrint -> return () + Internal.BuiltinFieldEq -> return () + Internal.BuiltinFieldAdd -> return () + Internal.BuiltinFieldSub -> return () + Internal.BuiltinFieldMul -> return () + Internal.BuiltinFieldDiv -> return () + Internal.BuiltinFieldFromInt -> return () + Internal.BuiltinFieldToNat -> return () registerInductiveAxiom :: Maybe BuiltinAxiom -> [(Tag, Text, Type -> Type, Maybe BuiltinConstructor)] -> Sem r () registerInductiveAxiom ax ctrs = do @@ -649,6 +657,21 @@ goAxiomDef a = maybe goAxiomNotBuiltin builtinBody (a ^. Internal.axiomBuiltin) natName <- getNatName natSym <- getNatSymbol registerAxiomDef (mkLambda' (mkTypeConstr (setInfoName natName mempty) natSym []) (mkBuiltinApp' OpShow [mkVar' 0])) + Internal.BuiltinField -> return () + Internal.BuiltinFieldEq -> + registerAxiomDef (mkLambda' mkTypeField' (mkLambda' mkTypeField' (mkBuiltinApp' OpEq [mkVar' 1, mkVar' 0]))) + Internal.BuiltinFieldAdd -> + registerAxiomDef (mkLambda' mkTypeField' (mkLambda' mkTypeField' (mkBuiltinApp' OpFieldAdd [mkVar' 1, mkVar' 0]))) + Internal.BuiltinFieldSub -> + registerAxiomDef (mkLambda' mkTypeField' (mkLambda' mkTypeField' (mkBuiltinApp' OpFieldSub [mkVar' 1, mkVar' 0]))) + Internal.BuiltinFieldMul -> + registerAxiomDef (mkLambda' mkTypeField' (mkLambda' mkTypeField' (mkBuiltinApp' OpFieldMul [mkVar' 1, mkVar' 0]))) + Internal.BuiltinFieldDiv -> + registerAxiomDef (mkLambda' mkTypeField' (mkLambda' mkTypeField' (mkBuiltinApp' OpFieldDiv [mkVar' 1, mkVar' 0]))) + Internal.BuiltinFieldFromInt -> + registerAxiomDef (mkLambda' mkTypeInteger' (mkBuiltinApp' OpFieldFromInt [mkVar' 0])) + Internal.BuiltinFieldToNat -> + registerAxiomDef (mkLambda' mkTypeField' (mkBuiltinApp' OpFieldToInt [mkVar' 0])) Internal.BuiltinString -> return () Internal.BuiltinIO -> return () Internal.BuiltinTrace -> return () @@ -1025,6 +1048,18 @@ goApplication a = do Just Internal.BuiltinFail -> app Just Internal.BuiltinIntToString -> app Just Internal.BuiltinIntPrint -> app + Just Internal.BuiltinField -> app + Just Internal.BuiltinFieldEq -> app + Just Internal.BuiltinFieldAdd -> app + Just Internal.BuiltinFieldSub -> app + Just Internal.BuiltinFieldMul -> app + Just Internal.BuiltinFieldDiv -> app + Just Internal.BuiltinFieldFromInt -> do + as <- exprArgs + case as of + [x] -> return $ mkBuiltinApp' OpFieldFromInt [x] + _ -> app + Just Internal.BuiltinFieldToNat -> 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 cab92c5dd..c021fa78a 100644 --- a/src/Juvix/Compiler/Core/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Core/Translation/FromSource.hs @@ -17,6 +17,7 @@ import Juvix.Compiler.Core.Info.LocationInfo as LocationInfo import Juvix.Compiler.Core.Info.NameInfo as NameInfo import Juvix.Compiler.Core.Transformation.Eta import Juvix.Compiler.Core.Translation.FromSource.Lexer +import Juvix.Data.Field import Juvix.Extra.Strings qualified as Str import Juvix.Parser.Error import Text.Megaparsec qualified as P @@ -559,6 +560,10 @@ builtinAppExpr varsNum vars = do <|> (kw kwDiv $> OpIntDiv) <|> (kw kwMul $> OpIntMul) <|> (kw kwMod $> OpIntMod) + <|> (kw kwFieldAdd $> OpFieldAdd) + <|> (kw kwFieldSub $> OpFieldSub) + <|> (kw kwFieldMul $> OpFieldMul) + <|> (kw kwFieldDiv $> OpFieldDiv) <|> (kw kwShow $> OpShow) <|> (kw kwStrConcat $> OpStrConcat) <|> (kw kwStrToInt $> OpStrToInt) @@ -583,7 +588,8 @@ atom :: HashMap Text Level -> ParsecS r Node atom varsNum vars = - exprConstInt + exprConstField + <|> exprConstInt <|> exprConstString <|> exprUniverse <|> exprDynamic @@ -609,6 +615,11 @@ exprConstString = P.try $ do (s, i) <- string return $ mkConstant (Info.singleton (LocationInfo i)) (ConstString s) +exprConstField :: ParsecS r Node +exprConstField = P.try $ do + (n, i) <- field + return $ mkConstant (Info.singleton (LocationInfo i)) (ConstField (fieldFromInteger defaultFieldSize n)) + exprUniverse :: ParsecS r Type exprUniverse = do kw kwType @@ -1090,6 +1101,7 @@ exprNamed varsNum vars = do (txt, i) <- identifierL case txt of "Int" -> return mkTypeInteger' + "Field" -> return mkTypeField' "String" -> return mkTypeString' _ -> case HashMap.lookup txt vars of diff --git a/src/Juvix/Compiler/Core/Translation/FromSource/Lexer.hs b/src/Juvix/Compiler/Core/Translation/FromSource/Lexer.hs index bd3fd6965..8b6a9ed04 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' decimal :: (Num n) => ParsecS r (n, Interval) decimal = lexemeInterval L.decimal +field :: ParsecS r (Integer, Interval) +field = lexemeInterval field' + integer :: ParsecS r (Integer, Interval) integer = integer' decimal diff --git a/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs b/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs index dfc4a8882..fd2c5d161 100644 --- a/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs +++ b/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs @@ -9,13 +9,14 @@ import Juvix.Compiler.Core.Info.NameInfo import Juvix.Compiler.Core.Language.Stripped qualified as Stripped import Juvix.Compiler.Core.Pretty -fromCore :: InfoTable -> Stripped.InfoTable -fromCore tab = +fromCore :: Natural -> InfoTable -> Stripped.InfoTable +fromCore fsize tab = Stripped.InfoTable { _infoMain = tab ^. infoMain, _infoFunctions = fmap (translateFunctionInfo tab) (tab' ^. infoIdentifiers), _infoInductives = fmap translateInductiveInfo (tab' ^. infoInductives), - _infoConstructors = fmap translateConstructorInfo (tab' ^. infoConstructors) + _infoConstructors = fmap translateConstructorInfo (tab' ^. infoConstructors), + _infoFieldSize = fsize } where tab' = @@ -78,6 +79,14 @@ fromCore tab = BuiltinStringToNat -> False BuiltinBoolPrint -> False BuiltinString -> False + BuiltinField -> False + BuiltinFieldEq -> False + BuiltinFieldAdd -> False + BuiltinFieldSub -> False + BuiltinFieldMul -> False + BuiltinFieldDiv -> False + BuiltinFieldFromInt -> False + BuiltinFieldToNat -> False BuiltinIOSequence -> False BuiltinIOReadline -> False BuiltinTrace -> False diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs index 445f6a62f..fd4a45ddf 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs @@ -574,6 +574,14 @@ registerBuiltinAxiom d = \case BuiltinStringConcat -> registerStringConcat d BuiltinStringEq -> registerStringEq d BuiltinStringToNat -> registerStringToNat d + BuiltinField -> registerField d + BuiltinFieldEq -> registerFieldEq d + BuiltinFieldAdd -> registerFieldAdd d + BuiltinFieldSub -> registerFieldSub d + BuiltinFieldMul -> registerFieldMul d + BuiltinFieldDiv -> registerFieldDiv d + BuiltinFieldFromInt -> registerFieldFromInt d + BuiltinFieldToNat -> registerFieldToNat d BuiltinBoolPrint -> registerBoolPrint d BuiltinTrace -> registerTrace d BuiltinFail -> registerFail d diff --git a/src/Juvix/Compiler/Nockma/Translation/FromTree.hs b/src/Juvix/Compiler/Nockma/Translation/FromTree.hs index 068d13850..5b063a3f2 100644 --- a/src/Juvix/Compiler/Nockma/Translation/FromTree.hs +++ b/src/Juvix/Compiler/Nockma/Translation/FromTree.hs @@ -321,6 +321,7 @@ compile = \case Tree.ConstString {} -> stringsErr Tree.ConstUnit -> OpQuote # constUnit Tree.ConstVoid -> OpQuote # constVoid + Tree.ConstField {} -> fieldErr goSave :: Tree.NodeSave -> Sem r (Term Natural) goSave Tree.NodeSave {..} = do @@ -367,6 +368,8 @@ compile = \case Tree.OpArgsNum -> let getF f = getClosureField f arg in sub (getF ClosureTotalArgsNum) (getF ClosureArgsNum) + Tree.OpIntToField -> fieldErr + Tree.OpFieldToInt -> fieldErr goTrace :: Term Natural -> Sem r (Term Natural) goTrace arg = do @@ -395,6 +398,10 @@ compile = \case Tree.OpIntLe -> return (callStdlib StdlibLe args) Tree.OpEq -> testEq _nodeBinopArg1 _nodeBinopArg2 Tree.OpStrConcat -> stringsErr + Tree.OpFieldAdd -> fieldErr + Tree.OpFieldSub -> fieldErr + Tree.OpFieldMul -> fieldErr + Tree.OpFieldDiv -> fieldErr goAllocClosure :: Tree.NodeAllocClosure -> Sem r (Term Natural) goAllocClosure Tree.NodeAllocClosure {..} = do @@ -554,6 +561,9 @@ unsupported thing = error ("The Nockma backend does not support " <> thing) stringsErr :: a stringsErr = unsupported "strings" +fieldErr :: a +fieldErr = unsupported "the field type" + -- | Computes a - b sub :: Term Natural -> Term Natural -> Term Natural sub a b = callStdlib StdlibSub [a, b] diff --git a/src/Juvix/Compiler/Pipeline.hs b/src/Juvix/Compiler/Pipeline.hs index 856a1301a..47a12957b 100644 --- a/src/Juvix/Compiler/Pipeline.hs +++ b/src/Juvix/Compiler/Pipeline.hs @@ -130,19 +130,16 @@ upToCoreTypecheck :: upToCoreTypecheck = upToCore >>= \r -> Core.toTypechecked (r ^. Core.coreResultModule) >>= \md -> return r {Core._coreResultModule = md} --------------------------------------------------------------------------------- --- Workflows from stripped Core --------------------------------------------------------------------------------- - -strippedCoreToTree :: Core.Module -> Sem r Tree.InfoTable -strippedCoreToTree = return . Tree.fromCore . Stripped.fromCore . Core.computeCombinedInfoTable - -------------------------------------------------------------------------------- -- Workflows from stored Core -------------------------------------------------------------------------------- storedCoreToTree :: (Members '[Error JuvixError, Reader EntryPoint] r) => Core.TransformationId -> Core.Module -> Sem r Tree.InfoTable -storedCoreToTree checkId = Core.toStripped checkId >=> strippedCoreToTree +storedCoreToTree checkId md = do + fsize <- asks (^. entryPointFieldSize) + Core.toStripped checkId + >=> return . Tree.fromCore . Stripped.fromCore fsize . Core.computeCombinedInfoTable + $ md storedCoreToAnoma :: (Members '[Error JuvixError, Reader EntryPoint] r) => Core.Module -> Sem r (Nockma.Cell Natural) storedCoreToAnoma = storedCoreToTree Core.CheckAnoma >=> treeToAnoma diff --git a/src/Juvix/Compiler/Pipeline/Driver.hs b/src/Juvix/Compiler/Pipeline/Driver.hs index 68c16c4be..437aca246 100644 --- a/src/Juvix/Compiler/Pipeline/Driver.hs +++ b/src/Juvix/Compiler/Pipeline/Driver.hs @@ -206,7 +206,8 @@ processModule' (EntryIndex entry) = do case m of Just info | info ^. Store.moduleInfoSHA256 == sha256 - && info ^. Store.moduleInfoOptions == opts -> do + && info ^. Store.moduleInfoOptions == opts + && info ^. Store.moduleInfoFieldSize == entry ^. entryPointFieldSize -> do (changed, mtab) <- processImports'' entry (info ^. Store.moduleInfoImports) -- We need to check whether any of the recursive imports is fragile, -- not only the direct ones, because identifiers may be re-exported @@ -247,7 +248,8 @@ processModule'' sha256 entry = over pipelineResult mkModuleInfo <$> processFileT _moduleInfoImports = map (^. importModulePath) $ scoperResult ^. Scoper.resultParserResult . Parser.resultParserState . parserStateImports, _moduleInfoOptions = StoredOptions.fromEntryPoint entry, _moduleInfoFragile = Core.moduleIsFragile _coreResultModule, - _moduleInfoSHA256 = sha256 + _moduleInfoSHA256 = sha256, + _moduleInfoFieldSize = entry ^. entryPointFieldSize } where scoperResult = _coreResultInternalTypedResult ^. InternalTyped.resultInternal . Internal.resultScoper diff --git a/src/Juvix/Compiler/Pipeline/EntryPoint.hs b/src/Juvix/Compiler/Pipeline/EntryPoint.hs index 775b3ab04..81954f6f5 100644 --- a/src/Juvix/Compiler/Pipeline/EntryPoint.hs +++ b/src/Juvix/Compiler/Pipeline/EntryPoint.hs @@ -7,6 +7,7 @@ where import Juvix.Compiler.Backend import Juvix.Compiler.Pipeline.Package.Base import Juvix.Compiler.Pipeline.Root.Base +import Juvix.Data.Field import Juvix.Prelude -- | An option specifying how symbols should be pruned in the Internal to Core translation @@ -38,7 +39,8 @@ data EntryPoint = EntryPoint _entryPointGenericOptions :: GenericOptions, _entryPointModulePath :: Maybe (Path Abs File), _entryPointSymbolPruningMode :: SymbolPruningMode, - _entryPointOffline :: Bool + _entryPointOffline :: Bool, + _entryPointFieldSize :: Natural } deriving stock (Eq, Show) @@ -72,7 +74,8 @@ defaultEntryPointNoFile pkg root = _entryPointInliningDepth = defaultInliningDepth, _entryPointModulePath = Nothing, _entryPointSymbolPruningMode = FilterUnreachable, - _entryPointOffline = False + _entryPointOffline = False, + _entryPointFieldSize = defaultFieldSize } defaultUnrollLimit :: Int diff --git a/src/Juvix/Compiler/Pipeline/Package/Loader/EvalEff/IO.hs b/src/Juvix/Compiler/Pipeline/Package/Loader/EvalEff/IO.hs index 5c4aa27f5..bb172926a 100644 --- a/src/Juvix/Compiler/Pipeline/Package/Loader/EvalEff/IO.hs +++ b/src/Juvix/Compiler/Pipeline/Package/Loader/EvalEff/IO.hs @@ -71,7 +71,7 @@ runEvalFileEffIO = interpretScopedAs allocator handler evalNode :: Node -> Sem r Node evalNode n = do - n' <- doEval False packageLoc tab n + n' <- doEval Nothing False packageLoc tab n case n' of Left e -> do throw diff --git a/src/Juvix/Compiler/Reg/Interpreter.hs b/src/Juvix/Compiler/Reg/Interpreter.hs index ebb380a31..0e303e375 100644 --- a/src/Juvix/Compiler/Reg/Interpreter.hs +++ b/src/Juvix/Compiler/Reg/Interpreter.hs @@ -68,6 +68,7 @@ runFunction hout infoTable args0 info0 = do readConst :: Constant -> Val readConst = \case ConstInt i -> ValInteger i + ConstField f -> ValField f ConstBool b -> ValBool b ConstString s -> ValString s ConstUnit -> ValUnit diff --git a/src/Juvix/Compiler/Reg/Keywords.hs b/src/Juvix/Compiler/Reg/Keywords.hs index e5b9f401d..0f2310127 100644 --- a/src/Juvix/Compiler/Reg/Keywords.hs +++ b/src/Juvix/Compiler/Reg/Keywords.hs @@ -6,7 +6,43 @@ module Juvix.Compiler.Reg.Keywords where import Juvix.Compiler.Tree.Keywords.Base -import Juvix.Data.Keyword.All (kwAdd_, kwAlloc, kwArgsNum, kwAtoi, kwBr, kwCAlloc, kwCCall, kwCCallTail, kwCExtend, kwCall, kwCallTail, kwCase, kwDefault, kwDiv_, kwDollar, kwDump, kwEq, kwEq_, kwFail, kwLe_, kwLive, kwLt_, kwMod_, kwMul_, kwNop, kwPrealloc, kwRet, kwShow, kwStrcat, kwSub_, kwTrace) +import Juvix.Data.Keyword.All + ( kwAdd_, + kwAlloc, + kwArgsNum, + kwAtoi, + kwBr, + kwCAlloc, + kwCCall, + kwCCallTail, + kwCExtend, + kwCall, + kwCallTail, + kwCase, + kwDefault, + kwDiv_, + kwDollar, + kwDump, + kwEq, + kwEq_, + kwFail, + kwFieldAdd, + kwFieldDiv, + kwFieldMul, + kwFieldSub, + kwLe_, + kwLive, + kwLt_, + kwMod_, + kwMul_, + kwNop, + kwPrealloc, + kwRet, + kwShow, + kwStrcat, + kwSub_, + kwTrace, + ) import Juvix.Prelude allKeywordStrings :: HashSet Text @@ -24,6 +60,10 @@ allKeywords = kwLt_, kwLe_, kwEq_, + kwFieldAdd, + kwFieldDiv, + kwFieldMul, + kwFieldSub, kwStrcat, kwEq, kwShow, diff --git a/src/Juvix/Compiler/Reg/Translation/FromAsm.hs b/src/Juvix/Compiler/Reg/Translation/FromAsm.hs index 268d3b358..a1b75b325 100644 --- a/src/Juvix/Compiler/Reg/Translation/FromAsm.hs +++ b/src/Juvix/Compiler/Reg/Translation/FromAsm.hs @@ -14,7 +14,8 @@ fromAsm tab = { _infoFunctions = HashMap.map convertFun (tab ^. Asm.infoFunctions), _infoConstrs = HashMap.map convertConstr (tab ^. Asm.infoConstrs), _infoInductives = HashMap.map convertInductive (tab ^. Asm.infoInductives), - _infoMainFunction = tab ^. Asm.infoMainFunction + _infoMainFunction = tab ^. Asm.infoMainFunction, + _infoFieldSize = tab ^. Asm.infoFieldSize } where convertFun :: Asm.FunctionInfo -> FunctionInfo diff --git a/src/Juvix/Compiler/Reg/Translation/FromSource.hs b/src/Juvix/Compiler/Reg/Translation/FromSource.hs index 25f3fbc8e..d3c333311 100644 --- a/src/Juvix/Compiler/Reg/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Reg/Translation/FromSource.hs @@ -96,6 +96,10 @@ instrBinop vref = <|> parseBinaryOp kwLt_ OpIntLt vref <|> parseBinaryOp kwLe_ OpIntLe vref <|> parseBinaryOp kwEq_ OpEq vref + <|> parseBinaryOp kwFieldAdd OpFieldAdd vref + <|> parseBinaryOp kwFieldSub OpFieldSub vref + <|> parseBinaryOp kwFieldMul OpFieldMul vref + <|> parseBinaryOp kwFieldDiv OpFieldDiv vref <|> parseBinaryOp kwStrcat OpStrConcat vref parseBinaryOp :: diff --git a/src/Juvix/Compiler/Store/Language.hs b/src/Juvix/Compiler/Store/Language.hs index b3668302b..1e5c0279d 100644 --- a/src/Juvix/Compiler/Store/Language.hs +++ b/src/Juvix/Compiler/Store/Language.hs @@ -17,7 +17,8 @@ data ModuleInfo = ModuleInfo -- | True if any module depending on this module requires recompilation -- whenever this module is changed _moduleInfoFragile :: Bool, - _moduleInfoSHA256 :: Text + _moduleInfoSHA256 :: Text, + _moduleInfoFieldSize :: Natural } deriving stock (Generic) diff --git a/src/Juvix/Compiler/Tree/Data/InfoTable/Base.hs b/src/Juvix/Compiler/Tree/Data/InfoTable/Base.hs index cbf57bbef..b8137695a 100644 --- a/src/Juvix/Compiler/Tree/Data/InfoTable/Base.hs +++ b/src/Juvix/Compiler/Tree/Data/InfoTable/Base.hs @@ -9,12 +9,14 @@ import Data.HashMap.Strict qualified as HashMap import Juvix.Compiler.Tree.Language import Juvix.Compiler.Tree.Language.Rep import Juvix.Compiler.Tree.Language.Type +import Juvix.Data.Field data InfoTable' code extra = InfoTable { _infoFunctions :: HashMap Symbol (FunctionInfo' code extra), _infoConstrs :: HashMap Tag ConstructorInfo, _infoInductives :: HashMap Symbol InductiveInfo, - _infoMainFunction :: Maybe Symbol + _infoMainFunction :: Maybe Symbol, + _infoFieldSize :: Natural } data FunctionInfo' code extra = FunctionInfo @@ -70,7 +72,8 @@ emptyInfoTable = { _infoFunctions = mempty, _infoConstrs = mempty, _infoInductives = mempty, - _infoMainFunction = Nothing + _infoMainFunction = Nothing, + _infoFieldSize = defaultFieldSize } lookupFunInfo :: InfoTable' a e -> Symbol -> FunctionInfo' a e diff --git a/src/Juvix/Compiler/Tree/Evaluator.hs b/src/Juvix/Compiler/Tree/Evaluator.hs index 95f5948c7..952b6e337 100644 --- a/src/Juvix/Compiler/Tree/Evaluator.hs +++ b/src/Juvix/Compiler/Tree/Evaluator.hs @@ -83,6 +83,7 @@ hEval hout tab = eval' [] mempty goConstant :: NodeConstant -> Value goConstant NodeConstant {..} = case _nodeConstant of ConstInt i -> ValInteger i + ConstField f -> ValField f ConstBool b -> ValBool b ConstString s -> ValString s ConstUnit -> ValUnit @@ -215,6 +216,7 @@ hEval hout tab = eval' [] mempty valueToNode :: Value -> Node valueToNode = \case ValInteger i -> mkConst $ ConstInt i + ValField f -> mkConst $ ConstField f ValBool b -> mkConst $ ConstBool b ValString s -> mkConst $ ConstString s ValUnit -> mkConst ConstUnit diff --git a/src/Juvix/Compiler/Tree/Evaluator/Builtins.hs b/src/Juvix/Compiler/Tree/Evaluator/Builtins.hs index 6643e1134..71e1af8ef 100644 --- a/src/Juvix/Compiler/Tree/Evaluator/Builtins.hs +++ b/src/Juvix/Compiler/Tree/Evaluator/Builtins.hs @@ -4,6 +4,7 @@ import Juvix.Compiler.Tree.Data.InfoTable.Base import Juvix.Compiler.Tree.Language.Builtins import Juvix.Compiler.Tree.Language.Value import Juvix.Compiler.Tree.Pretty.Base +import Juvix.Data.Field import Juvix.Data.PPOutput import Juvix.Prelude import Text.Read qualified as T @@ -23,6 +24,13 @@ evalBinop op arg1 arg2 = case op of | otherwise -> goIntBinop rem arg1 arg2 OpIntLe -> goIntCmpBinop (<=) arg1 arg2 OpIntLt -> goIntCmpBinop (<) arg1 arg2 + OpFieldAdd -> goFieldBinop fieldAdd arg1 arg2 + OpFieldSub -> goFieldBinop fieldSub arg1 arg2 + OpFieldMul -> goFieldBinop fieldMul arg1 arg2 + OpFieldDiv -> case arg2 of + ValField arg2' + | fieldToInteger arg2' == 0 -> Left "division by zero" + _ -> goFieldBinop fieldDiv arg1 arg2 OpEq | arg1 == arg2 -> Right $ ValBool True | otherwise -> Right $ ValBool False @@ -38,6 +46,11 @@ evalBinop op arg1 arg2 = case op of (ValInteger i1, ValInteger i2) -> Right $ ValBool (f i1 i2) _ -> Left "expected two integer arguments" + goFieldBinop :: (FField -> FField -> FField) -> Value -> Value -> Either ErrorMsg Value + goFieldBinop f v1 v2 = case (v1, v2) of + (ValField i1, ValField i2) -> Right $ ValField (f i1 i2) + _ -> Left "expected two field elements as arguments" + goStrConcat :: Value -> Value -> Either ErrorMsg Value goStrConcat v1 v2 = case (v1, v2) of (ValString s1, ValString s2) -> Right $ ValString (s1 <> s2) @@ -47,6 +60,8 @@ evalUnop :: InfoTable' t e -> UnaryOp -> Value -> Either ErrorMsg Value evalUnop tab op v = case op of OpShow -> Right $ ValString (printValue tab v) OpStrToInt -> goStringUnop strToInt v + OpFieldToInt -> goFieldToInt v + OpIntToField -> goIntToField v OpArgsNum -> goArgsNum v where strToInt :: Text -> Either ErrorMsg Value @@ -71,6 +86,20 @@ evalUnop tab op v = case op of _ -> Left "expected a closure" + goFieldToInt :: Value -> Either ErrorMsg Value + goFieldToInt = \case + ValField f -> + Right $ ValInteger $ fieldToInteger f + _ -> + Left "expected a field element" + + goIntToField :: Value -> Either ErrorMsg Value + goIntToField = \case + ValInteger i -> + Right $ ValField $ fieldFromInteger (tab ^. infoFieldSize) i + _ -> + Left "expected an integer" + printValue :: InfoTable' t e -> Value -> Text printValue tab = \case ValString s -> s diff --git a/src/Juvix/Compiler/Tree/EvaluatorEff.hs b/src/Juvix/Compiler/Tree/EvaluatorEff.hs index 6d1ed1541..6eb7a460d 100644 --- a/src/Juvix/Compiler/Tree/EvaluatorEff.hs +++ b/src/Juvix/Compiler/Tree/EvaluatorEff.hs @@ -79,6 +79,7 @@ eval tab = E.runReader emptyEvalCtx . eval' goConstant :: NodeConstant -> Value goConstant NodeConstant {..} = case _nodeConstant of ConstInt i -> ValInteger i + ConstField f -> ValField f ConstBool b -> ValBool b ConstString s -> ValString s ConstUnit -> ValUnit diff --git a/src/Juvix/Compiler/Tree/EvaluatorSem.hs b/src/Juvix/Compiler/Tree/EvaluatorSem.hs index 7d9d96ce7..2831f70b1 100644 --- a/src/Juvix/Compiler/Tree/EvaluatorSem.hs +++ b/src/Juvix/Compiler/Tree/EvaluatorSem.hs @@ -77,6 +77,7 @@ eval tab = runReader emptyEvalCtx . eval' goConstant :: NodeConstant -> Value goConstant NodeConstant {..} = case _nodeConstant of ConstInt i -> ValInteger i + ConstField f -> ValField f ConstBool b -> ValBool b ConstString s -> ValString s ConstUnit -> ValUnit diff --git a/src/Juvix/Compiler/Tree/Extra/Type.hs b/src/Juvix/Compiler/Tree/Extra/Type.hs index f3382f12d..2425f0d2e 100644 --- a/src/Juvix/Compiler/Tree/Extra/Type.hs +++ b/src/Juvix/Compiler/Tree/Extra/Type.hs @@ -76,6 +76,7 @@ isSubtype ty1 ty2 = case (ty1, ty2) of checkBounds cmp (Just x) (Just y) = cmp x y (TyBool {}, TyBool {}) -> True (TyString, TyString) -> True + (TyField, TyField) -> True (TyUnit, TyUnit) -> True (TyVoid, TyVoid) -> True (TyInductive {}, TyInductive {}) -> ty1 == ty2 @@ -87,6 +88,8 @@ isSubtype ty1 ty2 = case (ty1, ty2) of (_, TyInteger {}) -> False (TyString, _) -> False (_, TyString) -> False + (TyField, _) -> False + (_, TyField) -> False (TyBool {}, _) -> False (_, TyBool {}) -> False (TyFun {}, _) -> False @@ -142,6 +145,7 @@ unifyTypes ty1 ty2 = case (ty1, ty2) of (TyBool {}, TyBool {}) | ty1 == ty2 -> return ty1 (TyString, TyString) -> return TyString + (TyField, TyField) -> return TyField (TyUnit, TyUnit) -> return TyUnit (TyVoid, TyVoid) -> return TyVoid (TyInductive {}, TyInductive {}) @@ -154,6 +158,8 @@ unifyTypes ty1 ty2 = case (ty1, ty2) of (_, TyInteger {}) -> err (TyString, _) -> err (_, TyString) -> err + (TyField, _) -> err + (_, TyField) -> err (TyBool {}, _) -> err (_, TyBool {}) -> err (TyFun {}, _) -> err diff --git a/src/Juvix/Compiler/Tree/Keywords.hs b/src/Juvix/Compiler/Tree/Keywords.hs index 0c757d85d..f965bd6aa 100644 --- a/src/Juvix/Compiler/Tree/Keywords.hs +++ b/src/Juvix/Compiler/Tree/Keywords.hs @@ -20,6 +20,10 @@ import Juvix.Data.Keyword.All kwDiv_, kwEq_, kwFail, + kwFieldAdd, + kwFieldDiv, + kwFieldMul, + kwFieldSub, kwLe_, kwLt_, kwMod_, @@ -45,6 +49,10 @@ allKeywords = kwDiv_, kwLt_, kwLe_, + kwFieldAdd, + kwFieldSub, + kwFieldMul, + kwFieldDiv, kwSeq_, kwEq_, kwStrcat, diff --git a/src/Juvix/Compiler/Tree/Language/Base.hs b/src/Juvix/Compiler/Tree/Language/Base.hs index 602661937..f434cc320 100644 --- a/src/Juvix/Compiler/Tree/Language/Base.hs +++ b/src/Juvix/Compiler/Tree/Language/Base.hs @@ -5,6 +5,7 @@ module Juvix.Compiler.Tree.Language.Base where import Juvix.Compiler.Core.Language.Base +import Juvix.Data.Field -- | Offset of a data field or an argument type Offset = Int @@ -14,6 +15,7 @@ data Constant = ConstInt Integer | ConstBool Bool | ConstString Text + | ConstField FField | ConstUnit | ConstVoid deriving stock (Eq) diff --git a/src/Juvix/Compiler/Tree/Language/Builtins.hs b/src/Juvix/Compiler/Tree/Language/Builtins.hs index eb3ebd57d..54f84f276 100644 --- a/src/Juvix/Compiler/Tree/Language/Builtins.hs +++ b/src/Juvix/Compiler/Tree/Language/Builtins.hs @@ -10,6 +10,10 @@ data BinaryOp | OpIntMod | OpIntLt | OpIntLe + | OpFieldAdd + | OpFieldSub + | OpFieldMul + | OpFieldDiv | OpEq | OpStrConcat deriving stock (Eq) @@ -19,6 +23,10 @@ data UnaryOp OpShow | -- | Convert a string to an integer. JV* opcode: `atoi`. OpStrToInt + | -- | Convert an integer to a field element. JV* opcode: `itof`. + OpIntToField + | -- | Convert a field element to an integer. JV* opcode: `ftoi`. + OpFieldToInt | -- | Compute the number of expected arguments for the given closure. JV* -- opcode: `argsnum`. OpArgsNum diff --git a/src/Juvix/Compiler/Tree/Language/Type.hs b/src/Juvix/Compiler/Tree/Language/Type.hs index 37bd52437..358dd3c26 100644 --- a/src/Juvix/Compiler/Tree/Language/Type.hs +++ b/src/Juvix/Compiler/Tree/Language/Type.hs @@ -7,6 +7,7 @@ data Type | TyInteger TypeInteger | TyBool TypeBool | TyString + | TyField | TyUnit | TyVoid | TyInductive TypeInductive @@ -77,6 +78,7 @@ instance HasAtomicity Type where TyInteger x -> atomicity x TyBool x -> atomicity x TyString -> Atom + TyField -> Atom TyUnit -> Atom TyVoid -> Atom TyInductive x -> atomicity x diff --git a/src/Juvix/Compiler/Tree/Language/Value.hs b/src/Juvix/Compiler/Tree/Language/Value.hs index 1ca1310d0..601d6e303 100644 --- a/src/Juvix/Compiler/Tree/Language/Value.hs +++ b/src/Juvix/Compiler/Tree/Language/Value.hs @@ -1,11 +1,13 @@ module Juvix.Compiler.Tree.Language.Value where import Juvix.Compiler.Tree.Language.Base +import Juvix.Data.Field {- A value may be one of: - Integer (arbitrary precision) + - Field element - Boolean - String - Constructor data @@ -14,6 +16,7 @@ import Juvix.Compiler.Tree.Language.Base data Value = ValInteger Integer + | ValField FField | ValBool Bool | ValString Text | ValUnit @@ -50,6 +53,7 @@ instance HasAtomicity Closure where instance HasAtomicity Value where atomicity = \case ValInteger {} -> Atom + ValField {} -> Atom ValBool {} -> Atom ValString {} -> Atom ValUnit -> Atom diff --git a/src/Juvix/Compiler/Tree/Pretty/Base.hs b/src/Juvix/Compiler/Tree/Pretty/Base.hs index 54680e66d..eaa23dfae 100644 --- a/src/Juvix/Compiler/Tree/Pretty/Base.hs +++ b/src/Juvix/Compiler/Tree/Pretty/Base.hs @@ -83,6 +83,8 @@ instance PrettyCode Value where ppCode = \case ValInteger i -> return $ integer i + ValField i -> + return $ integer i ValBool True -> return $ annotate (AnnKind KNameConstructor) (pretty (Str.true_ :: String)) ValBool False -> @@ -137,6 +139,8 @@ instance PrettyCode Type where return $ annotate (AnnKind KNameInductive) Str.mul TyInteger {} -> return $ annotate (AnnKind KNameInductive) Str.integer + TyField {} -> + return $ annotate (AnnKind KNameInductive) Str.field TyBool {} -> return $ annotate (AnnKind KNameInductive) Str.bool TyString -> @@ -181,6 +185,8 @@ instance PrettyCode Constant where ppCode = \case ConstInt v -> return $ annotate AnnLiteralInteger (pretty v) + ConstField v -> + return $ annotate AnnLiteralInteger (pretty v <> "F") ConstBool True -> return $ annotate (AnnKind KNameConstructor) Str.true_ ConstBool False -> @@ -201,6 +207,10 @@ instance PrettyCode BinaryOp where OpIntMod -> Str.instrMod OpIntLt -> Str.instrLt OpIntLe -> Str.instrLe + OpFieldAdd -> Str.fadd + OpFieldSub -> Str.fsub + OpFieldMul -> Str.fmul + OpFieldDiv -> Str.fdiv OpEq -> Str.instrEq OpStrConcat -> Str.instrStrConcat @@ -220,6 +230,8 @@ instance PrettyCode UnaryOp where ppCode op = return $ primitive $ case op of OpShow -> Str.instrShow OpStrToInt -> Str.instrStrToInt + OpFieldToInt -> Str.instrFieldToInt + OpIntToField -> Str.instrIntToField OpArgsNum -> Str.instrArgsNum instance PrettyCode UnaryOpcode where diff --git a/src/Juvix/Compiler/Tree/Transformation/Validate.hs b/src/Juvix/Compiler/Tree/Transformation/Validate.hs index c2294ef8c..dd568108d 100644 --- a/src/Juvix/Compiler/Tree/Transformation/Validate.hs +++ b/src/Juvix/Compiler/Tree/Transformation/Validate.hs @@ -52,6 +52,10 @@ inferType tab funInfo = goInfer mempty OpIntMod -> checkBinop mkTypeInteger mkTypeInteger mkTypeInteger OpIntLt -> checkBinop mkTypeInteger mkTypeInteger mkTypeBool OpIntLe -> checkBinop mkTypeInteger mkTypeInteger mkTypeBool + OpFieldAdd -> checkBinop TyField TyField TyField + OpFieldSub -> checkBinop TyField TyField TyField + OpFieldMul -> checkBinop TyField TyField TyField + OpFieldDiv -> checkBinop TyField TyField TyField OpEq -> checkBinop TyDynamic TyDynamic mkTypeBool OpStrConcat -> checkBinop TyString TyString TyString @@ -74,12 +78,15 @@ inferType tab funInfo = goInfer mempty OpShow -> checkUnop TyDynamic TyString OpStrToInt -> checkUnop TyString mkTypeInteger OpArgsNum -> checkUnop TyDynamic mkTypeInteger + OpIntToField -> checkUnop mkTypeInteger TyField + OpFieldToInt -> checkUnop TyField mkTypeInteger goConst :: BinderList Type -> NodeConstant -> Sem r Type goConst _ NodeConstant {..} = case _nodeConstant of ConstInt {} -> return mkTypeInteger ConstBool {} -> return mkTypeBool ConstString {} -> return TyString + ConstField {} -> return TyField ConstUnit {} -> return TyUnit ConstVoid {} -> return TyVoid diff --git a/src/Juvix/Compiler/Tree/Translation/FromAsm.hs b/src/Juvix/Compiler/Tree/Translation/FromAsm.hs index 034677fa0..76e5fc999 100644 --- a/src/Juvix/Compiler/Tree/Translation/FromAsm.hs +++ b/src/Juvix/Compiler/Tree/Translation/FromAsm.hs @@ -23,7 +23,8 @@ fromAsm tab = do { _infoMainFunction = tab ^. Asm.infoMainFunction, _infoFunctions = fns, _infoInductives = tab ^. Asm.infoInductives, - _infoConstrs = tab ^. Asm.infoConstrs + _infoConstrs = tab ^. Asm.infoConstrs, + _infoFieldSize = tab ^. Asm.infoFieldSize } goFunction :: (Member (Error TreeError) r') => Asm.InfoTable -> Asm.FunctionInfo -> Sem r' FunctionInfo diff --git a/src/Juvix/Compiler/Tree/Translation/FromCore.hs b/src/Juvix/Compiler/Tree/Translation/FromCore.hs index c12ab170f..8488ab30c 100644 --- a/src/Juvix/Compiler/Tree/Translation/FromCore.hs +++ b/src/Juvix/Compiler/Tree/Translation/FromCore.hs @@ -17,7 +17,8 @@ fromCore tab = { _infoMainFunction = tab ^. Core.infoMain, _infoFunctions = genCode tab <$> tab ^. Core.infoFunctions, _infoInductives = translateInductiveInfo <$> tab ^. Core.infoInductives, - _infoConstrs = translateConstructorInfo <$> tab ^. Core.infoConstructors + _infoConstrs = translateConstructorInfo <$> tab ^. Core.infoConstructors, + _infoFieldSize = tab ^. Core.infoFieldSize } -- Generate code for a single function. @@ -82,6 +83,8 @@ genCode infoTable fi = mkConst (ConstInt i) Core.Constant _ (Core.ConstString s) -> mkConst (ConstString s) + Core.Constant _ (Core.ConstField fld) -> + mkConst (ConstField fld) goApps :: Int -> BinderList MemRef -> Core.Apps -> Node goApps tempSize refs Core.Apps {..} = @@ -268,6 +271,10 @@ genCode infoTable fi = Core.OpIntMod -> PrimBinop OpIntMod Core.OpIntLt -> PrimBinop OpIntLt Core.OpIntLe -> PrimBinop OpIntLe + Core.OpFieldAdd -> PrimBinop OpFieldAdd + Core.OpFieldSub -> PrimBinop OpFieldSub + Core.OpFieldMul -> PrimBinop OpFieldMul + Core.OpFieldDiv -> PrimBinop OpFieldDiv Core.OpEq -> PrimBinop OpEq Core.OpStrConcat -> PrimBinop OpStrConcat Core.OpSeq -> OpSeq @@ -277,6 +284,8 @@ genCode infoTable fi = genUnOp = \case Core.OpShow -> PrimUnop OpShow Core.OpStrToInt -> PrimUnop OpStrToInt + Core.OpFieldFromInt -> PrimUnop OpIntToField + Core.OpFieldToInt -> PrimUnop OpFieldToInt Core.OpTrace -> OpTrace Core.OpFail -> OpFail _ -> impossible @@ -314,6 +323,8 @@ convertPrimitiveType = \case TyBool (TypeBool _infoTrueTag _infoFalseTag) Core.PrimString -> TyString + Core.PrimField -> + TyField -- | `convertNestedType` ensures that the conversion of a type with Dynamic in the -- target is curried. The result of `convertType 0 ty` is always uncurried. diff --git a/src/Juvix/Compiler/Tree/Translation/FromSource.hs b/src/Juvix/Compiler/Tree/Translation/FromSource.hs index 504c243cc..669245fbe 100644 --- a/src/Juvix/Compiler/Tree/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Tree/Translation/FromSource.hs @@ -75,6 +75,10 @@ parseBinop = <|> parseBinaryOp kwMod_ (PrimBinop OpIntMod) <|> parseBinaryOp kwLt_ (PrimBinop OpIntLt) <|> parseBinaryOp kwLe_ (PrimBinop OpIntLe) + <|> parseBinaryOp kwFieldAdd (PrimBinop OpFieldAdd) + <|> parseBinaryOp kwFieldSub (PrimBinop OpFieldSub) + <|> parseBinaryOp kwFieldMul (PrimBinop OpFieldMul) + <|> parseBinaryOp kwFieldDiv (PrimBinop OpFieldDiv) <|> parseBinaryOp kwEq_ (PrimBinop OpEq) <|> parseBinaryOp kwStrcat (PrimBinop OpStrConcat) <|> parseBinaryOp kwSeq_ OpSeq diff --git a/src/Juvix/Compiler/Tree/Translation/FromSource/Base.hs b/src/Juvix/Compiler/Tree/Translation/FromSource/Base.hs index b9448e10b..a92cc9444 100644 --- a/src/Juvix/Compiler/Tree/Translation/FromSource/Base.hs +++ b/src/Juvix/Compiler/Tree/Translation/FromSource/Base.hs @@ -23,6 +23,7 @@ import Juvix.Compiler.Tree.Keywords.Base import Juvix.Compiler.Tree.Language.Base import Juvix.Compiler.Tree.Translation.FromSource.Lexer.Base import Juvix.Compiler.Tree.Translation.FromSource.Sig +import Juvix.Data.Field import Juvix.Parser.Error import Text.Megaparsec qualified as P @@ -306,6 +307,7 @@ typeNamed = do txt <- identifier @t @e @d case txt of "integer" -> return mkTypeInteger + "field" -> return TyField "bool" -> return mkTypeBool "string" -> return TyString "unit" -> return TyUnit @@ -316,7 +318,12 @@ typeNamed = do _ -> parseFailure off ("not a type: " ++ fromText txt) constant :: ParsecS r Constant -constant = integerValue <|> boolValue <|> stringValue <|> unitValue <|> voidValue +constant = fieldValue <|> integerValue <|> boolValue <|> stringValue <|> unitValue <|> voidValue + +fieldValue :: ParsecS r Constant +fieldValue = P.try $ do + (i, _) <- field + return $ ConstField (fieldFromInteger defaultFieldSize i) integerValue :: ParsecS r Constant integerValue = do diff --git a/src/Juvix/Compiler/Tree/Translation/FromSource/Lexer/Base.hs b/src/Juvix/Compiler/Tree/Translation/FromSource/Lexer/Base.hs index 45bf30c1b..b8b6d0cd6 100644 --- a/src/Juvix/Compiler/Tree/Translation/FromSource/Lexer/Base.hs +++ b/src/Juvix/Compiler/Tree/Translation/FromSource/Lexer/Base.hs @@ -31,6 +31,9 @@ integer = integer' decimal number :: Int -> Int -> ParsecS r (Int, Interval) number = number' integer +field :: ParsecS r (Integer, Interval) +field = lexemeInterval field' + string :: ParsecS r (Text, Interval) string = lexemeInterval string' diff --git a/src/Juvix/Data/Field.hs b/src/Juvix/Data/Field.hs new file mode 100644 index 000000000..3d84cb306 --- /dev/null +++ b/src/Juvix/Data/Field.hs @@ -0,0 +1,106 @@ +module Juvix.Data.Field where + +import Data.Serialize as S +import Data.Singletons.Decide +import GHC.Show qualified as S +import GHC.TypeLits.Singletons () +import Juvix.Data.FiniteField.PrimeField +import Juvix.Prelude hiding (toInteger) +import Juvix.Prelude.Pretty + +newtype FField = FField + { _unFField :: Sigma Natural (TyCon1 PrimeField) + } + deriving stock (Generic) + +makeLenses ''FField + +defaultFieldSize :: Natural +defaultFieldSize = smallFieldSize + +cairoFieldSize :: Natural +cairoFieldSize = 3618502788666131213697322783095070105623107215331596699973092056135872020481 + +smallFieldSize :: Natural +smallFieldSize = 2147483647 + +allowedFieldSizes :: [Natural] +allowedFieldSizes = [11, smallFieldSize, cairoFieldSize] + +instance Serialize FField where + put f = S.put (fieldSize f, fieldToInteger f) + + get = do + (n, f) <- S.get + return $ fieldFromInteger n f + +instance Pretty FField where + pretty (FField (_ :&: f)) = pretty (toInteger f) + +instance Show FField where + show (FField (_ :&: f)) = show (toInteger f) + +fieldAdd :: FField -> FField -> FField +fieldAdd + (FField ((n1 :: Sing (p :: Natural)) :&: (f1 :: PrimeField p))) + (FField ((n2 :: Sing (r :: Natural)) :&: (f2 :: PrimeField r))) = + let x = decideEquality n1 n2 + in case x :: Maybe (p :~: r) of + Just Refl -> FField (n1 :&: withSingI n1 (f1 + f2)) + Nothing -> impossible + +fieldSub :: FField -> FField -> FField +fieldSub + (FField ((n1 :: Sing (p :: Natural)) :&: (f1 :: PrimeField p))) + (FField ((n2 :: Sing (r :: Natural)) :&: (f2 :: PrimeField r))) = + let x = decideEquality n1 n2 + in case x :: Maybe (p :~: r) of + Just Refl -> FField (n1 :&: withSingI n1 (f1 - f2)) + Nothing -> impossible + +fieldMul :: FField -> FField -> FField +fieldMul + (FField ((n1 :: Sing (p :: Natural)) :&: (f1 :: PrimeField p))) + (FField ((n2 :: Sing (r :: Natural)) :&: (f2 :: PrimeField r))) = + let x = decideEquality n1 n2 + in case x :: Maybe (p :~: r) of + Just Refl -> FField (n1 :&: withSingI n1 (f1 * f2)) + Nothing -> impossible + +fieldDiv :: FField -> FField -> FField +fieldDiv + (FField ((n1 :: Sing (p :: Natural)) :&: (f1 :: PrimeField p))) + (FField ((n2 :: Sing (r :: Natural)) :&: (f2 :: PrimeField r))) = + let x = decideEquality n1 n2 + in case x :: Maybe (p :~: r) of + Just Refl -> FField (n1 :&: withSingI n1 (f1 / f2)) + Nothing -> impossible + +fieldFromInteger :: Natural -> Integer -> FField +fieldFromInteger fsize n = + FField (withSomeSing fsize $ \s -> s :&: withSingI s (fromInteger n)) + +fieldSize :: FField -> Natural +fieldSize + (FField ((n :: Sing (p :: Natural)) :&: (_ :: PrimeField p))) = + fromSing n + +fieldToInteger :: FField -> Integer +fieldToInteger + (FField ((_ :: Sing (p :: Natural)) :&: (f1 :: PrimeField p))) = + toInteger f1 + +fieldResize :: Natural -> FField -> FField +fieldResize n f = fieldFromInteger n (fieldToInteger f) + +fieldEq :: FField -> FField -> Bool +fieldEq + (FField ((n1 :: Sing (p :: Natural)) :&: (f1 :: PrimeField p))) + (FField ((n2 :: Sing (r :: Natural)) :&: (f2 :: PrimeField r))) = + let x = decideEquality n1 n2 + in case x :: Maybe (p :~: r) of + Just Refl -> f1 == f2 + Nothing -> False + +instance Eq FField where + (==) = fieldEq diff --git a/src/Juvix/Data/FiniteField/Base.hs b/src/Juvix/Data/FiniteField/Base.hs new file mode 100644 index 000000000..8181254c6 --- /dev/null +++ b/src/Juvix/Data/FiniteField/Base.hs @@ -0,0 +1,18 @@ +module Juvix.Data.FiniteField.Base where + +import Juvix.Prelude.Base + +class (Fractional k) => FiniteField k where + -- | The order is number of elements of a finite field @k@. + -- It of the form @p^n@, where @p@ is prime number called the characteristic + -- of the field, and @n@ is a positive integer. + order :: k -> Integer + + -- | The characteristic of a field, @p@. + char :: k -> Integer + + -- | The inverse of Frobenius endomorphism @x@ ↦ @x^p@. + pthRoot :: k -> k + + -- | All values of a field + allValues :: [k] diff --git a/src/Juvix/Data/FiniteField/PrimeField.hs b/src/Juvix/Data/FiniteField/PrimeField.hs new file mode 100644 index 000000000..1e68ffd77 --- /dev/null +++ b/src/Juvix/Data/FiniteField/PrimeField.hs @@ -0,0 +1,142 @@ +----------------------------------------------------------------------------- + +----------------------------------------------------------------------------- + +-- | +-- Module : Data.FiniteField.PrimeField +-- Copyright : (c) Masahiro Sakai 2013-2014 +-- License : BSD-style +-- +-- Maintainer : masahiro.sakai@gmail.com +-- Stability : provisional +-- Portability : non-portable (ScopedTypeVariables, MultiParamTypeClasses, DeriveDataTypeable, TemplateHaskell, BangPatterns) +-- +-- Finite field of prime order p, Fp = Z/pZ. +-- +-- References: +-- +-- * +module Juvix.Data.FiniteField.PrimeField + ( PrimeField, + toInteger, + + -- * Template haskell utilities + -- $TH + primeField, + ) +where + +import Data.Hashable +import Data.Ratio (denominator, numerator) +import Data.Singletons +import GHC.TypeLits +import GHC.TypeLits.Singletons () +import Juvix.Data.FiniteField.Base +import Language.Haskell.TH qualified as TH +import Prelude hiding (toInteger) + +-- | Finite field of prime order p, Fp = Z/pZ. +-- +-- NB: Primality of @p@ is assumed, but not checked. +newtype PrimeField (p :: Natural) + = PrimeField Integer + deriving stock (Eq) + +-- | conversion to 'Integer' +toInteger :: PrimeField p -> Integer +toInteger (PrimeField a) = a + +toInt :: (Integral a) => PrimeField p -> a +toInt = fromInteger . toInteger + +instance Show (PrimeField p) where + showsPrec n (PrimeField x) = showsPrec n x + +instance (SingI p) => Read (PrimeField p) where + readsPrec n s = [(fromInteger a, s') | (a, s') <- readsPrec n s] + +instance (SingI p) => Num (PrimeField p) where + PrimeField a + PrimeField b = fromInteger $ a + b + PrimeField a * PrimeField b = fromInteger $ a * b + PrimeField a - PrimeField b = fromInteger $ a - b + negate (PrimeField a) = fromInteger $ negate a + abs a = a + signum _ = 1 + fromInteger a = ret + where + ret = PrimeField $ a `mod` char ret + +instance (SingI p) => Fractional (PrimeField p) where + fromRational r = fromInteger (numerator r) / fromInteger (denominator r) + + -- recip a = a ^ (char a - 2 :: Integer) + recip x@(PrimeField a) = + case exgcd a p of + (_, r, _) -> fromInteger r + where + p :: Integer + p = char x + +instance (SingI p) => Bounded (PrimeField p) where + minBound = PrimeField 0 + maxBound = ret + where + ret :: PrimeField p + ret = PrimeField (char ret - 1) + +instance (SingI p) => Enum (PrimeField p) where + toEnum x + | toInteger (minBound :: PrimeField p) <= x' && x' <= toInteger (maxBound :: PrimeField p) = PrimeField x' + | otherwise = error "PrimeField.toEnum: bad argument" + where + x' = fromIntegral x + fromEnum = toInt + +instance Ord (PrimeField p) where + PrimeField a `compare` PrimeField b = a `compare` b + +instance (SingI (p :: Natural)) => FiniteField (PrimeField p) where + order x = char x + + -- char _ = natVal (Proxy :: Proxy p) + char _ = + let c :: Natural + c = demote @p + in fromIntegral c + pthRoot a = a + allValues = [minBound .. maxBound] + +instance (SingI p) => Hashable (PrimeField p) where + hashWithSalt s x@(PrimeField a) = + s `hashWithSalt` char x `hashWithSalt` a + +-- | Extended GCD algorithm +exgcd :: (Integral a) => a -> a -> (a, a, a) +exgcd f1 f2 = f $ go f1 f2 1 0 0 1 + where + go :: forall t. (Integral t) => t -> t -> t -> t -> t -> t -> (t, t, t) + go !r0 !r1 !s0 !s1 !t0 !t1 + | r1 == 0 = (r0, s0, t0) + | otherwise = go r1 r2 s1 s2 t1 t2 + where + (q, r2) = r0 `divMod` r1 + s2 = s0 - q * s1 + t2 = t0 - q * t1 + f :: forall a b c. (Ord a, Num a, Num b, Num c) => (a, b, c) -> (a, b, c) + f (g, u, v) + | g < 0 = (-g, -u, -v) + | otherwise = (g, u, v) + +-- --------------------------------------------------------------------------- + +-- | Create a PrimeField type +primeField :: Integer -> TH.TypeQ +primeField n + | n <= 0 = error "primeField: negative value" + | otherwise = [t|PrimeField $(TH.litT (TH.numTyLit n))|] + +-- $TH +-- Here is usage example for primeField: +-- +-- > a :: $(primeField 15485867) +-- > a = 1 diff --git a/src/Juvix/Data/Keyword/All.hs b/src/Juvix/Data/Keyword/All.hs index c8852e253..c8df62273 100644 --- a/src/Juvix/Data/Keyword/All.hs +++ b/src/Juvix/Data/Keyword/All.hs @@ -343,6 +343,18 @@ kwLt_ = asciiKw Str.lt_ kwLe_ :: Keyword kwLe_ = asciiKw Str.le_ +kwFieldAdd :: Keyword +kwFieldAdd = asciiKw Str.fadd + +kwFieldSub :: Keyword +kwFieldSub = asciiKw Str.fsub + +kwFieldMul :: Keyword +kwFieldMul = asciiKw Str.fmul + +kwFieldDiv :: Keyword +kwFieldDiv = asciiKw Str.fdiv + kwSeq_ :: Keyword kwSeq_ = asciiKw Str.sseq_ diff --git a/src/Juvix/Extra/Strings.hs b/src/Juvix/Extra/Strings.hs index 408356183..295f59582 100644 --- a/src/Juvix/Extra/Strings.hs +++ b/src/Juvix/Extra/Strings.hs @@ -179,6 +179,30 @@ int_ = "int" boolPrint :: (IsString s) => s boolPrint = "bool-print" +fieldEq :: (IsString s) => s +fieldEq = "field-eq" + +fieldAdd :: (IsString s) => s +fieldAdd = "field-add" + +fieldSub :: (IsString s) => s +fieldSub = "field-sub" + +fieldMul :: (IsString s) => s +fieldMul = "field-mul" + +fieldDiv :: (IsString s) => s +fieldDiv = "field-div" + +field :: (IsString s) => s +field = "field" + +fieldFromInt :: (IsString s) => s +fieldFromInt = "field-from-int" + +fieldToNat :: (IsString s) => s +fieldToNat = "field-to-nat" + io :: (IsString s) => s io = "IO" @@ -302,6 +326,24 @@ any = "Any" questionMark :: (IsString s) => s questionMark = "?" +fadd :: (IsString s) => s +fadd = "fadd" + +fsub :: (IsString s) => s +fsub = "fsub" + +fmul :: (IsString s) => s +fmul = "fmul" + +fdiv :: (IsString s) => s +fdiv = "fdiv" + +ftoi :: (IsString s) => s +ftoi = "ftoi" + +itof :: (IsString s) => s +itof = "itof" + delimiter :: (IsString s) => s delimiter = "delimiter" @@ -674,6 +716,12 @@ instrStrConcat = "strcat" instrStrToInt :: (IsString s) => s instrStrToInt = "atoi" +instrFieldToInt :: (IsString s) => s +instrFieldToInt = "ftoi" + +instrIntToField :: (IsString s) => s +instrIntToField = "itof" + instrShow :: (IsString s) => s instrShow = "show" diff --git a/src/Juvix/Parser/Lexer.hs b/src/Juvix/Parser/Lexer.hs index 80f288457..5d14a0cae 100644 --- a/src/Juvix/Parser/Lexer.hs +++ b/src/Juvix/Parser/Lexer.hs @@ -136,6 +136,12 @@ number' int mn mx = do string' :: ParsecS r Text string' = pack <$> (char '"' >> manyTill L.charLiteral (char '"')) +field' :: ParsecS r Integer +field' = do + d <- L.decimal + P.chunk "F" + 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/Casm/Run/Base.hs b/test/Casm/Run/Base.hs index 35a177719..6e50c148c 100644 --- a/test/Casm/Run/Base.hs +++ b/test/Casm/Run/Base.hs @@ -5,6 +5,7 @@ import Juvix.Compiler.Casm.Error import Juvix.Compiler.Casm.Interpreter import Juvix.Compiler.Casm.Translation.FromSource import Juvix.Compiler.Casm.Validate +import Juvix.Data.Field import Juvix.Data.PPOutput import Juvix.Parser.Error @@ -65,5 +66,5 @@ parseFile f = do doRun :: LabelInfo -> Code -> - IO (Either CasmError Integer) + IO (Either CasmError FField) doRun labi instrs = catchRunErrorIO (runCode labi instrs) diff --git a/test/Casm/Run/Positive.hs b/test/Casm/Run/Positive.hs index e8944e9fd..41c756a8e 100644 --- a/test/Casm/Run/Positive.hs +++ b/test/Casm/Run/Positive.hs @@ -99,5 +99,10 @@ tests = "Test013: Currying and uncurrying" $(mkRelDir ".") $(mkRelFile "test013.casm") - $(mkRelFile "out/test013.out") + $(mkRelFile "out/test013.out"), + PosTest + "Test014: Field arithmetic" + $(mkRelDir ".") + $(mkRelFile "test014.casm") + $(mkRelFile "out/test014.out") ] diff --git a/test/Compilation/Positive.hs b/test/Compilation/Positive.hs index cc7c4ff7c..2c3572a61 100644 --- a/test/Compilation/Positive.hs +++ b/test/Compilation/Positive.hs @@ -440,5 +440,10 @@ tests = "Test073: Import and use a syntax alias" $(mkRelDir "test073") $(mkRelFile "test073.juvix") - $(mkRelFile "out/test073.out") + $(mkRelFile "out/test073.out"), + posTestEval + "Test074: Fields" + $(mkRelDir ".") + $(mkRelFile "test074.juvix") + $(mkRelFile "out/test074.out") ] diff --git a/test/Core/Asm/Base.hs b/test/Core/Asm/Base.hs index 22de08843..2faf7cf73 100644 --- a/test/Core/Asm/Base.hs +++ b/test/Core/Asm/Base.hs @@ -12,6 +12,7 @@ import Juvix.Compiler.Core.Pipeline import Juvix.Compiler.Core.Translation.FromSource import Juvix.Compiler.Core.Translation.Stripped.FromCore qualified as Stripped import Juvix.Compiler.Tree.Translation.FromCore qualified as Tree +import Juvix.Data.Field import Juvix.Data.PPOutput newtype Test = Test @@ -55,5 +56,5 @@ coreAsmAssertion mainFile expectedFile step = do case run $ runReader defaultCoreOptions $ runError $ toStored' >=> toStripped' Identity $ moduleFromInfoTable $ setupMainFunction defaultModuleId tabIni node of Left err -> assertFailure (show (pretty (fromJuvixError @GenericError err))) Right m -> do - let tab = Asm.fromTree $ Tree.fromCore $ Stripped.fromCore $ computeCombinedInfoTable m + let tab = Asm.fromTree $ Tree.fromCore $ Stripped.fromCore (maximum allowedFieldSizes) $ computeCombinedInfoTable m Asm.asmRunAssertion' tab expectedFile step diff --git a/test/Core/Compile/Base.hs b/test/Core/Compile/Base.hs index be6b8cffa..6013129b0 100644 --- a/test/Core/Compile/Base.hs +++ b/test/Core/Compile/Base.hs @@ -15,6 +15,7 @@ import Juvix.Compiler.Core.Pipeline import Juvix.Compiler.Core.Translation.FromSource import Juvix.Compiler.Core.Translation.Stripped.FromCore qualified as Stripped import Juvix.Compiler.Tree.Translation.FromCore qualified as Tree +import Juvix.Data.Field import Juvix.Data.PPOutput newtype Test = Test @@ -54,7 +55,7 @@ coreCompileAssertion' optLevel tab mainFile expectedFile stdinText step = do Right m -> do let tab0 = computeCombinedInfoTable m assertBool "Check info table" (checkInfoTable tab0) - let tab' = Asm.fromTree . Tree.fromCore $ Stripped.fromCore tab0 + let tab' = Asm.fromTree . Tree.fromCore $ Stripped.fromCore (maximum allowedFieldSizes) tab0 length (fromText (Asm.ppPrint tab' tab') :: String) `seq` Asm.asmCompileAssertion' optLevel tab' mainFile expectedFile stdinText step where diff --git a/test/Core/Compile/Positive.hs b/test/Core/Compile/Positive.hs index f783a91d2..67d558feb 100644 --- a/test/Core/Compile/Positive.hs +++ b/test/Core/Compile/Positive.hs @@ -7,7 +7,7 @@ import Core.Eval.Positive qualified as Eval allTests :: TestTree allTests = testGroup "JuvixCore compilation tests" (map liftTest (Eval.filterOutTests ignoredTests Eval.compilableTests)) --- Arbitrary precision integers not yet supported +-- Arbitrary precision integers and fields not yet supported ignoredTests :: [String] ignoredTests = [ "Test011: Tail recursion: Fibonacci numbers in linear time", @@ -15,7 +15,8 @@ ignoredTests = "Test025: Mutual recursion", "Test026: Nested 'case', 'let' and 'if' with variable capture", "Test036: Big numbers", - "Test040: LetRec - fib, fact" + "Test040: LetRec - fib, fact", + "Test061: Fields" ] liftTest :: Eval.PosTest -> TestTree diff --git a/test/Core/Eval/Positive.hs b/test/Core/Eval/Positive.hs index dcddc9b92..7817faaee 100644 --- a/test/Core/Eval/Positive.hs +++ b/test/Core/Eval/Positive.hs @@ -342,5 +342,10 @@ tests = "Test060: Bottom" $(mkRelDir ".") $(mkRelFile "test060.jvc") - $(mkRelFile "out/test060.out") + $(mkRelFile "out/test060.out"), + PosTest + "Test061: Fields" + $(mkRelDir ".") + $(mkRelFile "test061.jvc") + $(mkRelFile "out/test061.out") ] diff --git a/test/Core/Normalize/Base.hs b/test/Core/Normalize/Base.hs index e230a11a8..2743c010a 100644 --- a/test/Core/Normalize/Base.hs +++ b/test/Core/Normalize/Base.hs @@ -8,6 +8,7 @@ import Juvix.Compiler.Core.Pipeline import Juvix.Compiler.Core.Pretty import Juvix.Compiler.Core.Transformation import Juvix.Compiler.Core.Translation.FromSource +import Juvix.Data.Field coreNormalizeAssertion :: Path Abs File -> @@ -29,6 +30,6 @@ coreNormalizeAssertion mainFile expectedFile step = do Right m -> do step "Normalize" let tab' = computeCombinedInfoTable m - node' = normalize m (lookupIdentifierNode m (fromJust $ tab' ^. infoMain)) + node' = normalize (maximum allowedFieldSizes) m (lookupIdentifierNode m (fromJust $ tab' ^. infoMain)) tab'' = setupMainFunction defaultModuleId tab' node' coreEvalAssertion' EvalModeJSON tab'' mainFile expectedFile step diff --git a/test/Repl/Positive.hs b/test/Repl/Positive.hs index c6cddffe7..3336b41f8 100644 --- a/test/Repl/Positive.hs +++ b/test/Repl/Positive.hs @@ -130,7 +130,7 @@ evalRepl artif ep n = do doEvalIO' artif' n' = mapRight (Core.toValue tab) . mapLeft (JuvixError @Core.CoreError) - <$> (Core.doEvalIO False replDefaultLoc tab n') + <$> (Core.doEvalIO Nothing False replDefaultLoc tab n') where tab :: Core.InfoTable tab = Core.computeCombinedInfoTable $ artif' ^. artifactCoreModule diff --git a/tests/Casm/positive/out/test014.out b/tests/Casm/positive/out/test014.out new file mode 100644 index 000000000..2c8b00b0f --- /dev/null +++ b/tests/Casm/positive/out/test014.out @@ -0,0 +1 @@ +2532951952066291849588125948166549073936175050732117689981164439295110414326 diff --git a/tests/Casm/positive/test014.casm b/tests/Casm/positive/test014.casm new file mode 100644 index 000000000..34ade6e45 --- /dev/null +++ b/tests/Casm/positive/test014.casm @@ -0,0 +1,22 @@ +-- field arithmetic + +start: + call main + jmp end + +func: + [ap] = 1; ap++ + [ap] = [ap - 1] / [fp - 3]; ap++ + [ap] = [fp - 4] * [ap - 1]; ap++ + [ap] = [fp - 3] + [ap - 1]; ap++ + [ap] = 0; ap++ + [ap] = [ap - 1] - [ap - 2]; ap++ + ret + +main: + [ap] = 7; ap++ + [ap] = 10; ap++ + call func + ret + +end: diff --git a/tests/Compilation/positive/out/test074.out b/tests/Compilation/positive/out/test074.out new file mode 100644 index 000000000..4c68a1a64 --- /dev/null +++ b/tests/Compilation/positive/out/test074.out @@ -0,0 +1 @@ +214748354 diff --git a/tests/Compilation/positive/test074.juvix b/tests/Compilation/positive/test074.juvix new file mode 100644 index 000000000..25dace84d --- /dev/null +++ b/tests/Compilation/positive/test074.juvix @@ -0,0 +1,8 @@ +-- Fields +module test074; + +import Stdlib.Prelude open; + +f (x y : Field) : Field := 0 - (x + y * (1 / x)); + +main : Field := f 10 7; diff --git a/tests/Core/positive/out/test061.out b/tests/Core/positive/out/test061.out new file mode 100644 index 000000000..4c68a1a64 --- /dev/null +++ b/tests/Core/positive/out/test061.out @@ -0,0 +1 @@ +214748354 diff --git a/tests/Core/positive/test061.jvc b/tests/Core/positive/test061.jvc new file mode 100644 index 000000000..e9637218f --- /dev/null +++ b/tests/Core/positive/test061.jvc @@ -0,0 +1,5 @@ +-- Fields + +def f := \x \y fsub 0F (fadd x (fmul y (fdiv 1F x))); + +f 10F 7F