module BNFC.Backend.Agda.Utilities.ReservedWords where

import BNFC.Backend.Common.Utils

import BNFC.CF

import BNFC.Prelude

import Data.Bifunctor (second)

-- | A list of Agda keywords that would clash with generated names.
agdaReservedWords :: [String]
agdaReservedWords =
  [ "abstract"
  , "codata"
  , "coinductive"
  , "constructor"
  , "data"
  , "do"
  , "eta-equality"
  , "field"
  , "forall"
  , "hiding"
  , "import"
  , "in"
  , "inductive"
  , "infix"
  , "infixl"
  , "infixr"
  , "instance"
  , "let"
  , "macro"
  , "module"
  , "mutual"
  , "no-eta-equality"
  , "open"
  , "overlap"
  , "pattern"
  , "postulate"
  , "primitive"
  , "private"
  , "public"
  , "quote"
  , "quoteContext"
  , "quoteGoal"
  , "quoteTerm"
  , "record"
  , "renaming"
  , "rewrite"
  , "Set"
  , "syntax"
  , "tactic"
  , "unquote"
  , "unquoteDecl"
  , "unquoteDef"
  , "using"
  , "variable"
  , "where"
  , "with"
  ]

-- | Turn identifier to non-capital identifier.
--   Needed, since in Agda a constructor cannot overload a data type
--   with the same name.
--
-- >>> map agdaLower ["SFun","foo","ABC","HelloWorld","module","Type_int","C1"]
-- ["sFun","foo","aBC","helloWorld","module'","type-int","c1"]
--
agdaLower :: String1 -> String1
agdaLower = avoidAgdaReservedWords . updateHead toLower
  where
  updateHead :: (Char -> Char) -> String1 -> String1
  updateHead f (x :| xs) = f x :| xs

-- | Avoid Agda reserved words.
avoidAgdaReservedWords :: String1 -> String1
avoidAgdaReservedWords s
  | toList s `elem` agdaReservedWords = replace '_' '-' $ s <> ('\'':|[])
  | otherwise = replace '_' '-' s

-- | Apply agdaLower function to AST rhs types.
avoidResWordsASTRulesAgda :: [(Type, [(Label, [Type])])]
                          -> [(Type, [(Label, [Type])])]
avoidResWordsASTRulesAgda = map avoidResWordsTypes
  where
    avoidResWordsTypes :: (Type, [(Label, [Type])])
                       -> (Type, [(Label, [Type])])
    avoidResWordsTypes (t, rhs) = (t, map (Data.Bifunctor.second (avoidResWordsType <$>)) rhs)

lowerLabel :: Label -> Label
lowerLabel = \case
  LId  name -> LId $ agdaLower name
  LDef name -> LDef $ agdaLower name
  LWild     -> LWild
  LNil      -> LNil
  LCons     -> LCons
  LSg       -> LSg

avoidResWordsType :: Type -> Type
avoidResWordsType = \case
  BaseType bc -> BaseType $ avoidResWordsBaseCat bc
  ListType ty -> ListType $ avoidResWordsType ty

avoidResWordsCat :: Cat -> Cat
avoidResWordsCat = \case
  Cat bc -> Cat $ avoidResWordsBaseCat bc
  ListCat ca -> ListCat $ avoidResWordsCat ca
  CoerceCat ne n -> CoerceCat (avoidAgdaReservedWords ne) n

avoidResWordsBaseCat :: BaseCat -> BaseCat
avoidResWordsBaseCat = \case
  BuiltinCat bc -> BuiltinCat bc
  IdentCat ic -> IdentCat ic
  TokenCat ne -> TokenCat $ avoidAgdaReservedWords ne
  BaseCat ne -> BaseCat $ avoidAgdaReservedWords ne

-- Apply agdaLower function to user defined functions names and body labels.
-- Check for Agda reserved words.
processFunctionsAgda :: [(LabelName, Function)]
                     -> [(LabelName, Function)]
processFunctionsAgda = map processFunction
  where
    processFunction :: (LabelName, Function) -> (LabelName, Function)
    processFunction (label,fun) = (agdaLower label, checkFun fun)

checkFun :: Function -> Function
checkFun f@Function {funPars=params, funBody=body} =
  f {funPars = checkPars params, funBody = checkBody body}

checkPars :: [Parameter] -> [Parameter]
checkPars pars = checkPar <$> pars

checkPar :: Parameter -> Parameter
checkPar p = p { paramName = avoidAgdaReservedWords $ paramName p}

checkBody :: Exp -> Exp
checkBody (App l t exps)   = App (lowerLabel l) t (checkBody <$> exps)
checkBody (Var p)          = Var $ checkPar p
checkBody e@(LitInteger _) = e
checkBody e@(LitDouble _)  = e
checkBody e@(LitChar _)    = e
checkBody e@(LitString _)  = e