| Line No. | Rev | Author | Line |
|---|---|---|---|
| 1 | 1 | paulosilva | |
| 2 | Version: 0.0.1 | ||
| 3 | Stability: experimental | ||
| 4 | License: LGPL | ||
| 5 | License-file: LICENSE | ||
| 6 | Copyright: (c) Paulo Silva | ||
| 7 | Cabal-Version: >= 1.2 | ||
| 8 | Author: Paulo Silva | ||
| 9 | Maintainer: paufil@di.uminho.pt | ||
| 10 | Homepage: http://wiki.di.uminho.pt/twiki/bin/view/Main/PauloSilva | ||
| 11 | |||
| 12 | |||
| 13 | Description: The Galculator is a prototype of a proof assistant based on | ||
| 14 | the algebra of Galois connections. When combined with the | ||
| 15 | pointfree transform and tactics such as the indirect | ||
| 16 | equality principle, Galois connections offer a very | ||
| 17 | powerful, generic device to tackle the complexity of proofs. | ||
| 18 | Category: Proof assistants | ||
| 19 | |||
| 20 | |||
| 21 | Extra-source-files: AUTHORS, | ||
| 22 | INSTALL, | ||
| 23 | README, | ||
| 24 | TODO, | ||
| 25 | src/Language/R/Syntax.hs-boot | ||
| 26 | src/Language/Type/Syntax.hs-boot | ||
| 27 | |||
| 28 | |||
| 29 | Build-Depends: base, | ||
| 30 | array, | ||
| 31 | containers, | ||
| 32 | old-locale, | ||
| 33 | old-time, | ||
| 34 | filepath, | ||
| 35 | directory, | ||
| 36 | process, | ||
| 37 | readline, | ||
| 38 | parsec, | ||
| 39 | mtl | ||
| 40 | Main-is: Galculator.hs | ||
| 41 | Hs-source-dirs: src | ||
| 42 | Extensions: | ||
| 43 | EmptyDataDecls, | ||
| 44 | ExistentialQuantification, | ||
| 45 | FlexibleContexts, | ||
| 46 | FlexibleInstances, | ||
| 47 | FunctionalDependencies, | ||
| 48 | GADTs, | ||
| 49 | MultiParamTypeClasses, | ||
| 50 | PatternSignatures, | ||
| 51 | Rank2Types, | ||
| 52 | TypeOperators, | ||
| 53 | TypeSynonymInstances | ||
| 54 | Ghc-options: -Wall | ||
| 55 | Other-modules: | ||
| 56 | Control.GalcError | ||
| 57 | Control.MonadOr | ||
| 58 | Control.MonadPosition | ||
| 59 | Control.Monad.Fresh | ||
| 60 | Data.Env | ||
| 61 | Data.Equal | ||
| 62 | Data.Existential | ||
| 63 | Data.Stream | ||
| 64 | Galculator.Engine.GcToLaw | ||
| 65 | Galculator.Engine.LawToRule | ||
| 66 | Galculator.Evaluate | ||
| 67 | Galculator.Interpreter | ||
| 68 | Galculator.Proof | ||
| 69 | 7 | paulosilva | Galculator.Rule |
| 70 | 1 | paulosilva | Galculator.RunCommand |
| 71 | Galculator.State | ||
| 72 | Galculator.StepEval | ||
| 73 | 7 | paulosilva | Language.Combinator.Parser |
| 74 | 1 | paulosilva | Language.Combinator.Syntax |
| 75 | Language.Command.Parser | ||
| 76 | Language.Command.Syntax | ||
| 77 | Language.Derivation.Parser | ||
| 78 | Language.Derivation.Syntax | ||
| 79 | Language.Law.Parser | ||
| 80 | Language.Law.Refresh | ||
| 81 | Language.Law.Syntax | ||
| 82 | Language.Law.SyntaxADT | ||
| 83 | Language.Law.TypeInference | ||
| 84 | Language.Law.Verify | ||
| 85 | Language.Module.Parser | ||
| 86 | Language.Module.Refresh | ||
| 87 | Language.Module.Syntax | ||
| 88 | Language.Module.SyntaxADT | ||
| 89 | Language.Module.TypeInference | ||
| 90 | Language.Module.Verify | ||
| 91 | Language.R.Constraint | ||
| 92 | Language.R.Equality | ||
| 93 | Language.R.Match | ||
| 94 | Language.R.Parser | ||
| 95 | Language.R.Pretty | ||
| 96 | Language.R.Refresh | ||
| 97 | Language.R.Rewrite | ||
| 98 | Language.R.SafeCast | ||
| 99 | Language.R.Spine | ||
| 100 | Language.R.Syntax | ||
| 101 | Language.R.SyntaxADT | ||
| 102 | Language.R.TypeInference | ||
| 103 | Language.R.Verify | ||
| 104 | Language.Step.Parser | ||
| 105 | 7 | paulosilva | Language.Step.Syntax |
| 106 | Language.Type.Constraint | ||
| 107 | 1 | paulosilva | Language.Type.Equality |
| 108 | Language.Type.Parser | ||
| 109 | Language.Type.Pretty | ||
| 110 | Language.Type.Rewrite | ||
| 111 | Language.Type.Syntax | ||
| 112 | Language.Type.Unification | ||
| 113 | Language.Type.Utils | ||
| 114 |