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 :: [String]
agdaReservedWords =
  [ String
"abstract"
  , String
"codata"
  , String
"coinductive"
  , String
"constructor"
  , String
"data"
  , String
"do"
  , String
"eta-equality"
  , String
"field"
  , String
"forall"
  , String
"hiding"
  , String
"import"
  , String
"in"
  , String
"inductive"
  , String
"infix"
  , String
"infixl"
  , String
"infixr"
  , String
"instance"
  , String
"let"
  , String
"macro"
  , String
"module"
  , String
"mutual"
  , String
"no-eta-equality"
  , String
"open"
  , String
"overlap"
  , String
"pattern"
  , String
"postulate"
  , String
"primitive"
  , String
"private"
  , String
"public"
  , String
"quote"
  , String
"quoteContext"
  , String
"quoteGoal"
  , String
"quoteTerm"
  , String
"record"
  , String
"renaming"
  , String
"rewrite"
  , String
"Set"
  , String
"syntax"
  , String
"tactic"
  , String
"unquote"
  , String
"unquoteDecl"
  , String
"unquoteDef"
  , String
"using"
  , String
"variable"
  , String
"where"
  , String
"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 :: String1 -> String1
agdaLower = String1 -> String1
avoidAgdaReservedWords (String1 -> String1) -> (String1 -> String1) -> String1 -> String1
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Char) -> String1 -> String1
updateHead Char -> Char
toLower
  where
  updateHead :: (Char -> Char) -> String1 -> String1
  updateHead :: (Char -> Char) -> String1 -> String1
updateHead Char -> Char
f (Char
x :| String
xs) = Char -> Char
f Char
x Char -> String -> String1
forall a. a -> [a] -> NonEmpty a
:| String
xs

-- | Avoid Agda reserved words.
avoidAgdaReservedWords :: String1 -> String1
avoidAgdaReservedWords :: String1 -> String1
avoidAgdaReservedWords String1
s
  | String1 -> String
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList String1
s String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
agdaReservedWords = Char -> Char -> String1 -> String1
forall a (f :: * -> *). (Eq a, Functor f) => a -> a -> f a -> f a
replace Char
'_' Char
'-' (String1 -> String1) -> String1 -> String1
forall a b. (a -> b) -> a -> b
$ String1
s String1 -> String1 -> String1
forall a. Semigroup a => a -> a -> a
<> (Char
'\''Char -> String -> String1
forall a. a -> [a] -> NonEmpty a
:|[])
  | Bool
otherwise = Char -> Char -> String1 -> String1
forall a (f :: * -> *). (Eq a, Functor f) => a -> a -> f a -> f a
replace Char
'_' Char
'-' String1
s

-- | Apply agdaLower function to AST rhs types.
avoidResWordsASTRulesAgda :: [(Type, [(Label, [Type])])]
                          -> [(Type, [(Label, [Type])])]
avoidResWordsASTRulesAgda :: [(Type, [(Label, [Type])])] -> [(Type, [(Label, [Type])])]
avoidResWordsASTRulesAgda = ((Type, [(Label, [Type])]) -> (Type, [(Label, [Type])]))
-> [(Type, [(Label, [Type])])] -> [(Type, [(Label, [Type])])]
forall a b. (a -> b) -> [a] -> [b]
map (Type, [(Label, [Type])]) -> (Type, [(Label, [Type])])
avoidResWordsTypes
  where
    avoidResWordsTypes :: (Type, [(Label, [Type])])
                       -> (Type, [(Label, [Type])])
    avoidResWordsTypes :: (Type, [(Label, [Type])]) -> (Type, [(Label, [Type])])
