ivor-0.1.11: ivor.cabal

Name:		ivor
Version:	0.1.11
Author:		Edwin Brady
License:	BSD3
License-file:	LICENSE
Author:		Edwin Brady
Maintainer:	Edwin Brady <eb@dcs.st-and.ac.uk>
Homepage:	http://www.dcs.st-and.ac.uk/~eb/Ivor/
Stability:      experimental
Build-depends:	base, haskell98, parsec, mtl, directory, containers
Extensions:	MultiParamTypeClasses, FunctionalDependencies,
		ExistentialQuantification, OverlappingInstances
Category:       Theorem provers, Dependent Types
Synopsis:       Theorem proving library based on dependent type theory
Description:    Ivor is a type theory based theorem prover, with a
                Haskell API, designed for easy extending and embedding
                of theorem proving technology in Haskell
                applications. It provides an implementation of the
                type theory and tactics for building terms, more or
                less along the lines of systems such as Coq or Agda,
                and taking much of its inspiration from Conor
                McBride's presentation of OLEG.
                .
                The API provides a collection of primitive tactics and
                combinators for building new tactics. It is therefore
                possible to build new tactics to suit specific
                applications. Ivor features a dependent type theory
                similar to Luo's ECC with definitions (and similar to
                that implemented in Epigram), with dependent pattern
                matching, and experimental multi-stage programming
                support. Optionally, it can be extended with
                heterogeneous equality, primitive types and operations,
                new parser rules, user defined tactics and (if you
                want your proofs to be untrustworthy) a fixpoint
                combinator.

Data-files:     BUGS, INSTALL, TODO, docs/macros.ltx, docs/local.ltx, docs/tt.tex, docs/conclusion.tex,
                docs/intro.tex, docs/hcar.sty, docs/tactics.tex, docs/library.ltx,
                docs/shell.tex, docs/dtp.bib, docs/HCAR.tex, docs/Makefile,
                docs/combinators.tex, docs/humett.tex, docs/interface.tex,
                papers/tutorial/tutorial.tex, papers/tutorial/macros.ltx, papers/tutorial/theoremproving.tex,
                papers/tutorial/introduction.tex, papers/tutorial/hslibrary.tex, papers/tutorial/library.ltx,
                papers/tutorial/programming.tex, papers/tutorial/Makefile, papers/bib/literature.bib,
                papers/ivor/examples.tex, papers/ivor/code.tex, papers/ivor/macros.ltx,
                papers/ivor/ivor.tex, papers/ivor/corett.tex, papers/ivor/conclusions.tex,
                papers/ivor/intro.tex, papers/ivor/llncs.cls, papers/ivor/tactics.tex,
                papers/ivor/library.ltx, papers/ivor/dtp.bib, papers/ivor/alink.bib,
                papers/ivor/Makefile, papers/ivor/embounded.bib

Extra-source-files: emacs/ivor-mode.el, examplett/staged.tt, examplett/test.c, examplett/partial.tt, examplett/nat.tt,
                    examplett/vec.tt, examplett/lt.tt, examplett/Test.hs, examplett/plus.tt,
                    examplett/jmeq.tt, examplett/eq.tt, examplett/logic.tt, examplett/interp.tt,
                    examplett/stageplus.tt, examplett/Nat.hs, examplett/general.tt, examplett/natsimpl.tt,
                    examplett/test.tt, examplett/vect.tt, examplett/fin.tt, examplett/ack.tt,
                    IOvor/IOPrims.lhs, IOvor/Main.lhs, IOvor/iobasics.tt, Jones/Main.lhs,
                    lib/nat.tt, lib/lt.tt, lib/list.tt, lib/eq.tt,
                    lib/basics.tt, lib/logic.tt, lib/vect.tt, lib/fin.tt



Build-depends:  base >=3 && <5, parsec, mtl, directory, binary
Build-type:     Simple

Extensions:     MultiParamTypeClasses, FunctionalDependencies,
                ExistentialQuantification, OverlappingInstances,
                TypeSynonymInstances, PatternGuards
-- Needs some -Wall cleanup
-- GHC-options:    -Wall

Exposed-modules:
		Ivor.TT, Ivor.Shell, Ivor.Primitives,
		Ivor.TermParser, Ivor.ViewTerm, Ivor.Equality,
		Ivor.Plugin, Ivor.Construction
Other-modules:	Ivor.Nobby, Ivor.TTCore, Ivor.State,
		Ivor.Tactics, Ivor.Typecheck, Ivor.Evaluator
		Ivor.Gadgets, Ivor.SC, Ivor.Bytecode, Ivor.Values,
		Ivor.CodegenC, Ivor.Datatype, Ivor.Display,
		Ivor.ICompile, Ivor.MakeData, Ivor.Unify,
		Ivor.Grouper, Ivor.ShellParser, Ivor.Constant,
		Ivor.RunTT, Ivor.Compiler, Ivor.Prefix, Ivor.Errors,
		Ivor.PatternDefs,  Ivor.ShellState, Ivor.Scopecheck