Foreign Function Interface

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

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 ()

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

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

src/Juvix/Compiler/Concrete/Keywords.hs

@@ -40,6 +40,7 @@ import Juvix.Data.Keyword.All
     kwElse,
     kwEnd,
     kwEq,
+    kwExtern,
     kwFixity,
     kwHiding,
     kwHole,

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

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 "<top level statement>" $ 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 "<function definition>" $ 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 "<function definition>" $ 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 <-

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
       }

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

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

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"
 

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

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

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
 

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

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

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 =