[parser] add parser / pretty for axiom backends

src/MiniJuvix/Internal/Strings.hs

@@ -127,3 +127,6 @@ colonZero = ":0"
 
 ghc :: IsString s => s
 ghc = "ghc"
+
+agda :: IsString s => s
+agda = "agda"

src/MiniJuvix/Syntax/Abstract/Language.hs

@@ -5,7 +5,7 @@ module MiniJuvix.Syntax.Abstract.Language
 where
 
 import MiniJuvix.Prelude
-import MiniJuvix.Syntax.Concrete.Language (ForeignBlock (..), Literal (..), Usage)
+import MiniJuvix.Syntax.Concrete.Language (ForeignBlock (..), Literal (..), Usage, BackendItem)
 import qualified MiniJuvix.Syntax.Concrete.Name as C
 import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
 import MiniJuvix.Syntax.Fixity
@@ -162,7 +162,8 @@ data InductiveConstructorDef = InductiveConstructorDef
 
 data AxiomDef = AxiomDef
   { _axiomName :: AxiomName,
-    _axiomType :: Expression
+    _axiomType :: Expression,
+    _axiomBackendItems :: [BackendItem]
   }
   deriving stock (Show, Eq)
 

src/MiniJuvix/Syntax/Concrete/Language.hs

@@ -90,7 +90,6 @@ data Statement (s :: Stage)
   | StatementEval (Eval s)
   | StatementPrint (Print s)
   | StatementForeign ForeignBlock
