parse and scope 'foreign' and 'compile' statements

src/MiniJuvix/Internal/Strings.hs

@@ -95,6 +95,12 @@ mapstoUnicode = "↦"
 mapstoAscii :: IsString s => s
 mapstoAscii = "->"
 
+foreign_ :: IsString s => s
+foreign_ = "foreign"
+
+compile :: IsString s => s
+compile = "compile"
+
 semicolon :: IsString s => s
 semicolon = ";"
 
@@ -118,3 +124,6 @@ colonOne = ":1"
 
 colonZero :: IsString s => s
 colonZero = ":0"
+
+ghc :: IsString s => s
+ghc = "ghc"

src/MiniJuvix/Syntax/Concrete/Language.hs

@@ -72,6 +72,8 @@ data Statement (s :: Stage)
   | StatementAxiom (AxiomDef s)
   | StatementEval (Eval s)
   | StatementPrint (Print s)
+  | StatementForeign ForeignBlock
+  | StatementCompile (CompileDef s)
 
 deriving stock instance
   ( Show (ImportType s),
@@ -103,6 +105,21 @@ deriving stock instance
   ) =>
   Ord (Statement s)
 
+data CompileDef (s :: Stage) = CompileDef {
+  _compileAxiom :: SymbolType s,
+  _compileBackend :: Backend,
+  _compileCode :: Text
+  }
+deriving stock instance (Eq (SymbolType s)) => Eq (CompileDef s)
+deriving stock instance (Ord (SymbolType s)) => Ord (CompileDef s)
+deriving stock instance (Show (SymbolType s)) => Show (CompileDef s)
+
+data ForeignBlock = ForeignBlock {
+  _foreignBackend :: Backend,
+  _foreignCode :: Text
+  }
+  deriving stock (Eq, Ord, Show)
+
 --------------------------------------------------------------------------------
 -- Import statement
 --------------------------------------------------------------------------------
@@ -842,6 +859,13 @@ deriving stock instance
   ) =>
   Ord (LetClause s)
 
+--------------------------------------------------------------------------------
+-- Backends
+--------------------------------------------------------------------------------
+
+data Backend = BackendGhc
+  deriving stock (Show, Eq, Ord)
+
 --------------------------------------------------------------------------------
 -- Debugging statements
 --------------------------------------------------------------------------------
@@ -887,3 +911,5 @@ makeLenses ''TypeSignature
 makeLenses ''AxiomDef
 makeLenses ''FunctionClause
 makeLenses ''InductiveParameter
+makeLenses ''CompileDef
+makeLenses ''ForeignBlock

src/MiniJuvix/Syntax/Concrete/Lexer.hs

@@ -47,6 +47,11 @@ integer = do
     Nothing -> return nat
     _ -> return (- nat)
 
