#
# ChangeLog for src/utilities
#
# Generated by Trac 1.2
# Jan 24, 2021, 5:09:02 AM

Tue, 30 Aug 2011 14:02:37 GMT mulligan [1145]
	* src/ASM/I8051.ma (modified)
	* src/utilities/Interference.ma (modified)

	changed naming in i8051 of classes of registers to make them
	consistent


Mon, 29 Aug 2011 13:30:40 GMT mulligan [1127]
	* src/ERTL/spill.ma (added)
	* src/ERTL/uses.ma (added)
	* src/utilities/Interference.ma (added)

	interference graphs axiomatised, more added to ertl


Thu, 28 Jul 2011 10:14:37 GMT campbell [1092]
	* src/common/Identifiers.ma (modified)
	* src/utilities/lists.ma (modified)

	Some minor definitions for identifiers and lists.


Mon, 18 Jul 2011 15:21:14 GMT mulligan [1075]
	* src/ASM/I8051.ma (modified)
	* src/ASM/Util.ma (modified)
	* src/RTL/RTLtoERTL.ma (modified)
	* src/utilities/RegisterSet.ma (modified)

	nearly completed rtl -> ertl pass removing all option types with dep. ...


Wed, 13 Jul 2011 15:12:10 GMT mulligan [1066]
	* src/ASM/I8051.ma (modified)
	* src/RTL/RTL.ma (modified)
	* src/RTLabs/RTLAbstoRTL.ma (modified)
	* src/utilities/Compare.ma (modified)

	changes from today


Mon, 04 Jul 2011 13:31:18 GMT mulligan [1052]
	* src/ASM/BitVectorTrie.ma (modified)
	* src/RTLabs/RTLAbstoRTL.ma (modified)
	* src/common/AST.ma (modified)
	* src/utilities/HMap.ma (modified)

	removed offsets after reading cerco mailing list


Mon, 04 Jul 2011 08:43:37 GMT mulligan [1050]
	* src/RTLabs/RTLAbstoRTL.ma (modified)
	* src/utilities/HMap.ma (modified)

	adding dependent types to map datastructure to remove all option ...


Fri, 01 Jul 2011 15:45:46 GMT mulligan [1049]
	* src/RTLabs/RTLAbstoRTL.ma (modified)
	* src/common/Order.ma (added)
	* src/common/Registers.ma (modified)
	* src/utilities/HMap.ma (modified)

	more stuff added


Fri, 01 Jul 2011 15:11:27 GMT mulligan [1048]
	* src/utilities/HMap.ma (added)

	added implementation of haskell associative maps to clean up the mess ...


Wed, 15 Jun 2011 14:15:52 GMT campbell [961]
	* src/ASM/Arithmetic.ma (modified)
	* src/ASM/BitVector.ma (modified)
	* src/ASM/Vector.ma (modified)
	* src/Clight/Cexec.ma (modified)
	* src/Clight/CexecComplete.ma (modified)
	* src/Clight/CexecEquiv.ma (modified)
	* src/Clight/CexecSound.ma (modified)
	* src/Clight/Csem.ma (modified)
	* src/Clight/Csyntax.ma (modified)
	* src/Clight/casts.ma (modified)
	* src/Clight/label.ma (modified)
	* src/Clight/test/memorymodel.ma (modified)
	* src/Clight/test/search.ma (modified)
	* src/Clight/test/sum.ma (modified)
	* src/Clight/toCminor.ma (modified)
	* src/Cminor/initialisation.ma (modified)
	* src/Cminor/semantics.ma (modified)
	* src/Cminor/syntax.ma (modified)
	* src/Cminor/toRTLabs.ma (modified)
	* src/RTLabs/semantics.ma (modified)
	* src/common/AST.ma (modified)
	* src/common/Animation.ma (modified)
	* src/common/Events.ma (modified)
	* src/common/Floats.ma (modified)
	* src/common/FrontEndOps.ma (modified)
	* src/common/Globalenvs.ma (modified)
	* src/common/IO.ma (modified)
	* src/common/Integers.ma (modified)
	* src/common/Values.ma (modified)
	* src/utilities/extranat.ma (modified)

	Use precise bitvector sizes throughout the front end, rather than ...


