{-# LANGUAGE OverloadedStrings #-}

module BNFC.Backend.Agda.Parser (agdaParser) 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.Agda.Utilities.ReservedWords
import BNFC.Backend.Agda.Utilities.Utils
import BNFC.Backend.Haskell.Options (TokenText (..))
import BNFC.Backend.Haskell.Parser (cf2parser)
import BNFC.Backend.Haskell.Utilities.Parser
import BNFC.Backend.Haskell.Utilities.Utils

import Control.Monad.State

import           Data.List       (intersperse)
import qualified Data.Map as Map
import           Data.String     (fromString)

import Prettyprinter
import System.FilePath (takeBaseName)


agdaParser :: LBNF -> State AgdaBackendState Result
agdaParser :: LBNF -> State AgdaBackendState Result
agdaParser 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
      rules :: [(Cat, Map RHS RuleLabel)]
rules       = AgdaBackendState -> [(Cat, Map RHS RuleLabel)]
parserRules AgdaBackendState
st
      rulesCats :: [Cat]
rulesCats   = (Cat, Map RHS RuleLabel) -> Cat
forall a b. (a, b) -> a
fst ((Cat, Map RHS RuleLabel) -> Cat)
-> [(Cat, Map RHS RuleLabel)] -> [Cat]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Cat, Map RHS RuleLabel)]
rules
      astCats :: [String]
astCats     = Type -> String
printTypeName (Type -> String)
-> ((Type, [(Label, [Type])]) -> Type)
-> (Type, [(Label, [Type])])
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Type
avoidResWordsType (Type -> Type)
-> ((Type, [(Label, [Type])]) -> Type)
-> (Type, [(Label, [Type])])
-> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type, [(Label, [Type])]) -> Type
forall a b. (a, b) -> a
fst ((Type, [(Label, [Type])]) -> String)
-> [(Type, [(Label, [Type])])] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AgdaBackendState -> [(Type, [(Label, [Type])])]
agdaAstRules AgdaBackendState
st
      tokenCats :: [String]
tokenCats   = NonEmpty Char -> String
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (NonEmpty Char -> String)
-> ((NonEmpty Char, TokenDef) -> NonEmpty Char)
-> (NonEmpty Char, TokenDef)
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty Char -> NonEmpty Char
avoidAgdaReservedWords (NonEmpty Char -> NonEmpty Char)
-> ((NonEmpty Char, TokenDef) -> NonEmpty Char)
-> (NonEmpty Char, TokenDef)
-> NonEmpty Char
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NonEmpty Char, TokenDef) -> NonEmpty Char
forall a b. (a, b) -> a
fst ((NonEmpty Char, TokenDef) -> String)
-> [(NonEmpty Char, TokenDef)] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AgdaBackendState -> [(NonEmpty Char, TokenDef)]
tokens AgdaBackendState
st
      builtins :: [String]
builtins    = [Cat] -> [BuiltinCat] -> [String]
builtinsToImport [Cat]
rulesCats (Map BuiltinCat (List1 Position) -> [BuiltinCat]
forall k a. Map k a -> [k]
Map.keys (Map BuiltinCat (List1 Position) -> [BuiltinCat])
-> Map BuiltinCat (List1 Position) -> [BuiltinCat]
forall a b. (a -> b) -> a -> b
$ LBNF -> Map BuiltinCat (List1 Position)
_lbnfParserBuiltins LBNF
lbnf)
      categories :: [String]
