{-# LANGUAGE OverloadedStrings #-}

module BNFC.Backend.Agda.Makefile where

import BNFC.Prelude

import Control.Monad.State

import Data.List       (intersperse)

import Prettyprinter
import Prettyprinter.Render.String

import System.FilePath (dropExtension, takeBaseName, (</>), (<.>))

import BNFC.Backend.CommonInterface.Backend ( Result )

import BNFC.Backend.Agda.Options
import BNFC.Backend.Agda.State

import BNFC.Backend.Common.Makefile
import BNFC.Backend.Common.Utils as Utils
import BNFC.Backend.Common.StringUtils

import BNFC.Backend.Haskell.Utilities.Utils

import BNFC.CF
import BNFC.Options.GlobalOptions


agdaMakefile :: LBNF -> State AgdaBackendState Result
agdaMakefile :: LBNF -> State AgdaBackendState Result
agdaMakefile LBNF
lbnf = do
  AgdaBackendState
st <- StateT AgdaBackendState Identity AgdaBackendState
forall s (m :: * -> *). MonadState s m => m s
get
  let
    opts :: AgdaBackendOptions
opts          = AgdaBackendState -> AgdaBackendOptions
agdaOpts AgdaBackendState
st
    force :: Bool
force         = GlobalOptions -> Bool
optForce (GlobalOptions -> Bool) -> GlobalOptions -> Bool
forall a b. (a -> b) -> a -> b
$ AgdaBackendState -> GlobalOptions
globalOpt AgdaBackendState
st
    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
    pathToGrammar :: String
pathToGrammar = GlobalOptions -> String
optInput (GlobalOptions -> String) -> GlobalOptions -> String
forall a b. (a -> b) -> a -> b
$ AgdaBackendState -> GlobalOptions
globalOpt AgdaBackendState
st
    outDir :: Maybe String
outDir        = GlobalOptions -> Maybe String
optOutDir (GlobalOptions -> Maybe String) -> GlobalOptions -> Maybe String
forall a b. (a -> b) -> a -> b
$ AgdaBackendState -> GlobalOptions
globalOpt AgdaBackendState
st
  Result -> State AgdaBackendState Result
forall (m :: * -> *) a. Monad m => a -> m a
return [(String
"Makefile", LBNF
-> AgdaBackendOptions
-> Bool
-> String
-> Maybe String
-> String
-> String
cf2makefile LBNF
lbnf AgdaBackendOptions
opts Bool
force String
cfName Maybe String
outDir String
pathToGrammar)]

cf2makefile :: LBNF
            -> AgdaBackendOptions
            -> Bool
            -> String
            -> Maybe FilePath
            -> FilePath
            -> String
cf2makefile :: LBNF
-> AgdaBackendOptions
-> Bool
-> String
-> Maybe String
-> String
-> String
cf2makefile LBNF
lbnf AgdaBackendOptions
agdaOpts Bool
force String
cfName Maybe String
outDir String
pathToGrammar  =
  SimpleDocStream () -> String
forall ann. SimpleDocStream ann -> String
renderString (SimpleDocStream () -> String)
-> (Doc () -> SimpleDocStream ()) -> Doc () -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LayoutOptions -> Doc () -> SimpleDocStream ()
forall ann. LayoutOptions -> Doc ann -> SimpleDocStream ann
layoutSmart LayoutOptions
defaultLayoutOptions (Doc () -> String) -> Doc () -> String
forall a b. (a -> b) -> a -> b
$
    LBNF
-> AgdaBackendOptions
-> Bool
-> String
-> Maybe String
-> String
-> Doc ()
makefileDoc LBNF
lbnf AgdaBackendOptions
agdaOpts Bool
force String
cfName Maybe String
outDir String
pathToGrammar

makefileDoc :: LBNF
            -> AgdaBackendOptions
            -> Bool
            -> String
            -> Maybe FilePath
            -> FilePath
            -> Doc ()
makefileDoc :: LBNF
-> AgdaBackendOptions
-> Bool
-> String
-> Maybe String
-> String
-> Doc ()
makefileDoc LBNF
lbnf AgdaBackendOptions
agdaOpts Bool
force String
cfName Maybe String
outDir String
pathToGrammar =
  [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 ()] -> Doc ()) -> [Doc ()] -> Doc ()
forall a b. (a -> b) -> a -> b
$
  [ Doc ()
header
  , Doc ()
phonyRule
  , Doc ()
defaultRule
  , Doc ()
"# Rules for building the parser."
  ]
  [Doc ()] -> [Doc ()] -> [Doc ()]