Tue, 07 Jun 2011 14:53:53 GMT campbell [891]
	* src/ASM/BitVectorZ.ma (modified)
	* src/Clight/Cexec.ma (modified)
	* src/Clight/CexecComplete.ma (modified)
	* src/Clight/CexecEquiv.ma (modified)
	* src/Clight/CexecSound.ma (modified)
	* src/Clight/TypeComparison.ma (modified)
	* src/common/Mem.ma (modified)
	* src/common/Smallstep.ma (modified)
	* src/common/Values.ma (modified)
	* src/utilities/binary/Z.ma (modified)
	* src/utilities/binary/positive.ma (modified)
	* src/utilities/extralib.ma (modified)

	Revise proofs affected by recent matita change.


Fri, 03 Jun 2011 15:35:32 GMT campbell [882]
	* src/Clight/CexecSound.ma (modified)
	* src/Clight/TypeComparison.ma (modified)
	* src/Clight/toCminor.ma (modified)
	* src/RTLabs/import.ma (modified)
	* src/common/AST.ma (modified)
	* src/utilities/extralib.ma (modified)

	Fix up fragile proofs for current version of matita.


Thu, 19 May 2011 13:06:42 GMT campbell [816]
	* src/CHANGES (modified)
	* src/Clight/Csem.ma (modified)
	* src/Clight/Csyntax.ma (modified)
	* src/Clight/test/search.ma (modified)
	* src/Clight/toCminor.ma (added)
	* src/Cminor/cminorMatitaPrinter.ml (modified)
	* src/Cminor/semantics.ma (modified)
	* src/Cminor/syntax.ma (modified)
	* src/Cminor/test/factorial.ma (modified)
	* src/Cminor/test/search.ma (modified)
	* src/Cminor/test/switcher.ma (modified)
	* src/Cminor/toRTLabs.ma (modified)
	* src/RTLabs/RTLabsMatitaPrinter.ml (modified)
	* src/RTLabs/import.ma (modified)
	* src/RTLabs/semantics.ma (modified)
	* src/RTLabs/syntax.ma (modified)
	* src/RTLabs/test/search.ma (modified)
	* src/common/Identifiers.ma (modified)
	* src/utilities/lists.ma (modified)

	Clight to Cminor compilation, modulo switch statements, temporary ...


Thu, 28 Apr 2011 15:36:33 GMT mulligan [782]
	* src/ASM/BitVectorTrie.ma (modified)
	* src/ASM/Util.ma (modified)
	* src/ERTL/ERTL.ma (modified)
	* src/RTL/RTL.ma (modified)
	* src/RTL/RTLtoERTL.ma (modified)
	* src/common/Identifiers.ma (modified)
	* src/utilities/RegisterSet.ma (modified)

	More work on rtl-ertl pass from today, plus resolved conflict.


Thu, 28 Apr 2011 08:55:49 GMT campbell [780]
	* src/Cminor/toRTLabs.ma (modified)
	* src/utilities/lists.ma (modified)

	Properly update set of registers that are used for pointers in Cminor ...


Thu, 28 Apr 2011 08:28:43 GMT mulligan [778]
	* src/utilities/RegisterSet.ma (moved)

	moved register set into correct place


Thu, 21 Apr 2011 17:24:04 GMT campbell [766]
	* src/Cminor/toRTLabs.ma (modified)
	* src/RTLabs/semantics.ma (modified)
	* src/utilities/lists.ma (added)

	Most of the Cminor to RTLabs stage.

	Is buggy, generates inefficient ...


Tue, 19 Apr 2011 10:22:32 GMT campbell [761]
	* src/ASM/BitVectorTrie.ma (modified)
	* src/Cminor/semantics.ma (modified)
	* src/Cminor/test/sum-bad.ma (added)
	* src/RTLabs/RTLabs-sem.ma (modified)
	* src/common/Identifiers.ma (modified)
	* src/utilities/Coqlib.ma (modified)
	* src/utilities/option.ma (added)

	Enforce the use of declared identifiers/registers in Cminor/RTLabs.