categories  = [String]
astCats [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
builtins [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
tokenCats
      toks :: [Token]
toks        = AgdaBackendState -> [Token]
lexerParserTokens 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
      funct :: Bool
funct       = AgdaBackendOptions -> Bool
functor (AgdaBackendOptions -> Bool) -> AgdaBackendOptions -> Bool
forall a b. (a -> b) -> a -> b
$ AgdaBackendState -> AgdaBackendOptions
agdaOpts AgdaBackendState
st
      parserAgda :: String
parserAgda  =
        LBNF
-> [Cat] -> [String] -> String -> Bool -> Maybe String -> String
cf2agdaparser LBNF
lbnf [Cat]
rulesCats [String]
categories String
cfName Bool
inDirectory Maybe String
nSpace
      parserHaskell :: String
parserHaskell = LBNF
-> [(Cat, Map RHS RuleLabel)]
-> String
-> Bool
-> Maybe String
-> TokenText
-> [Token]
-> Bool
-> String
cf2parser LBNF
lbnf [(Cat, Map RHS RuleLabel)]
rules String
cfName Bool
inDirectory Maybe String
nSpace TokenText
TextToken [Token]
toks Bool
funct
  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
"Parser" String
"agda", String
parserAgda)
    , (Bool -> Maybe String -> String -> String -> String -> String
mkFilePath Bool
inDirectory Maybe String
nSpace String
cfName String
"Par" String
"y", String
parserHaskell)
    ]

    where
      -- Import builtins which were used as list categories.
      builtinsToImport :: [Cat] -> [BuiltinCat] -> [String]
      builtinsToImport :: [Cat] -> [BuiltinCat] -> [String]
builtinsToImport [Cat]
cats [BuiltinCat]
builtins = let
        builtinsListCats :: [String]
builtinsListCats = Cat -> String
printCatName (Cat -> String) -> [Cat] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Cat -> Bool) -> [Cat] -> [Cat]
forall a. (a -> Bool) -> [a] -> [a]
filter (\Cat
a -> Cat -> Bool
isCatList Cat
a Bool -> Bool -> Bool
&& Cat -> Bool
isCatBuiltin Cat
a) [Cat]
cats
        builtins' :: [String]
