{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}

module BNFC.Backend.Agda.Utilities.Utils where

import BNFC.Backend.Common.Utils as Utils

import BNFC.CF

import BNFC.Prelude

import Control.Monad.State

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

import Prettyprinter

-- | Import the builtin numeric types (content of some token categories)?

data ImportNumeric
  = YesImportNumeric  -- ^ Import the numeric types.
  | NoImportNumeric   -- ^ Don't import the numeric types.
  deriving (Eq)

imports :: ImportNumeric -- ^ Import also numeric types?
        -> Bool          -- ^ If have layout, import booleans.
        -> Bool          -- ^ If have position information, import natural numbers.
        -> Bool          -- ^ Do we need @Maybe@?
        -> Doc ()
imports numeric layout hasPos needMaybe = vsep $ concat
  [ Utils.when layout
    [ "open import Agda.Builtin.Bool using () renaming (Bool to #Bool)" ]
  , [ "open import Agda.Builtin.Char using (Char)" ]
  , Utils.when (numeric == YesImportNumeric) [ importNumeric ]
  , [ "open import Agda.Builtin.List using ([]; _∷_) renaming (List to #List)" ]
  , Utils.when needMaybe
    [ hang 2 $ vsep
      [ "open import Agda.Builtin.Maybe using () renaming"
      , "( Maybe to #Maybe"
      , "; nothing to #nothing"
      , "; just to #just"
      , ")"
      ]
    ]
  , Utils.when hasPos
    [ "open import Agda.Builtin.Nat using () renaming (Nat to #Nat)" ]
  , [ hang 2 $ vsep
      [ "open import Agda.Builtin.String using () renaming"
      , "( String to #String"
      , "; primStringFromList to #stringFromList"
      , ")"
      ]
    ]
  ]

  where

    importNumeric :: Doc ()
    importNumeric = vsep
      [ "open import Agda.Builtin.Float public using () renaming (Float to Double)"
      , "open import Agda.Builtin.Int   public using () renaming (Int to Integer)"
      , "open import Agda.Builtin.Int using () renaming (pos to #pos)"
      ]

importPragmas :: Bool         -- ^ Do we use position information?
              -> [ModuleName] -- ^ Haskell modules to import.
              -> Doc ()
importPragmas pos mods = vsep $ map imp $ base ++ mods

  where
    imp :: String -> Doc ()
    imp p = "{-# FOREIGN GHC import" <+> fromString p <+> "#-}"

    base :: [String]
    base = concat
      [ ["Prelude (" ++ preludeImports ++ ")"]
      , Utils.when pos [ "qualified Prelude" ]
      , [ "qualified Data.Text" ]
      ]

    preludeImports :: String
    preludeImports =  intercalate ", " $
      ["Bool", "Char", "Double", "Integer", "String", "(.)", "Either (..)" ]
      ++
      Utils.when pos
      [ "error" ] -- used unqualified by the GHC backend for postulates

-- Replace _ by - in Agda names to avoid illegal names like Foo_'.
sanitize :: String -> String
sanitize = replace '_' '-'

-- | How to print the types of constructors in Agda?

data ConstructorStyle
  = UnnamedArg  -- ^ Simply typed, like @E → S → S → S@.
  | NamedArg    -- ^ Dependently typed, like @(e : E) (s₁ s₂ : S) → S@.


-- | Suggest the name of a bound variable of the given category.
--
-- >>> map nameSuggestion
-- [ ListType (BaseType (BaseCat 'S':|"tm")), BaseType (TokenCat 'V':|"ar"), (BaseType (BaseCat 'E':|"xp") ]
-- ["ss","x","e"]
--

nameSuggestion :: Type -> String
nameSuggestion = \case
  BaseType bc -> case bc of
    BuiltinCat b -> nameFor $ printBuiltinCat b
    IdentCat _   -> "x"
    TokenCat _   -> "x"
    BaseCat x    -> nameFor x
  ListType ty -> nameSuggestion ty ++ "s"

-- | Suggest the name of a bound variable of the given base category.
--
-- >>> map nameFor ["Stm","ABC","#String"]
-- ["s","a","s"]
--
nameFor :: String1 -> String
nameFor d = [ toLower $ head $ dropWhile (== '#') $ toList d ]

-- | Number duplicate elements in a list consecutively, starting with 1.
--
-- >>> numberUniquely ["a", "b", "a", "a", "c", "b"]
-- [(Just 1,"a"),(Just 1,"b"),(Just 2,"a"),(Just 3,"a"),(Nothing,"c"),(Just 2,"b")]
--
numberUniquely :: forall a. Ord a => [a] -> [(Maybe Int, a)]
numberUniquely as = mapM step as `evalState` Map.empty
  where
  -- First pass: determine frequency of each element.
  counts :: Frequency a
  counts = foldl (flip incr) Map.empty as
  -- Second pass: consecutively number elements with frequency > 1.
  step :: a -> State (Frequency a) (Maybe Int, a)
  step a = do
    -- If the element has a unique occurrence, we do not need to number it.
    let n = Map.findWithDefault (error "numberUniquelyWith") a counts
    if n == 1 then return (Nothing, a) else do
      -- Otherwise, increase the counter for that element and number it
      -- with the new value.
      modify $ incr a
      gets ((, a) . Map.lookup a)

-- | A frequency map.
--
--   NB: this type synonym should be local to 'numberUniquely', but
--   Haskell lacks local type synonyms.
--   https://gitlab.haskell.org/ghc/ghc/issues/4020
type Frequency a = Map a Int

-- | Increase the frequency of the given key.
incr :: Ord a => a -> Frequency a -> Frequency a
incr = Map.alter $ maybe (Just 1) (Just . succ)

uArrow :: String
uArrow = "→"