MiniAgda-0.2019.12.13: MiniAgda.cabal
name: MiniAgda
version: 0.2019.12.13
build-type: Simple
cabal-version: 1.24
license: OtherLicense
license-file: LICENSE
author: Andreas Abel and Karl Mehltretter
maintainer: Andreas Abel <andreas.abel@cse.gu.se>
homepage: http://www.cse.chalmers.se/~abela/miniagda/
bug-reports: https://github.com/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 == 7.6.3
GHC == 7.8.4
GHC == 7.10.3
GHC == 8.0.2
GHC == 8.2.2
GHC == 8.4.4
GHC == 8.6.5
GHC == 8.8.1
extra-source-files: Makefile
CHANGELOG
README.md
data-files: test/succeed/Makefile
test/succeed/*.ma
test/fail/Makefile
test/fail/*.ma
test/fail/*.err
test/fail/adm/*.ma
test/fail/adm/*.err
lib/*.ma
source-repository head
type: git
location: https://github.com/andreasabel/miniagda
executable miniagda
hs-source-dirs: src
build-depends: array >= 0.3 && < 0.6,
base >= 4.6 && < 5,
containers >= 0.3 && < 0.7,
haskell-src-exts >= 1.21 && < 1.22,
mtl >= 2.2.2 && < 2.3,
pretty >= 1.0 && < 1.2
-- haskell-src-exts is a nervous package with incompatibilities
-- in every new version, thus, we need tight bounds.
build-tools: happy >= 1.15 && < 2,
alex >= 3.0 && < 4
default-language: Haskell98
default-extensions: CPP
MultiParamTypeClasses
TypeSynonymInstances
FlexibleInstances
FlexibleContexts
GeneralizedNewtypeDeriving
NoMonomorphismRestriction
PatternGuards
TupleSections
NamedFieldPuns
main-is: Main.hs
other-modules: Abstract
Collection
Concrete
Eval
Extract
HsSyntax
Lexer
Parser
Polarity
PrettyTCM
ScopeChecker
Semiring
SparseMatrix
TCM
Termination
ToHaskell
Tokens
TraceError
TreeShapedOrder
TypeChecker
Util
Value
Warshall