builtins' = NonEmpty Char -> String
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (NonEmpty Char -> String)
-> (BuiltinCat -> NonEmpty Char) -> BuiltinCat -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinCat -> NonEmpty Char
printBuiltinCat (BuiltinCat -> String) -> [BuiltinCat] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [BuiltinCat]
builtins
        in (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter (String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
builtinsListCats) [String]
builtins'


cf2agdaparser :: LBNF
              -> [Cat]
              -> [String]
              -> String
              -> Bool
              -> Maybe String
              -> String
cf2agdaparser :: LBNF
-> [Cat] -> [String] -> String -> Bool -> Maybe String -> String
cf2agdaparser LBNF
lbnf [Cat]
rulesCats [String]
categories 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
-> [Cat] -> [String] -> String -> Bool -> Maybe String -> Doc ()
cf2doc LBNF
lbnf [Cat]
rulesCats [String]
categories String
cfName Bool
inDir Maybe String
nameSpace

cf2doc :: LBNF
       -> [Cat]
       -> [String]
       -> String
       -> Bool
       -> Maybe String
       -> Doc ()
cf2doc :: LBNF
-> [Cat] -> [String] -> String -> Bool -> Maybe String -> Doc ()
cf2doc LBNF
lbnf [Cat]
rulesCats [String]
cats String
cfName Bool
inDir Maybe String
nameSpace =
  ([Doc ()] -> Doc ()
forall ann. [Doc ann] -> Doc ann
vsep ([Doc ()] -> Doc ())
-> ([Doc ()] -> [Doc ()]) -> [Doc ()] -> Doc ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc () -> [Doc ()] -> [Doc ()]
forall a. a -> [a] -> [a]
intersperse Doc ()
forall ann. Doc ann
emptyDoc)
    [ Doc ()
header
    , Doc ()
"module" 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 ()
"where"
    , ImportNumeric -> Bool -> Bool -> Bool -> Doc ()
imports ImportNumeric
NoImportNumeric (LBNF -> Bool
layoutsAreUsed LBNF
lbnf) Bool
False Bool
False
    , String -> [String] -> Doc ()
importCats String
agdaASTName [String]
cats
    , Bool -> [String] -> Doc ()
importPragmas Bool
False [String]
mods
    , Doc ()
eitherErr
    , Doc ()
"-- Happy parsers"
    , Maybe String -> [Cat] -> Doc ()
parsers Maybe String
layoutName [Cat]
rulesCats
    ]
  where

    mods :: [ModuleName]
    mods :: [String]
mods = if LBNF -> Bool
layoutsAreUsed LBNF
lbnf
      then [ Bool -> Maybe String -> String -> String -> String
mkModule Bool
inDir Maybe String
nameSpace String
cfName String
"Layout"
           , Bool -> Maybe String -> String -> String -> String
mkModule Bool
inDir Maybe String
nameSpace String
cfName String
"Par"
           ]
      else [ Bool -> Maybe String -> String -> String -> String
mkModule Bool
inDir Maybe String
nameSpace String
cfName String
"Par"]

    layoutName :: Maybe ModuleName
    layoutName :: Maybe String
layoutName = if LBNF -> Bool
layoutsAreUsed LBNF
lbnf
      then String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ Bool -> Maybe String -> String -> String -> String
mkModule Bool
inDir Maybe String
nameSpace String
cfName String
"Layout"
      else Maybe String
forall a. Maybe a
Nothing

    parserName :: ModuleName
    parserName :: String
parserName = Bool -> Maybe String -> String -> String -> String
mkModule Bool
inDir Maybe String
nameSpace String
cfName String
"Parser"

    agdaASTName :: ModuleName
    agdaASTName :: String
agdaASTName = Bool -> Maybe String -> String -> String -> String
mkModule Bool
inDir Maybe String
nameSpace String
cfName String
"AST"


header :: Doc ()
header :: Doc ()
header = [Doc ()] -> Doc ()
forall ann. [Doc ann] -> Doc ann
vsep
  [ Doc ()
"-- File generated by the BNF Converter (bnfc 2.9.4)."
  , Doc ()
forall ann. Doc ann
emptyDoc
  , Doc ()
"-- Agda bindings for the Haskell parsers."
  ]

-- Import categories from Agda AST module.
importCats :: ModuleName -> [String] -> Doc ()
importCats :: String -> [String] -> Doc ()
importCats String
agdaAST [String]
cats = Int -> Doc () -> Doc ()
forall ann. Int -> Doc ann -> Doc ann
hang Int
2 (Doc () -> Doc ()) -> Doc () -> Doc ()
forall a b. (a -> b) -> a -> b
$ [Doc ()] -> Doc ()
forall ann. [Doc ann] -> Doc ann
vsep ([Doc ()] -> Doc ()) -> [Doc ()] -> Doc ()
forall a b. (a -> b) -> a -> b
$
  [Doc ()
"open import" Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> Doc ()
forall a. IsString a => String -> a
fromString String
agdaAST Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"using"]
  [Doc ()] -> [Doc ()] -> [Doc ()]
forall a. [a] -> [a] -> [a]
++
  (String -> String -> Doc ()) -> [String] -> [String] -> [Doc ()]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\String
a String
b -> String -> Doc ()
forall a. IsString a => String -> a
fromString (String -> Doc ()) -> String -> Doc ()
forall a b. (a -> b) -> a -> b
$ String
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
b) (String
"( " String -> [String] -> [String]
forall a. a -> [a] -> [a]
: String -> [String]
forall a. a -> [a]
repeat String
"; ") [String]
cats
  [Doc ()] -> [Doc ()] -> [Doc ()]
forall a. [a] -> [a] -> [a]
++
  [ Doc ()
forall ann. Doc ann
rparen ]

eitherErr :: Doc ()
eitherErr :: Doc ()
eitherErr = [Doc ()] -> Doc ()
forall ann. [Doc ann] -> Doc ann
vsep
  [ Doc ()
"-- Either monad used for error handling"
  , Doc ()
"data HsEither A B : Set where"
  , Doc ()
"  right : B → HsEither A B"
  , Doc ()
"  left : A → HsEither A B"
  , Doc ()
forall ann. Doc ann
emptyDoc
  , Doc ()
"Err : Set → Set"
  , Doc ()
"Err = HsEither (#List Char)"
  , Doc ()
forall ann. Doc ann
emptyDoc
  , Doc ()
"{-# COMPILE GHC HsEither = data Either"
  , Doc ()
"  ( Right"
  , Doc ()
"  | Left"
  , Doc ()
"  ) #-}"
  ]