forall a. [a] -> [a] -> [a]
++
  Bool -> [Doc ()] -> [Doc ()]
forall m. Monoid m => Bool -> m -> m
Utils.when (Maybe String -> Bool
forall a. Maybe a -> Bool
isNothing Maybe String
outDir) [ Doc ()
bnfcRule ]
  [Doc ()] -> [Doc ()] -> [Doc ()]
forall a. [a] -> [a] -> [a]
++
  [ Doc ()
happyRule
  , Doc ()
alexRule
  , Doc ()
testParserRule
  , Doc ()
mainRule
  , Doc ()
"# Rules for cleaning generated files."
  , Doc ()
cleanRule
  , Doc ()
distClean
  , Doc ()
"# EOF"
  ]

  where

  inDirectory :: Bool
  inDirectory :: Bool
inDirectory = AgdaBackendOptions -> Bool
inDir AgdaBackendOptions
agdaOpts
  nSpace :: Maybe String
  nSpace :: Maybe String
nSpace = AgdaBackendOptions -> Maybe String
nameSpace AgdaBackendOptions
agdaOpts

  header :: Doc ()
  header :: Doc ()
header = [Doc ()] -> Doc ()
forall ann. [Doc ann] -> Doc ann
vsep
    [ Doc ()
"# Makefile for building the parser and test program."
    , Doc ()
forall ann. Doc ann
emptyDoc
    , Doc ()
"AGDA       = agda"
    , Doc ()
"GHC        = ghc"
    , Doc ()
"GHC_OPTS   = -package containers -package prettyprinter -package prettyprinter-ansi-terminal"
    , Doc ()
"HAPPY      = happy"
    , Doc ()
"HAPPY_OPTS = --array --info --ghc --coerce"
    , Doc ()
"ALEX       = alex"
    , Doc ()
"ALEX_OPTS  = --ghc"
    ]

  phonyRule :: Doc ()
  phonyRule :: Doc ()
phonyRule = [Doc ()] -> Doc ()
forall ann. [Doc ann] -> Doc ann
vsep
    [ Doc ()
"# List of goals not corresponding to file names."
    , Doc ()
forall ann. Doc ann
emptyDoc
    , String -> [String] -> String -> Doc ()
mkRule String
".PHONY" [ String
"all", String
"clean", String
"distclean" ] []
    ]

  defaultRule :: Doc ()
  defaultRule :: Doc ()
defaultRule = [Doc ()] -> Doc ()
forall ann. [Doc ann] -> Doc ann
vsep
    [ Doc ()
"# Default goal."
    , Doc ()
forall ann. Doc ann
emptyDoc
    , String -> [String] -> String -> Doc ()
mkRule String
"all" [String]
dependencies []
    ]
    where
      dependencies :: [String]
dependencies = [ Bool -> Maybe String -> String -> String -> String
mkDir Bool
inDirectory Maybe String
nSpace String
cfName String
"Test", String
"Main" ]

  bnfcRule :: Doc ()
  bnfcRule :: Doc ()
bnfcRule = String -> [String] -> String -> Doc ()
mkRule String
target [ String
pathToGrammar ] String
recipe
    where
      target :: String
target = [String] -> String
unwords [ String
absSintax, String
lexerSpec, String
parserSpec, String
parserTest , String
printer ]

      recipe :: String
recipe = String
"bnfc " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (if Bool
force then String
"-f " else String
"") String -> String -> String
forall a. [a] -> [a] -> [a]
++
        String
pathToGrammar String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" agda" String -> String -> String
forall a. [a] -> [a] -> [a]
++ AgdaBackendOptions -> String
printAgdaOptions AgdaBackendOptions
agdaOpts

  -- | Rule to invoke @happy@.
  happyRule :: Doc ()
  happyRule :: Doc ()
happyRule = String -> [String] -> String -> Doc ()
mkRule String
"%.hs" [ String
"%.y" ] String
"${HAPPY} ${HAPPY_OPTS} $<"

  -- | Rule to invoke @alex@.
  alexRule :: Doc ()
  alexRule :: Doc ()
alexRule = String -> [String] -> String -> Doc ()
mkRule String
"%.hs" [ String
"%.x" ] String
"${ALEX} ${ALEX_OPTS} $<"

  -- | Rule to build Haskell test parser.
  testParserRule :: Doc ()
  testParserRule :: Doc ()
testParserRule = String -> [String] -> String -> Doc ()
mkRule String
targets [String]
dependencies String
"${GHC} ${GHC_OPTS} $@"
    where
    targets :: String
    targets :: String