-  | StatementCompile (CompileDef s)
 
 deriving stock instance
   ( Show (ImportType s),
@@ -125,18 +124,6 @@ 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
@@ -194,7 +181,8 @@ deriving stock instance (Ord (ExpressionType s), Ord (SymbolType s)) => Ord (Typ
 
 data AxiomDef (s :: Stage) = AxiomDef
   { _axiomName :: SymbolType s,
-    _axiomType :: ExpressionType s
+    _axiomType :: ExpressionType s,
+    _axiomBackendItems :: [BackendItem]
   }
 
 deriving stock instance (Show (ExpressionType s), Show (SymbolType s)) => Show (AxiomDef s)
@@ -1061,7 +1049,13 @@ deriving stock instance
 -- Backends
 --------------------------------------------------------------------------------
 
-data Backend = BackendGhc
+data Backend = BackendGhc | BackendAgda
+  deriving stock (Show, Eq, Ord)
+
+data BackendItem = BackendItem
+  { _backendItemBackend :: Backend,
+    _backendItemCode :: Text
+  }
   deriving stock (Show, Eq, Ord)
 
 --------------------------------------------------------------------------------
@@ -1109,7 +1103,6 @@ makeLenses ''TypeSignature
 makeLenses ''AxiomDef
 makeLenses ''FunctionClause
 makeLenses ''InductiveParameter
-makeLenses ''CompileDef
 makeLenses ''ForeignBlock
 makeLenses ''AxiomRef'
 makeLenses ''InductiveRef'
@@ -1117,6 +1110,7 @@ makeLenses ''ModuleRef'
 makeLenses ''ModuleRef''
 makeLenses ''FunctionRef'
 makeLenses ''ConstructorRef'
+makeLenses ''BackendItem
 
 idenOverName :: (forall s. S.Name' s -> S.Name' s) -> ScopedIden -> ScopedIden
 idenOverName f = \case

src/MiniJuvix/Syntax/Concrete/Lexer.hs

@@ -50,7 +50,7 @@ integer = do
 -- | TODO allow escaping { inside the string using \{
 bracedString :: MonadParsec e Text m => m Text
 bracedString =
-  Text.strip . pack <$> (char '{' >> manyTill anySingle (char '}'))
+  pack <$> (char '{' >> manyTill anySingle (char '}'))
 
 string :: MonadParsec e Text m => m Text
 string = pack <$> (char '"' >> manyTill L.charLiteral (char '"'))
@@ -256,3 +256,6 @@ kwWildcard = symbol Str.underscore
 
 ghc :: MonadParsec e Text m => m ()
 ghc = symbol Str.ghc
+
+agda :: MonadParsec e Text m => m ()
+agda = symbol Str.agda

src/MiniJuvix/Syntax/Concrete/Parser.hs

@@ -78,7 +78,6 @@ statement =
     <|> (StatementInductive <$> inductiveDef)
     <|> (StatementPrint <$> printS)
     <|> (StatementForeign <$> foreignBlock)
-    <|> (StatementCompile <$> compileDef)
     <|> (StatementModule <$> moduleDef)
     <|> (StatementAxiom <$> axiomDef)
     <|> ( either StatementTypeSignature StatementFunctionClause
@@ -86,11 +85,12 @@ statement =
         )
 
 --------------------------------------------------------------------------------
--- Foreign and compile
+-- Foreign
 --------------------------------------------------------------------------------
 
 backend :: forall e m. MonadParsec e Text m => m Backend
 backend = ghc $> BackendGhc
+  <|> agda $> BackendAgda
 
 foreignBlock :: forall e m. MonadParsec e Text m => m ForeignBlock
 foreignBlock = do
@@ -99,14 +99,6 @@ foreignBlock = do
   _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
 --------------------------------------------------------------------------------
@@ -250,7 +242,15 @@ axiomDef = do
   _axiomName <- symbol
   kwColon
   _axiomType <- expressionAtoms
+  _axiomBackendItems <- fromMaybe [] <$> optional backends
   return AxiomDef {..}
+  where
+    backends = toList <$> braces (P.sepEndBy1 backendItem kwSemicolon)
+    backendItem = do
+      _backendItemBackend <- backend
+      kwMapsTo
+      _backendItemCode <- string
+      return BackendItem {..}
 
 --------------------------------------------------------------------------------
 -- Function expression

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

@@ -66,6 +66,9 @@ kwLambda = keyword Str.lambdaUnicode
 kwGhc :: Doc Ann
 kwGhc = keyword Str.ghc
 
+kwAgda :: Doc Ann
+kwAgda = keyword Str.agda
+
 kwWhere :: Doc Ann
 kwWhere = keyword Str.where_
 
@@ -211,8 +214,6 @@ 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
@@ -278,28 +279,26 @@ 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
+    BackendAgda -> return kwAgda
 
 instance PrettyCode ForeignBlock where
   ppCode ForeignBlock {..} = do
     _foreignBackend' <- ppCode _foreignBackend
     return $
-      kwForeign <+> _foreignBackend' <+> lbrace <> line
+      kwForeign <+> _foreignBackend' <+> lbrace
         <> 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
+instance PrettyCode BackendItem where
+  ppCode BackendItem {..} = do
+    backend <- ppCode _backendItemBackend
+    return $
+      backend <+> kwMapsto <+> ppStringLit _backendItemCode
 
 ppStringLit :: Text -> Doc Ann
 ppStringLit = annotate AnnLiteralString . doubleQuotes . pretty
@@ -587,7 +586,10 @@ instance SingI s => PrettyCode (AxiomDef s) where
   ppCode AxiomDef {..} = do
     axiomName' <- ppSymbol _axiomName
     axiomType' <- ppExpression _axiomType
-    return $ kwAxiom <+> axiomName' <+> kwColon <+> axiomType'
+    axiomBackendItems' <- case _axiomBackendItems of
+      [] -> return Nothing
+      bs -> Just <$> ppBlock bs
+    return $ kwAxiom <+> axiomName' <+> kwColon <+> axiomType' <+?> axiomBackendItems'
 
 instance SingI s => PrettyCode (Eval s) where
   ppCode (Eval p) = do

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

@@ -770,7 +770,8 @@ checkAxiomDef AxiomDef {..} = do
   return
     AxiomDef
       { _axiomName = axiomName',
-        _axiomType = axiomType'
+        _axiomType = axiomType',
+        ..
       }
 
 localScope :: Sem (Reader LocalVars : r) a -> Sem r a
@@ -1081,7 +1082,6 @@ checkStatement s = case s of
   StatementAxiom ax -> StatementAxiom <$> checkAxiomDef ax
   StatementEval e -> StatementEval <$> checkEval e
   StatementPrint e -> StatementPrint <$> checkPrint e
-  StatementCompile {} -> undefined
   StatementForeign d -> return $ StatementForeign d
 
 -------------------------------------------------------------------------------

src/MiniJuvix/Translation/ScopedToAbstract.hs

@@ -231,4 +231,6 @@ goPattern p = case p of
   PatternEmpty -> return A.PatternEmpty
 
 goAxiom :: Members '[Error Err] r => AxiomDef 'Scoped -> Sem r A.AxiomDef
-goAxiom (AxiomDef n m) = A.AxiomDef n <$> goExpression m
+goAxiom (AxiomDef n m bs) = do
+  e <- goExpression m
+  return (A.AxiomDef n e bs)

test/Scope/Positive.hs

@@ -73,4 +73,6 @@ tests = [
      "." "Operators.mjuvix"
   , PosTest "Literals"
      "." "Literals.mjuvix"
+  , PosTest "Hello World backends"
+     "." "HelloWorld.mjuvix"
  ]