diff --git a/src/Juvix/Compiler/Builtins/Anoma.hs b/src/Juvix/Compiler/Builtins/Anoma.hs index 2f3a39e4c6..ca74dbda57 100644 --- a/src/Juvix/Compiler/Builtins/Anoma.hs +++ b/src/Juvix/Compiler/Builtins/Anoma.hs @@ -6,6 +6,22 @@ import Juvix.Compiler.Internal.Extra import Juvix.Compiler.Internal.Pretty import Juvix.Prelude +checkAnomaFFI :: forall r. (Members '[Reader BuiltinsTable, Error ScoperError] r) => InductiveDef -> Sem r () +checkAnomaFFI d = do + let err :: forall a. Text -> Sem r a + err = builtinsErrorText (getLoc d) + let eqTxt = prettyText BuiltinAnomaFFI + unless (isSmallUniverse' (d ^. inductiveType)) (err (eqTxt <> " should be in the small universe")) + case d ^. inductiveParameters of + [_] -> return () + _ -> err (eqTxt <> " should have exactly one type parameter") + case d ^. inductiveConstructors of + [c1] -> checkMkAnomaFFI c1 + _ -> err (eqTxt <> " should have exactly one constructor") + +checkMkAnomaFFI :: ConstructorDef -> Sem r () +checkMkAnomaFFI _ = return () + checkAnomaGet :: (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => AxiomDef -> Sem r () checkAnomaGet f = do let ftype = f ^. axiomType diff --git a/src/Juvix/Compiler/Builtins/Ord.hs b/src/Juvix/Compiler/Builtins/Ord.hs index 5146870ef8..15dc398cbd 100644 --- a/src/Juvix/Compiler/Builtins/Ord.hs +++ b/src/Juvix/Compiler/Builtins/Ord.hs @@ -16,7 +16,7 @@ checkOrdDef d = do _ -> err (eqTxt <> " should have exactly one type parameter") case d ^. inductiveConstructors of [c1] -> checkMkOrd c1 - _ -> err (eqTxt <> " should have exactly two constructors") + _ -> err (eqTxt <> " should have exactly one constructor") checkMkOrd :: ConstructorDef -> Sem r () checkMkOrd _ = return () diff --git a/src/Juvix/Compiler/Concrete/Data/Builtins.hs b/src/Juvix/Compiler/Concrete/Data/Builtins.hs index d87c0e3dd9..43ce02e1cc 100644 --- a/src/Juvix/Compiler/Concrete/Data/Builtins.hs +++ b/src/Juvix/Compiler/Concrete/Data/Builtins.hs @@ -67,6 +67,7 @@ builtinConstructors = \case BuiltinOrd -> [BuiltinMkOrd] BuiltinOrdering -> [BuiltinOrderingLT, BuiltinOrderingEQ, BuiltinOrderingGT] BuiltinNockmaNoun -> [BuiltinNockmaAtom, BuiltinNockmaCell] + BuiltinAnomaFFI -> [BuiltinMkAnomaFFI] data BuiltinInductive = BuiltinNat @@ -87,6 +88,7 @@ data BuiltinInductive | BuiltinAnomaComplianceInputs | BuiltinAnomaShieldedTransaction | BuiltinNockmaNoun + | BuiltinAnomaFFI deriving stock (Show, Eq, Ord, Enum, Bounded, Generic, Data) instance Hashable BuiltinInductive @@ -115,6 +117,7 @@ instance Pretty BuiltinInductive where BuiltinAnomaComplianceInputs -> Str.anomaComplianceInputs BuiltinAnomaShieldedTransaction -> Str.anomaShieldedTransaction BuiltinNockmaNoun -> Str.nockmaNoun + BuiltinAnomaFFI -> Str.anomaFFI instance Pretty BuiltinConstructor where pretty = \case @@ -143,6 +146,7 @@ instance Pretty BuiltinConstructor where BuiltinMkAnomaShieldedTransaction -> Str.anomaMkShieldedTransaction BuiltinMkEq -> Str.mkEq BuiltinMkOrd -> Str.mkOrd + BuiltinMkAnomaFFI -> Str.mkAnomaFFI BuiltinOrderingLT -> Str.lt BuiltinOrderingEQ -> Str.eq BuiltinOrderingGT -> Str.gt @@ -163,6 +167,7 @@ data BuiltinConstructor | BuiltinListCons | BuiltinMkEq | BuiltinMkOrd + | BuiltinMkAnomaFFI | BuiltinMaybeNothing | BuiltinMaybeJust | BuiltinPairConstr diff --git a/src/Juvix/Compiler/Concrete/Gen.hs b/src/Juvix/Compiler/Concrete/Gen.hs index b63a1b6356..003d406df5 100644 --- a/src/Juvix/Compiler/Concrete/Gen.hs +++ b/src/Juvix/Compiler/Concrete/Gen.hs @@ -39,6 +39,7 @@ simplestFunctionDef funName funBody = _funLhsTerminating = Nothing, _funLhsInstance = Nothing, _funLhsCoercion = Nothing, + _funLhsExtern = Nothing, _funLhsIsTop = FunctionNotTop } in FunctionDef diff --git a/src/Juvix/Compiler/Concrete/Keywords.hs b/src/Juvix/Compiler/Concrete/Keywords.hs index fb4c7ba6ab..7de39d254c 100644 --- a/src/Juvix/Compiler/Concrete/Keywords.hs +++ b/src/Juvix/Compiler/Concrete/Keywords.hs @@ -40,6 +40,7 @@ import Juvix.Data.Keyword.All kwElse, kwEnd, kwEq, + kwExtern, kwFixity, kwHiding, kwHole, diff --git a/src/Juvix/Compiler/Concrete/Language/Base.hs b/src/Juvix/Compiler/Concrete/Language/Base.hs index 114b5d18d4..328870354e 100644 --- a/src/Juvix/Compiler/Concrete/Language/Base.hs +++ b/src/Juvix/Compiler/Concrete/Language/Base.hs @@ -3034,6 +3034,7 @@ data FunctionLhs (s :: Stage) = FunctionLhs _funLhsTerminating :: Maybe KeywordRef, _funLhsInstance :: Maybe KeywordRef, _funLhsCoercion :: Maybe KeywordRef, + _funLhsExtern :: Maybe KeywordRef, _funLhsName :: FunctionSymbolType s, _funLhsTypeSig :: TypeSig s, _funLhsIsTop :: FunctionIsTop diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs index 6c00f87788..98dc37a33c 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs @@ -41,6 +41,7 @@ import Juvix.Prelude.Pretty data FunctionSyntaxOptions = FunctionSyntaxOptions { _funAllowOmitType :: Bool, _funAllowInstance :: Bool, + _funAllowExtern :: Bool, _funIsTop :: FunctionIsTop } @@ -472,6 +473,7 @@ derivingInstance = do FunctionSyntaxOptions { _funAllowOmitType = False, _funAllowInstance = True, + _funAllowExtern = False, _funIsTop = FunctionTop } _derivingFunLhs <- functionDefinitionLhs opts Nothing @@ -491,6 +493,7 @@ statement = P.label "" $ do FunctionSyntaxOptions { _funAllowInstance = True, _funAllowOmitType = False, + _funAllowExtern = True, _funIsTop = FunctionTop } ms <- @@ -677,6 +680,7 @@ builtinFunctionDef = functionDefinition funSyntax . Just FunctionSyntaxOptions { _funAllowInstance = True, _funAllowOmitType = False, + _funAllowExtern = False, _funIsTop = FunctionTop } @@ -1029,6 +1033,7 @@ pnamedArgumentFunctionDef = do FunctionSyntaxOptions { _funAllowOmitType = True, _funAllowInstance = False, + _funAllowExtern = False, _funIsTop = FunctionNotTop } fun <- functionDefinition funSyntax Nothing @@ -1141,6 +1146,7 @@ letFunDef = do FunctionSyntaxOptions { _funAllowOmitType = True, _funAllowInstance = False, + _funAllowExtern = False, _funIsTop = FunctionNotTop } @@ -1346,6 +1352,11 @@ functionDefinitionLhs :: functionDefinitionLhs opts _funLhsBuiltin = P.label "" $ do let allowInstance = opts ^. funAllowInstance allowOmitType = opts ^. funAllowOmitType + allowExtern = opts ^. funAllowExtern + _funLhsExtern <- optional (kw kwExtern) + unless (allowExtern || isNothing _funLhsExtern) $ + P.lift . throw . ErrExternNotAllowed . ExternNotAllowedError $ + getLoc (fromJust _funLhsExtern) _funLhsTerminating <- optional (kw kwTerminating) _funLhsCoercion <- optional (kw kwCoercion) unless (allowInstance || isNothing _funLhsCoercion) $ @@ -1379,6 +1390,7 @@ functionDefinitionLhs opts _funLhsBuiltin = P.label "" $ do { _funLhsInstance, _funLhsBuiltin, _funLhsCoercion, + _funLhsExtern, _funLhsName, _funLhsTypeSig, _funLhsTerminating, @@ -1697,6 +1709,7 @@ checkNoNamedApplicationMissingAt = recoverStashes $ do FunctionSyntaxOptions { _funAllowOmitType = True, _funAllowInstance = False, + _funAllowExtern = False, _funIsTop = FunctionNotTop } x <- diff --git a/src/Juvix/Compiler/Core/Data/InfoTable/Base.hs b/src/Juvix/Compiler/Core/Data/InfoTable/Base.hs index b450bbb840..f741a3216a 100644 --- a/src/Juvix/Compiler/Core/Data/InfoTable/Base.hs +++ b/src/Juvix/Compiler/Core/Data/InfoTable/Base.hs @@ -2,6 +2,7 @@ module Juvix.Compiler.Core.Data.InfoTable.Base where import Juvix.Compiler.Concrete.Data.Builtins import Juvix.Compiler.Core.Language.Base +import Juvix.Compiler.FFI data InfoTable' n = InfoTable { _identContext :: HashMap Symbol n, @@ -13,7 +14,8 @@ data InfoTable' n = InfoTable _infoSpecialisations :: HashMap Symbol [SpecialisationInfo' n], _infoLiteralIntToNat :: Maybe Symbol, _infoLiteralIntToInt :: Maybe Symbol, - _infoBuiltins :: HashMap BuiltinPrim IdentKind + _infoBuiltins :: HashMap BuiltinPrim IdentKind, + _infoExterns :: [Symbol] } deriving stock (Generic) @@ -33,7 +35,8 @@ data IdentifierInfo' n = IdentifierInfo _identifierIsExported :: Bool, _identifierBuiltin :: Maybe BuiltinFunction, _identifierPragmas :: Pragmas, - _identifierArgNames :: [Maybe Text] + _identifierArgNames :: [Maybe Text], + _identifierFFI :: [FFI] } deriving stock (Generic) @@ -125,7 +128,8 @@ instance Semigroup (InfoTable' n) where _infoSpecialisations = t1 ^. infoSpecialisations <> t2 ^. infoSpecialisations, _infoLiteralIntToNat = (t1 ^. infoLiteralIntToNat) <|> (t2 ^. infoLiteralIntToNat), _infoLiteralIntToInt = (t1 ^. infoLiteralIntToInt) <|> (t2 ^. infoLiteralIntToInt), - _infoBuiltins = t1 ^. infoBuiltins <> t2 ^. infoBuiltins + _infoBuiltins = t1 ^. infoBuiltins <> t2 ^. infoBuiltins, + _infoExterns = t1 ^. infoExterns <> t2 ^. infoExterns } instance Monoid (InfoTable' n) where @@ -140,5 +144,6 @@ instance Monoid (InfoTable' n) where _infoSpecialisations = mempty, _infoLiteralIntToNat = Nothing, _infoLiteralIntToInt = Nothing, - _infoBuiltins = mempty + _infoBuiltins = mempty, + _infoExterns = mempty } diff --git a/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs b/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs index 929b54b96c..c61bfc3336 100644 --- a/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs +++ b/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs @@ -20,6 +20,7 @@ data InfoTableBuilder :: Effect where RegisterSpecialisation :: Symbol -> SpecialisationInfo -> InfoTableBuilder m () RegisterIdentNode :: Symbol -> Node -> InfoTableBuilder m () RegisterMain :: Symbol -> InfoTableBuilder m () + RegisterExtern :: Symbol -> InfoTableBuilder m () RegisterLiteralIntToNat :: Symbol -> InfoTableBuilder m () RegisterLiteralIntToInt :: Symbol -> InfoTableBuilder m () RemoveSymbol :: Symbol -> InfoTableBuilder m () @@ -147,6 +148,8 @@ runInfoTableBuilder' st = reinterpret (runState st) interp modify' (over (builderStateModule . moduleInfoTable . identContext) (HashMap.insert sym node)) RegisterMain sym -> do modify' (set (builderStateModule . moduleInfoTable . infoMain) (Just sym)) + RegisterExtern sym -> do + modify' (over (builderStateModule . moduleInfoTable . infoExterns) (sym :)) RegisterLiteralIntToInt sym -> do modify' (set (builderStateModule . moduleInfoTable . infoLiteralIntToInt) (Just sym)) RegisterLiteralIntToNat sym -> do @@ -343,7 +346,8 @@ setupLiteralIntToNat mkNode = do _identifierIsExported = False, _identifierBuiltin = Nothing, _identifierPragmas = mempty, - _identifierArgNames = [Just "x"] + _identifierArgNames = [Just "x"], + _identifierFFI = [] } targetType :: Sem r Node @@ -379,7 +383,8 @@ setupLiteralIntToInt node = do _identifierIsExported = False, _identifierBuiltin = Nothing, _identifierPragmas = mempty, - _identifierArgNames = [Just "x"] + _identifierArgNames = [Just "x"], + _identifierFFI = [] } targetType :: Sem r Node diff --git a/src/Juvix/Compiler/Core/Data/TransformationId.hs b/src/Juvix/Compiler/Core/Data/TransformationId.hs index be43898852..81f6d29edb 100644 --- a/src/Juvix/Compiler/Core/Data/TransformationId.hs +++ b/src/Juvix/Compiler/Core/Data/TransformationId.hs @@ -10,6 +10,7 @@ data TransformationId | TopEtaExpand | RemoveTypeArgs | RemoveInductiveParams + | ResolveExterns | MoveApps | NatToPrimInt | IntToPrimInt @@ -59,7 +60,12 @@ type TransformationLikeId = TransformationLikeId' TransformationId PipelineId toTypecheckTransformations :: [TransformationId] toTypecheckTransformations = - [DetectConstantSideConditions, DetectRedundantPatterns, MatchToCase] + [ EtaExpandApps, + DetectConstantSideConditions, + DetectRedundantPatterns, + MatchToCase, + ResolveExterns + ] toEvalTransformations :: [TransformationId] toEvalTransformations = @@ -76,7 +82,7 @@ toEvalTransformations = toExecTransformations :: [TransformationId] toExecTransformations = - toEvalTransformations ++ [OptPhasePreLifting, LambdaLetRecLifting, TopEtaExpand, OptPhaseExec, MoveApps] + toEvalTransformations ++ [ResolveExterns, OptPhasePreLifting, LambdaLetRecLifting, TopEtaExpand, OptPhaseExec, MoveApps] toNormalizeTransformations :: [TransformationId] toNormalizeTransformations = @@ -114,6 +120,7 @@ instance TransformationId' TransformationId where IdentityTrans -> strIdentity RemoveTypeArgs -> strRemoveTypeArgs RemoveInductiveParams -> strRemoveInductiveParams + ResolveExterns -> strResolveExterns MoveApps -> strMoveApps NatToPrimInt -> strNatToPrimInt IntToPrimInt -> strIntToPrimInt diff --git a/src/Juvix/Compiler/Core/Data/TransformationId/Strings.hs b/src/Juvix/Compiler/Core/Data/TransformationId/Strings.hs index c99d3c9645..d94a27de72 100644 --- a/src/Juvix/Compiler/Core/Data/TransformationId/Strings.hs +++ b/src/Juvix/Compiler/Core/Data/TransformationId/Strings.hs @@ -53,6 +53,9 @@ strRemoveTypeArgs = "remove-type-args" strRemoveInductiveParams :: Text strRemoveInductiveParams = "remove-inductive-params" +strResolveExterns :: Text +strResolveExterns = "resolve-externs" + strMoveApps :: Text strMoveApps = "move-apps" diff --git a/src/Juvix/Compiler/Core/Error.hs b/src/Juvix/Compiler/Core/Error.hs index 36a62e4420..964cb7bc2c 100644 --- a/src/Juvix/Compiler/Core/Error.hs +++ b/src/Juvix/Compiler/Core/Error.hs @@ -1,5 +1,6 @@ module Juvix.Compiler.Core.Error where +import GHC.Show import Juvix.Compiler.Core.Language import Juvix.Compiler.Core.Pretty import Juvix.Parser.Error.Base @@ -37,5 +38,8 @@ instance Pretty CoreError where Just node -> pretty _coreErrorMsg <> colon <> space <> pretty (ppTrace node) Nothing -> pretty _coreErrorMsg +instance Show CoreError where + show e = fromText (prettyText e) + instance HasLoc CoreError where getLoc CoreError {..} = _coreErrorLoc diff --git a/src/Juvix/Compiler/Core/Evaluator.hs b/src/Juvix/Compiler/Core/Evaluator.hs index 1be438e598..28a5cfd49d 100644 --- a/src/Juvix/Compiler/Core/Evaluator.hs +++ b/src/Juvix/Compiler/Core/Evaluator.hs @@ -71,6 +71,16 @@ evalInfoTable herr tab = eval herr tab [] mainNode mainSym = fromJust (tab ^. infoMain) mainNode = fromJust (HashMap.lookup mainSym (tab ^. identContext)) +evalPartial :: Natural -> InfoTable -> Node -> Node +evalPartial optFieldSize tab = removeClosures . geval eopts stderr tab [] + where + eopts = + defaultEvalOptions + { _evalOptionsNoFailure = True, + _evalOptionsSilent = True, + _evalOptionsFieldSize = optFieldSize + } + -- | `eval ctx env n` evaluates a node `n` whose all free variables point into -- `env`. All nodes in `ctx` must be closed. All nodes in `env` must be values. -- Invariant for values v: eval ctx env v = v diff --git a/src/Juvix/Compiler/Core/Pretty/Base.hs b/src/Juvix/Compiler/Core/Pretty/Base.hs index 94b8b58943..4234ef5871 100644 --- a/src/Juvix/Compiler/Core/Pretty/Base.hs +++ b/src/Juvix/Compiler/Core/Pretty/Base.hs @@ -685,6 +685,7 @@ instance PrettyCode InfoTable where BuiltinNat -> False BuiltinInt -> False BuiltinBool -> False + BuiltinAnomaFFI -> False Just (BuiltinTypeAxiom _) -> False Nothing -> True diff --git a/src/Juvix/Compiler/Core/Transformation.hs b/src/Juvix/Compiler/Core/Transformation.hs index decdac0e37..09fd2a9778 100644 --- a/src/Juvix/Compiler/Core/Transformation.hs +++ b/src/Juvix/Compiler/Core/Transformation.hs @@ -49,6 +49,7 @@ import Juvix.Compiler.Core.Transformation.Optimize.SimplifyIfs import Juvix.Compiler.Core.Transformation.Optimize.SpecializeArgs import Juvix.Compiler.Core.Transformation.RemoveInductiveParams import Juvix.Compiler.Core.Transformation.RemoveTypeArgs +import Juvix.Compiler.Core.Transformation.ResolveExterns import Juvix.Compiler.Core.Transformation.TopEtaExpand import Juvix.Compiler.Core.Transformation.Trace qualified as Trace import Juvix.Compiler.Core.Transformation.UnrollRecursion @@ -78,6 +79,7 @@ applyTransformations ts = flip (foldM (flip appTrans)) ts TopEtaExpand -> return . topEtaExpand RemoveTypeArgs -> return . removeTypeArgs RemoveInductiveParams -> return . removeInductiveParams + ResolveExterns -> mapError (JuvixError @CoreError) . resolveExterns MoveApps -> return . moveApps NatToPrimInt -> return . natToPrimInt IntToPrimInt -> return . intToPrimInt diff --git a/src/Juvix/Compiler/Core/Transformation/LambdaLetRecLifting.hs b/src/Juvix/Compiler/Core/Transformation/LambdaLetRecLifting.hs index 86dea31e24..a4ffaff699 100644 --- a/src/Juvix/Compiler/Core/Transformation/LambdaLetRecLifting.hs +++ b/src/Juvix/Compiler/Core/Transformation/LambdaLetRecLifting.hs @@ -77,7 +77,8 @@ lambdaLiftNode aboveBl top = _identifierIsExported = False, _identifierBuiltin = Nothing, _identifierPragmas = adjustPragmas freeVarsNum (getInfoPragma (l ^. lambdaInfo)), - _identifierArgNames = [] + _identifierArgNames = [], + _identifierFFI = [] } registerIdentNode f fBody' let fApp = mkApps' (mkIdent (setInfoName name mempty) f) (map NVar allfreevars) @@ -160,7 +161,8 @@ lambdaLiftNode aboveBl top = _identifierIsExported = False, _identifierBuiltin = Nothing, _identifierPragmas = adjustPragmas freeVarsNum pragma, - _identifierArgNames = [] + _identifierArgNames = [], + _identifierFFI = [] } | (((sym, name), (itemBinder, (b, bty))), pragma) <- zip diff --git a/src/Juvix/Compiler/Core/Transformation/Optimize/ConstantFolding.hs b/src/Juvix/Compiler/Core/Transformation/Optimize/ConstantFolding.hs index 97f7105947..1063a27dd1 100644 --- a/src/Juvix/Compiler/Core/Transformation/Optimize/ConstantFolding.hs +++ b/src/Juvix/Compiler/Core/Transformation/Optimize/ConstantFolding.hs @@ -53,14 +53,7 @@ convertNode opts nonRecSyms tab md = umap go _ -> isType' node doEval' :: Node -> Node - doEval' = removeClosures . geval eopts stderr tab [] - where - eopts = - defaultEvalOptions - { _evalOptionsNoFailure = True, - _evalOptionsSilent = True, - _evalOptionsFieldSize = opts ^. optFieldSize - } + doEval' = evalPartial (opts ^. optFieldSize) tab constantFolding' :: CoreOptions -> HashSet Symbol -> InfoTable -> Module -> Module constantFolding' opts nonRecSyms tab md = diff --git a/src/Juvix/Compiler/Core/Transformation/Optimize/SpecializeArgs.hs b/src/Juvix/Compiler/Core/Transformation/Optimize/SpecializeArgs.hs index e61c9014c8..3aae19d04e 100644 --- a/src/Juvix/Compiler/Core/Transformation/Optimize/SpecializeArgs.hs +++ b/src/Juvix/Compiler/Core/Transformation/Optimize/SpecializeArgs.hs @@ -189,7 +189,8 @@ convertNode = dmapLRM go _identifierBuiltin = Nothing, _identifierPragmas = pragmas, _identifierArgNames = - removeSpecargs specargs (ii ^. identifierArgNames) + removeSpecargs specargs (ii ^. identifierArgNames), + _identifierFFI = [] } registerIdentNode sym' (reLambdas lams' body') let si = diff --git a/src/Juvix/Compiler/Core/Transformation/ResolveExterns.hs b/src/Juvix/Compiler/Core/Transformation/ResolveExterns.hs new file mode 100644 index 0000000000..e4034d43d3 --- /dev/null +++ b/src/Juvix/Compiler/Core/Transformation/ResolveExterns.hs @@ -0,0 +1,74 @@ +module Juvix.Compiler.Core.Transformation.ResolveExterns + ( resolveExterns, + module Juvix.Compiler.Core.Transformation.Base, + ) +where + +import Data.HashMap.Strict qualified as HashMap +import Juvix.Compiler.Core.Error +import Juvix.Compiler.Core.Evaluator +import Juvix.Compiler.Core.Options +import Juvix.Compiler.Core.Transformation.Base +import Juvix.Compiler.FFI (FFI (..)) +import Juvix.Compiler.FFI qualified as FFI + +resolveExterns :: forall r. (Members '[Reader CoreOptions, Error CoreError] r) => Module -> Sem r Module +resolveExterns md = do + opts <- ask @CoreOptions + let combinedTab = computeCombinedInfoTable md + externSyms = md ^. moduleInfoTable . infoExterns + externInfos = + map + ( over identifierType (evalPartial (opts ^. optFieldSize) combinedTab) + . lookupIdentifierInfo md + ) + externSyms + externNodes = + map + ( evalPartial (opts ^. optFieldSize) combinedTab + . lookupIdentifierNode md + ) + externSyms + ffis <- foldl' (\acc (k, v) -> HashMap.insertWith (++) k [v] acc) mempty <$> mapM resolveFFI (zipExact externInfos externNodes) + let identInfos = fmap (updateFFI ffis) (md ^. moduleInfoTable . infoIdentifiers) + return $ + over + moduleInfoTable + ( set infoExterns [] + . set infoIdentifiers identInfos + ) + md + where + resolveFFI :: (IdentifierInfo, Node) -> Sem r (Symbol, FFI) + resolveFFI (info, node) = + case info ^. identifierType of + NTyp TypeConstr {..} + | ii <- lookupInductiveInfo md _typeConstrSymbol -> + case ii ^. inductiveBuiltin of + Just (BuiltinTypeInductive BuiltinAnomaFFI) -> + maybe throwFFIError (return . second FFIAnoma) $ + FFI.resolveAnomaFFI node + _ -> + throwFFIError + _ -> + throwFFIError + where + throwFFIError :: Sem r a + throwFFIError = + throwError $ + CoreError + { _coreErrorMsg = "Invalid FFI declaration", + _coreErrorNode = Just node, + _coreErrorLoc = fromMaybe defaultLoc $ info ^. identifierLocation + } + + updateFFI :: HashMap Symbol [FFI] -> IdentifierInfo -> IdentifierInfo + updateFFI ffis info = case HashMap.lookup (info ^. identifierSymbol) ffis of + Just ffiList -> over identifierFFI (ffiList ++) info + Nothing -> info + + defaultLoc :: Interval + defaultLoc = singletonInterval (mkInitialLoc mockFile) + where + mockFile :: Path Abs File + mockFile = $(mkAbsFile "/resolve-externs") diff --git a/src/Juvix/Compiler/Core/Translation/FromInternal.hs b/src/Juvix/Compiler/Core/Translation/FromInternal.hs index d8f399a126..01cc25a9ed 100644 --- a/src/Juvix/Compiler/Core/Translation/FromInternal.hs +++ b/src/Juvix/Compiler/Core/Translation/FromInternal.hs @@ -277,6 +277,7 @@ goConstructor sym ctor = do Internal.BuiltinMkAnomaComplianceInputs -> freshTag Internal.BuiltinMkAnomaShieldedTransaction -> freshTag Internal.BuiltinMkOrd -> freshTag + Internal.BuiltinMkAnomaFFI -> freshTag Internal.BuiltinOrderingLT -> freshTag Internal.BuiltinOrderingGT -> freshTag Internal.BuiltinOrderingEQ -> freshTag @@ -374,13 +375,16 @@ preFunctionDef f = do _identifierBuiltin = f ^. Internal.funDefBuiltin, _identifierPragmas = adjustPragmas' implArgs (f ^. Internal.funDefPragmas), - _identifierArgNames = argnames + _identifierArgNames = argnames, + _identifierFFI = [] } case f ^. Internal.funDefBuiltin of Just b | isIgnoredBuiltin b -> return () _ -> do registerIdent (mkIdentIndex (f ^. Internal.funDefName)) info + when (f ^. Internal.funDefExtern) $ + registerExtern sym return PreFunctionDef { _preFunInternal = f, @@ -1243,6 +1247,7 @@ goAxiomDef a = maybe goAxiomNotBuiltin builtinBody (a ^. Internal.axiomBuiltin) _identifierBuiltin = Nothing, _identifierPragmas = a ^. Internal.axiomPragmas, _identifierArgNames = [], + _identifierFFI = [], _identifierName } registerIdent (mkIdentIndex name) info diff --git a/src/Juvix/Compiler/Core/Translation/FromSource.hs b/src/Juvix/Compiler/Core/Translation/FromSource.hs index e2448bcbae..c762682fac 100644 --- a/src/Juvix/Compiler/Core/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Core/Translation/FromSource.hs @@ -66,7 +66,8 @@ setupMainFunction mid tab node = _identifierBuiltin = Nothing, _identifierIsExported = True, _identifierPragmas = mempty, - _identifierArgNames = [] + _identifierArgNames = [], + _identifierFFI = [] } throwCoreError :: @@ -172,7 +173,8 @@ statementDef = do _identifierIsExported = False, _identifierBuiltin = Nothing, _identifierPragmas = mempty, - _identifierArgNames = [] + _identifierArgNames = [], + _identifierFFI = [] } lift $ registerIdent txt info void $ optional (parseDefinition sym ty) diff --git a/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs b/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs index 7abb7863dd..1522260b66 100644 --- a/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs +++ b/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs @@ -80,6 +80,7 @@ fromCore' tab = BuiltinJsonObject -> True BuiltinMkEq -> True BuiltinMkOrd -> True + BuiltinMkAnomaFFI -> True BuiltinOrderingLT -> True BuiltinOrderingGT -> True BuiltinOrderingEQ -> True @@ -200,6 +201,7 @@ fromCore' tab = BuiltinAnomaComplianceInputs -> True BuiltinAnomaShieldedTransaction -> True BuiltinNockmaNoun -> True + BuiltinAnomaFFI -> True translateFunctionInfo :: InfoTable -> IdentifierInfo -> Stripped.FunctionInfo translateFunctionInfo tab IdentifierInfo {..} = diff --git a/src/Juvix/Compiler/FFI.hs b/src/Juvix/Compiler/FFI.hs new file mode 100644 index 0000000000..00988dcb30 --- /dev/null +++ b/src/Juvix/Compiler/FFI.hs @@ -0,0 +1,16 @@ +module Juvix.Compiler.FFI + ( module Juvix.Compiler.FFI.Anoma, + module Juvix.Compiler.FFI, + ) +where + +import Juvix.Compiler.FFI.Anoma +import Juvix.Prelude + +data FFI + = FFIAnoma Anoma + deriving stock (Generic, Show) + +instance NFData FFI + +instance Serialize FFI diff --git a/src/Juvix/Compiler/FFI/Anoma.hs b/src/Juvix/Compiler/FFI/Anoma.hs new file mode 100644 index 0000000000..c6faac62fd --- /dev/null +++ b/src/Juvix/Compiler/FFI/Anoma.hs @@ -0,0 +1,44 @@ +module Juvix.Compiler.FFI.Anoma where + +import Juvix.Compiler.Core.Language qualified as Core +import Juvix.Compiler.Nockma.Language qualified as Nockma +import Juvix.Prelude + +data Anoma = Anoma + { _anomaStdlibCall :: Nockma.Term Natural + } + deriving stock (Generic, Show) + +instance NFData Anoma + +instance Serialize Anoma + +makeLenses ''Anoma + +nockmaTermFromCoreNode :: Core.Node -> Maybe (Nockma.Term Natural) +nockmaTermFromCoreNode node = + case node of + Core.NCtr Core.Constr {..} -> + case _constrArgs of + [Core.NCst Core.Constant {..}] -> + case _constantValue of + Core.ConstInteger v + | v >= 0 -> + return $ + Nockma.TAtom (fromIntegral v) + _ -> Nothing + [arg1, arg2] -> do + arg1' <- nockmaTermFromCoreNode arg1 + arg2' <- nockmaTermFromCoreNode arg2 + return $ Nockma.TCell arg1' arg2' + _ -> Nothing + _ -> Nothing + +resolveAnomaFFI :: Core.Node -> Maybe (Core.Symbol, Anoma) +resolveAnomaFFI node = + case node of + Core.NCtr Core.Constr {..} + | [Core.NIdt Core.Ident {..}, stdlibCall] <- _constrArgs -> do + stdlibCall' <- nockmaTermFromCoreNode stdlibCall + return (_identSymbol, Anoma {_anomaStdlibCall = stdlibCall'}) + _ -> Nothing diff --git a/src/Juvix/Compiler/Internal/Extra.hs b/src/Juvix/Compiler/Internal/Extra.hs index c688f12a09..2785b712af 100644 --- a/src/Juvix/Compiler/Internal/Extra.hs +++ b/src/Juvix/Compiler/Internal/Extra.hs @@ -123,6 +123,7 @@ genFieldProjection kind _funDefName _funDefType _funDefBuiltin _funDefArgsInfo m cloneFunctionDefSameName FunctionDef { _funDefTerminating = False, + _funDefExtern = False, _funDefIsInstanceCoercion = if | kind == ProjectionCoercion -> Just IsInstanceCoercionCoercion @@ -212,6 +213,7 @@ genPatternDefs valueName pat = output $ FunctionDef { _funDefTerminating = False, + _funDefExtern = False, _funDefIsInstanceCoercion = Nothing, _funDefPragmas = mempty, _funDefBody = body', diff --git a/src/Juvix/Compiler/Internal/Extra/Base.hs b/src/Juvix/Compiler/Internal/Extra/Base.hs index 846310009b..358eb4f2c8 100644 --- a/src/Juvix/Compiler/Internal/Extra/Base.hs +++ b/src/Juvix/Compiler/Internal/Extra/Base.hs @@ -242,6 +242,7 @@ instance HasExpressions FunctionDef where _funDefArgsInfo = infos', _funDefTerminating, _funDefIsInstanceCoercion, + _funDefExtern, _funDefName, _funDefBuiltin, _funDefPragmas, @@ -912,6 +913,7 @@ simpleFunDef funName ty body = _funDefPragmas = mempty, _funDefArgsInfo = mempty, _funDefTerminating = False, + _funDefExtern = False, _funDefBuiltin = Nothing, _funDefBody = body, _funDefDocComment = Nothing diff --git a/src/Juvix/Compiler/Internal/Extra/Clonable.hs b/src/Juvix/Compiler/Internal/Extra/Clonable.hs index ef406047a9..1fd2273b7b 100644 --- a/src/Juvix/Compiler/Internal/Extra/Clonable.hs +++ b/src/Juvix/Compiler/Internal/Extra/Clonable.hs @@ -282,6 +282,7 @@ instance Clonable FunctionDef where _funDefArgsInfo = defaultSig', _funDefTerminating, _funDefIsInstanceCoercion, + _funDefExtern, _funDefBuiltin, _funDefPragmas, _funDefDocComment diff --git a/src/Juvix/Compiler/Internal/Extra/DependencyBuilder.hs b/src/Juvix/Compiler/Internal/Extra/DependencyBuilder.hs index 5c7b28adca..e8dd62855c 100644 --- a/src/Juvix/Compiler/Internal/Extra/DependencyBuilder.hs +++ b/src/Juvix/Compiler/Internal/Extra/DependencyBuilder.hs @@ -252,6 +252,7 @@ checkBuiltinInductiveStartNode i = whenJust (i ^. inductiveBuiltin) go BuiltinOrd -> return () BuiltinOrdering -> return () BuiltinNockmaNoun -> return () + BuiltinAnomaFFI -> return () addInductiveStartNode :: Sem r () addInductiveStartNode = addStartNode (i ^. inductiveName) diff --git a/src/Juvix/Compiler/Internal/Language.hs b/src/Juvix/Compiler/Internal/Language.hs index 66a85eaeda..786287ecf6 100644 --- a/src/Juvix/Compiler/Internal/Language.hs +++ b/src/Juvix/Compiler/Internal/Language.hs @@ -135,6 +135,7 @@ data FunctionDef = FunctionDef _funDefType :: Expression, _funDefBody :: Expression, _funDefTerminating :: Bool, + _funDefExtern :: Bool, _funDefIsInstanceCoercion :: Maybe IsInstanceCoercion, _funDefBuiltin :: Maybe BuiltinFunction, _funDefArgsInfo :: [ArgInfo], diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs index a8afe4145a..be3702cd29 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs @@ -541,6 +541,7 @@ deriveOrd der@DerivingArgs {..} = do return Internal.FunctionDef { _funDefTerminating = False, + _funDefExtern = False, _funDefIsInstanceCoercion = Just Internal.IsInstanceCoercionInstance, _funDefPragmas = pragmas', _funDefArgsInfo = argsInfo, @@ -681,6 +682,7 @@ deriveRecursiveBinaryFunction label nonSelfRec DerivingArgs {..} mkLamDef = do let lamDef = Internal.FunctionDef { _funDefTerminating = False, + _funDefExtern = False, _funDefIsInstanceCoercion = Nothing, _funDefPragmas = mempty, _funDefArgsInfo = [], @@ -724,6 +726,7 @@ deriveEq der@DerivingArgs {..} = do return Internal.FunctionDef { _funDefTerminating = False, + _funDefExtern = False, _funDefIsInstanceCoercion = Just Internal.IsInstanceCoercionInstance, _funDefPragmas = pragmas', _funDefArgsInfo = argsInfo, @@ -838,6 +841,7 @@ goFunctionDef def@FunctionDef {..} = do | isJust (def ^. functionDefInstance) = Just Internal.IsInstanceCoercionInstance | otherwise = Nothing _funDefCoercion = isJust (def ^. functionDefCoercion) + _funDefExtern = isJust (def ^. functionDefLhs . funLhsExtern) _funDefBuiltin = (^. withLocParam) <$> (def ^. functionDefBuiltin) _funDefType <- goDefType (def ^. functionDefLhs) _funDefPragmas <- goPragmas _functionDefPragmas @@ -985,6 +989,7 @@ checkBuiltinInductive d b = localBuiltins $ case b of BuiltinAnomaComplianceInputs -> checkComplianceInputs d BuiltinAnomaShieldedTransaction -> checkShieldedTransaction d BuiltinNockmaNoun -> checkNockmaNoun d + BuiltinAnomaFFI -> checkAnomaFFI d localBuiltins :: (Members '[Reader S.InfoTable] r) => Sem (Reader BuiltinsTable ': r) a -> Sem r a localBuiltins m = do diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs index 062d7471f8..407ce30f37 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs @@ -410,6 +410,7 @@ checkFunctionDef FunctionDef {..} = do _funDefName, _funDefTerminating, _funDefIsInstanceCoercion, + _funDefExtern, _funDefBuiltin, _funDefPragmas, _funDefDocComment diff --git a/src/Juvix/Compiler/Pipeline/Package/Loader.hs b/src/Juvix/Compiler/Pipeline/Package/Loader.hs index 44c60871f0..e321515eb2 100644 --- a/src/Juvix/Compiler/Pipeline/Package/Loader.hs +++ b/src/Juvix/Compiler/Pipeline/Package/Loader.hs @@ -97,6 +97,7 @@ toConcrete t p = run . runReader l $ do _funLhsBuiltin = Nothing, _funLhsName = FunctionDefName name', _funLhsInstance = Nothing, + _funLhsExtern = Nothing, _funLhsTypeSig, _funLhsIsTop = FunctionTop } diff --git a/src/Juvix/Compiler/Pipeline/Repl.hs b/src/Juvix/Compiler/Pipeline/Repl.hs index 1fecfe100c..5e685c3ef3 100644 --- a/src/Juvix/Compiler/Pipeline/Repl.hs +++ b/src/Juvix/Compiler/Pipeline/Repl.hs @@ -231,7 +231,8 @@ runTransformations shouldDisambiguate ts n = runCoreInfoTableBuilderArtifacts $ _identifierIsExported = False, _identifierBuiltin = Nothing, _identifierPragmas = mempty, - _identifierArgNames = [] + _identifierArgNames = [], + _identifierFFI = [] } Core.registerIdent name idenInfo return sym diff --git a/src/Juvix/Compiler/Store/Core/Extra.hs b/src/Juvix/Compiler/Store/Core/Extra.hs index cba918d404..c87ceb8b5b 100644 --- a/src/Juvix/Compiler/Store/Core/Extra.hs +++ b/src/Juvix/Compiler/Store/Core/Extra.hs @@ -16,6 +16,7 @@ toCore InfoTable {..} = _infoInductives = fmap goInductiveInfo _infoInductives, _infoConstructors = fmap goConstructorInfo _infoConstructors, _infoSpecialisations = fmap (map goSpecialisationInfo) _infoSpecialisations, + _infoExterns = mempty, _infoLiteralIntToNat, _infoLiteralIntToInt, _infoBuiltins @@ -95,6 +96,7 @@ fromCore Core.InfoTable {..} = _infoInductives = fmap goInductiveInfo _infoInductives, _infoConstructors = fmap goConstructorInfo _infoConstructors, _infoSpecialisations = fmap (map goSpecialisationInfo) _infoSpecialisations, + _infoExterns = mempty, _infoLiteralIntToNat, _infoLiteralIntToInt, _infoBuiltins diff --git a/src/Juvix/Data/Keyword/All.hs b/src/Juvix/Data/Keyword/All.hs index 87a7f93dda..d7fe16b9e2 100644 --- a/src/Juvix/Data/Keyword/All.hs +++ b/src/Juvix/Data/Keyword/All.hs @@ -178,6 +178,9 @@ kwPipe = asciiKw Str.pipe kwType :: Keyword kwType = asciiKw Str.type_ +kwExtern :: Keyword +kwExtern = asciiKw Str.extern + kwTerminating :: Keyword kwTerminating = asciiKw Str.terminating diff --git a/src/Juvix/Extra/Strings.hs b/src/Juvix/Extra/Strings.hs index 3da7226c67..72b2c8e9aa 100644 --- a/src/Juvix/Extra/Strings.hs +++ b/src/Juvix/Extra/Strings.hs @@ -701,6 +701,9 @@ dot = "." colon :: (IsString s) => s colon = ":" +extern :: (IsString s) => s +extern = "extern" + terminating :: (IsString s) => s terminating = "terminating" @@ -1175,6 +1178,9 @@ cairoEcPoint = "ec_point" cairoMkEcPoint :: (IsString s) => s cairoMkEcPoint = "mkEcPoint" +anomaFFI :: (IsString s) => s +anomaFFI = "anoma-ffi" + nockmaNoun :: (IsString s) => s nockmaNoun = "nockma-noun" @@ -1220,6 +1226,9 @@ mkEq = "mkEq" mkOrd :: (IsString s) => s mkOrd = "mkOrd" +mkAnomaFFI :: (IsString s) => s +mkAnomaFFI = "mkAnomaFFI" + rustFn :: (IsString s) => s rustFn = "fn" diff --git a/src/Juvix/Parser/Error.hs b/src/Juvix/Parser/Error.hs index 1606749474..b54babd05b 100644 --- a/src/Juvix/Parser/Error.hs +++ b/src/Juvix/Parser/Error.hs @@ -32,6 +32,7 @@ data ParserError | ErrExpectedDerivingInstance ExpectedDerivingInstanceError | ErrDerivingInstancePatterns DerivingInstancePatternsError | ErrYamlParseError YamlParseError + | ErrExternNotAllowed ExternNotAllowedError | ErrCoercionNotAllowed CoercionNotAllowedError | ErrInstanceNotAllowed InstanceNotAllowedError | ErrExpectedInstance ExpectedInstanceError @@ -57,6 +58,7 @@ instance ToGenericError ParserError where ErrExpectedDerivingInstance e -> genericError e ErrDerivingInstancePatterns e -> genericError e ErrYamlParseError e -> genericError e + ErrExternNotAllowed e -> genericError e ErrCoercionNotAllowed e -> genericError e ErrInstanceNotAllowed e -> genericError e ErrExpectedInstance e -> genericError e @@ -132,6 +134,23 @@ instance ToGenericError ExpectedInstanceError where _genericErrorIntervals = [getLoc e] } +newtype ExternNotAllowedError = ExternNotAllowedError + { _externNotAllowedErrorLoc :: Interval + } + deriving stock (Show) + +instance HasLoc ExternNotAllowedError where + getLoc ExternNotAllowedError {..} = _externNotAllowedErrorLoc + +instance ToGenericError ExternNotAllowedError where + genericError e = + return + GenericError + { _genericErrorLoc = getLoc e, + _genericErrorMessage = mkAnsiText ("'extern' not allowed here" :: Text), + _genericErrorIntervals = [getLoc e] + } + newtype InstanceNotAllowedError = InstanceNotAllowedError { _instanceNotAllowedErrorLoc :: Interval }