name:           dedukti
version:        1.0.2
author:         Mathieu Boespflug
maintainer:     Mathieu Boespflug <mboes@lix.polytechnique.fr>
copyright:      © 2009 CNRS - École Polytechnique - INRIA
homepage:       http://www.lix.polytechnique.fr/~mboes/src/dedukti.git
synopsis:       A type-checker for the λΠ-modulo calculus.
description:
    Dedukti is a proof checker for the λΠ-modulo calculus, a
    dependently typed λ-calculus with the addition of typed rewrite
    rules, capable of expressing proofs in Deduction Modulo [1].
    .
    [1] G. Dowek, Th. Hardin, C. Kirchner, Theorem proving modulo,
    /Journal of Automated Reasoning/, 31, 2003, pp. 33-72.
category:       Theorem Provers, Compilers/Interpreters
license:        GPL
license-file:   COPYING
cabal-version:  >= 1.6.0
build-type:     Simple
tested-with:    GHC ==6.10
data-files:     t/bug.dk
                t/coc.dk
                t/coq/Datatypes.dk
                t/delta1.dk
                t/delta2.dk
                t/exemple.dk
                t/f.dk
                t/fold/arith.dk
                t/logic.dk
                t/nat.dk
                t/peano.dk
                t/plus.dk
extra-source-files:   doc/mkfile
                      doc/manual.texi.in
                      doc/fdl.texi
                      doc/references.texi
		      scripts/dkrun


executable dedukti
  main-is:             Dedukti.hs
  other-modules:       Dedukti.Core,
                       Dedukti.Parser,
                       Dedukti.Pretty,
                       Dedukti.Driver.Interactive,
                       Dedukti.Driver.Batch,
                       Dedukti.Driver.Compile,
                       Dedukti.Rule,
                       Dedukti.DkM,
                       Dedukti.Config,
                       Dedukti.Module,
                       Dedukti.CodeGen
                       Dedukti.CodeGen.Exts,
                       Dedukti.Analysis.Rule,
                       Dedukti.Analysis.Scope,
                       Dedukti.Analysis.Dependency

  build-depends:       base >= 4 && < 5, mtl >= 1.1, containers >= 0.2,
                       directory, filepath, process,
                       parsec >= 3.0.0, wl-pprint >= 1.0, bytestring >= 0.9.1.0,
                       haskell-src-exts >= 1.1.0, Stream >= 0.3, text >= 0.3,
                       hmk >= 0.9
  extensions:          EmptyDataDecls, PatternGuards, GeneralizedNewtypeDeriving
                       DeriveDataTypeable, TypeFamilies, LiberalTypeSynonyms,
                       FlexibleInstances, FlexibleContexts, OverloadedStrings,
                       RecordWildCards, TypeSynonymInstances, ScopedTypeVariables
                       MultiParamTypeClasses
  ghc-options:         -fwarn-unused-binds -fwarn-unused-imports

library
  exposed-modules:     Dedukti.Runtime
  build-depends:       time >= 1.1
  extensions:          DeriveDataTypeable, PatternGuards, FlexibleInstances
  ghc-options:         -fwarn-unused-binds -fwarn-unused-imports