cabal-version:   2.4
  -- 2.4 introduces the ** glob patterns used in data-files
name:            MiniAgda
version:         0.2025.7.23
build-type:      Simple
license:         MIT
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 == 9.12.2
  GHC == 9.10.2
  GHC == 9.8.4
  GHC == 9.6.7
  GHC == 9.4.8
  GHC == 9.2.8
  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

extra-doc-files:
  CHANGELOG
  README.md

extra-source-files:
  Makefile
  src/Makefile
  stack-9.12.yaml
  stack-9.10.yaml
  stack-9.8.yaml
  stack-9.6.yaml
  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://github.com/andreasabel/miniagda

library
  hs-source-dirs:       src
  build-depends:        array             >= 0.3    && < 0.6
                      , base              >= 4.9    && < 5
                      , containers        >= 0.3    && < 1
                      , 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

  build-tool-depends:   happy:happy       >= 1.15   && < 3
                      , 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
                        -Wcompat
                        -Wno-type-defaults
                        -Wno-dodgy-imports
                        -Wno-unused-binds
                        -Wno-unused-matches
                        -Wno-name-shadowing
                        -Wno-incomplete-patterns

  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 && < 5
                          -- 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.