parsers :: Maybe ModuleName
           -- ^ Grammar uses layout?  If yes, Haskell layout module name.
        -> [Cat]
           -- ^ Bind parsers for these non-terminals.
        -> Doc ()
parsers :: Maybe String -> [Cat] -> Doc ()
parsers Maybe String
layout [Cat]
parserCats = [Doc ()] -> Doc ()
forall ann. [Doc ann] -> Doc ann
vsep
  [ Int -> Doc () -> Doc ()
forall ann. Int -> Doc ann -> Doc ann
hang Int
2 (Doc () -> Doc ()) -> Doc () -> Doc ()
forall a b. (a -> b) -> a -> b
$ [Doc ()] -> Doc ()
forall ann. [Doc ann] -> Doc ann
vsep ([Doc ()] -> Doc ()) -> [Doc ()] -> Doc ()
forall a b. (a -> b) -> a -> b
$ Doc ()
"postulate" Doc () -> [Doc ()] -> [Doc ()]
forall a. a -> [a] -> [a]
: (Cat -> Doc ()
printRule (Cat -> Doc ()) -> [Cat] -> [Doc ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Cat]
parserCats)
  , Doc ()
forall ann. Doc ann
emptyDoc
  , [Doc ()] -> Doc ()
forall ann. [Doc ann] -> Doc ann
vsep ([Doc ()] -> Doc ()) -> [Doc ()] -> Doc ()
forall a b. (a -> b) -> a -> b
$ Cat -> Doc ()
printPragmaBind (Cat -> Doc ()) -> [Cat] -> [Doc ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Cat]
parserCats
  ]

  where
    -- When grammar uses layout, we parametrize the parser by a boolean @tl@
    -- that indicates whether top layout should be used for this parser.
    -- Also, we add @resolveLayout tl@ to the pipeline after lexing.

  printRule :: Cat -> Doc ()
  printRule :: Cat -> Doc ()
printRule Cat
c = if Maybe String -> Bool
forall a. Maybe a -> Bool
isJust Maybe String
layout
    then Cat -> Doc ()
parserBind Cat
c Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
forall ann. Doc ann
colon Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"#Bool → #String → Err" Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Cat -> Doc ()
prCat (Cat -> Cat
avoidResWordsCat Cat
c)
    else Cat -> Doc ()
parserBind Cat
c Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
forall ann. Doc ann
colon Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"#String → Err" Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Cat -> Doc ()
prCat (Cat -> Cat
avoidResWordsCat Cat
c)

  parserBind :: Cat -> Doc ()
  parserBind :: Cat -> Doc ()
parserBind Cat
c = Doc ()
"parse" Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> String -> Doc ()
forall a. IsString a => String -> a
fromString (Cat -> String
printCatNamePrec' (Cat -> String) -> Cat -> String
forall a b. (a -> b) -> a -> b
$ Cat -> Cat
avoidResWordsCat Cat
c)

  prCat :: Cat -> Doc ()
  prCat :: Cat -> Doc ()
prCat Cat
c = if Cat -> Bool
isCatList Cat
c
    then Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
parens (Doc ()
"#List" Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> Doc ()
forall a. IsString a => String -> a
fromString (Cat -> String
printCatName Cat
c))
    else String -> Doc ()
forall a. IsString a => String -> a
fromString (Cat -> String
printCatName Cat
c)

  printPragmaBind :: Cat -> Doc ()
  printPragmaBind :: Cat -> Doc ()
printPragmaBind Cat
c = case Maybe String
layout of
    Maybe String
Nothing -> Doc ()
"{-# COMPILE GHC" Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Cat -> Doc ()
parserBind Cat
c Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"=" Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+>
      Cat -> Doc ()
parserCatName Cat
c Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
". myLexer #-}"
    Just String
layoutMod -> Doc ()
"{-# COMPILE GHC" Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Cat -> Doc ()
parserBind Cat
c Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"= \\ tl ->" Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+>
      Cat -> Doc ()
parserCatName Cat
c Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
forall ann. Doc ann
dot Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> Doc ()
forall a. IsString a => String -> a
fromString String
layoutMod Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
".resolveLayout tl" Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
". myLexer #-}"