{-# 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 (ImportNumeric -> ImportNumeric -> Bool
(ImportNumeric -> ImportNumeric -> Bool)
-> (ImportNumeric -> ImportNumeric -> Bool) -> Eq ImportNumeric
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ImportNumeric -> ImportNumeric -> Bool
$c/= :: ImportNumeric -> ImportNumeric -> Bool
== :: ImportNumeric -> ImportNumeric -> Bool
$c== :: ImportNumeric -> ImportNumeric -> Bool
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 :: ImportNumeric -> Bool -> Bool -> Bool -> Doc ()
imports ImportNumeric
numeric Bool
layout Bool
hasPos Bool
needMaybe = [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
  [ Bool -> [Doc ()] -> [Doc ()]
forall m. Monoid m => Bool -> m -> m
Utils.when Bool
layout
    [ Doc ()
"open import Agda.Builtin.Bool using () renaming (Bool to #Bool)" ]
  , [ Doc ()
"open import Agda.Builtin.Char using (Char)" ]
  , Bool -> [Doc ()] -> [Doc ()]
forall m. Monoid m => Bool -> m -> m
Utils.when (ImportNumeric
numeric ImportNumeric -> ImportNumeric -> Bool
forall a. Eq a => a -> a -> Bool
== ImportNumeric
YesImportNumeric) [ Doc ()
importNumeric ]
  , [ Doc ()
"open import Agda.Builtin.List using ([]; _∷_) renaming (List to #List)" ]
  , Bool -> [Doc ()] -> [Doc ()]
forall m. Monoid m => Bool -> m -> m
Utils.when Bool
needMaybe
    [ 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 ()
"open import Agda.Builtin.Maybe using () renaming"
      , Doc ()
"( Maybe to #Maybe"
      , Doc ()
"; nothing to #nothing"
      , Doc ()
"; just to #just"
      , Doc ()
")"
      ]
    ]
  , Bool -> [Doc ()] -> [Doc ()]
forall m. Monoid m => Bool -> m -> m
Utils.when Bool
hasPos
    [ Doc ()
"open import Agda.Builtin.Nat using () renaming (Nat to #Nat)" ]
  , [ 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 ()
"open import Agda.Builtin.String using () renaming"
      , Doc ()
"( String to #String"
      , Doc ()
"; primStringFromList to #stringFromList"
      , Doc ()
")"
      ]
    ]
  ]

  where

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

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

  where
    imp :: String -> Doc ()
    imp :: ModuleName -> Doc ()
imp ModuleName
p = Doc ()
"{-# FOREIGN GHC import" Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> ModuleName -> Doc ()
forall a. IsString a => ModuleName -> a
fromString ModuleName
p Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"#-}"

    base :: [String]
    base :: [ModuleName]
base = [[ModuleName]] -> [ModuleName]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ [ModuleName
"Prelude (" ModuleName -> ModuleName -> ModuleName
forall a. [a] -> [a] -> [a]
++ ModuleName
preludeImports ModuleName -> ModuleName -> ModuleName
forall a. [a] -> [a] -> [a]
++ ModuleName
")"]
      , Bool -> [ModuleName] -> [ModuleName]
forall m. Monoid m => Bool -> m -> m
Utils.when Bool
pos [ ModuleName
"qualified Prelude" ]
      , [ ModuleName
"qualified Data.Text" ]
      ]

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

-- Replace _ by - in Agda names to avoid illegal names like Foo_'.
sanitize :: String -> String
sanitize :: ModuleName -> ModuleName
sanitize = Char -> Char -> ModuleName -> ModuleName
forall a (f :: * -> *). (Eq a, Functor f) => a -> a -> f a -> f a
replace Char
'_' Char
'-'

-- | 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 :: Type -> ModuleName
nameSuggestion = \case
  BaseType BaseCat
bc -> case BaseCat
bc of
    BuiltinCat BuiltinCat
b -> String1 -> ModuleName
nameFor (String1 -> ModuleName) -> String1 -> ModuleName
forall a b. (a -> b) -> a -> b
$ BuiltinCat -> String1
printBuiltinCat BuiltinCat
b
    IdentCat IdentCat
_   -> ModuleName
"x"
    TokenCat String1
