[Initial version of intuitionistic propositional decision procedure. lennart@augustsson.net**20051207130726] [A proper prover lennart@augustsson.net**20051207163748] [Generate a proof term lennart@augustsson.net**20051207163806] [Implement all functions lennart@augustsson.net**20051207191324] [switch target lennart@augustsson.net**20051207191405] [Monadify lennart@augustsson.net**20051207194159] [Add MRoy.hs lennart@augustsson.net**20051207194240] [Use the list monad for proofs. lennart@augustsson.net**20051207205328] [bigger test lennart@augustsson.net**20051207211753] [no debug lennart@augustsson.net**20051207211806] [Fix warnings and clean up lennart@augustsson.net**20051207232313] [More tests lennart@augustsson.net**20051207232339] [Warnings on lennart@augustsson.net**20051207232350] [sync lennart@augustsson.net**20051207233540] [Add clean target lennart@augustsson.net**20051207235151] [Special type for AtomImp lennart@augustsson.net**20051207235217] [Special type for NestImp lennart@augustsson.net**20051208000116] [Make Symbol a new type. lennart@augustsson.net**20051208000311] [Remove warnings. Extend tests lennart@augustsson.net**20051208001724] [Special type for AtomF lennart@augustsson.net**20051208001755] [test reference output lennart@augustsson.net**20051208001806] [Clean up a little. lennart@augustsson.net**20051208002054] [Simple regression test lennart@augustsson.net**20051208002224] [Turn on heuristics. lennart@augustsson.net**20051208081226] [Add test cases lennart@augustsson.net**20051208081407] [Remove formulas with quantifiers. lennart@augustsson.net**20051208081834] [Rename Roy to LJT lennart@augustsson.net**20051208085239] [Add comments, clean up a little, break out exported types. lennart@augustsson.net**20051208090750] [Original code lennart@augustsson.net**20051208092739] [Change pretty printer to LJT syntax. lennart@augustsson.net**20051208092930] [Add an LJT parser. lennart@augustsson.net**20051208100640] [Add tests. lennart@augustsson.net**20051208102310] [Actually do negation. lennart@augustsson.net**20051208102902] [Split into fast and slow tests. lennart@augustsson.net**20051208103003] [Better accounting of test results lennart@augustsson.net**20051208103815] [Add a classical provable function lennart@augustsson.net**20051208113015] [Fix a transcription bug lennart@augustsson.net**20051208113109] [Better debiugging lennart@augustsson.net**20051208113204] [Better showing of symbols lennart@augustsson.net**20051208113238] [A proper top level lennart@augustsson.net**20051208113308] [Remove slow tests lennart@augustsson.net**20051208113457] [Remove junk lennart@augustsson.net**20051208113901] [Some more test targets lennart@augustsson.net**20051208114145] [Use -O2 and add a time target lennart@augustsson.net**20051208115546] [Make various function local to avoid so many arguments. lennart@augustsson.net**20051208130242] [Small cleanup lennart@augustsson.net**20051208130947] [Get rid of cprovable lennart@augustsson.net**20051208132328] [Handle true and false lennart@augustsson.net**20051208143145] [Make a special proof type. lennart@augustsson.net**20051208143201] [Allow profiling. lennart@augustsson.net**20051208143229] [Switch to a monad that also has state. lennart@augustsson.net**20051208150258] [Switch to generating variables with the state. lennart@augustsson.net**20051208150549] [Switch newVar to newSym lennart@augustsson.net**20051208152604] [Label antecedents with terms. Very incomplete. lennart@augustsson.net**20051208153617] [Label atoms with terms. Insert Lam. lennart@augustsson.net**20051208155021] [Insert Pair. lennart@augustsson.net**20051208155232] [More proof terms lennart@augustsson.net**20051208230531] [More proof terms. lennart@augustsson.net**20051209062119] [Make all constants argument free. lennart@augustsson.net**20051209073621] [Comments and some more unimplemented. lennart@augustsson.net**20051209090120] [More proof terms. Only some weird absurdity cases left. lennart@augustsson.net**20051209115955] [Add Haskell printer lennart@augustsson.net**20051209123157] [Reduce proof to normal form. lennart@augustsson.net**20051209123213] [Print Haskell lennart@augustsson.net**20051209123236] [Add some better support for generating Haskell. lennart@augustsson.net**20051209214617] [Implement one more proof object. lennart@augustsson.net**20051210103416] [Update for environment changes. lennart@augustsson.net**20051210103445] [Rename function. lennart@augustsson.net**20051210134431] [Handle one more case. lennart@augustsson.net**20051210134458] [Implement the last proof case ad get rid of Unimplemented. lennart@augustsson.net**20051210135748] [Get rid a bad comment. lennart@augustsson.net**20051210135935] [Simplify absurdity elimination. lennart@augustsson.net**20051210140436] [Start of using a read-eval-print-loop. lennart@augustsson.net**20051210142854] [More repl stuff. lennart@augustsson.net**20051210145302] [Make top level work. lennart@augustsson.net**20051210154901] [Improve top level. lennart@augustsson.net**20051210172459] [Add NL lennart@augustsson.net**20051210172621] [More examples. lennart@augustsson.net**20051210213813] [Change from fst/snd to split. lennart@augustsson.net**20051210213833] [Change binary conjunction to n-ary. This is a better fit for Haskell's tuples. lennart@augustsson.net**20051211100753] [Rename constructors. lennart@augustsson.net**20051211101031] [Change the query syntax. lennart@augustsson.net**20051211103749] [Add a Haskell expression type. lennart@augustsson.net**20051211111445] [Print exception. lennart@augustsson.net**20051211114347] [Use conversion to Haskell types to get nicer output. lennart@augustsson.net**20051211121307] [Replace unused vars by _ in Haskell version. lennart@augustsson.net**20051211134502] [Fix a typo lennart@augustsson.net**20051211141420] [More examples lennart@augustsson.net**20051211141432] [More examples lennart@augustsson.net**20051211141743] [Add :env command lennart@augustsson.net**20051211164115] [More examples lennart@augustsson.net**20051211164138] [Strip comments from files. lennart@augustsson.net**20051211164151] [Rename to djinn and add better version handling. lennart@augustsson.net**20051211200150] [Prepare for verbose help lennart@augustsson.net**20051211201025] [Fix dist target lennart@augustsson.net**20051211201247] [Add verbose help lennart@augustsson.net**20051211210908] [Add type synonyms. lennart@augustsson.net**20051211215024] [Make bindC work again lennart@augustsson.net**20051211215636] [Add usage message lennart@augustsson.net**20051211215649] [More help lennart@augustsson.net**20051211215928] [Add *.old to clean lennart@augustsson.net**20051211220148] [Put Not in the initial environment. lennart@augustsson.net**20051211232911] [More about Void lennart@augustsson.net**20051211233327] [Clean up use of State. Add possibility for multiple solutions. lennart@augustsson.net**20051211234635] [Add another example lennart@augustsson.net**20051211234715] [Do a better job of merging patterns. Use _ in case patterns. lennart@augustsson.net**20051212012903] [Prepare for debug. lennart@augustsson.net**20051212012941] [Allow ambigous command parsing. lennart@augustsson.net**20051212013100] [Add a "set command to set multiple solution switch. lennart@augustsson.net**20051212013741] [Fix a typo. lennart@augustsson.net**20051212013936] [Add a comment. lennart@augustsson.net**20051212014749] [Add things to do. lennart@augustsson.net**20051212014802] [Add "set docs. lennart@augustsson.net**20051212015145] [more to do lennart@augustsson.net**20051212015334] [More help. lennart@augustsson.net**20051212095849] [Parse Haskell symbols more faithfully. lennart@augustsson.net**20051212100404] [Add comments. lennart@augustsson.net**20051212120105] [Add another thing to do. lennart@augustsson.net**20051212120127] [Fix comments. lennart@augustsson.net**20051212121338] [Add URL to Roy's paper. lennart@augustsson.net**20051212121809] [Parse symbols right. lennart@augustsson.net**20051212122529] [Add an example for pretty printing. lennart@augustsson.net**20051212122758] [Pretty print better. lennart@augustsson.net**20051212122813] [Change printing of multiple solutions lennart@augustsson.net**20051212131113] [Update for type change lennart@augustsson.net**20051212131142] [Another example lennart@augustsson.net**20051212131152] [Remove a test that is slow now. lennart@augustsson.net**20051212132655] [Combine the state and list monad the other way around for better speed. lennart@augustsson.net**20051212132708] [Fix typo. lennart@augustsson.net**20051212133745] [Indent less lennart@augustsson.net**20051212141127] [Prepare for generating more solutions. lennart@augustsson.net**20051212141138] [Add some multiple result examples lennart@augustsson.net**20051212141705] [Remove a fast path to generate more solutions. lennart@augustsson.net**20051212141722] [Generate more solutions when +m is set. lennart@augustsson.net**20051212142655] [One item done. lennart@augustsson.net**20051212142819] [Switch to n-ary disjunction. lennart@augustsson.net**20051212190307] [Get rid of some function to print in Haskell notation. lennart@augustsson.net**20051212190534] [Add a flag to sort the solutions according to how many _ are used. Fewer is better. lennart@augustsson.net**20051212194405] [More on option settings. lennart@augustsson.net**20051212195813] [Better option decoding. lennart@augustsson.net**20051212211405] [Better usage message. lennart@augustsson.net**20051212211446] [More tests and a simple target to check them. lennart@augustsson.net**20051212212238] [Some tnings are done. lennart@augustsson.net**20051212212306] [Move utility functions around. lennart@augustsson.net**20051212212839] [Add and subtract. lennart@augustsson.net**20051212215506] [Some space. lennart@augustsson.net**20051212215712] [let :d remove from axioms and synonyms. lennart@augustsson.net**20051213075508] [Add a :clear command lennart@augustsson.net**20051213085402] [Improve symbol parsing. lennart@augustsson.net**20051213101211] [Add a cutoff for sorting. lennart@augustsson.net**20051213130916] [Translate Haskell data types to formulae. lennart@augustsson.net**20051213131019] [Add more examples. lennart@augustsson.net**20051213140312] [Add warning. lennart@augustsson.net**20051213140736] [Get rid of Truth and Falsity lennart@augustsson.net**20051213140816] [Add Void lennart@augustsson.net**20051213141649] [Update documentation. lennart@augustsson.net**20051213141702] [New version. lennart@augustsson.net**20051213141742] [Update docs. lennart@augustsson.net**20051213141938] [Get rid of unused code. lennart@augustsson.net**20051213142622] [Eta reduce Haskell expression. lennart@augustsson.net**20051213190000] [More simplications. lennart@augustsson.net**20051213190030 case e of p -> p same as e case _ of p1 -> e ... pn -> e same as e ] [Update for simplified code. lennart@augustsson.net**20051213190230] [Turn on sorting by default lennart@augustsson.net**20051213190354] [More done. lennart@augustsson.net**20051213190724] [Get rid of HTList lennart@augustsson.net**20051213205118] [Add kind checking and recursive type definition check. lennart@augustsson.net**20051213213059] [Improve messages. lennart@augustsson.net**20051213214149] [Add a NEWS file. lennart@augustsson.net**20051213214715] [Remove obsolete warning. lennart@augustsson.net**20051213214726] [Add utilities lennart@augustsson.net**20051213223726] [Clean better lennart@augustsson.net**20051213234511] [axioms start with lowe case lennart@augustsson.net**20051214004417] [Fix typo lennart@augustsson.net**20051214021820] [Better simplification. lennart@augustsson.net**20051214021832] [More examples lennart@augustsson.net**20051214022038] [non-working simplification lennart@augustsson.net**20051214022300] [Remove double use of void lennart@augustsson.net**20051214022504] [Fix some typos. lennart@augustsson.net**20051214095838] [Make fast path more general, but sill commented out. lennart@augustsson.net**20051214100718] [Make a special case so we don't construct 'void p : Void', but just p. lennart@augustsson.net**20051214102254] [Get ridof Util lennart@augustsson.net**20051214102813] [Put back simplification. lennart@augustsson.net**20051214102835] [Add some negation. lennart@augustsson.net**20051214102901] [Remove Util.hs lennart@augustsson.net**20051214102948] [New date. lennart@augustsson.net**20051214103139] [Add another test that is fast enough. lennart@augustsson.net**20051214104130] [Add a fast path when looking for solutions. Adjust reference output. lennart@augustsson.net**20051214104206] [Parse and print data types with no constructors like ghc. lennart@augustsson.net**20051214104816] [Adding cabal support h.guenther@tu-bs.de**20051214095851 Makes it possible to use cabal for building djinn. Just do: ghc --make Setup.lhs -o setup ./setup configure ./setup build ./setup install ] [Fix a sorting bug when there are no variables. lennart@augustsson.net**20051214105218] [Prefer solutions with fewer variables. lennart@augustsson.net**20051214105317] [More examples lennart@augustsson.net**20051214110835] [Add licensing info. lennart@augustsson.net**20051214111630] [Change a name. lennart@augustsson.net**20051214112404] [More examples lennart@augustsson.net**20051214180619] [Implement alphaEq properly. lennart@augustsson.net**20051214183226] [nub the list of solutions. lennart@augustsson.net**20051214183419] [Add a comment. lennart@augustsson.net**20051214184242] [Update version number and license. lennart@augustsson.net**20051214184631] [Say what's new today. lennart@augustsson.net**20051214184857] [Use liftM instead of fmap for consistency. lennart@augustsson.net**20051214185232] [Collapse tuple patterns with only _ to a single _ lennart@augustsson.net**20051214190915] [Don't use case when pattern is _ lennart@augustsson.net**20051214192152] [Refactor lennart@augustsson.net**20051214192228] [Some half done code lennart@augustsson.net**20051214193244] [Refactor so that the typ environment contains a kind, so far unused. lennart@augustsson.net**20051214195700] [Do kind checking of axiom and goal types. lennart@augustsson.net**20051214201111] [Fix typo lennart@augustsson.net**20051214202610] [Update with stuff from Isaac Jones. lennart@augustsson.net**20051214215254] [Float lambdas out of case. lennart@augustsson.net**20051214231918] [Another example. lennart@augustsson.net**20051214232102] [New version lennart@augustsson.net**20051214232151] [More debug. lennart@augustsson.net**20051214162838] [Make findAtoms return a list instead of in the monad. lennart@augustsson.net**20051215082045] [Add Herbelin's MJ (LJT) calculus. lennart@augustsson.net**20051216184028] [Only use Ax on variables. lennart@augustsson.net**20051217105623] [More debug. lennart@augustsson.net**20051217105901] [Prepare for MJ. lennart@augustsson.net**20051217105932] [Rename variables to make it look nicer. lennart@augustsson.net**20051217112432] [Test more than 26 variables. lennart@augustsson.net**20051217112610] [Print parens around case when needed. lennart@augustsson.net**20051217113535] [Prepare for more transformations lennart@augustsson.net**20051218183958] [Add temporary Xsel. lennart@augustsson.net**20051218184248] [Fix two types so it improves the code better. lennart@augustsson.net**20051218223904] [Convrt Xsel to split by inserting the split at the earliest place possible. lennart@augustsson.net**20051218223935] [Add freeVars. lennart@augustsson.net**20051218224022] [Remove unneeded import. lennart@augustsson.net**20051218224055] [Nub the selectors. lennart@augustsson.net**20051219091802] [Add routines for solving fixed point equations over N+infinity. lennart@augustsson.net**20051219200158] [Finish equation solver. lennart@augustsson.net**20051219213759] [Add function to test for inf. lennart@augustsson.net**20051219214057] [Change isInf to ninfToN. lennart@augustsson.net**20051219225150] [Avoid inserting double splits. lennart@augustsson.net**20051219094813] [Add function to build sequent graph. lennart@augustsson.net**20051219225331] [Strictify data types. lennart@augustsson.net**20051220111313] [Make a conction to construct constant polynomials. lennart@augustsson.net**20051220111337] [Speed up equation solving. lennart@augustsson.net**20051220111414] [Build and solve equation system. Build a pruned graph. lennart@augustsson.net**20051220111429] [Generate solutions from the graph. lennart@augustsson.net**20051220134310] [Rename search to unfld. lennart@augustsson.net**20051220172807] [Use a BFS monad. lennart@augustsson.net**20051220172838] [Import Poly. lennart@augustsson.net**20051219225646] [Make mplus more fair. lennart@augustsson.net**20051219225656] [Use cutOff even when not sorting. lennart@augustsson.net**20051220234355] [Add a monad for breadth first search. Based on Mike Spivey's BFS monads. lennart@augustsson.net**20051220234428] [Switch to BFS monad. lennart@augustsson.net**20051220234504] [Clean up a little lennart@augustsson.net**20051221002110] [Use two-list queues to remove a bottleneck. lennart@augustsson.net**20051221012638] [Fix typo lennart@augustsson.net**20051221014842] [Make a module with some utilities. lennart@augustsson.net**20051221093537] [Make a smart constructor mkS that simplifies polynomials with an infinite coefficient. lennart@augustsson.net**20051221104730] [Add some utility functions. lennart@augustsson.net**20051221105203] [Speed up solving equations. lennart@augustsson.net**20051221105225] [Build a recursive data structure for the unfolder to speed up graph traversal. lennart@augustsson.net**20051221113436] [Rename FSet lennart@augustsson.net**20051221121447] [More debug lennart@augustsson.net**20051221121517] [Make faster variables for equation solution. lennart@augustsson.net**20051221121535] [Small speedup lennart@augustsson.net**20051221121626] [Rename Forest to BFS. lennart@augustsson.net**20051221195234] [Be a little more verbose when loading files. lennart@augustsson.net**20060721123657] [Fix typos. lennart@augustsson.net**20060721123722] [Update with new version. lennart@augustsson.net**20060721123821] [Implement class definitions and contexts in queries. lennart@augustsson.net**20070419232639] [Allow operators for methods. lennart@augustsson.net**20070419234913] [Update version. lennart@augustsson.net**20070419235506] [Optional context in query parsing misc@alpheccar.org**20070504212813] [Use hierarchical imports only (removes haskell98 dep), and untab Don Stewart **20070507004713] [Make it compile again after Dons' change. lennart@augustsson.net**20070507122419] [update .cabal to work with GHC 6.8.2 gwern0@gmail.com**20080111203411] [Tidy-up: mv source files into Djinn/ and avoid clutting top dir gwern0@gmail.com**20080111203647 I'd also like to mention that this could use a Hackage release: the current one lacks enumerated imports (which I added in the preceding patch), and so dies if you try to install under GHC 6.8.x. ] [Freshen up a little. lennart@augustsson.net**20080118193403] [Update Cabal file. lennart@augustsson.net**20080709193636]