{-# LANGUAGE DataKinds #-} {-# LANGUAGE TypeFamilies #-} module BNFC.Backend.Agda where import BNFC.CF import BNFC.Prelude import BNFC.Options.GlobalOptions import BNFC.Options.Target import BNFC.Backend.CommonInterface.Backend import BNFC.Backend.Agda.AbstractSyntax import BNFC.Backend.Agda.InitState import BNFC.Backend.Agda.Lexer import BNFC.Backend.Agda.Makefile import BNFC.Backend.Agda.Options import BNFC.Backend.Agda.Parser import BNFC.Backend.Agda.Test import BNFC.Backend.Agda.Printer import BNFC.Backend.Agda.State import Control.Monad.Except import Control.Monad.State import Options.Applicative instance Backend 'TargetAgda where type BackendOptions 'TargetAgda = AgdaBackendOptions type BackendState 'TargetAgda = AgdaBackendState parseOpts :: Parser AgdaBackendOptions parseOpts = agdaOptionsParser initState :: LBNF -> GlobalOptions -> BackendOptions 'TargetAgda -> Except String (BackendState 'TargetAgda) initState = agdaInitState abstractSyntax :: LBNF -> State (BackendState 'TargetAgda) Result abstractSyntax = agdaAbstractSyntax printer :: LBNF -> State (BackendState 'TargetAgda) Result printer = agdaPrinter lexer :: LBNF -> State (BackendState 'TargetAgda) Result lexer = agdaLexer parser :: LBNF -> State (BackendState 'TargetAgda) Result parser = agdaParser parserTest :: LBNF -> State (BackendState 'TargetAgda) Result parserTest = agdaParserTest makefile :: LBNF -> State (BackendState 'TargetAgda) Result makefile = agdaMakefile