avoidResWordsTypes (Type
t, [(Label, [Type])]
rhs) = (Type
t, ((Label, [Type]) -> (Label, [Type]))
-> [(Label, [Type])] -> [(Label, [Type])]
forall a b. (a -> b) -> [a] -> [b]
map (([Type] -> [Type]) -> (Label, [Type]) -> (Label, [Type])
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
Data.Bifunctor.second (Type -> Type
avoidResWordsType (Type -> Type) -> [Type] -> [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>)) [(Label, [Type])]
rhs)

lowerLabel :: Label -> Label
lowerLabel :: Label -> Label
lowerLabel = \case
  LId  String1
name -> String1 -> Label
LId (String1 -> Label) -> String1 -> Label
forall a b. (a -> b) -> a -> b
$ String1 -> String1
agdaLower String1
name
  LDef String1
name -> String1 -> Label
LDef (String1 -> Label) -> String1 -> Label
forall a b. (a -> b) -> a -> b
$ String1 -> String1
agdaLower String1
name
  Label
LWild     -> Label
LWild
  Label
LNil      -> Label
LNil
  Label
LCons     -> Label
LCons
  Label
LSg       -> Label
LSg

avoidResWordsType :: Type -> Type
avoidResWordsType :: Type -> Type
avoidResWordsType = \case
  BaseType BaseCat
bc -> BaseCat -> Type
BaseType (BaseCat -> Type) -> BaseCat -> Type
forall a b. (a -> b) -> a -> b
$ BaseCat -> BaseCat
avoidResWordsBaseCat BaseCat
bc
  ListType Type
ty -> Type -> Type
ListType (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
avoidResWordsType Type
ty

avoidResWordsCat :: Cat -> Cat
avoidResWordsCat :: Cat -> Cat
avoidResWordsCat = \case
  Cat BaseCat
bc -> BaseCat -> Cat
forall a. a -> Cat' a
Cat (BaseCat -> Cat) -> BaseCat -> Cat
forall a b. (a -> b) -> a -> b
$ BaseCat -> BaseCat
avoidResWordsBaseCat BaseCat
bc
  ListCat Cat
ca -> Cat -> Cat
forall a. Cat' a -> Cat' a
ListCat (Cat -> Cat) -> Cat -> Cat
forall a b. (a -> b) -> a -> b
$ Cat -> Cat
avoidResWordsCat Cat
ca
  CoerceCat String1
ne Integer
n -> String1 -> Integer -> Cat
forall a. String1 -> Integer -> Cat' a
CoerceCat (String1 -> String1
avoidAgdaReservedWords String1
ne) Integer
n

avoidResWordsBaseCat :: BaseCat -> BaseCat
avoidResWordsBaseCat :: BaseCat -> BaseCat
avoidResWordsBaseCat = \case
  BuiltinCat BuiltinCat
bc -> BuiltinCat -> BaseCat
BuiltinCat BuiltinCat
bc
  IdentCat IdentCat
ic -> IdentCat -> BaseCat
IdentCat IdentCat
ic
  TokenCat String1
ne -> String1 -> BaseCat
TokenCat (String1 -> BaseCat) -> String1 -> BaseCat
forall a b. (a -> b) -> a -> b
$ String1 -> String1
avoidAgdaReservedWords String1
ne
  BaseCat String1
ne -> String1 -> BaseCat
BaseCat (String1 -> BaseCat) -> String1 -> BaseCat
forall a b. (a -> b) -> a -> b
$ String1 -> String1
avoidAgdaReservedWords String1
ne

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

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

checkPars :: [Parameter] -> [Parameter]
checkPars :: [Parameter] -> [Parameter]
checkPars [Parameter]
pars = Parameter -> Parameter
checkPar (Parameter -> Parameter) -> [Parameter] -> [Parameter]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Parameter]
pars

checkPar :: Parameter -> Parameter
checkPar :: Parameter -> Parameter
checkPar Parameter
p = Parameter
p { paramName :: String1
paramName = String1 -> String1
avoidAgdaReservedWords (String1 -> String1) -> String1 -> String1
forall a b. (a -> b) -> a -> b
$ Parameter -> String1
paramName Parameter
p}

checkBody :: Exp -> Exp
checkBody :: Exp -> Exp
checkBody (App Label
l FunType
t [Exp]
exps)   = Label -> FunType -> [Exp] -> Exp
App (Label -> Label
lowerLabel Label
l) FunType
t (Exp -> Exp
checkBody (Exp -> Exp) -> [Exp] -> [Exp]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Exp]
exps)
checkBody (Var Parameter
p)          = Parameter -> Exp
Var (Parameter -> Exp) -> Parameter -> Exp
forall a b. (a -> b) -> a -> b
$ Parameter -> Parameter
checkPar Parameter
p
checkBody e :: Exp
e@(LitInteger Integer
_) = Exp
e
checkBody e :: Exp
e@(LitDouble Double
_)  = Exp
e
checkBody e :: Exp
e@(LitChar Char
_)    = Exp
e
checkBody e :: Exp
e@(LitString String
_)  = Exp
e