#
# ChangeLog for src
#
# Generated by Trac 1.2
# Jan 16, 2021, 10:00:38 AM

Wed, 30 Mar 2011 16:47:35 GMT campbell [726]
	* src/ASM/BitVector.ma (modified)
	* src/ASM/BitVectorTrie.ma (modified)
	* src/ASM/Vector.ma (modified)
	* src/Clight/AST.ma (modified)
	* src/Clight/CexecComplete.ma (modified)
	* src/Clight/test/duff.ma (modified)
	* src/Clight/test/factorial.ma (modified)
	* src/Clight/test/insertsort.ma (modified)
	* src/Clight/test/io.ma (modified)
	* src/Clight/test/io2.ma (modified)
	* src/Clight/test/search.ma (modified)
	* src/RTLabs/import.ma (modified)
	* src/common/Graphs.ma (modified)
	* src/common/Registers.ma (modified)

	Change identifiers to Words in Clight and RTLabs semantics.


Wed, 30 Mar 2011 14:16:08 GMT campbell [725]
	* src/Clight/Cexec.ma (modified)
	* src/Clight/Csem.ma (modified)
	* src/Clight/Csyntax.ma (modified)
	* src/Clight/test/duff.ma (modified)
	* src/Clight/test/factorial.ma (modified)
	* src/Clight/test/insertsort.ma (modified)
	* src/Clight/test/io.ma (modified)
	* src/Clight/test/io2.ma (modified)
	* src/Clight/test/search.ma (modified)
	* src/Clight/test/transform1.ma (modified)

	Do some light manual disambiguation to make Clight examples go ...


Wed, 30 Mar 2011 12:03:05 GMT campbell [724]
	* src/ASM/Arithmetic.ma (modified)
	* src/ASM/BitVector.ma (modified)
	* src/ASM/I8051.ma (modified)

	More tractable version of bitvector_of_nat / nat_of_bitvector.


Wed, 30 Mar 2011 10:34:25 GMT mulligan [723]
	* src/CHANGES (modified)
	* src/LIN/LIN.ma (modified)
	* src/LIN/LINToASM.ma (modified)
	* src/LTL/LTL.ma (modified)
	* src/LTL/LTLToLIN.ma (modified)

	Added dependent type internalising the invariant that LIN function ...


Tue, 29 Mar 2011 16:32:47 GMT mulligan [722]
	* src/ASM/ASM.ma (modified)
	* src/LIN/LIN.ma (modified)
	* src/LIN/LINToASM.ma (modified)
	* src/LTL/LTL.ma (modified)
	* src/LTL/LTLToLIN.ma (modified)
	* src/LTL/LTLToLINI.ma (modified)
	* src/common/AST.ma (modified)

	Committing changes from today.  Several files do not typecheck.


Tue, 29 Mar 2011 16:22:19 GMT mulligan [721]
	* src/CHANGES (added)

	Added diary of changes to project files.


Tue, 29 Mar 2011 16:21:16 GMT campbell [720]
	* src/Clight/Csyntax.ma (modified)
	* src/RTLabs/RTLabs-syntax.ma (modified)
	* src/common/CostLabel.ma (moved)
	* src/common/Events.ma (modified)

	Sort out cost labels.


Tue, 29 Mar 2011 16:17:57 GMT mulligan [719]
	* src/ASM/Assembly.ma (added)

	Added missing assembly file ported to matita.


Tue, 29 Mar 2011 15:54:37 GMT campbell [718]
	* src/Clight/AST.ma (modified)
	* src/Clight/Animation.ma (modified)
	* src/Clight/Cexec.ma (modified)
	* src/Clight/Csyntax.ma (modified)
	* src/RTLabs/RTLabs-sem.ma (modified)
	* src/common/Mem.ma (modified)
	* src/common/Values.ma (modified)

	Add an AST type (i.e., intermediate language type) for pointers.


