{-# 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 :: Parser AgdaBackendOptions
parseOpts = Parser AgdaBackendOptions
agdaOptionsParser
  initState :: LBNF -> GlobalOptions -> BackendOptions 'TargetAgda -> Except String (BackendState 'TargetAgda)
  initState :: LBNF
-> GlobalOptions
-> BackendOptions 'TargetAgda
-> Except String (BackendState 'TargetAgda)
initState = LBNF
-> GlobalOptions
-> BackendOptions 'TargetAgda
-> Except String (BackendState 'TargetAgda)
LBNF
-> GlobalOptions
-> AgdaBackendOptions
-> Except String AgdaBackendState
agdaInitState
  abstractSyntax :: LBNF -> State (BackendState 'TargetAgda) Result
  abstractSyntax :: LBNF -> State (BackendState 'TargetAgda) Result
abstractSyntax = LBNF -> State (BackendState 'TargetAgda) Result
LBNF -> State AgdaBackendState Result
agdaAbstractSyntax
  printer :: LBNF -> State (BackendState 'TargetAgda) Result
  printer :: LBNF -> State (BackendState 'TargetAgda) Result
printer = LBNF -> State (BackendState 'TargetAgda) Result
LBNF -> State AgdaBackendState Result
agdaPrinter
  lexer :: LBNF -> State (BackendState 'TargetAgda) Result
  lexer :: LBNF -> State (BackendState 'TargetAgda) Result
lexer = LBNF -> State (BackendState 'TargetAgda) Result
LBNF -> State AgdaBackendState Result
agdaLexer
  parser :: LBNF -> State (BackendState 'TargetAgda) Result
  parser :: LBNF -> State (BackendState 'TargetAgda) Result
parser = LBNF -> State (BackendState 'TargetAgda) Result
LBNF -> State AgdaBackendState Result
agdaParser
  parserTest :: LBNF -> State (BackendState 'TargetAgda) Result
  parserTest :: LBNF -> State (BackendState 'TargetAgda) Result
parserTest = LBNF -> State (BackendState 'TargetAgda) Result
LBNF -> State AgdaBackendState Result
agdaParserTest
  makefile :: LBNF -> State (BackendState 'TargetAgda) Result
  makefile :: LBNF -> State (BackendState 'TargetAgda) Result
makefile = LBNF -> State (BackendState 'TargetAgda) Result
LBNF -> State AgdaBackendState Result
agdaMakefile