Thu, 14 Apr 2011 15:54:37 GMT mulligan [753]
	* src/ERTL/ERTL.ma (modified)
	* src/ERTL/ERTLToLTL.ma (modified)
	* src/LTL/Branch.ma (deleted)
	* src/LTL/LTL.ma (modified)
	* src/LTL/LTLToLIN.ma (modified)
	* src/common/Identifiers.ma (modified)
	* src/utilities/BitVectorTrieSet.ma (modified)

	Work from today.


Fri, 08 Apr 2011 12:06:46 GMT campbell [747]
	* src/Clight/AST.ma (deleted)
	* src/Clight/Csyntax.ma (modified)
	* src/RTLabs/RTLabs-syntax.ma (modified)
	* src/common/AST.ma (modified)
	* src/common/CostLabel.ma (modified)
	* src/common/Globalenvs.ma (modified)
	* src/common/Integers.ma (modified)
	* src/common/Maps.ma (modified)
	* src/common/Values.ma (modified)
	* src/utilities/Coqlib.ma (modified)

	Merge the two AST files together (although some definitions still ...


Fri, 08 Apr 2011 09:51:38 GMT mulligan [746]
	* src/ASM/I8051.ma (modified)
	* src/ASM/Util.ma (modified)
	* src/ERTL/Liveness.ma (modified)
	* src/ERTL/Uses.ma (modified)
	* src/ERTL/VariableSet.ma (added)
	* src/common/Graphs.ma (modified)
	* src/utilities/BitVectorTrieSet.ma (modified)

	Changes to bitvectortrieset: equality on sets.  Added new file for ...


Thu, 07 Apr 2011 16:53:59 GMT campbell [744]
	* src/ASM/Arithmetic.ma (modified)
	* src/ASM/BitVector.ma (modified)
	* src/ASM/Vector.ma (modified)
	* src/Clight/AST.ma (modified)
	* src/Clight/Cexec.ma (modified)
	* src/Clight/CexecSound.ma (modified)
	* src/Clight/Csem.ma (modified)
	* src/Clight/Csyntax.ma (modified)
	* src/RTLabs/RTLabs-sem.ma (modified)
	* src/common/FrontEndOps.ma (modified)
	* src/common/Globalenvs.ma (modified)
	* src/common/Integers.ma (modified)
	* src/common/Mem.ma (modified)
	* src/common/Values.ma (modified)
	* src/utilities/Coqlib.ma (modified)
	* src/utilities/extranat.ma (added)

	Evict Coq-style integers from common/Integers.ma.

	Make more ...


Fri, 01 Apr 2011 16:12:57 GMT mulligan [735]
	* src/ERTL/ERTL.ma (modified)
	* src/ERTL/Liveness.ma (modified)
	* src/utilities/IdentifierTools.ma (modified)

	Changes from today


Fri, 01 Apr 2011 14:09:51 GMT mulligan [733]
	* src/ERTL (added)
	* src/ERTL/Build.ma (added)
	* src/ERTL/ERTL.ma (added)
	* src/ERTL/ERTLToLTL.ma (added)
	* src/ERTL/Liveness.ma (added)
	* src/LIN/JointLTLLIN.ma (added)
	* src/LTL/Branch.ma (added)
	* src/LTL/LTLToLIN.ma (modified)
	* src/LTL/LTLToLINI.ma (deleted)
	* src/utilities/UnionFind.ma (added)

	Fixed partial commit.


Sun, 27 Mar 2011 13:06:13 GMT sacerdot [711]
	* src/utilities/extralib.ma (modified)

	...


Wed, 23 Mar 2011 15:39:01 GMT sacerdot [709]
	* src/utilities/extralib.ma (modified)

	Notations should NOT be redefined. Just add a new interpretation.


Fri, 18 Mar 2011 13:53:25 GMT mulligan [699]
	* src/LIN/LIN.ma (modified)
	* src/LIN/LINToASM.ma (modified)
	* src/common/AST.ma (modified)
	* src/common/CostLabel.ma (modified)
	* src/utilities/IdentifierTools.ma (added)
	* src/utilities/StringTools.ma (deleted)

	More or less finished formalisation of LIN.


Fri, 18 Mar 2011 12:47:53 GMT mulligan [698]
	* src/ASM/ASM.ma (modified)
	* src/ASM/Arithmetic.ma (modified)
	* src/ASM/BitVector.ma (modified)
	* src/ASM/BitVectorTrie.ma (modified)
	* src/ASM/Fetch.ma (modified)
	* src/ASM/I8051.ma (modified)
	* src/ASM/Interpret.ma (modified)
	* src/ASM/Status.ma (modified)
	* src/ASM/String.ma (modified)
	* src/ASM/Util.ma (modified)
	* src/ASM/Vector.ma (modified)
	* src/LIN/LIN.ma (modified)
	* src/LIN/LINToASM.ma (modified)
	* src/common/AST.ma (modified)
	* src/common/CostLabel.ma (modified)
	* src/utilities/BitVectorTrieSet.ma (modified)
	* src/utilities/StringTools.ma (modified)

	Commit with changes to files to get our files to typecheck.


Fri, 18 Mar 2011 12:28:33 GMT campbell [697]
	* src/ASM (modified)
	* src/ASM/Arithmetic.ma (modified)
	* src/ASM/BitVector.ma (modified)
	* src/ASM/BitVectorTrie.ma (modified)
	* src/ASM/BitVectorZ.ma (copied)
	* src/ASM/Char.ma (modified)
	* src/ASM/Util.ma (modified)
	* src/ASM/Vector.ma (modified)
	* src/common/Integers.ma (modified)
	* src/utilities/Coqlib.ma (modified)
	* src/utilities/binary/Z.ma (modified)
	* src/utilities/binary/positive.ma (modified)
	* src/utilities/extralib.ma (modified)
	* src/utilities/oldlib (moved)

	Merge Clight branch of vectors and friends.
	Start making stuff build.


Fri, 18 Mar 2011 11:59:56 GMT campbell [695]
	* src/Clight/depends (deleted)
	* src/Clight/root (deleted)
	* src/RTLabs (moved)
	* src/common/Errors.ma (moved)
	* src/common/Events.ma (moved)
	* src/common/Floats.ma (moved)
	* src/common/FrontEndOps.ma (moved)
	* src/common/Globalenvs.ma (moved)
	* src/common/Graphs.ma (moved)
	* src/common/IOMonad.ma (moved)
	* src/common/Integers.ma (moved)
	* src/common/Maps.ma (moved)
	* src/common/Mem.ma (moved)
	* src/common/Registers.ma (moved)
	* src/common/Smallstep.ma (moved)
	* src/common/SmallstepExec.ma (moved)
	* src/common/Values.ma (moved)
	* src/utilities/Coqlib.ma (moved)
	* src/utilities/binary (moved)
	* src/utilities/extralib.ma (moved)

	Rearrange Clight files a bit - will try to make them work again
	soon...


Fri, 18 Mar 2011 10:36:15 GMT mulligan [691]
	* src/LIN/LINToASM.ma (copied)
	* src/common (copied)
	* src/utilities (copied)

	More movement of files within the repository.


Thu, 10 Feb 2011 14:28:59 GMT mulligan [491]
	* Deliverables/D4.2-4.3/ASM (added)
	* Deliverables/D4.2-4.3/ASM/I8051.ma (added)
	* Deliverables/D4.2-4.3/LIN (added)
	* Deliverables/D4.2-4.3/LIN/LIN.ma (added)
	* Deliverables/D4.2-4.3/LIN/LinToAsm.ma (added)
	* Deliverables/D4.2-4.3/common (added)
	* Deliverables/D4.2-4.3/common/AST.ma (added)
	* Deliverables/D4.2-4.3/common/CostLabel.ma (added)
	* Deliverables/D4.2-4.3/utilities (added)
	* Deliverables/D4.2-4.3/utilities/BitVectorTrieSet.ma (added)
	* Deliverables/D4.2-4.3/utilities/Compare.ma (added)
	* Deliverables/D4.2-4.3/utilities/StringTools.ma (added)

	Initial commit of (part)-formalisation of LIN intermediate language.