Repository navigation
Expand file tree
/
Copy pathagda2hs.cabal
More file actions
116 lines (111 loc) · 5.27 KB
/
Copy pathagda2hs.cabal
File metadata and controls
116 lines (111 loc) · 5.27 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
cabal-version: 2.4
name: agda2hs
version: 1.5
license: BSD-3-Clause
license-file: LICENSE
author: Ulf Norell, Jesper Cockx, Orestis Melkonian, Sára Juhošová, James Chapman, Lucas Escot, Henry Blanchette, Viktor Csimma, Aleksander Wolska, Paul Bittner, Andreas Källberg, Bohdan Liesnikov, Jakob Naucke, Heinrich Apfelmus, Andreas Abel, and Copilot
maintainer: jesper@sikanda.be
copyright: 2025 Ulf Norell, Jesper Cockx, Orestis Melkonian, Sára Juhošová, James Chapman, Lucas Escot, Henry Blanchette, Viktor Csimma, Aleksander Wolska, Paul Bittner, Andreas Källberg, Bohdan Liesnikov, Jakob Naucke, Heinrich Apfelmus, Andreas Abel, and Copilot
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.
extra-doc-files: CHANGELOG.md
README.md
data-files:
lib/base/base.agda-lib
lib/base/**/*.agda
test/Deprecated/deprecated.agda-lib
test/Deprecated/**/*.agda
test/Deprecated/**/*.hs
test/Fail/fail.agda-lib
test/Succeed/succeed.agda-lib
test/Succeed/*.agda
test/Succeed/*.hs
test/Succeed/**/*.agda
test/Succeed/**/*.hs
test/Fail/*.agda
test/Fail/*.err
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.Exports,
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.Compile.Var,
Agda2Hs.Config,
Agda2Hs.Language.Haskell,
Agda2Hs.Language.Haskell.Pretty,
Agda2Hs.Language.Haskell.Utils,
Agda2Hs.Pragma,
Agda2Hs.Render,
AgdaInternals,
Paths_agda2hs
autogen-modules: Paths_agda2hs
build-depends: base >= 4.13 && < 4.23,
Agda >= 2.8.0 && < 2.9.0,
bytestring >= 0.11.5 && < 0.13,
containers >= 0.6 && < 0.9,
unordered-containers >= 0.2.19 && < 0.3,
mtl (>= 2.2 && < 2.3)
|| (>= 2.3.1 && < 2.4),
transformers >= 0.6 && < 0.7,
monad-control >= 1.0 && < 1.1,
directory >= 1.2.6.2 && < 1.4,
filepath >= 1.4.1.0 && < 1.6,
haskell-src-exts >= 1.23 && < 1.25,
syb >= 0.7.2 && < 0.8,
text >= 2.0.2 && < 2.2,
deepseq >= 1.4.4 && < 1.6,
yaml >= 0.11 && < 0.12,
aeson >= 2.0.3 && < 2.4,
default-language: Haskell2010
default-extensions: LambdaCase
RecordWildCards
FlexibleContexts
MultiWayIf
TupleSections
ScopedTypeVariables
ViewPatterns
NamedFieldPuns
PatternSynonyms
NondecreasingIndentation
OverloadedStrings
ghc-options: -Werror -Werror=unused-imports -rtsopts
test-suite agda2hs-test
type: exitcode-stdio-1.0
hs-source-dirs: test
main-is: Main.hs
build-depends: base >= 4.13 && < 4.23,
bytestring >= 0.11.5 && < 0.13,
directory >= 1.2.6.2 && < 1.4,
filepath >= 1.4.1.0 && < 1.6,
process >= 1.6 && < 1.7,
tasty >= 1.4 && < 1.6,
tasty-golden >= 2.3 && < 2.4,
text >= 2.0.2 && < 2.2,
time >= 1.9 && < 1.17,
default-language: Haskell2010
default-extensions: OverloadedStrings
ScopedTypeVariables
build-tool-depends: agda2hs:agda2hs
ghc-options: -threaded -Werror=unused-imports