djinn 2011.7.23 → 2014.9.7
raw patch · 3 files changed
+60/−47 lines, 3 filesdep ~base
Dependency ranges changed: base
Files
- LICENSE +25/−27
- djinn.cabal +26/−20
- src/LJT.hs +9/−0
LICENSE view
@@ -1,32 +1,30 @@-Copyright (c) 2005 Lennart Augustsson, Thomas Johnsson- Chalmers University of Technology+Copyright (c) 2005-2014, Lennart Augustsson All rights reserved. -This code is derived from software written by Lennart Augustsson-(lennart@augustsson.net).- Redistribution and use in source and binary forms, with or without-modification, are permitted provided that the following conditions-are met:-1. Redistributions of source code must retain the above copyright- notice, this list of conditions and the following disclaimer.-2. Redistributions in binary form must reproduce the above copyright- notice, this list of conditions and the following disclaimer in the- documentation and/or other materials provided with the distribution.-3. None of the names of the copyright holders may be used to endorse- or promote products derived from this software without specific- prior written permission.+modification, are permitted provided that the following conditions are+met: -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS ``AS IS'' AND ANY-EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE-IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR-PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDERS BE-LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR-CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF-SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR-BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY,-WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE-OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN-IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.+ * Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer. -*** End of disclaimer. ***+ * Redistributions in binary form must reproduce the above+ copyright notice, this list of conditions and the following+ disclaimer in the documentation and/or other materials provided+ with the distribution.++ * Neither the name of Lennart Augustsson nor the names of other+ contributors may be used to endorse or promote products derived+ from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
djinn.cabal view
@@ -1,22 +1,28 @@-Name: djinn-Version: 2011.7.23-License: BSD3-License-file: LICENSE-Author: Lennart Augustsson-Maintainer: lennart@augustsson.net-Description: Djinn uses an theorem prover for intuitionistic propositional logic- to generate a Haskell expression when given a type.-Category: source-tools-Homepage: http://www.augustsson.net/Darcs/Djinn/-Synopsis: Generate Haskell code from a type-Build-type: Simple-Build-Depends: base >= 4 && < 5, mtl, haskeline -any, pretty, array, containers+Name: djinn+Version: 2014.9.7+Synopsis: Generate Haskell code from a type+Description: Djinn uses an theorem prover for intuitionistic propositional logic+ to generate a Haskell expression when given a type.+Bug-reports: https://github.com/haskell/augustss/djinn/issues+License: BSD3+License-File: LICENSE+Author: Lennart Augustsson+Maintainer: Lennart Augustsson+Copyright: 2014 Lennart Augustsson+Category: source-tools+Build-type: Simple+Cabal-Version: >= 1.8+Stability: experimental -Executable: djinn-Main-Is: Djinn.hs-Hs-Source-Dirs: src-Other-modules: Help, HCheck, LJT, HTypes, LJTFormula, REPL+source-repository head+ type: git+ location: https://github.com/augustss/djinn -ghc-options: -O2 -Wall -optl-Wl---ghc-options: -Wall -optl-Wl-ghc-prof-options: -prof -auto-all+executable djinn+ Main-Is: Djinn.hs++ Build-Depends: base >= 4 && < 6, mtl, haskeline -any, pretty, array, containers++ Other-modules: Help, HCheck, LJT, HTypes, LJTFormula, REPL++ Hs-Source-Dirs: src
src/LJT.hs view
@@ -20,6 +20,7 @@ module LJT (module LJTFormula, provable, prove, Proof) where +import Control.Applicative(Applicative(..), Alternative(empty, (<|>))) import Control.Monad import Data.List (partition) import Debug.Trace@@ -138,6 +139,10 @@ -- results. But this is much better for backtracking. newtype P a = P { unP :: PS -> [(PS, a)] } +instance Applicative P where+ pure = return+ (<*>) = ap+ instance Monad P where return x = P $ \ s -> [(s, x)] P m >>= f = P $ \ s ->@@ -146,6 +151,10 @@ instance Functor P where fmap f (P m) = P $ \ s -> [ (s', f x) | (s', x) <- m s ]++instance Alternative P where+ empty = mzero+ (<|>) = mplus instance MonadPlus P where mzero = P $ \ _s -> []