opentheory-transform - Opentheory proof trace optimizer

Age	Commit message (Collapse)	Author
2012-10-07	Added function to add many graphparts at once	Jed Barber

2012-10-07	Dictionary methods cleaned up, Cost model library added	Jed Barber

2012-10-04	Substitute test updated	Jed Barber

2012-10-04	Alpha equivalence typing fixed	Jed Barber

2012-09-28	Types only tracked in alpha equivalence for bound variables	Jed Barber

2012-09-28	Now shows what the differences between article files are	Jed Barber

2012-09-28	Exposed function to convert machineStates to strings	Jed Barber

2012-09-28	Added function to compute the difference of two stacks	Jed Barber

2012-09-28	Type alpha equivalence in limbo	Jed Barber

2012-09-27	Utility to compare two article files to see if they produce the same results	Jed Barber

2012-09-27	Stack datatype now deriving Eq	Jed Barber

2012-09-27	Placeholder file to ensure git records the /bin directory	Jed Barber

2012-09-27	The rest of the article files for testing specific commands	Jed Barber

2012-09-26	Fixed minor alpha conversion argument ordering bug	Jed Barber

2012-09-24	Compiles properly	Jed Barber

2012-09-24	Allowed output of a graphpart to be used by multiple nodes	Jed Barber

2012-09-22	Added standard AbsTerm and AppTerm datatypes	Jed Barber

2012-09-22	TermNet working properly	Jed Barber

2012-09-22	Added a function to check whether a given type is a type variable	Jed Barber

2012-09-22	Moved some functions from graphpart to proofgraph	Jed Barber

2012-09-14	Misc test files	Jed Barber

2012-09-14	Code complete, but buggy	Jed Barber

2012-09-14	Test article files for specific commands	Jed Barber

2012-09-14	Testing package	Jed Barber

2012-09-13	Cleaner directory structure, addition of make clean, grouping of library ↵	Jed Barber
	modules into a single package
2012-08-23	Not quite finished work on instantiation optimisation	Jed Barber

2012-08-23	Simplified to construct graph fully and check for duplicate nodes afterwards	Jed Barber

2012-08-23	Encapsulates a partial graph with at most one each input/output	Jed Barber

2012-08-23	Functions to convert internal datatypes to (unoptimised) proof trace ↵	Jed Barber
	snippets that generate them
2012-08-09	Fixed getArgs error when compiling with GHC 7+	Jed Barber

2012-08-09	Concat explanation added	Jed Barber

2012-08-09	Instructions on how to use the programs	Jed Barber

2012-08-09	Compilation now automated	Jed Barber

2012-08-09	Theorems now displayed properly instead of as maybe values	Jed Barber

2012-08-02	Moved fst3, snd3, thd3 functions to Parse.hs	Jed Barber

2012-08-02	Converted to module	Jed Barber

2012-08-02	Generates a numbered list of theorems in an article file	Jed Barber

2012-08-02	Removes theorems from article, specified by number	Jed Barber

2012-08-02	Allows concatenation of article files	Jed Barber

2012-08-02	Moved proof trace output formatting function to Parse.hs	Jed Barber

2012-08-02	Bugfixes for multiCommandsSimple	Jed Barber

2012-07-26	Linearisation of multi-output commands (has a few compile errors)	Jed Barber

2012-07-12	Fixed selection of new dictionary indices	Jed Barber

2012-07-12	Functions to linearise a graph into a proof trace (currently include ↵	Jed Barber
	removing unused portions and resolving single-output commands)
2012-07-12	Graph generating functions accessible as a module	Jed Barber

2012-07-05	Fixed bug in not detecting duplicate nodes in the graph	Jed Barber

2012-06-18	Graph generator rewritten to use fgl graphs	Jed Barber

2012-06-17	Switched to fgl graph implementation	Jed Barber

2012-06-14	Changed numbers to be handled specially since they're only used by ↵	Jed Barber
	def/ref/remove
2012-06-14	Removed ID: marking from graph display	Jed Barber