-
Notifications
You must be signed in to change notification settings - Fork 4
/
MiniAgda.cabal
157 lines (144 loc) · 5.35 KB
/
MiniAgda.cabal
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
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
cabal-version: 2.4
-- 2.4 introduces the ** glob patterns used in data-files
name: MiniAgda
version: 0.2022.4.6
build-type: Simple
license: MIT
license-file: LICENSE
author: Andreas Abel and Karl Mehltretter
maintainer: Andreas Abel <[email protected]>
homepage: http://www.cse.chalmers.se/~abela/miniagda/
bug-reports: https:/andreasabel/miniagda/issues
category: Dependent types
synopsis: A toy dependently typed programming language with type-based termination.
description:
MiniAgda is a tiny dependently-typed programming language in the style
of Agda. It serves as a laboratory to test potential additions to the
language and type system of Agda. MiniAgda's termination checker is a
fusion of sized types and size-change termination and supports
coinduction. Equality incorporates eta-expansion at record and
singleton types. Function arguments can be declared as static; such
arguments are discarded during equality checking and compilation.
Recent features include bounded size quantification and destructor
patterns for a more general handling of coinduction.
tested-with:
GHC == 9.4.3
GHC == 9.2.5
GHC == 9.0.2
GHC == 8.10.7
GHC == 8.8.4
GHC == 8.6.5
GHC == 8.4.4
GHC == 8.2.2
GHC == 8.0.2
GHC == 7.10.3
extra-source-files:
CHANGELOG
README.md
Makefile
src/Makefile
stack-9.4.3.yaml
stack-9.2.5.yaml
stack-9.0.2.yaml
stack-8.10.7.yaml
data-files:
test/fail/Makefile
test/succeed/Makefile
test/**/*.ma
test/*.goldplate
test/**/*.golden
test/**/*.err
lib/*.ma
source-repository head
type: git
location: https:/andreasabel/miniagda
library
hs-source-dirs: src
build-depends: array >= 0.3 && < 0.6
, base >= 4.8 && < 5
, containers >= 0.3 && < 0.7
, haskell-src-exts >= 1.21 && < 1.22
-- haskell-src-exts is a nervous package with incompatibilities
-- in every new version, thus, we need tight bounds.
, mtl >= 2.2.1 && < 2.4
, optparse-applicative
>= 0.16.0.0 && < 1
-- optparse-applicative-0.16.0.0 adds some1
, pretty >= 1.0 && < 1.2
, string-qq
, transformers
if impl(ghc < 8)
build-depends: semigroups >= 0.5 && < 1
-- semigroups-0.5 adds Data.List.NonEmpty
build-tool-depends: happy:happy >= 1.15 && < 2
, alex:alex >= 3.0 && < 4
default-language: Haskell98
default-extensions: CPP
MultiParamTypeClasses
TypeSynonymInstances
FlexibleInstances
FlexibleContexts
GeneralizedNewtypeDeriving
NoMonomorphismRestriction
PatternGuards
TupleSections
NamedFieldPuns
LambdaCase
exposed-modules: Abstract
Collection
Concrete
Eval
Extract
HsSyntax
Lexer
License
MainLib
Options
Parser
Polarity
PrettyTCM
ScopeChecker
Semiring
SparseMatrix
TCM
Termination
ToHaskell
TraceError
TreeShapedOrder
TypeChecker
Util
Value
Version
Warshall
other-modules: Paths_MiniAgda
autogen-modules: Paths_MiniAgda
ghc-options: -Wall
-fno-warn-type-defaults
-fno-warn-dodgy-imports
-fno-warn-unused-binds
-fno-warn-unused-matches
-fno-warn-name-shadowing
-fno-warn-incomplete-patterns
if impl(ghc >= 8.0)
ghc-options: -Wcompat
if impl(ghc >= 9.2)
ghc-options: -Wno-incomplete-uni-patterns
-Wno-incomplete-record-updates
executable miniagda
hs-source-dirs: main
main-is: Main.hs
build-depends: MiniAgda
default-language: Haskell2010
test-suite test
type: exitcode-stdio-1.0
hs-source-dirs: test
main-is: GoldplateTests.hs
default-language: Haskell2010
ghc-options: -threaded
build-depends: base >= 4.11
-- goldplate requires ghc >= 8.4
, process
build-tool-depends: goldplate:goldplate >= 0.2
-- goldplate-0.2.0 adds "working_directory"
, MiniAgda:miniagda
-- We also need to depend on ourselves since goldplate calls us.