targets = Bool -> Maybe String -> String -> String -> String
mkDir Bool
inDirectory Maybe String
nSpace String
cfName String
"Test"
    dependencies :: [String]
    dependencies :: [String]
dependencies =
      [ String
absSintax ]
      [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
      Bool -> [String] -> [String]
forall m. Monoid m => Bool -> m -> m
Utils.when (LBNF -> Bool
layoutsAreUsed LBNF
lbnf) [ String
layout ]
      [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
      [ String
lexer
      , String
parserSpec
      , String
parser
      , String
printer
      , String
parserTest
      ]

  -- | Rule to compile Agda files.
  mainRule :: Doc ()
  mainRule :: Doc ()
mainRule = String -> [String] -> String -> Doc ()
mkRule String
"Main" [String]
dependencies String
recipe
    where
      dependencies :: [String]
      dependencies :: [String]
dependencies =
        [ String
main
        , String
ast
        , String
agdaParser
        , String
ioLib
        ]
        [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
        Bool -> [String] -> [String]
forall m. Monoid m => Bool -> m -> m
Utils.when (LBNF -> Bool
layoutsAreUsed LBNF
lbnf) [ String
layout ]
        [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
        [ String
lexer
        , String
parser
        , String
printer
        ]
      recipe :: String
      recipe :: String
recipe = String
"${AGDA} --no-libraries --ghc --ghc-flag=-Wwarn $<"

  cleanRule :: Doc ()
  cleanRule :: Doc ()
cleanRule = String -> [String] -> String -> Doc ()
mkRule String
"clean" [] String
recipe
    where
      recipe :: String
recipe = String
"-rm " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
filesToClean
            String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n\t" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"-rm -rf MAlonzo"

      filesToClean :: String
filesToClean
        | Bool
inDirectory
          = if Maybe String -> Bool
forall a. Maybe a -> Bool
isJust Maybe String
nSpace
            then
              [String] -> String
unwords ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$
                String
executable String -> [String] -> [String]
forall a. a -> [a] -> [a]
: String
agdaMainExecutable String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ((Maybe String -> String
forall a. HasCallStack => Maybe a -> a
fromJust Maybe String
nSpace String -> String -> String
</> String -> String
fstCharUpper String
cfName String -> String -> String
</> String
"*") String -> String -> String
forall a. Semigroup a => a -> a -> a
<>) [String]
genHs
            else
              [String] -> String
unwords ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ String
executable String -> [String] -> [String]
forall a. a -> [a] -> [a]
: String
agdaMainExecutable String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ((String -> String
fstCharUpper String
cfName String -> String -> String
</> String
"*") String -> String -> String
forall a. Semigroup a => a -> a -> a
<>) [String]
genHs
        | Maybe String -> Bool
forall a. Maybe a -> Bool
isJust Maybe String
nSpace
          = [String] -> String
unwords ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ String
executable String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ((Maybe String -> String
forall a. HasCallStack => Maybe a -> a
fromJust Maybe String
nSpace String -> String -> String
</> String
"*") String -> String -> String
forall a. Semigroup a => a -> a -> a
<>) [String]
genHs
        | Bool
otherwise = [String] -> String
unwords ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ String
executable String -> [String] -> [String]
forall a. a -> [a] -> [a]
: String
agdaMainExecutable String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String
"*" String -> String -> String
forall a. Semigroup a => a -> a -> a
<>) [String]
genHs

      genHs :: [String]
genHs  = [ String
".agdai", String
".hi", String
".o" ]

  distClean :: Doc ()
  distClean :: Doc ()
distClean = String -> [String] -> String -> Doc ()
mkRule String
"distclean" [String
"clean"] String
recipe
    where
      recipe :: String
recipe = String
"-rm " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords
        [ String
absSintax
        , String
lexerSpec
        , String
lexer
        , String
parserSpec
        , String
parser
        , String
parserTest
        , String
printer
        , String
template
        , String
ast
        , String
ioLib
        , String
main
        , String
agdaParser
        , String
absSintax String -> String -> String
<.> String
"bak"
        , String
lexerSpec String -> String -> String
<.> String
"bak"
        , String
lexer String -> String -> String
<.> String
"bak"
        , String
parserSpec String -> String -> String
<.> String
"bak"
        , String
parser String -> String -> String
<.> String
"bak"
        , String
parserTest String -> String -> String
<.> String
"bak"
        , String
printer String -> String -> String
<.> String
"bak"
        , String
template String -> String -> String
<.> String
"bak"
        , String
ast String -> String -> String
<.> String
"bak"
        , String
ioLib String -> String -> String
<.> String
"bak"
        , String
main String -> String -> String
<.> String
"bak"
        , String
agdaParser String -> String -> String
<.> String
"bak"
        , String
parserInfo
        , String
"Makefile"
        , String
"Makefile.bak"
        , [String] -> String
unwords (Bool -> [String] -> [String]
forall m. Monoid m => Bool -> m -> m
Utils.when (LBNF -> Bool
layoutsAreUsed LBNF
lbnf) [String
layout, String
layout String -> String -> String
<.> String
"bak"])
        ]
        String -> String -> String
forall a. [a] -> [a] -> [a]
++ Bool -> Maybe String -> String
rmdir Bool
inDirectory Maybe String
nSpace

  rmdir :: Bool -> Maybe String -> String
  rmdir :: Bool -> Maybe String -> String
rmdir Bool
True  Maybe String
Nothing  = String
"\n\t" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"-rmdir " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
fstCharUpper String
cfName
  rmdir Bool
False Maybe String
Nothing  = String
""
  rmdir Bool
True  (Just String
s) = String
"\n\t" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"-rmdir -p " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
fstCharUpper String
s String -> String -> String
</> String -> String
fstCharUpper String
cfName
  rmdir Bool
False (Just String
s) = String
"\n\t" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"-rmdir " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
fstCharUpper String
s


  -- Paths to Haskell generated components.
  absSintax :: String
absSintax  = Bool -> Maybe String -> String -> String -> String -> String
mkFilePath Bool
inDirectory Maybe String
nSpace String
cfName String
"Abs" String
"hs"
  layout :: String
layout     = Bool -> Maybe String -> String -> String -> String -> String
mkFilePath Bool
inDirectory Maybe String
nSpace String
cfName String
"Layout" String
"hs"
  lexerSpec :: String
lexerSpec  = Bool -> Maybe String -> String -> String -> String -> String
mkFilePath Bool
inDirectory Maybe String
nSpace String
cfName String
"Lex" String
"x"
  lexer :: String
lexer      = Bool -> Maybe String -> String -> String -> String -> String
mkFilePath Bool
inDirectory Maybe String
nSpace String
cfName String
"Lex" String
"hs"
  parserSpec :: String
parserSpec = Bool -> Maybe String -> String -> String -> String -> String
mkFilePath Bool
inDirectory Maybe String
nSpace String
cfName String
"Par" String
"y"
  parser :: String
parser     = Bool -> Maybe String -> String -> String -> String -> String
mkFilePath Bool
inDirectory Maybe String
nSpace String
cfName String
"Par" String
"hs"
  parserInfo :: String
parserInfo = Bool -> Maybe String -> String -> String -> String -> String
mkFilePath Bool
inDirectory Maybe String
nSpace String
cfName String
"Par" String
"info"
  parserTest :: String
parserTest = Bool -> Maybe String -> String -> String -> String -> String
mkFilePath Bool
inDirectory Maybe String
nSpace String
cfName String
"Test" String
"hs"
  printer :: String
printer    = Bool -> Maybe String -> String -> String -> String -> String
mkFilePath Bool
inDirectory Maybe String
nSpace String
cfName String
"Print" String
"hs"
  template :: String
template   = Bool -> Maybe String -> String -> String -> String -> String
mkFilePath Bool
inDirectory Maybe String
nSpace String
cfName String
"Skel" String
"hs"

  -- Paths to Agda generated components.
  ast :: String
ast        = Bool -> Maybe String -> String -> String -> String -> String
mkFilePath Bool
inDirectory Maybe String
nSpace String
cfName String
"AST" String
"agda"
  ioLib :: String
ioLib      = Bool -> Maybe String -> String -> String -> String -> String
mkFilePath Bool
inDirectory Maybe String
nSpace String
cfName String
"IOLib" String
"agda"
  main :: String
main       = Bool -> Maybe String -> String -> String -> String -> String
mkFilePath Bool
inDirectory Maybe String
nSpace String
cfName String
"Main" String
"agda"
  agdaParser :: String
agdaParser = Bool -> Maybe String -> String -> String -> String -> String
mkFilePath Bool
inDirectory Maybe String
nSpace String
cfName String
"Parser" String
"agda"

  -- Parser test executable.
  executable :: String
executable = String -> String
dropExtension String
parserTest
  -- Agda main executable.
  agdaMainExecutable :: String
agdaMainExecutable = String
"Main"