name:            Sit
version:         0.2023.8.3
x-revision:      1
build-type:      Simple
cabal-version:   >= 1.10
license:         OtherLicense
license-file:    LICENSE
author:          Andreas Abel <andreas.abel@gu.se>
maintainer:      Andreas Abel <andreas.abel@gu.se>
homepage:        https://github.com/andreasabel/Sit
category:        Dependent types
synopsis:        Prototypical type checker for Type Theory with Sized Natural Numbers
description:
  Sit = Size-irrelevant types
  .
  Sit is a prototypical language with an Agda-compatible syntax.
  It has dependent function types, universes, sized natural numbers,
  and case and recursion over natural numbers.
  There is a relevant and an irrelevant quantifier over sizes.
  For an example, see file test/Test.agda.

tested-with:
                    GHC == 9.10.1
                    GHC == 9.8.2
                    GHC == 9.6.6
                    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

data-files:         test/Makefile
                    test/Base.agda
                    test/Test.agda

extra-source-files: Makefile
                    src/Makefile
                    src/Sit.cf
                    src/undefined.h
                    CHANGELOG.md
                    README.md

source-repository head
  type:     git
  location: https://github.com/andreasabel/Sit

library
  hs-source-dirs:   src

  build-depends:    array >= 0.3 && < 1,
                    base >= 4.7 && < 5,
                    containers >= 0.3 && < 1,
                    data-lens-light >= 0.1.2.2 && < 0.2,
                    mtl >= 2.2.1 && < 3
  build-tools:      alex >= 3.2.2 && < 4
                  , happy >= 1.19.6 && < 3

  default-language: Haskell98

  other-extensions: MultiParamTypeClasses
                    FunctionalDependencies
                    TypeSynonymInstances
                    FlexibleInstances
                    FlexibleContexts
                    GeneralizedNewtypeDeriving
                    LambdaCase
                    TupleSections

  exposed-modules:  Sit

  other-modules:    Abstract
                    Evaluation
                    Impossible
                    Internal
                    Lens
                    Substitute
                    TypeChecker
                    Sit.Abs
                    Sit.Lex
                    Sit.Par
                    Sit.Print

executable Sit.bin

  hs-source-dirs:   main
  main-is:          Main.hs

  build-depends:    base, Sit

  default-language: Haskell98
  ghc-options:      -rtsopts

test-suite system-test
  type:             exitcode-stdio-1.0

  hs-source-dirs:   test
  main-is:          Main.hs

  other-modules:    Paths_Sit

  build-depends:    base, Sit

  default-language: Haskell98