name:                  upts
version:               0.1.0
cabal-version:         >= 1.6 && < 2
build-type:            Simple
license:               BSD3
license-file:          LICENSE
category:              Language
author:                Dan Doel
copyright:             (c) Dan Doel, 2008-2009
maintainer:            Dan Doel <dan.doel@gmail.com>
homepage:              http://code.haskell.org/~dolio/
stability:             experimental
synopsis:              An implementation of a pure type system with universe polymorphism.
description:           upts provides several modules for working with a type theory
                       similar to pure type systems. It is based on the pts library
                       by the same author, but rather than being parameterized by the
                       axioms to be used, a specific dependent type theory has been
                       chosen, so that more interesting features can be developed.
                       .
                       The type theory in upts has a predicative hierarchy of universes,
                       Type[i], for each integer i. However, levels are treated as an
                       ordinary type, and can be quantified over using both Pi and Sigma
                       types. This enables universe polymorphism, where a single type
                       definition is able to be used on many levels of the hierarchy. To
                       avoid paradox (hopefully), universe polymorphic types such as:
                          (i : Level) -> Type[i]
                          { i : Level | Type[i] }
                       inhabit a 'top' universe, denoted by a capital omega, which cannot
                       be quantified over. In this manner, it is similar to the lambda
                       cube, which has values, types, * and [] in its hierarchy, the
                       last being the top, and not subject to discussion from within the
                       calculus.
tested-with:           GHC == 6.10.3 && == 6.10.4

source-repository head
  type:                darcs
  location:            http://code.haskell.org/~dolio/upts/

library
  hs-source-dirs:      .
  ghc-options:         -O2 -Wall
  extensions:          ScopedTypeVariables, PatternGuards, MultiParamTypeClasses
  build-depends:       base>=4 && < 5, parsec>=3 && < 4, mtl, bound >= 0.4, containers, prelude-extras
  exposed-modules:     Language.UPTS.SyntaxTree
                       Language.UPTS.TypeCheck
                       Language.UPTS.Parser

executable upts-repl
  main-is:             REPL.hs
  build-depends:       base==4.*, mtl, haskeline > 0.6 && < 1, bound >= 0.4, containers, prelude-extras
  extensions:          Rank2Types, ExistentialQuantification,
                       GeneralizedNewtypeDeriving, PatternGuards
  ghc-options:         -O2 -Wall