{-# 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