Tue, 29 Mar 2011 15:54:36 GMT campbell [717]
	* src/Clight/Csem.ma (modified)
	* src/Clight/test/duff.ma (modified)
	* src/Clight/test/factorial.ma (modified)
	* src/Clight/test/funptr.ma (deleted)
	* src/Clight/test/insertsort.ma (added)
	* src/Clight/test/io.c.ma (deleted)
	* src/Clight/test/io.ma (added)
	* src/Clight/test/io2.c.ma (deleted)
	* src/Clight/test/io2.ma (added)
	* src/Clight/test/memorymodel.ma (modified)
	* src/Clight/test/search.c (added)
	* src/Clight/test/search.ma (added)
	* src/Clight/test/transform1.ma (modified)
	* src/Clight/test/trivial.ma (deleted)

	Clean up Clight examples; better temporary definition of multiply.


Tue, 29 Mar 2011 12:29:12 GMT mulligan [716]
	* src/LTL/LTL.ma (modified)
	* src/LTL/LTLToLIN.ma (modified)
	* src/LTL/LTLToLINI.ma (added)

	Finished translating LTL statements to LIN statements.  Need to ...


Tue, 29 Mar 2011 11:49:57 GMT mulligan [715]
	* src/ASM/Util.ma (modified)
	* src/LTL/LTLToLIN.ma (modified)

	Restored rev from Util as it appears that list reversal is not a part ...


Tue, 29 Mar 2011 10:24:45 GMT mulligan [714]
	* src/ASM/ASM.ma (modified)
	* src/LIN/LIN.ma (modified)
	* src/LTL/LTL.ma (modified)
	* src/LTL/LTLToLIN.ma (added)
	* src/common/AST.ma (modified)

	Work on translation from LTL to LIN.


Tue, 29 Mar 2011 09:48:33 GMT mulligan [713]
	* src/LTL (added)
	* src/LTL/LTL.ma (added)

	Commit of initial LTL files.


Mon, 28 Mar 2011 15:40:51 GMT mulligan [712]
	* src/ASM/Arithmetic.ma (modified)
	* src/ASM/Fetch.ma (modified)
	* src/ASM/Interpret.ma (modified)
	* src/ASM/Util.ma (modified)

	Changes to get things to typecheck.


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

	...


Fri, 25 Mar 2011 17:37:49 GMT campbell [710]
	* src/RTLabs/import.ma (added)
	* src/common/Graphs.ma (modified)
	* src/common/Registers.ma (modified)

	Start of way to import RTLabs from prototype compiler.


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.


Wed, 23 Mar 2011 13:28:55 GMT campbell [708]
	* src/Clight/Cexec.ma (modified)
	* src/Clight/CexecComplete.ma (modified)
	* src/Clight/CexecEquiv.ma (modified)
	* src/Clight/CexecSound.ma (modified)

	Use a more normalize-friendly definition of clight_exec to make the ...


Wed, 23 Mar 2011 10:37:24 GMT campbell [707]
	* src/Clight/cerco/ASM.ma (deleted)
	* src/Clight/cerco/Arithmetic.ma (deleted)
	* src/Clight/cerco/BitVector.ma (deleted)
	* src/Clight/cerco/BitVectorTrie.ma (deleted)
	* src/Clight/cerco/BitVectorZ.ma (deleted)
	* src/Clight/cerco/Char.ma (deleted)
	* src/Clight/cerco/Fetch.ma (deleted)
	* src/Clight/cerco/Interpret.ma (deleted)
	* src/Clight/cerco/Status.ma (deleted)
	* src/Clight/cerco/String.ma (deleted)
	* src/Clight/cerco/Util.ma (deleted)
	* src/Clight/cerco/Vector.ma (deleted)

	Remove old branch, which was merged after the move to src.


Wed, 23 Mar 2011 01:24:11 GMT sacerdot [706]
	* src/ASM/Fetch.ma (modified)

	Fixed (reference to basics/pairs was dandling).


Wed, 23 Mar 2011 01:21:47 GMT sacerdot [705]
	* src/ASM/Status.ma (modified)

	Ported to new library (notation).


Wed, 23 Mar 2011 01:19:21 GMT sacerdot [704]
	* src/ASM/Util.ma (modified)

	Minor speedup in one theorem (less automation).


