[parser] Remove agda backend code (#86)

src/MiniJuvix/Internal/Strings.hs

@@ -155,9 +155,6 @@ colonZero = ":0"
 ghc :: IsString s => s
 ghc = "ghc"
 
-agda :: IsString s => s
-agda = "agda"
-
 cBackend :: IsString s => s
 cBackend = "c"
 

src/MiniJuvix/Syntax/Backends.hs

@@ -2,7 +2,7 @@ module MiniJuvix.Syntax.Backends where
 
 import MiniJuvix.Prelude
 
-data Backend = BackendGhc | BackendAgda | BackendC
+data Backend = BackendGhc | BackendC
   deriving stock (Show, Eq, Ord, Generic)
 
 instance Hashable Backend

src/MiniJuvix/Syntax/Concrete/Lexer.hs

@@ -275,8 +275,5 @@ kwWildcard = keyword Str.underscore
 ghc :: Member InfoTableBuilder r => ParsecS r ()
 ghc = keyword Str.ghc
 
-agda :: Member InfoTableBuilder r => ParsecS r ()
-agda = keyword Str.agda
-
 cBackend :: Member InfoTableBuilder r => ParsecS r ()
 cBackend = keyword Str.cBackend

src/MiniJuvix/Syntax/Concrete/Parser.hs

@@ -140,10 +140,7 @@ compileBlock = do
 --------------------------------------------------------------------------------
 
 backend :: Member InfoTableBuilder r => ParsecS r Backend
-backend =
-  ghc $> BackendGhc
-    <|> agda $> BackendAgda
-    <|> cBackend $> BackendC
+backend = ghc $> BackendGhc <|> cBackend $> BackendC
 
 foreignBlock :: Member InfoTableBuilder r => ParsecS r ForeignBlock
 foreignBlock = do

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

@@ -62,9 +62,6 @@ kwLambda = keyword Str.lambdaUnicode
 kwGhc :: Doc Ann
 kwGhc = keyword Str.ghc
 
-kwAgda :: Doc Ann
-kwAgda = keyword Str.agda
-
 kwC :: Doc Ann
 kwC = keyword Str.cBackend
 
@@ -288,7 +285,6 @@ instance SingI s => PrettyCode (Statement s) where
 instance PrettyCode Backend where
   ppCode = \case
     BackendGhc -> return kwGhc
-    BackendAgda -> return kwAgda
     BackendC -> return kwC
 
 instance SingI s => PrettyCode (Compile s) where

src/MiniJuvix/Syntax/MicroJuvix/Pretty/Base.hs

@@ -96,9 +96,6 @@ kwForeign = keyword Str.foreign_
 kwCompile :: Doc Ann
 kwCompile = keyword Str.compile
 
-kwAgda :: Doc Ann
-kwAgda = keyword Str.agda
-
 kwC :: Doc Ann
 kwC = keyword Str.cBackend
 
@@ -247,7 +244,6 @@ instance PrettyCode FunctionClause where
 instance PrettyCode Backend where
   ppCode = \case
     BackendGhc -> return kwGhc
-    BackendAgda -> return kwAgda
     BackendC -> return kwC
 
 instance PrettyCode ForeignBlock where

src/MiniJuvix/Syntax/MonoJuvix/Pretty/Base.hs

@@ -76,9 +76,6 @@ kwForeign = keyword Str.foreign_
 kwCompile :: Doc Ann
 kwCompile = keyword Str.compile
 
-kwAgda :: Doc Ann
-kwAgda = keyword Str.agda
-
 kwC :: Doc Ann
 kwC = keyword Str.cBackend
 
@@ -199,7 +196,6 @@ instance PrettyCode FunctionClause where
 instance PrettyCode Backend where
   ppCode = \case
     BackendGhc -> return kwGhc
-    BackendAgda -> return kwAgda
     BackendC -> return kwC
 
 instance PrettyCode ForeignBlock where

tests/positive/Foreign.mjuvix

@@ -4,7 +4,7 @@ foreign ghc {};
 
 foreign ghc { import Foo.Bar };
 
-foreign agda { import Foo.Bar };
+foreign c { import Foo.Bar };
 
 foreign ghc { import Foo.Bar
   import Foo.Baz };