cabal-version:       2.2
name:                agda2hs
version:             1.0.20231012
license:             BSD-3-Clause
license-file:        LICENSE
author:              Ulf Norell, Jesper Cockx, Orestis Melkonian, Sára Juhošová, James Chapman, Lucas Escot, Henry Blanchette
maintainer:          jesper@sikanda.be
copyright:           2023 Ulf Norell, Jesper Cockx, Orestis Melkonian, Sára Juhošová, James Chapman, Lucas Escot, Henry Blanchette
category:            Language, Compiler
build-type:          Simple
synopsis:            Compiling Agda code to readable Haskell.
description:
  Produces verified and readable Haskell code by extracting it from a
  (lightly annotated) Agda program.
  The tool is implemented as an Agda backend, which means that `agda2hs` is a
  fully functional Agda compiler.

data-dir:           src/data
data-files:         emacs-mode/*.el

source-repository head
  type:     git
  location: https://github.com/agda/agda2hs.git

executable agda2hs
  hs-source-dirs:      src
  main-is:             Main.hs
  other-modules:       Agda2Hs.AgdaUtils,
                       Agda2Hs.Compile,
                       Agda2Hs.Compile.ClassInstance,
                       Agda2Hs.Compile.Data,
                       Agda2Hs.Compile.Function,
                       Agda2Hs.Compile.Imports,
                       Agda2Hs.Compile.Name,
                       Agda2Hs.Compile.Postulate,
                       Agda2Hs.Compile.Record,
                       Agda2Hs.Compile.Rewrites,
                       Agda2Hs.Compile.Term,
                       Agda2Hs.Compile.Type,
                       Agda2Hs.Compile.TypeDefinition,
                       Agda2Hs.Compile.Types,
                       Agda2Hs.Compile.Utils,
                       Agda2Hs.HsUtils,
                       Agda2Hs.Pragma
                       Agda2Hs.Render
                       AgdaInternals
  build-depends:       base >= 4.10 && < 4.18,
                       Agda >= 2.6.4 && < 2.6.5,
                       bytestring >= 0.11.5 && < 0.12,
                       containers >= 0.6 && < 0.7,
                       unordered-containers >= 0.2.19 && < 0.3,
                       mtl >= 2.2.2 && < 2.3,
                       directory >= 1.2.6.2 && < 1.4,
                       filepath >= 1.4.1.0 && < 1.5,
                       haskell-src-exts >= 1.23 && < 1.25,
                       syb >= 0.7.2 && < 0.8,
                       text >= 2.0.2 && < 2.1,
                       deepseq >= 1.4.4 && < 1.5,
                       yaml-light >= 0.1.4 && < 2.0
  default-language:    Haskell2010
  default-extensions:  LambdaCase,
                       RecordWildCards,
                       FlexibleContexts,
                       MultiWayIf,
                       TupleSections,
                       ScopedTypeVariables

executable agda2hs-mode
  hs-source-dirs:      src/agda2hs-mode
  main-is:             Main.hs
  other-modules:       Paths_agda2hs
  autogen-modules:     Paths_agda2hs
  build-depends:       base >= 4.10 && < 4.18,
                       Agda >= 2.6.4 && < 2.6.5,
                       bytestring >= 0.11.5 && < 0.12,
                       containers >= 0.6 && < 0.7,
                       unordered-containers >= 0.2.19 && < 0.3,
                       mtl >= 2.2.2 && < 2.3,
                       directory >= 1.2.6.2 && < 1.4,
                       filepath >= 1.4.1.0 && < 1.5,
                       haskell-src-exts >= 1.23 && < 1.25,
                       syb >= 0.7.2 && < 0.8,
                       text >= 2.0.2 && < 2.1,
                       deepseq >= 1.4.4 && < 1.5,
                       yaml-light >= 0.1.4 && < 2.0,
                       process   >= 1.6.3.0  && < 1.7
  default-language:    Haskell2010
  default-extensions:  LambdaCase,
                       RecordWildCards,
                       FlexibleContexts,
                       MultiWayIf,
                       TupleSections,
                       ScopedTypeVariables