Tue, 22 Mar 2011 16:42:04 GMT sacerdot [703]
	* src/root (modified)

	lib is now the default standard library (after commit 11216 in ...


Mon, 21 Mar 2011 17:27:22 GMT campbell [702]
	* src/Clight/Cexec.ma (modified)
	* src/Clight/CexecEquiv.ma (modified)
	* src/RTLabs/RTLabs-sem.ma (modified)
	* src/RTLabs/RTLabs-syntax.ma (modified)
	* src/common/FrontEndOps.ma (modified)
	* src/common/Graphs.ma (modified)
	* src/common/Registers.ma (modified)
	* src/common/SmallstepExec.ma (modified)

	Refine small-step executable semantics abstraction a little.
	Some ...


Fri, 18 Mar 2011 15:28:26 GMT campbell [700]
	* src/ASM/BitVector.ma (modified)
	* src/ASM/BitVectorZ.ma (modified)
	* src/ASM/Vector.ma (modified)
	* src/Clight/AST.ma (modified)
	* src/Clight/Animation.ma (modified)
	* src/Clight/Cexec.ma (modified)
	* src/Clight/CexecComplete.ma (modified)
	* src/Clight/CexecEquiv.ma (modified)
	* src/Clight/CexecSound.ma (modified)
	* src/Clight/CostLabel.ma (modified)
	* src/Clight/Csem.ma (modified)
	* src/Clight/Csyntax.ma (modified)
	* src/common/Events.ma (modified)
	* src/common/Floats.ma (modified)
	* src/common/Globalenvs.ma (modified)
	* src/common/IOMonad.ma (modified)
	* src/common/Integers.ma (modified)
	* src/common/Maps.ma (modified)
	* src/common/Mem.ma (modified)
	* src/common/Smallstep.ma (modified)
	* src/common/SmallstepExec.ma (modified)
	* src/common/Values.ma (modified)

	Get Clight semantics going again (except for problems CexecEquiv that ...


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 12:01:58 GMT mulligan [696]
	* src/ASM/I8051.ma (added)
	* src/LIN/LIN.ma (modified)
	* src/LIN/LINToASM.ma (modified)
	* src/root (added)

	Added missing I8051 file and completed most of LIN formalisation.


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 11:30:38 GMT campbell [694]
	* src/Clight (moved)

	Start moving Clight into common directory.


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.


Fri, 18 Mar 2011 10:34:13 GMT mulligan [690]
	* src/ASM/ASM.ma (copied)
	* src/ASM/Arithmetic.ma (copied)
	* src/ASM/BitVector.ma (copied)
	* src/ASM/BitVectorTrie.ma (copied)
	* src/ASM/Char.ma (copied)
	* src/ASM/Fetch.ma (copied)
	* src/ASM/Interpret.ma (copied)
	* src/ASM/Status.ma (copied)
	* src/ASM/String.ma (copied)
	* src/ASM/Util.ma (copied)
	* src/ASM/Vector.ma (copied)
	* src/ASM/new-matita-development (deleted)

	Moved new matita files into correct place.


Fri, 18 Mar 2011 10:33:37 GMT mulligan [689]
	* src/ASM/ASM.ma (deleted)
	* src/ASM/Arithmetic.ma (deleted)
	* src/ASM/Assembly.ma (deleted)
	* src/ASM/BitVector.ma (deleted)
	* src/ASM/BitVectorTrie.ma (deleted)
	* src/ASM/Char.ma (deleted)
	* src/ASM/Debug.ma (deleted)
	* src/ASM/DoTest.ma (deleted)
	* src/ASM/Fetch.ma (deleted)
	* src/ASM/Interpret.ma (deleted)
	* src/ASM/Status.ma (deleted)
	* src/ASM/String.ma (deleted)
	* src/ASM/Test.ma (deleted)
	* src/ASM/Util.ma (deleted)
	* src/ASM/Vector.ma (deleted)
	* src/ASM/depends (deleted)
	* src/ASM/root (deleted)

	Got rid of old Matita development files.


Fri, 18 Mar 2011 10:31:32 GMT mulligan [688]
	* Deliverables/D4.1/Demo-March-2011 (deleted)
	* Deliverables/D4.2-4.3/LIN/LinToAsm.ma (deleted)
	* src (added)
	* src/ASM (moved)
	* src/LIN (moved)
	* src/LIN/LIN.ma (copied)

	Fixed local conflicts.  Restructured svn repository.