name:            Sit
version:         0.2023.1.14
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:        NONE
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 == 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.4
                    GHC == 8.10.7
                    GHC == 9.0.2
                    GHC == 9.2.5
                    GHC == 9.4.4

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

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

source-repository head
  type:     git
  location: NONE

executable Sit.bin
  ghc-options:      -rtsopts
  hs-source-dirs:   src

  build-depends:    array >= 0.3 && < 1.0,
                    base >= 4.2 && < 5.0,
                    containers >= 0.3 && < 1.0,
                    data-lens-light >= 0.1.2.2 && < 0.2,
                    mtl >= 2.2.1 && < 3.0

--  -- The lexer and parser are shipped as .hs files, thus, no tools necessary.
--  build-tools:      happy >= 1.15 && < 2,
--                    alex >= 3.0 && < 4

  default-language: Haskell2010
  default-extensions:
                    MultiParamTypeClasses
                    FunctionalDependencies
                    TypeSynonymInstances
                    FlexibleInstances
                    FlexibleContexts
                    GeneralizedNewtypeDeriving
                    LambdaCase
                    TupleSections

  main-is:          Sit.hs

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