Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- agdaAbstractSyntax :: LBNF -> State AgdaBackendState Result
- cf2AST :: LBNF -> String -> Bool -> Maybe String -> [(Type, [(Label, [Type])])] -> [(LabelName, Function)] -> [(CatName, TokenDef)] -> [CatName] -> Bool -> String
- cf2doc :: LBNF -> String -> Bool -> Maybe String -> [(Type, [(Label, [Type])])] -> [(LabelName, Function)] -> [(CatName, TokenDef)] -> [CatName] -> Bool -> Doc ()
- prTokens :: ModuleName -> [(CatName, TokenDef)] -> Doc ()
- prToken :: ModuleName -> (CatName, TokenDef) -> Doc ()
- prDatas :: Bool -> ModuleName -> ConstructorStyle -> [(Type, [(Label, [Type])])] -> Doc ()
- prData :: Bool -> ModuleName -> ConstructorStyle -> (Type, [(Label, [Type])]) -> Doc ()
- prData' :: ModuleName -> ConstructorStyle -> Doc () -> Doc () -> [(Label, [Type])] -> Doc ()
- prettyData :: ConstructorStyle -> Doc () -> [(Label, [Type])] -> Doc ()
- printCase :: ConstructorStyle -> Doc () -> (Label, [Type]) -> Doc ()
- printConstructorArgs :: ConstructorStyle -> [Type] -> Doc ()
- prettyType :: Type -> String
- compilePragma :: ModuleName -> Doc () -> Doc () -> [Doc ()] -> Doc ()
- prFunctions :: Bool -> [(LabelName, Function)] -> Doc ()
- prFunction :: Bool -> (LabelName, Function) -> Doc ()
- printerBindings :: ModuleName -> [Type] -> [BuiltinCat] -> [CatName] -> Doc ()
- prPrinterBindings :: [(Doc (), Doc ())] -> Doc ()
- prPrinterBinding :: (Doc (), Doc ()) -> Doc ()
- prPrinterPragmas :: [(Doc (), (Doc (), Doc ()))] -> Doc ()
- prPrinterPragma :: (Doc (), (Doc (), Doc ())) -> Doc ()
Documentation
cf2AST :: LBNF -> String -> Bool -> Maybe String -> [(Type, [(Label, [Type])])] -> [(LabelName, Function)] -> [(CatName, TokenDef)] -> [CatName] -> Bool -> String Source #
cf2doc :: LBNF -> String -> Bool -> Maybe String -> [(Type, [(Label, [Type])])] -> [(LabelName, Function)] -> [(CatName, TokenDef)] -> [CatName] -> Bool -> Doc () Source #
prTokens :: ModuleName -> [(CatName, TokenDef)] -> Doc () Source #
Print Agda types for user defined tokens.
prDatas :: Bool -> ModuleName -> ConstructorStyle -> [(Type, [(Label, [Type])])] -> Doc () Source #
Print Agda types for categories in AST rules.
prData :: Bool -> ModuleName -> ConstructorStyle -> (Type, [(Label, [Type])]) -> Doc () Source #
Pretty-print Agda data types and pragmas for AST.
prData' :: ModuleName -> ConstructorStyle -> Doc () -> Doc () -> [(Label, [Type])] -> Doc () Source #
Pretty-print Agda data types and pragmas.
prettyData :: ConstructorStyle -> Doc () -> [(Label, [Type])] -> Doc () Source #
Pretty-print AST definition in Agda syntax.
printConstructorArgs :: ConstructorStyle -> [Type] -> Doc () Source #
prettyType :: Type -> String Source #
compilePragma :: ModuleName -> Doc () -> Doc () -> [Doc ()] -> Doc () Source #
prFunctions :: Bool -> [(LabelName, Function)] -> Doc () Source #
Generate Haskell/Agda code for the define
d constructors.
printerBindings :: ModuleName -> [Type] -> [BuiltinCat] -> [CatName] -> Doc () Source #