{-# LANGUAGE OverloadedStrings #-}
module BNFC.Backend.Agda.Main (agdaMain) where
import BNFC.CF
import BNFC.Options.GlobalOptions
import BNFC.Prelude
import BNFC.Backend.CommonInterface.Backend
import BNFC.Backend.Common.Utils as Utils
import BNFC.Backend.Agda.Options
import BNFC.Backend.Agda.State
import BNFC.Backend.Haskell.Utilities.Utils
import Control.Monad.State
import qualified Data.Map as Map
import Data.List (sortBy)
import Data.String (fromString)
import Prettyprinter
import System.FilePath (takeBaseName)
agdaMain :: LBNF -> State AgdaBackendState Result
agdaMain :: LBNF -> State AgdaBackendState Result
agdaMain LBNF
lbnf = do
AgdaBackendState
st <- StateT AgdaBackendState Identity AgdaBackendState
forall s (m :: * -> *). MonadState s m => m s
get
let
cfName :: String
cfName = String -> String
takeBaseName (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ GlobalOptions -> String
optInput (GlobalOptions -> String) -> GlobalOptions -> String
forall a b. (a -> b) -> a -> b
$ AgdaBackendState -> GlobalOptions
globalOpt AgdaBackendState
st
inDirectory :: Bool
inDirectory = AgdaBackendOptions -> Bool
inDir (AgdaBackendOptions -> Bool) -> AgdaBackendOptions -> Bool
forall a b. (a -> b) -> a -> b
$ AgdaBackendState -> AgdaBackendOptions
agdaOpts AgdaBackendState
st
nSpace :: Maybe String
nSpace = AgdaBackendOptions -> Maybe String
nameSpace (AgdaBackendOptions -> Maybe String)
-> AgdaBackendOptions -> Maybe String
forall a b. (a -> b) -> a -> b
$ AgdaBackendState -> AgdaBackendOptions
agdaOpts AgdaBackendState
st
main :: String
main = LBNF -> String -> Bool -> Maybe String -> String
cf2main LBNF
lbnf String
cfName Bool
inDirectory Maybe String
nSpace
Result -> State AgdaBackendState Result
forall (m :: * -> *) a. Monad m => a -> m a
return [(Bool -> Maybe String -> String -> String -> String -> String
mkFilePath Bool
inDirectory Maybe String
nSpace String
cfName String
"Main" String
"agda", String
main)]
cf2main :: LBNF -> String -> Bool -> Maybe String -> String
cf2main :: LBNF -> String -> Bool -> Maybe String -> String
cf2main LBNF
lbnf String
cfName Bool
inDir Maybe String
nameSpace =
LayoutOptions -> Doc () -> String
docToString LayoutOptions
defaultLayoutOptions (Doc () -> String) -> Doc () -> String
forall a b. (a -> b) -> a -> b
$ LBNF -> String -> Bool -> Maybe String -> Doc ()
cf2doc LBNF
lbnf String
cfName Bool
inDir Maybe String
nameSpace
cf2doc :: LBNF -> String -> Bool -> Maybe String -> Doc ()
cf2doc :: LBNF -> String -> Bool -> Maybe String -> Doc ()
cf2doc LBNF
lbnf String
cfName Bool
inDir Maybe String
nameSpace = [Doc ()] -> Doc ()
forall ann. [Doc ann] -> Doc ann
vsep ([Doc ()] -> Doc ()) -> [Doc ()] -> Doc ()
forall a b. (a -> b) -> a -> b
$ [[Doc ()]] -> [Doc ()]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[ [ Doc ()
"-- File generated by the BNF Converter."
, Doc ()
forall ann. Doc ann
emptyDoc
, Doc ()
"-- Test for Agda binding of parser. Requires Agda >= 2.5.4."
, Doc ()
forall ann. Doc ann
emptyDoc
]
, [Doc ()
"module" Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> Doc ()
forall a. IsString a => String -> a
fromString String
mainName Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"where"
, Doc ()
forall ann. Doc ann
emptyDoc
]
, Bool -> [Doc ()] -> [Doc ()]
forall m. Monoid m => Bool -> m -> m
Utils.when (LBNF -> Bool
layoutsAreUsed LBNF
lbnf) [ Doc ()
"open import Agda.Builtin.Bool using (true)" ]
, [ Doc ()
"open import" Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> Doc ()
forall a. IsString a => String -> a
fromString String
ioLibName
, Doc ()
"open import" Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> Doc ()
forall a. IsString a => String -> a
fromString String
astName Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"using" Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
parens Doc ()
printFun
, Doc ()
"open import" Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> Doc ()
forall a. IsString a => String -> a
fromString String
parserName Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"using" Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+>
Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
parens ([Doc ()] -> Doc ()
forall ann. [Doc ann] -> Doc ann
hsep [Doc ()
"HsEither;", Doc ()
parseFun])
, Doc ()
forall ann. Doc ann
emptyDoc
, Doc ()
"main : IO ⊤"
, Doc ()
"main = do"
, Doc ()
" file ∷ [] ← getArgs where"
, Doc ()
" _ → do"
, Doc ()
" putStrLn \"usage: Main <SourceFile>\""
, Doc ()
" exitFailure"
, Doc ()
" HsEither.right result ←" Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+>
(if LBNF -> Bool
layoutsAreUsed LBNF
lbnf
then Doc ()
parseFun Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"true"
else Doc ()
parseFun)
Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"<$> readFiniteFile file where"
, Doc ()
" HsEither.left msg → do"
, Doc ()
" putStrLn \"PARSE FAILED\\n\""
, Doc ()
" putStrLn (stringFromList msg)"
, Doc ()
" exitFailure"
, Doc ()
" putStrLn \"PARSE SUCCESSFUL\\n\""
, Doc ()
" putStrLn" Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
parens (Doc ()
printFun Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"result")
]
]
where
parseFun :: Doc ()
parseFun :: Doc ()
parseFun = Doc ()
"parse" Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> String -> Doc ()
forall a. IsString a => String -> a
fromString (Cat -> String
printCatName Cat
firstCat)
printFun :: Doc ()
printFun :: Doc ()
printFun = Doc ()
"print" Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> String -> Doc ()
forall a. IsString a => String -> a
fromString (Cat -> String
printCatName Cat
firstCat)
firstCat :: Cat
firstCat :: Cat
firstCat = [Cat] -> Cat
forall a. [a] -> a
head [Cat]
entrypoints
entrypoints :: [Cat]
entrypoints :: [Cat]
entrypoints = (Cat, List1 Position) -> Cat
forall a b. (a, b) -> a
fst ((Cat, List1 Position) -> Cat) -> [(Cat, List1 Position)] -> [Cat]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Cat, List1 Position) -> (Cat, List1 Position) -> Ordering)
-> [(Cat, List1 Position)] -> [(Cat, List1 Position)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (List1 Position -> List1 Position -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (List1 Position -> List1 Position -> Ordering)
-> ((Cat, List1 Position) -> List1 Position)
-> (Cat, List1 Position)
-> (Cat, List1 Position)
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Cat, List1 Position) -> List1 Position
forall a b. (a, b) -> b
snd) (Map Cat (List1 Position) -> [(Cat, List1 Position)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map Cat (List1 Position) -> [(Cat, List1 Position)])
-> Map Cat (List1 Position) -> [(Cat, List1 Position)]
forall a b. (a -> b) -> a -> b
$ LBNF -> Map Cat (List1 Position)
_lbnfEntryPoints LBNF
lbnf)
astName :: ModuleName
astName :: String
astName = Bool -> Maybe String -> String -> String -> String
mkModule Bool
inDir Maybe String
nameSpace String
cfName String
"AST"
ioLibName :: ModuleName
ioLibName :: String
ioLibName = Bool -> Maybe String -> String -> String -> String
mkModule Bool
inDir Maybe String
nameSpace String
cfName String
"IOLib"
mainName :: ModuleName
mainName :: String
mainName = Bool -> Maybe String -> String -> String -> String
mkModule Bool
inDir Maybe String
nameSpace String
cfName String
"Main"
parserName :: ModuleName
parserName :: String
parserName = Bool -> Maybe String -> String -> String -> String
mkModule Bool
inDir Maybe String
nameSpace String
cfName String
"Parser"