agda2hs-1.0: agda2hs.cabal
cabal-version: 2.2
name: agda2hs
version: 1.0
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
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.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