cabal-version: 2.2 name: agda2hs version: 0.1.20230328 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. source-repository head type: git location: https://github.com/agda/agda2hs.git flag smuggler2 description: Rewrite sources to cleanup imports, and create explicit exports default: False manual: True common smuggler-options if flag(smuggler2) ghc-options: -fplugin=Smuggler2.Plugin -fplugin-opt=Smuggler2.Plugin:MinimiseImports -fplugin-opt=Smuggler2.Plugin:NoExportProcessing build-depends: smuggler2 >= 0.3 && < 0.4 executable agda2hs import: smuggler-options 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.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.3 && < 2.6.4, containers >= 0.6 && < 0.7, unordered-containers >= 0.2, mtl >= 2.2, directory >= 1.2.6.2 && < 1.4, filepath >= 1.4.1.0 && < 1.5, haskell-src-exts >= 1.23 && < 1.25, syb >= 0.7, text >= 1.2.3.0, deepseq >= 1.4.1.1 default-language: Haskell2010 default-extensions: LambdaCase, RecordWildCards, FlexibleContexts, MultiWayIf, TupleSections, ScopedTypeVariables