{-# 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)

    -- Top parser.
    firstCat :: Cat
    firstCat :: Cat
firstCat = [Cat] -> Cat
forall a. [a] -> a
head [Cat]
entrypoints

    -- Entrypoints sorted according to their declaration order in the grammar file.
    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)

    -- Agda module names.
    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"