_   -> ModuleName
"x"
    BaseCat String1
x    -> String1 -> ModuleName
nameFor String1
x
  ListType Type
ty -> Type -> ModuleName
nameSuggestion Type
ty ModuleName -> ModuleName -> ModuleName
forall a. [a] -> [a] -> [a]
++ ModuleName
"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 :: String1 -> ModuleName
nameFor String1
d = [ Char -> Char
toLower (Char -> Char) -> Char -> Char
forall a b. (a -> b) -> a -> b
$ ModuleName -> Char
forall a. [a] -> a
head (ModuleName -> Char) -> ModuleName -> Char
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> ModuleName -> ModuleName
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'#') (ModuleName -> ModuleName) -> ModuleName -> ModuleName
forall a b. (a -> b) -> a -> b
$ String1 -> ModuleName
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList String1
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 :: [a] -> [(Maybe Int, a)]
numberUniquely [a]
as = (a -> StateT (Frequency a) Identity (Maybe Int, a))
-> [a] -> StateT (Frequency a) Identity [(Maybe Int, a)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM a -> StateT (Frequency a) Identity (Maybe Int, a)
step [a]
as StateT (Frequency a) Identity [(Maybe Int, a)]
-> Frequency a -> [(Maybe Int, a)]
forall s a. State s a -> s -> a
`evalState` Frequency a
forall k a. Map k a
Map.empty
  where
  -- First pass: determine frequency of each element.
  counts :: Frequency a
  counts :: Frequency a
counts = (Frequency a -> a -> Frequency a)
-> Frequency a -> [a] -> Frequency a
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ((a -> Frequency a -> Frequency a)
-> Frequency a -> a -> Frequency a
forall a b c. (a -> b -> c) -> b -> a -> c
flip a -> Frequency a -> Frequency a
forall a. Ord a => a -> Frequency a -> Frequency a
incr) Frequency a
forall k a. Map k a
Map.empty [a]
as
  -- Second pass: consecutively number elements with frequency > 1.
  step :: a -> State (Frequency a) (Maybe Int, a)
  step :: a -> StateT (Frequency a) Identity (Maybe Int, a)
step a
a = do
    -- If the element has a unique occurrence, we do not need to number it.
    let n :: Int
n = Int -> a -> Frequency a -> Int
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (ModuleName -> Int
forall a. HasCallStack => ModuleName -> a
error ModuleName
"numberUniquelyWith") a
a Frequency a
counts
    if Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 then (Maybe Int, a) -> StateT (Frequency a) Identity (Maybe Int, a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Int
forall a. Maybe a
Nothing, a
a) else do
      -- Otherwise, increase the counter for that element and number it
      -- with the new value.
      (Frequency a -> Frequency a) -> StateT (Frequency a) Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Frequency a -> Frequency a) -> StateT (Frequency a) Identity ())
-> (Frequency a -> Frequency a) -> StateT (Frequency a) Identity ()
forall a b. (a -> b) -> a -> b
$ a -> Frequency a -> Frequency a
forall a. Ord a => a -> Frequency a -> Frequency a
incr a
a
      (Frequency a -> (Maybe Int, a))
-> StateT (Frequency a) Identity (Maybe Int, a)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ((, a
a) (Maybe Int -> (Maybe Int, a))
-> (Frequency a -> Maybe Int) -> Frequency a -> (Maybe Int, a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Frequency a -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup a
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 :: a -> Frequency a -> Frequency a
incr = (Maybe Int -> Maybe Int) -> a -> Frequency a -> Frequency a
forall k a.
Ord k =>
(Maybe a -> Maybe a) -> k -> Map k a -> Map k a
Map.alter ((Maybe Int -> Maybe Int) -> a -> Frequency a -> Frequency a)
-> (Maybe Int -> Maybe Int) -> a -> Frequency a -> Frequency a
forall a b. (a -> b) -> a -> b
$ Maybe Int -> (Int -> Maybe Int) -> Maybe Int -> Maybe Int
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
1) (Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> (Int -> Int) -> Int -> Maybe Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int
forall a. Enum a => a -> a
succ)

uArrow :: String
uArrow :: ModuleName
uArrow = ModuleName
"→"