+-- | TODO allow escaping { inside the string using \{
+bracedString :: MonadParsec e Text m => m Text
+bracedString =
+  Text.strip . pack <$> (char '{' >> manyTill anySingle (char '}'))
+
 string :: MonadParsec e Text m => m Text
 string = pack <$> (char '"' >> manyTill L.charLiteral (char '"'))
 
@@ -115,8 +120,10 @@ allKeywords =
     kwColonOmega,
     kwColonOne,
     kwColonZero,
+    kwCompile,
     kwEnd,
     kwEval,
+    kwForeign,
     kwHiding,
     kwImport,
     kwIn,
@@ -181,6 +188,12 @@ kwHiding = symbol Str.hiding
 kwImport :: MonadParsec e Text m => m ()
 kwImport = symbol Str.import_
 
+kwForeign :: MonadParsec e Text m => m ()
+kwForeign = symbol Str.foreign_
+
+kwCompile :: MonadParsec e Text m => m ()
+kwCompile = symbol Str.compile
+
 kwIn :: MonadParsec e Text m => m ()
 kwIn = symbol Str.in_
 
@@ -240,3 +253,6 @@ kwWhere = symbol Str.where_
 
 kwWildcard :: MonadParsec e Text m => m ()
 kwWildcard = symbol Str.underscore
+
+ghc :: MonadParsec e Text m => m ()
+ghc = symbol Str.ghc

src/MiniJuvix/Syntax/Concrete/Parser.hs

@@ -77,12 +77,36 @@ statement =
     <|> (StatementImport <$> import_)
     <|> (StatementInductive <$> inductiveDef)
     <|> (StatementPrint <$> printS)
+    <|> (StatementForeign <$> foreignBlock)
+    <|> (StatementCompile <$> compileDef)
     <|> (StatementModule <$> moduleDef)
     <|> (StatementAxiom <$> axiomDef)
     <|> ( either StatementTypeSignature StatementFunctionClause
             <$> auxTypeSigFunClause
         )
 
+--------------------------------------------------------------------------------
+-- Foreign and compile
+--------------------------------------------------------------------------------
+
+backend :: forall e m. MonadParsec e Text m => m Backend
+backend = ghc $> BackendGhc
+
+foreignBlock :: forall e m. MonadParsec e Text m => m ForeignBlock
+foreignBlock = do
+  kwForeign
+  _foreignBackend <- backend
+  _foreignCode <- bracedString
+  return ForeignBlock {..}
+
+compileDef :: forall e m. MonadParsec e Text m => m (CompileDef 'Parsed)
+compileDef = do
+  kwCompile
+  _compileAxiom <- symbol
+  _compileBackend <- backend
+  _compileCode <- string
+  return CompileDef {..}
+
 --------------------------------------------------------------------------------
 -- Operator syntax declaration
 --------------------------------------------------------------------------------

src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Base.hs

@@ -64,6 +64,9 @@ kwMatch = keyword Str.match
 kwLambda :: Doc Ann
 kwLambda = keyword Str.lambdaUnicode
 
+kwGhc :: Doc Ann
+kwGhc = keyword Str.ghc
+
 kwWhere :: Doc Ann
 kwWhere = keyword Str.where_
 
@@ -130,6 +133,12 @@ kwImport = keyword Str.import_
 kwSemicolon :: Doc Ann
 kwSemicolon = delimiter Str.semicolon
 
+kwCompile :: Doc Ann
+kwCompile = keyword Str.compile
+
+kwForeign :: Doc Ann
+kwForeign = keyword Str.foreign_
+
 kwBraceL :: Doc Ann
 kwBraceL = delimiter "{"
 
@@ -198,6 +207,9 @@ groupStatements = reverse . map reverse . uncurry cons . foldl' aux ([], [])
   -- blank line
   g :: Statement s -> Statement s -> Bool
   g a b = case (a, b) of
+    (StatementCompile _, StatementCompile _) -> True
+    (StatementCompile _, _) -> False
+    (StatementForeign _, _) -> False
     (StatementOperator _, StatementOperator _) -> True
     (StatementOperator o, s) -> definesSymbol (opSymbol o) s
     (StatementImport _, StatementImport _) -> True
@@ -261,6 +273,28 @@ instance SingI s => PrettyCode (Statement s) where
     StatementAxiom a -> ppCode a
     StatementEval e -> ppCode e
     StatementPrint p -> ppCode p
+    StatementCompile p -> ppCode p
+    StatementForeign p -> ppCode p
+
+instance PrettyCode Backend where
+  ppCode = \case
+    BackendGhc -> return kwGhc
+
+instance PrettyCode ForeignBlock where
+  ppCode ForeignBlock {..} = do
+    _foreignBackend' <- ppCode _foreignBackend
+    return $ kwForeign <+> _foreignBackend' <+> lbrace <> line
+        <> pretty _foreignCode <> line <> rbrace
+
+instance SingI s => PrettyCode (CompileDef s) where
+  ppCode CompileDef {..} = do
+    _compileAxiom' <- ppSymbol _compileAxiom
+    _compileBackend' <- ppCode _compileBackend
+    _compileBackend' <- ppCode _compileBackend
+    return $ kwCompile <+> _compileAxiom' <+> _compileBackend' <+> ppStringLit _compileCode
+
+ppStringLit :: Text -> Doc Ann
+ppStringLit = annotate AnnLiteralString . doubleQuotes . pretty
 
 ppTopModulePath :: forall s r. (SingI s, Members '[Reader Options] r) =>
   ModulePathType s 'ModuleTop -> Sem r (Doc Ann)
@@ -608,7 +642,7 @@ instance PrettyCode Application where
 instance PrettyCode Literal where
   ppCode l = case l of
     LitInteger n -> return $ annotate AnnLiteralInteger (pretty n)
-    LitString s -> return $ annotate AnnLiteralString (doubleQuotes (pretty s))
+    LitString s -> return $ ppStringLit s
 
 instance PrettyCode Expression where
   ppCode e = case e of

src/MiniJuvix/Syntax/Concrete/Scoped/Scoper.hs

@@ -658,7 +658,7 @@ checkFunctionClause ::
   FunctionClause 'Parsed ->
   Sem r (FunctionClause 'Scoped)
 checkFunctionClause clause@FunctionClause {..} = do
-  clauseOwnerFunction' <- checkSymbolInScope
+  clauseOwnerFunction' <- checkTypeSigInScope
   (clausePatterns', clauseWhere', clauseBody') <- do
     clp <- mapM checkParsePatternAtom _clausePatterns
     withBindCurrentGroup $ do
@@ -676,18 +676,36 @@ checkFunctionClause clause@FunctionClause {..} = do
       }
   where
     fun = _clauseOwnerFunction
-    checkSymbolInScope :: Sem r S.Symbol
-    checkSymbolInScope = do
-      SymbolInfo {..} <- fromMaybeM err (HashMap.lookup fun <$> gets _scopeSymbols)
-      -- The symbol must be defined in the same path
-      path <- gets _scopePath
-      e <- maybe err return (HashMap.lookup path _symbolInfo)
+    checkTypeSigInScope :: Sem r S.Symbol
+    checkTypeSigInScope = do
+      e <- fromMaybeM err (lookupLocalEntry fun)
       when (S._nameKind e /= S.KNameFunction) err
       return (entryToSName fun e)
       where
         err :: Sem r a
         err = throw (ErrLacksTypeSig (LacksTypeSig clause))
 
+lookupAxiom :: forall r.  Members '[Error ScopeError, State Scope, State ScoperState] r =>
+  Symbol -> Sem r S.Symbol
+lookupAxiom ax = do
+  e <- fromMaybeM err (lookupLocalEntry ax)
+  when (S._nameKind e /= S.KNameAxiom) err
+  return (entryToSName ax e)
+  where
+    -- TODO generate proper error
+    err :: Sem r a
+    err = throw (ErrGeneric "Axiom not in scope")
+
+lookupLocalEntry :: Members '[Error ScopeError, State Scope, State ScoperState] r =>
+  Symbol -> Sem r (Maybe SymbolEntry)
+lookupLocalEntry sym = do
+  ms <- HashMap.lookup sym <$> gets _scopeSymbols
+  path <- gets _scopePath
+  -- The symbol must be defined in the same path
+  return $ do
+    SymbolInfo {..} <- ms
+    HashMap.lookup path _symbolInfo
+
 checkAxiom ::
   Members '[Error ScopeError, State Scope, State ScoperState] r =>
   AxiomDef 'Parsed ->
@@ -983,6 +1001,16 @@ checkParsePatternAtom ::
   Sem r Pattern
 checkParsePatternAtom = checkPatternAtom >=> parsePatternAtom
 
+checkCompileDef ::
+  Members '[Error ScopeError, State Scope, State ScoperState] r =>
+  CompileDef 'Parsed ->
+  Sem r (CompileDef 'Scoped)
+checkCompileDef CompileDef {..} = do
+  _compileAxiom' <- lookupAxiom _compileAxiom
+  return CompileDef {
+    _compileAxiom = _compileAxiom', ..
+    }
+
 checkStatement ::
   Members '[Error ScopeError, Reader ScopeParameters, Files, State Scope, State ScoperState, Reader LocalVars] r =>
   Statement 'Parsed ->
@@ -998,6 +1026,8 @@ checkStatement s = case s of
   StatementAxiom ax -> StatementAxiom <$> checkAxiom ax
   StatementEval e -> StatementEval <$> checkEval e
   StatementPrint e -> StatementPrint <$> checkPrint e
+  StatementCompile d -> StatementCompile <$> checkCompileDef d
+  StatementForeign d -> return $ StatementForeign d
 
 -------------------------------------------------------------------------------
 -- Infix Expression

tests/positive/HelloWorld.mjuvix

@@ -0,0 +1,30 @@
+module HelloWorld;
+
+-- the foreign keyword has two arguments:
+-- 1. The name of the backend. Only ghc is available now.
+-- 2. A string. For ease of use, the string is given between braces
+-- and can have multiple lines. Space at the beginning and at the end is ignored.
+-- The given code is inlined verbatim when compiling to the given backend.
+
+foreign ghc {
+
+import Data.Text
+import Data.Text.IO
+
+};
+
+axiom Action : Type;
+axiom String : Type;
+axiom putStr : String -> Action;
+
+-- the compile keyword has three arguments:
+-- 1. The name of the MiniJuvix Axiom.
+-- 2. The name of the backend.
+-- 3. The thing we should inline when compiling this
+-- axiom to the given backend.
+compile Action ghc "IO ()";
+
+main : Action;
+main := putStr "hello world";
+
+end;