Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- agdaReservedWords :: [String]
- agdaLower :: String1 -> String1
- avoidAgdaReservedWords :: String1 -> String1
- avoidResWordsASTRulesAgda :: [(Type, [(Label, [Type])])] -> [(Type, [(Label, [Type])])]
- lowerLabel :: Label -> Label
- avoidResWordsType :: Type -> Type
- avoidResWordsCat :: Cat -> Cat
- avoidResWordsBaseCat :: BaseCat -> BaseCat
- processFunctionsAgda :: [(LabelName, Function)] -> [(LabelName, Function)]
- checkFun :: Function -> Function
- checkPars :: [Parameter] -> [Parameter]
- checkPar :: Parameter -> Parameter
- checkBody :: Exp -> Exp
Documentation
agdaReservedWords :: [String] Source #
A list of Agda keywords that would clash with generated names.
agdaLower :: String1 -> String1 Source #
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"]
avoidAgdaReservedWords :: String1 -> String1 Source #
Avoid Agda reserved words.
avoidResWordsASTRulesAgda :: [(Type, [(Label, [Type])])] -> [(Type, [(Label, [Type])])] Source #
Apply agdaLower function to AST rhs types.
lowerLabel :: Label -> Label Source #
avoidResWordsType :: Type -> Type Source #
avoidResWordsCat :: Cat -> Cat Source #